- Timestamp:
- Jul 26, 2012, 2:56:58 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2264 r2268 575 575 definition instruction_size ≝ 576 576 λlookup_labels. 577 λlookup_datalabels. 577 578 λsigma: Word → Word. 578 579 λpolicy: Word → bool. 579 580 λppc. 580 581 λi. 581 \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i). 582 582 \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels i). 583 583 584 584 (* Labels *) … … 622 622 sigma (zero …) = zero … ∧ 623 623 let instr_list ≝ \snd program in 624 let preamble ≝ \fst program in 624 625 ∀ppc: Word. ∀ppc_ok: nat_of_bitvector … ppc < |instr_list|. 625 626 let pc ≝ sigma ppc in 626 627 let labels ≝ \fst (create_label_cost_map instr_list) in 627 628 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 629 let lookup_datalabels ≝ λx. lookup_def … (construct_datalabels preamble) x (zero …) in 628 630 let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in 629 631 let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in 630 next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction))632 next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels lookup_datalabels sigma policy ppc instruction)) 631 633 ∧ 632 (nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction < 2^16634 (nat_of_bitvector … pc + instruction_size lookup_labels lookup_datalabels sigma policy ppc instruction < 2^16 633 635 ∨ 634 636 (∀ppc'. ∀ppc_ok':nat_of_bitvector … ppc' < |instr_list|. nat_of_bitvector … ppc < nat_of_bitvector … ppc' → 635 637 let instruction' ≝ \fst (fetch_pseudo_instruction instr_list ppc' ppc_ok') in 636 instruction_size lookup_labels sigma policy ppc' instruction' = 0)638 instruction_size lookup_labels lookup_datalabels sigma policy ppc' instruction' = 0) 637 639 ∧ 638 nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction = 2^16).640 nat_of_bitvector … pc + instruction_size lookup_labels lookup_datalabels sigma policy ppc instruction = 2^16). 639 641 640 642 … … 823 825 (|pre| < 2^16 → ∀ppc'. ∀ppc_ok':nat_of_bitvector … ppc' < |instr_list|. nat_of_bitvector … ppc ≤ nat_of_bitvector … ppc' → 824 826 let instruction' ≝ \fst (fetch_pseudo_instruction instr_list ppc' ppc_ok') in 825 instruction_size lookup_labels sigma policy ppc' instruction' = 0)827 instruction_size lookup_labels lookup_datalabels sigma policy ppc' instruction' = 0) 826 828 ) ∧ 827 829 ∀ppc'.∀ppc_ok'. … … 884 886 @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? p2) 885 887 @assembly1_pseudoinstruction_lt_2_to_16 ] #pc_delta_ok 886 cut (pc_delta = instruction_size lookup_labels sigma policy ppc (\snd hd))888 cut (pc_delta = instruction_size lookup_labels lookup_datalabels sigma policy ppc (\snd hd)) 887 889 [ whd in match instruction_size; normalize nodelta 888 890 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip] % ]
Note: See TracChangeset
for help on using the changeset viewer.