Changeset 2023
 Timestamp:
 Jun 7, 2012, 2:08:18 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2020 r2023 311 311 qed. 312 312 313 lemma set_program_counter_set_program_counter: 314 ∀M: Type[0]. 315 ∀cm: M. 316 ∀s: PreStatus M cm. 317 ∀pc: Word. 318 ∀pc': Word. 319 set_program_counter M cm (set_program_counter M cm s pc) pc' = 320 set_program_counter M cm s pc'. 321 #M #cm #s #pc #pc' % 322 qed. 323 313 324 lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P. 314 325 #P #A #a #abs destruct … … 397 408 398 409 lemma main_lemma_preinstruction: 399 ∀M,M': internal_pseudo_address_map. 400 ∀preamble : preamble. ∀instr_list : list labelled_instruction. 401 ∀cm: pseudo_assembly_program. 402 ∀EQcm: cm = 〈preamble,instr_list〉. 403 ∀sigma : Word→Word. ∀policy : Word→bool. 404 ∀sigma_policy_witness : sigma_policy_specification cm sigma policy. 405 ∀ps : PseudoStatus cm. 406 ∀ppc : Word. 407 ∀EQppc : ppc=program_counter pseudo_assembly_program cm ps. 408 ∀labels : label_map. 409 ∀costs : BitVectorTrie costlabel 16. 410 ∀create_label_cost_refl : create_label_cost_map instr_list=〈labels,costs〉. 411 ∀newppc : Word. 412 ∀lookup_labels : Identifier→Word. 413 ∀EQlookup_labels : lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x). 414 ∀lookup_datalabels : identifier ASMTag→Word. 415 ∀EQlookup_datalabels : lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)). 416 ∀EQnewppc : newppc=add 16 ppc (bitvector_of_nat 16 1). 417 ∀instr: preinstruction Identifier. 418 ∀ticks. 419 ∀EQticks: ticks = ticks_of0 〈preamble,instr_list〉 sigma policy ppc (Instruction instr). 420 ∀addr_of. 421 ∀EQaddr_of: addr_of = (λx:Identifier 422 .λy:PreStatus pseudo_assembly_program cm 423 .address_of_word_labels cm x). 424 ∀s. 425 ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps 426 (add 16 ppc (bitvector_of_nat 16 1))). 427 ∀P. 428 ∀EQP: P = (λinstr, s. 429 sigma (add 16 ppc (bitvector_of_nat 16 1)) 430 =add 16 (sigma ppc) 431 (bitvector_of_nat 16 432 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc 433 lookup_datalabels (Instruction instr)))) 434 →next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) 435 M cm ps 436 =Some internal_pseudo_address_map M' 437 →fetch_many (load_code_memory (\fst (assembly cm sigma policy))) 438 (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps)) 439 (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels 440 (Instruction instr)) 441 → ∃n. execute n 442 (code_memory_of_pseudo_assembly_program cm sigma 443 policy) 444 (status_of_pseudo_status M cm ps sigma policy) 445 =status_of_pseudo_status M' cm s sigma policy). 446 P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm 447 addr_of instr s). 448 #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels 449 #costs #create_label_cost_refl #newppc 450 #lookup_labels #EQlookup_labels #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr 451 #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP 452 (*#sigma_increment_commutation #maps_assm #fetch_many_assm *) 453 letin a ≝ Identifier letin m ≝ pseudo_assembly_program 454 cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s)) 455 [2: * // ] 456 @( 410 ∀M, M': internal_pseudo_address_map. 411 ∀preamble: preamble. 412 ∀instr_list: list labelled_instruction. 413 ∀cm: pseudo_assembly_program. 414 ∀EQcm: cm = 〈preamble, instr_list〉. 415 ∀sigma: Word → Word. 416 ∀policy: Word → bool. 417 ∀sigma_policy_witness: sigma_policy_specification cm sigma policy. 418 ∀ps: PseudoStatus cm. 419 ∀ppc: Word. 420 ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps. 421 ∀labels: label_map. 422 ∀costs: BitVectorTrie costlabel 16. 423 ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉. 424 ∀newppc: Word. 425 ∀lookup_labels: Identifier → Word. 426 ∀EQlookup_labels: lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x). 427 ∀lookup_datalabels: Identifier → Word. 428 ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)). 429 ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1). 430 ∀instr: preinstruction Identifier. 431 ∀ticks: nat × nat. 432 ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr). 433 ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16. 434 ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x). 435 ∀s: PreStatus pseudo_assembly_program cm. 436 ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))). 437 ∀P: preinstruction Identifier → PseudoStatus cm → Prop. 438 ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc) 439 (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc 440 lookup_datalabels (Instruction instr)))) → 441 next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cm ps = Some internal_pseudo_address_map M' → 442 fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps)) 443 (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) → 444 ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) = 445 status_of_pseudo_status M' cm s sigma policy). 446 P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s). 447 #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels 448 #costs #create_label_cost_refl #newppc 449 #lookup_labels #EQlookup_labels #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr 450 #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP 451 (*#sigma_increment_commutation #maps_assm #fetch_many_assm *) 452 letin a ≝ Identifier letin m ≝ pseudo_assembly_program 453 cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s)) 454 [2: * // ] 455 @( 457 456 let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in 458 457 let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in … … 860 859 try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*) 861 860 whd in match execute_1_preinstruction; normalize nodelta 862 [31 : (* DJNZ *)861 [31,32: (* DJNZ *) 863 862 (* XXX: work on the right hand side *) 864 863 >p normalize nodelta … … 872 871 @pair_elim #upper #lower #split_refl 873 872 cases (eq_bv ???) normalize nodelta 874 [1 :873 [1,3: 875 874 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 876 875 whd in ⊢ (??%?); 877 876 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 878 877 (* XXX: work on the left hand side *) 879 check pair_replace880 878 @(pair_replace ?????????? p) normalize nodelta 881 [1 :879 [1,3: 882 880 cases daemon 883 881 ] … … 889 887 @split_eq_status try % 890 888 cases daemon 891 2 :889 2,4: 892 890 >EQppc 893 891 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl … … 899 897 #status_after_1 #EQstatus_after_1 900 898 <(?: ? = status_after_1) 901 [3 :899 [3,6: 902 900 >EQstatus_after_1 in ⊢ (???%); 903 901 whd in ⊢ (???%); 904 <fetch_refl in ⊢ (???%); 902 [1: 903 <fetch_refl in ⊢ (???%); 904 2: 905 <fetch_refl in ⊢ (???%); 906 ] 905 907 whd in ⊢ (???%); 906 908 @(pair_replace ?????????? p) 907 [1 :909 [1,3: 908 910 cases daemon 909 2 :911 2,4: 910 912 normalize nodelta 911 913 whd in match (addr_of_relative ????); … … 915 917 change with (add ???) in match (\snd (half_add ???)); 916 918 >set_arg_8_set_program_counter in ⊢ (???%); 917 [2,4 : cases daemon ]919 [2,4,6,8: cases daemon ] 918 920 >program_counter_set_program_counter in ⊢ (???%); 919 921 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') 920 [2,4 :922 [2,4,6,8: 921 923 >bitvector_of_nat_sign_extension_equivalence 922 [1,3 :924 [1,3,5,7: 923 925 >EQintermediate_pc' % 924 926 *: … … 926 928 ] 927 929 ] 928 [1 : % ]930 [1,3: % ] 929 931 ] 930 1 :932 1,4: 931 933 skip 932 934 ] 933 [ 2:935 [3,4: 934 936 status_after_1 935 937 @(pose … (execute_1 ? (mk_PreStatus …))) 936 938 #status_after_1 #EQstatus_after_1 937 939 <(?: ? = status_after_1) 938 [3 :940 [3,6: 939 941 >EQstatus_after_1 in ⊢ (???%); 940 942 whd in ⊢ (???%); 941 943 (* XXX: matita bug with patterns across multiple goals *) 942 <fetch_refl'' in ⊢ (???%); 943 whd in ⊢ (???%); % 944 1: 945 skip 944 [1: 945 <fetch_refl'' in ⊢ (???%); 946 2: 947 <fetch_refl'' in ⊢ (???%); 948 ] 949 [2: % 1: whd in ⊢ (???%); % ] 950 1,4: 951 skip 952 ] 953 status_after_1 whd in ⊢ (??%?); 954 (* XXX: switch to the right hand side *) 955 normalize nodelta >EQs s >EQticks ticks 956 cases (¬ eq_bv ???) normalize nodelta 957 whd in ⊢ (??%%); 946 958 ] 947 status_after_1 whd in ⊢ (??%?); 948 (* XXX: switch to the right hand side *) 949 normalize nodelta >EQs s >EQticks ticks 950 cases (¬ eq_bv ???) normalize nodelta 959 (* XXX: finally, prove the equality using sigma commutation *) 960 @split_eq_status try % 951 961 whd in ⊢ (??%%); 962 cases daemon 952 963 ] 953 (* XXX: finally, prove the equality using sigma commutation *)954 @split_eq_status XXX try %955 cases daemon956 964 30: (* CJNE *) 957 965 (* XXX: work on the right hand side *) … … 1055 1063 (* XXX: finally, prove the equality using sigma commutation *) 1056 1064 @split_eq_status try % 1057 [3: 1058 whd in ⊢ (??%?); 1059 cases daemon 1060 *: 1061 cases daemon 1062 ] 1065 cases daemon 1063 1066 ] 1064 1067 17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *) … … 1238 1241 (* XXX: finally, prove the equality using sigma commutation *) 1239 1242 try @split_eq_status try % whd in ⊢ (??%%); 1240 [1: 1241 >low_internal_ram_set_8051_sfr >low_internal_ram_set_clock 1242 >low_internal_ram_set_program_counter @eq_f2 try % 1243 whd in maps_assm:(??%?); destruct % 1244 2: 1245 >high_internal_ram_set_8051_sfr >high_internal_ram_set_clock 1246 >high_internal_ram_set_program_counter @eq_f2 try % 1247 whd in maps_assm:(??%?); destruct % 1248 3: 1249 >clock_set_program_counter >clock_set_program_counter <instr_refl % 1250 4,6: 1251 >set_clock_set_program_counter >get_arg_8_set_program_counter 1252 >clock_set_program_counter >set_clock_mk_Status_commutation 1253 >set_clock_mk_Status_commutation >clock_set_program_counter <instr_refl 1254 8: 1255 cases daemon 1256 ] 1243 cases daemon 1257 1244 1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI *) 1258 1245 (* XXX: work on the right hand side *) … … 1283 1270 (* XXX: finally, prove the equality using sigma commutation *) 1284 1271 try @split_eq_status try % 1285 >set_clock_mk_Status_commutation 1286 cases daemon (* 1287 @split_eq_status try % 1288 [*: whd in ⊢ (??%%); >set_clock_mk_Status_commutation 1289 whd in match (set_flags ??????); 1290 (* CSC: TO BE COMPLETED *) 1291 ] *) 1272 cases daemon 1292 1273 10,42,43,44,45,49,52,56: (* MUL *) 1293 1274 (* XXX: work on the right hand side *) … … 1410 1391 cases daemon 1411 1392 ] 1412 ] 1413 cases daemon (* XXX: CJNE and DJNZ cases *) 1414 qed. 1415 (* 1416 1417 1418 @list_addressing_mode_tags_elim_prop try % whd 1419 @list_addressing_mode_tags_elim_prop try % whd #arg 1420 (* XXX: we first work on sigma_increment_commutation *) 1421 #sigma_increment_commutation 1422 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; 1423 (* XXX: we work on the maps *) 1424 whd in ⊢ (??%? → ?); 1425 try (change with (if ? then ? else ? = ? → ?) 1426 cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta) 1427 #H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm <map_refl_assm 1428 (* XXX: we assume the fetch_many hypothesis *) 1429 #fetch_many_assm 1430 (* XXX: we give the existential *) 1431 %{1} 1432 whd in match (execute_1_pseudo_instruction0 ?????); 1433 (* XXX: work on the left hand side of the equality *) 1434 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc 1435 (* XXX: execute fetches some more *) 1436 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 1437 whd in fetch_many_assm; 1438 >EQassembled in fetch_many_assm; 1439 cases (fetch ??) * #instr #newpc #ticks normalize nodelta * * 1440 #eq_instr #EQticks whd in EQticks:(???%); >EQticks 1441 #fetch_many_assm whd in fetch_many_assm; 1442 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 1443 >(eq_instruction_to_eq … eq_instr) instr 1444 [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs 1445 @(pose … 1446 (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy)) 1447 #Pl #EQPl 1448 cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq 1449 lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) XX >EQlhs lhs 1450 whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%))); 1451 @pair_elim 1452 >tech_pi1_let_as_commute 1453 1454 *) 1455 1393 qed. 1456 1394 1457 1395 theorem main_thm:
Note: See TracChangeset
for help on using the changeset viewer.