Theory Voblint_Analysis_Relational.Rel_Order_Domain

theory Rel_Order_Domain
  imports "Voblint_Framework.DG_Spec_Sound" "Voblint_Framework.DG_Indexed_Generator"
    "Voblint_Framework.State_Restriction" "Voblint_Domain.Order_Lattice"
begin

section ‹A minimal relational analysis for \<^const>‹analysis_contract››

text ‹
  The analysis over \<^typ>‹relc›, the order lattice of
  \<^theory>‹Voblint_Domain.Order_Lattice›. The purpose of this file is not a useful
  analysis. It demonstrates that a non-‹abs_state› carrier discharges
  \<^locale>‹analysis_contract› with zero changes to the DG framework. Every transfer
  below is deliberately the most imprecise sound choice (forget on assign, havoc on
  call) except for a precise ‹assume_step›/‹assume_not_step› pair, which is
  enough to make the carrier genuinely relational.
›

subsection ‹Local and global state together›

definition gammaDG_relc :: "relc ⇒ relc ⇒ store set" where
  "gammaDG_relc d g = γ d ∩ γ g"

lemma gammaDG_relc_top [simp]: "gammaDG_relc ⊤ ⊤ = UNIV"
  unfolding gammaDG_relc_def by simp

subsection ‹Refining bare-variable comparisons›

text ‹
  Only guards between two bare variables refine a ‹relc›. On the true branch
  ‹assume_step› adds ‹(x, y)› for a guard implying that ‹x› is at most ‹y›;
  every other guard leaves the state unchanged.
›

definition assume_step :: "exp ⇒ relc ⇒ relc" where
  "assume_step b d =
     (case d of
        RelBot ⇒ RelBot
      | RelC ps ⇒
          (case b of
             Less (V x) (V y) ⇒ RelC (insert (x, y) ps)
           | LessEq (V x) (V y) ⇒ RelC (insert (x, y) ps)
           | Greater (V x) (V y) ⇒ RelC (insert (y, x) ps)
           | GreaterEq (V x) (V y) ⇒ RelC (insert (y, x) ps)
           | Eq (V x) (V y) ⇒ RelC (insert (x, y) (insert (y, x) ps))
           | _ ⇒ RelC ps))"

lemma assume_step_sound[intro]:
  assumes "s ∈ γ d" "truthy (⟦b⟧⇩e s)"
  shows "s ∈ γ (assume_step b d)"
  using assms
  by (cases d; cases b) (auto simp: assume_step_def split: exp.splits if_splits)

text ‹The false branch records the reversed order.  Equality records both
  directions, on the true branch of ‹Eq› or the false branch of ‹NotEq›.
  Disequality alone cannot be represented by a conjunction of weak orders.›

definition assume_not_step :: "exp ⇒ relc ⇒ relc" where
  "assume_not_step b d =
     (case d of
        RelBot ⇒ RelBot
      | RelC ps ⇒
          (case b of
             Less (V x) (V y) ⇒ RelC (insert (y, x) ps)
           | LessEq (V x) (V y) ⇒ RelC (insert (y, x) ps)
           | Greater (V x) (V y) ⇒ RelC (insert (x, y) ps)
           | GreaterEq (V x) (V y) ⇒ RelC (insert (x, y) ps)
           | NotEq (V x) (V y) ⇒ RelC (insert (x, y) (insert (y, x) ps))
           | _ ⇒ RelC ps))"

lemma assume_not_step_sound[intro]:
  assumes "s ∈ γ d" "¬ truthy (⟦b⟧⇩e s)"
  shows "s ∈ γ (assume_not_step b d)"
  using assms
  by (cases d; cases b) (auto simp: assume_not_step_def split: exp.splits if_splits)

subsection ‹The transfer functions›

text ‹Every step except the comparison refinements above
  is sound by forgetting or by leaving the carrier untouched -- deliberately
  imprecise: no closure, no normalization, havoc-based calls.›

definition relc_skip :: "relc ⇒ relc ⇒ relc × relc" where
  "relc_skip d g = (g, d)"

