Changeset 2212 for src

Timestamp:

Jul 18, 2012, 5:30:26 PM (9 years ago)

Author:

mulligan

Message:

More work on the INC case

Location:

src/ASM

Files:

• AssemblyProofSplit.ma (modified) (3 diffs)
• Interpret.ma (modified) (4 diffs)

src/ASM/AssemblyProofSplit.ma

@@ -445 +445 @@
             ]
         | INC addr ⇒ λinstr_refl.
-            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm. ? with
+            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → ? with
               [ ACC_A ⇒ λacc_a: True. λEQaddr.
                 let s' ≝ add_ticks1 s in
@@ -767 +767 @@
   try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
   whd in match execute_1_preinstruction; normalize nodelta
-  [35: (* XRL *)
+  [(* 35: (* XRL *)
     inversion addr
     [1:
@@ -869 +869 @@
       ]
     ]
-  |4,5,6,7,8,9: (* INC and DEC *)
+  |33,34: (* ANL and ORL *)
+    inversion addr
+    [1,3:
+      *
+      [1,3:
+        #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
+        >EQP -P normalize nodelta
+        #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,4: normalize nodelta #absurd destruct(absurd) ]
+        inversion (addressing_mode_ok ?????) #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
+        change with (set_arg_8 ????? = ?)
+        @set_arg_8_status_of_pseudo_status try %
+        >EQs >EQticks <instr_refl >addr_refl
+        [1,4:
+          @sym_eq @set_clock_status_of_pseudo_status
+          [1,3:
+            @sym_eq @set_program_counter_status_of_pseudo_status %
+          |2,4:
+            @eq_f2 %
+          ]
+        |2,5:
+          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
+          [1,3: @(subaddressing_mode_elim … acc_a) % ] %
+        |3,6:
+          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
+          [1,5:
+            @(subaddressing_mode_elim … acc_a) %
+          |4,8:
+            @eq_f2
+            @(pose … (set_clock ????)) #status #status_refl
+            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
+            [1,5:
+              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
+              [1,5: @(subaddressing_mode_elim … acc_a) % |*: % ]
+            |3,7:
+              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
+              [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
+            |2,6:
+              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
+              [1,3: @(subaddressing_mode_elim … acc_a) % |*: % ]
+            |4,8:
+              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
+              [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
+            ]
+          |*:
+            %
+          ]
+        ]
+      |2,4:
+        #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
+        >EQP -P normalize nodelta
+        #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,4: normalize nodelta #absurd destruct(absurd) ]
+        inversion (addressing_mode_ok ?????) #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
+        change with (set_arg_8 ????? = ?)
+        @set_arg_8_status_of_pseudo_status try %
+        >EQs >EQticks <instr_refl >addr_refl
+        [1,4:
+          @sym_eq @set_clock_status_of_pseudo_status
+          [1,3:
+            @sym_eq @set_program_counter_status_of_pseudo_status %
+          |2,4:
+            @eq_f2 %
+          ]
+        |2,5:
+          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
+          [1,3: @(subaddressing_mode_elim … direct) #w % ] %
+        |3,6:
+          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
+          [1,5:
+            @(subaddressing_mode_elim … direct) #w %
+          |4,8:
+            @eq_f2
+            @(pose … (set_clock ????)) #status #status_refl
+            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
+            [1,5:
+              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
+              [1,5: @(subaddressing_mode_elim … direct) #w % |*: % ]
+            |3,7:
+              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
+              [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
+            |2,6:
+              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
+              [1,3: @(subaddressing_mode_elim … direct) #w % |*: % ]
+            |4,8:
+              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
+              [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
+            ]
+          |*:
+            %
+          ]
+        ]
+      ]
+    |2,4:
+      #carry_others inversion carry_others #carry #others #carry_others_refl #addr_refl
+      >EQP -P normalize nodelta
+      #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,4: normalize nodelta #absurd destruct(absurd) ]
+      inversion (addressing_mode_ok ?????) #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
+      change with (set_flags ?????? = ?)
+      [1,4: @set_flags_status_of_pseudo_status try % |*: skip ]
+      >EQs >EQticks <instr_refl >addr_refl
+      @sym_eq @set_clock_status_of_pseudo_status %
+    ]
+  |*)4: (* INC *)
+    (* XXX: work on the right hand side *)
+    (* XXX: switch to the left hand side *)
+    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
+    @(subaddressing_mode_elim … addr) normalize nodelta
+    [1:
+      #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) ]
+      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
+      whd in ⊢ (??%?);
+      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
+      whd in ⊢ (??%?);
+      inversion (half_add ???) #carry #result #carry_result_refl normalize nodelta
+      @(pair_replace ?????????? (refl_to_jmrefl ??? carry_result_refl))
+      [1:
+        @eq_f2 try %
+        @(pose … (set_clock ????)) #status #status_refl
+        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
+        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
+      |2:
+        @set_arg_8_status_of_pseudo_status try %
+        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
+      ]
+    |2:
+    |3:
+    |4:
+    |5:
+      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
+      whd in maps_assm:(??%%); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
+      whd in ⊢ (??%?);
+      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
+      whd in ⊢ (??%?);
+      inversion (half_add ???) #carry #bl #carry_bl_refl normalize nodelta
+      @(pair_replace ?????????? (refl_to_jmrefl ??? carry_bl_refl))
+      [1:
+      |2:
+      ]
+    ]
+  |5,6,7,8,9: (* INC and DEC *)
     cases daemon
   |42,44: (* RL and RR *)

src/ASM/Interpret.ma

@@ -159 +159 @@
             ]
         | INC addr ⇒ λinstr_refl.
-            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. ? with
+            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → ? with
               [ ACC_A ⇒ λacc_a: True.
                 let s' ≝ add_ticks1 s in
@@ -231 +231 @@
                 s
         | CLR addr ⇒ λinstr_refl.
-          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
+          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
             [ ACC_A ⇒ λacc_a: True.
               let s ≝ add_ticks1 s in
@@ -244 +244 @@
             ] (subaddressing_modein … addr)
         | CPL addr ⇒ λinstr_refl.
-          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
+          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
             [ ACC_A ⇒ λacc_a: True.
                 let s ≝ add_ticks1 s in
@@ -298 +298 @@
               set_8051_sfr … s SFR_ACC_A new_acc
         | PUSH addr ⇒ λinstr_refl.
-            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with
+            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
               [ DIRECT d ⇒ λdirect: True.
                 let s ≝ add_ticks1 s in