Changeset 854 for src/ASM/AssemblyProof.ma
 Timestamp:
 May 27, 2011, 5:13:29 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r853 r854 44 44 (* RUSSEL **) 45 45 46 let rec bitvector_elim_internal 47 (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n  m) → bool ≝ 48 match m return λm. m ≤ n → BitVector (n  m) → bool with 49 [ O ⇒ λprf1. λprefix. P ? 50  S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?) 51 ]. 52 [ applyS prefix 53  letin res ≝ (bit ::: prefix) 54 < (minus_S_S ? ?) 55 > (minus_Sn_m ? ?) 56 [ @ res 57  @ prf2 58 ] 59  /2/ 60 ]. 61 qed. 62 63 definition bitvector_elim ≝ 64 λn: nat. 65 λP: BitVector n → bool. 66 bitvector_elim_internal n P n ? ?. 67 [ @ (le_n ?) 68  < (minus_n_n ?) 69 @ [[ ]] 70 ] 71 qed. 72 73 lemma subvector_hd_tl: 74 ∀A: Type[0]. 75 ∀ 76 ∀hd: A. 77 ∀ 78 79 let rec list_addressing_mode_tags_elim 80 (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝ 81 match l return λx.match x with [O ⇒ λl: Vector … O. bool  S x' ⇒ λl: Vector addressing_mode_tag (S x'). 82 (l → bool) → bool ] with 83 [ VEmpty ⇒ true 84  VCons len hd tl ⇒ λP. 85 let process_hd ≝ 86 match hd return λhd. ∀P: hd:::tl → bool. bool with 87 [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x)) 88  indirect ⇒ λP.bit_elim (λx. P (INDIRECT x)) 89  ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x)) 90  registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x)) 91  acc_a ⇒ λP.P ACC_A 92  acc_b ⇒ λP.P ACC_B 93  dptr ⇒ λP.P DPTR 94  data ⇒ λP.bitvector_elim 8 (λx. P (DATA x)) 95  data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x)) 96  acc_dptr ⇒ λP.P ACC_DPTR 97  acc_pc ⇒ λP.P ACC_PC 98  ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR 99  indirect_dptr ⇒ λP.P INDIRECT_DPTR 100  carry ⇒ λP.P CARRY 101  bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x)) 102  n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x)) 103  relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x)) 104  addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x)) 105  addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x)) 106 ] 107 in 108 andb (process_hd P) 109 (match len return λlen. Vector addressing_mode_tag len → bool with 110 [ O ⇒ λ_.true 111  S y ⇒ λtl.list_addressing_mode_tags_elim y tl (λaddr.P addr) ] tl) 112 ]. 113 [1: @ (execute_1_technical ? ? tl) 114 [ // 115  116 ] 117 ]. 118 119 definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝ 120 λP. 121 P (ADD … ACC_A 122 P (DA … ACC_A). 123 % 124 qed. 125 126 127 definition instruction_elim: ∀P: instruction → bool. bool. 128 129 130 lemma instruction_elim_correct: 131 ∀i: instruction. 132 ∀P: instruction → bool. 133 instruction_elim P = true → ∀j. P j = true. 134 135 lemma test: 136 ∀i: instruction. 137 ∃pc. 138 let assembled ≝ assembly1 i in 139 let code_memory ≝ load_code_memory assembled in 140 let fetched ≝ fetch code_memory pc in 141 let 〈instr_pc, ticks〉 ≝ fetched in 142 \fst instr_pc = i. 143 # INSTR 144 @ (ex_intro ?) 145 [ @ (zero 16) 146  @ (instruction_elim INSTR) 147 ]. 148 149 (* > append_cons_commute 150 @ 46 151 47 152 include "basics/jmeq.ma".
Note: See TracChangeset
for help on using the changeset viewer.