Changeset 2059
 Timestamp:
 Jun 13, 2012, 3:44:20 PM (6 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r2055 r2059 7 7 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (S (l)) 2^16) (n: ℕ) 8 8 on n:(Σx:bool × (option ppc_pc_map). 9 let 〈 c,pol〉 ≝ x in9 let 〈no_ch,pol〉 ≝ x in 10 10 And 11 11 (match pol with 12 12 [ None ⇒ True 13 13  Some x ⇒ 14 And (And (And (And 14 And (And (And (And (And 15 15 (out_of_program_none program x) 16 16 (jump_not_in_policy program x)) 17 (n > 0→ policy_compact program (create_label_map program) x))17 (no_ch = true → policy_compact program (create_label_map program) x)) 18 18 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0)) 19 (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd x) 〈0,short_jump〉))) 19 20 (\fst x < 2^16) 20 ]) (n = 0 → c = true)) ≝21 ]) (n = 0 → no_ch = false)) ≝ 21 22 let labels ≝ create_label_map program in 22 23 match n return λx.n = x → Σa:bool × (option ppc_pc_map).? with 23 [ O ⇒ λp.〈 true,pi1 ?? (jump_expansion_start program labels)〉24  S m ⇒ λp.let 〈 ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in24 [ O ⇒ λp.〈false,pi1 ?? (jump_expansion_start program labels)〉 25  S m ⇒ λp.let 〈no_ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in 25 26 match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with 26 27 [ None ⇒ λp2.〈false,None ?〉 27  Some op ⇒ λp2.if ch28 then pi1 ?? (jump_expansion_ step program labels «op,?»)29 else pi1 ?? (jump_expansion_ internal program m)28  Some op ⇒ λp2.if no_ch 29 then pi1 ?? (jump_expansion_internal program m) 30 else pi1 ?? (jump_expansion_step program labels «op,?») 30 31 ] (refl … z) 31 32 ] (refl … n). … … 33 34 #x cases x x 34 35 [ #H @conj / by I/ 35  #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj 36  #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj [ @conj 36 37 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 37  >p #H @⊥ @(absurd ? H) @le_to_not_lt @le_n38  >p #H destruct (H) 38 39 ] 39 40  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 40 41 ] 42  cases daemon (* XXX add this to jump_expansion_start *) 43 ] 41 44  @(proj2 ?? H) 42 45 ] … … 45 48 ] 46 49  normalize nodelta @conj [ / by I/  >p #H destruct (H) ] 47  cases ch in p1; #p1 48 [ normalize nodelta 49 cases (jump_expansion_step program (create_label_map program) «op,?») 50  cases no_ch in p1; #p1 51 [ normalize nodelta lapply (pi2 ?? (jump_expansion_internal program m)) 52 <p1 >p2 normalize nodelta #H @conj 53 [ @(proj1 ?? H) 54  >p #H2 destruct (H2) 55 ] 56  cases (jump_expansion_step program (create_label_map program) «op,?») 50 57 #x cases x x #ch2 #z2 cases z2 normalize nodelta 51 58 [ #_ @conj [ / by I/  >p #H2 destruct (H2) ] 52  #j2 #H2 @conj [ @conj [ @conj [ @conj 53 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))) 54  #_ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))) 59  #j2 #H2 @conj [ @conj [ @conj [ @conj [ @conj 60 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))) 61  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))) 62 ] 63  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))) 55 64 ] 56 65  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))) … … 60 69  >p #H3 destruct (H3) 61 70 ] 62 ]63  normalize nodelta lapply (pi2 ?? (jump_expansion_internal program m))64 <p1 >p2 normalize nodelta #H @conj [ @conj [ @conj [ @conj65 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))66  >p #Hm cases (le_to_or_lt_eq … Hm) Hm #Hm67 [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @(le_S_S_to_le … Hm)68  lapply ((proj2 ?? H) (sym_eq … (injective_S … Hm))) #H2 destruct (H2)69 ]70 ]71  @(proj2 ?? (proj1 ?? (proj1 ?? H)))72 ]73  @(proj2 ?? (proj1 ?? H))74 ]75  >p #H2 destruct (H2)76 71 ] 77 72 ] … … 80 75 [ #_ >p2 #ABS destruct (ABS) 81 76  #map >p2 normalize nodelta 82 #H #eq destruct (eq) @conj [ @conj 83 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 77 #H #eq destruct (eq) @conj [ @conj [ @conj 78 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 79  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 80 ] 84 81  @(proj2 ?? (proj1 ?? (proj1 ?? H))) 85 82 ] … … 90 87 qed. 91 88 92 lemma pe_int_refl: ∀program.reflexive ? (policy_ equal program).89 lemma pe_int_refl: ∀program.reflexive ? (policy_jump_equal program). 93 90 #program whd #x whd #n #Hn 94 91 cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,short_jump〉) … … 96 93 qed. 97 94 98 lemma pe_int_sym: ∀program.symmetric ? (policy_ equal program).95 lemma pe_int_sym: ∀program.symmetric ? (policy_jump_equal program). 99 96 #program whd #x #y #Hxy whd #n #Hn 100 97 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉) … … 104 101 qed. 105 102 106 lemma pe_int_trans: ∀program.transitive ? (policy_ equal program).107 #program whd #x #y #z whd in match (policy_ equal ???); whd in match (policy_equal ?y ?);108 whd in match (policy_ equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) Hxy103 lemma pe_int_trans: ∀program.transitive ? (policy_jump_equal program). 104 #program whd #x #y #z whd in match (policy_jump_equal ???); whd in match (policy_jump_equal ?y ?); 105 whd in match (policy_jump_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) Hxy 109 106 lapply (Hyz n Hn) Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉) 110 107 #x1 #x2 … … 118 115 match p1 with 119 116 [ Some x1 ⇒ match p2 with 120 [ Some x2 ⇒ policy_ equal program x1 x2117 [ Some x2 ⇒ policy_jump_equal program x1 x2 121 118  _ ⇒ False 122 119 ] … … 252 249 jump_not_in_policy program p ∧ 253 250 \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧ 251 \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉) ∧ 254 252 \fst p < 2^16. 255 253 ∀l.l ≤ program → ∀acc:ℕ. … … 265 263 [ / by I/ 266 264  #x normalize nodelta #Hx #Hjeq 267 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx))))) (t) Hp)265 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))))) (t) (le_S_to_le … Hp)) 268 266 whd in match (measure_int ???); whd in match (measure_int ? x ?); 269 267 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd (pi1 ?? policy)) 〈0,short_jump〉) … … 336 334 out_of_program_none program p ∧ jump_not_in_policy program p ∧ 337 335 \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧ 336 \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉) ∧ 338 337 \fst p < 2^16. 339 338 match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with 340 339 [ None ⇒ True 341  Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_ equal program policy p ].340  Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_jump_equal program policy p ]. 342 341 #program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) 343 342 cases (jump_expansion_step program (create_label_map program) policy) in ⊢ (???% → %); … … 347 346 @(list_ind ? (λx.x ≤ pi1 ?? program → 348 347 measure_int x policy 0 = measure_int x p 0 → 349 policy_ equal x policy p) ?? (pi1 ?? program))348 policy_jump_equal x policy p) ?? (pi1 ?? program)) 350 349 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @le_to_not_lt @le_O_n 351 350  #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi … … 353 352 [ @(transitive_le … Hp) / by / 354 353  whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; 355 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))))) (t) Hp) #Hinc356 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉) in Hm Hinc; #x1 #x2357 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉); #y1 #y2358 # Hm #Hinc lapply Hm Hm; lapply Hinc Hinc; normalize nodelta354 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (t) (le_S_to_le … Hp)) 355 #Hinc cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉) in Hm Hinc; 356 #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉); 357 #y1 #y2 #Hm #Hinc lapply Hm Hm; lapply Hinc Hinc; normalize nodelta 359 358 cases x2 cases y2 normalize nodelta 360 359 [1: / by / … … 376 375 ] 377 376  >Hi whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; 378 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))))) (t) Hp)377 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (t) (le_S_to_le … Hp)) 379 378 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉) in Hm; 380 379 #x1 #x2 … … 436 435 [ None ⇒ True 437 436  Some pol ⇒ And (out_of_program_none program pol) 438 ( (pi1 ?? program) ≠ [] →policy_compact program (create_label_map program) pol)437 (policy_compact program (create_label_map program) pol) 439 438 ]) 440 439 (∃n.∀k.n < k → … … 442 441 #program @(\snd (pi1 ?? (jump_expansion_internal program (2*program)))) @conj 443 442 [ lapply (pi2 ?? (jump_expansion_internal program (2*program))) 444 445 446 447  #x normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))448  #Hneq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) cases (pi1 ?? program) in Hneq;449 [ #H cases H #H @⊥ @H @refl450  #h #t #_ / by /451 ]]452 443 cases (jump_expansion_internal program (2*program)) #p cases p p 444 #c #pol #Hp cases pol 445 [ normalize nodelta // 446  #x normalize nodelta #H @conj 447 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))) 448  #Hneq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 449 cases daemon (* XXX add invariant here *) 450 ] 451 ] 453 452  cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program) 454 453 (\snd (pi1 ?? (jump_expansion_internal program k))) … … 477 476 >EQ normalize nodelta 478 477 lapply (refl ? (jump_expansion_step program (create_label_map program) «Fp,?»)) 479 [ @conj [ @conj 480 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) 481  @(proj2 ?? (proj1 ?? (proj1 ?? HFp))) ] 482  @(proj2 ?? (proj1 ?? HFp)) ] 478 [ @conj [ @conj [ @conj 479 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))) 480  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) 481 ] 482  @(proj2 ?? (proj1 ?? (proj1 ?? HFp))) 483 ] 484  @(proj2 ?? (proj1 ?? HFp)) 485 ] 483 486  lapply (measure_full program Fp ?) 484 487 [ @le_to_le_to_eq … … 517 520 [ cases (jump_expansion_internal program x) in Hxpol; 518 521 #z cases z z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H; 519 normalize nodelta #H @conj [ @conj 520 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 522 normalize nodelta #H @conj [ @conj [ @conj 523 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 524  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) ] 521 525  @(proj2 ?? (proj1 ?? (proj1 ?? H))) ] 522 526  @(proj2 ?? (proj1 ?? H)) ] … … 524 528 lapply (refl ? (jump_expansion_internal program x)) 525 529 lapply Hxpol Hxpol 526 whd in match (jump_expansion_internal program (S x)); 530 cases daemon (* this whd takes an enormous amount of time *) 531 (* whd in match (pi1 ?? (jump_expansion_internal program (S x))); 527 532 cases (jump_expansion_internal program x) in ⊢ (% → ???% → %); 528 533 #z cases z z #xch #b normalize nodelta #H #Heq >(proj1 ?? Heq) in H; 529 534 #H #Heq2 cases xch in H Heq2; #H #Heq2 normalize nodelta 530 535 [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»)) 531 [ @conj [ @conj 532 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 536 [ @conj [ @conj [ @conj 537 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 538  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) ] 533 539  @(proj2 ?? (proj1 ?? (proj1 ?? H))) ] 534 540  @(proj2 ?? (proj1 ?? H)) ] … … 559 565 ] 560 566 ] 561 ] 567 ] *) 562 568 ] 563 569 ] … … 572 578 [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull 573 579  #Gp #HGp #EQ2 cases Fch 574 [ normalize nodelta #i #Hi 580 [ normalize nodelta /2 by pe_int_refl/ 581  normalize nodelta #i #Hi 575 582 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj 576 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))) i Hi)583 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))))) i (le_S_to_le … Hi)) 577 584 lapply (Hfull i Hi Hj) 578 585 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉) … … 583 590 3: #_ @refl 584 591 ] 585  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))))) i Hi Hj)586 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl592  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))))) i Hi Hj) 593 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))) i Hi Hj) @refl 587 594 ] 588  normalize nodelta /2 by pe_int_refl/589 595 ] 590 596 ] … … 599 605 cases npol in Hnpol; cases Spol in HSpol; 600 606 [ #Hnpol #HSpol %1 // 601 2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal ???); //607 2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); // 602 608 #H destruct (H) 603 4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); cases program #p #_ cases p609 4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); cases program #p #_ cases p 604 610 [ %1 #m #Hm @⊥ @(absurd ? Hm) @le_to_not_lt @le_O_n 605 611  #h #t elim (dec_bounded_forall ?? (t)) 
src/ASM/PolicyFront.ma
r2048 r2059 128 128 ppc_pc_map → Prop ≝ 129 129 λprogram.λop.λp. 130 ∀i.i <program →130 ∀i.i ≤ program → 131 131 let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,short_jump〉 in 132 132 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉 in 133 133 (*opc ≤ pc ∧*) jmpleq oj j. 134 134 135 135 (* this is the instruction size as determined by the jump length given *) 136 136 definition expand_relative_jump_internal_unsafe: … … 639 639 qed. 640 640 641 definition policy_equal ≝ 641 (* NOTE: we only compare the first elements here because otherwise the 642 * added = 0 → policy_equal property of jump_expansion_step doesn't hold: 643 * if we have not added anything to the pc, we only know the PC hasn't changed, 644 * there might still have been a short/medium jump change *) 645 definition policy_pc_equal ≝ 642 646 λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. 643 647 (∀n:ℕ.n ≤ program → 644 bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 = 645 bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉). 648 \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = 649 \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). 650 651 definition policy_jump_equal ≝ 652 λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. 653 (∀n:ℕ.n < program → 654 \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = 655 \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). 646 656 647 657 definition nec_plus_ultra ≝ 
src/ASM/PolicyStep.ma
r2038 r2059 1 1 include "ASM/PolicyFront.ma". 2 3 2 include alias "basics/lists/list.ma". 4 3 include alias "arithmetics/nat.ma". … … 12 11 address_of_word_labels_code_mem program l). 13 12 ∀old_policy:(Σpolicy:ppc_pc_map. 14 And (And (And ( out_of_program_none program policy)13 And (And (And (And (out_of_program_none program policy) 15 14 (jump_not_in_policy program policy)) 16 15 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 16 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd policy) 〈0,short_jump〉))) 17 17 (\fst policy < 2^16)). 18 18 (Σx:bool × (option ppc_pc_map). … … 20 20 match y with 21 21 [ None ⇒ nec_plus_ultra program old_policy 22  Some p ⇒ And (And (And (And (And (And (And ( out_of_program_none program p)22  Some p ⇒ And (And (And (And (And (And (And (And (out_of_program_none program p) 23 23 (jump_not_in_policy program p)) 24 24 (policy_increase program old_policy p)) 25 ( policy_compact program labels p))25 (no_ch = true → policy_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 (no_ch = true → policy_equal program old_policy p)) 28 (no_ch = true → policy_pc_equal program old_policy p)) 29 (policy_jump_equal program old_policy p → no_ch = true)) 29 30 (\fst p < 2^16) 30 31 ]) … … 35 36 (λprefix.Σx:ℕ × ppc_pc_map. 36 37 let 〈added,policy〉 ≝ x in 37 And (And (And (And (And (And (And ( out_of_program_none prefix policy)38 And (And (And (And (And (And (And (And (out_of_program_none prefix policy) 38 39 (jump_not_in_policy prefix policy)) 39 40 (policy_increase prefix old_sigma policy)) 40 41 (policy_compact_unsafe prefix labels policy)) 41 (policy_safe prefix labels policy))42 (policy_safe prefix labels added old_sigma policy)) 42 43 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 43 44 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉))) 44 (added = 0 → policy_equal prefix old_sigma policy)) 45 (added = 0 → policy_pc_equal prefix old_sigma policy)) 46 (policy_jump_equal prefix old_sigma policy → added = 0)) 45 47 program 46 48 (λprefix.λx.λtl.λprf.λacc. … … 74 76  Some x ⇒ plus inc_added (minus isize old_size) 75 77 ] in 78 let old_Slength ≝ 79 \snd (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in 76 80 let updated_sigma ≝ 77 81 (* we add the new PC to the next position and the new jump length to this one *) 78 bvt_insert … (bitvector_of_nat ? (S (prefix))) 〈inc_pc + isize, short_jump〉82 bvt_insert … (bitvector_of_nat ? (S (prefix))) 〈inc_pc + isize, old_Slength〉 79 83 (bvt_insert … (bitvector_of_nat ? (prefix)) 〈inc_pc, new_length〉 inc_sigma) in 80 84 〈new_added, 〈plus inc_pc isize, updated_sigma〉〉 81 ) 〈0, 〈0, bvt_insert … (bitvector_of_nat 16 0) 〈0, short_jump〉 (Stub ??)〉〉) in 85 ) 〈0, 〈0, 86 bvt_insert … 87 (bitvector_of_nat ? 0) 88 〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉 89 (Stub ??)〉〉 90 ) in 82 91 if geb (\fst final_policy) 2^16 then 83 92 〈eqb final_added 0, None ?〉 84 93 else 85 94 〈eqb final_added 0, Some ? final_policy〉. 86 [ normalize nodelta cases daemon (* XXX nec_plus_ultra *) 95 [ normalize nodelta @nmk #Habs lapply p generalize in match (foldl_strong ?????); * 96 #x #H #Heq >Heq in H; normalize nodelta Heq x #Hind 97 (* USE: inc_pc = fst of policy (from fold) *) 98 >(proj2 ?? (proj1 ?? (proj1 ?? Hind))) in p1; 99 (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *) 100 lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (pi2 ?? old_sigma))) 101 #Hsig #Hge 102 (* USE: added = 0 → policy_pc_equal (from fold) *) 103 lapply ((proj2 ?? (proj1 ?? Hind)) ? (program) (le_n (program))) 104 [ @(proj2 ?? Hind) #i #Hi 105 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 106 [ #Hj 107 (* USE: policy_increase (from fold) *) 108 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi)) 109 lapply (Habs i Hi Hj) 110 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉) 111 #opc #oj 112 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd final_policy) 〈0,short_jump〉) 113 #pc #j normalize nodelta #Heq >Heq cases j 114 [1,2: #abs cases abs #abs2 try (cases abs2) @refl 115 3: #_ @refl 116 ] 117  #Hnj 118 (* USE: jump_not_in_policy (from fold and old_sigma) *) 119 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))))) i Hi Hnj) 120 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj) 121 @refl 122 ] 123  #abs >abs in Hsig; #Hsig 124 @(absurd ? Hsig) @le_to_not_lt @leb_true_to_le <geb_to_leb @Hge 125 ] 87 126  normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2 88 127 >H2 in H; normalize nodelta H2 x #H @conj 89 [ @conj 90 [ @conj 91 [ @conj 92 [ @conj 93 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 94  (* policy_compact_unsafe → policy_compact (in the end) *) 95 #i #Hi 96 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) i Hi) 97 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))) i Hi) 98 lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd final_policy))) 99 cases (lookup_opt … (bitvector_of_nat ? i) (\snd final_policy)) in ⊢ (???% → %); 100 [ / by / 101  #x cases x x #x1 #x2 #EQ 102 cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd final_policy)) 103 [ / by / 104  #y cases y y #y1 #y2 normalize nodelta #H #H2 105 cut ( 106 instruction_size_jmplen x2 107 (\snd (nth i ? (pi1 ?? program) 〈None ?, Comment []〉)) = 108 instruction_size … (bitvector_of_nat ? i) 109 (\snd (nth i ? (pi1 ?? program) 〈None ?, Comment []〉)) 110 ) 111 [5: #H3 <H3 @H2 112 4: whd in match (instruction_size_jmplen ??); 113 whd in match (instruction_size …); 114 whd in match (assembly_1_pseudoinstruction …); 115 whd in match (expand_pseudo_instruction …); 116 normalize nodelta whd in match (append …) in H; 117 cases (nth i ? (pi1 ?? program) 〈None ?,Comment []〉) in H; 118 #lbl #instr cases instr 119 [2,3,6: #x [3: #y] normalize nodelta #H @refl 120 4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 121 #Hj lapply (Hj x (refl ? x)) Hj 122 normalize nodelta >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O 123 cases x2 normalize nodelta 124 [1,4: 125 whd in match short_jump_cond; normalize nodelta 126 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 127 #result #flags normalize nodelta 128 cases (vsplit bool 8 8 result) 129 #upper #lower normalize nodelta 130 cases (eq_bv 8 upper (zero 8)) 131 [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3) 132 1: #_ normalize @refl 133 3: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/ 134 ] 135 2,5: whd in match short_jump_cond; whd in match medium_jump_cond; 136 normalize nodelta 137 cases (vsplit bool 5 11 ?) #addr1 #addr2 138 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 139 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 140 #result #flags normalize nodelta 141 cases (vsplit bool 8 8 result) 142 #upper #lower normalize nodelta 143 #H >(not_true_is_false ? (proj2 ?? (proj1 ?? H))) 144 >(proj1 ?? (proj1 ?? H)) normalize @refl 145 3,6: whd in match short_jump_cond; whd in match medium_jump_cond; 146 normalize nodelta 147 cases (vsplit bool 5 11 ?) #addr1 #addr2 148 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 149 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 150 #result #flags normalize nodelta 151 cases (vsplit bool 8 8 result) 152 #upper #lower normalize nodelta 153 #H >(not_true_is_false ? (proj1 ?? H)) >(not_true_is_false ? (proj2 ?? H)) 154 normalize nodelta normalize @refl 155 ] 156 1: #pi cases pi 157 [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: 158 [1,2,3,6,7,24,25: #x #y 159 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 160 normalize nodelta #H @refl 161 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta 162 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj 163 [1,2,3,4,5: lapply (Hj y (refl ? y))  6,7,8,9: lapply (Hj x (refl ? x))] Hj 164 whd in match expand_relative_jump; normalize nodelta 165 whd in match expand_relative_jump_internal; normalize nodelta 166 whd in match expand_relative_jump_unsafe; normalize nodelta 167 whd in match expand_relative_jump_internal_unsafe; 168 normalize nodelta >(add_bitvector_of_nat_plus ? i 1) 169 <(plus_n_Sm i 0) <plus_n_O cases x2 normalize nodelta 170 [1,4,7,10,13,16,19,22,25: 171 whd in match short_jump_cond; normalize nodelta 172 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 173 #result #flags normalize nodelta 174 cases (vsplit bool 8 8 result) 175 #upper #lower normalize nodelta 176 cases (eq_bv 8 upper (zero 8)) 177 [2,4,6,8,10,12,14,16,18: #H lapply (proj1 ?? H) #H3 destruct (H3) 178 1,3,5,7,9,11,13,15,17: #_ normalize nodelta 179 [6,7,8,9: normalize @refl] 180 whd in match (map ????); 181 whd in match (map ??? []); 182 whd in match (map ????); 183 whd in match (map ??? []); 184 normalize cases x 185 [1,2,3,6: #am cases am normalize nodelta 186 [1,2,3,4,8,9,16,17,18,19: #z #Ham cases Ham 187 5,6,7,10,11,12,13,14: #Ham cases Ham 188 15: #z #Ham normalize @refl 189 20,21,22,23,27,28,35,36,37,38: #z #Ham cases Ham 190 24,25,26,29,30,31,32,33: #Ham cases Ham 191 34: #z #Ham normalize @refl 192 39,40,41,42,46,47,54,55,56,57: #z #Ham cases Ham 193 43,44,45,48,49,50,51,52: #Ham cases Ham 194 53: #z #Ham normalize @refl 195 59,60,65,66,72,73,74,75,76: #z #Ham cases Ham 196 62,63,64,67,68,69,70,71: #Ham cases Ham 197 58,61: #z #Ham normalize @refl 198 ] 199 ] 200 #w cases w #w1 #w2 cases w2 #am cases am normalize nodelta 201 [1,2,3,4,8,9,15,16,17,18,19: #z #Ham @refl 202 5,6,7,10,11,12,13,14: #Ham @refl 203 20,21,22,23,28: #z #Ham cases Ham 204 24,25,26: #Ham cases Ham 205 27: #z #Ham cases w1 #am cases am normalize nodelta 206 [1,2,3,4,8,9,15,16,17,18,19: #z #Ham @refl 207 5,6,7,10,11,12,13,14: #Ham @refl 208 ] 209 34,35,36,37,38: #z #Ham cases Ham 210 29,30,31,32,33: #Ham cases Ham 211 ] 212 ] 213 2,5,8,11,14,17,20,23,26: 214 whd in match short_jump_cond; whd in match medium_jump_cond; 215 normalize nodelta 216 cases (vsplit bool 5 11 ?) #addr1 #addr2 217 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 218 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 219 #result #flags normalize nodelta 220 cases (vsplit bool 8 8 result) 221 #upper #lower normalize nodelta 222 #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/ 223 3,6,9,12,15,18,21,24,27: 224 whd in match short_jump_cond; whd in match medium_jump_cond; 225 normalize nodelta 226 cases (vsplit bool 5 11 ?) #addr1 #addr2 227 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 228 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 229 #result #flags normalize nodelta 230 cases (vsplit bool 8 8 result) 231 #upper #lower normalize nodelta 232 #H >(not_true_is_false ? (proj1 ?? H)) >(not_true_is_false ? (proj2 ?? H)) 233 [6,7,8,9: normalize @refl] 234 cases x normalize nodelta 235 [1,2,3,6: #am cases am normalize nodelta 236 [1,2,3,4,8,9,16,17,18,19: #z #Ham cases Ham 237 5,6,7,10,11,12,13,14: #Ham cases Ham 238 15: #z #Ham @refl 239 20,21,22,23,27,28,35,36,37,38: #z #Ham cases Ham 240 24,25,26,29,30,31,32,33: #Ham cases Ham 241 34: #z #Ham @refl 242 39,40,41,42,46,47,54,55,56,57: #z #Ham cases Ham 243 43,44,45,48,49,50,51,52: #Ham cases Ham 244 53: #z #Ham @refl 245 59,60,65,66,72,73,74,75,76: #z #Ham cases Ham 246 62,63,64,67,68,69,70,71: #Ham cases Ham 247 58,61: #z #Ham @refl 248 ] 249 ] 250 #w cases w normalize nodelta #w1 #w2 cases w2 normalize nodelta 251 #am cases am normalize nodelta 252 [2,3,4,9,15,16,17,18,19: #z #Ham cases Ham 253 5,6,7,10,11,12,13,14: #Ham cases Ham 254 1,8: #z #Ham @refl 255 20,21,22,23,28: #z #Ham cases Ham 256 24,25,26: #Ham cases Ham 257 27: #z #Ham cases w1 normalize nodelta #am cases am normalize nodelta 258 [1,3,8,9,15,16,17,18,19: #z #Ham cases Ham 259 5,6,7,10,11,12,13,14: #Ham cases Ham 260 2,4: #z #Ham @refl 261 ] 262 34,35,36,37,38: #z #Ham cases Ham 263 29,30,31,32,33: #Ham cases Ham 264 ] 265 ] 266 ] 267 ] 268 ] 128 [ @conj [ @conj [ @conj [ @conj [ @conj 129 [ (* USE[pass]: out_of_program_none, jump_not_in_policy, 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: cases daemon (* XXX *) ] 168 [1,5: >(eqb_true_to_eq … Hch) <plus_n_O] 169 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 170 #result #flags normalize nodelta 171 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 172 cases (get_index' bool 2 0 flags) normalize nodelta 173 [1,3,5,7: cases (eq_bv 9 upper ?) 174 2,4,6,8: cases (eq_bv 9 upper (zero 9))] 175 [2,4,6,8,10,12,14,16: #H lapply (proj1 ?? H) #H3 destruct (H3) 176 5,7,13,15: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/ 177 1,3,9,11: #_ normalize nodelta @refl 269 178 ] 270 ] 271 ] 272  @(proj2 ?? (proj1 ?? (proj1 ?? H))) 273 ] 274  @(proj2 ?? (proj1 ?? H)) 275 ] 276  #H2 @(proj2 ?? H) @eqb_true_to_eq @H2 277 ] 278  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1 279 ] 179 2,5: whd in match short_jump_cond; whd in match medium_jump_cond; 180 lapply (refl ? (leb i (lookup_def ?? labels x 0))) 181 cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab 182 normalize nodelta 183 (* USE: added = 0 → policy_pc_equal *) 184 >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?) 185 [2,4,6,8: cases daemon (* XXX *)] 186 [1,3: >(eqb_true_to_eq … Hch) <plus_n_O] 187 normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2 188 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 189 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 190 #result #flags normalize nodelta 191 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 192 cases (get_index' bool 2 0 flags) normalize nodelta 193 #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl 194 3,6: whd in match short_jump_cond; whd in match medium_jump_cond; 195 lapply (refl ? (leb i (lookup_def ?? labels x 0))) 196 cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab 197 normalize nodelta 198 >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?) 199 [2,4,6,8: cases daemon (* XXX *)] 200 [1,3: >(eqb_true_to_eq … Hch) <plus_n_O] 201 normalize nodelta 202 cases (vsplit bool 5 11 ?) #addr1 #addr2 203 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 204 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 205 #result #flags normalize nodelta 206 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 207 cases (get_index' bool 2 0 flags) normalize nodelta 208 #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl 209 ] 210 1: #pi cases pi 211 [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: 212 [1,2,3,6,7,24,25: #x #y 213 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 214 normalize nodelta #H @refl 215 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x 3,4,5,8,9: #y #x] 216 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 217 #Hj lapply (Hj x (refl ? x)) Hj 218 whd in match expand_relative_jump; normalize nodelta 219 whd in match expand_relative_jump_internal; normalize nodelta 220 whd in match expand_relative_jump_unsafe; normalize nodelta 221 whd in match expand_relative_jump_internal_unsafe; 222 normalize nodelta >(add_bitvector_of_nat_plus ? i 1) 223 <(plus_n_Sm i 0) <plus_n_O 224 cases daemon (* XXX *) 225 ] 226 ] 227 ] 228 ] 229 ] 230 ] 231  (* USE: 0 ↦ 0 (from fold) *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 232 ] 233  (* USE: inc_pc = fst of policy (from fold) *) @(proj2 ?? (proj1 ?? (proj1 ?? H))) 234 ] 235  #H2 (* USE: added = 0 → policy_pc_equal (from fold) *) 236 @(proj2 ?? (proj1 ?? H)) @eqb_true_to_eq @H2 237 ] 238  #H2 (* USE: policy_jump_equal → added = 0 (from fold *) 239 @eq_to_eqb_true @(proj2 ?? H) @H2 240 ] 241  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1 242 ] 280 243 4: lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma 281 244 lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)) … … 283 246 #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta 284 247 @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2 285 @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 248 @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 286 249 [ (* out_of_program_none *) #i #Hi2 >append_length <commutative_plus @conj 287 250 [ (* → *) #Hi normalize in Hi; … … 289 252 #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss 290 253 [1,3,5,7,9,11: >lookup_opt_insert_miss 291 [1,3,5,7,9,11: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i Hi2)) 254 [1,3,5,7,9,11: (* USE: out_of_program_none → *) 255 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi2)) 292 256 @le_S_to_le @Hi 293 257 2,4,6,8,10,12: @bitvector_of_nat_abs … … 307 271 [ #Hi 308 272 lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl)))) 309 #Hl2 310 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i Hi2) Hl2)273 #Hl2 (* USE: out_of_program_none ← *) 274 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi2) Hl2) 311 275 #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3 312 276  #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi)) … … 325 289 [ >lookup_insert_miss 326 290 [ >(nth_append_first ? i prefix ?? Hi) 327 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i Hi) 291 (* USE: jump_not_in_policy *) 292 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi) 328 293  @bitvector_of_nat_abs 329 294 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm … … 368 333 ] 369 334  (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi; 370 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi; #Hi 371 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i Hi) 372 <(proj2 ?? (pair_destruct ?????? Heq2)) 373 @pair_elim #opc #oj #EQ1 >lookup_insert_miss 374 [ >lookup_insert_miss 375 [ @pair_elim #pc #j #EQ2 / by / 335 cases (le_to_or_lt_eq … Hi) Hi; #Hi 336 [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 337 [ (* USE: policy_increase *) 338 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi)) 339 <(proj2 ?? (pair_destruct ?????? Heq2)) 340 @pair_elim #opc #oj #EQ1 >lookup_insert_miss 341 [ >lookup_insert_miss 342 [ @pair_elim #pc #j #EQ2 / by / 343  @bitvector_of_nat_abs 344 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S 345 >commutative_plus @le_plus_a @Hi 346  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r 347  @lt_to_not_eq @Hi 348 ] 349 ] 376 350  @bitvector_of_nat_abs 377 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S <commutative_plus351 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S >commutative_plus 378 352 @le_plus_a @Hi 379  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r 380  @lt_to_not_eq @Hi 381 ] 382 ] 383  @bitvector_of_nat_abs 384 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S >commutative_plus 385 @le_plus_a @Hi 386  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_plus_n_r 387  @lt_to_not_eq @le_S @Hi 388 ] 389 ] 390  >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 391 [ >lookup_insert_hit 392 cases (dec_is_jump instr) 393 [ cases instr in Heq1; normalize nodelta 394 [ #pi cases pi 395 [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: 396 [1,2,3,6,7,24,25: #x #y 397 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj 398 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 399 whd in match jump_expansion_step_instruction; normalize nodelta #Heq1 400 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ >Holdeq normalize nodelta 401 @jmpleq_max_length 353  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_plus_n_r 354  @lt_to_not_eq @le_S @Hi 355 ] 356 ] 357  >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) @pair_elim #opc #oj #EQ1 358 >lookup_insert_miss 359 [ >lookup_insert_hit cases (dec_is_jump instr) 360 [ cases instr in Heq1; normalize nodelta 361 [ #pi cases pi 362 [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: 363 [1,2,3,6,7,24,25: #x #y 364 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj 365 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 366 whd in match jump_expansion_step_instruction; normalize nodelta #Heq1 367 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq in EQ1; normalize nodelta 368 #H42 >(proj2 ?? (pair_destruct ?????? H42)) @jmpleq_max_length 369 ] 370 2,3,6: #x [3: #y] #_ #Hj cases Hj 371 4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq in EQ1; 372 normalize nodelta #H42 >(proj2 ?? (pair_destruct ?????? H42)) @jmpleq_max_length 402 373 ] 403 2,3,6: #x [3: #y] #_ #Hj cases Hj 404 4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq normalize nodelta 405 @jmpleq_max_length 406 ] 407  lapply Heq1 Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta 408 [ #pi cases pi 409 [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: 410 [1,2,3,6,7,24,25: #x #y 411 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 412 whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1 413 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 414 lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (prefix) ??) 415 [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: 416 >prf >nth_append_second 417 [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: 418 <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 419 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: 420 @le_n 374  lapply Heq1 Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta 375 [ #pi cases pi 376 [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: 377 [1,2,3,6,7,24,25: #x #y 378 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 379 whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1 380 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 381 (* USE: jump_not_in_policy (from old_sigma) *) 382 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??) 383 [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: 384 >prf >nth_append_second 385 [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: 386 <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 387 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: 388 @le_n 389 ] 390 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: 391 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 392 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: 393 cases (lookup ?? (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in EQ1; 394 #a #b #EQ1 >(proj2 ?? (pair_destruct ?????? EQ1)) #EQ2 >EQ2 395 %2 @refl 421 396 ] 422 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: 423 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 424 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: 425 cases (lookup ?? (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 426 #a #b #H >H normalize nodelta %2 @refl 397 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 398 #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/ 427 399 ] 428 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 429 #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/ 400 2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 401 (* USE: jump_not_in_policy (from old_sigma) *) 402 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??) 403 [1,4,7: >prf >nth_append_second 404 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 405 2,4,6: @le_n 406 ] 407 2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 408 3,6,9: 409 cases (lookup ?? (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in EQ1; 410 #a #b #EQ1 >(proj2 ?? (pair_destruct ?????? EQ1)) #EQ2 >EQ2 %2 @refl 411 ] 412 4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/ 430 413 ] 431 2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 432 lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (prefix) ??) 433 [1,4,7: >prf >nth_append_second 434 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 435 2,4,6: @le_n 436 ] 437 2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 438 3,6,9: cases (lookup ?? (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 439 #a #b #H >H normalize nodelta %2 @refl 440 ] 441 4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/ 442 ] 443 ] 444  @bitvector_of_nat_abs 445 [ @(transitive_lt … (pi2 … program)) >prf @le_S_S >append_length @le_plus_n_r 446  @(transitive_lt … (pi2 … program)) @le_S_S >prf >append_length <plus_n_Sm 447 @le_S_S @le_plus_n_r 448  @lt_to_not_eq @le_n 449 ] 450 ] 414 ] 415  @bitvector_of_nat_abs 416 [ @(transitive_lt … (pi2 … program)) >prf @le_S_S >append_length @le_plus_n_r 417  @(transitive_lt … (pi2 … program)) @le_S_S >prf >append_length <plus_n_Sm 418 @le_S_S @le_plus_n_r 419  @lt_to_not_eq @le_n 420 ] 421 ] 422 ] 423  <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit 424 normalize nodelta 425 cases (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma) 〈0,short_jump〉) 426 #a #b normalize nodelta %2 @refl 451 427 ] 452 428 ] … … 459 435 [ cases (le_to_or_lt_eq … Hi) Hi #Hi 460 436 [ >lookup_opt_insert_miss 461 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?) 437 [ (* USE: policy_compact_unsafe *) 438 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?) 462 439 [ @le_S_to_le @Hi ] 463 440 cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) … … 477 454 ] 478 455  >Hi >lookup_opt_insert_hit normalize nodelta 479 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?) 456 (* USE: policy_compact_unsafe *) 457 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?) 480 458 [ <Hi @le_n 481 459  cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) 482 460 [ normalize nodelta / by / 483 461  #x cases x x #x1 #x2 484 lapply (proj2 ?? (proj1 ?? Hpolicy)) <Hi 462 (* USE: inc_pc = fst inc_sigma *) 463 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) <Hi 485 464 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)) 486 465 cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %); … … 522 501 ] 523 502 >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta 524 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i ?)) 503 (* USE: out_of_program_none ← *) 504 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i ?)) 525 505 [ >Hi @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r 526 506  >Hi 527 lapply (proj2 ?? (proj1 ?? Hpolicy)) 507 (* USE: inc_pc = fst policy *) 508 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) 528 509 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) inc_sigma)) 529 510 cases (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) inc_sigma) in ⊢ (???% → %); … … 556 537 ] 557 538 ] 558  (* policy_safe *) cases daemon (*#i >append_length >commutative_plus #Hi normalize in Hi; 539  (* policy_safe *) cases daemon 540 (* #i >append_length >commutative_plus #Hi normalize in Hi; 559 541 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 560 542 [ >nth_append_first 561 543 [2: @Hi] 562 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi)563 544 <(proj2 ?? (pair_destruct ?????? Heq2)) 564 545 >lookup_insert_miss 565 [ 546 [ >lookup_insert_miss 547 [ >lookup_insert_miss 548 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi) 549 cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉) 550 #pc #j cases (nth i ? prefix 〈None ?, Comment []〉) #label #instr cases j 551 normalize nodelta 552 [ #H cases (le_to_or_lt_eq … Hi) Hi #Hi 553 [ >lookup_insert_miss 554 [ #dest #Hjmp <(proj1 ?? (pair_destruct ?????? Heq2)) 555 566 556  567 557 ] … … 572 562 [ cases (decidable_eq_nat 0 (prefix)) 573 563 [ #Heq <Heq >lookup_insert_hit 574 lapply (proj2 ?? (proj1 ?? Hpolicy)) 575 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) <Heq 564 (* USE: inc_pc = fst policy *) 565 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) 566 (* USE: 0 ↦ 0 *) 567 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) <Heq 576 568 #ONE #TWO >TWO >ONE @refl 577 569  #Hneq >lookup_insert_miss 578 [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))570 [ (* USE: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) 579 571  @bitvector_of_nat_abs 580 572 [3: @Hneq] … … 593 585 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 594 586 ] 595  (* added = 0 → policy_equal *) lapply (proj2 ?? Hpolicy) 587  (* added = 0 → policy_pc_equal *) 588 (* USE: added = 0 → policy_pc_equal *) 589 lapply (proj2 ?? (proj1 ?? Hpolicy)) 596 590 lapply Heq2 Heq2 lapply Heq1 Heq1 lapply (refl ? instr) 597 cases instr in ⊢ (???% → % → % → %); normalize nodelta 591 cases daemon 592 (*cases instr in ⊢ (???% → % → % → %); normalize nodelta 598 593 [ #pi cases pi normalize nodelta 599 594 [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: … … 609 604 (bitvector_of_nat 16 i)) 610 605 [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: 606 (* le_to_or_lt_eq, part 2 *) 611 607 >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc,new_length〉 16 612 608 (bitvector_of_nat 16 (prefix)) (bitvector_of_nat 16 i)) … … 617 613 [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 614 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 619 @le_S_S @le_plus_a @ le_S_to_le @(le_S_S_to_le … Hi)615 @le_S_S @le_plus_a @(le_S_S_to_le … Hi) 620 616 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 617 @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S 622 618 @le_plus_n_r 623 619 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_S_to_le … Hi)620 @lt_to_not_eq @(le_S_to_le … Hi) 625 621 ] 626 622 ] … … 807 803 ] 808 804 ] 809 ] 805 ]*) 810 806 ] 811  normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 807  (* policy_jump_equal → added = 0 *) 808 cases daemon 809 ] 810  normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 812 811 [ #i cases i 813 812 [ #Hi2 @conj … … 832 831 ] 833 832 ] 833  #i #Hi <(le_n_O_to_eq … Hi) 834 >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉) 835 #a #b normalize nodelta %2 @refl 836 ] 834 837  #i cases i 835 838 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O … … 842 845 ] 843 846 ] 844  #i cases i845 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O846  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O847 ]848 ]849 847  >lookup_insert_hit @refl 850 848 ] 851 849  >lookup_insert_hit @refl 852 850 ] 853  #_ #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 851  #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit 852 (* USE: 0 ↦ 0 (from old_sigma *) 853 @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) 854 ] 855  #_ @refl 854 856 ] 855 857 ]
Note: See TracChangeset
for help on using the changeset viewer.