Changeset 1870
 Timestamp:
 Apr 3, 2012, 2:52:10 PM (9 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r1646 r1870 161 161 definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝ 162 162 λn,v. nat_of_bitvector_aux n O v. 163 163 164 lemma bitvector_of_nat_ok: 165 ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y. 166 #n elim n n 167 [ #x #y #Hx #Hy #Heq <(le_n_O_to_eq ? (le_S_S_to_le ?? Hx)) <(le_n_O_to_eq ? (le_S_S_to_le ?? Hy)) @refl 168  #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *) 169 ] 170 qed. 171 172 lemma bitvector_of_nat_abs: 173 ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y). 174 #n #x #y #Hx #Hy #Heq @notb_elim 175 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y))) 176 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %); 177 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/ 178  #H / by I/ 179 ] 180 qed. 181 164 182 definition two_complement_negation ≝ 165 183 λn: nat. 
src/ASM/Assembly.ma
r1668 r1870 635 635 let lookup_datalabels ≝ λx.zero ? in 636 636 let pc_delta_assembled ≝ 637 assembly_1_pseudoinstruction (λx. bitvector_of_nat ? program_counter)637 assembly_1_pseudoinstruction (λx.pc_bv) 638 638 jump_expansion (*ppc_bv*) pc_bv lookup_datalabels i in 639 639 let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in 640 640 〈pc_delta + program_counter, costs〉 641 641 ]. 642 643 axiom nat_of_bitvector_bitvector_of_nat: 644 ∀n,v.n < 2^v → nat_of_bitvector v (bitvector_of_nat v n) = n. 645 646 axiom bitvector_of_nat_nat_of_bitvector: 647 ∀n,v.bitvector_of_nat n (nat_of_bitvector n v) = v. 648 649 lemma nth_cons: 650 ∀n,A,h,t,y. 651 nth (S n) A (h::t) y = nth n A t y. 652 #n #A #h #t #y /2 by refl/ 653 qed. 654 655 lemma fetch_pseudo_instruction_prefix: 656 ∀prefix.∀x.∀ppc.ppc < (prefix) → 657 fetch_pseudo_instruction prefix (bitvector_of_nat ? ppc) = 658 fetch_pseudo_instruction (prefix@x) (bitvector_of_nat ? ppc). 659 #prefix #x #ppc elim prefix 660 [ #Hppc @⊥ @(absurd … Hppc) @le_to_not_lt @le_O_n 661  #h #t #Hind #Hppc whd in match (fetch_pseudo_instruction ??); 662 whd in match (fetch_pseudo_instruction ((h::t)@x) ?); 663 >nth_append_first 664 [ // 665  >nat_of_bitvector_bitvector_of_nat 666 [ @Hppc 667  cases daemon (* XXX invariant *) 668 ] 669 ] 670 ] 671 qed. 642 672 643 673 (* This establishes the correspondence between pseudo program counters and 644 674 program counters. It is at the heart of the proof. *) 645 675 (*CSC: code taken from build_maps *) 646 (*JPB: Here it gets strange because we need a program counter for the jump 647 *expansion, but we can't give it to the type because we don't have it yet. Argh. 648 *add a forall type?*) 649 definition sigma00: policy_type2 → list ? → ? → (nat × (nat × (BitVectorTrie Word 16))) ≝ 676 definition sigma00: ∀jump_expansion:policy_type2.∀l:list labelled_instruction.? → 677 (Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)). 678 let 〈ppc,pc_map〉 ≝ ppc_pc_map in 679 let 〈program_counter, sigma_map〉 ≝ pc_map in 680 ppc = l ∧ 681 (ppc = l → 682 (bvt_lookup ?? (bitvector_of_nat ? ppc) sigma_map (zero ?) = (bitvector_of_nat ? program_counter)) ∧ 683 (∀x.x < l → 684 ∀pi.\fst (fetch_pseudo_instruction l (bitvector_of_nat ? x)) = pi → 685 let pc_x ≝ bvt_lookup ?? (bitvector_of_nat 16 x) sigma_map (zero ?) in 686 bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) = 687 bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) + 688 (\fst 689 (assembly_1_pseudoinstruction (λx.pc_x) (jump_expansion (λx.pc_x)) pc_x (λx.zero ?) pi))))) 690 ) ≝ 650 691 λjump_expansion: policy_type2. 651 692 λl:list labelled_instruction. 652 693 λacc. 653 foldl … 654 (λppc_pc_map,i. 694 foldl_strong ? 695 (λprefix.(Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)). 696 let 〈ppc,pc_map〉 ≝ ppc_pc_map in 697 let 〈program_counter, sigma_map〉 ≝ pc_map in 698 (ppc = prefix) ∧ 699 (ppc = prefix → 700 (bvt_lookup ?? (bitvector_of_nat ? ppc) sigma_map (zero ?) = (bitvector_of_nat ? program_counter)) ∧ 701 (∀x.x < prefix → 702 ∀pi.\fst (fetch_pseudo_instruction l (bitvector_of_nat ? x)) = pi → 703 let pc_x ≝ bvt_lookup ?? (bitvector_of_nat 16 x) sigma_map (zero ?) in 704 bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) = 705 bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) + 706 (\fst (assembly_1_pseudoinstruction (λx.pc_x) (jump_expansion (λx.pc_x)) pc_x (λx.zero ?) pi)))))) 707 ) 708 l 709 (λhd.λi.λtl.λp.λppc_pc_map. 655 710 let 〈ppc,pc_map〉 ≝ ppc_pc_map in 656 711 let 〈program_counter, sigma_map〉 ≝ pc_map in 657 712 let 〈label, i〉 ≝ i in 658 713 let 〈pc,ignore〉 ≝ construct_costs program_counter (jump_expansion (λx.bitvector_of_nat ? program_counter)) ppc (Stub …) i in 659 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 ppc) (bitvector_of_nat 16 pc) sigma_map〉〉 660 ) acc l. 714 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 (S ppc)) (bitvector_of_nat 16 pc) sigma_map〉〉 715 ) acc. 716 cases i in p; #label #ins #p @pair_elim #new_ppc #x normalize nodelta cases x x #old_pc #old_map 717 @pair_elim #new_pc #ignore #Hc #Heq normalize nodelta @conj 718 [ lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind 719 <(pair_eq1 ?????? Heq) >(proj1 ?? Hind) >append_length <commutative_plus normalize @refl 720  #Hnew <(pair_eq2 ?????? (pair_eq2 ?????? Heq)) <(pair_eq1 ?????? Heq) @conj 721 [ >lookup_insert_hit >(pair_eq1 ?????? (pair_eq2 ?????? Heq)) @refl 722  #x <(pair_eq1 ?????? Heq) >append_length <commutative_plus #Hx normalize in Hx; 723 #pi #Hpi <(pair_eq2 ?????? (pair_eq2 ?????? Heq)) <(pair_eq1 ?????? Heq) in Hnew; 724 >append_length <commutative_plus #Hnew normalize in Hnew; >(injective_S … Hnew) 725 elim (le_to_or_lt_eq … Hx) Hx #Hx 726 [ lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind 727 lapply (proj2 ?? ((proj2 ?? Hind) (proj1 ?? Hind)) x (le_S_S_to_le … Hx) pi Hpi) 728 Hind #Hind >lookup_insert_miss 729 [2: @bitvector_of_nat_abs 730 [3: @lt_to_not_eq @Hx 731 1: @(transitive_le … Hx) 732 ] 733 cases daemon (* XXX invariant *) 734 ] 735 >lookup_insert_miss 736 [2: @bitvector_of_nat_abs 737 [3: @lt_to_not_eq @(transitive_le … (le_S_S_to_le … Hx)) @le_S @le_n 738 1: @(transitive_le … (le_S_S_to_le … Hx)) 739 ] 740 cases daemon (* XXX invariant *) 741 ] 742 @Hind 743  lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta 744 #Hind lapply (proj1 ?? ((proj2 ?? Hind) (proj1 ?? Hind))) Hind 745 >(injective_S … Hnew) #Hind <(injective_S … Hx) >lookup_insert_hit >lookup_insert_miss 746 [2: @bitvector_of_nat_abs 747 [3: @lt_to_not_eq @le_n 748 1: @(transitive_le ??? (le_n (S x))) 749 ] 750 cases daemon (* XXX invariant *) 751 ] 752 >p in Hpi; whd in match (fetch_pseudo_instruction ??); >nth_append_second 753 >nat_of_bitvector_bitvector_of_nat >(injective_S … Hx) 754 [3: @le_n] 755 [2,3: cases daemon (* XXX invariant *)] 756 <minus_n_n cases (half_add ???) #x #y normalize nodelta x y #Heq <Heq 757 whd in match (construct_costs ?????) in Hc; whd in match (assembly_1_pseudoinstruction ?????); 758 cases ins in p Hc; normalize nodelta 759 [1,2,4,5: #x #p >Hind #H <(pair_eq1 ?????? H) >commutative_plus >nat_of_bitvector_bitvector_of_nat 760 [1,3,5,7: @refl 761 2,4,6,8: cases daemon (* XXX invariant *) 762 ] 763 3: #c #p >Hind #H <(pair_eq1 ?????? H) >nat_of_bitvector_bitvector_of_nat 764 [2: cases daemon (* XXX invariant *) ] 765 whd in match (expand_pseudo_instruction ?????); normalize <plus_n_O @refl 766 6: #x #y #p >Hind #H <(pair_eq1 ?????? H) >commutative_plus >nat_of_bitvector_bitvector_of_nat 767 [ @refl 768  cases daemon (* XXX invariant *) 769 ] 770 ] 771 ] 772 ] 773 ] 774 qed. 661 775 662 776 definition sigma0: pseudo_assembly_program → policy_type2 → (nat × (nat × (BitVectorTrie Word 16))) ≝ 663 777 λprog. 664 778 λjump_expansion. 665 sigma00 jump_expansion (\snd prog) 〈0, 〈0, Stub …〉〉. 779 sigma00 jump_expansion (\snd prog) 780 〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub …))〉〉. 781 normalize nodelta @conj 782 [ / by refl/ 783  #H @conj 784 [ >lookup_insert_hit @refl 785  #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n 786 ] 787 ] 788 qed. 666 789 667 790 definition tech_pc_sigma00: pseudo_assembly_program → policy_type2 → 668 791 list labelled_instruction → (nat × nat) ≝ 669 792 λprogram,jump_expansion,instr_list. 670 let 〈ppc,pc_sigma_map〉 ≝ sigma00 jump_expansion instr_list 〈0, 〈0, (Stub ? ?)〉〉 in (* acc copied from sigma0 *) 793 let 〈ppc,pc_sigma_map〉 ≝ sigma00 jump_expansion instr_list 794 〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub ? ?))〉〉 in 795 (* acc copied from sigma0 *) 671 796 let 〈pc,map〉 ≝ pc_sigma_map in 672 797 〈ppc,pc〉. 798 normalize nodelta @conj 799 [ / by refl/ 800  #H @conj 801 [ >lookup_insert_hit @refl 802  #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n 803 ] 804 ] 805 qed. 673 806 674 807 definition sigma_safe: pseudo_assembly_program → policy_type2 → … … 699 832 [ None ⇒ λabs. ⊥ 700 833  Some r ⇒ λ_.r] (pi2 … policy). 701 cases abs /2 /834 cases abs /2 by / 702 835 qed. 703 836 704 837 (*CSC: Main axiom here, needs to be proved soon! *) 705 axiomsnd_assembly_1_pseudoinstruction_ok:838 lemma snd_assembly_1_pseudoinstruction_ok: 706 839 ∀program:pseudo_assembly_program.∀pol: policy program. 707 840 ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels. … … 712 845 sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) = 713 846 bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len). 714 847 #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl 848 whd in match (sigma ???); whd in match (sigma_safe ??); normalize nodelta 849 lapply (pi2 ?? ( 850 sigma00 pol (\snd program) 851 〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub …))〉〉)) 852 normalize nodelta 853 [ @conj 854 [ / by refl/ 855  #H >lookup_insert_hit @conj 856 [ @refl 857  #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n 858 ] 859 ] 860  861 862 whd in match (sigma0 program pol); 863 (* here we go *) 864 cases daemon 865 qed. 866 715 867 example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0. 716 868 cases daemon. … … 722 874 (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list. 723 875 724 lemma sigma00_append: 725 ∀jump_expansion,l1,l2,acc. 876 (*lemma sigma00_append: 877 ∀jump_expansion,l1,l2. 878 ∀acc:ℕ×ℕ×(BitVectorTrie Word 16). 726 879 sigma00 jump_expansion (l1@l2) acc = 727 sigma00 jump_expansion 728 l2 (sigma00 jump_expansion l1 acc). 729 whd in match sigma00; normalize nodelta; 730 #jump_expansion #l1 #l2 #acc @foldl_append 731 qed. 880 sigma00 jump_expansion 881 l2 (pi1 ?? (sigma00 jump_expansion l1 acc)).*) 732 882 733 883 (* lemma sigma00_strict:
Note: See TracChangeset
for help on using the changeset viewer.