definition relc_assign :: "vname ⇒ exp ⇒ relc ⇒ relc ⇒ relc × relc" where
  "relc_assign x e d g = (forget_relc x g, forget_relc x d)"

definition relc_body :: "pname ⇒ relc ⇒ relc ⇒ relc × relc" where
  "relc_body p d g = (g, d)"

text ‹
  ‹return› reuses the same forget-based imprecision ‹relc_assign› already
  applies to every ordinary assignment: with an expression, forget ‹ret_var›;
  without one, behave like ‹skip›.
›
definition relc_return :: "exp option ⇒ pname ⇒ relc ⇒ relc ⇒ relc × relc" where
  "relc_return e p d g =
     (case e of None ⇒ relc_skip d g
      | Some a ⇒ relc_assign ret_var a d g)"

definition relc_special :: "special_call ⇒ vname ⇒ relc ⇒ relc ⇒ relc × relc" where
  "relc_special sc x d g = (forget_relc x g, forget_relc x d)"

text ‹A check observes its condition but never refines the state, matching
  ‹relc_skip›'s own imprecision.›
definition relc_event :: "analysis_event ⇒ relc ⇒ relc ⇒ relc × relc" where
  "relc_event ev d g = (g, d)"

text ‹
  ‹assume_step›/‹assume_not_step› stay separate, genuinely asymmetric
  operations (‹x < y› vs.\ its mirror ‹y ≤ x› insert different pairs, not
  the same formula under a polarity flag); only the interface-level dispatch
  consolidates them into one polarity-parametrized branch operation.
›
definition relc_branch_step :: "exp ⇒ bool ⇒ relc ⇒ relc" where
  "relc_branch_step b pol d = (if pol then assume_step b d else assume_not_step b d)"

text ‹The relational counterpart of ‹bfilter_sound›, in the same shape: refining
  at a guard keeps every store at which the guard has the required truth value.›
lemma relc_branch_step_sound [intro]:
  assumes "s ∈ γ d" "truthy (⟦b⟧⇩e s) = pol"
  shows "s ∈ γ (relc_branch_step b pol d)"
  using assms by (cases pol) (auto simp: relc_branch_step_def)

definition relc_branch :: "exp ⇒ bool ⇒ relc ⇒ relc ⇒ relc × relc" where
  "relc_branch b pol d g = (g, relc_branch_step b pol d)"

definition relc_enter :: "call_info ⇒ relc ⇒ relc ⇒ relc × relc" where
  "relc_enter ci dc g = (⊤, ⊤)"

text ‹
  The caller continuation is the identity.  This carrier discards every caller
  relation at its environment merge anyway, so there is no call-side
  invalidation for a continuation to express: filtering before a merge that
  already returns \<^term>‹⊤ :: relc› would be indistinguishable from not filtering.
  Keeping it identity leaves this instance the least interesting sound one, which
  is its purpose.
›
definition relc_caller_cont :: "call_info ⇒ relc ⇒ relc ⇒ relc" where
  "relc_caller_cont ci dc g = dc"

definition relc_combine_env :: "call_info ⇒ relc ⇒ relc ⇒ relc ⇒ relc × relc" where
  "relc_combine_env ci dc de g = (⊤, ⊤)"

definition relc_combine_assign ::
  "call_info ⇒ relc ⇒ relc ⇒ relc × relc ⇒ relc × relc"
where
  "relc_combine_assign ci de g merged = merged"

text ‹
  Unlike the local-only domains, this one really uses the global channel:
  \<^const>‹relc_special› forgets the assigned name on both halves, and entry
  and the environment merge reset the shared relation to \<^term>‹⊤ :: relc›.
  Its transfers are therefore written as a read-compute-publish sequence.

  ‹relc_transfer› is the adapter that turns one of this file's
  ‹d ⇒ g ⇒ (g, d)› operations into a manager transfer: query the shared
  relation, run the operation, publish its global half, answer with its local
  half. The manager interface does not require that pairing shape; here it is
  one domain's private convenience, which is the point.
