Changeset 876 for src

Timestamp:

Jun 3, 2011, 4:03:00 PM (10 years ago)

Author:

sacerdot

Message:

...

Location:

src/ASM

Files:

• AssemblyProof.ma (modified) (4 diffs)
• Fetch.ma (modified) (2 diffs)

src/ASM/AssemblyProof.ma

@@ -439 +439 @@
  ∀P. instruction_elim P = true → ∀i. P i = true.
 
-definition eq_instruction ≝
+(*definition eq_instruction ≝
   λi, j: instruction.
-    true.
-    
-let rec list_addressing_mode_tags_elim_prop
-  (n: nat) (l: Vector addressing_mode_tag (S n))
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
-  (if is_in ? l relative then ∀x. P (RELATIVE x) else True) →
-  (if is_in ? l addr11 then ∀x. P (ADDR11 x) else True) →
-  (if is_in ? l addr16 then ∀x. P (ADDR16 x) else True) →
-  (P: addressing_mode → Prop) (x: l) 
-   on l : P x ≝
-  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
-   (l → bool) → bool ] with
-  [ VEmpty      ⇒  true  
-  | VCons len hd tl ⇒ λP.
-    let process_hd ≝
-      match hd return λhd. ∀P: hd:::tl → bool. bool with
-      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
-      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
-      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
-      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
-      | acc_a ⇒ λP.P ACC_A
-      | acc_b ⇒ λP.P ACC_B
-      | dptr ⇒ λP.P DPTR
-      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
-      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
-      | acc_dptr ⇒ λP.P ACC_DPTR
-      | acc_pc ⇒ λP.P ACC_PC
-      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
-      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
-      | carry ⇒ λP.P CARRY
-      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
-      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
-      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
-      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
-      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
-      ]
-    in
-      andb (process_hd P)
-       (match len return λx. x = len → bool with
-         [ O ⇒ λprf. true
-         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
-  ].
-  try %
-  [ 2: cases (sym_eq ??? prf); @tl
-  | generalize in match H; generalize in match tl; cases prf;
-    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
-    #tl
-    normalize in ⊢ (∀_: %. ?)
-    # H
-    whd
-    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
-    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
-qed.
+    true.*)
+axiom eq_instruction: instruction → instruction → bool.
 
 (*
@@ -522 +456 @@
  ]*)
 
