source: src/ASM/Policy.ma @ 1934

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