Theory DG_Local_State_Exec_Refinement

theory DG_Local_State_Exec_Refinement
  imports
    DG_Local_State_Exec
    "Voblint_Framework.DG_Reader_Transport"
begin

unbundle default_st_syntax

section ‹The mathematical run an executable D/G run represents›

text ‹
  The executable construction above computes on association-list states; the
  soundness statements are about function-valued ones. This theory is the
  bridge: it fixes a domain whose executable transfer agrees with its abstract
  transfer on the represented functions (‹dg_domain_exec›) and derives, from
  those three agreements alone, that a whole D/G specification is sound at the
  executable carrier -- with no separate abstract-carrier run to compare against.
›

subsection ‹The function one return combine represents›

text ‹
  The one fact about the executable state representation this theory needs
  that no lifter supplies: merging caller against callee and then writing the
  return value represents the mathematical \<^const>‹combine_collect_abs› of
  the two represented functions. Everything else transports through
  \<^const>‹transfer_lift›/\<^const>‹transfer_lift2› naturality.
›

lemma default_st_to_fun_combine_assign:
  "ρ⇘𝒢⇙
     (combine_assign_default_st 𝒢 dst y⟨location_of 𝒢 ret_var⟩
        (combine_default_st x y))
   = combine⇧♯ 𝒢 dst (ρ⇘𝒢⇙ x) (ρ⇘𝒢⇙ y)"
  unfolding default_st_to_fun_def
  by (auto simp add: combine_collect_abs_def fun_eq_iff location_of_def
      split: option.splits)

subsection ‹Routed-domain compatibility, independent of any routing context›

text ‹
  Every routed domain instance needs the same shapes
  -- the compiled edge, enter and combine trees commuting under
  \<^const>‹default_st_to_fun›, plus \<^locale>‹dg_reader_commute_gen› at that
  same reader -- from its own executable/abstract transfer-commute facts,
  citing this theory's packaging theorems verbatim. Nothing in that derivation
  is domain-specific beyond the two primitive commute facts a domain's own
  executable-transfer soundness development already proves
  (‹sign_tf.tf_st_for_commute›, ‹ivl_tf.tf_st_for_commute›, ...): this locale states
  the derivation once, so a domain interprets it instead of restating it. The
  locale is deliberately free of any routing context (‹route›, ‹Seed›,
  ‹Global›, a solver): those are context-owned and solver-owned respectively,
  not domain-owned.
›

text ‹
  \<^locale>‹dg_reader_commute_gen›'s instance at the same reader on both sides needs no
  domain fact at all: \<^const>‹default_st_to_fun› is already carrier-polymorphic and
  ‹sup›-homomorphic (‹default_st_to_fun_sup›,
  ‹Voblint_Exec.Default_St_Transfer›), so this
  is a free-standing fact, not part of the ‹dg_domain_exec› locale below -- keeping it
  outside means citing it never drags in that locale's ‹empty_pred›/transfer obligations.
›

lemma dg_reader_commute_gen_lifted_for:
  "dg_reader_commute_gen
     (ρ⇘𝒢⇙ :: _ default_st lifted ⇒ _) (ρ⇘𝒢⇙ :: _ default_st lifted ⇒ _)"
  by unfold_locales (simp_all add: map_lift_sup)

text ‹
  ‹dg_domain_exec› relates an executable transfer on ‹default_st›
  to the abstract state specification: on live states the step, the entry
  transfer and the emptiness test agree with their abstract counterparts after
  readback through ‹default_st_to_fun›.
›

