Ignore:
Timestamp:
Jun 16, 2011, 6:08:12 PM (9 years ago)
Author:
sacerdot
Message:

Real parameterization over the policy.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r985 r987  
    681681
    682682lemma fetch_assembly_pseudo:
    683  ∀program,ppc,lookup_labels,lookup_datalabels.
     683 ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.
    684684  ∀pi,code_memory,len,assembled,instructions,pc.
    685    let expansion ≝ jump_expansion ppc program in
     685   let expansion ≝ pol ppc in
    686686   Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
    687     Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
     687    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program pol ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
    688688     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
    689689      fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
    690  #program #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
     690 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
    691691 #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2
    692692 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
     
    779779
    780780axiom assembly_ok:
    781  ∀program,assembled.
    782   let 〈labels,costs〉 ≝ build_maps program in
    783   Some … 〈assembled,costs〉 = assembly program
     781 ∀program,pol,assembled.
     782  let 〈labels,costs〉 ≝ build_maps program pol in
     783  Some … 〈assembled,costs〉 = assembly program pol
    784784  let code_memory ≝ load_code_memory assembled in
    785785  let preamble ≝ \fst program in
    786786  let datalabels ≝ construct_datalabels preamble in
    787   let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
     787  let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
    788788  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
    789789   ∀ppc,len,assembledi.
    790790    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    791      Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi →
    792       encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧
    793        sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
     791     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi →
     792      encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧
     793       sigma program pol newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
    794794
    795795axiom bitvector_of_nat_nat_of_bitvector:
     
    798798
    799799axiom assembly_ok_to_expand_pseudo_instruction_ok:
    800  ∀program,assembled,costs.
    801   Some … 〈assembled,costs〉 = assembly program
     800 ∀program,pol,assembled,costs.
     801  Some … 〈assembled,costs〉 = assembly program pol
    802802   ∀ppc.
    803803    let code_memory ≝ load_code_memory assembled in
    804804    let preamble ≝ \fst program in   
    805805    let data_labels ≝ construct_datalabels preamble in
    806     let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
     806    let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
    807807    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
    808     let expansion ≝ jump_expansion ppc program in
     808    let expansion ≝ pol ppc in
    809809    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    810810     ∃instructions.
    811       Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi.
     811      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi.
    812812
    813813axiom pair_elim':
     
    849849
    850850lemma fetch_assembly_pseudo2:
    851  ∀program,assembled.
    852   let 〈labels,costs〉 ≝ build_maps program in
    853   Some … 〈assembled,costs〉 = assembly program
     851 ∀program,pol,assembled.
     852  let 〈labels,costs〉 ≝ build_maps program pol in
     853  Some … 〈assembled,costs〉 = assembly program pol
    854854   ∀ppc.
    855855    let code_memory ≝ load_code_memory assembled in
    856856    let preamble ≝ \fst program in
    857857    let data_labels ≝ construct_datalabels preamble in
    858     let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
     858    let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
    859859    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
    860     let expansion ≝ jump_expansion ppc program in
     860    let expansion ≝ pol ppc in
    861861    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    862862     ∃instructions.
    863       Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧
    864        fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
    865  #program #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc
    866  generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program assembled costs ASSEMBLY ppc)
     863      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi ∧
     864       fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
     865 #program #pol #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc
     866 generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program pol assembled costs ASSEMBLY ppc)
    867867 letin code_memory ≝ (load_code_memory assembled)
    868868 letin preamble ≝ (\fst program)
    869869 letin data_labels ≝ (construct_datalabels preamble)
    870  letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x))
     870 letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x))
    871871 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
    872  whd in ⊢ (% → %) generalize in match (assembly_ok program assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
     872 whd in ⊢ (% → %) generalize in match (assembly_ok program pol assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
    873873 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
    874  generalize in match (fetch_assembly_pseudo program ppc
    875   (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
     874 generalize in match (fetch_assembly_pseudo program pol ppc
     875  (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
    876876  (load_code_memory assembled));
    877877 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
    878878 whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
    879879 normalize nodelta in EXPAND; (* HERE *)
    880  generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program ppc))) -H1; #H1
     880 generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program pol ppc))) -H1; #H1
    881881 >bitvector_of_nat_nat_of_bitvector in H1; #H1
    882882 <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
     
    943943
    944944axiom low_internal_ram_of_pseudo_internal_ram_hit:
    945  ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7.
     945 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀pol:policy (code_memory … s).∀addr:BitVector 7.
    946946  member ? (eq_bv 8) (false:::addr) M = true →
    947947   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
     
    950950   let bl ≝ lookup ? 7 addr ram (zero 8) in
    951951   let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
    952     bu@@bl = sigma (code_memory … s) (pbu@@pbl).
     952    bu@@bl = sigma (code_memory … s) pol (pbu@@pbl).
    953953
    954954(* changed from add to sub *)
     
    10331033   
    10341034definition status_of_pseudo_status:
    1035  internal_pseudo_address_map → PseudoStatus → option Status ≝
    1036  λM,ps.
     1035 internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → option Status ≝
     1036 λM,ps,pol.
    10371037  let pap ≝ code_memory … ps in
    1038    match assembly pap with
     1038   match assembly pap pol with
    10391039    [ None ⇒ None …
    10401040    | Some p ⇒
    10411041       let cm ≝ load_code_memory (\fst p) in
    1042        let pc ≝ sigma pap (program_counter ? ps) in
     1042       let pc ≝ sigma pap pol (program_counter ? ps) in
    10431043       let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
    10441044       let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
     
    11561156 ∀M:internal_pseudo_address_map.
    11571157 ∀ps,ps': PseudoStatus.
    1158   code_memory … ps = code_memory … ps' →
    1159    match status_of_pseudo_status M ps with
    1160     [ None ⇒ status_of_pseudo_status M ps' = None …
    1161     | Some _ ⇒ ∃w. status_of_pseudo_status M ps' = Some … w
     1158 ∀pol.
     1159  ∀prf:code_memory … ps = code_memory … ps'.
     1160   let pol' ≝ ? in
     1161   match status_of_pseudo_status M ps pol with
     1162    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
     1163    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
    11621164    ].
    1163  #M #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
    1164  generalize in match (refl … (assembly (code_memory … ps)))
    1165  cases (assembly ?) in ⊢ (???% → %)
     1165 [2: <prf @pol]
     1166 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     1167 generalize in match (refl … (assembly (code_memory … ps) pol))
     1168 cases (assembly ??) in ⊢ (???% → %)
    11661169  [ #K whd whd in ⊢ (??%?) <H >K %
    11671170  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
    11681171qed.
    11691172
    1170 definition ticks_of0: pseudo_assembly_program → Word → ? → nat × nat ≝
    1171   λprogram: pseudo_assembly_program.
     1173definition ticks_of0: ∀p:pseudo_assembly_program. policy p → Word → ? → nat × nat ≝
     1174  λprogram: pseudo_assembly_program.λpol.
    11721175  λppc: Word.
    11731176  λfetched.
     
    11761179      match instr with
    11771180      [ JC lbl ⇒
    1178         match jump_expansion ppc program with
     1181        match pol ppc with
    11791182        [ short_jump ⇒ 〈2, 2〉
    11801183        | medium_jump ⇒ ?
     
    11821185        ]
    11831186      | JNC lbl ⇒
    1184         match jump_expansion ppc program with
     1187        match pol ppc with
    11851188        [ short_jump ⇒ 〈2, 2〉
    11861189        | medium_jump ⇒ ?
     
    11881191        ]
    11891192      | JB bit lbl ⇒
    1190         match jump_expansion ppc program with
     1193        match pol ppc with
    11911194        [ short_jump ⇒ 〈2, 2〉
    11921195        | medium_jump ⇒ ?
     
    11941197        ]
    11951198      | JNB bit lbl ⇒
    1196         match jump_expansion ppc program with
     1199        match pol ppc with
    11971200        [ short_jump ⇒ 〈2, 2〉
    11981201        | medium_jump ⇒ ?
     
    12001203        ]
    12011204      | JBC bit lbl ⇒
    1202         match jump_expansion ppc program with
     1205        match pol ppc with
    12031206        [ short_jump ⇒ 〈2, 2〉
    12041207        | medium_jump ⇒ ?
     
    12061209        ]
    12071210      | JZ lbl ⇒
    1208         match jump_expansion ppc program with
     1211        match pol ppc with
    12091212        [ short_jump ⇒ 〈2, 2〉
    12101213        | medium_jump ⇒ ?
     
    12121215        ]
    12131216      | JNZ lbl ⇒
    1214         match jump_expansion ppc program with
     1217        match pol ppc with
    12151218        [ short_jump ⇒ 〈2, 2〉
    12161219        | medium_jump ⇒ ?
     
    12181221        ]
    12191222      | CJNE arg lbl ⇒
    1220         match jump_expansion ppc program with
     1223        match pol ppc with
    12211224        [ short_jump ⇒ 〈2, 2〉
    12221225        | medium_jump ⇒ ?
     
    12241227        ]
    12251228      | DJNZ arg lbl ⇒
    1226         match jump_expansion ppc program with
     1229        match pol ppc with
    12271230        [ short_jump ⇒ 〈2, 2〉
    12281231        | medium_jump ⇒ ?
     
    13231326qed.
    13241327
    1325 definition ticks_of: pseudo_assembly_program → Word → nat × nat ≝
    1326   λprogram: pseudo_assembly_program.
     1328definition ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat ≝
     1329  λprogram: pseudo_assembly_program.λpol.
    13271330  λppc: Word.
    13281331    let 〈preamble, pseudo〉 ≝ program in
    13291332    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
    1330      ticks_of0 program ppc fetched.
     1333     ticks_of0 program pol ppc fetched.
    13311334
    13321335lemma get_register_set_program_counter:
Note: See TracChangeset for help on using the changeset viewer.