Changeset 993 for src/ASM/Assembly.ma
 Timestamp:
 Jun 17, 2011, 6:28:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r989 r993 666 666 lookup ? ? pc policy long_jump. 667 667 668 definition assembly_1_pseudoinstruction ≝668 definition assembly_1_pseudoinstruction_safe ≝ 669 669 λprogram: pseudo_assembly_program. 670 670 λjump_expansion: policy_type. … … 684 684 ]. 685 685 686 definition construct_costs ≝686 definition construct_costs_safe ≝ 687 687 λprogram. 688 688 λjump_expansion: policy_type. 689 689 λpseudo_program_counter: nat. 690 690 λprogram_counter: nat. 691 λlookup_labels.692 λlookup_datalabels.693 691 λcosts: BitVectorTrie Word 16. 694 692 λi. … … 700 698 let pc_bv ≝ bitvector_of_nat ? program_counter in 701 699 let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in 700 let lookup_labels ≝ λx.pc_bv in 701 let lookup_datalabels ≝ λx.zero ? in 702 702 let pc_delta_assembled ≝ 703 assembly_1_pseudoinstruction program jump_expansion ppc_bv pc_bv703 assembly_1_pseudoinstruction_safe program jump_expansion ppc_bv pc_bv 704 704 lookup_labels lookup_datalabels i 705 705 in … … 727 727 let 〈program_counter, sigma_map〉 ≝ pc_map in 728 728 let 〈label, i〉 ≝ i in 729 match construct_costs instr_list jump_expansion ppc program_counter (λx. zero ?) (λx. zero ?)(Stub …) i with729 match construct_costs_safe instr_list jump_expansion ppc program_counter (Stub …) i with 730 730 [ None ⇒ None ? 731 731  Some pc_ignore ⇒ … … 775 775 [ None ⇒ λabs. ⊥ 776 776  Some r ⇒ λ_.r] (sig2 … policy). 777 cases abs / /777 cases abs /2/ 778 778 qed. 779 779 … … 782 782 qed. 783 783 784 (* MAIN AXIOM HERE, HIDDEN USING cases daemon *) 785 definition assembly_1_pseudoinstruction: 786 ∀program:pseudo_assembly_program.∀pol: policy program. 787 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi. 788 lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) → 789 lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) → 790 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 791 Σres:(nat × (list Byte)). 792 let 〈len,code〉 ≝ res in 793 sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) = 794 bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len) 795 ≝ λprogram: pseudo_assembly_program. 796 λpol: policy program. 797 λppc: Word. 798 λlookup_labels. 799 λlookup_datalabels. 800 λpi. 801 λprf1,prf2,prf3. 802 match assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi with 803 [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy 804  Some res ⇒ res ]. 805 [ @⊥ elim pi in p [*] 806 try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs 807 generalize in match (jmeq_to_eq ??? abs) abs; #abs whd in abs:(??%?); try destruct(abs) 808 whd in abs:(??match % with [_ ⇒ ?  _ ⇒ ?]?); 809 (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *) 810 cases daemon 811  cases res in p ⊢ %; res; #len #code #EQ normalize nodelta; 812 (* THIS SHOULD BE TRUE INSTEAD *) 813 cases daemon] 814 qed. 815 816 (* MAIN AXIOM HERE, HIDDEN USING cases daemon *) 817 definition construct_costs': 818 ∀program. policy program → nat → nat → ? → ? → 819 Σres:(nat × (BitVectorTrie Word 16)). True 820 ≝ 821 λprogram.λpol: policy program.λppc,pc,costs,i. 822 match construct_costs_safe program pol ppc pc costs i with 823 [ None ⇒ let dummy ≝ 〈0, Stub ??〉 in dummy 824  Some res ⇒ res ]. 825 [ cases daemon 826  %] 827 qed. 828 829 definition construct_costs ≝ 830 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i). 831 784 832 axiom construct_costs_sigma: 785 ∀p.∀pol:policy p.∀ppc,pc, pc',costs,costs',i.833 ∀p.∀pol:policy p.∀ppc,pc,costs,i. 786 834 bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) → 787 Some … 〈pc',costs'〉 = construct_costs p pol ppc pc (λx.zero 16) (λx.zero 16) costs i → 788 bitvector_of_nat ? pc' = sigma p pol (bitvector_of_nat 16 (S ppc)). 835 bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)). 789 836 790 837 axiom tech_pc_sigma00_append_Some: 791 ∀program.∀pol:policy program.∀prefix,costs,label,i,p c',code,ppc,pc.838 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc. 792 839 tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 → 793 construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 → 794 tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉. 795 796 axiom tech_pc_sigma00_append_None: 797 ∀program.∀pol:policy program.∀prefix,i,ppc,pc,costs. 798 tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 → 799 construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = None … 800 → False. 840 tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉. 801 841 802 842 definition build_maps: … … 806 846 ∀id. occurs_exactly_once id (\snd pseudo_program) → 807 847 lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) 808 848 ≝ 809 849 λpseudo_program.λpol:policy pseudo_program. 810 850 let result ≝ … … 815 855 let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in 816 856 let 〈pc',costs〉 ≝ pc_costs in 817 bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc') ∧ 818 ppc' = length … pre ∧ 819 tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉 ∧ 820 ∀id. occurs_exactly_once id pre → 821 lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)) 857 And ( And ( 858 And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*) 859 (ppc' = length … pre)) (*∧ *) 860 (tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*) 861 (∀id. occurs_exactly_once id pre → 862 lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id))) 822 863 (\snd pseudo_program) 823 864 (λprefix,i,tl,prf,t. … … 831 872  Some label ⇒ 832 873 let program_counter_bv ≝ bitvector_of_nat ? pc in 833 insert ? ? label program_counter_bv labels 834 ] 874 insert ? ? label program_counter_bv labels] 835 875 in 836 match construct_costs pseudo_program pol ppc pc (λx. zero ?) (λx. zero ?) costs i' with 837 [ None ⇒ 838 let dummy ≝ 〈labels,ppc_pc_costs〉 in 839 dummy 840  Some construct ⇒ 〈labels, 〈S ppc,construct〉〉 841 ] 876 let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in 877 〈labels, 〈S ppc,construct〉〉 842 878 ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉 843 879 in … … 846 882 let 〈pc, costs〉 ≝ pc_costs in 847 883 〈labels, costs〉. 848 [4: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ // 849 2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2 850 cases construct in p4 #PC #CODE #JMEQ % [% [%]] 851 [ @(construct_costs_sigma … IHn1) [4: <JMEQ % *: skip] 884 [2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2 885 generalize in match (refl … construct); cases construct in ⊢ (???% → %) #PC #CODE #JMEQ % [% [%]] 886 [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ % 852 887  >length_append <IH0 normalize; IHn1; (*CSC: otherwise it diverges!*) // 853  @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))888  >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ % 854 889  #id normalize nodelta; labels1; cases label; normalize nodelta 855 890 [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 IHn1; (*CSC: otherwise it diverges!*) // … … 860 895  #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: IHn1; /2/] 861 896 <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 IHn1; //]]] 862 3: (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2863 @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4))864  generalize in match (sig2 … result) >p normalize nodelta; >p1 normalize nodelta;865 >p2; normalize nodelta; * #_; #H @H]897 3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ // 898  generalize in match (sig2 … result) in ⊢ ?; 899 normalize nodelta in p ⊢ %; result; >p in ⊢ (match % with [_ ⇒ ?] → ?) 900 normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H] 866 901 qed. 867 902 868 definition assembly: ∀p:pseudo_assembly_program. policy p → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 869 λp,pol. 870 let 〈preamble, instr_list〉 ≝ p in 871 let 〈labels,costs〉 ≝ build_maps p pol in 903 definition assembly: 904 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie Identifier 16) ≝ 905 λp.let 〈preamble, instr_list〉 ≝ p in 906 λpol. 907 let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in 872 908 let datalabels ≝ construct_datalabels preamble in 873 909 let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in 874 910 let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in 875 let result ≝ foldr ? ? (λx. λy. 876 match y with 877 [ None ⇒ None ? 878  Some lst ⇒ 879 let 〈pc, ppc_y〉 ≝ lst in 880 let 〈ppc, y〉 ≝ ppc_y in 881 let x ≝ assembly_1_pseudoinstruction p pol ppc pc lookup_labels lookup_datalabels (\snd x) in 882 match x with 883 [ None ⇒ None ? 884  Some x ⇒ 885 let 〈pc_delta, program〉 ≝ x in 886 let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in 887 let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in 888 Some ? 〈new_pc, 〈new_ppc, (program @ y)〉〉 889 ] 890 ]) (Some ? 〈(zero ?), 〈(zero ?), [ ]〉〉) instr_list 911 let result ≝ 912 foldl_strong 913 (option Identifier × pseudo_instruction) 914 (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))). 915 let 〈pc,ppc_code〉 ≝ pc_ppc_code in 916 let 〈ppc,code〉 ≝ ppc_code in 917 ∀ppc'. 918 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in 919 let 〈len,assembledi〉 ≝ 920 assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc' lookup_labels lookup_datalabels pi ??? in 921 True) 922 instr_list 923 (λprefix,hd,tl,prf,pc_ppc_code. 924 let 〈pc, ppc_code〉 ≝ pc_ppc_code in 925 let 〈ppc, code〉 ≝ ppc_code in 926 let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc lookup_labels lookup_datalabels (\snd hd) ??? in 927 let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in 928 let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in 929 〈new_pc, 〈new_ppc, (code @ program)〉〉) 930 〈(zero ?), 〈(zero ?), [ ]〉〉 891 931 in 892 match result with 893 [ None ⇒ None ? 894  Some result ⇒ Some ? (〈\snd (\snd result), costs〉)]. 932 〈\snd (\snd result), costs〉. 933 [2,5: % 934 *: cases daemon ] 935 qed. 895 936 896 937 definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
Note: See TracChangeset
for help on using the changeset viewer.