locale dg_domain_exec =
  fixes 𝒢 :: "vname ⇒ bool"
    and empty_pred :: "'a::numeric_domain default_st ⇒ bool"
    and tf_st :: "edge_action ⇒ 'a default_st ⇒ 'a default_st"
    and enter_st :: "call_info ⇒ 'a default_st ⇒ 'a default_st"
    and sk :: "'a 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_st_commute:
      "⋀a s. live_default_st 𝒢 s ⟹
         ρ⇘𝒢⇙ (tf_st a s)
           = local_spec_step sk asn sp br bd rt ev a (ρ⇘𝒢⇙ s)"
    and enter_st_commute:
      "⋀ci s. ρ⇘𝒢⇙ (enter_st ci s)
                   = en ci (ρ⇘𝒢⇙ s)"
    and empty_pred_exact:
      "⋀s. empty_pred s = is_empty_state (ρ⇘𝒢⇙ s)"
begin

text ‹With ‹𝒢› fixed, ‹γ s› is the carrier's concretization, for a plain and
  for a lifted carrier state alike.›

adhoc_overloading gamma_S == "default_st_gamma 𝒢"
adhoc_overloading gamma_S == "gamma_lift (default_st_gamma 𝒢)"

abbreviation reader :: "'a default_st lifted ⇒ 'a abs_state lifted" where
  "reader ≡ map_lift ρ⇘𝒢⇙"

text ‹Each field's equation on the represented function, once. These are the only inputs the tree
  commutes below take: a local-only transfer compiles to a single answer, so
  its transport is exactly the pure equation on the function it wraps.›

text ‹
  Unlike ‹enter_st_commute›/‹combine›'s field equations, ‹tf_st_commute› only
  holds on live inputs (a domain's ‹branch_st›-style raw result need not
  match its abstract ‹branch›'s on a dead one), so this cannot go through the
  blanket ‹transfer_lift_commute›. ‹normalized_lift› supplies liveness
  directly instead: production only ever feeds ‹tf_st› a ‹d› that is
  itself ‹Bot› or the (always-normalized, ‹transfer_lift_normalized›) result
  of a prior step.
›

lemma step_lift_commute:
  assumes norm: "normalized_lift empty_pred d"
  shows "reader (transfer_lift empty_pred (tf_st a) d)
     = transfer_lift is_empty_state (local_spec_step sk asn sp br bd rt ev a) (reader d)"
using norm proof (cases d)
  case Bot
  then show ?thesis by (simp add: transfer_lift_def)
next
  case (Lifted s)
  with norm have "live_default_st 𝒢 s"
    by (simp add: live_default_st_def empty_pred_exact)
  then show ?thesis
    unfolding Lifted
    by (simp add: transfer_lift_def normalize_lift_def tf_st_commute empty_pred_exact)
qed

lemma enter_lift_commute:
  "reader (transfer_lift empty_pred (enter_st ci) d)
     = transfer_lift is_empty_state (en ci) (reader d)"
proof (rule transfer_lift_commute)
  show "⋀s. ρ⇘𝒢⇙ (enter_st ci s)
              = en ci (ρ⇘𝒢⇙ s)"
    by (simp add: enter_st_commute)
  show "⋀s. empty_pred s = is_empty_state (ρ⇘𝒢⇙ s)"
    by (rule empty_pred_exact)
qed

text ‹The env stage merges into the assign stage: both collapse on the same two
  \<^const>‹Bot› cases, so the composed combine is a single \<^const>‹transfer_lift2›
  and transports by the same naturality lemma as every other field.›

lemma transfer_lift2_combine_env_st_lifted:
  "transfer_lift2 empty_pred g (combine_env_st_lifted dc de) de
     = transfer_lift2 empty_pred (λx y. g (combine_default_st x y) y) dc de"
  by (cases dc; cases de) (simp_all add: combine_env_st_lifted_def transfer_lift2_def)

lemma combine_lift_commute:
  "reader (transfer_lift2 empty_pred
            (λenv0 de0. combine_assign_default_st 𝒢 dst
                 de0⟨location_of 𝒢 ret_var⟩ env0)
            (combine_env_st_lifted dc de) de)
     = transfer_lift2 is_empty_state (combine⇧♯ 𝒢 dst) (reader dc) (reader de)"
  unfolding transfer_lift2_combine_env_st_lifted
