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