Changeset 2269

Timestamp:

Jul 26, 2012, 3:29:15 PM (7 years ago)

Author:

sacerdot

Message:

Proof completely repaired up to write_at_stack_pointer_status_of_pseudo_status,
which is missing from the library.

File:

• src/ASM/AssemblyProofSplitSplit.ma (modified) (7 diffs)

src/ASM/AssemblyProofSplitSplit.ma

@@ -51 +51 @@
 qed.
 
+(*CSC: move elsewhere*)
+lemma bv_append_eq_to_eq:
+ ∀A,n. ∀v1,v2: Vector A n. ∀m. ∀v3,v4: Vector A m.
+  v1@@v3 = v2@@v4 → v1=v2 ∧ v3=v4.
+ #A #n #v1 elim v1
+ [ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %%
+ | #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ2
+   #m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ]
+qed.
+   
 theorem main_thm:
   ∀M, M': internal_pseudo_address_map.
@@ -102 +112 @@
       %{0}
       whd in match execute_1_pseudo_instruction0; normalize nodelta
-      change with (status_of_pseudo_status ????? = ?) cases daemon (*CSC: ???
-      whd in match (execute_1_pseudo_instruction0 ?????);
-      (* XXX: work on the left hand side of the equality *)
-      whd in ⊢ (??%?);
-      @split_eq_status try %
-      /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) *)
+      change with (status_of_pseudo_status ????? = ?)
+      whd in ⊢ (??%%); @split_eq_status try %
+      [ >set_clock_set_program_counter ]
+      >program_counter_set_program_counter >sigma_increment_commutation @add_zero
     |6: (* Mov *)
       #arg1 #arg2 #_
@@ -206 +214 @@
       whd in match (expand_pseudo_instruction ??????);
       whd in match (execute_1_pseudo_instruction0 ?????);
+      whd in match (ticks_of0 ??????);
       inversion (absolute_jump_cond ??) #aj_possible #offset #ajc_refl normalize nodelta
       inversion (aj_possible ∧ ¬ policy ?) #aj_possible_refl normalize nodelta
@@ -231 +240 @@
       [1:
         @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
-        [ @eq_f2 try %
-          cases daemon (*CSC*)
+        [ @eq_f2 try % @sym_eq
+          @(pose … (set_clock ????)) #status #status_refl @sym_eq >status_refl
+          /demod nohyps/
+          (*CSC: mess with get_8051_sfr_set_program_counter + missing high level lemmas*)
+          cut (∀A,B:Type[0]. ∀f,g:A → B. ∀a:A. f=g → f a = g a) [#A #B #f #f #a * %] #eq_fun
+          >(eq_fun ???? ? (get_8051_sfr_set_program_counter (BitVectorTrie Byte 16) … SFR_SP …))
+          >(eq_fun ???? ? (get_8051_sfr_set_program_counter pseudo_assembly_program … SFR_SP …))
+          whd in match get_8051_sfr; normalize nodelta whd in match status_of_pseudo_status;
+          normalize nodelta whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
+          cases accM try % normalize nodelta #ul #addr cases (vsplit bool ???)
+          normalize nodelta #v1 #v2 cases (eq_upper_lower ul upper) normalize nodelta
+          >get_index_v_set_index_miss try % #abs normalize in abs; destruct(abs)
         ] whd in ⊢ (??%?);
         @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
         @(pair_replace ????? ?? ??? carry_new_sp_refl')
-        [ @eq_f2 try %
-          cases daemon (*CSC*)
+        [ @eq_f2 try % @sym_eq
+          @(pose … (write_at_stack_pointer ????)) #status #status_refl @sym_eq
+          @(get_8051_sfr_status_of_pseudo_status … 〈callM,accM〉 … status) >status_refl -status_refl try %
+          @sym_eq cases daemon (*CSC: write_at_stack_pointer_status_of_pseudo_status*)
         ]
         whd in ⊢ (??%?);
@@ -243 +264 @@
         change with (set_program_counter ???? = ?)
         @set_program_counter_status_of_pseudo_status
-        [2: @sym_eq cases daemon (*@write_at_stack_pointer_status_of_pseudo_status try %
+        [2: @sym_eq cases daemon (*CSC: missing @write_at_stack_pointer_status_of_pseudo_status try %
           [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try %
                   @sigma_increment_commutation
@@ -263 +284 @@
         [1: <fst_5_rest_refl whd in match address_of_word_labels; normalize nodelta
             >create_label_cost_refl %
-        |2:  
-          cases daemon (*CSC: make a lemma here!*)
-        ]
+        |2: cases (bv_append_eq_to_eq … relevant3) #H #_ >H
+            cases (conjunction_true … aj_possible_refl) #K #_ @sym_eq
+            @eq_bv_eq assumption ]
       | @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
-        [ @eq_f2 try % cases daemon ]
+        [ @eq_f2 try %
+          @sym_eq @(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 try %
+          @sym_eq @set_program_counter_status_of_pseudo_status try % assumption ]
         @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
         @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
-        [ @eq_f2 try % cases daemon ]
+        [ @eq_f2 try % @sym_eq
+          @(pose … (write_at_stack_pointer ????)) #status #status_refl @sym_eq
+          @(get_8051_sfr_status_of_pseudo_status … 〈callM,accM〉 … status) >status_refl -status_refl try %
+          @sym_eq cases daemon (*CSC: write_at_stack_pointer_status_of_pseudo_status*) ]
         change with (set_program_counter ???? = ?)
         @set_program_counter_status_of_pseudo_status
@@ -284 +313 @@
           >program_counter_set_8051_sfr >set_clock_set_program_counter
           >program_counter_set_program_counter assumption ] #sigma_pc_bu_pc_bl_refl
-        @sym_eq
+        @sym_eq (*CSC: write_at_stack_pointer_status_of_pseudo_status*)
         cases daemon
       ]