Changeset 1933
 Timestamp:
 May 10, 2012, 12:00:21 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r1932 r1933 509 509 ∀labels:label_map. 510 510 Σpolicy:ppc_pc_map. 511 And (out_of_program_none (pi1 ?? program) policy) 512 (jump_in_policy (pi1 ?? program) policy) ≝ 511 And (And (out_of_program_none (pi1 ?? program) policy) 512 (jump_in_policy (pi1 ?? program) policy)) 513 (policy_isize_sum (pi1 ?? program) labels policy) ≝ 513 514 λprogram.λlabels. 514 515 foldl_strong (option Identifier × pseudo_instruction) 515 (λprefix.Σpolicy:ppc_pc_map. 516 (And (out_of_program_none prefix policy) 517 (jump_in_policy prefix policy))) 516 (λprefix.Σpolicy:ppc_pc_map. 517 And (And (out_of_program_none prefix policy) 518 (jump_in_policy prefix policy)) 519 (policy_isize_sum prefix labels policy)) 518 520 program 519 521 (λprefix.λx.λtl.λprf.λp. … … 540 542 ]〉 541 543 ) 〈0, Stub ? ?〉. 542 [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;544 [ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi; 543 545 [ #Hi2 544 546 cases (le_to_or_lt_eq … Hi) Hi #Hi … … 558 560 ] 559 561 ] 560 @(proj1 ?? Hpi ? Hi2) @le_S_to_le @le_S_to_le @Hi562 @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 561 563 38,39,40,41,42,43,44,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74: 562 564 [1,2,3,6,7,24,25: #x #y … … 573 575 ] 574 576 ] 575 <Hi @(proj1 ?? Hp(S (prefix)) (le_S ?? (le_n (prefix))) ?)577 <Hi @(proj1 ?? (proj1 ?? Hp) (S (prefix)) (le_S ?? (le_n (prefix))) ?) 576 578 >Hi @Hi2 577 579 9,10,11,12,13,14,15,16,17: … … 583 585 ] 584 586 1,3,5,7,9,11,13,15,17: 585 @(proj1 ?? Hpi ? Hi2) @le_S_to_le @le_S_to_le @Hi587 @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 586 588 ] 587 589 46,47,48,49,50,51,52,53,54: … … 593 595 ] 594 596 1,3,5,7,9,11,13,15,17: 595 @(proj1 ?? Hpi ? Hi2) <Hi @le_S @le_n597 @(proj1 ?? (proj1 ?? Hp) i ? Hi2) <Hi @le_S @le_n 596 598 ] 597 599 ] … … 605 607 ] 606 608 ] 607 [1,3,4: @(proj1 ?? Hpi ? Hi2) @le_S_to_le @le_S_to_le @Hi609 [1,3,4: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 608 610 2,5,6: 609 <Hi @(proj1 ?? Hp(S (prefix)) (le_S ?? (le_n (prefix))) ?)611 <Hi @(proj1 ?? (proj1 ?? Hp) (S (prefix)) (le_S ?? (le_n (prefix))) ?) 610 612 >Hi @Hi2 611 613 ] … … 618 620 9,12: @sym_neq @lt_to_not_eq <Hi @le_n 619 621 ] 620 1,3: @(proj1 ?? Hpi ? Hi2) @le_S_to_le @le_S_to_le @Hi621 5,7: @(proj1 ?? Hpi ? Hi2) <Hi @le_S @le_n622 1,3: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 623 5,7: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) <Hi @le_S @le_n 622 624 ] 623 625 ] … … 691 693 ] 692 694 ] 693 @(proj1 ?? (proj2 ?? Hpi (le_S_S_to_le … Hi)) Hj)694  #H @(proj2 ?? (proj2 ?? (p i2 ?? p) i (le_S_S_to_le … Hi)))695 @(proj1 ?? (proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi)) Hj) 696  #H @(proj2 ?? (proj2 ?? (proj1 ?? (pi2 ?? p)) i (le_S_S_to_le … Hi))) 695 697 cases p in H; p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta 696 698 [1: #id cases id … … 781 783 ] 782 784 2,3,6: #x [3: #id] @conj 783 [1,3,5: #H @⊥ @H785 [1,3,5: #H cases H 784 786 2,4,6: 785 787 cases p p #p cases p p #pc #pol #Hp #H elim H H #p 786 788 normalize nodelta >lookup_insert_hit #H destruct (H) 787 (* [1,3,5: #_ #H destruct (H)788 2,4,6: @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm789 @le_S_S_to_le @le_plus_n_r790 ] *)791 789 ] 792 790 4,5: #x @conj … … 798 796 ] 799 797 ] 798  cases daemon 799 ] 800 800  @conj 801 [ #i #_ #Hi2 / by refl/ 802  #i #_ @conj 803 [ >nth_nil #H @⊥ @H 804  #H elim H H #p >lookup_stub #H destruct (H) 805 ] 801 [ @conj 802 [#i #_ #Hi2 / by refl/ 803  #i #_ @conj 804 [ >nth_nil #H @⊥ @H 805  #H elim H H #p >lookup_stub #H destruct (H) 806 ] 807 ] 808  whd in match policy_isize_sum; normalize nodelta 809 cases daemon 806 810 ] 807 811 ] … … 889 893 ] in 890 894 let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in 891 let 〈old_pc, old_length〉 ≝ bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,None ?〉 in 892 match add_instr with 893 [ None ⇒ 894 let isize ≝ instruction_size_jmplen short_jump instr in 895 (* instruction is not a jump: nothing changes *) 896 〈inc_added, 〈plus inc_pc isize, bvt_insert … (bitvector_of_nat 16 (prefix)) 〈inc_pc, None ?〉 inc_sigma〉〉 897  Some proj_length ⇒ 898 let x ≝ match old_length with 899 [ None ⇒ (* this should not happen! *) short_jump 900  Some y ⇒ y 901 ] in 902 let new_length ≝ max_length x proj_length in 903 let old_size ≝ instruction_size_jmplen x instr in 904 let isize ≝ instruction_size_jmplen new_length instr in 905 〈plus inc_added (minus isize old_size), 〈plus inc_pc isize, 906 bvt_insert … (bitvector_of_nat 16 (prefix)) 〈inc_pc, Some ? new_length〉 inc_sigma〉〉 907 ] 895 let 〈old_pc, ol〉 ≝ bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,None ?〉 in 896 let old_length ≝ match ol with 897 [ None ⇒ short_jump 898  Some x ⇒ x 899 ] in 900 let old_size ≝ instruction_size_jmplen old_length instr in 901 let 〈new_length, isize〉 ≝ match add_instr with 902 [ None ⇒ 〈None ?, instruction_size_jmplen short_jump instr〉 903  Some pl ⇒ 〈Some ? (max_length old_length pl), instruction_size_jmplen (max_length old_length pl) instr〉 904 ] in 905 let new_added ≝ match add_instr with 906 [ None ⇒ inc_added 907  Some x ⇒ plus inc_added (minus isize old_size) 908 ] in 909 〈new_added, 〈plus inc_pc isize, bvt_insert … (bitvector_of_nat ? (prefix)) 〈inc_pc, new_length〉 inc_sigma〉〉 908 910 ) 〈0, 〈0, Stub ??〉〉 in 909 911 if geb (\fst final_policy) 2^16 then … … 920 922  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1 921 923 ] 922  (* XXX complicated proof *) cases daemon 924  lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma 925 cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,None ?〉) 926 #old_pc #old_length normalize nodelta 927 (* XXX complicated proof *) cases daemon 923 928  normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj 924 929 [ #i #Hi / by refl/ … … 1354 1359 (jump_in_policy program x)) 1355 1360 (policy_isize_sum program (create_label_map program) x)) 1356 1357 1361 (\fst x < 2^16) 1358 1362 ]) ≝ … … 1369 1373 ]. 1370 1374 [ normalize nodelta @conj 1371 [ @conj 1372 [ @(pi2 ?? (jump_expansion_start program (create_label_map program))) 1373  (* XXX *) cases daemon 1374 ] 1375 [ @(pi2 ?? (jump_expansion_start program (create_label_map program))) 1375 1376  (* XXX *) cases daemon 1376 1377 ]
Note: See TracChangeset
for help on using the changeset viewer.