Changeset 2144 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jul 2, 2012, 3:59:09 PM (7 years ago)
Author:
sacerdot
Message:
  1. Policy specification fixed
  2. Proof of monotonicity of sigma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2138 r2144  
    698698  λpolicy: Word → bool.
    699699  sigma (zero …) = zero … ∧
    700   ∀ppc: Word. ∀ppc_ok.
    701     let instr_list ≝ \snd program in
     700  let instr_list ≝ \snd program in
     701  ∀ppc: Word. ∀ppc_ok: nat_of_bitvector … ppc < |instr_list|.
    702702    let pc ≝ sigma ppc in
    703703    let labels ≝ \fst (create_label_cost_map instr_list) in
     
    705705    let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
    706706    let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
    707      (nat_of_bitvector … ppc ≤ |instr_list| →
    708        next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction)))
    709      ∧       
    710       (  (nat_of_bitvector … ppc < |instr_list| → nat_of_bitvector … pc < nat_of_bitvector … next_pc)
    711        ∨ (nat_of_bitvector … ppc = |instr_list| → nat_of_bitvector … pc < nat_of_bitvector … next_pc ∨ next_pc = (zero …))).
     707     next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction))
     708     ∧
     709     (nat_of_bitvector … pc < nat_of_bitvector … next_pc ∨
     710      nat_of_bitvector … ppc = |instr_list| ∧ next_pc = zero …).
    712711
    713712definition assembly:
Note: See TracChangeset for help on using the changeset viewer.