Changeset 987 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 16, 2011, 6:08:12 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
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.