source: Deliverables/D4.1/Matita/Status.ma @ 352

Last change on this file since 352 was 352, checked in by mulligan, 10 years ago

Do not use ndestruct for injectivity since it introduces StreickerK that
blocks reductions.

File size: 38.3 KB
RevLine 
[257]1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Interpret.ma: Operational semantics for the 8051/8052 processor.           *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
[314]5include "ASM.ma".
[259]6include "Arithmetic.ma".
[257]7include "BitVectorTrie.ma".
8
[276]9ndefinition Time ≝ Nat.
10
11ninductive SerialBufferType: Type[0] ≝
12  Eight: Byte → SerialBufferType
13| Nine: Bit → Byte → SerialBufferType.
14
15ninductive LineType: Type[0] ≝
16  P1: Byte → LineType
17| P3: Byte → LineType
18| SerialBuffer: SerialBufferType → LineType.
19
20(* What is a continuation, now? *)
21
[257]22ninductive SFR8051: Type[0] ≝
23  SFR_SP: SFR8051
24| SFR_DPL: SFR8051
25| SFR_DPH: SFR8051
26| SFR_PCON: SFR8051
27| SFR_TCON: SFR8051
28| SFR_TMOD: SFR8051
29| SFR_TL0: SFR8051
30| SFR_TL1: SFR8051
31| SFR_TH0: SFR8051
32| SFR_TH1: SFR8051
33| SFR_P1: SFR8051
34| SFR_SCON: SFR8051
35| SFR_SBUF: SFR8051
36| SFR_IE: SFR8051
37| SFR_P3: SFR8051
38| SFR_IP: SFR8051
39| SFR_PSW: SFR8051
40| SFR_ACC_A: SFR8051
41| SFR_ACC_B: SFR8051.
42
43ndefinition sfr_8051_index ≝
44  λs: SFR8051.
45    match s with
46      [ SFR_SP ⇒ Z
47      | SFR_DPL ⇒ S Z
48      | SFR_DPH ⇒ two
49      | SFR_PCON ⇒ three
50      | SFR_TCON ⇒ four
51      | SFR_TMOD ⇒ five
52      | SFR_TL0 ⇒ six
53      | SFR_TL1 ⇒ seven
54      | SFR_TH0 ⇒ eight
55      | SFR_TH1 ⇒ nine
56      | SFR_P1 ⇒ ten
57      | SFR_SCON ⇒ eleven
58      | SFR_SBUF ⇒ twelve
59      | SFR_IE ⇒ thirteen
60      | SFR_P3 ⇒ fourteen
61      | SFR_IP ⇒ fifteen
62      | SFR_PSW ⇒ sixteen
63      | SFR_ACC_A ⇒ seventeen
64      | SFR_ACC_B ⇒ eighteen
65      ].
66     
67ninductive SFR8052: Type[0] ≝
68   SFR_T2CON: SFR8052
69|  SFR_RCAP2L: SFR8052
70|  SFR_RCAP2H: SFR8052
71|  SFR_TL2: SFR8052
72|  SFR_TH2: SFR8052.
73
74ndefinition sfr_8052_index ≝
75  λs: SFR8052.
76    match s with
77      [ SFR_T2CON ⇒ Z
78      | SFR_RCAP2L ⇒ S Z
79      | SFR_RCAP2H ⇒ two
80      | SFR_TL2 ⇒ three
81      | SFR_TH2 ⇒ four
82      ].
83
84(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
85(* Processor status.                                                          *)
86(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
87nrecord Status: Type[0] ≝
88{
89  code_memory: BitVectorTrie Byte sixteen;
90  low_internal_ram: BitVectorTrie Byte seven;
91  high_internal_ram: BitVectorTrie Byte seven;
92  external_ram: BitVectorTrie Byte sixteen;
93 
94  program_counter: Word;
95 
96  special_function_registers_8051: Vector Byte nineteen;
[281]97  special_function_registers_8052: Vector Byte five;
98 
99  p1_latch: Byte;
[329]100  p3_latch: Byte;
101 
102  clock: Time
[257]103}.
104
[351]105nlemma sfr8051_index_nineteen:
[265]106  ∀i: SFR8051.
107    sfr_8051_index i < nineteen.
[351]108 #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone);
109 napply less_than_or_equal_zero.
110nqed.
[265]111   
[351]112nlemma sfr8052_index_five:
[265]113  ∀i: SFR8052.
114    sfr_8052_index i < five.
[351]115 #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone);
116 napply less_than_or_equal_zero.
117nqed.
[285]118   
[329]119ndefinition set_clock ≝
120  λs: Status.
121  λt: Time.
122    let old_code_memory ≝ code_memory s in
123    let old_low_internal_ram ≝ low_internal_ram s in
124    let old_high_internal_ram ≝ high_internal_ram s in
125    let old_external_ram ≝ external_ram s in
126    let old_program_counter ≝ program_counter s in
127    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
128    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
129    let old_p1_latch ≝ p1_latch s in   
130    let old_p3_latch ≝ p3_latch s in
131      mk_Status old_code_memory
132                old_low_internal_ram
133                old_high_internal_ram
134                old_external_ram
135                old_program_counter
136                old_special_function_registers_8051
137                old_special_function_registers_8052
138                old_p1_latch
139                old_p3_latch
140                t.
141   
[285]142ndefinition set_p1_latch ≝
143  λs: Status.
144  λb: Byte.
145    let old_code_memory ≝ code_memory s in
146    let old_low_internal_ram ≝ low_internal_ram s in
147    let old_high_internal_ram ≝ high_internal_ram s in
148    let old_external_ram ≝ external_ram s in
149    let old_program_counter ≝ program_counter s in
150    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
151    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
152    let old_p3_latch ≝ p3_latch s in
[329]153    let old_clock ≝ clock s in
[285]154      mk_Status old_code_memory
155                old_low_internal_ram
156                old_high_internal_ram
157                old_external_ram
158                old_program_counter
159                old_special_function_registers_8051
160                old_special_function_registers_8052
161                b
[329]162                old_p3_latch
163                old_clock.
[265]164
[285]165ndefinition set_p3_latch ≝
166  λs: Status.
167  λb: Byte.
168    let old_code_memory ≝ code_memory s in
169    let old_low_internal_ram ≝ low_internal_ram s in
170    let old_high_internal_ram ≝ high_internal_ram s in
171    let old_external_ram ≝ external_ram s in
172    let old_program_counter ≝ program_counter s in
173    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
174    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
175    let old_p1_latch ≝ p1_latch s in
[329]176    let old_clock ≝ clock s in
[285]177      mk_Status old_code_memory
178                old_low_internal_ram
179                old_high_internal_ram
180                old_external_ram
181                old_program_counter
182                old_special_function_registers_8051
183                old_special_function_registers_8052
184                old_p1_latch
[329]185                b
186                old_clock.
[285]187
[265]188ndefinition get_8051_sfr ≝
189  λs: Status.
190  λi: SFR8051.
191    let sfr ≝ special_function_registers_8051 s in
192    let index ≝ sfr_8051_index i in
[351]193      get_index ?? sfr index ?.
[265]194    napply (sfr8051_index_nineteen i).
195nqed.
196
197ndefinition get_8052_sfr ≝
198  λs: Status.
199  λi: SFR8052.
200    let sfr ≝ special_function_registers_8052 s in
201    let index ≝ sfr_8052_index i in
[351]202      get_index ?? sfr index ?.
[265]203    napply (sfr8052_index_five i).
204nqed.
205
[259]206ndefinition set_8051_sfr ≝
207  λs: Status.
208  λi: SFR8051.
209  λb: Byte.
[265]210    let index ≝ sfr_8051_index i in
211    let old_code_memory ≝ code_memory s in
212    let old_low_internal_ram ≝ low_internal_ram s in
213    let old_high_internal_ram ≝ high_internal_ram s in
214    let old_external_ram ≝ external_ram s in
215    let old_program_counter ≝ program_counter s in
216    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
217    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
218    let new_special_function_registers_8051 ≝
[351]219      set_index Byte nineteen old_special_function_registers_8051 index b ? in
[285]220    let old_p1_latch ≝ p1_latch s in
221    let old_p3_latch ≝ p3_latch s in
[329]222    let old_clock ≝ clock s in
[265]223      mk_Status old_code_memory
224                old_low_internal_ram
225                old_high_internal_ram
226                old_external_ram
227                old_program_counter
228                new_special_function_registers_8051
[285]229                old_special_function_registers_8052
230                old_p1_latch
[329]231                old_p3_latch
232                old_clock.
[265]233    napply (sfr8051_index_nineteen i).
234nqed.
[258]235
[265]236ndefinition set_8052_sfr ≝
237  λs: Status.
238  λi: SFR8052.
239  λb: Byte.
240    let index ≝ sfr_8052_index i in
241    let old_code_memory ≝ code_memory s in
242    let old_low_internal_ram ≝ low_internal_ram s in
243    let old_high_internal_ram ≝ high_internal_ram s in
244    let old_external_ram ≝ external_ram s in
245    let old_program_counter ≝ program_counter s in
246    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
247    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
248    let new_special_function_registers_8052 ≝
[351]249      set_index Byte five old_special_function_registers_8052 index b ? in
[285]250    let old_p1_latch ≝ p1_latch s in
251    let old_p3_latch ≝ p3_latch s in
[329]252    let old_clock ≝ clock s in
[265]253      mk_Status old_code_memory
254                old_low_internal_ram
255                old_high_internal_ram
256                old_external_ram
257                old_program_counter
258                old_special_function_registers_8051
[285]259                new_special_function_registers_8052
260                old_p1_latch
[329]261                old_p3_latch
262                old_clock.
[265]263    napply (sfr8052_index_five i).
264nqed.
265
266ndefinition set_program_counter ≝
267  λs: Status.
268  λw: Word.
269    let old_code_memory ≝ code_memory s in
270    let old_low_internal_ram ≝ low_internal_ram s in
271    let old_high_internal_ram ≝ high_internal_ram s in
272    let old_external_ram ≝ external_ram s in
273    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
274    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
[285]275    let old_p1_latch ≝ p1_latch s in
276    let old_p3_latch ≝ p3_latch s in
[329]277    let old_clock ≝ clock s in
[265]278      mk_Status old_code_memory
279                old_low_internal_ram
280                old_high_internal_ram
281                old_external_ram
282                w
283                old_special_function_registers_8051
[285]284                old_special_function_registers_8052
285                old_p1_latch
[329]286                old_p3_latch
287                old_clock.
[265]288               
289ndefinition set_code_memory ≝
290  λs: Status.
291  λr: BitVectorTrie Byte sixteen.
292    let old_low_internal_ram ≝ low_internal_ram s in
293    let old_high_internal_ram ≝ high_internal_ram s in
294    let old_external_ram ≝ external_ram s in
295    let old_program_counter ≝ program_counter s in
296    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
297    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
[285]298    let old_p1_latch ≝ p1_latch s in
299    let old_p3_latch ≝ p3_latch s in
[329]300    let old_clock ≝ clock s in
[265]301      mk_Status r
302                old_low_internal_ram
303                old_high_internal_ram
304                old_external_ram
305                old_program_counter
306                old_special_function_registers_8051
[285]307                old_special_function_registers_8052
308                old_p1_latch
[329]309                old_p3_latch
310                old_clock.
[265]311               
312ndefinition set_low_internal_ram ≝
313  λs: Status.
314  λr: BitVectorTrie Byte seven.
315    let old_code_memory ≝ code_memory s in
316    let old_high_internal_ram ≝ high_internal_ram s in
317    let old_external_ram ≝ external_ram s in
318    let old_program_counter ≝ program_counter s in
319    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
320    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
[285]321    let old_p1_latch ≝ p1_latch s in
322    let old_p3_latch ≝ p3_latch s in
[329]323    let old_clock ≝ clock s in
[265]324      mk_Status old_code_memory
325                r
326                old_high_internal_ram
327                old_external_ram
328                old_program_counter
329                old_special_function_registers_8051
[285]330                old_special_function_registers_8052
331                old_p1_latch
[329]332                old_p3_latch
333                old_clock.
[265]334               
[285]335ndefinition set_high_internal_ram ≝
336  λs: Status.
337  λr: BitVectorTrie Byte seven.
338    let old_code_memory ≝ code_memory s in
339    let old_low_internal_ram ≝ low_internal_ram s in
340    let old_high_internal_ram ≝ high_internal_ram s in
341    let old_external_ram ≝ external_ram s in
342    let old_program_counter ≝ program_counter s in
343    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
344    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
345    let old_p1_latch ≝ p1_latch s in
346    let old_p3_latch ≝ p3_latch s in
[329]347    let old_clock ≝ clock s in
[285]348      mk_Status old_code_memory
349                old_low_internal_ram
350                r
351                old_external_ram
352                old_program_counter
353                old_special_function_registers_8051
354                old_special_function_registers_8052
355                old_p1_latch
[329]356                old_p3_latch
357                old_clock.
[285]358               
[313]359ndefinition set_external_ram ≝
360  λs: Status.
361  λr: BitVectorTrie Byte sixteen.
362    let old_code_memory ≝ code_memory s in
363    let old_low_internal_ram ≝ low_internal_ram s in
364    let old_high_internal_ram ≝ high_internal_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
[329]370    let old_clock ≝ clock s in
[313]371      mk_Status old_code_memory
372                old_low_internal_ram
373                old_high_internal_ram
374                r
375                old_program_counter
376                old_special_function_registers_8051
377                old_special_function_registers_8052
378                old_p1_latch
[329]379                old_p3_latch
380                old_clock.
[313]381               
[265]382ndefinition get_cy_flag ≝
383  λs: Status.
384    let sfr ≝ special_function_registers_8051 s in
[267]385    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
386      get_index Bool eight psw Z ?.
387    nnormalize.
388    napply (less_than_or_equal_monotone ? ?).
389    napply (less_than_or_equal_zero).
390    nrepeat (napply (less_than_or_equal_monotone ? ?)).
391    napply (less_than_or_equal_zero).
392nqed.
393
394ndefinition get_ac_flag ≝
395  λs: Status.
396    let sfr ≝ special_function_registers_8051 s in
397    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
398      get_index Bool eight psw (S Z) ?.
399    nnormalize.
400    nrepeat (napply (less_than_or_equal_monotone ? ?)).
401    napply (less_than_or_equal_zero).
402    nrepeat (napply (less_than_or_equal_monotone ? ?)).
403    napply (less_than_or_equal_zero).
404nqed.
405
406ndefinition get_fo_flag ≝
407  λs: Status.
408    let sfr ≝ special_function_registers_8051 s in
409    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
410      get_index Bool eight psw two ?.
411    nnormalize.
412    nrepeat (napply (less_than_or_equal_monotone ? ?)).
413    napply (less_than_or_equal_zero).
414    nrepeat (napply (less_than_or_equal_monotone ? ?)).
415    napply (less_than_or_equal_zero).
416nqed.
417
418ndefinition get_rs1_flag ≝
419  λs: Status.
420    let sfr ≝ special_function_registers_8051 s in
421    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
422      get_index Bool eight psw three ?.
423    nnormalize.
424    nrepeat (napply (less_than_or_equal_monotone ? ?)).
425    napply (less_than_or_equal_zero).
426    nrepeat (napply (less_than_or_equal_monotone ? ?)).
427    napply (less_than_or_equal_zero).
428nqed.
429
430ndefinition get_rs0_flag ≝
431  λs: Status.
432    let sfr ≝ special_function_registers_8051 s in
433    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
434      get_index Bool eight psw four ?.
435    nnormalize.
436    nrepeat (napply (less_than_or_equal_monotone ? ?)).
437    napply (less_than_or_equal_zero).
438    nrepeat (napply (less_than_or_equal_monotone ? ?)).
439    napply (less_than_or_equal_zero).
440nqed.
441
442ndefinition get_ov_flag ≝
443  λs: Status.
444    let sfr ≝ special_function_registers_8051 s in
445    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
446      get_index Bool eight psw five ?.
447    nnormalize.
448    nrepeat (napply (less_than_or_equal_monotone ? ?)).
449    napply (less_than_or_equal_zero).
450    nrepeat (napply (less_than_or_equal_monotone ? ?)).
451    napply (less_than_or_equal_zero).
452nqed.
453
454ndefinition get_ud_flag ≝
455  λs: Status.
456    let sfr ≝ special_function_registers_8051 s in
457    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
458      get_index Bool eight psw six ?.
459    nnormalize.
460    nrepeat (napply (less_than_or_equal_monotone ? ?)).
461    napply (less_than_or_equal_zero).
462    nrepeat (napply (less_than_or_equal_monotone ? ?)).
463    napply (less_than_or_equal_zero).
464nqed.
465
466ndefinition get_p_flag ≝
467  λs: Status.
468    let sfr ≝ special_function_registers_8051 s in
469    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
470      get_index Bool eight psw seven ?.
471    nnormalize.
472    nrepeat (napply (less_than_or_equal_monotone ? ?)).
473    napply (less_than_or_equal_zero).
474    nrepeat (napply (less_than_or_equal_monotone ? ?)).
475    napply (less_than_or_equal_zero).
476nqed.
[265]477
[290]478ndefinition set_flags ≝
479  λs: Status.
480  λcy: Bit.
481  λac: Maybe Bit.
482  λov: Bit.
483    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in
484    let old_cy ≝ get_index … nu Z ? in
485    let old_ac ≝ get_index … nu one ? in
486    let old_fo ≝ get_index … nu two ? in
487    let old_rs1 ≝ get_index … nu three ? in
488    let old_rs0 ≝ get_index … nl Z ? in
489    let old_ov ≝ get_index … nl one ? in
490    let old_ud ≝ get_index … nl two ? in
491    let old_p ≝ get_index … nl three ? in
492    let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in
493    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
494                     old_rs0 ; old_ov ; old_ud ; old_p ]] in
495      set_8051_sfr s SFR_PSW new_psw.
496    ##[##1,2,3,4,5,6,7,8:
497        nnormalize;
498        nrepeat (napply less_than_or_equal_monotone);
499        napply (less_than_or_equal_zero);
500    ##]
501nqed.
502
[257]503ndefinition initialise_status ≝
[285]504  let status ≝ mk_Status (Stub Byte sixteen)                    (* Code mem. *)
505                         (Stub Byte seven)                      (* Low mem.  *)
506                         (Stub Byte seven)                      (* High mem. *)
507                         (Stub Byte sixteen)                    (* Ext mem.  *)
508                         (zero sixteen)                         (* PC.       *)
509                         (replicate Byte nineteen (zero eight)) (* 8051 SFR. *)
510                         (replicate Byte five (zero eight))     (* 8052 SFR. *)
511                         (zero eight)                           (* P1 latch. *)
[329]512                         (zero eight)                           (* P3 latch. *)
513                         Z                                      (* Clock.    *)
514  in
515    set_program_counter status (bitvector_of_nat sixteen seven).
[281]516 
517naxiom not_implemented: False.
518 
519include "Arithmetic.ma".
520 
521ndefinition get_bit_addressable_sfr ≝
522  λs: Status.
523  λn: Nat.
524  λb: BitVector n.
525  λl: Bool.
526    let address ≝ nat_of_bitvector … b in
[350]527      if (eq_n address one_hundred_and_twenty_eight) then
[281]528        ?
[350]529      else if (eq_n address one_hundred_and_forty_four) then
[281]530        if l then
531          (p1_latch s)
532        else
533          (get_8051_sfr s SFR_P1)
[350]534      else if (eq_n address one_hundred_and_sixty) then
[281]535        ?
[350]536      else if (eq_n address one_hundred_and_seventy_six) then
[281]537        if l then
538          (p3_latch s)
539        else
540          (get_8051_sfr s SFR_P3)
[350]541      else if (eq_n address one_hundred_and_fifty_three) then
[281]542        get_8051_sfr s SFR_SBUF
[350]543      else if (eq_n address one_hundred_and_thirty_eight) then
[281]544        get_8051_sfr s SFR_TL0
[350]545      else if (eq_n address one_hundred_and_thirty_nine) then
[281]546        get_8051_sfr s SFR_TL1
[350]547      else if (eq_n address one_hundred_and_forty) then
[281]548        get_8051_sfr s SFR_TH0
[350]549      else if (eq_n address one_hundred_and_forty_one) then
[281]550        get_8051_sfr s SFR_TH1
[350]551      else if (eq_n address two_hundred) then
[281]552        get_8052_sfr s SFR_T2CON
[350]553      else if (eq_n address two_hundred_and_two) then
[281]554        get_8052_sfr s SFR_RCAP2L
[350]555      else if (eq_n address two_hundred_and_three) then
[281]556        get_8052_sfr s SFR_RCAP2H
[350]557      else if (eq_n address two_hundred_and_four) then
[281]558        get_8052_sfr s SFR_TL2
[350]559      else if (eq_n address two_hundred_and_five) then
[281]560        get_8052_sfr s SFR_TH2
[350]561      else if (eq_n address one_hundred_and_thirty_five) then
[281]562        get_8051_sfr s SFR_PCON
[350]563      else if (eq_n address one_hundred_and_thirty_six) then
[281]564        get_8051_sfr s SFR_TCON
[350]565      else if (eq_n address one_hundred_and_thirty_seven) then
[281]566        get_8051_sfr s SFR_TMOD
[350]567      else if (eq_n address one_hundred_and_fifty_two) then
[281]568        get_8051_sfr s SFR_SCON
[350]569      else if (eq_n address one_hundred_and_sixty_eight) then
[281]570        get_8051_sfr s SFR_IE
[350]571      else if (eq_n address one_hundred_and_eighty_four) then
[281]572        get_8051_sfr s SFR_IP
[350]573      else if (eq_n address one_hundred_and_twenty_nine) then
[281]574        get_8051_sfr s SFR_SP
[350]575      else if (eq_n address one_hundred_and_thirty) then
[281]576        get_8051_sfr s SFR_DPL
[350]577      else if (eq_n address one_hundred_and_thirty_one) then
[281]578        get_8051_sfr s SFR_DPH
[350]579      else if (eq_n address two_hundred_and_eight) then
[281]580        get_8051_sfr s SFR_PSW
[350]581      else if (eq_n address two_hundred_and_twenty_four) then
[281]582        get_8051_sfr s SFR_ACC_A
[350]583      else if (eq_n address two_hundred_and_forty) then
[281]584        get_8051_sfr s SFR_ACC_B
585      else
586        ?.
587      ncases not_implemented.
[285]588nqed.
589
590ndefinition set_bit_addressable_sfr ≝
591  λs: Status.
592  λb: Byte.
[313]593  λv: Byte.
[285]594    let address ≝ nat_of_bitvector … b in
[350]595      if (eq_n address one_hundred_and_twenty_eight) then
[285]596        ?
[350]597      else if (eq_n address one_hundred_and_forty_four) then
[313]598        let status_1 ≝ set_8051_sfr s SFR_P1 v in
599        let status_2 ≝ set_p1_latch s v in
[285]600          status_2
[350]601      else if (eq_n address one_hundred_and_sixty) then
[285]602        ?
[350]603      else if (eq_n address one_hundred_and_seventy_six) then
[313]604        let status_1 ≝ set_8051_sfr s SFR_P3 v in
605        let status_2 ≝ set_p3_latch s v in
[285]606          status_2
[350]607      else if (eq_n address one_hundred_and_fifty_three) then
[313]608        set_8051_sfr s SFR_SBUF v
[350]609      else if (eq_n address one_hundred_and_thirty_eight) then
[313]610        set_8051_sfr s SFR_TL0 v
[350]611      else if (eq_n address one_hundred_and_thirty_nine) then
[313]612        set_8051_sfr s SFR_TL1 v
[350]613      else if (eq_n address one_hundred_and_forty) then
[313]614        set_8051_sfr s SFR_TH0 v
[350]615      else if (eq_n address one_hundred_and_forty_one) then
[313]616        set_8051_sfr s SFR_TH1 v
[350]617      else if (eq_n address two_hundred) then
[313]618        set_8052_sfr s SFR_T2CON v
[350]619      else if (eq_n address two_hundred_and_two) then
[313]620        set_8052_sfr s SFR_RCAP2L v
[350]621      else if (eq_n address two_hundred_and_three) then
[313]622        set_8052_sfr s SFR_RCAP2H v
[350]623      else if (eq_n address two_hundred_and_four) then
[313]624        set_8052_sfr s SFR_TL2 v
[350]625      else if (eq_n address two_hundred_and_five) then
[313]626        set_8052_sfr s SFR_TH2 v
[350]627      else if (eq_n address one_hundred_and_thirty_five) then
[313]628        set_8051_sfr s SFR_PCON v
[350]629      else if (eq_n address one_hundred_and_thirty_six) then
[313]630        set_8051_sfr s SFR_TCON v
[350]631      else if (eq_n address one_hundred_and_thirty_seven) then
[313]632        set_8051_sfr s SFR_TMOD v
[350]633      else if (eq_n address one_hundred_and_fifty_two) then
[313]634        set_8051_sfr s SFR_SCON v
[350]635      else if (eq_n address one_hundred_and_sixty_eight) then
[313]636        set_8051_sfr s SFR_IE v
[350]637      else if (eq_n address one_hundred_and_eighty_four) then
[313]638        set_8051_sfr s SFR_IP v
[350]639      else if (eq_n address one_hundred_and_twenty_nine) then
[313]640        set_8051_sfr s SFR_SP v
[350]641      else if (eq_n address one_hundred_and_thirty) then
[313]642        set_8051_sfr s SFR_DPL v
[350]643      else if (eq_n address one_hundred_and_thirty_one) then
[313]644        set_8051_sfr s SFR_DPH v
[350]645      else if (eq_n address two_hundred_and_eight) then
[313]646        set_8051_sfr s SFR_PSW v
[350]647      else if (eq_n address two_hundred_and_twenty_four) then
[313]648        set_8051_sfr s SFR_ACC_A v
[350]649      else if (eq_n address two_hundred_and_forty) then
[313]650        set_8051_sfr s SFR_ACC_B v
[285]651      else
652        ?.
653      ncases not_implemented.
[286]654nqed.
655
656ndefinition bit_address_of_register ≝
657  λs: Status.
[317]658  λr: BitVector three.
[337]659    let b ≝ get_index_bv ? r Z ? in
660    let c ≝ get_index_bv ? r one ? in
661    let d ≝ get_index_bv ? r two ? in
[286]662    let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
[337]663    let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_bv four un two ?) (get_index_bv four un three ?) in
[286]664    let offset ≝
665      if conjunction (negation r1) (negation r0) then
666        Z
667      else if conjunction (negation r1) r0 then
668        eight
669      else if conjunction r1 r0 then
670        twenty_four
671      else
672        sixteen
673    in
674      bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
[317]675  ##[##1,2,3,4,5:
676      nnormalize;
677      nrepeat (napply less_than_or_equal_monotone);
678      napply less_than_or_equal_zero;
679  ##]
[287]680nqed.
681
682ndefinition get_register ≝
683  λs: Status.
[317]684  λr: BitVector three.
685    let address ≝ bit_address_of_register s r in
[287]686      lookup … address (low_internal_ram s) (zero eight).
687     
688ndefinition set_register ≝
689  λs: Status.
[317]690  λr: BitVector three.
[287]691  λv: Byte.
[317]692    let address ≝ bit_address_of_register s r in
[287]693    let old_low_internal_ram ≝ low_internal_ram s in
694    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
695      set_low_internal_ram s new_low_internal_ram.
696     
697ndefinition read_at_stack_pointer ≝
698  λs: Status.
699    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
[343]700    let m ≝ get_index_bv … nu Z ? in
701    let r1 ≝ get_index_bv … nu one ? in
702    let r2 ≝ get_index_bv … nu two ? in
703    let r3 ≝ get_index_bv … nu three ? in
[287]704    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
705    let memory ≝
706      if m then
707        (low_internal_ram s)
708      else
709        (high_internal_ram s)
710    in
711      lookup … address memory (zero eight).
712    ##[##1,2,3,4:
713        nnormalize;
714        nrepeat (napply less_than_or_equal_monotone);
715        napply less_than_or_equal_zero;
716    ##]
[288]717nqed.
718
[289]719ndefinition write_at_stack_pointer ≝
[288]720  λs: Status.
721  λv: Byte.
[289]722    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
723    let bit_zero ≝ get_index … nu Z ? in
724    let bit_one ≝ get_index … nu one ? in
725    let bit_two ≝ get_index … nu two ? in
726    let bit_three ≝ get_index … nu three ? in
727      if bit_zero then
728        let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
729                              v (low_internal_ram s) in
730          set_low_internal_ram s memory
731      else
732        let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
733                              v (high_internal_ram s) in
734          set_high_internal_ram s memory.
735    ##[##1,2,3,4:
736        nnormalize;
737        nrepeat (napply less_than_or_equal_monotone);
738        napply less_than_or_equal_zero;
739    ##]
[294]740nqed.
741
742ndefinition set_arg_16: Status → Word → [[ dptr ]] → Status ≝
743  λs,v,a.
744   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with
745     [ DPTR ⇒ λ_:True.
746       let 〈 bu, bl 〉 ≝ split … eight eight v in
747       let status ≝ set_8051_sfr s SFR_DPH bu in
748       let status ≝ set_8051_sfr status SFR_DPL bl in
749         status
750     | _ ⇒ λK.
751       match K in False with
752       [
753       ]
754     ] (subaddressing_modein … a).
755   
756ndefinition get_arg_16: Status → [[ data16 ]] → Word ≝
757  λs, a.
758    match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
759      [ DATA16 d ⇒ λ_:True. d
760      | _ ⇒ λK.
761        match K in False with
762        [
763        ]
[310]764      ] (subaddressing_modein … a).
765     
766ndefinition get_arg_8: Status → Bool → [[ direct ; indirect ; register ;
767                                          acc_a ; acc_b ; data ; acc_dptr ;
768                                          acc_pc ; ext_indirect ;
769                                          ext_indirect_dptr ]] → Byte ≝
770  λs, l, a.
771    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
772                                                acc_a ; acc_b ; data ; acc_dptr ;
773                                                acc_pc ; ext_indirect ;
774                                                ext_indirect_dptr ]] x) → ? with
[311]775      [ ACC_A ⇒ λacc_a: True. get_8051_sfr s SFR_ACC_A
776      | ACC_B ⇒ λacc_b: True. get_8051_sfr s SFR_ACC_B
777      | DATA d ⇒ λdata: True. d
[316]778      | REGISTER r ⇒ λregister: True. get_register s r
[310]779      | EXT_INDIRECT_DPTR ⇒
[311]780        λext_indirect_dptr: True.
[310]781          let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
782            lookup … sixteen address (external_ram s) (zero eight)
783      | EXT_INDIRECT e ⇒
[311]784        λext_indirect: True.
[317]785          let address ≝ get_register s [[ false; false; e ]]  in
[310]786          let padded_address ≝ pad eight eight address in
[311]787            lookup … sixteen padded_address (external_ram s) (zero eight)
[310]788      | ACC_DPTR ⇒
[311]789        λacc_dptr: True.
[310]790          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
791          let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
[313]792          let 〈 carry, address 〉 ≝ half_add sixteen dptr padded_acc in
[310]793            lookup … sixteen address (external_ram s) (zero eight)
794      | ACC_PC ⇒
[311]795        λacc_pc: True.
[310]796          let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
[313]797          let 〈 carry, address 〉 ≝ half_add sixteen (program_counter s) padded_acc in
[310]798            lookup … sixteen address (external_ram s) (zero eight)
799      | DIRECT d ⇒
[311]800        λdirect: True.
801          let 〈 nu, nl 〉 ≝ split … four four d in
[343]802          let bit_one ≝ get_index_bv … nu one ? in
[311]803            match bit_one with
804              [ true ⇒
805                  let 〈 bit_one, three_bits 〉 ≝ split ? one three nu in
806                  let address ≝ three_bits @@ nl in
807                    lookup ? seven address (low_internal_ram s) (zero eight)
808              | false ⇒ get_bit_addressable_sfr s eight d l
809              ]
[310]810      | INDIRECT i ⇒
[311]811        λindirect: True.
[317]812          let 〈 nu, nl 〉 ≝ split ? four four (get_register s [[ false; false; i]]) in
[311]813          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
[343]814          let bit_one ≝ get_index_bv … bit_one_v Z ? in
[311]815          match bit_one with
816            [ true ⇒
817                lookup ? seven (three_bits @@ nl) (low_internal_ram s) (zero eight)
818            | false ⇒
819                lookup ? seven (three_bits @@ nl) (high_internal_ram s) (zero eight)
820            ]
821      | _ ⇒ λother.
822        match other in False with [ ]
[310]823      ] (subaddressing_modein … a).
[311]824      ##[##1,2:
825          nnormalize;
826          nrepeat (napply less_than_or_equal_monotone);
827          napply less_than_or_equal_zero;
828      ##]
829nqed.
[313]830
[314]831ndefinition set_arg_8: Status → [[ direct ; indirect ; register ;
832                                   acc_a ; acc_b ; ext_indirect ;
833                                   ext_indirect_dptr ]] → Byte → Status ≝
834  λs, a, v.
835    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
836                                                acc_a ; acc_b ; ext_indirect ;
837                                                ext_indirect_dptr ]] x) → ? with
838      [ DIRECT d ⇒
839        λdirect: True.
840          let 〈 nu, nl 〉 ≝ split … four four d in
[343]841          let bit_one ≝ get_index_bv … nu one ? in
[314]842          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
843            match bit_one with
844              [ true ⇒ set_bit_addressable_sfr s d v
845              | false ⇒
846                let memory ≝ insert ? seven (three_bits @@ nl) v (low_internal_ram s) in
847                  set_low_internal_ram s memory
848              ]
849      | INDIRECT i ⇒
850        λindirect: True.
[317]851          let register ≝ get_register s [[ false; false; i ]] in
[314]852          let 〈 nu, nl 〉 ≝ split ? four four register in
[343]853          let bit_one ≝ get_index_bv ? nu one ? in
[314]854          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
855          match bit_one with
856            [ true ⇒
857              let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in
858                set_low_internal_ram s memory
859            | false ⇒
860              let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in
861                set_high_internal_ram s memory
862            ]
[317]863      | REGISTER r ⇒ λregister: True. set_register s r v
[314]864      | ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v
865      | ACC_B ⇒ λacc_b: True. set_8051_sfr s SFR_ACC_B v
866      | EXT_INDIRECT e ⇒
867        λext_indirect: True.
[317]868          let address ≝ get_register s [[ false; false; e ]] in
[314]869          let padded_address ≝ pad eight eight address in
870          let memory ≝ insert ? sixteen padded_address v (external_ram s) in
871            set_external_ram s memory
872      | EXT_INDIRECT_DPTR ⇒
873        λext_indirect_dptr: True.
874          let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
875          let memory ≝ insert ? sixteen address v (external_ram s) in
876            set_external_ram s memory
877      | _ ⇒
878        λother: False.
879          match other in False with [ ]
880      ] (subaddressing_modein … a).
881      ##[##1,2:
882          nnormalize;
883          nrepeat (napply less_than_or_equal_monotone);
884          napply less_than_or_equal_zero
885      ##]
886nqed.
887
[351]888ntheorem modulus_less_than:
889  ∀m,n: Nat. (m mod (S n)) < S n.
890 #n m; nnormalize; napply less_than_or_equal_monotone;
891 nlapply (ltoe_refl n);
892 ngeneralize in ⊢ (?%? → ?(??%?)?);
893 nelim n in ⊢ (∀_:?. ??% → ?(?%??)?)
894  [ nnormalize; #n; napply (less_than_or_equal_b_elim n m); nnormalize
[352]895     [ // | #H K; ninversion K [ #H1; nrewrite < H1; // | #x H1 H2 H3; ndestruct ]##]
[351]896##| nnormalize; #y H1 n H2; napply (less_than_or_equal_b_elim n m); nnormalize
897     [ // | #K; napply H1; ncut (n ≤ S y → n - S m ≤ y); /2/;
898       ncases n; nnormalize; //;
899       #x K1; nlapply (less_than_or_equal_injective … K1); ngeneralize in match m;
900       nelim x; nnormalize; //; #w1 H m; ncases m; nnormalize; //;
901       #q K2; napply H; /3/]
902nqed.
[314]903
[313]904ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →
905                       Bool → Bool ≝
906  λs, a, l.
907    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
908                                                 n_bit_addr ;
909                                                 carry ]] x) → ? with
910      [ BIT_ADDR b ⇒
911        λbit_addr: True.
912          let 〈 nu, nl 〉 ≝ split … four four b in
[343]913          let bit_one ≝ get_index_bv … nu one ? in
[313]914          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
915            match bit_one with
916              [ true ⇒
917                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
918                let d ≝ address ÷ eight in
919                let m ≝ address mod eight in
[314]920                let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
[313]921                let sfr ≝ get_bit_addressable_sfr s ? trans l in
[343]922                  get_index_bv ? sfr m ?
[313]923              | false ⇒
924                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
[314]925                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
[313]926                let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
[343]927                  get_index_bv ? t (modulus address eight) ?
[313]928              ]
929      | N_BIT_ADDR n ⇒
930        λn_bit_addr: True.
931          let 〈 nu, nl 〉 ≝ split … four four n in
[343]932          let bit_one ≝ get_index_bv … nu one ? in
[313]933          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
934            match bit_one with
935              [ true ⇒
936                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
937                let d ≝ address ÷ eight in
938                let m ≝ address mod eight in
[314]939                let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
[313]940                let sfr ≝ get_bit_addressable_sfr s ? trans l in
[343]941                  negation (get_index_bv ? sfr m ?)
[313]942              | false ⇒
943                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
[314]944                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
[313]945                let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
[343]946                  negation (get_index_bv ? trans (modulus address eight) ?)
[313]947              ]
948      | CARRY ⇒ λcarry: True. get_cy_flag s
949      | _ ⇒ λother.
950        match other in False with [ ]
[314]951      ] (subaddressing_modein … a).
952      ##[##3,6:
953          nnormalize;
954          nrepeat (napply less_than_or_equal_monotone);
955          napply less_than_or_equal_zero;
956      ##|##1,2,4,5:
957          napply modulus_less_than;
958      ##]
959nqed.
960     
961ndefinition set_arg_1: Status → [[ bit_addr ; carry ]] →
962                       Bit → Status ≝
[313]963  λs, a, v.
[314]964    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with
965      [ BIT_ADDR b ⇒ λbit_addr: True.
966          let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
[343]967          let bit_one ≝ get_index_bv ? nu one ? in
[313]968          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
[314]969          match bit_one with
970            [ true ⇒
971                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
972                let d ≝ address ÷ eight in
973                let m ≝ address mod eight in
974                let t ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
975                let sfr ≝ get_bit_addressable_sfr s ? t true in
976                let new_sfr ≝ set_index … sfr m v ? in
977                  set_bit_addressable_sfr s new_sfr t
978            | false ⇒
979                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
980                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
981                let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
982                let n_bit ≝ set_index … t (modulus address eight) v ? in
983                let memory ≝ insert ? seven address' n_bit (low_internal_ram s) in
[313]984                  set_low_internal_ram s memory
[314]985            ]
986      | CARRY ⇒
987        λcarry: True.
988          let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
989          let bit_one ≝ get_index … nu one ? in
990          let bit_two ≝ get_index … nu two ? in
991          let bit_three ≝ get_index … nu three ? in
992          let new_psw ≝ [[ v; bit_one ; bit_two; bit_three ]] @@ nl in
993            set_8051_sfr s SFR_PSW new_psw
[313]994      | _ ⇒
995        λother: False.
[314]996          match other in False with
997            [ ]
998      ] (subaddressing_modein … a).
999      ##[##1,2,3,6:
1000          nnormalize;
1001          nrepeat (napply less_than_or_equal_monotone);
1002          napply less_than_or_equal_zero;
1003      ##|##4,5:
[351]1004          napply modulus_less_than;
[314]1005      ##]
[345]1006nqed.
1007
1008ndefinition load_code_memory ≝
[350]1009 fold_left_i … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte sixteen).
[345]1010
1011ndefinition load ≝
[351]1012 λl,status. set_code_memory status (load_code_memory l).
Note: See TracBrowser for help on using the repository browser.