Changeset 2272 for src/ASM/AssemblyProofSplit.ma

Timestamp:

Jul 27, 2012, 5:53:25 PM (8 years ago)

Author:

mulligan

Message:

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

File:

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

src/ASM/AssemblyProofSplit.ma

@@ -390 +390 @@
 qed.
 
-lemma get_index_v_set_index_hit:
-  ∀A: Type[0].
-  ∀n: nat.
-  ∀v: Vector A n.
-  ∀i: nat.
-  ∀e: A.
-  ∀i_lt_n_proof: i < n.
-  ∀i_lt_n_proof': i < n.
-    get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e.
-  #A #n #v elim v
-  [1:
-    #i #e #i_lt_n_proof
-    cases (lt_to_not_zero … i_lt_n_proof)
-  |2:
-    #n' #hd #tl #inductive_hypothesis #i #e
-    cases i
-    [1:
-      #i_lt_n_proof #i_lt_n_proof' %
-    |2:
-      #i' #i_lt_n_proof' #i_lt_n_proof''
-      whd in ⊢ (??%?); @inductive_hypothesis
-    ]
-  ]
-qed.
+axiom insert_low_internal_ram_of_pseudo_low_internal_ram':
+  ∀M, M', sigma,cm,s,addr,v,v'.
+    (∀addr'.
+      ((false:::addr) = addr' →
+        map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v =
+        map_internal_ram_address_using_pseudo_address_map M' sigma (false:::addr) v') ∧
+      ((false:::addr) ≠ addr' →
+        let 〈callM, accM〉 ≝ M in
+        let 〈callM', accM'〉 ≝ M' in
+          accM = accM' ∧
+            assoc_list_lookup … addr' (eq_bv 8) … callM =
+              assoc_list_lookup … addr' (eq_bv 8) … callM')) →
+    insert Byte 7 addr v'
+      (low_internal_ram_of_pseudo_low_internal_ram M'
+      (low_internal_ram pseudo_assembly_program cm s)) =
+    low_internal_ram_of_pseudo_low_internal_ram M
+      (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
 
-(*
 lemma write_at_stack_pointer_status_of_pseudo_status:
   ∀M, M'.
@@ -423 +415 @@
   ∀s, s'.
   ∀new_b, new_b'.
-    M = M' →
-    map_internal_ram_address_using_pseudo_address_map M sigma new_b = new_b' →
+    map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' →
     status_of_pseudo_status M cm s sigma policy = s' →
     write_at_stack_pointer ?? s' new_b' =
-    status_of_pseudo_status M cm (write_at_stack_pointer ? cm s new_b) sigma policy.
+    status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy.
   #M #M' #cm #sigma #policy #s #s' #new_b #new_b'
-  #Mrefl #new_b_refl #s_refl <Mrefl <new_b_refl <s_refl
+  #new_b_refl #s_refl <new_b_refl <s_refl
   whd in match write_at_stack_pointer; normalize nodelta
   @pair_elim #nu #nl #nu_nl_refl normalize nodelta
@@ -449 +440 @@
     ]
   |2:
-    cases (get_index_v bool ????) normalize nodelta
-    whd in match status_of_pseudo_status; normalize nodelta
-    whd in match set_low_internal_ram; normalize nodelta
-    @split_eq_status try %
-    [1:
-      @(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma)
-    |2:
-      @(insert_high_internal_ram_of_pseudo_high_internal_ram … sigma)
+    @if_then_else_status_of_pseudo_status try %
+    [2:
+      @sym_eq <set_low_internal_ram_status_of_pseudo_status
+      [1:
+        @eq_f2
+        [2:
+          @insert_low_internal_ram_of_pseudo_low_internal_ram'
+    @sym_eq
+    [2:
+      <set_low_internal_ram_status_of_pseudo_status
+      [1:
+        @eq_f2
+        [2:
+          @sym_eq
+          >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b')
+          [2:
+            >new_b_refl
+    ]
   ]
-*)
+qed.
 
 lemma main_lemma_preinstruction:
@@ -519 +520 @@
             let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
                                                    (get_arg_8 … s false addr2) false in
-            let cy_flag ≝ get_index' ? O  ? flags in
+            let cy_flag ≝ get_index' ? O ? flags in
             let ac_flag ≝ get_index' ? 1 ? flags in
             let ov_flag ≝ get_index' ? 2 ? flags in
@@ -917 +918 @@
   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 *)
@@ -1535 +1536 @@
       ]
     ]
-  |12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
+  |*)12: (* JC *)
+    >EQP -P normalize nodelta
+    whd in match expand_pseudo_instruction; normalize nodelta
+    whd in match expand_relative_jump; normalize nodelta
+    whd in match expand_relative_jump_internal; normalize nodelta
+    @pair_elim #sj_possible #disp #sj_possible_disp_refl
+    inversion sj_possible #sj_possible_refl normalize nodelta
+    [1:
+      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
+      whd in maps_assm:(??%%);
+      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
+      whd in ⊢ (??%?); normalize nodelta
+      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
+      whd in ⊢ (??%?);
+      @if_then_else_status_of_pseudo_status
+      >EQs >EQticks <instr_refl normalize nodelta
+      [1:
+        @(get_cy_flag_status_of_pseudo_status M') %
+      |2:
+        @sym_eq @set_program_counter_status_of_pseudo_status
+        [1:
+        |2:
+          @sym_eq @set_clock_status_of_pseudo_status try %
+          whd in match ticks_of0; normalize nodelta
+          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
+          [1:
+            @eq_f2 try %
+            >sigma_increment_commutation
+            lapply sigma_policy_witness whd in match sigma_policy_specification; normalize nodelta
+            * #sigma_zero_assm #relevant cases (relevant ppc ?)
+            [1:
+              -relevant
+              [2:
+                >EQcm assumption
+              |1:
+                #relevant #_ <EQppc >relevant @eq_f @eq_f @eq_f
+                >EQlookup_labels >EQcm >create_label_cost_refl @eq_f2
+              ]
+            |2:
+            ]
+          |2:
+            >sj_possible_refl %
+          ]
+        ]
+      |3:
+      ]
+    ]
     cases daemon
-  |29,30: (* ANL and ORL *)
+  |13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
+    cases daemon
+  |(*29,30: (* ANL and ORL *)
     inversion addr
     [1,3:
@@ -2228 +2277 @@
       @(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