Theory Example_Interval_Source_Ctx

theory Example_Interval_Source_Ctx
  imports
    Example_Interval_DG_Ctx_Collect
begin

section ‹Source-level context-sensitive certification for repeated calls›

text ‹
  The ‹twice› program calls one procedure from two sites.  The theorems below connect each
  source configuration to the solved reader of Interval's entry-state registration
  ‹interval_es_rule› at \<^const>‹Globals_Warrow›, for an activation admitted for the
  trace that produced it, published and then through the lifted concretization
  \<^const>‹gamma_state_lift›.  The admitted-context relation
  \<^const>‹dg_analysis.admitted_contexts› keeps the two calls separate while the
  source/CFG simulation preserves the concrete frame stack; being a relation rather than a
  function, what a trace admits is membership in \<^const>‹activation_context_rel›, not an equation.
›

text ‹The analysis' own solved reader, abbreviated for the two statements below.›

abbreviation twice_ctx_sg ::
  "pp × ivl list + (unit, ivl list) global_unknown ⇒ ivl default_st lifted" where
  "twice_ctx_sg ≡ interval_es_rule.reader Globals_Warrow twice_gs twice_program"

abbreviation twice_ctx_gamma :: "ivl default_st lifted ⇒ store set" where
  "twice_ctx_gamma m ≡ gamma_lift (default_st_gamma twice_gs) m"

text ‹Context-sensitive source soundness.  Any ‹twice› run reaches a store bounded at the
  interval slot indexed by some context the trace that produced it admits.›
theorem twice_source_ctx_run_sound:
  assumes run: "twice_gs, twice_pi ⊢ (twice_main, s0, []) →⇩p⇧* (residual, s, frs)"
    and init: "s0 ∈ cinit_stores twice_gs"
  shows "∃v stk t c.
           twice_pi, compile_prog twice_pi twice_procs, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)
           ∧ activation_context_rel twice_gs
               (interval_es_rule.admitted_contexts Globals_Warrow twice_gs twice_program)
               [] (compile_prog twice_pi twice_procs) t c
           ∧ s ∈ twice_ctx_gamma (twice_ctx_sg (Inl (v, c)))"
proof -
  have run': "twice_gs, twice_pi ⊢ (main_body twice_pi, s0, []) →⇩p⇧* (residual, s, frs)"
    using run by simp
  show ?thesis
    by (rule source_sound_from_collecting_cap
          [where adm = "interval_es_rule.admitted_contexts Globals_Warrow twice_gs twice_program"
             and c⇩0 = "[]"
             and γ⇩M = twice_ctx_gamma,
           OF twice_wf init run'
              interval_es_rule.entry_state_has_context[OF twice_entry_state_hyps,
                unfolded twice_cfg_alt]
              twice_activation_collect_sound])
qed

text ‹The witness-free specialisation: a ‹twice› store reached at the top level (empty source
  frame stack) is certified at the concrete seed context ‹[]› (no formal binds the root
  activation) --- no \<^typ>‹activation_trace› witness, no context existential.  This is the clean user-facing
  statement for main-level program points.›
theorem twice_source_toplevel_at_bot:
  assumes run: "twice_gs, twice_pi ⊢ (twice_main, s0, []) →⇩p⇧* (residual, s, [])"
    and init: "s0 ∈ cinit_stores twice_gs"
  shows "∃v. twice_pi, compile_prog twice_pi twice_procs, prog_main_name ⊢ (residual, s, []) ≈ (v, s, [])
             ∧ s ∈ twice_ctx_gamma (twice_ctx_sg (Inl (v, [])))"
proof -
  have run': "twice_gs, twice_pi ⊢ (main_body twice_pi, s0, []) →⇩p⇧* (residual, s, [])"
    using run by simp
  show ?thesis
    by (rule source_sound_toplevel_from_collecting_cap
          [where adm = "interval_es_rule.admitted_contexts Globals_Warrow twice_gs twice_program"
             and c⇩0 = "[]"
             and γ⇩M = twice_ctx_gamma,
           OF twice_wf init run' twice_activation_collect_sound])
qed

end