source: src/ASM/Status.ma @ 2276

Last change on this file since 2276 was 2272, checked in by mulligan, 7 years ago

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

File size: 38.3 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 
548
549definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝
550  λb: Byte.
551    let address ≝ nat_of_bitvector … b in
552      if (eqb address 128) then None ?
553      else if (eqb address 144) then Some … (inl … SFR_P1)
554      else if (eqb address 160) then None ?
555      else if (eqb address 176) then Some … (inl … SFR_P3)
556      else if (eqb address 153) then Some … (inl … SFR_SBUF)
557      else if (eqb address 138) then Some … (inl … SFR_TL0)
558      else if (eqb address 139) then Some … (inl … SFR_TL1)
559      else if (eqb address 140) then Some … (inl … SFR_TH0)
560      else if (eqb address 141) then Some … (inl … SFR_TH1)
561      else if (eqb address 200) then Some … (inr … SFR_T2CON)
562      else if (eqb address 202) then Some … (inr … SFR_RCAP2L)
563      else if (eqb address 203) then Some … (inr … SFR_RCAP2H)
564      else if (eqb address 204) then Some … (inr … SFR_TL2)
565      else if (eqb address 205) then Some … (inr … SFR_TH2)
566      else if (eqb address 135) then Some … (inl … SFR_PCON)
567      else if (eqb address 136) then Some … (inl … SFR_TCON)
568      else if (eqb address 137) then Some … (inl … SFR_TMOD)
569      else if (eqb address 152) then Some … (inl … SFR_SCON)
570      else if (eqb address 168) then Some … (inl … SFR_IE)
571      else if (eqb address 184) then Some … (inl … SFR_IP)
572      else if (eqb address 129) then Some … (inl … SFR_SP)
573      else if (eqb address 130) then Some … (inl … SFR_DPL)
574      else if (eqb address 131) then Some … (inl … SFR_DPH)
575      else if (eqb address 208) then Some … (inl … SFR_PSW)
576      else if (eqb address 224) then Some … (inl … SFR_ACC_A)
577      else if (eqb address 240) then Some … (inl … SFR_ACC_B)
578      else None ?.
579
580definition get_bit_addressable_sfr:
581    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝
582  λM: Type[0].
583  λcode_memory:M.
584  λs: PreStatus M code_memory.
585  λb: Byte.
586  λl: bool.
587  match sfr_of_Byte b with
588  [ None ⇒ match not_implemented in False with [ ]
589  | Some sfr8051_8052 ⇒
590    match sfr8051_8052 with
591    [ inl sfr ⇒
592      match sfr with
593      [ SFR_P1 ⇒
594        if l then
595          p1_latch … s
596        else
597          get_8051_sfr … s SFR_P1
598      | SFR_P3 ⇒
599        if l then
600          p3_latch … s
601        else
602          get_8051_sfr … s SFR_P3
603      | _ ⇒ get_8051_sfr … s sfr
604      ]
605    | inr sfr ⇒ get_8052_sfr M code_memory s sfr
606    ]
607  ].
608
609definition set_bit_addressable_sfr:
610    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → PreStatus M code_memory ≝
611  λM: Type[0].
612  λcode_memory:M.
613  λs: PreStatus M code_memory.
614  λb: Byte.
615  λv: Byte.
616   match sfr_of_Byte b with
617   [ None ⇒ match not_implemented in False with [ ]
618   | Some sfr8051_8052 ⇒
619      match sfr8051_8052 with
620      [ inl sfr ⇒
621         match sfr with
622         [ SFR_P1 ⇒
623           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
624           set_p1_latch ?? s v
625         | SFR_P3 ⇒
626           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
627           set_p3_latch ?? s v
628         | _ ⇒ set_8051_sfr ?? s sfr v ]
629      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]].
630
631lemma clock_set_bit_addressable_sfr:
632    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte.
633        clock … code_memory s = clock … code_memory (set_bit_addressable_sfr M code_memory s b v).
634  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
635  cases (sfr_of_Byte ?)
636  [1:
637    normalize nodelta cases not_implemented
638  |2:
639    * * normalize nodelta %
640  ]
641qed.
642
643lemma program_counter_set_bit_addressable_sfr:
644    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte.
645        program_counter … code_memory s = program_counter … code_memory (set_bit_addressable_sfr M code_memory s b v).
646  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
647  cases (sfr_of_Byte ?)
648  [1:
649    normalize nodelta cases not_implemented
650  |2:
651    * * %
652  ]
653qed.
654
655definition bit_address_of_register ≝
656  λM: Type[0].
657  λcode_memory:M.
658  λs: PreStatus M code_memory.
659  λr: BitVector 3.
660    let b ≝ get_index_v … r O ? in
661    let c ≝ get_index_v … r 1 ? in
662    let d ≝ get_index_v … r 2 ? in
663    let 〈 un, ln 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
664    let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in
665    let offset ≝
666      if ¬r1 ∧ ¬r0 then
667        O
668      else if ¬r1 ∧ r0 then
669        8
670      else if r1 ∧ r0 then
671        24
672      else
673        16
674    in
675      bitvector_of_nat 7 (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
676  [1,2,3,4,5:
677    normalize
678    repeat (@ le_S_S)
679    @ le_O_n;
680  ]
681qed.
682
683definition get_register ≝
684  λM: Type[0].
685  λcode_memory:M.
686  λs: PreStatus M code_memory.
687  λr: BitVector 3.
688    let address ≝ bit_address_of_register … s r in
689      lookup ?? address (low_internal_ram … s) (zero 8).
690     
691definition set_register ≝
692  λM: Type[0].
693  λcode_memory:M.
694  λs: PreStatus M code_memory.
695  λr: BitVector 3.
696  λv: Byte.
697    let address ≝ bit_address_of_register … s r in
698    let old_low_internal_ram ≝ low_internal_ram ?? s in
699    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
700      set_low_internal_ram … s new_low_internal_ram.
701     
702definition read_from_internal_ram ≝
703  λM: Type[0].
704  λcode_memory:M.
705  λs: PreStatus M code_memory.
706  λaddr: Byte.
707    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
708    let memory ≝
709      if head' … bit_one then
710        (low_internal_ram ?? s)
711      else
712        (high_internal_ram ?? s)
713    in
714      lookup … seven_bits memory (zero 8).
715
716definition read_at_stack_pointer ≝
717  λM: Type[0].
718  λcode_memory:M.
719  λs: PreStatus M code_memory.
720    read_from_internal_ram M code_memory s (get_8051_sfr ?? s SFR_SP).
721
722definition write_at_stack_pointer ≝
723  λM: Type[0].
724  λcode_memory:M.
725  λs: PreStatus M code_memory.
726  λv: Byte.
727    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr ?? s SFR_SP) in
728      if head' … 0 bit_one then
729        let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
730          set_high_internal_ram ?? s memory
731      else
732        let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
733          set_low_internal_ram ?? s memory.
734
735definition 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' ≝
736  λM,code_memory,s,v,a.
737   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M ? s = clock M ? s' with
738     [ DPTR ⇒ λ_:True.
739       let 〈 bu, bl 〉 ≝ vsplit … 8 8 v in
740       let status ≝ set_8051_sfr … s SFR_DPH bu in
741       let status ≝ set_8051_sfr … status SFR_DPL bl in
742         status
743     | _ ⇒ λK.
744       match K in False with
745       [
746       ]
747     ] (subaddressing_modein … a).
748 //
749qed.
750
751definition set_arg_16: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → PreStatus M code_memory ≝
752 set_arg_16'.
753
754lemma set_arg_16_ok: ∀M,cm,s,v,x. clock M cm s = clock M cm (set_arg_16 M cm s v x).
755 #M #cm #s #x #v whd in match set_arg_16; normalize nodelta @pi2
756qed.
757
758   
759definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ data16 ]] → Word ≝
760  λm, cm, s, a.
761    match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
762      [ DATA16 d ⇒ λ_:True. d
763      | _ ⇒ λK.
764        match K in False with
765        [
766        ]
767      ] (subaddressing_modein … a).
768     
769definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ;
770                                          acc_a ; acc_b ; data ; acc_dptr ;
771                                          acc_pc ; ext_indirect ;
772                                          ext_indirect_dptr ]] → Byte ≝
773  λm, cm, s, l, a.
774    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
775                                                acc_a ; acc_b ; data ; acc_dptr ;
776                                                acc_pc ; ext_indirect ;
777                                                ext_indirect_dptr ]] x) → ? with
778      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
779      | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
780      | DATA d ⇒ λdata: True. d
781      | REGISTER r ⇒ λregister: True. get_register ?? s r
782      | EXT_INDIRECT_DPTR ⇒
783        λext_indirect_dptr: True.
784          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
785            lookup ? 16 address (external_ram ?? s) (zero 8)
786      | EXT_INDIRECT e ⇒
787        λext_indirect: True.
788          let address ≝ get_register ?? s [[ false; false; e ]]  in
789          let padded_address ≝ pad 8 8 address in
790            lookup ? 16 padded_address (external_ram ?? s) (zero 8)
791      | ACC_DPTR ⇒
792        λacc_dptr: True.
793          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
794          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
795          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
796            lookup ? 16 address (external_ram ?? s) (zero 8)
797      | ACC_PC ⇒
798        λacc_pc: True.
799          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
800          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
801            lookup ? 16 address (external_ram ?? s) (zero 8)
802      | DIRECT d ⇒
803        λdirect: True.
804          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
805            match head' … hd with
806            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
807            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
808            ]
809      | INDIRECT i ⇒
810        λindirect: True.
811          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
812            match head' … hd with
813            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)
814            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
815            ]
816      | _ ⇒ λother.
817        match other in False with [ ]
818      ] (subaddressing_modein … a).
819
820definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
821                                   acc_a ; acc_b ; ext_indirect ;
822                                   ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝
823  λm, cm, s, a, v.
824    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
825                                                acc_a ; acc_b ; ext_indirect ;
826                                                ext_indirect_dptr ]] x) →
827                   PreStatus m cm
828            with
829      [ DIRECT d ⇒
830        λdirect: True.
831          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
832            match head' … bit_one with
833              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
834              | false ⇒
835                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
836                  set_low_internal_ram ?? s memory
837              ]
838      | INDIRECT i ⇒
839        λindirect: True.
840          let register ≝ get_register ?? s [[ false; false; i ]] in
841          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
842            match head' … bit_one with
843              [ false ⇒
844                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
845                  set_low_internal_ram ?? s memory
846              | true ⇒
847                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
848                  set_high_internal_ram ?? s memory
849              ]
850      | REGISTER r ⇒ λregister: True. set_register ?? s r v
851      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
852      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
853      | EXT_INDIRECT e ⇒
854        λext_indirect: True.
855          let address ≝ get_register ?? s [[ false; false; e ]] in
856          let padded_address ≝ pad 8 8 address in
857          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
858            set_external_ram ?? s memory
859      | EXT_INDIRECT_DPTR ⇒
860        λext_indirect_dptr: True.
861          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
862          let memory ≝ insert ? 16 address v (external_ram ?? s) in
863            set_external_ram ?? s memory
864      | _ ⇒
865        λother: False.
866          match other in False with [ ]
867      ] (subaddressing_modein … a).
868
869lemma clock_set_arg_8: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v).
870  cases daemon
871qed.
872
873lemma 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).
874  cases daemon
875qed.
876
877lemma 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).
878  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
879  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
880  cases daemon
881qed.
882
883lemma 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).
884  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
885  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
886  cases daemon
887qed.
888
889lemma 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).
890  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
891  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
892  cases daemon
893qed.
894
895theorem modulus_less_than:
896  ∀m,n: nat. (m mod (S n)) < S n.
897  #n #m
898  normalize
899  @ le_S_S
900  lapply (le_n n)
901  generalize in ⊢ (?%? → ?(??%?)?);
902  elim n in ⊢ (∀_:?. ??% → ?(?%??)?);
903  [ normalize
904    #n
905    @ (less_than_or_equal_b_elim n m)
906    normalize
907    [ //
908    | #H #K
909      @(le_inv_ind ?? K …)
910      [ # H1
911        < H1
912        //
913      | #x #H1 #H2 #H3
914        destruct
915      ]
916    ]
917  | normalize
918    # y # H1 # n # H2
919    @ (less_than_or_equal_b_elim n m)
920    normalize
921    [ //
922    | # K
923      @ H1
924      cut (n ≤ S y → n - S m ≤ y)
925      /2 by/
926      cases n
927      normalize
928      //
929      # x # K1
930      lapply (le_S_S_to_le … K1)
931      generalize in match m;
932      elim x
933      normalize
934      //
935      # w1 # H # m
936      cases m
937      normalize
938      //
939      # q # K2
940      @H
941      /3/
942    ]
943  ]
944qed.
945
946definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] →
947                       bool → bool ≝
948  λm, cm, s, a, l.
949    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
950                                                 n_bit_addr ;
951                                                 carry ]] x) → ? with
952      [ BIT_ADDR b ⇒
953        λbit_addr: True.
954        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
955        match head' … bit_1 with
956        [ true ⇒
957          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
958          let trans ≝ true:::four_bits @@ [[false; false; false]] in
959          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
960            get_index_v … sfr (nat_of_bitvector … three_bits) ?
961        | false ⇒
962          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
963          let address' ≝ [[true; false; false]]@@four_bits in
964          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
965            get_index_v … t (nat_of_bitvector … three_bits) ?
966        ]
967      | N_BIT_ADDR n ⇒
968        λn_bit_addr: True.
969        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
970        match head' … bit_1 with
971        [ true ⇒
972          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
973          let trans ≝ true:::four_bits @@ [[false; false; false]] in
974          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
975            ¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?)
976        | false ⇒
977          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
978          let address' ≝ [[true; false; false]]@@four_bits in
979          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
980            ¬(get_index_v … t (nat_of_bitvector … three_bits) ?)
981        ]
982      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
983      | _ ⇒ λother.
984        match other in False with [ ]
985      ] (subaddressing_modein … a).
986  //
987qed.
988     
989definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝
990  λm: Type[0].
991  λcm.
992  λs: PreStatus m cm.
993  λa: [[bit_addr; carry]].
994  λv: Bit.
995    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ? with
996      [ BIT_ADDR b ⇒ λbit_addr: True.
997        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
998        match head' … bit_1 with
999        [ true ⇒
1000          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1001          let trans ≝ true:::four_bits @@ [[false; false; false]] in
1002          let sfr ≝ get_bit_addressable_sfr … s trans true in
1003          let new_sfr ≝ set_index … sfr (nat_of_bitvector … three_bits) v ? in
1004            set_bit_addressable_sfr … s new_sfr trans
1005        | false ⇒
1006          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1007          let address' ≝ [[true; false; false]]@@four_bits in
1008          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1009          let n_bit ≝ set_index … t (nat_of_bitvector … three_bits) v ? in
1010          let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1011            set_low_internal_ram … s memory
1012        ]
1013      | CARRY ⇒
1014        λcarry: True.
1015        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1016        let new_psw ≝ v:::seven_bits in
1017          set_8051_sfr ?? s SFR_PSW new_psw
1018      | _ ⇒
1019        λother: False.
1020          match other in False with
1021            [ ]
1022      ] (subaddressing_modein … a).
1023  //
1024qed.
1025
1026lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v).
1027  cases daemon
1028qed.
1029
1030definition fetch_pseudo_instruction:
1031 ∀code_mem:list labelled_instruction. ∀pc:Word.
1032  nat_of_bitvector … pc < |code_mem| → (pseudo_instruction × Word) ≝
1033  λcode_mem.
1034  λpc: Word.
1035  λpc_ok.
1036    let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? pc) … code_mem pc_ok in
1037    let new_pc ≝ add ? pc (bitvector_of_nat … 1) in
1038      〈instr, new_pc〉.
1039
1040lemma snd_fetch_pseudo_instruction:
1041 ∀l,ppc,ppc_ok. \snd (fetch_pseudo_instruction l ppc ppc_ok) = add ? ppc (bitvector_of_nat ? 1).
1042 #l #ppc #ppc_ok whd in ⊢ (??(???%)?); @pair_elim
1043 #lft #rgt #_ %
1044qed.
1045
1046lemma fetch_pseudo_instruction_vsplit:
1047 ∀instr_list,ppc,ppc_ok.
1048  ∃pre,suff,lbl.
1049   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
1050#instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
1051cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
1052lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
1053#EQ %{lbl0} @EQ
1054qed.
1055
1056lemma fetch_pseudo_instruction_append:
1057 ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.
1058  let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
1059  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
1060  〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
1061 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
1062 cut (|l1| + nat_of_bitvector … ppc < 2^16)
1063 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
1064 -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
1065 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
1066 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ]
1067 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
1068 #lbl #instr normalize nodelta >add_associative %
1069qed.
1070
1071definition is_well_labelled_p ≝
1072  λinstr_list.
1073  ∀id: Identifier.
1074  ∀ppc.
1075  ∀ppc_ok.
1076  ∀i.
1077    \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) = i →
1078      instruction_has_label id i →
1079        occurs_exactly_once ASMTag pseudo_instruction id instr_list.
1080
1081definition construct_datalabels: preamble → ? ≝
1082  λthe_preamble: preamble.
1083    \fst (foldl ((identifier_map ASMTag Word) × Word) ? (
1084    λt. λpreamble.
1085      let 〈datalabels, addr〉 ≝ t in
1086      let 〈name, size〉 ≝ preamble in
1087      let 〈carry, sum〉 ≝ half_add … addr size in
1088        〈add ? ? datalabels name addr, sum〉)
1089          〈empty_map …, zero 16〉 (\snd the_preamble)).
Note: See TracBrowser for help on using the repository browser.