source: src/ASM/Policy.ma @ 1965

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