Ignore:
Timestamp:
May 14, 2012, 10:40:38 PM (8 years ago)
Author:
sacerdot
Message:

All proof statements repaired.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1941 r1945  
    16101610
    16111611axiom low_internal_ram_of_pseudo_internal_ram_hit:
    1612  ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀pol:policy cm.∀addr:BitVector 7.
     1612 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀addr:BitVector 7.
    16131613  member ? (eq_bv 8) (false:::addr) M = true →
    16141614   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
     
    16171617   let bl ≝ lookup ? 7 addr ram (zero 8) in
    16181618   let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
    1619     bu@@bl = sigma cm pol (pbu@@pbl).
     1619    bu@@bl = \fst (sigma (pbu@@pbl)).
    16201620
    16211621(* changed from add to sub *)
     
    17021702
    17031703definition code_memory_of_pseudo_assembly_program:
    1704  ∀pap:pseudo_assembly_program. policy pap → BitVectorTrie Byte 16
    1705 ≝ λpap,pol.
    1706    let p ≝ assembly pap pol in
     1704 ∀pap:pseudo_assembly_program. (Word → Word × bool) → BitVectorTrie Byte 16
     1705≝ λpap,sigma.
     1706   let p ≝ assembly pap sigma in
    17071707    load_code_memory (\fst p).
    17081708
    17091709definition status_of_pseudo_status:
    1710  internal_pseudo_address_map → ∀pap.∀ps:PseudoStatus pap. ∀pol:policy pap.
    1711   Status (code_memory_of_pseudo_assembly_program … pol) ≝
    1712  λM,pap,ps,pol.
    1713   let cm ≝ code_memory_of_pseudo_assembly_program … pol in
    1714   let pc ≝ sigma pap pol (program_counter … ps) in
     1710 internal_pseudo_address_map → ∀pap.∀ps:PseudoStatus pap. ∀sigma: Word → Word × bool.
     1711  Status (code_memory_of_pseudo_assembly_program pap sigma) ≝
     1712 λM,pap,ps,sigma.
     1713  let cm ≝ code_memory_of_pseudo_assembly_program … sigma in
     1714  let pc ≝ \fst (sigma (program_counter … ps)) in
    17151715  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
    17161716  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
     
    18401840*)
    18411841
    1842 definition ticks_of0: ∀p:pseudo_assembly_program. policy p → (Identifier→Word) → Word → ? → nat × nat ≝
    1843   λprogram: pseudo_assembly_program.λpol.λlookup_labels.
     1842definition ticks_of0: ∀p:pseudo_assembly_program. (Word → Word × bool) → Word → pseudo_instruction → nat × nat ≝
     1843  λprogram: pseudo_assembly_program.λsigma.
    18441844  λppc: Word.
    1845   λfetched.
     1845  λfetched. ?.
     1846cases daemon(*
    18461847    match fetched with
    18471848    [ Instruction instr ⇒
     
    19931994    ].
    19941995  cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
    1995 qed.
    1996 
    1997 definition ticks_of: ∀p:pseudo_assembly_program. policy p → (Identifier→Word) → Word → nat × nat ≝
    1998   λprogram: pseudo_assembly_program.λpol.λlookup_labels.
     1996*)qed.
     1997
     1998definition ticks_of: ∀p:pseudo_assembly_program. (Word → Word × bool) → Word → nat × nat ≝
     1999  λprogram: pseudo_assembly_program.λsigma.
    19992000  λppc: Word.
    20002001    let 〈preamble, pseudo〉 ≝ program in
    20012002    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
    2002      ticks_of0 program pol lookup_labels ppc fetched.
     2003     ticks_of0 program sigma ppc fetched.
    20032004
    20042005lemma eq_rect_Type1_r:
     
    21102111
    21112112axiom low_internal_ram_write_at_stack_pointer:
    2112  ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
    2113   get_8051_sfr ? cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
     2113 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word × bool.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
     2114  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
    21142115  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
    21152116  sp1 = \snd (half_add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1)) →
    21162117  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
    2117   bu@@bl = sigma cm2 pol (pbu@@pbl) →
     2118  bu@@bl = \fst (sigma (pbu@@pbl)) →
    21182119   low_internal_ram T1 cm1
    21192120     (write_at_stack_pointer …
     
    21362137
    21372138axiom high_internal_ram_write_at_stack_pointer:
    2138  ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
    2139   get_8051_sfr ? cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
     2139 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word × bool.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
     2140  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
    21402141  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
    21412142  sp1 = \snd (half_add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1)) →
    21422143  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
    2143   bu@@bl = sigma cm2 pol (pbu@@pbl) →
     2144  bu@@bl = \fst (sigma (pbu@@pbl)) →
    21442145   high_internal_ram T1 cm1
    21452146     (write_at_stack_pointer …
     
    21662167qed.
    21672168
    2168 (*usare snd_assembly_1_pseudoinstruction_ok:
    2169  ∀program:pseudo_assembly_program.∀pol: policy program.
     2169(*CSC: ???*)
     2170axiom snd_assembly_1_pseudoinstruction_ok:
     2171 ∀program:pseudo_assembly_program.∀sigma.
    21702172 ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels.
    2171   lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
     2173  lookup_labels = (λx. \fst (sigma (address_of_word_labels_code_mem (\snd program) x))) →
    21722174  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    21732175  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    2174    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels  pi) in
    2175     sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
    2176      bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
    2177 *)
     2176   let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma (\fst (sigma ppc)) lookup_datalabels  pi) in
     2177    \fst (sigma (add … ppc (bitvector_of_nat ? 1))) =
     2178     add … (\fst (sigma ppc)) (bitvector_of_nat ? len).
    21782179
    21792180lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
     
    21882189
    21892190theorem main_thm:
    2190  ∀M,M',cm,ps,pol,lookup_labels.
     2191 ∀M,M',cm,ps,sigma.
    21912192  next_internal_pseudo_address_map M cm ps = Some … M' →
    21922193   ∃n.
    2193       execute n … (status_of_pseudo_status M … ps pol)
    2194     = status_of_pseudo_status M' … (execute_1_pseudo_instruction (ticks_of cm pol lookup_labels) cm ps) pol.
    2195  #M #M' * #preamble #instr_list #ps #pol #lookup_labels
     2194      execute n … (status_of_pseudo_status M … ps sigma)
     2195    = status_of_pseudo_status M' … (execute_1_pseudo_instruction (ticks_of cm sigma) cm ps) sigma.
     2196 #M #M' * #preamble #instr_list #ps #sigma
    21962197 change with (next_internal_pseudo_address_map0 ????? = ? → ?)
    21972198 @(pose … (program_counter ?? ps)) #ppc #EQppc
    2198  generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ?;
    2199  @(pose … (\fst (assembly ? pol))) #assembled #EQassembled
    2200  @(pose … (λx.sigma … pol (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
     2199 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma ppc) in ⊢ ?;
     2200 @pair_elim #labels #costs #H0 normalize nodelta
     2201 @pair_elim #assembled #costs' #EQ1 normalize nodelta
     2202 @pair_elim #pi #newppc #EQ2 normalize nodelta
     2203 @(pose … (λx. \fst (sigma (address_of_word_labels_code_mem instr_list x)))) #lookup_labels #EQlookup_labels
    22012204 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
    22022205 whd in match execute_1_pseudo_instruction; normalize nodelta
    2203  @pair_elim #pi #newppc #H1
    2204  whd in match ticks_of; normalize nodelta <EQppc #H2 >H1 normalize nodelta;
    2205  lapply (snd_fetch_pseudo_instruction instr_list ppc) >H1 #EQnewppc >EQnewppc
    2206  lapply (snd_assembly_1_pseudoinstruction_ok … ppc pi … EQlookup_labels EQlookup_datalabels ?)
    2207  [>H1 %]
     2206 whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta
     2207 lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc
     2208 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … ppc pi … EQlookup_labels EQlookup_datalabels ?)
     2209 [>EQ2 %]
    22082210 inversion pi
    22092211  [2,3: (* Comment, Cost *) #ARG #EQ
     
    22112213   whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
    22122214   whd in match (execute_1_pseudo_instruction0 ?????);
    2213    %{0} @split_eq_status //
     2215   %{0} @split_eq_status CSC:STOP HERE //
    22142216  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)
    22152217   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.