source: src/ASM/Policy.ma @ 1956

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