Changeset 2141 for src/ASM/Policy.ma
 Timestamp:
 Jun 28, 2012, 8:08:58 PM (8 years ago)
 File:

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