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

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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/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
Note: See TracChangeset for help on using the changeset viewer.