source: src/ASM/Status.ma @ 1939

Last change on this file since 1939 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 40.3 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Interpret.ma: Operational semantics for the 8051/8052 processor.           *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5include "ASM/ASM.ma".
6include "ASM/Arithmetic.ma".
7include "ASM/BitVectorTrie.ma".
8include "basics/russell.ma".
9
10definition Time ≝ nat.
11
12inductive SerialBufferType: Type[0] ≝
13  Eight: Byte → SerialBufferType
14| Nine: Bit → Byte → SerialBufferType.
15
16inductive LineType: Type[0] ≝
17  P1: Byte → LineType
18| P3: Byte → LineType
19| SerialBuffer: SerialBufferType → LineType.
20
21(* What is a continuation, now? *)
22
23inductive 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
44definition 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     
68inductive SFR8052: Type[0] ≝
69   SFR_T2CON: SFR8052
70|  SFR_RCAP2L: SFR8052
71|  SFR_RCAP2H: SFR8052
72|  SFR_TL2: SFR8052
73|  SFR_TH2: SFR8052.
74
75definition 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(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
88record PreStatus (M: Type[0]) (code_memory: M) : Type[0] ≝
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
105definition Status ≝ PreStatus (BitVectorTrie Byte 16).
106definition PseudoStatus ≝ PreStatus (pseudo_assembly_program).
107
108lemma 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
116qed.
117   
118lemma 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
126qed.
127   
128definition set_clock ≝
129  λM: Type[0].
130  λcode_memory:M.
131  λs: PreStatus M code_memory.
132  λt: Time.
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
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   
152definition set_p1_latch ≝
153  λM: Type[0].
154  λcode_memory:M.
155  λs: PreStatus M code_memory.
156  λb: Byte.
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
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
176definition set_p3_latch ≝
177  λM: Type[0].
178  λcode_memory:M.
179  λs: PreStatus M code_memory.
180  λb: Byte.
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
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
200definition get_8051_sfr ≝
201  λM: Type[0].
202  λcode_memory:M.
203  λs: PreStatus M code_memory.
204  λi: SFR8051.
205    let sfr ≝ special_function_registers_8051 ?? s in
206    let index ≝ sfr_8051_index i in
207      get_index_v … sfr index ?.
208    @ sfr8051_index_19
209qed.
210
211definition get_8052_sfr ≝
212  λM: Type[0].
213  λcode_memory:M.
214  λs: PreStatus M code_memory.
215  λi: SFR8052.
216    let sfr ≝ special_function_registers_8052 ?? s in
217    let index ≝ sfr_8052_index i in
218      get_index_v … sfr index ?.
219    @ sfr8052_index_5
220qed.
221
222definition set_8051_sfr ≝
223  λM: Type[0].
224  λcode_memory:M.
225  λs: PreStatus M code_memory.
226  λi: SFR8051.
227  λb: Byte.
228    let index ≝ sfr_8051_index i in
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
235    let new_special_function_registers_8051 ≝
236      set_index Byte 19 old_special_function_registers_8051 index b ? in
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
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)
251qed.
252
253definition set_8052_sfr ≝
254  λM: Type[0].
255  λcode_memory:M.
256  λs: PreStatus M code_memory.
257  λi: SFR8052.
258  λb: Byte.
259    let index ≝ sfr_8052_index i in
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
266    let new_special_function_registers_8052 ≝
267      set_index Byte 5 old_special_function_registers_8052 index b ? in
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
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)
282qed.
283
284definition set_program_counter ≝
285  λM: Type[0].
286  λcode_memory:M.
287  λs: PreStatus M code_memory.
288  λw: Word.
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
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               
308definition set_code_memory ≝
309  λM,M': Type[0].
310  λcode_memory:M.
311  λs: PreStatus M code_memory.
312  λr: M'.
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
322      mk_PreStatus M' r
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               
333definition set_low_internal_ram ≝
334  λM: Type[0].
335  λcode_memory:M.
336  λs: PreStatus M code_memory.
337  λr: BitVectorTrie Byte 7.
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
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               
357definition set_high_internal_ram ≝
358  λM: Type[0].
359  λcode_memory:M.
360  λs: PreStatus M code_memory.
361  λr: BitVectorTrie Byte 7.
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
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               
382definition set_external_ram ≝
383  λM: Type[0].
384  λcode_memory:M.
385  λs: PreStatus M code_memory.
386  λr: BitVectorTrie Byte 16.
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
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               
406definition get_cy_flag ≝
407  λM: Type[0].
408  λcode_memory:M.
409  λs: PreStatus M code_memory.
410    let sfr ≝ special_function_registers_8051 ?? s in
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    ]
419qed.
420
421definition get_ac_flag ≝
422  λM: Type[0].
423  λcode_memory:M.
424  λs: PreStatus M code_memory.
425    let sfr ≝ special_function_registers_8051 ?? s in
426    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
427      get_index_v bool 8 psw 1 ?.
428    normalize
429    repeat (@ (le_S_S ? ?))
430    @ le_O_n
431qed.
432
433definition get_fo_flag ≝
434  λM: Type[0].
435  λcode_memory:M.
436  λs: PreStatus M code_memory.
437    let sfr ≝ special_function_registers_8051 ?? s in
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
443qed.
444
445definition get_rs1_flag ≝
446  λM: Type[0].
447  λcode_memory:M.
448  λs: PreStatus M code_memory.
449    let sfr ≝ special_function_registers_8051 ?? s in
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
455qed.
456
457definition get_rs0_flag ≝
458  λM: Type[0].
459  λcode_memory:M.
460  λs: PreStatus M code_memory.
461    let sfr ≝ special_function_registers_8051 ?? s in
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
467qed.
468
469definition get_ov_flag ≝
470  λM: Type[0].
471  λcode_memory:M.
472  λs: PreStatus M code_memory.
473    let sfr ≝ special_function_registers_8051 ?? s in
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
479qed.
480
481definition get_ud_flag ≝
482  λM: Type[0].
483  λcode_memory:M.
484  λs: PreStatus M code_memory.
485    let sfr ≝ special_function_registers_8051 ?? s in
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
491qed.
492
493definition get_p_flag ≝
494  λM: Type[0].
495  λcode_memory:M.
496  λs: PreStatus M code_memory.
497    let sfr ≝ special_function_registers_8051 ?? s in
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
503qed.
504
505definition set_flags ≝
506  λM: Type[0].
507  λcode_memory:M.
508  λs: PreStatus M code_memory.
509  λcy: Bit.
510  λac: option Bit.
511  λov: Bit.
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
521    let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
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 ]].
525    [1,2,3,4,5,6,7,8:
526       normalize
527       repeat (@ le_S_S)
528       @ le_O_n
529    ]
530qed.
531
532definition initialise_status ≝
533  λM: Type[0].
534  λcode_mem: M.
535  let status ≝ mk_PreStatus M code_mem                    (* Code mem. *)
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
546    set_8051_sfr ?? status SFR_SP (bitvector_of_nat 8 7).
547 
548definition get_bit_addressable_sfr ≝
549  λM: Type[0].
550  λcode_memory:M.
551  λs: PreStatus M code_memory.
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
560          (p1_latch ?? s)
561        else
562          (get_8051_sfr ?? s SFR_P1)
563      else if (eqb address 160) then
564        ?
565      else if (eqb address 176) then
566        if l then
567          (p3_latch ?? s)
568        else
569          (get_8051_sfr ?? s SFR_P3)
570      else if (eqb address 153) then
571        get_8051_sfr ?? s SFR_SBUF
572      else if (eqb address 138) then
573        get_8051_sfr ?? s SFR_TL0
574      else if (eqb address 139) then
575        get_8051_sfr ?? s SFR_TL1
576      else if (eqb address 140) then
577        get_8051_sfr ?? s SFR_TH0
578      else if (eqb address 141) then
579        get_8051_sfr ?? s SFR_TH1
580      else if (eqb address 200) then
581        get_8052_sfr ?? s SFR_T2CON
582      else if (eqb address 202) then
583        get_8052_sfr ?? s SFR_RCAP2L
584      else if (eqb address 203) then
585        get_8052_sfr ?? s SFR_RCAP2H
586      else if (eqb address 204) then
587        get_8052_sfr ?? s SFR_TL2
588      else if (eqb address 205) then
589        get_8052_sfr ?? s SFR_TH2
590      else if (eqb address 135) then
591        get_8051_sfr ?? s SFR_PCON
592      else if (eqb address 136) then
593        get_8051_sfr ?? s SFR_TCON
594      else if (eqb address 137) then
595        get_8051_sfr ?? s SFR_TMOD
596      else if (eqb address 152) then
597        get_8051_sfr ?? s SFR_SCON
598      else if (eqb address 168) then
599        get_8051_sfr ?? s SFR_IE
600      else if (eqb address 184) then
601        get_8051_sfr ?? s SFR_IP
602      else if (eqb address 129) then
603        get_8051_sfr ?? s SFR_SP
604      else if (eqb address 130) then
605        get_8051_sfr ?? s SFR_DPL
606      else if (eqb address 131) then
607        get_8051_sfr ?? s SFR_DPH
608      else if (eqb address 208) then
609        get_8051_sfr ?? s SFR_PSW
610      else if (eqb address 224) then
611        get_8051_sfr ?? s SFR_ACC_A
612      else if (eqb address 240) then
613        get_8051_sfr ?? s SFR_ACC_B
614      else
615        ?.
616      cases not_implemented
617qed.
618
619definition set_bit_addressable_sfr ≝
620  λM: Type[0].
621  λcode_memory:M.
622  λs: PreStatus M code_memory.
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
629        let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
630        let status_2 ≝ set_p1_latch ?? s v in
631          status_2
632      else if (eqb address 160) then
633        ?
634      else if (eqb address 176) then
635        let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
636        let status_2 ≝ set_p3_latch ?? s v in
637          status_2
638      else if (eqb address 153) then
639        set_8051_sfr ?? s SFR_SBUF v
640      else if (eqb address 138) then
641        set_8051_sfr ?? s SFR_TL0 v
642      else if (eqb address 139) then
643        set_8051_sfr ?? s SFR_TL1 v
644      else if (eqb address 140) then
645        set_8051_sfr ?? s SFR_TH0 v
646      else if (eqb address 141) then
647        set_8051_sfr ?? s SFR_TH1 v
648      else if (eqb address 200) then
649        set_8052_sfr ?? s SFR_T2CON v
650      else if (eqb address 202) then
651        set_8052_sfr ?? s SFR_RCAP2L v
652      else if (eqb address 203) then
653        set_8052_sfr ?? s SFR_RCAP2H v
654      else if (eqb address 204) then
655        set_8052_sfr ?? s SFR_TL2 v
656      else if (eqb address 205) then
657        set_8052_sfr ?? s SFR_TH2 v
658      else if (eqb address 135) then
659        set_8051_sfr ?? s SFR_PCON v
660      else if (eqb address 136) then
661        set_8051_sfr ?? s SFR_TCON v
662      else if (eqb address 137) then
663        set_8051_sfr ?? s SFR_TMOD v
664      else if (eqb address 152) then
665        set_8051_sfr ?? s SFR_SCON v
666      else if (eqb address 168) then
667        set_8051_sfr ?? s SFR_IE v
668      else if (eqb address 184) then
669        set_8051_sfr ?? s SFR_IP v
670      else if (eqb address 129) then
671        set_8051_sfr ?? s SFR_SP v
672      else if (eqb address 130) then
673        set_8051_sfr ?? s SFR_DPL v
674      else if (eqb address 131) then
675        set_8051_sfr ?? s SFR_DPH v
676      else if (eqb address 208) then
677        set_8051_sfr ?? s SFR_PSW v
678      else if (eqb address 224) then
679        set_8051_sfr ?? s SFR_ACC_A v
680      else if (eqb address 240) then
681        set_8051_sfr ?? s SFR_ACC_B v
682      else
683        ?.
684      cases not_implemented
685qed.
686
687definition bit_address_of_register ≝
688  λM: Type[0].
689  λcode_memory:M.
690  λs: PreStatus M code_memory.
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
695    let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
696    let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in
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  ]
713qed.
714
715definition get_register ≝
716  λM: Type[0].
717  λcode_memory:M.
718  λs: PreStatus M code_memory.
719  λr: BitVector 3.
720    let address ≝ bit_address_of_register … s r in
721      lookup ?? address (low_internal_ram … s) (zero 8).
722     
723definition set_register ≝
724  λM: Type[0].
725  λcode_memory:M.
726  λs: PreStatus M code_memory.
727  λr: BitVector 3.
728  λv: Byte.
729    let address ≝ bit_address_of_register … s r in
730    let old_low_internal_ram ≝ low_internal_ram ?? s in
731    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
732      set_low_internal_ram … s new_low_internal_ram.
733     
734definition read_at_stack_pointer ≝
735  λM: Type[0].
736  λcode_memory:M.
737  λs: PreStatus M code_memory.
738    let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_SP) in
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
743    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
744    let memory ≝
745      if m then
746        (low_internal_ram ?? s)
747      else
748        (high_internal_ram ?? s)
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  ]
756qed.
757
758definition write_at_stack_pointer ≝
759  λM: Type[0].
760  λcode_memory:M.
761  λs: PreStatus M code_memory.
762  λv: Byte.
763    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ?? s SFR_SP) in
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
768      if bit_zero then
769        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
770                              v (low_internal_ram ?? s) in
771          set_low_internal_ram ?? s memory
772      else
773        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
774                              v (high_internal_ram ?? s) in
775          set_high_internal_ram ?? s memory.
776  [1,2,3,4:
777     normalize
778     repeat (@ le_S_S)
779     @ le_O_n
780  ]
781qed.
782
783definition 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
786     [ DPTR ⇒ λ_:True.
787       let 〈 bu, bl 〉 ≝ split … 8 8 v in
788       let status ≝ set_8051_sfr … s SFR_DPH bu in
789       let status ≝ set_8051_sfr … status SFR_DPL bl in
790         status
791     | _ ⇒ λK.
792       match K in False with
793       [
794       ]
795     ] (subaddressing_modein … a).
796 //
797qed.
798
799definition set_arg_16: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → PreStatus M code_memory ≝
800 set_arg_16'.
801
802lemma 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
804qed.
805
806   
807definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ data16 ]] → Word ≝
808  λm, cm, s, a.
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     
817definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ;
818                                          acc_a ; acc_b ; data ; acc_dptr ;
819                                          acc_pc ; ext_indirect ;
820                                          ext_indirect_dptr ]] → Byte ≝
821  λm, cm, s, l, a.
822    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
823                                                acc_a ; acc_b ; data ; acc_dptr ;
824                                                acc_pc ; ext_indirect ;
825                                                ext_indirect_dptr ]] x) → ? with
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
828      | DATA d ⇒ λdata: True. d
829      | REGISTER r ⇒ λregister: True. get_register ?? s r
830      | EXT_INDIRECT_DPTR ⇒
831        λext_indirect_dptr: True.
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)
834      | EXT_INDIRECT e ⇒
835        λext_indirect: True.
836          let address ≝ get_register ?? s [[ false; false; e ]]  in
837          let padded_address ≝ pad 8 8 address in
838            lookup ? 16 padded_address (external_ram ?? s) (zero 8)
839      | ACC_DPTR ⇒
840        λacc_dptr: True.
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
843          let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in
844            lookup ? 16 address (external_ram ?? s) (zero 8)
845      | ACC_PC ⇒
846        λacc_pc: True.
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)
850      | DIRECT d ⇒
851        λdirect: True.
852          let 〈 nu, nl 〉 ≝ split ? 4 4 d in
853          let bit_one ≝ get_index_v ? ? nu 0 ? in
854          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
855            match bit_one with
856              [ false ⇒
857                  let address ≝ three_bits @@ nl in
858                    lookup ? 7 address (low_internal_ram ?? s) (zero 8)
859              | true ⇒ get_bit_addressable_sfr ?? s 8 d l
860              ]
861      | INDIRECT i ⇒
862        λindirect: True.
863          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ?? s [[ false; false; i]]) in
864          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
865          let bit_1 ≝ get_index_v ?? bit_one_v O ? in
866          match  bit_1 with
867            [ false ⇒
868                lookup ? 7 (three_bits @@ nl) (low_internal_ram ?? s) (zero 8)
869            | true ⇒
870                lookup ? 7 (three_bits @@ nl) (high_internal_ram ?? s) (zero 8)
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  ]
880qed.
881
882axiom clock_set_bit_addressable_sfr: ∀m,cm,s,d,v. clock m cm s = clock … (set_bit_addressable_sfr … s d v).
883
884definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ;
885                                   acc_a ; acc_b ; ext_indirect ;
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.
889    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
890                                                acc_a ; acc_b ; ext_indirect ;
891                                                ext_indirect_dptr ]] x) →
892                   Σs':PreStatus m cm. clock m cm s = clock m cm s'
893                   (*CSC: bug here if one specified the two clock above*)
894            with
895      [ DIRECT d ⇒
896        λdirect: True.
897          let 〈 nu, nl 〉 ≝ split … 4 4 d in
898          let bit_one ≝ get_index_v ? ? nu 0 ? in
899          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
900            match bit_one with
901              [ true ⇒ set_bit_addressable_sfr ?? s d v
902              | false ⇒
903                let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in
904                  set_low_internal_ram ?? s memory
905              ]
906      | INDIRECT i ⇒
907        λindirect: True.
908          let register ≝ get_register ?? s [[ false; false; i ]] in
909          let 〈nu, nl〉 ≝ split ? 4 4 register in
910          let bit_1 ≝ get_index_v … nu 0 ? in
911          let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
912            match bit_1 with
913              [ false ⇒
914                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in
915                  set_low_internal_ram ?? s memory
916              | true ⇒
917                let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in
918                  set_high_internal_ram ?? s memory
919              ]
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
923      | EXT_INDIRECT e ⇒
924        λext_indirect: True.
925          let address ≝ get_register ?? s [[ false; false; e ]] in
926          let padded_address ≝ pad 8 8 address in
927          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
928            set_external_ram ?? s memory
929      | EXT_INDIRECT_DPTR ⇒
930        λext_indirect_dptr: True.
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
934      | _ ⇒
935        λother: False.
936          match other in False with [ ]
937      ] (subaddressing_modein … a).
938// qed.
939
940definition 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 ≝
941 set_arg_8'.
942
943lemma 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
945qed.
946
947theorem 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)
953  generalize in ⊢ (?%? → ?(??%?)?);
954  elim n in ⊢ (∀_:?. ??% → ?(?%??)?);
955  [ normalize
956    #n
957    @ (less_than_or_equal_b_elim n m)
958    normalize
959    [ //
960    | #H #K
961      @(le_inv_ind ?? K …)
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)
977      /2 by/
978      cases n
979      normalize
980      //
981      # x # K1
982      lapply (le_S_S_to_le … K1)
983      generalize in match m;
984      elim x
985      normalize
986      //
987      # w1 # H # m
988      cases m
989      normalize
990      //
991      # q # K2
992      @H
993      /3/
994    ]
995  ]
996qed.
997
998definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] →
999                       bool → bool ≝
1000  λm, cm, s, a, l.
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.
1006          let 〈 nu, nl 〉 ≝ split … 4 4 b in
1007          let bit_1 ≝ get_index_v ? ? nu 0 ? in
1008          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
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
1015                let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in
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
1020                let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1021                  get_index_v … t (modulus address 8) ?
1022              ]
1023      | N_BIT_ADDR n ⇒
1024        λn_bit_addr: True.
1025          let 〈 nu, nl 〉 ≝ split … 4 4 n in
1026          let bit_1 ≝ get_index_v ? ? nu 0 ? in
1027          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
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
1034                let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in
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
1039                let trans ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1040                  ¬(get_index_v … trans (modulus address 8) ?)
1041              ]
1042      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
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:
1051         @modulus_less_than
1052      ]
1053qed.
1054     
1055definition 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' ≝
1056  λm: Type[0].
1057  λcm.
1058  λs: PreStatus m cm.
1059  λa: [[bit_addr; carry]].
1060  λv: Bit.
1061    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with
1062      [ BIT_ADDR b ⇒ λbit_addr: True.
1063        let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
1064        let bit_1 ≝ get_index_v ?? nu 0 ? in
1065        let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
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
1072            let sfr ≝ get_bit_addressable_sfr ?? s ? t true in
1073            let new_sfr ≝ set_index … sfr m v ? in
1074              set_bit_addressable_sfr ?? s new_sfr t
1075          | false ⇒
1076            let address ≝ nat_of_bitvector … (three_bits @@ nl) in
1077            let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1078            let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1079            let n_bit ≝ set_index … t (modulus address 8) v ? in
1080            let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1081              set_low_internal_ram ?? s memory
1082          ]
1083      | CARRY ⇒
1084        λcarry: True.
1085        let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
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
1090          set_8051_sfr ?? s SFR_PSW new_psw
1091      | _ ⇒
1092        λother: False.
1093          match other in False with
1094            [ ]
1095      ] (subaddressing_modein … a).
1096try (repeat @le_S_S @le_O_n)
1097/by/
1098qed.
1099
1100definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝ set_arg_1'.
1101
1102lemma 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
1104qed.
1105
1106definition load_code_memory ≝
1107 fold_left_i … (
1108   λi, mem, v.
1109     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
1110
1111definition load ≝
1112 λl,cm.
1113 λstatus.
1114   set_code_memory (BitVectorTrie Word 16) ? cm status (load_code_memory l).
1115
1116definition 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
1120    let 〈flags, new_pc〉 ≝ half_add ? pc (bitvector_of_nat ? 1) in
1121      〈instr, new_pc〉.
1122    cases not_implemented.
1123qed.
1124
1125lemma snd_fetch_pseudo_instruction:
1126 ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = \snd (half_add ? ppc (bitvector_of_nat ? 1)).
1127 #l #ppc whd in ⊢ (??(???%)?); @pair_elim
1128 #lft #rgt @pair_elim #x #y #_ #_ %
1129qed.
1130
1131definition address_of_word_labels_code_mem ≝
1132  λcode_mem : list labelled_instruction.
1133  λid: Identifier.
1134    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
1135
1136lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
1137 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
1138  address_of_word_labels_code_mem instr_list id =
1139  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
1140 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
1141 >(index_of_internal_None ?????? H) %
1142qed.
1143
1144lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
1145 eq_identifier ? id' id = false →
1146  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
1147   address_of_word_labels_code_mem instr_list id =
1148   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
1149 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
1150 >(index_of_internal_Some_miss ???????? H) [ @refl | // ]
1151qed.
1152
1153lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
1154  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
1155   address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
1156   = bitvector_of_nat … (|instr_list|).
1157 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
1158 >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl
1159qed.
1160
1161definition address_of_word_labels ≝
1162  λpr: pseudo_assembly_program.
1163  λid: Identifier.
1164    address_of_word_labels_code_mem (\snd pr) id.
1165
1166definition construct_datalabels: preamble → ? ≝
1167  λthe_preamble: preamble.
1168    \fst (foldl ((identifier_map ASMTag Word) × Word) ? (
1169    λt. λpreamble.
1170      let 〈datalabels, addr〉 ≝ t in
1171      let 〈name, size〉 ≝ preamble in
1172      let 〈carry, sum〉 ≝ half_add … addr size in
1173        〈add ? ? datalabels name addr, sum〉)
1174          〈empty_map …, zero 16〉 (\snd the_preamble)).
Note: See TracBrowser for help on using the repository browser.