Theory Nonrelational_Ops

theory Nonrelational_Ops
  imports
    Special_Ops
    Exec_Backward
    "Voblint_Framework.DG_Local_State_Spec"
    "Voblint_Exec.Default_St_Restriction_Refinement"
begin

unbundle default_st_syntax

section ‹The primitives one abstract value per variable is built from›

text ‹
  Say what an expression evaluates to, which comparisons the domain decides, how
  a guard refines its operands, how the two special calls combine two values,
  and every edge of a compiled graph is determined; the whole-value element is
  the class \<^const>‹top›. ‹nonrelational_ops› is that bundle of primitive choices, written
  once per domain. Everything else is derived from it: the guard filter on the
  executable store here, the abstract branch and the transfer in
  ‹Nonrelational_Transfer›, which certifies one such bundle.

  Two constructions follow from it here. ‹generic_enter_st_for› is procedure
  entry on the executable store: evaluate the actuals in the caller's state,
  reset the callee frame to the whole-value element, bind the formals.
  ‹generic_tf_st_for› is the per-edge executable step, and
  ‹generic_tf_st_for_commute› says it agrees with the abstract dispatcher
  ‹generic_tf_abs› on the function the executable store represents, provided the guard
  filter commutes with the abstract branch on the state at hand.

  ‹generic_tf_abs› takes the abstract branch as a separate argument so this
  commutation lemma needs no soundness locale. For a certified bundle the branch
  is not an independent choice: ‹sound_nonrelational_ops› instantiates
  it with the backward branch of ‹n_aval› and ‹n_refine› and discharges the
  guard obligation once, generically.
›

text ‹
  The bundle is constrained to ‹'a::{bot, top}› and the executable step to
  ‹'a::executable_domain›, never ‹'a::numeric_domain›. ‹numeric_domain› fixes
  ‹gamma› as a class operation, and code generation for a definition at that
  sort must resolve ‹gamma›'s code equation for the concrete type even though
  nothing here calls it. ‹ivl›'s ‹gamma_ivl› has no well-sorted code equation
  (‹int› is not of sort ‹enum›), so that unused obligation breaks unrelated
  ‹by eval› proofs downstream.
›

text ‹
  The comparisons a domain decides, each answering ‹None› when it cannot tell.
›

record 'a query_ops =
  q_less :: "'a ⇒ 'a ⇒ bool option"
  q_eq   :: "'a ⇒ 'a ⇒ bool option"

