Changeset 987

Timestamp:

Jun 16, 2011, 6:08:12 PM (9 years ago)

Author:

sacerdot

Message:

Real parameterization over the policy.

Location:

src/ASM

Files:

• Assembly.ma (modified) (14 diffs)
• AssemblyProof.ma (modified) (18 diffs)

src/ASM/Assembly.ma

@@ -656 +656 @@
     jump_expansion_policy_internal program old_labels old_policy in
     jump_expansion_internal n' program new_labels new_policy ].
-         
-definition jump_expansion ≝
- λpc.λprogram.
+
+definition policy_type ≝ Word → jump_length.
+
+definition jump_expansion': pseudo_assembly_program → policy_type ≝
+ λprogram.λpc.
   let policy ≝ jump_expansion_internal (length ? (\snd program)) program (Stub ? ?) (Stub ? ?) in
   lookup ? ? pc policy long_jump.
@@ -664 +666 @@
 definition assembly_1_pseudoinstruction ≝
   λprogram: pseudo_assembly_program.
+  λjump_expansion: policy_type.
   λppc: Word.
   λpc: Word.
@@ -669 +672 @@
   λlookup_datalabels.
   λi.
-  let expansion ≝ jump_expansion ppc program in
+  let expansion ≝ jump_expansion ppc in
     match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
     [ None ⇒ None ?
@@ -681 +684 @@
 definition construct_costs ≝
   λprogram.
+  λjump_expansion: policy_type.
   λpseudo_program_counter: nat.
   λprogram_counter: nat.
@@ -695 +699 @@
     let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
     let pc_delta_assembled ≝
-      assembly_1_pseudoinstruction program ppc_bv pc_bv
+      assembly_1_pseudoinstruction program jump_expansion ppc_bv pc_bv
         lookup_labels lookup_datalabels i
     in
@@ -709 +713 @@
    program counters. It is at the heart of the proof. *)
 (*CSC: code taken from build_maps *)
-definition sigma00: pseudo_assembly_program → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
- λinstr_list.λl:list labelled_instruction.
+definition sigma00: pseudo_assembly_program → policy_type → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
+ λinstr_list.
+ λjump_expansion: policy_type.
+ λl:list labelled_instruction.
   foldl ??
    (λt,i.
@@ -719 +725 @@
          let 〈program_counter, sigma_map〉 ≝ pc_map in
          let 〈label, i〉 ≝ i in
-          match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
+          match construct_costs instr_list jump_expansion ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
            [ None ⇒ None ?
            | Some pc_ignore ⇒
@@ -726 +732 @@
        ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
 
-definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16)))
- ≝ λprog.sigma00 prog (\snd prog).
-
-definition tech_pc_sigma00: pseudo_assembly_program → list labelled_instruction → option (nat × nat) ≝
- λprogram,instr_list.
-  match sigma00 program instr_list with
+definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
+ ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog).
+
+definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
+ λprogram,jump_expansion,instr_list.
+  match sigma00 program jump_expansion instr_list with
    [ None ⇒ None …
    | Some result ⇒
@@ -738 +744 @@
        Some … 〈ppc,pc〉 ].
 
-definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝
- λinstr_list.
-  match sigma0 instr_list with
+definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
+ λinstr_list,jump_expansion.
+  match sigma0 instr_list jump_expansion with
   [ None ⇒ None ?
   | Some result ⇒
@@ -752 +758 @@
 (* stuff about policy *)
 
-axiom policy_ok: ∀p. sigma_safe p ≠ None ….
-
-definition sigma: pseudo_assembly_program → Word → Word ≝
- λp.
-  match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
+definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
+
+definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
+
+lemma eject_policy: ∀p. policy p → policy_type.
+ #p #pol @(eject … pol)
+qed.
+
+coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
+
+definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
+ λp,policy.
+  match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
    [ None ⇒ λabs. ⊥
-   | Some r ⇒ λ_.r] (policy_ok p).
+   | Some r ⇒ λ_.r] (sig2 … policy).
  cases abs //
 qed.
 
