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

 1 edited
Legend:
 Unmodified
 Added
 Removed

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 casesdaemon'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.