›

definition relc_transfer ::
  "(relc ⇒ relc ⇒ relc × relc) ⇒ ('x,'k,unit,relc,relc) man_transfer"
where
  "relc_transfer f m =
     do {
       g ← man_global m ();
       let r = f (man_local m) g;
       _ ← man_sideg m () (fst r);
       sp_return (snd r)
     }"

text ‹Entry at this carrier: the same global read and publication, answering the one
  alternative whose continuation is the caller value unchanged.›

definition relc_enter_transfer ::
  "(relc ⇒ relc ⇒ relc × relc) ⇒ ('x,'k,unit,relc,relc) man_enter_transfer"
where
  "relc_enter_transfer f m =
     do {
       g ← man_global m ();
       let r = f (man_local m) g;
       _ ← man_sideg m () (fst r);
       sp_return [(man_local m, snd r)]
     }"

definition relc_combine_transfer ::
  "(relc ⇒ relc ⇒ relc ⇒ relc × relc) ⇒ ('x,'k,unit,relc,relc) man_combine_transfer"
where
  "relc_combine_transfer f m de =
     do {
       g ← man_global m ();
       let r = f (man_local m) de g;
       _ ← man_sideg m () (fst r);
       sp_return (snd r)
     }"

text ‹The observations of a compiled ‹relc_transfer›: its answer is the operation's
  local half, and what it publishes at the routed key is the global half. These are
  what \<^locale>‹analysis_contract› is stated against.›

lemma traverse_relc_transfer [simp]:
  "dg_local (traverse_program (transfer_program (relc_transfer f) src (λ_. gk)) τ)
     = snd (f (dg_local (τ src)) (dg_global (τ (Inr gk))))"
  by (cases src)
     (simp_all add: transfer_program_def transfer_program_at_def relc_transfer_def
        mk_dg_man_def dg_read_at_def dg_read_global_def dg_sideg_def sp_bind_assoc
        Let_def)

lemma sides_relc_transfer [simp]:
  "dg_global (sides_of_program (transfer_program (relc_transfer f) src (λ_. gk)) τ (Inr gk))
     = fst (f (dg_local (τ src)) (dg_global (τ (Inr gk))))"
  by (cases src)
     (simp_all add: transfer_program_def transfer_program_at_def relc_transfer_def
        mk_dg_man_def dg_read_at_def dg_read_global_def dg_sideg_def sp_bind_assoc
        Let_def)

text ‹The order analysis never asks, so the query channel the generator installs
  leaves its transfers unchanged.›

lemma relc_transfer_outer_man [simp]:
  "relc_transfer f (outer_man Q m) = relc_transfer f m"
  by (simp add: relc_transfer_def)

definition rel_order_spec :: "('x,'k,unit,relc,relc) dg_spec" where
  "rel_order_spec = local_dg_spec_template⦇
     dgs_skip := relc_transfer relc_skip,
     dgs_assign := (λx e. relc_transfer (relc_assign x e)),
     dgs_special := (λsc x. relc_transfer (relc_special sc x)),
     dgs_branch := (λb pol. relc_transfer (relc_branch b pol)),
     dgs_body := (λp. relc_transfer (relc_body p)),
     dgs_return := (λe p. relc_transfer (relc_return e p)),
     dgs_enter := (λci. relc_enter_transfer (relc_enter ci)),
     dgs_event := (λev. relc_transfer (relc_event ev)),
     dgs_combine_env := (λci. relc_combine_transfer (relc_combine_env ci))
   ⦈"

text ‹Expand the template and transfer in this code equation so the argument-free
  specification is a record of functions in generated ML. This avoids the value
  restriction on record updates without inlining the specification into its callers.›

lemmas [code] =
  rel_order_spec_def[unfolded local_dg_spec_template_def relc_transfer_def, simplified]

text ‹Every field reads the shared slot, publishes once and answers, so the
  specification runs its continuation once wherever the generator runs it.›