+lemma BitVectorTrie_O:
+ ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
+ #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
+  [ #w #_ %1 %[@w] %
+  | #n #l #r #abs @⊥ //
+  | #n #EQ %2 >EQ %]
+qed.
+
+lemma BitVectorTrie_Sn:
+ ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
+ #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
+  [ #m #abs @⊥ //
+  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
+  | #m #EQ %2 // ]
+qed.
+
+lemma lookup_prepare_trie_for_insertion_hit:
+ ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
+  lookup … b (prepare_trie_for_insertion … b v) a = v. 
+ #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
+qed.
+ 
+lemma lookup_insert_hit:
+ ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
+  lookup … b (insert … b v t) a = v.
+ #A #a #v #n #b elim b -b -n //
+ #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
+  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
+  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
+qed.
+
+lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
+ #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
+ #n #hd #tl #abs @⊥ //
+qed.
+
+lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
+ ∃hd.∃tl.v ≃ VCons bool n hd tl.
+ #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
+ [ #abs @⊥ //
+ | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
+qed.
+
+coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 
+
+lemma lookup_prepare_trie_for_insertion_miss:
+ ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
+  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
+ #A #a #v #n #c elim c
+  [ #b >(BitVector_O … b) normalize #abs @⊥ //
+  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
+    cases hd cases hd' normalize
+    [2,3: #_ cases tl' //
+    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
+qed.
+  
+lemma lookup_insert_miss:
+ ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
+  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
+ #A #a #v #n #c elim c -c -n
+  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
+  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
+    #t cases(BitVectorTrie_Sn … t)
+    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
+     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
+    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
+     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
+     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
+qed.
+
+definition load_code_memory_aux ≝
+ fold_left_i_aux … (
+   λi, mem, v.
+     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
+
+axiom split_elim:
+ ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
+  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
+
+axiom half_add_SO:
+ ∀pc.
+ \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
+
+axiom not_eqvb_S:
+ ∀pc.
+ (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).
+
+axiom not_eqvb_SS:
+ ∀pc.
+ (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
+
 lemma test:
-  ∀i.
-      (let assembled ≝ assembly1 i in
-      let code_memory ≝ load_code_memory assembled in
-      let fetched ≝ fetch code_memory ? in
+  ∀pc,i.
+     (let assembled ≝ assembly1 i in
+      let code_memory ≝ load_code_memory_aux pc assembled in
+      let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
       let 〈instr_pc, ticks〉 ≝ fetched in
         eq_instruction (\fst instr_pc)) i = true.
- [ #i cases i #arg try #arg2 whd in ⊢ (??%?)
-   [2: whd in ⊢ (??(match ? (? %) ?with [ _ ⇒ ?] ?)?)
+ #pc #i cases i #arg try #arg2 whd in ⊢ (??%?)
+   [2,4: whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?)
        cases arg #sam cases sam #XX try #PP normalize in PP; try cases PP;
-       whd in ⊢ (??(match ? (? %) ? with [ _ ⇒ ?] ?)?)
+       whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?) try cases PP normalize in XX;
+       [1,2,3,4,5,6,7,8,10,11,12,13,14,15,16,17: cases XX
+       |*:@split_elim #b1 #b2 #EQ >EQ -EQ;
+        change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
+        whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
+        >lookup_insert_miss //
+        >lookup_insert_miss //
+        >lookup_insert_hit
+        whd in ⊢ (??(match % with [ _ ⇒ ?] ?)?)
+        whd in ⊢ (??%?) whd in ⊢ (??(?%?)?)
+        >half_add_SO >half_add_SO
+        >lookup_insert_miss [2,4: @not_eqvb_S]
+        >lookup_insert_hit >lookup_insert_hit]
+   |
+        
+        
+         
  
    [2: #addr whd in ⊢ (??%?) 
@@ -630 +671 @@
 qed.
 
-coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 
-
 lemma index_of_internal_None: ∀i,id,instr_list,n.
  occurs_exactly_once id (instr_list@[〈None …,i〉]) →
@@ -665 +704 @@
     → False.
 
-lemma BitVectorTrie_O:
- ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
- #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
-  [ #w #_ %1 %[@w] %
-  | #n #l #r #abs @⊥ //
-  | #n #EQ %2 >EQ %]
-qed.
-
-lemma BitVectorTrie_Sn:
- ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
- #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
-  [ #m #abs @⊥ //
-  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
-  | #m #EQ %2 // ]
-qed.
-
-lemma lookup_prepare_trie_for_insertion_hit:
- ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
-  lookup … b (prepare_trie_for_insertion … b v) a = v. 
- #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
-qed.
- 
-lemma lookup_insert_hit:
- ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
-  lookup … b (insert … b v t) a = v.
- #A #a #v #n #b elim b -b -n //
- #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
-  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
-  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
-qed.
-
-lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
- #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
- #n #hd #tl #abs @⊥ //
-qed.
-
-lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
- ∃hd.∃tl.v ≃ VCons bool n hd tl.
- #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
- [ #abs @⊥ //
- | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
-qed.
-
-lemma lookup_prepare_trie_for_insertion_miss:
- ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
-  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
- #A #a #v #n #c elim c
-  [ #b >(BitVector_O … b) normalize #abs @⊥ //
-  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
-    cases hd cases hd' normalize
-    [2,3: #_ cases tl' //
-    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
-qed.
-  
-lemma lookup_insert_miss:
- ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
-  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
- #A #a #v #n #c elim c -c -n
-  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
-  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
-    #t cases(BitVectorTrie_Sn … t)
-    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
-     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
-    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
-     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
-     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
-qed.
 
 definition build_maps' ≝

src/ASM/Fetch.ma

@@ -6 +6 @@
  λpmem: BitVectorTrie Byte 16.
  λpc: Word.
- let 〈x,res〉 ≝ half_add … pc (bitvector_of_nat 16 (S O)) in
-   〈res, lookup … pc pmem (zero 8)〉.
+  〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup … pc pmem (zero 8)〉.
 
 (* timings taken from SIEMENS *)
 
-definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝
+definition fetch0: BitVectorTrie Byte 16 → Word × Byte → instruction × Word × nat ≝
  λpmem: BitVectorTrie Byte 16.
- λpc: Word.
-  let 〈pc,v〉 ≝ next pmem pc in
+ λpc_v.
+  let 〈pc,v〉 ≝ pc_v in
    let 〈b,v〉 ≝ head … v in if b then
     let 〈b,v〉 ≝ head … v in if b then
@@ -390 +389 @@
   %.
 qed.
+
+definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝
+ λpmem: BitVectorTrie Byte 16.
+ λpc: Word.
+  fetch0 pmem (next pmem pc).