Changeset 2165

Timestamp:

Jul 7, 2012, 3:23:57 AM (7 years ago)

Author:

sacerdot

Message:

Only three daemons left.

File:

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

src/ASM/Test.ma

@@ -467 +467 @@
 qed.
 
+lemma external_ram_status_of_pseudo_status:
+ ∀M,cm,s,sigma,policy.
+  external_ram …
+   (code_memory_of_pseudo_assembly_program cm sigma policy)
+   (status_of_pseudo_status M cm s sigma policy) =
+  external_ram … cm s.
+ //
+qed.
+
+lemma set_external_ram_status_of_pseudo_status:
+  ∀M,cm,ps,sigma,policy,ram.
+    set_external_ram …
+      (code_memory_of_pseudo_assembly_program cm sigma policy)
+      (status_of_pseudo_status M cm ps sigma policy)
+      ram =
+    status_of_pseudo_status M cm (set_external_ram … cm ps ram) sigma policy.
+  //
+qed.
+
 definition map_address_mode_using_internal_pseudo_address_map_ok ≝
  λM,sigma,cm.λs:PreStatus ? cm.λaddr,v,v'.
@@ -482 +501 @@
      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'].
 
@@ -624 +647 @@
       whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
       >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
-      [
+      [ cases daemon (*CSC*)
       | >(insert_low_internal_ram_status_of_pseudo_status … v) // <EQ2
         @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % ]
-qed.
+  |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
+      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ]
+qed.