lemma dg_spec_wf_rel_order_spec [intro, simp]: "dg_spec_wf rel_order_spec"
proof (unfold dg_spec_wf_def, intro conjI allI impI)
  fix a :: edge_action and d :: relc and unknown_of :: "unit ⇒ 'b" and A
  show "sp_wf (dg_spec_step rel_order_spec a ((mk_dg_man d unknown_of)⦇man_ask := A⦈))"
    by (cases a) (auto simp: rel_order_spec_def relc_transfer_def Let_def mk_dg_man_def)
next
  fix d :: relc and unknown_of :: "unit ⇒ 'b" and A q
  show "sp_wf (dgs_query rel_order_spec ((mk_dg_man d unknown_of)⦇man_ask := A⦈) q)"
    by (simp add: rel_order_spec_def)
next
  fix ci and d :: relc and unknown_of :: "unit ⇒ 'b"
  show "sp_wf (enter⇧♯ rel_order_spec ci (mk_dg_man d unknown_of))"
    by (auto simp: rel_order_spec_def relc_enter_transfer_def Let_def)
next
  fix ci and d :: relc and unknown_of :: "unit ⇒ 'b" and ex :: relc
  show "sp_wf (dg_spec_combine_transfer rel_order_spec ci (mk_dg_man d unknown_of) ex)"
    by (auto simp: rel_order_spec_def dg_spec_combine_transfer_def relc_combine_transfer_def
        local_combine_transfer_def Let_def)
qed

named_theorems rel_order_simps

declare
  relc_branch_def     [rel_order_simps]
  relc_branch_step_def    [rel_order_simps]
  relc_skip_def       [rel_order_simps]
  relc_body_def       [rel_order_simps]
  relc_return_def     [rel_order_simps]
  relc_event_def      [rel_order_simps]
  rel_order_spec_def     [rel_order_simps]
  gammaDG_relc_def        [rel_order_simps]
  relc_assign_def     [rel_order_simps]
  relc_special_def    [rel_order_simps]

subsection ‹Per-edge soundness›

text ‹
  Each edge operation over-approximates the concrete edge semantics on
  ‹gammaDG_relc›, the stores both the local and the global component describe.
  Assignments and special calls forget every pair that mentions the target.
›

lemma relc_skip_sound[intro]:
  "edge_collect EA_Nop (gammaDG_relc d g) ⊆
     (case relc_skip d g of (g', d') ⇒ gammaDG_relc d' g')"
  unfolding relc_skip_def by simp

lemma relc_assign_sound[intro]:
  "edge_collect (EA_Assign x e) (gammaDG_relc d g) ⊆
     (case relc_assign x e d g of (g', d') ⇒ gammaDG_relc d' g')"
proof -
  have "edge_collect (EA_Assign x e) (gammaDG_relc d g)
      = {s(x := ⟦e⟧⇩e s) | s. s ∈ gammaDG_relc d g}"
    by simp
  also have "... ⊆ γ (forget_relc x d) ∩ γ (forget_relc x g)"
    using forget_relc_sound unfolding gammaDG_relc_def by blast
  finally show ?thesis
    unfolding relc_assign_def gammaDG_relc_def by simp
qed

lemma relc_special_sound[intro]:
  "edge_collect (EA_Special sc x) (gammaDG_relc d g) ⊆
     (case relc_special sc x d g of (g', d') ⇒ gammaDG_relc d' g')"
proof -
  have "edge_collect (EA_Special sc x) (gammaDG_relc d g)
      ⊆ {s(x := v) | s v. s ∈ gammaDG_relc d g}"
    by (cases sc) auto
  also have "... ⊆ γ (forget_relc x d) ∩ γ (forget_relc x g)"
    using forget_relc_sound unfolding gammaDG_relc_def by blast
  finally show ?thesis
    unfolding relc_special_def gammaDG_relc_def by simp
qed

lemma relc_branch_sound_True[intro]:
  "edge_collect (EA_Assume b) (gammaDG_relc d g) ⊆
     (case relc_branch b True d g of (g', d') ⇒ gammaDG_relc d' g')"
