Changeset 987 for src/ASM/Assembly.ma
- Timestamp:
- Jun 16, 2011, 6:08:12 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r985 r987 656 656 jump_expansion_policy_internal program old_labels old_policy in 657 657 jump_expansion_internal n' program new_labels new_policy ]. 658 659 definition jump_expansion ≝ 660 λpc.λprogram. 658 659 definition policy_type ≝ Word → jump_length. 660 661 definition jump_expansion': pseudo_assembly_program → policy_type ≝ 662 λprogram.λpc. 661 663 let policy ≝ jump_expansion_internal (length ? (\snd program)) program (Stub ? ?) (Stub ? ?) in 662 664 lookup ? ? pc policy long_jump. … … 664 666 definition assembly_1_pseudoinstruction ≝ 665 667 λprogram: pseudo_assembly_program. 668 λjump_expansion: policy_type. 666 669 λppc: Word. 667 670 λpc: Word. … … 669 672 λlookup_datalabels. 670 673 λi. 671 let expansion ≝ jump_expansion ppc programin674 let expansion ≝ jump_expansion ppc in 672 675 match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with 673 676 [ None ⇒ None ? … … 681 684 definition construct_costs ≝ 682 685 λprogram. 686 λjump_expansion: policy_type. 683 687 λpseudo_program_counter: nat. 684 688 λprogram_counter: nat. … … 695 699 let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in 696 700 let pc_delta_assembled ≝ 697 assembly_1_pseudoinstruction program ppc_bv pc_bv701 assembly_1_pseudoinstruction program jump_expansion ppc_bv pc_bv 698 702 lookup_labels lookup_datalabels i 699 703 in … … 709 713 program counters. It is at the heart of the proof. *) 710 714 (*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. 715 definition sigma00: pseudo_assembly_program → policy_type → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝ 716 λinstr_list. 717 λjump_expansion: policy_type. 718 λl:list labelled_instruction. 713 719 foldl ?? 714 720 (λt,i. … … 719 725 let 〈program_counter, sigma_map〉 ≝ pc_map in 720 726 let 〈label, i〉 ≝ i in 721 match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with727 match construct_costs instr_list jump_expansion ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with 722 728 [ None ⇒ None ? 723 729 | Some pc_ignore ⇒ … … 726 732 ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l. 727 733 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 with734 definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16))) 735 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog). 736 737 definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝ 738 λprogram,jump_expansion,instr_list. 739 match sigma00 program jump_expansion instr_list with 734 740 [ None ⇒ None … 735 741 | Some result ⇒ … … 738 744 Some … 〈ppc,pc〉 ]. 739 745 740 definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝741 λinstr_list .742 match sigma0 instr_list with746 definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝ 747 λinstr_list,jump_expansion. 748 match sigma0 instr_list jump_expansion with 743 749 [ None ⇒ None ? 744 750 | Some result ⇒ … … 752 758 (* stuff about policy *) 753 759 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 760 definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None …. 761 762 definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p. 763 764 lemma eject_policy: ∀p. policy p → policy_type. 765 #p #pol @(eject … pol) 766 qed. 767 768 coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type. 769 770 definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝ 771 λp,policy. 772 match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with 759 773 [ None ⇒ λabs. ⊥ 760 | Some r ⇒ λ_.r] ( policy_ok p).774 | Some r ⇒ λ_.r] (sig2 … policy). 761 775 cases abs // 762 776 qed. 763 777 764 example sigma_0: ∀p . sigma p(bitvector_of_nat ? 0) = bitvector_of_nat ? 0.778 example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0. 765 779 cases daemon. 766 780 qed. 767 781 768 782 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 p pc pc (λx.zero 16) (λx.zero 16) costs i →772 bitvector_of_nat ? pc' = sigma p (bitvector_of_nat 16 (S ppc)).783 ∀p.∀pol:policy p.∀ppc,pc,pc',costs,costs',i. 784 bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) → 785 Some … 〈pc',costs'〉 = construct_costs p pol ppc pc (λx.zero 16) (λx.zero 16) costs i → 786 bitvector_of_nat ? pc' = sigma p pol (bitvector_of_nat 16 (S ppc)). 773 787 774 788 axiom tech_pc_sigma00_append_Some: 775 ∀program ,prefix,costs,label,i,pc',code,ppc,pc.776 tech_pc_sigma00 program p refix = 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'〉.789 ∀program.∀pol:policy program.∀prefix,costs,label,i,pc',code,ppc,pc. 790 tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 → 791 construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 → 792 tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉. 779 793 780 794 axiom tech_pc_sigma00_append_None: 781 ∀program ,prefix,i,ppc,pc,costs.782 tech_pc_sigma00 program p refix = Some … 〈ppc,pc〉 →783 construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …795 ∀program.∀pol:policy program.∀prefix,i,ppc,pc,costs. 796 tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 → 797 construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = None … 784 798 → False. 785 799 786 800 definition build_maps ≝ 787 λpseudo_program. 801 λpseudo_program.λpol:policy pseudo_program. 788 802 let result ≝ 789 803 foldl_strong … … 793 807 let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in 794 808 let 〈pc',costs〉 ≝ pc_costs in 795 bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧809 bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc') ∧ 796 810 ppc' = length … pre ∧ 797 tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧811 tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉 ∧ 798 812 ∀id. occurs_exactly_once id pre → 799 lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id))813 lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)) 800 814 (\snd pseudo_program) 801 815 (λprefix,i,tl,prf,t. … … 812 826 ] 813 827 in 814 match construct_costs pseudo_program p pc pc (λx. zero ?) (λx. zero ?) costs i' with828 match construct_costs pseudo_program pol ppc pc (λx. zero ?) (λx. zero ?) costs i' with 815 829 [ None ⇒ 816 830 let dummy ≝ 〈labels,ppc_pc_costs〉 in … … 858 872 *) 859 873 860 definition assembly: pseudo_assembly_program→ option (list Byte × (BitVectorTrie Identifier 16)) ≝861 λp .874 definition assembly: ∀p:pseudo_assembly_program. policy p → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 875 λp,pol. 862 876 let 〈preamble, instr_list〉 ≝ p in 863 let 〈labels,costs〉 ≝ build_maps p in877 let 〈labels,costs〉 ≝ build_maps p pol in 864 878 let datalabels ≝ construct_datalabels preamble in 865 879 let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in … … 871 885 let 〈pc, ppc_y〉 ≝ lst in 872 886 let 〈ppc, y〉 ≝ ppc_y in 873 let x ≝ assembly_1_pseudoinstruction p p pc pc lookup_labels lookup_datalabels (\snd x) in887 let x ≝ assembly_1_pseudoinstruction p pol ppc pc lookup_labels lookup_datalabels (\snd x) in 874 888 match x with 875 889 [ None ⇒ None ?
Note: See TracChangeset
for help on using the changeset viewer.