 Timestamp:
 Apr 3, 2013, 3:01:54 PM (7 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r2771 r3078 640 640 [ <plus_n_O #_ @le_n 641 641  n #n <plus_n_Sm #Hind #H @(transitive_le ??? (Hind (le_S_to_le … H))) 642 lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (λx.zero 16) (i+n) H) 643 lapply (refl ? (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol))) 644 cases (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)) in ⊢ (???% → %); 645 [ normalize nodelta #_ #abs cases abs 646  #x cases x x #pc #jl #EQ normalize nodelta 647 lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol))) 648 cases (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)) in ⊢ (???% → %); 649 [ normalize nodelta #_ #abs cases abs 650  #x cases x x #Spc #Sjl #SEQ normalize nodelta #Hcomp 642 lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (λx.〈XData, bv_zero 16〉) (i+n) H) 643 inversion (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)) 644 [ normalize nodelta #_ * 645  * #pc #jl #EQ normalize nodelta 646 inversion (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)) 647 [ normalize nodelta #_ * 648  * #Spc #Sjl #SEQ normalize nodelta #Hcomp 651 649 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 652 650 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hcomp @le_plus_n_r 
src/ASM/PolicyFront.ma
r3039 r3078 661 661 try % lapply Hsafe Hsafe lapply Hnth_eq Hnth_eq lapply id id 662 662 2,3,5: #x [3: #y #z  4: #y] normalize nodelta #_ #_ % 663 7: * [ #x normalize nodelta #y #z #_ #_ % ] 664 * #x @(subaddressing_mode_elim … x) [2,3: #y] * #lbl #off 665 normalize nodelta #_ #_ lapply (vsplit ? 8 8 ?) * #w1 #w2 % ] 663 7: * 664 [ #x @(subaddressing_mode_elim … x) 665  * #x @(subaddressing_mode_elim … x) [2,3: #y] * 666 ] normalize nodelta #lbl #off #_ #_ 667 @pair_elim * #addr normalize nodelta #_ % 668 ] 666 669 #id lapply (Hpc_equal i (le_S_to_le … Hi)) 667 670 lapply (Hpc_equal (S i) Hi)
Note: See TracChangeset
for help on using the changeset viewer.