proof -
  have "edge_collect (EA_Assume b) (gammaDG_relc d g)
      = {s. s ∈ gammaDG_relc d g ∧ truthy (⟦b⟧⇩e s)}"
    by simp
  also have "... ⊆ γ (assume_step b d) ∩ γ g"
    using assume_step_sound unfolding gammaDG_relc_def by blast
  finally show ?thesis
    unfolding relc_branch_def relc_branch_step_def gammaDG_relc_def by simp
qed

lemma relc_branch_sound_False[intro]:
  "edge_collect (EA_AssumeNot b) (gammaDG_relc d g) ⊆
     (case relc_branch b False d g of (g', d') ⇒ gammaDG_relc d' g')"
proof -
  have "edge_collect (EA_AssumeNot b) (gammaDG_relc d g)
      = {s. s ∈ gammaDG_relc d g ∧ ¬ truthy (⟦b⟧⇩e s)}"
    by simp
  also have "... ⊆ γ (assume_not_step b d) ∩ γ g"
    using assume_not_step_sound unfolding gammaDG_relc_def by blast
  finally show ?thesis
    unfolding relc_branch_def relc_branch_step_def gammaDG_relc_def by simp
qed

lemma relc_return_sound[intro]:
  "edge_collect (EA_Ret e p) (gammaDG_relc d g) ⊆
     (case relc_return e p d g of (g', d') ⇒ gammaDG_relc d' g')"
proof (cases e)
  case None
  then show ?thesis
    by (simp add: relc_return_def relc_skip_def)
next
  case (Some a)
  have "edge_collect (EA_Ret (Some a) p) (gammaDG_relc d g)
      = {s(ret_var := ⟦a⟧⇩e s) | s. s ∈ gammaDG_relc d g}"
    by simp
  also have "... ⊆ γ (forget_relc ret_var d) ∩ γ (forget_relc ret_var g)"
    using forget_relc_sound unfolding gammaDG_relc_def by blast
  finally show ?thesis
    using Some
    by (simp add: relc_return_def relc_assign_def gammaDG_relc_def)
qed

text ‹The edge dispatch as one pure pairing operation, so the specification's
  compiled step reduces to \<^const>‹relc_transfer› of it.›

fun relc_step_for :: "edge_action ⇒ relc ⇒ relc ⇒ relc × relc" where
  "relc_step_for EA_Nop = relc_skip"
| "relc_step_for (EA_Assign x e) = relc_assign x e"
| "relc_step_for (EA_Special sc x) = relc_special sc x"
| "relc_step_for (EA_Assume b) = relc_branch b True"
| "relc_step_for (EA_AssumeNot b) = relc_branch b False"
| "relc_step_for (EA_Body p) = relc_body p"
| "relc_step_for (EA_Ret e p) = relc_return e p"
| "relc_step_for (EA_Check l cnd) = relc_event (Check_Event l cnd)"

lemma dg_spec_step_rel_order_spec [simp]:
  "dg_spec_step rel_order_spec a = relc_transfer (relc_step_for a)"
  unfolding rel_order_spec_def by (cases a) simp_all

lemma dgs_enter_rel_order_spec [simp]:
  "enter⇧♯ rel_order_spec ci = relc_enter_transfer (relc_enter ci)"
  unfolding rel_order_spec_def by simp

lemma relc_step_sound:
  "edge_collect a (gammaDG_relc d g) ⊆
     (case relc_step_for a d g of (g', d') ⇒ gammaDG_relc d' g')"
  by (cases a) (auto simp add: rel_order_simps split: option.splits)

subsection ‹Call-entry and combine soundness -- havoc-based, both trivial via ‹⊤››

text ‹The composed return pipeline: ‹combine_assign› keeps the template's
  identity default, so the whole combine is the environment merge, which resets both halves
  to \<^term>‹⊤ :: relc›.›

