Changeset 2176 for src/joint/BEMem.ma

Timestamp:

Jul 12, 2012, 1:28:28 PM (8 years ago)

Author:

campbell

Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:

• src/joint/BEMem.ma (modified) (8 diffs)

src/joint/BEMem.ma

@@ -23 +23 @@
 definition is_address : (beval × beval) → Prop ≝ λa.
   ∃p : Σp.bool_to_Prop (is_addressable (ptype p)).∃p0,p1.
-    \fst a = BVptr p p0 ∧ part_no ? p0 = 0 ∧
-    \snd a = BVptr p p1 ∧ part_no ? p1 = 1.
+    \fst a = BVptr p p0 ∧ part_no … p0 = 0 ∧
+    \snd a = BVptr p p1 ∧ part_no … p1 = 1.
 
 definition is_addressb : (beval × beval) → bool ≝ λa.
@@ -44 +44 @@
   (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a).
 #P * *
-[4:|*: [|#b0|#r0#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)]
+[4:|*: [|#b0|(*#r0*)#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)]
 #p0 #part0 #a1
 whd in match is_addressb; normalize nodelta
@@ -50 +50 @@
 #H >H
 [ @(eqb_elim part0 0) #Heq
-  [ cases a1 [|#b0|#r0#part0|#p1#part1] whd in match (?∧?);
+  [ cases a1 [|#b0|(*#r0*)#part0|#p1#part1] whd in match (?∧?);
     [4: @eq_pointer_elim #Heq'
       [ @(eqb_elim part1 1) #Heq''
@@ -89 +89 @@
 destruct(H0 H4)
 qed.
-
+(* For full 8051 memory spaces 
 definition pointer_compat' ≝ λb,r.
   match b with
@@ -116 +116 @@
 ]
 qed.
-
+*)
 lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
+** #a0 #a1 ***** #z #o 
+#Hr
+(*
 ** #a0 #a1 ***** #r #z #Hr #o * lapply (pointer_compat_from_ind ?? Hr)
 cases r in Hr ⊢ %; #Hr *
+*)
 ** #part0 #H0 ** #part1 #H1 *** #EQa0 #EQpart0 #EQa1 #EQpart1
 destruct normalize
@@ -133 +137 @@
 #p
 lapply (refl … p)
-generalize in match p in ⊢ (???%→%); **
+generalize in match p in ⊢ (???%→%); *(***)
 whd in match (address_of_pointer ?);
-#b #H #o #EQp * #a0 #a1
+#b (*#H*) #o #EQp * #a0 #a1
 normalize #EQ destruct(EQ)
+%{p} >EQp [ cases (block_region b) // | % [2: % [2: % [ % [ % ] ] ] ] %
+(*
 %{p} >EQp [1,3: %]
 % [2,4: % [2,4: % [1,3: % [1,3: %]]]] %
+*)
 qed.
 
@@ -146 +153 @@
 lemma address_of_pointer_is_safe :
   ∀p.address_of_pointer p = ! a ← safe_address_of_pointer p ; return (a : address).
+#p normalize % qed.
+(*
 ****#z #H
 lapply (pointer_compat_from_ind ?? H) * #o
 normalize %
-qed.
+qed.*)
 
 definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝
@@ -157 +166 @@
 
 definition safe_address_of_code_pointer: (Σp:pointer. ptype p = Code) → safe_address ≝ address_of_code_pointer.
+cases H -H * #b #o normalize cases b * #z #EQ destruct
+%{«mk_pointer  (mk_block Code z)  o,I»}
+% [2: % [2: % [ % [ % ]]]] %
+qed.
+(*
 cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
 lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
 %{«mk_pointer ? (mk_block Code z) H o,I»}
 % [2: % [2: % [ % [ % ]] % |]|]
-qed.
+qed.*)
 
 (* Paolo: why only code pointers and not XRAM too? *)