Theory DG_Local_State_Spec

theory DG_Local_State_Spec
  imports "Voblint_Framework.MCP_Spec" Transfer_Algebra "Voblint_Domain.Nonrelational_Reachability"
begin

section ‹What a whole-state analysis supplies, and when it is sound›

text ‹
  A Base-style analysis answers from one pointwise abstract state per program
  point and never touches a global: its transfers read the manager's local value,
  compute, and return, so the compiled equations carry no ‹QueryG› and no
  ‹Side›. Such an analysis supplies seven pure edge-operation families ---
  skip, assign, special, branch, body, return, event, with branch covering both
  ‹EA_Assume› and ‹EA_AssumeNot› --- plus the callee entry, and this theory
  turns them into a
  \<^type>‹dg_spec› two ways: ‹state_dg_spec› on the raw
  states, and ‹lifted_state_dg_spec› on states carrying an
  explicit unreachable value, where a dead point collapses to \<^const>‹Bot›
  before any transfer runs.

  ‹sound_nonrelational_transfer› is the contract those operations owe: every
  concrete transition the collecting semantics allows must land inside the
  concretization of what the corresponding operation computes. A domain discharges
  it once, by ‹interpretation›, and ‹state_dg_spec› becomes a sound
  specification. ‹lifted_state_dg_spec› is the structural target its
  executable mirror refines; ‹DG_Local_State_Exec_Refinement› proves that
  mirror sound directly.

  The call boundary is fixed here rather than supplied. A call answers exactly one
  alternative, whose continuation is the caller value unchanged. That is sound
  because of what the fixed combine does later, not because of anything about the
  carrier: the continuation is kept for its ∗‹local› part, and whatever the
  callee may have invalidated --- the globals --- is taken from the callee exit
  instead. A nonrelational caller still holds global facts a callee can
  invalidate; it is the combine protocol that repairs them, not the absence of
  relations. The environment stage passes that continuation through, and the
  whole return happens in the assign stage as
  \<^const>‹combine_collect_abs›: caller locals, callee globals, and the callee's
  \<^const>‹ret_var› written to the destination. An analysis that needs a
  different boundary overrides those three fields of its own specification instead
  of using these builders, the way ‹varEq› supplies its own
  ‹combine_env› upstream.
›

subsection ‹The transfer contract›

text ‹One assumption per operation, each an inference rule from a concrete store
  in an abstract state's concretization to the corresponding concrete successor in
  the operation's own result. A domain proves one fact per operation about its
  own functions and interprets this locale once; nothing below asks it for
  more.›

locale sound_nonrelational_transfer =
  fixes 𝒢 :: "vname ⇒ bool"
    and sk :: "'a::numeric_domain abs_state ⇒ 'a abs_state"
    and asn :: "vname ⇒ exp ⇒ 'a abs_state ⇒ 'a abs_state"
    and sp :: "special_call ⇒ vname ⇒ 'a abs_state ⇒ 'a abs_state"
    and br :: "exp ⇒ bool ⇒ 'a abs_state ⇒ 'a abs_state"
    and bd :: "pname ⇒ 'a abs_state ⇒ 'a abs_state"
    and rt :: "exp option ⇒ pname ⇒ 'a abs_state ⇒ 'a abs_state"
    and en :: "call_info ⇒ 'a abs_state ⇒ 'a abs_state"
    and ev :: "analysis_event ⇒ 'a abs_state ⇒ 'a abs_state"
  assumes tf_sound_assign_for[intro]:
    "s ∈ γ d ⟹ s(x := ⟦a⟧⇩e s) ∈ γ (asn x a d)"
  assumes tf_sound_special_for[intro]:
    "s ∈ γ d ⟹ special_result sc s v ⟹ s(x := v) ∈ γ (sp sc x d)"
  assumes tf_sound_branch_for[intro]:
    "s ∈ γ d ⟹ truthy (⟦b⟧⇩e s) = pol ⟹ s ∈ γ (br b pol d)"
  assumes tf_sound_skip_for[intro]:
    "s ∈ γ d ⟹ s ∈ γ (sk d)"
  assumes tf_sound_body_for[intro]:
    "s ∈ γ d ⟹ s ∈ γ (bd p d)"
  assumes tf_sound_return_for[intro]:
    "s ∈ γ d ⟹
       s(ret_var := (case e of None ⇒ s ret_var | Some a ⇒ ⟦a⟧⇩e s))
         ∈ γ (rt e p d)"
  assumes tf_sound_enter_entry_for[intro]:
    "s ∈ γ d ⟹
       bind_formals (ci_formals ci) (map (λe. ⟦e⟧⇩e s) (ci_args ci)) (enter_state 𝒢 s)
         ∈ γ (en ci d)"
  assumes tf_sound_event_for[intro]:
    "s ∈ γ d ⟹ s ∈ γ (ev evt d)"

