source: src/ASM/Status.ma @ 1522

Last change on this file since 1522 was 1522, checked in by mulligan, 10 years ago

changes to preamble and lin to asm pass, resolved conflict in interpret

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