source: src/ASM/Status.ma @ 2173

Last change on this file since 2173 was 2172, checked in by mulligan, 7 years ago

Moved new versions of get_ / set_arg_* into Status.ma. Commented out proofs that are no longer working.

File size: 40.2 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 
548
549definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝
550  λb: Byte.
551    let address ≝ nat_of_bitvector … b in
552      if (eqb address 128) then None ?
553      else if (eqb address 144) then Some … (inl … SFR_P1)
554      else if (eqb address 160) then None ?
555      else if (eqb address 176) then Some … (inl … SFR_P3)
556      else if (eqb address 153) then Some … (inl … SFR_SBUF)
557      else if (eqb address 138) then Some … (inl … SFR_TL0)
558      else if (eqb address 139) then Some … (inl … SFR_TL1)
559      else if (eqb address 140) then Some … (inl … SFR_TH0)
560      else if (eqb address 141) then Some … (inl … SFR_TH1)
561      else if (eqb address 200) then Some … (inr … SFR_T2CON)
562      else if (eqb address 202) then Some … (inr … SFR_RCAP2L)
563      else if (eqb address 203) then Some … (inr … SFR_RCAP2H)
564      else if (eqb address 204) then Some … (inr … SFR_TL2)
565      else if (eqb address 205) then Some … (inr … SFR_TH2)
566      else if (eqb address 135) then Some … (inl … SFR_PCON)
567      else if (eqb address 136) then Some … (inl … SFR_TCON)
568      else if (eqb address 137) then Some … (inl … SFR_TMOD)
569      else if (eqb address 152) then Some … (inl … SFR_SCON)
570      else if (eqb address 168) then Some … (inl … SFR_IE)
571      else if (eqb address 184) then Some … (inl … SFR_IP)
572      else if (eqb address 129) then Some … (inl … SFR_SP)
573      else if (eqb address 130) then Some … (inl … SFR_DPL)
574      else if (eqb address 131) then Some … (inl … SFR_DPH)
575      else if (eqb address 208) then Some … (inl … SFR_PSW)
576      else if (eqb address 224) then Some … (inl … SFR_ACC_A)
577      else if (eqb address 240) then Some … (inl … SFR_ACC_B)
578      else None ?.
579
580definition get_bit_addressable_sfr:
581    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝
582  λM: Type[0].
583  λcode_memory:M.
584  λs: PreStatus M code_memory.
585  λb: Byte.
586  λl: bool.
587  match sfr_of_Byte b with
588  [ None ⇒ match not_implemented in False with [ ]
589  | Some sfr8051_8052 ⇒
590    match sfr8051_8052 with
591    [ inl sfr ⇒
592      match sfr with
593      [ SFR_P1 ⇒
594        if l then
595          p1_latch … s
596        else
597          get_8051_sfr … s SFR_P1
598      | SFR_P3 ⇒
599        if l then
600          p3_latch … s
601        else
602          get_8051_sfr … s SFR_P3
603      | _ ⇒ get_8051_sfr … s sfr
604      ]
605    | inr sfr ⇒ get_8052_sfr M code_memory s sfr
606    ]
607  ].
608
609definition set_bit_addressable_sfr:
610    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → PreStatus M code_memory ≝
611  λM: Type[0].
612  λcode_memory:M.
613  λs: PreStatus M code_memory.
614  λb: Byte.
615  λv: Byte.
616   match sfr_of_Byte b with
617   [ None ⇒ match not_implemented in False with [ ]
618   | Some sfr8051_8052 ⇒
619      match sfr8051_8052 with
620      [ inl sfr ⇒
621         match sfr with
622         [ SFR_P1 ⇒
623           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
624           set_p1_latch ?? s v
625         | SFR_P3 ⇒
626           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
627           set_p3_latch ?? s v
628         | _ ⇒ set_8051_sfr ?? s sfr v ]
629      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]].
630
631lemma clock_set_bit_addressable_sfr:
632    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte.
633        clock … code_memory s = clock … code_memory (set_bit_addressable_sfr M code_memory s b v).
634  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
635  cases (sfr_of_Byte ?)
636  [1:
637    normalize nodelta cases not_implemented
638  |2:
639    * * normalize nodelta %
640  ]
641qed.
642
643lemma program_counter_set_bit_addressable_sfr:
644    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte.
645        program_counter … code_memory s = program_counter … code_memory (set_bit_addressable_sfr M code_memory s b v).
646  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
647  cases (sfr_of_Byte ?)
648  [1:
649    normalize nodelta cases not_implemented
650  |2:
651    * * %
652  ]
653qed.
654
655definition bit_address_of_register ≝
656  λM: Type[0].
657  λcode_memory:M.
658  λs: PreStatus M code_memory.
659  λr: BitVector 3.
660    let b ≝ get_index_v … r O ? in
661    let c ≝ get_index_v … r 1 ? in
662    let d ≝ get_index_v … r 2 ? in
663    let 〈 un, ln 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
664    let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in
665    let offset ≝
666      if ¬r1 ∧ ¬r0 then
667        O
668      else if ¬r1 ∧ r0 then
669        8
670      else if r1 ∧ r0 then
671        24
672      else
673        16
674    in
675      bitvector_of_nat 7 (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
676  [1,2,3,4,5:
677    normalize
678    repeat (@ le_S_S)
679    @ le_O_n;
680  ]
681qed.
682
683definition get_register ≝
684  λM: Type[0].
685  λcode_memory:M.
686  λs: PreStatus M code_memory.
687  λr: BitVector 3.
688    let address ≝ bit_address_of_register … s r in
689      lookup ?? address (low_internal_ram … s) (zero 8).
690     
691definition set_register ≝
692  λM: Type[0].
693  λcode_memory:M.
694  λs: PreStatus M code_memory.
695  λr: BitVector 3.
696  λv: Byte.
697    let address ≝ bit_address_of_register … s r in
698    let old_low_internal_ram ≝ low_internal_ram ?? s in
699    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
700      set_low_internal_ram … s new_low_internal_ram.
701     
702definition read_at_stack_pointer ≝
703  λM: Type[0].
704  λcode_memory:M.
705  λs: PreStatus M code_memory.
706    let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_SP) in
707    let m ≝ get_index_v ?? nu O ? in
708    let r1 ≝ get_index_v ?? nu 1 ? in
709    let r2 ≝ get_index_v ?? nu 2 ? in
710    let r3 ≝ get_index_v ?? nu 3 ? in
711    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
712    let memory ≝
713      if m then
714        (low_internal_ram ?? s)
715      else
716        (high_internal_ram ?? s)
717    in
718      lookup … address memory (zero 8).
719  [1,2,3,4:
720     normalize
721     repeat (@ le_S_S)
722     @ le_O_n
723  ]
724qed.
725
726definition write_at_stack_pointer ≝
727  λM: Type[0].
728  λcode_memory:M.
729  λs: PreStatus M code_memory.
730  λv: Byte.
731    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ?? s SFR_SP) in
732    let bit_zero ≝ get_index_v ?? nu O ? in
733    let bit_1 ≝ get_index_v ?? nu 1 ? in
734    let bit_2 ≝ get_index_v ?? nu 2 ? in
735    let bit_3 ≝ get_index_v ?? nu 3 ? in
736      if bit_zero then
737        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
738                              v (low_internal_ram ?? s) in
739          set_low_internal_ram ?? s memory
740      else
741        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
742                              v (high_internal_ram ?? s) in
743          set_high_internal_ram ?? s memory.
744  [1,2,3,4:
745     normalize
746     repeat (@ le_S_S)
747     @ le_O_n
748  ]
749qed.
750
751definition 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' ≝
752  λM,code_memory,s,v,a.
753   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M ? s = clock M ? s' with
754     [ DPTR ⇒ λ_:True.
755       let 〈 bu, bl 〉 ≝ vsplit … 8 8 v in
756       let status ≝ set_8051_sfr … s SFR_DPH bu in
757       let status ≝ set_8051_sfr … status SFR_DPL bl in
758         status
759     | _ ⇒ λK.
760       match K in False with
761       [
762       ]
763     ] (subaddressing_modein … a).
764 //
765qed.
766
767definition set_arg_16: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → PreStatus M code_memory ≝
768 set_arg_16'.
769
770lemma set_arg_16_ok: ∀M,cm,s,v,x. clock M cm s = clock M cm (set_arg_16 M cm s v x).
771 #M #cm #s #x #v whd in match set_arg_16; normalize nodelta @pi2
772qed.
773
774   
775definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ data16 ]] → Word ≝
776  λm, cm, s, a.
777    match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
778      [ DATA16 d ⇒ λ_:True. d
779      | _ ⇒ λK.
780        match K in False with
781        [
782        ]
783      ] (subaddressing_modein … a).
784     
785definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ;
786                                          acc_a ; acc_b ; data ; acc_dptr ;
787                                          acc_pc ; ext_indirect ;
788                                          ext_indirect_dptr ]] → Byte ≝
789  λm, cm, s, l, a.
790    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
791                                                acc_a ; acc_b ; data ; acc_dptr ;
792                                                acc_pc ; ext_indirect ;
793                                                ext_indirect_dptr ]] x) → ? with
794      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
795      | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
796      | DATA d ⇒ λdata: True. d
797      | REGISTER r ⇒ λregister: True. get_register ?? s r
798      | EXT_INDIRECT_DPTR ⇒
799        λext_indirect_dptr: True.
800          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
801            lookup ? 16 address (external_ram ?? s) (zero 8)
802      | EXT_INDIRECT e ⇒
803        λext_indirect: True.
804          let address ≝ get_register ?? s [[ false; false; e ]]  in
805          let padded_address ≝ pad 8 8 address in
806            lookup ? 16 padded_address (external_ram ?? s) (zero 8)
807      | ACC_DPTR ⇒
808        λacc_dptr: True.
809          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
810          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
811          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
812            lookup ? 16 address (external_ram ?? s) (zero 8)
813      | ACC_PC ⇒
814        λacc_pc: True.
815          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
816          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
817            lookup ? 16 address (external_ram ?? s) (zero 8)
818      | DIRECT d ⇒
819        λdirect: True.
820          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
821            match head' … hd with
822            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
823            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
824            ]
825      | INDIRECT i ⇒
826        λindirect: True.
827          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
828            match head' … hd with
829            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)
830            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
831            ]
832      | _ ⇒ λother.
833        match other in False with [ ]
834      ] (subaddressing_modein … a).
835
836definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
837                                   acc_a ; acc_b ; ext_indirect ;
838                                   ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝
839  λm, cm, s, a, v.
840    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
841                                                acc_a ; acc_b ; ext_indirect ;
842                                                ext_indirect_dptr ]] x) →
843                   PreStatus m cm
844            with
845      [ DIRECT d ⇒
846        λdirect: True.
847          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
848            match head' … bit_one with
849              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
850              | false ⇒
851                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
852                  set_low_internal_ram ?? s memory
853              ]
854      | INDIRECT i ⇒
855        λindirect: True.
856          let register ≝ get_register ?? s [[ false; false; i ]] in
857          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
858            match head' … bit_one with
859              [ false ⇒
860                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
861                  set_low_internal_ram ?? s memory
862              | true ⇒
863                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
864                  set_high_internal_ram ?? s memory
865              ]
866      | REGISTER r ⇒ λregister: True. set_register ?? s r v
867      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
868      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
869      | EXT_INDIRECT e ⇒
870        λext_indirect: True.
871          let address ≝ get_register ?? s [[ false; false; e ]] in
872          let padded_address ≝ pad 8 8 address in
873          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
874            set_external_ram ?? s memory
875      | EXT_INDIRECT_DPTR ⇒
876        λext_indirect_dptr: True.
877          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
878          let memory ≝ insert ? 16 address v (external_ram ?? s) in
879            set_external_ram ?? s memory
880      | _ ⇒
881        λother: False.
882          match other in False with [ ]
883      ] (subaddressing_modein … a).
884
885lemma clock_set_arg_8: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v).
886  cases daemon
887qed.
888
889lemma program_counter_set_arg_8: ∀M,cm,s,x,v. program_counter M cm s = program_counter … (set_arg_8 M cm s x v).
890  cases daemon
891qed.
892
893lemma p1_latch_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. p1_latch M cm s = p1_latch … (set_arg_8 M cm s x v).
894  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
895  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
896  cases daemon
897qed.
898
899lemma p3_latch_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. p3_latch M cm s = p3_latch … (set_arg_8 M cm s x v).
900  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
901  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
902  cases daemon
903qed.
904
905lemma special_function_registers_8052_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. special_function_registers_8052 M cm s = special_function_registers_8052 … (set_arg_8 M cm s x v).
906  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
907  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
908  cases daemon
909qed.
910
911theorem modulus_less_than:
912  ∀m,n: nat. (m mod (S n)) < S n.
913  #n #m
914  normalize
915  @ le_S_S
916  lapply (le_n n)
917  generalize in ⊢ (?%? → ?(??%?)?);
918  elim n in ⊢ (∀_:?. ??% → ?(?%??)?);
919  [ normalize
920    #n
921    @ (less_than_or_equal_b_elim n m)
922    normalize
923    [ //
924    | #H #K
925      @(le_inv_ind ?? K …)
926      [ # H1
927        < H1
928        //
929      | #x #H1 #H2 #H3
930        destruct
931      ]
932    ]
933  | normalize
934    # y # H1 # n # H2
935    @ (less_than_or_equal_b_elim n m)
936    normalize
937    [ //
938    | # K
939      @ H1
940      cut (n ≤ S y → n - S m ≤ y)
941      /2 by/
942      cases n
943      normalize
944      //
945      # x # K1
946      lapply (le_S_S_to_le … K1)
947      generalize in match m;
948      elim x
949      normalize
950      //
951      # w1 # H # m
952      cases m
953      normalize
954      //
955      # q # K2
956      @H
957      /3/
958    ]
959  ]
960qed.
961
962definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] →
963                       bool → bool ≝
964  λm, cm, s, a, l.
965    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
966                                                 n_bit_addr ;
967                                                 carry ]] x) → ? with
968      [ BIT_ADDR b ⇒
969        λbit_addr: True.
970        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
971        match head' … bit_1 with
972        [ true ⇒
973          let address ≝ nat_of_bitvector … seven_bits in
974          let d ≝ address ÷ 8 in
975          let m ≝ address mod 8 in
976          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
977          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
978            get_index_v … sfr m ?
979        | false ⇒
980          let address ≝ nat_of_bitvector … seven_bits in
981          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
982          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
983            get_index_v … t (modulus address 8) ?
984        ]
985      | N_BIT_ADDR n ⇒
986        λn_bit_addr: True.
987        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
988        match head' … bit_1 with
989        [ true ⇒
990          let address ≝ nat_of_bitvector … seven_bits in
991          let d ≝ address ÷ 8 in
992          let m ≝ address mod 8 in
993          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
994          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
995            ¬(get_index_v … sfr m ?)
996        | false ⇒
997          let address ≝ nat_of_bitvector … seven_bits in
998          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
999          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1000            ¬(get_index_v … t (modulus address 8) ?)
1001        ]
1002      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
1003      | _ ⇒ λother.
1004        match other in False with [ ]
1005      ] (subaddressing_modein … a).
1006      @modulus_less_than
1007qed.
1008     
1009definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝
1010  λm: Type[0].
1011  λcm.
1012  λs: PreStatus m cm.
1013  λa: [[bit_addr; carry]].
1014  λv: Bit.
1015    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ? with
1016      [ BIT_ADDR b ⇒ λbit_addr: True.
1017        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1018        match head' … bit_1 with
1019        [ true ⇒
1020          let address ≝ nat_of_bitvector … seven_bits in
1021          let d ≝ address ÷ 8 in
1022          let m ≝ address mod 8 in
1023          let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1024          let sfr ≝ get_bit_addressable_sfr … s t true in
1025          let new_sfr ≝ set_index … sfr m v ? in
1026            set_bit_addressable_sfr … s new_sfr t
1027        | false ⇒
1028          let address ≝ nat_of_bitvector … seven_bits in
1029          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1030          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1031          let n_bit ≝ set_index … t (modulus address 8) v ? in
1032          let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1033            set_low_internal_ram … s memory
1034        ]
1035      | CARRY ⇒
1036        λcarry: True.
1037        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1038        let new_psw ≝ v:::seven_bits in
1039          set_8051_sfr ?? s SFR_PSW new_psw
1040      | _ ⇒
1041        λother: False.
1042          match other in False with
1043            [ ]
1044      ] (subaddressing_modein … a).
1045  @modulus_less_than
1046qed.
1047
1048lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v).
1049  cases daemon
1050qed.
1051
1052definition fetch_pseudo_instruction:
1053 ∀code_mem:list labelled_instruction. ∀pc:Word.
1054  nat_of_bitvector … pc < |code_mem| → (pseudo_instruction × Word) ≝
1055  λcode_mem.
1056  λpc: Word.
1057  λpc_ok.
1058    let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? pc) … code_mem pc_ok in
1059    let new_pc ≝ add ? pc (bitvector_of_nat … 1) in
1060      〈instr, new_pc〉.
1061
1062lemma snd_fetch_pseudo_instruction:
1063 ∀l,ppc,ppc_ok. \snd (fetch_pseudo_instruction l ppc ppc_ok) = add ? ppc (bitvector_of_nat ? 1).
1064 #l #ppc #ppc_ok whd in ⊢ (??(???%)?); @pair_elim
1065 #lft #rgt #_ %
1066qed.
1067
1068lemma fetch_pseudo_instruction_vsplit:
1069 ∀instr_list,ppc,ppc_ok.
1070  ∃pre,suff,lbl.
1071   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
1072#instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
1073cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
1074lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
1075#EQ %{lbl0} @EQ
1076qed.
1077
1078lemma fetch_pseudo_instruction_append:
1079 ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.
1080  let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
1081  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
1082  〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
1083 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
1084 cut (|l1| + nat_of_bitvector … ppc < 2^16)
1085 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
1086 -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
1087 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
1088 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ]
1089 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
1090 #lbl #instr normalize nodelta >add_associative %
1091qed.
1092
1093definition is_well_labelled_p ≝
1094  λinstr_list.
1095  ∀id: Identifier.
1096  ∀ppc.
1097  ∀ppc_ok.
1098  ∀i.
1099    \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) = i →
1100      instruction_has_label id i →
1101        occurs_exactly_once ASMTag pseudo_instruction id instr_list.
1102
1103definition address_of_word_labels_code_mem ≝
1104  λcode_mem : list labelled_instruction.
1105  λid: Identifier.
1106    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
1107
1108lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
1109 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
1110  address_of_word_labels_code_mem instr_list id =
1111  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
1112 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
1113 >(index_of_internal_None ?????? H) %
1114qed.
1115
1116lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
1117 eq_identifier ? id' id = false →
1118  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
1119   address_of_word_labels_code_mem instr_list id =
1120   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
1121 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
1122 >(index_of_internal_Some_miss ???????? H) [ @refl | // ]
1123qed.
1124
1125lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
1126  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
1127   address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
1128   = bitvector_of_nat … (|instr_list|).
1129 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
1130 >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl
1131qed.
1132
1133definition address_of_word_labels ≝
1134  λpr: pseudo_assembly_program.
1135  λid: Identifier.
1136    address_of_word_labels_code_mem (\snd pr) id.
1137
1138definition construct_datalabels: preamble → ? ≝
1139  λthe_preamble: preamble.
1140    \fst (foldl ((identifier_map ASMTag Word) × Word) ? (
1141    λt. λpreamble.
1142      let 〈datalabels, addr〉 ≝ t in
1143      let 〈name, size〉 ≝ preamble in
1144      let 〈carry, sum〉 ≝ half_add … addr size in
1145        〈add ? ? datalabels name addr, sum〉)
1146          〈empty_map …, zero 16〉 (\snd the_preamble)).
Note: See TracBrowser for help on using the repository browser.