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