Changeset 2059 for src/ASM/Policy.ma
- Timestamp:
- Jun 13, 2012, 3:44:20 PM (8 years ago)
- File:
-
- 1 edited
-
src/ASM/Policy.ma (modified) (24 diffs)
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.
