Changeset 2282 for src/ASM/AssemblyProofSplit.ma

Timestamp:

Jul 31, 2012, 6:08:00 PM (9 years ago)

Author:

sacerdot

Message:

PUSH case almost finished

File:

• src/ASM/AssemblyProofSplit.ma (modified) (2 diffs)

src/ASM/AssemblyProofSplit.ma

@@ -1157 +1157 @@
       ]
     ]
-  |*)12: (* JC *)
+  |12: (* JC *)
     >EQP -P normalize nodelta
     whd in match assembly_1_pseudoinstruction; normalize nodelta
@@ -1923 +1923 @@
     cases bitone #bit_one_seven_bits_refl normalize nodelta
     [ @eq_bv_elim #seven_bits_refl normalize nodelta
-    | inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry]
+    | FUFFA inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry]
       #lookup_from_internal_ram_refl ]
-    @Some_Some_elim #Mrefl destruct(Mrefl) #fetch_many_assm %{1}
+    @Some_Some_elim #Mrefl <Mrefl -M' #fetch_many_assm %{1}
     whd in ⊢ (??%?);
     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
-    whd in ⊢ (??%?);
-    @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta
-    @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl))
-    [1,3,5,7:
-      @eq_f2 try %
-      @(pose … (set_clock ????)) #status #status_refl
-      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl -status_refl try %
-      @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
-    |*:
-      >EQs >EQticks <instr_refl
-      @(write_at_stack_pointer_status_of_pseudo_status 〈low,high,accA〉)
-      [2,4,6,8: @set_8051_sfr_status_of_pseudo_status try %
-      | >get_8051_sfr_set_8051_sfr
-        cut (new_sp = (add … (get_8051_sfr … ps SFR_SP) (bitvector_of_nat … 1)))
-        [ >(pair_destruct_2 ????? (sym_eq … carry_new_sp_refl))
-          change with (add ??? = ?); @eq_f2 try %
-          cases daemon (*CSC: use @get_8051_sfr_status_of_pseudo_status*) ] #EQnew_sp
-        >EQnew_sp
-        @internal_pseudo_address_map_equal_up_to_address_overwrite_or_delete_from_internal_ram
-        
-      
-         XXX
-        (*CSC: lemma here*)
-        cases accA
-        whd in match overwrite_or_delete_from_internal_ram; normalize nodelta
-        [ whd whd in match delete_from_internal_ram; normalize nodelta
-          @pair_elim #bit_one
-        |
-        ]
-      |
-      |
-      ]
+    whd in match execute_1_0; normalize nodelta
+    whd in match execute_1_preinstruction; normalize nodelta
+    >bit_one_seven_bits_refl
+    [ alias id "write_at_stack_pointer_accA" = "cic:/matita/cerco/ASM/Test3/write_at_stack_pointer_accA.def(29)".
+      >seven_bits_refl
+      @(write_at_stack_pointer_status_of_pseudo_status_accA … 〈low,high,accA〉)
+      [ @set_8051_sfr_status_of_pseudo_status >EQs >EQticks <instr_refl @(subaddressing_mode_elim … addr) #y
+        try %
+        change with (add ??? = ?); @eq_f2 try %
+        @(pose … (set_clock ????)) #status #status_refl
+        @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl %
+      | >EQs /demod nohyps/ >add_commutative % ]
+    |
+    |
+    |
     ]
   |43: (* POP *)