 Timestamp:
 Dec 14, 2011, 11:52:28 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Fetch.ma
r1602 r1604 10 10 definition code_memory_size ≝ bitvector_max_nat 16. 11 11 12 axiom bitvector_lt_bitvector_max_nat: 13 ∀length: nat. 14 ∀v: BitVector length. 15 nat_of_bitvector length v < bitvector_max_nat length. 16 17 lemma word_lt_bitvector_max_nat: 18 ∀w: Word. 19 nat_of_bitvector … w < code_memory_size. 20 #w // 21 qed. 22 23 axiom w_lt_half_add_increment: 24 ∀length: nat. 25 ∀v: BitVector length. 26 ∀proof: nat_of_bitvector … v < bitvector_max_nat length  1. 27 nat_of_bitvector … v < nat_of_bitvector … (\snd (half_add … v (bitvector_of_nat … (S O)))). 28 29 lemma minus_leq_minus: 30 ∀m, n, o: nat. 31 n ≤ m → o ≤ m → o ≤ n → m  n ≤ m  o. 32 #m #n #o #m_le_n #m_le_o #o_le_n 33 cases daemon (* XXX: todo *) 34 qed. 35 36 definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. 37 nat_of_bitvector … program_counter < (code_memory_size  24) → 38 Σret: Word × Byte. nat_of_bitvector … program_counter < nat_of_bitvector … (\fst ret) ∧ 39 (nat_of_bitvector … (\fst ret)) ≤ code_memory_size ≝ 12 definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝ 40 13 λpmem: BitVectorTrie Byte 16. 41 14 λpc: Word. 42 λproof.43 15 〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉. 44 @conj45 [1:46 @w_lt_half_add_increment47 @(transitive_le48 (S (nat_of_bitvector … pc))49 (code_memory_size  24)50 (code_memory_size  1) ? ?)51 [1:52 @proof53 2:54 @(minus_leq_minus code_memory_size 24 1) //55 ]56 2:57 cases daemon (* XXX: todo *)58 ]59 qed.60 61 axiom o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p:62 ∀m, n, o, p: nat.63 p < o → m < n  o → m < n  p.64 65 lemma pair_eq_1_jmeq:66 ∀a, b: Type[0].67 ∀a1, a2: a.68 ∀b1, b2: b.69 〈a1, b1〉 ≃ 〈a2, b2〉 → a1 = a2.70 #a #b #a1 #a2 #b1 #b2 #assm71 cases daemon (* XXX: no jm discrimination for pairs *)72 qed.73 74 lemma prod_fst_jmeq:75 ∀a, b: Type[0].76 ∀p: a × b.77 ∀l: a.78 ∀r: b.79 p ≃ 〈l, r〉 → l = fst … p.80 #a #b #p #l #r81 cases p #aa #bb #assm @sym_eq82 lapply (pair_eq_1_jmeq a b aa l bb r assm)83 #assm assumption84 qed.85 86 lemma lt_to_le:87 ∀m, n: nat.88 m < n → m ≤ n.89 #m #n #assm /2 by le_S_to_le/90 qed.91 16 92 17 lemma Prod_inv_rect_Type0: … … 112 37 (* timings taken from SIEMENS *) 113 38 114 definition fetch0: BitVectorTrie Byte 16 → ∀program_counter: Word. Byte → 115 nat_of_bitvector … program_counter < code_memory_size  24 (* 3 bytes *) → 116 Σret: instruction × Word × nat. nat_of_bitvector … program_counter ≤ nat_of_bitvector … (\snd (\fst ret)) ≝ 39 definition fetch0: ∀code_memory: BitVectorTrie Byte 16. 40 ∀program_counter: Word. Byte → instruction × Word × nat ≝ 117 41 λpmem. 118 42 λpc. 119 43 λv. 120 λproof.121 44 let 〈b,v〉 ≝ head … v in if b then 122 45 let 〈b,v〉 ≝ head … v in if b then … … 131 54 else 132 55 let 〈b,v〉≝ head … v in if b then 133 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉56 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉 134 57 else 135 58 〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉 … … 139 62 else 140 63 let 〈b,v〉≝ head … v in if b then 141 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉64 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉 142 65 else 143 66 〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉 … … 151 74 else 152 75 let 〈b,v〉≝ head … v in if b then 153 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉76 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉 154 77 else 155 78 〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉 … … 159 82 else 160 83 let 〈b,v〉≝ head … v in if b then 161 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉84 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉 162 85 else 163 86 〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉 … … 165 88 let 〈b,v〉≝ head … v in if b then 166 89 let 〈b,v〉≝ head … v in if b then 167 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉90 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉 168 91 else 169 92 let 〈b,v〉≝ head … v in if b then … … 172 95 else 173 96 let 〈b,v〉≝ head … v in if b then 174 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉97 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉 175 98 else 176 99 〈〈RealInstruction (DA … ACC_A), pc〉, 1〉 … … 180 103 〈〈RealInstruction (SETB … CARRY), pc〉, 1〉 181 104 else 182 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉183 else 184 let 〈b,v〉≝ head … v in if b then 185 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉186 else 187 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉105 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉 106 else 107 let 〈b,v〉≝ head … v in if b then 108 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 109 else 110 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉 188 111 else 189 112 let 〈b,v〉≝ head … v in if b then … … 195 118 else 196 119 let 〈b,v〉≝ head … v in if b then 197 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉120 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉 198 121 else 199 122 〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉 … … 203 126 〈〈RealInstruction (CLR … CARRY), pc〉, 1〉 204 127 else 205 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉206 else 207 let 〈b,v〉≝ head … v in if b then 208 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉209 else 210 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉128 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉 129 else 130 let 〈b,v〉≝ head … v in if b then 131 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 132 else 133 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉 211 134 else 212 135 let 〈b,v〉≝ head … v in if b then 213 136 let 〈b,v〉≝ head … v in if b then 214 137 let 〈b,v〉≝ head … v in if b then 215 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈RealInstruction (CJNE … (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉216 else 217 let 〈b,v〉≝ head … v in if b then 218 let 〈b,v〉≝ head … v in if b then 219 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉220 else 221 let 〈b,v〉≝ head … v in if b then 222 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉223 else 224 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉138 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE … (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉 139 else 140 let 〈b,v〉≝ head … v in if b then 141 let 〈b,v〉≝ head … v in if b then 142 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉 143 else 144 let 〈b,v〉≝ head … v in if b then 145 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉 146 else 147 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉 225 148 else 226 149 let 〈b,v〉≝ head … v in if b then … … 228 151 〈〈RealInstruction (CPL … CARRY), pc〉, 1〉 229 152 else 230 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉231 else 232 let 〈b,v〉≝ head … v in if b then 233 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉234 else 235 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉236 else 237 let 〈b,v〉≝ head … v in if b then 238 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉239 else 240 let 〈b,v〉≝ head … v in if b then 241 let 〈b,v〉≝ head … v in if b then 242 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉153 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉 154 else 155 let 〈b,v〉≝ head … v in if b then 156 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 157 else 158 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉 159 else 160 let 〈b,v〉≝ head … v in if b then 161 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉 162 else 163 let 〈b,v〉≝ head … v in if b then 164 let 〈b,v〉≝ head … v in if b then 165 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉 243 166 else 244 167 〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉 … … 248 171 〈〈RealInstruction (INC … DPTR), pc〉, 2〉 249 172 else 250 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉251 else 252 let 〈b,v〉≝ head … v in if b then 253 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉254 else 255 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉173 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉 174 else 175 let 〈b,v〉≝ head … v in if b then 176 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 177 else 178 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉 256 179 else 257 180 let 〈b,v〉≝ head … v in if b then … … 264 187 else 265 188 let 〈b,v〉≝ head … v in if b then 266 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉267 else 268 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉189 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉 190 else 191 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉 269 192 else 270 193 let 〈b,v〉≝ head … v in if b then … … 272 195 〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉 273 196 else 274 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉275 else 276 let 〈b,v〉≝ head … v in if b then 277 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉278 else 279 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉280 else 281 let 〈b,v〉≝ head … v in if b then 282 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉283 else 284 let 〈b,v〉≝ head … v in if b then 285 let 〈b,v〉≝ head … v in if b then 286 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉287 else 288 let 〈b,v〉≝ head … v in if b then 289 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉197 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉 198 else 199 let 〈b,v〉≝ head … v in if b then 200 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 201 else 202 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉 203 else 204 let 〈b,v〉≝ head … v in if b then 205 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉 206 else 207 let 〈b,v〉≝ head … v in if b then 208 let 〈b,v〉≝ head … v in if b then 209 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉 210 else 211 let 〈b,v〉≝ head … v in if b then 212 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉 290 213 else 291 214 〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉 … … 295 218 〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉 296 219 else 297 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉298 else 299 let 〈b,v〉≝ head … v in if b then 300 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉301 else 302 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉220 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉 221 else 222 let 〈b,v〉≝ head … v in if b then 223 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 224 else 225 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉 303 226 else 304 227 let 〈b,v〉≝ head … v in if b then … … 306 229 let 〈b,v〉≝ head … v in if b then 307 230 let 〈b,v〉≝ head … v in if b then 308 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉309 else 310 let 〈b,v〉≝ head … v in if b then 311 let 〈b,v〉≝ head … v in if b then 312 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉313 else 314 let 〈b,v〉≝ head … v in if b then 315 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉316 else 317 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉231 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉 232 else 233 let 〈b,v〉≝ head … v in if b then 234 let 〈b,v〉≝ head … v in if b then 235 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉 236 else 237 let 〈b,v〉≝ head … v in if b then 238 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉 239 else 240 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉 318 241 else 319 242 let 〈b,v〉≝ head … v in if b then … … 321 244 〈〈JMP … INDIRECT_DPTR, pc〉, 2〉 322 245 else 323 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉324 else 325 let 〈b,v〉≝ head … v in if b then 326 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉327 else 328 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉246 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉 247 else 248 let 〈b,v〉≝ head … v in if b then 249 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 250 else 251 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉 329 252 else 330 253 let 〈b,v〉≝ head … v in if b then … … 336 259 else 337 260 let 〈b,v〉≝ head … v in if b then 338 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉339 else 340 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉341 else 342 let 〈b,v〉≝ head … v in if b then 343 let 〈b,v〉≝ head … v in if b then 344 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉345 else 346 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉347 else 348 let 〈b,v〉≝ head … v in if b then 349 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉350 else 351 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉261 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉 262 else 263 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉 264 else 265 let 〈b,v〉≝ head … v in if b then 266 let 〈b,v〉≝ head … v in if b then 267 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉 268 else 269 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉 270 else 271 let 〈b,v〉≝ head … v in if b then 272 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 273 else 274 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉 352 275 else 353 276 let 〈b,v〉≝ head … v in if b then … … 360 283 else 361 284 let 〈b,v〉≝ head … v in if b then 362 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉363 else 364 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉365 else 366 let 〈b,v〉≝ head … v in if b then 367 let 〈b,v〉≝ head … v in if b then 368 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉369 else 370 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉371 else 372 let 〈b,v〉≝ head … v in if b then 373 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉374 else 375 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉285 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉 286 else 287 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉 288 else 289 let 〈b,v〉≝ head … v in if b then 290 let 〈b,v〉≝ head … v in if b then 291 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉 292 else 293 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉 294 else 295 let 〈b,v〉≝ head … v in if b then 296 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 297 else 298 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉 376 299 else 377 300 let 〈b,v〉≝ head … v in if b then … … 383 306 else 384 307 let 〈b,v〉≝ head … v in if b then 385 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉386 else 387 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉388 else 389 let 〈b,v〉≝ head … v in if b then 390 let 〈b,v〉≝ head … v in if b then 391 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉392 else 393 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉394 else 395 let 〈b,v〉≝ head … v in if b then 396 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉397 else 398 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉308 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉 309 else 310 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉 311 else 312 let 〈b,v〉≝ head … v in if b then 313 let 〈b,v〉≝ head … v in if b then 314 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉 315 else 316 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉 317 else 318 let 〈b,v〉≝ head … v in if b then 319 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 320 else 321 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉 399 322 else 400 323 let 〈b,v〉≝ head … v in if b then … … 408 331 else 409 332 let 〈b,v〉≝ head … v in if b then 410 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉411 else 412 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉333 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉 334 else 335 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉 413 336 else 414 337 let 〈b,v〉≝ head … v in if b then … … 419 342 else 420 343 let 〈b,v〉≝ head … v in if b then 421 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉422 else 423 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉344 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 345 else 346 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 424 347 else 425 348 let 〈b,v〉≝ head … v in if b then … … 431 354 else 432 355 let 〈b,v〉≝ head … v in if b then 433 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉434 else 435 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉356 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉 357 else 358 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉 436 359 else 437 360 let 〈b,v〉≝ head … v in if b then … … 442 365 else 443 366 let 〈b,v〉≝ head … v in if b then 444 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉445 else 446 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉367 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 368 else 369 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 447 370 else 448 371 let 〈b,v〉≝ head … v in if b then … … 455 378 else 456 379 let 〈b,v〉≝ head … v in if b then 457 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉380 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉 458 381 else 459 382 〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉 … … 463 386 〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉 464 387 else 465 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉466 else 467 let 〈b,v〉≝ head … v in if b then 468 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉469 else 470 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉388 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉 389 else 390 let 〈b,v〉≝ head … v in if b then 391 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 392 else 393 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 471 394 else 472 395 let 〈b,v〉≝ head … v in if b then … … 478 401 else 479 402 let 〈b,v〉≝ head … v in if b then 480 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉403 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉 481 404 else 482 405 〈〈RealInstruction (INC … ACC_A), pc〉, 1〉 … … 486 409 〈〈RealInstruction (RR … ACC_A), pc〉, 1〉 487 410 else 488 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ?in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉489 else 490 let 〈b,v〉≝ head … v in if b then 491 let 〈pc,b1〉 {EQ} ≝ next pmem pc ?in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉411 let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉 412 else 413 let 〈b,v〉≝ head … v in if b then 414 let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 492 415 else 493 416 〈〈RealInstruction (NOP …), pc〉, 1〉. 494 try % 495 cases daemon (* 496 try ( 497 @(o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p 498 (nat_of_bitvector 16 pc) code_memory_size 24 1 499 (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof) 500 ) 501 [6,8,14,15,16,17,20,21,22,23,25,28,30,31,32,33,34,37,38,39,40,41,44,45,46,47, 502 50,51,52,53,56,57,58,59,65,69,71,73,75: 503 cases daemon (* XXX: segmentation fault *) 504 1,2,3,4,5,7,8,9,10,11,12,13,18,19,24,26,27,29,35,36,42,43,48,49,54,55,60,61, 505 62,63,64,66,67,68,70,72,74,76: 506 @breakup_pair' cases (next pmem pc ?) 507 normalize * normalize #pc' #byte @lt_to_le 508 [30: 509 generalize in match pc in EQ; #pc' #EQ' pc 510 cut(nat_of_bitvector … pc < nat_of_bitvector … pc') 511 [1: 512 cut(pc' = \fst (next pmem pc (o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p (nat_of_bitvector 16 pc) 513 code_memory_size 24 1 (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof))) 514 [1: 515 // 516 2: 517 #assm >assm @sig2 518 ] 519  #lt_assm 520 lapply(transitive_le 521 (S (nat_of_bitvector … pc)) 522 (nat_of_bitvector … pc') 523 (S (nat_of_bitvector … pc')) lt_assm ?) 524 [1: 525 // 526 2: 527 #le_assm 528 lapply(transitive_le 529 (S (nat_of_bitvector … pc)) 530 (S (nat_of_bitvector … pc')) 531 (code_memory_size  1) le_assm ?) 532 [2: 533 // 534 1: 535 @(o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p 536 (nat_of_bitvector … pc) code_memory_size 24 1 ? ?) 537 [1: 538 @le_S_S @le_S_S @le_O_n 539 2: 540 assumption 541 ] 542 ] 543 ] 544 ] XXX: blah! *) 417 % 545 418 qed. 546 419 547 definition fetch: BitVectorTrie Byte 16 → ∀program_counter: Word.548 Σret: instruction × Word × nat. nat_of_bitvector … program_counter < nat_of_bitvector … (\snd (\fst ret))≝420 definition fetch: ∀code_memory: BitVectorTrie Byte 16. 421 ∀program_counter: Word. instruction × Word × nat ≝ 549 422 λpmem: BitVectorTrie Byte 16. 550 423 λpc: Word. 551 let 〈word, byte〉 ≝ next pmem pc ? in 552 fetch0 pmem word byte ?. 553 cases daemon (* XXX: todo, proofs about size of pc *) 554 qed. 424 let 〈word, byte〉 ≝ next pmem pc in 425 fetch0 pmem word byte. 426 427 let rec fetch_program_counter_n 428 (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word) 429 on n: Word ≝ 430 match n with 431 [ O ⇒ program_counter 432  S n ⇒ 433 let tail_pc ≝ fetch_program_counter_n n code_memory program_counter in 434 let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in 435 program_counter 436 ].
Note: See TracChangeset
for help on using the changeset viewer.