Theory Activation_Trace_Abstract

theory Activation_Trace_Abstract
  imports Activation_Trace_Collect
begin

section ‹What an analysis must satisfy to be sound›

text ‹
  An analysis claims: "at node ‹v›, in context ‹c›, only these stores can occur".  This
  theory says what such a claim must satisfy to be believed, and proves that satisfying it
  is enough --- every valid activation trace's final store really does lie in the set claimed for its
  own node and every context it carries.  No domain, solver or dependency graph appears
  here; they instantiate this.

  The claim is a function ‹cover› from a node and a context to a set of stores, and there
  are five obligations on it: the seed stores are covered at the entry (‹INIT›), each intra
  edge keeps them covered (‹INTRA›), a call covers the entered store at the callee in every
  context the policy admits (‹CALL›), a return covers the combined store back at the caller
  (‹RETURN›), and every covered call admits at least one context (‹TOTAL›).

  ‹RETURN› is the load-bearing one.  The callee is read at a context admitted for the
  transition from the caller's own carried context, so a return may only compose a callee
  whose context came from the caller it is resuming --- not any context that happens to
  cover that callee's entry.  This correlation is not an extra parameter to assume:
  ‹activation_context_rel_caller_entry› makes it a theorem about \<^const>‹valid_activation_trace›.

  ‹TOTAL› is what makes the buckets meaningful rather than merely safe.  A resumed caller
  may carry a context under which its callee was never assigned one; the callee's exit
  store would then be bounded by no bucket, and the combined store by nothing.  With it,
  every valid activation trace carries some context, so the context-insensitive collection is exactly
  the union of the buckets.

  A context is not claimed to identify an activation: two activations may carry the same
  context, and one activation may carry several.  The theorem is that each trace lands in
  every slot it carries.
›

subsection ‹The abstract interface›

text ‹‹cover› is the claim itself, ‹adm› the context policy it is indexed by, and
  ‹c⇩0› the context the seed stores arrive under.  An analysis interprets this once,
  with its own solved table in place of ‹cover›; nothing below asks how that table was
  computed.›
