Theory Nonrel_Registration

theory Nonrel_Registration
  imports
    Nonrelational_Transfer
    "Voblint_Result.DG_Live_Unknowns"
    "Voblint_Framework.Call_String_Context"
    "Voblint_Solver.Globals_Rule"
begin

section ‹Registering a non-relational bundle with the pipeline›

text ‹
  ⬚‹dg_analysis_execI› leaves a non-relational domain four obligations: the
  context policy's route agreement and seed key, the solver, and the initial state.
  The first three belong to the context policy and the solver, not to the domain, so
  they are discharged here once per policy. A domain supplies its bundle and its
  initial state with the coverage lemma, and one interpretation of the locale for a
  policy registers it there for every update rule ‹r› (and, for call strings, every
  bound ‹k›).
›

locale nonrel_registration = sound_nonrelational_ops ops
  for ops :: "'a::numeric_domain nonrelational_ops" +
  fixes init_st :: "'a default_st"
  assumes init_gamma: "⋀𝒢. cinit_stores 𝒢 ⊆ default_st_gamma 𝒢 init_st"

subsection ‹At the unit context›

text ‹
  One context per callee: every activation is keyed by ‹()›, so the route reads
  nothing of the entered state and agrees with its abstraction trivially.
›

locale nonrel_unit_rule = nonrel_registration ops init_st for ops init_st +
  fixes r :: globals_rule
begin

sublocale dg_analysis_exec
    "generic_tf_st_for ops" "generic_enter_st_for ops" init_st
    "Analysis_Global ()" Analysis_Global Activation_Seed "λ_. route_unit" "()"
    "TD_side_rule_Interp_solve r"
    "TD_side_rule_Interp.solve_dom TYPE((unit, unit) global_unknown)
       TYPE(('a default_st lifted, 'a default_st lifted) dg_state) r"
    bot check.classify_check
    skip assign special_transfer backward.branch body ret
    enter_ci_for event "λ_. route_unit"
    "TD_side_rule_Interp_solve_c r"
  by (rule dg_analysis_execI) (simp_all add: td_certified_solver init_gamma)

end

subsection ‹At the entry-state context›

text ‹
  An activation is keyed by the abstract values its formals hold on entry. The
  executable route reads them off the stored state, and
  ‹exec_formals_route_commute› says it agrees with the route on the abstraction.
›

locale nonrel_es_rule = nonrel_registration ops init_st for ops init_st +
  fixes r :: globals_rule
begin

sublocale dg_analysis_exec
    "generic_tf_st_for ops" "generic_enter_st_for ops" init_st
    "Analysis_Global ()" Analysis_Global Activation_Seed exec_formals_route "[]"
    "TD_side_rule_Interp_solve r"
    "TD_side_rule_Interp.solve_dom TYPE((unit, 'a list) global_unknown)
       TYPE(('a default_st lifted, 'a default_st lifted) dg_state) r"
    bot check.classify_check
    skip assign special_transfer backward.branch body ret
    enter_ci_for event "λ_. formals_route_lifted_gen"
    "TD_side_rule_Interp_solve_c r"
  by (rule dg_analysis_execI)
     (simp_all add: exec_formals_route_commute[symmetric] td_certified_solver init_gamma)

end

subsection ‹At the call-string context›

text ‹
  An activation is keyed by its last ‹k› call sites. The route reads only the call
  site, never the entered state, which is ‹cs_route_indep_of_data›.
›

locale nonrel_cs_rule = nonrel_registration ops init_st for ops init_st +
  fixes k :: nat and r :: globals_rule
begin

sublocale dg_analysis_exec
    "generic_tf_st_for ops" "generic_enter_st_for ops" init_st
    Call_String_Context.Global "λ_. Call_String_Context.Global"
    Call_String_Context.Seed "λ_. cs_route k" "[]"
    "TD_side_rule_Interp_solve r"
    "TD_side_rule_Interp.solve_dom TYPE(call_string_gk)
       TYPE(('a default_st lifted, 'a default_st lifted) dg_state) r"
    bot check.classify_check
    skip assign special_transfer backward.branch body ret
    enter_ci_for event "λ_. cs_route k"
    "TD_side_rule_Interp_solve_c r"
  by (rule dg_analysis_execI)
     (simp_all add: cs_route_indep_of_data td_certified_solver init_gamma)

end

text ‹A domain discharges each policy's locale from the same two facts.›

lemma nonrel_registrationI:
  assumes "sound_nonrelational_ops ops"
    and "⋀𝒢. cinit_stores 𝒢 ⊆ default_st_gamma 𝒢 init_st"
  shows "nonrel_registration ops init_st"
  using assms by (intro nonrel_registration.intro nonrel_registration_axioms.intro)

lemma nonrel_unit_ruleI:
  "nonrel_registration ops init_st ⟹ nonrel_unit_rule ops init_st"
  by (rule nonrel_unit_rule.intro)

lemma nonrel_es_ruleI:
  "nonrel_registration ops init_st ⟹ nonrel_es_rule ops init_st"
  by (rule nonrel_es_rule.intro)

lemma nonrel_cs_ruleI:
  "nonrel_registration ops init_st ⟹ nonrel_cs_rule ops init_st"
  by (rule nonrel_cs_rule.intro)

end