- Timestamp:
- Jul 23, 2012, 10:35:43 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Policy.ma
r2229 r2230 653 653 cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉) 654 654 #lbl #ins % ] 655 lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok) >bitvector_of_nat_inverse_nat_of_bitvector 656 inversion (lookup_opt ????) normalize nodelta [ #Hl #abs cases abs ] 657 * #pc #jl #Hl normalize nodelta 658 inversion (lookup_opt ????) normalize nodelta [ #Hl #abs cases abs ] 659 * #Spc #Sjl #SHL lapply SHL 660 <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative 661 #SHl normalize nodelta #Hcompact 655 662 @conj 656 [ lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok) 657 >bitvector_of_nat_inverse_nat_of_bitvector 658 inversion (lookup_opt ????) normalize nodelta 659 [ #Hl #abs cases abs 660 | * #pc #jl #Hl normalize nodelta <add_bitvector_of_nat_Sm 661 >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative 662 inversion (lookup_opt ????) normalize nodelta 663 [ #_ #abs cases abs 664 | * #Spc #Sjl #SHl normalize nodelta #Hcompact 665 >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta 666 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta 667 >add_bitvector_of_nat_plus >Hcompact % ]] 663 [ >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) 664 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) 665 >add_bitvector_of_nat_plus >Hcompact % 668 666 | (* Basic proof scheme: 669 667 - ppc < |snd program|, hence our instruction is in the program … … 676 674 elim (le_to_or_lt_eq … Hfpol4) #Hfpc 677 675 [ %1 @(le_to_lt_to_lt … Hfpc) >Hfpol2 678 lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok) 679 >bitvector_of_nat_inverse_nat_of_bitvector 680 inversion (lookup_opt ????) normalize nodelta 681 [ #_ #abs cases abs 682 | * #pc #jl #Hl normalize nodelta 683 inversion (lookup_opt ????) normalize nodelta 684 [ #_ #abs cases abs 685 | * #Spc #Sjl #SHl normalize nodelta #Hcompact 686 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta 687 >nat_of_bitvector_bitvector_of_nat_inverse 688 [2: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)) 689 >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) 690 #H @(le_to_lt_to_lt … Hfpc) >Hfpol2 @H ] 691 lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)) 692 >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) >Hcompact #X @X ]] 676 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) 677 >nat_of_bitvector_bitvector_of_nat_inverse 678 [2: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)) 679 >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) 680 #H @(le_to_lt_to_lt … Hfpc) >Hfpol2 @H ] 681 lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)) 682 >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >Hcompact #X @X 693 683 | (* the program is of length 2^16 and ppc is followed by only zero-size instructions 694 684 * until the end of the program *) 695 685 elim (le_to_or_lt_eq … (pc_increases (nat_of_bitvector ? ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))) 696 [ lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok) 697 >bitvector_of_nat_inverse_nat_of_bitvector 698 lapply (refl ? (lookup_opt … ppc fpol)) 699 cases (lookup_opt … ppc fpol) in ⊢ (???% → %); 700 [ #_ normalize nodelta #abs cases abs 701 | #x cases x -x #pc #jl #EQ normalize nodelta 702 lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol)) 703 cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %); 704 [ #_ normalize nodelta #abs cases abs 705 | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hc 706 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hpc normalize nodelta 707 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) 708 >nat_of_bitvector_bitvector_of_nat_inverse 709 [2: <Hfpc >Hfpol2 @Hpc ] 710 elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))) 711 <Hfpol2 >Hfpc >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #HSpc 712 [ %1 >Hc in HSpc; #X @X 713 | %2 @conj 714 [2: >Hc in HSpc; #X @X 715 | #ppc' #ppc_ok' #Hppc' 686 [ >bitvector_of_nat_inverse_nat_of_bitvector 687 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #Hpc normalize nodelta 688 >nat_of_bitvector_bitvector_of_nat_inverse 689 [2: <Hfpc >Hfpol2 @Hpc ] 690 elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))) 691 <Hfpol2 >Hfpc >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) #HSpc 692 [ %1 >Hcompact in HSpc; #X @X 693 | %2 @conj 694 [2: >Hcompact in HSpc; #X @X 695 | #ppc' #ppc_ok' #Hppc' 716 696 (* S ppc < ppc' < |\snd program| *) 717 697 (* lookup S ppc = 2^16 *) … … 728 708 #Hpcompact 729 709 lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok')) 730 >(lookup_opt_lookup_hit … S EQ〈0,short_jump〉) >HSpc #Hle1710 >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1 731 711 lapply (pc_increases (nat_of_bitvector ? ppc') (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?)) 732 712 <Hfpol2 >Hfpc #Hle2 … … 735 715 >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) #Hxpc 736 716 lapply (pc_increases (S (nat_of_bitvector ? ppc)) (S (nat_of_bitvector ? ppc')) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … (le_S_S … Hppc')) ppc_ok') 737 >(lookup_opt_lookup_hit … S EQ〈0,short_jump〉) >HSpc #Hle1717 >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1 738 718 lapply (pc_increases (S (nat_of_bitvector ? ppc')) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?)) 739 719 <Hfpol2 >Hfpc #Hle2 … … 747 727 ] 748 728 ] 749 ]750 ]751 729 ] 752 730 ] 753 731 | >bitvector_of_nat_inverse_nat_of_bitvector 754 <Hfpol2 >Hfpc 755 cases (lookup … ppc fpol 〈0,short_jump〉) #pc #jl normalize nodelta #Hpc%1 >Hpc732 <Hfpol2 >Hfpc >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #Hpc 733 %1 >Hpc 756 734 >bitvector_of_nat_exp_zero whd in match (nat_of_bitvector ? (zero ?)); 757 735 <plus_O_n whd in match instruction_size; normalize nodelta 758 lapply (refl ? (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?)) 759 [5: cases (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?) in ⊢ (???% → %); 760 #len #ins #Hass lapply (fst_snd_assembly_1_pseudoinstruction … Hass) 761 #Hli >Hli 762 lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc (λx0.zero 16) ?) 763 [5: >Hass / by / 764 ] 765 ] 736 inversion (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?) 737 #len #ins #Hass lapply (fst_snd_assembly_1_pseudoinstruction … Hass) 738 #Hli >Hli 739 lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc (λx0.zero 16) ?) 740 [5: >Hass / by / ] 766 741 ] 767 742 ]
Note: See TracChangeset
for help on using the changeset viewer.