Changeset 2256 for src/ASM

Timestamp:

Jul 25, 2012, 12:12:57 PM (7 years ago)

Author:

mulligan

Message:

MOV and MOVX cases complete

Location:

src/ASM

Files:

• AssemblyProof.ma (modified) (2 diffs)
• AssemblyProofSplit.ma (modified) (6 diffs)

src/ASM/AssemblyProof.ma

@@ -480 +480 @@
           ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) ∧
             ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
-    | EXT_INDIRECT _ ⇒ true
+    | EXT_INDIRECT e ⇒
+        let address ≝ bit_address_of_register … s [[false;false;e]] in
+          ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M)
     | REGISTER r ⇒
         let address ≝ bit_address_of_register … s r in
@@ -679 +681 @@
             None ?
       | NOP ⇒ Some … M
-      | MOVX addr1 ⇒ Some … M
+      | MOVX addr1 ⇒
+        match addr1 with
+        [ inl l ⇒
+          let 〈acc_a, others〉 ≝ l in
+          let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
+          let others_ok ≝ addressing_mode_ok T M … s others in
+            if acc_a_ok ∧ others_ok then
+              Some ? M
+            else
+              None ?
+        | inr r ⇒
+          let 〈others, acc_a〉 ≝ r in
+          let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
+          let others_ok ≝ addressing_mode_ok T M … s others in
+            if others_ok ∧ acc_a_ok then
+              Some ? M
+            else
+              None ?
+        ]
       | XRL addr1 ⇒
         match addr1 with

src/ASM/AssemblyProofSplit.ma

@@ -123 +123 @@
 lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr:
   ∀M', cm, status, status', sigma.
-  ∀addr1: [[acc_a; registr; direct; indirect; data]]. (* XXX: expand as needed *)
+  ∀addr1: [[acc_a; registr; direct; indirect; data; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
     get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
     addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →
@@ -129 +129 @@
   #M' #cm #status #status' #sigma #addr1 #sfr_refl
   @(subaddressing_mode_elim … addr1) try (#w #_ @I)
-  [1: #_ @I ]
-  #w whd in ⊢ (??%? → %);
+  [1,4: #_ @I ] #w
+  whd in ⊢ (??%? → %);
   inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta
-  [1:
+  [1,3:
     #absurd destruct(absurd)
-  |2:
+  |2,4:
     #_
     @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
@@ -221 +221 @@
   ∀M', cm.
   ∀sigma, status, status', b, b'.
-  ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr]]. (* XXX: expand as needed *)
+  ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
     get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
     low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' →
@@ -275 +275 @@
       ]
     ]
-  |5,6:
-    #w #_ %
+  |5,6,7,8:
+    #w try #w' %
   ]
 qed.
@@ -1935 +1935 @@
       ]      
     ]
-  |*)43: (* MOV *)
+  |43: (* MOV *)
     >EQP -P normalize nodelta
     inversion addr
@@ -2121 +2121 @@
       change with (set_arg_1 ????? = ?)
       @set_arg_1_status_of_pseudo_status
-      >EQs >EQticks <instr_refl >addr_refl try %
-      [1:
+      [1:
+        >EQs >EQticks <instr_refl >addr_refl
         @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
         @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
         @(subaddressing_mode_elim … carry) @I
       |2:
-        @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps)
-        [1:
-          normalize nodelta
+        >EQs >EQticks <instr_refl >addr_refl %
+      |3,4: (* XXX: following two cases same proof but Matita is too slow if merged *)
+        @(pose … (set_clock ????)) #status #status_refl
+        [1:
+          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … status) try %
         |2:
-          assumption
-        ]
-      ]
-    ]
-  |44: (* MOVX *)
+          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … status) try %
+        ]
+        >status_refl -status_refl >EQs >EQticks <instr_refl >addr_refl
+        lapply addressing_mode_ok_assm_1 whd in ⊢ (??%? → ??%?);
+        @(subaddressing_mode_elim … bit_addr) #w normalize nodelta #relevant assumption
+      ]
+    ]
+  |*)44: (* MOVX *)
+    >EQP -P normalize nodelta
+    inversion addr
+    [1:
+      #acc_a_others cases acc_a_others #acc_a #others normalize nodelta
+      #addr_refl
+      #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
+      [2: normalize nodelta #absurd destruct(absurd) ]
+      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
+      [2: normalize nodelta #absurd destruct(absurd) ]
+      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
+      whd in ⊢ (??%?);
+      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
+      change with (set_arg_8 ????? = ?)
+      @set_arg_8_status_of_pseudo_status try %
+      >EQs >EQticks <instr_refl >addr_refl
+      [1:
+        @sym_eq @set_clock_status_of_pseudo_status %
+      |2:
+        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
+        [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
+      |3:
+        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
+        [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] try %
+        @(pose … (set_clock ????)) #status #status_refl
+        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
+        [1:
+          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
+          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
+        |2:
+          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
+          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
+        ]
+      ]
+    |2:
+      #others_acc_a cases others_acc_a #others #acc_a
+      #addr_refl
+      #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
+      [2: normalize nodelta #absurd destruct(absurd) ]
+      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
+      [2: normalize nodelta #absurd destruct(absurd) ]
+      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
+      whd in ⊢ (??%?);
+      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
+      change with (set_arg_8 ????? = ?)
+      @set_arg_8_status_of_pseudo_status
+      >EQs >EQticks <instr_refl >addr_refl try %
+      [1:
+        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
+        [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
+      |2:
+        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
+        [1:
+          /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
+        |2,3:
+          %
+        |4:
+          @(pose … (set_clock ????)) #status #status_refl
+          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
+          [1:
+            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_2)
+            [1: @(subaddressing_mode_elim … acc_a) % ] %
+          |2:
+            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_2)
+            [1: @(subaddressing_mode_elim … acc_a) % ] %
+          ]
+        ]
+      ]
+    ]
   |45: (* SETB *)
     >EQP -P normalize nodelta