-example sigma_0: ∀p. sigma p (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
+example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
  cases daemon.
 qed.
 
 axiom construct_costs_sigma:
- ∀p,ppc,pc,pc',costs,costs',i.
-  bitvector_of_nat ? pc = sigma p (bitvector_of_nat ? ppc) →
-   Some … 〈pc',costs'〉 = construct_costs p ppc pc (λx.zero 16) (λx.zero 16) costs i →
-    bitvector_of_nat ? pc' = sigma p (bitvector_of_nat 16 (S ppc)).
+ ∀p.∀pol:policy p.∀ppc,pc,pc',costs,costs',i.
+  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
+   Some … 〈pc',costs'〉 = construct_costs p pol ppc pc (λx.zero 16) (λx.zero 16) costs i →
+    bitvector_of_nat ? pc' = sigma p pol (bitvector_of_nat 16 (S ppc)).
 
 axiom tech_pc_sigma00_append_Some:
- ∀program,prefix,costs,label,i,pc',code,ppc,pc.
-  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
-   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
-    tech_pc_sigma00 program (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
+ ∀program.∀pol:policy program.∀prefix,costs,label,i,pc',code,ppc,pc.
+  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
+   construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
+    tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
 
 axiom tech_pc_sigma00_append_None:
- ∀program,prefix,i,ppc,pc,costs.
-  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
-   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
+ ∀program.∀pol:policy program.∀prefix,i,ppc,pc,costs.
+  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
+   construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
     → False.
 
 definition build_maps ≝
-  λpseudo_program.
+  λpseudo_program.λpol:policy pseudo_program.
   let result ≝
    foldl_strong
@@ -793 +807 @@
       let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
       let 〈pc',costs〉 ≝ pc_costs in
-       bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧
+       bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc') ∧
        ppc' = length … pre ∧
-       tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
+       tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉 ∧
        ∀id. occurs_exactly_once id pre →
-        lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id))
+        lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id))
     (\snd pseudo_program)
     (λprefix,i,tl,prf,t.
@@ -812 +826 @@
          ]
        in
-         match construct_costs pseudo_program ppc pc (λx. zero ?) (λx. zero ?) costs i' with
+         match construct_costs pseudo_program pol ppc pc (λx. zero ?) (λx. zero ?) costs i' with
          [ None ⇒
             let dummy ≝ 〈labels,ppc_pc_costs〉 in
@@ -858 +872 @@
 *)
 
-definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
-  λp.
+definition assembly: ∀p:pseudo_assembly_program. policy p → option (list Byte × (BitVectorTrie Identifier 16)) ≝
+  λp,pol.
     let 〈preamble, instr_list〉 ≝ p in
-    let 〈labels,costs〉 ≝ build_maps p in
+    let 〈labels,costs〉 ≝ build_maps p pol in
     let datalabels ≝ construct_datalabels preamble in
     let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
@@ -871 +885 @@
           let 〈pc, ppc_y〉 ≝ lst in
           let 〈ppc, y〉 ≝ ppc_y in
-          let x ≝ assembly_1_pseudoinstruction p ppc pc lookup_labels lookup_datalabels (\snd x) in
+          let x ≝ assembly_1_pseudoinstruction p pol ppc pc lookup_labels lookup_datalabels (\snd x) in
           match x with
           [ None ⇒ None ?

src/ASM/AssemblyProof.ma

@@ -681 +681 @@
 
 lemma fetch_assembly_pseudo:
- ∀program,ppc,lookup_labels,lookup_datalabels.
+ ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.
   ∀pi,code_memory,len,assembled,instructions,pc.
-   let expansion ≝ jump_expansion ppc program in
+   let expansion ≝ pol ppc in
    Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
-    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
+    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program pol ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
      encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
       fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
- #program #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
+ #program #pol #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
  #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2
  cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
@@ -779 +779 @@
 
 axiom assembly_ok:
- ∀program,assembled.
-  let 〈labels,costs〉 ≝ build_maps program in
-  Some … 〈assembled,costs〉 = assembly program →
+ ∀program,pol,assembled.
+  let 〈labels,costs〉 ≝ build_maps program pol in
+  Some … 〈assembled,costs〉 = assembly program pol →
   let code_memory ≝ load_code_memory assembled in
   let preamble ≝ \fst program in
   let datalabels ≝ construct_datalabels preamble in
-  let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
+  let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
   let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
    ∀ppc,len,assembledi.
     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
-     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi →
-      encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧
-       sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
+     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi →
+      encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧
+       sigma program pol newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
 
 axiom bitvector_of_nat_nat_of_bitvector:
@@ -798 +798 @@
 
 axiom assembly_ok_to_expand_pseudo_instruction_ok:
- ∀program,assembled,costs.
-  Some … 〈assembled,costs〉 = assembly program →
+ ∀program,pol,assembled,costs.
+  Some … 〈assembled,costs〉 = assembly program pol →
    ∀ppc.
     let code_memory ≝ load_code_memory assembled in
     let preamble ≝ \fst program in   
     let data_labels ≝ construct_datalabels preamble in
-    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
+    let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
     let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
-    let expansion ≝ jump_expansion ppc program in
+    let expansion ≝ pol ppc in
     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
      ∃instructions.
-      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi.
+      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi.
 
 axiom pair_elim':
@@ -849 +849 @@
 
 lemma fetch_assembly_pseudo2:
- ∀program,assembled.
-  let 〈labels,costs〉 ≝ build_maps program in
-  Some … 〈assembled,costs〉 = assembly program →
+ ∀program,pol,assembled.
+  let 〈labels,costs〉 ≝ build_maps program pol in
+  Some … 〈assembled,costs〉 = assembly program pol →
    ∀ppc.
     let code_memory ≝ load_code_memory assembled in
     let preamble ≝ \fst program in
     let data_labels ≝ construct_datalabels preamble in
-    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
+    let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
     let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
-    let expansion ≝ jump_expansion ppc program in
+    let expansion ≝ pol ppc in
     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
      ∃instructions.
-      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧
-       fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
- #program #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc
- generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program assembled costs ASSEMBLY ppc)
+      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi ∧
+       fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
+ #program #pol #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc
+ generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program pol assembled costs ASSEMBLY ppc)
  letin code_memory ≝ (load_code_memory assembled)
  letin preamble ≝ (\fst program)
  letin data_labels ≝ (construct_datalabels preamble)
- letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x))
+ letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x))
  letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
- whd in ⊢ (% → %) generalize in match (assembly_ok program assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
+ whd in ⊢ (% → %) generalize in match (assembly_ok program pol assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
  cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
- generalize in match (fetch_assembly_pseudo program ppc
-  (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
+ generalize in match (fetch_assembly_pseudo program pol ppc
+  (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
   (load_code_memory assembled));
  whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
  whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
  normalize nodelta in EXPAND; (* HERE *)
- generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program ppc))) -H1; #H1
+ generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program pol ppc))) -H1; #H1
  >bitvector_of_nat_nat_of_bitvector in H1; #H1
  <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
@@ -943 +943 @@
 
 axiom low_internal_ram_of_pseudo_internal_ram_hit:
- ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7.
+ ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀pol:policy (code_memory … s).∀addr:BitVector 7.
   member ? (eq_bv 8) (false:::addr) M = true →
    let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 
@@ -950 +950 @@
    let bl ≝ lookup ? 7 addr ram (zero 8) in
    let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
-    bu@@bl = sigma (code_memory … s) (pbu@@pbl).
+    bu@@bl = sigma (code_memory … s) pol (pbu@@pbl).
 
 (* changed from add to sub *)
@@ -1033 +1033 @@
     
 definition status_of_pseudo_status:
- internal_pseudo_address_map → PseudoStatus → option Status ≝
- λM,ps.
+ internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → option Status ≝
+ λM,ps,pol.
   let pap ≝ code_memory … ps in
-   match assembly pap with
+   match assembly pap pol with
     [ None ⇒ None …
     | Some p ⇒
        let cm ≝ load_code_memory (\fst p) in
-       let pc ≝ sigma pap (program_counter ? ps) in
+       let pc ≝ sigma pap pol (program_counter ? ps) in
        let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
        let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
@@ -1156 +1156 @@
  ∀M:internal_pseudo_address_map.
  ∀ps,ps': PseudoStatus.
-  code_memory … ps = code_memory … ps' →
-   match status_of_pseudo_status M ps with
-    [ None ⇒ status_of_pseudo_status M ps' = None …
-    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' = Some … w
+ ∀pol.
+  ∀prf:code_memory … ps = code_memory … ps'.
+   let pol' ≝ ? in
+   match status_of_pseudo_status M ps pol with
+    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
+    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
     ].
- #M #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
- generalize in match (refl … (assembly (code_memory … ps)))
- cases (assembly ?) in ⊢ (???% → %)
+ [2: <prf @pol]
+ #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
+ generalize in match (refl … (assembly (code_memory … ps) pol))
+ cases (assembly ??) in ⊢ (???% → %)
   [ #K whd whd in ⊢ (??%?) <H >K %
   | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
 qed.
 
-definition ticks_of0: pseudo_assembly_program → Word → ? → nat × nat ≝
-  λprogram: pseudo_assembly_program.
+definition ticks_of0: ∀p:pseudo_assembly_program. policy p → Word → ? → nat × nat ≝
+  λprogram: pseudo_assembly_program.λpol.
   λppc: Word.
   λfetched.
@@ -1176 +1179 @@
       match instr with
       [ JC lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1182 +1185 @@
         ]
       | JNC lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1188 +1191 @@
         ]
       | JB bit lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1194 +1197 @@
         ]
       | JNB bit lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1200 +1203 @@
         ]
       | JBC bit lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1206 +1209 @@
         ]
       | JZ lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1212 +1215 @@
         ]
       | JNZ lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1218 +1221 @@
         ]
       | CJNE arg lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1224 +1227 @@
         ]
       | DJNZ arg lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1323 +1326 @@
 qed.
 
-definition ticks_of: pseudo_assembly_program → Word → nat × nat ≝
-  λprogram: pseudo_assembly_program.
+definition ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat ≝
+  λprogram: pseudo_assembly_program.λpol.
   λppc: Word.
     let 〈preamble, pseudo〉 ≝ program in
     let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
-     ticks_of0 program ppc fetched.
+     ticks_of0 program pol ppc fetched.
 
 lemma get_register_set_program_counter: