[2034] | 1 | include "ASM/PolicyFront.ma". |
---|
| 2 | include alias "basics/lists/list.ma". |
---|
| 3 | include alias "arithmetics/nat.ma". |
---|
| 4 | include alias "basics/logic.ma". |
---|
| 5 | |
---|
[2243] | 6 | lemma not_is_jump_to_destination_of_None: |
---|
[2225] | 7 | ∀pi. ¬is_jump (Instruction pi) → destination_of pi = None …. |
---|
| 8 | * try (#x #y #H) try (#y #H) try #H cases H % |
---|
| 9 | qed. |
---|
| 10 | |
---|
[2243] | 11 | lemma destination_of_None_to_is_jump_false: |
---|
| 12 | ∀instr. destination_of instr = None … → is_jump' instr = false. |
---|
| 13 | * normalize // try (#H1 #H2 #abs) try (#H1 #abs) destruct(abs) |
---|
| 14 | qed. |
---|
| 15 | |
---|
| 16 | lemma destination_of_Some_to_is_jump_true: |
---|
| 17 | ∀instr,dst. destination_of instr = Some … dst → is_jump' instr = true. |
---|
| 18 | #instr #dst cases instr normalize // try (#H1 #H2 #abs) try (#H1 #abs) try #abs |
---|
| 19 | destruct(abs) |
---|
| 20 | qed. |
---|
| 21 | |
---|
[2215] | 22 | lemma jump_expansion_step1: |
---|
[2225] | 23 | ∀prefix: list labelled_instruction. S (|prefix|) < 2^16 → |prefix| < 2^16 → (*redundant*) |
---|
[2215] | 24 | ∀labels: label_map. |
---|
| 25 | ∀old_sigma : ppc_pc_map. |
---|
| 26 | ∀inc_added : ℕ. |
---|
| 27 | ∀inc_pc_sigma : ppc_pc_map. |
---|
| 28 | ∀label : (option Identifier). |
---|
| 29 | ∀instr : pseudo_instruction. |
---|
| 30 | ∀inc_pc : ℕ. |
---|
| 31 | ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16). |
---|
| 32 | ∀old_length : jump_length. |
---|
| 33 | ∀Hpolicy : not_jump_default prefix 〈inc_pc,inc_sigma〉. |
---|
| 34 | ∀policy : ppc_pc_map. |
---|
| 35 | ∀new_length : jump_length. |
---|
| 36 | ∀isize : ℕ. |
---|
| 37 | let add_instr ≝ match instr with |
---|
[2316] | 38 | [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j) |
---|
| 39 | | Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c) |
---|
| 40 | | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma (|prefix|) i |
---|
[2215] | 41 | | _ ⇒ None ? |
---|
| 42 | ] in |
---|
| 43 | ∀Heq1 : |
---|
| 44 | match add_instr with |
---|
| 45 | [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 |
---|
| 46 | |Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉] |
---|
| 47 | =〈new_length,isize〉. |
---|
| 48 | ∀Heq2 : |
---|
| 49 | 〈inc_pc+isize, |
---|
| 50 | insert … (bitvector_of_nat … (S (|prefix|))) |
---|
| 51 | 〈inc_pc+isize, \snd (lookup … (bitvector_of_nat … (S (|prefix|))) (\snd old_sigma) 〈O,short_jump〉)〉 |
---|
| 52 | (insert … (bitvector_of_nat … (|prefix|)) 〈inc_pc,new_length〉 inc_sigma)〉 |
---|
| 53 | = policy. |
---|
| 54 | not_jump_default (prefix@[〈label,instr〉]) policy. |
---|
[2225] | 55 | #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc |
---|
| 56 | #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2 |
---|
[2215] | 57 | #i >append_length <commutative_plus #Hi normalize in Hi; |
---|
| 58 | cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
| 59 | [ <Heq2 >lookup_insert_miss |
---|
| 60 | [ >lookup_insert_miss |
---|
| 61 | [ >(nth_append_first ? i prefix ?? Hi) |
---|
| 62 | @(Hpolicy i Hi) |
---|
[2225] | 63 | | @bitvector_of_nat_abs try assumption |
---|
| 64 | [ @(transitive_lt ??? Hi) assumption ] |
---|
| 65 | @lt_to_not_eq @Hi |
---|
[2215] | 66 | ] |
---|
[2225] | 67 | | @bitvector_of_nat_abs try assumption |
---|
| 68 | [ @(transitive_lt ??? Hi) assumption ] |
---|
| 69 | @lt_to_not_eq @le_S @Hi |
---|
[2215] | 70 | ] |
---|
| 71 | | <Heq2 >Hi >lookup_insert_miss |
---|
| 72 | [ >lookup_insert_hit cases instr in Heq1; |
---|
[3039] | 73 | [2,3: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl |
---|
| 74 | |5,7: #x #y #z normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ % |
---|
| 75 | |4,6: #x normalize nodelta #Heq1 >nth_append_second try % |
---|
[2225] | 76 | <minus_n_n #abs cases abs |
---|
| 77 | |1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); |
---|
[2316] | 78 | #H #non_jump whd in match (jump_expansion_step_instruction ?????) in H; |
---|
[2243] | 79 | >not_is_jump_to_destination_of_None in H; normalize nodelta // ] |
---|
[2225] | 80 | | @bitvector_of_nat_abs [3: // | @le_S_to_le ] assumption ]] |
---|
[2215] | 81 | qed. |
---|
| 82 | |
---|
[2225] | 83 | lemma jump_expansion_step2: |
---|
| 84 | ∀prefix: list labelled_instruction. S (|prefix|) < 2^16 → |prefix| < 2^16 → (*redundant*) |
---|
| 85 | ∀labels : label_map. |
---|
| 86 | ∀old_sigma : ppc_pc_map. |
---|
| 87 | ∀inc_pc : ℕ. |
---|
| 88 | ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16). |
---|
| 89 | ∀Hpolicy1 : |
---|
| 90 | \fst (lookup … (bitvector_of_nat … O) inc_sigma 〈O,short_jump〉) = O. |
---|
| 91 | ∀Hpolicy2: |
---|
| 92 | inc_pc =\fst (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉). |
---|
| 93 | ∀policy : ppc_pc_map. |
---|
| 94 | ∀new_length : jump_length. |
---|
| 95 | ∀isize : ℕ. |
---|
| 96 | ∀Heq2 : |
---|
| 97 | 〈inc_pc+isize, |
---|
| 98 | insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 99 | 〈inc_pc+isize, |
---|
| 100 | \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 101 | (\snd old_sigma) 〈O,short_jump〉)〉 |
---|
| 102 | (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) |
---|
| 103 | 〈inc_pc,new_length〉 inc_sigma)〉 |
---|
| 104 | = policy. |
---|
| 105 | \fst (lookup … (bitvector_of_nat … O) (\snd policy) 〈O,short_jump〉) = O. |
---|
| 106 | #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_pc |
---|
| 107 | #inc_sigma #Hpolicy1 #Hpolicy2 #policy #new_length #isize #Heq2 |
---|
| 108 | <Heq2 >lookup_insert_miss |
---|
| 109 | [ cases (decidable_eq_nat 0 (|prefix|)) |
---|
| 110 | [ #Heq <Heq >lookup_insert_hit >Hpolicy2 <Heq @Hpolicy1 |
---|
| 111 | | #Hneq >lookup_insert_miss |
---|
| 112 | [ @Hpolicy1 |
---|
| 113 | | @bitvector_of_nat_abs try assumption @lt_O_S ]] |
---|
| 114 | | @bitvector_of_nat_abs [ @lt_O_S | @prefix_ok1 | 3: @lt_to_not_eq @lt_O_S ] ] |
---|
| 115 | qed. |
---|
| 116 | |
---|
| 117 | lemma jump_expansion_step3: |
---|
[2237] | 118 | ∀program. |
---|
| 119 | ∀labels : label_map. |
---|
| 120 | ∀old_sigma : Σpolicy:ppc_pc_map.not_jump_default program policy. |
---|
| 121 | ∀prefix,x,tl. program=prefix@[x]@tl → |
---|
[2316] | 122 | (* ∀inc_added : ℕ. *) |
---|
[2237] | 123 | ∀inc_pc_sigma : ppc_pc_map. |
---|
[2225] | 124 | ∀label : option Identifier. |
---|
[2236] | 125 | ∀instr : pseudo_instruction. |
---|
[2237] | 126 | ∀p1 : x≃〈label,instr〉. |
---|
[2236] | 127 | ∀inc_pc : ℕ. |
---|
[2237] | 128 | ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16). |
---|
[2236] | 129 | ∀old_pc : ℕ. |
---|
| 130 | ∀old_length : jump_length. |
---|
| 131 | ∀Holdeq : |
---|
| 132 | lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd old_sigma) |
---|
[2237] | 133 | 〈O,short_jump〉 =〈old_pc,old_length〉. |
---|
| 134 | ∀Hpolicy : jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉. |
---|
[2225] | 135 | ∀policy : ppc_pc_map. |
---|
[2236] | 136 | ∀new_length : jump_length. |
---|
| 137 | ∀isize : ℕ. |
---|
| 138 | ∀Heq1 : |
---|
| 139 | match |
---|
[2225] | 140 | match instr |
---|
| 141 | in pseudo_instruction |
---|
| 142 | return λ_:pseudo_instruction.(option jump_length) |
---|
| 143 | with |
---|
| 144 | [Instruction (i:(preinstruction Identifier))⇒ |
---|
[2316] | 145 | jump_expansion_step_instruction labels old_sigma inc_pc_sigma |
---|
[2225] | 146 | (|prefix|) i |
---|
| 147 | |Comment (_:String)⇒None jump_length |
---|
| 148 | |Cost (_:costlabel)⇒None jump_length |
---|
[2714] | 149 | |Jnz _ _ _ ⇒ None ? |
---|
[2225] | 150 | |Jmp (j:Identifier)⇒ |
---|
| 151 | Some jump_length |
---|
[2316] | 152 | (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j) |
---|
[2225] | 153 | |Call (c:Identifier)⇒ |
---|
| 154 | Some jump_length |
---|
[2316] | 155 | (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c) |
---|
[3039] | 156 | |Mov _ _ _ ⇒ None jump_length] |
---|
[2225] | 157 | in option |
---|
[2236] | 158 | return λ_:(option jump_length).(jump_length×ℕ) |
---|
[2225] | 159 | with |
---|
| 160 | [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 |
---|
| 161 | |Some (pl:jump_length)⇒ |
---|
| 162 | 〈max_length old_length pl, |
---|
| 163 | instruction_size_jmplen (max_length old_length pl) instr〉] |
---|
[2236] | 164 | =〈new_length,isize〉. |
---|
| 165 | ∀prefix_ok1 : S (|prefix|)< 2 \sup 16. |
---|
[2237] | 166 | ∀prefix_ok : |prefix|< 2 \sup 16. |
---|
[2236] | 167 | ∀Heq2b : |
---|
| 168 | 〈inc_pc+isize, |
---|
[2225] | 169 | insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 170 | 〈inc_pc+isize, |
---|
| 171 | \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 172 | (\snd old_sigma) 〈O,short_jump〉)〉 |
---|
| 173 | (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) |
---|
| 174 | 〈inc_pc,new_length〉 inc_sigma)〉 |
---|
[2236] | 175 | =policy. |
---|
[2225] | 176 | jump_increase (prefix@[〈label,instr〉]) old_sigma policy. |
---|
[2316] | 177 | #program #labels #old_sigma #prefix #x #tl #prf #inc_pc_sigma #label |
---|
[2236] | 178 | #instr #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy #policy #new_length |
---|
| 179 | #isize #Heq1 #prefix_ok1 #prefix_ok #Heq2 |
---|
[2225] | 180 | #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
| 181 | cases (le_to_or_lt_eq … Hi) -Hi; #Hi |
---|
| 182 | [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
| 183 | [ (* USE[pass]: jump_increase *) |
---|
[2236] | 184 | lapply (Hpolicy i (le_S_to_le … Hi)) |
---|
| 185 | <Heq2 |
---|
[2225] | 186 | @pair_elim #opc #oj #EQ1 >lookup_insert_miss |
---|
| 187 | [ >lookup_insert_miss |
---|
| 188 | [ @pair_elim #pc #j #EQ2 #X @X |
---|
| 189 | | @bitvector_of_nat_abs |
---|
| 190 | [ @(transitive_lt ??? Hi) ] |
---|
[2236] | 191 | [1,2: assumption |
---|
[2225] | 192 | | @lt_to_not_eq @Hi |
---|
| 193 | ] |
---|
| 194 | ] |
---|
| 195 | | @bitvector_of_nat_abs |
---|
| 196 | [ @(transitive_lt ??? Hi) @le_S_to_le ] |
---|
[2236] | 197 | [1,2: assumption |
---|
[2225] | 198 | | @lt_to_not_eq @le_S @Hi |
---|
| 199 | ] |
---|
| 200 | ] |
---|
[2236] | 201 | | >Hi <Heq2 >Holdeq normalize nodelta |
---|
| 202 | cut (|prefix| < |program|) |
---|
| 203 | [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r ] #lt_prefix_program |
---|
[2225] | 204 | >lookup_insert_miss |
---|
[2237] | 205 | [ >lookup_insert_hit normalize nodelta |
---|
| 206 | inversion instr in Heq1; normalize nodelta |
---|
[3039] | 207 | [4,6: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length |
---|
[2237] | 208 | | #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta |
---|
| 209 | lapply (destination_of_None_to_is_jump_false pi) |
---|
| 210 | lapply (destination_of_Some_to_is_jump_true pi) |
---|
| 211 | cases (destination_of ?) normalize nodelta |
---|
| 212 | [ #tgt #Hx |
---|
| 213 | | #tgt #_ #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length |
---|
[2225] | 214 | ] |
---|
[3039] | 215 | |5,7: #x #y #z #Heqi |
---|
| 216 | |2,3: #x [3: #y] #Heqi ] |
---|
[2237] | 217 | #Hj <(proj1 ?? (pair_destruct ?????? Hj)) |
---|
| 218 | lapply (pi2 ?? old_sigma (|prefix|) ??) try assumption |
---|
[2714] | 219 | [1,3,5,7,9,11: >prf >nth_append_second try @le_n |
---|
[2237] | 220 | <minus_n_n whd in match (nth ????); >p1 >Heqi |
---|
| 221 | whd in match is_jump; normalize nodelta try % >Hx % |
---|
| 222 | |*: >Holdeq #EQ2 >EQ2 %2 %] |
---|
[2225] | 223 | | @bitvector_of_nat_abs |
---|
| 224 | [ @le_S_to_le ] |
---|
[2236] | 225 | [1,2: assumption |
---|
[2225] | 226 | | @lt_to_not_eq @le_n |
---|
| 227 | ] |
---|
| 228 | ] |
---|
| 229 | ] |
---|
[2236] | 230 | | <Heq2 >Hi >lookup_insert_hit |
---|
[2225] | 231 | normalize nodelta |
---|
| 232 | cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉) |
---|
| 233 | #a #b normalize nodelta %2 @refl |
---|
| 234 | ] |
---|
[2236] | 235 | qed. |
---|
[2225] | 236 | |
---|
[2239] | 237 | lemma jump_expansion_step4: |
---|
| 238 | ∀labels : label_map. |
---|
| 239 | ∀old_sigma : ppc_pc_map. |
---|
| 240 | ∀prefix : list (option Identifier×pseudo_instruction). |
---|
| 241 | ∀inc_added : ℕ. |
---|
| 242 | ∀inc_pc_sigma : ppc_pc_map. |
---|
| 243 | ∀label : option Identifier. |
---|
| 244 | ∀instr : pseudo_instruction. |
---|
| 245 | ∀inc_pc : ℕ. |
---|
| 246 | ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16. |
---|
| 247 | ∀old_length : jump_length. |
---|
| 248 | ∀Hpolicy1 : sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉. |
---|
| 249 | ∀Hpolicy2: inc_pc |
---|
| 250 | =\fst (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma |
---|
| 251 | 〈O,short_jump〉). |
---|
| 252 | ∀Hpolicy3: out_of_program_none prefix 〈inc_pc,inc_sigma〉. |
---|
| 253 | ∀policy : ppc_pc_map. |
---|
| 254 | ∀new_length : jump_length. |
---|
| 255 | ∀isize : ℕ. |
---|
| 256 | ∀Heq1 : |
---|
| 257 | match |
---|
| 258 | match instr |
---|
| 259 | in pseudo_instruction |
---|
| 260 | return λ_:pseudo_instruction.(option jump_length) |
---|
| 261 | with |
---|
| 262 | [Instruction (i:(preinstruction Identifier))⇒ |
---|
[2316] | 263 | jump_expansion_step_instruction labels old_sigma inc_pc_sigma (|prefix|) i |
---|
[2239] | 264 | |Comment (_:String)⇒None jump_length |
---|
| 265 | |Cost (_:costlabel)⇒None jump_length |
---|
[2714] | 266 | |Jnz _ _ _ ⇒ None ? |
---|
[2239] | 267 | |Jmp (j:Identifier)⇒ |
---|
| 268 | Some jump_length |
---|
[2316] | 269 | (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j) |
---|
[2239] | 270 | |Call (c:Identifier)⇒ |
---|
| 271 | Some jump_length |
---|
[2316] | 272 | (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c) |
---|
[3039] | 273 | |Mov _ _ _⇒None jump_length] |
---|
[2239] | 274 | in option |
---|
| 275 | return λ_:(option jump_length).(jump_length×ℕ) |
---|
| 276 | with |
---|
| 277 | [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 |
---|
| 278 | |Some (pl:jump_length)⇒ |
---|
| 279 | 〈max_length old_length pl, |
---|
| 280 | instruction_size_jmplen (max_length old_length pl) instr〉] |
---|
| 281 | =〈new_length,isize〉. |
---|
| 282 | ∀prefix_ok1 : S (|prefix|)< 2 \sup 16. |
---|
| 283 | ∀prefix_ok : |prefix|< 2 \sup 16. |
---|
| 284 | ∀Heq2b : |
---|
| 285 | 〈inc_pc+isize, |
---|
| 286 | insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 287 | 〈inc_pc+isize, |
---|
| 288 | \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 289 | (\snd old_sigma) 〈O,short_jump〉)〉 |
---|
| 290 | (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) |
---|
| 291 | 〈inc_pc,new_length〉 inc_sigma)〉 |
---|
| 292 | =policy. |
---|
| 293 | sigma_compact_unsafe (prefix@[〈label,instr〉]) labels policy. |
---|
| 294 | #labels #old_sigma #prefix #inc_added #inc_pc_sigma #label #instr #inc_pc #inc_sigma |
---|
| 295 | #old_length #Hpolicy1 #Hpolicy2 #Hpolicy3 #policy #new_length #isize |
---|
| 296 | #Heq1 #prefix_ok1 #prefix_ok #Heq2b |
---|
| 297 | #i >append_length <commutative_plus #Hi normalize in Hi; |
---|
| 298 | <Heq2b |
---|
| 299 | cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
| 300 | [ >lookup_opt_insert_miss |
---|
| 301 | [ >lookup_opt_insert_miss |
---|
| 302 | [ >lookup_opt_insert_miss |
---|
| 303 | [ cases (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
| 304 | [ >lookup_opt_insert_miss |
---|
| 305 | [ (* USE[pass]: sigma_compact_unsafe *) |
---|
| 306 | lapply (Hpolicy1 i ?) |
---|
| 307 | [ @le_S_to_le @Hi ] |
---|
| 308 | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) |
---|
| 309 | [ normalize nodelta #X @X |
---|
| 310 | | #x cases x -x #x1 #x2 |
---|
| 311 | cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) |
---|
| 312 | normalize nodelta |
---|
| 313 | [ #X @X |
---|
| 314 | | #y cases y -y #y1 #y2 normalize nodelta >nth_append_first |
---|
| 315 | [ #X @X |
---|
| 316 | | @le_S_to_le @Hi |
---|
| 317 | ] |
---|
| 318 | ] |
---|
| 319 | ] |
---|
| 320 | | @bitvector_of_nat_abs |
---|
| 321 | [3: @lt_to_not_eq @Hi ] |
---|
| 322 | ] |
---|
| 323 | | >Hi >lookup_opt_insert_hit normalize nodelta |
---|
| 324 | (* USE[pass]: sigma_compact_unsafe *) |
---|
| 325 | lapply (Hpolicy1 i ?) |
---|
| 326 | [ <Hi @le_n |
---|
| 327 | | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) |
---|
| 328 | [ normalize nodelta #X @X |
---|
| 329 | | #x cases x -x #x1 #x2 |
---|
| 330 | (* USE: inc_pc = fst inc_sigma *) |
---|
| 331 | lapply Hpolicy2 |
---|
| 332 | <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)) |
---|
| 333 | cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %); |
---|
| 334 | [ normalize nodelta #_ #_ #H cases H |
---|
| 335 | | #y cases y -y #y1 #y2 #Heq >nth_append_first |
---|
| 336 | [ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉) |
---|
| 337 | #Heq2 <Heq2 #X @X |
---|
| 338 | | <Hi @le_n]]]]]]]] |
---|
| 339 | [3,4,5: @bitvector_of_nat_abs] |
---|
| 340 | [ @(transitive_lt ??? (le_S_S … Hi)) |
---|
| 341 | |3: @lt_to_not_eq @le_S_S @Hi |
---|
| 342 | |4,7,10: @(transitive_lt ??? Hi) assumption |
---|
| 343 | |5,11: @le_S_to_le |
---|
| 344 | |6: @lt_to_not_eq @Hi |
---|
| 345 | |9: @lt_to_not_eq @le_S @Hi |
---|
| 346 | ] |
---|
| 347 | assumption |
---|
| 348 | | >Hi >lookup_opt_insert_miss |
---|
| 349 | [2: @bitvector_of_nat_abs try assumption @lt_to_not_eq % ] |
---|
| 350 | >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta |
---|
| 351 | (* USE: out_of_program_none ← *) |
---|
| 352 | lapply (Hpolicy3 i ?) |
---|
| 353 | [ >Hi assumption |
---|
| 354 | | >Hi |
---|
| 355 | (* USE: inc_pc = fst policy *) |
---|
| 356 | lapply Hpolicy2 |
---|
| 357 | inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma) |
---|
| 358 | [ #Heq #_ #H @⊥ @(absurd (|prefix| > |prefix|)) |
---|
| 359 | [ cases H #_ #X @X % |
---|
| 360 | | @le_to_not_lt @le_n] |
---|
| 361 | | * #x1 #x2 #Heq #Hip #_ >nth_append_second |
---|
| 362 | [2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta |
---|
| 363 | >Hip >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉) |
---|
| 364 | cases instr in Heq1; normalize nodelta |
---|
[2316] | 365 | [1: #pi cases (jump_expansion_step_instruction ?????) normalize nodelta] |
---|
[2239] | 366 | try (#x #y #Heq1) try (#x #Heq1) try #Heq1 |
---|
| 367 | @eq_f <(proj2 ?? (pair_destruct ?????? Heq1)) |
---|
| 368 | try % <(proj1 ?? (pair_destruct ?????? Heq1)) %]]] |
---|
| 369 | qed. |
---|
| 370 | |
---|
| 371 | lemma jump_expansion_step5: |
---|
| 372 | ∀labels : label_map. |
---|
| 373 | ∀old_sigma : ppc_pc_map. |
---|
| 374 | ∀prefix : list (option Identifier×pseudo_instruction). |
---|
| 375 | ∀inc_added : ℕ. |
---|
| 376 | ∀inc_pc_sigma : ppc_pc_map. |
---|
| 377 | ∀label : option Identifier. |
---|
| 378 | ∀instr : pseudo_instruction. |
---|
| 379 | ∀inc_pc : ℕ. |
---|
| 380 | ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16. |
---|
| 381 | ∀old_pc : ℕ. |
---|
| 382 | ∀old_length : jump_length. |
---|
| 383 | ∀Holdeq : |
---|
| 384 | lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd old_sigma) |
---|
| 385 | 〈O,short_jump〉 |
---|
| 386 | =〈old_pc,old_length〉. |
---|
| 387 | ∀Hpolicy1 : sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O. |
---|
| 388 | ∀Hpolicy2: inc_pc |
---|
| 389 | =\fst (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉). |
---|
| 390 | ∀added : ℕ. |
---|
| 391 | ∀policy : ppc_pc_map. |
---|
| 392 | ∀new_length : jump_length. |
---|
| 393 | ∀isize : ℕ. |
---|
| 394 | let add_instr ≝ match instr with |
---|
[2316] | 395 | [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j) |
---|
| 396 | | Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c) |
---|
| 397 | | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma (|prefix|) i |
---|
[2239] | 398 | | _ ⇒ None ? |
---|
| 399 | ] in |
---|
| 400 | ∀Heq1 : |
---|
| 401 | match add_instr with |
---|
| 402 | [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 |
---|
| 403 | |Some (pl:jump_length)⇒ |
---|
| 404 | 〈max_length old_length pl, |
---|
| 405 | instruction_size_jmplen (max_length old_length pl) instr〉] |
---|
| 406 | =〈new_length,isize〉. |
---|
| 407 | ∀prefix_ok1 : S (|prefix|)< 2 \sup 16. |
---|
| 408 | ∀prefix_ok : |prefix|< 2 \sup 16. |
---|
| 409 | ∀Heq2a : |
---|
| 410 | match add_instr with |
---|
| 411 | [None⇒inc_added |
---|
| 412 | |Some (x0:jump_length)⇒ |
---|
| 413 | inc_added+(isize-instruction_size_jmplen old_length instr)] |
---|
| 414 | =added. |
---|
| 415 | ∀Heq2b : |
---|
| 416 | 〈inc_pc+isize, |
---|
| 417 | insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 418 | 〈inc_pc+isize, |
---|
| 419 | \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 420 | (\snd old_sigma) 〈O,short_jump〉)〉 |
---|
| 421 | (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) |
---|
| 422 | 〈inc_pc,new_length〉 inc_sigma)〉 |
---|
| 423 | =policy. |
---|
| 424 | sigma_jump_equal (prefix@[〈label,instr〉]) old_sigma policy→added=O. |
---|
| 425 | #labels #old_sigma #prefix #inc_added #inc_pc #label #instr #inc_pc #inc_sigma |
---|
| 426 | #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2 #added #policy #new_length #isize |
---|
| 427 | #Heq1 #prefix_ok1 #prefix_ok #Heq2a #Heq2b |
---|
| 428 | <Heq2b #Heq <Heq2a |
---|
| 429 | (* USE[pass]: policy_jump_equal → added = 0 *) |
---|
| 430 | >Hpolicy1 |
---|
| 431 | [ cases instr in Heq1 Heq; |
---|
[3039] | 432 | [2,3: #x [3: #y] normalize nodelta #_ #_ % |
---|
| 433 | |5,7: #x #y #z #_ #_ % |
---|
[2239] | 434 | |1: #pi normalize nodelta whd in match jump_expansion_step_instruction; |
---|
| 435 | normalize nodelta cases (destination_of ?) normalize nodelta [#_ #_ %]] |
---|
| 436 | #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) |
---|
| 437 | #Heq (*CSC: make a lemma here!*) lapply Holdeq -Holdeq |
---|
| 438 | (* USE: inc_pc = fst inc_sigma *) |
---|
| 439 | >Hpolicy2 |
---|
| 440 | lapply (Heq (|prefix|) ?) |
---|
| 441 | [1,3,5: >append_length <plus_n_Sm @le_S_S @le_plus_n_r] |
---|
| 442 | -Heq >lookup_insert_miss |
---|
| 443 | [1,3,5: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1)) |
---|
| 444 | #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) |
---|
| 445 | #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n % |
---|
| 446 | |*: @bitvector_of_nat_abs try assumption @lt_to_not_eq %] |
---|
| 447 | | #i #Hi lapply (Heq i ?) |
---|
| 448 | [ >append_length <plus_n_Sm @le_S <plus_n_O @Hi |
---|
| 449 | | >lookup_insert_miss |
---|
| 450 | [ >lookup_insert_miss |
---|
| 451 | [ #X @X |
---|
| 452 | | @bitvector_of_nat_abs [ @(transitive_lt ??? Hi) ] try assumption |
---|
| 453 | @lt_to_not_eq @Hi] |
---|
| 454 | | @bitvector_of_nat_abs [ @(transitive_lt ??? Hi) ] try assumption |
---|
| 455 | @lt_to_not_eq @le_S @Hi ]]] |
---|
| 456 | qed. |
---|
| 457 | |
---|
[2240] | 458 | lemma jump_expansion_step6: |
---|
[2248] | 459 | ∀program : list labelled_instruction. |
---|
| 460 | ∀labels : label_map. |
---|
| 461 | ∀old_sigma : Σpolicy:ppc_pc_map.sigma_compact_unsafe program labels policy. |
---|
[2245] | 462 | ∀prefix : list (option Identifier×pseudo_instruction). |
---|
| 463 | ∀x : option Identifier×pseudo_instruction. |
---|
| 464 | ∀tl : list (option Identifier×pseudo_instruction). |
---|
[2248] | 465 | ∀prf : program=prefix@[x]@tl. |
---|
[2245] | 466 | ∀inc_added : ℕ. |
---|
[2248] | 467 | ∀inc_pc_sigma : ppc_pc_map. |
---|
[2240] | 468 | ∀label : option Identifier. |
---|
[2245] | 469 | ∀instr : pseudo_instruction. |
---|
[2248] | 470 | ∀p1 : x≃〈label,instr〉. |
---|
[2245] | 471 | ∀inc_pc : ℕ. |
---|
[2248] | 472 | ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16. |
---|
[2245] | 473 | ∀old_pc : ℕ. |
---|
| 474 | ∀old_length : jump_length. |
---|
| 475 | ∀Holdeq : |
---|
| 476 | lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd old_sigma) |
---|
[2240] | 477 | 〈O,short_jump〉 |
---|
[2245] | 478 | =〈old_pc,old_length〉. |
---|
[2248] | 479 | ∀Hpolicy1 : inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉. |
---|
| 480 | ∀Hpolic2: inc_pc =\fst (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉). |
---|
[2240] | 481 | ∀added : ℕ. |
---|
[2245] | 482 | ∀policy : ppc_pc_map. |
---|
| 483 | ∀new_length : jump_length. |
---|
| 484 | ∀isize : ℕ. |
---|
| 485 | let add_instr ≝ match instr with |
---|
[2316] | 486 | [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j) |
---|
| 487 | | Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c) |
---|
| 488 | | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma (|prefix|) i |
---|
[2245] | 489 | | _ ⇒ None ? |
---|
| 490 | ] in |
---|
| 491 | ∀Heq1 : |
---|
| 492 | match add_instr with |
---|
[2240] | 493 | [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 |
---|
| 494 | |Some (pl:jump_length)⇒ |
---|
| 495 | 〈max_length old_length pl, |
---|
| 496 | instruction_size_jmplen (max_length old_length pl) instr〉] |
---|
[2245] | 497 | =〈new_length,isize〉. |
---|
| 498 | ∀prefix_ok1 : S (|prefix|)< 2 \sup 16. |
---|
| 499 | ∀prefix_ok : |prefix|< 2 \sup 16. |
---|
| 500 | ∀Heq2a : |
---|
| 501 | match add_instr with |
---|
[2240] | 502 | [None⇒inc_added |
---|
| 503 | |Some (x0:jump_length)⇒ |
---|
| 504 | inc_added+(isize-instruction_size_jmplen old_length instr)] |
---|
[2245] | 505 | =added. |
---|
| 506 | ∀Heq2b : |
---|
| 507 | 〈inc_pc+isize, |
---|
[2240] | 508 | insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 509 | 〈inc_pc+isize, |
---|
| 510 | \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 511 | (\snd old_sigma) 〈O,short_jump〉)〉 |
---|
| 512 | (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) |
---|
| 513 | 〈inc_pc,new_length〉 inc_sigma)〉 |
---|
[2245] | 514 | =policy. |
---|
[2240] | 515 | added=O→sigma_pc_equal (prefix@[〈label,instr〉]) old_sigma policy. |
---|
[2245] | 516 | #program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label |
---|
| 517 | #instr #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2 |
---|
| 518 | #added #policy #new_length #isize #Heq1 #prefix_ok #prefix_ok1 #Heq2a #Heq2b |
---|
[2211] | 519 | (* USE[pass]: added = 0 → policy_pc_equal *) |
---|
[2245] | 520 | lapply Hpolicy1 <Heq2b <Heq2a lapply Heq1 -Heq1 |
---|
[2248] | 521 | #Hins #Hold #Hadded #i #Hi |
---|
[2246] | 522 | >append_length in Hi; >commutative_plus #Hi normalize in Hi; |
---|
| 523 | cases (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
[2248] | 524 | [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
| 525 | [ <Heq2b >lookup_insert_miss |
---|
| 526 | [ >lookup_insert_miss |
---|
| 527 | [ cases instr in Hadded; normalize nodelta |
---|
| 528 | [ whd in match jump_expansion_step_instruction; normalize nodelta |
---|
| 529 | #pi cases (destination_of ?) normalize nodelta ] |
---|
| 530 | try (#x #y #Hadded) try (#x #Hadded) try #Hadded |
---|
[2246] | 531 | try @(Hold Hadded i (le_S_to_le … Hi)) |
---|
| 532 | @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded; @plus_zero_zero |
---|
[2248] | 533 | | @bitvector_of_nat_abs try assumption |
---|
| 534 | [2: @lt_to_not_eq @Hi |
---|
| 535 | | @(transitive_lt ??? Hi) assumption ]] |
---|
| 536 | | @bitvector_of_nat_abs try assumption |
---|
| 537 | [2: @lt_to_not_eq @le_S @Hi |
---|
| 538 | | @(transitive_lt … Hi) assumption ]] |
---|
| 539 | | >Hi >lookup_insert_miss |
---|
| 540 | [ cases instr in Hadded; normalize nodelta |
---|
| 541 | [ whd in match jump_expansion_step_instruction; normalize nodelta |
---|
| 542 | #pi cases (destination_of ?) normalize nodelta ] |
---|
| 543 | try (#x #y #Hadded) try (#x #Hadded) try #Hadded |
---|
| 544 | >lookup_insert_hit |
---|
[2246] | 545 | try (>(Hold Hadded (|prefix|) (le_n (|prefix|))) |
---|
| 546 | @sym_eq (* USE: fst p = lookup |prefix| *) |
---|
| 547 | @Hpolicy2) |
---|
| 548 | >(Hold ? (|prefix|) (le_n (|prefix|))) |
---|
| 549 | [2,4,6,8: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq |
---|
[2152] | 550 | (* USE: fst p = lookup |prefix| *) |
---|
[2246] | 551 | @Hpolicy2 |
---|
| 552 | |*: @bitvector_of_nat_abs try assumption |
---|
| 553 | @lt_to_not_eq %]] |
---|
| 554 | |*: >Hi >lookup_insert_hit |
---|
| 555 | (* USE fst p = lookup |prefix| *) |
---|
| 556 | >Hpolicy2 |
---|
[2248] | 557 | <(Hold ? (|prefix|) (le_n (|prefix|))) |
---|
| 558 | [2: cases instr in Hadded; normalize nodelta |
---|
| 559 | [ whd in match jump_expansion_step_instruction; normalize nodelta |
---|
| 560 | #pi cases (destination_of ?) normalize nodelta ] |
---|
| 561 | try (#x #y #Hadded) try (#x #Hadded) try #Hadded |
---|
| 562 | try @Hadded |
---|
| 563 | @plus_zero_zero [2,4,6: >commutative_plus @Hadded |*: skip]] |
---|
[2246] | 564 | (* USE: sigma_compact (from old_sigma) *) |
---|
| 565 | lapply (pi2 ?? old_sigma (|prefix|) ?) |
---|
[2248] | 566 | [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r |
---|
| 567 | | inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) |
---|
| 568 | [ normalize nodelta #_ #ABS cases ABS |
---|
| 569 | | inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) |
---|
| 570 | [ normalize nodelta #Hl * #pc #j normalize nodelta #Hl2 #ABS cases ABS |
---|
| 571 | | normalize nodelta * #Spc #Sj #EQS * #pc #j #EQ |
---|
[2246] | 572 | normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) |
---|
| 573 | >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) |
---|
| 574 | >prf >p1 >Hins >nth_append_second try % |
---|
[2248] | 575 | <minus_n_n whd in match (nth ????); |
---|
| 576 | cases instr in Hins Hadded; normalize nodelta |
---|
| 577 | [ whd in match jump_expansion_step_instruction; normalize nodelta |
---|
| 578 | #pi lapply (destination_of_None_to_is_jump_false pi) |
---|
| 579 | lapply (destination_of_Some_to_is_jump_true pi) |
---|
| 580 | cases (destination_of ?) normalize nodelta |
---|
| 581 | [ #_ #dest_None | #tgt #dest_Some #_ ]] |
---|
[2714] | 582 | try (#x #y #z #Heq1 #Hadded #X) |
---|
[2248] | 583 | try (#x #y #Heq1 #Hadded #X) try (#x #Heq1 #Hadded #X) try (#Heq1 #Hadded #X) |
---|
| 584 | <(proj2 ?? (pair_destruct ?????? Heq1)) >X @plus_left_monotone |
---|
[3039] | 585 | [1,3,4,6,8: @instruction_size_irrelevant try % |
---|
[2246] | 586 | whd in match is_jump; normalize nodelta >dest_None % |
---|
| 587 | |*: >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; #EQ' |
---|
| 588 | >(proj2 … (pair_destruct … EQ')) |
---|
| 589 | elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded))) |
---|
| 590 | [1,3,5: #H @⊥ @(absurd ? H) @le_to_not_lt |
---|
| 591 | <(proj2 ?? (pair_destruct ?????? Heq1)) |
---|
| 592 | @jump_length_le_max try % |
---|
| 593 | whd in match is_jump; normalize nodelta >dest_Some %] |
---|
| 594 | #EQisize >(proj2 … (pair_destruct … Heq1)) >EQisize % ]]]]] |
---|
[2240] | 595 | qed. |
---|
| 596 | |
---|
| 597 | lemma jump_expansion_step7: |
---|
[2242] | 598 | ∀old_sigma : ppc_pc_map. |
---|
| 599 | ∀prefix : list (option Identifier×pseudo_instruction). |
---|
[2240] | 600 | ∀label : option Identifier. |
---|
[2242] | 601 | ∀instr : pseudo_instruction. |
---|
| 602 | ∀inc_pc : ℕ. |
---|
| 603 | ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16. |
---|
| 604 | ∀Hpolicy1 : out_of_program_none prefix 〈inc_pc,inc_sigma〉. |
---|
| 605 | ∀policy : ppc_pc_map. |
---|
| 606 | ∀new_length : jump_length. |
---|
| 607 | ∀isize : ℕ. |
---|
| 608 | ∀Heq2b : |
---|
| 609 | 〈inc_pc+isize, |
---|
[2240] | 610 | insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 611 | 〈inc_pc+isize, |
---|
| 612 | \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 613 | (\snd old_sigma) 〈O,short_jump〉)〉 |
---|
| 614 | (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) |
---|
| 615 | 〈inc_pc,new_length〉 inc_sigma)〉 |
---|
[2242] | 616 | =policy. |
---|
[2240] | 617 | out_of_program_none (prefix@[〈label,instr〉]) policy. |
---|
[2242] | 618 | #old_sigma #prefix #label #instr #inc_pc #inc_sigma #Hpolicy1 #policy #new_length |
---|
| 619 | #isize #Heq2b |
---|
[2240] | 620 | #i #Hi2 >append_length <commutative_plus @conj |
---|
[2242] | 621 | [ (* → *) #Hi normalize in Hi; <Heq2b >lookup_opt_insert_miss |
---|
| 622 | [ >lookup_opt_insert_miss |
---|
| 623 | [ cases (Hpolicy1 i Hi2) #X #_ @X @le_S_to_le @Hi |
---|
| 624 | | @bitvector_of_nat_abs try assumption |
---|
| 625 | [ @(transitive_lt … Hi2) @le_S_to_le assumption |
---|
| 626 | | % #EQ <EQ in Hi; #abs @(absurd ?? (not_le_Sn_n (S i))) |
---|
| 627 | @(transitive_le … abs) %2 % ]] |
---|
| 628 | | @bitvector_of_nat_abs try assumption |
---|
| 629 | [ @(transitive_lt … Hi2) assumption |
---|
| 630 | | % #EQ <EQ in Hi; #abs @(absurd ?? (not_le_Sn_n i)) assumption ]] |
---|
| 631 | | (* ← *) <Heq2b #Hl normalize |
---|
| 632 | @(leb_elim (S i) (|prefix|)) |
---|
| 633 | [ #Hi |
---|
[2152] | 634 | lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl)))) |
---|
| 635 | #Hl2 (* USE[pass]: out_of_program_none ← *) |
---|
[2242] | 636 | cases (Hpolicy1 i Hi2) #_ |
---|
| 637 | #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3 assumption |
---|
[2152] | 638 | | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi)) |
---|
| 639 | [ #Hi3 elim (le_to_or_lt_eq … Hi3) |
---|
[2242] | 640 | [ #X @X |
---|
[2152] | 641 | | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H) |
---|
| 642 | ] |
---|
| 643 | | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl)))) |
---|
[2242] | 644 | >X >eq_bv_refl #H normalize in H; destruct (H)]]] |
---|
[2240] | 645 | qed. |
---|
| 646 | |
---|
| 647 | lemma jump_expansion_step8: |
---|
[2243] | 648 | ∀program : list labelled_instruction. |
---|
| 649 | ∀labels : label_map. |
---|
| 650 | ∀old_sigma : |
---|
| 651 | Σpolicy:ppc_pc_map.sigma_compact_unsafe program labels policy ∧\fst policy≤ 2 \sup 16. |
---|
| 652 | ∀prefix : list (option Identifier×pseudo_instruction). |
---|
| 653 | ∀x : option Identifier×pseudo_instruction. |
---|
| 654 | ∀tl : list (option Identifier×pseudo_instruction). |
---|
| 655 | ∀prf : program=prefix@[x]@tl. |
---|
| 656 | ∀inc_added : ℕ. |
---|
| 657 | ∀inc_pc_sigma : ppc_pc_map. |
---|
[2240] | 658 | ∀label : option Identifier. |
---|
[2243] | 659 | ∀instr : pseudo_instruction. |
---|
| 660 | ∀p1 : x≃〈label,instr〉. |
---|
| 661 | ∀inc_pc : ℕ. |
---|
| 662 | ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16. |
---|
| 663 | ∀old_pc : ℕ. |
---|
| 664 | ∀old_length : jump_length. |
---|
| 665 | ∀Holdeq : |
---|
| 666 | lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd old_sigma) |
---|
[2240] | 667 | 〈O,short_jump〉 |
---|
[2243] | 668 | =〈old_pc,old_length〉. |
---|
| 669 | ∀Hpolicy1 : inc_pc |
---|
| 670 | =\fst (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉). |
---|
| 671 | ∀Hpolicy2: \fst (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉) |
---|
| 672 | =old_pc+inc_added. |
---|
[2240] | 673 | ∀added : ℕ. |
---|
[2243] | 674 | ∀policy : ppc_pc_map. |
---|
| 675 | ∀new_length : jump_length. |
---|
| 676 | ∀isize : ℕ. |
---|
| 677 | let add_instr ≝ match instr with |
---|
[2316] | 678 | [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j) |
---|
| 679 | | Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c) |
---|
| 680 | | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma (|prefix|) i |
---|
[2243] | 681 | | _ ⇒ None ? |
---|
| 682 | ] in |
---|
| 683 | ∀Heq1 : |
---|
| 684 | match add_instr with |
---|
[2240] | 685 | [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 |
---|
| 686 | |Some (pl:jump_length)⇒ |
---|
| 687 | 〈max_length old_length pl, |
---|
| 688 | instruction_size_jmplen (max_length old_length pl) instr〉] |
---|
[2243] | 689 | =〈new_length,isize〉. |
---|
| 690 | ∀Heq2a : |
---|
| 691 | match add_instr with |
---|
[2240] | 692 | [None⇒inc_added |
---|
| 693 | |Some (x0:jump_length)⇒ |
---|
| 694 | inc_added+(isize-instruction_size_jmplen old_length instr)] |
---|
[2243] | 695 | =added. |
---|
| 696 | ∀Heq2b : |
---|
| 697 | 〈inc_pc+isize, |
---|
[2240] | 698 | insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 699 | 〈inc_pc+isize, |
---|
| 700 | \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 701 | (\snd old_sigma) 〈O,short_jump〉)〉 |
---|
| 702 | (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) |
---|
| 703 | 〈inc_pc,new_length〉 inc_sigma)〉 |
---|
[2243] | 704 | =policy. |
---|
[2240] | 705 | \fst (lookup (ℕ×jump_length) 16 |
---|
| 706 | (bitvector_of_nat 16 (|(prefix@[〈label,instr〉])|)) (\snd policy) |
---|
| 707 | 〈O,short_jump〉) |
---|
| 708 | =\fst (lookup (ℕ×jump_length) 16 |
---|
| 709 | (bitvector_of_nat 16 (|(prefix@[〈label,instr〉])|)) (\snd old_sigma) |
---|
| 710 | 〈O,short_jump〉) |
---|
| 711 | +added. |
---|
[2243] | 712 | #program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label #instr |
---|
| 713 | #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2 #added |
---|
| 714 | #policy #new_length #isize #Heq1 #Heq2a #Heq2b |
---|
| 715 | <Heq2b >append_length <plus_n_Sm <plus_n_O |
---|
[2152] | 716 | >lookup_insert_hit |
---|
[2243] | 717 | <Heq2a cases instr in p1 Heq1; |
---|
| 718 | [1: #pi normalize nodelta whd in match jump_expansion_step_instruction; |
---|
| 719 | normalize nodelta lapply (destination_of_None_to_is_jump_false pi) |
---|
| 720 | lapply (destination_of_Some_to_is_jump_true pi) |
---|
| 721 | cases (destination_of ?) normalize nodelta ] |
---|
| 722 | try (#x #y #z #p1 #Heq1) try (#x #y #p1 #Heq1) try (#x #p1 #Heq1) try (#p1 #Heq1) |
---|
| 723 | <(proj2 ?? (pair_destruct ?????? Heq1)) |
---|
| 724 | (* USE: sigma_compact_unsafe (from old_sigma) *) |
---|
| 725 | lapply (proj1 ?? (pi2 ?? old_sigma) (|prefix|) ?) |
---|
[2714] | 726 | [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r] |
---|
[2243] | 727 | lapply Holdeq -Holdeq |
---|
| 728 | inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) |
---|
[2714] | 729 | [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #abs cases abs] |
---|
[2243] | 730 | inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) |
---|
[2714] | 731 | normalize nodelta |
---|
| 732 | [1,3,5,7,9,11,13,15,17: #_ * #Spc #Sj normalize nodelta #_ #_ #abs cases abs] |
---|
[2243] | 733 | * #Spc #Sj #EQS * #pc #j #Holdeq #EQ normalize nodelta |
---|
| 734 | #H (* USE: fst p = lookup |prefix| *) (*CSC: This part of the proof is repeated somewhere else*) |
---|
| 735 | >Hpolicy1 |
---|
| 736 | (* USE[pass]: lookup p = lookup old_sigma + added *) |
---|
| 737 | >Hpolicy2 |
---|
[3039] | 738 | [1,3,4,6,8: |
---|
[2243] | 739 | >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; |
---|
| 740 | -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ)) |
---|
| 741 | >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second try % |
---|
| 742 | <minus_n_n >p1 whd in match (nth ????); >associative_plus |
---|
| 743 | >(associative_plus pc) @plus_left_monotone >commutative_plus |
---|
| 744 | @plus_right_monotone @instruction_size_irrelevant try % |
---|
| 745 | whd in match is_jump; normalize nodelta >y % |
---|
[3039] | 746 | |*: |
---|
[2243] | 747 | >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H |
---|
| 748 | >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; #EQ |
---|
| 749 | -Holdeq <(proj1 ?? (pair_destruct ?????? EQ)) |
---|
| 750 | >associative_plus |
---|
| 751 | >(associative_plus pc) @plus_left_monotone >assoc_plus1 |
---|
| 752 | >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative |
---|
| 753 | [1,3,5: >(proj2 ?? (pair_destruct ?????? EQ)) >prf in old_sigma; #old_sigma |
---|
| 754 | >nth_append_second try % |
---|
| 755 | <minus_n_n whd in match (nth ????); >p1 in old_sigma; #old_sigma |
---|
| 756 | >commutative_plus @minus_plus_m_m |
---|
| 757 | |*: <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max try % |
---|
| 758 | whd in match is_jump; normalize nodelta >y %]] |
---|
[2240] | 759 | qed. |
---|
| 760 | |
---|
| 761 | lemma jump_expansion_step9: |
---|
[2316] | 762 | ∀program : list labelled_instruction. |
---|
| 763 | (*(Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l).*) |
---|
[2240] | 764 | ∀labels : label_map.(* |
---|
| 765 | (Σlm:label_map |
---|
| 766 | .(∀l:identifier ASMTag |
---|
| 767 | .occurs_exactly_once ASMTag pseudo_instruction l program |
---|
| 768 | →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O) |
---|
| 769 | =address_of_word_labels_code_mem program l))*) |
---|
| 770 | ∀old_sigma : ppc_pc_map.(* |
---|
| 771 | (Σpolicy:ppc_pc_map |
---|
| 772 | .not_jump_default program policy |
---|
| 773 | ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) |
---|
| 774 | 〈O,short_jump〉) |
---|
| 775 | =O |
---|
| 776 | ∧\fst policy |
---|
| 777 | =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|)) |
---|
| 778 | (\snd policy) 〈O,short_jump〉) |
---|
| 779 | ∧sigma_compact_unsafe program labels policy |
---|
| 780 | ∧\fst policy≤ 2 \sup 16 )*) |
---|
[2316] | 781 | ∀prefix : list (option Identifier×pseudo_instruction). |
---|
| 782 | ∀x : (option Identifier×pseudo_instruction). |
---|
| 783 | ∀tl : (list (option Identifier×pseudo_instruction)). |
---|
| 784 | ∀prf : (program=prefix@[x]@tl). |
---|
| 785 | (*acc : |
---|
[2240] | 786 | (Σx0:ℕ×ppc_pc_map |
---|
| 787 | .(let 〈added,policy〉 ≝x0 in |
---|
| 788 | not_jump_default prefix policy |
---|
| 789 | ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) |
---|
| 790 | 〈O,short_jump〉) |
---|
| 791 | =O |
---|
| 792 | ∧\fst policy |
---|
| 793 | =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) |
---|
| 794 | (\snd policy) 〈O,short_jump〉) |
---|
| 795 | ∧jump_increase prefix old_sigma policy |
---|
| 796 | ∧sigma_compact_unsafe prefix labels policy |
---|
| 797 | ∧(sigma_jump_equal prefix old_sigma policy→added=O) |
---|
| 798 | ∧(added=O→sigma_pc_equal prefix old_sigma policy) |
---|
| 799 | ∧out_of_program_none prefix policy |
---|
| 800 | ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) |
---|
| 801 | (\snd policy) 〈O,short_jump〉) |
---|
| 802 | =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) |
---|
| 803 | (\snd old_sigma) 〈O,short_jump〉) |
---|
| 804 | +added |
---|
[2316] | 805 | ∧sigma_safe prefix labels added old_sigma policy))*) |
---|
| 806 | (*∀inc_added:ℕ.*) |
---|
| 807 | ∀inc_pc_sigma : ppc_pc_map. |
---|
| 808 | (*p : (acc≃〈inc_added,inc_pc_sigma〉)*) |
---|
[2240] | 809 | ∀label : option Identifier. |
---|
[2316] | 810 | ∀instr : pseudo_instruction. |
---|
| 811 | ∀p1 : (x≃〈label,instr〉). |
---|
| 812 | (*add_instr ≝ |
---|
[2240] | 813 | match instr |
---|
| 814 | in pseudo_instruction |
---|
| 815 | return λ_:pseudo_instruction.(option jump_length) |
---|
| 816 | with |
---|
| 817 | [Instruction (i:(preinstruction Identifier))⇒ |
---|
| 818 | jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added |
---|
| 819 | (|prefix|) i |
---|
| 820 | |Comment (_:String)⇒None jump_length |
---|
| 821 | |Cost (_:costlabel)⇒None jump_length |
---|
| 822 | |Jmp (j:Identifier)⇒ |
---|
| 823 | Some jump_length |
---|
| 824 | (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j) |
---|
| 825 | |Call (c:Identifier)⇒ |
---|
| 826 | Some jump_length |
---|
| 827 | (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c) |
---|
[3039] | 828 | |Mov _ _ _⇒None jump_length] *) |
---|
[2316] | 829 | ∀inc_pc : ℕ. |
---|
| 830 | ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16). |
---|
| 831 | ∀Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉). |
---|
| 832 | ∀old_pc : ℕ. |
---|
| 833 | ∀old_length : jump_length. |
---|
| 834 | ∀Holdeq : |
---|
| 835 | bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd old_sigma) |
---|
| 836 | 〈O,short_jump〉=〈old_pc,old_length〉. |
---|
| 837 | (*Hpolicy : |
---|
[2240] | 838 | (not_jump_default prefix 〈inc_pc,inc_sigma〉 |
---|
| 839 | ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma |
---|
| 840 | 〈O,short_jump〉) |
---|
| 841 | =O |
---|
| 842 | ∧inc_pc |
---|
| 843 | =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma |
---|
| 844 | 〈O,short_jump〉) |
---|
| 845 | ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉 |
---|
| 846 | ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉 |
---|
| 847 | ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O) |
---|
| 848 | ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉) |
---|
| 849 | ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉 |
---|
| 850 | ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma |
---|
| 851 | 〈O,short_jump〉) |
---|
| 852 | =old_pc+inc_added |
---|
| 853 | ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*) |
---|
| 854 | ∀added : ℕ. |
---|
[2316] | 855 | ∀policy : ppc_pc_map. |
---|
| 856 | ∀new_length : jump_length. |
---|
| 857 | ∀isize : ℕ. |
---|
| 858 | ∀Heq1 : |
---|
[2240] | 859 | (match |
---|
| 860 | match instr |
---|
| 861 | in pseudo_instruction |
---|
| 862 | return λ_:pseudo_instruction.(option jump_length) |
---|
| 863 | with |
---|
| 864 | [Instruction (i:(preinstruction Identifier))⇒ |
---|
[2316] | 865 | jump_expansion_step_instruction labels old_sigma 〈inc_pc,inc_sigma〉 (|prefix|) i |
---|
[2240] | 866 | |Comment (_:String)⇒None jump_length |
---|
| 867 | |Cost (_:costlabel)⇒None jump_length |
---|
[2714] | 868 | |Jnz _ _ _ ⇒ None ? |
---|
[2240] | 869 | |Jmp (j:Identifier)⇒ |
---|
| 870 | Some jump_length |
---|
[2316] | 871 | (select_jump_length labels old_sigma 〈inc_pc,inc_sigma〉 (|prefix|) j) |
---|
[2240] | 872 | |Call (c:Identifier)⇒ |
---|
| 873 | Some jump_length |
---|
[2316] | 874 | (select_call_length labels old_sigma 〈inc_pc,inc_sigma〉 (|prefix|) c) |
---|
[3039] | 875 | |Mov _ _ _⇒None jump_length] |
---|
[2240] | 876 | in option |
---|
[2316] | 877 | return λ_:(option jump_length).(jump_length×ℕ) |
---|
[2240] | 878 | with |
---|
| 879 | [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 |
---|
| 880 | |Some (pl:jump_length)⇒ |
---|
| 881 | 〈max_length old_length pl, |
---|
| 882 | instruction_size_jmplen (max_length old_length pl) instr〉] |
---|
[2316] | 883 | =〈new_length,isize〉). |
---|
| 884 | ∀prefix_ok1 : (S (|prefix|)< 2 \sup 16 ). |
---|
| 885 | ∀prefix_ok : (|prefix|< 2 \sup 16 ). |
---|
| 886 | (*∀Heq2a : |
---|
[2240] | 887 | (match |
---|
| 888 | match instr |
---|
| 889 | in pseudo_instruction |
---|
[2316] | 890 | return λ_:pseudo_instruction.(option jump_length) |
---|
[2240] | 891 | with |
---|
| 892 | [Instruction (i:(preinstruction Identifier))⇒ |
---|
[2316] | 893 | jump_expansion_step_instruction labels old_sigma inc_pc_sigma |
---|
[2240] | 894 | (|prefix|) i |
---|
[2316] | 895 | |Comment (_:String)⇒None jump_length |
---|
| 896 | |Cost (_:costlabel)⇒None jump_length |
---|
[2240] | 897 | |Jmp (j:Identifier)⇒ |
---|
| 898 | Some jump_length |
---|
[2316] | 899 | (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j) |
---|
[2240] | 900 | |Call (c:Identifier)⇒ |
---|
| 901 | Some jump_length |
---|
[2316] | 902 | (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c) |
---|
[3039] | 903 | |Mov _ _ _⇒None jump_length] |
---|
[2240] | 904 | in option |
---|
[2316] | 905 | return λ_:(option jump_length).ℕ |
---|
[2240] | 906 | with |
---|
| 907 | [None⇒inc_added |
---|
| 908 | |Some (x0:jump_length)⇒ |
---|
| 909 | inc_added+(isize-instruction_size_jmplen old_length instr)] |
---|
[2316] | 910 | =added).*) |
---|
| 911 | ∀Heq2b: |
---|
| 912 | 〈inc_pc+isize, |
---|
[2240] | 913 | insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 914 | 〈inc_pc+isize, |
---|
| 915 | \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) |
---|
| 916 | (\snd old_sigma) 〈O,short_jump〉)〉 |
---|
| 917 | (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) |
---|
| 918 | 〈inc_pc,new_length〉 inc_sigma)〉 |
---|
[2316] | 919 | =policy. |
---|
| 920 | sigma_compact_unsafe program labels old_sigma → |
---|
| 921 | \fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma |
---|
| 922 | 〈O,short_jump〉) |
---|
| 923 | =old_pc+added → |
---|
| 924 | inc_pc = \fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma |
---|
| 925 | 〈O,short_jump〉) → |
---|
| 926 | sigma_safe prefix labels old_sigma 〈inc_pc,inc_sigma〉 → |
---|
| 927 | (*sigma_safe_weak program labels old_sigma → *) |
---|
| 928 | sigma_safe (prefix@[〈label,instr〉]) labels old_sigma policy. |
---|
| 929 | #program #labels #old_sigma #prefix #x #tl #prf (*#inc_added*) #inc_pc_sigma |
---|
| 930 | #label #instr #p1 #inc_pc #inc_sigma #Hips #old_pc #old_length #Holdeq #added |
---|
| 931 | #policy #new_length #isize #Heq1 #prefix_ok1 #prefix_ok (*#Heq2a*) #Heq2b |
---|
| 932 | #Hold_compact #Hold_pc #Hinc_pc #Hsigma_safe |
---|
| 933 | #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
| 934 | <Heq2b |
---|
| 935 | elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
| 936 | [ >nth_append_first [2: @Hi] lapply (Hsigma_safe i Hi) |
---|
[2652] | 937 | inversion (nth i ? prefix 〈None ?, Comment EmptyString〉) #lbl #ins #Heq normalize nodelta |
---|
[2316] | 938 | #Hsafe #dest #Hjump lapply (Hsafe dest Hjump) -Hsafe |
---|
| 939 | inversion (leb (lookup_def … labels dest 0) i) #Hle normalize nodelta |
---|
| 940 | [ elim (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
| 941 | [ >lookup_insert_miss |
---|
| 942 | [ >lookup_insert_miss |
---|
| 943 | [ >lookup_insert_miss |
---|
| 944 | [ >lookup_insert_miss |
---|
| 945 | [ >lookup_insert_miss |
---|
| 946 | [ >lookup_insert_miss |
---|
| 947 | [ #H @H |
---|
| 948 | ] |
---|
| 949 | ] |
---|
| 950 | ] |
---|
| 951 | ] |
---|
| 952 | ] |
---|
| 953 | ] |
---|
| 954 | @bitvector_of_nat_abs try assumption |
---|
| 955 | try (@(transitive_lt … prefix_ok)) |
---|
| 956 | try (@lt_to_not_eq) |
---|
| 957 | try (@(transitive_lt … Hi) @le_S_S @leb_true_to_le @Hle) |
---|
| 958 | try assumption |
---|
| 959 | try (@le_S_S) try (@(le_S_to_le … Hi)) |
---|
| 960 | [ @(lt_to_le_to_le ? (S i)) |
---|
| 961 | [ @le_S_S @leb_true_to_le @Hle |
---|
| 962 | | @le_S_to_le @Hi |
---|
| 963 | ] |
---|
| 964 | | @le_S_to_le @le_S_to_le @Hi |
---|
| 965 | ] |
---|
| 966 | ] |
---|
| 967 | | #H >lookup_insert_miss |
---|
| 968 | [2: @bitvector_of_nat_abs [ @(transitive_lt … prefix_ok) @Hi | @prefix_ok1 | |
---|
| 969 | @lt_to_not_eq @(transitive_lt … Hi) @le_n ] ] |
---|
| 970 | >lookup_insert_miss |
---|
| 971 | [2: @bitvector_of_nat_abs [ @(transitive_lt … prefix_ok) @Hi | @prefix_ok | |
---|
| 972 | @lt_to_not_eq @Hi ] ] |
---|
| 973 | @H |
---|
| 974 | ] |
---|
| 975 | | >Hi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta |
---|
| 976 | #dest #Hjump (*cases instr in Hjump Heq1; |
---|
| 977 | [2,3,6: #y [3: #id] normalize nodelta #abs cases abs |
---|
| 978 | |1: #pi normalize nodelta cases pi |
---|
| 979 | try (#y #id #Hjump #Heq1) try (#id #Hjump #Heq1) try (#Hjump #Heq1) |
---|
| 980 | try (cases Hjump) lapply Heq1 -Heq1 lapply Hjump -Hjump lapply id -id] |
---|
| 981 | #id #Hjump normalize nodelta*) |
---|
| 982 | >lookup_insert_miss |
---|
| 983 | [2: @bitvector_of_nat_abs [ @prefix_ok | @prefix_ok1 | @lt_to_not_eq @le_n ] ] |
---|
| 984 | >lookup_insert_hit >lookup_insert_hit |
---|
| 985 | inversion (leb (lookup_def … labels dest 0) (|prefix|)) #Hle normalize nodelta |
---|
| 986 | [ >lookup_insert_miss [2: @bitvector_of_nat_abs |
---|
| 987 | [ @(le_to_lt_to_lt … prefix_ok) @leb_true_to_le @Hle |
---|
| 988 | | @prefix_ok1 |
---|
| 989 | | @lt_to_not_eq @le_S_S @leb_true_to_le @Hle |
---|
| 990 | ]] |
---|
| 991 | elim (le_to_or_lt_eq … (leb_true_to_le … Hle)) -Hle #Hle |
---|
[2141] | 992 | [ >lookup_insert_miss |
---|
[2316] | 993 | [2: @bitvector_of_nat_abs |
---|
| 994 | [3: @lt_to_not_eq @Hle |
---|
| 995 | |1: @(transitive_lt ??? Hle) |
---|
| 996 | ] @prefix_ok |
---|
| 997 | ] |
---|
| 998 | | >Hle >lookup_insert_hit |
---|
| 999 | ] |
---|
| 1000 | normalize nodelta cases instr in Hjump Heq1; |
---|
[3039] | 1001 | [1,8: #pi normalize nodelta cases pi |
---|
[2316] | 1002 | try (#y #id #Hjump #Heq1) try (#id #Hjump #Heq1) try (#Hjump #Heq1) |
---|
| 1003 | try (cases Hjump) lapply Heq1 -Heq1 lapply Hjump -Hjump lapply id -id |
---|
[3039] | 1004 | |2,3,7,9,10,14: #y [3,6: #id #off] normalize nodelta #abs cases abs |
---|
| 1005 | |5,12: #x #y #z #abs cases abs |
---|
[2316] | 1006 | ] |
---|
| 1007 | #id #Hjump normalize nodelta #Heq1 |
---|
| 1008 | <(proj1 ?? (pair_destruct ?????? Heq1)) |
---|
| 1009 | <(proj2 ?? (pair_destruct ?????? Heq1)) <Hjump |
---|
| 1010 | whd in match (select_jump_length labels old_sigma ? (|prefix|) dest); |
---|
| 1011 | whd in match (select_call_length labels old_sigma ? (|prefix|) dest); |
---|
| 1012 | whd in match (select_reljump_length labels old_sigma ? (|prefix|) dest ?); |
---|
| 1013 | try (>(le_to_leb_true … (le_S_to_le … Hle))) |
---|
| 1014 | try (>Hle >(le_to_leb_true … (le_n (|prefix|))) >(le_to_leb_true … (le_n (|prefix|)))) |
---|
| 1015 | normalize nodelta |
---|
| 1016 | inversion (absolute_jump_cond ??) #aj_poss #disp2 normalize nodelta |
---|
| 1017 | inversion (short_jump_cond ??); #sj_poss #disp normalize nodelta |
---|
| 1018 | cases sj_poss #Hsj #Haj cases old_length normalize nodelta |
---|
| 1019 | try (>Hsj %) try (cases aj_poss @I) |
---|
| 1020 | [1,2,3: @(subaddressing_mode_elim … y) #w >Hsj % |
---|
| 1021 | |4: cases y in Hsj; #y cases y #a1 #a2 #Hsj normalize nodelta |
---|
| 1022 | @(subaddressing_mode_elim … a1) [2,3: #w >Hsj %] |
---|
| 1023 | @(subaddressing_mode_elim … a2) #w >Hsj % |
---|
| 1024 | |5: cases y in Hsj; * try (#a1 #a2 #Hsj) try (#a1 #Hsj) normalize nodelta |
---|
| 1025 | try (>Hsj %) try (cases a2) try (cases a1) |
---|
| 1026 | ] |
---|
| 1027 | <Hinc_pc in Hsj; #Hsj |
---|
| 1028 | try (>Hsj %) |
---|
| 1029 | [1,2,3: @(subaddressing_mode_elim … y) #w >Hsj % |
---|
| 1030 | |4: cases y in Hsj; #y cases y #a1 #a2 #Hsj normalize nodelta |
---|
| 1031 | @(subaddressing_mode_elim … a1) [2,3: #w >Hsj %] |
---|
| 1032 | @(subaddressing_mode_elim … a2) #w >Hsj % |
---|
| 1033 | |5: cases y in Hsj; * try (#a1 #a2 #Hsj) try (#a1 #Hsj) normalize nodelta |
---|
| 1034 | try (>Hsj %) try (cases a2) try (cases a1) |
---|
| 1035 | ] |
---|
| 1036 | try (cases aj_poss in Haj; #Haj >Haj %) cases aj_poss in Haj; #Haj try @I |
---|
| 1037 | normalize nodelta |
---|
| 1038 | <Hinc_pc in Haj; #Haj >Haj % |
---|
| 1039 | | normalize nodelta lapply (Hold_compact (|prefix|) ?) |
---|
| 1040 | [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r ] |
---|
| 1041 | inversion (lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) |
---|
| 1042 | [ #_ #H cases H |
---|
| 1043 | | #x cases x -x #opc #ojl #EQ normalize nodelta |
---|
| 1044 | inversion (lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) |
---|
| 1045 | [ #_ #H cases H |
---|
| 1046 | | #x cases x -x #oSpc #oSjl #SEQ normalize nodelta -Hold_compact #Hold_compact |
---|
| 1047 | >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hold_compact |
---|
| 1048 | >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; normalize nodelta |
---|
| 1049 | #Holdeq >prf >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); |
---|
| 1050 | >p1 cases instr in Hjump Heq1; |
---|
[3039] | 1051 | [1,8: #pi normalize nodelta cases pi |
---|
[2316] | 1052 | try (#y #id #Hjump #Heq1) try (#id #Hjump #Heq1) try (#Hjump #Heq1) |
---|
| 1053 | try (cases Hjump) lapply Heq1 -Heq1 lapply Hjump -Hjump lapply id -id |
---|
[3039] | 1054 | |2,3,7,9,10,14: #y [3,6: #id #off] normalize nodelta #abs cases abs |
---|
| 1055 | |5,12: #x #y #z #abs cases abs |
---|
[2316] | 1056 | ] |
---|
| 1057 | #id #Hjump normalize nodelta <Hjump #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) |
---|
| 1058 | whd in match (select_jump_length labels old_sigma ? (|prefix|) dest); |
---|
| 1059 | whd in match (select_call_length labels old_sigma ? (|prefix|) dest); |
---|
| 1060 | whd in match (select_reljump_length labels old_sigma ? (|prefix|) dest ?); >Hle normalize nodelta |
---|
| 1061 | >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) <(proj2 ?? (pair_destruct ?????? Holdeq)) |
---|
| 1062 | cases ojl normalize nodelta |
---|
| 1063 | [1,2,4,5,8,11,14,16,17,19,20,23,26: |
---|
| 1064 | inversion (short_jump_cond ??); #sj_poss #disp #Hsj cases sj_poss try (%) @I |
---|
| 1065 | |3,6,9,12,15,18,21,24,27,30,33: @I |
---|
| 1066 | |28,29: inversion (short_jump_cond ??); #sj_poss #disp #Hsj normalize nodelta |
---|
| 1067 | cases sj_poss [1,3: % |2,4: inversion (absolute_jump_cond ??); |
---|
| 1068 | #aj_poss #disp2 #Haj cases aj_poss try (%) @I ] |
---|
| 1069 | |31,32: inversion (absolute_jump_cond ??); #aj_poss #disp #Haj cases aj_poss |
---|
| 1070 | % |
---|
| 1071 | ] |
---|
| 1072 | [1,2,3,5: @(subaddressing_mode_elim … y) #w |
---|
| 1073 | cases (short_jump_cond ??) #sj_poss #disp cases sj_poss |
---|
| 1074 | try (%) @I |
---|
| 1075 | |4: cases y * try (#a1 #a2) try (#a1) normalize nodelta |
---|
| 1076 | @(subaddressing_mode_elim … a1) |
---|
| 1077 | [2,3: #w cases (short_jump_cond ??); #sj_poss #disp cases sj_poss try (%) @I] |
---|
| 1078 | @(subaddressing_mode_elim … a2) #w whd in match (length_of ?); |
---|
| 1079 | normalize nodelta cases (short_jump_cond ??); #sj_poss #disp cases sj_poss |
---|
| 1080 | try (%) @I |
---|
| 1081 | ] |
---|
| 1082 | ] |
---|
| 1083 | ] |
---|
| 1084 | ] |
---|
| 1085 | ] |
---|
| 1086 | <Hi >lookup_insert_miss |
---|
| 1087 | [ >lookup_insert_miss |
---|
| 1088 | [ >lookup_insert_miss |
---|
| 1089 | [ >lookup_insert_hit >lookup_insert_miss |
---|
[2141] | 1090 | [ >lookup_insert_miss |
---|
[2316] | 1091 | [ >Hinc_pc <Hi #H @H |
---|
| 1092 | ] |
---|
| 1093 | ] |
---|
| 1094 | ] |
---|
| 1095 | ] |
---|
| 1096 | ] |
---|
| 1097 | @bitvector_of_nat_abs |
---|
| 1098 | try (>Hi @prefix_ok) try (>Hi @prefix_ok1) |
---|
| 1099 | [1,3: @(transitive_lt … prefix_ok) <Hi @le_S_S |
---|
| 1100 | | @lt_to_not_eq @le_S_S |
---|
| 1101 | | @lt_to_not_eq @le_S @le_S_S |
---|
| 1102 | |5,7: @lt_to_not_eq @le_n |
---|
| 1103 | |6,8: whd >Hi @le_S_to_le @prefix_ok |
---|
| 1104 | |9: @lt_to_not_eq @le_S @le_n |
---|
| 1105 | ] |
---|
| 1106 | @leb_true_to_le @Hle |
---|
[2240] | 1107 | qed. |
---|
| 1108 | |
---|
| 1109 | (* One step in the search for a jump expansion fixpoint. *) |
---|
| 1110 | definition jump_expansion_step: ∀program:(Σl:list labelled_instruction. |
---|
| 1111 | S (|l|) < 2^16 ∧ is_well_labelled_p l). |
---|
| 1112 | ∀labels:(Σlm:label_map.∀l. |
---|
| 1113 | occurs_exactly_once ?? l program → |
---|
| 1114 | bitvector_of_nat ? (lookup_def … lm l 0) = |
---|
[2264] | 1115 | address_of_word_labels program l). |
---|
[2240] | 1116 | ∀old_policy:(Σpolicy:ppc_pc_map. |
---|
| 1117 | (* out_of_program_none program policy *) |
---|
| 1118 | And (And (And (And (not_jump_default program policy) |
---|
| 1119 | (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) |
---|
| 1120 | (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉))) |
---|
| 1121 | (sigma_compact_unsafe program labels policy)) |
---|
| 1122 | (\fst policy ≤ 2^16)). |
---|
| 1123 | (Σx:bool × (option ppc_pc_map). |
---|
| 1124 | let 〈no_ch,y〉 ≝ x in |
---|
| 1125 | match y with |
---|
| 1126 | [ None ⇒ nec_plus_ultra program old_policy |
---|
| 1127 | | Some p ⇒ And (And (And (And (And (And (And |
---|
| 1128 | (not_jump_default program p) |
---|
| 1129 | (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) |
---|
| 1130 | (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉))) |
---|
| 1131 | (jump_increase program old_policy p)) |
---|
| 1132 | (sigma_compact_unsafe program labels p)) |
---|
| 1133 | (sigma_jump_equal program old_policy p → no_ch = true)) |
---|
| 1134 | (no_ch = true → sigma_pc_equal program old_policy p)) |
---|
| 1135 | (\fst p ≤ 2^16) |
---|
| 1136 | ]) |
---|
| 1137 | ≝ |
---|
| 1138 | λprogram.λlabels.λold_sigma. |
---|
[3097] | 1139 | let 〈ignore,res〉 ≝ |
---|
[2240] | 1140 | pi1 ?? (foldl_strong (option Identifier × pseudo_instruction) |
---|
[3097] | 1141 | (λprefix.Σxx:(ℕ × Word) × (ℕ × ppc_pc_map). |
---|
| 1142 | let 〈prefixlens,x〉 ≝ xx in |
---|
| 1143 | let 〈prefixlen,bvprefixlen〉 ≝ prefixlens in |
---|
[2240] | 1144 | let 〈added,policy〉 ≝ x in |
---|
[3097] | 1145 | And (And (prefixlen = |prefix|) (bvprefixlen = bitvector_of_nat … prefixlen)) |
---|
| 1146 | (And (And (And (And (And (And (And (And (And (not_jump_default prefix policy) |
---|
[2240] | 1147 | (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) |
---|
| 1148 | (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉))) |
---|
| 1149 | (jump_increase prefix old_sigma policy)) |
---|
| 1150 | (sigma_compact_unsafe prefix labels policy)) |
---|
| 1151 | (sigma_jump_equal prefix old_sigma policy → added = 0)) |
---|
| 1152 | (added = 0 → sigma_pc_equal prefix old_sigma policy)) |
---|
| 1153 | (out_of_program_none prefix policy)) |
---|
| 1154 | (\fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉) = |
---|
| 1155 | \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) + added)) |
---|
[3097] | 1156 | (sigma_safe prefix labels old_sigma policy))) |
---|
[2240] | 1157 | program |
---|
[3097] | 1158 | (λprefix.λx.λtl.λprf.λprefixlens_acc. |
---|
| 1159 | let 〈prefixlens,acc〉 ≝ (pi1 ?? prefixlens_acc) in |
---|
| 1160 | let 〈prefixlen,bvprefixlen〉 ≝ prefixlens in |
---|
| 1161 | let bvSprefixlen ≝ increment … bvprefixlen in |
---|
| 1162 | let 〈inc_added, inc_pc_sigma〉 ≝ acc in |
---|
[2240] | 1163 | let 〈label,instr〉 ≝ x in |
---|
| 1164 | (* Now, we must add the current ppc and its pc translation. |
---|
| 1165 | * Three possibilities: |
---|
| 1166 | * - Instruction is not a jump; i.e. constant size whatever the sigma we use; |
---|
| 1167 | * - Instruction is a backward jump; we can use the sigma we're constructing, |
---|
| 1168 | * since it will already know the translation of its destination; |
---|
| 1169 | * - Instruction is a forward jump; we must use the old sigma (the new sigma |
---|
| 1170 | * does not know the translation yet), but compensate for the jumps we |
---|
| 1171 | * have lengthened. |
---|
| 1172 | *) |
---|
| 1173 | let add_instr ≝ match instr with |
---|
[3095] | 1174 | [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma prefixlen j) |
---|
| 1175 | | Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma prefixlen c) |
---|
| 1176 | | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma prefixlen i |
---|
[2240] | 1177 | | _ ⇒ None ? |
---|
| 1178 | ] in |
---|
| 1179 | let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in |
---|
| 1180 | let old_length ≝ |
---|
[3095] | 1181 | \snd (bvt_lookup … bvprefixlen (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in |
---|
[2240] | 1182 | let old_size ≝ instruction_size_jmplen old_length instr in |
---|
| 1183 | let 〈new_length, isize〉 ≝ match add_instr with |
---|
| 1184 | [ None ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉 |
---|
| 1185 | | Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉 |
---|
| 1186 | ] in |
---|
| 1187 | let new_added ≝ match add_instr with |
---|
| 1188 | [ None ⇒ inc_added |
---|
| 1189 | | Some x ⇒ plus inc_added (minus isize old_size) |
---|
| 1190 | ] in |
---|
| 1191 | let old_Slength ≝ |
---|
[3095] | 1192 | \snd (bvt_lookup … bvSprefixlen (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in |
---|
[2240] | 1193 | let updated_sigma ≝ |
---|
| 1194 | (* we add the new PC to the next position and the new jump length to this one *) |
---|
[3095] | 1195 | bvt_insert … bvSprefixlen 〈inc_pc + isize, old_Slength〉 |
---|
| 1196 | (bvt_insert … bvprefixlen 〈inc_pc, new_length〉 inc_sigma) in |
---|
[3097] | 1197 | 〈〈S prefixlen,increment … bvprefixlen〉,〈new_added, 〈plus inc_pc isize, updated_sigma〉〉〉 |
---|
| 1198 | ) 〈〈0,zero 16〉,〈0, 〈0, |
---|
[2240] | 1199 | bvt_insert … |
---|
| 1200 | (bitvector_of_nat ? 0) |
---|
| 1201 | 〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉 |
---|
[3097] | 1202 | (Stub ??)〉〉〉 |
---|
[2240] | 1203 | ) in |
---|
[3097] | 1204 | let 〈final_added, final_policy〉 ≝ res in |
---|
[2240] | 1205 | if gtb (\fst final_policy) 2^16 then |
---|
| 1206 | 〈eqb final_added 0, None ?〉 |
---|
| 1207 | else |
---|
| 1208 | 〈eqb final_added 0, Some ? final_policy〉. |
---|
| 1209 | [ normalize nodelta @nmk #Habs lapply p -p cases (foldl_strong ? (λ_.Σx.?) ???) |
---|
[3097] | 1210 | #x #H #Heq >Heq in H; normalize nodelta -Heq -x cases ignore #prefixlen #bvprefixlen |
---|
| 1211 | >p1 -res normalize nodelta * #EQprefixlens #Hind |
---|
[2240] | 1212 | (* USE: inc_pc = fst of policy (from fold) *) |
---|
[3097] | 1213 | >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p2; |
---|
[2240] | 1214 | (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *) |
---|
| 1215 | lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) |
---|
| 1216 | #Hsig #Hge |
---|
| 1217 | (* USE: added = 0 → policy_pc_equal (from fold) *) |
---|
| 1218 | lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) ? (|program|) (le_n (|program|))) |
---|
| 1219 | [ (* USE: policy_jump_equal → added = 0 (from fold) *) |
---|
| 1220 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi |
---|
[2652] | 1221 | inversion (is_jump (\snd (nth i ? program 〈None ?, Comment EmptyString〉))) |
---|
[2240] | 1222 | [ #Hj |
---|
| 1223 | (* USE: policy_increase (from fold) *) |
---|
| 1224 | lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi)) |
---|
| 1225 | lapply (Habs i Hi ?) [ >Hj %] |
---|
| 1226 | cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉) |
---|
| 1227 | #opc #oj |
---|
| 1228 | cases (bvt_lookup … (bitvector_of_nat ? i) (\snd final_policy) 〈0,short_jump〉) |
---|
| 1229 | #pc #j normalize nodelta #Heq >Heq cases j |
---|
| 1230 | [1,2: #abs cases abs #abs2 try (cases abs2) @refl |
---|
| 1231 | |3: #_ @refl |
---|
| 1232 | ] |
---|
| 1233 | | #Hnj |
---|
| 1234 | (* USE: not_jump_default (from fold and old_sigma) *) |
---|
| 1235 | >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi ?) |
---|
| 1236 | [2: >Hnj %] |
---|
| 1237 | >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi ?) try % |
---|
| 1238 | >Hnj % |
---|
| 1239 | ] |
---|
| 1240 | | #abs >abs in Hsig; #Hsig |
---|
| 1241 | @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge |
---|
| 1242 | ] |
---|
[3097] | 1243 | | normalize nodelta lapply p -p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); |
---|
| 1244 | #x normalize nodelta #H #H2 |
---|
| 1245 | >H2 in H; normalize nodelta -H2 -x cases ignore -ignore #prefixlen #bvprefixlen |
---|
| 1246 | normalize nodelta >p1 -p1 normalize nodelta * #EQprefixlens #H @conj |
---|
| 1247 | [ @conj [ @conj |
---|
[2240] | 1248 | [ (* USE[pass]: not_jump_default, 0 ↦ 0, inc_pc = fst policy, |
---|
| 1249 | * jump_increase, sigma_compact_unsafe (from fold) *) |
---|
| 1250 | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) |
---|
| 1251 | | #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *) |
---|
| 1252 | @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) @H2 |
---|
| 1253 | ] |
---|
| 1254 | | (* USE[pass]: added = 0 → sigma_pc_equal (from fold) *) |
---|
| 1255 | #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2 |
---|
| 1256 | ] |
---|
[3097] | 1257 | | @not_lt_to_le @ltb_false_to_not_lt @p2 |
---|
[2240] | 1258 | ] |
---|
[3095] | 1259 | |4: |
---|
[3097] | 1260 | lapply (pi2 ?? prefixlens_acc) >p in ⊢ (% → ?); -prefixlens_acc normalize nodelta |
---|
| 1261 | >p1 -prefixlens >p2 -acc >p3 in prf; -x #prf normalize nodelta inversion inc_pc_sigma |
---|
[2245] | 1262 | #inc_pc #inc_sigma #Hips normalize nodelta |
---|
[3095] | 1263 | inversion (bvt_lookup … bvprefixlen (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) |
---|
[3097] | 1264 | #old_pc #old_length #Holdeq ** #Hpolicy1 >Hpolicy1 -prefixlen |
---|
| 1265 | #Hpolicy2 >Hpolicy2 in Holdeq; -bvprefixlen #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim * |
---|
| 1266 | #prefixlen' #bvprefixlen' * #added #policy normalize nodelta @pair_elim #new_length #isize |
---|
| 1267 | normalize nodelta #Heq1 #Heq2 cases (pair_destruct ?????? Heq2) -Heq2 |
---|
| 1268 | #Heq2c cases (pair_destruct ?????? Heq2c) -Heq2c #Heq2c <Heq2c -prefixlen' |
---|
| 1269 | #Heq2d <Heq2d -bvprefixlen' #Heq2 |
---|
[2240] | 1270 | cut (S (|prefix|) < 2^16) |
---|
| 1271 | [ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length |
---|
| 1272 | <plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1 |
---|
| 1273 | cut (|prefix| < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok |
---|
[3097] | 1274 | cases (pair_destruct ?????? Heq2) -Heq2 #Heq2a |
---|
| 1275 | >(?:increment … (bitvector_of_nat … (|prefix|)) = bitvector_of_nat … (S (|prefix|))) |
---|
| 1276 | [2: >increment_zero_bitvector_of_nat_1 <add_bitvector_of_nat %] |
---|
| 1277 | #Heq2b <Heq2a normalize nodelta |
---|
| 1278 | % [ % | % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]] |
---|
| 1279 | [ >length_append <plus_n_Sm <plus_n_O % |
---|
| 1280 | | % |
---|
| 1281 | | (* not_jump_default *) |
---|
[2240] | 1282 | @(jump_expansion_step1 … Heq1 Heq2b) try assumption |
---|
| 1283 | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) |
---|
| 1284 | | (* 0 ↦ 0 *) |
---|
| 1285 | @(jump_expansion_step2 … Heq2b) try assumption |
---|
| 1286 | [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) |
---|
| 1287 | | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) ] |
---|
| 1288 | | (* inc_pc = fst of policy *) |
---|
| 1289 | <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl |
---|
| 1290 | | (* jump_increase *) |
---|
[3097] | 1291 | @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … ???? old_length Holdeq |
---|
[2240] | 1292 | … Heq1 prefix_ok1 prefix_ok Heq2b) |
---|
| 1293 | try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) |
---|
[3097] | 1294 | try % cases (pi2 … old_sigma) * * * #Hnjd #_ #_ #_ #_ @Hnjd |
---|
[2240] | 1295 | | (* sigma_compact_unsafe *) |
---|
| 1296 | @(jump_expansion_step4 … Heq1 … Heq2b) try assumption |
---|
| 1297 | try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) |
---|
| 1298 | try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) |
---|
| 1299 | @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) |
---|
| 1300 | | (* policy_jump_equal → added = 0 *) |
---|
[2316] | 1301 | @(jump_expansion_step5 … inc_added … Holdeq … Heq1 … Heq2b) try assumption |
---|
[3097] | 1302 | try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) try % |
---|
[2240] | 1303 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) |
---|
[2248] | 1304 | | (* added = 0 → policy_pc_equal *) |
---|
[3097] | 1305 | >Heq2a |
---|
[2248] | 1306 | @(jump_expansion_step6 (pi1 ?? program) (pi1 ?? labels) (pi1 ?? old_sigma) … Holdeq … Heq1 … Heq2a Heq2b) try assumption |
---|
[2240] | 1307 | try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) |
---|
[2248] | 1308 | try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) |
---|
[3097] | 1309 | try (cases (pi2 … old_sigma) * #_ #X #_ @X) % |
---|
[2244] | 1310 | | (* out_of_program_none *) |
---|
| 1311 | @(jump_expansion_step7 … Heq2b) |
---|
| 1312 | @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) |
---|
| 1313 | | (* lookup p = lookup old_sigma + added *) |
---|
[3097] | 1314 | >Heq2a |
---|
[2244] | 1315 | @(jump_expansion_step8 (pi1 ?? program) (pi1 ?? labels) (pi1 ?? old_sigma) … Holdeq … Heq1 Heq2a Heq2b) try assumption |
---|
| 1316 | [ cases (pi2 … old_sigma) * #_ #H1 #H2 % assumption |
---|
[3097] | 1317 | | % |
---|
[2244] | 1318 | | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) |
---|
[3097] | 1319 | | >(proj2 ?? (proj1 ?? Hpolicy)) @eq_f2 try % |
---|
| 1320 | cases (lookup (? × ?)????) in Holdeq; #x #y #H destruct (H) % |
---|
| 1321 | ] |
---|
[2248] | 1322 | | (* sigma_safe *) |
---|
[3097] | 1323 | >Heq2a |
---|
| 1324 | @(jump_expansion_step9 … prf … Holdeq … Heq1 prefix_ok1 prefix_ok) |
---|
[2316] | 1325 | [ @inc_pc_sigma |
---|
[3097] | 1326 | | % |
---|
[2316] | 1327 | | >Hips % |
---|
| 1328 | | @inc_added |
---|
| 1329 | | >Hips @Heq2b |
---|
| 1330 | | @(proj2 ?? (proj1 ?? (pi2 ?? old_sigma))) |
---|
[3097] | 1331 | | >Hips >(proj2 ?? (proj1 ?? Hpolicy)) @eq_f2 try % |
---|
| 1332 | cases (lookup (? × ?)????) in Holdeq; #x #y #H destruct (H) % |
---|
[2316] | 1333 | | >Hips @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) |
---|
| 1334 | | >Hips @(proj2 ?? Hpolicy) |
---|
| 1335 | ] |
---|
| 1336 | ] |
---|
[3097] | 1337 | | normalize nodelta % [% | % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]] |
---|
| 1338 | [ % |
---|
| 1339 | | % |
---|
| 1340 | | #i cases i |
---|
[2034] | 1341 | [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
| 1342 | | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
| 1343 | ] |
---|
[2141] | 1344 | | >lookup_insert_hit @refl |
---|
[3097] | 1345 | | >lookup_insert_hit @refl |
---|
[2059] | 1346 | | #i #Hi <(le_n_O_to_eq … Hi) |
---|
| 1347 | >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉) |
---|
| 1348 | #a #b normalize nodelta %2 @refl |
---|
[2034] | 1349 | | #i cases i |
---|
| 1350 | [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
| 1351 | | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
| 1352 | ] |
---|
[2141] | 1353 | | #_ % |
---|
| 1354 | | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit |
---|
| 1355 | (* USE: 0 ↦ 0 (from old_sigma) *) |
---|
| 1356 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) |
---|
[2152] | 1357 | | #i cases i |
---|
| 1358 | [ #Hi2 @conj |
---|
| 1359 | [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by / |
---|
| 1360 | | >lookup_opt_insert_hit #H destruct (H) |
---|
| 1361 | ] |
---|
| 1362 | | -i #i #Hi2 @conj |
---|
| 1363 | [ #Hi >lookup_opt_insert_miss |
---|
| 1364 | [ / by refl/ |
---|
| 1365 | | @bitvector_of_nat_abs |
---|
| 1366 | [ @Hi2 |
---|
| 1367 | | / by / |
---|
| 1368 | | @sym_neq @lt_to_not_eq / by / |
---|
| 1369 | ] |
---|
| 1370 | ] |
---|
| 1371 | | #_ @le_S_S @le_O_n |
---|
| 1372 | ] |
---|
| 1373 | ] |
---|
| 1374 | | >lookup_insert_hit (* USE: 0 ↦ 0 (from old_sigma) *) |
---|
| 1375 | >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) <plus_n_O % |
---|
[2034] | 1376 | | #i cases i |
---|
| 1377 | [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
| 1378 | | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
| 1379 | ] |
---|
| 1380 | ] |
---|
| 1381 | ] |
---|
[3097] | 1382 | qed. |
---|