Changeset 854 for src/ASM/AssemblyProof.ma

Timestamp:

May 27, 2011, 5:13:29 PM (10 years ago)

Author:

mulligan

Message:

commit to avoid conflicts

File:

• src/ASM/AssemblyProof.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -44 +44 @@
 (* RUSSEL **)
 
+let rec bitvector_elim_internal
+  (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝
+  match m return λm. m ≤ n → BitVector (n - m) → bool with
+  [ O    ⇒ λprf1. λprefix. P ?
+  | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
+  ].
+  [ applyS prefix
+  | letin res ≝ (bit ::: prefix)
+    < (minus_S_S ? ?)
+    > (minus_Sn_m ? ?)
+    [ @ res
+    | @ prf2
+    ]
+  | /2/
+  ].
+qed.
+
+definition bitvector_elim ≝
+  λn: nat.
+  λP: BitVector n → bool.
+    bitvector_elim_internal n P n ? ?.
+  [ @ (le_n ?)
+  | < (minus_n_n ?)
+    @ [[ ]]
+  ]
+qed.
+
+lemma subvector_hd_tl:
+  ∀A: Type[0].
+  ∀
+  ∀hd: A.
+  ∀
+
+let rec list_addressing_mode_tags_elim
+  (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
+  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 λlen. Vector addressing_mode_tag len → bool with
+         [ O ⇒ λ_.true
+         | S y ⇒ λtl.list_addressing_mode_tags_elim y tl (λaddr.P addr) ] tl)
+  ].
+  [1: @ (execute_1_technical ? ? tl)
+      [ //
+      | 
+      ]
+  ].
+
+definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
+ λP.
+   P (ADD … ACC_A 
+   P (DA … ACC_A).
+ %
+qed.
+  
+
+definition instruction_elim: ∀P: instruction → bool. bool.
+  
+ 
+lemma instruction_elim_correct:
+  ∀i: instruction.
+  ∀P: instruction → bool.
+    instruction_elim P = true → ∀j. P j = true.
+  
+lemma test:
+  ∀i: instruction.
+  ∃pc.
+  let assembled ≝ assembly1 i in
+  let code_memory ≝ load_code_memory assembled in
+  let fetched ≝ fetch code_memory pc in
+  let 〈instr_pc, ticks〉 ≝ fetched in
+    \fst instr_pc = i.
+  # INSTR
+  @ (ex_intro ?)
+  [ @ (zero 16)
+  | @ (instruction_elim INSTR)
+  ].
+  
+    (* > append_cons_commute
+    @ 
 
 include "basics/jmeq.ma".