source: src/ASM/Status.ma @ 2168

Last change on this file since 2168 was 2160, checked in by mulligan, 7 years ago

Added a new scratch file Test.ma for working on lemmas that are needed in the massive proof to avoid having to retypecheck everything. Lots of work from the last week on the AssemblyProofSplit?.ma file, as well as an attempt to use Russell-style types on set_arg_8.

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