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