Changeset 2078 for src/ASM/Assembly.ma
 Timestamp:
 Jun 14, 2012, 11:44:46 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2073 r2078 768 768 #lbl #instr normalize nodelta >add_associative % 769 769 qed. 770 771 definition sigma_policy_specification ≝ 772 λprogram: pseudo_assembly_program. 773 λsigma: Word → Word. 774 λpolicy: Word → bool. 775 ∀ppc: Word. ∀ppc_ok. 776 let instr_list ≝ \snd program in 777 let pc ≝ sigma ppc in 778 let labels ≝ \fst (create_label_cost_map instr_list) in 779 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 780 let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in 781 let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in 782 sigma (zero …) = zero … 783 ∧ 784 (nat_of_bitvector … ppc ≤ instr_list → 785 next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction))) 786 ∧ 787 ( (nat_of_bitvector … ppc < instr_list → nat_of_bitvector … pc < nat_of_bitvector … next_pc) 788 ∨ (nat_of_bitvector … ppc = instr_list → next_pc = (zero …))). 770 789 771 790 definition assembly:
Note: See TracChangeset
for help on using the changeset viewer.