Changeset 2166 for src

Timestamp:

Jul 8, 2012, 3:59:01 PM (8 years ago)

Author:

sacerdot

Message:

1. less daemons
2. more easily usable statement

File:

• src/ASM/Test.ma (modified) (5 diffs)

src/ASM/Test.ma

@@ -486 +486 @@
 qed.
 
-definition map_address_mode_using_internal_pseudo_address_map_ok ≝
- λM,sigma,cm.λs:PreStatus ? cm.λaddr,v,v'.
+definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝
+ λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λaddr.
+  match addr with
+  [ INDIRECT i ⇒
+     assoc_list_lookup ??
+      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None …
+  | EXT_INDIRECT e ⇒
+     assoc_list_lookup ??
+      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None …
+  | _ ⇒ True ].
+
+definition map_address_mode_using_internal_pseudo_address_map_ok2 ≝
+ λT,M,sigma,cm.λs:PreStatus T cm.λaddr,v.
   match addr with
   [ DIRECT d ⇒
@@ -495 +506 @@
       map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v
      | false ⇒
-      map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ] = v'
+      map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ]
   | INDIRECT i ⇒
-     assoc_list_lookup ??
-      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None … ∧
      let register ≝ get_register ?? s [[ false; false; i ]] in
-     map_internal_ram_address_using_pseudo_address_map M sigma register v = v'
-  | EXT_INDIRECT e ⇒
-     assoc_list_lookup ??
-      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None … ∧
-     v = v'
-  | _ ⇒ v = v'].
+     map_internal_ram_address_using_pseudo_address_map M sigma register v
+  | ACC_A ⇒
+     map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v
+  | _ ⇒ v ].
 
 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
@@ -584 +591 @@
   ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
   ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'.
-   map_address_mode_using_internal_pseudo_address_map_ok … M sigma cm ps addr value value' →
+   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps addr →
+   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
     set_arg_8 (BitVectorTrie Byte 16)
       (code_memory_of_pseudo_assembly_program cm sigma policy)
@@ -638 +646 @@
           match other in False with [ ]
       ] (subaddressing_modein … a)) normalize nodelta
-  #M #sigma #policy #v' whd in match map_address_mode_using_internal_pseudo_address_map_ok; normalize nodelta
+  #M #sigma #policy #v'
+  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
+  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
   [1,2:
     <vsplit_refl normalize nodelta >p normalize nodelta
-    [ >(vsplit_ok … vsplit_refl) @set_bit_addressable_sfr_status_of_pseudo_status
-    | #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
-  |3,4: * #EQ1 #EQ2 change with (get_register ????) in match register in p;
+    [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status
+    | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
+  |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p;
       >get_register_status_of_pseudo_status
       whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
@@ -650 +660 @@
       | >(insert_low_internal_ram_status_of_pseudo_status … v) // <EQ2
         @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % ]
-  |5: * #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status
+  |5: #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status
       whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
       >EQ1 normalize nodelta
       >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status
-  |6: #EQ <EQ cases daemon (*CSC*)
-  |7: #EQ <EQ @set_8051_sfr_status_of_pseudo_status cases daemon (*CSC*)
-  |8: #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
-  |9: #EQ <EQ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
+  |6: #_ #EQ <EQ cases daemon (*CSC*)
+  |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/
+  |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
+  |9: #_ #EQ <EQ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
       >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ]
 qed.