Changeset 987
- Timestamp:
- Jun 16, 2011, 6:08:12 PM (10 years ago)
- Location:
- src/ASM
- Files:
-
- 2 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 ? -
src/ASM/AssemblyProof.ma
r985 r987 681 681 682 682 lemma fetch_assembly_pseudo: 683 ∀program ,ppc,lookup_labels,lookup_datalabels.683 ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels. 684 684 ∀pi,code_memory,len,assembled,instructions,pc. 685 let expansion ≝ jump_expansion ppc programin685 let expansion ≝ pol ppc in 686 686 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi → 687 Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program p pc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →687 Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program pol ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi → 688 688 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled → 689 689 fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions. 690 #program #p pc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc690 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc 691 691 #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2 692 692 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b … … 779 779 780 780 axiom assembly_ok: 781 ∀program, assembled.782 let 〈labels,costs〉 ≝ build_maps program in783 Some … 〈assembled,costs〉 = assembly program →781 ∀program,pol,assembled. 782 let 〈labels,costs〉 ≝ build_maps program pol in 783 Some … 〈assembled,costs〉 = assembly program pol → 784 784 let code_memory ≝ load_code_memory assembled in 785 785 let preamble ≝ \fst program in 786 786 let datalabels ≝ construct_datalabels preamble in 787 let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in787 let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in 788 788 let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in 789 789 ∀ppc,len,assembledi. 790 790 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 791 Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program p pc (sigma programppc) lookup_labels lookup_datalabels pi →792 encoding_check code_memory (sigma program p pc) (bitvector_of_nat … (nat_of_bitvector … (sigma programppc) + len)) assembledi ∧793 sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma programppc) + len).791 Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi → 792 encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧ 793 sigma program pol newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len). 794 794 795 795 axiom bitvector_of_nat_nat_of_bitvector: … … 798 798 799 799 axiom assembly_ok_to_expand_pseudo_instruction_ok: 800 ∀program, assembled,costs.801 Some … 〈assembled,costs〉 = assembly program →800 ∀program,pol,assembled,costs. 801 Some … 〈assembled,costs〉 = assembly program pol → 802 802 ∀ppc. 803 803 let code_memory ≝ load_code_memory assembled in 804 804 let preamble ≝ \fst program in 805 805 let data_labels ≝ construct_datalabels preamble in 806 let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in806 let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in 807 807 let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in 808 let expansion ≝ jump_expansion ppc programin808 let expansion ≝ pol ppc in 809 809 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 810 810 ∃instructions. 811 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program p pc) expansion pi.811 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi. 812 812 813 813 axiom pair_elim': … … 849 849 850 850 lemma fetch_assembly_pseudo2: 851 ∀program, assembled.852 let 〈labels,costs〉 ≝ build_maps program in853 Some … 〈assembled,costs〉 = assembly program →851 ∀program,pol,assembled. 852 let 〈labels,costs〉 ≝ build_maps program pol in 853 Some … 〈assembled,costs〉 = assembly program pol → 854 854 ∀ppc. 855 855 let code_memory ≝ load_code_memory assembled in 856 856 let preamble ≝ \fst program in 857 857 let data_labels ≝ construct_datalabels preamble in 858 let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in858 let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in 859 859 let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in 860 let expansion ≝ jump_expansion ppc programin860 let expansion ≝ pol ppc in 861 861 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 862 862 ∃instructions. 863 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program p pc) expansion pi ∧864 fetch_many code_memory (sigma program newppc) (sigma programppc) instructions.865 #program # assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc866 generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program assembled costs ASSEMBLY ppc)863 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi ∧ 864 fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions. 865 #program #pol #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc 866 generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program pol assembled costs ASSEMBLY ppc) 867 867 letin code_memory ≝ (load_code_memory assembled) 868 868 letin preamble ≝ (\fst program) 869 869 letin data_labels ≝ (construct_datalabels preamble) 870 letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x))870 letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) 871 871 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?)) 872 whd in ⊢ (% → %) generalize in match (assembly_ok program assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;872 whd in ⊢ (% → %) generalize in match (assembly_ok program pol assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX; 873 873 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc 874 generalize in match (fetch_assembly_pseudo program p pc875 (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi874 generalize in match (fetch_assembly_pseudo program pol ppc 875 (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi 876 876 (load_code_memory assembled)); 877 877 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND 878 878 whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?); 879 879 normalize nodelta in EXPAND; (* HERE *) 880 generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program p pc))) -H1; #H1880 generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program pol ppc))) -H1; #H1 881 881 >bitvector_of_nat_nat_of_bitvector in H1; #H1 882 882 <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?) … … 943 943 944 944 axiom low_internal_ram_of_pseudo_internal_ram_hit: 945 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀ addr:BitVector 7.945 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀pol:policy (code_memory … s).∀addr:BitVector 7. 946 946 member ? (eq_bv 8) (false:::addr) M = true → 947 947 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in … … 950 950 let bl ≝ lookup ? 7 addr ram (zero 8) in 951 951 let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in 952 bu@@bl = sigma (code_memory … s) (pbu@@pbl).952 bu@@bl = sigma (code_memory … s) pol (pbu@@pbl). 953 953 954 954 (* changed from add to sub *) … … 1033 1033 1034 1034 definition status_of_pseudo_status: 1035 internal_pseudo_address_map → PseudoStatus→ option Status ≝1036 λM,ps .1035 internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → option Status ≝ 1036 λM,ps,pol. 1037 1037 let pap ≝ code_memory … ps in 1038 match assembly pap with1038 match assembly pap pol with 1039 1039 [ None ⇒ None … 1040 1040 | Some p ⇒ 1041 1041 let cm ≝ load_code_memory (\fst p) in 1042 let pc ≝ sigma pap (program_counter ? ps) in1042 let pc ≝ sigma pap pol (program_counter ? ps) in 1043 1043 let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in 1044 1044 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in … … 1156 1156 ∀M:internal_pseudo_address_map. 1157 1157 ∀ps,ps': PseudoStatus. 1158 code_memory … ps = code_memory … ps' → 1159 match status_of_pseudo_status M ps with 1160 [ None ⇒ status_of_pseudo_status M ps' = None … 1161 | Some _ ⇒ ∃w. status_of_pseudo_status M ps' = Some … w 1158 ∀pol. 1159 ∀prf:code_memory … ps = code_memory … ps'. 1160 let pol' ≝ ? in 1161 match status_of_pseudo_status M ps pol with 1162 [ None ⇒ status_of_pseudo_status M ps' pol' = None … 1163 | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w 1162 1164 ]. 1163 #M #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) 1164 generalize in match (refl … (assembly (code_memory … ps))) 1165 cases (assembly ?) in ⊢ (???% → %) 1165 [2: <prf @pol] 1166 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) 1167 generalize in match (refl … (assembly (code_memory … ps) pol)) 1168 cases (assembly ??) in ⊢ (???% → %) 1166 1169 [ #K whd whd in ⊢ (??%?) <H >K % 1167 1170 | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ] 1168 1171 qed. 1169 1172 1170 definition ticks_of0: pseudo_assembly_program→ Word → ? → nat × nat ≝1171 λprogram: pseudo_assembly_program. 1173 definition ticks_of0: ∀p:pseudo_assembly_program. policy p → Word → ? → nat × nat ≝ 1174 λprogram: pseudo_assembly_program.λpol. 1172 1175 λppc: Word. 1173 1176 λfetched. … … 1176 1179 match instr with 1177 1180 [ JC lbl ⇒ 1178 match jump_expansion ppc programwith1181 match pol ppc with 1179 1182 [ short_jump ⇒ 〈2, 2〉 1180 1183 | medium_jump ⇒ ? … … 1182 1185 ] 1183 1186 | JNC lbl ⇒ 1184 match jump_expansion ppc programwith1187 match pol ppc with 1185 1188 [ short_jump ⇒ 〈2, 2〉 1186 1189 | medium_jump ⇒ ? … … 1188 1191 ] 1189 1192 | JB bit lbl ⇒ 1190 match jump_expansion ppc programwith1193 match pol ppc with 1191 1194 [ short_jump ⇒ 〈2, 2〉 1192 1195 | medium_jump ⇒ ? … … 1194 1197 ] 1195 1198 | JNB bit lbl ⇒ 1196 match jump_expansion ppc programwith1199 match pol ppc with 1197 1200 [ short_jump ⇒ 〈2, 2〉 1198 1201 | medium_jump ⇒ ? … … 1200 1203 ] 1201 1204 | JBC bit lbl ⇒ 1202 match jump_expansion ppc programwith1205 match pol ppc with 1203 1206 [ short_jump ⇒ 〈2, 2〉 1204 1207 | medium_jump ⇒ ? … … 1206 1209 ] 1207 1210 | JZ lbl ⇒ 1208 match jump_expansion ppc programwith1211 match pol ppc with 1209 1212 [ short_jump ⇒ 〈2, 2〉 1210 1213 | medium_jump ⇒ ? … … 1212 1215 ] 1213 1216 | JNZ lbl ⇒ 1214 match jump_expansion ppc programwith1217 match pol ppc with 1215 1218 [ short_jump ⇒ 〈2, 2〉 1216 1219 | medium_jump ⇒ ? … … 1218 1221 ] 1219 1222 | CJNE arg lbl ⇒ 1220 match jump_expansion ppc programwith1223 match pol ppc with 1221 1224 [ short_jump ⇒ 〈2, 2〉 1222 1225 | medium_jump ⇒ ? … … 1224 1227 ] 1225 1228 | DJNZ arg lbl ⇒ 1226 match jump_expansion ppc programwith1229 match pol ppc with 1227 1230 [ short_jump ⇒ 〈2, 2〉 1228 1231 | medium_jump ⇒ ? … … 1323 1326 qed. 1324 1327 1325 definition ticks_of: pseudo_assembly_program→ Word → nat × nat ≝1326 λprogram: pseudo_assembly_program. 1328 definition ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat ≝ 1329 λprogram: pseudo_assembly_program.λpol. 1327 1330 λppc: Word. 1328 1331 let 〈preamble, pseudo〉 ≝ program in 1329 1332 let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in 1330 ticks_of0 program p pc fetched.1333 ticks_of0 program pol ppc fetched. 1331 1334 1332 1335 lemma get_register_set_program_counter:
Note: See TracChangeset
for help on using the changeset viewer.