Changeset 1942 for src/ASM/Policy.ma


Ignore:
Timestamp:
May 14, 2012, 6:02:20 PM (8 years ago)
Author:
mulligan
Message:

Work on showing the equivalence of two methods of looking up from the maps.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1940 r1942  
    16651665qed.
    16661666
     1667include alias "arithmetics/nat.ma".
     1668include alias "basics/logic.ma".
     1669
     1670check create_label_cost_map
     1671
    16671672(* The glue between Policy and Assembly. *)
    16681673definition jump_expansion':
    16691674 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
    16701675  option (Σsigma:Word → Word × bool.
    1671    ∀ppc:ℕ.
    1672     And (ppc ≤ (|\snd program|) →
    1673     \snd
    1674      (half_add ?
    1675       (\fst (sigma (bitvector_of_nat 16 ppc)))
    1676       (bitvector_of_nat ?
    1677        (instruction_size
    1678         (λid. bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) id 0))
    1679         sigma (bitvector_of_nat ? ppc)
    1680          (\fst (fetch_pseudo_instruction (\snd program) (bitvector_of_nat ? ppc))))))
    1681     = (* \fst (sigma (\snd (half_add ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? 1)))) *)
    1682       \fst (sigma (bitvector_of_nat ? (S ppc))))
    1683     (ppc < (|\snd program|) →
    1684       Or (lt_u ? (\fst (sigma (bitvector_of_nat ? ppc))) (\fst (sigma (bitvector_of_nat ? (S ppc)))) = true)
    1685        (And (S ppc = (|\snd program|)) (\fst (sigma (bitvector_of_nat ? (S ppc))) = (zero 16))))
    1686   )
    1687 ≝ λprogram.? (*
    1688   let policy ≝ pi1 … (je_fixpoint (\snd program)) in
    1689   match policy with
    1690   [ None ⇒ None ?
    1691   | Some x ⇒ Some ?
    1692       «λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
    1693         〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?»
    1694   ]*).
     1676   ∀ppc: Word.
     1677   let pc ≝ \fst (sigma ppc) in
     1678   let labels ≝ \fst (create_label_cost_map (\snd program)) in
     1679   let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def ?? labels x 0) in
     1680   let instruction ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
     1681   let next_pc ≝ \fst (sigma (add … ppc (bitvector_of_nat ? 1))) in
     1682     (nat_of_bitvector … ppc ≤ |\snd program| →
     1683       next_pc = add … pc (bitvector_of_nat … (instruction_size lookup_labels sigma ppc instruction)))
     1684     ∧
     1685      ((nat_of_bitvector … ppc < |\snd program| →
     1686        nat_of_bitvector … pc < nat_of_bitvector … next_pc)
     1687      ∨
     1688       (nat_of_bitvector … ppc = |\snd program| → next_pc = (zero …)))).
    16951689 cases daemon
    16961690qed.
Note: See TracChangeset for help on using the changeset viewer.