locale activation_coverage =
  fixes g :: cfg and S :: "store set"
    and cover :: "cfg_node ⇒ 'c ⇒ store set"
    and adm :: "'c context_policy"
    and c⇩0 :: 'c
    and 𝒢 :: "vname ⇒ bool"
  assumes INIT[intro]: "⋀s. s ∈ S ⟹ s ∈ cover (cfg_entry g) c⇩0"
    and INTRA[intro]: "⋀u a v c s s'. (u, a, v) ∈ intra g
        ⟹ s ∈ cover u c ⟹ s' ∈ edge_step a s ⟹ s' ∈ cover v c"
    and CALL[intro]: "⋀u dst pars args p cont c c' s.
        (u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g
        ⟹ s ∈ cover u c
        ⟹ c' ∈ adm u c (call_info_of (CallEdge dst pars args) p) s
              (call_enter 𝒢 (CallEdge dst pars args) s)
        ⟹ call_enter 𝒢 (CallEdge dst pars args) s ∈ cover (FunctionEntry p) c'"
    and RETURN[intro]: "⋀u dst pars args p cont c c' p' s t es.
        (u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g
        ⟹ s ∈ cover u c
        ⟹ admits_call_context 𝒢 g adm u c p' s es c'
        ⟹ t ∈ cover (FunctionResult p) c'
        ⟹ combine_collect 𝒢 dst s t ∈ cover cont c"
    and TOTAL: "call_context_total_on cover adm 𝒢 g"
begin

text ‹The trace-level objects at the locale's fixed arguments: the collection ‹𝒞›, the
  valid activation traces ‹𝒯›, the context relation ‹carries›, the buckets ‹𝒜›, and the
  admitted call contexts ‹admits›.›
abbreviation collect :: "cfg_node ⇒ store set" ("𝒞")
  where "𝒞 ≡ 𝒞⇘𝒢,g,S⇙"
abbreviation traces :: "activation_trace set" ("𝒯")
  where "𝒯 ≡ 𝒯⇘𝒢,g,S⇙"
abbreviation carries :: "activation_trace ⇒ 'c ⇒ bool"
  where "carries ≡ activation_context_rel 𝒢 adm c⇩0 g"
abbreviation buckets :: "cfg_node ⇒ 'c ⇒ store set" ("𝒜")
  where "𝒜 ≡ 𝒜⇘𝒢,adm,c⇩0,g,S⇙"
abbreviation admits :: "cfg_node ⇒ 'c ⇒ pname ⇒ store ⇒ store ⇒ 'c ⇒ bool"
  where "admits ≡ admits_call_context 𝒢 g adm"

text ‹‹trace_covered u›: ‹u› carries some context, and its sink store is admitted at its
  own node under every context it carries.›
definition trace_covered :: "activation_trace ⇒ bool" where
  "trace_covered u ⟷
     (∃c. carries u c)
     ∧ (∀c. carries u c ⟶ sink_store u ∈ cover (sink_node u) c)"

lemma trace_coveredI:
  assumes "carries u c0"
    and "⋀c. carries u c ⟹ sink_store u ∈ cover (sink_node u) c"
  shows "trace_covered u"
  using assms unfolding trace_covered_def by blast

lemma trace_covered_someE:
  assumes "trace_covered u"
  obtains c where "carries u c" "sink_store u ∈ cover (sink_node u) c"
  using assms unfolding trace_covered_def by blast

lemma trace_coveredD:
  "trace_covered u ⟹ carries u c
   ⟹ sink_store u ∈ cover (sink_node u) c"
  unfolding trace_covered_def by blast

subsection ‹Closure under the four constructor clauses›

text ‹‹init_covered›: the main activation's seed store is admitted at ‹c⇩0›, the
  one context every \<^const>‹Root› carries.›
lemma init_covered: "s ∈ S ⟹ trace_covered (Root [(cfg_entry g, s)])"
  by (auto simp: trace_covered_def)

text ‹‹intra_covered›: an intra edge preserves the carried contexts (‹activation_context_rel_extend›)
  and covers the concrete step through ‹INTRA› at each of them.›
lemma intra_covered:
  assumes e: "(sink_node t, a, v) ∈ intra g"
    and st: "s' ∈ edge_step a (sink_store t)" and pne: "path_of t ≠ []" and iht: "trace_covered t"
  shows "trace_covered (extend t (v, s'))"
  using iht unfolding trace_covered_def
  by (auto simp: activation_context_rel_extend[OF pne] intro: INTRA[OF e _ st])

text ‹‹call_covered›: ‹TOTAL› gives the new activation some context, from a context its
  caller carries; ‹CALL› covers the entered store at every context it carries, each of
  which names its own edge out of the call site.›
lemma call_covered:
  assumes e: "(sink_node caller, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
    and ihc: "trace_covered caller"
  shows "trace_covered (Call caller
           [(FunctionEntry p, call_enter 𝒢 (CallEdge dst pars args) (sink_store caller))])"
proof -
  let ?es = "call_enter 𝒢 (CallEdge dst pars args) (sink_store caller)"
  from ihc obtain c where c: "carries caller c"
    and cov: "sink_store caller ∈ cover (sink_node caller) c"
    by (rule trace_covered_someE)
  obtain c' where
    adm: "admits (sink_node caller) c p (sink_store caller) ?es c'"
    by (rule call_context_total_onE[OF TOTAL e cov])
  have some: "carries (Call caller [(FunctionEntry p, ?es)]) c'"
    using c adm by (rule activation_context_rel.Call)
  show ?thesis
  proof (rule trace_coveredI[OF some])
    fix c' assume "carries (Call caller [(FunctionEntry p, ?es)]) c'"
    then obtain c0 where c0: "carries caller c0"
      and adm0: "admits (sink_node caller) c0 p (sink_store caller) ?es c'"
      by (auto simp: activation_context_rel_Call_iff)
    from adm0 obtain dst' pars' args' cont'
      where e': "(sink_node caller, CallEdge dst' pars' args', FunctionEntry p, cont') ∈ calls g"
        and es: "?es = call_enter 𝒢 (CallEdge dst' pars' args') (sink_store caller)"
        and Rc: "c' ∈ adm (sink_node caller) c0 (call_info_of (CallEdge dst' pars' args') p)
                   (sink_store caller) ?es"
      by (rule admits_call_contextE)
    have "sink_store caller ∈ cover (sink_node caller) c0"
      using ihc c0 by (rule trace_coveredD)
    from CALL[OF e' this Rc[unfolded es]] es
    show "sink_store (Call caller [(FunctionEntry p, ?es)])
            ∈ cover (sink_node (Call caller [(FunctionEntry p, ?es)])) c'" by simp
  qed
qed

text ‹‹return_covered›: the matched return.  For each context ‹c› the resumed caller carries,
  ‹TOTAL› re-enters the callee at a context ‹c'› admitted from ‹c› along the callee's own
  entry edge (‹activation_context_rel_caller_entry›, both directions), the callee's hypothesis
  bounds its exit at ‹c'›, and ‹RETURN› composes the two at ‹c› --- never at a context
  rediscovered independently.›
lemma return_covered:
  assumes callee_val: "callee ∈ 𝒯"
    and cof: "caller_of callee = Some caller"
    and res: "sink_node callee = FunctionResult p"
    and comb: "(sink_node caller, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
    and ih_caller: "trace_covered caller"
    and ih_callee: "trace_covered callee"
  shows "trace_covered (Resume caller callee (path_of caller
               @ [(cont, combine_collect 𝒢 dst (sink_store caller) (sink_store callee))]))"
proof -
  let ?u = "Resume caller callee (path_of caller
    @ [(cont, combine_collect 𝒢 dst (sink_store caller) (sink_store callee))])"
  have sn: "sink_node ?u = cont"
    and ss: "sink_store ?u = combine_collect 𝒢 dst (sink_store caller) (sink_store callee)"
    by (simp_all add: sink_node_def sink_store_def)
  from ih_caller obtain c1 where c1: "carries caller c1"
    by (rule trace_covered_someE)
  have some: "carries ?u c1" using c1 by simp
  from ih_callee obtain ce where ce: "carries callee ce"
    by (rule trace_covered_someE)
  obtain c0 p' where hd: "hd (path_of callee) = (FunctionEntry p', entry_store callee)"
    and adm: "admits (sink_node caller) c0 p' (sink_store caller)
                (entry_store callee) ce"
    by (rule activation_context_rel_caller_entryE[OF callee_val cof ce])
  from adm obtain dst' pars' args' cont'
    where e': "(sink_node caller, CallEdge dst' pars' args', FunctionEntry p', cont') ∈ calls g"
      and es: "entry_store callee = call_enter 𝒢 (CallEdge dst' pars' args') (sink_store caller)"
    by (rule admits_call_contextE)
  show ?thesis
  proof (rule trace_coveredI[OF some])
    fix c assume "carries ?u c"
    then have cc: "carries caller c" by simp
    have s_cov: "sink_store caller ∈ cover (sink_node caller) c"
      using ih_caller cc by (rule trace_coveredD)
    obtain c' where adm': "admits (sink_node caller) c p' (sink_store caller)
                             (call_enter 𝒢 (CallEdge dst' pars' args') (sink_store caller)) c'"
      by (rule call_context_total_onE[OF TOTAL e' s_cov])
    have tc': "carries callee c'"
      by (rule activation_context_rel_caller_entryI[OF callee_val cof hd cc adm'[folded es]])
    have t_cov: "sink_store callee ∈ cover (FunctionResult p) c'"
      using trace_coveredD[OF ih_callee tc'] res by simp
    have "combine_collect 𝒢 dst (sink_store caller) (sink_store callee) ∈ cover cont c"
      by (rule RETURN[OF comb s_cov adm'[folded es] t_cov])
    then show "sink_store ?u ∈ cover (sink_node ?u) c" by (simp add: sn ss)
  qed
qed

subsection ‹The generic soundness theorem›

text ‹The bound holds along the whole caller chain, by \<^const>‹valid_activation_trace› rule induction
  feeding the four closure lemmas.  The chain, not a per-node statement, is what the
  ‹RETURN› case needs: it recovers its caller structurally, and the caller lies in the
  callee's chain.›
lemma caller_chain_covered:
  "t ∈ 𝒯 ⟹ ∀u ∈ callers t. trace_covered u"
proof (rule caller_chain_closure)
  fix s assume "s ∈ S"
  then show "trace_covered (Root [(cfg_entry g, s)])" by (rule init_covered)
next
  fix t a v s' assume ht: "t ∈ 𝒯" and ch: "∀u ∈ callers t. trace_covered u"
    and e: "(sink_node t, a, v) ∈ intra g" and st: "s' ∈ edge_step a (sink_store t)"
  have pt: "path_of t ≠ []" using ht valid_activation_trace_path_nonempty by blast
  have iht: "trace_covered t" using ch callers_refl by blast
  show "trace_covered (extend t (v, s'))" by (rule intra_covered[OF e st pt iht])
next
  fix caller dst pars args p cont
  assume ch: "∀u ∈ callers caller. trace_covered u"
    and e: "(sink_node caller, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
  have ihc: "trace_covered caller" using ch callers_refl by blast
  show "trace_covered (Call caller
          [(FunctionEntry p, call_enter 𝒢 (CallEdge dst pars args) (sink_store caller))])"
    by (rule call_covered[OF e ihc])
next
  fix callee caller p dst pars args cont
  assume cv: "callee ∈ 𝒯" and ch: "∀u ∈ callers callee. trace_covered u"
    and cof: "caller_of callee = Some caller" and res: "sink_node callee = FunctionResult p"
    and e: "(sink_node caller, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
  have ih_caller: "trace_covered caller" using ch cof callers_caller_subset callers_refl by blast
  have ih_callee: "trace_covered callee" using ch callers_refl by blast
  show "trace_covered (Resume caller callee (path_of caller
             @ [(cont, combine_collect 𝒢 dst (sink_store caller) (sink_store callee))]))"
    by (rule return_covered[OF cv cof res e ih_caller ih_callee])
qed

text ‹Every valid activation trace carries a context, and its sink lies in every slot it carries:
  \<^const>‹valid_activation_trace› is soundly over-approximated by ‹trace_covered›.›
theorem valid_activation_trace_covered: "t ∈ 𝒯 ⟹ trace_covered t"
proof -
  assume "t ∈ 𝒯"
  then have "∀u ∈ callers t. trace_covered u" by (rule caller_chain_covered)
  then show "trace_covered t" using callers_refl by blast
qed

theorem valid_activation_trace_has_context:
  assumes "t ∈ 𝒯"
  obtains c where "carries t c"
  using valid_activation_trace_covered[OF assms] by (rule trace_covered_someE)

theorem valid_activation_trace_covered_at:
  "t ∈ 𝒯 ⟹ carries t c
   ⟹ sink_store t ∈ cover (sink_node t) c"
  using valid_activation_trace_covered by (rule trace_coveredD)

text ‹Bridge (2) of \<^theory>‹Voblint_CFG.Activation_Trace_Collect›, earned: under ‹TOTAL› the
  context-insensitive collection is the union of the buckets.›
theorem node_collect_eq_Union_activation_collect:
  "𝒞 v = (⋃c. 𝒜 v c)"
proof
  show "𝒞 v ⊆ (⋃c. 𝒜 v c)"
  proof
    fix x assume "x ∈ 𝒞 v"
    then obtain t where t: "t ∈ 𝒯" "sink_node t = v" "sink_store t = x"
      by (rule node_collect_E)
    from valid_activation_trace_has_context[OF t(1)] obtain c where "carries t c" .
    with t show "x ∈ (⋃c. 𝒜 v c)" by blast
  qed
next
  show "(⋃c. 𝒜 v c) ⊆ 𝒞 v"
    by (rule Union_activation_collect_le_node_collect)
qed

text ‹The two results together: the claims of all contexts contain the context-insensitive
  collection.›
corollary node_collect_covered: "𝒞 v ⊆ (⋃c. cover v c)"
proof
  fix x assume "x ∈ 𝒞 v"
  then obtain t where t: "t ∈ 𝒯" "sink_node t = v" "sink_store t = x"
    by (rule node_collect_E)
  from valid_activation_trace_has_context[OF t(1)] obtain c where "carries t c" .
  then have "x ∈ cover v c"
    using valid_activation_trace_covered_at[OF t(1)] t(2,3) by blast
  then show "x ∈ (⋃c. cover v c)" by blast
qed

end

subsection ‹Non-vacuity›

text ‹The interface is satisfiable for every graph, seed set, and initial context: choosing
  the top cover ‹cover = (λ_ _. UNIV)› together with any total functional context policy
  discharges all five obligations, ‹TOTAL› included, since a functional policy is total
  (‹call_context_total_on_of_fun›). It is not satisfiable at an arbitrary ‹adm›: taking
  ‹adm = (λ_ _ _ _ _. {})› fails ‹TOTAL› for any graph with a reachable call, however
  wide ‹cover› is chosen --- ‹TOTAL› genuinely constrains the context policy, not merely
  the cover.›

lemma activation_coverage_exists:
  "activation_coverage g S (λ_ _. UNIV) (context_policy_of_fun (λ_ _ _. ())) () 𝒢"
  by unfold_locales auto

subsection ‹Monovariant semantic post-fixpoint›

text ‹
  Set-valued entry, edge, call, and combine closure of a candidate node map ‹B› bounds the
  stack-faithful \<^const>‹node_collect› at every node.  The proof interprets
  \<^locale>‹activation_coverage› at ‹cover v _ = B v› with the trivial one-point context, whose policy
  is total outright; its combine obligation follows one caller and one callee exit.
›
lemma node_collect_semantic_postfix:
  fixes g :: cfg and B :: "cfg_node ⇒ store set"
    and S0 :: "store set" and v :: cfg_node and 𝒢 :: "vname ⇒ bool"
  assumes entry: "S0 ⊆ B (cfg_entry g)"
    and edge: "⋀u a w s s'. (u, a, w) ∈ intra g
        ⟹ s ∈ B u ⟹ s' ∈ edge_step a s ⟹ s' ∈ B w"
    and call: "⋀u dst pars args p cont s.
        (u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g
        ⟹ s ∈ B u
        ⟹ call_enter 𝒢 (CallEdge dst pars args) s ∈ B (FunctionEntry p)"
    and combine: "⋀cl dst pars args p cont s t.
        (cl, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g
        ⟹ s ∈ B cl ⟹ t ∈ B (FunctionResult p)
        ⟹ combine_collect 𝒢 dst s t ∈ B cont"
  shows "𝒞⇘𝒢,g,S0⇙ v ⊆ B v"
proof -
  interpret G: activation_coverage g S0 "λv _. B v" "context_policy_of_fun (λ_ _ _. ())" "()" 𝒢
  proof (standard, goal_cases INIT INTRA CALL RETURN TOTAL)
    case (INIT s) then show ?case using entry by auto
  next
    case (INTRA u a w c s s') then show ?case using edge by simp
  next
    case (CALL u dst pars args p cont c c' s) then show ?case using call by simp
  next
    case (RETURN cl dst pars args p cont c1 c' p' s t es) then show ?case using combine by simp
  next
    case TOTAL then show ?case by simp
  qed
  show ?thesis
  proof (rule subsetI)
    fix x assume "x ∈ 𝒞⇘𝒢,g,S0⇙ v"
    then obtain u where u: "u ∈ 𝒯⇘𝒢,g,S0⇙" "sink_node u = v" "sink_store u = x"
      by (rule node_collect_E)
    from G.valid_activation_trace_has_context[OF u(1)] obtain c
      where c: "activation_context_rel 𝒢 (context_policy_of_fun (λ_ _ _. ())) () g u c" .
    have "sink_store u ∈ B (sink_node u)" using G.valid_activation_trace_covered_at[OF u(1) c]
      by simp
    then show "x ∈ B v" using u(2,3) by simp
  qed
qed


end