Changeset 998 for src/ASM/Assembly.ma
 Timestamp:
 Jun 20, 2011, 5:05:23 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r993 r998 591 591 ]. 592 592 593 definition expand_pseudo_instruction : ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝593 definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝ 594 594 λlookup_labels. 595 595 λlookup_datalabels. … … 675 675 λi. 676 676 let expansion ≝ jump_expansion ppc in 677 match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with677 match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with 678 678 [ None ⇒ None ? 679 679  Some pseudos ⇒ … … 715 715 program counters. It is at the heart of the proof. *) 716 716 (*CSC: code taken from build_maps *) 717 definition sigma00: pseudo_assembly_program → policy_type → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝717 definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝ 718 718 λinstr_list. 719 719 λjump_expansion: policy_type. 720 720 λl:list labelled_instruction. 721 λacc. 721 722 foldl ?? 722 723 (λt,i. … … 732 733 let 〈pc,ignore〉 ≝ pc_ignore in 733 734 Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ] 734 ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉)l.735 ]) acc l. 735 736 736 737 definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16))) 737 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) .738 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, (Stub ? ?)〉〉). 738 739 739 740 definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝ 740 741 λprogram,jump_expansion,instr_list. 741 match sigma00 program jump_expansion instr_list with742 match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with 742 743 [ None ⇒ None … 743 744  Some result ⇒ … … 782 783 qed. 783 784 785 definition expand_pseudo_instruction: 786 ∀program:pseudo_assembly_program.∀pol: policy program. 787 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc,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 pc = sigma program pol ppc → 792 Σres:list instruction. Some … res = expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi 793 ≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,pi,prf1,prf2,prf3,prf4. 794 match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi with 795 [ None ⇒ let dummy ≝ [ ] in dummy 796  Some res ⇒ res ]. 797 [ cases daemon 798  >p %] 799 qed. 800 784 801 (* MAIN AXIOM HERE, HIDDEN USING cases daemon *) 785 definition assembly_1_pseudoinstruction :802 definition assembly_1_pseudoinstruction': 786 803 ∀program:pseudo_assembly_program.∀pol: policy program. 787 804 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi. … … 790 807 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 791 808 Σres:(nat × (list Byte)). 809 Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧ 792 810 let 〈len,code〉 ≝ res in 793 811 sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) = … … 809 827 (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *) 810 828 cases daemon 811  cases res in p ⊢ %; res; #len #code #EQ normalize nodelta; 829  % [ >p %] 830 cases res in p ⊢ %; res; #len #code #EQ normalize nodelta; 812 831 (* THIS SHOULD BE TRUE INSTEAD *) 813 832 cases daemon] 814 833 qed. 815 834 835 definition assembly_1_pseudoinstruction: 836 ∀program:pseudo_assembly_program.∀pol: policy program. 837 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi. 838 lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) → 839 lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) → 840 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 841 nat × (list Byte) 842 ≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3. 843 assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 844 prf2 prf3. 845 846 lemma assembly_1_pseudoinstruction_ok1: 847 ∀program:pseudo_assembly_program.∀pol: policy program. 848 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi. 849 ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)). 850 ∀prf2:lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)). 851 ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi. 852 Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3) 853 = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi. 854 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3 855 cases (sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)) 856 #H1 #_ @H1 857 qed. 858 816 859 (* MAIN AXIOM HERE, HIDDEN USING cases daemon *) 817 860 definition construct_costs': 818 ∀program. policy program → nat → nat → ? → ? →819 Σres:(nat × (BitVectorTrie Word 16)). True861 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i. 862 Σres:(nat × (BitVectorTrie Word 16)). Some … res = construct_costs_safe program pol ppc pc costs i 820 863 ≝ 821 864 λprogram.λpol: policy program.λppc,pc,costs,i. … … 824 867  Some res ⇒ res ]. 825 868 [ cases daemon 826  %]869  >p %] 827 870 qed. 828 871 829 872 definition construct_costs ≝ 830 873 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i). 874 875 (* 876 axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A. 877 axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l. 878 879 let rec foldl_strong_internal 880 (A: Type[0]) (P: list A → Type[0]) (l: list A) (suffix2: list A) 881 (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl @suffix2 → P prefix → P (prefix @ [hd])) 882 (prefix: list A) (suffix: list A) (acc: P prefix) on suffix: 883 l = prefix @ suffix @ suffix2 → P(prefix @ suffix) ≝ 884 match suffix return λl'. l = prefix @ l' @ suffix2 → P (prefix @ l') with 885 [ nil ⇒ λprf. ? 886  cons hd tl ⇒ λprf. ? 887 ]. 888 [ > (append_nil ?) 889 @ acc 890  applyS (foldl_strong_internal A P l suffix2 H (prefix @ [hd]) tl ? ?) 891 [ @(H prefix hd tl prf acc) 892  >prf /2/]] 893 qed. 894 895 definition foldl_strong ≝ 896 λA: Type[0]. 897 λP: list A → Type[0]. 898 λl: list A. 899 λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]). 900 λacc: P [ ]. 901 foldl_strong_internal A P l [ ] ? [ ] l acc ?. 902 [ #prefix #hd #tl >append_nil @H 903  >append_nil % ] 904 qed. 905 906 axiom foldl_strong_step: 907 ∀A:Type[0]. 908 ∀P: list A → Type[0]. 909 ∀l: list A. 910 ∀H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]). 911 ∀acc: P [ ]. 912 ∀Q: ∀prefix. P prefix → Prop. 913 ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl. 914 ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc). 915 Q [ ] acc → 916 Q l (foldl_strong A P l H acc). 917 (* 918 #A #P #l #H #acc #Q #HQ #Hacc normalize; 919 generalize in match 920 (foldl_strong ? 921 (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?)) 922 l ? Hacc) 923 [3: >suffix_of_ok %  2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ] 924 [2: #prefix #hd #tl #prf #X whd in ⊢ (??%) 925 #K 926 927 generalize in match 928 (foldl_strong ? 929 (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre)))) 930 [2: @H 931 *) 932 933 axiom foldl_elim: 934 ∀A:Type[0]. 935 ∀B: Type[0]. 936 ∀H: A → B → A. 937 ∀acc: A. 938 ∀l: list B. 939 ∀Q: A → Prop. 940 (∀acc:A.∀b:B. Q acc → Q (H acc b)) → 941 Q acc → 942 Q (foldl A B H acc l). 943 *) 944 945 lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b. 946 #A #a #b #EQ destruct // 947 qed. 948 949 lemma sigma00_strict: 950 ∀instr_list,jump_expansion,l,acc. acc = None ? → 951 sigma00 instr_list jump_expansion l acc = None …. 952 #instr_list #jump_expansion #l elim l 953 [ #acc #H >H % 954  #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ] 955 qed. 956 957 lemma sigma00_append: 958 ∀instr_list,jump_expansion,l1,l2,acc. 959 sigma00 instr_list jump_expansion (l1@l2) acc = 960 sigma00 instr_list jump_expansion 961 l2 (sigma00 instr_list jump_expansion l1 acc). 962 whd in match sigma00; normalize nodelta; 963 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append 964 qed. 965 966 lemma policy_ok_prefix_ok: 967 ∀program.∀pol:policy program.∀suffix,prefix. 968 prefix@suffix = \snd program → 969 sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None …. 970 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%); 971 generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol 972 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0 973 normalize nodelta >sigma00_append 974 cases (sigma00 ?? prefix ?) 975 [2: #x #_ % #abs destruct(abs) 976  * #abs @⊥ @abs >sigma00_strict % ] 977 qed. 978 979 lemma policy_ok_prefix_hd_ok: 980 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map. 981 (prefix@[hd])@suffix = \snd program → 982 Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) → 983 let 〈ppc,pc_map〉 ≝ ppc_pc_map in 984 let 〈program_counter, sigma_map〉 ≝ pc_map in 985 let 〈label, i〉 ≝ hd in 986 construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None …. 987 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2 988 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix 989 (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?) 990 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta 991 @pair_elim' #pc #map #EQ4 normalize nodelta 992 @pair_elim' #l' #i' #EQ5 normalize nodelta 993 cases (construct_costs_safe ??????) normalize 994 [* #abs @⊥ @abs %  #X #_ % #abs destruct(abs)] 995 qed. 996 997 (* 998 lemma tech_pc_sigma00_append_Some: 999 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc. 1000 tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 → 1001 tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉. 1002 #program #pol #prefix #costs #label #i #ppc #pc #H 1003 whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta; 1004 whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %; 1005 generalize in match (sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?) 1006 whd in match sigma0; normalize nodelta; 1007 >foldl_step 1008 change with (? → match match sigma00 program pol prefix with [None ⇒ ?  Some res ⇒ ?] with [ None ⇒ ?  Some res ⇒ ? ] = ?) 1009 whd in match tech_pc_sigma00 in H; normalize nodelta in H; 1010 cases (sigma00 program pol prefix) in H ⊢ % 1011 [ whd in ⊢ (??%% → ?) #abs destruct(abs) 1012  * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H) 1013 1014 normalize nodelta; H; 1015 1016 1017 generalize in match H; H; 1018 generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ?  _ ⇒ ?] with [_ ⇒ ?  _ ⇒ ?]?) 1019 [2: whd in ⊢ (??%%) 1020 XXX 1021 *) 831 1022 832 1023 axiom construct_costs_sigma:
Note: See TracChangeset
for help on using the changeset viewer.