Changeset 875 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 3, 2011, 11:21:12 AM (10 years ago)

Author:

sacerdot

Message:

...

File:

• src/ASM/AssemblyProof.ma (modified) (2 diffs)

src/ASM/AssemblyProof.ma

@@ -442 +442 @@
   λ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.
+
 (*
 lemma test:
@@ -461 +529 @@
       let 〈instr_pc, ticks〉 ≝ fetched in
         eq_instruction (\fst instr_pc)) i = true.
- [ @ (instruction_elim_complete )
+ [ #i cases i #arg try #arg2 whd in ⊢ (??%?)
+   [2: whd in ⊢ (??(match ? (? %) ?with [ _ ⇒ ?] ?)?)
+       cases arg #sam cases sam #XX try #PP normalize in PP; try cases PP;
+       whd in ⊢ (??(match ? (? %) ? with [ _ ⇒ ?] ?)?)
+ 
+   [2: #addr whd in ⊢ (??%?) 
+ 
+   @ (instruction_elim_complete )
  | @ zero
  ]