[1614] | 1 | include "ASM/ASM.ma". |
---|
| 2 | include "ASM/Arithmetic.ma". |
---|
| 3 | include "ASM/Fetch.ma". |
---|
| 4 | include "ASM/Status.ma". |
---|
| 5 | include alias "basics/logic.ma". |
---|
| 6 | include alias "arithmetics/nat.ma". |
---|
| 7 | include "utilities/extralib.ma". |
---|
[1615] | 8 | include "ASM/Assembly.ma". |
---|
[1614] | 9 | |
---|
| 10 | definition 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 | |
---|
| 22 | definition 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 | |
---|
| 38 | definition jmpleq: jump_length → jump_length → Prop ≝ |
---|
| 39 | λj1.λj2.jmple j1 j2 ∨ j1 = j2. |
---|
| 40 | |
---|
| 41 | lemma 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/ |
---|
| 43 | qed. |
---|
| 44 | |
---|
| 45 | lemma 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/ |
---|
| 49 | qed. |
---|
| 50 | |
---|
| 51 | lemma 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) |
---|
| 54 | qed. |
---|
| 55 | |
---|
| 56 | |
---|
| 57 | (* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *) |
---|
| 58 | definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16. |
---|
| 59 | |
---|
| 60 | (* label_map: identifier ↦ 〈instruction number, address〉 *) |
---|
| 61 | definition label_map ≝ identifier_map ASMTag (nat × nat). |
---|
| 62 | |
---|
| 63 | definition 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 | |
---|
| 71 | definition 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 | |
---|
| 81 | lemma 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 | ] |
---|
| 104 | qed. |
---|
| 105 | |
---|
| 106 | definition 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 | ] |
---|
| 163 | qed. |
---|
| 164 | |
---|
| 165 | definition 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 | |
---|
| 176 | definition 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 | |
---|
| 187 | definition 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 | |
---|
| 198 | definition 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 | |
---|
| 214 | definition 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 | |
---|
| 229 | definition 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 | |
---|
| 239 | lemma 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 | ] |
---|
| 254 | qed. |
---|
| 255 | |
---|
| 256 | |
---|
| 257 | definition 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 *) |
---|
| 264 | lemma 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 | ] |
---|
| 270 | qed. |
---|
| 271 | |
---|
| 272 | lemma 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 | ] |
---|
| 280 | qed. |
---|
| 281 | |
---|
| 282 | lemma 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 | ] |
---|
| 299 | qed. |
---|
| 300 | |
---|
| 301 | definition 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 | ] |
---|
| 435 | qed. |
---|
| 436 | |
---|
| 437 | definition 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 | |
---|
| 445 | definition 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 | |
---|
| 462 | definition 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 | ] |
---|
| 685 | qed. |
---|
| 686 | |
---|
| 687 | let 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 | ] |
---|
| 700 | qed. |
---|
| 701 | |
---|
| 702 | definition 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 | |
---|
| 709 | lemma 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 |
---|
| 713 | qed. |
---|
| 714 | |
---|
| 715 | lemma 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 // |
---|
| 721 | qed. |
---|
| 722 | |
---|
| 723 | lemma 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 // |
---|
| 732 | qed. |
---|
| 733 | |
---|
| 734 | lemma 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 | ] |
---|
| 760 | qed. |
---|
| 761 | |
---|
| 762 | (* this is in the stdlib, but commented out, why? *) |
---|
| 763 | theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n. |
---|
| 764 | #n (elim n) normalize /2 by S_pred/ qed. |
---|
| 765 | |
---|
| 766 | lemma 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 | ] |
---|
| 777 | qed. |
---|
| 778 | |
---|
| 779 | lemma thingie: |
---|
| 780 | ∀A:Prop.(A + ¬A) → (¬¬A) → A. |
---|
| 781 | #A #Adec #nnA cases Adec |
---|
| 782 | [ // |
---|
| 783 | | #H @⊥ @(absurd (¬A) H nnA) |
---|
| 784 | ] |
---|
| 785 | qed. |
---|
| 786 | |
---|
| 787 | lemma 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 | ] |
---|
| 814 | qed. |
---|
| 815 | |
---|
| 816 | lemma 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 | // |
---|
| 821 | qed. |
---|
| 822 | |
---|
| 823 | let 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 | |
---|
| 837 | lemma 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 | ] |
---|
| 851 | qed. |
---|
| 852 | |
---|
| 853 | lemma 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 | ] |
---|
| 879 | qed. |
---|
| 880 | |
---|
| 881 | lemma 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 | ] |
---|
| 892 | qed. |
---|
| 893 | |
---|
| 894 | (* these lemmas seem superfluous, but not sure how *) |
---|
| 895 | lemma 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 | ] |
---|
| 902 | qed. |
---|
| 903 | |
---|
| 904 | lemma sth_not_s: ∀x.x ≠ S x. |
---|
| 905 | #x cases x |
---|
| 906 | [ // | #y // ] |
---|
| 907 | qed. |
---|
| 908 | |
---|
| 909 | lemma 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 | ] |
---|
| 938 | qed. |
---|
| 939 | |
---|
| 940 | lemma 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 | ] |
---|
| 999 | qed. |
---|
| 1000 | |
---|
| 1001 | lemma 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 | ] |
---|
| 1015 | qed. |
---|
| 1016 | |
---|
| 1017 | definition 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 | ] |
---|
| 1075 | qed. |
---|
| 1076 | |
---|
| 1077 | let 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 | ]. |
---|
[1615] | 1088 | |
---|
| 1089 | definition 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/ |
---|
| 1097 | qed. |
---|