[475] | 1 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 2 | (* Interpret.ma: Operational semantics for the 8051/8052 processor. *) |
---|
| 3 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 4 | |
---|
[698] | 5 | include "ASM/ASM.ma". |
---|
| 6 | include "ASM/Arithmetic.ma". |
---|
| 7 | include "ASM/BitVectorTrie.ma". |
---|
[1600] | 8 | include "basics/russell.ma". |
---|
[475] | 9 | |
---|
| 10 | definition Time ≝ nat. |
---|
| 11 | |
---|
| 12 | inductive SerialBufferType: Type[0] ≝ |
---|
| 13 | Eight: Byte → SerialBufferType |
---|
| 14 | | Nine: Bit → Byte → SerialBufferType. |
---|
| 15 | |
---|
| 16 | inductive LineType: Type[0] ≝ |
---|
| 17 | P1: Byte → LineType |
---|
| 18 | | P3: Byte → LineType |
---|
| 19 | | SerialBuffer: SerialBufferType → LineType. |
---|
| 20 | |
---|
| 21 | (* What is a continuation, now? *) |
---|
| 22 | |
---|
| 23 | inductive SFR8051: Type[0] ≝ |
---|
| 24 | SFR_SP: SFR8051 |
---|
| 25 | | SFR_DPL: SFR8051 |
---|
| 26 | | SFR_DPH: SFR8051 |
---|
| 27 | | SFR_PCON: SFR8051 |
---|
| 28 | | SFR_TCON: SFR8051 |
---|
| 29 | | SFR_TMOD: SFR8051 |
---|
| 30 | | SFR_TL0: SFR8051 |
---|
| 31 | | SFR_TL1: SFR8051 |
---|
| 32 | | SFR_TH0: SFR8051 |
---|
| 33 | | SFR_TH1: SFR8051 |
---|
| 34 | | SFR_P1: SFR8051 |
---|
| 35 | | SFR_SCON: SFR8051 |
---|
| 36 | | SFR_SBUF: SFR8051 |
---|
| 37 | | SFR_IE: SFR8051 |
---|
| 38 | | SFR_P3: SFR8051 |
---|
| 39 | | SFR_IP: SFR8051 |
---|
| 40 | | SFR_PSW: SFR8051 |
---|
| 41 | | SFR_ACC_A: SFR8051 |
---|
| 42 | | SFR_ACC_B: SFR8051. |
---|
| 43 | |
---|
| 44 | definition sfr_8051_index ≝ |
---|
| 45 | λs: SFR8051. |
---|
| 46 | match s with |
---|
| 47 | [ SFR_SP ⇒ O |
---|
| 48 | | SFR_DPL ⇒ 1 |
---|
| 49 | | SFR_DPH ⇒ 2 |
---|
| 50 | | SFR_PCON ⇒ 3 |
---|
| 51 | | SFR_TCON ⇒ 4 |
---|
| 52 | | SFR_TMOD ⇒ 5 |
---|
| 53 | | SFR_TL0 ⇒ 6 |
---|
| 54 | | SFR_TL1 ⇒ 7 |
---|
| 55 | | SFR_TH0 ⇒ 8 |
---|
| 56 | | SFR_TH1 ⇒ 9 |
---|
| 57 | | SFR_P1 ⇒ 10 |
---|
| 58 | | SFR_SCON ⇒ 11 |
---|
| 59 | | SFR_SBUF ⇒ 12 |
---|
| 60 | | SFR_IE ⇒ 13 |
---|
| 61 | | SFR_P3 ⇒ 14 |
---|
| 62 | | SFR_IP ⇒ 15 |
---|
| 63 | | SFR_PSW ⇒ 16 |
---|
| 64 | | SFR_ACC_A ⇒ 17 |
---|
| 65 | | SFR_ACC_B ⇒ 18 |
---|
| 66 | ]. |
---|
| 67 | |
---|
| 68 | inductive SFR8052: Type[0] ≝ |
---|
| 69 | SFR_T2CON: SFR8052 |
---|
| 70 | | SFR_RCAP2L: SFR8052 |
---|
| 71 | | SFR_RCAP2H: SFR8052 |
---|
| 72 | | SFR_TL2: SFR8052 |
---|
| 73 | | SFR_TH2: SFR8052. |
---|
| 74 | |
---|
| 75 | definition sfr_8052_index ≝ |
---|
| 76 | λs: SFR8052. |
---|
| 77 | match s with |
---|
| 78 | [ SFR_T2CON ⇒ O |
---|
| 79 | | SFR_RCAP2L ⇒ 1 |
---|
| 80 | | SFR_RCAP2H ⇒ 2 |
---|
| 81 | | SFR_TL2 ⇒ 3 |
---|
| 82 | | SFR_TH2 ⇒ 4 |
---|
| 83 | ]. |
---|
| 84 | |
---|
| 85 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 86 | (* Processor status. *) |
---|
| 87 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[1666] | 88 | record PreStatus (M: Type[0]) (code_memory: M) : Type[0] ≝ |
---|
[475] | 89 | { |
---|
| 90 | low_internal_ram: BitVectorTrie Byte 7; |
---|
| 91 | high_internal_ram: BitVectorTrie Byte 7; |
---|
| 92 | external_ram: BitVectorTrie Byte 16; |
---|
| 93 | |
---|
| 94 | program_counter: Word; |
---|
| 95 | |
---|
| 96 | special_function_registers_8051: Vector Byte 19; |
---|
| 97 | special_function_registers_8052: Vector Byte 5; |
---|
| 98 | |
---|
| 99 | p1_latch: Byte; |
---|
| 100 | p3_latch: Byte; |
---|
| 101 | |
---|
| 102 | clock: Time |
---|
| 103 | }. |
---|
| 104 | |
---|
[821] | 105 | definition Status ≝ PreStatus (BitVectorTrie Byte 16). |
---|
[827] | 106 | definition PseudoStatus ≝ PreStatus (pseudo_assembly_program). |
---|
[821] | 107 | |
---|
[475] | 108 | lemma sfr8051_index_19: |
---|
| 109 | ∀i: SFR8051. |
---|
| 110 | sfr_8051_index i < 19. |
---|
| 111 | # i |
---|
| 112 | cases i |
---|
| 113 | normalize |
---|
| 114 | repeat (@ le_S_S) |
---|
| 115 | @ le_O_n |
---|
| 116 | qed. |
---|
| 117 | |
---|
| 118 | lemma sfr8052_index_5: |
---|
| 119 | ∀i: SFR8052. |
---|
| 120 | sfr_8052_index i < 5. |
---|
| 121 | # i |
---|
| 122 | cases i |
---|
| 123 | normalize |
---|
| 124 | repeat (@ le_S_S) |
---|
| 125 | @ le_O_n |
---|
| 126 | qed. |
---|
| 127 | |
---|
| 128 | definition set_clock ≝ |
---|
[821] | 129 | λM: Type[0]. |
---|
[1666] | 130 | λcode_memory:M. |
---|
| 131 | λs: PreStatus M code_memory. |
---|
[475] | 132 | λt: Time. |
---|
[1666] | 133 | let old_low_internal_ram ≝ low_internal_ram ?? s in |
---|
| 134 | let old_high_internal_ram ≝ high_internal_ram ?? s in |
---|
| 135 | let old_external_ram ≝ external_ram ?? s in |
---|
| 136 | let old_program_counter ≝ program_counter ?? s in |
---|
| 137 | let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in |
---|
| 138 | let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in |
---|
| 139 | let old_p1_latch ≝ p1_latch ?? s in |
---|
| 140 | let old_p3_latch ≝ p3_latch ?? s in |
---|
| 141 | mk_PreStatus M code_memory |
---|
[475] | 142 | old_low_internal_ram |
---|
| 143 | old_high_internal_ram |
---|
| 144 | old_external_ram |
---|
| 145 | old_program_counter |
---|
| 146 | old_special_function_registers_8051 |
---|
| 147 | old_special_function_registers_8052 |
---|
| 148 | old_p1_latch |
---|
| 149 | old_p3_latch |
---|
| 150 | t. |
---|
| 151 | |
---|
| 152 | definition set_p1_latch ≝ |
---|
[821] | 153 | λM: Type[0]. |
---|
[1666] | 154 | λcode_memory:M. |
---|
| 155 | λs: PreStatus M code_memory. |
---|
[475] | 156 | λb: Byte. |
---|
[1666] | 157 | let old_low_internal_ram ≝ low_internal_ram ?? s in |
---|
| 158 | let old_high_internal_ram ≝ high_internal_ram ?? s in |
---|
| 159 | let old_external_ram ≝ external_ram ?? s in |
---|
| 160 | let old_program_counter ≝ program_counter ?? s in |
---|
| 161 | let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in |
---|
| 162 | let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in |
---|
| 163 | let old_p3_latch ≝ p3_latch ?? s in |
---|
| 164 | let old_clock ≝ clock ?? s in |
---|
| 165 | mk_PreStatus M code_memory |
---|
[475] | 166 | old_low_internal_ram |
---|
| 167 | old_high_internal_ram |
---|
| 168 | old_external_ram |
---|
| 169 | old_program_counter |
---|
| 170 | old_special_function_registers_8051 |
---|
| 171 | old_special_function_registers_8052 |
---|
| 172 | b |
---|
| 173 | old_p3_latch |
---|
| 174 | old_clock. |
---|
| 175 | |
---|
| 176 | definition set_p3_latch ≝ |
---|
[821] | 177 | λM: Type[0]. |
---|
[1666] | 178 | λcode_memory:M. |
---|
| 179 | λs: PreStatus M code_memory. |
---|
[475] | 180 | λb: Byte. |
---|
[1666] | 181 | let old_low_internal_ram ≝ low_internal_ram ?? s in |
---|
| 182 | let old_high_internal_ram ≝ high_internal_ram ?? s in |
---|
| 183 | let old_external_ram ≝ external_ram ?? s in |
---|
| 184 | let old_program_counter ≝ program_counter ?? s in |
---|
| 185 | let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in |
---|
| 186 | let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in |
---|
| 187 | let old_p1_latch ≝ p1_latch ?? s in |
---|
| 188 | let old_clock ≝ clock ?? s in |
---|
| 189 | mk_PreStatus M code_memory |
---|
[475] | 190 | old_low_internal_ram |
---|
| 191 | old_high_internal_ram |
---|
| 192 | old_external_ram |
---|
| 193 | old_program_counter |
---|
| 194 | old_special_function_registers_8051 |
---|
| 195 | old_special_function_registers_8052 |
---|
| 196 | old_p1_latch |
---|
| 197 | b |
---|
| 198 | old_clock. |
---|
| 199 | |
---|
| 200 | definition get_8051_sfr ≝ |
---|
[821] | 201 | λM: Type[0]. |
---|
[1666] | 202 | λcode_memory:M. |
---|
| 203 | λs: PreStatus M code_memory. |
---|
[475] | 204 | λi: SFR8051. |
---|
[1666] | 205 | let sfr ≝ special_function_registers_8051 ?? s in |
---|
[475] | 206 | let index ≝ sfr_8051_index i in |
---|
| 207 | get_index_v … sfr index ?. |
---|
| 208 | @ sfr8051_index_19 |
---|
| 209 | qed. |
---|
| 210 | |
---|
| 211 | definition get_8052_sfr ≝ |
---|
[821] | 212 | λM: Type[0]. |
---|
[1666] | 213 | λcode_memory:M. |
---|
| 214 | λs: PreStatus M code_memory. |
---|
[475] | 215 | λi: SFR8052. |
---|
[1666] | 216 | let sfr ≝ special_function_registers_8052 ?? s in |
---|
[475] | 217 | let index ≝ sfr_8052_index i in |
---|
| 218 | get_index_v … sfr index ?. |
---|
| 219 | @ sfr8052_index_5 |
---|
| 220 | qed. |
---|
| 221 | |
---|
| 222 | definition set_8051_sfr ≝ |
---|
[821] | 223 | λM: Type[0]. |
---|
[1666] | 224 | λcode_memory:M. |
---|
| 225 | λs: PreStatus M code_memory. |
---|
[475] | 226 | λi: SFR8051. |
---|
| 227 | λb: Byte. |
---|
| 228 | let index ≝ sfr_8051_index i in |
---|
[1666] | 229 | let old_low_internal_ram ≝ low_internal_ram ?? s in |
---|
| 230 | let old_high_internal_ram ≝ high_internal_ram ?? s in |
---|
| 231 | let old_external_ram ≝ external_ram ?? s in |
---|
| 232 | let old_program_counter ≝ program_counter ?? s in |
---|
| 233 | let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in |
---|
| 234 | let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in |
---|
[475] | 235 | let new_special_function_registers_8051 ≝ |
---|
| 236 | set_index Byte 19 old_special_function_registers_8051 index b ? in |
---|
[1666] | 237 | let old_p1_latch ≝ p1_latch ?? s in |
---|
| 238 | let old_p3_latch ≝ p3_latch ?? s in |
---|
| 239 | let old_clock ≝ clock ?? s in |
---|
| 240 | mk_PreStatus M code_memory |
---|
[475] | 241 | old_low_internal_ram |
---|
| 242 | old_high_internal_ram |
---|
| 243 | old_external_ram |
---|
| 244 | old_program_counter |
---|
| 245 | new_special_function_registers_8051 |
---|
| 246 | old_special_function_registers_8052 |
---|
| 247 | old_p1_latch |
---|
| 248 | old_p3_latch |
---|
| 249 | old_clock. |
---|
| 250 | @ (sfr8051_index_19 i) |
---|
| 251 | qed. |
---|
| 252 | |
---|
| 253 | definition set_8052_sfr ≝ |
---|
[821] | 254 | λM: Type[0]. |
---|
[1666] | 255 | λcode_memory:M. |
---|
| 256 | λs: PreStatus M code_memory. |
---|
[475] | 257 | λi: SFR8052. |
---|
| 258 | λb: Byte. |
---|
| 259 | let index ≝ sfr_8052_index i in |
---|
[1666] | 260 | let old_low_internal_ram ≝ low_internal_ram ?? s in |
---|
| 261 | let old_high_internal_ram ≝ high_internal_ram ?? s in |
---|
| 262 | let old_external_ram ≝ external_ram ?? s in |
---|
| 263 | let old_program_counter ≝ program_counter ?? s in |
---|
| 264 | let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in |
---|
| 265 | let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in |
---|
[475] | 266 | let new_special_function_registers_8052 ≝ |
---|
| 267 | set_index Byte 5 old_special_function_registers_8052 index b ? in |
---|
[1666] | 268 | let old_p1_latch ≝ p1_latch ?? s in |
---|
| 269 | let old_p3_latch ≝ p3_latch ?? s in |
---|
| 270 | let old_clock ≝ clock ?? s in |
---|
| 271 | mk_PreStatus M code_memory |
---|
[475] | 272 | old_low_internal_ram |
---|
| 273 | old_high_internal_ram |
---|
| 274 | old_external_ram |
---|
| 275 | old_program_counter |
---|
| 276 | old_special_function_registers_8051 |
---|
| 277 | new_special_function_registers_8052 |
---|
| 278 | old_p1_latch |
---|
| 279 | old_p3_latch |
---|
| 280 | old_clock. |
---|
| 281 | @ (sfr8052_index_5 i) |
---|
| 282 | qed. |
---|
| 283 | |
---|
| 284 | definition set_program_counter ≝ |
---|
[821] | 285 | λM: Type[0]. |
---|
[1666] | 286 | λcode_memory:M. |
---|
| 287 | λs: PreStatus M code_memory. |
---|
[475] | 288 | λw: Word. |
---|
[1666] | 289 | let old_low_internal_ram ≝ low_internal_ram ?? s in |
---|
| 290 | let old_high_internal_ram ≝ high_internal_ram ?? s in |
---|
| 291 | let old_external_ram ≝ external_ram ?? s in |
---|
| 292 | let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in |
---|
| 293 | let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in |
---|
| 294 | let old_p1_latch ≝ p1_latch ?? s in |
---|
| 295 | let old_p3_latch ≝ p3_latch ?? s in |
---|
| 296 | let old_clock ≝ clock ?? s in |
---|
| 297 | mk_PreStatus M code_memory |
---|
[475] | 298 | old_low_internal_ram |
---|
| 299 | old_high_internal_ram |
---|
| 300 | old_external_ram |
---|
| 301 | w |
---|
| 302 | old_special_function_registers_8051 |
---|
| 303 | old_special_function_registers_8052 |
---|
| 304 | old_p1_latch |
---|
| 305 | old_p3_latch |
---|
| 306 | old_clock. |
---|
| 307 | |
---|
| 308 | definition set_code_memory ≝ |
---|
[911] | 309 | λM,M': Type[0]. |
---|
[1666] | 310 | λcode_memory:M. |
---|
| 311 | λs: PreStatus M code_memory. |
---|
[911] | 312 | λr: M'. |
---|
[1666] | 313 | let old_low_internal_ram ≝ low_internal_ram ?? s in |
---|
| 314 | let old_high_internal_ram ≝ high_internal_ram ?? s in |
---|
| 315 | let old_external_ram ≝ external_ram ?? s in |
---|
| 316 | let old_program_counter ≝ program_counter ?? s in |
---|
| 317 | let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in |
---|
| 318 | let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in |
---|
| 319 | let old_p1_latch ≝ p1_latch ?? s in |
---|
| 320 | let old_p3_latch ≝ p3_latch ?? s in |
---|
| 321 | let old_clock ≝ clock ?? s in |
---|
[911] | 322 | mk_PreStatus M' r |
---|
[475] | 323 | old_low_internal_ram |
---|
| 324 | old_high_internal_ram |
---|
| 325 | old_external_ram |
---|
| 326 | old_program_counter |
---|
| 327 | old_special_function_registers_8051 |
---|
| 328 | old_special_function_registers_8052 |
---|
| 329 | old_p1_latch |
---|
| 330 | old_p3_latch |
---|
| 331 | old_clock. |
---|
| 332 | |
---|
| 333 | definition set_low_internal_ram ≝ |
---|
[821] | 334 | λM: Type[0]. |
---|
[1666] | 335 | λcode_memory:M. |
---|
| 336 | λs: PreStatus M code_memory. |
---|
[475] | 337 | λr: BitVectorTrie Byte 7. |
---|
[1666] | 338 | let old_high_internal_ram ≝ high_internal_ram ?? s in |
---|
| 339 | let old_external_ram ≝ external_ram ?? s in |
---|
| 340 | let old_program_counter ≝ program_counter ?? s in |
---|
| 341 | let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in |
---|
| 342 | let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in |
---|
| 343 | let old_p1_latch ≝ p1_latch ?? s in |
---|
| 344 | let old_p3_latch ≝ p3_latch ?? s in |
---|
| 345 | let old_clock ≝ clock ?? s in |
---|
| 346 | mk_PreStatus M code_memory |
---|
[475] | 347 | r |
---|
| 348 | old_high_internal_ram |
---|
| 349 | old_external_ram |
---|
| 350 | old_program_counter |
---|
| 351 | old_special_function_registers_8051 |
---|
| 352 | old_special_function_registers_8052 |
---|
| 353 | old_p1_latch |
---|
| 354 | old_p3_latch |
---|
| 355 | old_clock. |
---|
| 356 | |
---|
| 357 | definition set_high_internal_ram ≝ |
---|
[821] | 358 | λM: Type[0]. |
---|
[1666] | 359 | λcode_memory:M. |
---|
| 360 | λs: PreStatus M code_memory. |
---|
[475] | 361 | λr: BitVectorTrie Byte 7. |
---|
[1666] | 362 | let old_low_internal_ram ≝ low_internal_ram ?? s in |
---|
| 363 | let old_high_internal_ram ≝ high_internal_ram ?? s in |
---|
| 364 | let old_external_ram ≝ external_ram ?? s in |
---|
| 365 | let old_program_counter ≝ program_counter ?? s in |
---|
| 366 | let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in |
---|
| 367 | let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in |
---|
| 368 | let old_p1_latch ≝ p1_latch ?? s in |
---|
| 369 | let old_p3_latch ≝ p3_latch ?? s in |
---|
| 370 | let old_clock ≝ clock ?? s in |
---|
| 371 | mk_PreStatus M code_memory |
---|
[475] | 372 | old_low_internal_ram |
---|
| 373 | r |
---|
| 374 | old_external_ram |
---|
| 375 | old_program_counter |
---|
| 376 | old_special_function_registers_8051 |
---|
| 377 | old_special_function_registers_8052 |
---|
| 378 | old_p1_latch |
---|
| 379 | old_p3_latch |
---|
| 380 | old_clock. |
---|
| 381 | |
---|
| 382 | definition set_external_ram ≝ |
---|
[821] | 383 | λM: Type[0]. |
---|
[1666] | 384 | λcode_memory:M. |
---|
| 385 | λs: PreStatus M code_memory. |
---|
[475] | 386 | λr: BitVectorTrie Byte 16. |
---|
[1666] | 387 | let old_low_internal_ram ≝ low_internal_ram ?? s in |
---|
| 388 | let old_high_internal_ram ≝ high_internal_ram ?? s in |
---|
| 389 | let old_program_counter ≝ program_counter ?? s in |
---|
| 390 | let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in |
---|
| 391 | let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in |
---|
| 392 | let old_p1_latch ≝ p1_latch ?? s in |
---|
| 393 | let old_p3_latch ≝ p3_latch ?? s in |
---|
| 394 | let old_clock ≝ clock ?? s in |
---|
| 395 | mk_PreStatus M code_memory |
---|
[475] | 396 | old_low_internal_ram |
---|
| 397 | old_high_internal_ram |
---|
| 398 | r |
---|
| 399 | old_program_counter |
---|
| 400 | old_special_function_registers_8051 |
---|
| 401 | old_special_function_registers_8052 |
---|
| 402 | old_p1_latch |
---|
| 403 | old_p3_latch |
---|
| 404 | old_clock. |
---|
| 405 | |
---|
| 406 | definition get_cy_flag ≝ |
---|
[821] | 407 | λM: Type[0]. |
---|
[1666] | 408 | λcode_memory:M. |
---|
| 409 | λs: PreStatus M code_memory. |
---|
| 410 | let sfr ≝ special_function_registers_8051 ?? s in |
---|
[475] | 411 | let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 412 | get_index_v bool 8 psw O ?. |
---|
| 413 | normalize |
---|
| 414 | @ (le_S_S ? ?) |
---|
| 415 | [ @ le_O_n |
---|
| 416 | | repeat (@ (le_S_S)); |
---|
| 417 | // |
---|
| 418 | ] |
---|
| 419 | qed. |
---|
| 420 | |
---|
| 421 | definition get_ac_flag ≝ |
---|
[821] | 422 | λM: Type[0]. |
---|
[1666] | 423 | λcode_memory:M. |
---|
| 424 | λs: PreStatus M code_memory. |
---|
| 425 | let sfr ≝ special_function_registers_8051 ?? s in |
---|
[475] | 426 | let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in |
---|
[949] | 427 | get_index_v bool 8 psw 1 ?. |
---|
[475] | 428 | normalize |
---|
| 429 | repeat (@ (le_S_S ? ?)) |
---|
| 430 | @ le_O_n |
---|
| 431 | qed. |
---|
| 432 | |
---|
| 433 | definition get_fo_flag ≝ |
---|
[821] | 434 | λM: Type[0]. |
---|
[1666] | 435 | λcode_memory:M. |
---|
| 436 | λs: PreStatus M code_memory. |
---|
| 437 | let sfr ≝ special_function_registers_8051 ?? s in |
---|
[475] | 438 | let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 439 | get_index_v bool 8 psw 2 ?. |
---|
| 440 | normalize |
---|
| 441 | repeat (@ (le_S_S ? ?)) |
---|
| 442 | @ le_O_n |
---|
| 443 | qed. |
---|
| 444 | |
---|
| 445 | definition get_rs1_flag ≝ |
---|
[821] | 446 | λM: Type[0]. |
---|
[1666] | 447 | λcode_memory:M. |
---|
| 448 | λs: PreStatus M code_memory. |
---|
| 449 | let sfr ≝ special_function_registers_8051 ?? s in |
---|
[475] | 450 | let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 451 | get_index_v bool 8 psw 3 ?. |
---|
| 452 | normalize |
---|
| 453 | repeat (@ (le_S_S ? ?)) |
---|
| 454 | @ le_O_n |
---|
| 455 | qed. |
---|
| 456 | |
---|
| 457 | definition get_rs0_flag ≝ |
---|
[821] | 458 | λM: Type[0]. |
---|
[1666] | 459 | λcode_memory:M. |
---|
| 460 | λs: PreStatus M code_memory. |
---|
| 461 | let sfr ≝ special_function_registers_8051 ?? s in |
---|
[475] | 462 | let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 463 | get_index_v bool 8 psw 4 ?. |
---|
| 464 | normalize |
---|
| 465 | repeat (@ (le_S_S ? ?)) |
---|
| 466 | @ le_O_n |
---|
| 467 | qed. |
---|
| 468 | |
---|
| 469 | definition get_ov_flag ≝ |
---|
[821] | 470 | λM: Type[0]. |
---|
[1666] | 471 | λcode_memory:M. |
---|
| 472 | λs: PreStatus M code_memory. |
---|
| 473 | let sfr ≝ special_function_registers_8051 ?? s in |
---|
[475] | 474 | let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 475 | get_index_v bool 8 psw 5 ?. |
---|
| 476 | normalize |
---|
| 477 | repeat (@ (le_S_S ? ?)) |
---|
| 478 | @ le_O_n |
---|
| 479 | qed. |
---|
| 480 | |
---|
| 481 | definition get_ud_flag ≝ |
---|
[821] | 482 | λM: Type[0]. |
---|
[1666] | 483 | λcode_memory:M. |
---|
| 484 | λs: PreStatus M code_memory. |
---|
| 485 | let sfr ≝ special_function_registers_8051 ?? s in |
---|
[475] | 486 | let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 487 | get_index_v bool 8 psw 6 ?. |
---|
| 488 | normalize |
---|
| 489 | repeat (@ (le_S_S ? ?)) |
---|
| 490 | @ le_O_n |
---|
| 491 | qed. |
---|
| 492 | |
---|
| 493 | definition get_p_flag ≝ |
---|
[821] | 494 | λM: Type[0]. |
---|
[1666] | 495 | λcode_memory:M. |
---|
| 496 | λs: PreStatus M code_memory. |
---|
| 497 | let sfr ≝ special_function_registers_8051 ?? s in |
---|
[475] | 498 | let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 499 | get_index_v bool 8 psw 7 ?. |
---|
| 500 | normalize |
---|
| 501 | repeat (@ (le_S_S ? ?)) |
---|
| 502 | @ le_O_n |
---|
| 503 | qed. |
---|
| 504 | |
---|
| 505 | definition set_flags ≝ |
---|
[821] | 506 | λM: Type[0]. |
---|
[1666] | 507 | λcode_memory:M. |
---|
| 508 | λs: PreStatus M code_memory. |
---|
[475] | 509 | λcy: Bit. |
---|
| 510 | λac: option Bit. |
---|
| 511 | λov: Bit. |
---|
[1882] | 512 | let sfr_psw ≝ get_8051_sfr ?? s SFR_PSW in |
---|
| 513 | let old_cy ≝ get_index_v ?? sfr_psw O ? in |
---|
| 514 | let old_ac ≝ get_index_v ?? sfr_psw 1 ? in |
---|
| 515 | let old_fo ≝ get_index_v ?? sfr_psw 2 ? in |
---|
| 516 | let old_rs1 ≝ get_index_v ?? sfr_psw 3 ? in |
---|
| 517 | let old_rs0 ≝ get_index_v ?? sfr_psw 4 ? in |
---|
| 518 | let old_ov ≝ get_index_v ?? sfr_psw 5 ? in |
---|
| 519 | let old_ud ≝ get_index_v ?? sfr_psw 6 ? in |
---|
| 520 | let old_p ≝ get_index_v ?? sfr_psw 7 ? in |
---|
[475] | 521 | let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in |
---|
[1666] | 522 | set_8051_sfr ?? s SFR_PSW |
---|
| 523 | [[ old_cy ; new_ac ; old_fo ; old_rs1 ; |
---|
| 524 | old_rs0 ; old_ov ; old_ud ; old_p ]]. |
---|
[475] | 525 | [1,2,3,4,5,6,7,8: |
---|
| 526 | normalize |
---|
| 527 | repeat (@ le_S_S) |
---|
| 528 | @ le_O_n |
---|
| 529 | ] |
---|
| 530 | qed. |
---|
| 531 | |
---|
| 532 | definition initialise_status ≝ |
---|
[821] | 533 | λM: Type[0]. |
---|
| 534 | λcode_mem: M. |
---|
| 535 | let status ≝ mk_PreStatus M code_mem (* Code mem. *) |
---|
[475] | 536 | (Stub Byte 7) (* Low mem. *) |
---|
| 537 | (Stub Byte 7) (* High mem. *) |
---|
| 538 | (Stub Byte 16) (* Ext mem. *) |
---|
| 539 | (zero 16) (* PC. *) |
---|
| 540 | (replicate Byte 19 (zero 8)) (* 8051 SFR. *) |
---|
| 541 | (replicate Byte 5 (zero 8)) (* 8052 SFR. *) |
---|
| 542 | (zero 8) (* P1 latch. *) |
---|
| 543 | (zero 8) (* P3 latch. *) |
---|
| 544 | O (* Clock. *) |
---|
| 545 | in |
---|
[1666] | 546 | set_8051_sfr ?? status SFR_SP (bitvector_of_nat 8 7). |
---|
[475] | 547 | |
---|
| 548 | definition get_bit_addressable_sfr ≝ |
---|
[821] | 549 | λM: Type[0]. |
---|
[1666] | 550 | λcode_memory:M. |
---|
| 551 | λs: PreStatus M code_memory. |
---|
[475] | 552 | λn: nat. |
---|
| 553 | λb: BitVector n. |
---|
| 554 | λl: bool. |
---|
| 555 | let address ≝ nat_of_bitvector … b in |
---|
| 556 | if (eqb address 128) then |
---|
| 557 | ? |
---|
| 558 | else if (eqb address 144) then |
---|
| 559 | if l then |
---|
[1666] | 560 | (p1_latch ?? s) |
---|
[475] | 561 | else |
---|
[1666] | 562 | (get_8051_sfr ?? s SFR_P1) |
---|
[475] | 563 | else if (eqb address 160) then |
---|
| 564 | ? |
---|
| 565 | else if (eqb address 176) then |
---|
| 566 | if l then |
---|
[1666] | 567 | (p3_latch ?? s) |
---|
[475] | 568 | else |
---|
[1666] | 569 | (get_8051_sfr ?? s SFR_P3) |
---|
[475] | 570 | else if (eqb address 153) then |
---|
[1666] | 571 | get_8051_sfr ?? s SFR_SBUF |
---|
[475] | 572 | else if (eqb address 138) then |
---|
[1666] | 573 | get_8051_sfr ?? s SFR_TL0 |
---|
[475] | 574 | else if (eqb address 139) then |
---|
[1666] | 575 | get_8051_sfr ?? s SFR_TL1 |
---|
[475] | 576 | else if (eqb address 140) then |
---|
[1666] | 577 | get_8051_sfr ?? s SFR_TH0 |
---|
[475] | 578 | else if (eqb address 141) then |
---|
[1666] | 579 | get_8051_sfr ?? s SFR_TH1 |
---|
[475] | 580 | else if (eqb address 200) then |
---|
[1666] | 581 | get_8052_sfr ?? s SFR_T2CON |
---|
[475] | 582 | else if (eqb address 202) then |
---|
[1666] | 583 | get_8052_sfr ?? s SFR_RCAP2L |
---|
[475] | 584 | else if (eqb address 203) then |
---|
[1666] | 585 | get_8052_sfr ?? s SFR_RCAP2H |
---|
[475] | 586 | else if (eqb address 204) then |
---|
[1666] | 587 | get_8052_sfr ?? s SFR_TL2 |
---|
[475] | 588 | else if (eqb address 205) then |
---|
[1666] | 589 | get_8052_sfr ?? s SFR_TH2 |
---|
[475] | 590 | else if (eqb address 135) then |
---|
[1666] | 591 | get_8051_sfr ?? s SFR_PCON |
---|
[475] | 592 | else if (eqb address 136) then |
---|
[1666] | 593 | get_8051_sfr ?? s SFR_TCON |
---|
[475] | 594 | else if (eqb address 137) then |
---|
[1666] | 595 | get_8051_sfr ?? s SFR_TMOD |
---|
[475] | 596 | else if (eqb address 152) then |
---|
[1666] | 597 | get_8051_sfr ?? s SFR_SCON |
---|
[475] | 598 | else if (eqb address 168) then |
---|
[1666] | 599 | get_8051_sfr ?? s SFR_IE |
---|
[475] | 600 | else if (eqb address 184) then |
---|
[1666] | 601 | get_8051_sfr ?? s SFR_IP |
---|
[475] | 602 | else if (eqb address 129) then |
---|
[1666] | 603 | get_8051_sfr ?? s SFR_SP |
---|
[475] | 604 | else if (eqb address 130) then |
---|
[1666] | 605 | get_8051_sfr ?? s SFR_DPL |
---|
[475] | 606 | else if (eqb address 131) then |
---|
[1666] | 607 | get_8051_sfr ?? s SFR_DPH |
---|
[475] | 608 | else if (eqb address 208) then |
---|
[1666] | 609 | get_8051_sfr ?? s SFR_PSW |
---|
[475] | 610 | else if (eqb address 224) then |
---|
[1666] | 611 | get_8051_sfr ?? s SFR_ACC_A |
---|
[475] | 612 | else if (eqb address 240) then |
---|
[1666] | 613 | get_8051_sfr ?? s SFR_ACC_B |
---|
[475] | 614 | else |
---|
| 615 | ?. |
---|
| 616 | cases not_implemented |
---|
| 617 | qed. |
---|
| 618 | |
---|
| 619 | definition set_bit_addressable_sfr ≝ |
---|
[821] | 620 | λM: Type[0]. |
---|
[1666] | 621 | λcode_memory:M. |
---|
| 622 | λs: PreStatus M code_memory. |
---|
[475] | 623 | λb: Byte. |
---|
| 624 | λv: Byte. |
---|
| 625 | let address ≝ nat_of_bitvector … b in |
---|
| 626 | if (eqb address 128) then |
---|
| 627 | ? |
---|
| 628 | else if (eqb address 144) then |
---|
[1666] | 629 | let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in |
---|
| 630 | let status_2 ≝ set_p1_latch ?? s v in |
---|
[475] | 631 | status_2 |
---|
| 632 | else if (eqb address 160) then |
---|
| 633 | ? |
---|
| 634 | else if (eqb address 176) then |
---|
[1666] | 635 | let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in |
---|
| 636 | let status_2 ≝ set_p3_latch ?? s v in |
---|
[475] | 637 | status_2 |
---|
| 638 | else if (eqb address 153) then |
---|
[1666] | 639 | set_8051_sfr ?? s SFR_SBUF v |
---|
[475] | 640 | else if (eqb address 138) then |
---|
[1666] | 641 | set_8051_sfr ?? s SFR_TL0 v |
---|
[475] | 642 | else if (eqb address 139) then |
---|
[1666] | 643 | set_8051_sfr ?? s SFR_TL1 v |
---|
[475] | 644 | else if (eqb address 140) then |
---|
[1666] | 645 | set_8051_sfr ?? s SFR_TH0 v |
---|
[475] | 646 | else if (eqb address 141) then |
---|
[1666] | 647 | set_8051_sfr ?? s SFR_TH1 v |
---|
[475] | 648 | else if (eqb address 200) then |
---|
[1666] | 649 | set_8052_sfr ?? s SFR_T2CON v |
---|
[475] | 650 | else if (eqb address 202) then |
---|
[1666] | 651 | set_8052_sfr ?? s SFR_RCAP2L v |
---|
[475] | 652 | else if (eqb address 203) then |
---|
[1666] | 653 | set_8052_sfr ?? s SFR_RCAP2H v |
---|
[475] | 654 | else if (eqb address 204) then |
---|
[1666] | 655 | set_8052_sfr ?? s SFR_TL2 v |
---|
[475] | 656 | else if (eqb address 205) then |
---|
[1666] | 657 | set_8052_sfr ?? s SFR_TH2 v |
---|
[475] | 658 | else if (eqb address 135) then |
---|
[1666] | 659 | set_8051_sfr ?? s SFR_PCON v |
---|
[475] | 660 | else if (eqb address 136) then |
---|
[1666] | 661 | set_8051_sfr ?? s SFR_TCON v |
---|
[475] | 662 | else if (eqb address 137) then |
---|
[1666] | 663 | set_8051_sfr ?? s SFR_TMOD v |
---|
[475] | 664 | else if (eqb address 152) then |
---|
[1666] | 665 | set_8051_sfr ?? s SFR_SCON v |
---|
[475] | 666 | else if (eqb address 168) then |
---|
[1666] | 667 | set_8051_sfr ?? s SFR_IE v |
---|
[475] | 668 | else if (eqb address 184) then |
---|
[1666] | 669 | set_8051_sfr ?? s SFR_IP v |
---|
[475] | 670 | else if (eqb address 129) then |
---|
[1666] | 671 | set_8051_sfr ?? s SFR_SP v |
---|
[475] | 672 | else if (eqb address 130) then |
---|
[1666] | 673 | set_8051_sfr ?? s SFR_DPL v |
---|
[475] | 674 | else if (eqb address 131) then |
---|
[1666] | 675 | set_8051_sfr ?? s SFR_DPH v |
---|
[475] | 676 | else if (eqb address 208) then |
---|
[1666] | 677 | set_8051_sfr ?? s SFR_PSW v |
---|
[475] | 678 | else if (eqb address 224) then |
---|
[1666] | 679 | set_8051_sfr ?? s SFR_ACC_A v |
---|
[475] | 680 | else if (eqb address 240) then |
---|
[1666] | 681 | set_8051_sfr ?? s SFR_ACC_B v |
---|
[475] | 682 | else |
---|
| 683 | ?. |
---|
| 684 | cases not_implemented |
---|
| 685 | qed. |
---|
| 686 | |
---|
| 687 | definition bit_address_of_register ≝ |
---|
[821] | 688 | λM: Type[0]. |
---|
[1666] | 689 | λcode_memory:M. |
---|
| 690 | λs: PreStatus M code_memory. |
---|
[475] | 691 | λr: BitVector 3. |
---|
| 692 | let b ≝ get_index_v … r O ? in |
---|
| 693 | let c ≝ get_index_v … r 1 ? in |
---|
| 694 | let d ≝ get_index_v … r 2 ? in |
---|
[2032] | 695 | let 〈 un, ln 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in |
---|
[705] | 696 | let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in |
---|
[475] | 697 | let offset ≝ |
---|
| 698 | if ¬r1 ∧ ¬r0 then |
---|
| 699 | O |
---|
| 700 | else if ¬r1 ∧ r0 then |
---|
| 701 | 8 |
---|
| 702 | else if r1 ∧ r0 then |
---|
| 703 | 24 |
---|
| 704 | else |
---|
| 705 | 16 |
---|
| 706 | in |
---|
| 707 | bitvector_of_nat 7 (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])). |
---|
| 708 | [1,2,3,4,5: |
---|
| 709 | normalize |
---|
| 710 | repeat (@ le_S_S) |
---|
| 711 | @ le_O_n; |
---|
| 712 | ] |
---|
| 713 | qed. |
---|
| 714 | |
---|
| 715 | definition get_register ≝ |
---|
[821] | 716 | λM: Type[0]. |
---|
[1666] | 717 | λcode_memory:M. |
---|
| 718 | λs: PreStatus M code_memory. |
---|
[475] | 719 | λr: BitVector 3. |
---|
[1666] | 720 | let address ≝ bit_address_of_register … s r in |
---|
| 721 | lookup ?? address (low_internal_ram … s) (zero 8). |
---|
[475] | 722 | |
---|
| 723 | definition set_register ≝ |
---|
[821] | 724 | λM: Type[0]. |
---|
[1666] | 725 | λcode_memory:M. |
---|
| 726 | λs: PreStatus M code_memory. |
---|
[475] | 727 | λr: BitVector 3. |
---|
| 728 | λv: Byte. |
---|
[1666] | 729 | let address ≝ bit_address_of_register … s r in |
---|
| 730 | let old_low_internal_ram ≝ low_internal_ram ?? s in |
---|
[475] | 731 | let new_low_internal_ram ≝ insert … address v old_low_internal_ram in |
---|
[1666] | 732 | set_low_internal_ram … s new_low_internal_ram. |
---|
[475] | 733 | |
---|
| 734 | definition read_at_stack_pointer ≝ |
---|
[821] | 735 | λM: Type[0]. |
---|
[1666] | 736 | λcode_memory:M. |
---|
| 737 | λs: PreStatus M code_memory. |
---|
[2032] | 738 | let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_SP) in |
---|
[1666] | 739 | let m ≝ get_index_v ?? nu O ? in |
---|
| 740 | let r1 ≝ get_index_v ?? nu 1 ? in |
---|
| 741 | let r2 ≝ get_index_v ?? nu 2 ? in |
---|
| 742 | let r3 ≝ get_index_v ?? nu 3 ? in |
---|
[475] | 743 | let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in |
---|
| 744 | let memory ≝ |
---|
| 745 | if m then |
---|
[1666] | 746 | (low_internal_ram ?? s) |
---|
[475] | 747 | else |
---|
[1666] | 748 | (high_internal_ram ?? s) |
---|
[475] | 749 | in |
---|
| 750 | lookup … address memory (zero 8). |
---|
| 751 | [1,2,3,4: |
---|
| 752 | normalize |
---|
| 753 | repeat (@ le_S_S) |
---|
| 754 | @ le_O_n |
---|
| 755 | ] |
---|
| 756 | qed. |
---|
| 757 | |
---|
| 758 | definition write_at_stack_pointer ≝ |
---|
[821] | 759 | λM: Type[0]. |
---|
[1666] | 760 | λcode_memory:M. |
---|
| 761 | λs: PreStatus M code_memory. |
---|
[475] | 762 | λv: Byte. |
---|
[2032] | 763 | let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ?? s SFR_SP) in |
---|
[1666] | 764 | let bit_zero ≝ get_index_v ?? nu O ? in |
---|
| 765 | let bit_1 ≝ get_index_v ?? nu 1 ? in |
---|
| 766 | let bit_2 ≝ get_index_v ?? nu 2 ? in |
---|
| 767 | let bit_3 ≝ get_index_v ?? nu 3 ? in |
---|
[475] | 768 | if bit_zero then |
---|
| 769 | let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) |
---|
[1666] | 770 | v (low_internal_ram ?? s) in |
---|
| 771 | set_low_internal_ram ?? s memory |
---|
[475] | 772 | else |
---|
| 773 | let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) |
---|
[1666] | 774 | v (high_internal_ram ?? s) in |
---|
| 775 | set_high_internal_ram ?? s memory. |
---|
[475] | 776 | [1,2,3,4: |
---|
| 777 | normalize |
---|
| 778 | repeat (@ le_S_S) |
---|
| 779 | @ le_O_n |
---|
| 780 | ] |
---|
| 781 | qed. |
---|
| 782 | |
---|
[1666] | 783 | definition set_arg_16': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → Σs':PreStatus M code_memory. clock ?? s = clock ?? s' ≝ |
---|
| 784 | λM,code_memory,s,v,a. |
---|
| 785 | match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M ? s = clock M ? s' with |
---|
[475] | 786 | [ DPTR ⇒ λ_:True. |
---|
[2032] | 787 | let 〈 bu, bl 〉 ≝ vsplit … 8 8 v in |
---|
[1666] | 788 | let status ≝ set_8051_sfr … s SFR_DPH bu in |
---|
| 789 | let status ≝ set_8051_sfr … status SFR_DPL bl in |
---|
[475] | 790 | status |
---|
| 791 | | _ ⇒ λK. |
---|
| 792 | match K in False with |
---|
| 793 | [ |
---|
| 794 | ] |
---|
| 795 | ] (subaddressing_modein … a). |
---|
[1588] | 796 | // |
---|
| 797 | qed. |
---|
| 798 | |
---|
[1666] | 799 | definition set_arg_16: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → PreStatus M code_memory ≝ |
---|
[1588] | 800 | set_arg_16'. |
---|
| 801 | |
---|
[1666] | 802 | lemma set_arg_16_ok: ∀M,cm,s,v,x. clock M cm s = clock M cm (set_arg_16 M cm s v x). |
---|
| 803 | #M #cm #s #x #v whd in match set_arg_16; normalize nodelta @pi2 |
---|
[1588] | 804 | qed. |
---|
| 805 | |
---|
[475] | 806 | |
---|
[1666] | 807 | definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ data16 ]] → Word ≝ |
---|
| 808 | λm, cm, s, a. |
---|
[475] | 809 | match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with |
---|
| 810 | [ DATA16 d ⇒ λ_:True. d |
---|
| 811 | | _ ⇒ λK. |
---|
| 812 | match K in False with |
---|
| 813 | [ |
---|
| 814 | ] |
---|
| 815 | ] (subaddressing_modein … a). |
---|
| 816 | |
---|
[1666] | 817 | definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ; |
---|
[475] | 818 | acc_a ; acc_b ; data ; acc_dptr ; |
---|
| 819 | acc_pc ; ext_indirect ; |
---|
| 820 | ext_indirect_dptr ]] → Byte ≝ |
---|
[1666] | 821 | λm, cm, s, l, a. |
---|
[757] | 822 | match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; |
---|
[475] | 823 | acc_a ; acc_b ; data ; acc_dptr ; |
---|
| 824 | acc_pc ; ext_indirect ; |
---|
| 825 | ext_indirect_dptr ]] x) → ? with |
---|
[1666] | 826 | [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A |
---|
| 827 | | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B |
---|
[475] | 828 | | DATA d ⇒ λdata: True. d |
---|
[1666] | 829 | | REGISTER r ⇒ λregister: True. get_register ?? s r |
---|
[475] | 830 | | EXT_INDIRECT_DPTR ⇒ |
---|
| 831 | λext_indirect_dptr: True. |
---|
[1666] | 832 | let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in |
---|
| 833 | lookup ? 16 address (external_ram ?? s) (zero 8) |
---|
[475] | 834 | | EXT_INDIRECT e ⇒ |
---|
| 835 | λext_indirect: True. |
---|
[1666] | 836 | let address ≝ get_register ?? s [[ false; false; e ]] in |
---|
[475] | 837 | let padded_address ≝ pad 8 8 address in |
---|
[1666] | 838 | lookup ? 16 padded_address (external_ram ?? s) (zero 8) |
---|
[475] | 839 | | ACC_DPTR ⇒ |
---|
| 840 | λacc_dptr: True. |
---|
[1666] | 841 | let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in |
---|
| 842 | let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in |
---|
[475] | 843 | let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in |
---|
[1666] | 844 | lookup ? 16 address (external_ram ?? s) (zero 8) |
---|
[475] | 845 | | ACC_PC ⇒ |
---|
| 846 | λacc_pc: True. |
---|
[1666] | 847 | let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in |
---|
| 848 | let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in |
---|
| 849 | lookup ? 16 address (external_ram ?? s) (zero 8) |
---|
[475] | 850 | | DIRECT d ⇒ |
---|
| 851 | λdirect: True. |
---|
[2032] | 852 | let 〈 nu, nl 〉 ≝ vsplit ? 4 4 d in |
---|
[949] | 853 | let bit_one ≝ get_index_v ? ? nu 0 ? in |
---|
[2032] | 854 | let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in |
---|
[949] | 855 | match bit_one with |
---|
| 856 | [ false ⇒ |
---|
[475] | 857 | let address ≝ three_bits @@ nl in |
---|
[1666] | 858 | lookup ? 7 address (low_internal_ram ?? s) (zero 8) |
---|
| 859 | | true ⇒ get_bit_addressable_sfr ?? s 8 d l |
---|
[475] | 860 | ] |
---|
| 861 | | INDIRECT i ⇒ |
---|
| 862 | λindirect: True. |
---|
[2032] | 863 | let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_register ?? s [[ false; false; i]]) in |
---|
| 864 | let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in |
---|
[1515] | 865 | let bit_1 ≝ get_index_v ?? bit_one_v O ? in |
---|
[949] | 866 | match bit_1 with |
---|
| 867 | [ false ⇒ |
---|
[1666] | 868 | lookup ? 7 (three_bits @@ nl) (low_internal_ram ?? s) (zero 8) |
---|
[949] | 869 | | true ⇒ |
---|
[1666] | 870 | lookup ? 7 (three_bits @@ nl) (high_internal_ram ?? s) (zero 8) |
---|
[475] | 871 | ] |
---|
| 872 | | _ ⇒ λother. |
---|
| 873 | match other in False with [ ] |
---|
| 874 | ] (subaddressing_modein … a). |
---|
| 875 | [1,2: |
---|
| 876 | normalize |
---|
| 877 | repeat (@ le_S_S) |
---|
| 878 | @ le_O_n |
---|
| 879 | ] |
---|
| 880 | qed. |
---|
| 881 | |
---|
[1666] | 882 | axiom clock_set_bit_addressable_sfr: ∀m,cm,s,d,v. clock m cm s = clock … (set_bit_addressable_sfr … s d v). |
---|
[1526] | 883 | |
---|
[1666] | 884 | definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; |
---|
[475] | 885 | acc_a ; acc_b ; ext_indirect ; |
---|
[1666] | 886 | ext_indirect_dptr ]] → Byte → Σs':PreStatus M code_memory. |
---|
| 887 | clock … code_memory s = clock … code_memory s' ≝ |
---|
| 888 | λm, cm, s, a, v. |
---|
[757] | 889 | match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; |
---|
[475] | 890 | acc_a ; acc_b ; ext_indirect ; |
---|
[1526] | 891 | ext_indirect_dptr ]] x) → |
---|
[1666] | 892 | Σs':PreStatus m cm. clock m cm s = clock m cm s' |
---|
[1526] | 893 | (*CSC: bug here if one specified the two clock above*) |
---|
| 894 | with |
---|
[475] | 895 | [ DIRECT d ⇒ |
---|
| 896 | λdirect: True. |
---|
[2032] | 897 | let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in |
---|
[949] | 898 | let bit_one ≝ get_index_v ? ? nu 0 ? in |
---|
[2032] | 899 | let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in |
---|
[949] | 900 | match bit_one with |
---|
[1666] | 901 | [ true ⇒ set_bit_addressable_sfr ?? s d v |
---|
[475] | 902 | | false ⇒ |
---|
[1666] | 903 | let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in |
---|
| 904 | set_low_internal_ram ?? s memory |
---|
[475] | 905 | ] |
---|
| 906 | | INDIRECT i ⇒ |
---|
| 907 | λindirect: True. |
---|
[1666] | 908 | let register ≝ get_register ?? s [[ false; false; i ]] in |
---|
[2032] | 909 | let 〈nu, nl〉 ≝ vsplit ? 4 4 register in |
---|
[949] | 910 | let bit_1 ≝ get_index_v … nu 0 ? in |
---|
[2032] | 911 | let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in |
---|
[475] | 912 | match bit_1 with |
---|
[949] | 913 | [ false ⇒ |
---|
[1666] | 914 | let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in |
---|
| 915 | set_low_internal_ram ?? s memory |
---|
[949] | 916 | | true ⇒ |
---|
[1666] | 917 | let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in |
---|
| 918 | set_high_internal_ram ?? s memory |
---|
[475] | 919 | ] |
---|
[1666] | 920 | | REGISTER r ⇒ λregister: True. set_register ?? s r v |
---|
| 921 | | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v |
---|
| 922 | | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v |
---|
[475] | 923 | | EXT_INDIRECT e ⇒ |
---|
| 924 | λext_indirect: True. |
---|
[1666] | 925 | let address ≝ get_register ?? s [[ false; false; e ]] in |
---|
[475] | 926 | let padded_address ≝ pad 8 8 address in |
---|
[1666] | 927 | let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in |
---|
| 928 | set_external_ram ?? s memory |
---|
[475] | 929 | | EXT_INDIRECT_DPTR ⇒ |
---|
| 930 | λext_indirect_dptr: True. |
---|
[1666] | 931 | let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in |
---|
| 932 | let memory ≝ insert ? 16 address v (external_ram ?? s) in |
---|
| 933 | set_external_ram ?? s memory |
---|
[1526] | 934 | | _ ⇒ |
---|
[475] | 935 | λother: False. |
---|
| 936 | match other in False with [ ] |
---|
| 937 | ] (subaddressing_modein … a). |
---|
[1526] | 938 | // qed. |
---|
[475] | 939 | |
---|
[1666] | 940 | definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M code_memory ≝ |
---|
[1588] | 941 | set_arg_8'. |
---|
| 942 | |
---|
[1666] | 943 | lemma set_arg_8_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v). |
---|
| 944 | #M #cm #s #x #v whd in match set_arg_8; normalize nodelta @pi2 |
---|
[1588] | 945 | qed. |
---|
| 946 | |
---|
[475] | 947 | theorem modulus_less_than: |
---|
| 948 | ∀m,n: nat. (m mod (S n)) < S n. |
---|
| 949 | #n #m |
---|
| 950 | normalize |
---|
| 951 | @ le_S_S |
---|
| 952 | lapply (le_n n) |
---|
[1516] | 953 | generalize in ⊢ (?%? → ?(??%?)?); |
---|
| 954 | elim n in ⊢ (∀_:?. ??% → ?(?%??)?); |
---|
[475] | 955 | [ normalize |
---|
| 956 | #n |
---|
| 957 | @ (less_than_or_equal_b_elim n m) |
---|
| 958 | normalize |
---|
| 959 | [ // |
---|
| 960 | | #H #K |
---|
[1516] | 961 | @(le_inv_ind ?? K …) |
---|
[475] | 962 | [ # H1 |
---|
| 963 | < H1 |
---|
| 964 | // |
---|
| 965 | | #x #H1 #H2 #H3 |
---|
| 966 | destruct |
---|
| 967 | ] |
---|
| 968 | ] |
---|
| 969 | | normalize |
---|
| 970 | # y # H1 # n # H2 |
---|
| 971 | @ (less_than_or_equal_b_elim n m) |
---|
| 972 | normalize |
---|
| 973 | [ // |
---|
| 974 | | # K |
---|
| 975 | @ H1 |
---|
| 976 | cut (n ≤ S y → n - S m ≤ y) |
---|
[1521] | 977 | /2 by/ |
---|
[475] | 978 | cases n |
---|
| 979 | normalize |
---|
| 980 | // |
---|
| 981 | # x # K1 |
---|
| 982 | lapply (le_S_S_to_le … K1) |
---|
[1516] | 983 | generalize in match m; |
---|
[475] | 984 | elim x |
---|
| 985 | normalize |
---|
| 986 | // |
---|
| 987 | # w1 # H # m |
---|
| 988 | cases m |
---|
| 989 | normalize |
---|
| 990 | // |
---|
| 991 | # q # K2 |
---|
[1516] | 992 | @H |
---|
[475] | 993 | /3/ |
---|
| 994 | ] |
---|
| 995 | ] |
---|
| 996 | qed. |
---|
| 997 | |
---|
[1666] | 998 | definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] → |
---|
[475] | 999 | bool → bool ≝ |
---|
[1666] | 1000 | λm, cm, s, a, l. |
---|
[475] | 1001 | match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; |
---|
| 1002 | n_bit_addr ; |
---|
| 1003 | carry ]] x) → ? with |
---|
| 1004 | [ BIT_ADDR b ⇒ |
---|
| 1005 | λbit_addr: True. |
---|
[2032] | 1006 | let 〈 nu, nl 〉 ≝ vsplit … 4 4 b in |
---|
[1393] | 1007 | let bit_1 ≝ get_index_v ? ? nu 0 ? in |
---|
[2032] | 1008 | let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in |
---|
[475] | 1009 | match bit_1 with |
---|
| 1010 | [ true ⇒ |
---|
| 1011 | let address ≝ nat_of_bitvector … (three_bits @@ nl) in |
---|
| 1012 | let d ≝ address ÷ 8 in |
---|
| 1013 | let m ≝ address mod 8 in |
---|
| 1014 | let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
[1666] | 1015 | let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in |
---|
[475] | 1016 | get_index_v … sfr m ? |
---|
| 1017 | | false ⇒ |
---|
| 1018 | let address ≝ nat_of_bitvector … (three_bits @@ nl) in |
---|
| 1019 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
[1666] | 1020 | let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
[475] | 1021 | get_index_v … t (modulus address 8) ? |
---|
| 1022 | ] |
---|
| 1023 | | N_BIT_ADDR n ⇒ |
---|
| 1024 | λn_bit_addr: True. |
---|
[2032] | 1025 | let 〈 nu, nl 〉 ≝ vsplit … 4 4 n in |
---|
[1393] | 1026 | let bit_1 ≝ get_index_v ? ? nu 0 ? in |
---|
[2032] | 1027 | let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in |
---|
[475] | 1028 | match bit_1 with |
---|
| 1029 | [ true ⇒ |
---|
| 1030 | let address ≝ nat_of_bitvector … (three_bits @@ nl) in |
---|
| 1031 | let d ≝ address ÷ 8 in |
---|
| 1032 | let m ≝ address mod 8 in |
---|
| 1033 | let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
[1666] | 1034 | let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in |
---|
[475] | 1035 | ¬(get_index_v … sfr m ?) |
---|
| 1036 | | false ⇒ |
---|
| 1037 | let address ≝ nat_of_bitvector … (three_bits @@ nl) in |
---|
| 1038 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
[1666] | 1039 | let trans ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
[475] | 1040 | ¬(get_index_v … trans (modulus address 8) ?) |
---|
| 1041 | ] |
---|
[1666] | 1042 | | CARRY ⇒ λcarry: True. get_cy_flag ?? s |
---|
[475] | 1043 | | _ ⇒ λother. |
---|
| 1044 | match other in False with [ ] |
---|
| 1045 | ] (subaddressing_modein … a). |
---|
| 1046 | [3,6: |
---|
| 1047 | normalize |
---|
| 1048 | repeat (@ le_S_S) |
---|
| 1049 | @ le_O_n |
---|
| 1050 | |1,2,4,5: |
---|
[1518] | 1051 | @modulus_less_than |
---|
[475] | 1052 | ] |
---|
| 1053 | qed. |
---|
| 1054 | |
---|
[1666] | 1055 | definition set_arg_1': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s' ≝ |
---|
[1581] | 1056 | λm: Type[0]. |
---|
[1666] | 1057 | λcm. |
---|
| 1058 | λs: PreStatus m cm. |
---|
[1581] | 1059 | λa: [[bit_addr; carry]]. |
---|
| 1060 | λv: Bit. |
---|
[1666] | 1061 | match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with |
---|
[475] | 1062 | [ BIT_ADDR b ⇒ λbit_addr: True. |
---|
[2032] | 1063 | let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in |
---|
[1581] | 1064 | let bit_1 ≝ get_index_v ?? nu 0 ? in |
---|
[2032] | 1065 | let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in |
---|
[1581] | 1066 | match bit_1 return λ_. ? with |
---|
| 1067 | [ true ⇒ |
---|
| 1068 | let address ≝ nat_of_bitvector … (three_bits @@ nl) in |
---|
| 1069 | let d ≝ address ÷ 8 in |
---|
| 1070 | let m ≝ address mod 8 in |
---|
| 1071 | let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
[1666] | 1072 | let sfr ≝ get_bit_addressable_sfr ?? s ? t true in |
---|
[1581] | 1073 | let new_sfr ≝ set_index … sfr m v ? in |
---|
[1666] | 1074 | set_bit_addressable_sfr ?? s new_sfr t |
---|
[1581] | 1075 | | false ⇒ |
---|
| 1076 | let address ≝ nat_of_bitvector … (three_bits @@ nl) in |
---|
| 1077 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
[1666] | 1078 | let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
[1581] | 1079 | let n_bit ≝ set_index … t (modulus address 8) v ? in |
---|
[1666] | 1080 | let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in |
---|
| 1081 | set_low_internal_ram ?? s memory |
---|
[1581] | 1082 | ] |
---|
[475] | 1083 | | CARRY ⇒ |
---|
| 1084 | λcarry: True. |
---|
[2032] | 1085 | let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in |
---|
[1581] | 1086 | let bit_1 ≝ get_index_v… nu 1 ? in |
---|
| 1087 | let bit_2 ≝ get_index_v… nu 2 ? in |
---|
| 1088 | let bit_3 ≝ get_index_v… nu 3 ? in |
---|
| 1089 | let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in |
---|
[1666] | 1090 | set_8051_sfr ?? s SFR_PSW new_psw |
---|
[475] | 1091 | | _ ⇒ |
---|
| 1092 | λother: False. |
---|
| 1093 | match other in False with |
---|
| 1094 | [ ] |
---|
| 1095 | ] (subaddressing_modein … a). |
---|
[1588] | 1096 | try (repeat @le_S_S @le_O_n) |
---|
| 1097 | /by/ |
---|
[475] | 1098 | qed. |
---|
| 1099 | |
---|
[1666] | 1100 | definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝ set_arg_1'. |
---|
[1588] | 1101 | |
---|
[1666] | 1102 | lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v). |
---|
| 1103 | #M #cm #s #x #v whd in match set_arg_1; normalize nodelta @pi2 |
---|
[1588] | 1104 | qed. |
---|
| 1105 | |
---|
[475] | 1106 | definition load_code_memory ≝ |
---|
| 1107 | fold_left_i … ( |
---|
| 1108 | λi, mem, v. |
---|
| 1109 | insert … (bitvector_of_nat … i) v mem) (Stub Byte 16). |
---|
| 1110 | |
---|
| 1111 | definition load ≝ |
---|
[1666] | 1112 | λl,cm. |
---|
[821] | 1113 | λstatus. |
---|
[1666] | 1114 | set_code_memory (BitVectorTrie Word 16) ? cm status (load_code_memory l). |
---|
[843] | 1115 | |
---|
| 1116 | definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝ |
---|
| 1117 | λcode_mem. |
---|
| 1118 | λpc: Word. |
---|
| 1119 | let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … code_mem ? in |
---|
[1946] | 1120 | let new_pc ≝ add ? pc (bitvector_of_nat ? 1) in |
---|
[843] | 1121 | 〈instr, new_pc〉. |
---|
| 1122 | cases not_implemented. |
---|
[985] | 1123 | qed. |
---|
| 1124 | |
---|
[993] | 1125 | lemma snd_fetch_pseudo_instruction: |
---|
[1946] | 1126 | ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = add ? ppc (bitvector_of_nat ? 1). |
---|
[1599] | 1127 | #l #ppc whd in ⊢ (??(???%)?); @pair_elim |
---|
[1946] | 1128 | #lft #rgt #_ % |
---|
[993] | 1129 | qed. |
---|
| 1130 | |
---|
[985] | 1131 | definition address_of_word_labels_code_mem ≝ |
---|
[1882] | 1132 | λcode_mem : list labelled_instruction. |
---|
[985] | 1133 | λid: Identifier. |
---|
[1882] | 1134 | bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem). |
---|
[985] | 1135 | |
---|
| 1136 | lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list. |
---|
[1882] | 1137 | occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) → |
---|
[985] | 1138 | address_of_word_labels_code_mem instr_list id = |
---|
| 1139 | address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id. |
---|
[1518] | 1140 | #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?)); |
---|
[1882] | 1141 | >(index_of_internal_None ?????? H) % |
---|
[985] | 1142 | qed. |
---|
| 1143 | |
---|
| 1144 | lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list. |
---|
[1515] | 1145 | eq_identifier ? id' id = false → |
---|
[1882] | 1146 | occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) → |
---|
[985] | 1147 | address_of_word_labels_code_mem instr_list id = |
---|
| 1148 | address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id. |
---|
[1518] | 1149 | #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?)); |
---|
[1882] | 1150 | >(index_of_internal_Some_miss ???????? H) [ @refl | // ] |
---|
[985] | 1151 | qed. |
---|
| 1152 | |
---|
| 1153 | lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list. |
---|
[1882] | 1154 | occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) → |
---|
[985] | 1155 | address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id |
---|
| 1156 | = bitvector_of_nat … (|instr_list|). |
---|
[1518] | 1157 | #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?); |
---|
[1882] | 1158 | >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl |
---|
[985] | 1159 | qed. |
---|
| 1160 | |
---|
| 1161 | definition address_of_word_labels ≝ |
---|
[1666] | 1162 | λpr: pseudo_assembly_program. |
---|
[985] | 1163 | λid: Identifier. |
---|
[1666] | 1164 | address_of_word_labels_code_mem (\snd pr) id. |
---|
[985] | 1165 | |
---|
[1541] | 1166 | definition construct_datalabels: preamble → ? ≝ |
---|
| 1167 | λthe_preamble: preamble. |
---|
| 1168 | \fst (foldl ((identifier_map ASMTag Word) × Word) ? ( |
---|
[985] | 1169 | λt. λpreamble. |
---|
| 1170 | let 〈datalabels, addr〉 ≝ t in |
---|
| 1171 | let 〈name, size〉 ≝ preamble in |
---|
[1541] | 1172 | let 〈carry, sum〉 ≝ half_add … addr size in |
---|
| 1173 | 〈add ? ? datalabels name addr, sum〉) |
---|
| 1174 | 〈empty_map …, zero 16〉 (\snd the_preamble)). |
---|