text ‹Each obligation is stated directly as an inference rule
  (‹P⇩1 ⟹ ... ⟹ P⇩n ⟹ Q›). Variables not fixed by the locale are
  implicitly generalized, so the assumptions compose directly with ‹rule›,
  ‹OF›, and ‹auto›; no separate Horn-clause restatement is needed.›

context sound_nonrelational_transfer
begin

text ‹The per-edge dispatcher's soundness, which is what an equation generator's
  step obligation asks for: \<^const>‹local_spec_step› selects the operation the
  action names, and each selected operation is sound by one locale assumption.›

lemma step_sound_for[intro]:
  "edge_collect a (γ d) ⊆ γ (local_spec_step sk asn sp br bd rt ev a d)"
proof (cases a)
  case (EA_Special sc x)
  then show ?thesis by (cases sc) auto
qed auto

end

subsection ‹The operations as a component›

text ‹What a whole-state analysis actually supplies: eight pure operations over
  \<^typ>‹'a abs_state›, packaged as a component whose handler answers nothing, whose
  entry yields the one callee state and leaves the caller's own value untouched,
  and whose return runs the fixed combine in the assign stage. The lifted sibling
  further down differs only in carrying the dead-code lift.›

definition state_local_spec ::
  "(vname ⇒ bool)
   ⇒ ('a::numeric_domain abs_state ⇒ 'a abs_state)
   ⇒ (vname ⇒ exp ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (special_call ⇒ vname ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (exp ⇒ bool ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (pname ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (exp option ⇒ pname ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (call_info ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (analysis_event ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ 'a abs_state local_spec"
where
  "state_local_spec 𝒢 sk asn sp br bd rt en ev = ⦇
     ls_query = (λ_ _. ⊤),
     ls_skip = (λ_. sk), ls_assign = (λ_. asn), ls_special = (λ_. sp),
     ls_branch = (λ_. br), ls_body = (λ_. bd), ls_return = (λ_. rt), ls_event = (λ_. ev),
     ls_enter = (λ_ ci p. [(fst p, en ci (fst p))]),
     ls_combine_env = (λ_ _ ci dc de. dc),
     ls_combine_assign = (λ_ ci. combine⇧♯ 𝒢 (ci_dst ci)) ⦈"

lemma closed_step_state_local_spec [simp]:
  "⟦a⟧⇧♯⇘state_local_spec 𝒢 sk asn sp br bd rt en ev⇙
     = local_spec_step sk asn sp br bd rt ev a"
  by (simp add: closed_step_def ls_step_def state_local_spec_def fun_eq_iff)

lemma ls_step_state_local_spec [simp]:
  "ls_step (state_local_spec 𝒢 sk asn sp br bd rt en ev) ch a
     = local_spec_step sk asn sp br bd rt ev a"
  by (simp add: ls_step_def state_local_spec_def)

lemma ls_combine_state_local_spec [simp]:
  "ls_combine (state_local_spec 𝒢 sk asn sp br bd rt en ev) ch ch' ci dc de
     = combine⇧♯ 𝒢 (ci_dst ci) dc de"
  by (simp add: state_local_spec_def)

context sound_nonrelational_transfer
begin

abbreviation tf_spec :: "'a abs_state local_spec" where
  "tf_spec ≡ state_local_spec 𝒢 sk asn sp br bd rt en ev"

theorem state_local_spec_sound: "sound_local_spec 𝒢 gamma_state tf_spec"
proof -
  have step: "edge_collect a (γ d ∩ Collect (eval_query.channel_holds ch))
      ⊆ γ (ls_step tf_spec ch a d)" for a ch and d :: "'a abs_state"
    by (simp only: ls_step_state_local_spec)
       (rule subset_trans[OF edge_collect_mono[OF Int_lower1] step_sound_for])
  show ?thesis
    unfolding sound_local_spec_def
    using gamma_state_mono step
    by (auto simp: state_local_spec_def call_enter_CallEdge combine_collect_sound)
qed

end

subsection ‹The unlifted specification›

text ‹
  ‹state_dg_spec› turns the state-level local specification into an
  equation-system specification via ‹dg_spec_of›, without the reachability
  lifting.
›

definition state_dg_spec ::
  "(vname ⇒ bool)
   ⇒ ('a::numeric_domain abs_state ⇒ 'a abs_state)
   ⇒ (vname ⇒ exp ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (special_call ⇒ vname ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (exp ⇒ bool ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (pname ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (exp option ⇒ pname ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (call_info ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (analysis_event ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ ('x,'k,unit,'a abs_state,'g::bounded_semilattice_sup_bot) dg_spec"
where
  "state_dg_spec 𝒢 sk asn sp br bd rt en ev
     = dg_spec_of (state_local_spec 𝒢 sk asn sp br bd rt en ev)"

lemma dg_spec_step_state_dg_spec:
  "dg_spec_step (state_dg_spec 𝒢 sk asn sp br bd rt en ev) a
     = local_transfer (local_spec_step sk asn sp br bd rt ev a)"
  by (simp add: state_dg_spec_def)

lemma dg_spec_wf_state_dg_spec [intro, simp]:
  "dg_spec_wf (state_dg_spec 𝒢 sk asn sp br bd rt en ev)"
  by (simp add: state_dg_spec_def)

theorem (in sound_nonrelational_transfer) state_dg_spec_contract:
  "analysis_contract (state_dg_spec 𝒢 sk asn sp br bd rt en ev) (λd g. γ d) 𝒢"
  unfolding state_dg_spec_def by (rule dg_spec_of_contract[OF state_local_spec_sound])


subsection ‹The reachability-lifted construction›

text ‹
  The same operations, each wrapped in \<^const>‹transfer_lift›: a \<^const>‹Bot› input
  stays \<^const>‹Bot›, and a result the supplied emptiness predicate flags
  collapses to it.
›

definition lifted_state_local_spec ::
  "(vname ⇒ bool)
   ⇒ ('a abs_state ⇒ bool)
   ⇒ ('a::numeric_domain abs_state ⇒ 'a abs_state)
   ⇒ (vname ⇒ exp ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (special_call ⇒ vname ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (exp ⇒ bool ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (pname ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (exp option ⇒ pname ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (call_info ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (analysis_event ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ 'a abs_state lifted local_spec"
where
  "lifted_state_local_spec 𝒢 empty_pred sk asn sp br bd rt en ev = ⦇
     ls_query = (λ_ _. ⊤),
     ls_skip = (λ_. transfer_lift empty_pred sk),
     ls_assign = (λ_ x e. transfer_lift empty_pred (asn x e)),
     ls_special = (λ_ sc x. transfer_lift empty_pred (sp sc x)),
     ls_branch = (λ_ b pol. transfer_lift empty_pred (br b pol)),
     ls_body = (λ_ p. transfer_lift empty_pred (bd p)),
     ls_return = (λ_ e p. transfer_lift empty_pred (rt e p)),
     ls_event = (λ_ evt. transfer_lift empty_pred (ev evt)),
     ls_enter = (λ_ ci p. [(fst p, transfer_lift empty_pred (en ci) (fst p))]),
     ls_combine_env = (λ_ _ ci dc de. dc),
     ls_combine_assign = (λ_ ci dcM de.
        transfer_lift2 empty_pred (combine⇧♯ 𝒢 (ci_dst ci)) dcM de) ⦈"

definition lifted_state_dg_spec ::
  "(vname ⇒ bool)
   ⇒ ('a abs_state ⇒ bool)
   ⇒ ('a::numeric_domain abs_state ⇒ 'a abs_state)
   ⇒ (vname ⇒ exp ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (special_call ⇒ vname ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (exp ⇒ bool ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (pname ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (exp option ⇒ pname ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (call_info ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ (analysis_event ⇒ 'a abs_state ⇒ 'a abs_state)
   ⇒ ('x,'k,unit,'a abs_state lifted,'g::bounded_semilattice_sup_bot) dg_spec"
where
  "lifted_state_dg_spec 𝒢 empty_pred sk asn sp br bd rt en ev
     = dg_spec_of (lifted_state_local_spec 𝒢 empty_pred sk asn sp br bd rt en ev)"


lemma local_spec_step_transfer_lift:
  "local_spec_step (transfer_lift empty_pred sk)
     (λx e. transfer_lift empty_pred (asn x e))
     (λsc x. transfer_lift empty_pred (sp sc x))
     (λb pol. transfer_lift empty_pred (br b pol))
     (λp. transfer_lift empty_pred (bd p))
     (λe p. transfer_lift empty_pred (rt e p))
     (λevt. transfer_lift empty_pred (ev evt)) a
     = transfer_lift empty_pred (local_spec_step sk asn sp br bd rt ev a)"
  by (cases a) simp_all

lemma ls_step_lifted_state_local_spec [simp]:
  "ls_step (lifted_state_local_spec 𝒢 empty_pred sk asn sp br bd rt en ev) ch a
     = transfer_lift empty_pred (local_spec_step sk asn sp br bd rt ev a)"
  by (simp add: ls_step_def lifted_state_local_spec_def local_spec_step_transfer_lift)

lemma closed_step_lifted_state_local_spec [simp]:
  "⟦a⟧⇧♯⇘lifted_state_local_spec 𝒢 empty_pred sk asn sp br bd rt en ev⇙
     = transfer_lift empty_pred (local_spec_step sk asn sp br bd rt ev a)"
  by (simp add: closed_step_def fun_eq_iff)

lemma dg_spec_step_lifted_state_dg_spec:
  "dg_spec_step (lifted_state_dg_spec 𝒢 empty_pred sk asn sp br bd rt en ev) a
     = local_transfer (transfer_lift empty_pred (local_spec_step sk asn sp br bd rt ev a))"
  by (simp add: lifted_state_dg_spec_def)

lemma dg_spec_wf_lifted_state_dg_spec [intro, simp]:
  "dg_spec_wf (lifted_state_dg_spec 𝒢 empty_pred sk asn sp br bd rt en ev)"
  by (simp add: lifted_state_dg_spec_def)

lemma dgs_enter_lifted_state_dg_spec:
  "enter⇧♯ (lifted_state_dg_spec 𝒢 empty_pred sk asn sp br bd rt en ev) ci
     = local_enter_transfer (λd. [(d, transfer_lift empty_pred (en ci) d)])"
  by (simp add: lifted_state_dg_spec_def lifted_state_local_spec_def)

text ‹The caller continuation and the env stage are both identities, so the
  whole return pipeline is the return assignment applied to the raw call-site
  value and the callee exit.›

lemma dg_spec_combine_transfer_lifted_state_dg_spec:
  "dg_spec_combine_transfer
     (lifted_state_dg_spec 𝒢 empty_pred sk asn sp br bd rt en ev) ci
     = local_combine_transfer
         (λdc de. transfer_lift2 empty_pred (combine⇧♯ 𝒢 (ci_dst ci)) dc de)"
  by (simp add: lifted_state_dg_spec_def lifted_state_local_spec_def)

end