source: src/ASM/Policy.ma @ 1809

Last change on this file since 1809 was 1809, checked in by boender, 8 years ago
  • committed partially compiling version of policy (up until jump_expansion_step)
File size: 62.4 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Status.ma".
5include alias "basics/logic.ma".
6include alias "arithmetics/nat.ma".
7include "utilities/extralib.ma".
8include "ASM/Assembly.ma".
9
10(* Internal types *)
11
12(* label_map: identifier ↦ 〈instruction number, address〉 *)
13definition label_map ≝ identifier_map ASMTag (ℕ × ℕ).
14
15(* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *)
16definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16.
17
18(* The different properties that we want/need to prove at some point *)
19(* Anything that's not in the program doesn't end up in the policy *)
20definition out_of_program_none ≝
21  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
22  ∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?.
23
24(* If instruction i is a jump, then there will be something in the policy at
25 * position i *)
26definition is_jump' ≝
27  λx:preinstruction Identifier.
28  match x with
29  [ JC _ ⇒ True
30  | JNC _ ⇒ True
31  | JZ _ ⇒ True
32  | JNZ _ ⇒ True
33  | JB _ _ ⇒ True
34  | JNB _ _ ⇒ True
35  | JBC _ _ ⇒ True
36  | CJNE _ _ ⇒ True
37  | DJNZ _ _ ⇒ True
38  | _ ⇒ False
39  ].
40 
41definition is_jump ≝
42  λx:labelled_instruction.
43  let 〈label,instr〉 ≝ x in
44  match instr with
45  [ Instruction i   ⇒ is_jump' i
46  | Call _ ⇒ True
47  | Jmp _ ⇒ True
48  | _ ⇒ False
49  ].
50
51definition jump_in_policy ≝
52  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
53  ∀i:ℕ.i < |prefix| →
54  (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
55   ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉).
56
57definition labels_okay ≝
58  λlabels:label_map.λpolicy:jump_expansion_policy.
59  bvt_forall ?? policy (λn.λx.let 〈pc,addr_nat,i〉 ≝ x in
60    ∃id:Identifier.
61      \snd (lookup_def … labels id 〈0,pc〉) = addr_nat
62  ).
63 
64(* Between two policies, jumps cannot decrease *)
65definition jmple: jump_length → jump_length → Prop ≝
66  λj1.λj2.
67  match j1 with
68  [ short_jump  ⇒
69    match j2 with
70    [ short_jump ⇒ False
71    | _          ⇒ True
72    ]
73  | medium_jump ⇒
74    match j2 with
75    [ long_jump ⇒ True
76    | _         ⇒ False
77    ]
78  | long_jump   ⇒ False
79  ].
80
81definition jmpleq: jump_length → jump_length → Prop ≝
82  λj1.λj2.jmple j1 j2 ∨ j1 = j2.
83 
84definition policy_increase: list labelled_instruction → jump_expansion_policy →
85  jump_expansion_policy → Prop ≝
86 λprogram.λop.λp.
87  (∀i:ℕ.i < |program| →
88    let 〈i1,i2,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) op 〈0,0,short_jump〉 in
89    let 〈i3,i4,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) p 〈0,0,short_jump〉 in
90    jmpleq oj j).
91
92(* Policy safety *)
93definition policy_safe: jump_expansion_policy → Prop ≝
94 λpolicy.
95 bvt_forall ?? policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in
96   match jmp_len with
97   [ short_jump  ⇒ if leb pc_nat addr_nat
98      then le (addr_nat - pc_nat) 126
99      else le (pc_nat - addr_nat) 129
100   | medium_jump ⇒
101      let addr ≝ bitvector_of_nat 16 addr_nat in
102      let pc ≝ bitvector_of_nat 16 pc_nat in
103      let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in
104      let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in
105      eq_bv 5 fst_5_addr fst_5_pc = true
106   | long_jump   ⇒ True
107   ]
108 ).
109 
110(* Definitions and theorems for the jump_length type (itself defined in Assembly) *)
111definition max_length: jump_length → jump_length → jump_length ≝
112  λj1.λj2.
113  match j1 with
114  [ long_jump   ⇒ long_jump
115  | medium_jump ⇒
116    match j2 with
117    [ medium_jump ⇒ medium_jump
118    | _           ⇒ long_jump
119    ]
120  | short_jump  ⇒
121    match j2 with
122    [ short_jump ⇒ short_jump
123    | _          ⇒ long_jump
124    ]
125  ].
126
127lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y).
128 #x #y cases x cases y /3 by inl, inr, nmk, I/
129qed.
130 
131lemma jmpleq_max_length: ∀ol,nl.
132  jmpleq ol (max_length ol nl).
133 #ol #nl cases ol cases nl
134 /2 by or_introl, or_intror, I/
135qed.
136
137lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b).
138  #a #b cases a cases b /2/
139  %2 @nmk #H destruct (H)
140qed.
141
142(* Labels *)
143definition is_label ≝
144  λx:labelled_instruction.λl:Identifier.
145  let 〈lbl,instr〉 ≝ x in
146  match lbl with
147  [ Some l' ⇒ l' = l
148  | _       ⇒ False
149  ].
150
151lemma label_does_not_occur:
152  ∀i,p,l.
153  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false.
154 #i #p #l generalize in match i; elim p
155 [ #i >nth_nil #H @⊥ @H
156 | #h #t #IH #i cases i -i
157   [ cases h #hi #hp cases hi
158     [ normalize #H @⊥ @H
159     | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ??);
160       whd in Heq; >Heq
161       >eq_identifier_refl / by refl/
162     ]
163   | #i #H whd in match (does_not_occur ??);
164     whd in match (instruction_matches_identifier ??);
165     cases h #hi #hp cases hi normalize nodelta
166     [ @(IH i) @H
167     | #l' @eq_identifier_elim
168       [ normalize / by /
169       | normalize #_ @(IH i) @H
170       ]
171     ]
172   ]
173 ]
174qed.
175
176definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
177  λpc.λjmp_len.λinstr.
178  let bv_pc ≝ bitvector_of_nat 16 pc in
179  let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) bv_pc jmp_len ? instr in
180  let bv: list (BitVector 8) ≝ match ilist with
181    [ None   ⇒ (* this shouldn't happen *) [ ]
182    | Some l ⇒ flatten … (map … assembly1 l)
183    ] in
184  pc + (|bv|).
185 @(λx.bv_pc)
186qed.
187
188(* The function that creates the label-to-address map *)
189definition create_label_map: ∀program:list labelled_instruction.
190  ∀policy:jump_expansion_policy.
191  (Σlabels:label_map.
192    ∀i:ℕ.lt i (|program|) →
193    ∀l.occurs_exactly_once l program →
194    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
195    ∃a.lookup … labels l = Some ? 〈i,a〉
196  ) ≝
197  λprogram.λpolicy.
198  let 〈final_pc, final_labels〉 ≝
199    foldl_strong (option Identifier × pseudo_instruction)
200    (λprefix.ℕ × (Σlabels.
201      ∀i:ℕ.lt i (|prefix|) →
202      ∀l.occurs_exactly_once l prefix →
203      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
204      ∃a.lookup … labels l = Some ? 〈i,a〉)
205    )
206    program
207    (λprefix.λx.λtl.λprf.λacc.
208     let 〈pc,labels〉 ≝ acc in
209     let 〈label,instr〉 ≝ x in
210       let new_labels ≝
211       match label with
212       [ None   ⇒ labels
213       | Some l ⇒ add … labels l 〈|prefix|, pc〉
214       ] in
215     let 〈i1,i2,jmp_len〉 ≝ bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈0, 0, long_jump〉 in
216       〈add_instruction_size pc jmp_len instr, new_labels〉
217    ) 〈0, empty_map …〉 in
218    final_labels.
219[ #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
220  [ #Hi #l normalize nodelta; cases label normalize nodelta
221    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
222      lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
223      % [ @addr | @Haddr ]
224    | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc;
225      @eq_identifier_elim #Heq #Hocc
226      [ normalize in Hocc;
227        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
228        @⊥ @(absurd … Hocc)
229      | normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
230        [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ]
231        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; / by /
232        ]
233      ]
234      >(label_does_not_occur i … Hl) normalize nodelta @nmk / by /
235    ]
236  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
237    [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
238      [ normalize nodelta #H @⊥ @H
239      | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_add_hit ]
240      ]
241    | @le_n
242    ]
243  ]
244| #i #Hi #l #Hl @⊥ @Hl
245]
246qed.
247
248definition select_reljump_length: label_map → ℕ → Identifier → ℕ ×jump_length ≝
249  λlabels.λpc.λlbl.
250  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
251  if leb pc addr (* forward jump *)
252  then if leb (addr - pc) 126
253       then 〈addr, short_jump〉
254       else 〈addr, long_jump〉
255  else if leb (pc - addr) 129
256       then 〈addr, short_jump〉
257       else 〈addr, long_jump〉.
258
259definition select_call_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
260  λlabels.λpc_nat.λlbl.
261  let pc ≝ bitvector_of_nat 16 pc_nat in
262  let addr_nat ≝ (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
263  let addr ≝ bitvector_of_nat 16 addr_nat in
264  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
265  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
266  if eq_bv ? fst_5_addr fst_5_pc
267  then 〈addr_nat, medium_jump〉
268  else 〈addr_nat, long_jump〉.
269 
270definition select_jump_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
271  λlabels.λpc.λlbl.
272  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
273  if leb pc addr
274  then if leb (addr - pc) 126
275       then 〈addr, short_jump〉
276       else select_call_length labels pc lbl
277  else if leb (pc - addr) 129
278       then 〈addr, short_jump〉
279       else select_call_length labels pc lbl.
280 
281definition jump_expansion_step_instruction: label_map → ℕ →
282  preinstruction Identifier → option (ℕ × jump_length) ≝
283  λlabels.λpc.λi.
284  match i with
285  [ JC j     ⇒ Some ? (select_reljump_length labels pc j)
286  | JNC j    ⇒ Some ? (select_reljump_length labels pc j)
287  | JZ j     ⇒ Some ? (select_reljump_length labels pc j)
288  | JNZ j    ⇒ Some ? (select_reljump_length labels pc j)
289  | JB _ j   ⇒ Some ? (select_reljump_length labels pc j)
290  | JBC _ j  ⇒ Some ? (select_reljump_length labels pc j)
291  | JNB _ j  ⇒ Some ? (select_reljump_length labels pc j)
292  | CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
293  | DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
294  | _        ⇒ None ?
295  ].
296
297lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x).
298#x cases x #l #i cases i
299[#id cases id
300 [1,2,3,6,7,33,34:
301  #x #y %2 whd in match (is_jump ?); /2 by nmk/
302 |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
303  #x %2 whd in match (is_jump ?); /2 by nmk/
304 |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
305 |9,10,14,15: #x %1 / by I/
306 |11,12,13,16,17: #x #y %1 / by I/
307 ]
308|2,3: #x %2 /2 by nmk/
309|4,5: #x %1 / by I/
310|6: #x #y %2 /2 by nmk/
311]
312qed.
313
314(* these should be moved to BitVector at some point, and proven *) 
315lemma bitvector_of_nat_ok:
316  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
317 #n elim n -n
318 [ #x #y #Hx #Hy #Heq <(le_n_O_to_eq ? (le_S_S_to_le ?? Hx)) <(le_n_O_to_eq ? (le_S_S_to_le ?? Hy)) @refl
319 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
320 ]
321qed.
322
323lemma bitvector_of_nat_abs:
324  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
325 #n #x #y #Hx #Hy #Heq @notb_elim
326 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
327 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
328 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/
329 | #H / by I/
330 ]
331qed.
332
333lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
334 ∀policy:(Σp:jump_expansion_policy.
335 out_of_program_none prefix p ∧ jump_in_policy prefix p).
336  ∀i:ℕ.i < |prefix| →
337  iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))
338  (lookup_opt … (bitvector_of_nat 16 i) policy = None ?).
339 #prefix #policy #i #Hi @conj
340 [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy))
341   cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);
342   [ #H @H
343   | #x cases x -x #x #z cases x -x #x #y #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
344     @(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H)))
345   ]
346 | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
347   #H elim H -H; #x #H elim H -H; #y #H elim H -H; #z #H >H in Hnone; #abs destruct (abs)
348 ] 
349qed.
350
351(* these two obviously belong somewhere else *) 
352lemma pi1_eq: ∀A:Type[0].∀P:A->Prop.∀s1:Σa1:A.P a1.∀s2:Σa2:A.P a2.
353  s1 = s2 → (pi1 ?? s1) = (pi1 ?? s2).
354 #A #P #s1 #s2 / by /
355qed.
356
357lemma Some_eq:
358 ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y.
359 #T #x #y #H @option_destruct_Some @H
360qed.
361
362(* The first step of the jump expansion: everything to short.
363 * The third condition of the dependent type implies jump_in_policy;
364 * I've left it in for convenience of type-checking. *)
365definition jump_expansion_start:
366  ∀program:(Σl:list labelled_instruction.|l| < 2^16).
367  Σpolicy:jump_expansion_policy.
368    out_of_program_none program policy ∧
369    jump_in_policy program policy ∧
370    ∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
371     lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉 ≝
372  λprogram.
373  foldl_strong (option Identifier × pseudo_instruction)
374  (λprefix.Σpolicy:jump_expansion_policy.
375    out_of_program_none prefix policy ∧
376    jump_in_policy prefix policy ∧
377    ∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
378      lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉)
379  program
380  (λprefix.λx.λtl.λprf.λpolicy.
381   let 〈label,instr〉 ≝ x in
382   match instr with
383   [ Instruction i ⇒ match i with
384     [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
385     | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
386     | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
387     | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
388     | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
389     | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
390     | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
391     | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
392     | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
393     | _ ⇒ (pi1 … policy)
394     ]
395   | Call c ⇒ bvt_insert (ℕ×ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
396   | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
397   | _      ⇒ (pi1 ?? policy)
398   ]
399  ) (Stub ? ?).
400[1,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,35,36,37,38,39,40,41,42:
401 @conj
402 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
403  @conj
404  #i >append_length <commutative_plus #Hi normalize in Hi;
405  [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
406   #Hi2 cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i)
407   [1,5,9,13,17,21,25,29,33,37,41,45,49,53,57,61,65,69,73,77,81,85,89,93,97,101,105,109,113,117,121:
408     @le_S_to_le @le_S_to_le @Hi
409   |2,6,10,14,18,22,26,30,34,38,42,46,50,54,58,62,66,70,74,78,82,86,90,94,98,102,106,110,114,118,122:
410     @Hi2
411   |3,7,11,15,19,23,27,31,35,39,43,47,51,55,59,63,67,71,75,79,83,87,91,95,99,103,107,111,115,119,123:
412     <Hi @le_n_Sn
413   |4,8,12,16,20,24,28,32,36,40,44,48,52,56,60,64,68,72,76,80,84,88,92,96,100,104,108,112,116,120,124:
414     @Hi2
415   ]
416  ]
417  cases (le_to_or_lt_eq … Hi) -Hi; #Hi
418  [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
419    >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi))
420    @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
421  ]
422  @conj >(injective_S … Hi)
423   [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
424    >(nth_append_second ? ? prefix ? ? (le_n (|prefix|))) <minus_n_n #H @⊥ @H
425   ]
426   #H elim H; -H; #t1 #H elim H; -H #t2 #H elim H; -H; #t3 #H
427   >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H;
428   [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
429     #H destruct (H)
430   ]
431   @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
432   @le_plus_n_r
433 ]
434 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
435 -Hi; #Hi
436 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
437  #Hj @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi))
438  >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; / by /
439 ]
440 >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n
441 #H @⊥ @H
442|2,3,26,27,28,29,30,31,32,33,34: @conj
443 [1,3,5,7,9,11,13,15,17,19,21: @conj
444  [1,3,5,7,9,11,13,15,17,19,21:
445    #i >append_length <commutative_plus #Hi #Hi2 normalize in Hi; >lookup_opt_insert_miss
446   [1,3,5,7,9,11,13,15,17,19,21:
447     @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
448   ]
449   >eq_bv_sym @bitvector_of_nat_abs
450   [1,4,7,10,13,16,19,22,25,28,31:
451     @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
452     @le_plus_n_r
453   |2,5,8,11,14,17,20,23,26,29,32: @Hi2
454   |3,6,9,12,15,18,21,24,27,30,33: @lt_to_not_eq @Hi
455   ]
456  ]
457  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
458  -Hi #Hi
459  [1,3,5,7,9,11,13,15,17,19,21:
460   >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) >lookup_opt_insert_miss
461   [1,3,5,7,9,11,13,15,17,19,21:
462    @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
463   ]
464   @bitvector_of_nat_abs
465   [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
466   |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
467   ]
468   @(transitive_lt … (pi2 ?? program))
469   >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
470  ]
471  @conj >(injective_S … Hi) #H
472  [2,4,6,8,10,12,14,16,18,20,22:
473   >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n / by I/
474  ]
475  @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy))))
476 ]
477 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
478  -Hi #Hi
479 [1,3,5,7,9,11,13,15,17,19,21:
480  >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #Hj >lookup_opt_insert_miss
481  [1,3,5,7,9,11,13,15,17,19,21:
482   @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi) Hj)
483  ]
484  @bitvector_of_nat_abs
485  [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
486  |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
487  ]
488  @(transitive_lt … (pi2 ?? program))
489  >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
490 ]
491 #_ >(injective_S … Hi) @lookup_opt_insert_hit
492|@conj
493 [@conj
494  [ #i #Hi / by refl/
495  | whd #i #Hi @⊥ @(absurd (i < 0) Hi (not_le_Sn_O ?))
496  ]
497 | #i #Hi >nth_nil #Hj @⊥ @Hj
498]
499qed.
500
501definition policy_equal_int ≝
502  λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
503  ∀n:ℕ.n < |program| →
504    let 〈i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,0,short_jump〉 in
505    let 〈i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,0,short_jump〉 in
506    j1 = j2.
507   
508(* One step in the search for a jump expansion fixpoint. *)
509definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
510  ∀labels:(Σlm:label_map.∀i:ℕ.lt i (|program|) →
511    ∀l.occurs_exactly_once l program →
512    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
513    ∃a.lookup … lm l = Some ? 〈i,a〉).
514  ∀old_policy:(Σpolicy.
515    out_of_program_none program policy ∧ jump_in_policy program policy).
516  (Σx:bool × ℕ × (option jump_expansion_policy).
517    let 〈changed,pc,y〉 ≝ x in
518    match y with
519    [ None ⇒ pc > 2^16
520    | Some p ⇒ out_of_program_none program p ∧ labels_okay labels p ∧
521        jump_in_policy program p ∧
522        policy_increase program old_policy p ∧
523        policy_safe p ∧
524        (changed = false → policy_equal_int program old_policy p)
525    ])
526    ≝
527  λprogram.λlabels.λold_policy.
528  let 〈final_changed, final_pc, final_policy〉 ≝
529    foldl_strong (option Identifier × pseudo_instruction)
530    (λprefix.Σx:bool × ℕ × jump_expansion_policy.
531        let 〈changed,pc,policy〉 ≝ x in
532        out_of_program_none prefix policy ∧ labels_okay labels policy ∧
533        jump_in_policy prefix policy ∧
534        policy_increase prefix old_policy policy ∧
535        policy_safe policy ∧
536        (changed = false → policy_equal_int prefix old_policy policy))
537    program
538    (λprefix.λx.λtl.λprf.λacc.
539      let 〈changed, pc, policy〉 ≝ acc in
540      let 〈label,instr〉 ≝ x in
541(*      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_policy in *)
542      let add_instr ≝
543        match instr with
544        [ Instruction i ⇒ jump_expansion_step_instruction labels pc i
545        | Call c        ⇒ Some ? (select_call_length labels pc c)
546        | Jmp j         ⇒ Some ? (select_jump_length labels pc j)
547        | _             ⇒ None ?
548        ] in
549        let 〈ignore,old_length〉 ≝ bvt_lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, 0, short_jump〉 in
550        match add_instr with
551        [ None    ⇒ (* i.e. it's not a jump *)
552          〈changed, add_instruction_size pc long_jump instr, policy〉
553        | Some z ⇒ let 〈addr,ai〉 ≝ z in
554          let new_length ≝ max_length old_length ai in
555          〈match dec_eq_jump_length new_length old_length with
556           [ inl _ ⇒ changed
557           | inr _ ⇒ true], add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, addr, new_length〉 policy〉
558        ]
559    ) 〈false, 0, Stub ? ?〉 in
560    if geb final_pc 2^16 then
561      〈final_changed,final_pc,None ?〉
562    else
563      〈final_changed,final_pc,Some jump_expansion_policy final_policy〉.
564[ normalize nodelta @leb_true_to_le @p2
565| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
566  >H2 in H; >p1 normalize nodelta //
567| lapply (pi2 ?? acc) >p >p1 normalize nodelta #Hpolicy
568 @conj [ @conj [ @conj [ @conj [ @conj
569[ (* out_of_policy_none *)
570  #i >append_length <commutative_plus #Hi normalize in Hi;
571  #Hi2 >lookup_opt_insert_miss
572  [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le … Hi)) @Hi2
573  | >eq_bv_sym @bitvector_of_nat_abs
574    [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
575      @le_S_S @le_plus_n_r
576    | @Hi2
577    | @lt_to_not_eq @Hi
578    ]
579  ]
580| (* labels_okay *)
581  @lookup_forall #i cases i -i #i cases i -i #p #a #j #n (*lapply (refl ? add_instr)
582  cases (lookup ??? old_policy ?); #x cases x -x #p1 #p2 #p3
583  cases add_instr in ⊢ (???% → %);
584  [ #Hai normalize nodelta #Hl
585    elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? n Hl)
586    #i #Hi @(ex_intro ?? i Hi)
587  | #x cases x -x #np #nl #Hai normalize nodelta *) #Hl
588    elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl
589    [ elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? n Hl)
590      #i #Hi @(ex_intro ?? i Hi)
591    | (*whd in match add_instr in Hai; cases instr in Hai;*) normalize nodelta
592      normalize nodelta in p4; cases instr in p4;
593      [2,3: #x #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
594      |6: #x #y #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
595      |1: #pi cases pi
596        [35,36,37: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
597        |1,2,3,6,7,33,34: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs)
598          #H destruct (H)
599        |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #abs normalize in abs;
600          lapply (jmeq_to_eq ??? abs) #H destruct (H)
601        |9,10,14,15: #id normalize nodelta whd in match (jump_expansion_step_instruction ???);
602          whd in match (select_reljump_length ???); >p5
603          lapply (refl ? (lookup_def ?? labels id 〈0,pc〉))
604          cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2
605          normalize nodelta #H
606          >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
607          >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
608          cases (leb pc q2) in ⊢ (???% → %); #Hle1
609          [1,3,5,7: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
610          |2,4,6,8: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
611          ]
612          #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H
613          <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl
614        |11,12,13,16,17: #x #id normalize nodelta whd in match (jump_expansion_step_instruction ???);
615          whd in match (select_reljump_length ???); >p5
616          lapply (refl ? (lookup_def ?? labels id 〈0,pc〉))
617          cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2
618          normalize nodelta #H
619          >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
620          >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
621          cases (leb pc q2) in ⊢ (???% → %); #Hle1
622          [1,3,5,7,9: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
623          |2,4,6,8,10: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
624          ]
625          #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H
626          <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl
627        ]
628      |4,5: #id normalize nodelta whd in match (select_jump_length ???);
629          whd in match (select_call_length ???); >p5
630          lapply (refl ? (lookup_def ?? labels id 〈0,pc〉))
631          cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2
632          normalize nodelta #H
633          [1: cases (leb pc q2)
634            [ cases (leb (q2-pc) 126) | cases (leb (pc-q2) 129) ]
635            [1,3: normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H;
636            #Hli @(ex_intro ?? id) lapply (proj2 ?? Hl)
637            #H >(pair_eq1 ?????? (pair_eq1 ?????? H))
638            >(pair_eq2 ?????? (pair_eq1 ?????? H)) >Hli @refl]
639          ]
640          cases (split ? 5 11 (bitvector_of_nat 16 q2)) #n1 #n2
641          cases (split ? 5 11 (bitvector_of_nat 16 pc)) #m1 #m2
642          normalize nodelta cases (eq_bv ? n1 m1)
643          normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; #H
644          @(ex_intro ?? id) lapply (proj2 ?? Hl) #H2
645          >(pair_eq1 ?????? (pair_eq1 ?????? H2)) >(pair_eq2 ?????? (pair_eq1 ?????? H2))
646          >H @refl
647      ]
648    ]
649  ]
650| (* jump_in_policy *)
651  #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
652  [ >append_length <commutative_plus #Hi normalize in Hi;
653    >(nth_append_first ?? prefix ??(le_S_S_to_le ?? Hi)) @conj
654    [ #Hj lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi))
655      #Hacc elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj
656      @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???);
657      >lookup_opt_insert_miss [ @Hj |  @bitvector_of_nat_abs ]
658      [3: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
659      |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
660      ]
661      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
662      @le_S_S @le_plus_n_r
663    | lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) #Hacc
664      #H elim H -H; #h #H elim H -H; #n #H elim H -H #j
665      #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))
666      <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs
667      [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
668      |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
669      ]
670      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
671      @le_S_S @le_plus_n_r
672    ]
673  | >append_length <commutative_plus #Hi normalize in Hi; >(injective_S … Hi)
674    >(nth_append_second ?? prefix ?? (le_n (|prefix|)))
675     <minus_n_n whd in match (nth ????); normalize nodelta in p4; cases instr in p4;
676     [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] #Hinstr @conj normalize nodelta
677     [3,5,11: #H @⊥ @H (* instr is not a jump *)
678     |4,6,12: normalize nodelta in Hinstr; lapply (jmeq_to_eq ??? Hinstr)
679      #H destruct (H)
680     |7,9: (* instr is a jump *) #_ @(ex_intro ?? pc)
681       @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
682       @lookup_opt_insert_hit
683     |8,10: #_ / by I/
684     |1,2: cases pi in Hinstr;
685       [35,36,37: #Hinstr #H @⊥ @H
686       |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hinstr #H @⊥ @H
687       |1,2,3,6,7,33,34: #x #y #Hinstr #H @⊥ @H
688       |9,10,14,15: #id #Hinstr #_
689         @(ex_intro ?? pc) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
690         @lookup_opt_insert_hit
691       |11,12,13,16,17: #x #id #Hinstr #_
692         @(ex_intro ?? pc) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
693         @lookup_opt_insert_hit
694       |72,73,74: #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)
695       |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x #Hinstr
696        lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)
697       |38,39,40,43,44,70,71: #x #y #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H
698         normalize in H; destruct (H)
699       |46,47,51,52: #id #Hinstr #_ / by I/
700       |48,49,50,53,54: #x #id #Hinstr #_ / by I/
701       ]
702     ]
703   ]
704 ]
705| (* policy increase *)
706  #i >append_length >commutative_plus #Hi normalize in Hi;
707  cases (le_to_or_lt_eq … Hi) -Hi; #Hi
708  [ >lookup_insert_miss
709    [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi))
710    | @bitvector_of_nat_abs
711      [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
712      |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
713      ]
714      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
715      @le_S_S @le_plus_n_r
716    ]
717  | >(injective_S … Hi) >p3 >lookup_insert_hit normalize nodelta
718    @pair_elim #x #y #_ @jmpleq_max_length
719  ]
720 ]
721| (* policy_safe *)
722  @lookup_forall #x cases x -x #x cases x -x #p #a #j #n normalize nodelta #Hl
723  elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl
724  [ @(forall_lookup … (proj2 ?? (proj1 ?? Hpolicy)) ? n Hl)
725  | normalize nodelta in p4; cases instr in p4;
726    [2,3: #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
727    |6: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
728    |1: #pi cases pi normalize nodelta
729     [35,36,37: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
730     |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
731       #x #abs @⊥ normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
732     |1,2,3,6,7,33,34: #x #y #abs @⊥ normalize in abs; lapply (jmeq_to_eq ??? abs) #H
733       destruct (H)
734     |9,10,14,15: #id >p5 whd in match (jump_expansion_step_instruction ???);
735       whd in match (select_reljump_length ???);
736       cases (lookup_def ?? labels id 〈0,pc〉) #q1 #q2 normalize nodelta
737       >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
738       >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
739       cases (leb pc q2) in ⊢ (???% → %); #Hle1
740       [1,3,5,7: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
741       |2,4,6,8: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
742       ]
743       #Hle2 normalize nodelta #Hli
744       <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1
745       >(pair_eq2 ?????? (proj2 ?? Hl)) <(pair_eq2 ?????? (Some_eq ??? Hli))
746       cases old_length
747       [1,7,13,19,25,31,37,43: @(leb_true_to_le … Hle2)
748       ] normalize @I (* much faster than / by I/, strangely enough *)
749     |11,12,13,16,17: #x #id >p5 whd in match (jump_expansion_step_instruction ???);
750       whd in match (select_reljump_length ???);
751       cases (lookup_def ?? labels id 〈0,pc〉) #q1 #q2 normalize nodelta
752       >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
753       >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
754       cases (leb pc q2) in ⊢ (???% → %); #Hle1
755       [1,3,5,7,9: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
756       |2,4,6,8,10: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
757       ]
758       #Hle2 normalize nodelta #Hli
759       <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 >(pair_eq2 ?????? (proj2 ?? Hl))
760       <(pair_eq2 ?????? (Some_eq ??? Hli))
761       cases old_length
762       [1,7,13,19,25,31,37,43,49,55: @(leb_true_to_le … Hle2)
763       ] normalize @I (* vide supra *)
764     ]
765    |4,5: #id >p5 normalize nodelta whd in match (select_jump_length ???);
766      whd in match (select_call_length ???); cases (lookup_def ?? labels id 〈0,pc〉)
767      #q1 #q2 normalize nodelta
768      >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
769      >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
770      [1: lapply (refl ? (leb pc q2)) cases (leb pc q2) in ⊢ (???% → %); #Hle1
771        [ lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
772        | lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
773        ]
774       #Hle2 normalize nodelta
775      ]
776      [2,4,5: lapply (refl ? (split ? 5 11 (bitvector_of_nat ? q2)))
777        cases (split ??? (bitvector_of_nat ? q2)) in ⊢ (???% → %); #x1 #x2 #Hle3
778        lapply (refl ? (split ? 5 11 (bitvector_of_nat ? pc)))
779        cases (split ??? (bitvector_of_nat ? pc)) in ⊢ (???% → %); #y1 #y2 #Hle4
780        normalize nodelta lapply (refl ? (eq_bv 5 x1 y1))
781        cases (eq_bv 5 x1 y1) in ⊢ (???% → %); #Hle5
782      ]
783      #Hli <(pair_eq1 ?????? (Some_eq ??? Hli)) >(pair_eq2 ?????? (proj2 ?? Hl))
784      <(pair_eq2 ?????? (Some_eq ??? Hli))
785      cases old_length
786      [2,8,14: >Hle3 @Hle5
787      |19,22: >Hle1 @(leb_true_to_le … Hle2)
788      ] normalize @I (* here too *)
789    ]
790  ]
791 ]
792| (* changed *)
793  cases (dec_eq_jump_length (max_length old_length ai) old_length) normalize nodelta
794  [ #Hml #Hc #i #Hi cases (le_to_or_lt_eq … Hi) -Hi >append_length >commutative_plus #Hi
795    normalize in Hi;
796    [ >lookup_insert_miss
797      [ @((proj2 ?? Hpolicy) Hc i (le_S_S_to_le … Hi))
798      | @bitvector_of_nat_abs
799        [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
800        |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
801        ]
802        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
803        @le_S_S @le_plus_n_r
804      ]
805    | >(injective_S … Hi) >p3 >lookup_insert_hit normalize nodelta
806      @pair_elim #x #y #_ @(sym_eq ??? Hml)
807    ]
808  | #_ #H destruct (H)
809  ]
810 ]
811| (* Case where add_instr = None *) normalize nodelta lapply (pi2 ?? acc) >p >p1
812  normalize nodelta #Hpolicy
813  @conj [ @conj [ @conj [ @conj [ @conj
814[ (* out_of_program_none *) #i >append_length >commutative_plus #Hi normalize in Hi;
815  #Hi2 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le ?? Hi) Hi2)
816| (* labels_okay *) @lookup_forall #x cases x -x #x cases x #p #a #j #lbl #Hl normalize nodelta
817  elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? lbl Hl)
818  #id #Hid @(ex_intro … id Hid)
819 ]
820| (* jump_in_policy *) #i >append_length >commutative_plus #Hi normalize in Hi;
821  elim (le_to_or_lt_eq … Hi) -Hi #Hi
822  [ >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi))
823    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le ?? Hi))
824  | >(injective_S … Hi) @conj
825    [ >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n whd in match (nth ????);
826      normalize nodelta in p4; cases instr in p4;
827      [ #pi cases pi
828        [1,2,3,6,7,33,34: #x #y #_ #H @⊥ @H
829        |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ #H @⊥ @H
830        |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
831          whd in match (jump_expansion_step_instruction ???);
832          #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
833        |11,12,13,16,17: #x #id normalize nodelta
834          whd in match (jump_expansion_step_instruction ???);
835          #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
836        |35,36,37: #_ #H @⊥ @H
837        ]
838      |2,3: #x #_ #H @⊥ @H
839      |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
840      |6: #x #id #_ #H @⊥ @H
841      ]
842    | #H elim H -H #p #H elim H -H #a #H elim H -H #j #H
843      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?) in H;
844      [ #H destruct (H)
845      | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
846        @le_S_S @le_plus_n_r
847      ]
848    ]
849  ]
850 ]
851| (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
852  elim (le_to_or_lt_eq … Hi) -Hi #Hi
853  [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi))
854  | >(injective_S … Hi) >lookup_opt_lookup_miss
855    [ >lookup_opt_lookup_miss
856      [ normalize nodelta %2 @refl
857      | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?)
858        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
859        @le_S_S @le_plus_n_r
860      ]
861    | @(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?)) >prf
862      [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
863      | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p2
864        whd in match (nth ????); normalize nodelta in p4; cases instr in p4;
865        [ #pi cases pi
866          [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/
867          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/
868          |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
869            whd in match (jump_expansion_step_instruction ???);
870            #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
871          |11,12,13,16,17: #x #id normalize nodelta
872            whd in match (jump_expansion_step_instruction ???);
873            #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
874          |35,36,37: #_ normalize /2 by nmk/
875          ]
876        |2,3: #x #_ normalize /2 by nmk/
877        |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
878        |6: #x #id #_ normalize /2 by nmk/
879        ]
880      ]
881    ]
882  ]
883 ]
884| (* policy_safe *) @lookup_forall #x cases x -x #x cases x -x #p #a #j #n #Hl
885  @(forall_lookup … (proj2 ?? (proj1 ?? Hpolicy)) ? n Hl)
886 ]
887| (* changed *) #Hc #i >append_length >commutative_plus #Hi normalize in Hi;
888  elim (le_to_or_lt_eq … Hi) -Hi #Hi
889  [ @((proj2 ?? Hpolicy) Hc i (le_S_S_to_le … Hi))
890  | >(injective_S … Hi) >lookup_opt_lookup_miss
891    [ >lookup_opt_lookup_miss
892      [ normalize nodelta @refl
893      | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?)
894        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
895        @le_S_S @le_plus_n_r
896      ]
897    | @(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?)) >prf
898      [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
899      | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p2
900        whd in match (nth ????); normalize nodelta in p4; cases instr in p4;
901        [ #pi cases pi
902          [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/
903          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/
904          |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
905            whd in match (jump_expansion_step_instruction ???);
906            #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
907          |11,12,13,16,17: #x #id normalize nodelta
908            whd in match (jump_expansion_step_instruction ???);
909            #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
910          |35,36,37: #_ normalize /2 by nmk/
911          ]
912        |2,3: #x #_ normalize /2 by nmk/
913        |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
914        |6: #x #id #_ normalize /2 by nmk/
915        ]
916      ]
917    ]
918  ]
919 ]       
920| @conj [ @conj [ @conj [ @conj [ @conj
921  [ #i #Hi //
922  | //
923  ]
924  | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3
925                   normalize in H3; destruct (H3) ]
926  ]                 
927  | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
928  ]
929  | //
930  ]
931  | #_ #i #Hi @⊥ @(absurd (i < 0)) [ @Hi | @not_le_Sn_O ]
932  ]
933qed.
934
935(* this might be replaced by a coercion: (∀x.A x → B x) → Σx.A x → Σx.B x *)
936(* definition weaken_policy:
937  ∀program,op.
938  option (Σp:jump_expansion_policy.
939    And (And (And (And (out_of_program_none program p)
940    (labels_okay (create_label_map program op) p))
941    (jump_in_policy program p)) (policy_increase program op p))
942    (policy_safe p)) →
943  option (Σp:jump_expansion_policy.And (out_of_program_none program p)
944    (jump_in_policy program p)) ≝
945 λprogram.λop.λx.
946 match x return λ_.option (Σp.And (out_of_program_none program p) (jump_in_policy program p)) with
947 [ None ⇒ None ?
948 | Some z ⇒ Some ? (mk_Sig ?? (pi1 ?? z) ?)
949 ].
950@conj
951[ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? z)))))
952| @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? z))))
953]
954qed. *)
955
956(* This function executes n steps from the starting point. *)
957let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (|l|) 2^16)
958  (n: ℕ) on n:(Σx:ℕ × (option jump_expansion_policy).
959    let 〈pc,y〉 ≝ x in
960    match y with
961    [ None ⇒ pc > 2^16
962    | Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p)
963    ]) ≝
964  match n with
965  [ O   ⇒ 〈0,Some ? (pi1 … (jump_expansion_start program))〉
966  | S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
967          match z return λx. z=x → Σa:ℕ × (option jump_expansion_policy).? with
968          [ None    ⇒ λp2.〈pc,None ?〉
969          | Some op ⇒ λp2.pi1 … (jump_expansion_step program (create_label_map program op) «op,?»)
970          ] (refl … z)
971  ].
972[ normalize nodelta @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
973| normalize nodelta lapply (pi2 ?? (jump_expansion_internal program m))
974    <p1 >p2 / by /
975|4: cases (jump_expansion_step program (create_label_map program op) «op,?»)
976    #p cases p #q #r cases r normalize nodelta
977    [ / by /
978    | #j #H @conj
979      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
980      | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
981      ]
982    ]
983| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 / by /
984]
985qed.
986 
987lemma pe_int_refl: ∀program.reflexive ? (policy_equal_int program).
988#program whd #x whd #n #Hn
989cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
990#y cases y -y #y #z normalize nodelta @refl
991qed.
992
993lemma pe_int_sym: ∀program.symmetric ? (policy_equal_int program).
994#program whd #x #y #Hxy whd #n #Hn
995lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
996#z cases z -z #x1 #x2 #x3
997cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉)
998#z cases z -z #y1 #y2 #y3 normalize nodelta //
999qed.
1000 
1001lemma pe_int_trans: ∀program.transitive ? (policy_equal_int program).
1002#program whd #x #y #z whd in match (policy_equal_int ???); whd in match (policy_equal_int ?y ?);
1003whd in match (policy_equal_int ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
1004lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
1005#z cases z -z #x1 #x2 #x3
1006cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z -z 
1007#y1 #y2 #y3
1008cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z -z 
1009#z1 #z2 #z3 normalize nodelta //
1010qed.
1011
1012definition policy_equal ≝
1013  λprogram:list labelled_instruction.λp1,p2:option jump_expansion_policy.
1014  match p1 with
1015  [ Some x1 ⇒ match p2 with
1016              [ Some x2 ⇒ policy_equal_int program x1 x2
1017              | _       ⇒ False
1018              ]
1019  | None    ⇒ p2 = None ?
1020  ].
1021
1022lemma pe_refl: ∀program.reflexive ? (policy_equal program).
1023#program whd #x whd cases x
1024[ //
1025| #y @pe_int_refl
1026]
1027qed.
1028
1029lemma pe_sym: ∀program.symmetric ? (policy_equal program).
1030#program whd #x #y #Hxy whd cases y in Hxy;
1031[ cases x
1032  [ //
1033  | #x' #H @⊥ @(absurd ? H) /2 by nmk/
1034  ]
1035| #y' cases x
1036  [ #H @⊥ @(absurd ? H) whd in match (policy_equal ???); @nmk #H destruct (H)
1037  | #x' #H @pe_int_sym @H
1038  ]
1039]
1040qed.
1041
1042lemma pe_trans: ∀program.transitive ? (policy_equal program).
1043#program whd #x #y #z cases x
1044[ #Hxy #Hyz >Hxy in Hyz; //
1045| #x' cases y
1046  [ #H @⊥ @(absurd ? H) /2 by nmk/
1047  | #y' cases z
1048    [ #_ #H @⊥ @(absurd ? H) /2 by nmk/
1049    | #z' @pe_int_trans
1050    ]
1051  ]
1052]
1053qed.
1054
1055definition step_none: ∀program.∀n.
1056  (\snd (pi1 ?? (jump_expansion_internal program n))) = None ? →
1057  ∀k.(\snd (pi1 ?? (jump_expansion_internal program (n+k)))) = None ?.
1058#program #n lapply (refl ? (jump_expansion_internal program n))
1059 cases (jump_expansion_internal program n) in ⊢ (???% → %);
1060 #x1 cases x1 #p1 #j1 -x1; #H1 #Heqj #Hj #k elim k
1061[ <plus_n_O >Heqj @Hj
1062| #k' -k <plus_n_Sm lapply (refl ? (jump_expansion_internal program (n+k')))
1063  cases (jump_expansion_internal program (n+k')) in ⊢ (???% → % → %);
1064  #x2 cases x2 #p2 #j2 -x2; normalize nodelta #H #Heqj2
1065  cases j2 in H Heqj2;
1066  [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??);
1067    >Heqj2 normalize nodelta @refl
1068  | #x #H #Heqj2 #abs destruct (abs)
1069  ]
1070]
1071qed.
1072
1073lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
1074  ∀n.policy_equal program (\snd (pi1 ?? (jump_expansion_internal program n)))
1075   (\snd (pi1 ?? (jump_expansion_internal program (S n)))) →
1076  policy_equal program (\snd (pi1 ?? (jump_expansion_internal program (S n))))
1077    (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))).
1078#program #n #Heq
1079cases daemon (* XXX *)
1080qed.
1081
1082(* this is in the stdlib, but commented out, why? *)
1083theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
1084  #n (elim n) normalize /2 by S_pred/ qed.
1085 
1086lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.|l| < 2^16).∀n:ℕ.
1087  policy_equal program (\snd (pi1 … (jump_expansion_internal program n)))
1088   (\snd (pi1 … (jump_expansion_internal program (S n)))) →
1089  ∀k.k ≥ n → policy_equal program (\snd (pi1 … (jump_expansion_internal program n)))
1090   (\snd (pi1 … (jump_expansion_internal program k))).
1091#program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
1092lapply Heq -Heq; lapply n -n; elim z -z;
1093[ #n #Heq <plus_n_O @pe_refl
1094| #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z);
1095  @(pe_trans … (\snd (pi1 … (jump_expansion_internal program (S n)))))
1096  [ @Heq
1097  | @Hind @pe_step @Heq
1098  ]
1099]
1100qed.
1101
1102(* this number monotonically increases over iterations, maximum 2*|program| *)
1103let rec measure_int (program: list labelled_instruction) (policy: jump_expansion_policy) (acc: ℕ)
1104 on program: ℕ ≝
1105 match program with
1106 [ nil      ⇒ acc
1107 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,00
1108,short_jump〉)) with
1109   [ long_jump   ⇒ measure_int t policy (acc + 2)
1110   | medium_jump ⇒ measure_int t policy (acc + 1)
1111   | _           ⇒ measure_int t policy acc
1112   ]
1113 ].
1114
1115lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
1116 measure_int program policy (x+d) = measure_int program policy x + d.
1117#program #policy #x #d generalize in match x; -x elim d
1118[ //
1119| -d; #d #Hind elim program
1120  [ / by refl/
1121  | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
1122    cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
1123    [ normalize nodelta @Hd
1124    |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
1125      @Hd
1126    ]
1127  ]
1128]
1129qed.
1130
1131lemma measure_le: ∀program.∀policy.
1132  measure_int program policy 0 ≤ 2*|program|.
1133#program #policy elim program
1134[ normalize @le_n
1135| #h #t #Hind whd in match (measure_int ???);
1136  cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
1137  [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
1138  |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
1139    @le_plus [1,3: @Hind |2,4: // ]
1140  ]
1141]
1142qed.
1143
1144lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
1145  ∀policy:Σp:jump_expansion_policy.
1146    out_of_program_none program p ∧ jump_in_policy program p.
1147  ∀l.|l| ≤ |program| → ∀acc:ℕ.
1148  match \snd (jump_expansion_step program (create_label_map program policy) policy) with
1149  [ None   ⇒ True
1150  | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
1151  ].
1152#program #policy #l elim l -l;
1153[ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ]
1154| #h #t #Hind #Hp #acc
1155  lapply (refl ? (jump_expansion_step program (create_label_map program policy) policy))
1156  cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 #p #q -pi1; cases q
1157  [ //
1158  | #x #Hx #Hjeq normalize nodelta lapply (proj2 ?? (proj1 ?? Hx) (|t|) Hp)
1159    whd in match (measure_int ???); whd in match (measure_int ? x ?);
1160    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)
1161    #z cases z -z #x1 #x2 #x3
1162    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) x 〈0,0,short_jump〉)
1163    #z cases z -z #y1 #y2 #y3
1164    normalize nodelta #Hj cases Hj
1165    [ cases x3 cases y3
1166      [1,4,5,7,8,9: #H @⊥ @H
1167      |2,3,6: #_ normalize nodelta
1168        [1,2: @(transitive_le ? (measure_int t x acc))
1169        |3: @(transitive_le ? (measure_int t x (acc+1)))
1170        ]
1171        [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus //]
1172        >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
1173        ]
1174    | #Heq >Heq cases y3 normalize nodelta
1175      [2,3: >measure_plus >measure_plus @le_plus //]
1176      >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
1177    ]
1178  ]
1179]
1180qed.
1181
1182(* these lemmas seem superfluous, but not sure how *)
1183lemma bla: ∀a,b:ℕ.a + a = b + b → a = b.
1184 #a elim a
1185 [ normalize #b //
1186 | -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ | -b #b normalize
1187   <plus_n_Sm <plus_n_Sm #H
1188   >(Hind b (injective_S ?? (injective_S ?? H))) // ]
1189 ]
1190qed.
1191
1192lemma sth_not_s: ∀x.x ≠ S x.
1193 #x cases x
1194 [ // | #y // ]
1195qed.
1196 
1197lemma measure_full: ∀program.∀policy.
1198  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
1199  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,0,short_jump〉)) = long_jump.
1200#program #policy elim program
1201[ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1202| #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
1203  [ whd in match (measure_int ???) in Hm;
1204    cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
1205    normalize nodelta
1206    [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
1207    | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
1208      <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize
1209      >(commutative_plus (|t|) 0) <plus_O_n <minus_n_O
1210      >plus_n_Sm @le_n
1211    | >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) //
1212    ]
1213  | #Hmt cases (le_to_or_lt_eq … Hi) -Hi;
1214  [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
1215  | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
1216    cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
1217    normalize nodelta
1218    [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
1219      >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s
1220    | >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize
1221      #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s
1222    | #_ //
1223    ]
1224  ]]
1225]
1226qed.
1227
1228lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
1229  ∀policy:Σp:jump_expansion_policy.
1230    out_of_program_none program p ∧ jump_in_policy program p.
1231  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy))) with
1232  [ None ⇒ True
1233  | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_equal_int program policy p ].
1234#program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy)))
1235cases (jump_expansion_step program (create_label_map program policy) policy) in ⊢ (???% → %);
1236#p cases p #pc #pol normalize nodelta cases pol
1237[ //
1238| #p normalize nodelta #Hpol #eqpol lapply (le_n (|program|))
1239  @(list_ind ?  (λx.|x| ≤ |pi1 ?? program| →
1240      measure_int x policy 0 = measure_int x p 0 →
1241      policy_equal_int x policy p) ?? (pi1 ?? program))
1242 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
1243 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
1244   [ #Hi @Hind
1245     [ @(transitive_le … Hp) //
1246     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
1247       lapply (proj2 ?? (proj1 ?? Hpol) (|t|) Hp)
1248       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
1249       #x cases x -x #x1 #x2 #x3
1250       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
1251       #y cases y -y #y1 #y2 #y3
1252       cases x3 cases y3 normalize nodelta
1253       [1: #H #_ @H
1254       |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
1255         lapply (measure_incr_or_equal program policy t ? 0)
1256         [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol //
1257       |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
1258       |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
1259         #H #_ @(injective_plus_r … H)
1260       |6: >measure_plus >measure_plus
1261          change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
1262          #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
1263          lapply (measure_incr_or_equal program policy t ? 0)
1264          [ @(transitive_le … Hp) @le_n_Sn ] >eqpol //
1265       |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
1266         #H #_ @(injective_plus_r … H)
1267       ]
1268     | @(le_S_S_to_le … Hi)
1269     ]
1270   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
1271     whd in match (measure_int ? p ?) in Hm;
1272     lapply (proj2 ?? (proj1 ?? Hpol) (|t|) Hp)
1273     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in   
1274Hm;
1275     #x cases x -x #x1 #x2 #x3
1276     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
1277     #y cases y -y #y1 #y2 #y3
1278     normalize nodelta cases x3 cases y3 normalize nodelta
1279     [1,5,9: #_ #_ //
1280     |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
1281     |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
1282       lapply (measure_incr_or_equal program policy t ? 0)
1283       [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
1284     |6: >measure_plus >measure_plus
1285        change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
1286        #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
1287        lapply (measure_incr_or_equal program policy t ? 0)
1288        [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
1289     ]
1290   ]
1291 ]
1292qed.
1293
1294lemma le_to_eq_plus: ∀n,z.
1295  n ≤ z → ∃k.z = n + k.
1296 #n #z elim z
1297 [ #H cases (le_to_or_lt_eq … H)
1298   [ #H2 @⊥ @(absurd … H2) @not_le_Sn_O
1299   | #H2 @(ex_intro … 0) >H2 //
1300   ]
1301 | #z' #Hind #H cases (le_to_or_lt_eq … H)
1302   [ #H' elim (Hind (le_S_S_to_le … H')) #k' #H2 @(ex_intro … (S k'))
1303     >H2 >plus_n_Sm //
1304   | #H' @(ex_intro … 0) >H' //
1305   ]
1306 ]
1307qed.
1308
1309lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
1310  |l| ≤ |program| → measure_int l (jump_expansion_start program) 0 = 0.
1311 #l #program elim l
1312 [ //
1313 | #h #t #Hind #Hp whd in match (measure_int ???);
1314   cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
1315   [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,0,short_jump〉)
1316     [ normalize nodelta @Hind @le_S_to_le ]
1317     @Hp
1318   | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (pi1 ?? (jump_expansion_start program)) (|t|) ?) Hj) 〈0,0,short_jump〉)
1319     [ normalize nodelta @Hind @le_S_to_le @Hp
1320     | @Hp
1321     | %
1322       [ @(proj1 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program))))
1323       | @(proj2 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program))))
1324       ]
1325     ]
1326   ]
1327 ]
1328qed.
1329
1330(* the actual computation of the fixpoint *)
1331definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
1332  Σp:option jump_expansion_policy.∃n.∀k.n < k →
1333    policy_equal program (\snd (pi1 ?? (jump_expansion_internal program k))) p.
1334#program @(\snd (pi1 ?? (jump_expansion_internal program (2*|program|))))
1335(*@(ex_intro … (2*|program|)) #k #Hk*)
1336cases (dec_bounded_exists (λk.policy_equal (pi1 ?? program)
1337   (\snd (pi1 ?? (jump_expansion_internal program k)))
1338   (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|))
1339[ #Hex elim Hex -Hex #x #Hx @(ex_intro … x) #k @pe_trans
1340  [ @(\snd (pi1 ?? (jump_expansion_internal program x)))
1341  | @pe_sym @equal_remains_equal
1342    [ @(proj2 ?? Hx)
1343    | @(transitive_le ? (2*|program|))
1344      [ @le_S_S_to_le @le_S @(proj1 ?? Hx)
1345      | @le_S_S_to_le @le_S @Hk
1346      ]
1347    ]
1348  | @equal_remains_equal
1349    [ @(proj2 ?? Hx)
1350    | @le_S_S_to_le @le_S @(proj1 ?? Hx)
1351    ]   
1352  ]
1353| #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @pe_sym @equal_remains_equal
1354  [ lapply (refl ? (jump_expansion_internal program (2*|program|)))
1355    cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
1356    #jep cases jep #pc #x -jep cases x normalize nodelta
1357    [ #Hjep #Heqx >Heqx lapply (step_none program (2*|pi1 ?? program|) ? 1)
1358      [ >Heqx // | <plus_n_Sm <plus_n_O #H >H // ]
1359    | #pol_2prog #H2prog #Heq2prog lapply (measure_full (pi1 ?? program) pol_2prog) #Hfull
1360      whd in match (policy_equal ???); lapply Heq2prog -Heq2prog;
1361      lapply (refl ? (jump_expansion_internal program (2*|program|)))
1362      cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → % → %);
1363      #z cases z #fpc #pol -z cases pol normalize nodelta
1364      [ #Heq2prog #Hjep #Hploq destruct (Hploq)
1365      | #p #Heq2prog #Hjep #Hploq whd in match (jump_expansion_internal ??);
1366        >Hjep normalize nodelta
1367        lapply (refl ? (jump_expansion_step program (create_label_map program p) «p,?»))
1368        [2: cases (jump_expansion_step program (create_label_map program p) «p,?») in ⊢ (???% → %);
1369        #x cases x #Spc #Spol -x cases Spol normalize nodelta
1370        [ #Hy #Hgnarf cases daemon (* XXX *)
1371        | #y #Hy #Hgnarf #i #Hi lapply (proj2 ?? (proj1 ?? Hy) i Hi)
1372          lapply (Hfull ? i Hi)
1373          [2: lapply (sym_eq ??? (proj1 ?? Hpy)) #Hblp >(Some_eq ??? Hblp)
1374                >(Some_eq ??? (pair_eq2 ?????? (pi1_eq ???? Hploq)))
1375                cases (bvt_lookup ?? (bitvector_of_nat 16 i) pol_2prog 〈0,0,short_jump〉)
1376                #blp cases blp #a #b #c -blp #EQ >EQ normalize nodelta
1377                cases (bvt_lookup ?? (bitvector_of_nat 16 i) y 〈0,0,short_jump〉)
1378                #blp cases blp #d #e #f -blp normalize nodelta cases f
1379                [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ]
1380                | #_ //
1381                ]
1382            | @le_to_le_to_eq
1383              [ @measure_le
1384              | cut (∀x.x ≤ (2*|pi1 ?? program|) →
1385                  ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧
1386                      x ≤ measure_int program p 0))
1387                [ #n elim n
1388                  [ #_ whd in match (jump_expansion_internal program 0);
1389                    @(ex_intro … (jump_expansion_start program)) % [ @refl |
1390                    >measure_zero @le_n ]
1391                  | -n #n' #Hind #Hn' elim (le_to_or_lt_eq … Hn')
1392                    [ #H2n' elim (Hind ?)
1393                      [ -Hgnarf #pn' lapply (refl ? (jump_expansion_internal program (S n')))
1394                        cases (jump_expansion_internal program (S n')) in ⊢ (???% → %);
1395                        #x cases x -x #npc #npol cases npol normalize nodelta
1396                        [ #Hbla #Hnone #Hsome lapply (step_none program (S n'))
1397                          >Hnone normalize nodelta #Ht elim (le_to_eq_plus ?? Hn')
1398                          #k #Hk lapply (Ht ? k) [ // | <Hk >Hjep #H destruct (H) ]
1399                        | #Spol #Hbla #HSpol #H3 @(ex_intro ?? Spol) @conj [ @refl |
1400                          lapply (measure_incr_or_equal program pn' program)
1401                          lapply (pi2 ?? (jump_expansion_internal program n'))
1402                          >(proj1 ?? H3)
1403                          lapply (refl ? (jump_expansion_internal program n'))
1404                          lapply H3 -H3
1405                          cases (jump_expansion_internal program n') in ⊢ (% → ???% → %);
1406                          #x cases x -x #npc #npol normalize nodelta #Hbli #H3 #EQ
1407                          >(proj1 ?? H3) in Hbli EQ; #Hbli #EQ
1408                          whd in match (jump_expansion_internal program (S n')) in HSpol;
1409                          >EQ in HSpol; normalize nodelta
1410                        ] ]                       
1411                       
1412                       
1413                       
1414                      |
1415                      ]
1416                     |
1417                     ]
1418                   ]
1419                   
1420                | #gloeirks elim (gloeirks (2*|program|) (le_n ?)) #q
1421                  >Hjep >(Some_eq ??? (pair_eq2 ?????? (pi1_eq ???? Hploq)))
1422                  #H >(Some_eq ??? (proj1 ?? H)) @(proj2 ?? H)
1423                ]
1424              ]
1425            ]
1426          ]
1427        ]]
1428      ]
1429    ]
1430  | @le_S_to_le @Hk
1431  ]
1432| (* TO BE CHANGED *)
1433  #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
1434  [ %1 //
1435  |2,3: #x %2 @nmk whd in match (policy_equal ???); [2: //]
1436    whd in match (eject_policy_opt ???); #H destruct (H)
1437  |4: #p1 #p2 whd in match (policy_equal ???); @dec_bounded_forall #m
1438      cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉)
1439      #x cases x -x #x1 #x2 #x3
1440      cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉)
1441      #y cases y -y #y1 #y2 #y3 normalize nodelta
1442      @dec_eq_jump_length 
1443  ]
1444]
1445
1446(* Take a policy of 〈pc, addr, jump_length〉 tuples, and transform it into
1447 * a map from pc to jump_length. This cannot be done earlier because the pc
1448 * changes between iterations. *)
1449let rec transform_policy (n: nat) policy (acc: BitVectorTrie jump_length 16) on n:
1450  BitVectorTrie jump_length 16 ≝
1451  match n with
1452  [ O    ⇒ acc
1453  | S n' ⇒
1454    match lookup_opt … (bitvector_of_nat 16 n') policy with
1455    [ None   ⇒ transform_policy n' policy acc
1456    | Some x ⇒ let 〈pc,length〉 ≝ x in
1457      transform_policy n' policy (insert … pc length acc)
1458    ]
1459  ].
1460
1461(* The glue between Policy and Assembly. *)
1462definition jump_expansion':
1463 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
1464 policy_type ≝
1465 λprogram.λpc.
1466  let policy ≝
1467    transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in
1468  lookup ? ? pc policy long_jump.
1469/2 by Stub, mk_Sig/
1470qed.
Note: See TracBrowser for help on using the repository browser.