Theory Voblint_Analysis_Relational.Rel_Order_Local

theory Rel_Order_Local
  imports Rel_Order_Domain "Voblint_Framework.MCP_Spec"
begin

section ‹The order carrier as a component that asks›

text ‹
  \<^const>‹rel_order_spec› reads and publishes the global channel, so it is not a
  local specification and cannot join the combination of cooperating analyses. This
  theory gives the same carrier a local-only form. Intraprocedurally it is the
  order analysis of \<^theory>‹Voblint_Analysis_Relational.Rel_Order_Domain›, with
  one addition: after an assignment it asks the query channel how the assigned value
  compares with the other variables, and records every order the answer fixes.
  At calls it is deliberately coarse, entering and returning with no facts, so
  that the component studies cooperation and not relational call boundaries.
›

subsection ‹Answering queries from the order›

text ‹
  A pair ‹(x, y)› means ‹s x ≤ s y›. It therefore decides ‹x <= y› and
  ‹y >= x› as true, ‹y < x› and ‹x > y› as false, and with the reverse pair
  also ‹x == y› as true and ‹x != y› as false. A comparison evaluates to ‹1›
  when true and ‹0› when false, so the answers are the exact integers ‹1› and ‹0›. Every
  other query is answered with ‹⊤›, the claim that holds of every store.
›

text ‹
  ‹relc_le d a b› holds when ‹a› and ‹b› are variables whose order ‹d› records,
  or the same variable. The reflexive case lets a copy ‹x = y› learn both orders
  between ‹x› and ‹y› from the channel's own answer to ‹y <= y›.
›

fun var_of :: "exp ⇒ vname option" where
  "var_of (V x) = Some x"
| "var_of _ = None"

definition relc_le :: "relc ⇒ exp ⇒ exp ⇒ bool" where
  "relc_le d a b =
     (case (var_of a, var_of b) of (Some x, Some y) ⇒ x = y ∨ relc_has x y d | _ ⇒ False)"

definition relc_eval :: "relc ⇒ exp ⇒ answer" where
  "relc_eval d e =
     (case e of
        LessEq a b ⇒ if relc_le d a b then answer_of_int 1 else ⊤
      | GreaterEq a b ⇒ if relc_le d b a then answer_of_int 1 else ⊤
      | Less a b ⇒ if relc_le d b a then answer_of_int 0 else ⊤
      | Greater a b ⇒ if relc_le d a b then answer_of_int 0 else ⊤
      | exp.Eq a b ⇒ if relc_le d a b ∧ relc_le d b a then answer_of_int 1 else ⊤
      | NotEq a b ⇒ if relc_le d a b ∧ relc_le d b a then answer_of_int 0 else ⊤
      | _ ⇒ ⊤)"

fun relc_qry :: "relc ⇒ channel" where
  "relc_qry d (EvalInt e) = relc_eval d e"

lemma relc_has_sound: "s ∈ γ d ⟹ relc_has x y d ⟹ s x ≤ s y"
  by (cases d) auto

lemma var_of_SomeD: "var_of a = Some x ⟹ a = V x"
  by (cases a) simp_all

lemma relc_le_sound: "s ∈ γ d ⟹ relc_le d a b ⟹ ⟦a⟧⇩e s ≤ ⟦b⟧⇩e s"
  by (auto simp: relc_le_def split: option.splits dest!: var_of_SomeD
      dest: relc_has_sound)

lemma relc_eval_sound:
  "s ∈ γ d ⟹ ⟦e⟧⇩e s ∈ gamma_answer (relc_eval d e)"
  by (cases e) (auto simp: relc_eval_def
      dest: relc_le_sound intro: order_antisym)

lemma relc_qry_sound: "s ∈ γ d ⟹ eval_holds q (relc_qry d q) s"
  by (cases q) (simp add: relc_eval_sound)

subsection ‹Learning orders from the query channel›

text ‹
  At ‹x = e› the question is asked about the state before the assignment, where
  ‹e› evaluates to the new value of ‹x› and every other variable keeps its
  value. The exact answer ‹1› to ‹e <= y› therefore makes ‹(x, y)› true
  afterwards, and ‹y <= e› makes ‹(y, x)› true. The candidate partners are the
  variables in ‹ys›, a parameter so that the construction stays executable.
