source: src/ASM/Status.ma

Last change on this file was 3075, checked in by mckinna, 7 years ago

Apologies for late folding in of old changes which were left over from earlier partial commits; hopefully no clash with paolo's recent commits

Cleaned up treatment of get_*_flag from SFR_PSW

Streamlined lots of typechecking constraints in favour of \ldots/?

Removed daemons by proving many of the clock_set_* lemmas, mostly Russell-style; but should these be moved to StatusProofs?*.ma?

Further streamlining possible: lots of vsplit 1 7 redundancy when dealing with the internal_memory space of the processor.

File size: 45.1 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Interpret.ma: Operational semantics for the 8051/8052 processor.           *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5include "basics/russell.ma".
6
7include "ASM/ASM.ma". (* includes "ASM/BitVectorTrie.ma".*)
8include "ASM/Arithmetic.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
253lemma clock_set_8051_sfr:
254    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀i,b.
255        clock … code_memory s = clock … code_memory (set_8051_sfr M code_memory s i b).
256  #M #code_memory #s #i #b //
257qed.
258
259definition set_8052_sfr ≝
260  λM: Type[0].
261  λcode_memory:M.
262  λs: PreStatus M code_memory.
263  λi: SFR8052.
264  λb: Byte.
265    let index ≝ sfr_8052_index i in
266    let old_low_internal_ram ≝ low_internal_ram ?? s in
267    let old_high_internal_ram ≝ high_internal_ram ?? s in
268    let old_external_ram ≝ external_ram ?? s in
269    let old_program_counter ≝ program_counter ?? s in
270    let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
271    let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
272    let new_special_function_registers_8052 ≝
273      set_index Byte 5 old_special_function_registers_8052 index b ? in
274    let old_p1_latch ≝ p1_latch ?? s in
275    let old_p3_latch ≝ p3_latch ?? s in
276    let old_clock ≝ clock ?? s in
277      mk_PreStatus M code_memory
278                old_low_internal_ram
279                old_high_internal_ram
280                old_external_ram
281                old_program_counter
282                old_special_function_registers_8051
283                new_special_function_registers_8052
284                old_p1_latch
285                old_p3_latch
286                old_clock.
287    @ (sfr8052_index_5 i)
288qed.
289
290lemma clock_set_8052_sfr:
291    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀i,b.
292        clock … code_memory s = clock … code_memory (set_8052_sfr M code_memory s i b).
293  #M #code_memory #s #i #b //
294qed.
295
296definition set_program_counter ≝
297  λM: Type[0].
298  λcode_memory:M.
299  λs: PreStatus M code_memory.
300  λw: Word.
301    let old_low_internal_ram ≝ low_internal_ram ?? s in
302    let old_high_internal_ram ≝ high_internal_ram ?? s in
303    let old_external_ram ≝ external_ram ?? s in
304    let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
305    let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
306    let old_p1_latch ≝ p1_latch ?? s in
307    let old_p3_latch ≝ p3_latch ?? s in
308    let old_clock ≝ clock ?? s in
309      mk_PreStatus M code_memory
310                old_low_internal_ram
311                old_high_internal_ram
312                old_external_ram
313                w
314                old_special_function_registers_8051
315                old_special_function_registers_8052
316                old_p1_latch
317                old_p3_latch
318                old_clock.
319               
320definition set_code_memory ≝
321  λM,M': Type[0].
322  λcode_memory:M.
323  λs: PreStatus M code_memory.
324  λr: M'.
325    let old_low_internal_ram ≝ low_internal_ram ?? s in
326    let old_high_internal_ram ≝ high_internal_ram ?? s in
327    let old_external_ram ≝ external_ram ?? s in
328    let old_program_counter ≝ program_counter ?? s in
329    let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
330    let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
331    let old_p1_latch ≝ p1_latch ?? s in
332    let old_p3_latch ≝ p3_latch ?? s in
333    let old_clock ≝ clock ?? s in
334      mk_PreStatus M' r
335                old_low_internal_ram
336                old_high_internal_ram
337                old_external_ram
338                old_program_counter
339                old_special_function_registers_8051
340                old_special_function_registers_8052
341                old_p1_latch
342                old_p3_latch
343                old_clock.
344               
345definition set_low_internal_ram ≝
346  λM: Type[0].
347  λcode_memory:M.
348  λs: PreStatus M code_memory.
349  λr: BitVectorTrie Byte 7.
350    let old_high_internal_ram ≝ high_internal_ram ?? s in
351    let old_external_ram ≝ external_ram ?? s in
352    let old_program_counter ≝ program_counter ?? s in
353    let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
354    let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
355    let old_p1_latch ≝ p1_latch ?? s in
356    let old_p3_latch ≝ p3_latch ?? s in
357    let old_clock ≝ clock ?? s in
358      mk_PreStatus M code_memory
359                r
360                old_high_internal_ram
361                old_external_ram
362                old_program_counter
363                old_special_function_registers_8051
364                old_special_function_registers_8052
365                old_p1_latch
366                old_p3_latch
367                old_clock.
368               
369definition update_low_internal_ram ≝
370  λM: Type[0].
371  λcode_memory:M.
372  λs: PreStatus M code_memory.
373  λaddr,v.
374  let old_low_internal_ram ≝ low_internal_ram ?? s in
375  let new_low_internal_ram ≝ insert ?? addr v old_low_internal_ram in
376      set_low_internal_ram … s new_low_internal_ram.
377           
378lemma clock_set_low_internal_ram:
379    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀r.
380        clock … code_memory s = clock … code_memory (set_low_internal_ram M code_memory s r).
381  #M #code_memory #s #r //
382qed.
383
384lemma clock_update_low_internal_ram:
385    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀addr,v.
386        clock … code_memory s = clock … code_memory (update_low_internal_ram M code_memory s addr v).
387  #M #code_memory #s #addr #v //
388qed.
389
390definition set_high_internal_ram ≝
391  λM: Type[0].
392  λcode_memory:M.
393  λs: PreStatus M code_memory.
394  λr: BitVectorTrie Byte 7.
395    let old_low_internal_ram ≝ low_internal_ram ?? s in
396    let old_high_internal_ram ≝ high_internal_ram ?? s in
397    let old_external_ram ≝ external_ram ?? s in
398    let old_program_counter ≝ program_counter ?? s in
399    let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
400    let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
401    let old_p1_latch ≝ p1_latch ?? s in
402    let old_p3_latch ≝ p3_latch ?? s in
403    let old_clock ≝ clock ?? s in
404      mk_PreStatus M code_memory
405                old_low_internal_ram
406                r
407                old_external_ram
408                old_program_counter
409                old_special_function_registers_8051
410                old_special_function_registers_8052
411                old_p1_latch
412                old_p3_latch
413                old_clock.
414               
415definition update_high_internal_ram ≝
416  λM: Type[0].
417  λcode_memory:M.
418  λs: PreStatus M code_memory.
419  λaddr,v.
420  let old_high_internal_ram ≝ high_internal_ram ?? s in
421  let new_high_internal_ram ≝ insert ?? addr v old_high_internal_ram in
422      set_high_internal_ram … s new_high_internal_ram.
423
424lemma clock_set_high_internal_ram:
425    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀r: BitVectorTrie Byte 7.
426        clock … code_memory s = clock … code_memory (set_high_internal_ram M code_memory s r).
427  #M #code_memory #s #r //
428qed.
429
430lemma clock_update_high_internal_ram:
431    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀addr,v.
432        clock … code_memory s = clock … code_memory (update_high_internal_ram M code_memory s addr v).
433  #M #code_memory #s #addr #v //
434qed.
435
436definition set_external_ram ≝
437  λM: Type[0].
438  λcode_memory:M.
439  λs: PreStatus M code_memory.
440  λr: BitVectorTrie Byte 16.
441    let old_low_internal_ram ≝ low_internal_ram ?? s in
442    let old_high_internal_ram ≝ high_internal_ram ?? s in
443    let old_program_counter ≝ program_counter ?? s in
444    let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in
445    let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in
446    let old_p1_latch ≝ p1_latch ?? s in
447    let old_p3_latch ≝ p3_latch ?? s in
448    let old_clock ≝ clock ?? s in
449      mk_PreStatus M code_memory
450                old_low_internal_ram
451                old_high_internal_ram
452                r
453                old_program_counter
454                old_special_function_registers_8051
455                old_special_function_registers_8052
456                old_p1_latch
457                old_p3_latch
458                old_clock.
459               
460definition update_external_ram ≝
461  λM: Type[0].
462  λcode_memory:M.
463  λs: PreStatus M code_memory.
464  λaddr,v.
465  let old_external_ram ≝ external_ram ?? s in
466  let new_external_ram ≝ insert ?? addr v old_external_ram in
467      set_external_ram … s new_external_ram.
468
469lemma clock_set_external_ram:
470    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀r: BitVectorTrie Byte 16.
471        clock … code_memory s = clock … code_memory (set_external_ram M code_memory s r).
472  #M #code_memory #s #r //
473qed.
474
475lemma clock_update_external_ram:
476    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀addr: Word. ∀v: Byte.
477        clock … code_memory s = clock … code_memory (update_external_ram M code_memory s addr v).
478  #M #code_memory #s #addr #v //
479qed.
480
481definition get_psw_flags ≝
482  λM: Type[0].
483  λcode_memory:M.
484  λs: PreStatus M code_memory.
485  λflag.
486  λflag_ok: flag < ?.       
487    let psw ≝ get_8051_sfr … s SFR_PSW in
488      get_index_v bool ? psw flag flag_ok.
489               
490definition get_cy_flag ≝
491  λM: Type[0].
492  λcode_memory:M.
493  λs: PreStatus M code_memory.
494    get_psw_flags … s 0 ?. //
495qed.
496
497definition get_ac_flag ≝
498  λM: Type[0].
499  λcode_memory:M.
500  λs: PreStatus M code_memory.
501    get_psw_flags … s 1 ?. //
502qed.
503
504definition get_fo_flag ≝
505  λM: Type[0].
506  λcode_memory:M.
507  λs: PreStatus M code_memory.
508    get_psw_flags … s 2 ?. //
509qed.
510
511definition get_rs1_flag ≝
512  λM: Type[0].
513  λcode_memory:M.
514  λs: PreStatus M code_memory.
515    get_psw_flags … s 3 ?. //
516qed.
517
518definition get_rs0_flag ≝
519  λM: Type[0].
520  λcode_memory:M.
521  λs: PreStatus M code_memory.
522    get_psw_flags … s 4 ?. //
523qed.
524
525definition get_ov_flag ≝
526  λM: Type[0].
527  λcode_memory:M.
528  λs: PreStatus M code_memory.
529    get_psw_flags … s 5 ?. //
530qed.
531
532definition get_ud_flag ≝
533  λM: Type[0].
534  λcode_memory:M.
535  λs: PreStatus M code_memory.
536    get_psw_flags … s 6 ?. //
537qed.
538
539definition get_p_flag ≝
540  λM: Type[0].
541  λcode_memory:M.
542  λs: PreStatus M code_memory.
543    get_psw_flags … s 7 ?. //
544qed.
545
546definition set_flags ≝
547  λM: Type[0].
548  λcode_memory:M.
549  λs: PreStatus M code_memory.
550  λcy: Bit.
551  λac: option Bit.
552  λov: Bit.
553    (*let sfr_psw ≝ get_8051_sfr ?? s SFR_PSW in *)
554    let old_cy ≝ get_cy_flag ?? s (* get_index_v ?? sfr_psw O ?*) in
555    let old_ac ≝ get_ac_flag ?? s (* get_index_v ?? sfr_psw 1 ?*) in
556    let old_fo ≝ get_fo_flag ?? s (* get_index_v ?? sfr_psw 2 ?*) in
557    let old_rs1 ≝ get_rs1_flag ?? s (* get_index_v ?? sfr_psw 3 ?*) in
558    let old_rs0 ≝ get_rs0_flag ?? s (* get_index_v ?? sfr_psw 4 ?*) in
559    let old_ov ≝ get_ov_flag ?? s (* get_index_v ?? sfr_psw 5 ?*) in
560    let old_ud ≝ get_ud_flag ?? s (* get_index_v ?? sfr_psw 6 ?*) in
561    let old_p ≝ get_p_flag ?? s (* get_index_v ?? sfr_psw 7 ?*) in
562    let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
563      set_8051_sfr ?? s SFR_PSW
564      [[ cy ; new_ac ; old_fo ; old_rs1 ;
565         old_rs0 ; ov ; old_ud ; old_p ]].
566
567definition initialise_status ≝
568  λM: Type[0].
569  λcode_mem: M.
570  let status ≝ mk_PreStatus M code_mem                 (* Code mem. *)
571                         (Stub …)                      (* Low mem.  *)
572                         (Stub …)                      (* High mem. *)
573                         (Stub …)                      (* Ext mem.  *)
574                         (zero ?)                      (* PC.       *)
575                         (replicate … (zero ?))        (* 8051 SFR. *)
576                         (replicate … (zero ?))        (* 8052 SFR. *)
577                         (zero ?)                      (* P1 latch. *)
578                         (zero ?)                      (* P3 latch. *)
579                         O                             (* Clock.    *)
580  in
581    set_8051_sfr ?? status SFR_SP (bitvector_of_nat ? 7).
582 
583definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝
584  λb: Byte.
585    let address ≝ nat_of_bitvector … b in
586      if (eqb address 128) then None ?
587      else if (eqb address 144) then Some … (inl … SFR_P1)
588      else if (eqb address 160) then None ?
589      else if (eqb address 176) then Some … (inl … SFR_P3)
590      else if (eqb address 153) then Some … (inl … SFR_SBUF)
591      else if (eqb address 138) then Some … (inl … SFR_TL0)
592      else if (eqb address 139) then Some … (inl … SFR_TL1)
593      else if (eqb address 140) then Some … (inl … SFR_TH0)
594      else if (eqb address 141) then Some … (inl … SFR_TH1)
595      else if (eqb address 200) then Some … (inr … SFR_T2CON)
596      else if (eqb address 202) then Some … (inr … SFR_RCAP2L)
597      else if (eqb address 203) then Some … (inr … SFR_RCAP2H)
598      else if (eqb address 204) then Some … (inr … SFR_TL2)
599      else if (eqb address 205) then Some … (inr … SFR_TH2)
600      else if (eqb address 135) then Some … (inl … SFR_PCON)
601      else if (eqb address 136) then Some … (inl … SFR_TCON)
602      else if (eqb address 137) then Some … (inl … SFR_TMOD)
603      else if (eqb address 152) then Some … (inl … SFR_SCON)
604      else if (eqb address 168) then Some … (inl … SFR_IE)
605      else if (eqb address 184) then Some … (inl … SFR_IP)
606      else if (eqb address 129) then Some … (inl … SFR_SP)
607      else if (eqb address 130) then Some … (inl … SFR_DPL)
608      else if (eqb address 131) then Some … (inl … SFR_DPH)
609      else if (eqb address 208) then Some … (inl … SFR_PSW)
610      else if (eqb address 224) then Some … (inl … SFR_ACC_A)
611      else if (eqb address 240) then Some … (inl … SFR_ACC_B)
612      else None ?.
613
614definition get_bit_addressable_sfr:
615    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝
616  λM: Type[0].
617  λcode_memory:M.
618  λs: PreStatus M code_memory.
619  λb: Byte.
620  λl: bool.
621  match sfr_of_Byte b with
622  [ None ⇒ match not_implemented in False with [ ]
623  | Some sfr8051_8052 ⇒
624    match sfr8051_8052 with
625    [ inl sfr ⇒
626      match sfr with
627      [ SFR_P1 ⇒
628        if l then
629          p1_latch … s
630        else
631          get_8051_sfr … s SFR_P1
632      | SFR_P3 ⇒
633        if l then
634          p3_latch … s
635        else
636          get_8051_sfr … s SFR_P3
637      | _ ⇒ get_8051_sfr … s sfr
638      ]
639    | inr sfr ⇒ get_8052_sfr M code_memory s sfr
640    ]
641  ].
642
643definition set_bit_addressable_sfr:
644    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → PreStatus M code_memory ≝
645  λM: Type[0].
646  λcode_memory:M.
647  λs: PreStatus M code_memory.
648  λb: Byte.
649  λv: Byte.
650   match sfr_of_Byte b with
651   [ None ⇒ match not_implemented in False with [ ]
652   | Some sfr8051_8052 ⇒
653      match sfr8051_8052 with
654      [ inl sfr ⇒
655         match sfr with
656         [ SFR_P1 ⇒
657           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
658           set_p1_latch ?? s v
659         | SFR_P3 ⇒
660           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
661           set_p3_latch ?? s v
662         | _ ⇒ set_8051_sfr ?? s sfr v ]
663      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]].
664
665lemma clock_set_bit_addressable_sfr:
666    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte.
667        clock … code_memory s = clock … code_memory (set_bit_addressable_sfr M code_memory s b v).
668  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
669  cases (sfr_of_Byte ?)
670  [1:
671    normalize nodelta cases not_implemented
672  |2:
673    * * %
674  ]
675qed.
676
677lemma program_counter_set_bit_addressable_sfr:
678    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte.
679        program_counter … code_memory s = program_counter … code_memory (set_bit_addressable_sfr M code_memory s b v).
680  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
681  cases (sfr_of_Byte ?)
682  [1:
683    normalize nodelta cases not_implemented
684  |2:
685    * * %
686  ]
687qed.
688
689definition bit_address_of_register ≝
690  λM: Type[0].
691  λcode_memory:M.
692  λs: PreStatus M code_memory.
693  λr: BitVector 3.
694    let b ≝ get_index_v … r O ? in
695    let c ≝ get_index_v … r 1 ? in
696    let d ≝ get_index_v … r 2 ? in
697(* JHM: redundant bit-twiddling, once you have get_*_flag helpers
698    let 〈 un, ln 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
699    let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in
700*)
701    let r1 ≝ get_rs1_flag ?? s in
702    let r0 ≝ get_rs0_flag ?? s in
703    let offset ≝
704      if ¬r1 ∧ ¬r0 then
705        O
706      else if ¬r1 ∧ r0 then
707        8
708      else if r1 ∧ r0 then
709        24
710      else
711        16
712    in
713      bitvector_of_nat 7 (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
714  //
715qed.
716
717definition get_register ≝
718  λM: Type[0].
719  λcode_memory:M.
720  λs: PreStatus M code_memory.
721  λr: BitVector 3.
722    let address ≝ bit_address_of_register … s r in
723      lookup ?? address (low_internal_ram … s) (zero ?).
724
725definition set_register ≝
726  λM: Type[0].
727  λcode_memory:M.
728  λs: PreStatus M code_memory.
729  λr: BitVector 3.
730  λv: Byte.
731    let address ≝ bit_address_of_register … s r in
732    (*     
733    let old_low_internal_ram ≝ low_internal_ram ?? s in
734    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
735      set_low_internal_ram … s new_low_internal_ram.
736    *)
737    update_low_internal_ram … s address v.
738     
739definition read_from_external_ram ≝
740  λM: Type[0].
741  λcode_memory:M.
742  λs: PreStatus M code_memory.
743  λaddr: Word.
744    lookup ?? addr (external_ram … s) (zero ?).
745
746definition read_from_internal_ram ≝ (* JHM: lots of 7bits+HI/Lo vs. 8bit redundancy throughout *)
747  λM: Type[0].
748  λcode_memory:M.
749  λs: PreStatus M code_memory.
750  λaddr: Byte.
751    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
752    let memory ≝
753      if head' … bit_one then
754        (high_internal_ram ?? s)
755      else
756        (low_internal_ram ?? s)
757    in
758      lookup … seven_bits memory (zero ?).
759
760definition read_at_stack_pointer ≝
761  λM: Type[0].
762  λcode_memory:M.
763  λs: PreStatus M code_memory.
764    read_from_internal_ram … s (get_8051_sfr ?? s SFR_SP).
765
766definition write_at_stack_pointer ≝
767  λM: Type[0].
768  λcode_memory:M.
769  λs: PreStatus M code_memory.
770  λv: Byte.
771    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr ?? s SFR_SP) in
772      if head' … bit_one then
773      (*
774        let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
775          set_high_internal_ram ?? s memory
776      *)
777        update_high_internal_ram … s seven_bits v
778      else
779      (*
780        let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
781          set_low_internal_ram ?? s memory.
782      *)
783        update_low_internal_ram … s seven_bits v.
784
785definition 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' ≝
786  λM,code_memory,s,v,a.
787   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M ? s = clock M ? s' with
788     [ DPTR ⇒ λ_:True.
789       let 〈 bu, bl 〉 ≝ vsplit … 8 8 v in
790       let status ≝ set_8051_sfr … s SFR_DPH bu in
791       let status ≝ set_8051_sfr … status SFR_DPL bl in
792         status
793     | _ ⇒ λK.
794       match K in False with
795       [
796       ]
797     ] (subaddressing_modein … a).
798 //
799qed.
800
801definition set_arg_16: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → PreStatus M code_memory ≝
802 set_arg_16'.
803
804lemma set_arg_16_ok: ∀M,cm,s,v,x. clock M cm s = clock M cm (set_arg_16 M cm s v x).
805 #M #cm #s #x #v whd in match set_arg_16; normalize nodelta @pi2
806qed.
807
808definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory →
809  [[ data16 ; acc_dptr ]] → Word ≝
810  λm, cm, s, a.
811    match a return λx. bool_to_Prop (is_in ? [[ data16 ; acc_dptr ]] x) → ? with
812      [ DATA16 d ⇒ λ_:True. d
813      | ACC_DPTR ⇒ λ_:True.
814        let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
815        let big_acc ≝ (zero ?) @@ (get_8051_sfr … s SFR_ACC_A) in
816        add … big_acc dptr
817      | _ ⇒ Ⓧ
818      ] (subaddressing_modein … a).
819     
820definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ;
821                                          acc_a ; acc_b ; data ; acc_dptr ;
822                                          acc_pc ; ext_indirect ;
823                                          ext_indirect_dptr ]] → Byte ≝
824  λm, cm, s, l, a.
825    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
826                                                acc_a ; acc_b ; data ; acc_dptr ;
827                                                acc_pc ; ext_indirect ;
828                                                ext_indirect_dptr ]] x) → ? with
829      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
830      | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
831      | DATA d ⇒ λdata: True. d
832      | REGISTER r ⇒ λregister: True. get_register ?? s r
833      | EXT_INDIRECT_DPTR ⇒
834        λext_indirect_dptr: True.
835          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
836            read_from_external_ram … s address
837      | EXT_INDIRECT e ⇒
838        λext_indirect: True.
839          let address ≝ get_register ?? s [[ false; false; e ]]  in
840          let padded_address ≝ pad 8 ? address in
841            read_from_external_ram … s padded_address
842      | ACC_DPTR ⇒
843        λacc_dptr: True.
844          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
845          let padded_acc ≝ pad 8 ? (get_8051_sfr ?? s SFR_ACC_A) in
846          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
847            read_from_external_ram … s address
848      | ACC_PC ⇒
849        λacc_pc: True.
850          let padded_acc ≝ pad 8 ? (get_8051_sfr ?? s SFR_ACC_A) in
851          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
852            read_from_external_ram … s address
853      | DIRECT d ⇒ (* JHM: simplify false branch with read_from_internal_ram *)
854        λdirect: True.
855          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
856            match head' … hd with
857            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
858             (* XXX: get_bit_addressable_sfr m cm s d l *)
859            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero ?)
860             (* XXX: read_from_internal_ram … s d *)
861            ]
862      | INDIRECT i ⇒ (* JHM: simplify completely with read_from_internal_ram *)
863        λindirect: True.
864          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
865            match head' … hd with
866            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero ?)
867            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero ?)
868            ]
869          (* XXX: read_from_internal_ram … s (get_register … s [[false;false;i]]) *)
870      | _ ⇒ λother.
871        match other in False with [ ]
872      ] (subaddressing_modein … a).
873
874definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
875                                   acc_a ; acc_b ; ext_indirect ;
876                                   ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝
877  λm, cm, s, a, v.
878    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
879                                                acc_a ; acc_b ; ext_indirect ;
880                                                ext_indirect_dptr ]] x) →
881                   PreStatus m cm
882            with
883      [ DIRECT d ⇒ (* JHM: should simplify false branch with update_internal_ram *)
884        λdirect: True.
885          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
886            match head' … bit_one with
887              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
888              | false ⇒ update_low_internal_ram … s seven_bits v
889                (*let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
890                  set_low_internal_ram ?? s memory*)
891              ]
892      | INDIRECT i ⇒ (* JHM: should simplify completely with update_internal_ram *)
893        λindirect: True.
894          let register ≝ get_register ?? s [[ false; false; i ]] in
895          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
896            match head' … bit_one with
897              [ false ⇒ update_low_internal_ram … s seven_bits v
898                (*let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
899                  set_low_internal_ram ?? s memory*)
900              | true ⇒ update_high_internal_ram … s seven_bits v
901                (*let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
902                  set_high_internal_ram ?? s memory*)
903              ]
904      | REGISTER r ⇒ λregister: True. set_register ?? s r v
905      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
906      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
907      | EXT_INDIRECT e ⇒
908        λext_indirect: True.
909          let address ≝ get_register ?? s [[ false; false; e ]] in
910          let padded_address ≝ pad 8 8 address in
911          (*
912          let memory ≝ insert ?? padded_address v (external_ram ?? s) in
913            set_external_ram ?? s memory
914          *)
915          update_external_ram … s padded_address v
916      | EXT_INDIRECT_DPTR ⇒
917        λext_indirect_dptr: True.
918          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
919          (*
920          let memory ≝ insert ?? address v (external_ram ?? s) in
921            set_external_ram ?? s memory
922          *)
923          update_external_ram … s address v
924      | _ ⇒
925        λother: False.
926          match other in False with [ ]
927      ] (subaddressing_modein … a).
928
929lemma clock_set_arg_8: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v) ≝
930  λm, cm, s, a, v.
931    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
932                                                acc_a ; acc_b ; ext_indirect ;
933                                                ext_indirect_dptr ]] x) →
934                   clock … cm s = clock … cm (set_arg_8 … s x v)
935            with
936      [ DIRECT d ⇒ (* JHM: should simplify false branch with update_internal_ram *)
937        λdirect: True.
938          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
939            match head' … bit_one with
940              [ true ⇒ ?
941              | false ⇒ ?
942              ]
943      | INDIRECT i ⇒ (* JHM: should simplify completely with update_internal_ram *)
944        λindirect: True.
945          let register ≝ get_register ?? s [[ false; false; i ]] in
946          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
947            match head' … bit_one with
948              [ false ⇒ ?
949              | true ⇒ ?
950              ]
951      | REGISTER r ⇒ λregister: True. ?
952      | ACC_A ⇒ λacc_a: True. ?
953      | ACC_B ⇒ λacc_b: True. ?
954      | EXT_INDIRECT e ⇒
955        λext_indirect: True.
956          let address ≝ get_register ?? s [[ false; false; e ]] in
957          let padded_address ≝ pad 8 8 address in
958            ?
959      | EXT_INDIRECT_DPTR ⇒
960        λext_indirect_dptr: True.
961          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
962            ?
963      | _ ⇒
964        λother: False.
965          match other in False with [ ]
966      ] (subaddressing_modein … a).
967  //
968  whd in match set_arg_8; normalize nodelta
969(* XXX: non-Russell way
970  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
971    cases x * normalize nodelta
972  [1: #d #ok cases (vsplit ? 1 7 d) normalize nodelta
973    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta
974    [1: @clock_set_bit_addressable_sfr
975    |2: @clock_update_low_internal_ram
976    ]
977  |2: #i #ok cases (vsplit ? 1 7 (get_register ?? s [[ false; false; i ]])) normalize nodelta
978    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta
979    [1: @clock_update_high_internal_ram
980    |2: @clock_update_low_internal_ram
981    ]
982  |3: #b1 #ok @clock_update_external_ram
983  |4: #b3 #ok @clock_update_low_internal_ram
984  |5,6: #ok @clock_set_8051_sfr
985  |12: #ok @clock_update_external_ram
986  ]
987  cases not_implemented (* JHM: there has to be a better way to deal with the absurd branches *)
988*)
989  [1: (* case DIRECT d *)
990    cases (vsplit ? 1 7 d) normalize nodelta
991    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta //
992  |2: (* case DIRECT d; why the repetition? *)
993    cases (vsplit ? 1 7 d) normalize nodelta
994    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta //
995  |3: (* case INDIRECT i *)
996    cases (vsplit ? 1 7 (get_register ?? s [[ false; false; i ]])) normalize nodelta
997    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta //
998   |4: (* case INDIRECT i; why the repetition? *)
999    cases (vsplit ? 1 7 (get_register ?? s [[ false; false; i ]])) normalize nodelta
1000    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta //
1001  ]
1002qed.
1003
1004(* XXX: these --- like those above --- belong in StatusProofs*.ma ??? *)
1005lemma 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).
1006  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
1007  cases daemon
1008qed.
1009
1010lemma 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).
1011  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
1012  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
1013  cases daemon
1014qed.
1015
1016lemma 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).
1017  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
1018  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
1019  cases daemon
1020qed.
1021
1022lemma 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).
1023  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
1024  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
1025  cases daemon
1026qed.
1027
1028theorem modulus_less_than:
1029  ∀m,n: nat. (m mod (S n)) < S n.
1030  #n #m
1031  normalize
1032  @ le_S_S
1033  lapply (le_n n)
1034  generalize in ⊢ (?%? → ?(??%?)?);
1035  elim n in ⊢ (∀_:?. ??% → ?(?%??)?);
1036  [ normalize
1037    #n
1038    @ (less_than_or_equal_b_elim n m)
1039    normalize
1040    [ //
1041    | #H #K
1042      @(le_inv_ind ?? K …)
1043      [ # H1
1044        < H1
1045        //
1046      | #x #H1 #H2 #H3
1047        destruct
1048      ]
1049    ]
1050  | normalize
1051    # y # H1 # n # H2
1052    @ (less_than_or_equal_b_elim n m)
1053    normalize
1054    [ //
1055    | # K
1056      @ H1
1057      cut (n ≤ S y → n - S m ≤ y)
1058      /2 by/
1059      cases n
1060      normalize
1061      //
1062      # x # K1
1063      lapply (le_S_S_to_le … K1)
1064      generalize in match m;
1065      elim x
1066      normalize
1067      //
1068      # w1 # H # m
1069      cases m
1070      normalize
1071      //
1072      # q # K2
1073      @H
1074      /3/
1075    ]
1076  ]
1077qed.
1078
1079definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] →
1080                       bool → bool ≝
1081  λm, cm, s, a, l.
1082    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
1083                                                 n_bit_addr ;
1084                                                 carry ]] x) → ? with
1085      [ BIT_ADDR b ⇒
1086        λbit_addr: True.
1087        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1088        let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1089        match head' … bit_1 with
1090        [ true ⇒
1091          let trans ≝ true:::four_bits @@ [[false; false; false]] in
1092          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
1093            get_index_v … sfr (nat_of_bitvector … three_bits) ?
1094        | false ⇒
1095          let address' ≝ [[true; false; false]]@@four_bits in
1096          let t ≝ lookup ?? address' (low_internal_ram ?? s) (zero ?) in
1097            get_index_v … t (nat_of_bitvector … three_bits) ?
1098        ]
1099      | N_BIT_ADDR n ⇒
1100        λn_bit_addr: True.
1101        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
1102        let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1103        match head' … bit_1 with
1104        [ true ⇒
1105          let trans ≝ true:::four_bits @@ [[false; false; false]] in
1106          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
1107            ¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?)
1108        | false ⇒
1109          let address' ≝ [[true; false; false]]@@four_bits in
1110          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1111            ¬(get_index_v … t (nat_of_bitvector … three_bits) ?)
1112        ]
1113      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
1114      | _ ⇒ λother.
1115        match other in False with [ ]
1116      ] (subaddressing_modein … a).
1117  //
1118qed.
1119     
1120definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝
1121  λm: Type[0].
1122  λcm.
1123  λs: PreStatus m cm.
1124  λa: [[bit_addr; carry]].
1125  λv: Bit.
1126    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ? with
1127      [ BIT_ADDR b ⇒ λbit_addr: True.
1128        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
1129        let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1130        match head' … bit_1 with
1131        [ true ⇒
1132          let trans ≝ true:::four_bits @@ [[false; false; false]] in
1133          let sfr ≝ get_bit_addressable_sfr … s trans true in
1134          let new_sfr ≝ set_index … sfr (nat_of_bitvector … three_bits) v ? in
1135            set_bit_addressable_sfr … s new_sfr trans
1136        | false ⇒
1137          let address' ≝ [[true; false; false]]@@four_bits in
1138          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero ?) in
1139          let n_bit ≝ set_index … t (nat_of_bitvector … three_bits) v ? in
1140          (*
1141          let memory ≝ insert ?? address' n_bit (low_internal_ram ?? s) in
1142            set_low_internal_ram … s memory
1143          *)
1144            update_low_internal_ram … s address' n_bit
1145        ]
1146      | CARRY ⇒
1147        λcarry: True.
1148        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1149        let new_psw ≝ v:::seven_bits in
1150          set_8051_sfr ?? s SFR_PSW new_psw
1151      | _ ⇒
1152        λother: False.
1153          match other in False with
1154            [ ]
1155      ] (subaddressing_modein … a).
1156  //
1157qed.
1158
1159(* JHM: Russell-style works, modulo some oddities...??? *)
1160lemma clock_set_arg_1: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v)
1161  ≝
1162  λm: Type[0].
1163  λcm.
1164  λs: PreStatus m cm.
1165  λa: [[bit_addr; carry]].
1166  λv: Bit.     
1167    match a
1168    return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) →
1169     clock m cm s = clock … (set_arg_1 m cm s x v)
1170    with
1171      [ BIT_ADDR b ⇒ λbit_addr: True.
1172        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
1173        let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1174        match head' … bit_1 with
1175        [ true ⇒
1176          let trans ≝ true:::four_bits @@ [[false; false; false]] in
1177          let sfr ≝ get_bit_addressable_sfr … s trans true in
1178          let new_sfr ≝ set_index … sfr (nat_of_bitvector … three_bits) v ? in
1179            ?
1180        | false ⇒
1181          let address' ≝ [[true; false; false]]@@four_bits in
1182          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1183          let n_bit ≝ set_index … t (nat_of_bitvector … three_bits) v ? in
1184            ?
1185        ]
1186      | CARRY ⇒
1187        λcarry: True.
1188        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1189        let new_psw ≝ v:::seven_bits in
1190          ?
1191      | _ ⇒
1192        λother: False.
1193          match other in False with
1194            [ ]
1195      ] (subaddressing_modein … a). //
1196      whd in match set_arg_1; normalize nodelta     
1197  [1: (* case: CARRY *)
1198    cases (vsplit bool 1 7 (get_8051_sfr … s SFR_PSW))
1199    #ignore #seven_bits normalize nodelta @clock_set_8051_sfr
1200  |2: (* case: BIT_ADDR *)
1201    cases (vsplit bool 1 7 b)
1202    #bit_1 #seven_bits normalize nodelta cases (vsplit bool 4 3 seven_bits)
1203    #four_bits #three_bits normalize nodelta cases (head' … bit_1)
1204    [1: @clock_set_bit_addressable_sfr
1205    |2: @clock_update_low_internal_ram
1206    ]
1207  |3: (* case: BIT_ADDR, again; why? *)
1208    cases (vsplit bool 1 7 b)
1209    #bit_1 #seven_bits normalize nodelta cases (vsplit bool 4 3 seven_bits)
1210    #four_bits #three_bits normalize nodelta cases (head' … bit_1)
1211    [1: @clock_set_bit_addressable_sfr
1212    |2: @clock_update_low_internal_ram
1213    ]
1214  ]
1215qed.
1216
1217lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v).
1218(* JHM: boring, non-Russell way
1219  #m #cm #s #x #v whd in match set_arg_1;
1220  cases x * normalize nodelta
1221  [14: #ok cases (vsplit bool 1 7 (get_8051_sfr … s SFR_PSW))
1222    #ignore #seven_bits @clock_set_8051_sfr
1223  |15: #b #ok cases (vsplit bool 1 7 b)
1224    #bit_1 #seven_bits normalize nodelta cases (vsplit bool 4 3 seven_bits)
1225    #four_bits #three_bits normalize nodelta cases (head' … bit_1)
1226    [1: @clock_set_bit_addressable_sfr
1227    |2: @clock_set_low_internal_ram
1228    ]
1229  ] cases not_implemented (* XXX: there has to be a better way to deal with the absurd branches *)
1230*)
1231  @clock_set_arg_1
1232qed.
1233
1234
1235definition construct_datalabels: list (Identifier × Word) →
1236  identifier_map ASMTag Word ≝
1237  λthe_preamble.
1238  \fst (foldl ?? (λt,preamble.
1239      let 〈datalabels, addr〉 ≝ t in
1240      let 〈name, size〉 ≝ preamble in
1241      let 〈addr, carry〉 ≝ sub_16_with_carry addr size false in
1242      〈add ?? datalabels name addr, addr〉)
1243    (* mcu8051ide disallows XDATA access at -1, bug or feature? *)
1244    〈empty_map …, maximum …〉 the_preamble).
Note: See TracBrowser for help on using the repository browser.