source: src/ASM/Policy.ma @ 1933

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