Changeset 1582 for src/ASM/Interpret.ma

Timestamp:

Dec 1, 2011, 5:24:41 PM (8 years ago)

Author:

mulligan

Message:

more added to the proof of execute_1_preinstruction --- ~260 cases now reduced to less than 20

File:

• src/ASM/Interpret.ma (modified) (4 diffs)

src/ASM/Interpret.ma

@@ -148 +148 @@
 qed.
 
+lemma set_high_internal_ram_ignores_clock:
+  ∀m: Type[0].
+  ∀s: PreStatus m.
+  ∀ram: BitVectorTrie Byte 7.
+    clock … (set_high_internal_ram … s ram) = clock … s.
+  #m #s #ram %
+qed.
+
 lemma set_8051_sfr_ignores_clock:
   ∀M: Type[0].
@@ -156 +164 @@
   #M #s #sfr #v %
 qed.
-  
+
+lemma set_arg_1_ignores_clock:
+  ∀m: Type[0].
+  ∀s: PreStatus m.
+  ∀addr: [[bit_addr; carry]].
+  ∀bit: Bit.
+    clock … (set_arg_1 m s addr bit) = clock … s.
+  #m #s #addr #bit
+  whd in match set_arg_1; normalize nodelta
+  cases addr #subaddressing_mode
+  cases subaddressing_mode
+  try #assm1 try #assm2
+  try (normalize in assm2; cases assm2)
+  try (normalize in assm1; cases assm1)
+  normalize nodelta
+  cases (split bool 4 4 (get_8051_sfr m s SFR_PSW))
+  #nu #nl normalize nodelta
+  [ @set_8051_sfr_ignores_clock
+  | cases(split … 1 3 nu)
+    #ignore #three_bits normalize nodelta
+    cases(get_index_v … 4 nu 0 ?)
+    normalize nodelta
+    [ <set_bit_addressable_sfr_ignores_clock | >set_low_internal_ram_ignores_clock ] %
+  ]
+qed.
+
+lemma set_arg_16_ignores_clock:
+  ∀m: Type[0].
+  ∀s: PreStatus m.
+  ∀w: Word.
+  ∀addr: [[dptr]].
+    clock … (set_arg_16 m s w addr) = clock … s.
+  #m #s #w #addr
+  whd in match set_arg_16; normalize nodelta
+  cases addr #subaddressing_modein
+  cases subaddressing_modein
+  try #assm1 try #assm2
+  try (normalize in assm2; cases assm2)
+  try (normalize in assm1; cases assm1)
+  normalize nodelta
+  cases (split … 8 8 w) #bu #bl normalize nodelta
+  >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock %
+qed.
+
+lemma write_at_stack_pointer_ignores_clock:
+  ∀m: Type[0].
+  ∀s: PreStatus m.
+  ∀v: Byte.
+    clock … (write_at_stack_pointer m s v) = clock … s.
+  #m #s #v
+  whd in match write_at_stack_pointer; normalize nodelta
+  cases(split … 4 4 ?) #nu #nl normalize nodelta
+  cases(get_index_v … 4 nu 0 ?) normalize nodelta
+  [ >set_low_internal_ram_ignores_clock | >set_high_internal_ram_ignores_clock ] %
+qed.
+
 lemma clock_set_clock:
   ∀M: Type[0].
@@ -576 +639 @@
                   s
         ]. (*15s*)
-    try (destruct(other))
+    try (cases(other))
     try assumption (*20s*)
     try % (*6s*)
@@ -587 +650 @@
     try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock /demod/ %)
     try (normalize nodelta <set_flags_ignores_clock /demod/ %)
-    try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %)
     try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock @commutative_plus)
     try (/demod/ normalize nodelta >clock_set_clock @commutative_plus)
-    [5: /demod/ normalize nodelta >clock_set_clock >set_arg_1_ignores_clock 
-(* XXX: weird open goals here *)
-(*    [14: normalize nodelta <set_arg_8_ignores_clock /demod/ normalize nodelta
-    try (normalize nodelta /demod/ %)
     try (/demod/ normalize nodelta >clock_set_clock >set_arg_1_ignores_clock @commutative_plus)
-
-    try (normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %)*)
+    try (/demod/ normalize nodelta >clock_set_clock <set_arg_8_ignores_clock @commutative_plus)
+    try (/demod/ normalize nodelta >set_arg_1_ignores_clock >clock_set_clock @commutative_plus)
+    try (normalize nodelta >clock_set_clock >set_arg_1_ignores_clock >clock_set_clock %)
+    try (normalize nodelta <set_arg_8_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %)
+    try (normalize nodelta >set_arg_1_ignores_clock >clock_set_clock %)
+    try (normalize nodelta >clock_set_clock >set_arg_16_ignores_clock >clock_set_clock %)
+    try (normalize nodelta >set_arg_16_ignores_clock >clock_set_clock %)
     cases daemon
 qed.