[1515] | 1 | include "common/CostLabel.ma". |
---|
[1882] | 2 | include "common/LabelledObjects.ma". |
---|
[2767] | 3 | include "common/AST.ma". |
---|
[2647] | 4 | include "joint/String.ma". |
---|
[2767] | 5 | include "ASM/BitVectorTrie.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 |
---|
[2705] | 563 | | NOP: preinstruction A |
---|
[3039] | 564 | | JMP: [[acc_dptr]] → preinstruction A. |
---|
[475] | 565 | |
---|
[2124] | 566 | definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝ |
---|
| 567 | λi, j. |
---|
| 568 | match i with |
---|
| 569 | [ ADD arg1 arg2 ⇒ |
---|
| 570 | match j with |
---|
| 571 | [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 572 | | _ ⇒ false |
---|
| 573 | ] |
---|
| 574 | | ADDC arg1 arg2 ⇒ |
---|
| 575 | match j with |
---|
| 576 | [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 577 | | _ ⇒ false |
---|
| 578 | ] |
---|
| 579 | | SUBB arg1 arg2 ⇒ |
---|
| 580 | match j with |
---|
| 581 | [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 582 | | _ ⇒ false |
---|
| 583 | ] |
---|
| 584 | | INC arg ⇒ |
---|
| 585 | match j with |
---|
| 586 | [ INC arg' ⇒ eq_addressing_mode arg arg' |
---|
| 587 | | _ ⇒ false |
---|
| 588 | ] |
---|
| 589 | | DEC arg ⇒ |
---|
| 590 | match j with |
---|
| 591 | [ DEC arg' ⇒ eq_addressing_mode arg arg' |
---|
| 592 | | _ ⇒ false |
---|
| 593 | ] |
---|
| 594 | | MUL arg1 arg2 ⇒ |
---|
| 595 | match j with |
---|
| 596 | [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 597 | | _ ⇒ false |
---|
| 598 | ] |
---|
| 599 | | DIV arg1 arg2 ⇒ |
---|
| 600 | match j with |
---|
| 601 | [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 602 | | _ ⇒ false |
---|
| 603 | ] |
---|
| 604 | | DA arg ⇒ |
---|
| 605 | match j with |
---|
| 606 | [ DA arg' ⇒ eq_addressing_mode arg arg' |
---|
| 607 | | _ ⇒ false |
---|
| 608 | ] |
---|
| 609 | | JC arg ⇒ |
---|
| 610 | match j with |
---|
| 611 | [ JC arg' ⇒ eq_addressing_mode arg arg' |
---|
| 612 | | _ ⇒ false |
---|
| 613 | ] |
---|
| 614 | | JNC arg ⇒ |
---|
| 615 | match j with |
---|
| 616 | [ JNC arg' ⇒ eq_addressing_mode arg arg' |
---|
| 617 | | _ ⇒ false |
---|
| 618 | ] |
---|
| 619 | | JB arg1 arg2 ⇒ |
---|
| 620 | match j with |
---|
| 621 | [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 622 | | _ ⇒ false |
---|
| 623 | ] |
---|
| 624 | | JNB arg1 arg2 ⇒ |
---|
| 625 | match j with |
---|
| 626 | [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 627 | | _ ⇒ false |
---|
| 628 | ] |
---|
| 629 | | JBC arg1 arg2 ⇒ |
---|
| 630 | match j with |
---|
| 631 | [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 632 | | _ ⇒ false |
---|
| 633 | ] |
---|
| 634 | | JZ arg ⇒ |
---|
| 635 | match j with |
---|
| 636 | [ JZ arg' ⇒ eq_addressing_mode arg arg' |
---|
| 637 | | _ ⇒ false |
---|
| 638 | ] |
---|
| 639 | | JNZ arg ⇒ |
---|
| 640 | match j with |
---|
| 641 | [ JNZ arg' ⇒ eq_addressing_mode arg arg' |
---|
| 642 | | _ ⇒ false |
---|
| 643 | ] |
---|
[2704] | 644 | | JMP arg ⇒ |
---|
| 645 | match j with |
---|
| 646 | [ JMP arg' ⇒ eq_addressing_mode arg arg' |
---|
| 647 | | _ ⇒ false |
---|
| 648 | ] |
---|
[2124] | 649 | | CJNE arg1 arg2 ⇒ |
---|
| 650 | match j with |
---|
| 651 | [ CJNE arg1' arg2' ⇒ |
---|
| 652 | let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in |
---|
| 653 | let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in |
---|
| 654 | let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in |
---|
| 655 | arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 656 | | _ ⇒ false |
---|
| 657 | ] |
---|
| 658 | | DJNZ arg1 arg2 ⇒ |
---|
| 659 | match j with |
---|
| 660 | [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 661 | | _ ⇒ false |
---|
| 662 | ] |
---|
| 663 | | CLR arg ⇒ |
---|
| 664 | match j with |
---|
| 665 | [ CLR arg' ⇒ eq_addressing_mode arg arg' |
---|
| 666 | | _ ⇒ false |
---|
| 667 | ] |
---|
| 668 | | CPL arg ⇒ |
---|
| 669 | match j with |
---|
| 670 | [ CPL arg' ⇒ eq_addressing_mode arg arg' |
---|
| 671 | | _ ⇒ false |
---|
| 672 | ] |
---|
| 673 | | RL arg ⇒ |
---|
| 674 | match j with |
---|
| 675 | [ RL arg' ⇒ eq_addressing_mode arg arg' |
---|
| 676 | | _ ⇒ false |
---|
| 677 | ] |
---|
| 678 | | RLC arg ⇒ |
---|
| 679 | match j with |
---|
| 680 | [ RLC arg' ⇒ eq_addressing_mode arg arg' |
---|
| 681 | | _ ⇒ false |
---|
| 682 | ] |
---|
| 683 | | RR arg ⇒ |
---|
| 684 | match j with |
---|
| 685 | [ RR arg' ⇒ eq_addressing_mode arg arg' |
---|
| 686 | | _ ⇒ false |
---|
| 687 | ] |
---|
| 688 | | RRC arg ⇒ |
---|
| 689 | match j with |
---|
| 690 | [ RRC arg' ⇒ eq_addressing_mode arg arg' |
---|
| 691 | | _ ⇒ false |
---|
| 692 | ] |
---|
| 693 | | SWAP arg ⇒ |
---|
| 694 | match j with |
---|
| 695 | [ SWAP arg' ⇒ eq_addressing_mode arg arg' |
---|
| 696 | | _ ⇒ false |
---|
| 697 | ] |
---|
| 698 | | SETB arg ⇒ |
---|
| 699 | match j with |
---|
| 700 | [ SETB arg' ⇒ eq_addressing_mode arg arg' |
---|
| 701 | | _ ⇒ false |
---|
| 702 | ] |
---|
| 703 | | PUSH arg ⇒ |
---|
| 704 | match j with |
---|
| 705 | [ PUSH arg' ⇒ eq_addressing_mode arg arg' |
---|
| 706 | | _ ⇒ false |
---|
| 707 | ] |
---|
| 708 | | POP arg ⇒ |
---|
| 709 | match j with |
---|
| 710 | [ POP arg' ⇒ eq_addressing_mode arg arg' |
---|
| 711 | | _ ⇒ false |
---|
| 712 | ] |
---|
| 713 | | XCH arg1 arg2 ⇒ |
---|
| 714 | match j with |
---|
| 715 | [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 716 | | _ ⇒ false |
---|
| 717 | ] |
---|
| 718 | | XCHD arg1 arg2 ⇒ |
---|
| 719 | match j with |
---|
| 720 | [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' |
---|
| 721 | | _ ⇒ false |
---|
| 722 | ] |
---|
| 723 | | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ] |
---|
| 724 | | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ] |
---|
| 725 | | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ] |
---|
| 726 | | MOVX arg ⇒ |
---|
| 727 | match j with |
---|
| 728 | [ MOVX arg' ⇒ |
---|
| 729 | let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in |
---|
| 730 | let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in |
---|
| 731 | let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in |
---|
| 732 | sum_eq arg arg' |
---|
| 733 | | _ ⇒ false |
---|
| 734 | ] |
---|
| 735 | | XRL arg ⇒ |
---|
| 736 | match j with |
---|
| 737 | [ XRL arg' ⇒ |
---|
| 738 | let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in |
---|
| 739 | let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in |
---|
| 740 | let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in |
---|
| 741 | sum_eq arg arg' |
---|
| 742 | | _ ⇒ false |
---|
| 743 | ] |
---|
| 744 | | ORL arg ⇒ |
---|
| 745 | match j with |
---|
| 746 | [ ORL arg' ⇒ |
---|
| 747 | let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in |
---|
| 748 | let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in |
---|
| 749 | let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in |
---|
| 750 | let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in |
---|
| 751 | let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in |
---|
| 752 | sum_eq arg arg' |
---|
| 753 | | _ ⇒ false |
---|
| 754 | ] |
---|
| 755 | | ANL arg ⇒ |
---|
| 756 | match j with |
---|
| 757 | [ ANL arg' ⇒ |
---|
| 758 | let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in |
---|
| 759 | let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in |
---|
| 760 | let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in |
---|
| 761 | let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in |
---|
| 762 | let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in |
---|
| 763 | sum_eq arg arg' |
---|
| 764 | | _ ⇒ false |
---|
| 765 | ] |
---|
| 766 | | MOV arg ⇒ |
---|
| 767 | match j with |
---|
| 768 | [ MOV arg' ⇒ |
---|
| 769 | let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in |
---|
| 770 | let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in |
---|
| 771 | let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in |
---|
| 772 | let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in |
---|
| 773 | let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in |
---|
| 774 | let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in |
---|
| 775 | let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in |
---|
| 776 | let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in |
---|
| 777 | let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in |
---|
| 778 | let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in |
---|
| 779 | let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in |
---|
| 780 | sum_eq_5 arg arg' |
---|
| 781 | | _ ⇒ false |
---|
| 782 | ] |
---|
| 783 | ]. |
---|
| 784 | |
---|
| 785 | lemma eq_preinstruction_refl: |
---|
| 786 | ∀i. |
---|
| 787 | eq_preinstruction i i = true. |
---|
| 788 | #i cases i try #arg1 try #arg2 |
---|
| 789 | try @eq_addressing_mode_refl |
---|
| 790 | [1,2,3,4,5,6,7,8,10,16,17,18,19,20: |
---|
| 791 | whd in ⊢ (??%?); try % |
---|
| 792 | >eq_addressing_mode_refl |
---|
| 793 | >eq_addressing_mode_refl % |
---|
| 794 | |13,15: |
---|
| 795 | whd in ⊢ (??%?); |
---|
| 796 | cases arg1 |
---|
| 797 | [*: |
---|
| 798 | #arg1_left normalize nodelta |
---|
| 799 | >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl] |
---|
| 800 | ] |
---|
| 801 | |11,12: |
---|
| 802 | whd in ⊢ (??%?); |
---|
| 803 | cases arg1 |
---|
| 804 | [1: |
---|
| 805 | #arg1_left normalize nodelta |
---|
| 806 | >(eq_sum_refl …) |
---|
| 807 | [1: % | 2,3: #arg @eq_prod_refl ] |
---|
| 808 | @eq_addressing_mode_refl |
---|
| 809 | |2: |
---|
| 810 | #arg1_left normalize nodelta |
---|
| 811 | @eq_prod_refl [*: @eq_addressing_mode_refl ] |
---|
| 812 | |3: |
---|
| 813 | #arg1_left normalize nodelta |
---|
| 814 | >(eq_sum_refl …) |
---|
| 815 | [1: |
---|
| 816 | % |
---|
| 817 | |2,3: |
---|
| 818 | #arg @eq_prod_refl #arg @eq_addressing_mode_refl |
---|
| 819 | ] |
---|
| 820 | |4: |
---|
| 821 | #arg1_left normalize nodelta |
---|
| 822 | @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] |
---|
| 823 | ] |
---|
| 824 | |14: |
---|
| 825 | whd in ⊢ (??%?); |
---|
| 826 | cases arg1 |
---|
| 827 | [1: |
---|
| 828 | #arg1_left normalize nodelta |
---|
| 829 | @eq_sum_refl |
---|
| 830 | [1: |
---|
| 831 | #arg @eq_sum_refl |
---|
| 832 | [1: |
---|
| 833 | #arg @eq_sum_refl |
---|
| 834 | [1: |
---|
| 835 | #arg @eq_sum_refl |
---|
| 836 | [1: |
---|
| 837 | #arg @eq_prod_refl |
---|
| 838 | [*: |
---|
| 839 | @eq_addressing_mode_refl |
---|
| 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 | #arg @eq_prod_refl |
---|
| 861 | [*: |
---|
| 862 | #arg @eq_addressing_mode_refl |
---|
| 863 | ] |
---|
| 864 | ] |
---|
| 865 | |2: |
---|
| 866 | #arg1_right normalize nodelta |
---|
| 867 | @eq_prod_refl |
---|
| 868 | [*: |
---|
| 869 | #arg @eq_addressing_mode_refl |
---|
| 870 | ] |
---|
| 871 | ] |
---|
| 872 | |*: |
---|
| 873 | whd in ⊢ (??%?); |
---|
| 874 | cases arg1 |
---|
| 875 | [*: |
---|
| 876 | #arg1 >eq_sum_refl |
---|
| 877 | [1,4: |
---|
| 878 | @eq_addressing_mode_refl |
---|
| 879 | |2,3,5,6: |
---|
| 880 | #arg @eq_prod_refl |
---|
| 881 | [*: |
---|
| 882 | #arg @eq_addressing_mode_refl |
---|
| 883 | ] |
---|
| 884 | ] |
---|
| 885 | ] |
---|
| 886 | ] |
---|
| 887 | qed. |
---|
| 888 | |
---|
[820] | 889 | inductive instruction: Type[0] ≝ |
---|
| 890 | | ACALL: [[addr11]] → instruction |
---|
| 891 | | LCALL: [[addr16]] → instruction |
---|
| 892 | | AJMP: [[addr11]] → instruction |
---|
| 893 | | LJMP: [[addr16]] → instruction |
---|
| 894 | | SJMP: [[relative]] → instruction |
---|
| 895 | | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction |
---|
| 896 | | RealInstruction: preinstruction [[ relative ]] → instruction. |
---|
| 897 | |
---|
| 898 | coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝ |
---|
| 899 | RealInstruction on _p: preinstruction ? to instruction. |
---|
[475] | 900 | |
---|
[2124] | 901 | definition eq_instruction: instruction → instruction → bool ≝ |
---|
| 902 | λi, j. |
---|
| 903 | match i with |
---|
| 904 | [ ACALL arg ⇒ |
---|
| 905 | match j with |
---|
| 906 | [ ACALL arg' ⇒ eq_addressing_mode arg arg' |
---|
| 907 | | _ ⇒ false |
---|
| 908 | ] |
---|
| 909 | | LCALL arg ⇒ |
---|
| 910 | match j with |
---|
| 911 | [ LCALL arg' ⇒ eq_addressing_mode arg arg' |
---|
| 912 | | _ ⇒ false |
---|
| 913 | ] |
---|
| 914 | | AJMP arg ⇒ |
---|
| 915 | match j with |
---|
| 916 | [ AJMP arg' ⇒ eq_addressing_mode arg arg' |
---|
| 917 | | _ ⇒ false |
---|
| 918 | ] |
---|
| 919 | | LJMP arg ⇒ |
---|
| 920 | match j with |
---|
| 921 | [ LJMP arg' ⇒ eq_addressing_mode arg arg' |
---|
| 922 | | _ ⇒ false |
---|
| 923 | ] |
---|
| 924 | | SJMP arg ⇒ |
---|
| 925 | match j with |
---|
| 926 | [ SJMP 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 | |
---|
[2704] | 973 | inductive word_side : Type[0] ≝ HIGH : word_side | LOW : word_side. |
---|
| 974 | |
---|
[722] | 975 | inductive pseudo_instruction: Type[0] ≝ |
---|
[820] | 976 | | Instruction: preinstruction Identifier → pseudo_instruction |
---|
| 977 | | Comment: String → pseudo_instruction |
---|
[1515] | 978 | | Cost: costlabel → pseudo_instruction |
---|
[820] | 979 | | Jmp: Identifier → pseudo_instruction |
---|
[2705] | 980 | | Jnz : [[acc_a]] → Identifier → Identifier → pseudo_instruction |
---|
[820] | 981 | | Call: Identifier → pseudo_instruction |
---|
[3039] | 982 | | Mov: ([[dptr]] ⊎ ([[ acc_a ; direct ; registr ]] × word_side)) → |
---|
| 983 | Identifier → Word → pseudo_instruction. |
---|
[475] | 984 | |
---|
[1882] | 985 | definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction. |
---|
[2757] | 986 | |
---|
[820] | 987 | definition assembly_program ≝ list instruction. |
---|
[2123] | 988 | |
---|
[2757] | 989 | definition fetch_pseudo_instruction: |
---|
| 990 | ∀code_mem:list labelled_instruction. ∀pc:Word. |
---|
| 991 | nat_of_bitvector … pc < |code_mem| → (pseudo_instruction × Word) ≝ |
---|
| 992 | λcode_mem. |
---|
| 993 | λpc: Word. |
---|
| 994 | λpc_ok. |
---|
| 995 | let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? pc) … code_mem pc_ok in |
---|
| 996 | let new_pc ≝ add ? pc (bitvector_of_nat … 1) in |
---|
| 997 | 〈instr, new_pc〉. |
---|
[2754] | 998 | |
---|
[2757] | 999 | lemma snd_fetch_pseudo_instruction: |
---|
| 1000 | ∀l,ppc,ppc_ok. \snd (fetch_pseudo_instruction l ppc ppc_ok) = add ? ppc (bitvector_of_nat ? 1). |
---|
| 1001 | #l #ppc #ppc_ok whd in ⊢ (??(???%)?); @pair_elim |
---|
| 1002 | #lft #rgt #_ % |
---|
| 1003 | qed. |
---|
| 1004 | |
---|
| 1005 | lemma fetch_pseudo_instruction_vsplit: |
---|
| 1006 | ∀instr_list,ppc,ppc_ok. |
---|
| 1007 | ∃pre,suff,lbl. |
---|
| 1008 | (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list. |
---|
| 1009 | #instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???); |
---|
| 1010 | cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff} |
---|
| 1011 | lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta |
---|
| 1012 | #EQ %{lbl0} @EQ |
---|
| 1013 | qed. |
---|
| 1014 | |
---|
| 1015 | lemma fetch_pseudo_instruction_append: |
---|
| 1016 | ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'. |
---|
| 1017 | let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in |
---|
| 1018 | fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' = |
---|
| 1019 | 〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉. |
---|
| 1020 | #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta |
---|
| 1021 | cut (|l1| + nat_of_bitvector … ppc < 2^16) |
---|
| 1022 | [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ] |
---|
| 1023 | -l1l2_ok #l1ppc_ok >nat_of_bitvector_add |
---|
| 1024 | >nat_of_bitvector_bitvector_of_nat_inverse try assumption |
---|
| 1025 | [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ] |
---|
| 1026 | #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???) |
---|
| 1027 | #lbl #instr normalize nodelta >add_associative % |
---|
| 1028 | qed. |
---|
| 1029 | |
---|
[2123] | 1030 | (* labels & instructions *) |
---|
| 1031 | definition instruction_has_label ≝ |
---|
| 1032 | λid: Identifier. |
---|
| 1033 | λi. |
---|
| 1034 | match i with |
---|
| 1035 | [ Jmp j ⇒ j = id |
---|
| 1036 | | Call j ⇒ j = id |
---|
| 1037 | | Instruction instr ⇒ |
---|
| 1038 | match instr with |
---|
| 1039 | [ JC j ⇒ j = id |
---|
| 1040 | | JNC j ⇒ j = id |
---|
| 1041 | | JZ j ⇒ j = id |
---|
| 1042 | | JNZ j ⇒ j = id |
---|
| 1043 | | JB _ j ⇒ j = id |
---|
[2139] | 1044 | | JNB _ j ⇒ j = id |
---|
[2123] | 1045 | | JBC _ j ⇒ j = id |
---|
| 1046 | | DJNZ _ j ⇒ j = id |
---|
| 1047 | | CJNE _ j ⇒ j = id |
---|
| 1048 | | _ ⇒ False |
---|
| 1049 | ] |
---|
| 1050 | | _ ⇒ False |
---|
[2128] | 1051 | ]. |
---|
[2316] | 1052 | |
---|
[2767] | 1053 | (* If instruction i is a jump, then there will be something in the policy at |
---|
| 1054 | * position i *) |
---|
| 1055 | definition is_jump' ≝ |
---|
| 1056 | λx:preinstruction Identifier. |
---|
| 1057 | match x with |
---|
| 1058 | [ JC _ ⇒ true |
---|
| 1059 | | JNC _ ⇒ true |
---|
| 1060 | | JZ _ ⇒ true |
---|
| 1061 | | JNZ _ ⇒ true |
---|
| 1062 | | JB _ _ ⇒ true |
---|
| 1063 | | JNB _ _ ⇒ true |
---|
| 1064 | | JBC _ _ ⇒ true |
---|
| 1065 | | CJNE _ _ ⇒ true |
---|
| 1066 | | DJNZ _ _ ⇒ true |
---|
| 1067 | | _ ⇒ false |
---|
| 1068 | ]. |
---|
| 1069 | |
---|
| 1070 | definition is_relative_jump ≝ |
---|
| 1071 | λinstr:pseudo_instruction. |
---|
| 1072 | match instr with |
---|
| 1073 | [ Instruction i ⇒ is_jump' i |
---|
| 1074 | | _ ⇒ false |
---|
| 1075 | ]. |
---|
| 1076 | |
---|
| 1077 | definition is_jump ≝ |
---|
| 1078 | λinstr:pseudo_instruction. |
---|
| 1079 | match instr with |
---|
| 1080 | [ Instruction i ⇒ is_jump' i |
---|
| 1081 | | Call _ ⇒ true |
---|
| 1082 | | Jmp _ ⇒ true |
---|
| 1083 | | _ ⇒ false |
---|
| 1084 | ]. |
---|
| 1085 | |
---|
| 1086 | definition is_call ≝ |
---|
| 1087 | λinstr:pseudo_instruction. |
---|
| 1088 | match instr with |
---|
| 1089 | [ Call _ ⇒ true |
---|
| 1090 | | _ ⇒ false |
---|
| 1091 | ]. |
---|
| 1092 | |
---|
[2757] | 1093 | definition is_jump_to ≝ |
---|
| 1094 | λx:pseudo_instruction.λd:Identifier. |
---|
| 1095 | match x with |
---|
| 1096 | [ Instruction i ⇒ match i with |
---|
| 1097 | [ JC j ⇒ d = j |
---|
| 1098 | | JNC j ⇒ d = j |
---|
| 1099 | | JZ j ⇒ d = j |
---|
| 1100 | | JNZ j ⇒ d = j |
---|
| 1101 | | JB _ j ⇒ d = j |
---|
| 1102 | | JNB _ j ⇒ d = j |
---|
| 1103 | | JBC _ j ⇒ d = j |
---|
| 1104 | | CJNE _ j ⇒ d = j |
---|
| 1105 | | DJNZ _ j ⇒ d = j |
---|
| 1106 | | _ ⇒ False |
---|
| 1107 | ] |
---|
| 1108 | | Call c ⇒ d = c |
---|
| 1109 | | Jmp j ⇒ d = j |
---|
| 1110 | | _ ⇒ False |
---|
| 1111 | ]. |
---|
[2316] | 1112 | |
---|
[2757] | 1113 | definition is_well_labelled_p ≝ |
---|
| 1114 | λinstr_list. |
---|
| 1115 | ∀id: Identifier. |
---|
| 1116 | ∀ppc. |
---|
| 1117 | ∀ppc_ok. |
---|
| 1118 | ∀i. |
---|
| 1119 | \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) = i → |
---|
| 1120 | (instruction_has_label id i → |
---|
| 1121 | occurs_exactly_once ASMTag pseudo_instruction id instr_list) ∧ |
---|
| 1122 | (is_jump_to i id → |
---|
| 1123 | occurs_exactly_once ASMTag pseudo_instruction id instr_list). |
---|
| 1124 | |
---|
| 1125 | definition asm_cost_label : ∀mem : list labelled_instruction. |
---|
| 1126 | (Σw : Word.nat_of_bitvector … w < |mem|) → option costlabel ≝ |
---|
| 1127 | λmem,w_prf. |
---|
| 1128 | match \fst (fetch_pseudo_instruction mem w_prf (pi2 ?? w_prf)) with |
---|
| 1129 | [ Cost c ⇒ Some ? c |
---|
| 1130 | | _ ⇒ None ? |
---|
| 1131 | ]. |
---|
| 1132 | |
---|
[2767] | 1133 | (* XXX JHM: avoid magic numbers! *) |
---|
| 1134 | definition ADDRESS_WIDTH ≝ 16. |
---|
| 1135 | definition MAX_CODE_SIZE ≝ 2^ADDRESS_WIDTH. |
---|
| 1136 | |
---|
| 1137 | definition code_size_p : list labelled_instruction → Prop ≝ |
---|
| 1138 | λcode. S (|code|) < MAX_CODE_SIZE. |
---|
| 1139 | |
---|
| 1140 | definition code_size_opt : ∀code. option (code_size_p code) ≝ |
---|
| 1141 | λcode. nat_bound_opt MAX_CODE_SIZE (S (|code|)). |
---|
| 1142 | |
---|
[3082] | 1143 | (* The first associative list assigns symbol names to addresses in data memory. |
---|
| 1144 | The second associative list assigns to Identifiers meant to be entry points |
---|
| 1145 | of functions the name of the function (that lives in a different namespace) *) |
---|
| 1146 | |
---|
[2757] | 1147 | record pseudo_assembly_program : Type[0] ≝ |
---|
| 1148 | { preamble : list (Identifier × Word) |
---|
| 1149 | ; code : list labelled_instruction |
---|
[2767] | 1150 | ; code_size_ok: code_size_p code |
---|
[2757] | 1151 | ; renamed_symbols : list (Identifier × ident) |
---|
[2760] | 1152 | ; final_label : Identifier |
---|
[2757] | 1153 | (* properties *) |
---|
| 1154 | ; asm_injective_costlabels : |
---|
| 1155 | partial_injection … (asm_cost_label code) |
---|
| 1156 | ; well_labelled_p : is_well_labelled_p code |
---|
| 1157 | }. |
---|
| 1158 | |
---|
[2999] | 1159 | definition object_code ≝ list Byte. |
---|
| 1160 | |
---|
| 1161 | include alias "ASM/BitVectorTrie.ma". |
---|
| 1162 | include alias "ASM/Arithmetic.ma". |
---|
| 1163 | |
---|
| 1164 | definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝ |
---|
| 1165 | λpmem: BitVectorTrie Byte 16. |
---|
| 1166 | λpc: Word. |
---|
| 1167 | 〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉. |
---|
| 1168 | |
---|
| 1169 | definition load_code_memory0: |
---|
| 1170 | ∀program: object_code. Σres: BitVectorTrie Byte 16. |
---|
| 1171 | let program_size ≝ |program| in |
---|
| 1172 | program_size ≤ 2^16 → |
---|
| 1173 | ∀pc. ∀pc_ok: pc < program_size. |
---|
| 1174 | nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc)) |
---|
| 1175 | ≝ |
---|
| 1176 | λprogram. \snd |
---|
| 1177 | (foldl_strong ? |
---|
| 1178 | (λprefix. |
---|
[3104] | 1179 | Σres: nat × Word × (BitVectorTrie Byte 16). |
---|
| 1180 | let 〈i,bvi,mem〉 ≝ res in |
---|
| 1181 | i = |prefix| ∧ bvi = bitvector_of_nat … i ∧ |
---|
[2999] | 1182 | (i ≤ 2^16 → |
---|
| 1183 | ∀pc. ∀pc_ok: pc < |prefix|. |
---|
| 1184 | nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc)))) |
---|
| 1185 | program |
---|
| 1186 | (λprefix,v,tl,prf,i_mem. |
---|
[3104] | 1187 | let 〈i,bvi,mem〉 ≝ i_mem in |
---|
| 1188 | 〈S i,increment … bvi,insert … bvi v mem〉) |
---|
| 1189 | 〈0,zero ?,Stub Byte 16〉). |
---|
| 1190 | [3: cases (foldl_strong ? (λprefix.Σres.?) ???) ** #i #bvi #mem ** #H1 #H3 >H1 #H2 @H2 |
---|
| 1191 | | % // % // (*#_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))*) |
---|
| 1192 | | cases i_mem in p; ** #i' #bvi' #mem' normalize nodelta #H #EQ destruct(EQ) |
---|
| 1193 | cases H -H * #H1 #H3 #H2 destruct (p1) % |
---|
| 1194 | [ % [ >length_append >H1 normalize // |
---|
| 1195 | | >increment_zero_bitvector_of_nat_1 >H3 <add_bitvector_of_nat % ] |
---|
[2999] | 1196 | | #LE #pc #pc_ok |
---|
| 1197 | cases (le_to_or_lt_eq … pc_ok) |
---|
| 1198 | [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok; |
---|
| 1199 | [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //] |
---|
| 1200 | #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?); |
---|
| 1201 | <H1 <plus_n_O whd in ⊢ (???%); // |
---|
[3104] | 1202 | | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix |
---|
| 1203 | [2: /2 by lt_plus_to_lt_l/] |
---|
[2999] | 1204 | >H2 [2: @(transitive_le … LE) //] |
---|
| 1205 | cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ |
---|
[3104] | 1206 | whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false % >H3 |
---|
[2999] | 1207 | #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption |
---|
| 1208 | @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]] |
---|
| 1209 | qed. |
---|
| 1210 | |
---|
| 1211 | definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝ |
---|
| 1212 | λprogram.load_code_memory0 program. |
---|
| 1213 | |
---|
| 1214 | lemma load_code_memory_ok: |
---|
| 1215 | ∀program: object_code. |
---|
| 1216 | let program_size ≝ |program| in |
---|
| 1217 | program_size ≤ 2^16 → |
---|
| 1218 | ∀pc. ∀pc_ok: pc < program_size. |
---|
| 1219 | nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)). |
---|
| 1220 | whd in match load_code_memory; normalize nodelta #program @pi2 |
---|
| 1221 | qed. |
---|
| 1222 | |
---|
| 1223 | |
---|
[2767] | 1224 | definition costlabel_map ≝ BitVectorTrie costlabel 16. (* XXX *) |
---|
| 1225 | definition symboltable_type ≝ BitVectorTrie ident 16. (* XXX *) |
---|
[2757] | 1226 | record labelled_object_code : Type[0] ≝ |
---|
[2760] | 1227 | { oc : object_code |
---|
[2999] | 1228 | ; cm: BitVectorTrie Byte 16 |
---|
| 1229 | ; cm_def: cm = load_code_memory oc |
---|
[2757] | 1230 | ; costlabels : costlabel_map |
---|
| 1231 | ; symboltable : symboltable_type |
---|
| 1232 | ; final_pc : Word |
---|
| 1233 | (* properties *) |
---|
| 1234 | ; oc_injective_costlabels : |
---|
| 1235 | partial_injection … (λpc.lookup_opt … pc costlabels) |
---|
[3112] | 1236 | ; oc_costlabels_are_zero : (* this will imply that cost labels are only assigned to nops *) |
---|
| 1237 | ∀ppc,l.lookup_opt … ppc costlabels = Some ? l → |
---|
| 1238 | lookup … ppc cm (zero …) = zero … |
---|
[2999] | 1239 | }. |
---|