Theory DG_Result_Construction

theory DG_Result_Construction
  imports
    "Voblint_Framework.DG_Analysis_Adapter"
    "Voblint_VIMP.VIMP_Program"
    "Voblint_Exec.Exec_DG_State"
begin

section ‹What a solved D/G system publishes›

text ‹
  Every analysis, at every context policy and every solver discipline, turns the
  solver's answer -- a covered key set and a map from unknowns to ‹dg_state›s over
  its carrier -- into an \<^type>‹solved_table› table of the locals. This
  theory states that construction once, over an arbitrary solved pair, so an
  analysis's result table is one application rather than a rewritten body.

  Publishing a local unknown means two steps in sequence.
  \<^const>‹canonicalize_lift› collapses a stored \<^const>‹Lifted› payload that
  describes no store to \<^const>‹Bot›, so a dead point reads as dead; the publication
  map ‹rd› then turns the carrier into the value the table publishes. Coverage is
  separate from deadness: a key the solver never visited is absent from the
  table, and \<^const>‹lookup_table› answers \<^const>‹Bot› for it without any
  claim about the program.
›

text ‹
  ‹sol› is the already-solved pair, not the solve function. Passing the pair keeps
  one solve per table in generated code -- the argument is evaluated once and the
  per-point closure captures it -- which is why no analysis needs a separate
  ‹[code]› equation with an explicit ‹let›.

  What a point publishes is read off its local unknown together with the solved
  global environment, each name read at its key ‹Inr (gk n)›: ‹rc› recombines
  the local half with that environment into the state the point describes. An analysis that keeps every variable in the local half passes a
  recombination that ignores the global.
›

definition dg_result_for ::
    "('s ⇒ 'v) ⇒ ('s ⇒ bool) ⇒ ('s lifted ⇒ ('n ⇒ 'g) ⇒ 's lifted) ⇒ ('n ⇒ 'k)
     ⇒ (pp × 'c) set × (pp × 'c + 'k ⇒ ('s lifted, 'g) dg_state)
     ⇒ ('c, 'v) solved_table" where
  "dg_result_for rd emp rc gk sol =
     Solved_Table (fst sol)
       (λv ctx. map_lift rd (canonicalize_lift emp
          (rc (dg_local (snd sol (Inl (v, ctx)))) (genv gk (snd sol)))))"

lemma covered_keys_dg_result_for [simp]:
  "covered_keys (dg_result_for rd emp rc gk sol) = fst sol"
  unfolding dg_result_for_def by simp

text ‹
  The one fact every soundness bridge needs about the table: a covered key reads
  back the normalized recombined state, an uncovered one answers \<^const>‹Bot›.
›

lemma lookup_table_dg_result_for [simp]:
  "lookup_table (dg_result_for rd emp rc gk sol) v ctx
     = (if (v, ctx) ∈ fst sol
        then map_lift rd (canonicalize_lift emp
               (rc (dg_local (snd sol (Inl (v, ctx)))) (genv gk (snd sol))))
        else Bot)"
  unfolding dg_result_for_def lookup_table_def by simp

text ‹
  Normalizing before publication agrees with normalizing after it whenever the
  two emptiness tests agree, so a soundness bridge stated after publication
  applies to the table built before it.
›

lemma map_lift_canonicalize_lift:
  assumes "⋀s. emp s = empty⇩V (rd s)"
  shows "map_lift rd (canonicalize_lift emp d) = canonicalize_lift empty⇩V (map_lift rd d)"
  by (cases d) (simp_all add: assms normalize_lift_def)

text ‹Collapsing a payload that denotes nothing to \<^const>‹Bot› does not change
  what the value denotes.›

lemma gamma_lift_canonicalize_lift:
  assumes "⋀v. empty⇩V v ⟹ gm v = {}"
  shows "gamma_lift gm (canonicalize_lift empty⇩V x) = gamma_lift gm x"
  by (cases x) (simp_all add: normalize_lift_def assms)

end