Changeset 2059 for src/ASM/Policy.ma
 Timestamp:
 Jun 13, 2012, 3:44:20 PM (8 years ago)
 File:

 1 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))
Note: See TracChangeset
for help on using the changeset viewer.