Theory DG_Local_State_Exec

theory DG_Local_State_Exec
  imports
    Ownership_Split_Exec
begin

unbundle default_st_syntax

section ‹Executable Base-style DG construction›

text ‹
  Executable mirror of \<^const>‹lifted_state_dg_spec›: a component
  over ‹'a default_st lifted› instead of ‹'a abs_state lifted›, with ‹tf_st› a
  bare ‹edge_action ⇒ _› dispatcher -- the executable side dispatches on the
  action rather than naming one operation per edge kind -- and ‹enter_st› its
  enter counterpart. Local-only means it reads no global and publishes none, so
  its compiled equations carry no ‹QueryG› and no ‹Side› -- exactly as on the
  mathematical side.

  One field differs from the mathematical construction: the env stage of ‹combine›
  is not the identity here. \<^const>‹combine_assign_default_st› (unlike
  \<^const>‹combine_collect_abs›) does not itself select
  locals-from-caller/globals-from-callee; that selection is what
  \<^const>‹combine_default_st› computes, so the env stage must compute it
  explicitly before the assign stage writes the return value.
›

text ‹The caller half of ‹enter› is the identity for the same reason as in the
  abstract Base record: the carrier relates no two locations, so a call has
  nothing in it to invalidate. What the env stage then merges is the raw
  call-site value against the callee exit.›

definition combine_env_st_lifted ::
  "'a::bounded_semilattice_sup_bot default_st lifted ⇒ 'a default_st lifted
   ⇒ 'a default_st lifted"
where
  "combine_env_st_lifted dc de =
     (case dc of Bot ⇒ Bot | Lifted x ⇒
        (case de of Bot ⇒ Bot | Lifted y ⇒ Lifted (combine_default_st x y)))"

text ‹
  The executable analysis is a component whose edge transfers are the one
  dispatcher ‹tf_st›, lifted over the unreachable state. Its handler answers
  nothing.
›

definition exec_local_spec ::
  "(vname ⇒ bool) ⇒ ('a::bounded_semilattice_sup_bot default_st ⇒ bool)
   ⇒ (edge_action ⇒ 'a default_st ⇒ 'a default_st)
   ⇒ (call_info ⇒ 'a default_st ⇒ 'a default_st)
   ⇒ 'a default_st lifted local_spec" where
  "exec_local_spec 𝒢 empty_pred tf_st enter_st = make_local_spec
     (λ_ _. ⊤)
     (λ_ a. transfer_lift empty_pred (tf_st a))
     (λ_ ci p. [(fst p, transfer_lift empty_pred (enter_st ci) (fst p))])
     (λ_ _ ci. combine_env_st_lifted)
     (λ_ ci. transfer_lift2 empty_pred
        (λenv0 de0. combine_assign_default_st 𝒢 (ci_dst ci)
             de0⟨location_of 𝒢 ret_var⟩ env0))"

lemma ls_step_exec_local_spec [simp]:
  "ls_step (exec_local_spec 𝒢 empty_pred tf_st enter_st) A a = transfer_lift empty_pred (tf_st a)"
  by (simp add: exec_local_spec_def)

lemma closed_step_exec_local_spec [simp]:
  "⟦a⟧⇧♯⇘exec_local_spec 𝒢 empty_pred tf_st enter_st⇙
     = transfer_lift empty_pred (tf_st a)"
  by (simp add: closed_step_def fun_eq_iff)

lemma ls_enter_exec_local_spec [simp]:
  "ls_enter (exec_local_spec 𝒢 empty_pred tf_st enter_st) A ci (d, d)
   = [(d, transfer_lift empty_pred (enter_st ci) d)]"
  by (simp add: exec_local_spec_def)

definition exec_dg_spec ::
  "(vname ⇒ bool)
   ⇒ ('a::bounded_semilattice_sup_bot default_st ⇒ bool)
   ⇒ (edge_action ⇒ 'a default_st ⇒ 'a default_st)
   ⇒ (call_info ⇒ 'a default_st ⇒ 'a default_st)
   ⇒ ('x,'k,unit,'a default_st lifted,'g::bounded_semilattice_sup_bot) dg_spec"
where
  "exec_dg_spec 𝒢 empty_pred tf_st enter_st
     = dg_spec_of (exec_local_spec 𝒢 empty_pred tf_st enter_st)"

subsection ‹Basic equations›

text ‹
  Unfolding equations for each field of ‹exec_dg_spec›: step, entry and
  combine are the executable transfers lifted over reachability.
›

lemma dg_spec_step_exec_dg_spec:
  "dg_spec_step (exec_dg_spec 𝒢 empty_pred tf_st enter_st) a
     = local_transfer (transfer_lift empty_pred (tf_st a))"
  by (simp add: exec_dg_spec_def)

lemma dg_spec_wf_exec_dg_spec [intro, simp]:
  "dg_spec_wf (exec_dg_spec 𝒢 empty_pred tf_st enter_st)"
  by (simp add: exec_dg_spec_def)

lemma dgs_enter_exec_dg_spec:
  "enter⇧♯ (exec_dg_spec 𝒢 empty_pred tf_st enter_st) ci
     = local_enter_transfer (λd. [(d, transfer_lift empty_pred (enter_st ci) d)])"
  by (simp add: exec_dg_spec_def)

lemma dg_spec_combine_transfer_exec_dg_spec:
  "dg_spec_combine_transfer (exec_dg_spec 𝒢 empty_pred tf_st enter_st) ci
     = local_combine_transfer
         (λdc de. transfer_lift2 empty_pred
            (λenv0 de0. combine_assign_default_st 𝒢 (ci_dst ci)
                 de0⟨location_of 𝒢 ret_var⟩ env0)
            (combine_env_st_lifted dc de) de)"
  by (simp add: exec_dg_spec_def exec_local_spec_def)

unbundle no default_st_syntax

end