Changeset 2152 for src/ASM/PolicyFront.ma
 Timestamp:
 Jul 4, 2012, 1:23:00 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2141 r2152 400 400 match policy with 401 401 [ None ⇒ True 402  Some p ⇒ And (And (And (And (And (And 403 (out_of_program_none (pi1 ?? program) p) 404 (not_jump_default (pi1 ?? program) p)) 402  Some p ⇒ And (And (And (And (And 403 (not_jump_default (pi1 ?? program) p) 405 404 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) 406 405 (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉))) … … 412 411 λprogram.λlabels. 413 412 let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction) 414 (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And 415 (out_of_program_none prefix policy) 416 (not_jump_default prefix policy)) 413 (λprefix.Σpolicy:ppc_pc_map.And (And (And (And 414 (not_jump_default prefix policy) 417 415 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 418 416 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉))) … … 434 432  lapply p p generalize in match (foldl_strong ?????); * #p #Hp #hg 435 433 @conj [ @Hp  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ] 436  @conj [ @conj [ @conj [ @conj [@conj434  @conj [ @conj [ @conj [ @conj (*[@conj 437 435 [ (* out_of_program_none *) 438 436 #i #Hi2 >append_length <commutative_plus @conj … … 482 480 ] 483 481 ] 484  (* not_jump_default *) cases p p #p cases p p #pc #sigma #Hp 482  *) 483 [ (* not_jump_default *) cases p p #p cases p p #pc #sigma #Hp 485 484 cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi 486 485 normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 487 486 [ >lookup_insert_miss 488 487 [ (* USE[pass]: not_jump_default *) 489 lapply ( (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi)488 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi) 490 489 >nth_append_first 491 490 [ #H #H2 @H @H2 … … 511 510 ] 512 511 ] 513 ]514 512  (* 0 ↦ 0 *) 515 513 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 516 514 >lookup_insert_miss 517 515 [ (* USE[pass]: 0 ↦ 0 *) 518 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) 516 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) 519 517  @bitvector_of_nat_abs 520 518 [ / by / … … 596 594 ] 597 595 ] 598  @conj [ @conj [ @conj [ @conj [ @conj596  @conj [ @conj [ @conj [ @conj (*[ @conj 599 597 [ #i cases i 600 598 [ #Hi2 @conj … … 613 611  #_ @le_S_S @le_O_n 614 612 ] 615 ] 616 #i cases i613 ] *) 614 [ #i cases i 617 615 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 618 616  i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O 619 617 ] 620 ] ] ]618 ] ] 621 619 >lookup_insert_hit @refl 622 620  #i cases i … … 862 860 ] 863 861 qed. 862 863 lemma instruction_size_irrelevant: ∀i. 864 ¬is_jump i → ∀j1,j2.instruction_size_jmplen j1 i = instruction_size_jmplen j2 i. 865 #i cases i 866 [2,3,6: #x [3: #y] #Hj #j1 #j2 % 867 4,5: #x #Hi cases Hi #abs @⊥ @abs @I 868 1: #pi cases pi 869 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 870 [1,2,3,6,7,24,25: #x #y 871 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 872 #Hj #j1 #j2 % 873 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x 3,4,5,8,9: #y #x] 874 #Hi cases Hi #abs @⊥ @abs @I 875 ] 876 ] 877 qed.
Note: See TracChangeset
for help on using the changeset viewer.