Changeset 2119 for src/ASM

Timestamp:

Jun 27, 2012, 12:09:25 PM (7 years ago)

Author:

sacerdot

Message:

load_code_memory moved to Fetch.ma and proved correct w.r.t. next
(fetching) using Russell

Location:

src/ASM

Files:

• AssemblyProof.ma (modified) (2 diffs)
• Fetch.ma (modified) (1 diff)
• Status.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -616 +616 @@
 qed.
 
-definition load_code_memory_aux ≝
- fold_left_i_aux … (
-   λi, mem, v.
-     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
-
 lemma vsplit_zero:
   ∀A,m.
@@ -1060 +1055 @@
     ].
 
-(* This is a trivial consequence of fetch_assembly_pseudo + the proof that the
-   function that load the code in memory is correct. The latter is based
-   on missing properties from the standard library on the BitVectorTrie
-   data structrure.
-   
-   Wrong at the moment, requires Jaap's precondition to ensure that the program
-   does not overflow when put into code memory (i.e. shorter than 2^16 bytes).
-*)
-
-lemma load_code_memory_ok:
- ∀program.
- let program_size ≝ |program| in
-  program_size ≤ 2^16 →
-   ∀pc. ∀pc_ok: pc < program_size.
-    nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
- #program elim program
- [ #_ #pc #abs normalize in abs; @⊥ /2/
- | #hd #tl #IH #size_ok *
-   [ #pc_ok whd in ⊢ (??%?); whd in match (load_code_memory ?);
-     whd in match next; normalize nodelta
-   | #pc' #pc_ok' whd in ⊢ (??%?);  whd in match (load_code_memory ?);
-     whd in match next; normalize nodelta
-   ]
- cases daemon (*CSC: complete! *)
-qed.
-(*NO! Prima dimostrare tipo Russell di assembly in Assembly.ma
-Poi dimostrare che per ogni i, se fetcho l'i-esimo bit di program
-e' come fetchare l'i-esimo bit dalla memoria.
-Concludere assembly_ok come semplice corollario.
-*)
+(* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *)      
 lemma assembly_ok:
   ∀program.

src/ASM/Fetch.ma

@@ -17 +17 @@
   λpc: Word.
     〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
+
+(*CSC: move elsewhere *)
+axiom eq_bitvector_of_nat_to_eq:
+ ∀n,n1,n2.
+  n1 < 2^n → n2 < 2^n →
+   bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2.
+
+discriminator Prod.
+
+definition load_code_memory0:
+ ∀program: list Byte. Σres: BitVectorTrie Byte 16.
+  let program_size ≝ |program| in
+   program_size ≤ 2^16 →
+    ∀pc. ∀pc_ok: pc < program_size.
+     nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc))
+≝
+ λprogram. \snd
+  (foldl_strong ?
+   (λprefix.
+     Σres: nat × (BitVectorTrie Byte 16).
+      let 〈i,mem〉 ≝ res in
+      i = |prefix| ∧
+      (i ≤ 2^16 →
+        ∀pc. ∀pc_ok: pc < |prefix|.
+         nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc))))
+   program 
+   (λprefix,v,tl,prf,i_mem.
+     let 〈i,mem〉 ≝ i_mem in
+      〈S i,insert … (bitvector_of_nat … i) v mem〉)
+  〈0,Stub Byte 16〉).
+[3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
+| % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
+| cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
+  [ >length_append >H1 normalize //
+  | #LE #pc #pc_ok
+    cases (le_to_or_lt_eq … pc_ok)
+    [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok;
+      [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //]
+      #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
+      <H1 <plus_n_O whd in ⊢ (???%); //
+    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
+      >H2 [2: @(transitive_le … LE) //]
+      cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
+      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
+      #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
+      @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
+qed.
+
+definition load_code_memory: list Byte → BitVectorTrie Byte 16 ≝
+ λprogram.load_code_memory0 program.
+
+lemma load_code_memory_ok:
+ ∀program: list Byte.
+  let program_size ≝ |program| in
+   program_size ≤ 2^16 →
+    ∀pc. ∀pc_ok: pc < program_size.
+     nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
+whd in match load_code_memory; normalize nodelta #program @pi2
+qed.
 
 lemma Prod_inv_rect_Type0:

src/ASM/Status.ma

@@ -1104 +1104 @@
 qed.
 
-definition load_code_memory ≝
- fold_left_i … (
-   λi, mem, v.
-     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
-
-definition load ≝
- λl,cm.
- λstatus.
-   set_code_memory (BitVectorTrie Word 16) ? cm status (load_code_memory l).
-
 definition fetch_pseudo_instruction:
  ∀code_mem:list labelled_instruction. ∀pc:Word.