proof (rule transfer_lift2_commute)
  show "⋀x y. ρ⇘𝒢⇙
      (combine_assign_default_st 𝒢 dst y⟨location_of 𝒢 ret_var⟩
         (combine_default_st x y))
        = combine⇧♯ 𝒢 dst (ρ⇘𝒢⇙ x) (ρ⇘𝒢⇙ y)"
    by (rule default_st_to_fun_combine_assign)
  show "⋀s. empty_pred s = is_empty_state (ρ⇘𝒢⇙ s)"
    by (rule empty_pred_exact)
qed


subsection ‹Tree-level transport of the two specifications›

text ‹
  The routed spine's transport hypotheses are commutes of compiled sub-trees.
  Both specifications are
  local-only, so each such commute reduces to the corresponding field equation
  above.
›

abbreviation spec_st :: "('x,'k,unit,'a default_st lifted,'a default_st lifted) dg_spec" where
  "spec_st ≡ exec_dg_spec 𝒢 empty_pred tf_st enter_st"

abbreviation spec_abs :: "('x,'k,unit,'a abs_state lifted,'a abs_state lifted) dg_spec" where
  "spec_abs ≡ lifted_state_dg_spec 𝒢 is_empty_state sk asn sp br bd rt en ev"

lemma Henter_lifted_for:
  "dg_reader_commute_gen.dg_enter_st_commute reader reader σ_st
     (enter⇧♯ spec_st ci (mk_dg_man d (λ_. gk)))
     (enter⇧♯ spec_abs ci (mk_dg_man (reader d) (λ_. gk)))"
  unfolding dgs_enter_exec_dg_spec dgs_enter_lifted_state_dg_spec
  by (rule dg_reader_commute_gen.dg_enter_st_commute_local_enter_transfer
        [OF dg_reader_commute_gen_lifted_for])
     (simp add: enter_lift_commute)

lemma Hcomb_lifted_for:
  "dg_reader_commute_gen.dg_tree_st_commute reader reader σ_st
     (sp_compile_with (λx. DG x bot)
        (dg_spec_combine_transfer spec_st ci (mk_dg_man d (λ_. gk)) de))
     (sp_compile_with (λx. DG x bot)
        (dg_spec_combine_transfer spec_abs ci (mk_dg_man (reader d) (λ_. gk)) (reader de)))"
  unfolding dg_spec_combine_transfer_exec_dg_spec
    dg_spec_combine_transfer_lifted_state_dg_spec
  by (rule dg_reader_commute_gen.dg_tree_st_commute_local_combine_transfer
        [OF dg_reader_commute_gen_lifted_for,
         where F = "transfer_lift2 is_empty_state (combine⇧♯ 𝒢 (ci_dst ci))"])
     (rule combine_lift_commute)

subsection ‹Soundness at the executable carrier, pulled back through its functions›

text ‹
  The framework is carrier-agnostic, so nothing forces it to be instantiated at
  ‹'a abs_state lifted›: with the carrier's own concretization
  \<^const>‹default_st_gamma›, the executable Base-style spec is itself a
  \<^locale>‹analysis_contract›, and the field equations above are all that the proof
  needs. An instance that interprets the routed spine at ‹spec_st› with this
  concretization feeds it the solver's own table and never transports a solved
  system between carriers.
›

definition gamma_exec :: "'a default_st lifted ⇒ 'a default_st lifted ⇒ store set" where
  "gamma_exec d g = γ d"

lemma gamma_exec_Bot [simp]: "gamma_exec Bot g = {}"
  by (simp add: gamma_exec_def)

text ‹
  Entry is not part of \<^locale>‹analysis_contract›, so a routed instance needs it
  separately. This is the same fact the collapse below proves for its own entry
  obligation, exported once because every routed instance over this carrier
  discharges its entry coverage from it.
