Changeset 3078
- Timestamp:
- Apr 3, 2013, 3:01:54 PM (5 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.