[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 | |
---|
[1809] | 10 | (* Internal types *) |
---|
| 11 | |
---|
| 12 | (* label_map: identifier ↦ 〈instruction number, address〉 *) |
---|
| 13 | definition label_map ≝ identifier_map ASMTag (ℕ × ℕ). |
---|
| 14 | |
---|
| 15 | (* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *) |
---|
| 16 | definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16. |
---|
| 17 | |
---|
| 18 | (* The different properties that we want/need to prove at some point *) |
---|
| 19 | (* Anything that's not in the program doesn't end up in the policy *) |
---|
| 20 | definition out_of_program_none ≝ |
---|
| 21 | λprefix:list labelled_instruction.λpolicy:jump_expansion_policy. |
---|
| 22 | ∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?. |
---|
| 23 | |
---|
| 24 | (* If instruction i is a jump, then there will be something in the policy at |
---|
| 25 | * position i *) |
---|
| 26 | definition is_jump' ≝ |
---|
| 27 | λx:preinstruction Identifier. |
---|
| 28 | match x with |
---|
| 29 | [ JC _ ⇒ True |
---|
| 30 | | JNC _ ⇒ True |
---|
| 31 | | JZ _ ⇒ True |
---|
| 32 | | JNZ _ ⇒ True |
---|
| 33 | | JB _ _ ⇒ True |
---|
| 34 | | JNB _ _ ⇒ True |
---|
| 35 | | JBC _ _ ⇒ True |
---|
| 36 | | CJNE _ _ ⇒ True |
---|
| 37 | | DJNZ _ _ ⇒ True |
---|
| 38 | | _ ⇒ False |
---|
[1614] | 39 | ]. |
---|
[1809] | 40 | |
---|
| 41 | definition is_jump ≝ |
---|
| 42 | λx:labelled_instruction. |
---|
| 43 | let 〈label,instr〉 ≝ x in |
---|
| 44 | match instr with |
---|
| 45 | [ Instruction i ⇒ is_jump' i |
---|
| 46 | | Call _ ⇒ True |
---|
| 47 | | Jmp _ ⇒ True |
---|
| 48 | | _ ⇒ False |
---|
| 49 | ]. |
---|
[1614] | 50 | |
---|
[1809] | 51 | definition jump_in_policy ≝ |
---|
| 52 | λprefix:list labelled_instruction.λpolicy:jump_expansion_policy. |
---|
| 53 | ∀i:ℕ.i < |prefix| → |
---|
| 54 | (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔ |
---|
| 55 | ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉). |
---|
| 56 | |
---|
| 57 | definition labels_okay ≝ |
---|
| 58 | λlabels:label_map.λpolicy:jump_expansion_policy. |
---|
| 59 | bvt_forall ?? policy (λn.λx.let 〈pc,addr_nat,i〉 ≝ x in |
---|
| 60 | ∃id:Identifier. |
---|
| 61 | \snd (lookup_def … labels id 〈0,pc〉) = addr_nat |
---|
| 62 | ). |
---|
| 63 | |
---|
| 64 | (* Between two policies, jumps cannot decrease *) |
---|
[1614] | 65 | definition jmple: jump_length → jump_length → Prop ≝ |
---|
| 66 | λj1.λj2. |
---|
| 67 | match j1 with |
---|
| 68 | [ short_jump ⇒ |
---|
| 69 | match j2 with |
---|
| 70 | [ short_jump ⇒ False |
---|
| 71 | | _ ⇒ True |
---|
| 72 | ] |
---|
| 73 | | medium_jump ⇒ |
---|
| 74 | match j2 with |
---|
| 75 | [ long_jump ⇒ True |
---|
| 76 | | _ ⇒ False |
---|
| 77 | ] |
---|
| 78 | | long_jump ⇒ False |
---|
| 79 | ]. |
---|
| 80 | |
---|
| 81 | definition jmpleq: jump_length → jump_length → Prop ≝ |
---|
| 82 | λj1.λj2.jmple j1 j2 ∨ j1 = j2. |
---|
| 83 | |
---|
[1809] | 84 | definition policy_increase: list labelled_instruction → jump_expansion_policy → |
---|
| 85 | jump_expansion_policy → Prop ≝ |
---|
| 86 | λprogram.λop.λp. |
---|
| 87 | (∀i:ℕ.i < |program| → |
---|
| 88 | let 〈i1,i2,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) op 〈0,0,short_jump〉 in |
---|
| 89 | let 〈i3,i4,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) p 〈0,0,short_jump〉 in |
---|
| 90 | jmpleq oj j). |
---|
| 91 | |
---|
| 92 | (* Policy safety *) |
---|
| 93 | definition policy_safe: jump_expansion_policy → Prop ≝ |
---|
| 94 | λpolicy. |
---|
| 95 | bvt_forall ?? policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in |
---|
| 96 | match jmp_len with |
---|
| 97 | [ short_jump ⇒ if leb pc_nat addr_nat |
---|
| 98 | then le (addr_nat - pc_nat) 126 |
---|
| 99 | else le (pc_nat - addr_nat) 129 |
---|
| 100 | | medium_jump ⇒ |
---|
| 101 | let addr ≝ bitvector_of_nat 16 addr_nat in |
---|
| 102 | let pc ≝ bitvector_of_nat 16 pc_nat in |
---|
| 103 | let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in |
---|
| 104 | let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in |
---|
| 105 | eq_bv 5 fst_5_addr fst_5_pc = true |
---|
| 106 | | long_jump ⇒ True |
---|
| 107 | ] |
---|
| 108 | ). |
---|
| 109 | |
---|
| 110 | (* Definitions and theorems for the jump_length type (itself defined in Assembly) *) |
---|
| 111 | definition max_length: jump_length → jump_length → jump_length ≝ |
---|
| 112 | λj1.λj2. |
---|
| 113 | match j1 with |
---|
| 114 | [ long_jump ⇒ long_jump |
---|
| 115 | | medium_jump ⇒ |
---|
| 116 | match j2 with |
---|
| 117 | [ medium_jump ⇒ medium_jump |
---|
| 118 | | _ ⇒ long_jump |
---|
| 119 | ] |
---|
| 120 | | short_jump ⇒ |
---|
| 121 | match j2 with |
---|
| 122 | [ short_jump ⇒ short_jump |
---|
| 123 | | _ ⇒ long_jump |
---|
| 124 | ] |
---|
| 125 | ]. |
---|
| 126 | |
---|
[1614] | 127 | lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y). |
---|
| 128 | #x #y cases x cases y /3 by inl, inr, nmk, I/ |
---|
| 129 | qed. |
---|
| 130 | |
---|
| 131 | lemma jmpleq_max_length: ∀ol,nl. |
---|
| 132 | jmpleq ol (max_length ol nl). |
---|
| 133 | #ol #nl cases ol cases nl |
---|
| 134 | /2 by or_introl, or_intror, I/ |
---|
| 135 | qed. |
---|
| 136 | |
---|
| 137 | lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b). |
---|
| 138 | #a #b cases a cases b /2/ |
---|
| 139 | %2 @nmk #H destruct (H) |
---|
| 140 | qed. |
---|
| 141 | |
---|
[1809] | 142 | (* Labels *) |
---|
[1614] | 143 | definition is_label ≝ |
---|
| 144 | λx:labelled_instruction.λl:Identifier. |
---|
| 145 | let 〈lbl,instr〉 ≝ x in |
---|
| 146 | match lbl with |
---|
| 147 | [ Some l' ⇒ l' = l |
---|
| 148 | | _ ⇒ False |
---|
| 149 | ]. |
---|
| 150 | |
---|
| 151 | lemma label_does_not_occur: |
---|
| 152 | ∀i,p,l. |
---|
| 153 | is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false. |
---|
| 154 | #i #p #l generalize in match i; elim p |
---|
| 155 | [ #i >nth_nil #H @⊥ @H |
---|
| 156 | | #h #t #IH #i cases i -i |
---|
| 157 | [ cases h #hi #hp cases hi |
---|
| 158 | [ normalize #H @⊥ @H |
---|
| 159 | | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ??); |
---|
| 160 | whd in Heq; >Heq |
---|
[1809] | 161 | >eq_identifier_refl / by refl/ |
---|
[1614] | 162 | ] |
---|
| 163 | | #i #H whd in match (does_not_occur ??); |
---|
| 164 | whd in match (instruction_matches_identifier ??); |
---|
| 165 | cases h #hi #hp cases hi normalize nodelta |
---|
| 166 | [ @(IH i) @H |
---|
| 167 | | #l' @eq_identifier_elim |
---|
[1809] | 168 | [ normalize / by / |
---|
[1614] | 169 | | normalize #_ @(IH i) @H |
---|
| 170 | ] |
---|
| 171 | ] |
---|
| 172 | ] |
---|
| 173 | ] |
---|
[1809] | 174 | qed. |
---|
[1614] | 175 | |
---|
[1809] | 176 | definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝ |
---|
| 177 | λpc.λjmp_len.λinstr. |
---|
| 178 | let bv_pc ≝ bitvector_of_nat 16 pc in |
---|
| 179 | let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) bv_pc jmp_len ? instr in |
---|
| 180 | let bv: list (BitVector 8) ≝ match ilist with |
---|
| 181 | [ None ⇒ (* this shouldn't happen *) [ ] |
---|
| 182 | | Some l ⇒ flatten … (map … assembly1 l) |
---|
| 183 | ] in |
---|
| 184 | pc + (|bv|). |
---|
| 185 | @(λx.bv_pc) |
---|
| 186 | qed. |
---|
| 187 | |
---|
| 188 | (* The function that creates the label-to-address map *) |
---|
[1614] | 189 | definition create_label_map: ∀program:list labelled_instruction. |
---|
| 190 | ∀policy:jump_expansion_policy. |
---|
| 191 | (Σlabels:label_map. |
---|
| 192 | ∀i:ℕ.lt i (|program|) → |
---|
| 193 | ∀l.occurs_exactly_once l program → |
---|
| 194 | is_label (nth i ? program 〈None ?, Comment [ ]〉) l → |
---|
| 195 | ∃a.lookup … labels l = Some ? 〈i,a〉 |
---|
| 196 | ) ≝ |
---|
| 197 | λprogram.λpolicy. |
---|
| 198 | let 〈final_pc, final_labels〉 ≝ |
---|
| 199 | foldl_strong (option Identifier × pseudo_instruction) |
---|
| 200 | (λprefix.ℕ × (Σlabels. |
---|
| 201 | ∀i:ℕ.lt i (|prefix|) → |
---|
| 202 | ∀l.occurs_exactly_once l prefix → |
---|
| 203 | is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l → |
---|
| 204 | ∃a.lookup … labels l = Some ? 〈i,a〉) |
---|
| 205 | ) |
---|
| 206 | program |
---|
| 207 | (λprefix.λx.λtl.λprf.λacc. |
---|
| 208 | let 〈pc,labels〉 ≝ acc in |
---|
| 209 | let 〈label,instr〉 ≝ x in |
---|
| 210 | let new_labels ≝ |
---|
| 211 | match label with |
---|
| 212 | [ None ⇒ labels |
---|
| 213 | | Some l ⇒ add … labels l 〈|prefix|, pc〉 |
---|
| 214 | ] in |
---|
| 215 | let 〈i1,i2,jmp_len〉 ≝ bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈0, 0, long_jump〉 in |
---|
| 216 | 〈add_instruction_size pc jmp_len instr, new_labels〉 |
---|
| 217 | ) 〈0, empty_map …〉 in |
---|
| 218 | final_labels. |
---|
| 219 | [ #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi; |
---|
| 220 | [ #Hi #l normalize nodelta; cases label normalize nodelta |
---|
| 221 | [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl |
---|
| 222 | lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr |
---|
| 223 | % [ @addr | @Haddr ] |
---|
| 224 | | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc; |
---|
| 225 | @eq_identifier_elim #Heq #Hocc |
---|
| 226 | [ normalize in Hocc; |
---|
| 227 | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl |
---|
| 228 | @⊥ @(absurd … Hocc) |
---|
| 229 | | normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?) |
---|
| 230 | [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ] |
---|
[1809] | 231 | | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; / by / |
---|
[1614] | 232 | ] |
---|
| 233 | ] |
---|
[1809] | 234 | >(label_does_not_occur i … Hl) normalize nodelta @nmk / by / |
---|
[1614] | 235 | ] |
---|
| 236 | | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second |
---|
| 237 | [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl; |
---|
| 238 | [ normalize nodelta #H @⊥ @H |
---|
| 239 | | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_add_hit ] |
---|
| 240 | ] |
---|
| 241 | | @le_n |
---|
| 242 | ] |
---|
| 243 | ] |
---|
| 244 | | #i #Hi #l #Hl @⊥ @Hl |
---|
| 245 | ] |
---|
| 246 | qed. |
---|
| 247 | |
---|
| 248 | definition select_reljump_length: label_map → ℕ → Identifier → ℕ ×jump_length ≝ |
---|
| 249 | λlabels.λpc.λlbl. |
---|
| 250 | let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in |
---|
| 251 | if leb pc addr (* forward jump *) |
---|
| 252 | then if leb (addr - pc) 126 |
---|
| 253 | then 〈addr, short_jump〉 |
---|
| 254 | else 〈addr, long_jump〉 |
---|
| 255 | else if leb (pc - addr) 129 |
---|
| 256 | then 〈addr, short_jump〉 |
---|
| 257 | else 〈addr, long_jump〉. |
---|
| 258 | |
---|
| 259 | definition select_call_length: label_map → ℕ → Identifier → ℕ × jump_length ≝ |
---|
| 260 | λlabels.λpc_nat.λlbl. |
---|
| 261 | let pc ≝ bitvector_of_nat 16 pc_nat in |
---|
| 262 | let addr_nat ≝ (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in |
---|
| 263 | let addr ≝ bitvector_of_nat 16 addr_nat in |
---|
| 264 | let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in |
---|
| 265 | let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in |
---|
| 266 | if eq_bv ? fst_5_addr fst_5_pc |
---|
| 267 | then 〈addr_nat, medium_jump〉 |
---|
| 268 | else 〈addr_nat, long_jump〉. |
---|
| 269 | |
---|
| 270 | definition select_jump_length: label_map → ℕ → Identifier → ℕ × jump_length ≝ |
---|
| 271 | λlabels.λpc.λlbl. |
---|
| 272 | let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in |
---|
| 273 | if leb pc addr |
---|
| 274 | then if leb (addr - pc) 126 |
---|
| 275 | then 〈addr, short_jump〉 |
---|
| 276 | else select_call_length labels pc lbl |
---|
| 277 | else if leb (pc - addr) 129 |
---|
| 278 | then 〈addr, short_jump〉 |
---|
| 279 | else select_call_length labels pc lbl. |
---|
| 280 | |
---|
| 281 | definition jump_expansion_step_instruction: label_map → ℕ → |
---|
| 282 | preinstruction Identifier → option (ℕ × jump_length) ≝ |
---|
| 283 | λlabels.λpc.λi. |
---|
| 284 | match i with |
---|
| 285 | [ JC j ⇒ Some ? (select_reljump_length labels pc j) |
---|
| 286 | | JNC j ⇒ Some ? (select_reljump_length labels pc j) |
---|
| 287 | | JZ j ⇒ Some ? (select_reljump_length labels pc j) |
---|
| 288 | | JNZ j ⇒ Some ? (select_reljump_length labels pc j) |
---|
| 289 | | JB _ j ⇒ Some ? (select_reljump_length labels pc j) |
---|
| 290 | | JBC _ j ⇒ Some ? (select_reljump_length labels pc j) |
---|
| 291 | | JNB _ j ⇒ Some ? (select_reljump_length labels pc j) |
---|
| 292 | | CJNE _ j ⇒ Some ? (select_reljump_length labels pc j) |
---|
| 293 | | DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j) |
---|
| 294 | | _ ⇒ None ? |
---|
| 295 | ]. |
---|
| 296 | |
---|
| 297 | lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x). |
---|
| 298 | #x cases x #l #i cases i |
---|
| 299 | [#id cases id |
---|
| 300 | [1,2,3,6,7,33,34: |
---|
| 301 | #x #y %2 whd in match (is_jump ?); /2 by nmk/ |
---|
| 302 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: |
---|
| 303 | #x %2 whd in match (is_jump ?); /2 by nmk/ |
---|
| 304 | |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/ |
---|
[1809] | 305 | |9,10,14,15: #x %1 / by I/ |
---|
| 306 | |11,12,13,16,17: #x #y %1 / by I/ |
---|
[1614] | 307 | ] |
---|
| 308 | |2,3: #x %2 /2 by nmk/ |
---|
[1809] | 309 | |4,5: #x %1 / by I/ |
---|
[1614] | 310 | |6: #x #y %2 /2 by nmk/ |
---|
| 311 | ] |
---|
| 312 | qed. |
---|
| 313 | |
---|
[1809] | 314 | (* these should be moved to BitVector at some point, and proven *) |
---|
[1614] | 315 | lemma bitvector_of_nat_ok: |
---|
| 316 | ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y. |
---|
| 317 | #n elim n -n |
---|
| 318 | [ #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 |
---|
| 319 | | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *) |
---|
| 320 | ] |
---|
| 321 | qed. |
---|
| 322 | |
---|
| 323 | lemma bitvector_of_nat_abs: |
---|
| 324 | ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y). |
---|
| 325 | #n #x #y #Hx #Hy #Heq @notb_elim |
---|
| 326 | lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y))) |
---|
| 327 | cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %); |
---|
[1809] | 328 | [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/ |
---|
| 329 | | #H / by I/ |
---|
[1614] | 330 | ] |
---|
| 331 | qed. |
---|
| 332 | |
---|
| 333 | lemma jump_not_in_policy: ∀prefix:list labelled_instruction. |
---|
| 334 | ∀policy:(Σp:jump_expansion_policy. |
---|
[1809] | 335 | out_of_program_none prefix p ∧ jump_in_policy prefix p). |
---|
[1614] | 336 | ∀i:ℕ.i < |prefix| → |
---|
| 337 | iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉)) |
---|
| 338 | (lookup_opt … (bitvector_of_nat 16 i) policy = None ?). |
---|
| 339 | #prefix #policy #i #Hi @conj |
---|
| 340 | [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy)) |
---|
| 341 | cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?); |
---|
| 342 | [ #H @H |
---|
| 343 | | #x cases x -x #x #z cases x -x #x #y #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi)) |
---|
| 344 | @(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H))) |
---|
| 345 | ] |
---|
| 346 | | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj) |
---|
| 347 | #H elim H -H; #x #H elim H -H; #y #H elim H -H; #z #H >H in Hnone; #abs destruct (abs) |
---|
| 348 | ] |
---|
| 349 | qed. |
---|
| 350 | |
---|
[1809] | 351 | (* these two obviously belong somewhere else *) |
---|
| 352 | lemma pi1_eq: ∀A:Type[0].∀P:A->Prop.∀s1:Σa1:A.P a1.∀s2:Σa2:A.P a2. |
---|
| 353 | s1 = s2 → (pi1 ?? s1) = (pi1 ?? s2). |
---|
| 354 | #A #P #s1 #s2 / by / |
---|
| 355 | qed. |
---|
| 356 | |
---|
| 357 | lemma Some_eq: |
---|
| 358 | ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y. |
---|
| 359 | #T #x #y #H @option_destruct_Some @H |
---|
| 360 | qed. |
---|
| 361 | |
---|
| 362 | (* The first step of the jump expansion: everything to short. |
---|
| 363 | * The third condition of the dependent type implies jump_in_policy; |
---|
| 364 | * I've left it in for convenience of type-checking. *) |
---|
[1614] | 365 | definition jump_expansion_start: |
---|
| 366 | ∀program:(Σl:list labelled_instruction.|l| < 2^16). |
---|
| 367 | Σpolicy:jump_expansion_policy. |
---|
[1809] | 368 | out_of_program_none program policy ∧ |
---|
[1614] | 369 | jump_in_policy program policy ∧ |
---|
| 370 | ∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) → |
---|
| 371 | lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉 ≝ |
---|
| 372 | λprogram. |
---|
| 373 | foldl_strong (option Identifier × pseudo_instruction) |
---|
| 374 | (λprefix.Σpolicy:jump_expansion_policy. |
---|
[1809] | 375 | out_of_program_none prefix policy ∧ |
---|
[1614] | 376 | jump_in_policy prefix policy ∧ |
---|
| 377 | ∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) → |
---|
| 378 | lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉) |
---|
| 379 | program |
---|
| 380 | (λprefix.λx.λtl.λprf.λpolicy. |
---|
| 381 | let 〈label,instr〉 ≝ x in |
---|
| 382 | match instr with |
---|
| 383 | [ Instruction i ⇒ match i with |
---|
| 384 | [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy |
---|
| 385 | | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy |
---|
| 386 | | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy |
---|
| 387 | | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy |
---|
| 388 | | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy |
---|
| 389 | | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy |
---|
| 390 | | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy |
---|
| 391 | | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy |
---|
| 392 | | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy |
---|
| 393 | | _ ⇒ (pi1 … policy) |
---|
| 394 | ] |
---|
| 395 | | Call c ⇒ bvt_insert (ℕ×ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy |
---|
| 396 | | Jmp j ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy |
---|
| 397 | | _ ⇒ (pi1 ?? policy) |
---|
| 398 | ] |
---|
| 399 | ) (Stub ? ?). |
---|
| 400 | [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: |
---|
| 401 | @conj |
---|
| 402 | [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: |
---|
| 403 | @conj |
---|
| 404 | #i >append_length <commutative_plus #Hi normalize in Hi; |
---|
| 405 | [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: |
---|
| 406 | #Hi2 cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i) |
---|
| 407 | [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: |
---|
| 408 | @le_S_to_le @le_S_to_le @Hi |
---|
| 409 | |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: |
---|
| 410 | @Hi2 |
---|
| 411 | |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: |
---|
| 412 | <Hi @le_n_Sn |
---|
| 413 | |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: |
---|
| 414 | @Hi2 |
---|
| 415 | ] |
---|
| 416 | ] |
---|
| 417 | cases (le_to_or_lt_eq … Hi) -Hi; #Hi |
---|
| 418 | [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: |
---|
| 419 | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) |
---|
| 420 | @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) |
---|
| 421 | ] |
---|
| 422 | @conj >(injective_S … Hi) |
---|
| 423 | [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: |
---|
| 424 | >(nth_append_second ? ? prefix ? ? (le_n (|prefix|))) <minus_n_n #H @⊥ @H |
---|
| 425 | ] |
---|
| 426 | #H elim H; -H; #t1 #H elim H; -H #t2 #H elim H; -H; #t3 #H |
---|
| 427 | >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H; |
---|
| 428 | [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: |
---|
| 429 | #H destruct (H) |
---|
| 430 | ] |
---|
| 431 | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S |
---|
| 432 | @le_plus_n_r |
---|
| 433 | ] |
---|
| 434 | #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) |
---|
| 435 | -Hi; #Hi |
---|
| 436 | [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: |
---|
| 437 | #Hj @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi)) |
---|
[1809] | 438 | >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; / by / |
---|
[1614] | 439 | ] |
---|
| 440 | >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n |
---|
| 441 | #H @⊥ @H |
---|
| 442 | |2,3,26,27,28,29,30,31,32,33,34: @conj |
---|
| 443 | [1,3,5,7,9,11,13,15,17,19,21: @conj |
---|
| 444 | [1,3,5,7,9,11,13,15,17,19,21: |
---|
| 445 | #i >append_length <commutative_plus #Hi #Hi2 normalize in Hi; >lookup_opt_insert_miss |
---|
| 446 | [1,3,5,7,9,11,13,15,17,19,21: |
---|
| 447 | @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2) |
---|
| 448 | ] |
---|
| 449 | >eq_bv_sym @bitvector_of_nat_abs |
---|
| 450 | [1,4,7,10,13,16,19,22,25,28,31: |
---|
| 451 | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S |
---|
| 452 | @le_plus_n_r |
---|
| 453 | |2,5,8,11,14,17,20,23,26,29,32: @Hi2 |
---|
| 454 | |3,6,9,12,15,18,21,24,27,30,33: @lt_to_not_eq @Hi |
---|
| 455 | ] |
---|
| 456 | ] |
---|
| 457 | #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) |
---|
| 458 | -Hi #Hi |
---|
| 459 | [1,3,5,7,9,11,13,15,17,19,21: |
---|
| 460 | >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) >lookup_opt_insert_miss |
---|
| 461 | [1,3,5,7,9,11,13,15,17,19,21: |
---|
| 462 | @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) |
---|
| 463 | ] |
---|
| 464 | @bitvector_of_nat_abs |
---|
| 465 | [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi)) |
---|
| 466 | |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) |
---|
| 467 | ] |
---|
| 468 | @(transitive_lt … (pi2 ?? program)) |
---|
| 469 | >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r |
---|
| 470 | ] |
---|
| 471 | @conj >(injective_S … Hi) #H |
---|
| 472 | [2,4,6,8,10,12,14,16,18,20,22: |
---|
[1809] | 473 | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n / by I/ |
---|
[1614] | 474 | ] |
---|
| 475 | @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy)))) |
---|
| 476 | ] |
---|
| 477 | #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) |
---|
| 478 | -Hi #Hi |
---|
| 479 | [1,3,5,7,9,11,13,15,17,19,21: |
---|
| 480 | >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #Hj >lookup_opt_insert_miss |
---|
| 481 | [1,3,5,7,9,11,13,15,17,19,21: |
---|
| 482 | @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi) Hj) |
---|
| 483 | ] |
---|
| 484 | @bitvector_of_nat_abs |
---|
| 485 | [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi)) |
---|
| 486 | |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) |
---|
| 487 | ] |
---|
| 488 | @(transitive_lt … (pi2 ?? program)) |
---|
| 489 | >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r |
---|
| 490 | ] |
---|
| 491 | #_ >(injective_S … Hi) @lookup_opt_insert_hit |
---|
| 492 | |@conj |
---|
| 493 | [@conj |
---|
[1809] | 494 | [ #i #Hi / by refl/ |
---|
[1614] | 495 | | whd #i #Hi @⊥ @(absurd (i < 0) Hi (not_le_Sn_O ?)) |
---|
| 496 | ] |
---|
| 497 | | #i #Hi >nth_nil #Hj @⊥ @Hj |
---|
| 498 | ] |
---|
| 499 | qed. |
---|
| 500 | |
---|
[1809] | 501 | definition policy_equal_int ≝ |
---|
| 502 | λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy. |
---|
| 503 | ∀n:ℕ.n < |program| → |
---|
| 504 | let 〈i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,0,short_jump〉 in |
---|
| 505 | let 〈i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,0,short_jump〉 in |
---|
| 506 | j1 = j2. |
---|
| 507 | |
---|
[1810] | 508 | definition nec_plus_ultra ≝ |
---|
| 509 | λprogram:list labelled_instruction.λp:jump_expansion_policy. |
---|
| 510 | ¬(∀i.i < |program| → \snd (bvt_lookup … (bitvector_of_nat 16 i) p 〈0,0,short_jump〉) = long_jump). |
---|
| 511 | |
---|
[1809] | 512 | (* One step in the search for a jump expansion fixpoint. *) |
---|
[1614] | 513 | definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16). |
---|
| 514 | ∀labels:(Σlm:label_map.∀i:ℕ.lt i (|program|) → |
---|
| 515 | ∀l.occurs_exactly_once l program → |
---|
| 516 | is_label (nth i ? program 〈None ?, Comment [ ]〉) l → |
---|
| 517 | ∃a.lookup … lm l = Some ? 〈i,a〉). |
---|
| 518 | ∀old_policy:(Σpolicy. |
---|
[1809] | 519 | out_of_program_none program policy ∧ jump_in_policy program policy). |
---|
| 520 | (Σx:bool × ℕ × (option jump_expansion_policy). |
---|
| 521 | let 〈changed,pc,y〉 ≝ x in |
---|
| 522 | match y with |
---|
[1810] | 523 | [ None ⇒ pc > 2^16 ∧ nec_plus_ultra program old_policy |
---|
[1809] | 524 | | Some p ⇒ out_of_program_none program p ∧ labels_okay labels p ∧ |
---|
| 525 | jump_in_policy program p ∧ |
---|
| 526 | policy_increase program old_policy p ∧ |
---|
| 527 | policy_safe p ∧ |
---|
| 528 | (changed = false → policy_equal_int program old_policy p) |
---|
| 529 | ]) |
---|
[1614] | 530 | ≝ |
---|
| 531 | λprogram.λlabels.λold_policy. |
---|
[1809] | 532 | let 〈final_changed, final_pc, final_policy〉 ≝ |
---|
[1614] | 533 | foldl_strong (option Identifier × pseudo_instruction) |
---|
[1809] | 534 | (λprefix.Σx:bool × ℕ × jump_expansion_policy. |
---|
| 535 | let 〈changed,pc,policy〉 ≝ x in |
---|
| 536 | out_of_program_none prefix policy ∧ labels_okay labels policy ∧ |
---|
| 537 | jump_in_policy prefix policy ∧ |
---|
| 538 | policy_increase prefix old_policy policy ∧ |
---|
| 539 | policy_safe policy ∧ |
---|
| 540 | (changed = false → policy_equal_int prefix old_policy policy)) |
---|
[1614] | 541 | program |
---|
| 542 | (λprefix.λx.λtl.λprf.λacc. |
---|
[1809] | 543 | let 〈changed, pc, policy〉 ≝ acc in |
---|
[1614] | 544 | let 〈label,instr〉 ≝ x in |
---|
[1809] | 545 | (* let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_policy in *) |
---|
[1614] | 546 | let add_instr ≝ |
---|
| 547 | match instr with |
---|
| 548 | [ Instruction i ⇒ jump_expansion_step_instruction labels pc i |
---|
| 549 | | Call c ⇒ Some ? (select_call_length labels pc c) |
---|
| 550 | | Jmp j ⇒ Some ? (select_jump_length labels pc j) |
---|
| 551 | | _ ⇒ None ? |
---|
| 552 | ] in |
---|
| 553 | let 〈ignore,old_length〉 ≝ bvt_lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, 0, short_jump〉 in |
---|
| 554 | match add_instr with |
---|
| 555 | [ None ⇒ (* i.e. it's not a jump *) |
---|
[1809] | 556 | 〈changed, add_instruction_size pc long_jump instr, policy〉 |
---|
[1614] | 557 | | Some z ⇒ let 〈addr,ai〉 ≝ z in |
---|
| 558 | let new_length ≝ max_length old_length ai in |
---|
[1809] | 559 | 〈match dec_eq_jump_length new_length old_length with |
---|
| 560 | [ inl _ ⇒ changed |
---|
| 561 | | inr _ ⇒ true], add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, addr, new_length〉 policy〉 |
---|
| 562 | ] |
---|
| 563 | ) 〈false, 0, Stub ? ?〉 in |
---|
| 564 | if geb final_pc 2^16 then |
---|
| 565 | 〈final_changed,final_pc,None ?〉 |
---|
| 566 | else |
---|
| 567 | 〈final_changed,final_pc,Some jump_expansion_policy final_policy〉. |
---|
[1810] | 568 | [ normalize nodelta @conj |
---|
| 569 | [ @leb_true_to_le @p2 |
---|
| 570 | | @nmk #Hfull (* XXX *) cases daemon |
---|
| 571 | ] |
---|
[1809] | 572 | | normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2 |
---|
| 573 | >H2 in H; >p1 normalize nodelta // |
---|
| 574 | | lapply (pi2 ?? acc) >p >p1 normalize nodelta #Hpolicy |
---|
| 575 | @conj [ @conj [ @conj [ @conj [ @conj |
---|
| 576 | [ (* out_of_policy_none *) |
---|
| 577 | #i >append_length <commutative_plus #Hi normalize in Hi; |
---|
| 578 | #Hi2 >lookup_opt_insert_miss |
---|
| 579 | [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le … Hi)) @Hi2 |
---|
| 580 | | >eq_bv_sym @bitvector_of_nat_abs |
---|
| 581 | [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
| 582 | @le_S_S @le_plus_n_r |
---|
| 583 | | @Hi2 |
---|
| 584 | | @lt_to_not_eq @Hi |
---|
[1614] | 585 | ] |
---|
| 586 | ] |
---|
[1809] | 587 | | (* labels_okay *) |
---|
| 588 | @lookup_forall #i cases i -i #i cases i -i #p #a #j #n (*lapply (refl ? add_instr) |
---|
| 589 | cases (lookup ??? old_policy ?); #x cases x -x #p1 #p2 #p3 |
---|
| 590 | cases add_instr in ⊢ (???% → %); |
---|
| 591 | [ #Hai normalize nodelta #Hl |
---|
| 592 | elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? n Hl) |
---|
| 593 | #i #Hi @(ex_intro ?? i Hi) |
---|
| 594 | | #x cases x -x #np #nl #Hai normalize nodelta *) #Hl |
---|
| 595 | elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl |
---|
| 596 | [ elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? n Hl) |
---|
| 597 | #i #Hi @(ex_intro ?? i Hi) |
---|
| 598 | | (*whd in match add_instr in Hai; cases instr in Hai;*) normalize nodelta |
---|
| 599 | normalize nodelta in p4; cases instr in p4; |
---|
| 600 | [2,3: #x #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
| 601 | |6: #x #y #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
| 602 | |1: #pi cases pi |
---|
| 603 | [35,36,37: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
| 604 | |1,2,3,6,7,33,34: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) |
---|
| 605 | #H destruct (H) |
---|
| 606 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #abs normalize in abs; |
---|
| 607 | lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
| 608 | |9,10,14,15: #id normalize nodelta whd in match (jump_expansion_step_instruction ???); |
---|
| 609 | whd in match (select_reljump_length ???); >p5 |
---|
| 610 | lapply (refl ? (lookup_def ?? labels id 〈0,pc〉)) |
---|
| 611 | cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2 |
---|
| 612 | normalize nodelta #H |
---|
| 613 | >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) |
---|
| 614 | >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2)) |
---|
| 615 | cases (leb pc q2) in ⊢ (???% → %); #Hle1 |
---|
| 616 | [1,3,5,7: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %); |
---|
| 617 | |2,4,6,8: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %); |
---|
| 618 | ] |
---|
| 619 | #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H |
---|
| 620 | <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl |
---|
| 621 | |11,12,13,16,17: #x #id normalize nodelta whd in match (jump_expansion_step_instruction ???); |
---|
| 622 | whd in match (select_reljump_length ???); >p5 |
---|
| 623 | lapply (refl ? (lookup_def ?? labels id 〈0,pc〉)) |
---|
| 624 | cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2 |
---|
| 625 | normalize nodelta #H |
---|
| 626 | >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) |
---|
| 627 | >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2)) |
---|
| 628 | cases (leb pc q2) in ⊢ (???% → %); #Hle1 |
---|
| 629 | [1,3,5,7,9: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %); |
---|
| 630 | |2,4,6,8,10: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %); |
---|
| 631 | ] |
---|
| 632 | #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H |
---|
| 633 | <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl |
---|
[1614] | 634 | ] |
---|
[1809] | 635 | |4,5: #id normalize nodelta whd in match (select_jump_length ???); |
---|
| 636 | whd in match (select_call_length ???); >p5 |
---|
| 637 | lapply (refl ? (lookup_def ?? labels id 〈0,pc〉)) |
---|
| 638 | cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2 |
---|
| 639 | normalize nodelta #H |
---|
| 640 | [1: cases (leb pc q2) |
---|
| 641 | [ cases (leb (q2-pc) 126) | cases (leb (pc-q2) 129) ] |
---|
| 642 | [1,3: normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; |
---|
| 643 | #Hli @(ex_intro ?? id) lapply (proj2 ?? Hl) |
---|
| 644 | #H >(pair_eq1 ?????? (pair_eq1 ?????? H)) |
---|
| 645 | >(pair_eq2 ?????? (pair_eq1 ?????? H)) >Hli @refl] |
---|
| 646 | ] |
---|
| 647 | cases (split ? 5 11 (bitvector_of_nat 16 q2)) #n1 #n2 |
---|
| 648 | cases (split ? 5 11 (bitvector_of_nat 16 pc)) #m1 #m2 |
---|
| 649 | normalize nodelta cases (eq_bv ? n1 m1) |
---|
| 650 | normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; #H |
---|
| 651 | @(ex_intro ?? id) lapply (proj2 ?? Hl) #H2 |
---|
| 652 | >(pair_eq1 ?????? (pair_eq1 ?????? H2)) >(pair_eq2 ?????? (pair_eq1 ?????? H2)) |
---|
| 653 | >H @refl |
---|
[1614] | 654 | ] |
---|
[1809] | 655 | ] |
---|
| 656 | ] |
---|
| 657 | | (* jump_in_policy *) |
---|
| 658 | #i #Hi cases (le_to_or_lt_eq … Hi) -Hi; |
---|
| 659 | [ >append_length <commutative_plus #Hi normalize in Hi; |
---|
| 660 | >(nth_append_first ?? prefix ??(le_S_S_to_le ?? Hi)) @conj |
---|
| 661 | [ #Hj lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) |
---|
| 662 | #Hacc elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj |
---|
| 663 | @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???); |
---|
| 664 | >lookup_opt_insert_miss [ @Hj | @bitvector_of_nat_abs ] |
---|
| 665 | [3: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi) |
---|
| 666 | |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) |
---|
| 667 | ] |
---|
| 668 | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
| 669 | @le_S_S @le_plus_n_r |
---|
| 670 | | lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) #Hacc |
---|
| 671 | #H elim H -H; #h #H elim H -H; #n #H elim H -H #j |
---|
[1614] | 672 | #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) |
---|
[1809] | 673 | <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs |
---|
| 674 | [3: @lt_to_not_eq @(le_S_S_to_le … Hi) |
---|
| 675 | |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) |
---|
| 676 | ] |
---|
| 677 | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
| 678 | @le_S_S @le_plus_n_r |
---|
[1614] | 679 | ] |
---|
[1809] | 680 | | >append_length <commutative_plus #Hi normalize in Hi; >(injective_S … Hi) |
---|
| 681 | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) |
---|
| 682 | <minus_n_n whd in match (nth ????); normalize nodelta in p4; cases instr in p4; |
---|
| 683 | [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] #Hinstr @conj normalize nodelta |
---|
[1614] | 684 | [3,5,11: #H @⊥ @H (* instr is not a jump *) |
---|
[1809] | 685 | |4,6,12: normalize nodelta in Hinstr; lapply (jmeq_to_eq ??? Hinstr) |
---|
| 686 | #H destruct (H) |
---|
| 687 | |7,9: (* instr is a jump *) #_ @(ex_intro ?? pc) |
---|
| 688 | @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) |
---|
| 689 | @lookup_opt_insert_hit |
---|
| 690 | |8,10: #_ / by I/ |
---|
| 691 | |1,2: cases pi in Hinstr; |
---|
| 692 | [35,36,37: #Hinstr #H @⊥ @H |
---|
| 693 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hinstr #H @⊥ @H |
---|
| 694 | |1,2,3,6,7,33,34: #x #y #Hinstr #H @⊥ @H |
---|
| 695 | |9,10,14,15: #id #Hinstr #_ |
---|
| 696 | @(ex_intro ?? pc) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) |
---|
[1614] | 697 | @lookup_opt_insert_hit |
---|
[1809] | 698 | |11,12,13,16,17: #x #id #Hinstr #_ |
---|
| 699 | @(ex_intro ?? pc) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) |
---|
[1614] | 700 | @lookup_opt_insert_hit |
---|
[1809] | 701 | |72,73,74: #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H) |
---|
| 702 | |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x #Hinstr |
---|
| 703 | lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H) |
---|
| 704 | |38,39,40,43,44,70,71: #x #y #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H |
---|
| 705 | normalize in H; destruct (H) |
---|
| 706 | |46,47,51,52: #id #Hinstr #_ / by I/ |
---|
| 707 | |48,49,50,53,54: #x #id #Hinstr #_ / by I/ |
---|
[1614] | 708 | ] |
---|
| 709 | ] |
---|
| 710 | ] |
---|
[1809] | 711 | ] |
---|
| 712 | | (* policy increase *) |
---|
| 713 | #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
| 714 | cases (le_to_or_lt_eq … Hi) -Hi; #Hi |
---|
| 715 | [ >lookup_insert_miss |
---|
| 716 | [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi)) |
---|
| 717 | | @bitvector_of_nat_abs |
---|
| 718 | [3: @lt_to_not_eq @(le_S_S_to_le … Hi) |
---|
| 719 | |1: @(transitive_lt ??? (le_S_S_to_le … Hi)) |
---|
| 720 | ] |
---|
| 721 | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
| 722 | @le_S_S @le_plus_n_r |
---|
| 723 | ] |
---|
| 724 | | >(injective_S … Hi) >p3 >lookup_insert_hit normalize nodelta |
---|
| 725 | @pair_elim #x #y #_ @jmpleq_max_length |
---|
[1614] | 726 | ] |
---|
[1809] | 727 | ] |
---|
| 728 | | (* policy_safe *) |
---|
| 729 | @lookup_forall #x cases x -x #x cases x -x #p #a #j #n normalize nodelta #Hl |
---|
| 730 | elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl |
---|
| 731 | [ @(forall_lookup … (proj2 ?? (proj1 ?? Hpolicy)) ? n Hl) |
---|
| 732 | | normalize nodelta in p4; cases instr in p4; |
---|
| 733 | [2,3: #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
| 734 | |6: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
| 735 | |1: #pi cases pi normalize nodelta |
---|
| 736 | [35,36,37: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
| 737 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: |
---|
| 738 | #x #abs @⊥ normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
| 739 | |1,2,3,6,7,33,34: #x #y #abs @⊥ normalize in abs; lapply (jmeq_to_eq ??? abs) #H |
---|
| 740 | destruct (H) |
---|
| 741 | |9,10,14,15: #id >p5 whd in match (jump_expansion_step_instruction ???); |
---|
| 742 | whd in match (select_reljump_length ???); |
---|
| 743 | cases (lookup_def ?? labels id 〈0,pc〉) #q1 #q2 normalize nodelta |
---|
| 744 | >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) |
---|
| 745 | >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2)) |
---|
| 746 | cases (leb pc q2) in ⊢ (???% → %); #Hle1 |
---|
| 747 | [1,3,5,7: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %); |
---|
| 748 | |2,4,6,8: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %); |
---|
| 749 | ] |
---|
| 750 | #Hle2 normalize nodelta #Hli |
---|
| 751 | <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 |
---|
| 752 | >(pair_eq2 ?????? (proj2 ?? Hl)) <(pair_eq2 ?????? (Some_eq ??? Hli)) |
---|
| 753 | cases old_length |
---|
| 754 | [1,7,13,19,25,31,37,43: @(leb_true_to_le … Hle2) |
---|
| 755 | ] normalize @I (* much faster than / by I/, strangely enough *) |
---|
| 756 | |11,12,13,16,17: #x #id >p5 whd in match (jump_expansion_step_instruction ???); |
---|
| 757 | whd in match (select_reljump_length ???); |
---|
| 758 | cases (lookup_def ?? labels id 〈0,pc〉) #q1 #q2 normalize nodelta |
---|
| 759 | >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) |
---|
| 760 | >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2)) |
---|
| 761 | cases (leb pc q2) in ⊢ (???% → %); #Hle1 |
---|
| 762 | [1,3,5,7,9: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %); |
---|
| 763 | |2,4,6,8,10: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %); |
---|
| 764 | ] |
---|
| 765 | #Hle2 normalize nodelta #Hli |
---|
| 766 | <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 >(pair_eq2 ?????? (proj2 ?? Hl)) |
---|
| 767 | <(pair_eq2 ?????? (Some_eq ??? Hli)) |
---|
| 768 | cases old_length |
---|
| 769 | [1,7,13,19,25,31,37,43,49,55: @(leb_true_to_le … Hle2) |
---|
| 770 | ] normalize @I (* vide supra *) |
---|
| 771 | ] |
---|
| 772 | |4,5: #id >p5 normalize nodelta whd in match (select_jump_length ???); |
---|
| 773 | whd in match (select_call_length ???); cases (lookup_def ?? labels id 〈0,pc〉) |
---|
| 774 | #q1 #q2 normalize nodelta |
---|
| 775 | >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) |
---|
| 776 | >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) |
---|
| 777 | [1: lapply (refl ? (leb pc q2)) cases (leb pc q2) in ⊢ (???% → %); #Hle1 |
---|
| 778 | [ lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %); |
---|
| 779 | | lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %); |
---|
[1614] | 780 | ] |
---|
[1809] | 781 | #Hle2 normalize nodelta |
---|
[1614] | 782 | ] |
---|
[1809] | 783 | [2,4,5: lapply (refl ? (split ? 5 11 (bitvector_of_nat ? q2))) |
---|
| 784 | cases (split ??? (bitvector_of_nat ? q2)) in ⊢ (???% → %); #x1 #x2 #Hle3 |
---|
| 785 | lapply (refl ? (split ? 5 11 (bitvector_of_nat ? pc))) |
---|
| 786 | cases (split ??? (bitvector_of_nat ? pc)) in ⊢ (???% → %); #y1 #y2 #Hle4 |
---|
| 787 | normalize nodelta lapply (refl ? (eq_bv 5 x1 y1)) |
---|
| 788 | cases (eq_bv 5 x1 y1) in ⊢ (???% → %); #Hle5 |
---|
| 789 | ] |
---|
| 790 | #Hli <(pair_eq1 ?????? (Some_eq ??? Hli)) >(pair_eq2 ?????? (proj2 ?? Hl)) |
---|
| 791 | <(pair_eq2 ?????? (Some_eq ??? Hli)) |
---|
| 792 | cases old_length |
---|
| 793 | [2,8,14: >Hle3 @Hle5 |
---|
| 794 | |19,22: >Hle1 @(leb_true_to_le … Hle2) |
---|
| 795 | ] normalize @I (* here too *) |
---|
[1614] | 796 | ] |
---|
[1809] | 797 | ] |
---|
| 798 | ] |
---|
| 799 | | (* changed *) |
---|
| 800 | cases (dec_eq_jump_length (max_length old_length ai) old_length) normalize nodelta |
---|
| 801 | [ #Hml #Hc #i #Hi cases (le_to_or_lt_eq … Hi) -Hi >append_length >commutative_plus #Hi |
---|
| 802 | normalize in Hi; |
---|
| 803 | [ >lookup_insert_miss |
---|
| 804 | [ @((proj2 ?? Hpolicy) Hc i (le_S_S_to_le … Hi)) |
---|
| 805 | | @bitvector_of_nat_abs |
---|
[1614] | 806 | [3: @lt_to_not_eq @(le_S_S_to_le … Hi) |
---|
| 807 | |1: @(transitive_lt ??? (le_S_S_to_le … Hi)) |
---|
| 808 | ] |
---|
| 809 | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
| 810 | @le_S_S @le_plus_n_r |
---|
| 811 | ] |
---|
[1809] | 812 | | >(injective_S … Hi) >p3 >lookup_insert_hit normalize nodelta |
---|
| 813 | @pair_elim #x #y #_ @(sym_eq ??? Hml) |
---|
| 814 | ] |
---|
| 815 | | #_ #H destruct (H) |
---|
| 816 | ] |
---|
| 817 | ] |
---|
| 818 | | (* Case where add_instr = None *) normalize nodelta lapply (pi2 ?? acc) >p >p1 |
---|
| 819 | normalize nodelta #Hpolicy |
---|
| 820 | @conj [ @conj [ @conj [ @conj [ @conj |
---|
| 821 | [ (* out_of_program_none *) #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
| 822 | #Hi2 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le ?? Hi) Hi2) |
---|
| 823 | | (* labels_okay *) @lookup_forall #x cases x -x #x cases x #p #a #j #lbl #Hl normalize nodelta |
---|
| 824 | elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? lbl Hl) |
---|
| 825 | #id #Hid @(ex_intro … id Hid) |
---|
| 826 | ] |
---|
| 827 | | (* jump_in_policy *) #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
| 828 | elim (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
| 829 | [ >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) |
---|
| 830 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le ?? Hi)) |
---|
| 831 | | >(injective_S … Hi) @conj |
---|
| 832 | [ >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n whd in match (nth ????); |
---|
| 833 | normalize nodelta in p4; cases instr in p4; |
---|
| 834 | [ #pi cases pi |
---|
| 835 | [1,2,3,6,7,33,34: #x #y #_ #H @⊥ @H |
---|
| 836 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ #H @⊥ @H |
---|
| 837 | |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta |
---|
| 838 | whd in match (jump_expansion_step_instruction ???); |
---|
| 839 | #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
| 840 | |11,12,13,16,17: #x #id normalize nodelta |
---|
| 841 | whd in match (jump_expansion_step_instruction ???); |
---|
| 842 | #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
| 843 | |35,36,37: #_ #H @⊥ @H |
---|
| 844 | ] |
---|
| 845 | |2,3: #x #_ #H @⊥ @H |
---|
| 846 | |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
| 847 | |6: #x #id #_ #H @⊥ @H |
---|
| 848 | ] |
---|
| 849 | | #H elim H -H #p #H elim H -H #a #H elim H -H #j #H |
---|
| 850 | >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?) in H; |
---|
| 851 | [ #H destruct (H) |
---|
| 852 | | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
| 853 | @le_S_S @le_plus_n_r |
---|
| 854 | ] |
---|
| 855 | ] |
---|
| 856 | ] |
---|
| 857 | ] |
---|
| 858 | | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
| 859 | elim (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
| 860 | [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi)) |
---|
| 861 | | >(injective_S … Hi) >lookup_opt_lookup_miss |
---|
| 862 | [ >lookup_opt_lookup_miss |
---|
| 863 | [ normalize nodelta %2 @refl |
---|
| 864 | | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?) |
---|
| 865 | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
| 866 | @le_S_S @le_plus_n_r |
---|
| 867 | ] |
---|
| 868 | | @(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?)) >prf |
---|
| 869 | [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r |
---|
| 870 | | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p2 |
---|
| 871 | whd in match (nth ????); normalize nodelta in p4; cases instr in p4; |
---|
| 872 | [ #pi cases pi |
---|
| 873 | [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/ |
---|
| 874 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/ |
---|
| 875 | |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta |
---|
| 876 | whd in match (jump_expansion_step_instruction ???); |
---|
| 877 | #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
| 878 | |11,12,13,16,17: #x #id normalize nodelta |
---|
| 879 | whd in match (jump_expansion_step_instruction ???); |
---|
| 880 | #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
| 881 | |35,36,37: #_ normalize /2 by nmk/ |
---|
[1614] | 882 | ] |
---|
[1809] | 883 | |2,3: #x #_ normalize /2 by nmk/ |
---|
| 884 | |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
| 885 | |6: #x #id #_ normalize /2 by nmk/ |
---|
| 886 | ] |
---|
[1614] | 887 | ] |
---|
[1809] | 888 | ] |
---|
| 889 | ] |
---|
| 890 | ] |
---|
| 891 | | (* policy_safe *) @lookup_forall #x cases x -x #x cases x -x #p #a #j #n #Hl |
---|
| 892 | @(forall_lookup … (proj2 ?? (proj1 ?? Hpolicy)) ? n Hl) |
---|
| 893 | ] |
---|
| 894 | | (* changed *) #Hc #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
| 895 | elim (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
| 896 | [ @((proj2 ?? Hpolicy) Hc i (le_S_S_to_le … Hi)) |
---|
| 897 | | >(injective_S … Hi) >lookup_opt_lookup_miss |
---|
| 898 | [ >lookup_opt_lookup_miss |
---|
| 899 | [ normalize nodelta @refl |
---|
| 900 | | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?) |
---|
| 901 | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
| 902 | @le_S_S @le_plus_n_r |
---|
| 903 | ] |
---|
| 904 | | @(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?)) >prf |
---|
| 905 | [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r |
---|
| 906 | | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p2 |
---|
| 907 | whd in match (nth ????); normalize nodelta in p4; cases instr in p4; |
---|
| 908 | [ #pi cases pi |
---|
| 909 | [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/ |
---|
| 910 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/ |
---|
| 911 | |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta |
---|
| 912 | whd in match (jump_expansion_step_instruction ???); |
---|
| 913 | #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
| 914 | |11,12,13,16,17: #x #id normalize nodelta |
---|
| 915 | whd in match (jump_expansion_step_instruction ???); |
---|
| 916 | #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
| 917 | |35,36,37: #_ normalize /2 by nmk/ |
---|
| 918 | ] |
---|
| 919 | |2,3: #x #_ normalize /2 by nmk/ |
---|
| 920 | |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
| 921 | |6: #x #id #_ normalize /2 by nmk/ |
---|
| 922 | ] |
---|
| 923 | ] |
---|
| 924 | ] |
---|
| 925 | ] |
---|
| 926 | ] |
---|
| 927 | | @conj [ @conj [ @conj [ @conj [ @conj |
---|
[1614] | 928 | [ #i #Hi // |
---|
[1809] | 929 | | // |
---|
| 930 | ] |
---|
[1614] | 931 | | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3 |
---|
| 932 | normalize in H3; destruct (H3) ] |
---|
| 933 | ] |
---|
| 934 | | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ] |
---|
[1809] | 935 | ] |
---|
| 936 | | // |
---|
| 937 | ] |
---|
| 938 | | #_ #i #Hi @⊥ @(absurd (i < 0)) [ @Hi | @not_le_Sn_O ] |
---|
| 939 | ] |
---|
| 940 | qed. |
---|
| 941 | |
---|
| 942 | (* this might be replaced by a coercion: (∀x.A x → B x) → Σx.A x → Σx.B x *) |
---|
| 943 | (* definition weaken_policy: |
---|
| 944 | ∀program,op. |
---|
| 945 | option (Σp:jump_expansion_policy. |
---|
| 946 | And (And (And (And (out_of_program_none program p) |
---|
| 947 | (labels_okay (create_label_map program op) p)) |
---|
| 948 | (jump_in_policy program p)) (policy_increase program op p)) |
---|
| 949 | (policy_safe p)) → |
---|
| 950 | option (Σp:jump_expansion_policy.And (out_of_program_none program p) |
---|
| 951 | (jump_in_policy program p)) ≝ |
---|
| 952 | λprogram.λop.λx. |
---|
| 953 | match x return λ_.option (Σp.And (out_of_program_none program p) (jump_in_policy program p)) with |
---|
| 954 | [ None ⇒ None ? |
---|
| 955 | | Some z ⇒ Some ? (mk_Sig ?? (pi1 ?? z) ?) |
---|
| 956 | ]. |
---|
| 957 | @conj |
---|
| 958 | [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? z))))) |
---|
| 959 | | @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? z)))) |
---|
[1614] | 960 | ] |
---|
[1809] | 961 | qed. *) |
---|
| 962 | |
---|
| 963 | (* This function executes n steps from the starting point. *) |
---|
[1810] | 964 | (*let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (|l|) 2^16) |
---|
| 965 | (n: ℕ) on n:(Σx:bool × ℕ × (option jump_expansion_policy). |
---|
| 966 | let 〈ch,pc,y〉 ≝ x in |
---|
[1809] | 967 | match y with |
---|
| 968 | [ None ⇒ pc > 2^16 |
---|
| 969 | | Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p) |
---|
| 970 | ]) ≝ |
---|
[1614] | 971 | match n with |
---|
[1809] | 972 | [ O ⇒ 〈0,Some ? (pi1 … (jump_expansion_start program))〉 |
---|
| 973 | | S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in |
---|
[1810] | 974 | match z return λx. z=x → Σa:bool × ℕ × (option jump_expansion_policy).? with |
---|
[1809] | 975 | [ None ⇒ λp2.〈pc,None ?〉 |
---|
| 976 | | Some op ⇒ λp2.pi1 … (jump_expansion_step program (create_label_map program op) «op,?») |
---|
| 977 | ] (refl … z) |
---|
[1810] | 978 | ].*) |
---|
| 979 | |
---|
| 980 | let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (|l|) 2^16) (n: ℕ) |
---|
| 981 | on n:(Σx:bool × ℕ × (option jump_expansion_policy). |
---|
| 982 | let 〈c,pc,y〉 ≝ x in |
---|
| 983 | match y with |
---|
| 984 | [ None ⇒ pc > 2^16 |
---|
| 985 | | Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p) |
---|
| 986 | ]) ≝ |
---|
| 987 | match n with |
---|
| 988 | [ O ⇒ 〈true,0,Some ? (pi1 ?? (jump_expansion_start program))〉 |
---|
| 989 | | S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in |
---|
| 990 | match z return λx. z=x → Σa:bool × ℕ × (option jump_expansion_policy).? with |
---|
| 991 | [ None ⇒ λp2.〈false,pc,None ?〉 |
---|
| 992 | | Some op ⇒ λp2.if ch |
---|
| 993 | then pi1 ?? (jump_expansion_step program (create_label_map program op) «op,?») |
---|
| 994 | else (jump_expansion_internal program m) |
---|
| 995 | ] (refl … z) |
---|
[1614] | 996 | ]. |
---|
[1809] | 997 | [ normalize nodelta @(proj1 ?? (pi2 ?? (jump_expansion_start program))) |
---|
[1810] | 998 | | lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / |
---|
| 999 | |3: lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / |
---|
| 1000 | | normalize nodelta cases (jump_expansion_step program (create_label_map program op) «op,?») |
---|
| 1001 | #p cases p -p #p cases p -p #p #q #r cases r normalize nodelta |
---|
| 1002 | [ #H @(proj1 ?? H) |
---|
| 1003 | | #j #H @conj |
---|
| 1004 | [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) |
---|
| 1005 | | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) |
---|
[1809] | 1006 | ] |
---|
[1810] | 1007 | ] |
---|
[1614] | 1008 | ] |
---|
| 1009 | qed. |
---|
[1810] | 1010 | |
---|
[1809] | 1011 | lemma pe_int_refl: ∀program.reflexive ? (policy_equal_int program). |
---|
| 1012 | #program whd #x whd #n #Hn |
---|
| 1013 | cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) |
---|
| 1014 | #y cases y -y #y #z normalize nodelta @refl |
---|
| 1015 | qed. |
---|
[1614] | 1016 | |
---|
[1809] | 1017 | lemma pe_int_sym: ∀program.symmetric ? (policy_equal_int program). |
---|
| 1018 | #program whd #x #y #Hxy whd #n #Hn |
---|
| 1019 | lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) |
---|
| 1020 | #z cases z -z #x1 #x2 #x3 |
---|
| 1021 | cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) |
---|
| 1022 | #z cases z -z #y1 #y2 #y3 normalize nodelta // |
---|
| 1023 | qed. |
---|
| 1024 | |
---|
| 1025 | lemma pe_int_trans: ∀program.transitive ? (policy_equal_int program). |
---|
| 1026 | #program whd #x #y #z whd in match (policy_equal_int ???); whd in match (policy_equal_int ?y ?); |
---|
| 1027 | whd in match (policy_equal_int ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy |
---|
| 1028 | lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) |
---|
| 1029 | #z cases z -z #x1 #x2 #x3 |
---|
| 1030 | cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z -z |
---|
| 1031 | #y1 #y2 #y3 |
---|
| 1032 | cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z -z |
---|
| 1033 | #z1 #z2 #z3 normalize nodelta // |
---|
| 1034 | qed. |
---|
| 1035 | |
---|
[1614] | 1036 | definition policy_equal ≝ |
---|
[1809] | 1037 | λprogram:list labelled_instruction.λp1,p2:option jump_expansion_policy. |
---|
| 1038 | match p1 with |
---|
| 1039 | [ Some x1 ⇒ match p2 with |
---|
| 1040 | [ Some x2 ⇒ policy_equal_int program x1 x2 |
---|
| 1041 | | _ ⇒ False |
---|
| 1042 | ] |
---|
| 1043 | | None ⇒ p2 = None ? |
---|
| 1044 | ]. |
---|
[1614] | 1045 | |
---|
[1809] | 1046 | lemma pe_refl: ∀program.reflexive ? (policy_equal program). |
---|
| 1047 | #program whd #x whd cases x |
---|
| 1048 | [ // |
---|
| 1049 | | #y @pe_int_refl |
---|
| 1050 | ] |
---|
[1614] | 1051 | qed. |
---|
| 1052 | |
---|
[1809] | 1053 | lemma pe_sym: ∀program.symmetric ? (policy_equal program). |
---|
| 1054 | #program whd #x #y #Hxy whd cases y in Hxy; |
---|
| 1055 | [ cases x |
---|
| 1056 | [ // |
---|
| 1057 | | #x' #H @⊥ @(absurd ? H) /2 by nmk/ |
---|
| 1058 | ] |
---|
| 1059 | | #y' cases x |
---|
| 1060 | [ #H @⊥ @(absurd ? H) whd in match (policy_equal ???); @nmk #H destruct (H) |
---|
| 1061 | | #x' #H @pe_int_sym @H |
---|
| 1062 | ] |
---|
| 1063 | ] |
---|
[1614] | 1064 | qed. |
---|
| 1065 | |
---|
[1809] | 1066 | lemma pe_trans: ∀program.transitive ? (policy_equal program). |
---|
| 1067 | #program whd #x #y #z cases x |
---|
| 1068 | [ #Hxy #Hyz >Hxy in Hyz; // |
---|
| 1069 | | #x' cases y |
---|
| 1070 | [ #H @⊥ @(absurd ? H) /2 by nmk/ |
---|
| 1071 | | #y' cases z |
---|
| 1072 | [ #_ #H @⊥ @(absurd ? H) /2 by nmk/ |
---|
| 1073 | | #z' @pe_int_trans |
---|
| 1074 | ] |
---|
| 1075 | ] |
---|
| 1076 | ] |
---|
[1614] | 1077 | qed. |
---|
| 1078 | |
---|
[1809] | 1079 | definition step_none: ∀program.∀n. |
---|
| 1080 | (\snd (pi1 ?? (jump_expansion_internal program n))) = None ? → |
---|
| 1081 | ∀k.(\snd (pi1 ?? (jump_expansion_internal program (n+k)))) = None ?. |
---|
| 1082 | #program #n lapply (refl ? (jump_expansion_internal program n)) |
---|
| 1083 | cases (jump_expansion_internal program n) in ⊢ (???% → %); |
---|
| 1084 | #x1 cases x1 #p1 #j1 -x1; #H1 #Heqj #Hj #k elim k |
---|
| 1085 | [ <plus_n_O >Heqj @Hj |
---|
[1810] | 1086 | | #k' -k <plus_n_Sm whd in match (jump_expansion_internal program (S (n+k'))); |
---|
| 1087 | lapply (refl ? (jump_expansion_internal program (n+k'))) |
---|
[1809] | 1088 | cases (jump_expansion_internal program (n+k')) in ⊢ (???% → % → %); |
---|
[1810] | 1089 | #x2 cases x2 -x2 #x2 cases x2 -x2 #c2 #p2 #j2 normalize nodelta #H #Heqj2 |
---|
[1809] | 1090 | cases j2 in H Heqj2; |
---|
| 1091 | [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??); |
---|
| 1092 | >Heqj2 normalize nodelta @refl |
---|
| 1093 | | #x #H #Heqj2 #abs destruct (abs) |
---|
| 1094 | ] |
---|
| 1095 | ] |
---|
| 1096 | qed. |
---|
| 1097 | |
---|
[1614] | 1098 | lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16). |
---|
[1809] | 1099 | ∀n.policy_equal program (\snd (pi1 ?? (jump_expansion_internal program n))) |
---|
| 1100 | (\snd (pi1 ?? (jump_expansion_internal program (S n)))) → |
---|
| 1101 | policy_equal program (\snd (pi1 ?? (jump_expansion_internal program (S n)))) |
---|
| 1102 | (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))). |
---|
| 1103 | #program #n #Heq |
---|
| 1104 | cases daemon (* XXX *) |
---|
[1614] | 1105 | qed. |
---|
| 1106 | |
---|
| 1107 | (* this is in the stdlib, but commented out, why? *) |
---|
| 1108 | theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n. |
---|
| 1109 | #n (elim n) normalize /2 by S_pred/ qed. |
---|
[1809] | 1110 | |
---|
[1614] | 1111 | lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.|l| < 2^16).∀n:ℕ. |
---|
[1809] | 1112 | policy_equal program (\snd (pi1 … (jump_expansion_internal program n))) |
---|
| 1113 | (\snd (pi1 … (jump_expansion_internal program (S n)))) → |
---|
| 1114 | ∀k.k ≥ n → policy_equal program (\snd (pi1 … (jump_expansion_internal program n))) |
---|
| 1115 | (\snd (pi1 … (jump_expansion_internal program k))). |
---|
| 1116 | #program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k; |
---|
| 1117 | lapply Heq -Heq; lapply n -n; elim z -z; |
---|
| 1118 | [ #n #Heq <plus_n_O @pe_refl |
---|
| 1119 | | #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z); |
---|
| 1120 | @(pe_trans … (\snd (pi1 … (jump_expansion_internal program (S n))))) |
---|
| 1121 | [ @Heq |
---|
| 1122 | | @Hind @pe_step @Heq |
---|
| 1123 | ] |
---|
| 1124 | ] |
---|
[1614] | 1125 | qed. |
---|
| 1126 | |
---|
[1809] | 1127 | (* this number monotonically increases over iterations, maximum 2*|program| *) |
---|
[1614] | 1128 | let rec measure_int (program: list labelled_instruction) (policy: jump_expansion_policy) (acc: ℕ) |
---|
| 1129 | on program: ℕ ≝ |
---|
| 1130 | match program with |
---|
| 1131 | [ nil ⇒ acc |
---|
[1809] | 1132 | | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,00 |
---|
| 1133 | ,short_jump〉)) with |
---|
[1614] | 1134 | [ long_jump ⇒ measure_int t policy (acc + 2) |
---|
| 1135 | | medium_jump ⇒ measure_int t policy (acc + 1) |
---|
| 1136 | | _ ⇒ measure_int t policy acc |
---|
| 1137 | ] |
---|
| 1138 | ]. |
---|
| 1139 | |
---|
| 1140 | lemma measure_plus: ∀program.∀policy.∀x,d:ℕ. |
---|
[1809] | 1141 | measure_int program policy (x+d) = measure_int program policy x + d. |
---|
| 1142 | #program #policy #x #d generalize in match x; -x elim d |
---|
| 1143 | [ // |
---|
| 1144 | | -d; #d #Hind elim program |
---|
| 1145 | [ / by refl/ |
---|
| 1146 | | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x); |
---|
| 1147 | cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) |
---|
| 1148 | [ normalize nodelta @Hd |
---|
| 1149 | |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus |
---|
| 1150 | @Hd |
---|
| 1151 | ] |
---|
| 1152 | ] |
---|
| 1153 | ] |
---|
[1614] | 1154 | qed. |
---|
[1809] | 1155 | |
---|
| 1156 | lemma measure_le: ∀program.∀policy. |
---|
| 1157 | measure_int program policy 0 ≤ 2*|program|. |
---|
| 1158 | #program #policy elim program |
---|
| 1159 | [ normalize @le_n |
---|
| 1160 | | #h #t #Hind whd in match (measure_int ???); |
---|
| 1161 | cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) |
---|
| 1162 | [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/ |
---|
| 1163 | |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?) |
---|
| 1164 | @le_plus [1,3: @Hind |2,4: // ] |
---|
| 1165 | ] |
---|
| 1166 | ] |
---|
| 1167 | qed. |
---|
| 1168 | |
---|
[1614] | 1169 | lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16. |
---|
| 1170 | ∀policy:Σp:jump_expansion_policy. |
---|
[1809] | 1171 | out_of_program_none program p ∧ jump_in_policy program p. |
---|
| 1172 | ∀l.|l| ≤ |program| → ∀acc:ℕ. |
---|
| 1173 | match \snd (jump_expansion_step program (create_label_map program policy) policy) with |
---|
| 1174 | [ None ⇒ True |
---|
| 1175 | | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc |
---|
| 1176 | ]. |
---|
[1614] | 1177 | #program #policy #l elim l -l; |
---|
[1809] | 1178 | [ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ] |
---|
| 1179 | | #h #t #Hind #Hp #acc |
---|
| 1180 | lapply (refl ? (jump_expansion_step program (create_label_map program policy) policy)) |
---|
[1810] | 1181 | cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #pi1 cases pi1 |
---|
| 1182 | #p #q #r -pi1; cases r |
---|
[1809] | 1183 | [ // |
---|
[1810] | 1184 | | #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? Hx)) (|t|) Hp) |
---|
[1809] | 1185 | whd in match (measure_int ???); whd in match (measure_int ? x ?); |
---|
| 1186 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉) |
---|
| 1187 | #z cases z -z #x1 #x2 #x3 |
---|
| 1188 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) x 〈0,0,short_jump〉) |
---|
| 1189 | #z cases z -z #y1 #y2 #y3 |
---|
[1614] | 1190 | normalize nodelta #Hj cases Hj |
---|
| 1191 | [ cases x3 cases y3 |
---|
| 1192 | [1,4,5,7,8,9: #H @⊥ @H |
---|
| 1193 | |2,3,6: #_ normalize nodelta |
---|
[1809] | 1194 | [1,2: @(transitive_le ? (measure_int t x acc)) |
---|
| 1195 | |3: @(transitive_le ? (measure_int t x (acc+1))) |
---|
[1614] | 1196 | ] |
---|
[1810] | 1197 | [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/] |
---|
[1809] | 1198 | >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn |
---|
| 1199 | ] |
---|
| 1200 | | #Heq >Heq cases y3 normalize nodelta |
---|
[1810] | 1201 | [2,3: >measure_plus >measure_plus @le_plus / by le_n/] |
---|
[1809] | 1202 | >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn |
---|
| 1203 | ] |
---|
[1614] | 1204 | ] |
---|
[1809] | 1205 | ] |
---|
[1614] | 1206 | qed. |
---|
| 1207 | |
---|
| 1208 | (* these lemmas seem superfluous, but not sure how *) |
---|
| 1209 | lemma bla: ∀a,b:ℕ.a + a = b + b → a = b. |
---|
| 1210 | #a elim a |
---|
[1809] | 1211 | [ normalize #b // |
---|
[1614] | 1212 | | -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ | -b #b normalize |
---|
| 1213 | <plus_n_Sm <plus_n_Sm #H |
---|
| 1214 | >(Hind b (injective_S ?? (injective_S ?? H))) // ] |
---|
| 1215 | ] |
---|
| 1216 | qed. |
---|
| 1217 | |
---|
| 1218 | lemma sth_not_s: ∀x.x ≠ S x. |
---|
| 1219 | #x cases x |
---|
| 1220 | [ // | #y // ] |
---|
| 1221 | qed. |
---|
[1809] | 1222 | |
---|
[1614] | 1223 | lemma measure_full: ∀program.∀policy. |
---|
| 1224 | measure_int program policy 0 = 2*|program| → ∀i.i<|program| → |
---|
| 1225 | (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,0,short_jump〉)) = long_jump. |
---|
[1809] | 1226 | #program #policy elim program |
---|
| 1227 | [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
| 1228 | | #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|) |
---|
| 1229 | [ whd in match (measure_int ???) in Hm; |
---|
| 1230 | cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm; |
---|
| 1231 | normalize nodelta |
---|
| 1232 | [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/ |
---|
| 1233 | | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy)) |
---|
| 1234 | <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize |
---|
| 1235 | >(commutative_plus (|t|) 0) <plus_O_n <minus_n_O |
---|
| 1236 | >plus_n_Sm @le_n |
---|
| 1237 | | >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) // |
---|
| 1238 | ] |
---|
| 1239 | | #Hmt cases (le_to_or_lt_eq … Hi) -Hi; |
---|
| 1240 | [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi)) |
---|
| 1241 | | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; |
---|
| 1242 | cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm; |
---|
| 1243 | normalize nodelta |
---|
| 1244 | [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|))) |
---|
| 1245 | >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s |
---|
| 1246 | | >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize |
---|
| 1247 | #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s |
---|
| 1248 | | #_ // |
---|
| 1249 | ] |
---|
| 1250 | ]] |
---|
| 1251 | ] |
---|
[1614] | 1252 | qed. |
---|
| 1253 | |
---|
| 1254 | lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16). |
---|
| 1255 | ∀policy:Σp:jump_expansion_policy. |
---|
[1809] | 1256 | out_of_program_none program p ∧ jump_in_policy program p. |
---|
| 1257 | match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy))) with |
---|
| 1258 | [ None ⇒ True |
---|
| 1259 | | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_equal_int program policy p ]. |
---|
| 1260 | #program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy))) |
---|
| 1261 | cases (jump_expansion_step program (create_label_map program policy) policy) in ⊢ (???% → %); |
---|
[1810] | 1262 | #p cases p -p #p cases p -p #ch #pc #pol normalize nodelta cases pol |
---|
[1809] | 1263 | [ // |
---|
| 1264 | | #p normalize nodelta #Hpol #eqpol lapply (le_n (|program|)) |
---|
| 1265 | @(list_ind ? (λx.|x| ≤ |pi1 ?? program| → |
---|
| 1266 | measure_int x policy 0 = measure_int x p 0 → |
---|
| 1267 | policy_equal_int x policy p) ?? (pi1 ?? program)) |
---|
| 1268 | [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O |
---|
[1614] | 1269 | | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi; |
---|
| 1270 | [ #Hi @Hind |
---|
| 1271 | [ @(transitive_le … Hp) // |
---|
[1809] | 1272 | | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; |
---|
[1810] | 1273 | lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpol)) (|t|) Hp) |
---|
[1809] | 1274 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm; |
---|
[1614] | 1275 | #x cases x -x #x1 #x2 #x3 |
---|
| 1276 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉); |
---|
| 1277 | #y cases y -y #y1 #y2 #y3 |
---|
[1809] | 1278 | cases x3 cases y3 normalize nodelta |
---|
| 1279 | [1: #H #_ @H |
---|
| 1280 | |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt |
---|
| 1281 | lapply (measure_incr_or_equal program policy t ? 0) |
---|
[1810] | 1282 | [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / |
---|
[1614] | 1283 | |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ] |
---|
[1809] | 1284 | |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1) |
---|
| 1285 | #H #_ @(injective_plus_r … H) |
---|
[1614] | 1286 | |6: >measure_plus >measure_plus |
---|
| 1287 | change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) |
---|
| 1288 | #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l |
---|
[1809] | 1289 | lapply (measure_incr_or_equal program policy t ? 0) |
---|
[1810] | 1290 | [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / |
---|
[1809] | 1291 | |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2) |
---|
| 1292 | #H #_ @(injective_plus_r … H) |
---|
[1614] | 1293 | ] |
---|
[1809] | 1294 | | @(le_S_S_to_le … Hi) |
---|
[1614] | 1295 | ] |
---|
[1809] | 1296 | | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; |
---|
| 1297 | whd in match (measure_int ? p ?) in Hm; |
---|
[1810] | 1298 | lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpol)) (|t|) Hp) |
---|
[1809] | 1299 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in |
---|
| 1300 | Hm; |
---|
| 1301 | #x cases x -x #x1 #x2 #x3 |
---|
| 1302 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉); |
---|
| 1303 | #y cases y -y #y1 #y2 #y3 |
---|
| 1304 | normalize nodelta cases x3 cases y3 normalize nodelta |
---|
| 1305 | [1,5,9: #_ #_ // |
---|
| 1306 | |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ] |
---|
| 1307 | |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt |
---|
| 1308 | lapply (measure_incr_or_equal program policy t ? 0) |
---|
| 1309 | [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / |
---|
| 1310 | |6: >measure_plus >measure_plus |
---|
| 1311 | change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) |
---|
| 1312 | #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l |
---|
| 1313 | lapply (measure_incr_or_equal program policy t ? 0) |
---|
| 1314 | [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / |
---|
| 1315 | ] |
---|
[1614] | 1316 | ] |
---|
[1809] | 1317 | ] |
---|
[1614] | 1318 | qed. |
---|
| 1319 | |
---|
[1809] | 1320 | lemma le_to_eq_plus: ∀n,z. |
---|
| 1321 | n ≤ z → ∃k.z = n + k. |
---|
| 1322 | #n #z elim z |
---|
| 1323 | [ #H cases (le_to_or_lt_eq … H) |
---|
| 1324 | [ #H2 @⊥ @(absurd … H2) @not_le_Sn_O |
---|
| 1325 | | #H2 @(ex_intro … 0) >H2 // |
---|
| 1326 | ] |
---|
| 1327 | | #z' #Hind #H cases (le_to_or_lt_eq … H) |
---|
| 1328 | [ #H' elim (Hind (le_S_S_to_le … H')) #k' #H2 @(ex_intro … (S k')) |
---|
| 1329 | >H2 >plus_n_Sm // |
---|
| 1330 | | #H' @(ex_intro … 0) >H' // |
---|
| 1331 | ] |
---|
| 1332 | ] |
---|
| 1333 | qed. |
---|
| 1334 | |
---|
[1614] | 1335 | lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16. |
---|
[1809] | 1336 | |l| ≤ |program| → measure_int l (jump_expansion_start program) 0 = 0. |
---|
| 1337 | #l #program elim l |
---|
[1614] | 1338 | [ // |
---|
| 1339 | | #h #t #Hind #Hp whd in match (measure_int ???); |
---|
| 1340 | cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj |
---|
| 1341 | [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,0,short_jump〉) |
---|
| 1342 | [ normalize nodelta @Hind @le_S_to_le ] |
---|
| 1343 | @Hp |
---|
[1809] | 1344 | | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (pi1 ?? (jump_expansion_start program)) (|t|) ?) Hj) 〈0,0,short_jump〉) |
---|
| 1345 | [ normalize nodelta @Hind @le_S_to_le @Hp |
---|
| 1346 | | @Hp |
---|
| 1347 | | % |
---|
| 1348 | [ @(proj1 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program)))) |
---|
| 1349 | | @(proj2 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program)))) |
---|
[1614] | 1350 | ] |
---|
| 1351 | ] |
---|
| 1352 | ] |
---|
| 1353 | ] |
---|
| 1354 | qed. |
---|
| 1355 | |
---|
[1809] | 1356 | (* the actual computation of the fixpoint *) |
---|
| 1357 | definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16). |
---|
| 1358 | Σp:option jump_expansion_policy.∃n.∀k.n < k → |
---|
| 1359 | policy_equal program (\snd (pi1 ?? (jump_expansion_internal program k))) p. |
---|
| 1360 | #program @(\snd (pi1 ?? (jump_expansion_internal program (2*|program|)))) |
---|
| 1361 | cases (dec_bounded_exists (λk.policy_equal (pi1 ?? program) |
---|
| 1362 | (\snd (pi1 ?? (jump_expansion_internal program k))) |
---|
| 1363 | (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|)) |
---|
[1810] | 1364 | [ #Hex elim Hex -Hex #x #Hx @(ex_intro … x) #k #Hk |
---|
| 1365 | @pe_trans |
---|
[1809] | 1366 | [ @(\snd (pi1 ?? (jump_expansion_internal program x))) |
---|
| 1367 | | @pe_sym @equal_remains_equal |
---|
| 1368 | [ @(proj2 ?? Hx) |
---|
[1810] | 1369 | | @le_S_S_to_le @le_S @Hk |
---|
[1809] | 1370 | ] |
---|
| 1371 | | @equal_remains_equal |
---|
| 1372 | [ @(proj2 ?? Hx) |
---|
| 1373 | | @le_S_S_to_le @le_S @(proj1 ?? Hx) |
---|
| 1374 | ] |
---|
| 1375 | ] |
---|
[1810] | 1376 | | #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @(ex_intro … (2*|program|)) #k #Hk |
---|
| 1377 | @pe_sym @equal_remains_equal |
---|
[1809] | 1378 | [ lapply (refl ? (jump_expansion_internal program (2*|program|))) |
---|
| 1379 | cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %); |
---|
[1810] | 1380 | #x cases x -x #x cases x #Fch #Fpc #Fpol normalize nodelta #HFpol cases Fpol in HFpol; |
---|
| 1381 | [ (* if we're at None in 2*|program|, we're at None in S 2*|program| too *) |
---|
| 1382 | #HFpol #EQ whd in match (jump_expansion_internal ??); >EQ |
---|
| 1383 | normalize nodelta // |
---|
| 1384 | | #Fp #HFp #EQ whd in match (jump_expansion_internal ??); |
---|
| 1385 | >EQ normalize nodelta |
---|
| 1386 | lapply (refl ? (jump_expansion_step program (create_label_map program Fp) «Fp,?»)) |
---|
| 1387 | [ @HFp |
---|
| 1388 | | lapply (measure_full program Fp ?) |
---|
| 1389 | [ @le_to_le_to_eq |
---|
| 1390 | [ @measure_le |
---|
| 1391 | | (* XXX *) cases daemon |
---|
| 1392 | ] |
---|
| 1393 | | #Hfull cases (jump_expansion_step program (create_label_map program Fp) «Fp,?») in ⊢ (???% → %); |
---|
| 1394 | #x cases x -x #x cases x -x #Gch #Gpc #Gpol cases Gpol normalize nodelta |
---|
| 1395 | [ #H #EQ2 @⊥ @(absurd ?? (proj2 ?? H)) @Hfull |
---|
| 1396 | | #Gp #HGp #EQ2 cases Fch |
---|
| 1397 | [ normalize nodelta #i #Hi |
---|
| 1398 | lapply (refl ? (lookup ?? (bitvector_of_nat 16 i) Fp 〈0,0,short_jump〉)) |
---|
| 1399 | cases (lookup ?? (bitvector_of_nat 16 i) Fp 〈0,0,short_jump〉) in ⊢ (???% → %); |
---|
| 1400 | #x cases x -x #p #a #j normalize nodelta #H |
---|
| 1401 | lapply (proj2 ?? (proj1 ?? (proj1 ?? HGp)) i Hi) lapply (Hfull i Hi) >H |
---|
| 1402 | #H2 >H2 normalize nodelta cases (lookup ?? (bitvector_of_nat 16 i) Gp 〈0,0,short_jump\rangle) |
---|
| 1403 | #x cases x -x #p #a #j' cases j' normalize nodelta #H elim H -H #H |
---|
| 1404 | [1,3: @⊥ @H |
---|
| 1405 | |2,4: destruct (H) |
---|
| 1406 | |5,6: @refl |
---|
[1809] | 1407 | ] |
---|
[1810] | 1408 | | normalize nodelta /2 by pe_int_refl/ |
---|
[1809] | 1409 | ] |
---|
| 1410 | ] |
---|
[1810] | 1411 | ] |
---|
[1809] | 1412 | ] |
---|
| 1413 | ] |
---|
[1810] | 1414 | | @le_S_S_to_le @le_S @Hk |
---|
[1809] | 1415 | ] |
---|
[1810] | 1416 | | #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n)) |
---|
| 1417 | #x cases x -x #x cases x -x #nch #npc #npol normalize nodelta #Hnpol |
---|
| 1418 | #x cases x -x #x cases x -x #Sch #Scp #Spol normalize nodelta #HSpol |
---|
| 1419 | cases npol in Hnpol; cases Spol in HSpol; |
---|
| 1420 | [ #Hnpol #HSpol %1 // |
---|
| 1421 | |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal ???); // |
---|
| 1422 | #H destruct (H) |
---|
| 1423 | |4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); @dec_bounded_forall #m |
---|
[1809] | 1424 | cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉) |
---|
| 1425 | #x cases x -x #x1 #x2 #x3 |
---|
| 1426 | cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉) |
---|
| 1427 | #y cases y -y #y1 #y2 #y3 normalize nodelta |
---|
| 1428 | @dec_eq_jump_length |
---|
| 1429 | ] |
---|
| 1430 | ] |
---|
[1810] | 1431 | qed. |
---|
[1809] | 1432 | |
---|
| 1433 | (* Take a policy of 〈pc, addr, jump_length〉 tuples, and transform it into |
---|
| 1434 | * a map from pc to jump_length. This cannot be done earlier because the pc |
---|
| 1435 | * changes between iterations. *) |
---|
[1614] | 1436 | let rec transform_policy (n: nat) policy (acc: BitVectorTrie jump_length 16) on n: |
---|
| 1437 | BitVectorTrie jump_length 16 ≝ |
---|
| 1438 | match n with |
---|
| 1439 | [ O ⇒ acc |
---|
| 1440 | | S n' ⇒ |
---|
| 1441 | match lookup_opt … (bitvector_of_nat 16 n') policy with |
---|
| 1442 | [ None ⇒ transform_policy n' policy acc |
---|
| 1443 | | Some x ⇒ let 〈pc,length〉 ≝ x in |
---|
| 1444 | transform_policy n' policy (insert … pc length acc) |
---|
| 1445 | ] |
---|
| 1446 | ]. |
---|
[1615] | 1447 | |
---|
[1809] | 1448 | (* The glue between Policy and Assembly. *) |
---|
[1615] | 1449 | definition jump_expansion': |
---|
| 1450 | ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16). |
---|
[1810] | 1451 | ∀lookup_labels.policy_type lookup_labels ≝ |
---|
| 1452 | λprogram.λlookup_labels.λpc. |
---|
[1615] | 1453 | let policy ≝ |
---|
| 1454 | transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in |
---|
[1810] | 1455 | (* here we must use jump_length_ok *) |
---|
| 1456 | bvt_lookup ? ? pc policy long_jump. |
---|
[1615] | 1457 | /2 by Stub, mk_Sig/ |
---|
| 1458 | qed. |
---|