source: src/ASM/Status.ma @ 1600

Last change on this file since 1600 was 1600, checked in by sacerdot, 8 years ago

utilities and ASM ported to the new standard library

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