source: src/ASM/Policy.ma @ 1886

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