Changeset 1598 for src/ASM/Fetch.ma
 Timestamp:
 Dec 12, 2011, 5:53:36 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Fetch.ma
r1597 r1598 38 38 qed. 39 39 40 axiom o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p: 41 ∀m, n, o, p: nat. 42 p < o → m < n  o → m < n  p. 43 44 lemma pair_eq_1_jmeq: 45 ∀a, b: Type[0]. 46 ∀a1, a2: a. 47 ∀b1, b2: b. 48 〈a1, b1〉 ≃ 〈a2, b2〉 → a1 = a2. 49 #a #b #a1 #a2 #b1 #b2 #assm 50 cases daemon (* XXX: no jm discrimination for pairs *) 51 qed. 52 53 lemma prod_fst_jmeq: 54 ∀a, b: Type[0]. 55 ∀p: a × b. 56 ∀l: a. 57 ∀r: b. 58 p ≃ 〈l, r〉 → l = fst … p. 59 #a #b #p #l #r 60 cases p #aa #bb #assm @sym_eq 61 lapply (pair_eq_1_jmeq a b aa l bb r assm) 62 #assm assumption 63 qed. 64 65 lemma lt_to_le: 66 ∀m, n: nat. 67 m < n → m ≤ n. 68 #m #n #assm /2 by le_S_to_le/ 69 qed. 70 71 lemma Prod_inv_rect_Type0: 72 ∀A,B. ∀P: A × B → Type[0].∀ab. 73 (∀a,b. ab = 〈a,b〉 → P 〈a,b〉) → P ab. 74 #A #B #P * /2/ 75 qed. 76 77 notation > "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)" 78 with precedence 10 79 for @{ Prod_inv_rect_Type0 ??? $t (λ${ident x}.λ${ident y}.λ${ident H}.$s) }. 80 81 notation < "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)" 82 with precedence 10 83 for @{ Prod_inv_rect_Type0 $z $w $r $t (λ${ident x}:$X.λ${ident y}:$Y.λ${ident H}:$h.$s) }. 84 85 lemma breakup_pair' : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:∀a:A.∀b:B. x=〈a,b〉 → C. 86 R (P (\fst x) (\snd x) ?) → R (let 〈a,b〉 {H} ≝ x in P a b H). 87 [2: // ] 88 #A #B #C *; normalize /2/ 89 qed. 90 40 91 (* timings taken from SIEMENS *) 41 92 42 93 definition fetch0: BitVectorTrie Byte 16 → ∀program_counter: Word. Byte → 43 94 nat_of_bitvector … program_counter < code_memory_size  24 (* 3 bytes *) → 44 Σret: instruction × Word × nat. nat_of_bitvector … program_counter <nat_of_bitvector … (\snd (\fst ret)) ≝95 Σret: instruction × Word × nat. nat_of_bitvector … program_counter ≤ nat_of_bitvector … (\snd (\fst ret)) ≝ 45 96 λpmem. 46 97 λpc. … … 59 110 else 60 111 let 〈b,v〉≝ head … v in if b then 61 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉112 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉 62 113 else 63 114 〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉 … … 67 118 else 68 119 let 〈b,v〉≝ head … v in if b then 69 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉120 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉 70 121 else 71 122 〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉 … … 79 130 else 80 131 let 〈b,v〉≝ head … v in if b then 81 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉132 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉 82 133 else 83 134 〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉 … … 87 138 else 88 139 let 〈b,v〉≝ head … v in if b then 89 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉140 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉 90 141 else 91 142 〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉 … … 93 144 let 〈b,v〉≝ head … v in if b then 94 145 let 〈b,v〉≝ head … v in if b then 95 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉146 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉 96 147 else 97 148 let 〈b,v〉≝ head … v in if b then … … 100 151 else 101 152 let 〈b,v〉≝ head … v in if b then 102 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉153 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉 103 154 else 104 155 〈〈RealInstruction (DA … ACC_A), pc〉, 1〉 … … 108 159 〈〈RealInstruction (SETB … CARRY), pc〉, 1〉 109 160 else 110 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉111 else 112 let 〈b,v〉≝ head … v in if b then 113 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉114 else 115 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉161 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉 162 else 163 let 〈b,v〉≝ head … v in if b then 164 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 165 else 166 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉 116 167 else 117 168 let 〈b,v〉≝ head … v in if b then … … 123 174 else 124 175 let 〈b,v〉≝ head … v in if b then 125 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉176 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉 126 177 else 127 178 〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉 … … 131 182 〈〈RealInstruction (CLR … CARRY), pc〉, 1〉 132 183 else 133 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉134 else 135 let 〈b,v〉≝ head … v in if b then 136 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉137 else 138 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉184 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉 185 else 186 let 〈b,v〉≝ head … v in if b then 187 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 188 else 189 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉 139 190 else 140 191 let 〈b,v〉≝ head … v in if b then 141 192 let 〈b,v〉≝ head … v in if b then 142 193 let 〈b,v〉≝ head … v in if b then 143 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉144 else 145 let 〈b,v〉≝ head … v in if b then 146 let 〈b,v〉≝ head … v in if b then 147 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉148 else 149 let 〈b,v〉≝ head … v in if b then 150 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉151 else 152 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉194 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉 195 else 196 let 〈b,v〉≝ head … v in if b then 197 let 〈b,v〉≝ head … v in if b then 198 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉 199 else 200 let 〈b,v〉≝ head … v in if b then 201 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉 202 else 203 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉 153 204 else 154 205 let 〈b,v〉≝ head … v in if b then … … 156 207 〈〈RealInstruction (CPL … CARRY), pc〉, 1〉 157 208 else 158 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉159 else 160 let 〈b,v〉≝ head … v in if b then 161 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉162 else 163 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉164 else 165 let 〈b,v〉≝ head … v in if b then 166 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉167 else 168 let 〈b,v〉≝ head … v in if b then 169 let 〈b,v〉≝ head … v in if b then 170 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉209 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉 210 else 211 let 〈b,v〉≝ head … v in if b then 212 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 213 else 214 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉 215 else 216 let 〈b,v〉≝ head … v in if b then 217 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉 218 else 219 let 〈b,v〉≝ head … v in if b then 220 let 〈b,v〉≝ head … v in if b then 221 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉 171 222 else 172 223 〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉 … … 176 227 〈〈RealInstruction (INC … DPTR), pc〉, 2〉 177 228 else 178 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉179 else 180 let 〈b,v〉≝ head … v in if b then 181 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉182 else 183 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉229 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉 230 else 231 let 〈b,v〉≝ head … v in if b then 232 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 233 else 234 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉 184 235 else 185 236 let 〈b,v〉≝ head … v in if b then … … 192 243 else 193 244 let 〈b,v〉≝ head … v in if b then 194 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉195 else 196 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉245 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉 246 else 247 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉 197 248 else 198 249 let 〈b,v〉≝ head … v in if b then … … 200 251 〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉 201 252 else 202 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉203 else 204 let 〈b,v〉≝ head … v in if b then 205 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉206 else 207 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉208 else 209 let 〈b,v〉≝ head … v in if b then 210 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉211 else 212 let 〈b,v〉≝ head … v in if b then 213 let 〈b,v〉≝ head … v in if b then 214 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉215 else 216 let 〈b,v〉≝ head … v in if b then 217 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉253 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉 254 else 255 let 〈b,v〉≝ head … v in if b then 256 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 257 else 258 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉 259 else 260 let 〈b,v〉≝ head … v in if b then 261 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉 262 else 263 let 〈b,v〉≝ head … v in if b then 264 let 〈b,v〉≝ head … v in if b then 265 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉 266 else 267 let 〈b,v〉≝ head … v in if b then 268 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉 218 269 else 219 270 〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉 … … 223 274 〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉 224 275 else 225 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉226 else 227 let 〈b,v〉≝ head … v in if b then 228 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉229 else 230 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉276 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉 277 else 278 let 〈b,v〉≝ head … v in if b then 279 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 280 else 281 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉 231 282 else 232 283 let 〈b,v〉≝ head … v in if b then … … 234 285 let 〈b,v〉≝ head … v in if b then 235 286 let 〈b,v〉≝ head … v in if b then 236 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉237 else 238 let 〈b,v〉≝ head … v in if b then 239 let 〈b,v〉≝ head … v in if b then 240 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉241 else 242 let 〈b,v〉≝ head … v in if b then 243 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉244 else 245 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉287 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,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 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉 292 else 293 let 〈b,v〉≝ head … v in if b then 294 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉 295 else 296 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉 246 297 else 247 298 let 〈b,v〉≝ head … v in if b then … … 249 300 〈〈JMP … INDIRECT_DPTR, pc〉, 2〉 250 301 else 251 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉252 else 253 let 〈b,v〉≝ head … v in if b then 254 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉255 else 256 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉302 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉 303 else 304 let 〈b,v〉≝ head … v in if b then 305 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 306 else 307 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉 257 308 else 258 309 let 〈b,v〉≝ head … v in if b then … … 264 315 else 265 316 let 〈b,v〉≝ head … v in if b then 266 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉267 else 268 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉269 else 270 let 〈b,v〉≝ head … v in if b then 271 let 〈b,v〉≝ head … v in if b then 272 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉273 else 274 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉275 else 276 let 〈b,v〉≝ head … v in if b then 277 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉278 else 279 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉317 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉 318 else 319 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉 320 else 321 let 〈b,v〉≝ head … v in if b then 322 let 〈b,v〉≝ head … v in if b then 323 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉 324 else 325 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉 326 else 327 let 〈b,v〉≝ head … v in if b then 328 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 329 else 330 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉 280 331 else 281 332 let 〈b,v〉≝ head … v in if b then … … 288 339 else 289 340 let 〈b,v〉≝ head … v in if b then 290 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉291 else 292 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉293 else 294 let 〈b,v〉≝ head … v in if b then 295 let 〈b,v〉≝ head … v in if b then 296 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉297 else 298 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉299 else 300 let 〈b,v〉≝ head … v in if b then 301 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉302 else 303 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉341 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉 342 else 343 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉 344 else 345 let 〈b,v〉≝ head … v in if b then 346 let 〈b,v〉≝ head … v in if b then 347 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉 348 else 349 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉 350 else 351 let 〈b,v〉≝ head … v in if b then 352 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 353 else 354 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉 304 355 else 305 356 let 〈b,v〉≝ head … v in if b then … … 311 362 else 312 363 let 〈b,v〉≝ head … v in if b then 313 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉314 else 315 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉316 else 317 let 〈b,v〉≝ head … v in if b then 318 let 〈b,v〉≝ head … v in if b then 319 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉320 else 321 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉322 else 323 let 〈b,v〉≝ head … v in if b then 324 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉325 else 326 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉364 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉 365 else 366 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉 367 else 368 let 〈b,v〉≝ head … v in if b then 369 let 〈b,v〉≝ head … v in if b then 370 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉 371 else 372 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉 373 else 374 let 〈b,v〉≝ head … v in if b then 375 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 376 else 377 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉 327 378 else 328 379 let 〈b,v〉≝ head … v in if b then … … 336 387 else 337 388 let 〈b,v〉≝ head … v in if b then 338 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉339 else 340 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉389 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉 390 else 391 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉 341 392 else 342 393 let 〈b,v〉≝ head … v in if b then … … 347 398 else 348 399 let 〈b,v〉≝ head … v in if b then 349 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉350 else 351 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉400 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 401 else 402 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 352 403 else 353 404 let 〈b,v〉≝ head … v in if b then … … 359 410 else 360 411 let 〈b,v〉≝ head … v in if b then 361 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉362 else 363 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉412 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉 413 else 414 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉 364 415 else 365 416 let 〈b,v〉≝ head … v in if b then … … 370 421 else 371 422 let 〈b,v〉≝ head … v in if b then 372 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉373 else 374 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉423 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 424 else 425 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 375 426 else 376 427 let 〈b,v〉≝ head … v in if b then … … 383 434 else 384 435 let 〈b,v〉≝ head … v in if b then 385 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉436 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉 386 437 else 387 438 〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉 … … 391 442 〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉 392 443 else 393 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉394 else 395 let 〈b,v〉≝ head … v in if b then 396 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉397 else 398 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉444 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉 445 else 446 let 〈b,v〉≝ head … v in if b then 447 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 448 else 449 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 399 450 else 400 451 let 〈b,v〉≝ head … v in if b then … … 406 457 else 407 458 let 〈b,v〉≝ head … v in if b then 408 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉459 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉 409 460 else 410 461 〈〈RealInstruction (INC … ACC_A), pc〉, 1〉 … … 414 465 〈〈RealInstruction (RR … ACC_A), pc〉, 1〉 415 466 else 416 let 〈pc,b1〉 ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉417 else 418 let 〈b,v〉≝ head … v in if b then 419 let 〈pc,b1〉 ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉467 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉 468 else 469 let 〈b,v〉≝ head … v in if b then 470 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 420 471 else 421 472 〈〈RealInstruction (NOP …), pc〉, 1〉. 422 473 try % 474 try ( 475 @(o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p 476 (nat_of_bitvector 16 pc) code_memory_size 24 1 477 (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof) 478 ) 479 [1,2,3,4,5,6,7,8: 480 @breakup_pair' cases (next pmem pc ?) 481 normalize * normalize #pc' #byte @lt_to_le 482 3: 483 @breakup_pair' cases (next pmem pc ?) 484 normalize * normalize #pc' #byte @lt_to_le 485 2: 486 @breakup_pair' cases(next pmem pc ?) 487 normalize * normalize #pc' #byte @lt_to_le 488 [ 489  92: 490 cases (next ???) in EQ; * #pc' #content #H #EQ whd in EQ:(??%?); destruct 491 492 493 lapply(eq_pair_fst_snd ? ? (next pmem pc ?)) 494 #assm >assm 495 cut(nat_of_bitvector … pc < nat_of_bitvector … 496 (\fst (next pmem pc 497 (o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p (nat_of_bitvector 16 pc) 498 code_memory_size 24 1 (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof)))) 499 [ @sig2 500  #assm @lt_to_le assumption 501 ] 502 92: 503 check next. 504 lapply pc pc 505 @sig2 423 506 cases daemon (* XXX: requires rewrite of the above to make it more russell friendly *) 424 507 qed.
Note: See TracChangeset
for help on using the changeset viewer.