Changeset 2225 for src/ASM/Policy.ma
- Timestamp:
- Jul 20, 2012, 6:15:40 PM (7 years ago)
- File:
-
- 1 edited
-
src/ASM/Policy.ma (modified) (22 diffs)
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 ]
Note: See TracChangeset
for help on using the changeset viewer.