record ('a::"{bot, top}") nonrelational_ops =
  n_aval    :: "exp => (vname => 'a) => 'a"
  n_query   :: "'a query_ops"
  n_refine  :: "'a refine_ops"
  n_special :: "'a special_ops"

text ‹
  The guard filter on the executable store is derived from the evaluator and the
  refinement operations, never supplied: the bundle determines it.
›

abbreviation n_bfilter ::
  "'a::executable_domain nonrelational_ops
   ⇒ (vname ⇒ bool) ⇒ exp ⇒ bool ⇒ 'a default_st ⇒ 'a default_st" where
  "n_bfilter ops ≡ branch_st_with (n_aval ops) (n_refine ops)"

subsection ‹Procedure entry›

text ‹
  ‹generic_enter_st_for› opens a callee frame with every local at ‹top›, then
  binds the formals to the arguments evaluated in the caller's store.
›

definition generic_enter_st_for ::
    "'a::{bot, top} nonrelational_ops => (vname => bool) => call_info =>
       'a default_st => 'a default_st" where
  "generic_enter_st_for ops 𝒢 ci s =
     bind_formals_default_st 𝒢 (ci_formals ci)
       (map (λe. n_aval ops e (ρ⇘𝒢⇙ s)) (ci_args ci))
       (enter_frame_D_default_st top s)"

subsection ‹The per-edge step, on both stores›

text ‹
  ‹generic_tf_st_for› is the executable step on the split local/global store,
  routing each write through ‹location_of›. ‹generic_tf_abs› states the same
  edge semantics on a plain abstract state via ‹local_spec_step›.
›

fun generic_tf_st_for ::
    "'a::executable_domain nonrelational_ops => (vname => bool) => edge_action =>
       'a default_st => 'a default_st" where
    "generic_tf_st_for ops 𝒢 EA_Nop s = s"
  | "generic_tf_st_for ops 𝒢 (EA_Assign x a) s =
       s⟨location_of 𝒢 x := n_aval ops a (ρ⇘𝒢⇙ s)⟩"
  | "generic_tf_st_for ops 𝒢 (EA_Special sc x) s =
       s⟨location_of 𝒢 x :=
         (case sc of
            Nondet_Int => top
          | Min a b => special_min (n_special ops)
                         (n_aval ops a (ρ⇘𝒢⇙ s))
                         (n_aval ops b (ρ⇘𝒢⇙ s))
          | Max a b => special_max (n_special ops)
                         (n_aval ops a (ρ⇘𝒢⇙ s))
                         (n_aval ops b (ρ⇘𝒢⇙ s)))⟩"
  | "generic_tf_st_for ops 𝒢 (EA_Assume b) s = n_bfilter ops 𝒢 b True s"
  | "generic_tf_st_for ops 𝒢 (EA_AssumeNot b) s = n_bfilter ops 𝒢 b False s"
  | "generic_tf_st_for ops 𝒢 (EA_Body p) s = s"
  | "generic_tf_st_for ops 𝒢 (EA_Ret None p) s = s"
  | "generic_tf_st_for ops 𝒢 (EA_Ret (Some a) p) s =
       s⟨location_of 𝒢 ret_var := n_aval ops a (ρ⇘𝒢⇙ s)⟩"
  | "generic_tf_st_for ops 𝒢 (EA_Check l cnd) s = s"

definition generic_tf_abs ::
    "'a::{bot, top} nonrelational_ops => (exp => bool => 'a abs_state => 'a abs_state) =>
       edge_action => 'a abs_state => 'a abs_state" where
  "generic_tf_abs ops br =
     local_spec_step
       (λsigma. sigma)
       (λx a sigma. sigma(x := n_aval ops a sigma))
       (λsc x sigma. sigma(x := (case sc of
            Nondet_Int => top
          | Min a b => special_min (n_special ops) (n_aval ops a sigma) (n_aval ops b sigma)
          | Max a b => special_max (n_special ops) (n_aval ops a sigma) (n_aval ops b sigma))))
       br
       (λp sigma. sigma)
       (λeo p sigma. case eo of None => sigma | Some a => sigma(ret_var := n_aval ops a sigma))
       (λevt sigma. sigma)"

lemma generic_tf_abs_simps [simp]:
  "generic_tf_abs ops br EA_Nop sigma = sigma"
  "generic_tf_abs ops br (EA_Assign x a) sigma = sigma(x := n_aval ops a sigma)"
  "generic_tf_abs ops br (EA_Special sc x) sigma =
     sigma(x := (case sc of
        Nondet_Int => top
      | Min a b => special_min (n_special ops) (n_aval ops a sigma) (n_aval ops b sigma)
      | Max a b => special_max (n_special ops) (n_aval ops a sigma) (n_aval ops b sigma)))"
  "generic_tf_abs ops br (EA_Assume b) = br b True"
  "generic_tf_abs ops br (EA_AssumeNot b) = br b False"
  "generic_tf_abs ops br (EA_Body p) sigma = sigma"
  "generic_tf_abs ops br (EA_Ret None p) sigma = sigma"
  "generic_tf_abs ops br (EA_Ret (Some a) p) sigma = sigma(ret_var := n_aval ops a sigma)"
  "generic_tf_abs ops br (EA_Check l cnd) sigma = sigma"
  by (simp_all add: generic_tf_abs_def)

text ‹
  Every case but the guard rewrites by \<^const>‹default_st_to_fun›'s own
  update equation, which is what leaves the guard as the only obligation an
  instance still has to discharge.
›

theorem generic_tf_st_for_commute:
  fixes ops :: "'a::executable_domain nonrelational_ops"
  assumes branch:
    "⋀b pol. ρ⇘𝒢⇙ (n_bfilter ops 𝒢 b pol s) =
               br b pol (ρ⇘𝒢⇙ s)"
  shows
    "ρ⇘𝒢⇙ (generic_tf_st_for ops 𝒢 a s) =
     generic_tf_abs ops br a (ρ⇘𝒢⇙ s)"
proof (cases a)
  case EA_Nop
  then show ?thesis by simp
next
  case (EA_Assign x e)
  then show ?thesis by simp
next
  case (EA_Special sc x)
  then show ?thesis by (cases sc) simp_all
next
  case (EA_Assume b)
  then show ?thesis by (simp add: branch)
next
  case (EA_AssumeNot b)
  then show ?thesis by (simp add: branch)
next
  case (EA_Body p)
  then show ?thesis by simp
next
  case (EA_Ret eo p)
  then show ?thesis by (cases eo) simp_all
next
  case (EA_Check l cnd)
  then show ?thesis by simp
qed

unbundle no default_st_syntax

end