Changeset 2108 for src/ASM/AssemblyProofSplit.ma
 Timestamp:
 Jun 25, 2012, 2:39:06 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2047 r2108 405 405 include alias "ASM/Vector.ma". 406 406 407 axiom main_lemma_preinstruction: 408 ∀M, M': internal_pseudo_address_map. 409 ∀preamble: preamble. 410 ∀instr_list: list labelled_instruction. 411 ∀cm: pseudo_assembly_program. 412 ∀EQcm: cm = 〈preamble, instr_list〉. 413 ∀sigma: Word → Word. 414 ∀policy: Word → bool. 415 ∀sigma_policy_witness: sigma_policy_specification cm sigma policy. 416 ∀ps: PseudoStatus cm. 417 ∀ppc: Word. 418 ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps. 419 ∀labels: label_map. 420 ∀costs: BitVectorTrie costlabel 16. 421 ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉. 422 ∀newppc: Word. 423 ∀lookup_labels: Identifier → Word. 424 ∀EQlookup_labels: lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x). 425 ∀lookup_datalabels: Identifier → Word. 426 ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)). 427 ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1). 428 ∀instr: preinstruction Identifier. 429 ∀ticks: nat × nat. 430 ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr). 431 ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16. 432 ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x). 433 ∀s: PreStatus pseudo_assembly_program cm. 434 ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))). 435 ∀P: preinstruction Identifier → PseudoStatus cm → Prop. 436 ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc) 437 (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc 438 lookup_datalabels (Instruction instr)))) → 439 next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cm ps = Some internal_pseudo_address_map M' → 440 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)) 441 (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) → 442 ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) = 443 status_of_pseudo_status M' cm s sigma policy). 444 P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s). 445 446 (* 407 axiom sub16_with_carry_overflow: 408 ∀left, right, result: BitVector 16. 409 ∀flags: BitVector 3. 410 ∀upper: BitVector 9. 411 ∀lower: BitVector 7. 412 sub_16_with_carry left right false = 〈result, flags〉 → 413 vsplit bool 9 7 result = 〈upper, lower〉 → 414 get_index_v bool 3 flags 2 ? = true → 415 upper = [[true; true; true; true; true; true; true; true; true]]. 416 // 417 qed. 418 447 419 lemma main_lemma_preinstruction: 448 420 ∀M, M': internal_pseudo_address_map. … … 477 449 (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc 478 450 lookup_datalabels (Instruction instr)))) → 479 next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cmps = Some internal_pseudo_address_map M' →451 next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' → 480 452 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)) 481 453 (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) → … … 899 871 [31,32: (* DJNZ *) 900 872 (* XXX: work on the right hand side *) 901 >p normalize nodelta 873 >p normalize nodelta >p1 normalize nodelta 902 874 (* XXX: switch to the left hand side *) 903 875 instr_refl >EQP P normalize nodelta 904 876 #sigma_increment_commutation #maps_assm #fetch_many_assm 905 877 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 906 whd in match (expand_relative_jump ????);907 878 <EQppc in fetch_many_assm; 879 whd in match (short_jump_cond ??); 880 @pair_elim #sj_possible #disp 908 881 @pair_elim #result #flags #sub16_refl 909 882 @pair_elim #upper #lower #vsplit_refl 910 cases (eq_bv ???) normalize nodelta 883 inversion (get_index' bool ???) #get_index_refl' normalize nodelta 884 #sj_possible_pair destruct(sj_possible_pair) 885 >p1 normalize nodelta 911 886 [1,3: 912 887 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 913 888 whd in ⊢ (??%?); 889 >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; 890 normalize nodelta in ⊢ (% → ?); #fetch_many_assm 914 891 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 915 892 (* XXX: work on the left hand side *) … … 927 904 cases daemon 928 905 2,4: 906 XXX: here 929 907 >EQppc 930 908 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
Note: See TracChangeset
for help on using the changeset viewer.