Changeset 2078 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 14, 2012, 11:44:46 AM (8 years ago)
Author:
sacerdot
Message:

sigma_policy_specification has been
1) strengthened
2) made nicer to see
3) moved to Assembly.ma
4) used into Policy

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2073 r2078  
    768768 #lbl #instr normalize nodelta >add_associative %
    769769qed.
     770
     771definition 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 …))).
    770789
    771790definition assembly:
Note: See TracChangeset for help on using the changeset viewer.