Changeset 1666


Ignore:
Timestamp:
Jan 28, 2012, 1:42:15 PM (6 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.

Location:
src/ASM
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1649 r1666  
    14751475
    14761476axiom low_internal_ram_of_pseudo_internal_ram_hit:
    1477  ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀pol:policy (code_memory … s).∀addr:BitVector 7.
     1477 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀pol:policy cm.∀addr:BitVector 7.
    14781478  member ? (eq_bv 8) (false:::addr) M = true →
    14791479   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
    1480    let pbl ≝ lookup ? 7 addr (low_internal_ram ? s) (zero 8) in
    1481    let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram ? s) (zero 8) in
     1480   let pbl ≝ lookup ? 7 addr (low_internal_ram s) (zero 8) in
     1481   let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram s) (zero 8) in
    14821482   let bl ≝ lookup ? 7 addr ram (zero 8) in
    14831483   let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
    1484     bu@@bl = sigma (code_memory … s) pol (pbu@@pbl).
     1484    bu@@bl = sigma cm pol (pbu@@pbl).
    14851485
    14861486(* changed from add to sub *)
    14871487axiom low_internal_ram_of_pseudo_internal_ram_miss:
    1488  ∀T.∀M:internal_pseudo_address_map.∀s:PreStatus T.∀addr:BitVector 7.
     1488 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
    14891489  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
    14901490  let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
     
    14981498
    14991499definition addressing_mode_ok ≝
    1500  λT.λM:internal_pseudo_address_map.λs:PreStatus T.
     1500 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
    15011501  λaddr:addressing_mode.
    15021502   match addr with
     
    15051505       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
    15061506    | INDIRECT i ⇒
    1507        let d ≝ get_register ? s [[false;false;i]] in
     1507       let d ≝ get_register s [[false;false;i]] in
    15081508       ¬(member ? (eq_bv 8) d M) ∧
    15091509       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
     
    15301530  λfetched.
    15311531  λM: internal_pseudo_address_map.
    1532   λs: PreStatus T.
     1532  λcm:T.
     1533  λs: PreStatus T cm.
    15331534   match fetched with
    15341535    [ Comment _ ⇒ Some ? M
     
    15411542       match instr with
    15421543        [ ADD addr1 addr2 ⇒
    1543            if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
     1544           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
    15441545            Some ? M
    15451546           else
    15461547            None ?
    15471548        | ADDC addr1 addr2 ⇒
    1548            if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
     1549           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
    15491550            Some ? M
    15501551           else
    15511552            None ?
    15521553        | SUBB addr1 addr2 ⇒
    1553            if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
     1554           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
    15541555            Some ? M
    15551556           else
     
    15601561definition next_internal_pseudo_address_map ≝
    15611562 λM:internal_pseudo_address_map.
    1562   λs:PseudoStatus.
     1563 λcm.
     1564  λs:PseudoStatus cm.
    15631565    next_internal_pseudo_address_map0 ?
    1564      (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s.
    1565    
     1566     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s))) M cm s.
     1567
     1568definition code_memory_of_pseudo_assembly_program:
     1569 ∀pap:pseudo_assembly_program. policy pap → BitVectorTrie Byte 16
     1570≝ λpap,pol.
     1571   let p ≝ assembly pap pol in
     1572    load_code_memory (\fst p).
     1573
    15661574definition status_of_pseudo_status:
    1567  internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → Status ≝
    1568  λM,ps,pol.
    1569   let pap ≝ code_memory … ps in
    1570   let p ≝ assembly pap pol in
    1571   let cm ≝ load_code_memory (\fst p) in
    1572   let pc ≝ sigma pap pol (program_counter ? ps) in
     1575 internal_pseudo_address_map → ∀pap.∀ps:PseudoStatus pap. ∀pol:policy pap.
     1576  Status (code_memory_of_pseudo_assembly_program … pol) ≝
     1577 λM,pap,ps,pol.
     1578  let cm ≝ code_memory_of_pseudo_assembly_program … pol in
     1579  let pc ≝ sigma pap pol (program_counter … ps) in
    15731580  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
    15741581  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
     
    16451652qed.
    16461653*)
    1647 
    1648 axiom execute_1_pseudo_instruction_preserves_code_memory:
    1649  ∀ticks_of,ps.
    1650   code_memory … (execute_1_pseudo_instruction ticks_of ps) = code_memory … ps.
    16511654
    16521655(*
     
    19721975
    19731976axiom low_internal_ram_write_at_stack_pointer:
    1974  ∀T1,T2,M,s1,s2,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
    1975   get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
    1976   low_internal_ram ? s2 = low_internal_ram T2 s3 →
    1977   sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
     1977 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
     1978  get_8051_sfr ? cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
     1979  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
     1980  sp1 = \snd (half_add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1)) →
    19781981  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
    1979   bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
    1980    low_internal_ram T1
    1981      (write_at_stack_pointer ?
    1982        (set_8051_sfr ?
    1983          (write_at_stack_pointer ?
    1984            (set_8051_sfr ?
    1985              (set_low_internal_ram ? s1
    1986                (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2)))
     1982  bu@@bl = sigma cm2 pol (pbu@@pbl) →
     1983   low_internal_ram T1 cm1
     1984     (write_at_stack_pointer
     1985       (set_8051_sfr
     1986         (write_at_stack_pointer
     1987           (set_8051_sfr
     1988             (set_low_internal_ram s1
     1989               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram s2)))
    19871990             SFR_SP sp1)
    19881991          bl)
     
    19901993      bu)
    19911994   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
    1992       (low_internal_ram ?
    1993        (write_at_stack_pointer ?
    1994          (set_8051_sfr ?
    1995            (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
     1995      (low_internal_ram
     1996       (write_at_stack_pointer
     1997         (set_8051_sfr
     1998           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
    19961999          SFR_SP sp2)
    19972000        pbu)).
    19982001
    19992002axiom high_internal_ram_write_at_stack_pointer:
    2000  ∀T1,T2,M,s1,s2,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
    2001   get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
    2002   high_internal_ram ? s2 = high_internal_ram T2 s3 →
    2003   sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
     2003 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
     2004  get_8051_sfr ? cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
     2005  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
     2006  sp1 = \snd (half_add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1)) →
    20042007  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
    2005   bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
    2006    high_internal_ram T1
    2007      (write_at_stack_pointer ?
    2008        (set_8051_sfr ?
    2009          (write_at_stack_pointer ?
    2010            (set_8051_sfr ?
    2011              (set_high_internal_ram ? s1
    2012                (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ? s2)))
     2008  bu@@bl = sigma cm2 pol (pbu@@pbl) →
     2009   high_internal_ram T1 cm1
     2010     (write_at_stack_pointer
     2011       (set_8051_sfr
     2012         (write_at_stack_pointer
     2013           (set_8051_sfr
     2014             (set_high_internal_ram s1
     2015               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram s2)))
    20132016             SFR_SP sp1)
    20142017          bl)
     
    20162019      bu)
    20172020   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
    2018       (high_internal_ram ?
    2019        (write_at_stack_pointer ?
    2020          (set_8051_sfr ?
    2021            (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
     2021      (high_internal_ram
     2022       (write_at_stack_pointer
     2023         (set_8051_sfr
     2024           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
    20222025          SFR_SP sp2)
    20232026        pbu)).
     
    20292032
    20302033theorem main_thm:
    2031  ∀M,M',ps,pol,lookup_labels.
    2032   next_internal_pseudo_address_map M ps = Some … M' →
     2034 ∀M,M',cm,ps,pol,lookup_labels.
     2035  next_internal_pseudo_address_map M cm ps = Some … M' →
    20332036   ∃n.
    2034       execute n (status_of_pseudo_status M ps pol)
    2035     = status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol lookup_labels) ps) ?.
    2036  [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
    2037  #M #M' #ps #pol #lookup_labels #SAFE
    2038  cut
    2039   (∀ps'.
    2040     ∀prf:ps'=execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol lookup_labels) ps.
    2041     ∃n. execute n (status_of_pseudo_status M ps pol) = status_of_pseudo_status M' ps' ?)
    2042  [ >prf >execute_1_pseudo_instruction_preserves_code_memory @pol |3: #K @(K ? (refl …))]
    2043  #ps' #EQ
    2044  whd in ⊢ (??(λ_.??(??%)?));
    2045  change with
    2046   (∃n.
    2047     execute n
    2048      (set_low_internal_ram ?
    2049        (set_high_internal_ram ?
    2050          (set_program_counter ?
    2051            (set_code_memory ?? ps (load_code_memory ?))
    2052           (sigma ? pol (program_counter ? ps)))
    2053         (high_internal_ram_of_pseudo_high_internal_ram M ?))
    2054       (low_internal_ram_of_pseudo_low_internal_ram M ?))
    2055    = set_low_internal_ram ?
    2056       (set_high_internal_ram ?
    2057         (set_program_counter ?
    2058           (set_code_memory ?? ? (load_code_memory ?))
    2059          (sigma ???)) ?) ?);
    2060  >EQ whd in match eq_rect_Type0_r; normalize nodelta
    2061  >execute_1_pseudo_instruction_preserves_code_memory normalize nodelta
    2062  generalize in match EQ; -EQ;
    2063  generalize in match (refl … (code_memory pseudo_assembly_program ps));
    2064  generalize in match pol; -pol; generalize in ⊢ (∀_.??%? → ?);
    2065  * #preamble #instr_list #pol #EQ1 generalize in match pol; -pol <EQ1 #pol #EQps' <EQps'
    2066  (* Dependent types madness ends here *)
    2067  letin ppc ≝ (program_counter … ps)
     2037      execute n … (status_of_pseudo_status M … ps pol)
     2038    = status_of_pseudo_status M' … (execute_1_pseudo_instruction (ticks_of cm pol lookup_labels) cm ps) pol.
     2039 #M #M' * #preamble #instr_list #ps
     2040 letin ppc ≝ (program_counter ?? ps)
     2041 #pol #lookup_labels
     2042 change with (next_internal_pseudo_address_map0 ????? = ? → ?)
     2043 change with (next_internal_pseudo_address_map0 ? (\fst (fetch_pseudo_instruction ? ppc)) ??? = ? → ?)
    20682044 generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ?;
    20692045 letin assembled ≝ (\fst (assembly ? pol))
    20702046 letin lookup_labels ≝ (λx.(address_of_word_labels_code_mem instr_list x))
    20712047 letin lookup_datalabels ≝ (λx. lookup_def … (construct_datalabels preamble) x (zero 16))
    2072  @pair_elim #pi #newppc #EQ2
    2073  letin instructions ≝
    2074   (expand_pseudo_instruction lookup_labels ppc ((pi1 ?? pol) lookup_labels ppc) lookup_datalabels
    2075     pi)
    2076  change with (fetch_many ???? → ?); #H1
    2077  change with (fetch_pseudo_instruction instr_list ppc = ?) in EQ2;
    2078  change with (next_internal_pseudo_address_map0 ???? = ?) in SAFE; <EQ1 in SAFE;
    2079  >EQ2 whd in ⊢ (??(??%??)? → ?); #SAFE
    2080  whd in EQps':(???%); <EQ1 in EQps'; >EQ2 normalize nodelta
    2081  generalize in match H1; -H1; generalize in match instructions; -instructions
    2082  * #instructions >EQ2 change with pi in match (\fst 〈pi,newppc〉);
    2083  whd in match ticks_of; normalize nodelta <EQ1 >EQ2
    2084  cases pi in SAFE;
    2085   [2,3: (* Comment, Cost *) #ARG whd in ⊢ (??%? → ???% → ?);
    2086    @Some_Some_elim #MAP #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
    2087    whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
    2088    #H2 #EQ %[1,3:@0]
    2089    <MAP >(eq_bv_eq … H2) >EQ %
     2048 whd in match execute_1_pseudo_instruction; normalize nodelta
     2049 @pair_elim #pi #newppc change with (fetch_pseudo_instruction ? ppc = ? → ?) #EQ2
     2050 whd in match ticks_of;
     2051 normalize nodelta change with ppc in match ppc; change with assembled in match assembled;
     2052 change with lookup_labels in match lookup_labels; change with lookup_datalabels in match lookup_datalabels;
     2053 #H1 >EQ2
     2054 inversion pi
     2055  [2,3: (* Comment, Cost *) #ARG #EQ >EQ in H1; #H1 whd in ⊢ (??%? → ?);
     2056   @Some_Some_elim #MAP <MAP NEEDS assembly_1_pseudoinstruction_ok now commented out
     2057   in Assembly.ma
     2058   %{0} @split_eq_status try %
     2059   lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQ3 >EQ3
     2060   
     2061   >(eq_bv_eq … H2) >EQ %
    20902062  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)
    20912063   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
  • src/ASM/Interpret.ma

    r1606 r1666  
    1 include "ASM/Status.ma".
     1include "ASM/StatusProofs.ma".
    22include "ASM/Fetch.ma".
    33
     
    119119include alias "ASM/BitVectorTrie.ma".
    120120
    121 
    122 lemma set_flags_ignores_clock:
    123  ∀M,s,f1,f2,f3. clock M s = clock … (set_flags … s f1 f2 f3).
    124 //
    125 qed.
    126 
    127 lemma set_program_counter_ignores_clock:
    128   ∀M: Type[0].
    129   ∀s: PreStatus M.
    130   ∀pc: Word.
    131     clock M (set_program_counter … s pc) = clock … s.
    132   #M #s #pc %
    133 qed.
    134 
    135 lemma set_low_internal_ram_ignores_clock:
    136   ∀M: Type[0].
    137   ∀s: PreStatus M.
    138   ∀ram: BitVectorTrie Byte 7.
    139     clock … (set_low_internal_ram … s ram) = clock … s.
    140   #M #s #ram %
    141 qed.
    142 
    143 lemma set_high_internal_ram_ignores_clock:
    144   ∀m: Type[0].
    145   ∀s: PreStatus m.
    146   ∀ram: BitVectorTrie Byte 7.
    147     clock … (set_high_internal_ram … s ram) = clock … s.
    148   #m #s #ram %
    149 qed.
    150 
    151 lemma set_8051_sfr_ignores_clock:
    152   ∀M: Type[0].
    153   ∀s: PreStatus M.
    154   ∀sfr: SFR8051.
    155   ∀v: Byte.
    156     clock … (set_8051_sfr ? s sfr v) = clock … s.
    157   #M #s #sfr #v %
    158 qed.
    159 
    160 lemma write_at_stack_pointer_ignores_clock:
    161   ∀m: Type[0].
    162   ∀s: PreStatus m.
    163   ∀v: Byte.
    164     clock … (write_at_stack_pointer m s v) = clock … s.
    165   #m #s #v
    166   whd in match write_at_stack_pointer; normalize nodelta
    167   cases(split … 4 4 ?) #nu #nl normalize nodelta
    168   cases(get_index_v … 4 nu 0 ?) normalize nodelta
    169   [ >set_low_internal_ram_ignores_clock | >set_high_internal_ram_ignores_clock ] %
    170 qed.
    171 
    172 lemma clock_set_clock:
    173   ∀M: Type[0].
    174   ∀s: PreStatus M.
    175   ∀v.
    176     clock … (set_clock … s v) = v.
    177   #M #s #v %
    178 qed.
    179 
    180121definition execute_1_preinstruction':
    181122  ∀ticks: nat × nat.
    182   ∀a, m: Type[0]. (a → PreStatus m → Word) → preinstruction a →
    183   ∀s: PreStatus m.
    184     Σs': PreStatus m.
    185       Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) ≝
     123  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a →
     124  ∀s: PreStatus m cm.
     125    Σs': PreStatus m cm.
     126      Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) ≝
    186127  λticks: nat × nat.
    187   λa, m: Type[0].
    188   λaddr_of: a → PreStatus m → Word.
     128  λa, m: Type[0]. λcm.
     129  λaddr_of: a → PreStatus m cm → Word.
    189130  λinstr: preinstruction a.
    190   λs: PreStatus m.
    191   let add_ticks1 ≝ λs: PreStatus m. set_clock … s (\fst ticks + clock … s) in
    192   let add_ticks2 ≝ λs: PreStatus m. set_clock … s (\snd ticks + clock … s) in
    193   match instr return λx. Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
     131  λs: PreStatus m cm.
     132  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
     133  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
     134  match instr in preinstruction return λx. Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock ?? s) (clock ?? s' = \snd ticks + clock ?? s) with
    194135        [ ADD addr1 addr2 ⇒
    195136            let s ≝ add_ticks1 s in
    196             let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
    197                                                    (get_arg_8 ? s false addr2) false in
     137            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
     138                                                   (get_arg_8 s false addr2) false in
    198139            let cy_flag ≝ get_index' ? O  ? flags in
    199140            let ac_flag ≝ get_index' ? 1 ? flags in
    200141            let ov_flag ≝ get_index' ? 2 ? flags in
    201             let s ≝ set_arg_8 ? s ACC_A result in
    202               set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
     142            let s ≝ set_arg_8 s ACC_A result in
     143              set_flags s cy_flag (Some Bit ac_flag) ov_flag
    203144        | ADDC addr1 addr2 ⇒
    204145            let s ≝ add_ticks1 s in
    205             let old_cy_flag ≝ get_cy_flag ? s in
    206             let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
    207                                                    (get_arg_8 ? s false addr2) old_cy_flag in
     146            let old_cy_flag ≝ get_cy_flag ?? s in
     147            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
     148                                                   (get_arg_8 s false addr2) old_cy_flag in
    208149            let cy_flag ≝ get_index' ? O ? flags in
    209150            let ac_flag ≝ get_index' ? 1 ? flags in
    210151            let ov_flag ≝ get_index' ? 2 ? flags in
    211             let s ≝ set_arg_8 ? s ACC_A result in
    212               set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
     152            let s ≝ set_arg_8 s ACC_A result in
     153              set_flags s cy_flag (Some Bit ac_flag) ov_flag
    213154        | SUBB addr1 addr2 ⇒
    214155            let s ≝ add_ticks1 s in
    215             let old_cy_flag ≝ get_cy_flag ? s in
    216             let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1)
    217                                                    (get_arg_8 ? s false addr2) old_cy_flag in
     156            let old_cy_flag ≝ get_cy_flag ?? s in
     157            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
     158                                                   (get_arg_8 s false addr2) old_cy_flag in
    218159            let cy_flag ≝ get_index' ? O ? flags in
    219160            let ac_flag ≝ get_index' ? 1 ? flags in
    220161            let ov_flag ≝ get_index' ? 2 ? flags in
    221             let s ≝ set_arg_8 ? s ACC_A result in
    222               set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
     162            let s ≝ set_arg_8 s ACC_A result in
     163              set_flags s cy_flag (Some Bit ac_flag) ov_flag
    223164        | ANL addr ⇒
    224165          let s ≝ add_ticks1 s in
     
    228169                [ inl l' ⇒
    229170                  let 〈addr1, addr2〉 ≝ l' in
    230                   let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    231                     set_arg_8 ? s addr1 and_val
     171                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     172                    set_arg_8 s addr1 and_val
    232173                | inr r ⇒
    233174                  let 〈addr1, addr2〉 ≝ r in
    234                   let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    235                     set_arg_8 ? s addr1 and_val
     175                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     176                    set_arg_8 s addr1 and_val
    236177                ]
    237178            | inr r ⇒
    238179              let 〈addr1, addr2〉 ≝ r in
    239               let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
    240                set_flags ? s and_val (None ?) (get_ov_flag ? s)
     180              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
     181               set_flags … s and_val (None ?) (get_ov_flag ?? s)
    241182            ]
    242183        | ORL addr ⇒
     
    247188                [ inl l' ⇒
    248189                  let 〈addr1, addr2〉 ≝ l' in
    249                   let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    250                     set_arg_8 ? s addr1 or_val
     190                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     191                    set_arg_8 s addr1 or_val
    251192                | inr r ⇒
    252193                  let 〈addr1, addr2〉 ≝ r in
    253                   let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    254                     set_arg_8 ? s addr1 or_val
     194                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     195                    set_arg_8 s addr1 or_val
    255196                ]
    256197            | inr r ⇒
    257198              let 〈addr1, addr2〉 ≝ r in
    258               let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in
    259                set_flags ? s or_val (None ?) (get_ov_flag ? s)
     199              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
     200               set_flags … s or_val (None ?) (get_ov_flag … s)
    260201            ]
    261202        | XRL addr ⇒
     
    264205            [ inl l' ⇒
    265206              let 〈addr1, addr2〉 ≝ l' in
    266               let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    267                 set_arg_8 ? s addr1 xor_val
     207              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     208                set_arg_8 s addr1 xor_val
    268209            | inr r ⇒
    269210              let 〈addr1, addr2〉 ≝ r in
    270               let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    271                 set_arg_8 ? s addr1 xor_val
     211              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     212                set_arg_8 s addr1 xor_val
    272213            ]
    273214        | INC addr ⇒
    274             match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
     215            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
    275216              [ ACC_A ⇒ λacc_a: True.
    276217                let s' ≝ add_ticks1 s in
    277                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true ACC_A) (bitvector_of_nat 8 1) in
    278                  set_arg_8 ? s' ACC_A result
     218                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s' true ACC_A) (bitvector_of_nat 8 1) in
     219                 set_arg_8 s' ACC_A result
    279220              | REGISTER r ⇒ λregister: True.
    280221                let s' ≝ add_ticks1 s in
    281                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (REGISTER r)) (bitvector_of_nat 8 1) in
    282                  set_arg_8 ? s' (REGISTER r) result
     222                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s' true (REGISTER r)) (bitvector_of_nat 8 1) in
     223                 set_arg_8 s' (REGISTER r) result
    283224              | DIRECT d ⇒ λdirect: True.
    284225                let s' ≝ add_ticks1 s in
    285                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (DIRECT d)) (bitvector_of_nat 8 1) in
    286                  set_arg_8 ? s' (DIRECT d) result
     226                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s' true (DIRECT d)) (bitvector_of_nat 8 1) in
     227                 set_arg_8 s' (DIRECT d) result
    287228              | INDIRECT i ⇒ λindirect: True.
    288229                let s' ≝ add_ticks1 s in
    289                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
    290                  set_arg_8 ? s' (INDIRECT i) result
     230                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
     231                 set_arg_8 s' (INDIRECT i) result
    291232              | DPTR ⇒ λdptr: True.
    292233                let s' ≝ add_ticks1 s in
    293                 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s' SFR_DPL) (bitvector_of_nat 8 1) in
    294                 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s' SFR_DPH) (zero 8) carry in
    295                 let s ≝ set_8051_sfr ? s' SFR_DPL bl in
    296                  set_8051_sfr ? s' SFR_DPH bu
     234                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s' SFR_DPL) (bitvector_of_nat 8 1) in
     235                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s' SFR_DPH) (zero 8) carry in
     236                let s ≝ set_8051_sfr s' SFR_DPL bl in
     237                 set_8051_sfr s' SFR_DPH bu
    297238              | _ ⇒ λother: False. ⊥
    298239              ] (subaddressing_modein … addr)
     
    302243        | DEC addr ⇒
    303244           let s ≝ add_ticks1 s in
    304            let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
    305              set_arg_8 ? s addr result
     245           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat 8 1) false in
     246             set_arg_8 s addr result
    306247        | MUL addr1 addr2 ⇒
    307248           let s ≝ add_ticks1 s in
    308            let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
    309            let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
     249           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in
     250           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in
    310251           let product ≝ acc_a_nat * acc_b_nat in
    311252           let ov_flag ≝ product ≥ 256 in
    312253           let low ≝ bitvector_of_nat 8 (product mod 256) in
    313254           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
    314            let s ≝ set_8051_sfr ? s SFR_ACC_A low in
    315              set_8051_sfr ? s SFR_ACC_B high
     255           let s ≝ set_8051_sfr s SFR_ACC_A low in
     256             set_8051_sfr s SFR_ACC_B high
    316257        | DIV addr1 addr2 ⇒
    317258           let s ≝ add_ticks1 s in
    318            let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
    319            let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
     259           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in
     260           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in
    320261             match acc_b_nat with
    321                [ O ⇒ set_flags ? s false (None Bit) true
     262               [ O ⇒ set_flags s false (None Bit) true
    322263               | S o ⇒
    323264                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
    324265                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
    325                  let s ≝ set_8051_sfr ? s SFR_ACC_A q in
    326                  let s ≝ set_8051_sfr ? s SFR_ACC_B r in
    327                    set_flags ? s false (None Bit) false
     266                 let s ≝ set_8051_sfr s SFR_ACC_A q in
     267                 let s ≝ set_8051_sfr s SFR_ACC_B r in
     268                   set_flags s false (None Bit) false
    328269               ]
    329270        | DA addr ⇒
    330271            let s ≝ add_ticks1 s in
    331             let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
    332               if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then
    333                 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in
     272            let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr s SFR_ACC_A) in
     273              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag s) then
     274                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat 8 6) false in
    334275                let cy_flag ≝ get_index' ? O ? flags in
    335276                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
     
    337278                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
    338279                    let new_acc ≝ nu @@ acc_nl' in
    339                     let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
    340                       set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ? s)
     280                    let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
     281                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
    341282                  else
    342283                    s
     
    344285                s
    345286        | CLR addr ⇒
    346           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
     287          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
    347288            [ ACC_A ⇒ λacc_a: True.
    348289              let s ≝ add_ticks1 s in
    349                set_arg_8 ? s ACC_A (zero 8)
     290               set_arg_8 s ACC_A (zero 8)
    350291            | CARRY ⇒ λcarry: True.
    351292              let s ≝ add_ticks1 s in
    352                set_arg_1 ? s CARRY false
     293               set_arg_1 s CARRY false
    353294            | BIT_ADDR b ⇒ λbit_addr: True.
    354295              let s ≝ add_ticks1 s in
    355                set_arg_1 ? s (BIT_ADDR b) false
     296               set_arg_1 s (BIT_ADDR b) false
    356297            | _ ⇒ λother: False. ⊥
    357298            ] (subaddressing_modein … addr)
    358299        | CPL addr ⇒
    359           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
     300          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
    360301            [ ACC_A ⇒ λacc_a: True.
    361302                let s ≝ add_ticks1 s in
    362                 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     303                let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    363304                let new_acc ≝ negation_bv ? old_acc in
    364                  set_8051_sfr ? s SFR_ACC_A new_acc
     305                 set_8051_sfr s SFR_ACC_A new_acc
    365306            | CARRY ⇒ λcarry: True.
    366307                let s ≝ add_ticks1 s in
    367                 let old_cy_flag ≝ get_arg_1 ? s CARRY true in
     308                let old_cy_flag ≝ get_arg_1 s CARRY true in
    368309                let new_cy_flag ≝ ¬old_cy_flag in
    369                  set_arg_1 ? s CARRY new_cy_flag
     310                 set_arg_1 s CARRY new_cy_flag
    370311            | BIT_ADDR b ⇒ λbit_addr: True.
    371312                let s ≝ add_ticks1 s in
    372                 let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
     313                let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in
    373314                let new_bit ≝ ¬old_bit in
    374                  set_arg_1 ? s (BIT_ADDR b) new_bit
     315                 set_arg_1 s (BIT_ADDR b) new_bit
    375316            | _ ⇒ λother: False. ?
    376317            ] (subaddressing_modein … addr)
    377318        | SETB b ⇒
    378319            let s ≝ add_ticks1 s in
    379             set_arg_1 ? s b false
     320            set_arg_1 s b false
    380321        | RL _ ⇒ (* DPM: always ACC_A *)
    381322            let s ≝ add_ticks1 s in
    382             let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     323            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    383324            let new_acc ≝ rotate_left … 1 old_acc in
    384               set_8051_sfr ? s SFR_ACC_A new_acc
     325              set_8051_sfr s SFR_ACC_A new_acc
    385326        | RR _ ⇒ (* DPM: always ACC_A *)
    386327            let s ≝ add_ticks1 s in
    387             let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     328            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    388329            let new_acc ≝ rotate_right … 1 old_acc in
    389               set_8051_sfr ? s SFR_ACC_A new_acc
     330              set_8051_sfr s SFR_ACC_A new_acc
    390331        | RLC _ ⇒ (* DPM: always ACC_A *)
    391332            let s ≝ add_ticks1 s in
    392             let old_cy_flag ≝ get_cy_flag ? s in
    393             let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     333            let old_cy_flag ≝ get_cy_flag ?? s in
     334            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    394335            let new_cy_flag ≝ get_index' ? O ? old_acc in
    395336            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
    396             let s ≝ set_arg_1 ? s CARRY new_cy_flag in
    397               set_8051_sfr ? s SFR_ACC_A new_acc
     337            let s ≝ set_arg_1 s CARRY new_cy_flag in
     338              set_8051_sfr s SFR_ACC_A new_acc
    398339        | RRC _ ⇒ (* DPM: always ACC_A *)
    399340            let s ≝ add_ticks1 s in
    400             let old_cy_flag ≝ get_cy_flag ? s in
    401             let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     341            let old_cy_flag ≝ get_cy_flag ?? s in
     342            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    402343            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
    403344            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
    404             let s ≝ set_arg_1 ? s CARRY new_cy_flag in
    405               set_8051_sfr ? s SFR_ACC_A new_acc
     345            let s ≝ set_arg_1 s CARRY new_cy_flag in
     346              set_8051_sfr s SFR_ACC_A new_acc
    406347        | SWAP _ ⇒ (* DPM: always ACC_A *)
    407348            let s ≝ add_ticks1 s in
    408             let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     349            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    409350            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
    410351            let new_acc ≝ nl @@ nu in
    411               set_8051_sfr ? s SFR_ACC_A new_acc
     352              set_8051_sfr s SFR_ACC_A new_acc
    412353        | PUSH addr ⇒
    413             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
     354            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
    414355              [ DIRECT d ⇒ λdirect: True.
    415356                let s ≝ add_ticks1 s in
    416                 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    417                 let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    418                   write_at_stack_pointer ? s d
     357                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     358                let s ≝ set_8051_sfr s SFR_SP new_sp in
     359                  write_at_stack_pointer s d
    419360              | _ ⇒ λother: False. ⊥
    420361              ] (subaddressing_modein … addr)
    421362        | POP addr ⇒
    422363            let s ≝ add_ticks1 s in
    423             let contents ≝ read_at_stack_pointer ? s in
    424             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
    425             let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    426               set_arg_8 ? s addr contents
     364            let contents ≝ read_at_stack_pointer ?? s in
     365            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
     366            let s ≝ set_8051_sfr s SFR_SP new_sp in
     367              set_arg_8 s addr contents
    427368        | XCH addr1 addr2 ⇒
    428369            let s ≝ add_ticks1 s in
    429             let old_addr ≝ get_arg_8 ? s false addr2 in
    430             let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    431             let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in
    432               set_arg_8 ? s addr2 old_acc
     370            let old_addr ≝ get_arg_8 s false addr2 in
     371            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     372            let s ≝ set_8051_sfr s SFR_ACC_A old_addr in
     373              set_arg_8 s addr2 old_acc
    433374        | XCHD addr1 addr2 ⇒
    434375            let s ≝ add_ticks1 s in
    435             let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in
    436             let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in
     376            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr s SFR_ACC_A) in
     377            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 s false addr2) in
    437378            let new_acc ≝ acc_nu @@ arg_nl in
    438379            let new_arg ≝ arg_nu @@ acc_nl in
    439             let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
    440               set_arg_8 ? s addr2 new_arg
     380            let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
     381              set_arg_8 s addr2 new_arg
    441382        | RET ⇒
    442383            let s ≝ add_ticks1 s in
    443             let high_bits ≝ read_at_stack_pointer ? s in
    444             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
    445             let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    446             let low_bits ≝ read_at_stack_pointer ? s in
    447             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
    448             let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     384            let high_bits ≝ read_at_stack_pointer ?? s in
     385            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
     386            let s ≝ set_8051_sfr s SFR_SP new_sp in
     387            let low_bits ≝ read_at_stack_pointer ?? s in
     388            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
     389            let s ≝ set_8051_sfr s SFR_SP new_sp in
    449390            let new_pc ≝ high_bits @@ low_bits in
    450               set_program_counter ? s new_pc
     391              set_program_counter s new_pc
    451392        | RETI ⇒
    452393            let s ≝ add_ticks1 s in
    453             let high_bits ≝ read_at_stack_pointer ? s in
    454             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
    455             let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    456             let low_bits ≝ read_at_stack_pointer ? s in
    457             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
    458             let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     394            let high_bits ≝ read_at_stack_pointer ?? s in
     395            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
     396            let s ≝ set_8051_sfr s SFR_SP new_sp in
     397            let low_bits ≝ read_at_stack_pointer ?? s in
     398            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
     399            let s ≝ set_8051_sfr s SFR_SP new_sp in
    459400            let new_pc ≝ high_bits @@ low_bits in
    460               set_program_counter ? s new_pc
     401              set_program_counter s new_pc
    461402        | MOVX addr ⇒
    462403          let s ≝ add_ticks1 s in
     
    465406            [ inl l ⇒
    466407              let 〈addr1, addr2〉 ≝ l in
    467                 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     408                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
    468409            | inr r ⇒
    469410              let 〈addr1, addr2〉 ≝ r in
    470                 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     411                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
    471412            ]
    472413        | MOV addr ⇒
     
    483424                            [ inl l'''' ⇒
    484425                              let 〈addr1, addr2〉 ≝ l'''' in
    485                                 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     426                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
    486427                            | inr r'''' ⇒
    487428                              let 〈addr1, addr2〉 ≝ r'''' in
    488                                 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     429                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
    489430                            ]
    490431                        | inr r''' ⇒
    491432                          let 〈addr1, addr2〉 ≝ r''' in
    492                             set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     433                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
    493434                        ]
    494435                    | inr r'' ⇒
    495436                      let 〈addr1, addr2〉 ≝ r'' in
    496                        set_arg_16 ? s (get_arg_16 ? s addr2) addr1
     437                       set_arg_16 … s (get_arg_16 … s addr2) addr1
    497438                    ]
    498439                | inr r ⇒
    499440                  let 〈addr1, addr2〉 ≝ r in
    500                    set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
     441                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
    501442                ]
    502443            | inr r ⇒
    503444              let 〈addr1, addr2〉 ≝ r in
    504                set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
     445               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
    505446            ]
    506447          | JC addr ⇒
    507                   if get_cy_flag ? s then
     448                  if get_cy_flag ?? s then
    508449                    let s ≝ add_ticks1 s in
    509                       set_program_counter ? s (addr_of addr s)
     450                      set_program_counter s (addr_of addr s)
    510451                  else
    511452                    let s ≝ add_ticks2 s in
    512453                      s
    513454            | JNC addr ⇒
    514                   if ¬(get_cy_flag ? s) then
     455                  if ¬(get_cy_flag ?? s) then
    515456                   let s ≝ add_ticks1 s in
    516                      set_program_counter ? s (addr_of addr s)
     457                     set_program_counter s (addr_of addr s)
    517458                  else
    518459                   let s ≝ add_ticks2 s in
    519460                    s
    520461            | JB addr1 addr2 ⇒
    521                   if get_arg_1 ? s addr1 false then
     462                  if get_arg_1 s addr1 false then
    522463                   let s ≝ add_ticks1 s in
    523                     set_program_counter ? s (addr_of addr2 s)
     464                    set_program_counter s (addr_of addr2 s)
    524465                  else
    525466                   let s ≝ add_ticks2 s in
    526467                    s
    527468            | JNB addr1 addr2 ⇒
    528                   if ¬(get_arg_1 ? s addr1 false) then
     469                  if ¬(get_arg_1 s addr1 false) then
    529470                   let s ≝ add_ticks1 s in
    530                     set_program_counter ? s (addr_of addr2 s)
     471                    set_program_counter s (addr_of addr2 s)
    531472                  else
    532473                   let s ≝ add_ticks2 s in
    533474                    s
    534475            | JBC addr1 addr2 ⇒
    535                   let s ≝ set_arg_1 ? s addr1 false in
    536                     if get_arg_1 ? s addr1 false then
     476                  let s ≝ set_arg_1 s addr1 false in
     477                    if get_arg_1 s addr1 false then
    537478                     let s ≝ add_ticks1 s in
    538                       set_program_counter ? s (addr_of addr2 s)
     479                      set_program_counter s (addr_of addr2 s)
    539480                    else
    540481                     let s ≝ add_ticks2 s in
    541482                      s
    542483            | JZ addr ⇒
    543                     if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
     484                    if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then
    544485                     let s ≝ add_ticks1 s in
    545                       set_program_counter ? s (addr_of addr s)
     486                      set_program_counter s (addr_of addr s)
    546487                    else
    547488                     let s ≝ add_ticks2 s in
    548489                      s
    549490            | JNZ addr ⇒
    550                     if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
     491                    if ¬(eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then
    551492                     let s ≝ add_ticks1 s in
    552                       set_program_counter ? s (addr_of addr s)
     493                      set_program_counter s (addr_of addr s)
    553494                    else
    554495                     let s ≝ add_ticks2 s in
     
    558499                    [ inl l ⇒
    559500                        let 〈addr1, addr2'〉 ≝ l in
    560                         let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
    561                                                  (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
    562                           if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
     501                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
     502                                                 (nat_of_bitvector ? (get_arg_8 s false addr2')) in
     503                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
    563504                            let s ≝ add_ticks1 s in
    564                             let s ≝ set_program_counter ? s (addr_of addr2 s) in
    565                               set_flags ? s new_cy (None ?) (get_ov_flag ? s)
     505                            let s ≝ set_program_counter s (addr_of addr2 s) in
     506                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
    566507                          else
    567508                            let s ≝ add_ticks2 s in
    568                               set_flags ? s new_cy (None ?) (get_ov_flag ? s)
     509                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
    569510                    | inr r' ⇒
    570511                        let 〈addr1, addr2'〉 ≝ r' in
    571                         let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
    572                                                  (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
    573                           if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
     512                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
     513                                                 (nat_of_bitvector ? (get_arg_8 s false addr2')) in
     514                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
    574515                            let s ≝ add_ticks1 s in
    575                             let s ≝ set_program_counter ? s (addr_of addr2 s) in
    576                               set_flags ? s new_cy (None ?) (get_ov_flag ? s)
     516                            let s ≝ set_program_counter s (addr_of addr2 s) in
     517                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
    577518                          else
    578519                            let s ≝ add_ticks2 s in
    579                               set_flags ? s new_cy (None ?) (get_ov_flag ? s)
     520                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
    580521                    ]
    581522            | DJNZ addr1 addr2 ⇒
    582               let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in
    583               let s ≝ set_arg_8 ? s addr1 result in
     523              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in
     524              let s ≝ set_arg_8 s addr1 result in
    584525                if ¬(eq_bv ? result (zero 8)) then
    585526                 let s ≝ add_ticks1 s in
    586                   set_program_counter ? s (addr_of addr2 s)
     527                  set_program_counter s (addr_of addr2 s)
    587528                else
    588529                 let s ≝ add_ticks2 s in
    589530                  s
    590         ]. (*15s*)
     531 |_ ⇒ ?            ]. (*15s*)
    591532    try (cases(other))
    592533    try assumption (*20s*)
     
    597538    ) (*66s*)
    598539    normalize nodelta /2 by or_introl, or_intror/ (*35s*)
     540    (*CSC: the times are now much longer. I suspect because the inclusion of
     541      all StatusProofs makes the search space larger :-( *)
    599542qed.
    600543
    601544definition execute_1_preinstruction:
    602545  ∀ticks: nat × nat.
    603   ∀a, m: Type[0]. (a → PreStatus m → Word) → preinstruction a →
    604   PreStatus m → PreStatus m ≝ execute_1_preinstruction'.
     546  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a →
     547  PreStatus m cm → PreStatus m cm ≝ execute_1_preinstruction'.
    605548 
    606549lemma execute_1_preinstruction_ok:
    607  ∀ticks,a,m,f,i,s.
    608   clock ? (execute_1_preinstruction ticks a m f i s) = \fst ticks + clock … s ∨
    609   clock ? (execute_1_preinstruction ticks a m f i s) = \snd ticks + clock … s.
    610  #ticks #a #m #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2
     550 ∀ticks,a,m,cm,f,i,s.
     551  clock ?? (execute_1_preinstruction ticks a m cm f i s) = \fst ticks + clock … s ∨
     552  clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s.
     553 #ticks #a #m #cm #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2
    611554qed.
    612555
    613 definition execute_1_0: ∀s: Status. ∀current:instruction × Word × nat.
    614   Σs': Status. clock … s' = \snd current + clock … s ≝
    615   λs0,instr_pc_ticks.
     556definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
     557  Σs': Status cm. clock ?? s' = \snd current + clock … s ≝
     558  λcm,s0,instr_pc_ticks.
    616559    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
    617560    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    618     let s ≝ set_program_counter ? s0 pc in
    619       match instr return λ_.Status with
    620       [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ?
     561    let s ≝ set_program_counter s0 pc in
     562      match instr return λ_.Status cm with
     563      [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]]
    621564        (λx. λs.
    622565        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    623         [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
     566        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter s) (sign_extension r))
    624567        | _ ⇒ λabsd. ⊥
    625568        ] (subaddressing_modein … x)) instr s
    626569      | MOVC addr1 addr2 ⇒
    627           let s ≝ set_clock ? s (ticks + clock ? s) in
    628           match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
     570          let s ≝ set_clock … s (ticks + clock … s) in
     571          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
    629572            [ ACC_DPTR ⇒ λacc_dptr: True.
    630               let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    631               let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
     573              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
     574              let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
    632575              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
    633               let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
    634                 set_8051_sfr ? s SFR_ACC_A result
     576              let result ≝ lookup ? ? new_addr cm (zero ?) in
     577                set_8051_sfr s SFR_ACC_A result
    635578            | ACC_PC ⇒ λacc_pc: True.
    636               let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    637               let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in
     579              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
     580              let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ?? s) (bitvector_of_nat 16 1) in
    638581              (* DPM: Under specified: does the carry from PC incrementation affect the *)
    639582              (*      addition of the PC with the DPTR? At the moment, no.              *)
    640               let s ≝ set_program_counter ? s inc_pc in
     583              let s ≝ set_program_counter s inc_pc in
    641584              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
    642               let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
    643                 set_8051_sfr ? s SFR_ACC_A result
     585              let result ≝ lookup ? ? new_addr cm (zero ?) in
     586                set_8051_sfr s SFR_ACC_A result
    644587            | _ ⇒ λother: False. ⊥
    645588            ] (subaddressing_modein … addr2)
    646589      | JMP _ ⇒ (* DPM: always indirect_dptr *)
    647           let s ≝ set_clock ? s (ticks + clock ? s) in
    648           let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    649           let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
     590          let s ≝ set_clock … s (ticks + clock … s) in
     591          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
     592          let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
    650593          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
    651           let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
    652             set_program_counter ? s new_pc
     594          let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in
     595            set_program_counter s new_pc
    653596      | LJMP addr ⇒
    654           let s ≝ set_clock ? s (ticks + clock ? s) in
    655           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
     597          let s ≝ set_clock … s (ticks + clock … s) in
     598          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
    656599            [ ADDR16 a ⇒ λaddr16: True.
    657                 set_program_counter ? s a
     600                set_program_counter s a
    658601            | _ ⇒ λother: False. ⊥
    659602            ] (subaddressing_modein … addr)
    660603      | SJMP addr ⇒
    661           let s ≝ set_clock ? s (ticks + clock ? s) in
    662           match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
     604          let s ≝ set_clock … s (ticks + clock … s) in
     605          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
    663606            [ RELATIVE r ⇒ λrelative: True.
    664                 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    665                   set_program_counter ? s new_pc
     607                let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     608                  set_program_counter s new_pc
    666609            | _ ⇒ λother: False. ⊥
    667610            ] (subaddressing_modein … addr)
    668611      | AJMP addr ⇒
    669           let s ≝ set_clock ? s (ticks + clock ? s) in
    670           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
     612          let s ≝ set_clock … s (ticks + clock … s) in
     613          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
    671614            [ ADDR11 a ⇒ λaddr11: True.
    672               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     615              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
    673616              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
    674617              let bit ≝ get_index' ? O ? nl in
    675618              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
    676619              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    677               let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
    678                 set_program_counter ? s new_pc
     620              let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
     621                set_program_counter s new_pc
    679622            | _ ⇒ λother: False. ⊥
    680623            ] (subaddressing_modein … addr)
    681624      | ACALL addr ⇒
    682           let s ≝ set_clock ? s (ticks + clock ? s) in
    683           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
     625          let s ≝ set_clock … s (ticks + clock … s) in
     626          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
    684627            [ ADDR11 a ⇒ λaddr11: True.
    685               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    686               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    687               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    688               let s ≝ write_at_stack_pointer ? s pc_bl in
    689               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    690               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    691               let s ≝ write_at_stack_pointer ? s pc_bu in
     628              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     629              let s ≝ set_8051_sfr s SFR_SP new_sp in
     630              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     631              let s ≝ write_at_stack_pointer s pc_bl in
     632              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     633              let s ≝ set_8051_sfr s SFR_SP new_sp in
     634              let s ≝ write_at_stack_pointer s pc_bu in
    692635              let 〈thr, eig〉 ≝ split ? 3 8 a in
    693636              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
    694637              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    695                 set_program_counter ? s new_addr
     638                set_program_counter s new_addr
    696639            | _ ⇒ λother: False. ⊥
    697640            ] (subaddressing_modein … addr)
    698641        | LCALL addr ⇒
    699           let s ≝ set_clock ? s (ticks + clock ? s) in
    700           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
     642          let s ≝ set_clock … s (ticks + clock … s) in
     643          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
    701644            [ ADDR16 a ⇒ λaddr16: True.
    702               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    703               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    704               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    705               let s ≝ write_at_stack_pointer ? s pc_bl in
    706               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    707               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    708               let s ≝ write_at_stack_pointer ? s pc_bu in
    709                 set_program_counter ? s a
     645              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     646              let s ≝ set_8051_sfr s SFR_SP new_sp in
     647              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     648              let s ≝ write_at_stack_pointer s pc_bl in
     649              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     650              let s ≝ set_8051_sfr s SFR_SP new_sp in
     651              let s ≝ write_at_stack_pointer s pc_bu in
     652                set_program_counter s a
    710653            | _ ⇒ λother: False. ⊥
    711654            ] (subaddressing_modein … addr)
    712       ]. (*10s*)
     655        ]. (*10s*)
    713656    [||||||||*:try assumption]
    714657    [1,2,3,4,5,7: @pi2 (*35s*)
    715     |8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ?
     658    |8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]]
    716659        (λx. λs.
    717660        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    718         [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
     661        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter s) (sign_extension r))
    719662        | _ ⇒ λabsd. ⊥
    720663        ] (subaddressing_modein … x)) instr1 s1) try @absd * #H @H
    721664    |*: normalize nodelta try // (*17s*)
    722         >set_program_counter_ignores_clock // (* Andrea:??*) ]
     665        >clock_set_program_counter // (* Andrea:??*) ]
    723666qed.
    724667
    725668definition current_instruction_cost ≝
    726   λs: Status.
    727     \snd (fetch (code_memory … s) (program_counter … s)).
    728 
    729 definition execute_1': ∀s:Status.
    730   Σs':Status. clock … s' = current_instruction_cost s + clock … s ≝
    731   λs: Status.
    732     let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
    733      execute_1_0 s instr_pc_ticks.
    734 
    735 definition execute_1: Status → Status ≝ execute_1'.
    736 
    737 lemma execute_1_ok: ∀s. clock … (execute_1 s) = current_instruction_cost s + clock … s.
    738  #s whd in match execute_1; normalize nodelta @pi2
     669  λcm.λs: Status cm.
     670    \snd (fetch cm (program_counter … s)).
     671
     672definition execute_1': ∀cm.∀s:Status cm.
     673  Σs':Status cm. clock ?? s' = current_instruction_cost cm s + clock … s ≝
     674  λcm. λs: Status cm.
     675    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
     676     execute_1_0 cm s instr_pc_ticks.
     677
     678definition execute_1: ∀cm. Status cm → Status cm ≝ execute_1'.
     679
     680lemma execute_1_ok: ∀cm.∀s. clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s.
     681 #cm #s whd in match execute_1; normalize nodelta @pi2
    739682qed-. (*x Andrea: indexing takes ages here *)
    740683
    741 definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus
    742   λticks,s,instr,pc.
    743   let s ≝ set_program_counter ? s pc in
     684definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm. PseudoStatus cm → ? → ? → PseudoStatus cm
     685  λticks,cm,s,instr,pc.
     686  let s ≝ set_program_counter ?? s pc in
    744687  let s ≝
    745688    match instr with
    746     [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s
    747     | Comment cmt ⇒
    748        let s ≝ set_clock ? s (\fst ticks + clock ? s) in
    749         s
     689    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels cm x) instr s
     690    | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
    750691    | Cost cst ⇒ s
    751692    | Jmp jmp ⇒
    752        let s ≝ set_clock ? s (\fst ticks + clock ? s) in
    753         set_program_counter ? s (address_of_word_labels s jmp)
     693       let s ≝ set_clock … s (\fst ticks + clock … s) in
     694        set_program_counter … s (address_of_word_labels cm jmp)
    754695    | Call call ⇒
    755       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
    756       let a ≝ address_of_word_labels s call in
    757       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    758       let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    759       let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    760       let s ≝ write_at_stack_pointer ? s pc_bl in
    761       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    762       let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    763       let s ≝ write_at_stack_pointer ? s pc_bu in
    764         set_program_counter ? s a
     696      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
     697      let a ≝ address_of_word_labels cm call in
     698      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     699      let s ≝ set_8051_sfr s SFR_SP new_sp in
     700      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     701      let s ≝ write_at_stack_pointer s pc_bl in
     702      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     703      let s ≝ set_8051_sfr s SFR_SP new_sp in
     704      let s ≝ write_at_stack_pointer s pc_bu in
     705        set_program_counter s a
    765706    | Mov dptr ident ⇒
    766       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
    767       let the_preamble ≝ \fst (code_memory ? s) in
     707      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
     708      let the_preamble ≝ \fst cm in
    768709      let data_labels ≝ construct_datalabels the_preamble in
    769         set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
     710        set_arg_16 … s (get_arg_16 … s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
    770711    ]
    771712  in
     
    775716qed.
    776717
    777 definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus
    778   λticks_of,s.
    779   let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
    780   let ticks ≝ ticks_of (program_counter ? s) in
    781    execute_1_pseudo_instruction0 ticks s instr pc.
    782 
    783 let rec execute (n: nat) (s: Status) on n: Status
     718definition execute_1_pseudo_instruction: (Word → nat × nat) → ∀cm. PseudoStatus cm → PseudoStatus cm
     719  λticks_of,cm,s.
     720  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) in
     721  let ticks ≝ ticks_of (program_counter s) in
     722   execute_1_pseudo_instruction0 ticks cm s instr pc.
     723
     724let rec execute (n: nat) (cm:?) (s: Status cm) on n: Status cm
    784725  match n with
    785726    [ O ⇒ s
    786     | S o ⇒ execute o (execute_1 s)
     727    | S o ⇒ execute o … (execute_1 … s)
    787728    ].
    788729
    789 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus
     730let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm
    790731  match n with
    791732    [ O ⇒ s
    792     | S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
     733    | S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s)
    793734    ].
  • 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 → ? ≝
  • src/ASM/StatusProofs.ma

    r1606 r1666  
    11include "ASM/Status.ma".
    22
     3(* clock_set_bit_addressable_sfr defined in ASM/Status.ma *)
     4
     5lemma clock_set_low_internal_ram:
     6  ∀M: Type[0]. ∀cm.
     7  ∀s: PreStatus M cm.
     8  ∀ram: BitVectorTrie Byte 7.
     9    clock M cm (set_low_internal_ram … s ram) = clock M cm s.
     10  //
     11qed.
     12
     13lemma clock_set_high_internal_ram:
     14  ∀m: Type[0]. ∀cm.
     15  ∀s: PreStatus m cm.
     16  ∀ram: BitVectorTrie Byte 7.
     17    clock ?? (set_high_internal_ram … s ram) = clock … s.
     18  //
     19qed.
     20
     21lemma clock_write_at_stack_pointer:
     22  ∀m: Type[0].
     23  ∀cm:m.
     24  ∀s: PreStatus m cm.
     25  ∀v: Byte.
     26    clock ?? (write_at_stack_pointer … s v) = clock ?? s.
     27  #m #s #v
     28  whd in match write_at_stack_pointer; normalize nodelta
     29  cases(split … 4 4 ?) #nu #nl normalize nodelta
     30  cases(get_index_v … 4 nu 0 ?) //
     31qed.
     32
     33lemma clock_set_clock:
     34  ∀M: Type[0]. ∀cm.
     35  ∀s: PreStatus M cm.
     36  ∀v.
     37    clock ?? (set_clock … s v) = v.
     38 //
     39qed.
     40
     41lemma clock_set_program_counter:
     42  ∀M: Type[0]. ∀cm.
     43  ∀s: PreStatus M cm.
     44  ∀pc: Word.
     45    clock M cm (set_program_counter … s pc) = clock … s.
     46  //
     47qed.
     48
     49lemma clock_set_8051_sfr:
     50  ∀M: Type[0]. ∀cm.
     51  ∀s: PreStatus M cm.
     52  ∀sfr: SFR8051.
     53  ∀v: Byte.
     54    clock ?? (set_8051_sfr … s sfr v) = clock … s.
     55 //
     56qed.
     57
     58lemma clock_set_flags:
     59 ∀M,cm,s,f1,f2,f3. clock M cm s = clock … (set_flags … s f1 f2 f3).
     60//
     61qed.
     62
    363lemma get_register_set_program_counter:
    4  ∀T,s,pc. get_register T (set_program_counter … s pc) = get_register … s.
    5  #T #s #pc %
     64 ∀T,cm,s,pc. get_register T cm (set_program_counter … s pc) = get_register … s.
     65 //
    666qed.
    767
    868lemma get_8051_sfr_set_program_counter:
    9  ∀T,s,pc. get_8051_sfr T (set_program_counter … s pc) = get_8051_sfr … s.
    10  #T #s #pc %
     69 ∀T,cm,s,pc. get_8051_sfr T cm (set_program_counter … s pc) = get_8051_sfr … s.
     70 //
    1171qed.
    1272
    1373lemma get_bit_addressable_sfr_set_program_counter:
    14  ∀T,s,pc. get_bit_addressable_sfr T (set_program_counter … s pc) = get_bit_addressable_sfr … s.
    15  #T #s #pc %
     74 ∀T,cm,s,pc. get_bit_addressable_sfr T cm (set_program_counter … s pc) = get_bit_addressable_sfr … s.
     75 //
    1676qed.
    1777
    1878lemma low_internal_ram_set_program_counter:
    19  ∀T,s,pc. low_internal_ram T (set_program_counter … s pc) = low_internal_ram … s.
    20  #T #s #pc %
     79 ∀T,cm,s,pc. low_internal_ram T cm (set_program_counter … s pc) = low_internal_ram … s.
     80 //
    2181qed.
    2282
    2383example get_arg_8_set_program_counter:
    2484 ∀n.∀l:Vector addressing_mode_tag (S n).
    25   ∀T,s,pc,b.∀arg:l.
     85  ∀T,cm,s,pc,b.∀arg:l.
    2686   ∀prf:is_in ?
    2787    [[direct;indirect;registr;acc_a;acc_b;data;acc_dptr;ext_indirect;ext_indirect_dptr]] arg.
    28    get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
    29  [ #n #l #T #s #pc #b * *; #X try (#Y #H) try #H try % @⊥ @H
     88   get_arg_8 T cm (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
     89 [ #n #l #T #cm #s #pc #b * *; #X try (#Y #H) try #H try % @⊥ @H
    3090 | cases arg in prf; *; normalize //
    3191 | skip ]
    3292qed.
    3393
     94(*
    3495lemma set_bit_addressable_sfr_set_code_memory:
    3596  ∀T, U: Type[0].
     
    121182  cases (get_index_v bool 4 nu' 0 ?) normalize nodelta
    122183  try % @set_bit_addressable_sfr_set_code_memory
    123 qed.
     184qed. *)
    124185
    125186example set_arg_8_set_program_counter:
    126187  ∀n:nat.
    127188  ∀l:Vector addressing_mode_tag (S n).
    128     ∀T: Type[0].
    129     ∀ps: PreStatus ?.
     189    ∀T: Type[0]. ∀cm.
     190    ∀ps: PreStatus ? cm.
    130191    ∀pc.
    131192    ∀val.
     
    133194    ∀prf:is_in ?
    134195     [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b.
    135   set_arg_8 ? (set_program_counter T ps pc) b val =
    136   set_program_counter T (set_arg_8 ? ps b val) pc.
     196  set_arg_8 … (set_program_counter T cm ps pc) b val =
     197  set_program_counter T cm (set_arg_8 ?? ps b val) pc.
    137198  [2,3: cases b in prf; *; normalize //]
    138   #n #l #T #ps #pc #val * *;
     199  #n #l #T #cm #ps #pc #val * *;
    139200  #x try (#y #H) try #H whd in H; try cases H try %
    140201  whd in match set_arg_8; normalize nodelta
     
    146207qed.
    147208 
    148 
    149 lemma get_arg_8_set_code_memory:
     209(*lemma get_arg_8_set_code_memory:
    150210 ∀T1,T2,s,code_mem,b,arg.
    151211   get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
     
    158218   set_flags … (set_code_memory … s code_mem) f1 f2 f3.
    159219 #T1 #T2 #s #f1 #f2 #f3 #code_mem %
    160 qed.
     220qed.*)
    161221
    162222lemma set_program_counter_set_flags:
    163  ∀T1,s,f1,f2,f3,pc.
    164   set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =
     223 ∀T1,cm,s,f1,f2,f3,pc.
     224  set_program_counter T1 cm (set_flags T1 cm s f1 f2 f3) pc =
    165225   set_flags … (set_program_counter … s pc) f1 f2 f3.
    166  #T1 #s #f1 #f2 #f3 #pc  %
     226 //
    167227qed.
    168228
    169229lemma program_counter_set_flags:
    170  ∀T1,s,f1,f2,f3.
    171   program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.
    172  #T1 #s #f1 #f2 #f3 %
     230 ∀T1,cm,s,f1,f2,f3.
     231  program_counter T1 cm (set_flags T1 cm s f1 f2 f3) = program_counter … s.
     232 //
    173233qed.
    174234
    175235lemma special_function_registers_8051_write_at_stack_pointer:
    176  ∀T,s,x.
    177     special_function_registers_8051 T (write_at_stack_pointer T s x)
    178   = special_function_registers_8051 T s.
    179  #T #s #x whd in ⊢ (??(??%)?);
     236 ∀T,cm,s,x.
     237    special_function_registers_8051 T cm (write_at_stack_pointer T cm s x)
     238  = special_function_registers_8051 T cm s.
     239 #T #cm #s #x whd in ⊢ (??(???%)?);
    180240 cases (split ????) #nu #nl normalize nodelta;
    181241 cases (get_index_v bool ????) %
     
    183243
    184244lemma get_8051_sfr_write_at_stack_pointer:
    185  ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
    186  #T #s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl
    187 qed.
    188 
    189 lemma code_memory_write_at_stack_pointer:
     245 ∀T,cm,s,x,y. get_8051_sfr T cm (write_at_stack_pointer T cm s x) y = get_8051_sfr T cm s y.
     246 #T #cm #s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl
     247qed.
     248
     249(*lemma code_memory_write_at_stack_pointer:
    190250 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
    191251 #T #s #x whd in ⊢ (??(??%)?);
    192252 cases (split ????) #nu #nl normalize nodelta;
    193253 cases (get_index_v bool ????) %
    194 qed.
     254qed.*)
    195255
    196256lemma set_program_counter_set_low_internal_ram:
    197  ∀T,s,x,y.
    198   set_program_counter T (set_low_internal_ram … s x) y =
     257 ∀T,cm,s,x,y.
     258  set_program_counter T cm (set_low_internal_ram … s x) y =
    199259   set_low_internal_ram … (set_program_counter … s y) x.
    200260 //
     
    202262
    203263lemma set_clock_set_low_internal_ram:
    204  ∀T,s,x,y.
    205   set_clock T (set_low_internal_ram … s x) y =
     264 ∀T,cm,s,x,y.
     265  set_clock T cm (set_low_internal_ram … s x) y =
    206266   set_low_internal_ram … (set_clock … s y) x.
    207267 //
     
    209269
    210270lemma set_program_counter_set_high_internal_ram:
    211  ∀T,s,x,y.
    212   set_program_counter T (set_high_internal_ram … s x) y =
     271 ∀T,cm,s,x,y.
     272  set_program_counter T cm (set_high_internal_ram … s x) y =
    213273   set_high_internal_ram … (set_program_counter … s y) x.
    214274 //
     
    216276
    217277lemma set_clock_set_high_internal_ram:
    218  ∀T,s,x,y.
    219   set_clock T (set_high_internal_ram … s x) y =
     278 ∀T,cm,s,x,y.
     279  set_clock T cm (set_high_internal_ram … s x) y =
    220280   set_high_internal_ram … (set_clock … s y) x.
    221281 //
     
    223283
    224284lemma set_low_internal_ram_set_high_internal_ram:
    225  ∀T,s,x,y.
    226   set_low_internal_ram T (set_high_internal_ram … s x) y =
     285 ∀T,cm,s,x,y.
     286  set_low_internal_ram T cm (set_high_internal_ram … s x) y =
    227287   set_high_internal_ram … (set_low_internal_ram … s y) x.
    228288 //
     
    230290
    231291lemma external_ram_write_at_stack_pointer:
    232  ∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s.
    233  #T #s #x whd in ⊢ (??(??%)?);
     292 ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s.
     293 #T #cm #s #x whd in ⊢ (??(???%)?);
    234294 cases (split ????) #nu #nl normalize nodelta;
    235295 cases (get_index_v bool ????) %
     
    237297
    238298lemma special_function_registers_8052_write_at_stack_pointer:
    239  ∀T,s,x.
    240     special_function_registers_8052 T (write_at_stack_pointer T s x)
    241   = special_function_registers_8052 T s.
    242  #T #s #x whd in ⊢ (??(??%)?);
     299 ∀T,cm,s,x.
     300    special_function_registers_8052 T cm (write_at_stack_pointer T cm s x)
     301  = special_function_registers_8052 T cm s.
     302 #T #cm #s #x whd in ⊢ (??(???%)?);
    243303 cases (split ????) #nu #nl normalize nodelta;
    244304 cases (get_index_v bool ????) %
     
    246306
    247307lemma p1_latch_write_at_stack_pointer:
    248  ∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s.
    249  #T #s #x whd in ⊢ (??(??%)?);
     308 ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s.
     309 #T #cm #s #x whd in ⊢ (??(???%)?);
    250310 cases (split ????) #nu #nl normalize nodelta;
    251311 cases (get_index_v bool ????) %
     
    253313
    254314lemma p3_latch_write_at_stack_pointer:
    255  ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s.
    256  #T #s #x whd in ⊢ (??(??%)?);
    257  cases (split ????) #nu #nl normalize nodelta;
    258  cases (get_index_v bool ????) %
    259 qed.
    260 
    261 lemma clock_write_at_stack_pointer:
    262  ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s.
    263  #T #s #x whd in ⊢ (??(??%)?);
     315 ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s.
     316 #T #cm #s #x whd in ⊢ (??(???%)?);
    264317 cases (split ????) #nu #nl normalize nodelta;
    265318 cases (get_index_v bool ????) %
     
    270323
    271324lemma get_8051_sfr_set_8051_sfr:
    272  ∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y.
    273  #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?);
     325 ∀T,cm,s,x,y. get_8051_sfr T cm (set_8051_sfr … s x y) x = y.
     326 #T #cm * #A #B #C #D #E #F #G #H #I * #y whd in ⊢ (??(???%?)?);
    274327 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
    275328qed.
    276329
    277330lemma program_counter_set_8051_sfr:
    278  ∀T,s,x,y. program_counter T (set_8051_sfr ? s x y) = program_counter ? s.
     331 ∀T,cm,s,x,y. program_counter T cm (set_8051_sfr … s x y) = program_counter … s.
    279332 //
    280333qed.
    281334
    282335axiom get_arg_8_set_low_internal_ram:
    283  ∀M,s,x,b,z. get_arg_8 M (set_low_internal_ram ? s x) b z = get_arg_8 ? s b z.
     336 ∀M,cm,s,x,b,z. get_arg_8 M cm (set_low_internal_ram … s x) b z = get_arg_8 … s b z.
    284337
    285338lemma split_eq_status:
    286  ∀T.
    287  ∀A1,A2,A3,A4,A5,A6,A7,A8,A9,A10.
    288  ∀B1,B2,B3,B4,B5,B6,B7,B8,B9,B10.
    289   A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 →
    290    mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 =
    291    mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10.
    292  //
    293 qed.
     339 ∀T,cm.
     340 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9.
     341 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9.
     342  A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 →
     343   mk_PreStatus T cm A1 A2 A3 A4 A5 A6 A7 A8 A9 =
     344   mk_PreStatus T cm B1 B2 B3 B4 B5 B6 B7 B8 B9.
     345 //
     346qed.
Note: See TracChangeset for help on using the changeset viewer.