Changeset 1666 for src/ASM/Status.ma


Ignore:
Timestamp:
Jan 28, 2012, 1:42:15 PM (7 years ago)
Author:
sacerdot
Message:

PreStatus? datatype change: the code_memory field is not a left parameter.
This greatly simplify the dependent type madness due to policy depending
on the code_memory and not really on the status. On the other hand it
makes the rest of the code uglier.

Note: the changes have not been propagated yet to ASMCosts, CostsProof? and
Interpret2. The AssemlyProof? is almost repaired.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r1600 r1666  
    8686(* Processor status.                                                          *)
    8787(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    88 record PreStatus (M: Type[0]): Type[0] ≝
     88record PreStatus (M: Type[0]) (code_memory: M) : Type[0] ≝
    8989{
    90   code_memory: M;
    9190  low_internal_ram: BitVectorTrie Byte 7;
    9291  high_internal_ram: BitVectorTrie Byte 7;
     
    129128definition set_clock ≝
    130129  λM: Type[0].
    131   λs: PreStatus M.
     130  λcode_memory:M.
     131  λs: PreStatus M code_memory.
    132132  λt: Time.
    133     let old_code_memory ≝ code_memory ? s in
    134     let old_low_internal_ram ≝ low_internal_ram ? s in
    135     let old_high_internal_ram ≝ high_internal_ram ? s in
    136     let old_external_ram ≝ external_ram ? s in
    137     let old_program_counter ≝ program_counter ? s in
    138     let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
    139     let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
    140     let old_p1_latch ≝ p1_latch ? s in   
    141     let old_p3_latch ≝ p3_latch ? s in
    142       mk_PreStatus M old_code_memory
     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
    143142                old_low_internal_ram
    144143                old_high_internal_ram
     
    153152definition set_p1_latch ≝
    154153  λM: Type[0].
    155   λs: PreStatus M.
     154  λcode_memory:M.
     155  λs: PreStatus M code_memory.
    156156  λb: Byte.
    157     let old_code_memory ≝ code_memory ? s in
    158     let old_low_internal_ram ≝ low_internal_ram ? s in
    159     let old_high_internal_ram ≝ high_internal_ram ? s in
    160     let old_external_ram ≝ external_ram ? s in
    161     let old_program_counter ≝ program_counter ? s in
    162     let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
    163     let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
    164     let old_p3_latch ≝ p3_latch ? s in
    165     let old_clock ≝ clock ? s in
    166       mk_PreStatus M old_code_memory
     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
    167166                old_low_internal_ram
    168167                old_high_internal_ram
     
    177176definition set_p3_latch ≝
    178177  λM: Type[0].
    179   λs: PreStatus M.
     178  λcode_memory:M.
     179  λs: PreStatus M code_memory.
    180180  λb: Byte.
    181     let old_code_memory ≝ code_memory ? s in
    182     let old_low_internal_ram ≝ low_internal_ram ? s in
    183     let old_high_internal_ram ≝ high_internal_ram ? s in
    184     let old_external_ram ≝ external_ram ? s in
    185     let old_program_counter ≝ program_counter ? s in
    186     let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
    187     let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
    188     let old_p1_latch ≝ p1_latch ? s in
    189     let old_clock ≝ clock ? s in
    190       mk_PreStatus M old_code_memory
     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
    191190                old_low_internal_ram
    192191                old_high_internal_ram
     
    201200definition get_8051_sfr ≝
    202201  λM: Type[0].
    203   λs: PreStatus M.
     202  λcode_memory:M.
     203  λs: PreStatus M code_memory.
    204204  λi: SFR8051.
    205     let sfr ≝ special_function_registers_8051 ? s in
     205    let sfr ≝ special_function_registers_8051 ?? s in
    206206    let index ≝ sfr_8051_index i in
    207207      get_index_v … sfr index ?.
     
    211211definition get_8052_sfr ≝
    212212  λM: Type[0].
    213   λs: PreStatus M.
     213  λcode_memory:M.
     214  λs: PreStatus M code_memory.
    214215  λi: SFR8052.
    215     let sfr ≝ special_function_registers_8052 ? s in
     216    let sfr ≝ special_function_registers_8052 ?? s in
    216217    let index ≝ sfr_8052_index i in
    217218      get_index_v … sfr index ?.
     
    221222definition set_8051_sfr ≝
    222223  λM: Type[0].
    223   λs: PreStatus M.
     224  λcode_memory:M.
     225  λs: PreStatus M code_memory.
    224226  λi: SFR8051.
    225227  λb: Byte.
    226228    let index ≝ sfr_8051_index i in
    227     let old_code_memory ≝ code_memory ? s in
    228     let old_low_internal_ram ≝ low_internal_ram ? s in
    229     let old_high_internal_ram ≝ high_internal_ram ? s in
    230     let old_external_ram ≝ external_ram ? s in
    231     let old_program_counter ≝ program_counter ? s in
    232     let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
    233     let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s 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
    234235    let new_special_function_registers_8051 ≝
    235236      set_index Byte 19 old_special_function_registers_8051 index b ? in
    236     let old_p1_latch ≝ p1_latch ? s in
    237     let old_p3_latch ≝ p3_latch ? s in
    238     let old_clock ≝ clock ? s in
    239       mk_PreStatus M old_code_memory
     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
    240241                old_low_internal_ram
    241242                old_high_internal_ram
     
    252253definition set_8052_sfr ≝
    253254  λM: Type[0].
    254   λs: PreStatus M.
     255  λcode_memory:M.
     256  λs: PreStatus M code_memory.
    255257  λi: SFR8052.
    256258  λb: Byte.
    257259    let index ≝ sfr_8052_index i in
    258     let old_code_memory ≝ code_memory ? s in
    259     let old_low_internal_ram ≝ low_internal_ram ? s in
    260     let old_high_internal_ram ≝ high_internal_ram ? s in
    261     let old_external_ram ≝ external_ram ? s in
    262     let old_program_counter ≝ program_counter ? s in
    263     let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
    264     let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s 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
    265266    let new_special_function_registers_8052 ≝
    266267      set_index Byte 5 old_special_function_registers_8052 index b ? in
    267     let old_p1_latch ≝ p1_latch ? s in
    268     let old_p3_latch ≝ p3_latch ? s in
    269     let old_clock ≝ clock ? s in
    270       mk_PreStatus M old_code_memory
     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
    271272                old_low_internal_ram
    272273                old_high_internal_ram
     
    283284definition set_program_counter ≝
    284285  λM: Type[0].
    285   λs: PreStatus M.
     286  λcode_memory:M.
     287  λs: PreStatus M code_memory.
    286288  λw: Word.
    287     let old_code_memory ≝ code_memory ? s in
    288     let old_low_internal_ram ≝ low_internal_ram ? s in
    289     let old_high_internal_ram ≝ high_internal_ram ? s in
    290     let old_external_ram ≝ external_ram ? s in
    291     let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
    292     let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
    293     let old_p1_latch ≝ p1_latch ? s in
    294     let old_p3_latch ≝ p3_latch ? s in
    295     let old_clock ≝ clock ? s in
    296       mk_PreStatus M old_code_memory
     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
    297298                old_low_internal_ram
    298299                old_high_internal_ram
     
    307308definition set_code_memory ≝
    308309  λM,M': Type[0].
    309   λs: PreStatus M.
     310  λcode_memory:M.
     311  λs: PreStatus M code_memory.
    310312  λr: M'.
    311     let old_low_internal_ram ≝ low_internal_ram ? s in
    312     let old_high_internal_ram ≝ high_internal_ram ? s in
    313     let old_external_ram ≝ external_ram ? s in
    314     let old_program_counter ≝ program_counter ? s in
    315     let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
    316     let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
    317     let old_p1_latch ≝ p1_latch ? s in
    318     let old_p3_latch ≝ p3_latch ? s in
    319     let old_clock ≝ clock ? s in
     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
    320322      mk_PreStatus M' r
    321323                old_low_internal_ram
     
    331333definition set_low_internal_ram ≝
    332334  λM: Type[0].
    333   λs: PreStatus M.
     335  λcode_memory:M.
     336  λs: PreStatus M code_memory.
    334337  λr: BitVectorTrie Byte 7.
    335     let old_code_memory ≝ code_memory ? s in
    336     let old_high_internal_ram ≝ high_internal_ram ? s in
    337     let old_external_ram ≝ external_ram ? s in
    338     let old_program_counter ≝ program_counter ? s in
    339     let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
    340     let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
    341     let old_p1_latch ≝ p1_latch ? s in
    342     let old_p3_latch ≝ p3_latch ? s in
    343     let old_clock ≝ clock ? s in
    344       mk_PreStatus M old_code_memory
     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
    345347                r
    346348                old_high_internal_ram
     
    355357definition set_high_internal_ram ≝
    356358  λM: Type[0].
    357   λs: PreStatus M.
     359  λcode_memory:M.
     360  λs: PreStatus M code_memory.
    358361  λr: BitVectorTrie Byte 7.
    359     let old_code_memory ≝ code_memory ? s in
    360     let old_low_internal_ram ≝ low_internal_ram ? s in
    361     let old_high_internal_ram ≝ high_internal_ram ? s in
    362     let old_external_ram ≝ external_ram ? s in
    363     let old_program_counter ≝ program_counter ? s in
    364     let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
    365     let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
    366     let old_p1_latch ≝ p1_latch ? s in
    367     let old_p3_latch ≝ p3_latch ? s in
    368     let old_clock ≝ clock ? s in
    369       mk_PreStatus M old_code_memory
     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
    370372                old_low_internal_ram
    371373                r
     
    380382definition set_external_ram ≝
    381383  λM: Type[0].
    382   λs: PreStatus M.
     384  λcode_memory:M.
     385  λs: PreStatus M code_memory.
    383386  λr: BitVectorTrie Byte 16.
    384     let old_code_memory ≝ code_memory ? s in
    385     let old_low_internal_ram ≝ low_internal_ram ? s in
    386     let old_high_internal_ram ≝ high_internal_ram ? s in
    387     let old_program_counter ≝ program_counter ? s in
    388     let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in
    389     let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in
    390     let old_p1_latch ≝ p1_latch ? s in
    391     let old_p3_latch ≝ p3_latch ? s in
    392     let old_clock ≝ clock ? s in
    393       mk_PreStatus M old_code_memory
     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
    394396                old_low_internal_ram
    395397                old_high_internal_ram
     
    404406definition get_cy_flag ≝
    405407  λM: Type[0].
    406   λs: PreStatus M.
    407     let sfr ≝ special_function_registers_8051 ? s in
     408  λcode_memory:M.
     409  λs: PreStatus M code_memory.
     410    let sfr ≝ special_function_registers_8051 ?? s in
    408411    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    409412      get_index_v bool 8 psw O ?.
     
    418421definition get_ac_flag ≝
    419422  λM: Type[0].
    420   λs: PreStatus M.
    421     let sfr ≝ special_function_registers_8051 ? s in
     423  λcode_memory:M.
     424  λs: PreStatus M code_memory.
     425    let sfr ≝ special_function_registers_8051 ?? s in
    422426    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    423427      get_index_v bool 8 psw 1 ?.
     
    429433definition get_fo_flag ≝
    430434  λM: Type[0].
    431   λs: PreStatus M.
    432     let sfr ≝ special_function_registers_8051 ? s in
     435  λcode_memory:M.
     436  λs: PreStatus M code_memory.
     437    let sfr ≝ special_function_registers_8051 ?? s in
    433438    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    434439      get_index_v bool 8 psw 2 ?.
     
    440445definition get_rs1_flag ≝
    441446  λM: Type[0].
    442   λs: PreStatus M.
    443     let sfr ≝ special_function_registers_8051 ? s in
     447  λcode_memory:M.
     448  λs: PreStatus M code_memory.
     449    let sfr ≝ special_function_registers_8051 ?? s in
    444450    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    445451      get_index_v bool 8 psw 3 ?.
     
    451457definition get_rs0_flag ≝
    452458  λM: Type[0].
    453   λs: PreStatus M.
    454     let sfr ≝ special_function_registers_8051 ? s in
     459  λcode_memory:M.
     460  λs: PreStatus M code_memory.
     461    let sfr ≝ special_function_registers_8051 ?? s in
    455462    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    456463      get_index_v bool 8 psw 4 ?.
     
    462469definition get_ov_flag ≝
    463470  λM: Type[0].
    464   λs: PreStatus M.
    465     let sfr ≝ special_function_registers_8051 ? s in
     471  λcode_memory:M.
     472  λs: PreStatus M code_memory.
     473    let sfr ≝ special_function_registers_8051 ?? s in
    466474    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    467475      get_index_v bool 8 psw 5 ?.
     
    473481definition get_ud_flag ≝
    474482  λM: Type[0].
    475   λs: PreStatus M.
    476     let sfr ≝ special_function_registers_8051 ? s in
     483  λcode_memory:M.
     484  λs: PreStatus M code_memory.
     485    let sfr ≝ special_function_registers_8051 ?? s in
    477486    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    478487      get_index_v bool 8 psw 6 ?.
     
    484493definition get_p_flag ≝
    485494  λM: Type[0].
    486   λs: PreStatus M.
    487     let sfr ≝ special_function_registers_8051 ? s in
     495  λcode_memory:M.
     496  λs: PreStatus M code_memory.
     497    let sfr ≝ special_function_registers_8051 ?? s in
    488498    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    489499      get_index_v bool 8 psw 7 ?.
     
    495505definition set_flags ≝
    496506  λM: Type[0].
    497   λs: PreStatus M.
     507  λcode_memory:M.
     508  λs: PreStatus M code_memory.
    498509  λcy: Bit.
    499510  λac: option Bit.
    500511  λov: Bit.
    501     let old_cy ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) O ? in
    502     let old_ac ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 1 ? in
    503     let old_fo ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 2 ? in
    504     let old_rs1 ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 3 ? in
    505     let old_rs0 ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 4 ? in
    506     let old_ov ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 5 ? in
    507     let old_ud ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 6 ? in
    508     let old_p ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 7 ? in
     512    let old_cy ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) O ? in
     513    let old_ac ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 1 ? in
     514    let old_fo ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 2 ? in
     515    let old_rs1 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 3 ? in
     516    let old_rs0 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 4 ? in
     517    let old_ov ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 5 ? in
     518    let old_ud ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 6 ? in
     519    let old_p ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 7 ? in
    509520    let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
    510     let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
    511                      old_rs0 ; old_ov ; old_ud ; old_p ]] in
    512       set_8051_sfr ? s SFR_PSW new_psw.
     521      set_8051_sfr ?? s SFR_PSW
     522      [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
     523         old_rs0 ; old_ov ; old_ud ; old_p ]].
    513524    [1,2,3,4,5,6,7,8:
    514525       normalize
     
    532543                         O                                      (* Clock.    *)
    533544  in
    534     set_8051_sfr ? status SFR_SP (bitvector_of_nat 8 7).
     545    set_8051_sfr ?? status SFR_SP (bitvector_of_nat 8 7).
    535546 
    536547definition get_bit_addressable_sfr ≝
    537548  λM: Type[0].
    538   λs: PreStatus M.
     549  λcode_memory:M.
     550  λs: PreStatus M code_memory.
    539551  λn: nat.
    540552  λb: BitVector n.
     
    545557      else if (eqb address 144) then
    546558        if l then
    547           (p1_latch ? s)
     559          (p1_latch ?? s)
    548560        else
    549           (get_8051_sfr ? s SFR_P1)
     561          (get_8051_sfr ?? s SFR_P1)
    550562      else if (eqb address 160) then
    551563        ?
    552564      else if (eqb address 176) then
    553565        if l then
    554           (p3_latch ? s)
     566          (p3_latch ?? s)
    555567        else
    556           (get_8051_sfr ? s SFR_P3)
     568          (get_8051_sfr ?? s SFR_P3)
    557569      else if (eqb address 153) then
    558         get_8051_sfr ? s SFR_SBUF
     570        get_8051_sfr ?? s SFR_SBUF
    559571      else if (eqb address 138) then
    560         get_8051_sfr ? s SFR_TL0
     572        get_8051_sfr ?? s SFR_TL0
    561573      else if (eqb address 139) then
    562         get_8051_sfr ? s SFR_TL1
     574        get_8051_sfr ?? s SFR_TL1
    563575      else if (eqb address 140) then
    564         get_8051_sfr ? s SFR_TH0
     576        get_8051_sfr ?? s SFR_TH0
    565577      else if (eqb address 141) then
    566         get_8051_sfr ? s SFR_TH1
     578        get_8051_sfr ?? s SFR_TH1
    567579      else if (eqb address 200) then
    568         get_8052_sfr ? s SFR_T2CON
     580        get_8052_sfr ?? s SFR_T2CON
    569581      else if (eqb address 202) then
    570         get_8052_sfr ? s SFR_RCAP2L
     582        get_8052_sfr ?? s SFR_RCAP2L
    571583      else if (eqb address 203) then
    572         get_8052_sfr ? s SFR_RCAP2H
     584        get_8052_sfr ?? s SFR_RCAP2H
    573585      else if (eqb address 204) then
    574         get_8052_sfr ? s SFR_TL2
     586        get_8052_sfr ?? s SFR_TL2
    575587      else if (eqb address 205) then
    576         get_8052_sfr ? s SFR_TH2
     588        get_8052_sfr ?? s SFR_TH2
    577589      else if (eqb address 135) then
    578         get_8051_sfr ? s SFR_PCON
     590        get_8051_sfr ?? s SFR_PCON
    579591      else if (eqb address 136) then
    580         get_8051_sfr ? s SFR_TCON
     592        get_8051_sfr ?? s SFR_TCON
    581593      else if (eqb address 137) then
    582         get_8051_sfr ? s SFR_TMOD
     594        get_8051_sfr ?? s SFR_TMOD
    583595      else if (eqb address 152) then
    584         get_8051_sfr ? s SFR_SCON
     596        get_8051_sfr ?? s SFR_SCON
    585597      else if (eqb address 168) then
    586         get_8051_sfr ? s SFR_IE
     598        get_8051_sfr ?? s SFR_IE
    587599      else if (eqb address 184) then
    588         get_8051_sfr ? s SFR_IP
     600        get_8051_sfr ?? s SFR_IP
    589601      else if (eqb address 129) then
    590         get_8051_sfr ? s SFR_SP
     602        get_8051_sfr ?? s SFR_SP
    591603      else if (eqb address 130) then
    592         get_8051_sfr ? s SFR_DPL
     604        get_8051_sfr ?? s SFR_DPL
    593605      else if (eqb address 131) then
    594         get_8051_sfr ? s SFR_DPH
     606        get_8051_sfr ?? s SFR_DPH
    595607      else if (eqb address 208) then
    596         get_8051_sfr ? s SFR_PSW
     608        get_8051_sfr ?? s SFR_PSW
    597609      else if (eqb address 224) then
    598         get_8051_sfr ? s SFR_ACC_A
     610        get_8051_sfr ?? s SFR_ACC_A
    599611      else if (eqb address 240) then
    600         get_8051_sfr ? s SFR_ACC_B
     612        get_8051_sfr ?? s SFR_ACC_B
    601613      else
    602614        ?.
     
    606618definition set_bit_addressable_sfr ≝
    607619  λM: Type[0].
    608   λs: PreStatus M.
     620  λcode_memory:M.
     621  λs: PreStatus M code_memory.
    609622  λb: Byte.
    610623  λv: Byte.
     
    613626        ?
    614627      else if (eqb address 144) then
    615         let status_1 ≝ set_8051_sfr ? s SFR_P1 v in
    616         let status_2 ≝ set_p1_latch ? s v in
     628        let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
     629        let status_2 ≝ set_p1_latch ?? s v in
    617630          status_2
    618631      else if (eqb address 160) then
    619632        ?
    620633      else if (eqb address 176) then
    621         let status_1 ≝ set_8051_sfr ? s SFR_P3 v in
    622         let status_2 ≝ set_p3_latch ? s v in
     634        let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
     635        let status_2 ≝ set_p3_latch ?? s v in
    623636          status_2
    624637      else if (eqb address 153) then
    625         set_8051_sfr ? s SFR_SBUF v
     638        set_8051_sfr ?? s SFR_SBUF v
    626639      else if (eqb address 138) then
    627         set_8051_sfr ? s SFR_TL0 v
     640        set_8051_sfr ?? s SFR_TL0 v
    628641      else if (eqb address 139) then
    629         set_8051_sfr ? s SFR_TL1 v
     642        set_8051_sfr ?? s SFR_TL1 v
    630643      else if (eqb address 140) then
    631         set_8051_sfr ? s SFR_TH0 v
     644        set_8051_sfr ?? s SFR_TH0 v
    632645      else if (eqb address 141) then
    633         set_8051_sfr ? s SFR_TH1 v
     646        set_8051_sfr ?? s SFR_TH1 v
    634647      else if (eqb address 200) then
    635         set_8052_sfr ? s SFR_T2CON v
     648        set_8052_sfr ?? s SFR_T2CON v
    636649      else if (eqb address 202) then
    637         set_8052_sfr ? s SFR_RCAP2L v
     650        set_8052_sfr ?? s SFR_RCAP2L v
    638651      else if (eqb address 203) then
    639         set_8052_sfr ? s SFR_RCAP2H v
     652        set_8052_sfr ?? s SFR_RCAP2H v
    640653      else if (eqb address 204) then
    641         set_8052_sfr ? s SFR_TL2 v
     654        set_8052_sfr ?? s SFR_TL2 v
    642655      else if (eqb address 205) then
    643         set_8052_sfr ? s SFR_TH2 v
     656        set_8052_sfr ?? s SFR_TH2 v
    644657      else if (eqb address 135) then
    645         set_8051_sfr ? s SFR_PCON v
     658        set_8051_sfr ?? s SFR_PCON v
    646659      else if (eqb address 136) then
    647         set_8051_sfr ? s SFR_TCON v
     660        set_8051_sfr ?? s SFR_TCON v
    648661      else if (eqb address 137) then
    649         set_8051_sfr ? s SFR_TMOD v
     662        set_8051_sfr ?? s SFR_TMOD v
    650663      else if (eqb address 152) then
    651         set_8051_sfr ? s SFR_SCON v
     664        set_8051_sfr ?? s SFR_SCON v
    652665      else if (eqb address 168) then
    653         set_8051_sfr ? s SFR_IE v
     666        set_8051_sfr ?? s SFR_IE v
    654667      else if (eqb address 184) then
    655         set_8051_sfr ? s SFR_IP v
     668        set_8051_sfr ?? s SFR_IP v
    656669      else if (eqb address 129) then
    657         set_8051_sfr ? s SFR_SP v
     670        set_8051_sfr ?? s SFR_SP v
    658671      else if (eqb address 130) then
    659         set_8051_sfr ? s SFR_DPL v
     672        set_8051_sfr ?? s SFR_DPL v
    660673      else if (eqb address 131) then
    661         set_8051_sfr ? s SFR_DPH v
     674        set_8051_sfr ?? s SFR_DPH v
    662675      else if (eqb address 208) then
    663         set_8051_sfr ? s SFR_PSW v
     676        set_8051_sfr ?? s SFR_PSW v
    664677      else if (eqb address 224) then
    665         set_8051_sfr ? s SFR_ACC_A v
     678        set_8051_sfr ?? s SFR_ACC_A v
    666679      else if (eqb address 240) then
    667         set_8051_sfr ? s SFR_ACC_B v
     680        set_8051_sfr ?? s SFR_ACC_B v
    668681      else
    669682        ?.
     
    673686definition bit_address_of_register ≝
    674687  λM: Type[0].
    675   λs: PreStatus M.
     688  λcode_memory:M.
     689  λs: PreStatus M code_memory.
    676690  λr: BitVector 3.
    677691    let b ≝ get_index_v … r O ? in
    678692    let c ≝ get_index_v … r 1 ? in
    679693    let d ≝ get_index_v … r 2 ? in
    680     let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
     694    let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    681695    let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in
    682696    let offset ≝
     
    700714definition get_register ≝
    701715  λM: Type[0].
    702   λs: PreStatus M.
     716  λcode_memory:M.
     717  λs: PreStatus M code_memory.
    703718  λr: BitVector 3.
    704     let address ≝ bit_address_of_register ? s r in
    705       lookup ?? address (low_internal_ram ? s) (zero 8).
     719    let address ≝ bit_address_of_register s r in
     720      lookup ?? address (low_internal_ram s) (zero 8).
    706721     
    707722definition set_register ≝
    708723  λM: Type[0].
    709   λs: PreStatus M.
     724  λcode_memory:M.
     725  λs: PreStatus M code_memory.
    710726  λr: BitVector 3.
    711727  λv: Byte.
    712     let address ≝ bit_address_of_register ? s r in
    713     let old_low_internal_ram ≝ low_internal_ram ? s in
     728    let address ≝ bit_address_of_register s r in
     729    let old_low_internal_ram ≝ low_internal_ram ?? s in
    714730    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
    715       set_low_internal_ram ? s new_low_internal_ram.
     731      set_low_internal_ram s new_low_internal_ram.
    716732     
    717733definition read_at_stack_pointer ≝
    718734  λM: Type[0].
    719   λs: PreStatus M.
    720     let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_SP) in
    721     let m ≝ get_index_v … nu O ? in
    722     let r1 ≝ get_index_v … nu 1 ? in
    723     let r2 ≝ get_index_v … nu 2 ? in
    724     let r3 ≝ get_index_v … nu 3 ? in
     735  λcode_memory:M.
     736  λs: PreStatus M code_memory.
     737    let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_SP) in
     738    let m ≝ get_index_v ?? nu O ? in
     739    let r1 ≝ get_index_v ?? nu 1 ? in
     740    let r2 ≝ get_index_v ?? nu 2 ? in
     741    let r3 ≝ get_index_v ?? nu 3 ? in
    725742    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
    726743    let memory ≝
    727744      if m then
    728         (low_internal_ram ? s)
     745        (low_internal_ram ?? s)
    729746      else
    730         (high_internal_ram ? s)
     747        (high_internal_ram ?? s)
    731748    in
    732749      lookup … address memory (zero 8).
     
    740757definition write_at_stack_pointer ≝
    741758  λM: Type[0].
    742   λs: PreStatus M.
     759  λcode_memory:M.
     760  λs: PreStatus M code_memory.
    743761  λv: Byte.
    744     let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
    745     let bit_zero ≝ get_index_v nu O ? in
    746     let bit_1 ≝ get_index_v nu 1 ? in
    747     let bit_2 ≝ get_index_v nu 2 ? in
    748     let bit_3 ≝ get_index_v nu 3 ? in
     762    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ?? s SFR_SP) in
     763    let bit_zero ≝ get_index_v ?? nu O ? in
     764    let bit_1 ≝ get_index_v ?? nu 1 ? in
     765    let bit_2 ≝ get_index_v ?? nu 2 ? in
     766    let bit_3 ≝ get_index_v ?? nu 3 ? in
    749767      if bit_zero then
    750768        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
    751                               v (low_internal_ram ? s) in
    752           set_low_internal_ram ? s memory
     769                              v (low_internal_ram ?? s) in
     770          set_low_internal_ram ?? s memory
    753771      else
    754772        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
    755                               v (high_internal_ram ? s) in
    756           set_high_internal_ram ? s memory.
     773                              v (high_internal_ram ?? s) in
     774          set_high_internal_ram ?? s memory.
    757775  [1,2,3,4:
    758776     normalize
     
    762780qed.
    763781
    764 definition set_arg_16': ∀M: Type[0]. ∀s:PreStatus M. Word → [[ dptr ]] → Σs':PreStatus M. clock … s = clock … s' ≝
    765   λM.
    766   λs.
    767   λv.
    768   λa.
    769    match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M s = clock M s' with
     782definition 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' ≝
     783  λM,code_memory,s,v,a.
     784   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M ? s = clock M ? s' with
    770785     [ DPTR ⇒ λ_:True.
    771786       let 〈 bu, bl 〉 ≝ split … 8 8 v in
    772        let status ≝ set_8051_sfr ? s SFR_DPH bu in
    773        let status ≝ set_8051_sfr ? status SFR_DPL bl in
     787       let status ≝ set_8051_sfr s SFR_DPH bu in
     788       let status ≝ set_8051_sfr status SFR_DPL bl in
    774789         status
    775790     | _ ⇒ λK.
     
    781796qed.
    782797
    783 definition set_arg_16: ∀M: Type[0]. ∀s:PreStatus M. Word → [[ dptr ]] → PreStatus M
     798definition set_arg_16: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → PreStatus M code_memory
    784799 set_arg_16'.
    785800
    786 lemma set_arg_16_ok: ∀M,s,v,x. clock M s = clock … (set_arg_16 M s v x).
    787  #M #s #x #v whd in match set_arg_16; normalize nodelta @pi2
     801lemma set_arg_16_ok: ∀M,cm,s,v,x. clock M cm s = clock M cm (set_arg_16 M cm s v x).
     802 #M #cm #s #x #v whd in match set_arg_16; normalize nodelta @pi2
    788803qed.
    789804
    790805   
    791 definition get_arg_16: ∀M: Type[0]. PreStatus M → [[ data16 ]] → Word ≝
    792   λm, s, a.
     806definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ data16 ]] → Word ≝
     807  λm, cm, s, a.
    793808    match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
    794809      [ DATA16 d ⇒ λ_:True. d
     
    799814      ] (subaddressing_modein … a).
    800815     
    801 definition get_arg_8: ∀M: Type[0]. PreStatus M → bool → [[ direct ; indirect ; registr ;
     816definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ;
    802817                                          acc_a ; acc_b ; data ; acc_dptr ;
    803818                                          acc_pc ; ext_indirect ;
    804819                                          ext_indirect_dptr ]] → Byte ≝
    805   λm, s, l, a.
     820  λm, cm, s, l, a.
    806821    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    807822                                                acc_a ; acc_b ; data ; acc_dptr ;
    808823                                                acc_pc ; ext_indirect ;
    809824                                                ext_indirect_dptr ]] x) → ? with
    810       [ ACC_A ⇒ λacc_a: True. get_8051_sfr ? s SFR_ACC_A
    811       | ACC_B ⇒ λacc_b: True. get_8051_sfr ? s SFR_ACC_B
     825      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
     826      | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
    812827      | DATA d ⇒ λdata: True. d
    813       | REGISTER r ⇒ λregister: True. get_register ? s r
     828      | REGISTER r ⇒ λregister: True. get_register ?? s r
    814829      | EXT_INDIRECT_DPTR ⇒
    815830        λext_indirect_dptr: True.
    816           let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    817             lookup ? 16 address (external_ram ? s) (zero 8)
     831          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
     832            lookup ? 16 address (external_ram ?? s) (zero 8)
    818833      | EXT_INDIRECT e ⇒
    819834        λext_indirect: True.
    820           let address ≝ get_register ? s [[ false; false; e ]]  in
     835          let address ≝ get_register ?? s [[ false; false; e ]]  in
    821836          let padded_address ≝ pad 8 8 address in
    822             lookup ? 16 padded_address (external_ram ? s) (zero 8)
     837            lookup ? 16 padded_address (external_ram ?? s) (zero 8)
    823838      | ACC_DPTR ⇒
    824839        λacc_dptr: True.
    825           let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    826           let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in
     840          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
     841          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
    827842          let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in
    828             lookup ? 16 address (external_ram ? s) (zero 8)
     843            lookup ? 16 address (external_ram ?? s) (zero 8)
    829844      | ACC_PC ⇒
    830845        λacc_pc: True.
    831           let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in
    832           let 〈 carry, address 〉 ≝ half_add 16 (program_counter ? s) padded_acc in
    833             lookup ? 16 address (external_ram ? s) (zero 8)
     846          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
     847          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
     848            lookup ? 16 address (external_ram ?? s) (zero 8)
    834849      | DIRECT d ⇒
    835850        λdirect: True.
     
    840855              [ false ⇒
    841856                  let address ≝ three_bits @@ nl in
    842                     lookup ? 7 address (low_internal_ram ? s) (zero 8)
    843               | true ⇒ get_bit_addressable_sfr ? s 8 d l
     857                    lookup ? 7 address (low_internal_ram ?? s) (zero 8)
     858              | true ⇒ get_bit_addressable_sfr ?? s 8 d l
    844859              ]
    845860      | INDIRECT i ⇒
    846861        λindirect: True.
    847           let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ? s [[ false; false; i]]) in
     862          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ?? s [[ false; false; i]]) in
    848863          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
    849864          let bit_1 ≝ get_index_v ?? bit_one_v O ? in
    850865          match  bit_1 with
    851866            [ false ⇒
    852                 lookup ? 7 (three_bits @@ nl) (low_internal_ram ? s) (zero 8)
     867                lookup ? 7 (three_bits @@ nl) (low_internal_ram ?? s) (zero 8)
    853868            | true ⇒
    854                 lookup ? 7 (three_bits @@ nl) (high_internal_ram ? s) (zero 8)
     869                lookup ? 7 (three_bits @@ nl) (high_internal_ram ?? s) (zero 8)
    855870            ]
    856871      | _ ⇒ λother.
     
    864879qed.
    865880
    866 axiom set_bit_addressable_sfr_ignores_clock: ∀m,s,d,v. clock m s = clock … (set_bit_addressable_sfr … s d v).
    867 
    868 definition set_arg_8': ∀M: Type[0]. ∀s:PreStatus M. [[ direct ; indirect ; registr ;
     881axiom clock_set_bit_addressable_sfr: ∀m,cm,s,d,v. clock m cm s = clock … (set_bit_addressable_sfr … s d v).
     882
     883definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ;
    869884                                   acc_a ; acc_b ; ext_indirect ;
    870                                    ext_indirect_dptr ]] → Byte → Σs':PreStatus M.
    871                                    clock … s = clock … s' ≝
    872   λm, s, a, v.
     885                                   ext_indirect_dptr ]] → Byte → Σs':PreStatus M code_memory.
     886                                   clock … code_memory s = clock … code_memory s' ≝
     887  λm, cm, s, a, v.
    873888    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    874889                                                acc_a ; acc_b ; ext_indirect ;
    875890                                                ext_indirect_dptr ]] x) →
    876                    Σs':PreStatus m. ?(*clock … s*) = ?(*clock … s'*)
     891                   Σs':PreStatus m cm. clock m cm s = clock m cm s'
    877892                   (*CSC: bug here if one specified the two clock above*)
    878893            with
     
    883898          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
    884899            match bit_one with
    885               [ true ⇒ set_bit_addressable_sfr ? s d v
     900              [ true ⇒ set_bit_addressable_sfr ?? s d v
    886901              | false ⇒
    887                 let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ? s) in
    888                   set_low_internal_ram ? s memory
     902                let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in
     903                  set_low_internal_ram ?? s memory
    889904              ]
    890905      | INDIRECT i ⇒
    891906        λindirect: True.
    892           let register ≝ get_register ? s [[ false; false; i ]] in
     907          let register ≝ get_register ?? s [[ false; false; i ]] in
    893908          let 〈nu, nl〉 ≝ split ? 4 4 register in
    894909          let bit_1 ≝ get_index_v … nu 0 ? in
     
    896911            match bit_1 with
    897912              [ false ⇒
    898                 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ? s) in
    899                   set_low_internal_ram ? s memory
     913                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in
     914                  set_low_internal_ram ?? s memory
    900915              | true ⇒
    901                 let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ? s) in
    902                   set_high_internal_ram ? s memory
     916                let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in
     917                  set_high_internal_ram ?? s memory
    903918              ]
    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
     919      | REGISTER r ⇒ λregister: True. set_register ?? s r v
     920      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
     921      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
    907922      | EXT_INDIRECT e ⇒
    908923        λext_indirect: True.
    909           let address ≝ get_register ? s [[ false; false; e ]] in
     924          let address ≝ get_register ?? s [[ false; false; e ]] in
    910925          let padded_address ≝ pad 8 8 address in
    911           let memory ≝ insert ? 16 padded_address v (external_ram ? s) in
    912             set_external_ram ? s memory
     926          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
     927            set_external_ram ?? s memory
    913928      | EXT_INDIRECT_DPTR ⇒
    914929        λext_indirect_dptr: True.
    915           let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    916           let memory ≝ insert ? 16 address v (external_ram ? s) in
    917             set_external_ram ? s memory
     930          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
     931          let memory ≝ insert ? 16 address v (external_ram ?? s) in
     932            set_external_ram ?? s memory
    918933      | _ ⇒
    919934        λother: False.
     
    922937// qed.
    923938
    924 definition set_arg_8: ∀M: Type[0]. ∀s:PreStatus M. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M
     939definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M code_memory
    925940 set_arg_8'.
    926941
    927 lemma set_arg_8_ok: ∀M,s,x,v. clock M s = clock … (set_arg_8 M s x v).
    928  #M #s #x #v whd in match set_arg_8; normalize nodelta @pi2
     942lemma set_arg_8_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v).
     943 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta @pi2
    929944qed.
    930945
     
    980995qed.
    981996
    982 definition get_arg_1: ∀M: Type[0]. PreStatus M → [[ bit_addr ; n_bit_addr ; carry ]] →
     997definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] →
    983998                       bool → bool ≝
    984   λm, s, a, l.
     999  λm, cm, s, a, l.
    9851000    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
    9861001                                                 n_bit_addr ;
     
    9971012                let m ≝ address mod 8 in
    9981013                let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    999                 let sfr ≝ get_bit_addressable_sfr ? s ? trans l in
     1014                let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in
    10001015                  get_index_v … sfr m ?
    10011016              | false ⇒
    10021017                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    10031018                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1004                 let t ≝ lookup … 7 address' (low_internal_ram ? s) (zero 8) in
     1019                let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
    10051020                  get_index_v … t (modulus address 8) ?
    10061021              ]
     
    10161031                let m ≝ address mod 8 in
    10171032                let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1018                 let sfr ≝ get_bit_addressable_sfr ? s ? trans l in
     1033                let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in
    10191034                  ¬(get_index_v … sfr m ?)
    10201035              | false ⇒
    10211036                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    10221037                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1023                 let trans ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in
     1038                let trans ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
    10241039                  ¬(get_index_v … trans (modulus address 8) ?)
    10251040              ]
    1026       | CARRY ⇒ λcarry: True. get_cy_flag ? s
     1041      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
    10271042      | _ ⇒ λother.
    10281043        match other in False with [ ]
     
    10371052qed.
    10381053     
    1039 definition set_arg_1': ∀M: Type[0]. ∀s:PreStatus M. [[bit_addr; carry]] → Bit → Σs':PreStatus M. clock … s = clock … s' ≝
     1054definition set_arg_1': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s' ≝
    10401055  λm: Type[0].
    1041   λs: PreStatus m.
     1056  λcm.
     1057  λs: PreStatus m cm.
    10421058  λa: [[bit_addr; carry]].
    10431059  λv: Bit.
    1044     match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m s = clock m s' with
     1060    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with
    10451061      [ BIT_ADDR b ⇒ λbit_addr: True.
    1046         let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
     1062        let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    10471063        let bit_1 ≝ get_index_v ?? nu 0 ? in
    10481064        let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
     
    10531069            let m ≝ address mod 8 in
    10541070            let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1055             let sfr ≝ get_bit_addressable_sfr ? s ? t true in
     1071            let sfr ≝ get_bit_addressable_sfr ?? s ? t true in
    10561072            let new_sfr ≝ set_index … sfr m v ? in
    1057               set_bit_addressable_sfr ? s new_sfr t
     1073              set_bit_addressable_sfr ?? s new_sfr t
    10581074          | false ⇒
    10591075            let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    10601076            let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1061             let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in
     1077            let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
    10621078            let n_bit ≝ set_index … t (modulus address 8) v ? in
    1063             let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in
    1064               set_low_internal_ram ? s memory
     1079            let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
     1080              set_low_internal_ram ?? s memory
    10651081          ]
    10661082      | CARRY ⇒
    10671083        λcarry: True.
    1068         let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
     1084        let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    10691085        let bit_1 ≝ get_index_v… nu 1 ? in
    10701086        let bit_2 ≝ get_index_v… nu 2 ? in
    10711087        let bit_3 ≝ get_index_v… nu 3 ? in
    10721088        let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
    1073           set_8051_sfr ? s SFR_PSW new_psw
     1089          set_8051_sfr ?? s SFR_PSW new_psw
    10741090      | _ ⇒
    10751091        λother: False.
     
    10811097qed.
    10821098
    1083 definition set_arg_1: ∀M: Type[0]. PreStatus M → [[bit_addr; carry]] → Bit → PreStatus M ≝ set_arg_1'.
    1084 
    1085 lemma set_arg_1_ok: ∀M,s,x,v. clock M s = clock … (set_arg_1 M s x v).
    1086  #M #s #x #v whd in match set_arg_1; normalize nodelta @pi2
     1099definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝ set_arg_1'.
     1100
     1101lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v).
     1102 #M #cm #s #x #v whd in match set_arg_1; normalize nodelta @pi2
    10871103qed.
    10881104
     
    10931109
    10941110definition load ≝
    1095  λl.
     1111 λl,cm.
    10961112 λstatus.
    1097    set_code_memory (BitVectorTrie Word 16) ? status (load_code_memory l).
     1113   set_code_memory (BitVectorTrie Word 16) ? cm status (load_code_memory l).
    10981114
    10991115definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝
     
    13181334
    13191335definition address_of_word_labels ≝
    1320   λps: PseudoStatus.
     1336  λpr: pseudo_assembly_program.
    13211337  λid: Identifier.
    1322     address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
     1338    address_of_word_labels_code_mem (\snd pr) id.
    13231339
    13241340definition construct_datalabels: preamble → ? ≝
Note: See TracChangeset for help on using the changeset viewer.