source: src/ASM/Status.ma @ 1666

Last change on this file since 1666 was 1666, checked in by sacerdot, 6 years ago

PreStatus? datatype change: the code_memory field is not a left parameter.
This greatly simplify the dependent type madness due to policy depending
on the code_memory and not really on the status. On the other hand it
makes the rest of the code uglier.

Note: the changes have not been propagated yet to ASMCosts, CostsProof? and
Interpret2. The AssemlyProof? is almost repaired.

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