source: src/ASM/Policy.ma @ 2018

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

CJNE case a complete mess.

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