Changeset 985 for src/ASM/Assembly.ma
 Timestamp:
 Jun 16, 2011, 4:50:23 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r982 r985 4 4 include "ASM/Fetch.ma". 5 5 include "ASM/Status.ma". 6 include "ASM/FoldStuff.ma".7 6 8 7 definition assembly_preinstruction ≝ … … 680 679 ]. 681 680 682 definition construct_datalabels ≝683 λpreamble.684 \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (685 λt. λpreamble.686 let 〈datalabels, addr〉 ≝ t in687 let 〈name, size〉 ≝ preamble in688 let addr_16 ≝ bitvector_of_nat 16 addr in689 〈insert ? ? name addr_16 datalabels, addr + size〉)690 〈(Stub ? ?), 0〉 preamble).691 692 681 definition construct_costs ≝ 693 682 λprogram. … … 717 706 ]. 718 707 719 definition build_maps ≝ 720 λinstr_list. 721 let result ≝ foldl (option ((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16))))) ? 722 (λt. λi. 723 let 〈label, i〉 ≝ i in 708 (* This establishes the correspondence between pseudo program counters and 709 program counters. It is at the heart of the proof. *) 710 (*CSC: code taken from build_maps *) 711 definition sigma00: pseudo_assembly_program → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝ 712 λinstr_list.λl:list labelled_instruction. 713 foldl ?? 714 (λt,i. 724 715 match t with 725 716 [ None ⇒ None ? 726  Some t ⇒ 727 let 〈labels, pc_ppc_costs〉 ≝ t in 728 let 〈program_counter, ppc_costs〉 ≝ pc_ppc_costs in 729 let 〈pseudo_program_counter, costs〉 ≝ ppc_costs in 730 let labels ≝ 731 match label with 732 [ None ⇒ labels 733  Some label ⇒ 734 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 735 insert ? ? label program_counter_bv labels 736 ] 737 in 738 match construct_costs instr_list pseudo_program_counter program_counter (λx. zero ?) (λx. zero ?) costs i with 717  Some ppc_pc_map ⇒ 718 let 〈ppc,pc_map〉 ≝ ppc_pc_map in 719 let 〈program_counter, sigma_map〉 ≝ pc_map in 720 let 〈label, i〉 ≝ i in 721 match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with 739 722 [ None ⇒ None ? 740  Some construct ⇒ Some ? 〈labels, 〈pseudo_program_counter + 1, construct〉〉 741 ] 742 ]) (Some ? 〈(Stub ? ?), 〈0, 〈0, (Stub ? ?)〉〉〉) (\snd instr_list) in 743 match result with 723  Some pc_ignore ⇒ 724 let 〈pc,ignore〉 ≝ pc_ignore in 725 Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ] 726 ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l. 727 728 definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16))) 729 ≝ λprog.sigma00 prog (\snd prog). 730 731 definition tech_pc_sigma00: pseudo_assembly_program → list labelled_instruction → option (nat × nat) ≝ 732 λprogram,instr_list. 733 match sigma00 program instr_list with 734 [ None ⇒ None … 735  Some result ⇒ 736 let 〈ppc,pc_sigma_map〉 ≝ result in 737 let 〈pc,map〉 ≝ pc_sigma_map in 738 Some … 〈ppc,pc〉 ]. 739 740 definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝ 741 λinstr_list. 742 match sigma0 instr_list with 744 743 [ None ⇒ None ? 745 744  Some result ⇒ 746 let 〈labels, pc_ppc_costs〉 ≝ result in 747 let 〈pc, ppc_costs〉 ≝ pc_ppc_costs in 748 let 〈ppc, costs〉 ≝ ppc_costs in 745 let 〈ppc,pc_sigma_map〉 ≝ result in 746 let 〈pc, sigma_map〉 ≝ pc_sigma_map in 749 747 if gtb pc (2^16) then 750 748 None ? 751 749 else 752 Some ? 〈labels, costs〉 753 ]. 750 Some ? (λx.lookup ?? x sigma_map (zero …)) ]. 751 752 (* stuff about policy *) 753 754 axiom policy_ok: ∀p. sigma_safe p ≠ None …. 755 756 definition sigma: pseudo_assembly_program → Word → Word ≝ 757 λp. 758 match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with 759 [ None ⇒ λabs. ⊥ 760  Some r ⇒ λ_.r] (policy_ok p). 761 cases abs // 762 qed. 763 764 example sigma_0: ∀p. sigma p (bitvector_of_nat ? 0) = bitvector_of_nat ? 0. 765 cases daemon. 766 qed. 767 768 axiom construct_costs_sigma: 769 ∀p,ppc,pc,pc',costs,costs',i. 770 bitvector_of_nat ? pc = sigma p (bitvector_of_nat ? ppc) → 771 Some … 〈pc',costs'〉 = construct_costs p ppc pc (λx.zero 16) (λx.zero 16) costs i → 772 bitvector_of_nat ? pc' = sigma p (bitvector_of_nat 16 (S ppc)). 773 774 axiom tech_pc_sigma00_append_Some: 775 ∀program,prefix,costs,label,i,pc',code,ppc,pc. 776 tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 → 777 construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 → 778 tech_pc_sigma00 program (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉. 779 780 axiom tech_pc_sigma00_append_None: 781 ∀program,prefix,i,ppc,pc,costs. 782 tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 → 783 construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None … 784 → False. 785 786 definition build_maps ≝ 787 λpseudo_program. 788 let result ≝ 789 foldl_strong 790 (option Identifier × pseudo_instruction) 791 (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))). 792 let 〈labels,ppc_pc_costs〉 ≝ res in 793 let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in 794 let 〈pc',costs〉 ≝ pc_costs in 795 bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧ 796 ppc' = length … pre ∧ 797 tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧ 798 ∀id. occurs_exactly_once id pre → 799 lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id)) 800 (\snd pseudo_program) 801 (λprefix,i,tl,prf,t. 802 let 〈labels, ppc_pc_costs〉 ≝ t in 803 let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in 804 let 〈pc,costs〉 ≝ pc_costs in 805 let 〈label, i'〉 ≝ i in 806 let labels ≝ 807 match label with 808 [ None ⇒ labels 809  Some label ⇒ 810 let program_counter_bv ≝ bitvector_of_nat ? pc in 811 insert ? ? label program_counter_bv labels 812 ] 813 in 814 match construct_costs pseudo_program ppc pc (λx. zero ?) (λx. zero ?) costs i' with 815 [ None ⇒ 816 let dummy ≝ 〈labels,ppc_pc_costs〉 in 817 dummy 818  Some construct ⇒ 〈labels, 〈S ppc,construct〉〉 819 ] 820 ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉 821 in 822 let 〈labels, ppc_pc_costs〉 ≝ result in 823 let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in 824 let 〈pc, costs〉 ≝ pc_costs in 825 〈labels, costs〉. 826 [3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ // 827  whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2 828 cases construct in p4 #PC #CODE #JMEQ % [% [%]] 829 [ @(construct_costs_sigma … IHn1) [4: <JMEQ % *: skip] 830  >length_append <IH0 normalize; IHn1; (*CSC: otherwise it diverges!*) // 831  @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ)) 832  #id normalize nodelta; labels1; cases label; normalize nodelta 833 [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 IHn1; (*CSC: otherwise it diverges!*) // 834  #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?; 835 generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %) 836 [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit 837 <IH0 [@IHn1  <(eq_bv_eq … EQ) in H #H @H] 838  #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: IHn1; /2/] 839 <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 IHn1; //]]] 840  (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2 841 @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ] 842 qed. 843 844 (* 845 lemma build_maps_ok: 846 ∀p:pseudo_assembly_program. 847 let 〈labels,costs〉 ≝ build_maps' p in 848 ∀pc. 849 (nat_of_bitvector … pc) < length … (\snd p) → 850 lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)). 851 #p cases p #preamble #instr_list 852 elim instr_list 853 [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ] 854  #hd #tl #IH 855 whd in ⊢ (match % with [ _ ⇒ ?]) 856 ] 857 qed. 858 *) 754 859 755 860 definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 756 861 λp. 757 862 let 〈preamble, instr_list〉 ≝ p in 758 match build_maps p with 863 let 〈labels,costs〉 ≝ build_maps p in 864 let datalabels ≝ construct_datalabels preamble in 865 let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in 866 let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in 867 let result ≝ foldr ? ? (λx. λy. 868 match y with 869 [ None ⇒ None ? 870  Some lst ⇒ 871 let 〈pc, ppc_y〉 ≝ lst in 872 let 〈ppc, y〉 ≝ ppc_y in 873 let x ≝ assembly_1_pseudoinstruction p ppc pc lookup_labels lookup_datalabels (\snd x) in 874 match x with 875 [ None ⇒ None ? 876  Some x ⇒ 877 let 〈pc_delta, program〉 ≝ x in 878 let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in 879 let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in 880 Some ? 〈new_pc, 〈new_ppc, (program @ y)〉〉 881 ] 882 ]) (Some ? 〈(zero ?), 〈(zero ?), [ ]〉〉) instr_list 883 in 884 match result with 759 885 [ None ⇒ None ? 760  Some labels_costs ⇒ 761 let datalabels ≝ construct_datalabels preamble in 762 let 〈labels,costs〉 ≝ labels_costs in 763 let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in 764 let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in 765 let result ≝ foldr ? ? (λx. λy. 766 match y with 767 [ None ⇒ None ? 768  Some lst ⇒ 769 let 〈pc, ppc_y〉 ≝ lst in 770 let 〈ppc, y〉 ≝ ppc_y in 771 let x ≝ assembly_1_pseudoinstruction p ppc pc lookup_labels lookup_datalabels (\snd x) in 772 match x with 773 [ None ⇒ None ? 774  Some x ⇒ 775 let 〈pc_delta, program〉 ≝ x in 776 let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in 777 let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in 778 Some ? 〈new_pc, 〈new_ppc, (program @ y)〉〉 779 ] 780 ]) (Some ? 〈(zero ?), 〈(zero ?), [ ]〉〉) instr_list 781 in 782 match result with 783 [ None ⇒ None ? 784  Some result ⇒ Some ? (〈\snd (\snd result), costs〉) 785 ] 786 ]. 886  Some result ⇒ Some ? (〈\snd (\snd result), costs〉)]. 787 887 788 888 definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
Note: See TracChangeset
for help on using the changeset viewer.