source: src/ASM/Policy.ma @ 1931

Last change on this file since 1931 was 1931, checked in by boender, 9 years ago
  • added latest bvt alias
  • temporary "cases daemon" commit of new policy type
File size: 84.7 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
1345let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (length ? l) 2^16) (n: ℕ)
1346  on n:(Σx:bool × (option ppc_pc_map).
1347    let 〈c,pol〉 ≝ x in
1348    match pol with
1349    [ None ⇒ True
1350    | Some x ⇒
1351      And (And (And
1352        (out_of_program_none program x)
1353        (jump_in_policy program x))
1354        (policy_isize_sum program (create_label_map program) x))
1355        (\fst x < 2^16)
1356    ]) ≝
1357  let labels ≝ create_label_map program in
1358  match n with
1359  [ O   ⇒ 〈true,Some ? (pi1 ?? (jump_expansion_start program labels))〉
1360  | S m ⇒ let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
1361          match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with
1362          [ None    ⇒ λp2.〈false,None ?〉
1363          | Some op ⇒ λp2.if ch
1364            then pi1 ?? (jump_expansion_step program labels «op,?»)
1365            else (jump_expansion_internal program m)
1366          ] (refl … z)
1367  ].
1368[ normalize nodelta @conj
1369  [ @conj
1370    [ @(pi2 ?? (jump_expansion_start program (create_label_map program)))
1371    | (* XXX *) cases daemon
1372    ]
1373  | (* XXX *) cases daemon
1374  ]
1375| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
1376| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
1377| normalize nodelta cases (jump_expansion_step program labels «op,?»)
1378  #p cases p -p #p #r cases r normalize nodelta
1379  [ #H / by I/
1380  | #j #H @conj
1381    [ @conj
1382      [ @conj
1383        [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))))
1384        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))))
1385        ]
1386      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
1387      ]
1388    | @(proj2 ?? H)
1389    ]
1390  ]
1391]
1392qed.
1393
1394lemma pe_int_refl: ∀program.reflexive ? (policy_equal program).
1395#program whd #x whd #n #Hn
1396cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,None ?〉)
1397#y #z normalize nodelta @refl
1398qed.
1399
1400lemma pe_int_sym: ∀program.symmetric ? (policy_equal program).
1401#program whd #x #y #Hxy whd #n #Hn
1402lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,None ?〉)
1403#x1 #x2
1404cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,None ?〉)
1405#y1 #y2 normalize nodelta //
1406qed.
1407 
1408lemma pe_int_trans: ∀program.transitive ? (policy_equal program).
1409#program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?);
1410whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
1411lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,None ?〉)
1412#x1 #x2
1413cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,None ?〉) #y1 #y2
1414cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,None ?〉) #z1 #z2
1415normalize nodelta //
1416qed.
1417
1418definition policy_equal_opt ≝
1419  λprogram:list labelled_instruction.λp1,p2:option ppc_pc_map.
1420  match p1 with
1421  [ Some x1 ⇒ match p2 with
1422              [ Some x2 ⇒ policy_equal program x1 x2
1423              | _       ⇒ False
1424              ]
1425  | None    ⇒ p2 = None ?
1426  ].
1427
1428lemma pe_refl: ∀program.reflexive ? (policy_equal_opt program).
1429#program whd #x whd cases x
1430[ //
1431| #y @pe_int_refl
1432]
1433qed.
1434
1435lemma pe_sym: ∀program.symmetric ? (policy_equal_opt program).
1436#program whd #x #y #Hxy whd cases y in Hxy;
1437[ cases x
1438  [ //
1439  | #x' #H @⊥ @(absurd ? H) /2 by nmk/
1440  ]
1441| #y' cases x
1442  [ #H @⊥ @(absurd ? H) whd in match (policy_equal_opt ???); @nmk #H destruct (H)
1443  | #x' #H @pe_int_sym @H
1444  ]
1445]
1446qed.
1447
1448lemma pe_trans: ∀program.transitive ? (policy_equal_opt program).
1449#program whd #x #y #z cases x
1450[ #Hxy #Hyz >Hxy in Hyz; //
1451| #x' cases y
1452  [ #H @⊥ @(absurd ? H) /2 by nmk/
1453  | #y' cases z
1454    [ #_ #H @⊥ @(absurd ? H) /2 by nmk/
1455    | #z' @pe_int_trans
1456    ]
1457  ]
1458]
1459qed.
1460
1461definition step_none: ∀program.∀n.
1462  (\snd (pi1 ?? (jump_expansion_internal program n))) = None ? →
1463  ∀k.(\snd (pi1 ?? (jump_expansion_internal program (n+k)))) = None ?.
1464#program #n lapply (refl ? (jump_expansion_internal program n))
1465 cases (jump_expansion_internal program n) in ⊢ (???% → %);
1466 #x1 cases x1 #p1 #j1 -x1; #H1 #Heqj #Hj #k elim k
1467[ <plus_n_O >Heqj @Hj
1468| #k' -k <plus_n_Sm whd in match (jump_expansion_internal program (S (n+k')));
1469  lapply (refl ? (jump_expansion_internal program (n+k')))
1470  cases (jump_expansion_internal program (n+k')) in ⊢ (???% → % → %);
1471  #x2 cases x2 -x2 #c2 #p2 normalize nodelta #H #Heqj2
1472  cases p2 in H Heqj2;
1473  [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??);
1474    >Heqj2 normalize nodelta @refl
1475  | #x #H #Heqj2 #abs destruct (abs)
1476  ]
1477]
1478qed.
1479
1480lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
1481  ∀n.policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program n)))
1482   (\snd (pi1 ?? (jump_expansion_internal program (S n)))) →
1483  policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program (S n))))
1484    (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))).
1485#program #n #Heq
1486cases daemon (* XXX *)
1487qed.
1488
1489(* this is in the stdlib, but commented out, why? *)
1490theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
1491  #n (elim n) normalize /2 by S_pred/ qed.
1492 
1493lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.|l| < 2^16).∀n:ℕ.
1494  policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n)))
1495   (\snd (pi1 … (jump_expansion_internal program (S n)))) →
1496  ∀k.k ≥ n → policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n)))
1497   (\snd (pi1 … (jump_expansion_internal program k))).
1498#program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
1499lapply Heq -Heq; lapply n -n; elim z -z;
1500[ #n #Heq <plus_n_O @pe_refl
1501| #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z);
1502  @(pe_trans … (\snd (pi1 … (jump_expansion_internal program (S n)))))
1503  [ @Heq
1504  | @Hind @pe_step @Heq
1505  ]
1506]
1507qed.
1508
1509(* this number monotonically increases over iterations, maximum 2*|program| *)
1510let rec measure_int (program: list labelled_instruction) (policy: ppc_pc_map) (acc: ℕ)
1511 on program: ℕ ≝
1512 match program with
1513 [ nil      ⇒ acc
1514 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)) with
1515   [ None ⇒ measure_int t policy acc
1516   | Some j ⇒ match j with
1517     [ long_jump   ⇒ measure_int t policy (acc + 2)
1518     | medium_jump ⇒ measure_int t policy (acc + 1)
1519     | _           ⇒ measure_int t policy acc
1520     ]
1521   ]
1522 ].
1523
1524lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
1525 measure_int program policy (x+d) = measure_int program policy x + d.
1526#program #policy #x #d generalize in match x; -x elim d
1527[ //
1528| -d; #d #Hind elim program
1529  [ / by refl/
1530  | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
1531    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉))
1532    [ normalize nodelta @Hd
1533    | #x cases x
1534      [ normalize nodelta @Hd
1535      |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
1536        @Hd
1537      ]
1538    ]
1539  ]
1540]
1541qed.
1542
1543lemma measure_le: ∀program.∀policy.
1544  measure_int program policy 0 ≤ 2*|program|.
1545#program #policy elim program
1546[ normalize @le_n
1547| #h #t #Hind whd in match (measure_int ???);
1548  cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉))
1549  [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
1550  | #x cases x
1551    [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
1552    |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
1553      @le_plus [1,3: @Hind |2,4: / by le_n/ ]
1554    ]
1555  ]
1556]
1557qed.
1558
1559lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
1560  ∀policy:Σp:ppc_pc_map.
1561    out_of_program_none program p ∧ jump_in_policy program p ∧
1562    policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16.
1563  ∀l.|l| ≤ |program| → ∀acc:ℕ.
1564  match \snd (jump_expansion_step program (create_label_map program) policy) with
1565  [ None   ⇒ True
1566  | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
1567  ].
1568#program #policy #l elim l -l;
1569[ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ]
1570| #h #t #Hind #Hp #acc
1571  lapply (refl ? (jump_expansion_step program (create_label_map program) policy))
1572  cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #c #r cases r
1573  [ / by I/
1574  | #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (|t|) Hp)
1575    whd in match (measure_int ???); whd in match (measure_int ? x ?);
1576    cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉))
1577    [ #Hj
1578      elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))))) (|t|) ?) Hj)
1579      [ #j2 elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? policy))) (|t|) ?) Hj)
1580        [ #j1 normalize nodelta
1581         cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)
1582         #x1 #x2
1583         cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,None ?〉)
1584         #y1 #y2 normalize nodelta #Hx #Hy >Hx >Hy normalize nodelta
1585         #Hblerp cases (proj2 ?? Hblerp) cases j1 cases j2
1586         [1,4,5,7,8,9: #H cases H
1587         |2,3,6: #_ normalize nodelta
1588           [1,2: @(transitive_le ? (measure_int t x acc))
1589           |3: @(transitive_le ? (measure_int t x (acc+1)))
1590           ]
1591           [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/]
1592           >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
1593         |11,12,13,15,16,17: #H destruct (H)
1594         |10,14,18: normalize nodelta #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
1595         ]
1596       | @(transitive_le … Hp) @le_n
1597       ]
1598     | @(transitive_le … Hp) @le_n
1599     ]
1600   | #Hnj   
1601     lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) (pi1 ?? policy) (|t|) ?) Hnj)
1602     [3: lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) x (|t|) ?) Hnj)
1603       [3: cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)
1604          #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,None ?〉)
1605          #y1 #y2 #Hy #Hx >Hx >Hy normalize nodelta
1606          #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
1607       |1: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx))))))
1608       |2: @(transitive_le … Hp) @le_n
1609       ]
1610     |1: @(proj1 ?? (proj1 ?? (pi2 ?? policy)))
1611     |2: @(transitive_le … Hp) @le_n
1612     ]
1613   ]
1614 ]
1615qed.
1616
1617(* these lemmas seem superfluous, but not sure how *)
1618lemma bla: ∀a,b:ℕ.a + a = b + b → a = b.
1619 #a elim a
1620 [ normalize #b //
1621 | -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ | -b #b normalize
1622   <plus_n_Sm <plus_n_Sm #H
1623   >(Hind b (injective_S ?? (injective_S ?? H))) // ]
1624 ]
1625qed.
1626
1627lemma sth_not_s: ∀x.x ≠ S x.
1628 #x cases x
1629 [ // | #y // ]
1630qed.
1631 
1632lemma measure_full: ∀program.∀policy.
1633  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
1634  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,None ?〉)) = None ? ∨
1635  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,None ?〉)) = Some ? long_jump.
1636#program #policy elim program
1637[ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1638| #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
1639  [ whd in match (measure_int ???) in Hm;
1640    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)) in Hm;
1641    normalize nodelta
1642    [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
1643    | #j cases j normalize nodelta
1644      [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
1645      | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
1646        <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize
1647        >(commutative_plus (|t|) 0) <plus_O_n <minus_n_O
1648        >plus_n_Sm @le_n
1649      | >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) //
1650      ]
1651    ]
1652  | #Hmt cases (le_to_or_lt_eq … Hi) -Hi;
1653  [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
1654  | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
1655    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)) in Hm;
1656    normalize nodelta
1657    [ #_ %1 @refl
1658    | #j cases j normalize nodelta
1659      [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
1660        >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s
1661      | >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize
1662        #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s
1663      | #_ %2 @refl
1664      ]
1665    ]
1666  ]]
1667]
1668qed.
1669
1670lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
1671  ∀policy:Σp:ppc_pc_map.
1672    out_of_program_none program p ∧ jump_in_policy program p ∧ policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16.
1673  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
1674  [ None ⇒ True
1675  | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_equal program policy p ].
1676#program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program) policy)))
1677cases (jump_expansion_step program (create_label_map program) policy) in ⊢ (???% → %);
1678#p cases p -p #ch #pol normalize nodelta cases pol
1679[ / by I/
1680| #p normalize nodelta #Hpol #eqpol lapply (le_n (|program|))
1681  @(list_ind ?  (λx.|x| ≤ |pi1 ?? program| →
1682      measure_int x policy 0 = measure_int x p 0 →
1683      policy_equal x policy p) ?? (pi1 ?? program))
1684 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
1685 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
1686   [ #Hi @Hind
1687     [ @(transitive_le … Hp) / by /
1688     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
1689       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) Hp) #Hinc
1690       cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉))
1691       [ #Hj elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (|t|) ?) Hj)
1692         [ #j2 elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? policy))) (|t|) ?) Hj)
1693           [ #j1 normalize nodelta
1694             cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,None ?〉) in Hm Hinc; #x1 #x2
1695             cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,None ?〉); #y1 #y2
1696             #Hm #Hinc #Hx #Hy lapply Hm -Hm; lapply Hinc -Hinc; >Hx >Hy normalize nodelta
1697             cases j1 cases j2 normalize nodelta
1698             [1: / by /
1699             |2,3: >measure_plus #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
1700               lapply (measure_incr_or_equal program policy t ? 0)
1701               [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
1702             |4,7,8: #H elim (proj2 ?? H) #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ]
1703             |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
1704               #_ #H @(injective_plus_r … H)
1705             |6: >measure_plus >measure_plus
1706               change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
1707               #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
1708               lapply (measure_incr_or_equal program policy t ? 0)
1709               [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
1710             |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
1711               #_ #H @(injective_plus_r … H)
1712             ]
1713           | @(transitive_le … Hp) @le_n
1714           ]
1715         | @(transitive_le … Hp) @le_n
1716         ]
1717       | #Hnj lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) (pi1 ?? policy) (|t|) ?) Hnj)
1718         [3: lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) p (|t|) ?) Hnj)
1719           [3: cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉) in Hm Hinc;
1720               #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd p) 〈0,None ?〉)
1721               #y1 #y2 #Hm #Hinc #Hy #Hx lapply Hm -Hm; lapply Hinc -Hinc; >Hx >Hy normalize nodelta
1722               #_ / by /
1723           |1: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))))))
1724           |2: @(transitive_le … Hp) @le_n
1725           ]
1726        |1: @(proj1 ?? (proj1 ?? (pi2 ?? policy)))
1727        |2: @(transitive_le … Hp) @le_n
1728        ]
1729      ]
1730      | @(le_S_S_to_le … Hi)
1731     ]
1732   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
1733     whd in match (measure_int ? p ?) in Hm;
1734     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) Hp)
1735     (* XXX *) cases daemon
1736     (* change proof for not_jump
1737     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in   
1738Hm;
1739     #x cases x -x #x1 #x2 #x3
1740     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
1741     #y cases y -y #y1 #y2 #y3
1742     normalize nodelta cases x3 cases y3 normalize nodelta
1743     [1,5,9: #_ #_ //
1744     |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
1745     |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
1746       lapply (measure_incr_or_equal program policy t ? 0)
1747       [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
1748     |6: >measure_plus >measure_plus
1749        change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
1750        #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
1751        lapply (measure_incr_or_equal program policy t ? 0)
1752        [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
1753     ] *)
1754   ]
1755 ]
1756qed.
1757
1758lemma le_to_eq_plus: ∀n,z.
1759  n ≤ z → ∃k.z = n + k.
1760 #n #z elim z
1761 [ #H cases (le_to_or_lt_eq … H)
1762   [ #H2 @⊥ @(absurd … H2) @not_le_Sn_O
1763   | #H2 @(ex_intro … 0) >H2 //
1764   ]
1765 | #z' #Hind #H cases (le_to_or_lt_eq … H)
1766   [ #H' elim (Hind (le_S_S_to_le … H')) #k' #H2 @(ex_intro … (S k'))
1767     >H2 >plus_n_Sm //
1768   | #H' @(ex_intro … 0) >H' //
1769   ]
1770 ]
1771qed.
1772
1773lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
1774  |l| ≤ |program| → measure_int l (jump_expansion_start program (create_label_map program)) 0 = 0.
1775 #l #program elim l
1776 [ //
1777 | #h #t #Hind #Hp cases daemon
1778 
1779 (* old proof whd in match (measure_int ???);
1780   cases daemo
1781   cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
1782   [ lapply
1783       (proj1 ?? (pi2 ??
1784          (jump_expansion_start program (create_label_map program))))) 〈0,None ?〉)
1785     [ normalize nodelta @Hind @le_S_to_le ]
1786     @Hp
1787   | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (pi1 ?? (jump_expansion_start program)) (|t|) ?) Hj) 〈0,0,short_jump〉)
1788     [ normalize nodelta @Hind @le_S_to_le @Hp
1789     | @Hp
1790     | %
1791       [ @(proj1 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program))))
1792       | @(proj2 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program))))
1793       ]
1794     ]
1795   ]*)
1796 ]
1797qed.
1798
1799(* the actual computation of the fixpoint *)
1800definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
1801  Σp:option ppc_pc_map.∃n.∀k.n < k →
1802    policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program k))) p.
1803#program @(\snd (pi1 ?? (jump_expansion_internal program (2*|program|))))
1804
1805cases daemon
1806
1807(* old proof
1808cases (dec_bounded_exists (λk.policy_equal (pi1 ?? program)
1809   (\snd (pi1 ?? (jump_expansion_internal program k)))
1810   (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|))
1811 cases daemon
1812[ #Hex elim Hex -Hex #x #Hx @(ex_intro … x) #k #Hk
1813  @pe_trans
1814  [ @(\snd (pi1 ?? (jump_expansion_internal program x)))
1815  | @pe_sym @equal_remains_equal
1816    [ @(proj2 ?? Hx)
1817    | @le_S_S_to_le @le_S @Hk
1818    ]
1819  | @equal_remains_equal
1820    [ @(proj2 ?? Hx)
1821    | @le_S_S_to_le @le_S @(proj1 ?? Hx)
1822    ]   
1823  ]
1824| #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @(ex_intro … (2*|program|)) #k #Hk
1825  @pe_sym @equal_remains_equal
1826  [ lapply (refl ? (jump_expansion_internal program (2*|program|)))
1827    cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
1828    #x cases x -x #Fch #Fpol normalize nodelta #HFpol cases Fpol in HFpol; normalize nodelta
1829    [ (* if we're at None in 2*|program|, we're at None in S 2*|program| too *)
1830      #HFpol #EQ whd in match (jump_expansion_internal ??); >EQ
1831      normalize nodelta / by /
1832    | #Fp #HFp #EQ whd in match (jump_expansion_internal ??);
1833      >EQ normalize nodelta
1834      lapply (refl ? (jump_expansion_step program (create_label_map program Fp) «Fp,?»))
1835      [ @HFp
1836      | lapply (measure_full program Fp ?)
1837        [ @le_to_le_to_eq
1838          [ @measure_le
1839          | cut (∀x:ℕ.x ≤ 2*|program| →
1840             ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧       
1841                x ≤ measure_int program p 0))
1842            [ #x elim x
1843              [ #Hx @(ex_intro ?? (jump_expansion_start program)) @conj
1844                [ whd in match (jump_expansion_internal ??); @refl
1845                | @le_O_n
1846                ]
1847              | -x #x #Hind #Hx
1848                lapply (refl ? (jump_expansion_internal program (S x)))
1849                cases (jump_expansion_internal program (S x)) in ⊢ (???% → %);
1850                #z cases z -z #Sxch #Sxpol cases Sxpol -Sxpol normalize nodelta
1851                [ #H #HeqSxpol @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk
1852                  @(absurd … (step_none program (S x) ? k))
1853                  [ >HeqSxpol / by /
1854                  | <Hk >EQ @nmk #H destruct (H)
1855                  ]
1856                | #Sxpol #HSxpol #HeqSxpol @(ex_intro ?? Sxpol) @conj
1857                  [ @refl
1858                  | elim (Hind (transitive_le … (le_n_Sn x) Hx))
1859                    #xpol #Hxpol @(le_to_lt_to_lt … (proj2 ?? Hxpol))
1860                    lapply (measure_incr_or_equal program xpol program (le_n (|program|)) 0)
1861                    [ cases (jump_expansion_internal program x) in Hxpol;
1862                      #z cases z -z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H;
1863                      normalize nodelta / by /
1864                    | lapply (Hfa x Hx) lapply HeqSxpol -HeqSxpol
1865                      whd in match (jump_expansion_internal program (S x));
1866                      lapply (refl ? (jump_expansion_internal program x))
1867                      lapply Hxpol -Hxpol cases (jump_expansion_internal program x) in ⊢ (% → ???% → %);
1868                      #z cases z -z #xch #b normalize nodelta #H #Heq >(proj1 ?? Heq) in H;
1869                      #H #Heq cases xch in Heq; #Heq normalize nodelta
1870                      [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program) xpol) «xpol,H»))
1871                        cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
1872                        normalize nodelta cases c normalize nodelta
1873                        [ #H1 #Heq #H2 destruct (H2)
1874                        | #d #H1 #Heq #H2 destruct (H2) #Hfull #H2 elim (le_to_or_lt_eq … H2)
1875                          [ / by /
1876                          | #H3 lapply (measure_special program «xpol,H») >Heq
1877                            normalize nodelta #H4 @⊥
1878                            @(absurd … (H4 H3))
1879                            @Hfull
1880                          ]
1881                        ]
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 #H3 #_ @⊥ @(absurd ?? H3) @pe_refl
1886                        | #d #H1 #Heq #H2 #H3 @⊥ @(absurd ?? H3) @pe_refl
1887                        ]
1888                      ]
1889                    ]
1890                  ]
1891                ]
1892              ]
1893            | #H elim (H (2*|program|) (le_n ?)) #plp >EQ #Hplp
1894              >(Some_eq ??? (proj1 ?? Hplp)) @(proj2 ?? Hplp)
1895            ]
1896          ]
1897        | #Hfull cases (jump_expansion_step program (create_label_map program Fp) «Fp,?») in ⊢ (???% → %);
1898          #x cases x -x #Gch #Gpol cases Gpol normalize nodelta
1899          [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull
1900          | #Gp #HGp #EQ2 cases Fch
1901            [ normalize nodelta #i #Hi
1902              lapply (refl ? (lookup ?? (bitvector_of_nat 16 i) (\snd Fp) 〈0,0,short_jump〉))
1903              cases (lookup ?? (bitvector_of_nat 16 i) (\snd Fp) 〈0,0,short_jump〉) in ⊢ (???% → %);
1904              #x cases x -x #p #a #j normalize nodelta #H
1905              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi) lapply (Hfull i Hi) >H
1906              #H2 >H2 normalize nodelta cases (lookup ?? (bitvector_of_nat 16 i) (\snd Gp) 〈0,0,short_jump〉)
1907              #x cases x -x #p #a #j' cases j' normalize nodelta #H elim H -H #H
1908              [1,3: @⊥ @H
1909              |2,4: destruct (H)
1910              |5,6: @refl
1911              ]
1912            | normalize nodelta /2 by pe_int_refl/
1913            ]
1914          ]
1915        ]
1916      ]
1917    ]
1918  | @le_S_S_to_le @le_S @Hk
1919  ]
1920| #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
1921  #x cases x -x #nch #npol normalize nodelta #Hnpol
1922  #x cases x -x #Sch #Spol normalize nodelta #HSpol
1923  cases npol in Hnpol; cases Spol in HSpol;
1924  [ #Hnpol #HSpol %1 //
1925  |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal ???); //
1926    #H destruct (H)
1927  |4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); @dec_bounded_forall #m
1928      cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉)
1929      #x cases x -x #x1 #x2 #x3
1930      cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉)
1931      #y cases y -y #y1 #y2 #y3 normalize nodelta
1932      @dec_eq_jump_length 
1933  ]
1934] *)
1935qed.
1936
1937(* The glue between Policy and Assembly. *)
1938definition jump_expansion':
1939 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
1940 ℕ → ℕ × (option jump_length) ≝
1941 λprogram.λppc:ℕ.
1942  let policy ≝ pi1 … (je_fixpoint (\snd program)) in
1943  match policy with
1944  [ None ⇒ 〈0, Some ? long_jump〉
1945  | Some x ⇒ bvt_lookup ?? (bitvector_of_nat 16 ppc) (\snd x) 〈0,Some ? long_jump〉
1946  ].
Note: See TracBrowser for help on using the repository browser.