 Timestamp:
 Jun 28, 2012, 8:08:58 PM (9 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r2101 r2141 5 5 include alias "basics/logic.ma". 6 6 7 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (S (l)) 2^16) (n: ℕ) 7 let rec jump_expansion_internal (program: Σl:list labelled_instruction. 8 lt (S (l)) 2^16 ∧ is_well_labelled_p l) (n: ℕ) 8 9 on n:(Σx:bool × (option ppc_pc_map). 9 10 let 〈no_ch,pol〉 ≝ x in … … 34 35 [ #H / by I/ 35 36  #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj 36 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))37 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 37 38  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 38 39 ] … … 52 53  #j2 #H2 @conj [ @conj [ @conj [ @conj 53 54 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))) 54  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))55 ] 56  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))55  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))) 56 ] 57  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))) 57 58 ] 58 59  @(proj2 ?? H2) 59 60 ] 60  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))) 61 ] 61  #Ht @(equal_compact_unsafe_compact ?? op) 62 [ @(proj2 ?? (proj1 ?? (proj1 ?? H2))) @Ht 63  cases daemon (* add to invvariants *) 64  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))) 65 ] 66 ] 62 67 ] 63 68 ] … … 66 71 [ #_ >p2 #ABS destruct (ABS) 67 72  #map >p2 normalize nodelta 68 #H #eq destruct (eq) @(proj1 ?? H)73 #H #eq destruct (eq) cases daemon (* change order *) 69 74 ] 70 75 ] … … 157 162 qed. 158 163 159 lemma pe_step: ∀program:(Σl:list labelled_instruction.S (l) < 2^16 ).164 lemma pe_step: ∀program:(Σl:list labelled_instruction.S (l) < 2^16 ∧ is_well_labelled_p l). 160 165 ∀n.policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program n))) 161 166 (\snd (pi1 ?? (jump_expansion_internal program (S n)))) → … … 166 171 qed. 167 172 168 (* this is in the stdlib, but commented out, why? *) 169 theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n. 170 #n (elim n) normalize /2 by S_pred/ qed. 171 172 lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.S (l) < 2^16).∀n:ℕ. 173 lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction. 174 S (l) < 2^16 ∧ is_well_labelled_p l).∀n:ℕ. 173 175 policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n))) 174 176 (\snd (pi1 … (jump_expansion_internal program (S n)))) → … … 228 230 229 231 (* uses the second part of policy_increase *) 230 lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.S (l) <2^16. 232 lemma measure_incr_or_equal: ∀program:(Σl:list labelled_instruction. 233 S (l) <2^16 ∧ is_well_labelled_p l). 231 234 ∀policy:Σp:ppc_pc_map. 232 out_of_program_none program p ∧235 (*out_of_program_none program p ∧*) 233 236 not_jump_default program p ∧ 234 237 \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧ 235 238 \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉) ∧ 239 sigma_compact_unsafe program (create_label_map program) p ∧ 236 240 \fst p < 2^16. 237 241 ∀l.l ≤ program → ∀acc:ℕ. … … 247 251 [ / by I/ 248 252  #x normalize nodelta #Hx #Hjeq 249 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))))) (t) (le_S_to_le … Hp))253 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (t) (le_S_to_le … Hp)) 250 254 whd in match (measure_int ???); whd in match (measure_int ? x ?); 251 255 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd (pi1 ?? policy)) 〈0,short_jump〉) … … 266 270 qed. 267 271 268 (* these lemmas seem superfluous, but not sure how *)269 lemma bla: ∀a,b:ℕ.a + a = b + b → a = b.270 #a elim a271 [ normalize #b //272  a #a #Hind #b cases b [ /2 by le_n_O_to_eq/  b #b normalize273 <plus_n_Sm <plus_n_Sm #H274 >(Hind b (injective_S ?? (injective_S ?? H))) // ]275 ]276 qed.277 278 lemma sth_not_s: ∀x.x ≠ S x.279 #x cases x280 [ //  #y // ]281 qed.282 283 272 lemma measure_full: ∀program.∀policy. 284 273 measure_int program policy 0 = 2*program → ∀i.i<program → … … 314 303 315 304 (* uses second part of policy_increase *) 316 lemma measure_special: ∀program:(Σl:list labelled_instruction.(S (l)) < 2^16). 305 lemma measure_special: ∀program:(Σl:list labelled_instruction. 306 (S (l)) < 2^16 ∧ is_well_labelled_p l). 317 307 ∀policy:Σp:ppc_pc_map. 318 out_of_program_none program p ∧not_jump_default program p ∧308 not_jump_default program p ∧ 319 309 \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧ 320 310 \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉) ∧ 311 sigma_compact_unsafe program (create_label_map program) p ∧ 321 312 \fst p < 2^16. 322 313 match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with … … 336 327 [ @(transitive_le … Hp) / by / 337 328  whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; 338 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (t) (le_S_to_le … Hp))329 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (t) (le_S_to_le … Hp)) 339 330 #Hinc cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉) in Hm Hinc; 340 331 #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉); … … 359 350 ] 360 351  >Hi whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; 361 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (t) (le_S_to_le … Hp))352 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (t) (le_S_to_le … Hp)) 362 353 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉) in Hm; 363 354 #x1 #x2 … … 379 370 qed. 380 371 381 lemma le_to_eq_plus: ∀n,z. 382 n ≤ z → ∃k.z = n + k. 383 #n #z elim z 384 [ #H cases (le_to_or_lt_eq … H) 385 [ #H2 @⊥ @(absurd … H2) @not_le_Sn_O 386  #H2 @(ex_intro … 0) >H2 // 387 ] 388  #z' #Hind #H cases (le_to_or_lt_eq … H) 389 [ #H' elim (Hind (le_S_S_to_le … H')) #k' #H2 @(ex_intro … (S k')) 390 >H2 >plus_n_Sm // 391  #H' @(ex_intro … 0) >H' // 392 ] 393 ] 394 qed. 395 396 lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.S (l) < 2^16. 372 lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction. 373 S (l) < 2^16 ∧ is_well_labelled_p l. 397 374 match jump_expansion_start program (create_label_map program) with 398 375 [ None ⇒ True … … 406 383 [ / by refl/ 407 384  #h #t #Hind #Hp whd in match (measure_int ???); 408 elim (proj2 ?? (proj1 ?? (proj1 ?? Hpl)) (t) (le_S_to_le … Hp))385 elim (proj2 ?? (proj1 ?? Hpl) (t) (le_S_to_le … Hp)) 409 386 #pc #Hpc >(lookup_opt_lookup_hit … Hpc 〈0,short_jump〉) normalize nodelta @Hind 410 387 @(transitive_le … Hp) @le_n_Sn … … 414 391 415 392 (* the actual computation of the fixpoint *) 416 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.S (l) < 2^16). 393 definition je_fixpoint: ∀program:(Σl:list labelled_instruction. 394 S (l) < 2^16 ∧ is_well_labelled_p l). 417 395 Σp:option ppc_pc_map. 418 396 match p with … … 513 491 normalize nodelta #Hpe 514 492 lapply (measure_incr_or_equal program Xp program (le_n (program)) 0) 515 [ @(proj1 ?? HXp)493 [ cases daemon (* reorder *) 516 494  lapply (Hfa x Hx) >Xeq >Seq 517 495 lapply (measure_special program «Xp,?») 518 [ @(proj1 ?? HXp)496 [ cases daemon (* reorder *) 519 497  lapply Seq whd in match (jump_expansion_internal program (S x)); (*340s*) 520 498 >Xeq normalize nodelta cases Xno_ch in HXp Xeq; #HXp #Xeq … … 556 534  sto #stp normalize nodelta #Hstp @conj [ @conj 557 535 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))))) 558  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))) 559 @(proj2 ?? (proj1 ?? Hstp)) #i #Hi 560 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 561 [ #Hj 562 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))) i (le_S_to_le … Hi)) 563 lapply (Hfull i Hi Hj) 564 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉) 565 #fp #fj #Hfj >Hfj normalize nodelta 566 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉) 567 #stp #stj cases stj normalize nodelta 568 [1,2: #H cases H #H2 cases H2 destruct (H2) 569 3: #_ @refl 536  @(equal_compact_unsafe_compact ?? Fp) 537 [ @(proj2 ?? (proj1 ?? (proj1 ?? Hstp))) @(proj2 ?? (proj1 ?? Hstp)) 538 #i #Hi 539 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 540 [ #Hj 541 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))) i (le_S_to_le … Hi)) 542 lapply (Hfull i Hi Hj) 543 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉) 544 #fp #fj #Hfj >Hfj normalize nodelta 545 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉) 546 #stp #stj cases stj normalize nodelta 547 [1,2: #H cases H #H2 cases H2 destruct (H2) 548 3: #_ @refl 549 ] 550  #Hj >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))) i Hi Hj) 551 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl 570 552 ] 571  #Hj >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))) i Hi Hj)572 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl553  cases daemon 554  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))) 573 555 ] 574 556 ] … … 597 579 include alias "arithmetics/nat.ma". 598 580 include alias "basics/logic.ma". 599 600 lemma nth_safe_nth:601 ∀A:Type[0].∀l:list A.∀i.∀proof:i < l.∀x.nth_safe A i l proof = nth i A l x.602 #A #l elim l603 [ #i #prf @⊥ @(absurd ? prf) @le_to_not_lt @le_O_n604  l #h #t #Hind #i elim i605 [ #prf #x normalize @refl606  i #i #Hind2 #prf #x whd in match (nth ????); whd in match (tail ??);607 whd in match (nth_safe ????); @Hind608 ]609 ]610 qed.611 581 612 582 (* The glue between Policy and Assembly. *) … … 686 656 ] 687 657 qed. 688 689 690 691 692 >(add_bitvector_of_nat_plus ?? ppc)693 694 qed. 
src/ASM/PolicyFront.ma
r2102 r2141 253 253 ∀dest.is_jump_to instr dest → 254 254 let paddr ≝ lookup_def … labels dest 0 in 255 let addr ≝ bitvector_of_nat ? (if leb i paddr (* forward jump*)256 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) + added257 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in255 let addr ≝ bitvector_of_nat ? (if leb paddr (prefix) (* jump to address already known *) 256 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉) 257 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in 258 258 match j with 259 259 [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧ … … 265 265 \fst (absolute_jump_cond pc_plus_jmp_length addr) = false 266 266 ]. 267 268 267 269 268 (* Definitions and theorems for the jump_length type (itself defined in Assembly) *) … … 324 323 let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in 325 324 let paddr ≝ lookup_def … labels lbl 0 in 326 let addr ≝ bitvector_of_nat ? (if leb p pc paddr (* forward jump*)327 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added328 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in325 let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *) 326 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) 327 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in 329 328 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in 330 329 if sj_possible … … 339 338 let paddr ≝ lookup_def ? ? labels lbl 0 in 340 339 let addr ≝ bitvector_of_nat ? 341 (if leb ppc paddr (* forward jump *) 342 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) 343 + added 344 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)) in 340 (if leb paddr ppc (* jump to address already known *) 341 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) 342 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in 345 343 let 〈aj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length addr in 346 344 if aj_possible … … 354 352 let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in 355 353 let paddr ≝ lookup_def … labels lbl 0 in 356 let addr ≝ bitvector_of_nat ? (if leb p pc paddr (* forward jump*)357 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added358 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in354 let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *) 355 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) 356 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in 359 357 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in 360 358 if sj_possible … … 395 393 qed. 396 394 397 lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.398 #a #b / by refl/399 qed.400 401 lemma nth_last: ∀A,a,l.402 nth (l) A l a = a.403 #A #a #l elim l404 [ / by /405  #h #t #Hind whd in match (nth ????); whd in match (tail ??); @Hind406 ]407 qed.408 409 395 (* The first step of the jump expansion: everything to short. *) 410 396 definition jump_expansion_start: 411 ∀program:(Σl:list labelled_instruction.S (l) < 2^16 ).397 ∀program:(Σl:list labelled_instruction.S (l) < 2^16 ∧ is_well_labelled_p l). 412 398 ∀labels:label_map. 413 399 Σpolicy:option ppc_pc_map. 414 400 match policy with 415 401 [ None ⇒ True 416  Some p ⇒ And (And (And (And (And (And (And402  Some p ⇒ And (And (And (And (And (And 417 403 (out_of_program_none (pi1 ?? program) p) 418 404 (not_jump_default (pi1 ?? program) p)) 419 (sigma_compact_unsafe program labels p))420 405 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) 421 406 (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉))) 407 (sigma_compact_unsafe program labels p)) 422 408 (∀i.i ≤ program → ∃pc. 423 409 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉)) 424 (bvt_lookup_opt … (bitvector_of_nat ? (program)) (\snd p) = Some ? 〈\fst p,short_jump〉)) 425 (\fst p < 2^16) 410 (\fst p < 2^16) 426 411 ] ≝ 427 412 λprogram.λlabels. 428 413 let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction) 429 (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And (And414 (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And 430 415 (out_of_program_none prefix policy) 431 416 (not_jump_default prefix policy)) 432 (sigma_compact_unsafe prefix labels policy))433 417 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 434 418 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉))) 419 (sigma_compact_unsafe prefix labels policy)) 435 420 (∀i.i ≤ prefix → ∃pc. 436 421 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉)) 437 (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd policy) =438 Some ? 〈\fst policy,short_jump〉))439 422 program 440 423 (λprefix.λx.λtl.λprf.λp. … … 451 434  lapply p p generalize in match (foldl_strong ?????); * #p #Hp #hg 452 435 @conj [ @Hp  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ] 453  @conj [ @conj [ @conj [ @conj [ @conj [ @conj436  @conj [ @conj [ @conj [ @conj [ @conj 454 437 [ (* out_of_program_none *) 455 438 #i #Hi2 >append_length <commutative_plus @conj … … 457 440 cases p p #p cases p p #pc #p #Hp cases x x #l #pi 458 441 [ >lookup_opt_insert_miss 459 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2)) 442 [ (* USE[pass]: out_of_program_none → *) 443 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2)) 460 444 @le_S_to_le @le_S_to_le @Hi 461 445  @bitvector_of_nat_abs … … 467 451  >lookup_opt_insert_miss 468 452 [ <Hi 469 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) (S (S (prefix))) ?)) 453 (* USE[pass]: out_of_program_none → *) 454 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (prefix))) ?)) 470 455 [ >Hi @Hi2 471 456  @le_S @le_n … … 483 468  #Hi >lookup_opt_insert_miss 484 469 [ #Hl 485 elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2) Hl)) 470 (* USE[pass]: out_of_program_none ← *) 471 elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2) Hl)) 486 472 [ #Hi3 @Hi3 487 473  #Hi3 @⊥ @(absurd ? Hi3) @sym_neq @Hi … … 489 475  @bitvector_of_nat_abs 490 476 [ @Hi2 491  @(transitive_lt … (p i2 ?? program)) >prf @le_S_S >append_length477  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length 492 478 <plus_n_Sm @le_S_S @le_plus_n_r 493 479  @Hi … … 500 486 normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 501 487 [ >lookup_insert_miss 502 [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))))) i Hi) 488 [ (* USE[pass]: not_jump_default *) 489 lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi) 503 490 >nth_append_first 504 491 [ #H #H2 @H @H2 … … 506 493 ] 507 494  @bitvector_of_nat_abs 508 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length <commutative_plus >plus_n_Sm 509 @le_plus_a @le_S @Hi 510  @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm @le_S_S 511 @le_plus_n_r 495 [ @(transitive_lt ??? Hi) @le_S_to_le] 496 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length 497 <plus_n_Sm @le_S_S @le_plus_n_r 512 498  @lt_to_not_eq @le_S @Hi 513 499 ] 514 500 ] 515 501  >Hi >lookup_insert_miss 516 [ #_ elim (proj2 ?? (proj1 ?? Hp) (prefix) (le_n (prefix))) #pc #Hl 502 [ #_ (* USE: everything is short *) 503 elim ((proj2 ?? Hp) (prefix) (le_n (prefix))) #pc #Hl 517 504 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) @refl 518 505  @bitvector_of_nat_abs 519 [ @(transitive_lt … (p i2 ?? program)) >prf @le_S_S >append_length @le_plus_n_r520  @(transitive_lt … (p i2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm @le_S_S506 [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length @le_plus_n_r 507  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm @le_S_S 521 508 @le_plus_n_r 522 509  @lt_to_not_eq @le_n … … 524 511 ] 525 512 ] 513 ] 514  (* 0 ↦ 0 *) 515 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 516 >lookup_insert_miss 517 [ (* USE[pass]: 0 ↦ 0 *) 518 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) 519  @bitvector_of_nat_abs 520 [ / by / 521  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S <plus_n_Sm 522 @le_S_S @le_plus_n_r 523  @lt_to_not_eq / by / 524 ] 525 ] 526 ] 527  (* fst p = pc *) 528 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 529 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 526 530 ] 527 531  (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi; … … 530 534 [ >lookup_opt_insert_miss 531 535 [ >lookup_opt_insert_miss 532 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi) 536 [ (* USE[pass]: policy_compact_unsafe *) 537 lapply (proj2 ?? (proj1 ?? Hp) i Hi) 533 538 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma)) 534 539 cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %); … … 548 553 [2: lapply (le_S_to_le … Hi) Hi #Hi] 549 554 @bitvector_of_nat_abs 550 [1,4: @(transitive_lt … (p i2 ?? program)) >prf @le_S_S >append_length <commutative_plus555 [1,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <commutative_plus 551 556 @le_plus_a @Hi 552 2,5: @(transitive_lt … (p i2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm557 2,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm 553 558 @le_S_S @le_plus_n_r 554 559 3,6: @lt_to_not_eq @le_S_S @Hi … … 556 561  >lookup_opt_insert_miss 557 562 [ >Hi >lookup_opt_insert_hit normalize nodelta 558 >(proj2 ?? Hp) normalize nodelta >nth_append_second 559 [ <minus_n_n whd in match (nth ????); @refl 563 (* USE: everything is short, fst p = pc *) 564 elim ((proj2 ?? Hp) (prefix) (le_n ?)) #pc #Hl 565 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hp))) >Hl 566 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #EQ normalize nodelta >nth_append_second 567 [ <minus_n_n whd in match (nth ????); >EQ @refl 560 568  @le_n 561 569 ] 562 570  @bitvector_of_nat_abs 563 [ @(transitive_lt … (p i2 ?? program)) >Hi >prf @le_S_S >append_length <commutative_plus571 [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >Hi >prf @le_S_S >append_length <commutative_plus 564 572 @le_plus_a @le_n 565  @(transitive_lt … (p i2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm573  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm 566 574 @le_S_S @le_plus_n_r 567 575  @lt_to_not_eq @le_S_S >Hi @le_n … … 570 578 ] 571 579 ] 572  (* 0 ↦ 0 *) 573 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 574 >lookup_insert_miss 575 [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) 576  @bitvector_of_nat_abs 577 [ / by / 578  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm 579 @le_S_S @le_plus_n_r 580  @lt_to_not_eq / by / 581 ] 582 ] 583 ] 584  (* fst p = pc *) 585 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 586 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 587 ] 588  (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi; 580  (* everything is short *) #i >append_length <commutative_plus #Hi normalize in Hi; 589 581 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 590 582 cases (le_to_or_lt_eq … Hi) Hi #Hi 591 583 [ >lookup_opt_insert_miss 592 [ @(proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi)) 584 [ (* USE[pass]: everything is short *) 585 @((proj2 ?? Hp) i (le_S_S_to_le … Hi)) 593 586  @bitvector_of_nat_abs 594 [ @(transitive_lt … (p i2 ?? program)) >prf >append_length @le_S_S >commutative_plus595 @le_plus_a @le_S_S_to_le @Hi596  @(transitive_lt … (p i2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S597 @le_S_S @le_ plus_n_r587 [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 588 >commutative_plus @le_plus_a @le_S_S_to_le @Hi 589  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length <plus_n_Sm 590 @le_S_S @le_S_S @le_plus_n_r 598 591  @lt_to_not_eq @Hi 599 592 ] … … 603 596 ] 604 597 ] 605  (* lookup at the end *) cases p p #p cases p p #pc #sigma #Hp cases x 606 #lbl #instr >append_length <plus_n_Sm <plus_n_O >lookup_opt_insert_hit 607 / by refl/ 608 ] 609  @conj [ @conj [ @conj [ @conj [ @conj [ @conj 598  @conj [ @conj [ @conj [ @conj [ @conj 610 599 [ #i cases i 611 600 [ #Hi2 @conj … … 629 618  i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O 630 619 ] 631 ] 620 ] ] ] 621 >lookup_insert_hit @refl 632 622  #i cases i 633 623 [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n 634 624  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 635 625 ] 636 ]637  >lookup_insert_hit @refl638 ]639  >lookup_insert_hit @refl640 626 ] 641 627  #i cases i … … 643 629  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 644 630 ] 645 ]646  >lookup_opt_insert_hit @refl647 631 ] 648 632 ] … … 676 660 include alias "basics/logic.ma". 677 661 678 lemma blerpque: ∀a,b,i.662 lemma jump_length_equal_max: ∀a,b,i. 679 663 is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i → 680 664 (max_length a b) = a. … … 699 683 qed. 700 684 701 lemma etblorp: ∀a,b,i.is_jump i →685 lemma jump_length_le_max: ∀a,b,i.is_jump i → 702 686 instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i. 703 687 #a #b #i cases i … … 706 690 1: #pi cases pi 707 691 [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: 708 [1,2,3,6,7,24,25: #x #y 709 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 710 #H cases H 692 try (#x #y #H) try (#x #H) try (#H) cases H 711 693 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 712 694 #_ cases a cases b 713 [2,3: cases x #ad cases ad 714 [15,34: #b #Hb / by le_n/ 715 1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb 716 1,4,5,6,7,8,9: / by le_n/ 717 11,12: cases x #ad cases ad 718 [15,34: #b #Hb / by le_n/ 719 1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb 695 [1,4,5,6,7,8,9: / by le_n/ 720 696 10,13,14,15,16,17,18: / by le_n/ 721 20,21: cases x #ad cases ad722 [15,34: #b #Hb / by le_n/723 1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb724 697 19,22,23,24,25,26,27: / by le_n/ 725 29,30: cases x #ad cases ad #a1 #a2726 [1,3: cases a2 #ad2 cases ad2727 [1,8,20,27: #b #Hb / by le_n/728 2,3,4,9,15,16,17,18,19,21,22,23,28,34,35,36,37,38: #b] #Hb cases Hb729 2,4: cases a1 #ad1 cases ad1730 [2,4,21,23: #b #Hb / by le_n/731 1,3,8,9,15,16,17,18,19,20,22,27,28,34,35,36,37,38: #b] #Hb cases Hb732 ]733 698 28,31,32,33,34,35,36: / by le_n/ 734 38,39: cases x #ad cases ad735 [1,4,20,23: #b #Hb / by le_n/736 2,3,8,9,15,16,17,18,19,21,22,27,28,34,35,36,37,38: #b] #Hb cases Hb737 699 37,40,41,42,43,44,45: / by le_n/ 738 700 46,47,48,49,50,51,52,53,54: / by le_n/ … … 741 703 73,74,75,76,77,78,79,80,81: / by le_n/ 742 704 ] 705 try (@(subaddressing_mode_elim … x) #w normalize @le_S @le_S @le_S @le_S @le_S @le_n) 706 cases x * #ad 707 try (@(subaddressing_mode_elim … ad) #w #z normalize @le_S @le_S @le_S @le_S @le_S @le_n) 708 #z @(subaddressing_mode_elim … z) #w normalize / by / 743 709 ] 744 710 ] 745 711 qed. 746 712 747 lemma minus_zero_to_le: ∀n,m:ℕ.n  m = 0 → n ≤ m. 748 #n 749 elim n 750 [ #m #_ @le_O_n 751  #n' #Hind #m cases m 752 [ #H n whd in match (minus ??) in H; >H @le_n 753  #m' m #H whd in match (minus ??) in H; @le_S_S @Hind @H 754 ] 755 ] 756 qed. 757 758 lemma plus_zero_zero: ∀n,m:ℕ.n + m = 0 → m = 0. 759 #n #m #Hn @sym_eq @le_n_O_to_eq <Hn >commutative_plus @le_plus_n_r 760 qed. 761 762 lemma not_true_is_false: 763 ∀b:bool.b ≠ true → b = false. 764 #b cases b 765 [ #H @⊥ @(absurd ?? H) @refl 766  #H @refl 767 ] 768 qed. 769 770 lemma occurs_does_not: ∀tag,A,id,list_instr. 771 does_not_occur tag A id list_instr = true → 772 occurs_exactly_once tag A id list_instr = true → 773 False. 774 #tag #A #id #list_instr elim list_instr 775 [ #_ whd in match (occurs_exactly_once ????); #ABS destruct (ABS) 776  #h #t #Hind whd in match (does_not_occur ????); 777 whd in match (occurs_exactly_once ????); 778 cases (instruction_matches_identifier ?? id h) normalize nodelta 779 [ #ABS destruct (ABS) 780  @Hind 781 ] 782 ] 783 qed. 784 785 lemma label_in_program: ∀program:(Σl.S (l) < 2^16).∀labels:(Σlm. 713 lemma label_in_program: ∀program:(Σl.S (l) < 2^16 ∧ is_well_labelled_p l).∀labels:(Σlm. 786 714 ∀l.occurs_exactly_once ?? l program → 787 715 bitvector_of_nat ? (lookup_def ?? lm l 0) = … … 789 717 occurs_exactly_once ?? x program → 790 718 lookup_def ASMTag ℕ labels x O≤program. 791 #program cases program program #program #Hprogram #labels #x cases labels 792 labels #labels #H lapply (H x) H 793 generalize in match (lookup_def … labels x 0); 794 whd in match address_of_word_labels_code_mem; 795 whd in match index_of; normalize nodelta elim program in Hprogram; 796 [ #Hprogram #n cases not_implemented 797  #h #t #Hind #Hprogram #n #Hlm #Hocc lapply (Hlm Hocc) Hlm #Hbv 798 whd in match (occurs_exactly_once ????) in Hocc; 799 whd in match (index_of_internal ????) in Hbv; 800 lapply (refl ? (instruction_matches_identifier … x h)) 801 lapply Hocc; lapply Hbv; Hocc Hbv 802 cases (instruction_matches_identifier … x h) in ⊢ (% → % → ???% → %); 803 normalize nodelta #Hbv #Hocc #EQ 804 [ >(bitvector_of_nat_ok 16 n 0) 805 [ @le_O_n 806  >(eq_eq_bv … Hbv) @I 807  / by / 808  cases daemon 809 ] 810  cases n in Hbv; 811 [ #_ @le_O_n 812  n #n #Hbv @le_S_S @(Hind … Hocc) 813 [ @(transitive_lt … Hprogram) @le_n 814  #_ lapply (bitvector_of_nat_ok 16 (S n) (index_of_internal ? (instruction_matches_identifier ?? x) t 1) ???) 815 [ >Hbv >eq_bv_refl @I 816  @(transitive_lt … Hprogram) cases daemon 817  cases daemon 818  #H >(index_of_label_from_internal … Hocc) 819 <plus_O_n >(index_of_label_from_internal … Hocc) in H; 820 #H >(injective_S … H) <plus_O_n @refl 821 ] 822 ] 823 ] 824 ] 825 ] 826 qed. 719 #program cases program program #program #Hprogram #labels #x cases labels 720 labels #labels #H lapply (H x) H 721 generalize in match (lookup_def … labels x 0); 722 whd in match address_of_word_labels_code_mem; 723 whd in match index_of; normalize nodelta elim program in Hprogram; 724 [ #Hprogram #n cases not_implemented 725  #h #t #Hind #Hprogram #n #Hlm #Hocc lapply (Hlm Hocc) Hlm #Hbv 726 whd in match (occurs_exactly_once ????) in Hocc; 727 whd in match (index_of_internal ????) in Hbv; 728 lapply (refl ? (instruction_matches_identifier … x h)) 729 lapply Hocc; lapply Hbv; Hocc Hbv 730 cases (instruction_matches_identifier … x h) in ⊢ (% → % → ???% → %); 731 normalize nodelta #Hbv #Hocc #EQ 732 [ >(bitvector_of_nat_ok 16 n 0) 733 [ @le_O_n 734  >(eq_eq_bv … Hbv) @I 735  / by / 736  cases daemon 737 ] 738  cases n in Hbv; 739 [ #_ @le_O_n 740  n #n #Hbv @le_S_S @(Hind … Hocc) 741 [ @conj 742 [ @(transitive_lt … (proj1 ?? Hprogram)) @le_n 743  cases daemon (* axiomatize this *) 744 ] 745  #_ lapply (bitvector_of_nat_ok 16 (S n) (index_of_internal ? (instruction_matches_identifier ?? x) t 1) ???) 746 [ >Hbv >eq_bv_refl @I 747  @(transitive_lt … (proj1 ?? Hprogram)) cases daemon 748  cases daemon 749  #H >(index_of_label_from_internal … Hocc) 750 <plus_O_n >(index_of_label_from_internal … Hocc) in H; 751 #H >(injective_S … H) <plus_O_n @refl 752 ] 753 ] 754 ] 755 ] 756 ] 757 qed. 758 759 lemma equal_compact_unsafe_compact: ∀program:(Σl.(S (l)) < 2^16 ∧ is_well_labelled_p l). 760 ∀labels.∀old_sigma.∀sigma. 761 sigma_pc_equal program old_sigma sigma → 762 sigma_safe program labels 0 old_sigma sigma → 763 sigma_compact_unsafe program labels sigma → 764 sigma_compact program labels sigma. 765 #program #labels #old_sigma #sigma #Hequal #Hsafe #Hcp_unsafe #i #Hi 766 lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi) 767 lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd sigma))) 768 cases (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)) in ⊢ (???% → %); 769 [ / by / 770  #x cases x x #x1 #x2 #EQ 771 cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd sigma)) 772 [ / by / 773  #y cases y y #y1 #y2 normalize nodelta #H #H2 774 cut (instruction_size_jmplen x2 775 (\snd (nth i ? program 〈None ?, Comment []〉)) = 776 instruction_size … (bitvector_of_nat ? i) 777 (\snd (nth i ? program 〈None ?, Comment []〉))) 778 [5: #H3 <H3 @H2 779 4: whd in match (instruction_size_jmplen ??); 780 whd in match (instruction_size …); 781 whd in match (assembly_1_pseudoinstruction …); 782 whd in match (expand_pseudo_instruction …); 783 normalize nodelta whd in match (append …) in H; 784 cases (nth i ? program 〈None ?,Comment []〉) in H; 785 #lbl #instr cases instr 786 [2,3,6: #x [3: #y] normalize nodelta #H @refl 787 4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj 788 lapply (Hj x (refl ? x)) Hj normalize nodelta 789 >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O 790 cases x2 normalize nodelta 791 [1,4: whd in match short_jump_cond; normalize nodelta 792 lapply (refl ? (leb (lookup_def ?? labels x 0) ([]@program))) 793 cases (leb (lookup_def ?? labels x 0) ([]@program)) in ⊢ (???% → %); #Hlab 794 normalize nodelta 795 >(Hequal (lookup_def ?? labels x 0) ?) 796 [2,4,6,8: @(label_in_program program labels x) 797 cases daemon (* XXX this has to come from somewhere else *) 798 ] 799 <plus_n_O 800 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 801 #result #flags normalize nodelta 802 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 803 cases (get_index' bool 2 0 flags) normalize nodelta 804 [5,6,7,8: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/ 805 1,2,3,4: cases (eq_bv 9 upper ?) 806 [2,4,6,8: #H lapply (proj1 ?? H) #H3 destruct (H3) 807 1,3,5,7: #_ normalize nodelta @refl 808 ] 809 ] 810 2,5: whd in match short_jump_cond; whd in match absolute_jump_cond; 811 lapply (refl ? (leb (lookup_def ?? labels x 0) ([]@program))) 812 cases (leb (lookup_def ?? labels x 0) ([]@program)) in ⊢ (???% → %); #Hlab 813 normalize nodelta 814 (* USE: added = 0 → policy_pc_equal (from fold) *) 815 >(Hequal (lookup_def ?? labels x 0) ?) 816 [2,4,6,8: @(label_in_program program labels x) 817 cases daemon (* XXX this has to come from somewhere else *)] 818 <plus_n_O 819 normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2 820 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 821 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 822 #result #flags normalize nodelta 823 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 824 cases (get_index' bool 2 0 flags) normalize nodelta 825 #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl 826 3,6: whd in match short_jump_cond; whd in match absolute_jump_cond; 827 lapply (refl ? (leb (lookup_def ?? labels x 0) ([]@program))) 828 cases (leb (lookup_def ?? labels x 0) ([]@program)) in ⊢ (???% → %); #Hlab 829 normalize nodelta 830 (* USE: added = 0 → policy_pc_equal (from fold) *) 831 >(Hequal (lookup_def ?? labels x 0) ?) 832 [2,4,6,8: @(label_in_program program labels x) 833 cases daemon (* XXX this has to come from somewhere else *)] 834 <plus_n_O normalize nodelta 835 cases (vsplit bool 5 11 ?) #addr1 #addr2 836 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 837 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 838 #result #flags normalize nodelta 839 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 840 cases (get_index' bool 2 0 flags) normalize nodelta 841 #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl 842 ] 843 1: #pi cases pi 844 [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: 845 [1,2,3,6,7,24,25: #x #y 846 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 847 normalize nodelta #H @refl 848 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x 3,4,5,8,9: #y #x] 849 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 850 #Hj lapply (Hj x (refl ? x)) Hj 851 whd in match expand_relative_jump; normalize nodelta 852 whd in match expand_relative_jump_internal; normalize nodelta 853 whd in match expand_relative_jump_unsafe; normalize nodelta 854 whd in match expand_relative_jump_internal_unsafe; 855 normalize nodelta >(add_bitvector_of_nat_plus ? i 1) 856 <(plus_n_Sm i 0) <plus_n_O 857 cases daemon (* XXX this needs subadressing mode magic, see above *) 858 ] 859 ] 860 ] 861 ] 862 ] 863 qed. 
src/ASM/PolicyStep.ma
r2102 r2141 5 5 6 6 (* One step in the search for a jump expansion fixpoint. *) 7 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.S (l) < 2^16). 7 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction. 8 S (l) < 2^16 ∧ is_well_labelled_p l). 8 9 ∀labels:(Σlm:label_map.∀l. 9 10 occurs_exactly_once ?? l program → … … 11 12 address_of_word_labels_code_mem program l). 12 13 ∀old_policy:(Σpolicy:ppc_pc_map. 13 And (And (And (And (out_of_program_none program policy)14 (not_jump_default program policy))14 (* out_of_program_none program policy *) 15 And (And (And (And (not_jump_default program policy) 15 16 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 16 17 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd policy) 〈0,short_jump〉))) 18 (sigma_compact_unsafe program labels policy)) 17 19 (\fst policy < 2^16)). 18 20 (Σx:bool × (option ppc_pc_map). … … 22 24  Some p ⇒ And (And (And (And (And (And (And (And (out_of_program_none program p) 23 25 (not_jump_default program p)) 24 (jump_increase program old_policy p))25 (no_ch = true → sigma_compact program labels p))26 26 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) 27 27 (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉))) 28 (jump_increase program old_policy p)) 29 (sigma_compact_unsafe program labels p)) 28 30 (no_ch = true → sigma_pc_equal program old_policy p)) 29 31 (sigma_jump_equal program old_policy p → no_ch = true)) … … 36 38 (λprefix.Σx:ℕ × ppc_pc_map. 37 39 let 〈added,policy〉 ≝ x in 38 And (And (And (And (And (And (And (And ( out_of_program_none prefix policy)40 And (And (And (And (And (And (And (And (And (out_of_program_none prefix policy) 39 41 (not_jump_default prefix policy)) 42 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 43 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉))) 40 44 (jump_increase prefix old_sigma policy)) 41 45 (sigma_compact_unsafe prefix labels policy)) 46 (sigma_jump_equal prefix old_sigma policy → added = 0)) 47 (added = 0 → sigma_pc_equal prefix old_sigma policy)) 48 (\fst (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd policy) 〈0,short_jump〉) = 49 \fst (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma) 〈0,short_jump〉) + added)) 42 50 (sigma_safe prefix labels added old_sigma policy)) 43 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))44 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉)))45 (added = 0 → sigma_pc_equal prefix old_sigma policy))46 (sigma_jump_equal prefix old_sigma policy → added = 0))47 51 program 48 52 (λprefix.λx.λtl.λprf.λacc. … … 96 100 #x #H #Heq >Heq in H; normalize nodelta Heq x #Hind 97 101 (* USE: inc_pc = fst of policy (from fold) *) 98 >(proj2 ?? (proj1 ?? (proj1 ?? Hind))) in p1;102 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))))) in p1; 99 103 (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *) 100 lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (p i2 ?? old_sigma)))104 lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) 101 105 #Hsig #Hge 102 106 (* USE: added = 0 → policy_pc_equal (from fold) *) 103 lapply ((proj2 ?? (proj1 ?? Hind)) ? (program) (le_n (program))) 104 [ @(proj2 ?? Hind) #i #Hi 107 lapply ((proj2 ?? (proj1 ?? (proj1 ?? Hind))) ? (program) (le_n (program))) 108 [ (* USE: policy_jump_equal → added = 0 (from fold) *) 109 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) #i #Hi 105 110 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 106 111 [ #Hj 107 112 (* USE: policy_increase (from fold) *) 108 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))113 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) i (le_S_to_le … Hi)) 109 114 lapply (Habs i Hi Hj) 110 115 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉) … … 117 122  #Hnj 118 123 (* USE: not_jump_default (from fold and old_sigma) *) 119 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))))) i Hi Hnj)120 >(proj 2?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj)124 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi Hnj) 125 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj) 121 126 @refl 122 127 ] … … 126 131  normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2 127 132 >H2 in H; normalize nodelta H2 x #H @conj 128 [ @conj [ @conj [ @conj [ @conj [ @conj 129 [ (* USE[pass]: out_of_program_none, not_jump_default, policy_increase (from fold) *) 130 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))) 131  (* policy_compact_unsafe → policy_compact (in the end) *) 132 #Hch #i #Hi 133 (* USE: policy_compact_unsafe (from fold) *) 134 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) i Hi) 135 (* USE: policy_safe (from fold) *) 136 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) i Hi) 137 lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd final_policy))) 138 cases (lookup_opt … (bitvector_of_nat ? i) (\snd final_policy)) in ⊢ (???% → %); 139 [ / by / 140  #x cases x x #x1 #x2 #EQ 141 cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd final_policy)) 142 [ / by / 143  #y cases y y #y1 #y2 normalize nodelta #H #H2 144 cut (instruction_size_jmplen x2 145 (\snd (nth i ? (pi1 ?? program) 〈None ?, Comment []〉)) = 146 instruction_size … (bitvector_of_nat ? i) 147 (\snd (nth i ? (pi1 ?? program) 〈None ?, Comment []〉))) 148 [5: #H3 <H3 @H2 149 4: whd in match (instruction_size_jmplen ??); 150 whd in match (instruction_size …); 151 whd in match (assembly_1_pseudoinstruction …); 152 whd in match (expand_pseudo_instruction …); 153 normalize nodelta whd in match (append …) in H; 154 cases (nth i ? (pi1 ?? program) 〈None ?,Comment []〉) in H; 155 #lbl #instr cases instr 156 [2,3,6: #x [3: #y] normalize nodelta #H @refl 157 4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj 158 lapply (Hj x (refl ? x)) Hj normalize nodelta 159 >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O 160 cases x2 normalize nodelta 161 [1,4: whd in match short_jump_cond; normalize nodelta 162 lapply (refl ? (leb i (lookup_def ?? labels x 0))) 163 cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab 164 normalize nodelta 165 (* USE: added = 0 → policy_pc_equal *) 166 >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?) 167 [2,4,6,8: @(label_in_program program labels x) 168 cases daemon (* XXX this has to come from somewhere else *) 169 ] 170 [1,5: >(eqb_true_to_eq … Hch) <plus_n_O] 171 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 172 #result #flags normalize nodelta 173 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 174 cases (get_index' bool 2 0 flags) normalize nodelta 175 [1,3,5,7: cases (eq_bv 9 upper ?) 176 2,4,6,8: cases (eq_bv 9 upper (zero 9))] 177 [2,4,6,8,10,12,14,16: #H lapply (proj1 ?? H) #H3 destruct (H3) 178 5,7,13,15: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/ 179 1,3,9,11: #_ normalize nodelta @refl 180 ] 181 2,5: whd in match short_jump_cond; whd in match absolute_jump_cond; 182 lapply (refl ? (leb i (lookup_def ?? labels x 0))) 183 cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab 184 normalize nodelta 185 (* USE: added = 0 → policy_pc_equal *) 186 >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?) 187 [2,4,6,8: @(label_in_program program labels x) 188 cases daemon (* XXX this has to come from somewhere else *)] 189 [1,3: >(eqb_true_to_eq … Hch) <plus_n_O] 190 normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2 191 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 192 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 193 #result #flags normalize nodelta 194 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 195 cases (get_index' bool 2 0 flags) normalize nodelta 196 #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl 197 3,6: whd in match short_jump_cond; whd in match absolute_jump_cond; 198 lapply (refl ? (leb i (lookup_def ?? labels x 0))) 199 cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab 200 normalize nodelta 201 >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?) 202 [2,4,6,8: @(label_in_program program labels x) 203 cases daemon (* XXX this has to come from somewhere else *)] 204 [1,3: >(eqb_true_to_eq … Hch) <plus_n_O] 205 normalize nodelta 206 cases (vsplit bool 5 11 ?) #addr1 #addr2 207 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 208 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 209 #result #flags normalize nodelta 210 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 211 cases (get_index' bool 2 0 flags) normalize nodelta 212 #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl 213 ] 214 1: #pi cases pi 215 [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: 216 [1,2,3,6,7,24,25: #x #y 217 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 218 normalize nodelta #H @refl 219 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x 3,4,5,8,9: #y #x] 220 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 221 #Hj lapply (Hj x (refl ? x)) Hj 222 whd in match expand_relative_jump; normalize nodelta 223 whd in match expand_relative_jump_internal; normalize nodelta 224 whd in match expand_relative_jump_unsafe; normalize nodelta 225 whd in match expand_relative_jump_internal_unsafe; 226 normalize nodelta >(add_bitvector_of_nat_plus ? i 1) 227 <(plus_n_Sm i 0) <plus_n_O 228 cases daemon (* XXX this needs subadressing mode magic, see above *) 229 ] 230 ] 231 ] 232 ] 233 ] 234 ] 235  (* USE: 0 ↦ 0 (from fold) *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 236 ] 237  (* USE: inc_pc = fst of policy (from fold) *) @(proj2 ?? (proj1 ?? (proj1 ?? H))) 238 ] 239  #H2 (* USE: added = 0 → policy_pc_equal (from fold) *) 240 @(proj2 ?? (proj1 ?? H)) @eqb_true_to_eq @H2 241 ] 242  #H2 (* USE: policy_jump_equal → added = 0 (from fold *) 243 @eq_to_eqb_true @(proj2 ?? H) @H2 244 ] 245  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1 246 ] 247 4: lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma 133 [ @conj [ @conj 134 [ (* USE[pass]: out_of_program_none, not_jump_default, 0 ↦ 0, inc_pc = fst policy, 135 * jump_increase, sigma_compact_unsafe (from fold) *) 136 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 137  (* USE[pass]: added = 0 → sigma_pc_equal (from fold) *) 138 #H2 @(proj2 ?? (proj1 ?? (proj1 ?? H))) @eqb_true_to_eq @H2 139 ] 140  #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *) 141 @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @H2 142 ] 143  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1 144 ] 145 4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %); 146 #inc_pc #inc_sigma #Hips 248 147 lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)) 249 148 cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in ⊢ (???% → %); 250 #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta 251 @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2 252 @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 253 [ (* out_of_program_none *) #i #Hi2 >append_length <commutative_plus @conj 149 #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim 150 #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta 151 #Heq1 #Heq2 152 @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 153 (* NOTE: to save memory and speed up work, there's cases daemon here. They can be 154 * commented out for full proofs, but this needs a lot of memory and time *) 155 [ (* out_of_program_none *) (* cases daemon *) 156 #i #Hi2 >append_length <commutative_plus @conj 254 157 [ (* → *) #Hi normalize in Hi; 255 158 cases instr in Heq2; normalize nodelta 256 159 #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss 257 160 [1,3,5,7,9,11: >lookup_opt_insert_miss 258 [1,3,5,7,9,11: (* USE : out_of_program_none → *)259 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi2))161 [1,3,5,7,9,11: (* USE[pass]: out_of_program_none → *) 162 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2)) 260 163 @le_S_to_le @Hi 261 164 2,4,6,8,10,12: @bitvector_of_nat_abs … … 275 178 [ #Hi 276 179 lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl)))) 277 #Hl2 (* USE : out_of_program_none ← *)278 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi2) Hl2)180 #Hl2 (* USE[pass]: out_of_program_none ← *) 181 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2) Hl2) 279 182 #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3 280 183  #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi)) … … 287 190 ] 288 191 ] 289 ] 290  (* not_jump_default *) #i >append_length <commutative_plus #Hi normalize in Hi; 192 ] 193  (* not_jump_default *) (* cases daemon *) 194 #i >append_length <commutative_plus #Hi normalize in Hi; 291 195 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 292 196 [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 293 197 [ >lookup_insert_miss 294 198 [ >(nth_append_first ? i prefix ?? Hi) 295 (* USE : not_jump_default *)296 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi)199 (* USE[pass]: not_jump_default *) 200 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi) 297 201  @bitvector_of_nat_abs 298 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm 299 >commutative_plus @le_plus_a @Hi 300  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S 202 [ @(transitive_lt ??? Hi) ] 203 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 301 204 @le_plus_n_r 302 205  @lt_to_not_eq @Hi … … 304 207 ] 305 208  @bitvector_of_nat_abs 306 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm 307 >commutative_plus @le_plus_a @Hi 308  @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm 309 @le_S_S @le_plus_n_r 209 [ @(transitive_lt ??? Hi) @le_S_to_le ] 210 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length 211 <plus_n_Sm @le_S_S @le_plus_n_r 310 212  @lt_to_not_eq @le_S @Hi 311 213 ] … … 328 230 ] 329 231  @bitvector_of_nat_abs 330 [ @ (transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length @le_plus_n_r331  @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm332 @le_S_S @le_plus_n_r232 [ @le_S_to_le ] 233 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S 234 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 333 235  @lt_to_not_eq @le_n 334 ] 335 ] 336 ] 337 ] 338  (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi; 236 ] 237 ] 238 ] 239 ] 240  (* 0 ↦ 0 *) (* cases daemon *) 241 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 242 [ cases (decidable_eq_nat 0 (prefix)) 243 [ #Heq <Heq >lookup_insert_hit 244 (* USE: inc_pc = fst policy *) 245 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 246 (* USE[pass]: 0 ↦ 0 *) 247 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 248 <Heq #ONE #TWO >TWO >ONE @refl 249  #Hneq >lookup_insert_miss 250 [ (* USE[pass]: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 251  @bitvector_of_nat_abs 252 [3: @Hneq] 253 ] 254 ] 255  @bitvector_of_nat_abs 256 [3: @lt_to_not_eq / by / ] 257 ] 258 [1,3: / by / 259 2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 260 [2: <plus_n_Sm @le_S_S] 261 @le_plus_n_r 262 ] 263 ] 264  (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2)) 265 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 266 ] 267  (* jump_increase *) (* cases daemon *) 268 #i >append_length >commutative_plus #Hi normalize in Hi; 339 269 cases (le_to_or_lt_eq … Hi) Hi; #Hi 340 270 [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 341 [ (* USE : policy_increase *)342 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi))271 [ (* USE[pass]: jump_increase *) 272 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le … Hi)) 343 273 <(proj2 ?? (pair_destruct ?????? Heq2)) 344 274 @pair_elim #opc #oj #EQ1 >lookup_insert_miss … … 346 276 [ @pair_elim #pc #j #EQ2 / by / 347 277  @bitvector_of_nat_abs 348 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S349 >commutative_plus @le_plus_a @Hi350  @(transitive_lt … (pi2 ?? program)) >prf >append_length@le_S_S @le_plus_n_r278 [ @(transitive_lt ??? Hi) ] 279 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 280 @le_S_S @le_plus_n_r 351 281  @lt_to_not_eq @Hi 352 282 ] 353 283 ] 354 284  @bitvector_of_nat_abs 355 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S >commutative_plus356 @le_plus_a @Hi357  @(transitive_lt … (pi2 ?? program)) >prf>append_length @le_S_S <plus_n_Sm @le_plus_n_r285 [ @(transitive_lt ??? Hi) @le_S_to_le ] 286 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 287 >append_length @le_S_S <plus_n_Sm @le_plus_n_r 358 288  @lt_to_not_eq @le_S @Hi 359 289 ] … … 384 314 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 385 315 (* USE: not_jump_default (from old_sigma) *) 386 lapply (proj 2?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??)316 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??) 387 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: 388 318 >prf >nth_append_second … … 404 334 2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 405 335 (* USE: not_jump_default (from old_sigma) *) 406 lapply (proj 2?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??)336 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??) 407 337 [1,4,7: >prf >nth_append_second 408 338 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj … … 418 348 ] 419 349  @bitvector_of_nat_abs 420 [ @ (transitive_lt … (pi2 … program)) >prf @le_S_S >append_length @le_plus_n_r421  @(transitive_lt … (pi2 … program)) @le_S_S >prf >append_length <plus_n_Sm422 @le_S_S @le_plus_n_r350 [ @le_S_to_le ] 351 [1,2: @(transitive_lt … (proj1 ?? (pi2 … program))) @le_S_S >prf 352 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 423 353  @lt_to_not_eq @le_n 424 354 ] … … 431 361 ] 432 362 ] 433  (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi; 363  (* sigma_compact_unsafe *) (* cases daemon *) 364 #i >append_length <commutative_plus #Hi normalize in Hi; 434 365 <(proj2 ?? (pair_destruct ?????? Heq2)) 435 366 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi … … 439 370 [ cases (le_to_or_lt_eq … Hi) Hi #Hi 440 371 [ >lookup_opt_insert_miss 441 [ (* USE : policy_compact_unsafe *)442 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)372 [ (* USE[pass]: sigma_compact_unsafe *) 373 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?) 443 374 [ @le_S_to_le @Hi ] 444 375 cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) … … 458 389 ] 459 390  >Hi >lookup_opt_insert_hit normalize nodelta 460 (* USE : policy_compact_unsafe *)461 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)391 (* USE[pass]: sigma_compact_unsafe *) 392 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?) 462 393 [ <Hi @le_n 463 394  cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) … … 465 396  #x cases x x #x1 #x2 466 397 (* USE: inc_pc = fst inc_sigma *) 467 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) <Hi468 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))398 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 399 <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)) 469 400 cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %); 470 401 [ normalize nodelta #_ #_ #H cases H … … 482 413 ] 483 414 [3,4,5: @bitvector_of_nat_abs] 484 [1: (* Si < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length 485 >commutative_plus @le_plus_a @Hi 486 2,8: (* Spref < 2*16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length 415 [ @(transitive_lt ??? (le_S_S … Hi)) 416 3: @lt_to_not_eq @le_S_S @Hi 417 4,7,10: @(transitive_lt ??? Hi) @le_S_to_le 418 5,11: @le_S_to_le 419 6: @lt_to_not_eq @Hi 420 9: @lt_to_not_eq @le_S @Hi 421 ] 422 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length 487 423 <plus_n_Sm @le_S_S @le_plus_n_r 488  (* Si ≠ Spref *) @lt_to_not_eq @le_S_S @Hi489 4,7: (* i < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length490 >commutative_plus @le_plus_a @le_S_to_le @Hi491 5,11: (* pref < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length492 @le_plus_n_r493  @lt_to_not_eq @Hi494  @lt_to_not_eq @le_S_to_le @le_S_S @Hi495  @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm496 >commutative_plus @le_plus_a @Hi497 ]498 424  >Hi >lookup_opt_insert_miss 499 425 [2: @bitvector_of_nat_abs 500 [ @ (transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r501  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S426 [ @le_S_to_le ] 427 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 502 428 <plus_n_Sm @le_S_S @le_plus_n_r 503 429  @lt_to_not_eq @le_n … … 506 432 >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta 507 433 (* USE: out_of_program_none ← *) 508 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i ?))509 [ >Hi @(transitive_lt … (p i2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r434 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i ?)) 435 [ >Hi @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S @le_plus_n_r 510 436  >Hi 511 437 (* USE: inc_pc = fst policy *) 512 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))438 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 513 439 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) inc_sigma)) 514 440 cases (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) inc_sigma) in ⊢ (???% → %); … … 522 448 cases instr in Heq1; 523 449 [2,3,6: #x [3: #y] #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 524 / by refl/450 <(proj1 ?? (pair_destruct ?????? Heq1)) % 525 451 4,5: #x #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 526 <(proj1 ?? (pair_destruct ?????? Heq1)) @refl452 <(proj1 ?? (pair_destruct ?????? Heq1)) % 527 453 1: #pi cases pi normalize nodelta 528 454 [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: … … 530 456 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 531 457 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 532 / by /458 <(proj1 ?? (pair_destruct ?????? Heq1)) % 533 459 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1 534 460 <(proj2 ?? (pair_destruct ?????? Heq1)) 535 <(proj1 ?? (pair_destruct ?????? Heq1)) 536 / by / 537 ] 538 ] 539 ] 461 <(proj1 ?? (pair_destruct ?????? Heq1)) % 462 ] 463 ] 464 ] 540 465 ] 541 466 ] 542 467 ] 543  (* policy_safe *) cases daemon 544 (* #i >append_length >commutative_plus #Hi normalize in Hi; 545 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 546 [ >nth_append_first 547 [2: @Hi] 548 <(proj2 ?? (pair_destruct ?????? Heq2)) 549 >lookup_insert_miss 550 [ >lookup_insert_miss 468  (* policy_jump_equal → added = 0 *) (* cases daemon *) 469 <(proj2 ?? (pair_destruct ?????? Heq2)) 470 #Heq <(proj1 ?? (pair_destruct ?????? Heq2)) 471 (* USE[pass]: policy_jump_equal → added = 0 *) 472 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) ?) 473 [ cases instr in Heq1 Heq; 474 [2,3,6: #x [3: #y] normalize nodelta #_ #_ % 475 4,5: #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 476 #Heq lapply Holdeq Holdeq 477 (* USE: inc_pc = fst inc_sigma *) 478 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 479 lapply (Heq (prefix) ?) 480 [1,3: >append_length <plus_n_Sm @le_S_S @le_plus_n_r] 481 Heq >lookup_insert_miss 482 [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1)) 483 #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉) 484 #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by / 485 2,4: @bitvector_of_nat_abs 486 [1,4: @le_S_to_le] 487 [1,2,3,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length 488 <plus_n_Sm @le_S_S @le_plus_n_r 489 4,6: @lt_to_not_eq @le_n 490 ] 491 ] 492 1: #pi cases pi normalize nodelta 493 [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: 494 [1,2,3,6,7,24,25: #x #y 495 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #_ @refl 496 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1 497 <(proj2 ?? (pair_destruct ?????? Heq1)) #Heq lapply Holdeq Holdeq 498 (* USE: inc_pc = fst inc_sigma *) 499 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 500 lapply (Heq (prefix) ?) 501 [1,3,5,7,9,11,13,15,17: >append_length <plus_n_Sm @le_S_S @le_plus_n_r] 502 Heq >lookup_insert_miss 503 [1,3,5,7,9,11,13,15,17: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1)) 504 #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉) 505 #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by / 506 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 507 [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n 508 1,4,7,10,13,16,19,22,25: @le_S_to_le 509 ] 510 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S 511 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 512 ] 513 ] 514 ] 515  #i #Hi lapply (Heq i ?) 516 [ >append_length <plus_n_Sm @le_S <plus_n_O @Hi 517  >lookup_insert_miss 551 518 [ >lookup_insert_miss 552 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi) 553 cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉) 554 #pc #j cases (nth i ? prefix 〈None ?, Comment []〉) #label #instr cases j 555 normalize nodelta 556 [ #H cases (le_to_or_lt_eq … Hi) Hi #Hi 557 [ >lookup_insert_miss 558 [ #dest #Hjmp <(proj1 ?? (pair_destruct ?????? Heq2)) 519 [ / by / 520  @bitvector_of_nat_abs 521 [ @(transitive_lt ??? Hi) ] 522 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 523 @le_plus_n_r 524  @lt_to_not_eq @Hi 525 ] 526 ] 527  @bitvector_of_nat_abs 528 [ @(transitive_lt ??? Hi) @le_S_to_le ] 529 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 530 <plus_n_Sm @le_S_S @le_plus_n_r 531  @lt_to_not_eq @le_S @Hi 532 ] 533 ] 534 ] 535 ] *) 536 ] 537  (* added = 0 → policy_pc_equal *) (* cases daemon *) 538 (* USE: added = 0 → policy_pc_equal *) 539 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) 540 <(proj2 ?? (pair_destruct ?????? Heq2)) 541 <(proj1 ?? (pair_destruct ?????? Heq2)) 542 lapply Heq1 Heq1 lapply (refl ? instr) 543 cases instr in ⊢ (???% → % → %); normalize nodelta 544 [2,3,6: #x [3: #y] #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus 545 #Hi normalize in Hi; 546 cases (le_to_or_lt_eq … Hi) Hi #Hi 547 [1,3,5: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 548 [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 549 [1,3,5: >lookup_insert_miss 550 [1,3,5: @(Hold Hadded i (le_S_to_le … Hi)) 551 2,4,6: @bitvector_of_nat_abs 552 [3,6,9: @lt_to_not_eq @Hi 553 1,4,7: @(transitive_lt ??? Hi) 554 ] 555 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 556 @le_S_S <plus_n_Sm @le_S @le_plus_n_r 557 ] 558 2,4,6: @bitvector_of_nat_abs 559 [3,6,9: @lt_to_not_eq @le_S @Hi 560 1,4,7: @(transitive_lt … Hi) @le_S_to_le 561 ] 562 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 563 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 564 ] 565 2,4,6: >Hi >lookup_insert_miss 566 [1,3,5: >lookup_insert_hit >(Hold Hadded (prefix) (le_n (prefix))) 567 @sym_eq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 568 2,4,6: @bitvector_of_nat_abs 569 [3,6,9: @lt_to_not_eq @le_n 570 1,4,7: @le_S_to_le 571 ] 572 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 573 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 574 ] 575 ] 576 2,4,6: >Hi >lookup_insert_hit 577 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 578 <(Hold Hadded (prefix) (le_n (prefix))) 579 (*<(proj2 ?? (pair_destruct ?????? Heq1))*) 580 (* USE: sigma_compact (from old_sigma) *) 581 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (prefix) ?) 582 [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 583 2,4,6: 584 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma))) 585 cases (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma)) in ⊢ (???% > %); 586 [1,3,5: normalize nodelta #_ #ABS cases ABS 587 2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma))) 588 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma)) in ⊢ (???% → %); 589 [1,3,5: normalize nodelta #Hl #x cases x x #pc #j normalize nodelta #Hl2 #ABS cases ABS 590 2,4,6: normalize nodelta #x cases x x #Spc #Sj #EQS #x cases x x #pc #j #EQ 591 normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) 592 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 593 >prf >p1 >Hins >nth_append_second 594 [2,4,6: @(le_n (prefix)) 595 1,3,5: <minus_n_n whd in match (nth ????); 596 559 597 560  561 ] 562  563 ] *) 564 ] 565  (* 0 ↦ 0 *) <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 566 [ cases (decidable_eq_nat 0 (prefix)) 567 [ #Heq <Heq >lookup_insert_hit 568 (* USE: inc_pc = fst policy *) 569 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) 570 (* USE: 0 ↦ 0 *) 571 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) <Heq 572 #ONE #TWO >TWO >ONE @refl 573  #Hneq >lookup_insert_miss 574 [ (* USE: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) 575  @bitvector_of_nat_abs 576 [3: @Hneq] 577 ] 578 ] 579  @bitvector_of_nat_abs 580 [3: @lt_to_not_eq / by / ] 581 ] 582 [1,3: / by / 583 2,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S 584 [2: <plus_n_Sm @le_S_S] 585 @le_plus_n_r 586 ] 587 ] 588  (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2)) 589 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 590 ] 591  (* added = 0 → policy_pc_equal *) 592 (* USE: added = 0 → policy_pc_equal *) 593 lapply (proj2 ?? (proj1 ?? Hpolicy)) 594 lapply Heq2 Heq2 lapply Heq1 Heq1 lapply (refl ? instr) 595 cases daemon 596 (*cases instr in ⊢ (???% → % → % → %); normalize nodelta 597 [ #pi cases pi normalize nodelta 598 599 ] 600 ] 601 4,5: cases daemon 602 1: cases daemon 603 ] (* 4,5 and 1 are equal to 2,3,6, but casesdaemon'd for the moment because of 604 * memory constraints *) 605 (*#x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus 606 #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi #Hi 607 [1,3: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 608 [1,3: >lookup_insert_miss 609 [1,3: >lookup_insert_miss 610 [1,3: @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded; 611 @plus_zero_zero 612 2,4: @bitvector_of_nat_abs 613 [1,4: @(transitive_lt ??? Hi)] 614 [1,2,3,5: @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length 615 @le_plus_n_r 616 4,6: @lt_to_not_eq @Hi 617 ] 618 ] 619 2,4: @bitvector_of_nat_abs 620 [1,4: @(transitive_lt ??? Hi) @le_S_to_le] 621 [1,2,3,5: @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length 622 <plus_n_Sm @le_S_S @le_plus_n_r 623 4,6: @lt_to_not_eq @le_S @Hi 624 ] 625 ] 626 2,4: >Hi >lookup_insert_miss 627 [1,3: >lookup_insert_hit >(Hold ? (prefix) (le_n (prefix))) 628 [2,4: >commutative_plus in Hadded; @plus_zero_zero] 629 @sym_eq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 630 2,4: @bitvector_of_nat_abs 631 [1,4: @(transitive_lt ??? (le_S_S … (le_n (prefix))))] 632 [1,2,3,5: @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length 633 <plus_n_Sm @le_S_S @le_plus_n_r 634 4,6: @lt_to_not_eq @le_n 635 ] 636 ] 637 ] 638 2,4: >Hi >lookup_insert_hit 639 elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded))) 640 [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt <(proj2 ?? (pair_destruct ?????? Heq1)) 641 @etblorp / by I/ 642 2,4: #H >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 643 <(Hold ? (prefix) (le_n (prefix))) 644 <(proj2 ?? (pair_destruct ?????? Heq1)) 645 (* USE: sigma_compact (from old_sigma) *) 646 cases daemon (* XXX add policy_compact_unsafe to old_sigma *) 647 ] 648 ] 649 1: #pi cases pi normalize nodelta 598 650 [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: 599 651 [1,2,3,6,7,24,25: #x #y 600 652 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 601 #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) #Hadded 602 #i >append_length >commutative_plus #Hi normalize in Hi; 653 #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus #Hi normalize in Hi; 603 654 cases (le_to_or_lt_eq … Hi) Hi #Hi 604 655 [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: 605 <(proj2 ?? (pair_destruct ?????? Heq2)) 606 >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16 607 (bitvector_of_nat 16 (S (prefix))) 608 (bitvector_of_nat 16 i)) 656 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 609 657 [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: 610 (* le_to_or_lt_eq, part 2 *) 611 >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc,new_length〉 16 612 (bitvector_of_nat 16 (prefix)) (bitvector_of_nat 16 i)) 613 [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: 614 @(Hold Hadded i (le_S_S_to_le … Hi)) 615 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: 616 @bitvector_of_nat_abs 617 [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: 618 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 619 @le_S_S @le_plus_a @(le_S_S_to_le … Hi) 620 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: 621 @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S 622 @le_plus_n_r 623 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: 624 @lt_to_not_eq @(le_S_to_le … Hi) 658 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 659 [1,3,5: >lookup_insert_miss 660 [1,3,5: @(Hold Hadded i (le_S_to_le … Hi)) 661 2,4,6: @bitvector_of_nat_abs 662 [1,4,7: @(transitive_lt ??? Hi) ] 663 [1,2,3,4,6,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 664 @le_S_S @le_plus_n_r 665 5,7,9: @lt_to_not_eq @Hi 625 666 ] 626 667 ] 627 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: 628 @bitvector_of_nat_abs 629 [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: 630 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 631 @le_S_S @le_plus_a @le_S_to_le @(le_S_S_to_le … Hi) 632 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: 633 @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm 634 @le_S_S @le_plus_n_r 635 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: 636 @lt_to_not_eq @le_S_to_le @Hi 637 ] 638 ] 639 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: 640 <(proj2 ?? (pair_destruct ?????? Heq2)) >(injective_S … Hi) 641 >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16 642 (bitvector_of_nat 16 (S (prefix))) (bitvector_of_nat ? (prefix))) 643 [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: 644 >lookup_insert_hit 645 lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (prefix) ??) 646 [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: 647 >prf >nth_append_second 648 [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: 649 <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H 650 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: 651 @le_n 652 ] 653 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: 654 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 655 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: 656 cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 657 #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl 658 ] 659 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: 660 @bitvector_of_nat_abs 661 [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: 662 @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r 663 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: 664 @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm 665 @le_S_S @le_plus_n_r 666 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: 667 @lt_to_not_eq @le_n 668 ] 669 ] 670 ] 671 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Heq2 #Hold 672 <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1)) 673 #H #i >append_length >commutative_plus #Hi normalize in Hi; 674 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 675 [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq2)) 676 >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16 677 (bitvector_of_nat 16 (S (prefix))) (bitvector_of_nat 16 i)) 678 [1,3,5,7,9,11,13,15,17: 679 >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc,new_length〉 16 680 (bitvector_of_nat 16 (prefix)) (bitvector_of_nat 16 i)) 681 [1,3,5,7,9,11,13,15,17: @(Hold ? i Hi) 682 [1,2,3,4,5,6,7,8,9: @sym_eq @le_n_O_to_eq <H @le_plus_n_r] 683 ] 684 @bitvector_of_nat_abs 685 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf 686 >append_length >commutative_plus @le_S @le_plus_a @Hi 687 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf 688 >append_length @le_S <plus_n_Sm @le_S_S @le_plus_n_r 689 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi 690 ] 691 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 692 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf 693 >append_length >commutative_plus @le_S @le_plus_a @Hi 694 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf 695 >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 696 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi 697 ] 698 ] 699 2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi 700 >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16 701 (bitvector_of_nat 16 (S (prefix))) (bitvector_of_nat 16 (prefix))) 702 [1,3,5,7,9,11,13,15,17: >lookup_insert_hit 703 <(proj1 ?? (pair_destruct ?????? Heq1)) 704 >Holdeq normalize nodelta @sym_eq @blerpque 705 [3,6,9,12,15,18,21,24,27: 706 elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H))) 707 [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp 708 2,4,6,8,10,12,14,16,18: #H @H 709 ] 710 / by I/ 711 2,5,8,11,14,17,20,23,26: / by I/ 712 ] 713 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 714 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf 715 >append_length @le_S_S @le_plus_n_r 716 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf 717 >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 718 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S_S @le_n 719 ] 720 ] 721 ] 722 ] 723 2,3,6: #x [3: #y] #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) 724 #Hadded #i >append_length >commutative_plus #Hi normalize in Hi; 725 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 726 [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 727 [1,3,5: >lookup_insert_miss 728 [1,3,5: @(Hold Hadded i Hi) 729 2,4,6: @bitvector_of_nat_abs 730 [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length 731 >commutative_plus @le_S @le_plus_a @Hi 732 2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 733 @le_S <plus_n_Sm @le_S_S @le_plus_n_r 734 3,6,9: @lt_to_not_eq @Hi 735 ] 736 ] 737 2,4,6: @bitvector_of_nat_abs 738 [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length 739 >commutative_plus @le_S @le_plus_a @Hi 740 2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 741 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 742 3,6,9: @lt_to_not_eq @le_S @Hi 743 ] 744 ] 745 2,4,6: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss 746 [1,3,5: >lookup_insert_hit 747 lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (prefix) ??) 748 [1,4,7: >prf >nth_append_second 749 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H 750 2,4,6: @le_n 751 ] 752 2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 753 3,6,9: 754 cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 755 #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl 756 ] 757 2,4,6: @bitvector_of_nat_abs 758 [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf 759 >append_length @le_S_S @le_plus_n_r 760 2,5,8: @(transitive_lt … (pi2 ?? program)) >prf 761 >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 762 3,6,9: @lt_to_not_eq @le_S_S @le_n 763 ] 764 ] 765 ] 766 4,5: #x #Hins #Heq1 #Heq2 #Hold 767 <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1)) 768 #H #i >append_length >commutative_plus #Hi normalize in Hi; 769 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 770 [1,3: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 771 [1,3: >lookup_insert_miss 772 [1,3: @(Hold ? i Hi) 773 [1,2: @sym_eq @le_n_O_to_eq <H @le_plus_n_r] 774 ] 775 @bitvector_of_nat_abs 776 [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length 777 >commutative_plus @le_S @le_plus_a @Hi 778 2,5: @(transitive_lt … (pi2 ?? program)) >prf >append_length 779 @le_S_S @le_plus_n_r 780 3,6: @lt_to_not_eq @Hi 781 ] 782 2,4: @bitvector_of_nat_abs 783 [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length 784 >commutative_plus @le_S @le_plus_a @Hi 785 2,5: @(transitive_lt … (pi2 ?? program)) >prf >append_length 786 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 787 3,6: @lt_to_not_eq @le_S @Hi 788 ] 789 ] 790 2,4: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss 791 [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1)) 792 >Holdeq normalize nodelta @sym_eq @blerpque 793 [3,6: elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H))) 794 [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp 795 2,4: #H @H 796 ] 797 / by I/ 798 2,5: / by I/ 799 ] 800 2,4: @bitvector_of_nat_abs 801 [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length 802 @le_S_S @le_plus_n_r 803 2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 804 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 805 3,6,9: @lt_to_not_eq @le_S_S @le_n 806 ] 807 ] 808 ] 809 ]*) 810 ] 811  (* policy_jump_equal → added = 0 *) 812 cases daemon 813 ] 814  normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 668 2,4,6: @bitvector_of_nat_abs 669 [1,4,7: @(transitive_lt … Hi) @le_S_to_le] 670 [1,2,3,4,6,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 671 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 672 5,7,9: @lt_to_not_eq @le_S @Hi 673 ] 674 ] 675 2,4,6: >Hi >lookup_insert_miss 676 [1,3,5: >lookup_insert_hit >(Hold Hadded (prefix) (le_n (prefix))) 677 @sym_eq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 678 2,4,6: @bitvector_of_nat_abs 679 [1,4,7: @(transitive_lt ??? (le_S_S … (le_n (prefix))))] 680 [1,2,3,4,6,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 681 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 682 5,7,9: @lt_to_not_eq @le_n 683 ] 684 ] 685 ] 686 2,4,6: >Hi >lookup_insert_hit 687 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 688 <(Hold Hadded (prefix) (le_n (prefix))) 689 <(proj2 ?? (pair_destruct ?????? Heq1)) 690 (* USE: sigma_compact (from old_sigma) *) 691 cases daemon (* XXX add policy_compact_unsafe to old_sigma *) 692 ]*) 693 ] 694  (* lookup p = lookup old_sigma + added *) 695 cases daemon 696 ] 697  (* sigma_safe *) (* cases daemon *) 698 #i >append_length >commutative_plus #Hi normalize in Hi; 699 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 700 [ >nth_append_first [2: @Hi] 701 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 702 [ >lookup_insert_miss 703 [ >lookup_insert_miss 704 [ elim (le_to_or_lt_eq … Hi) Hi #Hi 705 [ >lookup_insert_miss 706 [ (* USE[pass]: sigma_safe *) 707 lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi)) 708 cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉) 709 #pc #j cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉) 710 #pc_plus_jmp_length #_ cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins 711 normalize nodelta #Hind #dest #Hj lapply (Hind dest Hj) Hind 712 lapply (refl ? (leb (lookup_def … labels dest 0) (S (prefix)))) 713 cases (leb (lookup_def … labels dest 0) (S (prefix))) in ⊢ (???% → %); 714 normalize nodelta 715 [ #Hle elim (le_to_or_lt_eq … (leb_true_to_le … Hle)) Hle #Hle 716 [ >(le_to_leb_true … (le_S_S_to_le … Hle)) normalize nodelta 717 >lookup_insert_miss 718 [ elim (le_to_or_lt_eq … (le_S_S_to_le … Hle)) Hle #Hle 719 [ >lookup_insert_miss 720 [ cases j / by / 721  @bitvector_of_nat_abs 722 [ @(transitive_lt ??? Hle) ] 723 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) 724 >prf @le_S_S >append_length @le_plus_n_r 725  @lt_to_not_eq @Hle 726 ] 727 ] 728  >Hle >lookup_insert_hit 729 (* USE: inc_pc = fst policy *) 730 <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 731 cases j / by / 732 ] 733  @bitvector_of_nat_abs 734 [ @(transitive_lt ??? Hle) ] 735 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) 736 @le_S_S >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 737  @lt_to_not_eq @Hle 738 ] 739 ] 740  >Hle >lookup_insert_hit >(not_le_to_leb_false (S (prefix)) (prefix)) 741 [2: @le_to_not_lt @le_n ] normalize nodelta 742 (* USE: lookup p = lookup old_sigma + added *) 743 <(proj2 ?? (proj1 ?? Hpolicy)) cases daemon (* use compactness here *) 744 ] 745  (* same, but with forward jump *) cases daemon 746 ] 747  @bitvector_of_nat_abs cases daemon (* trivial, see above *) 748 ] 749  >Hi >lookup_insert_hit cases daemon 750 ] 751  @bitvector_of_nat_abs cases daemon (* see above *) 752 ] 753  @bitvector_of_nat_abs cases daemon 754 ] 755  @bitvector_of_nat_abs cases daemon 756 ] 757  >Hi cases daemon 758 ] *) 759 ] 760  normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 815 761 [ #i cases i 816 762 [ #Hi2 @conj … … 829 775  #_ @le_S_S @le_O_n 830 776 ] 831 ] 777 ] 832 778  #i cases i 833 779 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O … … 835 781 ] 836 782 ] 783  >lookup_insert_hit @refl 784 ] 785  >lookup_insert_hit @refl 786 ] 837 787  #i #Hi <(le_n_O_to_eq … Hi) 838 788 >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉) … … 844 794 ] 845 795 ] 796  #_ % 797 ] 798  #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit 799 (* USE: 0 ↦ 0 (from old_sigma) *) 800 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) 801 ] 802  cases daemon (* empty program here *) 803 ] 846 804  #i cases i 847 805 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O … … 849 807 ] 850 808 ] 851  >lookup_insert_hit @refl852 ]853  >lookup_insert_hit @refl854 ]855  #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit856 (* USE: 0 ↦ 0 (from old_sigma *)857 @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))858 ]859  #_ @refl860 ]861 809 ] 862 810 qed.
Note: See TracChangeset
for help on using the changeset viewer.