Changeset 1932 for src/ASM/Policy.ma


Ignore:
Timestamp:
May 10, 2012, 10:35:18 AM (8 years ago)
Author:
boender
Message:
  • added some more dependent types (we love 'em)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1931 r1932  
    13421342          ] (refl … z)
    13431343  ].*)
     1344 
    13441345
    13451346let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (length ? l) 2^16) (n: ℕ)
     
    13531354        (jump_in_policy program x))
    13541355        (policy_isize_sum program (create_label_map program) x))
     1356       
    13551357        (\fst x < 2^16)
    13561358    ]) ≝
     
    17991801(* the actual computation of the fixpoint *)
    18001802definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    1801   Σp:option ppc_pc_map.∃n.∀k.n < k →
    1802     policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program k))) p.
     1803  Σp:option ppc_pc_map.
     1804    And (match p with
     1805      [ None ⇒ True
     1806      | Some pol ⇒ And (And (And (And (
     1807      (out_of_program_none program pol))
     1808      (jump_in_policy program pol))
     1809      (policy_isize_sum program (create_label_map program) pol))
     1810      (policy_safe program (create_label_map program) pol))
     1811      (policy_compact program (create_label_map program) pol)
     1812      ])
     1813    (∃n.∀k.n < k →
     1814      policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program k))) p).
    18031815#program @(\snd (pi1 ?? (jump_expansion_internal program (2*|program|))))
    1804 
    18051816cases daemon
    18061817
     
    19381949definition jump_expansion':
    19391950 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
    1940  ℕ → ℕ × (option jump_length) ≝
    1941  λprogram.λppc:ℕ.
     1951 Σf:ℕ → ℕ × (option jump_length).
     1952   ∀ppc.match je_fixpoint (\snd program) with
     1953   [ None ⇒ True
     1954   | Some pol ⇒ \fst (f ppc) +
     1955      (instruction_size_sigma (create_label_map (\snd program)) pol (bitvector_of_nat ? (\fst (f ppc)))
     1956      (\snd (nth ppc ? (\snd program) 〈None ?, Comment []〉)))
     1957     = \fst (f (S ppc))
     1958   ] ≝
     1959λprogram.λppc:ℕ.
    19421960  let policy ≝ pi1 … (je_fixpoint (\snd program)) in
    19431961  match policy with
     
    19451963  | Some x ⇒ bvt_lookup ?? (bitvector_of_nat 16 ppc) (\snd x) 〈0,Some ? long_jump〉
    19461964  ].
     1965 cases daemon
     1966qed.
Note: See TracChangeset for help on using the changeset viewer.