- Timestamp:
- Jul 20, 2012, 6:15:40 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Policy.ma
r2211 r2225 27 27 | Some op ⇒ λp2.if no_ch 28 28 then pi1 ?? (jump_expansion_internal program m) 29 else pi1 ?? (jump_expansion_step program labels«op,?»)29 else pi1 ?? (jump_expansion_step program (pi1 ?? labels) «op,?») 30 30 ] (refl … z) 31 31 ] (refl … n). 32 [ normalize nodelta cases (jump_expansion_start program (create_label_map program)) 32 [5: cases labels #label_map #spec #id #id_ok cases (spec … id_ok) // 33 | normalize nodelta cases (jump_expansion_start program (create_label_map program)) 33 34 #x cases x -x 34 [ #H / by I/35 [ #H % 35 36 | #sigma normalize nodelta #H @conj [ @conj 36 37 [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) … … 40 41 ] 41 42 ] 42 | / by I/43 | % 43 44 | cases no_ch in p1; #p1 44 45 [ @(pi2 ?? (jump_expansion_internal program m)) 45 | cases (jump_expansion_step program (create_label_map program) «op,?»)46 | cases (jump_expansion_step ???) 46 47 #x cases x -x #ch2 #z2 cases z2 normalize nodelta 47 [ #_ / by I/48 [ #_ % 48 49 | #j2 #H2 @conj [ @conj 49 50 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))) … … 99 100 100 101 lemma pe_refl: ∀program.reflexive ? (policy_equal_opt program). 101 #program whd #x whd cases x 102 [ // 103 | #y @pe_int_refl 104 ] 102 #program whd #x whd cases x try % #y @pe_int_refl 105 103 qed. 106 104 … … 108 106 #program whd #x #y #Hxy whd cases y in Hxy; 109 107 [ cases x 110 [ //108 [ #_ % 111 109 | #x' #H @⊥ @(absurd ? H) /2 by nmk/ 112 110 ] … … 171 169 [ #HN normalize nodelta #SEQ >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? SEQ)))) 172 170 / by / 173 | #HN normalize nodelta cases (jump_expansion_step program (create_label_map program) «Npol,?»)171 | #HN normalize nodelta cases (jump_expansion_step ???) 174 172 #x cases x -x #Stno_ch #Stno_o normalize nodelta cases Stno_o 175 173 [ normalize nodelta #_ #H destruct (H) … … 181 179 ] 182 180 ] 183 qed. 184 181 qed. 185 182 186 183 lemma pe_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l). … … 189 186 policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program (S n)))) 190 187 (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))). 191 #program #n #Heq 192 cases daemon (* XXX *) 188 #program #n #Heq cases daemon (* XXX *) 193 189 qed. 194 190 … … 259 255 \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧ 260 256 \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧ 261 sigma_compact_unsafe program ( create_label_map program) p ∧257 sigma_compact_unsafe program (pi1 … (create_label_map program)) p ∧ 262 258 \fst p ≤ 2^16. 263 259 ∀l.|l| ≤ |program| → ∀acc:ℕ. 264 match \snd (pi1 ?? (jump_expansion_step program ( create_label_map program) policy)) with260 match \snd (pi1 ?? (jump_expansion_step program (pi1 … (create_label_map program)) policy)) with 265 261 [ None ⇒ True 266 262 | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc 267 263 ]. 264 [2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) // ] 268 265 #program #policy #l elim l -l; 269 266 [ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ] 270 267 | #h #t #Hind #Hp #acc 271 lapply (refl ? (jump_expansion_step program (create_label_map program) policy)) 272 cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #c #r cases r 268 inversion (jump_expansion_step ???) #pi1 cases pi1 -pi1 #c #r cases r 273 269 [ / by I/ 274 270 | #x normalize nodelta #Hx #Hjeq … … 331 327 \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧ 332 328 \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧ 333 sigma_compact_unsafe program ( create_label_map program) p ∧329 sigma_compact_unsafe program (pi1 … (create_label_map program)) p ∧ 334 330 \fst p ≤ 2^16. 335 match (\snd (pi1 ?? (jump_expansion_step program ( create_label_map program) policy))) with331 match (\snd (pi1 ?? (jump_expansion_step program (pi1 … (create_label_map program)) policy))) with 336 332 [ None ⇒ True 337 333 | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ]. 338 #program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) 339 cases (jump_expansion_step program (create_label_map program) policy) in ⊢ (???% → %); 334 [2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) //] 335 #program #policy inversion (jump_expansion_step ???) 340 336 #p cases p -p #ch #pol normalize nodelta cases pol 341 337 [ / by I/ … … 421 417 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0) 422 418 (\fst pol = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd pol) 〈0,short_jump〉))) 423 (sigma_compact program ( create_label_map program) pol))419 (sigma_compact program (pi1 … (create_label_map program)) pol)) 424 420 (\fst pol ≤ 2^16) 425 421 ]. … … 429 425 (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|)) 430 426 [ #Hex cases Hex -Hex #k #Hk 431 lapply (refl ? (jump_expansion_internal program (S (2*|program|)))) 432 cases (jump_expansion_internal ? (S (2*|program|))) in ⊢ (???% → %); 427 inversion (jump_expansion_internal ??) 433 428 #x cases x -x #Gno_ch #Go cases Go normalize nodelta 434 429 [ #H #Heq / by I/ … … 447 442 | @(proj2 ?? (proj1 ?? (proj1 ?? HGp))) 448 443 ] 449 | @(equal_compact_unsafe_compact ? ?Fp)444 | @(equal_compact_unsafe_compact ? Fp) 450 445 [ lapply (jump_pc_equal program (2*|program|)) 451 446 >Feq >Geq normalize nodelta #H @H @Heq … … 546 541 | @(proj2 ?? (proj1 ?? (proj1 ?? HGp))) 547 542 ] 548 | @(equal_compact_unsafe_compact ? ?Fp)543 | @(equal_compact_unsafe_compact ? Fp) 549 544 [ lapply (jump_pc_equal program (2*(|program|))) >Feq >Geq normalize nodelta 550 545 #H @H #i #Hi 551 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))546 inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 552 547 [ #Hj whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*85s*) 553 548 >Feq in Geq; normalize nodelta cases Fno_ch 554 549 [ normalize nodelta #Heq 555 550 >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) % 556 | normalize nodelta cases (jump_expansion_step program (create_label_map program) «Fp,?»)551 | normalize nodelta cases (jump_expansion_step ???) 557 552 #x cases x -x #stch #sto normalize nodelta cases sto 558 553 [ normalize nodelta #_ #X destruct (X) … … 560 555 <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) 561 556 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hst)))) i (le_S_to_le … Hi)) 562 lapply (Hfull i Hi Hj)557 lapply (Hfull i Hi ?) [>Hj %] 563 558 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉) 564 559 #fp #fj #Hfj >Hfj normalize nodelta … … 570 565 ] 571 566 ] 572 | #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi Hj)573 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl567 | #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi ?) [2:>Hj %] 568 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi ?) [2:>Hj] % 574 569 ] 575 570 | cases daemon (* true, but have to add to properties in some way *) … … 630 625 631 626 (* The glue between Policy and Assembly. *) 632 (*CSC: modified to really use the specification in Assembly.ma.*)633 627 definition jump_expansion': 634 628 ∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l). … … 642 636 [ None ⇒ λp.None ? 643 637 | Some x ⇒ λp.Some ? 644 «〈(λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉in638 «〈(λppc.let pc ≝ \fst (bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉) in 645 639 bitvector_of_nat 16 pc), 646 (λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉in640 (λppc.let jl ≝ \snd (bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉) in 647 641 jmpeqb jl long_jump)〉,?» 648 642 ] (refl ? f). … … 666 660 >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta 667 661 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta 668 >add_bitvector_of_nat_plus >Hcompact whd in match instruction_size; 669 normalize nodelta whd in match assembly_1_pseudoinstruction; 670 normalize nodelta whd in match expand_pseudo_instruction; 671 normalize nodelta whd in match fetch_pseudo_instruction; 672 normalize nodelta 673 lapply (refl ? (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok)) 674 cases (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok) in ⊢ (???% → %); 675 #label #instr normalize nodelta #Hli <(nth_safe_nth ? (\snd program) (nat_of_bitvector 16 ppc) ppc_ok 〈None ?, Comment []〉) 676 >Hli normalize nodelta cases instr 677 [2,3,6: #x [3: #y] normalize nodelta % 678 |4,5: #x normalize nodelta 679 >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta 680 whd in match create_label_map; normalize nodelta 681 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta 682 cases (bvt_lookup … (bitvector_of_nat ? 683 (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 684 #lpc #ljl normalize nodelta @refl 685 |1: #pi cases pi 686 [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: 687 [1,2,3,6,7,24,25: #x #y 688 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 689 normalize nodelta % 690 |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta 691 whd in match expand_relative_jump; normalize nodelta 692 whd in match expand_relative_jump_internal; normalize nodelta 693 >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta 694 whd in match create_label_map; normalize nodelta 695 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta 696 cases (bvt_lookup … (bitvector_of_nat ? 697 (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 698 #lpc #ljl normalize nodelta % 699 ] 700 ] 701 ] 702 ] 662 >add_bitvector_of_nat_plus >Hcompact @eq_f @eq_f @eq_f 663 whd in match (fetch_pseudo_instruction ???); >nth_safe_nth 664 [ cases (nth ? labelled_instruction ??) |2: skip] normalize nodelta // ]] 703 665 | (* Basic proof scheme: 704 666 - ppc < |snd program|, hence our instruction is in the program … … 719 681 cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %); 720 682 [ normalize nodelta #_ #abs cases abs 721 | #x cases x -x #Spc #Sjl #SEQ normalize nodelta whd in match instruction_size; 722 normalize nodelta whd in match assembly_1_pseudoinstruction; 723 normalize nodelta whd in match expand_pseudo_instruction; 724 normalize nodelta whd in match fetch_pseudo_instruction; 725 normalize nodelta 726 lapply (refl ? (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok)) 727 cases (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok) in ⊢ (???% → %); 728 #label #instr normalize nodelta #Hli <(nth_safe_nth ? (\snd program) (nat_of_bitvector 16 ppc) ppc_ok 〈None ?, Comment []〉) 729 >Hli normalize nodelta cases instr 730 [2,3,6: #x [3: #y] normalize nodelta #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 731 normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse 732 [1,3,5: <H 733 lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)) 734 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #X @X 735 |2,4,6: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)) 683 | #x cases x -x #Spc #Sjl #SEQ normalize nodelta 684 #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 685 >nat_of_bitvector_bitvector_of_nat_inverse 686 [2: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)) 736 687 >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 737 #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H 738 ] 739 |4,5: #x normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 740 normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse 741 [1,3: <add_bitvector_of_nat_Sm in SEQ; 742 >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative #SEQ 743 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) normalize nodelta 744 cases (bvt_lookup ?? (bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 745 #lpc #ljl normalize nodelta #H <H 746 lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)) 747 <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector 748 >add_commutative >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #H2 @H2 749 |2,4: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)) 750 >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 751 #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H 752 ] 753 |1: #pi cases pi 754 [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: 755 [1,2,3,6,7,24,25: #x #y 756 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 757 normalize nodelta #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 758 normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse 759 [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: 760 <H lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)) 761 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #X @X 762 |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: 763 lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)) 764 >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 765 #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H 766 ] 767 |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] 768 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 769 normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse 770 [1,3,5,7,9,11,13,15,17: <add_bitvector_of_nat_Sm in SEQ; 771 >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative #SEQ 772 whd in match expand_relative_jump; normalize nodelta 773 whd in match expand_relative_jump_internal; normalize nodelta 774 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) normalize nodelta 775 cases (bvt_lookup ?? (bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 776 #lpc #ljl normalize nodelta #H <H 777 lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)) 778 <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector 779 >add_commutative >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #H2 @H2 780 |2,4,6,8,10,12,14,16,18: 781 lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)) 782 >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 783 #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H 784 ] 785 ] 786 ] 787 ] 788 ] 688 #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H ] 689 lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)) 690 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >H -H #H @(transitive_le … H) 691 cut (∀x,y. x=y → x ≤ y) [ #x #y * %] #eq_to_leq @eq_to_leq @eq_f @eq_f 692 whd in match (fetch_pseudo_instruction ???); >nth_safe_nth 693 [ cases (nth ? labelled_instruction ??) |2: skip] normalize nodelta // ]] 789 694 | (* the program is of length 2^16 and ppc is followed by only zero-size instructions 790 695 * until the end of the program *) … … 812 717 >(nth_safe_nth … 〈None ?, Comment []〉) 813 718 cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉) 814 #lbl #ins normalize nodelta 815 whd in match instruction_size; 816 whd in match assembly_1_pseudoinstruction; 817 whd in match expand_pseudo_instruction; normalize nodelta 818 <add_bitvector_of_nat_Sm in SEQ; >bitvector_of_nat_inverse_nat_of_bitvector 819 >add_commutative #SEQ cases ins 820 [2,3,6: #x [3: #y] normalize nodelta #H @H 821 |4,5: #x normalize nodelta 822 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 823 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) 824 cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 825 #lpc #ljl normalize nodelta #H @H 826 |1: #pi cases pi 827 [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: 828 [1,2,3,6,7,24,25: #x #y 829 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 830 normalize nodelta #H @H 831 |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta 832 whd in match expand_relative_jump; 833 whd in match expand_relative_jump_internal; normalize nodelta 834 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 835 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) 836 cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 837 #lpc #ljl normalize nodelta #H @H 838 ] 839 ] 719 #lbl #ins normalize nodelta #X @X 840 720 | <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc 841 721 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #Hspc %2 @conj … … 873 753 normalize nodelta >(nth_safe_nth … 〈None ?, Comment []〉) 874 754 cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment []〉) in H; 875 #lbl #ins normalize nodelta 876 whd in match instruction_size; 877 whd in match assembly_1_pseudoinstruction; 878 whd in match expand_pseudo_instruction; normalize nodelta 879 <add_bitvector_of_nat_Sm in SXEQ; >bitvector_of_nat_inverse_nat_of_bitvector 880 >add_commutative #SXEQ cases ins 881 [2,3,6: #x [3: #y] normalize nodelta #H @(sym_eq ??? H) 882 |4,5: #x normalize nodelta 883 >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) 884 >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉) 885 cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 886 #lpc #ljl normalize nodelta #H @(sym_eq ??? H) 887 |1: #pi cases pi 888 [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: 889 [1,2,3,6,7,24,25: #x #y 890 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta 891 #H @(sym_eq ??? H) 892 |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta 893 whd in match expand_relative_jump; 894 whd in match expand_relative_jump_internal; normalize nodelta 895 >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) 896 >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉) 897 cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 898 #lpc #ljl normalize nodelta #H @(sym_eq ??? H) 899 ] 900 ] 755 #lbl #ins normalize nodelta #X @sym_eq @X 901 756 ] 902 757 ] … … 918 773 cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 919 774 #lpc #ljl normalize nodelta #H @H 920 |1: #pi cases pi 921 [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: 922 [1,2,3,6,7,24,25: #x #y 923 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta 924 #H @H 925 |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta 926 whd in match expand_relative_jump; 927 whd in match expand_relative_jump_internal; normalize nodelta 928 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 929 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) 930 cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 931 #lpc #ljl normalize nodelta #H @H 932 ] 775 |1: #pi normalize nodelta #X @X 933 776 ] 934 777 ] -
src/ASM/PolicyFront.ma
r2222 r2225 22 22 λx:preinstruction Identifier. 23 23 match x with 24 [ JC _ ⇒ True25 | JNC _ ⇒ True26 | JZ _ ⇒ True27 | JNZ _ ⇒ True28 | JB _ _ ⇒ True29 | JNB _ _ ⇒ True30 | JBC _ _ ⇒ True31 | CJNE _ _ ⇒ True32 | DJNZ _ _ ⇒ True33 | _ ⇒ False24 [ JC _ ⇒ true 25 | JNC _ ⇒ true 26 | JZ _ ⇒ true 27 | JNZ _ ⇒ true 28 | JB _ _ ⇒ true 29 | JNB _ _ ⇒ true 30 | JBC _ _ ⇒ true 31 | CJNE _ _ ⇒ true 32 | DJNZ _ _ ⇒ true 33 | _ ⇒ false 34 34 ]. 35 35 … … 38 38 match instr with 39 39 [ Instruction i ⇒ is_jump' i 40 | _ ⇒ False40 | _ ⇒ false 41 41 ]. 42 42 … … 45 45 match instr with 46 46 [ Instruction i ⇒ is_jump' i 47 | Call _ ⇒ True48 | Jmp _ ⇒ True49 | _ ⇒ False47 | Call _ ⇒ true 48 | Jmp _ ⇒ true 49 | _ ⇒ false 50 50 ]. 51 51 … … 53 53 λinstr:pseudo_instruction. 54 54 match instr with 55 [ Call _ ⇒ True56 | _ ⇒ False55 [ Call _ ⇒ true 56 | _ ⇒ false 57 57 ]. 58 58 … … 258 258 match j with 259 259 [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧ 260 ¬is_call instr260 bool_to_Prop (¬is_call instr) 261 261 | absolute_jump ⇒ \fst (absolute_jump_cond pc_plus_jmp_length addr) = true ∧ 262 262 \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ 263 ¬is_relative_jump instr263 bool_to_Prop (¬is_relative_jump instr) 264 264 | long_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ 265 265 \fst (absolute_jump_cond pc_plus_jmp_length addr) = false … … 360 360 then short_jump 361 361 else select_call_length labels old_sigma inc_sigma added ppc lbl. 362 362 363 definition destination_of: preinstruction Identifier → option Identifier ≝ 364 λi. 365 match i with 366 [ JC j ⇒ Some ? j 367 | JNC j ⇒ Some ? j 368 | JZ j ⇒ Some ? j 369 | JNZ j ⇒ Some ? j 370 | JB _ j ⇒ Some ? j 371 | JBC _ j ⇒ Some ? j 372 | JNB _ j ⇒ Some ? j 373 | CJNE _ j ⇒ Some ? j 374 | DJNZ _ j ⇒ Some ? j 375 | _ ⇒ None ? 376 ]. 377 363 378 definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map → 364 379 ℕ → ℕ → preinstruction Identifier → option jump_length ≝ 365 380 λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi. 366 match i with 367 [ JC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 368 | JNC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 369 | JZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 370 | JNZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 371 | JB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 372 | JBC _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 373 | JNB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 374 | CJNE _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 375 | DJNZ _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 376 | _ ⇒ None ? 377 ]. 378 379 lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x). 380 #i cases i 381 [#id cases id 382 [1,2,3,6,7,33,34: 383 #x #y %2 whd in match (is_jump ?); /2 by nmk/ 384 |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: 385 #x %2 whd in match (is_jump ?); /2 by nmk/ 386 |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/ 387 |9,10,14,15: #x %1 / by I/ 388 |11,12,13,16,17: #x #y %1 / by I/ 389 ] 390 |2,3: #x %2 /2 by nmk/ 391 |4,5: #x %1 / by I/ 392 |6: #x #y %2 /2 by nmk/ 393 ] 394 qed. 381 match destination_of i with 382 [ Some j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 383 | None ⇒ None ? 384 ]. 395 385 396 386 (* The first step of the jump expansion: everything to short. *) … … 599 589 #a #b #i cases i 600 590 [1: #pi cases pi 601 [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: 602 try (#x #y #H #_) try (#x #H #_) try (#H #_) cases H 603 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #_ try (#_ %) 604 try (#abs normalize in abs; destruct (abs) @I) 605 cases a; cases b; try (#_ %) try (#abs normalize in abs; destruct(abs) @I) 606 try (@(subaddressing_mode_elim … x) #w #abs normalize in abs; destruct (abs) @I) 607 cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w 608 try ( #abs normalize in abs; destruct (abs) @I) 609 @(subaddressing_mode_elim … a1) #w2 #abs normalize in abs; destruct (abs) 610 ] 591 try (#x #y #H #EQ) try (#x #H #EQ) try (#H #EQ) cases H 592 cases a in EQ; cases b #EQ try % 593 try (normalize in EQ; destruct(EQ) @False) 594 try (lapply EQ @(subaddressing_mode_elim … x) #w #EQ normalize in EQ; destruct(EQ) @False) 595 lapply EQ -EQ cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w 596 try (#EQ normalize in EQ; destruct(EQ) @False) 597 @(subaddressing_mode_elim … a1) #w 598 #EQ normalize in EQ; destruct(EQ) 611 599 |2,3,6: #x [3: #y] #H cases H 612 |4,5: #id #_ cases a cases b 613 [2,3,4,6,11,12,13,15: normalize #H destruct (H) 614 |1,5,7,8,9,10,14,16,17,18: #H / by refl/ 615 ] 616 ] 600 |4,5: #id #_ cases a cases b #H try % normalize in H; destruct(H) 601 ] 617 602 qed. 618 603 … … 623 608 |4,5: #id #_ cases a cases b / by le_n/ 624 609 |1: #pi cases pi 625 [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: 626 try (#x #y #H) try (#x #H) try (#H) cases H 627 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 628 #_ cases a cases b 629 [1,4,5,6,7,8,9: / by le_n/ 630 |10,13,14,15,16,17,18: / by le_n/ 631 |19,22,23,24,25,26,27: / by le_n/ 632 |28,31,32,33,34,35,36: / by le_n/ 633 |37,40,41,42,43,44,45: / by le_n/ 634 |46,47,48,49,50,51,52,53,54: / by le_n/ 635 |55,56,57,58,59,60,61,62,63: / by le_n/ 636 |64,65,66,67,68,69,70,71,72: / by le_n/ 637 |73,74,75,76,77,78,79,80,81: / by le_n/ 638 ] 639 try (@(subaddressing_mode_elim … x) #w normalize @le_S @le_S @le_S @le_S @le_S @le_n) 640 cases x * #ad 641 try (@(subaddressing_mode_elim … ad) #w #z normalize @le_S @le_S @le_S @le_S @le_S @le_n) 642 #z @(subaddressing_mode_elim … z) #w normalize / by / 643 ] 610 try (#x #y #H) try (#x #H) try (#H) cases H 611 -H cases a cases b @leb_true_to_le try % 612 try (@(subaddressing_mode_elim … x) #w % @False) 613 cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try % 614 @(subaddressing_mode_elim … a1) #w % 644 615 ] 645 616 qed. … … 701 672 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 702 673 cases (get_index' bool 2 0 flags) normalize nodelta 703 [3,4: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/674 [3,4: #H cases (proj2 ?? H) 704 675 |1,2: cases (eq_bv 9 upper ?) 705 676 [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3) … … 761 732 ] 762 733 ] 763 |1: #pi cases pi 764 [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: 765 [1,2,3,6,7,24,25: #x #y 766 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 767 normalize nodelta #H #Heq @refl 768 |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x] 769 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 770 #Hj #Heq lapply (Hj x (refl ? x)) -Hj 734 |1: cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a)) 735 [#A #B * / by refl/] #fst_foo 736 cut (∀x. 737 instruction_has_label x (\snd (nth i labelled_instruction program 〈None (identifier ASMTag),Comment []〉)) → 738 lookup_def ?? (create_label_map program) x 0 ≤ (|program|)) 739 [#x #Heq cases (create_label_map program) #clm #Hclm 740 @le_S_to_le @(proj2 ?? (Hclm x ?)) 741 @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??) 742 [ >nat_of_bitvector_bitvector_of_nat_inverse 743 [2: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 744 | whd in match fetch_pseudo_instruction; normalize nodelta 745 >nth_safe_nth 746 [ >nat_of_bitvector_bitvector_of_nat_inverse 747 [ @pair_elim // ] 748 @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi ] 749 | assumption ]] #lookup_in_program 750 -H #pi cases pi 751 try (#y #x #H #Heq) try (#x #H #Heq) try (#H #Heq) try % 752 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in H; 753 #Hj lapply (Hj x (refl ? x)) -Hj 771 754 whd in match expand_relative_jump; normalize nodelta 772 755 whd in match expand_relative_jump_internal; normalize nodelta … … 776 759 <(plus_n_Sm i 0) <plus_n_O <plus_n_O cases x2 normalize nodelta 777 760 [1,4,7,10,13,16,19,22,25: 778 cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a)) 779 [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ] 780 #fst_foo >fst_foo @pair_elim #sj_possible #disp #H #H2 761 >fst_foo @pair_elim #sj_possible #disp #H #H2 781 762 @(pair_replace ?????????? (eq_to_jmeq … H)) 782 [1,3,5,7,9,11,13,15,17: 783 cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|)) 784 [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm 785 @le_S_to_le @(proj2 ?? (Hclm x ?)) 786 @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??) 787 [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse 788 [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 789 |2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta 790 >nth_safe_nth 791 [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse 792 [1,3,5,7,9,11,13,15,17: >Heq %] 793 @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi 794 ] 795 ] 796 >Heq / by / 797 ] 798 #X >(le_to_leb_true … X) @refl 799 ] 763 [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …)) 764 try % >Heq % ] 800 765 >(proj1 ?? H2) try (@refl) normalize nodelta 801 766 [1,2,3,5: @(subaddressing_mode_elim … y) #w % … … 803 768 @(subaddressing_mode_elim … sth2) #x [3,4: #x2] % 804 769 ] 805 |2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs #abs2 @⊥ @abs2 / by I/770 |2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs 806 771 ] 807 cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a)) 808 [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ] 809 #fst_foo * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H 772 * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H 810 773 @(pair_replace ?????????? (eq_to_jmeq … H)) 811 [1,3,5,7,9,11,13,15,17: 812 cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|)) 813 [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm 814 @le_S_to_le @(proj2 ?? (Hclm x ?)) 815 @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??) 816 [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse 817 [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 818 |2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta 819 >nth_safe_nth 820 [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse 821 [1,3,5,7,9,11,13,15,17: >Heq %] 822 @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi 823 ] 824 ] 825 >Heq / by / 826 ] 827 #X >(le_to_leb_true … X) @refl 828 ] 774 [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …)) 775 try % >Heq % ] 829 776 #H2 >H2 try (@refl) normalize nodelta 830 777 [1,2,3,5: @(subaddressing_mode_elim … y) #w % … … 832 779 [1,2: %] whd in match (map ????); whd in match (flatten ??); 833 780 whd in match (map ????) in ⊢ (???%); whd in match (flatten ??) in ⊢ (???%); 834 >length_append >length_append @eq_f2 % 835 ] 836 ] 837 ] 838 ] 839 ] 840 ] 781 >length_append >length_append %]]]]] 841 782 qed. 842 783 … … 845 786 #i cases i 846 787 [2,3,6: #x [3: #y] #Hj #j1 #j2 % 847 |4,5: #x #Hi cases Hi #abs @⊥ @abs @I 848 |1: #pi cases pi 849 [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: 850 [1,2,3,6,7,24,25: #x #y 851 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 852 #Hj #j1 #j2 % 853 |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x] 854 #Hi cases Hi #abs @⊥ @abs @I 855 ] 856 ] 857 qed. 788 |4,5: #x #Hi cases Hi 789 |1: #pi cases pi try (#x #y #Hj #j1 #j2) try (#y #Hj #j1 #j2) try (#Hj #j1 #j2) 790 try % cases Hj ] 791 qed. -
src/ASM/PolicyStep.ma
r2220 r2225 4 4 include alias "basics/logic.ma". 5 5 6 lemma not_is_jump_to_destination_of_Nome: 7 ∀pi. ¬is_jump (Instruction pi) → destination_of pi = None …. 8 * try (#x #y #H) try (#y #H) try #H cases H % 9 qed. 10 6 11 lemma jump_expansion_step1: 7 ∀program : Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l. 8 ∀prefix,x,tl. pi1 … program=prefix@[x]@tl → 12 ∀prefix: list labelled_instruction. S (|prefix|) < 2^16 → |prefix| < 2^16 → (*redundant*) 9 13 ∀labels: label_map. 10 14 ∀old_sigma : ppc_pc_map. … … 38 42 = policy. 39 43 not_jump_default (prefix@[〈label,instr〉]) policy. 40 #pr ogram #prefix #x #tl #prf#labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc41 #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2 44 #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc 45 #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2 42 46 #i >append_length <commutative_plus #Hi normalize in Hi; 43 47 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi … … 46 50 [ >(nth_append_first ? i prefix ?? Hi) 47 51 @(Hpolicy i Hi) 48 | @bitvector_of_nat_abs 49 [ @(transitive_lt ??? Hi) ] 50 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 51 @le_plus_n_r 52 | @lt_to_not_eq @Hi 53 ] 52 | @bitvector_of_nat_abs try assumption 53 [ @(transitive_lt ??? Hi) assumption ] 54 @lt_to_not_eq @Hi 54 55 ] 55 | @bitvector_of_nat_abs 56 [ @(transitive_lt ??? Hi) @le_S_to_le ] 57 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length 58 <plus_n_Sm @le_S_S @le_plus_n_r 59 | @lt_to_not_eq @le_S @Hi 60 ] 56 | @bitvector_of_nat_abs try assumption 57 [ @(transitive_lt ??? Hi) assumption ] 58 @lt_to_not_eq @le_S @Hi 61 59 ] 62 60 | <Heq2 >Hi >lookup_insert_miss 63 61 [ >lookup_insert_hit cases instr in Heq1; 64 62 [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl 65 |4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second 66 [1,3: <minus_n_n whd in match (nth ????); % 67 |2,4: @le_n 68 ] 69 |1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi 70 [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: 71 [1,2,3,6,7,24,25: #x #y 72 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1 73 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl 74 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta 75 #_ #H @⊥ cases H #H2 @H2 % 76 ] 77 ] 78 | @bitvector_of_nat_abs 79 [ @le_S_to_le ] 80 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S 81 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 82 | @lt_to_not_eq @le_n 83 ] 84 ] 85 ] 63 |4,5: #x normalize nodelta #Heq1 >nth_append_second try % 64 <minus_n_n #abs cases abs 65 |1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); 66 #H #non_jump whd in match (jump_expansion_step_instruction ??????) in H; 67 >not_is_jump_to_destination_of_Nome in H; normalize nodelta // ] 68 | @bitvector_of_nat_abs [3: // | @le_S_to_le ] assumption ]] 86 69 qed. 70 71 lemma jump_expansion_step2: 72 ∀prefix: list labelled_instruction. S (|prefix|) < 2^16 → |prefix| < 2^16 → (*redundant*) 73 ∀labels : label_map. 74 ∀old_sigma : ppc_pc_map. 75 ∀inc_pc : ℕ. 76 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16). 77 ∀Hpolicy1 : 78 \fst (lookup … (bitvector_of_nat … O) inc_sigma 〈O,short_jump〉) = O. 79 ∀Hpolicy2: 80 inc_pc =\fst (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉). 81 ∀policy : ppc_pc_map. 82 ∀new_length : jump_length. 83 ∀isize : ℕ. 84 ∀Heq2 : 85 〈inc_pc+isize, 86 insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) 87 〈inc_pc+isize, 88 \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) 89 (\snd old_sigma) 〈O,short_jump〉)〉 90 (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 91 〈inc_pc,new_length〉 inc_sigma)〉 92 = policy. 93 \fst (lookup … (bitvector_of_nat … O) (\snd policy) 〈O,short_jump〉) = O. 94 #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_pc 95 #inc_sigma #Hpolicy1 #Hpolicy2 #policy #new_length #isize #Heq2 96 <Heq2 >lookup_insert_miss 97 [ cases (decidable_eq_nat 0 (|prefix|)) 98 [ #Heq <Heq >lookup_insert_hit >Hpolicy2 <Heq @Hpolicy1 99 | #Hneq >lookup_insert_miss 100 [ @Hpolicy1 101 | @bitvector_of_nat_abs try assumption @lt_O_S ]] 102 | @bitvector_of_nat_abs [ @lt_O_S | @prefix_ok1 | 3: @lt_to_not_eq @lt_O_S ] ] 103 qed. 104 105 (* 106 lemma jump_expansion_step3: 107 (* 108 program : 109 (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l) 110 labels : 111 (Σlm:label_map 112 .(∀l:identifier ASMTag 113 .occurs_exactly_once ASMTag pseudo_instruction l program 114 →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O) 115 =address_of_word_labels_code_mem program l))*) 116 ∀old_sigma : 117 Σpolicy:ppc_pc_map 118 .True(*not_jump_default program policy 119 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 120 〈O,short_jump〉) 121 =O 122 ∧\fst policy 123 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|)) 124 (\snd policy) 〈O,short_jump〉) 125 ∧sigma_compact_unsafe program labels policy 126 ∧\fst policy≤ 2 \sup 16*). 127 ∀prefix : list (option Identifier×pseudo_instruction). (* 128 x : (option Identifier×pseudo_instruction) 129 tl : (list (option Identifier×pseudo_instruction)) 130 prf : (program=prefix@[x]@tl) 131 acc : 132 (Σx0:ℕ×ppc_pc_map 133 .(let 〈added,policy〉 ≝x0 in 134 not_jump_default prefix policy 135 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 136 〈O,short_jump〉) 137 =O 138 ∧\fst policy 139 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 140 (\snd policy) 〈O,short_jump〉) 141 ∧jump_increase prefix old_sigma policy 142 ∧sigma_compact_unsafe prefix labels policy 143 ∧(sigma_jump_equal prefix old_sigma policy→added=O) 144 ∧(added=O→sigma_pc_equal prefix old_sigma policy) 145 ∧out_of_program_none prefix policy 146 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 147 (\snd policy) 〈O,short_jump〉) 148 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 149 (\snd old_sigma) 〈O,short_jump〉) 150 +added 151 ∧sigma_safe prefix labels added old_sigma policy)) 152 inc_added : ℕ 153 inc_pc_sigma : ppc_pc_map 154 p : (acc≃〈inc_added,inc_pc_sigma〉)*) 155 ∀label : option Identifier. 156 ∀instr : pseudo_instruction.(* 157 p1 : (x≃〈label,instr〉) 158 add_instr ≝ 159 match instr 160 in pseudo_instruction 161 return λ_:pseudo_instruction.(option jump_length) 162 with 163 [Instruction (i:(preinstruction Identifier))⇒ 164 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 165 (|prefix|) i 166 |Comment (_:String)⇒None jump_length 167 |Cost (_:costlabel)⇒None jump_length 168 |Jmp (j:Identifier)⇒ 169 Some jump_length 170 (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j) 171 |Call (c:Identifier)⇒ 172 Some jump_length 173 (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c) 174 |Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 175 inc_pc : ℕ 176 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16) 177 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉) 178 old_pc : ℕ 179 old_length : jump_length 180 Holdeq : 181 (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd old_sigma) 182 〈O,short_jump〉 183 =〈old_pc,old_length〉) 184 Hpolicy : 185 (not_jump_default prefix 〈inc_pc,inc_sigma〉 186 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma 187 〈O,short_jump〉) 188 =O 189 ∧inc_pc 190 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma 191 〈O,short_jump〉) 192 ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉 193 ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉 194 ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O) 195 ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉) 196 ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉 197 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma 198 〈O,short_jump〉) 199 =old_pc+inc_added 200 ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉) 201 added : ℕ*) 202 ∀policy : ppc_pc_map. 203 (*new_length : jump_length 204 isize : ℕ 205 Heq1 : 206 (match 207 match instr 208 in pseudo_instruction 209 return λ_:pseudo_instruction.(option jump_length) 210 with 211 [Instruction (i:(preinstruction Identifier))⇒ 212 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 213 (|prefix|) i 214 |Comment (_:String)⇒None jump_length 215 |Cost (_:costlabel)⇒None jump_length 216 |Jmp (j:Identifier)⇒ 217 Some jump_length 218 (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j) 219 |Call (c:Identifier)⇒ 220 Some jump_length 221 (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c) 222 |Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 223 in option 224 return λ_0:(option jump_length).(jump_length×ℕ) 225 with 226 [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 227 |Some (pl:jump_length)⇒ 228 〈max_length old_length pl, 229 instruction_size_jmplen (max_length old_length pl) instr〉] 230 =〈new_length,isize〉) 231 prefix_ok1 : (S (|prefix|)< 2 \sup 16 ) 232 prefix_ok : (|prefix|< 2 \sup 16 ) 233 Heq2a : 234 (match 235 match instr 236 in pseudo_instruction 237 return λ_0:pseudo_instruction.(option jump_length) 238 with 239 [Instruction (i:(preinstruction Identifier))⇒ 240 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 241 (|prefix|) i 242 |Comment (_0:String)⇒None jump_length 243 |Cost (_0:costlabel)⇒None jump_length 244 |Jmp (j:Identifier)⇒ 245 Some jump_length 246 (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j) 247 |Call (c:Identifier)⇒ 248 Some jump_length 249 (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c) 250 |Mov (_0:[[dptr]]) (_00:Identifier)⇒None jump_length] 251 in option 252 return λ_0:(option jump_length).ℕ 253 with 254 [None⇒inc_added 255 |Some (x0:jump_length)⇒ 256 inc_added+(isize-instruction_size_jmplen old_length instr)] 257 =added) 258 Heq2b : 259 (〈inc_pc+isize, 260 insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) 261 〈inc_pc+isize, 262 \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) 263 (\snd old_sigma) 〈O,short_jump〉)〉 264 (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 265 〈inc_pc,new_length〉 inc_sigma)〉 266 =policy)*) 267 jump_increase (prefix@[〈label,instr〉]) old_sigma policy. 268 #old_sigma #prefix #label #instr #policy 269 #i >append_length >commutative_plus #Hi normalize in Hi; 270 cases (le_to_or_lt_eq … Hi) -Hi; #Hi 271 [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 272 [ (* USE[pass]: jump_increase *) 273 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi)) 274 <(proj2 ?? (pair_destruct ?????? Heq2)) 275 @pair_elim #opc #oj #EQ1 >lookup_insert_miss 276 [ >lookup_insert_miss 277 [ @pair_elim #pc #j #EQ2 #X @X 278 | @bitvector_of_nat_abs 279 [ @(transitive_lt ??? Hi) ] 280 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 281 @le_S_S @le_plus_n_r 282 | @lt_to_not_eq @Hi 283 ] 284 ] 285 | @bitvector_of_nat_abs 286 [ @(transitive_lt ??? Hi) @le_S_to_le ] 287 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 288 >append_length @le_S_S <plus_n_Sm @le_plus_n_r 289 | @lt_to_not_eq @le_S @Hi 290 ] 291 ] 292 | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >Holdeq normalize nodelta 293 >lookup_insert_miss 294 [ >lookup_insert_hit cases (dec_is_jump instr) 295 [ cases instr in Heq1; normalize nodelta 296 [ #pi cases pi 297 [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: 298 [1,2,3,6,7,24,25: #x #y 299 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj 300 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 301 whd in match jump_expansion_step_instruction; normalize nodelta #Heq1 302 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) 303 @jmpleq_max_length 304 ] 305 |2,3,6: #x [3: #y] #_ #Hj cases Hj 306 |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length 307 ] 308 | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta 309 [ #pi cases pi 310 [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: 311 [1,2,3,6,7,24,25: #x #y 312 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 313 whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1 314 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 315 (* USE: not_jump_default (from old_sigma) *) 316 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??) 317 [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: 318 >prf >nth_append_second 319 [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: 320 <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 321 |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: 322 @le_n 323 ] 324 |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 325 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 326 |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: 327 >Holdeq #EQ2 >EQ2 %2 @refl 328 ] 329 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 330 #_ #_ #abs @⊥ @(absurd ? I abs) 331 ] 332 |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 333 (* USE: not_jump_default (from old_sigma) *) 334 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??) 335 [1,4,7: >prf >nth_append_second 336 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 337 |2,4,6: @le_n 338 ] 339 |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 340 |3,6,9: >Holdeq #EQ2 >EQ2 %2 @refl 341 ] 342 |4,5: #x #_ #_ #abs @⊥ @(absurd ? I abs) 343 ] 344 ] 345 | @bitvector_of_nat_abs 346 [ @le_S_to_le ] 347 [1,2: @(transitive_lt … (proj1 ?? (pi2 … program))) @le_S_S >prf 348 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 349 | @lt_to_not_eq @le_n 350 ] 351 ] 352 ] 353 | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit 354 normalize nodelta 355 cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉) 356 #a #b normalize nodelta %2 @refl 357 ] 358 ] 359 qed.*) 87 360 88 361 (* One step in the search for a jump expansion fixpoint. *) … … 190 463 [ (* USE: policy_jump_equal → added = 0 (from fold) *) 191 464 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi 192 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))465 inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 193 466 [ #Hj 194 467 (* USE: policy_increase (from fold) *) 195 468 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi)) 196 lapply (Habs i Hi Hj)469 lapply (Habs i Hi ?) [ >Hj %] 197 470 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉) 198 471 #opc #oj … … 204 477 | #Hnj 205 478 (* USE: not_jump_default (from fold and old_sigma) *) 206 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi Hnj) 207 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj) 208 @refl 479 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi ?) 480 [2: >Hnj %] 481 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi ?) try % 482 >Hnj % 209 483 ] 210 484 | #abs >abs in Hsig; #Hsig … … 232 506 #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta 233 507 #Heq1 #Heq2 234 @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 508 cut (S (|prefix|) < 2^16) 509 [ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length 510 <plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1 511 cut (|prefix| < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok 512 cases (pair_destruct ?????? Heq2) -Heq2 #Heq2a #Heq2b 513 % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]] 235 514 (* NOTE: to save memory and speed up work, there's cases daemon here. They can be 236 515 * commented out for full proofs, but this needs a lot of memory and time *) 237 516 [ (* not_jump_default *) 238 cases (pair_destruct ?????? Heq2) -Heq2 #_ #Heq2 239 @(jump_expansion_step1 … prf … Heq1 Heq2) 517 @(jump_expansion_step1 … Heq1 Heq2b) try assumption 240 518 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) 241 519 | (* 0 ↦ 0 *) 242 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 243 [ cases (decidable_eq_nat 0 (|prefix|)) 244 [ #Heq <Heq >lookup_insert_hit 245 (* USE: inc_pc = fst policy *) 246 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 247 <Heq 248 (* USE[pass]: 0 ↦ 0 *) 249 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) 250 | #Hneq >lookup_insert_miss 251 [ (* USE[pass]: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) 252 | @bitvector_of_nat_abs 253 [3: @Hneq] 254 ] 255 ] 256 | @bitvector_of_nat_abs 257 [3: @lt_to_not_eq @lt_O_S ] 258 ] 259 [1,3: @lt_O_S 260 |2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 261 [2: <plus_n_Sm @le_S_S] 262 @le_plus_n_r 263 ] 264 ] 265 | (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2)) 266 >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl 267 ] 268 | (* jump_increase *) (* cases daemon *) 269 #i >append_length >commutative_plus #Hi normalize in Hi; 270 cases (le_to_or_lt_eq … Hi) -Hi; #Hi 271 [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 272 [ (* USE[pass]: jump_increase *) 273 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi)) 274 <(proj2 ?? (pair_destruct ?????? Heq2)) 275 @pair_elim #opc #oj #EQ1 >lookup_insert_miss 276 [ >lookup_insert_miss 277 [ @pair_elim #pc #j #EQ2 #X @X 278 | @bitvector_of_nat_abs 279 [ @(transitive_lt ??? Hi) ] 280 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 281 @le_S_S @le_plus_n_r 282 | @lt_to_not_eq @Hi 283 ] 284 ] 285 | @bitvector_of_nat_abs 286 [ @(transitive_lt ??? Hi) @le_S_to_le ] 287 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 288 >append_length @le_S_S <plus_n_Sm @le_plus_n_r 289 | @lt_to_not_eq @le_S @Hi 290 ] 291 ] 292 | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >Holdeq normalize nodelta 293 >lookup_insert_miss 294 [ >lookup_insert_hit cases (dec_is_jump instr) 295 [ cases instr in Heq1; normalize nodelta 296 [ #pi cases pi 297 [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: 298 [1,2,3,6,7,24,25: #x #y 299 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj 300 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 301 whd in match jump_expansion_step_instruction; normalize nodelta #Heq1 302 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) 303 @jmpleq_max_length 304 ] 305 |2,3,6: #x [3: #y] #_ #Hj cases Hj 306 |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length 307 ] 308 | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta 309 [ #pi cases pi 310 [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: 311 [1,2,3,6,7,24,25: #x #y 312 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 313 whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1 314 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 315 (* USE: not_jump_default (from old_sigma) *) 316 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??) 317 [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: 318 >prf >nth_append_second 319 [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: 320 <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 321 |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: 322 @le_n 323 ] 324 |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 325 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 326 |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: 327 >Holdeq #EQ2 >EQ2 %2 @refl 328 ] 329 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 330 #_ #_ #abs @⊥ @(absurd ? I abs) 331 ] 332 |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 333 (* USE: not_jump_default (from old_sigma) *) 334 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??) 335 [1,4,7: >prf >nth_append_second 336 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 337 |2,4,6: @le_n 338 ] 339 |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 340 |3,6,9: >Holdeq #EQ2 >EQ2 %2 @refl 341 ] 342 |4,5: #x #_ #_ #abs @⊥ @(absurd ? I abs) 343 ] 344 ] 345 | @bitvector_of_nat_abs 346 [ @le_S_to_le ] 347 [1,2: @(transitive_lt … (proj1 ?? (pi2 … program))) @le_S_S >prf 348 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 349 | @lt_to_not_eq @le_n 350 ] 351 ] 352 ] 353 | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit 354 normalize nodelta 355 cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉) 356 #a #b normalize nodelta %2 @refl 357 ] 358 ] 359 | (* sigma_compact_unsafe *) 520 @(jump_expansion_step2 … Heq2b) try assumption 521 [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) 522 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) ] 523 | (* inc_pc = fst of policy *) 524 <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl 525 | (* jump_increase *) 526 cases daemon (*XXX*) 527 | (* sigma_compact_unsafe *) cases daemon (* 360 528 #i >append_length <commutative_plus #Hi normalize in Hi; 361 529 <(proj2 ?? (pair_destruct ?????? Heq2)) … … 461 629 ] 462 630 ] 463 ] 464 | (* policy_jump_equal → added = 0 *) 631 ] *) 632 | (* policy_jump_equal → added = 0 *) cases daemon (* 465 633 <(proj2 ?? (pair_destruct ?????? Heq2)) 466 634 #Heq <(proj1 ?? (pair_destruct ?????? Heq2)) … … 530 698 ] 531 699 ] 532 ] 700 ] *) 533 701 | (* added = 0 → policy_pc_equal *) cases daemon 534 702 (* USE[pass]: added = 0 → policy_pc_equal *) … … 831 999 ] 832 1000 ] *) 833 ]834 1001 | (* out_of_program_none *) cases daemon 835 1002 (* #i #Hi2 >append_length <commutative_plus @conj … … 870 1037 ] 871 1038 ] *) 872 ]873 1039 | (* lookup p = lookup old_sigma + added *) cases daemon 874 1040 (* <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O … … 1003 1169 ] 1004 1170 ] *) 1005 ]1006 1171 | (* sigma_safe *) cases daemon (*#i >append_length >commutative_plus #Hi normalize in Hi; 1007 1172 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi … … 1024 1189 [1,4,7: *) 1025 1190 1026 ] 1027 | normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj1191 ] 1192 | normalize nodelta % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]] 1028 1193 [ #i cases i 1029 1194 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1030 1195 | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O 1031 1196 ] 1197 | >lookup_insert_hit @refl 1032 1198 | >lookup_insert_hit @refl 1033 ]1034 | >lookup_insert_hit @refl1035 ]1036 1199 | #i #Hi <(le_n_O_to_eq … Hi) 1037 1200 >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉) 1038 1201 #a #b normalize nodelta %2 @refl 1039 ]1040 1202 | #i cases i 1041 1203 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1042 1204 | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1043 1205 ] 1044 ]1045 1206 | #_ % 1046 ]1047 1207 | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit 1048 1208 (* USE: 0 ↦ 0 (from old_sigma) *) 1049 1209 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) 1050 ]1051 1210 | #i cases i 1052 1211 [ #Hi2 @conj … … 1066 1225 ] 1067 1226 ] 1068 ]1069 1227 | >lookup_insert_hit (* USE: 0 ↦ 0 (from old_sigma) *) 1070 1228 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) <plus_n_O % 1071 ]1072 1229 | #i cases i 1073 1230 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O … … 1077 1234 ] 1078 1235 qed. 1079
Note: See TracChangeset
for help on using the changeset viewer.