source: src/ASM/Policy.ma @ 1942

Last change on this file since 1942 was 1942, checked in by mulligan, 8 years ago

Work on showing the equivalence of two methods of looking up from the maps.

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