Changeset 3098 for src/ASM/PolicyFront.ma
 Timestamp:
 Apr 6, 2013, 11:44:00 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r3078 r3098 409 409 ] ≝ 410 410 λprogram.λlabels. 411 let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction) 412 (λprefix.Σpolicy:ppc_pc_map.And (And (And (And 411 let 〈ignore,final_policy〉 ≝ foldl_strong (option Identifier × pseudo_instruction) 412 (λprefix.Σacc_policy:Word × ppc_pc_map. 413 let 〈acc,policy〉 ≝ acc_policy in 414 And (acc = bitvector_of_nat … (prefix)) 415 (And (And (And (And 413 416 (not_jump_default prefix policy) 414 417 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) … … 416 419 (sigma_compact_unsafe prefix labels policy)) 417 420 (∀i.i ≤ prefix → ∃pc. 418 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉)) 421 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉))) 419 422 program 420 (λprefix.λx.λtl.λprf.λp. 421 let 〈pc,sigma〉 ≝ pi1 ?? p in 423 (λprefix.λx.λtl.λprf.λacc_pol. 424 let 〈acc,p〉 ≝ pi1 ?? acc_pol in 425 let 〈pc,sigma〉 ≝ p in 422 426 let 〈label,instr〉 ≝ x in 423 427 let isize ≝ instruction_size_jmplen short_jump instr in 424 〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (prefix))) 〈pc+isize,short_jump〉 sigma〉 425 ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in 426 if gtb (\fst (pi1 ?? final_policy)) 2^16 then 428 let Sacc ≝ increment … acc in 429 〈Sacc,〈pc + isize, bvt_insert … Sacc 〈pc+isize,short_jump〉 sigma〉〉 430 ) 〈zero ?,〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉〉 in 431 if gtb (\fst final_policy) 2^16 then 427 432 None ? 428 433 else 429 Some ? (pi1 ?? final_policy).434 Some ? final_policy. 430 435 [ / by I/ 431  lapply p p cases final_policy final_policy #p #Hp #hg 432 @conj [ @Hp  @not_lt_to_le @ltb_false_to_not_lt @hg ] 433  @conj [ @conj [ @conj [ @conj 434 [ (* not_jump_default *) cases p p #p cases p p #pc #sigma #Hp 435 cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi 436  cases (foldl_strong ?(λprefix.Σx.?)???) in p; #pi1 #IS #EQp1 >EQp1 in IS; * 437 #_ #X % try assumption @not_lt_to_le @ltb_false_to_not_lt @p1 438  cases p in p1; p #pc #sigma #p1 lapply (pi2 ?? acc_pol) >p1 acc_pol 439 normalize nodelta * #EQacc #Hp cases x in prf; #lbl #ins #prf normalize nodelta 440 % [ >EQacc >increment_zero_bitvector_of_nat_1 <add_bitvector_of_nat 441 >length_append >commutative_plus % 442  @conj [ @conj [ @conj [ @conj 443 [ (* not_jump_default *) #i >append_length <commutative_plus #Hi 436 444 normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 437 445 [ >lookup_insert_miss … … 442 450  @Hi 443 451 ] 444  @bitvector_of_nat_abs 452  >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 453 @bitvector_of_nat_abs 445 454 [ @(transitive_lt ??? Hi) @le_S_to_le] 446 455 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length … … 453 462 elim ((proj2 ?? Hp) (prefix) (le_n (prefix))) #pc #Hl 454 463 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) @refl 455  @bitvector_of_nat_abs 464  >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 465 @bitvector_of_nat_abs 456 466 [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length @le_plus_n_r 457 467  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm @le_S_S … … 462 472 ] 463 473  (* 0 ↦ 0 *) 464 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta465 474 >lookup_insert_miss 466 475 [ (* USE[pass]: 0 ↦ 0 *) 467 476 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) 468  @bitvector_of_nat_abs 477  >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 478 @bitvector_of_nat_abs 469 479 [ @ltb_true_to_lt / by refl/ 470 480  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S <plus_n_Sm … … 475 485 ] 476 486  (* fst p = pc *) 477 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 478 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 487 >append_length >(commutative_plus (prefix)) 488 >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 489 >lookup_insert_hit @refl 490 479 491 ] 480 492  (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi; 481 cases p p #p cases p p #fpc #sigma #Hp cases x #lbl #instr normalize nodelta482 493 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 483 494 [ >lookup_opt_insert_miss … … 501 512 ] 502 513 [2: lapply (le_S_to_le … Hi) Hi #Hi] 514 >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 503 515 @bitvector_of_nat_abs 504 516 [1,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <commutative_plus … … 509 521 ] 510 522  >lookup_opt_insert_miss 511 [ >Hi >lookup_opt_insert_hit normalize nodelta 523 [ >Hi 524 >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 525 >lookup_opt_insert_hit normalize nodelta 512 526 (* USE: everything is short, fst p = pc *) 513 527 elim ((proj2 ?? Hp) (prefix) (le_n ?)) #pc #Hl … … 517 531  @le_n 518 532 ] 519  @bitvector_of_nat_abs 533  >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 534 @bitvector_of_nat_abs 520 535 [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >Hi >prf @le_S_S >append_length <commutative_plus 521 536 @le_plus_a @le_n … … 528 543 ] 529 544  (* everything is short *) #i >append_length <commutative_plus #Hi normalize in Hi; 530 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta531 545 cases (le_to_or_lt_eq … Hi) Hi #Hi 532 546 [ >lookup_opt_insert_miss 533 547 [ (* USE[pass]: everything is short *) 534 548 @((proj2 ?? Hp) i (le_S_S_to_le … Hi)) 535  @bitvector_of_nat_abs 549  550 >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 551 @bitvector_of_nat_abs 536 552 [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 537 553 >commutative_plus @le_plus_a @le_S_S_to_le @Hi … … 541 557 ] 542 558 ] 543  >Hi >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump instr)) 559  >Hi 560 >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 561 >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump ins)) 544 562 @refl 545 563 ] 546 ] 547  @conj[ @conj [ @conj [ @conj564 ]] 565  normalize nodelta % % [ @conj [ @conj [ @conj 548 566 [ #i cases i 549 567 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
Note: See TracChangeset
for help on using the changeset viewer.