source: src/ASM/Policy.ma @ 1937

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