Changeset 2225 for src/ASM/PolicyStep.ma
 Timestamp:
 Jul 20, 2012, 6:15:40 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyStep.ma
r2220 r2225 4 4 include alias "basics/logic.ma". 5 5 6 lemma not_is_jump_to_destination_of_Nome: 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 6 11 lemma jump_expansion_step1: 7 ∀program : Σl:list labelled_instruction.S (l)< 2 \sup 16 ∧is_well_labelled_p l. 8 ∀prefix,x,tl. pi1 … program=prefix@[x]@tl → 12 ∀prefix: list labelled_instruction. S (prefix) < 2^16 → prefix < 2^16 → (*redundant*) 9 13 ∀labels: label_map. 10 14 ∀old_sigma : ppc_pc_map. … … 38 42 = policy. 39 43 not_jump_default (prefix@[〈label,instr〉]) policy. 40 #pr ogram #prefix #x #tl #prf#labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc41 #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2 44 #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc 45 #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2 42 46 #i >append_length <commutative_plus #Hi normalize in Hi; 43 47 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi … … 46 50 [ >(nth_append_first ? i prefix ?? Hi) 47 51 @(Hpolicy i Hi) 48  @bitvector_of_nat_abs 49 [ @(transitive_lt ??? Hi) ] 50 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 51 @le_plus_n_r 52  @lt_to_not_eq @Hi 53 ] 52  @bitvector_of_nat_abs try assumption 53 [ @(transitive_lt ??? Hi) assumption ] 54 @lt_to_not_eq @Hi 54 55 ] 55  @bitvector_of_nat_abs 56 [ @(transitive_lt ??? Hi) @le_S_to_le ] 57 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length 58 <plus_n_Sm @le_S_S @le_plus_n_r 59  @lt_to_not_eq @le_S @Hi 60 ] 56  @bitvector_of_nat_abs try assumption 57 [ @(transitive_lt ??? Hi) assumption ] 58 @lt_to_not_eq @le_S @Hi 61 59 ] 62 60  <Heq2 >Hi >lookup_insert_miss 63 61 [ >lookup_insert_hit cases instr in Heq1; 64 62 [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl 65 4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second 66 [1,3: <minus_n_n whd in match (nth ????); % 67 2,4: @le_n 68 ] 69 1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi 70 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 71 [1,2,3,6,7,24,25: #x #y 72 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1 73 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl 74 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta 75 #_ #H @⊥ cases H #H2 @H2 % 76 ] 77 ] 78  @bitvector_of_nat_abs 79 [ @le_S_to_le ] 80 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S 81 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 82  @lt_to_not_eq @le_n 83 ] 84 ] 85 ] 63 4,5: #x normalize nodelta #Heq1 >nth_append_second try % 64 <minus_n_n #abs cases abs 65 1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); 66 #H #non_jump whd in match (jump_expansion_step_instruction ??????) in H; 67 >not_is_jump_to_destination_of_Nome in H; normalize nodelta // ] 68  @bitvector_of_nat_abs [3: //  @le_S_to_le ] assumption ]] 86 69 qed. 70 71 lemma jump_expansion_step2: 72 ∀prefix: list labelled_instruction. S (prefix) < 2^16 → prefix < 2^16 → (*redundant*) 73 ∀labels : label_map. 74 ∀old_sigma : ppc_pc_map. 75 ∀inc_pc : ℕ. 76 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16). 77 ∀Hpolicy1 : 78 \fst (lookup … (bitvector_of_nat … O) inc_sigma 〈O,short_jump〉) = O. 79 ∀Hpolicy2: 80 inc_pc =\fst (lookup … (bitvector_of_nat … (prefix)) inc_sigma 〈O,short_jump〉). 81 ∀policy : ppc_pc_map. 82 ∀new_length : jump_length. 83 ∀isize : ℕ. 84 ∀Heq2 : 85 〈inc_pc+isize, 86 insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 87 〈inc_pc+isize, 88 \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 89 (\snd old_sigma) 〈O,short_jump〉)〉 90 (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 91 〈inc_pc,new_length〉 inc_sigma)〉 92 = policy. 93 \fst (lookup … (bitvector_of_nat … O) (\snd policy) 〈O,short_jump〉) = O. 94 #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_pc 95 #inc_sigma #Hpolicy1 #Hpolicy2 #policy #new_length #isize #Heq2 96 <Heq2 >lookup_insert_miss 97 [ cases (decidable_eq_nat 0 (prefix)) 98 [ #Heq <Heq >lookup_insert_hit >Hpolicy2 <Heq @Hpolicy1 99  #Hneq >lookup_insert_miss 100 [ @Hpolicy1 101  @bitvector_of_nat_abs try assumption @lt_O_S ]] 102  @bitvector_of_nat_abs [ @lt_O_S  @prefix_ok1  3: @lt_to_not_eq @lt_O_S ] ] 103 qed. 104 105 (* 106 lemma jump_expansion_step3: 107 (* 108 program : 109 (Σl:list labelled_instruction.S (l)< 2 \sup 16 ∧is_well_labelled_p l) 110 labels : 111 (Σlm:label_map 112 .(∀l:identifier ASMTag 113 .occurs_exactly_once ASMTag pseudo_instruction l program 114 →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O) 115 =address_of_word_labels_code_mem program l))*) 116 ∀old_sigma : 117 Σpolicy:ppc_pc_map 118 .True(*not_jump_default program policy 119 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 120 〈O,short_jump〉) 121 =O 122 ∧\fst policy 123 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (program)) 124 (\snd policy) 〈O,short_jump〉) 125 ∧sigma_compact_unsafe program labels policy 126 ∧\fst policy≤ 2 \sup 16*). 127 ∀prefix : list (option Identifier×pseudo_instruction). (* 128 x : (option Identifier×pseudo_instruction) 129 tl : (list (option Identifier×pseudo_instruction)) 130 prf : (program=prefix@[x]@tl) 131 acc : 132 (Σx0:ℕ×ppc_pc_map 133 .(let 〈added,policy〉 ≝x0 in 134 not_jump_default prefix policy 135 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 136 〈O,short_jump〉) 137 =O 138 ∧\fst policy 139 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 140 (\snd policy) 〈O,short_jump〉) 141 ∧jump_increase prefix old_sigma policy 142 ∧sigma_compact_unsafe prefix labels policy 143 ∧(sigma_jump_equal prefix old_sigma policy→added=O) 144 ∧(added=O→sigma_pc_equal prefix old_sigma policy) 145 ∧out_of_program_none prefix policy 146 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 147 (\snd policy) 〈O,short_jump〉) 148 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 149 (\snd old_sigma) 〈O,short_jump〉) 150 +added 151 ∧sigma_safe prefix labels added old_sigma policy)) 152 inc_added : ℕ 153 inc_pc_sigma : ppc_pc_map 154 p : (acc≃〈inc_added,inc_pc_sigma〉)*) 155 ∀label : option Identifier. 156 ∀instr : pseudo_instruction.(* 157 p1 : (x≃〈label,instr〉) 158 add_instr ≝ 159 match instr 160 in pseudo_instruction 161 return λ_:pseudo_instruction.(option jump_length) 162 with 163 [Instruction (i:(preinstruction Identifier))⇒ 164 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 165 (prefix) i 166 Comment (_:String)⇒None jump_length 167 Cost (_:costlabel)⇒None jump_length 168 Jmp (j:Identifier)⇒ 169 Some jump_length 170 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 171 Call (c:Identifier)⇒ 172 Some jump_length 173 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 174 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 175 inc_pc : ℕ 176 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16) 177 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉) 178 old_pc : ℕ 179 old_length : jump_length 180 Holdeq : 181 (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) (\snd old_sigma) 182 〈O,short_jump〉 183 =〈old_pc,old_length〉) 184 Hpolicy : 185 (not_jump_default prefix 〈inc_pc,inc_sigma〉 186 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma 187 〈O,short_jump〉) 188 =O 189 ∧inc_pc 190 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma 191 〈O,short_jump〉) 192 ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉 193 ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉 194 ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O) 195 ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉) 196 ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉 197 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma 198 〈O,short_jump〉) 199 =old_pc+inc_added 200 ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉) 201 added : ℕ*) 202 ∀policy : ppc_pc_map. 203 (*new_length : jump_length 204 isize : ℕ 205 Heq1 : 206 (match 207 match instr 208 in pseudo_instruction 209 return λ_:pseudo_instruction.(option jump_length) 210 with 211 [Instruction (i:(preinstruction Identifier))⇒ 212 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 213 (prefix) i 214 Comment (_:String)⇒None jump_length 215 Cost (_:costlabel)⇒None jump_length 216 Jmp (j:Identifier)⇒ 217 Some jump_length 218 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 219 Call (c:Identifier)⇒ 220 Some jump_length 221 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 222 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 223 in option 224 return λ_0:(option jump_length).(jump_length×ℕ) 225 with 226 [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 227 Some (pl:jump_length)⇒ 228 〈max_length old_length pl, 229 instruction_size_jmplen (max_length old_length pl) instr〉] 230 =〈new_length,isize〉) 231 prefix_ok1 : (S (prefix)< 2 \sup 16 ) 232 prefix_ok : (prefix< 2 \sup 16 ) 233 Heq2a : 234 (match 235 match instr 236 in pseudo_instruction 237 return λ_0:pseudo_instruction.(option jump_length) 238 with 239 [Instruction (i:(preinstruction Identifier))⇒ 240 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 241 (prefix) i 242 Comment (_0:String)⇒None jump_length 243 Cost (_0:costlabel)⇒None jump_length 244 Jmp (j:Identifier)⇒ 245 Some jump_length 246 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 247 Call (c:Identifier)⇒ 248 Some jump_length 249 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 250 Mov (_0:[[dptr]]) (_00:Identifier)⇒None jump_length] 251 in option 252 return λ_0:(option jump_length).ℕ 253 with 254 [None⇒inc_added 255 Some (x0:jump_length)⇒ 256 inc_added+(isizeinstruction_size_jmplen old_length instr)] 257 =added) 258 Heq2b : 259 (〈inc_pc+isize, 260 insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 261 〈inc_pc+isize, 262 \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 263 (\snd old_sigma) 〈O,short_jump〉)〉 264 (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 265 〈inc_pc,new_length〉 inc_sigma)〉 266 =policy)*) 267 jump_increase (prefix@[〈label,instr〉]) old_sigma policy. 268 #old_sigma #prefix #label #instr #policy 269 #i >append_length >commutative_plus #Hi normalize in Hi; 270 cases (le_to_or_lt_eq … Hi) Hi; #Hi 271 [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 272 [ (* USE[pass]: jump_increase *) 273 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi)) 274 <(proj2 ?? (pair_destruct ?????? Heq2)) 275 @pair_elim #opc #oj #EQ1 >lookup_insert_miss 276 [ >lookup_insert_miss 277 [ @pair_elim #pc #j #EQ2 #X @X 278  @bitvector_of_nat_abs 279 [ @(transitive_lt ??? Hi) ] 280 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 281 @le_S_S @le_plus_n_r 282  @lt_to_not_eq @Hi 283 ] 284 ] 285  @bitvector_of_nat_abs 286 [ @(transitive_lt ??? Hi) @le_S_to_le ] 287 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 288 >append_length @le_S_S <plus_n_Sm @le_plus_n_r 289  @lt_to_not_eq @le_S @Hi 290 ] 291 ] 292  >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >Holdeq normalize nodelta 293 >lookup_insert_miss 294 [ >lookup_insert_hit cases (dec_is_jump instr) 295 [ cases instr in Heq1; normalize nodelta 296 [ #pi cases pi 297 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 298 [1,2,3,6,7,24,25: #x #y 299 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj 300 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 301 whd in match jump_expansion_step_instruction; normalize nodelta #Heq1 302 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) 303 @jmpleq_max_length 304 ] 305 2,3,6: #x [3: #y] #_ #Hj cases Hj 306 4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length 307 ] 308  lapply Heq1 Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta 309 [ #pi cases pi 310 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 311 [1,2,3,6,7,24,25: #x #y 312 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 313 whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1 314 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 315 (* USE: not_jump_default (from old_sigma) *) 316 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??) 317 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 318 >prf >nth_append_second 319 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 320 <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 321 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 322 @le_n 323 ] 324 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 325 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 326 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 327 >Holdeq #EQ2 >EQ2 %2 @refl 328 ] 329 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 330 #_ #_ #abs @⊥ @(absurd ? I abs) 331 ] 332 2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 333 (* USE: not_jump_default (from old_sigma) *) 334 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??) 335 [1,4,7: >prf >nth_append_second 336 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 337 2,4,6: @le_n 338 ] 339 2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 340 3,6,9: >Holdeq #EQ2 >EQ2 %2 @refl 341 ] 342 4,5: #x #_ #_ #abs @⊥ @(absurd ? I abs) 343 ] 344 ] 345  @bitvector_of_nat_abs 346 [ @le_S_to_le ] 347 [1,2: @(transitive_lt … (proj1 ?? (pi2 … program))) @le_S_S >prf 348 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 349  @lt_to_not_eq @le_n 350 ] 351 ] 352 ] 353  <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit 354 normalize nodelta 355 cases (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma) 〈0,short_jump〉) 356 #a #b normalize nodelta %2 @refl 357 ] 358 ] 359 qed.*) 87 360 88 361 (* One step in the search for a jump expansion fixpoint. *) … … 190 463 [ (* USE: policy_jump_equal → added = 0 (from fold) *) 191 464 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi 192 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))465 inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 193 466 [ #Hj 194 467 (* USE: policy_increase (from fold) *) 195 468 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi)) 196 lapply (Habs i Hi Hj)469 lapply (Habs i Hi ?) [ >Hj %] 197 470 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉) 198 471 #opc #oj … … 204 477  #Hnj 205 478 (* USE: not_jump_default (from fold and old_sigma) *) 206 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi Hnj) 207 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj) 208 @refl 479 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi ?) 480 [2: >Hnj %] 481 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi ?) try % 482 >Hnj % 209 483 ] 210 484  #abs >abs in Hsig; #Hsig … … 232 506 #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta 233 507 #Heq1 #Heq2 234 @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 508 cut (S (prefix) < 2^16) 509 [ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length 510 <plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1 511 cut (prefix < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok 512 cases (pair_destruct ?????? Heq2) Heq2 #Heq2a #Heq2b 513 % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]] 235 514 (* NOTE: to save memory and speed up work, there's cases daemon here. They can be 236 515 * commented out for full proofs, but this needs a lot of memory and time *) 237 516 [ (* not_jump_default *) 238 cases (pair_destruct ?????? Heq2) Heq2 #_ #Heq2 239 @(jump_expansion_step1 … prf … Heq1 Heq2) 517 @(jump_expansion_step1 … Heq1 Heq2b) try assumption 240 518 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) 241 519  (* 0 ↦ 0 *) 242 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 243 [ cases (decidable_eq_nat 0 (prefix)) 244 [ #Heq <Heq >lookup_insert_hit 245 (* USE: inc_pc = fst policy *) 246 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 247 <Heq 248 (* USE[pass]: 0 ↦ 0 *) 249 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) 250  #Hneq >lookup_insert_miss 251 [ (* USE[pass]: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) 252  @bitvector_of_nat_abs 253 [3: @Hneq] 254 ] 255 ] 256  @bitvector_of_nat_abs 257 [3: @lt_to_not_eq @lt_O_S ] 258 ] 259 [1,3: @lt_O_S 260 2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 261 [2: <plus_n_Sm @le_S_S] 262 @le_plus_n_r 263 ] 264 ] 265  (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2)) 266 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 267 ] 268  (* jump_increase *) (* cases daemon *) 269 #i >append_length >commutative_plus #Hi normalize in Hi; 270 cases (le_to_or_lt_eq … Hi) Hi; #Hi 271 [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 272 [ (* USE[pass]: jump_increase *) 273 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi)) 274 <(proj2 ?? (pair_destruct ?????? Heq2)) 275 @pair_elim #opc #oj #EQ1 >lookup_insert_miss 276 [ >lookup_insert_miss 277 [ @pair_elim #pc #j #EQ2 #X @X 278  @bitvector_of_nat_abs 279 [ @(transitive_lt ??? Hi) ] 280 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 281 @le_S_S @le_plus_n_r 282  @lt_to_not_eq @Hi 283 ] 284 ] 285  @bitvector_of_nat_abs 286 [ @(transitive_lt ??? Hi) @le_S_to_le ] 287 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 288 >append_length @le_S_S <plus_n_Sm @le_plus_n_r 289  @lt_to_not_eq @le_S @Hi 290 ] 291 ] 292  >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >Holdeq normalize nodelta 293 >lookup_insert_miss 294 [ >lookup_insert_hit cases (dec_is_jump instr) 295 [ cases instr in Heq1; normalize nodelta 296 [ #pi cases pi 297 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 298 [1,2,3,6,7,24,25: #x #y 299 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj 300 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 301 whd in match jump_expansion_step_instruction; normalize nodelta #Heq1 302 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) 303 @jmpleq_max_length 304 ] 305 2,3,6: #x [3: #y] #_ #Hj cases Hj 306 4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length 307 ] 308  lapply Heq1 Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta 309 [ #pi cases pi 310 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 311 [1,2,3,6,7,24,25: #x #y 312 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 313 whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1 314 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 315 (* USE: not_jump_default (from old_sigma) *) 316 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??) 317 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 318 >prf >nth_append_second 319 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 320 <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 321 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 322 @le_n 323 ] 324 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 325 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 326 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 327 >Holdeq #EQ2 >EQ2 %2 @refl 328 ] 329 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 330 #_ #_ #abs @⊥ @(absurd ? I abs) 331 ] 332 2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 333 (* USE: not_jump_default (from old_sigma) *) 334 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??) 335 [1,4,7: >prf >nth_append_second 336 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 337 2,4,6: @le_n 338 ] 339 2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 340 3,6,9: >Holdeq #EQ2 >EQ2 %2 @refl 341 ] 342 4,5: #x #_ #_ #abs @⊥ @(absurd ? I abs) 343 ] 344 ] 345  @bitvector_of_nat_abs 346 [ @le_S_to_le ] 347 [1,2: @(transitive_lt … (proj1 ?? (pi2 … program))) @le_S_S >prf 348 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 349  @lt_to_not_eq @le_n 350 ] 351 ] 352 ] 353  <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit 354 normalize nodelta 355 cases (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma) 〈0,short_jump〉) 356 #a #b normalize nodelta %2 @refl 357 ] 358 ] 359  (* sigma_compact_unsafe *) 520 @(jump_expansion_step2 … Heq2b) try assumption 521 [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) 522  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) ] 523  (* inc_pc = fst of policy *) 524 <Heq2b >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 525  (* jump_increase *) 526 cases daemon (*XXX*) 527  (* sigma_compact_unsafe *) cases daemon (* 360 528 #i >append_length <commutative_plus #Hi normalize in Hi; 361 529 <(proj2 ?? (pair_destruct ?????? Heq2)) … … 461 629 ] 462 630 ] 463 ] 464  (* policy_jump_equal → added = 0 *) 631 ] *) 632  (* policy_jump_equal → added = 0 *) cases daemon (* 465 633 <(proj2 ?? (pair_destruct ?????? Heq2)) 466 634 #Heq <(proj1 ?? (pair_destruct ?????? Heq2)) … … 530 698 ] 531 699 ] 532 ] 700 ] *) 533 701  (* added = 0 → policy_pc_equal *) cases daemon 534 702 (* USE[pass]: added = 0 → policy_pc_equal *) … … 831 999 ] 832 1000 ] *) 833 ]834 1001  (* out_of_program_none *) cases daemon 835 1002 (* #i #Hi2 >append_length <commutative_plus @conj … … 870 1037 ] 871 1038 ] *) 872 ]873 1039  (* lookup p = lookup old_sigma + added *) cases daemon 874 1040 (* <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O … … 1003 1169 ] 1004 1170 ] *) 1005 ]1006 1171  (* sigma_safe *) cases daemon (*#i >append_length >commutative_plus #Hi normalize in Hi; 1007 1172 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi … … 1024 1189 [1,4,7: *) 1025 1190 1026 ] 1027  normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj1191 ] 1192  normalize nodelta % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]] 1028 1193 [ #i cases i 1029 1194 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1030 1195  i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O 1031 1196 ] 1197  >lookup_insert_hit @refl 1032 1198  >lookup_insert_hit @refl 1033 ]1034  >lookup_insert_hit @refl1035 ]1036 1199  #i #Hi <(le_n_O_to_eq … Hi) 1037 1200 >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉) 1038 1201 #a #b normalize nodelta %2 @refl 1039 ]1040 1202  #i cases i 1041 1203 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1042 1204  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1043 1205 ] 1044 ]1045 1206  #_ % 1046 ]1047 1207  #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit 1048 1208 (* USE: 0 ↦ 0 (from old_sigma) *) 1049 1209 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) 1050 ]1051 1210  #i cases i 1052 1211 [ #Hi2 @conj … … 1066 1225 ] 1067 1226 ] 1068 ]1069 1227  >lookup_insert_hit (* USE: 0 ↦ 0 (from old_sigma) *) 1070 1228 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) <plus_n_O % 1071 ]1072 1229  #i cases i 1073 1230 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O … … 1077 1234 ] 1078 1235 qed. 1079
Note: See TracChangeset
for help on using the changeset viewer.