›

lemma entered_st:
  assumes tf_sound: "sound_nonrelational_transfer 𝒢 sk asn sp br bd rt en ev"
    and s: "s ∈ γ d"
  shows "call_enter 𝒢 (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci)) s
           ∈ γ (transfer_lift empty_pred (enter_st ci) d)"
  using s unfolding gamma_lift_default_st_gamma_to_fun enter_lift_commute
  by (intro transfer_lift_sound_mem[OF _ is_empty_state_gamma_state_empty])
     (simp add: call_enter_CallEdge
       sound_nonrelational_transfer.tf_sound_enter_entry_for[OF tf_sound])

theorem entry_pairs_cover_st:
  assumes tf_sound: "sound_nonrelational_transfer 𝒢 sk asn sp br bd rt en ev"
    and sin: "s ∈ γ d"
  shows "entry_pairs_cover (λd'. γ d') s
           (call_enter 𝒢 (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci)) s)
           [(d, transfer_lift empty_pred (enter_st ci) d)]"
  by (rule entry_pairs_coverI
        [where cont = d and entry = "transfer_lift empty_pred (enter_st ci) d"])
     (simp_all add: sin entered_st[OF tf_sound sin])

text ‹
  The executable analysis as a component, sound for the carrier's
  concretization. The proof maps each state to its function through ‹reader›; the
  contract below is its one-line consequence.
›

theorem exec_local_spec_sound:
  assumes tf_sound: "sound_nonrelational_transfer 𝒢 sk asn sp br bd rt en ev"
  shows "sound_local_spec 𝒢 (λd. γ d) (exec_local_spec 𝒢 empty_pred tf_st enter_st)"
proof -
  have step: "edge_collect a (γ⇩⊥ (reader d)) ⊆ γ⇩⊥ (reader (transfer_lift empty_pred (tf_st a) d))"
    for a d
  proof (cases "normalized_lift empty_pred d")
    case True
    show ?thesis
      unfolding step_lift_commute[OF True]
      by (rule transfer_lift_sound_collect
            [OF sound_nonrelational_transfer.step_sound_for[OF tf_sound]
                edge_collect_empty_set is_empty_state_gamma_state_empty])
  next
    case False
    then obtain s where "d = Lifted s" "empty_pred s" by (cases d) simp_all
    then show ?thesis by (simp add: empty_pred_exact is_empty_state_gamma_state_empty)
  qed
  have comb: "combine_collect 𝒢 (ci_dst ci) s t ∈ γ⇩⊥ (reader (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))"
    if "s ∈ γ⇩⊥ (reader dc)" "t ∈ γ⇩⊥ (reader de)" for s t dc de ci
    unfolding combine_lift_commute
    by (rule
      transfer_lift2_sound_mem[OF combine_collect_sound is_empty_state_gamma_state_empty that])
  have mono: "∀x y. x ≤ y ⟶ γ⇩⊥ (reader x) ⊆ γ⇩⊥ (reader y)"
    by (meson gamma_lift_mono gamma_state_mono map_lift_default_st_to_fun_mono)
  show ?thesis
    unfolding sound_local_spec_def gamma_lift_default_st_gamma_to_fun
    using mono subset_trans[OF edge_collect_mono[OF Int_lower1] step]
      entered_st[OF tf_sound, unfolded gamma_lift_default_st_gamma_to_fun] comb
    by (auto simp: exec_local_spec_def)
qed

theorem analysis_contract_st:
  assumes tf_sound: "sound_nonrelational_transfer 𝒢 sk asn sp br bd rt en ev"
  shows "analysis_contract spec_st (λd e. gamma_exec d (e ())) 𝒢"
  unfolding exec_dg_spec_def gamma_exec_def[abs_def]
  by (rule dg_spec_of_contract[OF exec_local_spec_sound[OF tf_sound]])

end

unbundle no default_st_syntax

end