›

definition relc_learn :: "channel ⇒ vname list ⇒ vname ⇒ exp ⇒ relc ⇒ relc" where
  "relc_learn ch ys x e d =
     (case d of
        RelBot ⇒ RelBot
      | RelC ps ⇒ RelC (ps
          ∪ set (map (λy. (x, y))
                (filter (λy. y ≠ x ∧ answer_const (ch (EvalInt (LessEq e (V y)))) = Some 1) ys))
          ∪ set (map (λy. (y, x))
                (filter (λy. y ≠ x ∧ answer_const (ch (EvalInt (LessEq (V y) e))) = Some 1) ys))))"

lemma relc_learn_sound:
  assumes "s(x := ⟦e⟧⇩e s) ∈ γ d"
    and "eval_query.channel_holds ch s"
  shows "s(x := ⟦e⟧⇩e s) ∈ γ (relc_learn ch ys x e d)"
proof (cases d)
  case RelBot
  with assms(1) show ?thesis by simp
next
  case (RelC ps)
  have up: "⟦e⟧⇩e s ≤ s y" if "answer_const (ch (EvalInt (LessEq e (V y)))) = Some 1" for y
    using eval_holds_constD[OF eval_query.channel_holdsD[OF assms(2)] that]
    by (simp split: if_splits)
  have down: "s y ≤ ⟦e⟧⇩e s" if "answer_const (ch (EvalInt (LessEq (V y) e))) = Some 1" for y
    using eval_holds_constD[OF eval_query.channel_holdsD[OF assms(2)] that]
    by (simp split: if_splits)
  show ?thesis
    using assms(1) RelC up down by (auto simp: relc_learn_def)
qed

subsection ‹The component›

text ‹
  The order analysis as a component of the combined state, over the variables
  ‹ys› it relates. It starts from the conservative local specification: skip,
  body and events keep the relation, and the first return stage keeps the
  caller's. It supplies the operations without a default -- assignments ask and
  learn, the callee starts from the empty relation, and the return keeps
  nothing, which is sound and imprecise by design -- and overrides the handler
  and the branch, where it decides more than the default.
›

definition relc_ret :: "exp option ⇒ relc ⇒ relc" where
  "relc_ret eo d = (case eo of None ⇒ d | Some a ⇒ forget_relc ret_var d)"

definition order_spec :: "vname list ⇒ relc local_spec" where
  "order_spec ys = (conservative_local_spec
       (λch x e d. relc_learn ch ys x e (forget_relc x d))
       (λch sc x d. forget_relc x d)
       (λch eo p d. relc_ret eo d)
       (λch ci p. [(fst p, ⊤)])
       (λch' ci d de. ⊤))
     ⦇ls_query := (λch. relc_qry), ls_branch := (λch b pol d. relc_branch_step b pol d)⦈"

theorem order_spec_sound: "sound_local_spec 𝒢 gamma_relc (order_spec ys)"
proof -
  have special: "sound_special gamma_relc (λch sc x d. forget_relc x d)"
    unfolding sound_special_def
  proof (intro allI impI)
    fix ch d s sc x t
    assume "s ∈ γ (d :: relc)" "t ∈ special_step sc x s"
    then show "t ∈ γ (forget_relc x d)" by (cases sc) auto
  qed
  have base: "sound_local_spec 𝒢 gamma_relc (conservative_local_spec
       (λch x e d. relc_learn ch ys x e (forget_relc x d)) (λch sc x d. forget_relc x d)
       (λch eo p d. relc_ret eo d) (λch ci p. [(fst p, ⊤)]) (λch' ci d de. ⊤))"
    by (rule sound_conservative_local_spec[OF gamma_relc_mono _ special])
       (auto simp: sound_assign_def sound_return_def sound_enter_def relc_ret_def
          sound_combine_env_identity split: option.splits intro!: relc_learn_sound)
  show ?thesis
    unfolding order_spec_def
    by (intro sound_local_spec_update_branch[OF sound_local_spec_update_query[OF base]])
       (auto simp: sound_query_def sound_branch_def relc_branch_step_def relc_qry_sound)
qed

lemma single_entry_order_spec: "single_entry (order_spec ys)"
  by (simp add: single_entry_def order_spec_def conservative_local_spec_def)

end