source: Deliverables/D3.3/id-lookup-branch/ASM/Status.ma @ 3033

Last change on this file since 3033 was 993, checked in by sacerdot, 9 years ago

More Russell everywhere; getting closer to the goal.

File size: 43.1 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      inversion 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/
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      apply 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         apply 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_bv ? 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_bv ? 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_bv ??? then ? else ?) then ? else ? = ?)
1129    >eq_bv_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_bv ? id' id ∨ occurs_exactly_once id prefix.
1154 #id #id' #i #prefix elim prefix
1155  [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
1156    change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/
1157  | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
1158    cases he; normalize nodelta
1159     [ #H @ (IH H)
1160     | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
1161       change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv ???) normalize nodelta;
1162       [generalize in match (refl … (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
1163        /2/ #H >does_not_occur_Some //
1164       | #H @IH @H]]]
1165qed.
1166
1167let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
1168  match l with
1169  [ nil ⇒ ?
1170  | cons hd tl ⇒
1171    if pred hd then
1172      acc
1173    else
1174      index_of_internal A pred tl (S acc)
1175  ].
1176  cases not_implemented.
1177qed.
1178
1179
1180definition index_of ≝
1181  λA.
1182  λeq.
1183  λl.
1184    index_of_internal A eq l 0.
1185
1186lemma index_of_internal_None: ∀i,id,instr_list,n.
1187 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
1188  index_of_internal ? (instruction_matches_identifier id) instr_list n =
1189   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
1190 #i #id #instr_list elim instr_list
1191  [ #n #abs whd in abs; cases abs
1192  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
1193    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
1194    [ #H %
1195    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
1196      [ #_ % | #abs cases abs ]]]
1197qed.
1198
1199lemma index_of_internal_Some_miss: ∀i,id,id'.
1200 eq_bv ? id' id = false →
1201 ∀instr_list,n.
1202 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
1203  index_of_internal ? (instruction_matches_identifier id) instr_list n =
1204   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.
1205 #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ
1206 change with (occurs_exactly_once ?? → ?) generalize in match n; -n H; elim instr_list
1207  [ #n #abs cases abs
1208  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
1209    [ // | #K @IH //]]
1210qed.
1211
1212lemma index_of_internal_Some_hit: ∀i,id.
1213 ∀instr_list,n.
1214  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
1215   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n
1216  = |instr_list| + n.
1217 #i #id #instr_list elim instr_list
1218  [ #n #_ whd in ⊢ (??%%) change with (if eq_bv … id id then ? else ? = ?) >eq_bv_refl %
1219  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
1220    [ >does_not_occur_absurd #abs cases abs | #H applyS (IH (S n)) //]]
1221qed.
1222
1223definition address_of_word_labels_code_mem ≝
1224  λcode_mem.
1225  λid: Identifier.
1226    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem).
1227
1228lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
1229 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
1230  address_of_word_labels_code_mem instr_list id =
1231  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
1232 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
1233 >(index_of_internal_None … H) %
1234qed.
1235
1236lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
1237 eq_bv ? id' id = false →
1238  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
1239   address_of_word_labels_code_mem instr_list id =
1240   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
1241 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
1242 >(index_of_internal_Some_miss … H) //
1243qed.
1244
1245lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
1246  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
1247   address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
1248   = bitvector_of_nat … (|instr_list|).
1249 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?)
1250 >(index_of_internal_Some_hit … H) //
1251qed.
1252
1253definition address_of_word_labels ≝
1254  λps: PseudoStatus.
1255  λid: Identifier.
1256    address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
1257
1258definition construct_datalabels ≝
1259  λpreamble.
1260    \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (
1261    λt. λpreamble.
1262      let 〈datalabels, addr〉 ≝ t in
1263      let 〈name, size〉 ≝ preamble in
1264      let addr_16 ≝ bitvector_of_nat 16 addr in
1265        〈insert ? ? name addr_16 datalabels, addr + size〉)
1266          〈(Stub ? ?), 0〉 preamble).
Note: See TracBrowser for help on using the repository browser.