lemma dg_spec_combine_transfer_rel_order_spec [simp]:
  "dg_spec_combine_transfer rel_order_spec ci = relc_combine_transfer (relc_combine_env ci)"
  unfolding dg_spec_combine_transfer_def rel_order_spec_def
  by (intro ext)
     (simp add: local_transfer_def local_combine_transfer_def relc_combine_transfer_def)

lemma traverse_relc_combine [simp]:
  "dg_local (traverse_program
             (combine_transfer_program (relc_combine_transfer f) src_cc src_ex (λ_. gk)) τ)
     = snd (f (dg_local (τ src_cc)) (dg_local (τ src_ex)) (dg_global (τ (Inr gk))))"
  by (cases src_cc; cases src_ex)
     (simp_all add: combine_transfer_program_def combine_program_at_def relc_combine_transfer_def
        mk_dg_man_def dg_read_at_def dg_read_global_def dg_sideg_def sp_bind_assoc Let_def)

lemma sides_relc_combine [simp]:
  "dg_global (sides_of_program
            (combine_transfer_program (relc_combine_transfer f) src_cc src_ex (λ_. gk))
            τ (Inr gk))
     = fst (f (dg_local (τ src_cc)) (dg_local (τ src_ex)) (dg_global (τ (Inr gk))))"
  by (cases src_cc; cases src_ex)
     (simp_all add: combine_transfer_program_def combine_program_at_def relc_combine_transfer_def
        mk_dg_man_def dg_read_at_def dg_read_global_def dg_sideg_def sp_bind_assoc Let_def)

subsection ‹The interpretation›

text ‹
  Interpreting ‹analysis_contract› at ‹rel_order_spec› discharges the framework's
  obligations: a well-formed spec, monotone concretization, and sound edge and
  combine transfers, each from the per-edge lemmas above.
›

interpretation rel_order: analysis_contract rel_order_spec "λd e. gammaDG_relc d (e ())" 𝒢
proof (rule analysis_contract_unitI)
  show "dg_spec_wf rel_order_spec" by (rule dg_spec_wf_rel_order_spec)
next
  fix d d' :: relc and g g' :: relc
  assume "d ≤ d'" "g ≤ g'"
  then show "gammaDG_relc d g ⊆ gammaDG_relc d' g'"
    using gamma_relc_mono unfolding gammaDG_relc_def by blast
next
  fix a and τ :: "'a + 'b ⇒ (relc, relc) dg_state" and src gk
  show "edge_collect a (gammaDG_relc (dg_local (τ src)) (dg_global (τ (Inr gk))))
          ⊆ gammaDG_relc
              (edge_out rel_order_spec a src (λ_. gk) τ)
              (dg_global (sides_of_program (dg_spec_edge_program rel_order_spec a src (λ_. gk))
                        τ (Inr gk)))"
    using relc_step_sound[of a "dg_local (τ src)" "dg_global (τ (Inr gk))"]
    by (simp add: dg_spec_edge_program_def split: prod.splits)
next
  fix s t dc de and τ :: "'a + 'b ⇒ (relc, relc) dg_state" and gk ci
  show "⟦s ∈ gammaDG_relc dc (dg_global (τ (Inr gk)));
         t ∈ gammaDG_relc de (dg_global (τ (Inr gk)))⟧ ⟹
          combine_collect 𝒢 (ci_dst ci) s t
            ∈ gammaDG_relc
                (dg_local (traverse_rhs (sp_compile_with (λd. DG d bot)
                   (dg_spec_combine_transfer rel_order_spec ci
                      (mk_dg_man dc (λ_. gk)) de)) τ))
                (dg_global (sides_of_rhs (sp_compile_with (λd. DG d bot)
                   (dg_spec_combine_transfer rel_order_spec ci
                      (mk_dg_man dc (λ_. gk)) de)) τ (Inr gk)))"
    by (simp add: relc_combine_transfer_def mk_dg_man_def dg_read_global_def
        dg_sideg_def sp_bind_assoc Let_def relc_combine_env_def)
qed

end