source: src/ASM/Policy.ma @ 1932

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