source: src/ASM/Status.ma @ 2136

Last change on this file since 2136 was 2123, checked in by boender, 8 years ago
File size: 41.7 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(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[1666]88record PreStatus (M: Type[0]) (code_memory: M) : Type[0] ≝
[475]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
[821]105definition Status ≝ PreStatus (BitVectorTrie Byte 16).
[827]106definition PseudoStatus ≝ PreStatus (pseudo_assembly_program).
[821]107
[475]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 ≝
[821]129  λM: Type[0].
[1666]130  λcode_memory:M.
131  λs: PreStatus M code_memory.
[475]132  λt: Time.
[1666]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
[475]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 ≝
[821]153  λM: Type[0].
[1666]154  λcode_memory:M.
155  λs: PreStatus M code_memory.
[475]156  λb: Byte.
[1666]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
[475]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 ≝
[821]177  λM: Type[0].
[1666]178  λcode_memory:M.
179  λs: PreStatus M code_memory.
[475]180  λb: Byte.
[1666]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
[475]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 ≝
[821]201  λM: Type[0].
[1666]202  λcode_memory:M.
203  λs: PreStatus M code_memory.
[475]204  λi: SFR8051.
[1666]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].
[1666]213  λcode_memory:M.
214  λs: PreStatus M code_memory.
[475]215  λi: SFR8052.
[1666]216    let sfr ≝ special_function_registers_8052 ?? s in
[475]217    let index ≝ sfr_8052_index i in
218      get_index_v … sfr index ?.
219    @ sfr8052_index_5
220qed.
221
222definition set_8051_sfr ≝
[821]223  λM: Type[0].
[1666]224  λcode_memory:M.
225  λs: PreStatus M code_memory.
[475]226  λi: SFR8051.
227  λb: Byte.
228    let index ≝ sfr_8051_index i in
[1666]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
[475]235    let new_special_function_registers_8051 ≝
236      set_index Byte 19 old_special_function_registers_8051 index b ? in
[1666]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
[475]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 ≝
[821]254  λM: Type[0].
[1666]255  λcode_memory:M.
256  λs: PreStatus M code_memory.
[475]257  λi: SFR8052.
258  λb: Byte.
259    let index ≝ sfr_8052_index i in
[1666]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
[475]266    let new_special_function_registers_8052 ≝
267      set_index Byte 5 old_special_function_registers_8052 index b ? in
[1666]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
[475]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 ≝
[821]285  λM: Type[0].
[1666]286  λcode_memory:M.
287  λs: PreStatus M code_memory.
[475]288  λw: Word.
[1666]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
[475]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 ≝
[911]309  λM,M': Type[0].
[1666]310  λcode_memory:M.
311  λs: PreStatus M code_memory.
[911]312  λr: M'.
[1666]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
[911]322      mk_PreStatus M' r
[475]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 ≝
[821]334  λM: Type[0].
[1666]335  λcode_memory:M.
336  λs: PreStatus M code_memory.
[475]337  λr: BitVectorTrie Byte 7.
[1666]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
[475]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 ≝
[821]358  λM: Type[0].
[1666]359  λcode_memory:M.
360  λs: PreStatus M code_memory.
[475]361  λr: BitVectorTrie Byte 7.
[1666]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
[475]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 ≝
[821]383  λM: Type[0].
[1666]384  λcode_memory:M.
385  λs: PreStatus M code_memory.
[475]386  λr: BitVectorTrie Byte 16.
[1666]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
[475]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 ≝
[821]407  λM: Type[0].
[1666]408  λcode_memory:M.
409  λs: PreStatus M code_memory.
410    let sfr ≝ special_function_registers_8051 ?? s in
[475]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 ≝
[821]422  λM: Type[0].
[1666]423  λcode_memory:M.
424  λs: PreStatus M code_memory.
425    let sfr ≝ special_function_registers_8051 ?? s in
[475]426    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
[949]427      get_index_v bool 8 psw 1 ?.
[475]428    normalize
429    repeat (@ (le_S_S ? ?))
430    @ le_O_n
431qed.
432
433definition get_fo_flag ≝
[821]434  λM: Type[0].
[1666]435  λcode_memory:M.
436  λs: PreStatus M code_memory.
437    let sfr ≝ special_function_registers_8051 ?? s in
[475]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 ≝
[821]446  λM: Type[0].
[1666]447  λcode_memory:M.
448  λs: PreStatus M code_memory.
449    let sfr ≝ special_function_registers_8051 ?? s in
[475]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 ≝
[821]458  λM: Type[0].
[1666]459  λcode_memory:M.
460  λs: PreStatus M code_memory.
461    let sfr ≝ special_function_registers_8051 ?? s in
[475]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 ≝
[821]470  λM: Type[0].
[1666]471  λcode_memory:M.
472  λs: PreStatus M code_memory.
473    let sfr ≝ special_function_registers_8051 ?? s in
[475]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 ≝
[821]482  λM: Type[0].
[1666]483  λcode_memory:M.
484  λs: PreStatus M code_memory.
485    let sfr ≝ special_function_registers_8051 ?? s in
[475]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 ≝
[821]494  λM: Type[0].
[1666]495  λcode_memory:M.
496  λs: PreStatus M code_memory.
497    let sfr ≝ special_function_registers_8051 ?? s in
[475]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 ≝
[821]506  λM: Type[0].
[1666]507  λcode_memory:M.
508  λs: PreStatus M code_memory.
[475]509  λcy: Bit.
510  λac: option Bit.
511  λov: Bit.
[1882]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
[475]521    let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
[1666]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 ]].
[475]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 ≝
[821]533  λM: Type[0].
534  λcode_mem: M.
535  let status ≝ mk_PreStatus M code_mem                    (* Code mem. *)
[475]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
[1666]546    set_8051_sfr ?? status SFR_SP (bitvector_of_nat 8 7).
[475]547 
548definition get_bit_addressable_sfr ≝
[821]549  λM: Type[0].
[1666]550  λcode_memory:M.
551  λs: PreStatus M code_memory.
[475]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
[1666]560          (p1_latch ?? s)
[475]561        else
[1666]562          (get_8051_sfr ?? s SFR_P1)
[475]563      else if (eqb address 160) then
564        ?
565      else if (eqb address 176) then
566        if l then
[1666]567          (p3_latch ?? s)
[475]568        else
[1666]569          (get_8051_sfr ?? s SFR_P3)
[475]570      else if (eqb address 153) then
[1666]571        get_8051_sfr ?? s SFR_SBUF
[475]572      else if (eqb address 138) then
[1666]573        get_8051_sfr ?? s SFR_TL0
[475]574      else if (eqb address 139) then
[1666]575        get_8051_sfr ?? s SFR_TL1
[475]576      else if (eqb address 140) then
[1666]577        get_8051_sfr ?? s SFR_TH0
[475]578      else if (eqb address 141) then
[1666]579        get_8051_sfr ?? s SFR_TH1
[475]580      else if (eqb address 200) then
[1666]581        get_8052_sfr ?? s SFR_T2CON
[475]582      else if (eqb address 202) then
[1666]583        get_8052_sfr ?? s SFR_RCAP2L
[475]584      else if (eqb address 203) then
[1666]585        get_8052_sfr ?? s SFR_RCAP2H
[475]586      else if (eqb address 204) then
[1666]587        get_8052_sfr ?? s SFR_TL2
[475]588      else if (eqb address 205) then
[1666]589        get_8052_sfr ?? s SFR_TH2
[475]590      else if (eqb address 135) then
[1666]591        get_8051_sfr ?? s SFR_PCON
[475]592      else if (eqb address 136) then
[1666]593        get_8051_sfr ?? s SFR_TCON
[475]594      else if (eqb address 137) then
[1666]595        get_8051_sfr ?? s SFR_TMOD
[475]596      else if (eqb address 152) then
[1666]597        get_8051_sfr ?? s SFR_SCON
[475]598      else if (eqb address 168) then
[1666]599        get_8051_sfr ?? s SFR_IE
[475]600      else if (eqb address 184) then
[1666]601        get_8051_sfr ?? s SFR_IP
[475]602      else if (eqb address 129) then
[1666]603        get_8051_sfr ?? s SFR_SP
[475]604      else if (eqb address 130) then
[1666]605        get_8051_sfr ?? s SFR_DPL
[475]606      else if (eqb address 131) then
[1666]607        get_8051_sfr ?? s SFR_DPH
[475]608      else if (eqb address 208) then
[1666]609        get_8051_sfr ?? s SFR_PSW
[475]610      else if (eqb address 224) then
[1666]611        get_8051_sfr ?? s SFR_ACC_A
[475]612      else if (eqb address 240) then
[1666]613        get_8051_sfr ?? s SFR_ACC_B
[475]614      else
615        ?.
616      cases not_implemented
617qed.
618
619definition set_bit_addressable_sfr ≝
[821]620  λM: Type[0].
[1666]621  λcode_memory:M.
622  λs: PreStatus M code_memory.
[475]623  λb: Byte.
624  λv: Byte.
625    let address ≝ nat_of_bitvector … b in
626      if (eqb address 128) then
627        ?
628      else if (eqb address 144) then
[1666]629        let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
630        let status_2 ≝ set_p1_latch ?? s v in
[475]631          status_2
632      else if (eqb address 160) then
633        ?
634      else if (eqb address 176) then
[1666]635        let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
636        let status_2 ≝ set_p3_latch ?? s v in
[475]637          status_2
638      else if (eqb address 153) then
[1666]639        set_8051_sfr ?? s SFR_SBUF v
[475]640      else if (eqb address 138) then
[1666]641        set_8051_sfr ?? s SFR_TL0 v
[475]642      else if (eqb address 139) then
[1666]643        set_8051_sfr ?? s SFR_TL1 v
[475]644      else if (eqb address 140) then
[1666]645        set_8051_sfr ?? s SFR_TH0 v
[475]646      else if (eqb address 141) then
[1666]647        set_8051_sfr ?? s SFR_TH1 v
[475]648      else if (eqb address 200) then
[1666]649        set_8052_sfr ?? s SFR_T2CON v
[475]650      else if (eqb address 202) then
[1666]651        set_8052_sfr ?? s SFR_RCAP2L v
[475]652      else if (eqb address 203) then
[1666]653        set_8052_sfr ?? s SFR_RCAP2H v
[475]654      else if (eqb address 204) then
[1666]655        set_8052_sfr ?? s SFR_TL2 v
[475]656      else if (eqb address 205) then
[1666]657        set_8052_sfr ?? s SFR_TH2 v
[475]658      else if (eqb address 135) then
[1666]659        set_8051_sfr ?? s SFR_PCON v
[475]660      else if (eqb address 136) then
[1666]661        set_8051_sfr ?? s SFR_TCON v
[475]662      else if (eqb address 137) then
[1666]663        set_8051_sfr ?? s SFR_TMOD v
[475]664      else if (eqb address 152) then
[1666]665        set_8051_sfr ?? s SFR_SCON v
[475]666      else if (eqb address 168) then
[1666]667        set_8051_sfr ?? s SFR_IE v
[475]668      else if (eqb address 184) then
[1666]669        set_8051_sfr ?? s SFR_IP v
[475]670      else if (eqb address 129) then
[1666]671        set_8051_sfr ?? s SFR_SP v
[475]672      else if (eqb address 130) then
[1666]673        set_8051_sfr ?? s SFR_DPL v
[475]674      else if (eqb address 131) then
[1666]675        set_8051_sfr ?? s SFR_DPH v
[475]676      else if (eqb address 208) then
[1666]677        set_8051_sfr ?? s SFR_PSW v
[475]678      else if (eqb address 224) then
[1666]679        set_8051_sfr ?? s SFR_ACC_A v
[475]680      else if (eqb address 240) then
[1666]681        set_8051_sfr ?? s SFR_ACC_B v
[475]682      else
683        ?.
684      cases not_implemented
685qed.
686
687definition bit_address_of_register ≝
[821]688  λM: Type[0].
[1666]689  λcode_memory:M.
690  λs: PreStatus M code_memory.
[475]691  λr: BitVector 3.
692    let b ≝ get_index_v … r O ? in
693    let c ≝ get_index_v … r 1 ? in
694    let d ≝ get_index_v … r 2 ? in
[2032]695    let 〈 un, ln 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
[705]696    let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in
[475]697    let offset ≝
698      if ¬r1 ∧ ¬r0 then
699        O
700      else if ¬r1 ∧ r0 then
701        8
702      else if r1 ∧ r0 then
703        24
704      else
705        16
706    in
707      bitvector_of_nat 7 (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
708  [1,2,3,4,5:
709    normalize
710    repeat (@ le_S_S)
711    @ le_O_n;
712  ]
713qed.
714
715definition get_register ≝
[821]716  λM: Type[0].
[1666]717  λcode_memory:M.
718  λs: PreStatus M code_memory.
[475]719  λr: BitVector 3.
[1666]720    let address ≝ bit_address_of_register … s r in
721      lookup ?? address (low_internal_ram … s) (zero 8).
[475]722     
723definition set_register ≝
[821]724  λM: Type[0].
[1666]725  λcode_memory:M.
726  λs: PreStatus M code_memory.
[475]727  λr: BitVector 3.
728  λv: Byte.
[1666]729    let address ≝ bit_address_of_register … s r in
730    let old_low_internal_ram ≝ low_internal_ram ?? s in
[475]731    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
[1666]732      set_low_internal_ram … s new_low_internal_ram.
[475]733     
734definition read_at_stack_pointer ≝
[821]735  λM: Type[0].
[1666]736  λcode_memory:M.
737  λs: PreStatus M code_memory.
[2032]738    let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_SP) in
[1666]739    let m ≝ get_index_v ?? nu O ? in
740    let r1 ≝ get_index_v ?? nu 1 ? in
741    let r2 ≝ get_index_v ?? nu 2 ? in
742    let r3 ≝ get_index_v ?? nu 3 ? in
[475]743    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
744    let memory ≝
745      if m then
[1666]746        (low_internal_ram ?? s)
[475]747      else
[1666]748        (high_internal_ram ?? s)
[475]749    in
750      lookup … address memory (zero 8).
751  [1,2,3,4:
752     normalize
753     repeat (@ le_S_S)
754     @ le_O_n
755  ]
756qed.
757
758definition write_at_stack_pointer ≝
[821]759  λM: Type[0].
[1666]760  λcode_memory:M.
761  λs: PreStatus M code_memory.
[475]762  λv: Byte.
[2032]763    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ?? s SFR_SP) in
[1666]764    let bit_zero ≝ get_index_v ?? nu O ? in
765    let bit_1 ≝ get_index_v ?? nu 1 ? in
766    let bit_2 ≝ get_index_v ?? nu 2 ? in
767    let bit_3 ≝ get_index_v ?? nu 3 ? in
[475]768      if bit_zero then
769        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
[1666]770                              v (low_internal_ram ?? s) in
771          set_low_internal_ram ?? s memory
[475]772      else
773        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
[1666]774                              v (high_internal_ram ?? s) in
775          set_high_internal_ram ?? s memory.
[475]776  [1,2,3,4:
777     normalize
778     repeat (@ le_S_S)
779     @ le_O_n
780  ]
781qed.
782
[1666]783definition 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' ≝
784  λM,code_memory,s,v,a.
785   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M ? s = clock M ? s' with
[475]786     [ DPTR ⇒ λ_:True.
[2032]787       let 〈 bu, bl 〉 ≝ vsplit … 8 8 v in
[1666]788       let status ≝ set_8051_sfr … s SFR_DPH bu in
789       let status ≝ set_8051_sfr … status SFR_DPL bl in
[475]790         status
791     | _ ⇒ λK.
792       match K in False with
793       [
794       ]
795     ] (subaddressing_modein … a).
[1588]796 //
797qed.
798
[1666]799definition set_arg_16: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → PreStatus M code_memory ≝
[1588]800 set_arg_16'.
801
[1666]802lemma set_arg_16_ok: ∀M,cm,s,v,x. clock M cm s = clock M cm (set_arg_16 M cm s v x).
803 #M #cm #s #x #v whd in match set_arg_16; normalize nodelta @pi2
[1588]804qed.
805
[475]806   
[1666]807definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ data16 ]] → Word ≝
808  λm, cm, s, a.
[475]809    match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
810      [ DATA16 d ⇒ λ_:True. d
811      | _ ⇒ λK.
812        match K in False with
813        [
814        ]
815      ] (subaddressing_modein … a).
816     
[1666]817definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ;
[475]818                                          acc_a ; acc_b ; data ; acc_dptr ;
819                                          acc_pc ; ext_indirect ;
820                                          ext_indirect_dptr ]] → Byte ≝
[1666]821  λm, cm, s, l, a.
[757]822    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
[475]823                                                acc_a ; acc_b ; data ; acc_dptr ;
824                                                acc_pc ; ext_indirect ;
825                                                ext_indirect_dptr ]] x) → ? with
[1666]826      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
827      | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
[475]828      | DATA d ⇒ λdata: True. d
[1666]829      | REGISTER r ⇒ λregister: True. get_register ?? s r
[475]830      | EXT_INDIRECT_DPTR ⇒
831        λext_indirect_dptr: True.
[1666]832          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
833            lookup ? 16 address (external_ram ?? s) (zero 8)
[475]834      | EXT_INDIRECT e ⇒
835        λext_indirect: True.
[1666]836          let address ≝ get_register ?? s [[ false; false; e ]]  in
[475]837          let padded_address ≝ pad 8 8 address in
[1666]838            lookup ? 16 padded_address (external_ram ?? s) (zero 8)
[475]839      | ACC_DPTR ⇒
840        λacc_dptr: True.
[1666]841          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
842          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
[475]843          let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in
[1666]844            lookup ? 16 address (external_ram ?? s) (zero 8)
[475]845      | ACC_PC ⇒
846        λacc_pc: True.
[1666]847          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
848          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
849            lookup ? 16 address (external_ram ?? s) (zero 8)
[475]850      | DIRECT d ⇒
851        λdirect: True.
[2032]852          let 〈 nu, nl 〉 ≝ vsplit ? 4 4 d in
[949]853          let bit_one ≝ get_index_v ? ? nu 0 ? in
[2032]854          let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
[949]855            match bit_one with
856              [ false ⇒
[475]857                  let address ≝ three_bits @@ nl in
[1666]858                    lookup ? 7 address (low_internal_ram ?? s) (zero 8)
859              | true ⇒ get_bit_addressable_sfr ?? s 8 d l
[475]860              ]
861      | INDIRECT i ⇒
862        λindirect: True.
[2032]863          let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_register ?? s [[ false; false; i]]) in
864          let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
[1515]865          let bit_1 ≝ get_index_v ?? bit_one_v O ? in
[949]866          match  bit_1 with
867            [ false ⇒
[1666]868                lookup ? 7 (three_bits @@ nl) (low_internal_ram ?? s) (zero 8)
[949]869            | true ⇒
[1666]870                lookup ? 7 (three_bits @@ nl) (high_internal_ram ?? s) (zero 8)
[475]871            ]
872      | _ ⇒ λother.
873        match other in False with [ ]
874      ] (subaddressing_modein … a).
875  [1,2:
876     normalize
877     repeat (@ le_S_S)
878     @ le_O_n
879  ]
880qed.
881
[1666]882axiom clock_set_bit_addressable_sfr: ∀m,cm,s,d,v. clock m cm s = clock … (set_bit_addressable_sfr … s d v).
[1526]883
[1666]884definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ;
[475]885                                   acc_a ; acc_b ; ext_indirect ;
[1666]886                                   ext_indirect_dptr ]] → Byte → Σs':PreStatus M code_memory.
887                                   clock … code_memory s = clock … code_memory s' ≝
888  λm, cm, s, a, v.
[757]889    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
[475]890                                                acc_a ; acc_b ; ext_indirect ;
[1526]891                                                ext_indirect_dptr ]] x) →
[1666]892                   Σs':PreStatus m cm. clock m cm s = clock m cm s'
[1526]893                   (*CSC: bug here if one specified the two clock above*)
894            with
[475]895      [ DIRECT d ⇒
896        λdirect: True.
[2032]897          let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in
[949]898          let bit_one ≝ get_index_v ? ? nu 0 ? in
[2032]899          let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
[949]900            match bit_one with
[1666]901              [ true ⇒ set_bit_addressable_sfr ?? s d v
[475]902              | false ⇒
[1666]903                let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in
904                  set_low_internal_ram ?? s memory
[475]905              ]
906      | INDIRECT i ⇒
907        λindirect: True.
[1666]908          let register ≝ get_register ?? s [[ false; false; i ]] in
[2032]909          let 〈nu, nl〉 ≝ vsplit ? 4 4 register in
[949]910          let bit_1 ≝ get_index_v … nu 0 ? in
[2032]911          let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
[475]912            match bit_1 with
[949]913              [ false ⇒
[1666]914                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in
915                  set_low_internal_ram ?? s memory
[949]916              | true ⇒
[1666]917                let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in
918                  set_high_internal_ram ?? s memory
[475]919              ]
[1666]920      | REGISTER r ⇒ λregister: True. set_register ?? s r v
921      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
922      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
[475]923      | EXT_INDIRECT e ⇒
924        λext_indirect: True.
[1666]925          let address ≝ get_register ?? s [[ false; false; e ]] in
[475]926          let padded_address ≝ pad 8 8 address in
[1666]927          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
928            set_external_ram ?? s memory
[475]929      | EXT_INDIRECT_DPTR ⇒
930        λext_indirect_dptr: True.
[1666]931          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
932          let memory ≝ insert ? 16 address v (external_ram ?? s) in
933            set_external_ram ?? s memory
[1526]934      | _ ⇒
[475]935        λother: False.
936          match other in False with [ ]
937      ] (subaddressing_modein … a).
[1526]938// qed.
[475]939
[1666]940definition 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 ≝
[1588]941 set_arg_8'.
942
[1666]943lemma set_arg_8_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v).
944 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta @pi2
[1588]945qed.
946
[475]947theorem modulus_less_than:
948  ∀m,n: nat. (m mod (S n)) < S n.
949  #n #m
950  normalize
951  @ le_S_S
952  lapply (le_n n)
[1516]953  generalize in ⊢ (?%? → ?(??%?)?);
954  elim n in ⊢ (∀_:?. ??% → ?(?%??)?);
[475]955  [ normalize
956    #n
957    @ (less_than_or_equal_b_elim n m)
958    normalize
959    [ //
960    | #H #K
[1516]961      @(le_inv_ind ?? K …)
[475]962      [ # H1
963        < H1
964        //
965      | #x #H1 #H2 #H3
966        destruct
967      ]
968    ]
969  | normalize
970    # y # H1 # n # H2
971    @ (less_than_or_equal_b_elim n m)
972    normalize
973    [ //
974    | # K
975      @ H1
976      cut (n ≤ S y → n - S m ≤ y)
[1521]977      /2 by/
[475]978      cases n
979      normalize
980      //
981      # x # K1
982      lapply (le_S_S_to_le … K1)
[1516]983      generalize in match m;
[475]984      elim x
985      normalize
986      //
987      # w1 # H # m
988      cases m
989      normalize
990      //
991      # q # K2
[1516]992      @H
[475]993      /3/
994    ]
995  ]
996qed.
997
[1666]998definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] →
[475]999                       bool → bool ≝
[1666]1000  λm, cm, s, a, l.
[475]1001    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
1002                                                 n_bit_addr ;
1003                                                 carry ]] x) → ? with
1004      [ BIT_ADDR b ⇒
1005        λbit_addr: True.
[2032]1006          let 〈 nu, nl 〉 ≝ vsplit … 4 4 b in
[1393]1007          let bit_1 ≝ get_index_v ? ? nu 0 ? in
[2032]1008          let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
[475]1009            match bit_1 with
1010              [ true ⇒
1011                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
1012                let d ≝ address ÷ 8 in
1013                let m ≝ address mod 8 in
1014                let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
[1666]1015                let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in
[475]1016                  get_index_v … sfr m ?
1017              | false ⇒
1018                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
1019                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
[1666]1020                let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
[475]1021                  get_index_v … t (modulus address 8) ?
1022              ]
1023      | N_BIT_ADDR n ⇒
1024        λn_bit_addr: True.
[2032]1025          let 〈 nu, nl 〉 ≝ vsplit … 4 4 n in
[1393]1026          let bit_1 ≝ get_index_v ? ? nu 0 ? in
[2032]1027          let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
[475]1028            match bit_1 with
1029              [ true ⇒
1030                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
1031                let d ≝ address ÷ 8 in
1032                let m ≝ address mod 8 in
1033                let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
[1666]1034                let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in
[475]1035                  ¬(get_index_v … sfr m ?)
1036              | false ⇒
1037                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
1038                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
[1666]1039                let trans ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
[475]1040                  ¬(get_index_v … trans (modulus address 8) ?)
1041              ]
[1666]1042      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
[475]1043      | _ ⇒ λother.
1044        match other in False with [ ]
1045      ] (subaddressing_modein … a).
1046      [3,6:
1047         normalize
1048         repeat (@ le_S_S)
1049         @ le_O_n
1050      |1,2,4,5:
[1518]1051         @modulus_less_than
[475]1052      ]
1053qed.
1054     
[1666]1055definition 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' ≝
[1581]1056  λm: Type[0].
[1666]1057  λcm.
1058  λs: PreStatus m cm.
[1581]1059  λa: [[bit_addr; carry]].
1060  λv: Bit.
[1666]1061    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with
[475]1062      [ BIT_ADDR b ⇒ λbit_addr: True.
[2032]1063        let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
[1581]1064        let bit_1 ≝ get_index_v ?? nu 0 ? in
[2032]1065        let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
[1581]1066        match bit_1 return λ_. ? with
1067          [ true ⇒
1068            let address ≝ nat_of_bitvector … (three_bits @@ nl) in
1069            let d ≝ address ÷ 8 in
1070            let m ≝ address mod 8 in
1071            let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
[1666]1072            let sfr ≝ get_bit_addressable_sfr ?? s ? t true in
[1581]1073            let new_sfr ≝ set_index … sfr m v ? in
[1666]1074              set_bit_addressable_sfr ?? s new_sfr t
[1581]1075          | false ⇒
1076            let address ≝ nat_of_bitvector … (three_bits @@ nl) in
1077            let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
[1666]1078            let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
[1581]1079            let n_bit ≝ set_index … t (modulus address 8) v ? in
[1666]1080            let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1081              set_low_internal_ram ?? s memory
[1581]1082          ]
[475]1083      | CARRY ⇒
1084        λcarry: True.
[2032]1085        let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
[1581]1086        let bit_1 ≝ get_index_v… nu 1 ? in
1087        let bit_2 ≝ get_index_v… nu 2 ? in
1088        let bit_3 ≝ get_index_v… nu 3 ? in
1089        let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
[1666]1090          set_8051_sfr ?? s SFR_PSW new_psw
[475]1091      | _ ⇒
1092        λother: False.
1093          match other in False with
1094            [ ]
1095      ] (subaddressing_modein … a).
[1588]1096try (repeat @le_S_S @le_O_n)
1097/by/
[475]1098qed.
1099
[1666]1100definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝ set_arg_1'.
[1588]1101
[1666]1102lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v).
1103 #M #cm #s #x #v whd in match set_arg_1; normalize nodelta @pi2
[1588]1104qed.
1105
[2055]1106definition fetch_pseudo_instruction:
1107 ∀code_mem:list labelled_instruction. ∀pc:Word.
1108  nat_of_bitvector … pc < |code_mem| → (pseudo_instruction × Word) ≝
[843]1109  λcode_mem.
1110  λpc: Word.
[2055]1111  λpc_ok.
1112    let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? pc) … code_mem pc_ok in
1113    let new_pc ≝ add ? pc (bitvector_of_nat … 1) in
[843]1114      〈instr, new_pc〉.
[985]1115
[993]1116lemma snd_fetch_pseudo_instruction:
[2055]1117 ∀l,ppc,ppc_ok. \snd (fetch_pseudo_instruction l ppc ppc_ok) = add ? ppc (bitvector_of_nat ? 1).
1118 #l #ppc #ppc_ok whd in ⊢ (??(???%)?); @pair_elim
[1946]1119 #lft #rgt #_ %
[993]1120qed.
1121
[2111]1122lemma fetch_pseudo_instruction_vsplit:
1123 ∀instr_list,ppc,ppc_ok.
1124  ∃pre,suff,lbl.
1125   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
1126#instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
1127cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
1128lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
1129#EQ %{lbl0} @EQ
1130qed.
1131
1132lemma fetch_pseudo_instruction_append:
1133 ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.
1134  let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
1135  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
1136  〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
1137 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
1138 cut (|l1| + nat_of_bitvector … ppc < 2^16)
1139 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
1140 -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
1141 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
1142 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ]
1143 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
1144 #lbl #instr normalize nodelta >add_associative %
1145qed.
1146
[2123]1147definition is_well_labelled_p ≝
1148  λinstr_list.
1149  ∀id: Identifier.
1150  ∀ppc. ∀ppc_ok.
1151  ∀i.
1152    fetch_pseudo_instruction instr_list ppc ppc_ok = i →
1153      instruction_has_label id (\fst i) →
1154        occurs_exactly_once ASMTag pseudo_instruction id instr_list.
1155
[985]1156definition address_of_word_labels_code_mem ≝
[1882]1157  λcode_mem : list labelled_instruction.
[985]1158  λid: Identifier.
[1882]1159    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
[985]1160
1161lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
[1882]1162 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
[985]1163  address_of_word_labels_code_mem instr_list id =
1164  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
[1518]1165 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
[1882]1166 >(index_of_internal_None ?????? H) %
[985]1167qed.
1168
1169lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
[1515]1170 eq_identifier ? id' id = false →
[1882]1171  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
[985]1172   address_of_word_labels_code_mem instr_list id =
1173   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
[1518]1174 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
[1882]1175 >(index_of_internal_Some_miss ???????? H) [ @refl | // ]
[985]1176qed.
1177
1178lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
[1882]1179  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
[985]1180   address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
1181   = bitvector_of_nat … (|instr_list|).
[1518]1182 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
[1882]1183 >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl
[985]1184qed.
1185
1186definition address_of_word_labels ≝
[1666]1187  λpr: pseudo_assembly_program.
[985]1188  λid: Identifier.
[1666]1189    address_of_word_labels_code_mem (\snd pr) id.
[985]1190
[1541]1191definition construct_datalabels: preamble → ? ≝
1192  λthe_preamble: preamble.
1193    \fst (foldl ((identifier_map ASMTag Word) × Word) ? (
[985]1194    λt. λpreamble.
1195      let 〈datalabels, addr〉 ≝ t in
1196      let 〈name, size〉 ≝ preamble in
[1541]1197      let 〈carry, sum〉 ≝ half_add … addr size in
1198        〈add ? ? datalabels name addr, sum〉)
1199          〈empty_map …, zero 16〉 (\snd the_preamble)).
Note: See TracBrowser for help on using the repository browser.