source: src/ASM/Policy.ma @ 1691

Last change on this file since 1691 was 1615, checked in by sacerdot, 8 years ago

Policy now depends on Assembly and not the other way around.

File size: 47.1 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Status.ma".
5include alias "basics/logic.ma".
6include alias "arithmetics/nat.ma".
7include "utilities/extralib.ma".
8include "ASM/Assembly.ma".
9
10definition max_length: jump_length → jump_length → jump_length ≝
11  λj1.λj2.
12  match j1 with
13  [ long_jump   ⇒ long_jump
14  | medium_jump ⇒
15    match j2 with
16    [ long_jump ⇒ long_jump
17    | _         ⇒ medium_jump
18    ]
19  | short_jump  ⇒ j2
20  ].
21
22definition jmple: jump_length → jump_length → Prop ≝
23  λj1.λj2.
24  match j1 with
25  [ short_jump  ⇒
26    match j2 with
27    [ short_jump ⇒ False
28    | _          ⇒ True
29    ]
30  | medium_jump ⇒
31    match j2 with
32    [ long_jump ⇒ True
33    | _         ⇒ False
34    ]
35  | long_jump   ⇒ False
36  ].
37
38definition jmpleq: jump_length → jump_length → Prop ≝
39  λj1.λj2.jmple j1 j2 ∨ j1 = j2.
40 
41lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y).
42 #x #y cases x cases y /3 by inl, inr, nmk, I/
43qed.
44 
45lemma jmpleq_max_length: ∀ol,nl.
46  jmpleq ol (max_length ol nl).
47 #ol #nl cases ol cases nl
48 /2 by or_introl, or_intror, I/
49qed.
50
51lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b).
52  #a #b cases a cases b /2/
53  %2 @nmk #H destruct (H)
54qed.
55
56 
57(* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *)
58definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16.
59
60(* label_map: identifier ↦ 〈instruction number, address〉 *)
61definition label_map ≝ identifier_map ASMTag (nat × nat).
62
63definition is_label ≝
64  λx:labelled_instruction.λl:Identifier.
65  let 〈lbl,instr〉 ≝ x in
66  match lbl with
67  [ Some l' ⇒ l' = l
68  | _       ⇒ False
69  ].
70
71definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
72  λpc.λjmp_len.λinstr.
73  let bv_pc ≝ bitvector_of_nat 16 pc in
74  let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_pc jmp_len instr in
75  let bv: list (BitVector 8) ≝ match ilist with
76    [ None   ⇒ (* this shouldn't happen *) [ ]
77    | Some l ⇒ flatten … (map … assembly1 l)
78    ] in
79  pc + (|bv|).
80
81lemma label_does_not_occur:
82  ∀i,p,l.
83  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false.
84 #i #p #l generalize in match i; elim p
85 [ #i >nth_nil #H @⊥ @H
86 | #h #t #IH #i cases i -i
87   [ cases h #hi #hp cases hi
88     [ normalize #H @⊥ @H
89     | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ??);
90       whd in Heq; >Heq
91       >eq_identifier_refl //
92     ]
93   | #i #H whd in match (does_not_occur ??);
94     whd in match (instruction_matches_identifier ??);
95     cases h #hi #hp cases hi normalize nodelta
96     [ @(IH i) @H
97     | #l' @eq_identifier_elim
98       [ normalize //
99       | normalize #_ @(IH i) @H
100       ]
101     ]
102   ]
103 ]
104qed. 
105
106definition create_label_map: ∀program:list labelled_instruction.
107  ∀policy:jump_expansion_policy.
108  (Σlabels:label_map.
109    ∀i:ℕ.lt i (|program|) →
110    ∀l.occurs_exactly_once l program →
111    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
112    ∃a.lookup … labels l = Some ? 〈i,a〉
113  ) ≝
114  λprogram.λpolicy.
115  let 〈final_pc, final_labels〉 ≝
116    foldl_strong (option Identifier × pseudo_instruction)
117    (λprefix.ℕ × (Σlabels.
118      ∀i:ℕ.lt i (|prefix|) →
119      ∀l.occurs_exactly_once l prefix →
120      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
121      ∃a.lookup … labels l = Some ? 〈i,a〉)
122    )
123    program
124    (λprefix.λx.λtl.λprf.λacc.
125     let 〈pc,labels〉 ≝ acc in
126     let 〈label,instr〉 ≝ x in
127       let new_labels ≝
128       match label with
129       [ None   ⇒ labels
130       | Some l ⇒ add … labels l 〈|prefix|, pc〉
131       ] in
132     let 〈i1,i2,jmp_len〉 ≝ bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈0, 0, long_jump〉 in
133       〈add_instruction_size pc jmp_len instr, new_labels〉
134    ) 〈0, empty_map …〉 in
135    final_labels.
136[ #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
137  [ #Hi #l normalize nodelta; cases label normalize nodelta
138    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
139      lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
140      % [ @addr | @Haddr ]
141    | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc;
142      @eq_identifier_elim #Heq #Hocc
143      [ normalize in Hocc;
144        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
145        @⊥ @(absurd … Hocc)
146      | normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
147        [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ]
148        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
149        ]
150      ]
151      >(label_does_not_occur i … Hl) normalize nodelta @nmk //
152    ]
153  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
154    [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
155      [ normalize nodelta #H @⊥ @H
156      | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_add_hit ]
157      ]
158    | @le_n
159    ]
160  ]
161| #i #Hi #l #Hl @⊥ @Hl
162]
163qed.
164
165definition select_reljump_length: label_map → ℕ → Identifier → ℕ ×jump_length ≝
166  λlabels.λpc.λlbl.
167  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
168  if leb pc addr (* forward jump *)
169  then if leb (addr - pc) 126
170       then 〈addr, short_jump〉
171       else 〈addr, long_jump〉
172  else if leb (pc - addr) 129
173       then 〈addr, short_jump〉
174       else 〈addr, long_jump〉.
175
176definition select_call_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
177  λlabels.λpc_nat.λlbl.
178  let pc ≝ bitvector_of_nat 16 pc_nat in
179  let addr_nat ≝ (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
180  let addr ≝ bitvector_of_nat 16 addr_nat in
181  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
182  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
183  if eq_bv ? fst_5_addr fst_5_pc
184  then 〈addr_nat, medium_jump〉
185  else 〈addr_nat, long_jump〉.
186 
187definition select_jump_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
188  λlabels.λpc.λlbl.
189  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
190  if leb pc addr
191  then if leb (addr - pc) 126
192       then 〈addr, short_jump〉
193       else select_call_length labels pc lbl
194  else if leb (pc - addr) 129
195       then 〈addr, short_jump〉
196       else select_call_length labels pc lbl.
197 
198definition jump_expansion_step_instruction: label_map → ℕ →
199  preinstruction Identifier → option (ℕ × jump_length) ≝
200  λlabels.λpc.λi.
201  match i with
202  [ JC j     ⇒ Some ? (select_reljump_length labels pc j)
203  | JNC j    ⇒ Some ? (select_reljump_length labels pc j)
204  | JZ j     ⇒ Some ? (select_reljump_length labels pc j)
205  | JNZ j    ⇒ Some ? (select_reljump_length labels pc j)
206  | JB _ j   ⇒ Some ? (select_reljump_length labels pc j)
207  | JBC _ j  ⇒ Some ? (select_reljump_length labels pc j)
208  | JNB _ j  ⇒ Some ? (select_reljump_length labels pc j)
209  | CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
210  | DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
211  | _        ⇒ None ?
212  ].
213
214definition is_jump' ≝
215  λx:preinstruction Identifier.
216  match x with
217  [ JC _ ⇒ True
218  | JNC _ ⇒ True
219  | JZ _ ⇒ True
220  | JNZ _ ⇒ True
221  | JB _ _ ⇒ True
222  | JNB _ _ ⇒ True
223  | JBC _ _ ⇒ True
224  | CJNE _ _ ⇒ True
225  | DJNZ _ _ ⇒ True
226  | _ ⇒ False
227  ].
228 
229definition is_jump ≝
230  λx:labelled_instruction.
231  let 〈label,instr〉 ≝ x in
232  match instr with
233  [ Instruction i   ⇒ is_jump' i
234  | Call _ ⇒ True
235  | Jmp _ ⇒ True
236  | _ ⇒ False
237  ].
238
239lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x).
240#x cases x #l #i cases i
241[#id cases id
242 [1,2,3,6,7,33,34:
243  #x #y %2 whd in match (is_jump ?); /2 by nmk/
244 |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
245  #x %2 whd in match (is_jump ?); /2 by nmk/
246 |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
247 |9,10,14,15: #x %1 //
248 |11,12,13,16,17: #x #y %1 //
249 ]
250|2,3: #x %2 /2 by nmk/
251|4,5: #x %1 //
252|6: #x #y %2 /2 by nmk/
253]
254qed.
255 
256
257definition jump_in_policy ≝
258  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
259  ∀i:ℕ.i < |prefix| →
260  (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
261   ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉).
262
263(* these should be moved to BitVector at some point *) 
264lemma bitvector_of_nat_ok:
265  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
266 #n elim n -n
267 [ #x #y #Hx #Hy #Heq <(le_n_O_to_eq ? (le_S_S_to_le ?? Hx)) <(le_n_O_to_eq ? (le_S_S_to_le ?? Hy)) @refl
268 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
269 ]
270qed.
271
272lemma bitvector_of_nat_abs:
273  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
274 #n #x #y #Hx #Hy #Heq @notb_elim
275 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
276 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
277 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H //
278 | #H //
279 ]
280qed.
281
282lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
283 ∀policy:(Σp:jump_expansion_policy.
284 (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
285 jump_in_policy prefix p).
286  ∀i:ℕ.i < |prefix| →
287  iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))
288  (lookup_opt … (bitvector_of_nat 16 i) policy = None ?).
289 #prefix #policy #i #Hi @conj
290 [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy))
291   cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);
292   [ #H @H
293   | #x cases x -x #x #z cases x -x #x #y #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
294     @(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H)))
295   ]
296 | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
297   #H elim H -H; #x #H elim H -H; #y #H elim H -H; #z #H >H in Hnone; #abs destruct (abs)
298 ] 
299qed.
300
301definition jump_expansion_start:
302  ∀program:(Σl:list labelled_instruction.|l| < 2^16).
303  Σpolicy:jump_expansion_policy.
304    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
305    jump_in_policy program policy ∧
306    ∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
307     lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉 ≝
308  λprogram.
309  foldl_strong (option Identifier × pseudo_instruction)
310  (λprefix.Σpolicy:jump_expansion_policy.
311    (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
312    jump_in_policy prefix policy ∧
313    ∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
314      lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉)
315  program
316  (λprefix.λx.λtl.λprf.λpolicy.
317   let 〈label,instr〉 ≝ x in
318   match instr with
319   [ Instruction i ⇒ match i with
320     [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
321     | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
322     | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
323     | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
324     | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
325     | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
326     | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
327     | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
328     | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
329     | _ ⇒ (pi1 … policy)
330     ]
331   | Call c ⇒ bvt_insert (ℕ×ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
332   | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
333   | _      ⇒ (pi1 ?? policy)
334   ]
335  ) (Stub ? ?).
336[1,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,35,36,37,38,39,40,41,42:
337 @conj
338 [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,57,59,61:
339  @conj
340  #i >append_length <commutative_plus #Hi normalize in Hi;
341  [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,57,59,61:
342   #Hi2 cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i)
343   [1,5,9,13,17,21,25,29,33,37,41,45,49,53,57,61,65,69,73,77,81,85,89,93,97,101,105,109,113,117,121:
344     @le_S_to_le @le_S_to_le @Hi
345   |2,6,10,14,18,22,26,30,34,38,42,46,50,54,58,62,66,70,74,78,82,86,90,94,98,102,106,110,114,118,122:
346     @Hi2
347   |3,7,11,15,19,23,27,31,35,39,43,47,51,55,59,63,67,71,75,79,83,87,91,95,99,103,107,111,115,119,123:
348     <Hi @le_n_Sn
349   |4,8,12,16,20,24,28,32,36,40,44,48,52,56,60,64,68,72,76,80,84,88,92,96,100,104,108,112,116,120,124:
350     @Hi2
351   ]
352  ]
353  cases (le_to_or_lt_eq … Hi) -Hi; #Hi
354  [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,57,59,61:
355    >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi))
356    @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
357  ]
358  @conj >(injective_S … Hi)
359   [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,57,59,61:
360    >(nth_append_second ? ? prefix ? ? (le_n (|prefix|))) <minus_n_n #H @⊥ @H
361   ]
362   #H elim H; -H; #t1 #H elim H; -H #t2 #H elim H; -H; #t3 #H
363   >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H;
364   [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,57,59,61:
365     #H destruct (H)
366   ]
367   @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
368   @le_plus_n_r
369 ]
370 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
371 -Hi; #Hi
372 [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,57,59,61:
373  #Hj @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi))
374  >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; //
375 ]
376 >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n
377 #H @⊥ @H
378|2,3,26,27,28,29,30,31,32,33,34: @conj
379 [1,3,5,7,9,11,13,15,17,19,21: @conj
380  [1,3,5,7,9,11,13,15,17,19,21:
381    #i >append_length <commutative_plus #Hi #Hi2 normalize in Hi; >lookup_opt_insert_miss
382   [1,3,5,7,9,11,13,15,17,19,21:
383     @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
384   ]
385   >eq_bv_sym @bitvector_of_nat_abs
386   [1,4,7,10,13,16,19,22,25,28,31:
387     @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
388     @le_plus_n_r
389   |2,5,8,11,14,17,20,23,26,29,32: @Hi2
390   |3,6,9,12,15,18,21,24,27,30,33: @lt_to_not_eq @Hi
391   ]
392  ]
393  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
394  -Hi #Hi
395  [1,3,5,7,9,11,13,15,17,19,21:
396   >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) >lookup_opt_insert_miss
397   [1,3,5,7,9,11,13,15,17,19,21:
398    @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
399   ]
400   @bitvector_of_nat_abs
401   [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
402   |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
403   ]
404   @(transitive_lt … (pi2 ?? program))
405   >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
406  ]
407  @conj >(injective_S … Hi) #H
408  [2,4,6,8,10,12,14,16,18,20,22:
409   >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n //
410  ]
411  @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy))))
412 ]
413 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
414  -Hi #Hi
415 [1,3,5,7,9,11,13,15,17,19,21:
416  >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #Hj >lookup_opt_insert_miss
417  [1,3,5,7,9,11,13,15,17,19,21:
418   @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi) Hj)
419  ]
420  @bitvector_of_nat_abs
421  [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
422  |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
423  ]
424  @(transitive_lt … (pi2 ?? program))
425  >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
426 ]
427 #_ >(injective_S … Hi) @lookup_opt_insert_hit
428|@conj
429 [@conj
430  [ #i #Hi //
431  | whd #i #Hi @⊥ @(absurd (i < 0) Hi (not_le_Sn_O ?))
432  ]
433 | #i #Hi >nth_nil #Hj @⊥ @Hj
434]
435qed.
436
437definition policy_increase: list labelled_instruction → jump_expansion_policy →
438  jump_expansion_policy → Prop ≝
439 λprogram.λop.λp.
440  (∀i:ℕ.i < |program| →
441    let 〈i1,i2,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) op 〈0,0,short_jump〉 in
442    let 〈i3,i4,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) p 〈0,0,short_jump〉 in
443    jmpleq oj j).
444
445definition policy_safe: (*label_map → *)jump_expansion_policy → Prop ≝
446 (*λlabels.*)λpolicy.
447 bvt_forall (ℕ×ℕ×jump_length) 16 policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in
448    match jmp_len with
449    [ short_jump  ⇒ if leb pc_nat addr_nat
450       then le (addr_nat - pc_nat) 126
451       else le (pc_nat - addr_nat) 129
452    | medium_jump ⇒
453       let addr ≝ bitvector_of_nat 16 addr_nat in
454       let pc ≝ bitvector_of_nat 16 pc_nat in
455       let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in
456       let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in
457       eq_bv 5 fst_5_addr fst_5_pc = true
458    | long_jump   ⇒ True
459    ]
460  ).
461 
462definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
463  ∀labels:(Σlm:label_map.∀i:ℕ.lt i (|program|) →
464    ∀l.occurs_exactly_once l program →
465    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
466    ∃a.lookup … lm l = Some ? 〈i,a〉).
467  ∀old_policy:(Σpolicy.
468    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
469    jump_in_policy program policy).
470  (Σpolicy.
471    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
472    jump_in_policy program policy ∧
473    policy_increase program old_policy policy)
474    ≝
475  λprogram.λlabels.λold_policy.
476  let 〈final_pc, final_policy〉 ≝
477    foldl_strong (option Identifier × pseudo_instruction)
478    (λprefix.ℕ × Σpolicy.
479      (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
480      jump_in_policy prefix policy ∧
481      policy_increase prefix old_policy policy
482    )
483    program
484    (λprefix.λx.λtl.λprf.λacc.
485      let 〈pc, policy〉 ≝ acc in
486      let 〈label,instr〉 ≝ x in
487      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_policy in
488      let add_instr ≝
489        match instr with
490        [ Instruction i ⇒ jump_expansion_step_instruction labels pc i
491        | Call c        ⇒ Some ? (select_call_length labels pc c)
492        | Jmp j         ⇒ Some ? (select_jump_length labels pc j)
493        | _             ⇒ None ?
494        ] in
495      let 〈new_pc, new_policy〉 ≝
496        let 〈ignore,old_length〉 ≝ bvt_lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, 0, short_jump〉 in
497        match add_instr with
498        [ None    ⇒ (* i.e. it's not a jump *)
499          〈add_instruction_size pc long_jump instr, policy〉
500        | Some z ⇒ let 〈addr,ai〉 ≝ z in
501          let new_length ≝ max_length old_length ai in
502          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, addr, new_length〉 policy〉
503        ] in
504      〈new_pc, new_policy〉
505    ) 〈0, Stub ? ?〉 in
506    final_policy.
507[ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
508[ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr
509  [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
510  | #z cases z -z #z1 #z2 whd in match (snd ???); >lookup_opt_insert_miss
511    [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
512    | >eq_bv_sym @bitvector_of_nat_abs
513      [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
514        @le_S_S @le_plus_n_r
515      | @Hi2
516      | @lt_to_not_eq @Hi
517      ]
518    ]
519  ]
520| cases (le_to_or_lt_eq … Hi) -Hi;
521  [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) @conj
522    [ #Hj lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
523      cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y
524      [ @(proj1 ?? Hacc Hj)
525      | #z cases z -z #z1 #z2 elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj
526        @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???);
527        >lookup_opt_insert_miss [ @Hj |  @bitvector_of_nat_abs ]
528        [3: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
529        |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
530        ]
531        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
532        @le_S_S @le_plus_n_r
533      ]
534    | lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
535      #H elim H -H; #h #H elim H -H; #n #H elim H -H #j cases add_instr cases (lookup ??? old_policy ?)
536      normalize nodelta #x #y [2: #z]
537      #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))
538      [ <Hl @sym_eq cases z #z1 #z2 whd in match (snd ???); @lookup_opt_insert_miss @bitvector_of_nat_abs
539        [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
540        |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
541        ]
542        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
543        @le_S_S @le_plus_n_r
544      | @Hl
545      ]
546    ]
547  | #Hi >(injective_S … Hi) >(nth_append_second ? ? prefix ? ? (le_n (|prefix|)))
548     <minus_n_n whd in match (nth ????); whd in match (add_instr); cases instr
549     [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] @conj normalize nodelta
550     [3,5,11: #H @⊥ @H (* instr is not a jump *)
551     |4,6,12: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
552       #x #y normalize nodelta >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
553       [1,3,5: #H destruct (H)]
554       @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
555       @le_S_S @le_plus_n_r
556     |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
557       whd in match (snd ???); @(ex_intro ?? pc)
558       [ @(ex_intro ?? (\fst (select_jump_length labels pc id)))
559         @(ex_intro ?? (max_length j (\snd (select_jump_length labels pc id))))
560         cases (select_jump_length labels pc id)
561       | @(ex_intro ?? (\fst (select_call_length labels pc id)))
562         @(ex_intro ?? (max_length j (\snd (select_call_length labels pc id))))
563         cases (select_call_length labels pc id)
564       ] #z1 #z2 normalize nodelta @lookup_opt_insert_hit
565     |8,10: #_ //
566     |1,2: cases pi
567       [35,36,37: #H @⊥ @H
568       |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H @⊥ @H
569       |1,2,3,6,7,33,34: #x #y #H @⊥ @H
570       |9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
571         whd in match (snd ???); @(ex_intro ?? pc)
572         @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
573         @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
574         normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
575         @lookup_opt_insert_hit
576       |11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
577         whd in match (snd ???); @(ex_intro ?? pc)
578         @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
579         @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
580         normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
581         @lookup_opt_insert_hit
582       |72,73,74: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
583        #z cases z -z #x #y #z normalize nodelta
584        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
585        [1,3,5: #H destruct (H)]
586        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
587        @le_S_S @le_plus_n_r     
588       |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x
589        #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
590        #z cases z -z #x #y #z normalize nodelta
591        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
592        [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)]
593        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
594        @le_S_S @le_plus_n_r
595       |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n #H elim H -H #j
596        cases (lookup ??? old_policy ?) #z cases z -z #x #y #z normalize nodelta
597        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
598        [1,3,5,7,9,11,13: #H destruct (H)]
599        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
600        @le_S_S @le_plus_n_r             
601       |46,47,51,52: #id #_ //
602       |48,49,50,53,54: #x #id #_ //
603       ]
604     ]
605   ]
606  ]
607| lapply (refl ? add_instr) cases add_instr in ⊢ (???% → %);
608  [ #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
609    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
610    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
611      #x #y @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
612    | normalize nodelta >(injective_S … Hi)
613      >lookup_opt_lookup_miss
614      [ >lookup_opt_lookup_miss
615        [ //
616        | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
617          #x #y normalize nodelta
618          >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
619          [ //
620          | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
621            @le_S_S @le_plus_n_r
622          ]
623        ]
624      | >(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?))
625        [ //
626        | >prf >p1 >nth_append_second [ <minus_n_n
627        generalize in match Ha; normalize nodelta cases instr normalize nodelta
628        [1: #pi cases pi
629         [1,2,3,6,7,33,34: #x #y #H normalize /2 by nmk/
630         |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize /2 by nmk/
631         |35,36,37: #H normalize /2 by nmk/
632         |9,10,14,15: #id whd in match (jump_expansion_step_instruction ???);
633           #H destruct (H)
634         |11,12,13,16,17: #x #id whd in match (jump_expansion_step_instruction ???);
635           #H destruct (H)
636         ]
637        |2,3: #x #H normalize /2 by nmk/
638        |6: #x #y #H normalize /2 by nmk/
639        |4,5: #id #H destruct (H)
640        ] | @le_n ]
641        | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
642        ]
643      ]
644    ]
645  | #x cases x -x #x1 #x2 #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
646    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
647    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
648      #y cases y -y #y1 #y2 #z whd in match (snd ???); normalize nodelta >lookup_insert_miss
649      [ @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
650      | @bitvector_of_nat_abs
651        [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
652        |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
653        ]
654        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
655        @le_S_S @le_plus_n_r
656      ]
657    | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (pi2 ?? old_policy) (|prefix|) ?) ?)
658      [ #a #H elim H -H; #b #H elim H -H #c #H >H >(lookup_opt_lookup_hit … 〈a,b,c〉 H)
659        normalize nodelta >lookup_insert_hit @jmpleq_max_length
660      | >prf >p1 >nth_append_second
661        [ <minus_n_n generalize in match Ha; normalize nodelta cases instr normalize nodelta
662          [1: #pi cases pi
663           [1,2,3,6,7,33,34: #x #y #H normalize in H; destruct (H)
664           |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize in H; destruct (H)
665           |35,36,37: #H normalize in H; destruct (H)
666           |9,10,14,15: #id #H //
667           |11,12,13,16,17: #x #id #H //
668           ]
669          |2,3: #x #H normalize in H; destruct (H)
670          |6: #x #y #H normalize in H; destruct (H)
671          |4,5: #id #H //
672          ]
673        | @le_n ]
674      | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
675      ]
676    ]
677  ] ]
678| @conj [ @conj
679  [ #i #Hi //
680  | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3
681                   normalize in H3; destruct (H3) ]
682  ]                 
683  | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
684]
685qed.
686 
687let rec jump_expansion_internal (program: Σl:list labelled_instruction.|l| < 2^16)
688  (n: ℕ) on n: (Σpolicy:jump_expansion_policy.
689    And
690    (∀i:ℕ.i ≥ |program| → i < 2^16 → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?)
691    (jump_in_policy program policy)) ≝
692  match n with
693  [ O   ⇒ jump_expansion_start program
694  | S m ⇒ let old_policy ≝ jump_expansion_internal program m in
695    jump_expansion_step program (create_label_map program old_policy) old_policy
696  ].
697[ @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
698| @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program old_policy) old_policy)))
699]
700qed.
701
702definition policy_equal ≝
703  λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
704  ∀n:ℕ.n < |program| →
705    let 〈i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,0,short_jump〉 in
706    let 〈i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,0,short_jump〉 in
707    j1 = j2.
708
709lemma pe_refl:
710  ∀program.reflexive ? (policy_equal program).
711 #program whd #x whd #n #Hn cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
712 #y cases y -y #y #z normalize nodelta @refl
713qed.
714
715lemma pe_sym:
716  ∀program.symmetric ? (policy_equal program).
717 #program whd #x #y #Hxy whd #n #Hn
718 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
719 #z cases z -z #x1 #x2 #x3 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉)
720 #z cases z -z #y1 #y2 #y3 normalize nodelta //
721qed.
722
723lemma pe_trans:
724  ∀program.transitive ? (policy_equal program).
725 #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?);
726 whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn
727 lapply (Hxy n Hn) -Hxy lapply (Hyz n Hn) -Hyz
728 cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3
729 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z -z #y1 #y2 #y3
730 cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z -z #z1 #z2 #z3
731 normalize nodelta //
732qed.
733
734lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
735 ∀p1,p2:Σpolicy.
736 (∀i:ℕ.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?)
737 ∧jump_in_policy program policy.
738  policy_equal program p1 p2 →
739  policy_equal program (jump_expansion_step program (create_label_map program p1) p1)
740    (jump_expansion_step program (create_label_map program p2) p2).
741 #program #p1 #p2 #Heq whd #n #Hn lapply (Heq n Hn) #H
742 lapply (refl ? (lookup_opt … (bitvector_of_nat ? n) p1))
743 cases (lookup_opt … (bitvector_of_nat ? n) p1) in ⊢ (???% → ?);
744 [ #Hl lapply ((proj2 ?? (jump_not_in_policy program p1 n Hn)) Hl)
745   #Hnotjmp >lookup_opt_lookup_miss
746   [ >lookup_opt_lookup_miss
747     [ @refl
748     | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p2) p2)) n Hn))
749       [ @(proj1 ?? (pi2 … (jump_expansion_step program (create_label_map program p2) p2)))
750       | @Hnotjmp
751       ]
752     ]
753   | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p1) p1)) n Hn))
754     [ @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program p1) p1)))
755     | @Hnotjmp
756     ]
757   ]
758 | #x #Hl cases daemon (* XXX *)
759 ]
760qed.
761
762(* this is in the stdlib, but commented out, why? *)
763theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
764  #n (elim n) normalize /2 by S_pred/ qed.
765
766lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.|l| < 2^16).∀n:ℕ.
767  policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program (S n)) →
768  ∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program k).
769 #program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
770 lapply Heq -Heq; lapply n -n; elim z -z;
771 [ #n #Heq <plus_n_O @pe_refl 
772 | #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z); @(pe_trans … (jump_expansion_internal program (S n)))
773   [ @Heq
774   | @pe_step @Hind @Heq
775   ]
776 ]
777qed.
778
779lemma thingie:
780  ∀A:Prop.(A + ¬A) → (¬¬A) → A.
781 #A #Adec #nnA cases Adec
782 [ //
783 | #H @⊥ @(absurd (¬A) H nnA)
784 ]
785qed.
786 
787lemma policy_not_equal_incr: ∀program:(Σl:list labelled_instruction.|l|<2^16).
788 ∀policy:(Σp:jump_expansion_policy.
789    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
790    jump_in_policy program p).
791  ¬policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy) →
792  ∃n:ℕ.n < (|program|) ∧ jmple
793    (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
794    (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉)).
795 #program #policy #Hp
796 cases (dec_bounded_exists (λn.jmple
797   (\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
798   (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))) ? (|program|))
799 [ #H elim H; -H #i #Hi @(ex_intro ?? i) @Hi
800 | #abs @⊥ @(absurd ?? Hp) #n #Hn
801   lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) n Hn)
802   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
803   cases (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉) in ⊢ (???% → %);
804   #z cases z -z #x1 #x2 #x3 #Hx
805   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))
806   cases (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) in ⊢ (???% → %);
807   #z cases z -z #y1 #y2 #y3 #Hy
808   normalize nodelta #Hj cases Hj
809   [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn | >Hx >Hy @Hj ]
810   | //
811   ]
812 | #n @dec_jmple
813 ]
814qed.
815
816lemma stupid:
817  ∀program,n.
818  pi1 … (jump_expansion_step program (create_label_map program (jump_expansion_internal program n)) (jump_expansion_internal program n)) =
819  pi1 … (jump_expansion_internal program (S n)).
820 //
821qed.
822
823let rec measure_int (program: list labelled_instruction) (policy: jump_expansion_policy) (acc: ℕ)
824 on program: ℕ ≝
825 match program with
826 [ nil      ⇒ acc
827 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) with
828   [ long_jump   ⇒ measure_int t policy (acc + 2)
829   | medium_jump ⇒ measure_int t policy (acc + 1)
830   | _           ⇒ measure_int t policy acc
831   ]
832 ].
833
834(* definition measure ≝
835  λprogram.λpolicy.measure_int program policy 0. *)
836 
837lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
838  measure_int program policy (x+d) = measure_int program policy x + d.
839 #program #policy #x #d generalize in match x; -x elim d
840 [ //
841 | -d; #d #Hind elim program
842   [ //
843   | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
844     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
845     [ normalize nodelta @Hd
846     |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
847       @Hd
848     ]
849   ]
850 ]
851qed.
852   
853lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
854  ∀policy:Σp:jump_expansion_policy.
855    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
856    jump_in_policy program p.∀l.|l| ≤ |program| → ∀acc:ℕ.
857  measure_int l policy acc ≤ measure_int l (jump_expansion_step program (create_label_map program policy) policy) acc.
858#program #policy #l elim l -l;
859  [ #Hp #acc normalize @le_n
860  | #h #t #Hind #Hp #acc
861    lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) Hp)
862    whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ???)?);
863    cases (bvt_lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3
864    cases (bvt_lookup … (bitvector_of_nat ? (|t|)) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) #z cases z -z #y1 #y2 #y3
865    normalize nodelta #Hj cases Hj
866    [ cases x3 cases y3
867      [1,4,5,7,8,9: #H @⊥ @H
868      |2,3,6: #_ normalize nodelta
869        [1,2: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) acc))
870        |3: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) (acc+1)))
871        ]
872        [1,3,5: @Hind @(transitive_le … Hp) @le_n_Sn
873        |2,4,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus [ @le_n | //]
874        ]
875      ]
876    | #Heq >Heq cases y3 normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
877    ]
878  ]
879qed.
880
881lemma measure_le: ∀program.∀policy.
882  measure_int program policy 0 ≤ 2*|program|.
883 #program #policy elim program
884 [ normalize @le_n
885 | #h #t #Hind whd in match (measure_int ???);
886   cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
887   [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
888   |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
889     @le_plus [1,3: @Hind |2,4: // ]
890   ]
891 ]
892qed.
893
894(* these lemmas seem superfluous, but not sure how *)
895lemma bla: ∀a,b:ℕ.a + a = b + b → a = b.
896 #a elim a
897 [ normalize #b //
898 | -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ | -b #b normalize
899   <plus_n_Sm <plus_n_Sm #H
900   >(Hind b (injective_S ?? (injective_S ?? H))) // ]
901 ]
902qed.
903
904lemma sth_not_s: ∀x.x ≠ S x.
905 #x cases x
906 [ // | #y // ]
907qed.
908
909lemma measure_full: ∀program.∀policy.
910  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
911  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,0,short_jump〉)) = long_jump.
912 #program #policy elim program
913 [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
914 | #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
915   [ whd in match (measure_int ???) in Hm;
916     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
917     normalize nodelta
918     [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
919     | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
920       <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize
921       >(commutative_plus (|t|) 0) <plus_O_n <minus_n_O
922       >plus_n_Sm @le_n
923     | >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) //
924     ]
925   | #Hmt cases (le_to_or_lt_eq … Hi) -Hi;
926   [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
927   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
928     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
929     normalize nodelta
930     [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
931       >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s
932     | >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize
933       #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s
934     | #_ //
935     ]
936   ]]
937 ]
938qed.
939
940lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
941  ∀policy:Σp:jump_expansion_policy.
942    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
943    jump_in_policy program p.
944  measure_int program policy 0 = measure_int program (jump_expansion_step program (create_label_map program policy) policy) 0 →
945  policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy).
946#program #policy lapply (le_n (|program|)) @(list_ind ?
947  (λx.|x| ≤ |program| → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program (create_label_map program policy) policy)) 0 →
948      policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program (create_label_map program policy) policy)))
949   ?? program)
950 [ #Hp #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
951 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
952   [ #Hi @Hind
953     [ @(transitive_le … Hp) //
954     | whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ???)?) in Hm;
955       lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
956       [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
957       | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
958         #x cases x -x #x1 #x2 #x3
959         cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
960         #y cases y -y #y1 #y2 #y3
961         normalize nodelta cases x3 cases y3 normalize nodelta
962         [1: #H #_ @H
963         |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
964           @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
965         |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
966         |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
967           #H #_ @(injective_plus_r … H)
968         |6: >measure_plus >measure_plus
969            change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
970            #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
971            @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
972         |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
973           #H #_ @(injective_plus_r … H)
974         ]
975       ]
976     | @(le_S_S_to_le … Hi)
977     ]
978   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 
979     whd in match (measure_int ?(jump_expansion_step ???)?) in Hm;
980     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
981     [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
982     | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
983       #x cases x -x #x1 #x2 #x3
984       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
985       #y cases y -y #y1 #y2 #y3
986       normalize nodelta cases x3 cases y3 normalize nodelta
987       [1,5,9: #_ #_ //
988       |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
989       |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
990         @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
991       |6: >measure_plus >measure_plus
992          change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
993          #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
994          @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
995       ]
996     ]
997   ]
998 ] 
999qed.
1000
1001lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
1002  |l| ≤ |program| → measure_int l (jump_expansion_internal program 0) 0 = 0.
1003 #l #program elim l
1004 [ //
1005 | #h #t #Hind #Hp whd in match (measure_int ???);
1006   cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
1007   [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,0,short_jump〉)
1008     [ normalize nodelta @Hind @le_S_to_le ]
1009     @Hp
1010   | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (jump_expansion_internal program 0) (|t|) ?) Hj) 〈0,0,short_jump〉)
1011     [ normalize nodelta @Hind @le_S_to_le ]
1012     @Hp
1013   ]
1014 ]
1015qed.
1016 
1017definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
1018  Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p.
1019 #program @(mk_Sig … (jump_expansion_internal program (2*|program|)))
1020 @(ex_intro … (2*|program|)) #k #Hk
1021 cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k)
1022   (jump_expansion_internal program (S k))) ? (2*|program|))
1023 [ #H elim H -H #x #Hx @pe_trans
1024   [ @(jump_expansion_internal program x)
1025   | @pe_sym @equal_remains_equal
1026     [ @(proj2 ?? Hx)
1027     | @(transitive_le ? (2*|program|))
1028       [ @le_S_S_to_le @le_S @(proj1 ?? Hx)
1029       | @le_S_S_to_le @le_S @Hk
1030       ]
1031     ]
1032   | @equal_remains_equal
1033     [ @(proj2 ?? Hx)
1034     | @le_S_S_to_le @le_S @(proj1 ?? Hx)
1035     ]
1036   ]
1037 | #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @pe_sym @equal_remains_equal
1038   [ lapply (measure_full program (jump_expansion_internal program (2*|program|)))
1039     #Hfull #i #Hi
1040     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program (jump_expansion_internal program (2*|program|))) (jump_expansion_internal program (2*|program|)))) i Hi)
1041     lapply (Hfull ? i Hi)
1042     [ -i @le_to_le_to_eq
1043       [ @measure_le
1044       | lapply (le_n (2*|program|)) elim (2*|program|) in ⊢ (?%? → %);
1045         [ #_ >measure_zero @le_n
1046         | #x #Hind #Hx
1047           cut (measure_int program (jump_expansion_internal program x) 0 <
1048                measure_int program (jump_expansion_internal program (S x)) 0)
1049           [ elim (le_to_or_lt_eq …
1050               (measure_incr_or_equal program (jump_expansion_internal program x) program (le_n (|program|)) 0))
1051             [ //
1052             | #H @⊥ @(absurd ?? (Hfa x Hx)) @measure_special @H
1053             ]
1054           | #H lapply (Hind (le_S_to_le … Hx)) #H2 @(le_to_lt_to_lt … H) @H2
1055           ]
1056         ]
1057       ]
1058     | -Hfull cases (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_internal program (2*|program|)) 〈0,0,short_jump〉)
1059       #x cases x -x #x1 #x2 #x3 normalize nodelta #Hfull
1060       >Hfull cases (bvt_lookup ?? (bitvector_of_nat ? i) ? 〈0,0,short_jump〉)
1061       #y cases y -y #y1 #y2 #y3 normalize nodelta cases y3 normalize nodelta 
1062       [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ]
1063       | #_ //
1064       ]
1065     ]
1066   | @le_S_to_le @Hk
1067   ]
1068 | #n @dec_bounded_forall #m
1069   cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉)
1070   #x cases x -x #x1 #x2 #x3
1071   cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉)
1072   #y cases y -y #y1 #y2 #y3 normalize nodelta
1073   @dec_eq_jump_length
1074 ]
1075qed.
1076
1077let rec transform_policy (n: nat) policy (acc: BitVectorTrie jump_length 16) on n:
1078  BitVectorTrie jump_length 16 ≝
1079  match n with
1080  [ O    ⇒ acc
1081  | S n' ⇒
1082    match lookup_opt … (bitvector_of_nat 16 n') policy with
1083    [ None   ⇒ transform_policy n' policy acc
1084    | Some x ⇒ let 〈pc,length〉 ≝ x in
1085      transform_policy n' policy (insert … pc length acc)
1086    ]
1087  ].
1088
1089definition jump_expansion':
1090 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
1091 policy_type ≝
1092 λprogram.λpc.
1093  let policy ≝
1094    transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in
1095  lookup ? ? pc policy long_jump.
1096/2 by Stub, mk_Sig/
1097qed.
Note: See TracBrowser for help on using the repository browser.