Changeset 2276 for src/ASM/AssemblyProofSplit.ma

Timestamp:

Jul 30, 2012, 2:36:41 PM (8 years ago)

Author:

sacerdot

Message:

...

File:

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

src/ASM/AssemblyProofSplit.ma

@@ -56 +56 @@
 qed.
 
+lemma get_arg_8_status_of_pseudo_status':
+  ∀cm,ps,l.
+  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
+  ∀M. ∀sigma. ∀policy. ∀s.
+      s = status_of_pseudo_status M cm ps sigma policy →
+      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
+      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr)
+      = get_arg_8 … ps l addr →
+      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
+      s l addr = get_arg_8 … ps l addr.
+ #cm #ps #l #addr #M #sigma #policy #s #H1 #H2 #H3 @get_arg_8_status_of_pseudo_status
+ try assumption %
+qed.
+
 lemma main_lemma_preinstruction:
   ∀M, M': internal_pseudo_address_map.
@@ -98 +112 @@
     P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
   (* XXX: takes about 45 minutes to type check! *)
-  #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
+  ** #low #high #accA #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
   #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
   #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
@@ -513 +527 @@
   try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
   whd in match execute_1_preinstruction; normalize nodelta
-  [(*1,2: (* ADD and ADDC *)
+  [1,2: (* ADD and ADDC *)
     (* XXX: work on the right hand side *)
     (* XXX: switch to the left hand side *)
@@ -519 +533 @@
     #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     whd in maps_assm:(??%%);
-    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
+    inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
     [2,4: normalize nodelta #absurd destruct(absurd) ]
-    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
+    inversion (assert_data ?????) #addressing_mode_ok_assm_2
     [2,4: normalize nodelta #absurd destruct(absurd) ]
     normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
-    whd in ⊢ (??%?);
-    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
+    letin M' ≝ (〈low,high,accA〉)
+    whd in ⊢ (??%?);
+    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     whd in ⊢ (??%?);
     normalize nodelta >EQs >EQticks <instr_refl
@@ -531 +546 @@
     [1,3:
       @eq_f3
-      [1,2,4,5: 
-        @(pose … (set_clock ????)) #status #status_refl
-        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
-        [1,5:
+      [1,2,4,5: @(get_arg_8_status_of_pseudo_status' … M')
+        [3,9:
           @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) try %
           @(subaddressing_mode_elim … addr1) %
-        |3,7:
+        |6,12:
           @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
           @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
-        |2,6:
+        |2,8:
           @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try %
           @(subaddressing_mode_elim … addr1) %
-        |4,8:
+        |5,11:
           @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try %
           @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
-        ]
+        |*: % ]
       |3:
         %
-      |6:
-        @sym_eq @(get_cy_flag_status_of_pseudo_status M')
-        @sym_eq @set_clock_status_of_pseudo_status %
-      ]
+      |6: @(get_cy_flag_status_of_pseudo_status M') @set_clock_status_of_pseudo_status % ]
     |2,4:
-      #result #flags @sym_eq
-      @set_flags_status_of_pseudo_status try %
-      @sym_eq @set_arg_8_status_of_pseudo_status try %
-      @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
-    ]
-  |3: (* SUBB *)
+      #result #flags @set_flags_status_of_pseudo_status try %
+      @set_arg_8_status_of_pseudo_status try %
+      @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)]
+  |(*3: (* SUBB *)
     (* XXX: work on the right hand side *)
     (* XXX: switch to the left hand side *)
@@ -1131 +1139 @@
       ]
     ]
-  |*)12: (* JC *)
+  |12: (* JC *)
     >EQP -P normalize nodelta
     whd in match expand_pseudo_instruction; normalize nodelta
@@ -1872 +1880 @@
       @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
     ]
-  |*)42: (* PUSH *)
+  |*)*)42: (* PUSH *)
     >EQP -P normalize nodelta lapply instr_refl
     @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta
     #sigma_increment_commutation
-    whd in ⊢ (??%? → ?); inversion M #callM #accM #callM_accM_refl normalize nodelta
+    whd in ⊢ (??%? → ?);
+    @vsplit_elim #bit_one #seven_bits
+    cases (Vector_Sn … bit_one) #bitone * #empty >(Vector_O … empty) #H >H -bit_one
+    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]
+      #lookup_from_internal_ram_refl ]
     @Some_Some_elim #Mrefl destruct(Mrefl) #fetch_many_assm %{1}
     whd in ⊢ (??%?);
@@ -1883 +1897 @@
     @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta
     @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl))
-    [1:
+    [1,3,5,7:
       @eq_f2 try %
       @(pose … (set_clock ????)) #status #status_refl
-      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈callM, accM〉 … status) >status_refl -status_refl try %
-      @sym_eq @set_clock_status_of_pseudo_status
-      >EQs >EQticks <instr_refl %
-    |2:
+      @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
       cases daemon (* XXX: write_at_stack_pointer_status_of_pseudo_status *)