Changeset 987


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

Real parameterization over the policy.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r985 r987  
    656656    jump_expansion_policy_internal program old_labels old_policy in
    657657    jump_expansion_internal n' program new_labels new_policy ].
    658          
    659 definition jump_expansion ≝
    660  λpc.λprogram.
     658
     659definition policy_type ≝ Word → jump_length.
     660
     661definition jump_expansion': pseudo_assembly_program → policy_type ≝
     662 λprogram.λpc.
    661663  let policy ≝ jump_expansion_internal (length ? (\snd program)) program (Stub ? ?) (Stub ? ?) in
    662664  lookup ? ? pc policy long_jump.
     
    664666definition assembly_1_pseudoinstruction ≝
    665667  λprogram: pseudo_assembly_program.
     668  λjump_expansion: policy_type.
    666669  λppc: Word.
    667670  λpc: Word.
     
    669672  λlookup_datalabels.
    670673  λi.
    671   let expansion ≝ jump_expansion ppc program in
     674  let expansion ≝ jump_expansion ppc in
    672675    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
    673676    [ None ⇒ None ?
     
    681684definition construct_costs ≝
    682685  λprogram.
     686  λjump_expansion: policy_type.
    683687  λpseudo_program_counter: nat.
    684688  λprogram_counter: nat.
     
    695699    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
    696700    let pc_delta_assembled ≝
    697       assembly_1_pseudoinstruction program ppc_bv pc_bv
     701      assembly_1_pseudoinstruction program jump_expansion ppc_bv pc_bv
    698702        lookup_labels lookup_datalabels i
    699703    in
     
    709713   program counters. It is at the heart of the proof. *)
    710714(*CSC: code taken from build_maps *)
    711 definition sigma00: pseudo_assembly_program → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
    712  λinstr_list.λl:list labelled_instruction.
     715definition sigma00: pseudo_assembly_program → policy_type → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
     716 λinstr_list.
     717 λjump_expansion: policy_type.
     718 λl:list labelled_instruction.
    713719  foldl ??
    714720   (λt,i.
     
    719725         let 〈program_counter, sigma_map〉 ≝ pc_map in
    720726         let 〈label, i〉 ≝ i in
    721           match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
     727          match construct_costs instr_list jump_expansion ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
    722728           [ None ⇒ None ?
    723729           | Some pc_ignore ⇒
     
    726732       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
    727733
    728 definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16)))
    729  ≝ λprog.sigma00 prog (\snd prog).
    730 
    731 definition tech_pc_sigma00: pseudo_assembly_program → list labelled_instruction → option (nat × nat) ≝
    732  λprogram,instr_list.
    733   match sigma00 program instr_list with
     734definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
     735 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog).
     736
     737definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
     738 λprogram,jump_expansion,instr_list.
     739  match sigma00 program jump_expansion instr_list with
    734740   [ None ⇒ None …
    735741   | Some result ⇒
     
    738744       Some … 〈ppc,pc〉 ].
    739745
    740 definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝
    741  λinstr_list.
    742   match sigma0 instr_list with
     746definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
     747 λinstr_list,jump_expansion.
     748  match sigma0 instr_list jump_expansion with
    743749  [ None ⇒ None ?
    744750  | Some result ⇒
     
    752758(* stuff about policy *)
    753759
    754 axiom policy_ok: ∀p. sigma_safe p ≠ None ….
    755 
    756 definition sigma: pseudo_assembly_program → Word → Word ≝
    757  λp.
    758   match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
     760definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
     761
     762definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
     763
     764lemma eject_policy: ∀p. policy p → policy_type.
     765 #p #pol @(eject … pol)
     766qed.
     767
     768coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
     769
     770definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
     771 λp,policy.
     772  match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
    759773   [ None ⇒ λabs. ⊥
    760    | Some r ⇒ λ_.r] (policy_ok p).
     774   | Some r ⇒ λ_.r] (sig2 … policy).
    761775 cases abs //
    762776qed.
    763777
    764 example sigma_0: ∀p. sigma p (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
     778example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
    765779 cases daemon.
    766780qed.
    767781
    768782axiom construct_costs_sigma:
    769  ∀p,ppc,pc,pc',costs,costs',i.
    770   bitvector_of_nat ? pc = sigma p (bitvector_of_nat ? ppc) →
    771    Some … 〈pc',costs'〉 = construct_costs p ppc pc (λx.zero 16) (λx.zero 16) costs i →
    772     bitvector_of_nat ? pc' = sigma p (bitvector_of_nat 16 (S ppc)).
     783 ∀p.∀pol:policy p.∀ppc,pc,pc',costs,costs',i.
     784  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
     785   Some … 〈pc',costs'〉 = construct_costs p pol ppc pc (λx.zero 16) (λx.zero 16) costs i →
     786    bitvector_of_nat ? pc' = sigma p pol (bitvector_of_nat 16 (S ppc)).
    773787
    774788axiom tech_pc_sigma00_append_Some:
    775  ∀program,prefix,costs,label,i,pc',code,ppc,pc.
    776   tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
    777    construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
    778     tech_pc_sigma00 program (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
     789 ∀program.∀pol:policy program.∀prefix,costs,label,i,pc',code,ppc,pc.
     790  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
     791   construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
     792    tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
    779793
    780794axiom tech_pc_sigma00_append_None:
    781  ∀program,prefix,i,ppc,pc,costs.
    782   tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
    783    construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
     795 ∀program.∀pol:policy program.∀prefix,i,ppc,pc,costs.
     796  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
     797   construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
    784798    → False.
    785799
    786800definition build_maps ≝
    787   λpseudo_program.
     801  λpseudo_program.λpol:policy pseudo_program.
    788802  let result ≝
    789803   foldl_strong
     
    793807      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
    794808      let 〈pc',costs〉 ≝ pc_costs in
    795        bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧
     809       bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc') ∧
    796810       ppc' = length … pre ∧
    797        tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
     811       tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉 ∧
    798812       ∀id. occurs_exactly_once id pre →
    799         lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id))
     813        lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id))
    800814    (\snd pseudo_program)
    801815    (λprefix,i,tl,prf,t.
     
    812826         ]
    813827       in
    814          match construct_costs pseudo_program ppc pc (λx. zero ?) (λx. zero ?) costs i' with
     828         match construct_costs pseudo_program pol ppc pc (λx. zero ?) (λx. zero ?) costs i' with
    815829         [ None ⇒
    816830            let dummy ≝ 〈labels,ppc_pc_costs〉 in
     
    858872*)
    859873
    860 definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
    861   λp.
     874definition assembly: ∀p:pseudo_assembly_program. policy p → option (list Byte × (BitVectorTrie Identifier 16)) ≝
     875  λp,pol.
    862876    let 〈preamble, instr_list〉 ≝ p in
    863     let 〈labels,costs〉 ≝ build_maps p in
     877    let 〈labels,costs〉 ≝ build_maps p pol in
    864878    let datalabels ≝ construct_datalabels preamble in
    865879    let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
     
    871885          let 〈pc, ppc_y〉 ≝ lst in
    872886          let 〈ppc, y〉 ≝ ppc_y in
    873           let x ≝ assembly_1_pseudoinstruction p ppc pc lookup_labels lookup_datalabels (\snd x) in
     887          let x ≝ assembly_1_pseudoinstruction p pol ppc pc lookup_labels lookup_datalabels (\snd x) in
    874888          match x with
    875889          [ None ⇒ None ?
  • 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.