Changeset 3078

Timestamp:

Apr 3, 2013, 3:01:54 PM (6 years ago)

Author:

tranquil

Message:

fixed change of Mov

Location:

src/ASM

Files:

• Policy.ma (modified) (1 diff)
• PolicyFront.ma (modified) (1 diff)

src/ASM/Policy.ma

@@ -640 +640 @@
  [ <plus_n_O #_ @le_n
  | -n #n <plus_n_Sm #Hind #H @(transitive_le ??? (Hind (le_S_to_le … H)))
-   lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (λx.zero 16) (i+n) H)
-   lapply (refl ? (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)))
-   cases (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)) in ⊢ (???% → %);
-   [ normalize nodelta #_ #abs cases abs
-   | #x cases x -x #pc #jl #EQ normalize nodelta
-     lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)))
-     cases (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)) in ⊢ (???% → %);
-     [ normalize nodelta #_ #abs cases abs
-     | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hcomp
+   lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (λx.〈XData, bv_zero 16〉) (i+n) H)
+   inversion (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol))
+   [ normalize nodelta #_ *
+   | * #pc #jl #EQ normalize nodelta
+     inversion (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol))
+     [ normalize nodelta #_ *
+     | * #Spc #Sjl #SEQ normalize nodelta #Hcomp
        >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
        >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hcomp @le_plus_n_r

src/ASM/PolicyFront.ma

@@ -661 +661 @@
               try % lapply Hsafe -Hsafe lapply Hnth_eq -Hnth_eq lapply id -id
           |2,3,5: #x [3: #y #z | 4: #y] normalize nodelta #_ #_ %
-          |7: * [ #x normalize nodelta #y #z #_ #_ % ]
-            * #x @(subaddressing_mode_elim … x) [2,3: #y] * #lbl #off
-            normalize nodelta #_ #_ lapply (vsplit ? 8 8 ?) * #w1 #w2 % ]
+          |7: *
+            [ #x @(subaddressing_mode_elim … x)
+            | * #x  @(subaddressing_mode_elim … x) [2,3: #y] *
+            ] normalize nodelta #lbl #off #_ #_
+            @pair_elim * #addr normalize nodelta #_ %
+          ]
             #id lapply (Hpc_equal i (le_S_to_le … Hi))
             lapply (Hpc_equal (S i) Hi)