Theory Channel_Wrappers

theory Channel_Wrappers
  imports "Voblint_Framework.MCP_Spec"
begin

section ‹Consulting the answers at an assignment›

text ‹
  A component that was written without queries can still use them through a
  wrapper around one transfer. At ‹x = e› it asks for the value of ‹e›; if the
  answer is a single integer ‹n›, the wrapper assigns the literal ‹n› instead
  of evaluating ‹e› itself. The component's own assignment of that literal
  then covers the concrete successor, because ‹e› evaluates to ‹n› at every
  store the answer holds at.
›

definition assign_ask ::
  "(channel ⇒ vname ⇒ exp ⇒ 'D ⇒ 'D) ⇒ channel ⇒ vname ⇒ exp ⇒ 'D ⇒ 'D" where
  "assign_ask asn ch x e d =
     (case answer_const (ch (EvalInt e)) of
        Some n ⇒ asn ch x (N n) d
      | None ⇒ asn ch x e d)"

text ‹The wrapper keeps an assignment's law: where it substitutes the literal, the
  answer holds at the store, so the literal evaluates to what ‹e› does.›

lemma assign_ask_sound:
  assumes "sound_assign gm asn"
  shows "sound_assign gm (assign_ask asn)"
  unfolding sound_assign_def
proof (intro allI impI)
  fix ch x s y e
  assume s: "s ∈ gm x" and o: "eval_query.channel_holds ch s"
  have base: "s(y := ⟦e'⟧⇩e s) ∈ gm (asn ch y e' x)" for e'
    using assms s o unfolding sound_assign_def by blast
  show "s(y := ⟦e⟧⇩e s) ∈ gm (assign_ask asn ch y e x)"
  proof (cases "answer_const (ch (EvalInt e))")
    case None
    then show ?thesis using base[of e] by (simp add: assign_ask_def)
  next
    case (Some n)
    have "⟦e⟧⇩e s = n"
      by (rule eval_holds_constD[OF eval_query.channel_holdsD[OF o] Some])
    then show ?thesis using Some base[of "N n"] by (simp add: assign_ask_def)
  qed
qed


section ‹A component that asks at its assignments›

text ‹
  The same wrapper around a whole component: at every assignment it asks the
  channel for the value of the right-hand side and runs the assignment on the
  literal when the answer is a single integer. It changes neither the
  component's concretization nor its entry, so soundness, framing and a single
  entry carry over. Where every answer is \<^term>‹⊤›, as when no active
  analysis answers, it is the component itself.
›

definition ask_assign :: "'s local_spec ⇒ 's local_spec" where
  "ask_assign c = c⦇ls_assign := assign_ask (ls_assign c)⦈"

lemma ask_assign_step_cases:
  "ls_step (ask_assign c) ch a x = ls_step c ch a x
   ∨ (∃y e n. a = EA_Assign y e ∧ answer_const (ch (EvalInt e)) = Some n
        ∧ ls_step (ask_assign c) ch a x = ls_step c ch (EA_Assign y (N n)) x)"
  by (cases a) (auto simp: ask_assign_def assign_ask_def split: option.splits)

lemma answer_const_top [simp]: "answer_const ⊤ = None"
  by (simp add: top_query_lift_def)

lemma single_entry_ask_assign: "single_entry c ⟹ single_entry (ask_assign c)"
  by (simp add: single_entry_def ask_assign_def)

theorem ask_assign_frame:
  assumes frame: "mcp_frame c g"
  shows "mcp_frame (ask_assign c) g"
proof -
  have st: "g (ls_step c ch a x) = g x" for ch a x
    using frame unfolding mcp_frame_def by blast
  have "g (ls_step (ask_assign c) ch a x) = g x" for ch a x
    using ask_assign_step_cases[of c ch a x] st by metis
  then show ?thesis
    using frame unfolding mcp_frame_def by (simp add: ask_assign_def)
qed

theorem ask_assign_sound:
  assumes sound: "sound_local_spec 𝒢 gm c"
  shows "sound_local_spec 𝒢 gm (ask_assign c)"
  unfolding ask_assign_def
  by (rule sound_local_spec_update_assign[OF sound
        assign_ask_sound[OF sound_local_spec_assignD[OF sound]]])

end