Changeset 2152
- Timestamp:
- Jul 4, 2012, 1:23:00 PM (7 years ago)
- Location:
- src/ASM
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Policy.ma
r2141 r2152 12 12 [ None ⇒ True 13 13 | Some x ⇒ 14 And (And (And (And (And 15 (out_of_program_none program x) 16 (not_jump_default program x)) 14 And (And (And (And 15 (not_jump_default program x) 17 16 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0)) 18 17 (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd x) 〈0,short_jump〉))) 19 ( \fst x < 2^16))20 ( no_ch = true → sigma_compact program (create_label_map program) x)18 (sigma_compact_unsafe program (create_label_map program) x)) 19 (\fst x < 2^16) 21 20 ]) ≝ 22 21 let labels ≝ create_label_map program in … … 34 33 #x cases x -x 35 34 [ #H / by I/ 36 | #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj 37 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 38 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 39 ] 40 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 35 | #sigma normalize nodelta #H @conj [ @conj 36 [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) 37 | (* #Ht destruct (Ht) *) @(proj2 ?? (proj1 ?? (proj1 ?? H))) 41 38 ] 42 39 | @(proj2 ?? H) 43 ]44 | #H destruct (H)45 40 ] 46 41 ] … … 51 46 #x cases x -x #ch2 #z2 cases z2 normalize nodelta 52 47 [ #_ / by I/ 53 | #j2 #H2 @conj [ @conj [ @conj [ @conj 54 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))) 55 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))) 56 ] 57 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))) 58 ] 48 | #j2 #H2 @conj [ @conj 49 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))) 50 | (*#Ht @(equal_compact_unsafe_compact ?? op) 51 [ @(proj2 ?? (proj1 ?? H2)) @Ht 52 | cases daemon (* add sigma_safe to properties *) 53 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))) 54 ]*) 55 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))) 56 ] 59 57 | @(proj2 ?? H2) 60 58 ] 61 | #Ht @(equal_compact_unsafe_compact ?? op)62 [ @(proj2 ?? (proj1 ?? (proj1 ?? H2))) @Ht63 | cases daemon (* add to invvariants *)64 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))65 ]66 ]67 59 ] 68 60 ] … … 71 63 [ #_ >p2 #ABS destruct (ABS) 72 64 | #map >p2 normalize nodelta 73 #H #eq destruct (eq) cases daemon (* change order *)65 #H #eq destruct (eq) @H 74 66 ] 75 67 ] … … 396 388 match p with 397 389 [ None ⇒ True 398 | Some pol ⇒ And ( And (out_of_program_none program pol)399 (sigma_compact program (create_label_map program) pol) )390 | Some pol ⇒ And (*And (out_of_program_none program pol)*) 391 (sigma_compact program (create_label_map program) pol) 400 392 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0) 401 393 ]. … … 419 411 [ #H #Feq whd in match policy_equal_opt; normalize nodelta #ABS destruct (ABS) 420 412 | -Fo #Fp #HFp #Feq whd in match policy_equal_opt; normalize nodelta #Heq 421 @conj [ @conj 422 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))) 423 | @(proj2 ?? HGp) whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*80s*) 413 @conj 414 [ @(equal_compact_unsafe_compact ?? Fp) 415 [ cases daemon 416 | cases daemon 417 | @(proj2 ?? (proj1 ?? HGp)) 418 ] 419 (*| @(proj2 ?? HGp) whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*80s*) 424 420 >Feq in Geq; cases Fno_ch in HFp Feq; normalize nodelta #HFp #Feq #Geq 425 421 [ destruct (Geq) / by / … … 436 432 ] 437 433 ] 434 ]*) 435 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) 438 436 ] 439 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))440 ]441 437 ] 442 438 ] … … 525 521 >Feq normalize nodelta cases Fno_ch in HFp Feq; #HFp #Feq 526 522 normalize nodelta 527 [ @conj [ @conj 528 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))) 529 | @((proj2 ?? HFp) (refl ? true)) ] 523 [ @conj 524 [ cases daemon (* XXX *) 530 525 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) 531 526 ] 532 527 | cases (jump_expansion_step ???); #z cases z -z #stch #sto cases sto 533 528 [ #_ / by I/ 534 | -sto #stp normalize nodelta #Hstp @conj [ @conj 535 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))))) 536 | @(equal_compact_unsafe_compact ?? Fp) 537 [ @(proj2 ?? (proj1 ?? (proj1 ?? Hstp))) @(proj2 ?? (proj1 ?? Hstp)) 529 | -sto #stp normalize nodelta #Hstp @conj 530 [ @(equal_compact_unsafe_compact ?? Fp) 531 [ @(proj2 ?? (proj1 ?? Hstp)) @(proj2 ?? (proj1 ?? (proj1 ?? Hstp))) 538 532 #i #Hi 539 533 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) … … 548 542 |3: #_ @refl 549 543 ] 550 | #Hj >(proj 2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))) i Hi Hj)551 >(proj 2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl544 | #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))) i Hi Hj) 545 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl 552 546 ] 553 547 | cases daemon 554 548 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))) 555 549 ] 550 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))) 556 551 ] 557 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))) ]558 552 ] 559 553 ] … … 583 577 (*CSC: modified to really use the specification in Assembly.ma.*) 584 578 definition jump_expansion': 585 ∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16 ).579 ∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l). 586 580 option (Σsigma_policy:(Word → Word) × (Word → bool). 587 581 let 〈sigma,policy〉≝ sigma_policy in … … 604 598 [ lapply (proj2 ?? Hfpol) cases (bvt_lookup ??? fpol 〈0,short_jump〉) 605 599 #x #y #Hx normalize nodelta >Hx / by refl/ 606 | #ppc #ppc_ok @conj 600 | cases daemon (* leaving this until stabilisation of sigma predicate *) 601 (*#ppc #ppc_ok normalize nodelta @conj 607 602 [ #Hppc lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector 16 ppc) ppc_ok) 608 603 >bitvector_of_nat_inverse_nat_of_bitvector … … 651 646 ] 652 647 ] 653 ] 648 ] 654 649 | cases daemon (* XXX remains to be done *) 655 ] 650 ] *) 656 651 ] 657 652 qed. -
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. -
src/ASM/PolicyStep.ma
r2141 r2152 22 22 match y with 23 23 [ None ⇒ nec_plus_ultra program old_policy 24 | Some p ⇒ And (And (And (And (And (And (And (And (out_of_program_none program p)25 (not_jump_default program p) )24 | Some p ⇒ And (And (And (And (And (And (And 25 (not_jump_default program p) 26 26 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) 27 27 (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉))) 28 28 (jump_increase program old_policy p)) 29 29 (sigma_compact_unsafe program labels p)) 30 (sigma_jump_equal program old_policy p → no_ch = true)) 30 31 (no_ch = true → sigma_pc_equal program old_policy p)) 31 (sigma_jump_equal program old_policy p → no_ch = true))32 32 (\fst p < 2^16) 33 33 ]) … … 38 38 (λprefix.Σx:ℕ × ppc_pc_map. 39 39 let 〈added,policy〉 ≝ x in 40 And (And (And (And (And (And (And (And (And (out_of_program_none prefix policy) 41 (not_jump_default prefix policy)) 40 And (And (And (And (And (And (And (And (And (not_jump_default prefix policy) 42 41 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 43 42 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉))) … … 46 45 (sigma_jump_equal prefix old_sigma policy → added = 0)) 47 46 (added = 0 → sigma_pc_equal prefix old_sigma policy)) 48 (\fst (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd policy) 〈0,short_jump〉) = 49 \fst (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉) + added)) 47 (out_of_program_none prefix policy)) 48 (\fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉) = 49 \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) + added)) 50 50 (sigma_safe prefix labels added old_sigma policy)) 51 51 program … … 100 100 #x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind 101 101 (* USE: inc_pc = fst of policy (from fold) *) 102 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))))) in p1;102 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p1; 103 103 (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *) 104 104 lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) 105 105 #Hsig #Hge 106 106 (* USE: added = 0 → policy_pc_equal (from fold) *) 107 lapply ((proj2 ?? (proj1 ?? (proj1 ?? Hind))) ? (|program|) (le_n (|program|)))107 lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) ? (|program|) (le_n (|program|))) 108 108 [ (* USE: policy_jump_equal → added = 0 (from fold) *) 109 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) #i #Hi109 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi 110 110 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 111 111 [ #Hj 112 112 (* USE: policy_increase (from fold) *) 113 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) i (le_S_to_le … Hi))113 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi)) 114 114 lapply (Habs i Hi Hj) 115 115 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉) … … 122 122 | #Hnj 123 123 (* USE: not_jump_default (from fold and old_sigma) *) 124 >(proj 2?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi Hnj)124 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi Hnj) 125 125 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj) 126 126 @refl … … 132 132 >H2 in H; normalize nodelta -H2 -x #H @conj 133 133 [ @conj [ @conj 134 [ (* USE[pass]: out_of_program_none,not_jump_default, 0 ↦ 0, inc_pc = fst policy,134 [ (* USE[pass]: not_jump_default, 0 ↦ 0, inc_pc = fst policy, 135 135 * jump_increase, sigma_compact_unsafe (from fold) *) 136 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 136 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 137 | #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *) 138 @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) @H2 139 ] 137 140 | (* USE[pass]: added = 0 → sigma_pc_equal (from fold) *) 138 #H2 @(proj2 ?? (proj1 ?? (proj1 ?? H))) @eqb_true_to_eq @H2 139 ] 140 | #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *) 141 @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @H2 141 #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2 142 142 ] 143 143 | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1 … … 153 153 (* NOTE: to save memory and speed up work, there's cases daemon here. They can be 154 154 * commented out for full proofs, but this needs a lot of memory and time *) 155 [ (* out_of_program_none *) (* cases daemon *) 156 #i #Hi2 >append_length <commutative_plus @conj 157 [ (* → *) #Hi normalize in Hi; 158 cases instr in Heq2; normalize nodelta 159 #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss 160 [1,3,5,7,9,11: >lookup_opt_insert_miss 161 [1,3,5,7,9,11: (* USE[pass]: out_of_program_none → *) 162 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2)) 163 @le_S_to_le @Hi 164 |2,4,6,8,10,12: @bitvector_of_nat_abs 165 [1,4,7,10,13,16: @Hi2 166 |2,5,8,11,14,17: @(transitive_lt … Hi2) 167 |3,6,9,12,15,18: @sym_neq @lt_to_not_eq 168 ] @le_S_to_le @Hi 169 ] 170 |2,4,6,8,10,12: @bitvector_of_nat_abs 171 [1,4,7,10,13,16: @Hi2 172 |2,5,8,11,14,17: @(transitive_lt … Hi2) 173 |3,6,9,12,15,18: @sym_neq @lt_to_not_eq 174 ] @Hi 175 ] 176 | (* ← *) <(proj2 ?? (pair_destruct ?????? Heq2)) #Hl 177 elim (decidable_lt i (|prefix|)) 178 [ #Hi 179 lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl)))) 180 #Hl2 (* USE[pass]: out_of_program_none ← *) 181 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2) Hl2) 182 #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3 183 | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi)) 184 [ #Hi3 elim (le_to_or_lt_eq … Hi3) 185 [ / by / 186 | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H) 187 ] 188 | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl)))) 189 >X >eq_bv_refl #H normalize in H; destruct (H) 190 ] 191 ] 192 ] 193 | (* not_jump_default *) (* cases daemon *) 155 [ (* not_jump_default *) cases daemon (* 194 156 #i >append_length <commutative_plus #Hi normalize in Hi; 195 157 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi … … 236 198 ] 237 199 ] 238 ] 239 ] 240 | (* 0 ↦ 0 *) (* cases daemon *) 200 ] *) 201 | (* 0 ↦ 0 *) cases daemon (* 241 202 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 242 203 [ cases (decidable_eq_nat 0 (|prefix|)) … … 260 221 [2: <plus_n_Sm @le_S_S] 261 222 @le_plus_n_r 262 ] 223 ] *) 263 224 ] 264 225 | (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2)) 265 226 >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl 266 227 ] 267 | (* jump_increase *) (* cases daemon *)228 | (* jump_increase *) cases daemon (* 268 229 #i >append_length >commutative_plus #Hi normalize in Hi; 269 230 cases (le_to_or_lt_eq … Hi) -Hi; #Hi … … 359 320 cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉) 360 321 #a #b normalize nodelta %2 @refl 361 ] 362 ] 363 | (* sigma_compact_unsafe *) (* cases daemon *)322 ] *) 323 ] 324 | (* sigma_compact_unsafe *) cases daemon (* 364 325 #i >append_length <commutative_plus #Hi normalize in Hi; 365 326 <(proj2 ?? (pair_destruct ?????? Heq2)) … … 464 425 ] 465 426 ] 466 ] 467 ] 468 | (* policy_jump_equal → added = 0 *) (* cases daemon *)427 ] *) 428 ] 429 | (* policy_jump_equal → added = 0 *) cases daemon (* 469 430 <(proj2 ?? (pair_destruct ?????? Heq2)) 470 431 #Heq <(proj1 ?? (pair_destruct ?????? Heq2)) … … 535 496 ] *) 536 497 ] 537 | (* added = 0 → policy_pc_equal *) (* cases daemon *)498 | (* added = 0 → policy_pc_equal *) cases daemon (* 538 499 (* USE: added = 0 → policy_pc_equal *) 539 500 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) … … 565 526 |2,4,6: >Hi >lookup_insert_miss 566 527 [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|))) 567 @sym_eq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 528 @sym_eq (* USE: fst p = lookup |prefix| *) 529 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 568 530 |2,4,6: @bitvector_of_nat_abs 569 531 [3,6,9: @lt_to_not_eq @le_n … … 575 537 ] 576 538 |2,4,6: >Hi >lookup_insert_hit 539 (* USE fst p = lookup |prefix| *) 577 540 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 578 541 <(Hold Hadded (|prefix|) (le_n (|prefix|))) 579 (*<(proj2 ?? (pair_destruct ?????? Heq1))*)580 542 (* USE: sigma_compact (from old_sigma) *) 581 543 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) … … 593 555 >prf >p1 >Hins >nth_append_second 594 556 [2,4,6: @(le_n (|prefix|)) 595 |1,3,5: <minus_n_n whd in match (nth ????); 596 597 598 599 ] 600 ] 601 |4,5: cases daemon 602 |1: cases daemon 603 ] (* 4,5 and 1 are equal to 2,3,6, but cases-daemon'd for the moment because of 604 * memory constraints *) 605 (*#x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus 557 |1,3,5: <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1)) 558 #H >H @plus_left_monotone @instruction_size_irrelevant @nmk / by / 559 ] 560 ] 561 ] 562 ] 563 ] 564 |4,5: #x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus 606 565 #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi 607 566 [1,3: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi … … 611 570 @plus_zero_zero 612 571 |2,4: @bitvector_of_nat_abs 613 [1,4: @(transitive_lt ??? Hi)] 614 [1,2,3,5: @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length 615 @le_plus_n_r 616 |4,6: @lt_to_not_eq @Hi 572 [3,6: @lt_to_not_eq @Hi 573 |1,4: @(transitive_lt ??? Hi) 617 574 ] 575 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf 576 >append_length @le_plus_n_r 618 577 ] 619 578 |2,4: @bitvector_of_nat_abs 620 [1,4: @(transitive_lt ??? Hi) @le_S_to_le] 621 [1,2,3,5: @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length 622 <plus_n_Sm @le_S_S @le_plus_n_r 623 |4,6: @lt_to_not_eq @le_S @Hi 579 [3,6: @lt_to_not_eq @le_S @Hi 580 |1,4: @(transitive_lt ??? Hi) @le_S_to_le 624 581 ] 582 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf 583 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 625 584 ] 626 585 |2,4: >Hi >lookup_insert_miss 627 586 [1,3: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|))) 628 [2,4: >commutative_plus in Hadded; @plus_zero_zero] 629 @sym_eq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 587 [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq 588 (* USE: fst p = lookup |prefix| *) 589 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 630 590 |2,4: @bitvector_of_nat_abs 631 [1,4: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))] 632 [1,2,3,5: @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length 633 <plus_n_Sm @le_S_S @le_plus_n_r 634 |4,6: @lt_to_not_eq @le_n 591 [3,6: @lt_to_not_eq @le_n 592 |1,4: @(transitive_lt ??? (le_S_S … (le_n (|prefix|)))) 635 593 ] 594 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf 595 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 636 596 ] 637 597 ] 638 |2,4: >Hi >lookup_insert_hit 598 |2,4: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1)) 639 599 elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded))) 640 600 [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt <(proj2 ?? (pair_destruct ?????? Heq1)) 641 @etblorp / by I/ 642 |2,4: #H >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 601 @jump_length_le_max / by I/ 602 |2,4: #H (* USE: fst p = lookup |prefix| *) 603 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 643 604 <(Hold ? (|prefix|) (le_n (|prefix|))) 644 <(proj2 ?? (pair_destruct ?????? Heq1)) 645 (* USE: sigma_compact (from old_sigma) *) 646 cases daemon (* XXX add policy_compact_unsafe to old_sigma *) 605 [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H 606 >(jump_length_equal_max … H) 607 [1,3: (* USE: sigma_compact_unsafe (from old_sigma) *) 608 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) 609 [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 610 |2,4: lapply Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))) 611 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %); 612 [1,3: normalize nodelta #_ #_ #ABS cases ABS 613 |2,4: normalize nodelta 614 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))) 615 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %); 616 [1,3: #_ #x cases x -x #pc #j normalize nodelta #_ #_ #ABS cases ABS 617 |2,4: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ 618 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 619 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair 620 >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second 621 [1,3: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H 622 |2,4: @le_n 623 ] 624 ] 625 ] 626 ] 627 |2,4: / by I/ 628 ] 629 |2,4: @plus_zero_zero [2,4: >commutative_plus @Hadded] 630 ] 647 631 ] 648 632 ] … … 656 640 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 657 641 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 658 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 659 [1,3,5: >lookup_insert_miss 660 [1,3,5: @(Hold Hadded i (le_S_to_le … Hi)) 661 |2,4,6: @bitvector_of_nat_abs 662 [1,4,7: @(transitive_lt ??? Hi) ] 663 [1,2,3,4,6,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 664 @le_S_S @le_plus_n_r 665 |5,7,9: @lt_to_not_eq @Hi 666 ] 667 ] 668 |2,4,6: @bitvector_of_nat_abs 669 [1,4,7: @(transitive_lt … Hi) @le_S_to_le] 670 [1,2,3,4,6,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 642 <(proj2 ?? (pair_destruct ?????? Heq2)) 643 >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i)) 644 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 645 >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc,new_length〉 16 (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i) inc_sigma) 646 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 647 @(Hold Hadded i (le_S_to_le … Hi)) 648 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 649 @bitvector_of_nat_abs 650 [3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 651 @lt_to_not_eq @Hi 652 |1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 653 @(transitive_lt ??? Hi) 654 ] 655 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 656 @le_S_S <plus_n_Sm @le_S @le_plus_n_r 657 ] 658 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 659 @bitvector_of_nat_abs 660 [3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 661 @lt_to_not_eq @le_S @Hi 662 |1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 663 @(transitive_lt … Hi) @le_S_to_le 664 ] 665 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 671 666 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 672 |5,7,9: @lt_to_not_eq @le_S @Hi 673 ] 674 ] 675 |2,4,6: >Hi >lookup_insert_miss 676 [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|))) 677 @sym_eq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 678 |2,4,6: @bitvector_of_nat_abs 679 [1,4,7: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))] 680 [1,2,3,4,6,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 681 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 682 |5,7,9: @lt_to_not_eq @le_n 683 ] 684 ] 685 ] 686 |2,4,6: >Hi >lookup_insert_hit 687 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 688 <(Hold Hadded (|prefix|) (le_n (|prefix|))) 689 <(proj2 ?? (pair_destruct ?????? Heq1)) 690 (* USE: sigma_compact (from old_sigma) *) 691 cases daemon (* XXX add policy_compact_unsafe to old_sigma *) 692 ]*) 693 ] 694 | (* lookup p = lookup old_sigma + added *) 695 cases daemon 696 ] 697 | (* sigma_safe *) (* cases daemon *) 698 #i >append_length >commutative_plus #Hi normalize in Hi; 667 ] 668 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 669 >Hi >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|))) 670 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 671 >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|))) @sym_eq 672 (* USE: fst p = lookup |prefix| *) 673 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 674 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 675 @bitvector_of_nat_abs 676 [3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 677 @lt_to_not_eq @le_n 678 |1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 679 @le_S_to_le 680 ] 681 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 682 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 683 ] 684 ] 685 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 686 >Hi >lookup_insert_hit 687 (* USE fst p = lookup |prefix| *) 688 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 689 <(Hold Hadded (|prefix|) (le_n (|prefix|))) 690 (* USE: sigma_compact (from old_sigma) *) 691 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) 692 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 693 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 694 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 695 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))) 696 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% -> %); 697 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 698 normalize nodelta #_ #ABS cases ABS 699 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 700 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))) 701 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %); 702 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 703 normalize nodelta #Hl #x cases x -x #pc #j normalize nodelta #Hl2 #ABS cases ABS 704 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 705 normalize nodelta #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ 706 normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) 707 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 708 >prf >p1 >Hins >nth_append_second 709 [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 710 @(le_n (|prefix|)) 711 |1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 712 <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1)) 713 #H >H @plus_left_monotone @instruction_size_irrelevant @nmk #H @H 714 ] 715 ] 716 ] 717 ] 718 ] 719 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Hold #Hadded 720 #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) 721 -Hi #Hi 722 [1,3,5,7,9,11,13,15,17: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 723 [1,3,5,7,9,11,13,15,17: 724 >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i)) 725 [1,3,5,7,9,11,13,15,17: 726 >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc,new_length〉 16 (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i) inc_sigma) 727 [1,3,5,7,9,11,13,15,17: @(Hold ? i (le_S_to_le … Hi)) 728 >commutative_plus in Hadded; @plus_zero_zero 729 |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 730 [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi 731 |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi) 732 ] 733 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf 734 >append_length @le_plus_n_r 735 ] 736 |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 737 [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi 738 |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi) @le_S_to_le 739 ] 740 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf 741 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 742 ] 743 |2,4,6,8,10,12,14,16,18: >Hi 744 >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|))) 745 [1,3,5,7,9,11,13,15,17: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|))) 746 [2,4,6,8,10,12,14,16,18: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq 747 (* USE: fst p = lookup |prefix| *) 748 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 749 |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 750 [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n 751 |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? (le_S_S … (le_n (|prefix|)))) 752 ] 753 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf 754 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 755 ] 756 ] 757 |2,4,6,8,10,12,14,16,18: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1)) 758 elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded))) 759 [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt 760 <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max / by I/ 761 |2,4,6,8,10,12,14,16,18: #H (* USE: fst p = lookup |prefix| *) 762 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 763 <(Hold ? (|prefix|) (le_n (|prefix|))) 764 [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H 765 >(jump_length_equal_max … H) 766 [1,3,5,7,9,11,13,15,17: (* USE: sigma_compact_unsafe (from old_sigma) *) 767 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) 768 [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 769 |2,4,6,8,10,12,14,16,18: lapply Holdeq 770 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))) 771 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %); 772 [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #ABS cases ABS 773 |2,4,6,8,10,12,14,16,18: normalize nodelta 774 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))) 775 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %); 776 [1,3,5,7,9,11,13,15,17: #_ #x cases x -x #pc #j normalize nodelta 777 #_ #_ #ABS cases ABS 778 |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x 779 #pc #j #EQ 780 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 781 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair 782 >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second 783 [1,3,5,7,9,11,13,15,17: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H 784 |2,4,6,8,10,12,14,16,18: @le_n 785 ] 786 ] 787 ] 788 ] 789 |2,4,6,8,10,12,14,16,18: / by I/ 790 ] 791 |2,4,6,8,10,12,14,16,18: @plus_zero_zero 792 [2,4,6,8,10,12,14,16,18: >commutative_plus @Hadded] 793 ] 794 ] 795 ] 796 ] 797 ] *) 798 ] 799 | (* out_of_program_none *) cases daemon 800 (* #i #Hi2 >append_length <commutative_plus @conj 801 [ (* → *) #Hi normalize in Hi; 802 cases instr in Heq2; normalize nodelta 803 #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss 804 [1,3,5,7,9,11: >lookup_opt_insert_miss 805 [1,3,5,7,9,11: (* USE[pass]: out_of_program_none → *) 806 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2)) 807 @le_S_to_le @Hi 808 |2,4,6,8,10,12: @bitvector_of_nat_abs 809 [1,4,7,10,13,16: @Hi2 810 |2,5,8,11,14,17: @(transitive_lt … Hi2) 811 |3,6,9,12,15,18: @sym_neq @lt_to_not_eq 812 ] @le_S_to_le @Hi 813 ] 814 |2,4,6,8,10,12: @bitvector_of_nat_abs 815 [1,4,7,10,13,16: @Hi2 816 |2,5,8,11,14,17: @(transitive_lt … Hi2) 817 |3,6,9,12,15,18: @sym_neq @lt_to_not_eq 818 ] @Hi 819 ] 820 | (* ← *) <(proj2 ?? (pair_destruct ?????? Heq2)) #Hl 821 elim (decidable_lt i (|prefix|)) 822 [ #Hi 823 lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl)))) 824 #Hl2 (* USE[pass]: out_of_program_none ← *) 825 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2) Hl2) 826 #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3 827 | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi)) 828 [ #Hi3 elim (le_to_or_lt_eq … Hi3) 829 [ / by / 830 | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H) 831 ] 832 | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl)))) 833 >X >eq_bv_refl #H normalize in H; destruct (H) 834 ] 835 ] 836 ] *) 837 ] 838 | (* lookup p = lookup old_sigma + added *) cases daemon 839 (* <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O 840 >lookup_insert_hit 841 <(proj1 ?? (pair_destruct ?????? Heq2)) cases instr in p1 Heq1; 842 [2,3,6: #x [3: #y] normalize nodelta #p1 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 843 (* USE: sigma_compact_unsafe (from old_sigma) *) 844 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) 845 [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 846 |2,4,6: lapply Holdeq -Holdeq 847 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))) 848 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %); 849 [1,3,5: normalize nodelta #_ #_ #abs cases abs 850 |2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))) 851 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %); 852 [1,3,5: normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs 853 |2,4,6: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta 854 #H (* USE: fst p = lookup |prefix| *) 855 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 856 (* USE[pass]: lookup p = lookup old_sigma + added *) 857 >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; 858 -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ)) 859 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second 860 [1,3,5: <minus_n_n >p1 whd in match (nth ????); >associative_plus 861 >(associative_plus pc) @plus_left_monotone >commutative_plus 862 @plus_right_monotone @instruction_size_irrelevant @nmk #H @H 863 |2,4,6: @le_n 864 ] 865 ] 866 ] 867 ] 868 |4,5: #x normalize nodelta #p1 #Heq1 869 (* USE: sigma_compact_unsafe (from old_sigma) *) 870 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) 871 [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 872 |2,4: lapply Holdeq -Holdeq 873 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))) 874 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %); 875 [1,3: normalize nodelta #_ #_ #abs cases abs 876 |2,4: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))) 877 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %); 878 [1,3: normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs 879 |2,4: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta 880 #H (* USE: fst p = lookup |prefix| *) 881 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 882 (* USE[pass]: lookup p = lookup old_sigma + added *) 883 >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; 884 -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ)) 885 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >associative_plus 886 >(associative_plus pc) @plus_left_monotone >assoc_plus1 887 >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative 888 [1,3: >(proj2 ?? (pair_destruct ?????? EQ)) >prf >nth_append_second 889 [1,3: <minus_n_n whd in match (nth ????); >p1 >commutative_plus 890 @minus_plus_m_m 891 |2,4: @le_n 892 ] 893 |2,4: <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max @I 894 ] 895 ] 896 ] 897 ] 898 |1: #pi cases pi 899 [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: 900 [1,2,3,6,7,24,25: #x #y 901 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 902 normalize nodelta #p1 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 903 (* USE: sigma_compact_unsafe (from old_sigma) *) 904 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) 905 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 906 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 907 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 908 lapply Holdeq -Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))) 909 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %); 910 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 911 normalize nodelta #_ #_ #abs cases abs 912 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 913 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))) 914 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %); 915 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 916 normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs 917 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 918 #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta 919 #H (* USE: fst p = lookup |prefix| *) 920 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 921 (* USE[pass]: lookup p = lookup old_sigma + added *) 922 >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; 923 -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ)) 924 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second 925 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 926 <minus_n_n >p1 whd in match (nth ????); >associative_plus 927 >(associative_plus pc) @plus_left_monotone >commutative_plus 928 @plus_right_monotone @instruction_size_irrelevant @nmk #H @H 929 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 930 @le_n 931 ] 932 ] 933 ] 934 ] 935 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta #p1 #Heq1 936 (* USE: sigma_compact_unsafe (from old_sigma) *) 937 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) 938 [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 939 |2,4,6,8,10,12,14,16,18: lapply Holdeq -Holdeq 940 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))) 941 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %); 942 [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #abs cases abs 943 |2,4,6,8,10,12,14,16,18: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))) 944 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %); 945 [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #x cases x -x #Spc #Sj 946 normalize nodelta #_ #_ #abs cases abs 947 |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j 948 #Holdeq #EQ normalize nodelta #H (* USE: fst p = lookup |prefix| *) 949 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 950 (* USE[pass]: lookup p = lookup old_sigma + added *) 951 >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; 952 -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ)) 953 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >associative_plus 954 >(associative_plus pc) @plus_left_monotone >assoc_plus1 955 >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative 956 [1,3,5,7,9,11,13,15,17: >(proj2 ?? (pair_destruct ?????? EQ)) >prf 957 >nth_append_second 958 [1,3,5,7,9,11,13,15,17: <minus_n_n whd in match (nth ????); >p1 959 >commutative_plus @minus_plus_m_m 960 |2,4,6,8,10,12,14,16,18: @le_n 961 ] 962 |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq1)) 963 @jump_length_le_max @I 964 ] 965 ] 966 ] 967 ] 968 ] 969 ] *) 970 ] 971 | (* sigma_safe *) cases daemon 972 (* #i >append_length >commutative_plus #Hi normalize in Hi; 699 973 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 700 974 [ >nth_append_first [2: @Hi] … … 704 978 [ elim (le_to_or_lt_eq … Hi) -Hi #Hi 705 979 [ >lookup_insert_miss 706 [ (* USE[pass]: sigma_safe *) 707 lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi)) 708 cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉) 709 #pc #j cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉) 710 #pc_plus_jmp_length #_ cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins 711 normalize nodelta #Hind #dest #Hj lapply (Hind dest Hj) -Hind 712 lapply (refl ? (leb (lookup_def … labels dest 0) (S (|prefix|)))) 713 cases (leb (lookup_def … labels dest 0) (S (|prefix|))) in ⊢ (???% → %); 714 normalize nodelta 715 [ #Hle elim (le_to_or_lt_eq … (leb_true_to_le … Hle)) -Hle #Hle 716 [ >(le_to_leb_true … (le_S_S_to_le … Hle)) normalize nodelta 717 >lookup_insert_miss 718 [ elim (le_to_or_lt_eq … (le_S_S_to_le … Hle)) -Hle #Hle 719 [ >lookup_insert_miss 720 [ cases j / by / 721 | @bitvector_of_nat_abs 722 [ @(transitive_lt ??? Hle) ] 723 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) 724 >prf @le_S_S >append_length @le_plus_n_r 725 | @lt_to_not_eq @Hle 980 [ lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi)) 981 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le … Hi)) 982 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)) 983 cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) in ⊢ (???% → %); 984 [ normalize nodelta #_ #abs cases abs 985 | #x cases x -x #ipc #ij #EQi normalize nodelta 986 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)) 987 cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %); 988 [ normalize nodelta #_ #abs cases abs 989 | #x cases x -x #Sipc #Sij #EQSi normalize nodelta #Hcompact 990 >(lookup_opt_lookup_hit … EQi 〈0,short_jump〉) 991 >(lookup_opt_lookup_hit … EQSi 〈0,short_jump〉) >Hcompact 992 normalize nodelta (*cases ij*) normalize nodelta 993 lapply (refl ? (nth i ? prefix 〈None ?, Comment []〉)) 994 cases (nth i ? prefix 〈None ?, Comment []〉) in ⊢ (???% → %); 995 #lbl #ins normalize nodelta #Hins #Hind #dest #Hi 996 lapply (Hind dest Hi) -Hind #Hind 997 elim (decidable_le (lookup_def … labels dest 0) (S (|prefix|))) 998 [ #Hle elim (le_to_or_lt_eq … Hle) -Hle #Hle 999 [ elim (le_to_or_lt_eq … (le_S_S_to_le … Hle)) -Hle #Hle 1000 [ >(le_to_leb_true ?? (le_S_to_le ?? Hle)) in Hind; 1001 >(le_to_leb_true ?? (le_S ?? (le_S_to_le ?? Hle))) 1002 normalize nodelta >lookup_insert_miss 1003 [ >lookup_insert_miss 1004 [ #H @H 1005 | @bitvector_of_nat_abs 1006 [3: @lt_to_not_eq @Hle 1007 |1: @(transitive_lt ??? Hle) 1008 ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 1009 >append_length @le_S_S @le_plus_n_r 1010 ] 1011 | @bitvector_of_nat_abs 1012 [3: @lt_to_not_eq @le_S_to_le @le_S_S @Hle 1013 |1: @(transitive_lt ??? Hle) @le_S_to_le 1014 ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 1015 >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 1016 ] 1017 | >Hle >Hle in Hind; >(le_to_leb_true ?? (le_n (|prefix|))) 1018 >(le_to_leb_true ?? (le_S ?? (le_n (|prefix|)))) 1019 normalize nodelta >lookup_insert_miss 1020 [ >lookup_insert_hit 1021 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 1022 #H @H 1023 | @bitvector_of_nat_abs 1024 [3: @lt_to_not_eq @le_n 1025 |1: @le_S_to_le 1026 ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 1027 >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 726 1028 ] 727 1029 ] 728 | >Hle >lookup_insert_hit 729 (* USE: inc_pc = fst policy *) 730 <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 731 cases j / by / 1030 | >Hle >Hle in Hind; 1031 >(not_le_to_leb_false (S (|prefix|)) (|prefix|)) 1032 [2: @le_to_not_lt @le_n] 1033 >(le_to_leb_true ?? (le_n (S (|prefix|)))) 1034 normalize nodelta >lookup_insert_hit 1035 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) 1036 [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 1037 | lapply (proj2 ?? (proj1 ?? Hpolicy)) 1038 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))) 1039 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %); 1040 [ normalize nodelta #_ #_ #abs cases abs 1041 | #x cases x -x #opc #oj #EQo 1042 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))) 1043 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %); 1044 [ normalize nodelta #_ #_ #abs cases abs 1045 | #x cases x -x #Sopc #Soj #EQSo normalize nodelta 1046 #Hadded #Hcommon 1047 >(lookup_opt_lookup_hit … EQSo 〈0,short_jump〉) 1048 >Hcommon >(lookup_opt_lookup_hit … EQo 〈0,short_jump〉) in Holdeq; 1049 #Holdeq >(proj1 ?? (pair_destruct ?????? Holdeq)) 1050 >(commutative_plus old_pc ?) >associative_plus 1051 <Hadded 1052 <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 1053 >prf >nth_append_second 1054 [ <minus_n_n whd in match (nth ????); >p1 cases instr in Heq1; 1055 [2,3,6: #x [3: #y] normalize nodelta #Heq1 1056 <(proj2 ?? (pair_destruct ?????? Heq1)) 1057 <(commutative_plus inc_pc) 1058 >(instruction_size_irrelevant ?? oj short_jump) 1059 [1,3,5: #H @H 1060 |2,4,6: @nmk #H @H 1061 ] 1062 |4,5: #x normalize nodelta #Heq1 1063 <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind 1064 cases daemon (* axiomatise this *) 1065 |1: #pi cases pi 1066 [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: 1067 [1,2,3,6,7,24,25: #x #y 1068 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 1069 normalize nodelta #Heq1 1070 <(proj2 ?? (pair_destruct ?????? Heq1)) 1071 <(commutative_plus inc_pc) 1072 >(instruction_size_irrelevant ?? oj short_jump) 1073 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 1074 #H @H 1075 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 1076 @nmk #H @H 1077 ] 1078 |9,10,11,12,13,14,15,16,17: 1079 #x [3,4,5,8,9: #y] normalize nodelta #Heq1 1080 <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind 1081 cases daemon (* axiomatise this *) 1082 ] 1083 ] 1084 | @le_n 1085 ] 1086 ] 1087 ] 1088 ] 732 1089 ] 733 | @bitvector_of_nat_abs 734 [ @(transitive_lt ??? Hle) ] 735 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) 736 @le_S_S >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 737 | @lt_to_not_eq @Hle 1090 | #X >(not_le_to_leb_false … X) 1091 >(not_le_to_leb_false … (lt_to_not_le … (le_S_to_le … (not_le_to_lt … X)))) in Hind; 1092 normalize nodelta <(proj1 ?? (pair_destruct ?????? Heq2)) 1093 cases instr in Heq1; 1094 [2,3,6: #x [3: #y] normalize nodelta #_ #H @H 1095 |4,5: #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind 1096 cases daemon (* axiomatise this *) 1097 |1: #pi cases pi 1098 [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: 1099 [1,2,3,6,7,24,25: #x #y 1100 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 1101 normalize nodelta #_ #H @H 1102 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 1103 normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 1104 #Hind cases daemon (* axiomatise this *) 1105 ] 738 1106 ] 739 1107 ] 740 | >Hle >lookup_insert_hit >(not_le_to_leb_false (S (|prefix|)) (|prefix|))741 [2: @le_to_not_lt @le_n ] normalize nodelta742 (* USE: lookup p = lookup old_sigma + added *)743 <(proj2 ?? (proj1 ?? Hpolicy)) cases daemon (* use compactness here *)744 1108 ] 745 | (* same, but with forward jump *) cases daemon746 1109 ] 747 | @bitvector_of_nat_abs cases daemon (* trivial, see above *) 748 ] 749 | >Hi >lookup_insert_hit cases daemon 750 ] 751 | @bitvector_of_nat_abs cases daemon (* see above *) 752 ] 753 | @bitvector_of_nat_abs cases daemon 754 ] 755 | @bitvector_of_nat_abs cases daemon 756 ] 757 | >Hi cases daemon 758 ] *) 759 ] 1110 | @bitvector_of_nat_abs 1111 [3: @lt_to_not_eq @Hi 1112 |1: @(transitive_lt ??? Hi) 1113 ] 1114 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 1115 @le_S_S @le_plus_n_r 1116 ] 1117 | >Hi >lookup_insert_hit lapply ((proj2 ?? Hpolicy) i) 1118 ] XXX to be continued *) 1119 ] 760 1120 | normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 761 1121 [ #i cases i 1122 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1123 | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O 1124 ] 1125 | >lookup_insert_hit @refl 1126 ] 1127 | >lookup_insert_hit @refl 1128 ] 1129 | #i #Hi <(le_n_O_to_eq … Hi) 1130 >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉) 1131 #a #b normalize nodelta %2 @refl 1132 ] 1133 | #i cases i 1134 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1135 | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1136 ] 1137 ] 1138 | #_ % 1139 ] 1140 | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit 1141 (* USE: 0 ↦ 0 (from old_sigma) *) 1142 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) 1143 ] 1144 | #i cases i 762 1145 [ #Hi2 @conj 763 1146 [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by / … … 776 1159 ] 777 1160 ] 778 | #i cases i 779 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 780 | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O 781 ] 782 ] 783 | >lookup_insert_hit @refl 784 ] 785 | >lookup_insert_hit @refl 786 ] 787 | #i #Hi <(le_n_O_to_eq … Hi) 788 >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉) 789 #a #b normalize nodelta %2 @refl 1161 ] 1162 | >lookup_insert_hit (* USE: 0 ↦ 0 (from old_sigma) *) 1163 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) <plus_n_O % 790 1164 ] 791 1165 | #i cases i … … 794 1168 ] 795 1169 ] 796 | #_ %797 ]798 | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit799 (* USE: 0 ↦ 0 (from old_sigma) *)800 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))))801 ]802 | cases daemon (* empty program here *)803 ]804 | #i cases i805 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O806 | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O807 ]808 ]809 1170 ] 810 1171 qed. 1172
Note: See TracChangeset
for help on using the changeset viewer.