[985] | 1 | include "ASM/BitVector.ma". |
---|
[1515] | 2 | include "common/Identifiers.ma". |
---|
| 3 | include "common/CostLabel.ma". |
---|
[1882] | 4 | include "common/LabelledObjects.ma". |
---|
[2647] | 5 | include "joint/String.ma". |
---|
[475] | 6 | |
---|
[1515] | 7 | definition Identifier ≝ identifier ASMTag. |
---|
| 8 | definition toASM_ident : ∀tag. identifier tag → Identifier ≝ λt,i. match i with [ an_identifier id ⇒ an_identifier ASMTag id ]. |
---|
[985] | 9 | |
---|
[475] | 10 | inductive addressing_mode: Type[0] ≝ |
---|
| 11 | DIRECT: Byte → addressing_mode |
---|
| 12 | | INDIRECT: Bit → addressing_mode |
---|
| 13 | | EXT_INDIRECT: Bit → addressing_mode |
---|
[698] | 14 | | REGISTER: BitVector 3 → addressing_mode |
---|
[475] | 15 | | ACC_A: addressing_mode |
---|
| 16 | | ACC_B: addressing_mode |
---|
| 17 | | DPTR: addressing_mode |
---|
| 18 | | DATA: Byte → addressing_mode |
---|
| 19 | | DATA16: Word → addressing_mode |
---|
| 20 | | ACC_DPTR: addressing_mode |
---|
| 21 | | ACC_PC: addressing_mode |
---|
| 22 | | EXT_INDIRECT_DPTR: addressing_mode |
---|
| 23 | | INDIRECT_DPTR: addressing_mode |
---|
| 24 | | CARRY: addressing_mode |
---|
| 25 | | BIT_ADDR: Byte → addressing_mode |
---|
| 26 | | N_BIT_ADDR: Byte → addressing_mode |
---|
| 27 | | RELATIVE: Byte → addressing_mode |
---|
| 28 | | ADDR11: Word11 → addressing_mode |
---|
| 29 | | ADDR16: Word → addressing_mode. |
---|
| 30 | |
---|
[2124] | 31 | definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝ |
---|
| 32 | λa, b: addressing_mode. |
---|
| 33 | match a with |
---|
| 34 | [ DIRECT d ⇒ |
---|
| 35 | match b with |
---|
| 36 | [ DIRECT e ⇒ eq_bv ? d e |
---|
| 37 | | _ ⇒ false |
---|
| 38 | ] |
---|
| 39 | | INDIRECT b' ⇒ |
---|
| 40 | match b with |
---|
| 41 | [ INDIRECT e ⇒ eq_b b' e |
---|
| 42 | | _ ⇒ false |
---|
| 43 | ] |
---|
| 44 | | EXT_INDIRECT b' ⇒ |
---|
| 45 | match b with |
---|
| 46 | [ EXT_INDIRECT e ⇒ eq_b b' e |
---|
| 47 | | _ ⇒ false |
---|
| 48 | ] |
---|
| 49 | | REGISTER bv ⇒ |
---|
| 50 | match b with |
---|
| 51 | [ REGISTER bv' ⇒ eq_bv ? bv bv' |
---|
| 52 | | _ ⇒ false |
---|
| 53 | ] |
---|
| 54 | | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ] |
---|
| 55 | | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ] |
---|
| 56 | | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ] |
---|
| 57 | | DATA b' ⇒ |
---|
| 58 | match b with |
---|
| 59 | [ DATA e ⇒ eq_bv ? b' e |
---|
| 60 | | _ ⇒ false |
---|
| 61 | ] |
---|
| 62 | | DATA16 w ⇒ |
---|
| 63 | match b with |
---|
| 64 | [ DATA16 e ⇒ eq_bv ? w e |
---|
| 65 | | _ ⇒ false |
---|
| 66 | ] |
---|
| 67 | | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ] |
---|
| 68 | | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ] |
---|
| 69 | | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ] |
---|
| 70 | | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ] |
---|
| 71 | | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ] |
---|
| 72 | | BIT_ADDR b' ⇒ |
---|
| 73 | match b with |
---|
| 74 | [ BIT_ADDR e ⇒ eq_bv ? b' e |
---|
| 75 | | _ ⇒ false |
---|
| 76 | ] |
---|
| 77 | | N_BIT_ADDR b' ⇒ |
---|
| 78 | match b with |
---|
| 79 | [ N_BIT_ADDR e ⇒ eq_bv ? b' e |
---|
| 80 | | _ ⇒ false |
---|
| 81 | ] |
---|
| 82 | | RELATIVE n ⇒ |
---|
| 83 | match b with |
---|
| 84 | [ RELATIVE e ⇒ eq_bv ? n e |
---|
| 85 | | _ ⇒ false |
---|
| 86 | ] |
---|
| 87 | | ADDR11 w ⇒ |
---|
| 88 | match b with |
---|
| 89 | [ ADDR11 e ⇒ eq_bv ? w e |
---|
| 90 | | _ ⇒ false |
---|
| 91 | ] |
---|
| 92 | | ADDR16 w ⇒ |
---|
| 93 | match b with |
---|
| 94 | [ ADDR16 e ⇒ eq_bv ? w e |
---|
| 95 | | _ ⇒ false |
---|
| 96 | ] |
---|
| 97 | ]. |
---|
| 98 | |
---|
| 99 | lemma eq_addressing_mode_refl: |
---|
| 100 | ∀a. eq_addressing_mode a a = true. |
---|
| 101 | #a |
---|
| 102 | cases a try #arg1 try #arg2 |
---|
| 103 | try @eq_bv_refl try @eq_b_refl |
---|
| 104 | try normalize % |
---|
| 105 | qed. |
---|
| 106 | |
---|
[757] | 107 | (* dpm: renamed register to registr to avoid clash with brian's types *) |
---|
[475] | 108 | inductive addressing_mode_tag : Type[0] ≝ |
---|
| 109 | direct: addressing_mode_tag |
---|
| 110 | | indirect: addressing_mode_tag |
---|
| 111 | | ext_indirect: addressing_mode_tag |
---|
[757] | 112 | | registr: addressing_mode_tag |
---|
[475] | 113 | | acc_a: addressing_mode_tag |
---|
| 114 | | acc_b: addressing_mode_tag |
---|
| 115 | | dptr: addressing_mode_tag |
---|
| 116 | | data: addressing_mode_tag |
---|
| 117 | | data16: addressing_mode_tag |
---|
| 118 | | acc_dptr: addressing_mode_tag |
---|
| 119 | | acc_pc: addressing_mode_tag |
---|
| 120 | | ext_indirect_dptr: addressing_mode_tag |
---|
| 121 | | indirect_dptr: addressing_mode_tag |
---|
| 122 | | carry: addressing_mode_tag |
---|
| 123 | | bit_addr: addressing_mode_tag |
---|
| 124 | | n_bit_addr: addressing_mode_tag |
---|
| 125 | | relative: addressing_mode_tag |
---|
| 126 | | addr11: addressing_mode_tag |
---|
| 127 | | addr16: addressing_mode_tag. |
---|
| 128 | |
---|
| 129 | definition eq_a ≝ |
---|
| 130 | λa, b: addressing_mode_tag. |
---|
| 131 | match a with |
---|
| 132 | [ direct ⇒ match b with [ direct ⇒ true | _ ⇒ false ] |
---|
| 133 | | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ] |
---|
| 134 | | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ] |
---|
[757] | 135 | | registr ⇒ match b with [ registr ⇒ true | _ ⇒ false ] |
---|
[475] | 136 | | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ] |
---|
| 137 | | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ] |
---|
| 138 | | dptr ⇒ match b with [ dptr ⇒ true | _ ⇒ false ] |
---|
| 139 | | data ⇒ match b with [ data ⇒ true | _ ⇒ false ] |
---|
| 140 | | data16 ⇒ match b with [ data16 ⇒ true | _ ⇒ false ] |
---|
| 141 | | acc_dptr ⇒ match b with [ acc_dptr ⇒ true | _ ⇒ false ] |
---|
| 142 | | acc_pc ⇒ match b with [ acc_pc ⇒ true | _ ⇒ false ] |
---|
| 143 | | ext_indirect_dptr ⇒ match b with [ ext_indirect_dptr ⇒ true | _ ⇒ false ] |
---|
| 144 | | indirect_dptr ⇒ match b with [ indirect_dptr ⇒ true | _ ⇒ false ] |
---|
| 145 | | carry ⇒ match b with [ carry ⇒ true | _ ⇒ false ] |
---|
| 146 | | bit_addr ⇒ match b with [ bit_addr ⇒ true | _ ⇒ false ] |
---|
| 147 | | n_bit_addr ⇒ match b with [ n_bit_addr ⇒ true | _ ⇒ false ] |
---|
| 148 | | relative ⇒ match b with [ relative ⇒ true | _ ⇒ false ] |
---|
| 149 | | addr11 ⇒ match b with [ addr11 ⇒ true | _ ⇒ false ] |
---|
| 150 | | addr16 ⇒ match b with [ addr16 ⇒ true | _ ⇒ false ] |
---|
| 151 | ]. |
---|
| 152 | |
---|
[2032] | 153 | lemma eq_a_to_eq: |
---|
| 154 | ∀a,b. |
---|
| 155 | eq_a a b = true → a = b. |
---|
| 156 | #a #b |
---|
| 157 | cases a cases b |
---|
| 158 | #K |
---|
| 159 | try cases (eq_true_false K) |
---|
| 160 | % |
---|
| 161 | qed. |
---|
| 162 | |
---|
| 163 | lemma eq_a_reflexive: |
---|
| 164 | ∀a. eq_a a a = true. |
---|
| 165 | #a cases a % |
---|
| 166 | qed. |
---|
| 167 | |
---|
| 168 | let rec member_addressing_mode_tag |
---|
| 169 | (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag) |
---|
| 170 | on v: Prop ≝ |
---|
| 171 | match v with |
---|
| 172 | [ VEmpty ⇒ False |
---|
| 173 | | VCons n' hd tl ⇒ |
---|
| 174 | bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a |
---|
| 175 | ]. |
---|
| 176 | |
---|
| 177 | lemma mem_decidable: |
---|
| 178 | ∀n: nat. |
---|
| 179 | ∀v: Vector addressing_mode_tag n. |
---|
| 180 | ∀element: addressing_mode_tag. |
---|
| 181 | mem … eq_a n v element = true ∨ |
---|
| 182 | mem … eq_a … v element = false. |
---|
| 183 | #n #v #element // |
---|
| 184 | qed. |
---|
| 185 | |
---|
| 186 | lemma eq_a_elim: |
---|
| 187 | ∀tag. |
---|
| 188 | ∀hd. |
---|
| 189 | ∀P: bool → Prop. |
---|
| 190 | (tag = hd → P (true)) → |
---|
| 191 | (tag ≠ hd → P (false)) → |
---|
| 192 | P (eq_a tag hd). |
---|
| 193 | #tag #hd #P |
---|
| 194 | cases tag |
---|
| 195 | cases hd |
---|
| 196 | #true_hyp #false_hyp |
---|
| 197 | try @false_hyp |
---|
| 198 | try @true_hyp |
---|
| 199 | try % |
---|
| 200 | #absurd destruct(absurd) |
---|
| 201 | qed. |
---|
| 202 | |
---|
[475] | 203 | (* to avoid expansion... *) |
---|
| 204 | let rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝ |
---|
| 205 | match d with |
---|
| 206 | [ direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ] |
---|
| 207 | | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ] |
---|
| 208 | | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ] |
---|
[757] | 209 | | registr ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ] |
---|
[475] | 210 | | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ] |
---|
| 211 | | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ] |
---|
| 212 | | dptr ⇒ match A with [ DPTR ⇒ true | _ ⇒ false ] |
---|
| 213 | | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ] |
---|
| 214 | | data16 ⇒ match A with [ DATA16 _ ⇒ true | _ ⇒ false ] |
---|
| 215 | | acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true | _ ⇒ false ] |
---|
| 216 | | acc_pc ⇒ match A with [ ACC_PC ⇒ true | _ ⇒ false ] |
---|
| 217 | | ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ] |
---|
| 218 | | indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ] |
---|
| 219 | | carry ⇒ match A with [ CARRY ⇒ true | _ ⇒ false ] |
---|
| 220 | | bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true | _ ⇒ false ] |
---|
| 221 | | n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true | _ ⇒ false ] |
---|
| 222 | | relative ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ] |
---|
| 223 | | addr11 ⇒ match A with [ ADDR11 _ ⇒ true | _ ⇒ false ] |
---|
[1112] | 224 | | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ] |
---|
| 225 | ]. |
---|
[475] | 226 | |
---|
[2032] | 227 | lemma is_a_decidable: |
---|
| 228 | ∀hd. |
---|
| 229 | ∀element. |
---|
| 230 | is_a hd element = true ∨ is_a hd element = false. |
---|
| 231 | #hd #element // |
---|
| 232 | qed. |
---|
[475] | 233 | |
---|
| 234 | let rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝ |
---|
| 235 | match l return λm.λ_:Vector addressing_mode_tag m.bool with |
---|
| 236 | [ VEmpty ⇒ false |
---|
| 237 | | VCons m he (tl: Vector addressing_mode_tag m) ⇒ |
---|
| 238 | is_a he A ∨ is_in ? tl A ]. |
---|
| 239 | |
---|
[2124] | 240 | definition is_in_cons_elim: |
---|
| 241 | ∀len.∀hd,tl.∀m:addressing_mode |
---|
| 242 | .is_in (S len) (hd:::tl) m → |
---|
| 243 | (bool_to_Prop (is_a hd m)) ∨ (bool_to_Prop (is_in len tl m)). |
---|
| 244 | #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN; |
---|
| 245 | cases (is_a hd am) in ISIN; /2/ |
---|
| 246 | qed. |
---|
| 247 | |
---|
[2128] | 248 | lemma is_in_monotonic_wrt_append: |
---|
| 249 | ∀m, n: nat. |
---|
| 250 | ∀p: Vector addressing_mode_tag m. |
---|
| 251 | ∀q: Vector addressing_mode_tag n. |
---|
| 252 | ∀to_search: addressing_mode. |
---|
| 253 | bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search). |
---|
| 254 | #m #n #p #q #to_search #assm |
---|
| 255 | elim q try assumption |
---|
| 256 | #n' #hd #tl #inductive_hypothesis |
---|
| 257 | normalize |
---|
| 258 | cases (is_a ??) try @I |
---|
| 259 | >inductive_hypothesis @I |
---|
| 260 | qed. |
---|
| 261 | |
---|
| 262 | corollary is_in_hd_tl: |
---|
| 263 | ∀to_search: addressing_mode. |
---|
| 264 | ∀hd: addressing_mode_tag. |
---|
| 265 | ∀n: nat. |
---|
| 266 | ∀v: Vector addressing_mode_tag n. |
---|
| 267 | bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search). |
---|
| 268 | #to_search #hd #n #v |
---|
| 269 | elim v |
---|
| 270 | [1: |
---|
| 271 | #absurd |
---|
| 272 | normalize in absurd; cases absurd |
---|
| 273 | |2: |
---|
| 274 | #n' #hd' #tl #inductive_hypothesis #assm |
---|
| 275 | >vector_cons_append >(vector_cons_append … hd' tl) |
---|
| 276 | @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search) |
---|
| 277 | assumption |
---|
| 278 | ] |
---|
| 279 | qed. |
---|
| 280 | |
---|
[2032] | 281 | lemma is_a_to_mem_to_is_in: |
---|
| 282 | ∀he,a,m,q. |
---|
| 283 | is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true. |
---|
| 284 | #he #a #m #q |
---|
| 285 | elim q |
---|
| 286 | [1: |
---|
| 287 | #_ #K assumption |
---|
| 288 | |2: |
---|
| 289 | #m' #t #q' #II #H1 #H2 |
---|
| 290 | normalize |
---|
| 291 | change with (orb ??) in H2:(??%?); |
---|
| 292 | cases (inclusive_disjunction_true … H2) |
---|
| 293 | [1: |
---|
| 294 | #K |
---|
| 295 | <(eq_a_to_eq … K) >H1 % |
---|
| 296 | |2: |
---|
| 297 | #K |
---|
| 298 | >II |
---|
| 299 | try assumption |
---|
| 300 | cases (is_a t a) |
---|
| 301 | normalize |
---|
| 302 | % |
---|
| 303 | ] |
---|
| 304 | ] |
---|
| 305 | qed. |
---|
| 306 | |
---|
| 307 | lemma is_a_true_to_is_in: |
---|
| 308 | ∀n: nat. |
---|
| 309 | ∀x: addressing_mode. |
---|
| 310 | ∀tag: addressing_mode_tag. |
---|
| 311 | ∀supervector: Vector addressing_mode_tag n. |
---|
| 312 | mem addressing_mode_tag eq_a n supervector tag → |
---|
| 313 | is_a tag x = true → |
---|
| 314 | is_in … supervector x. |
---|
| 315 | #n #x #tag #supervector |
---|
| 316 | elim supervector |
---|
| 317 | [1: |
---|
| 318 | #absurd cases absurd |
---|
| 319 | |2: |
---|
| 320 | #n' #hd #tl #inductive_hypothesis |
---|
| 321 | whd in match (mem … eq_a (S n') (hd:::tl) tag); |
---|
| 322 | @eq_a_elim normalize nodelta |
---|
| 323 | [1: |
---|
| 324 | #tag_hd_eq #irrelevant |
---|
| 325 | whd in match (is_in (S n') (hd:::tl) x); |
---|
| 326 | <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta |
---|
| 327 | @I |
---|
| 328 | |2: |
---|
| 329 | #tag_hd_neq |
---|
| 330 | whd in match (is_in (S n') (hd:::tl) x); |
---|
| 331 | change with ( |
---|
| 332 | mem … eq_a n' tl tag) |
---|
| 333 | in match (fold_right … n' ? false tl); |
---|
| 334 | #mem_hyp #is_a_hyp |
---|
| 335 | cases(is_a hd x) |
---|
| 336 | [1: |
---|
| 337 | normalize nodelta // |
---|
| 338 | |2: |
---|
| 339 | normalize nodelta |
---|
| 340 | @inductive_hypothesis assumption |
---|
| 341 | ] |
---|
| 342 | ] |
---|
| 343 | ] |
---|
| 344 | qed. |
---|
| 345 | |
---|
[475] | 346 | record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝ |
---|
| 347 | { |
---|
| 348 | subaddressing_modeel:> addressing_mode; |
---|
| 349 | subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel) |
---|
| 350 | }. |
---|
| 351 | |
---|
| 352 | coercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0] |
---|
| 353 | ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0]. |
---|
| 354 | |
---|
| 355 | coercion mk_subaddressing_mode : |
---|
| 356 | ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode. |
---|
| 357 | ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l |
---|
| 358 | ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?. |
---|
[2032] | 359 | |
---|
| 360 | lemma is_in_subvector_is_in_supervector: |
---|
| 361 | ∀m, n: nat. |
---|
| 362 | ∀subvector: Vector addressing_mode_tag m. |
---|
| 363 | ∀supervector: Vector addressing_mode_tag n. |
---|
| 364 | ∀element: addressing_mode. |
---|
| 365 | subvector_with … eq_a subvector supervector → |
---|
| 366 | is_in m subvector element → is_in n supervector element. |
---|
| 367 | #m #n #subvector #supervector #element |
---|
| 368 | elim subvector |
---|
| 369 | [1: |
---|
| 370 | #subvector_with_proof #is_in_proof |
---|
| 371 | cases is_in_proof |
---|
| 372 | |2: |
---|
| 373 | #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof |
---|
| 374 | whd in match (is_in … (hd':::tl') element); |
---|
| 375 | cases (is_a_decidable hd' element) |
---|
| 376 | [1: |
---|
| 377 | #is_a_true >is_a_true |
---|
| 378 | #irrelevant |
---|
| 379 | whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof; |
---|
| 380 | @(is_a_true_to_is_in … is_a_true) |
---|
| 381 | lapply(subvector_with_proof) |
---|
| 382 | cases(mem … eq_a n supervector hd') // |
---|
| 383 | |2: |
---|
| 384 | #is_a_false >is_a_false normalize nodelta |
---|
| 385 | #assm |
---|
| 386 | @inductive_hypothesis |
---|
| 387 | [1: |
---|
| 388 | generalize in match subvector_with_proof; |
---|
| 389 | whd in match (subvector_with … eq_a (hd':::tl') supervector); |
---|
| 390 | cases(mem_decidable n supervector hd') |
---|
| 391 | [1: |
---|
| 392 | #mem_true >mem_true normalize nodelta |
---|
| 393 | #assm assumption |
---|
| 394 | |2: |
---|
| 395 | #mem_false >mem_false #absurd |
---|
| 396 | cases absurd |
---|
| 397 | ] |
---|
| 398 | |2: |
---|
| 399 | assumption |
---|
| 400 | ] |
---|
| 401 | ] |
---|
| 402 | ] |
---|
| 403 | qed. |
---|
| 404 | |
---|
[2143] | 405 | (* XXX: move back into ASM.ma *) |
---|
| 406 | lemma subvector_with_to_subvector_with_tl: |
---|
| 407 | ∀n: nat. |
---|
| 408 | ∀m: nat. |
---|
| 409 | ∀v. |
---|
| 410 | ∀fixed_v. |
---|
| 411 | ∀proof: (subvector_with addressing_mode_tag n (S m) eq_a v fixed_v). |
---|
| 412 | ∀n': nat. |
---|
| 413 | ∀hd: addressing_mode_tag. |
---|
| 414 | ∀tl: Vector addressing_mode_tag n'. |
---|
| 415 | ∀m_refl: S n'=n. |
---|
| 416 | ∀v_refl: v≃hd:::tl. |
---|
| 417 | subvector_with addressing_mode_tag n' (S m) eq_a tl fixed_v. |
---|
| 418 | #n #m #v #fixed_v #proof #n' #hd #tl #m_refl #v_refl |
---|
| 419 | generalize in match proof; destruct |
---|
| 420 | whd in match (subvector_with … eq_a (hd:::tl) fixed_v); |
---|
| 421 | cases (mem … eq_a ? fixed_v hd) normalize nodelta |
---|
| 422 | [1: |
---|
| 423 | whd in match (subvector_with … eq_a tl fixed_v); |
---|
| 424 | #assm assumption |
---|
| 425 | |2: |
---|
| 426 | normalize in ⊢ (% → ?); |
---|
| 427 | #absurd cases absurd |
---|
| 428 | ] |
---|
| 429 | qed. |
---|
[2032] | 430 | |
---|
| 431 | let rec subaddressing_mode_elim_type |
---|
| 432 | (m: nat) (fixed_v: Vector addressing_mode_tag (S m)) (origaddr: fixed_v) |
---|
| 433 | (Q: fixed_v → Prop) |
---|
| 434 | (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v) |
---|
| 435 | on v: Prop ≝ |
---|
| 436 | match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with |
---|
| 437 | [ VEmpty ⇒ λm_refl. λv_refl. Q origaddr |
---|
| 438 | | VCons n' hd tl ⇒ λm_refl. λv_refl. |
---|
| 439 | let tail_call ≝ subaddressing_mode_elim_type m fixed_v origaddr Q n' tl ? |
---|
| 440 | in |
---|
| 441 | match hd return λa: addressing_mode_tag. a = hd → ? with |
---|
| 442 | [ addr11 ⇒ λhd_refl. (∀w: Word11. Q (ADDR11 w)) → tail_call |
---|
| 443 | | addr16 ⇒ λhd_refl. (∀w: Word. Q (ADDR16 w)) → tail_call |
---|
| 444 | | direct ⇒ λhd_refl. (∀w: Byte. Q (DIRECT w)) → tail_call |
---|
| 445 | | indirect ⇒ λhd_refl. (∀w: Bit. Q (INDIRECT w)) → tail_call |
---|
| 446 | | ext_indirect ⇒ λhd_refl. (∀w: Bit. Q (EXT_INDIRECT w)) → tail_call |
---|
| 447 | | acc_a ⇒ λhd_refl. Q ACC_A → tail_call |
---|
| 448 | | registr ⇒ λhd_refl. (∀w: BitVector 3. Q (REGISTER w)) → tail_call |
---|
| 449 | | acc_b ⇒ λhd_refl. Q ACC_B → tail_call |
---|
| 450 | | dptr ⇒ λhd_refl. Q DPTR → tail_call |
---|
| 451 | | data ⇒ λhd_refl. (∀w: Byte. Q (DATA w)) → tail_call |
---|
| 452 | | data16 ⇒ λhd_refl. (∀w: Word. Q (DATA16 w)) → tail_call |
---|
| 453 | | acc_dptr ⇒ λhd_refl. Q ACC_DPTR → tail_call |
---|
| 454 | | acc_pc ⇒ λhd_refl. Q ACC_PC → tail_call |
---|
| 455 | | ext_indirect_dptr ⇒ λhd_refl. Q EXT_INDIRECT_DPTR → tail_call |
---|
| 456 | | indirect_dptr ⇒ λhd_refl. Q INDIRECT_DPTR → tail_call |
---|
| 457 | | carry ⇒ λhd_refl. Q CARRY → tail_call |
---|
| 458 | | bit_addr ⇒ λhd_refl. (∀w: Byte. Q (BIT_ADDR w)) → tail_call |
---|
| 459 | | n_bit_addr ⇒ λhd_refl. (∀w: Byte. Q (N_BIT_ADDR w)) → tail_call |
---|
| 460 | | relative ⇒ λhd_refl. (∀w: Byte. Q (RELATIVE w)) → tail_call |
---|
| 461 | ] (refl … hd) |
---|
| 462 | ] (refl … n) (refl_jmeq … v). |
---|
| 463 | [20: |
---|
[2143] | 464 | @(subvector_with_to_subvector_with_tl … proof … m_refl v_refl) |
---|
[2032] | 465 | ] |
---|
| 466 | @(is_in_subvector_is_in_supervector … proof) |
---|
| 467 | destruct @I |
---|
| 468 | qed. |
---|
| 469 | |
---|
| 470 | lemma subaddressing_mode_elim0: |
---|
| 471 | ∀n: nat. |
---|
| 472 | ∀v: Vector addressing_mode_tag (S n). |
---|
| 473 | ∀addr: v. |
---|
| 474 | ∀Q: v → Prop. |
---|
| 475 | ∀m,w,H. |
---|
| 476 | (∀xaddr: v. ¬ is_in … w xaddr → Q xaddr) → |
---|
| 477 | subaddressing_mode_elim_type n v addr Q m w H. |
---|
[2143] | 478 | #n #v #addr #Q #m #w elim w |
---|
| 479 | [1: |
---|
| 480 | /2/ |
---|
| 481 | |2: |
---|
| 482 | #n' #hd #tl #IH cases hd #H |
---|
| 483 | #INV whd #PO @IH #xaddr cases xaddr * |
---|
| 484 | try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV |
---|
| 485 | @ALREADYSEEN |
---|
| 486 | ] |
---|
[2032] | 487 | qed. |
---|
| 488 | |
---|
| 489 | lemma subaddressing_mode_elim: |
---|
| 490 | ∀n: nat. |
---|
| 491 | ∀v: Vector addressing_mode_tag (S n). |
---|
| 492 | ∀addr: v. |
---|
| 493 | ∀Q: v → Prop. |
---|
| 494 | subaddressing_mode_elim_type n v addr Q (S n) v ?. |
---|
[2143] | 495 | [1: |
---|
| 496 | #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; // |
---|
| 497 | |2: |
---|
| 498 | @subvector_with_refl @eq_a_reflexive |
---|
| 499 | ] |
---|
[2032] | 500 | qed. |
---|
[832] | 501 | |
---|
[475] | 502 | inductive preinstruction (A: Type[0]) : Type[0] ≝ |
---|
[757] | 503 | ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A |
---|
| 504 | | ADDC: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A |
---|
| 505 | | SUBB: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A |
---|
| 506 | | INC: [[ acc_a ; registr ; direct ; indirect ; dptr ]] → preinstruction A |
---|
| 507 | | DEC: [[ acc_a ; registr ; direct ; indirect ]] → preinstruction A |
---|
[475] | 508 | | MUL: [[acc_a]] → [[acc_b]] → preinstruction A |
---|
| 509 | | DIV: [[acc_a]] → [[acc_b]] → preinstruction A |
---|
| 510 | | DA: [[acc_a]] → preinstruction A |
---|
| 511 | |
---|
[820] | 512 | (* conditional jumps *) |
---|
| 513 | | JC: A → preinstruction A |
---|
| 514 | | JNC: A → preinstruction A |
---|
| 515 | | JB: [[bit_addr]] → A → preinstruction A |
---|
| 516 | | JNB: [[bit_addr]] → A → preinstruction A |
---|
| 517 | | JBC: [[bit_addr]] → A → preinstruction A |
---|
| 518 | | JZ: A → preinstruction A |
---|
| 519 | | JNZ: A → preinstruction A |
---|
| 520 | | CJNE: |
---|
| 521 | [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → preinstruction A |
---|
| 522 | | DJNZ: [[registr ; direct]] → A → preinstruction A |
---|
[475] | 523 | (* logical operations *) |
---|
| 524 | | ANL: |
---|
[757] | 525 | [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎ |
---|
[475] | 526 | [[direct]] × [[ acc_a ; data ]] ⊎ |
---|
| 527 | [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A |
---|
| 528 | | ORL: |
---|
[757] | 529 | [[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎ |
---|
[475] | 530 | [[direct]] × [[ acc_a ; data ]] ⊎ |
---|
| 531 | [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A |
---|
| 532 | | XRL: |
---|
[757] | 533 | [[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎ |
---|
[475] | 534 | [[direct]] × [[ acc_a ; data ]] → preinstruction A |
---|
| 535 | | CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A |
---|
| 536 | | CPL: [[ acc_a ; carry ; bit_addr ]] → preinstruction A |
---|
| 537 | | RL: [[acc_a]] → preinstruction A |
---|
| 538 | | RLC: [[acc_a]] → preinstruction A |
---|
| 539 | | RR: [[acc_a]] → preinstruction A |
---|
| 540 | | RRC: [[acc_a]] → preinstruction A |
---|
| 541 | | SWAP: [[acc_a]] → preinstruction A |
---|
| 542 | |
---|
| 543 | (* data transfer *) |
---|
| 544 | | MOV: |
---|
[757] | 545 | [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎ |
---|
| 546 | [[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎ |
---|
| 547 | [[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎ |
---|
[475] | 548 | [[dptr]] × [[data16]] ⊎ |
---|
| 549 | [[carry]] × [[bit_addr]] ⊎ |
---|
| 550 | [[bit_addr]] × [[carry]] → preinstruction A |
---|
| 551 | | MOVX: |
---|
| 552 | [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎ |
---|
| 553 | [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] → preinstruction A |
---|
| 554 | | SETB: [[ carry ; bit_addr ]] → preinstruction A |
---|
| 555 | | PUSH: [[direct]] → preinstruction A |
---|
| 556 | | POP: [[direct]] → preinstruction A |
---|
[757] | 557 | | XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A |
---|
[475] | 558 | | XCHD: [[acc_a]] → [[indirect]] → preinstruction A |
---|
| 559 | |
---|
| 560 | (* program branching *) |
---|
| 561 | | RET: preinstruction A |
---|
| 562 | | RETI: preinstruction A |
---|
| 563 | | NOP: preinstruction A. |
---|
| 564 | |
---|
[2124] | 565 | definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝ |
---|
| 566 | λi, j. |
---|
| 567 | match i with |
---|
| 568 | [ ADD arg1 arg2 ⇒ |
---|
| 569 | match j with |
---|
| 570 | [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 571 | | _ ⇒ false |
---|
| 572 | ] |
---|
| 573 | | ADDC arg1 arg2 ⇒ |
---|
| 574 | match j with |
---|
| 575 | [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 576 | | _ ⇒ false |
---|
| 577 | ] |
---|
| 578 | | SUBB arg1 arg2 ⇒ |
---|
| 579 | match j with |
---|
| 580 | [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 581 | | _ ⇒ false |
---|
| 582 | ] |
---|
| 583 | | INC arg ⇒ |
---|
| 584 | match j with |
---|
| 585 | [ INC arg' ⇒ eq_addressing_mode arg arg' |
---|
| 586 | | _ ⇒ false |
---|
| 587 | ] |
---|
| 588 | | DEC arg ⇒ |
---|
| 589 | match j with |
---|
| 590 | [ DEC arg' ⇒ eq_addressing_mode arg arg' |
---|
| 591 | | _ ⇒ false |
---|
| 592 | ] |
---|
| 593 | | MUL arg1 arg2 ⇒ |
---|
| 594 | match j with |
---|
| 595 | [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 596 | | _ ⇒ false |
---|
| 597 | ] |
---|
| 598 | | DIV arg1 arg2 ⇒ |
---|
| 599 | match j with |
---|
| 600 | [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 601 | | _ ⇒ false |
---|
| 602 | ] |
---|
| 603 | | DA arg ⇒ |
---|
| 604 | match j with |
---|
| 605 | [ DA arg' ⇒ eq_addressing_mode arg arg' |
---|
| 606 | | _ ⇒ false |
---|
| 607 | ] |
---|
| 608 | | JC arg ⇒ |
---|
| 609 | match j with |
---|
| 610 | [ JC arg' ⇒ eq_addressing_mode arg arg' |
---|
| 611 | | _ ⇒ false |
---|
| 612 | ] |
---|
| 613 | | JNC arg ⇒ |
---|
| 614 | match j with |
---|
| 615 | [ JNC arg' ⇒ eq_addressing_mode arg arg' |
---|
| 616 | | _ ⇒ false |
---|
| 617 | ] |
---|
| 618 | | JB arg1 arg2 ⇒ |
---|
| 619 | match j with |
---|
| 620 | [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 621 | | _ ⇒ false |
---|
| 622 | ] |
---|
| 623 | | JNB arg1 arg2 ⇒ |
---|
| 624 | match j with |
---|
| 625 | [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 626 | | _ ⇒ false |
---|
| 627 | ] |
---|
| 628 | | JBC arg1 arg2 ⇒ |
---|
| 629 | match j with |
---|
| 630 | [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 631 | | _ ⇒ false |
---|
| 632 | ] |
---|
| 633 | | JZ arg ⇒ |
---|
| 634 | match j with |
---|
| 635 | [ JZ arg' ⇒ eq_addressing_mode arg arg' |
---|
| 636 | | _ ⇒ false |
---|
| 637 | ] |
---|
| 638 | | JNZ arg ⇒ |
---|
| 639 | match j with |
---|
| 640 | [ JNZ arg' ⇒ eq_addressing_mode arg arg' |
---|
| 641 | | _ ⇒ false |
---|
| 642 | ] |
---|
| 643 | | CJNE arg1 arg2 ⇒ |
---|
| 644 | match j with |
---|
| 645 | [ CJNE arg1' arg2' ⇒ |
---|
| 646 | let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in |
---|
| 647 | let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in |
---|
| 648 | let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in |
---|
| 649 | arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 650 | | _ ⇒ false |
---|
| 651 | ] |
---|
| 652 | | DJNZ arg1 arg2 ⇒ |
---|
| 653 | match j with |
---|
| 654 | [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 655 | | _ ⇒ false |
---|
| 656 | ] |
---|
| 657 | | CLR arg ⇒ |
---|
| 658 | match j with |
---|
| 659 | [ CLR arg' ⇒ eq_addressing_mode arg arg' |
---|
| 660 | | _ ⇒ false |
---|
| 661 | ] |
---|
| 662 | | CPL arg ⇒ |
---|
| 663 | match j with |
---|
| 664 | [ CPL arg' ⇒ eq_addressing_mode arg arg' |
---|
| 665 | | _ ⇒ false |
---|
| 666 | ] |
---|
| 667 | | RL arg ⇒ |
---|
| 668 | match j with |
---|
| 669 | [ RL arg' ⇒ eq_addressing_mode arg arg' |
---|
| 670 | | _ ⇒ false |
---|
| 671 | ] |
---|
| 672 | | RLC arg ⇒ |
---|
| 673 | match j with |
---|
| 674 | [ RLC arg' ⇒ eq_addressing_mode arg arg' |
---|
| 675 | | _ ⇒ false |
---|
| 676 | ] |
---|
| 677 | | RR arg ⇒ |
---|
| 678 | match j with |
---|
| 679 | [ RR arg' ⇒ eq_addressing_mode arg arg' |
---|
| 680 | | _ ⇒ false |
---|
| 681 | ] |
---|
| 682 | | RRC arg ⇒ |
---|
| 683 | match j with |
---|
| 684 | [ RRC arg' ⇒ eq_addressing_mode arg arg' |
---|
| 685 | | _ ⇒ false |
---|
| 686 | ] |
---|
| 687 | | SWAP arg ⇒ |
---|
| 688 | match j with |
---|
| 689 | [ SWAP arg' ⇒ eq_addressing_mode arg arg' |
---|
| 690 | | _ ⇒ false |
---|
| 691 | ] |
---|
| 692 | | SETB arg ⇒ |
---|
| 693 | match j with |
---|
| 694 | [ SETB arg' ⇒ eq_addressing_mode arg arg' |
---|
| 695 | | _ ⇒ false |
---|
| 696 | ] |
---|
| 697 | | PUSH arg ⇒ |
---|
| 698 | match j with |
---|
| 699 | [ PUSH arg' ⇒ eq_addressing_mode arg arg' |
---|
| 700 | | _ ⇒ false |
---|
| 701 | ] |
---|
| 702 | | POP arg ⇒ |
---|
| 703 | match j with |
---|
| 704 | [ POP arg' ⇒ eq_addressing_mode arg arg' |
---|
| 705 | | _ ⇒ false |
---|
| 706 | ] |
---|
| 707 | | XCH arg1 arg2 ⇒ |
---|
| 708 | match j with |
---|
| 709 | [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 710 | | _ ⇒ false |
---|
| 711 | ] |
---|
| 712 | | XCHD arg1 arg2 ⇒ |
---|
| 713 | match j with |
---|
| 714 | [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 715 | | _ ⇒ false |
---|
| 716 | ] |
---|
| 717 | | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ] |
---|
| 718 | | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ] |
---|
| 719 | | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ] |
---|
| 720 | | MOVX arg ⇒ |
---|
| 721 | match j with |
---|
| 722 | [ MOVX arg' ⇒ |
---|
| 723 | let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in |
---|
| 724 | let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in |
---|
| 725 | let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in |
---|
| 726 | sum_eq arg arg' |
---|
| 727 | | _ ⇒ false |
---|
| 728 | ] |
---|
| 729 | | XRL arg ⇒ |
---|
| 730 | match j with |
---|
| 731 | [ XRL arg' ⇒ |
---|
| 732 | let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in |
---|
| 733 | let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in |
---|
| 734 | let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in |
---|
| 735 | sum_eq arg arg' |
---|
| 736 | | _ ⇒ false |
---|
| 737 | ] |
---|
| 738 | | ORL arg ⇒ |
---|
| 739 | match j with |
---|
| 740 | [ ORL arg' ⇒ |
---|
| 741 | let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in |
---|
| 742 | let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in |
---|
| 743 | let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in |
---|
| 744 | let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in |
---|
| 745 | let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in |
---|
| 746 | sum_eq arg arg' |
---|
| 747 | | _ ⇒ false |
---|
| 748 | ] |
---|
| 749 | | ANL arg ⇒ |
---|
| 750 | match j with |
---|
| 751 | [ ANL arg' ⇒ |
---|
| 752 | let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in |
---|
| 753 | let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in |
---|
| 754 | let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in |
---|
| 755 | let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in |
---|
| 756 | let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in |
---|
| 757 | sum_eq arg arg' |
---|
| 758 | | _ ⇒ false |
---|
| 759 | ] |
---|
| 760 | | MOV arg ⇒ |
---|
| 761 | match j with |
---|
| 762 | [ MOV arg' ⇒ |
---|
| 763 | let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in |
---|
| 764 | let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in |
---|
| 765 | let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in |
---|
| 766 | let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in |
---|
| 767 | let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in |
---|
| 768 | let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in |
---|
| 769 | let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in |
---|
| 770 | let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in |
---|
| 771 | let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in |
---|
| 772 | let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in |
---|
| 773 | let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in |
---|
| 774 | sum_eq_5 arg arg' |
---|
| 775 | | _ ⇒ false |
---|
| 776 | ] |
---|
| 777 | ]. |
---|
| 778 | |
---|
| 779 | lemma eq_preinstruction_refl: |
---|
| 780 | ∀i. |
---|
| 781 | eq_preinstruction i i = true. |
---|
| 782 | #i cases i try #arg1 try #arg2 |
---|
| 783 | try @eq_addressing_mode_refl |
---|
| 784 | [1,2,3,4,5,6,7,8,10,16,17,18,19,20: |
---|
| 785 | whd in ⊢ (??%?); try % |
---|
| 786 | >eq_addressing_mode_refl |
---|
| 787 | >eq_addressing_mode_refl % |
---|
| 788 | |13,15: |
---|
| 789 | whd in ⊢ (??%?); |
---|
| 790 | cases arg1 |
---|
| 791 | [*: |
---|
| 792 | #arg1_left normalize nodelta |
---|
| 793 | >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl] |
---|
| 794 | ] |
---|
| 795 | |11,12: |
---|
| 796 | whd in ⊢ (??%?); |
---|
| 797 | cases arg1 |
---|
| 798 | [1: |
---|
| 799 | #arg1_left normalize nodelta |
---|
| 800 | >(eq_sum_refl …) |
---|
| 801 | [1: % | 2,3: #arg @eq_prod_refl ] |
---|
| 802 | @eq_addressing_mode_refl |
---|
| 803 | |2: |
---|
| 804 | #arg1_left normalize nodelta |
---|
| 805 | @eq_prod_refl [*: @eq_addressing_mode_refl ] |
---|
| 806 | |3: |
---|
| 807 | #arg1_left normalize nodelta |
---|
| 808 | >(eq_sum_refl …) |
---|
| 809 | [1: |
---|
| 810 | % |
---|
| 811 | |2,3: |
---|
| 812 | #arg @eq_prod_refl #arg @eq_addressing_mode_refl |
---|
| 813 | ] |
---|
| 814 | |4: |
---|
| 815 | #arg1_left normalize nodelta |
---|
| 816 | @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] |
---|
| 817 | ] |
---|
| 818 | |14: |
---|
| 819 | whd in ⊢ (??%?); |
---|
| 820 | cases arg1 |
---|
| 821 | [1: |
---|
| 822 | #arg1_left normalize nodelta |
---|
| 823 | @eq_sum_refl |
---|
| 824 | [1: |
---|
| 825 | #arg @eq_sum_refl |
---|
| 826 | [1: |
---|
| 827 | #arg @eq_sum_refl |
---|
| 828 | [1: |
---|
| 829 | #arg @eq_sum_refl |
---|
| 830 | [1: |
---|
| 831 | #arg @eq_prod_refl |
---|
| 832 | [*: |
---|
| 833 | @eq_addressing_mode_refl |
---|
| 834 | ] |
---|
| 835 | |2: |
---|
| 836 | #arg @eq_prod_refl |
---|
| 837 | [*: |
---|
| 838 | #arg @eq_addressing_mode_refl |
---|
| 839 | ] |
---|
| 840 | ] |
---|
| 841 | |2: |
---|
| 842 | #arg @eq_prod_refl |
---|
| 843 | [*: |
---|
| 844 | #arg @eq_addressing_mode_refl |
---|
| 845 | ] |
---|
| 846 | ] |
---|
| 847 | |2: |
---|
| 848 | #arg @eq_prod_refl |
---|
| 849 | [*: |
---|
| 850 | #arg @eq_addressing_mode_refl |
---|
| 851 | ] |
---|
| 852 | ] |
---|
| 853 | |2: |
---|
| 854 | #arg @eq_prod_refl |
---|
| 855 | [*: |
---|
| 856 | #arg @eq_addressing_mode_refl |
---|
| 857 | ] |
---|
| 858 | ] |
---|
| 859 | |2: |
---|
| 860 | #arg1_right normalize nodelta |
---|
| 861 | @eq_prod_refl |
---|
| 862 | [*: |
---|
| 863 | #arg @eq_addressing_mode_refl |
---|
| 864 | ] |
---|
| 865 | ] |
---|
| 866 | |*: |
---|
| 867 | whd in ⊢ (??%?); |
---|
| 868 | cases arg1 |
---|
| 869 | [*: |
---|
| 870 | #arg1 >eq_sum_refl |
---|
| 871 | [1,4: |
---|
| 872 | @eq_addressing_mode_refl |
---|
| 873 | |2,3,5,6: |
---|
| 874 | #arg @eq_prod_refl |
---|
| 875 | [*: |
---|
| 876 | #arg @eq_addressing_mode_refl |
---|
| 877 | ] |
---|
| 878 | ] |
---|
| 879 | ] |
---|
| 880 | ] |
---|
| 881 | qed. |
---|
| 882 | |
---|
[820] | 883 | inductive instruction: Type[0] ≝ |
---|
| 884 | | ACALL: [[addr11]] → instruction |
---|
| 885 | | LCALL: [[addr16]] → instruction |
---|
| 886 | | AJMP: [[addr11]] → instruction |
---|
| 887 | | LJMP: [[addr16]] → instruction |
---|
| 888 | | SJMP: [[relative]] → instruction |
---|
| 889 | | JMP: [[indirect_dptr]] → instruction |
---|
| 890 | | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction |
---|
| 891 | | RealInstruction: preinstruction [[ relative ]] → instruction. |
---|
| 892 | |
---|
| 893 | coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝ |
---|
| 894 | RealInstruction on _p: preinstruction ? to instruction. |
---|
[475] | 895 | |
---|
[2124] | 896 | definition eq_instruction: instruction → instruction → bool ≝ |
---|
| 897 | λi, j. |
---|
| 898 | match i with |
---|
| 899 | [ ACALL arg ⇒ |
---|
| 900 | match j with |
---|
| 901 | [ ACALL arg' ⇒ eq_addressing_mode arg arg' |
---|
| 902 | | _ ⇒ false |
---|
| 903 | ] |
---|
| 904 | | LCALL arg ⇒ |
---|
| 905 | match j with |
---|
| 906 | [ LCALL arg' ⇒ eq_addressing_mode arg arg' |
---|
| 907 | | _ ⇒ false |
---|
| 908 | ] |
---|
| 909 | | AJMP arg ⇒ |
---|
| 910 | match j with |
---|
| 911 | [ AJMP arg' ⇒ eq_addressing_mode arg arg' |
---|
| 912 | | _ ⇒ false |
---|
| 913 | ] |
---|
| 914 | | LJMP arg ⇒ |
---|
| 915 | match j with |
---|
| 916 | [ LJMP arg' ⇒ eq_addressing_mode arg arg' |
---|
| 917 | | _ ⇒ false |
---|
| 918 | ] |
---|
| 919 | | SJMP arg ⇒ |
---|
| 920 | match j with |
---|
| 921 | [ SJMP arg' ⇒ eq_addressing_mode arg arg' |
---|
| 922 | | _ ⇒ false |
---|
| 923 | ] |
---|
| 924 | | JMP arg ⇒ |
---|
| 925 | match j with |
---|
| 926 | [ JMP arg' ⇒ eq_addressing_mode arg arg' |
---|
| 927 | | _ ⇒ false |
---|
| 928 | ] |
---|
| 929 | | MOVC arg1 arg2 ⇒ |
---|
| 930 | match j with |
---|
| 931 | [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 932 | | _ ⇒ false |
---|
| 933 | ] |
---|
| 934 | | RealInstruction instr ⇒ |
---|
| 935 | match j with |
---|
| 936 | [ RealInstruction instr' ⇒ eq_preinstruction instr instr' |
---|
| 937 | | _ ⇒ false |
---|
| 938 | ] |
---|
| 939 | ]. |
---|
| 940 | |
---|
| 941 | lemma eq_instruction_refl: |
---|
| 942 | ∀i. eq_instruction i i = true. |
---|
| 943 | #i cases i [*: #arg1 ] |
---|
| 944 | try @eq_addressing_mode_refl |
---|
| 945 | try @eq_preinstruction_refl |
---|
| 946 | #arg2 whd in ⊢ (??%?); |
---|
| 947 | >eq_addressing_mode_refl >eq_addressing_mode_refl % |
---|
| 948 | qed. |
---|
| 949 | |
---|
| 950 | lemma eq_instruction_to_eq: |
---|
| 951 | ∀i1, i2: instruction. |
---|
| 952 | eq_instruction i1 i2 = true → i1 ≃ i2. |
---|
| 953 | #i1 #i2 |
---|
| 954 | cases i1 cases i2 cases daemon (* easy but tedious |
---|
| 955 | [1,10,19,28,37,46: |
---|
| 956 | #arg1 #arg2 |
---|
| 957 | whd in match (eq_instruction ??); |
---|
| 958 | cases arg1 #subaddressing_mode |
---|
| 959 | cases subaddressing_mode |
---|
| 960 | try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I) |
---|
| 961 | try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I) |
---|
| 962 | try (normalize in ⊢ (% → ?); #absurd cases absurd @I) |
---|
| 963 | #word11 #irrelevant |
---|
| 964 | cases arg2 #subaddressing_mode |
---|
| 965 | cases subaddressing_mode |
---|
| 966 | try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I) |
---|
| 967 | try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I) |
---|
| 968 | try (normalize in ⊢ (% → ?); #absurd cases absurd @I) |
---|
| 969 | #word11' #irrelevant normalize nodelta |
---|
| 970 | #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *) |
---|
| 971 | qed. |
---|
| 972 | |
---|
[722] | 973 | inductive pseudo_instruction: Type[0] ≝ |
---|
[820] | 974 | | Instruction: preinstruction Identifier → pseudo_instruction |
---|
| 975 | | Comment: String → pseudo_instruction |
---|
[1515] | 976 | | Cost: costlabel → pseudo_instruction |
---|
[820] | 977 | | Jmp: Identifier → pseudo_instruction |
---|
| 978 | | Call: Identifier → pseudo_instruction |
---|
| 979 | | Mov: [[dptr]] → Identifier → pseudo_instruction. |
---|
[475] | 980 | |
---|
[1882] | 981 | definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction. |
---|
[1522] | 982 | definition preamble ≝ (identifier_map SymbolTag nat) × (list (Identifier × Word)). |
---|
[820] | 983 | definition assembly_program ≝ list instruction. |
---|
| 984 | definition pseudo_assembly_program ≝ preamble × (list labelled_instruction). |
---|
[2123] | 985 | |
---|
| 986 | (* labels & instructions *) |
---|
| 987 | definition instruction_has_label ≝ |
---|
| 988 | λid: Identifier. |
---|
| 989 | λi. |
---|
| 990 | match i with |
---|
| 991 | [ Jmp j ⇒ j = id |
---|
| 992 | | Call j ⇒ j = id |
---|
| 993 | | Instruction instr ⇒ |
---|
| 994 | match instr with |
---|
| 995 | [ JC j ⇒ j = id |
---|
| 996 | | JNC j ⇒ j = id |
---|
| 997 | | JZ j ⇒ j = id |
---|
| 998 | | JNZ j ⇒ j = id |
---|
| 999 | | JB _ j ⇒ j = id |
---|
[2139] | 1000 | | JNB _ j ⇒ j = id |
---|
[2123] | 1001 | | JBC _ j ⇒ j = id |
---|
| 1002 | | DJNZ _ j ⇒ j = id |
---|
| 1003 | | CJNE _ j ⇒ j = id |
---|
| 1004 | | _ ⇒ False |
---|
| 1005 | ] |
---|
| 1006 | | _ ⇒ False |
---|
[2128] | 1007 | ]. |
---|
[2316] | 1008 | |
---|
| 1009 | |
---|
| 1010 | (* If instruction i is a jump, then there will be something in the policy at |
---|
| 1011 | * position i *) |
---|
| 1012 | definition is_jump' ≝ |
---|
| 1013 | λx:preinstruction Identifier. |
---|
| 1014 | match x with |
---|
| 1015 | [ JC _ ⇒ true |
---|
| 1016 | | JNC _ ⇒ true |
---|
| 1017 | | JZ _ ⇒ true |
---|
| 1018 | | JNZ _ ⇒ true |
---|
| 1019 | | JB _ _ ⇒ true |
---|
| 1020 | | JNB _ _ ⇒ true |
---|
| 1021 | | JBC _ _ ⇒ true |
---|
| 1022 | | CJNE _ _ ⇒ true |
---|
| 1023 | | DJNZ _ _ ⇒ true |
---|
| 1024 | | _ ⇒ false |
---|
| 1025 | ]. |
---|
| 1026 | |
---|
| 1027 | definition is_relative_jump ≝ |
---|
| 1028 | λinstr:pseudo_instruction. |
---|
| 1029 | match instr with |
---|
| 1030 | [ Instruction i ⇒ is_jump' i |
---|
| 1031 | | _ ⇒ false |
---|
| 1032 | ]. |
---|
| 1033 | |
---|
| 1034 | definition is_jump ≝ |
---|
| 1035 | λinstr:pseudo_instruction. |
---|
| 1036 | match instr with |
---|
| 1037 | [ Instruction i ⇒ is_jump' i |
---|
| 1038 | | Call _ ⇒ true |
---|
| 1039 | | Jmp _ ⇒ true |
---|
| 1040 | | _ ⇒ false |
---|
| 1041 | ]. |
---|
| 1042 | |
---|
| 1043 | definition is_call ≝ |
---|
| 1044 | λinstr:pseudo_instruction. |
---|
| 1045 | match instr with |
---|
| 1046 | [ Call _ ⇒ true |
---|
| 1047 | | _ ⇒ false |
---|
| 1048 | ]. |
---|
| 1049 | |
---|
| 1050 | definition is_jump_to ≝ |
---|
| 1051 | λx:pseudo_instruction.λd:Identifier. |
---|
| 1052 | match x with |
---|
| 1053 | [ Instruction i ⇒ match i with |
---|
| 1054 | [ JC j ⇒ d = j |
---|
| 1055 | | JNC j ⇒ d = j |
---|
| 1056 | | JZ j ⇒ d = j |
---|
| 1057 | | JNZ j ⇒ d = j |
---|
| 1058 | | JB _ j ⇒ d = j |
---|
| 1059 | | JNB _ j ⇒ d = j |
---|
| 1060 | | JBC _ j ⇒ d = j |
---|
| 1061 | | CJNE _ j ⇒ d = j |
---|
| 1062 | | DJNZ _ j ⇒ d = j |
---|
| 1063 | | _ ⇒ False |
---|
| 1064 | ] |
---|
| 1065 | | Call c ⇒ d = c |
---|
| 1066 | | Jmp j ⇒ d = j |
---|
| 1067 | | _ ⇒ False |
---|
[2645] | 1068 | ]. |
---|