Theory CFG_Enumeration

theory CFG_Enumeration
  imports "Voblint_CFG.CFG_Def"
begin

section ‹Solver-facing CFG enumeration›

text ‹
  Backward predecessor relations and deterministic edge enumeration over a compiled
  two-relation CFG.  These are the equation-generation and code-generation views the TD
  solver reads to build and evaluate the constraint system; they are not part of the
  concrete CFG semantics --- ‹valid_activation_trace› never refers to them.  Ordinary control flow is
  enumerated over \<^const>‹intra›; procedure calls --- entry routing and return combining ---
  over \<^const>‹calls›.  There is no unified edge set and no separate combine relation: a
  return is recovered from the same \<^const>‹calls› tuple that created the activation.

  Every enumeration appears twice: as a set, which the proofs reason over, and as a list,
  which code generation and the solver's folds consume, identified by a ‹set_..._list›
  lemma whenever the edge set is finite.  On the return side there is one of each ---
  the set ‹call_targets› and the list ‹call_target_list› --- and every other return view
  is an image or a ‹map› of those, so the views cannot come to disagree about which edges
  they enumerate.
›

subsection ‹Intra predecessors›

text ‹The ordinary incoming transitions of a node: an intra edge is a total store
  transformer within one activation, so this is the transfer fold the equation system runs
  at every node --- including the \<^term>‹EA_Ret e p› edges into \<^term>‹FunctionResult p›, by
  which return values are summarised as ordinary predecessor folding.›

definition intra_predecessors :: "cfg ⇒ cfg_node ⇒ (cfg_node × edge_action) set" where
  "intra_predecessors g v = {(u, a). (u, a, v) ∈ intra g}"

lemma intra_predecessors_iff [simp]:
  "(u, a) ∈ intra_predecessors g v ⟷ (u, a, v) ∈ intra g"
  by (simp add: intra_predecessors_def)

lemma finite_intra_predecessors [intro]:
  assumes "finite (intra g)"
  shows "finite (intra_predecessors g v)"
proof -
  have "intra_predecessors g v
          ⊆ (λe :: cfg_node × edge_action × cfg_node. (fst e, fst (snd e))) ` intra g"
    unfolding intra_predecessors_def by force
  then show ?thesis using assms finite_subset finite_imageI by blast
qed

definition intra_predecessor_list ::
    "cfg ⇒ cfg_node ⇒ (cfg_node × edge_action) list" where
  "intra_predecessor_list g v =
     map (λ(u, a, w). (u, a)) (filter (λ(u, a, w). w = v) (cfg_intra_list g))"

lemma set_intra_predecessor_list [simp]:
  assumes "finite (intra g)"
  shows "set (intra_predecessor_list g v) = intra_predecessors g v"
  unfolding intra_predecessor_list_def intra_predecessors_def
  using set_cfg_intra_list[OF assms] by (force simp: image_iff)

subsection ‹Call-entry enumeration›

text ‹The call tuples whose callee entry is the queried node ‹v› (a \<^term>‹FunctionEntry p›).
  The continuation does not affect the callee-entry state, so it is projected away; the
  entry contribution is the caller state routed through the call action's parameter
  binding, which is what an analysis's entry operation computes.›

definition entry_calls :: "cfg ⇒ cfg_node ⇒ (cfg_node × call_action) set" where
  "entry_calls g v = {(c, ca). ∃k. (c, ca, v, k) ∈ calls g}"

lemma entry_calls_iff [simp]:
  "(c, ca) ∈ entry_calls g v ⟷ (∃k. (c, ca, v, k) ∈ calls g)"
  by (simp add: entry_calls_def)

lemma finite_entry_calls [intro]:
  assumes "finite (calls g)"
  shows "finite (entry_calls g v)"
proof -
  have "entry_calls g v
          ⊆ (λe :: cfg_node × call_action × cfg_node × cfg_node. (fst e, fst (snd e))) ` calls g"
    unfolding entry_calls_def by force
  then show ?thesis using assms finite_subset finite_imageI by blast
qed

definition entry_call_list :: "cfg ⇒ cfg_node ⇒ (cfg_node × call_action) list" where
  "entry_call_list g v =
     map (λ(c, ca, ce, k). (c, ca)) (filter (λ(c, ca, ce, k). ce = v) (cfg_calls_list g))"

lemma set_entry_call_list [simp]:
  assumes "finite (calls g)"
  shows "set (entry_call_list g v) = entry_calls g v"
  unfolding entry_call_list_def entry_calls_def
  using set_cfg_calls_list[OF assms] by (force simp: image_iff)

subsection ‹Outgoing call enumeration (caller perspective)›

text ‹The call tuples whose call site is the queried node ‹v›: the entry, action, and
  continuation of every call ‹v› makes. This is the caller-side counterpart of
  \<^const>‹entry_calls› (callee-indexed) --- routing a call-entry seed publication at its call
  site needs the callee entry and the whole \<^typ>‹call_action› together, which the
  continuation-indexed enumerations below do not expose.›

definition call_successors ::
    "cfg ⇒ cfg_node ⇒ (cfg_node × call_action × cfg_node) set" where
  "call_successors g v = {(ce, ca, k). (v, ca, ce, k) ∈ calls g}"

lemma call_successors_iff [simp]:
  "(ce, ca, k) ∈ call_successors g v ⟷ (v, ca, ce, k) ∈ calls g"
  by (simp add: call_successors_def)

lemma finite_call_successors [intro]:
  assumes "finite (calls g)"
  shows "finite (call_successors g v)"
proof -
  have "call_successors g v
          ⊆ (λ(c, ca, ce, k). (ce, ca, k)) ` calls g"
    unfolding call_successors_def by force
  then show ?thesis using assms finite_subset finite_imageI by blast
qed

definition call_successor_list ::
    "cfg ⇒ cfg_node ⇒ (cfg_node × call_action × cfg_node) list" where
  "call_successor_list g v =
     map (λ(c, ca, ce, k). (ce, ca, k)) (filter (λ(c, ca, ce, k). c = v) (cfg_calls_list g))"

lemma set_call_successor_list [simp]:
  assumes "finite (calls g)"
  shows "set (call_successor_list g v) = call_successors g v"
  unfolding call_successor_list_def call_successors_def
  using set_cfg_calls_list[OF assms] by (force simp: image_iff)


subsection ‹Call targets at a continuation›

text ‹
  The call edges whose continuation is ‹v›, each paired with the procedure its callee entry
  names.  This is the one continuation-indexed enumeration that reads \<^const>‹calls›
  directly; every return-side view below is an image or a map of it.

  ‹call_target_at› decodes a single call edge, selecting on the continuation and reading the
  callee's procedure off \<^term>‹FunctionEntry p› in one total function, so there is no
  unreachable-but-present branch and no later definition has to re-establish that the node
  it is looking at really is a callee entry.

  Naming the callee by its procedure rather than by the \<^term>‹FunctionResult p› node its
  result is read at keeps the call site's own data --- where the call is, what it passes,
  where it returns to --- separate from the callee, which is what lets a resolver choose
  among candidates rather than read a callee the enumeration already fixed.  The result
  node is then ‹FunctionResult p› at the point of use.
›

definition call_targets ::
    "cfg ⇒ cfg_node ⇒ (cfg_node × call_action × pname) set" where
  "call_targets g v = {(c, ca, p). (c, ca, FunctionEntry p, v) ∈ calls g}"

lemma call_targets_iff [simp]:
  "(c, ca, p) ∈ call_targets g v ⟷ (c, ca, FunctionEntry p, v) ∈ calls g"
  by (simp add: call_targets_def)

fun call_target_at ::
    "cfg_node ⇒ (cfg_node × call_action × cfg_node × cfg_node)
       ⇒ (cfg_node × call_action × pname) option" where
  "call_target_at v (c, ca, FunctionEntry p, k) =
     (if k = v then Some (c, ca, p) else None)"
| "call_target_at v _ = None"

definition call_target_list ::
    "cfg ⇒ cfg_node ⇒ (cfg_node × call_action × pname) list" where
  "call_target_list g v = List.map_filter (call_target_at v) (cfg_calls_list g)"

lemma set_map_filter_call_target_at:
  "set (List.map_filter (call_target_at v) es)
     = {(c, ca, p). (c, ca, FunctionEntry p, v) ∈ set es}"
proof (induction es)
  case Nil
  show ?case by simp
next
  case (Cons e es)
  obtain c ca ce k where e: "e = (c, ca, ce, k)" by (cases e) auto
  show ?case by (cases ce) (auto simp: e Cons.IH)
qed

text ‹Membership, in the form a call-site obligation states it: the enumeration lists
  exactly the call edges of ‹g› whose continuation is ‹v›, each paired with the
  procedure its callee entry names.›

lemma set_call_target_list [simp]:
  assumes "finite (calls g)"
  shows "set (call_target_list g v) = call_targets g v"
  unfolding call_target_list_def call_targets_def
  by (simp add: set_map_filter_call_target_at set_cfg_calls_list[OF assms])

lemma finite_call_targets [intro]:
  assumes "finite (calls g)"
  shows "finite (call_targets g v)"
proof -
  have "call_targets g v = set (call_target_list g v)"
    using set_call_target_list[OF assms] by simp
  then show ?thesis by simp
qed

text ‹The enumeration lists each call edge once: \<^const>‹cfg_calls_list› is duplicate-free
  and \<^const>‹call_target_at› discards exactly the components a decoded entry does not
  determine.  This is what makes the site and target lists below duplicate-free too, so
  the generator builds one contribution per site-target pair rather than one per pair of
  co-listed callees.›

lemma distinct_map_filter_call_target_at:
  assumes "distinct es"
  shows "distinct (List.map_filter (call_target_at v) es)"
  using assms
proof (induction es)
  case Nil
  show ?case by simp
next
  case (Cons e es)
  obtain c ca ce k where e: "e = (c, ca, ce, k)" by (cases e) auto
  show ?case
    using Cons by (cases ce) (auto simp: e set_map_filter_call_target_at)
qed

lemma distinct_call_target_list [simp]:
  assumes "finite (calls g)"
  shows "distinct (call_target_list g v)"
  unfolding call_target_list_def
  by (rule distinct_map_filter_call_target_at) (simp add: cfg_calls_list_def assms)

lemma call_target_list_iff:
  assumes "finite (calls g)"
  shows "(c, ca, p) ∈ set (call_target_list g v)
           ⟷ (c, ca, FunctionEntry p, v) ∈ calls g"
  by (simp add: set_call_target_list[OF assms])


subsection ‹Return enumeration›

text ‹The return edges, as an image of \<^const>‹call_targets› that keeps the triggering
  \<^typ>‹call_action› whole.  The return contribution is the caller state and the callee-exit
  state assembled by ‹combine⇧♯›.  The callee's \<^term>‹FunctionResult p› node comes back
  directly --- recovered from the callee entry \<^term>‹FunctionEntry p› --- so no separate
  combine relation is needed and no client has to rebuild the result node.

  The action is kept whole rather than packaged into the call's \<^typ>‹call_info›, because
  the generator must route the callee-entry seed publication and the return-side context
  read from the ∗‹same› action, exactly as \<^const>‹entry_call_list› keeps ‹ca› whole on
  the entry side.  This layer is the only one holding the \<^const>‹calls› relation, so
  whatever a consumer needs about a call site is projected here: a combine tree never sees
  the CFG, and \<^const>‹wf_cfg› does not force a call site's outgoing call edge to be
  unique, so there is no well-defined downstream lookup that could recover it instead.›

definition return_call_actions ::
    "cfg ⇒ cfg_node ⇒ (cfg_node × call_action × cfg_node) set" where
  "return_call_actions g v =
     (λ(c, ca, p). (c, ca, FunctionResult p)) ` call_targets g v"

lemma return_call_actions_iff [simp]:
  "(c, ca, r) ∈ return_call_actions g v
     ⟷ (∃p. r = FunctionResult p ∧ (c, ca, FunctionEntry p, v) ∈ calls g)"
  by (auto simp: return_call_actions_def image_iff Bex_def)

lemma finite_return_call_actions [intro]:
  assumes "finite (calls g)"
  shows "finite (return_call_actions g v)"
  using finite_call_targets[OF assms] by (simp add: return_call_actions_def)

definition return_call_action_list ::
    "cfg ⇒ cfg_node ⇒ (cfg_node × call_action × cfg_node) list" where
  "return_call_action_list g v =
     map (λ(c, ca, p). (c, ca, FunctionResult p)) (call_target_list g v)"

lemma set_return_call_action_list [simp]:
  assumes "finite (calls g)"
  shows "set (return_call_action_list g v) = return_call_actions g v"
  unfolding return_call_action_list_def return_call_actions_def
  by (simp add: set_call_target_list[OF assms])

subsection ‹Call sites and the resolver adapter›

text ‹
  The call site alone, with no callee: what a call-site-owned resolver is given.  The list
  is duplicate-free, so a site with several statically known callees is listed once; with
  ‹distinct_static_targets› below, resolving every listed site therefore visits each
  site-target pair exactly once.

  ‹static_targets› below is the resolver that answers from the CFG and ignores the caller's
  abstract state --- the behaviour a statically enumerated generator already has.  A
  resolver reading that state instead is what makes an indirect call expressible, and the
  shape of the equation does not change when it does.  Two limits are worth stating,
  because the resolver type ‹cfg ⇒ cfg_node ⇒ cfg_node ⇒ call_action ⇒ 'd ⇒ pname list›
  does not: a resolver may answer with any procedures at all, so a sound instance needs an
  explicit coverage assumption relating its answer to the concrete callees reachable at the
  site; and the sites themselves come from \<^const>‹call_target_list›, so a call with no
  statically enumerated target is not listed and no resolver is consulted for it.  What
  this supports is therefore state-dependent choice among enumerated candidates, not a
  fully late-bound call whose site exists independently of any known target.
›

definition call_site_list ::
    "cfg ⇒ cfg_node ⇒ (cfg_node × call_action) list" where
  "call_site_list g v = remdups (map (λ(c, ca, p). (c, ca)) (call_target_list g v))"

lemma distinct_call_site_list [simp]:
  "distinct (call_site_list g v)"
  by (simp add: call_site_list_def)

lemma set_call_site_list [simp]:
  assumes "finite (calls g)"
  shows "set (call_site_list g v)
           = {(c, ca) | c ca. ∃p. (c, ca, FunctionEntry p, v) ∈ calls g}"
  unfolding call_site_list_def
  by (force simp: set_call_target_list[OF assms] call_targets_def image_iff)

definition static_targets ::
    "cfg ⇒ cfg_node ⇒ cfg_node ⇒ call_action ⇒ pname list" where
  "static_targets g v cc ca =
     map (λ(c, a, p). p)
       (filter (λ(c, a, p). c = cc ∧ a = ca) (call_target_list g v))"

lemma static_targets_iff [simp]:
  assumes "finite (calls g)"
  shows "p ∈ set (static_targets g v cc ca)
           ⟷ (cc, ca, FunctionEntry p, v) ∈ calls g"
  unfolding static_targets_def
  by (force simp: call_target_list_iff[OF assms, symmetric] image_iff)

lemma distinct_static_targets [simp]:
  assumes "finite (calls g)"
  shows "distinct (static_targets g v cc ca)"
proof -
  let ?es = "filter (λ(c, a, p). c = cc ∧ a = ca) (call_target_list g v)"
  have "inj_on (λ(c, a, p). p) (set ?es)" by (auto simp: inj_on_def)
  moreover have "distinct ?es" using distinct_call_target_list[OF assms] by simp
  ultimately show ?thesis unfolding static_targets_def by (simp add: distinct_map)
qed

text ‹Exactly when a site has a statically known callee, which is the form a coverage
  obligation stated over the enumeration needs.›

lemma static_targets_neq_Nil_iff [simp]:
  assumes "finite (calls g)"
  shows "static_targets g v cc ca ≠ []
           ⟷ (∃p. (cc, ca, FunctionEntry p, v) ∈ calls g)"
proof -
  have "static_targets g v cc ca ≠ [] ⟷ (∃p. p ∈ set (static_targets g v cc ca))"
    by (cases "static_targets g v cc ca") auto
  thus ?thesis using static_targets_iff[OF assms] by blast
qed

definition static_resolve ::
  "cfg ⇒ cfg_node ⇒ cfg_node ⇒ call_action ⇒ 'd ⇒ pname list" where
  "static_resolve g v cc ca d = static_targets g v cc ca"

lemma static_resolve_iff [simp]:
  assumes "finite (calls g)"
  shows "p ∈ set (static_resolve g v cc ca d)
           ⟷ (cc, ca, FunctionEntry p, v) ∈ calls g"
  unfolding static_resolve_def by (rule static_targets_iff[OF assms])

section ‹Which unknowns a run has to have solved›

text ‹
  ‹vars_cover g vars› is the one recurring premise every post-solution
  soundness theorem here needs: the solved key set ‹vars› contains the CFG
  entry, the target of every ‹intra› edge, and both halves of every call ---
  the callee's entry and the caller's continuation.

  Read it as a statement about a solver run, not about the graph. It
  quantifies over every edge ‹g› has, so a graph carrying a call the run never
  activated does not satisfy it: in a routed system a callee's entry unknown is
  solved only once some caller publishes its seed, and an unreachable call site
  publishes nothing. That is why a run establishes it by deciding
  ‹vars_cover_exec› against the keys it actually solved, on a graph
  ∗‹pruned› to what it can reach, rather than by an argument about
  connectivity.

  The four components travel together, so callers state and discharge one
  premise instead of four positional ones. Global, not locale-local: every
  analysis instance and the executable pipeline cite it under this name.
›

definition vars_cover :: "cfg ⇒ (cfg_node × unit) set ⇒ bool" where
  "vars_cover g vars ⟷
     (cfg_entry g, ()) ∈ vars
   ∧ (∀u a v. (u, a, v) ∈ intra g ⟶ (v, ()) ∈ vars)
   ∧ (∀c dst fs as q k. (c, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g
        ⟶ (FunctionEntry q, ()) ∈ vars ∧ (k, ()) ∈ vars)"

lemma vars_coverI [intro]:
  assumes "(cfg_entry g, ()) ∈ vars"
    and "⋀u a v. (u, a, v) ∈ intra g ⟹ (v, ()) ∈ vars"
    and "⋀c dst fs as q k. (c, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g
           ⟹ (FunctionEntry q, ()) ∈ vars"
    and "⋀c dst fs as q k. (c, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g
           ⟹ (k, ()) ∈ vars"
  shows "vars_cover g vars"
  unfolding vars_cover_def using assms by blast

lemma vars_cover_entryD [dest]: "vars_cover g vars ⟹ (cfg_entry g, ()) ∈ vars"
  unfolding vars_cover_def by blast

lemma vars_cover_edgeD [dest]:
  "vars_cover g vars ⟹ (u, a, v) ∈ intra g ⟹ (v, ()) ∈ vars"
  unfolding vars_cover_def by blast

lemma vars_cover_enterD [dest]:
  assumes cover: "vars_cover g vars"
  shows "⋀c dst fs as q k. (c, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g
     ⟹ (FunctionEntry q, ()) ∈ vars"
  using cover unfolding vars_cover_def by blast

lemma vars_cover_combineD [dest]:
  assumes cover: "vars_cover g vars"
  shows "⋀c dst fs as q k. (c, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g
     ⟹ (k, ()) ∈ vars"
  using cover unfolding vars_cover_def by blast

text ‹
  Coverage of a finite graph is testable: walk the two edge enumerations and
  test membership. The test is sufficient, not equivalent, and deliberately so.
  \<^const>‹vars_cover› asks only about calls of the shape
  ‹(c, CallEdge dst fs as, FunctionEntry q, k)›, while the test asks about
  every tuple the enumeration yields, so it is the stronger of the two: it also
  covers a ‹calls› entry whose action or target has some other shape. Turning
  it into an equivalence would mean assuming that ‹g› has no such entry, which
  is a well-formedness fact about the graph and not something a coverage check
  should carry.
›

definition vars_cover_exec :: "cfg ⇒ (cfg_node × unit) set ⇒ bool" where
  "vars_cover_exec g vars ⟷
     (cfg_entry g, ()) ∈ vars
   ∧ list_all (λ(u, a, v). (v, ()) ∈ vars) (cfg_intra_list g)
   ∧ list_all (λ(c, ca, ce, k). (ce, ()) ∈ vars ∧ (k, ()) ∈ vars) (cfg_calls_list g)"


subsection ‹Coverage when the unknowns carry a context›

text ‹
  \<^const>‹vars_cover› is fixed at the unit context: its unknowns are nodes, so it
  can demand that every successor of every edge was solved.  A context-sensitive
  system cannot demand that.  Its unknowns are node-context pairs, and which
  contexts a node was solved at is decided by the run, so coverage becomes
  ∗‹closure›: whenever a pair was solved, the pairs its edges lead to were
  solved too.  Hence the conditional shape here against the unconditional shape
  above.

  Where a call leads is not a fact about the graph.  A context policy computes
  the callee's context from the call site, the caller's context, the callee, and
  in general the state published at the call --- which is why ‹succ_ctx› is a
  parameter rather than something read off ‹g›.  An instance supplies its own
  route already applied to its own solved environment.

  The return side takes no such argument: a combine resumes the caller's own
  activation, so the continuation is covered at the context the call was made
  in.
›

definition ctx_vars_cover ::
    "cfg ⇒ (cfg_node ⇒ 'c ⇒ call_action ⇒ pname ⇒ 'c) ⇒ 'c
       ⇒ (cfg_node × 'c) set ⇒ bool" where
  "ctx_vars_cover g succ_ctx rc vars ⟷
     (cfg_entry g, rc) ∈ vars
   ∧ (∀u a v ctx. (u, ctx) ∈ vars ⟶ (u, a, v) ∈ intra g ⟶ (v, ctx) ∈ vars)
   ∧ (∀u ctx dst fs as q k. (u, ctx) ∈ vars
        ⟶ (u, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g
        ⟶ (FunctionEntry q, succ_ctx u ctx (CallEdge dst fs as) q) ∈ vars
          ∧ (k, ctx) ∈ vars)"

lemma ctx_vars_coverI [intro]:
  assumes "(cfg_entry g, rc) ∈ vars"
    and "⋀u a v ctx. (u, ctx) ∈ vars ⟹ (u, a, v) ∈ intra g ⟹ (v, ctx) ∈ vars"
    and "⋀u ctx dst fs as q k. (u, ctx) ∈ vars
           ⟹ (u, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g
           ⟹ (FunctionEntry q, succ_ctx u ctx (CallEdge dst fs as) q) ∈ vars"
    and "⋀u ctx dst fs as q k. (u, ctx) ∈ vars
           ⟹ (u, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g ⟹ (k, ctx) ∈ vars"
  shows "ctx_vars_cover g succ_ctx rc vars"
  unfolding ctx_vars_cover_def using assms by blast

lemma ctx_vars_cover_entryD [dest]:
  "ctx_vars_cover g succ_ctx rc vars ⟹ (cfg_entry g, rc) ∈ vars"
  unfolding ctx_vars_cover_def by blast

lemma ctx_vars_cover_edgeD [dest]:
  "ctx_vars_cover g succ_ctx rc vars ⟹ (u, ctx) ∈ vars ⟹ (u, a, v) ∈ intra g
     ⟹ (v, ctx) ∈ vars"
  unfolding ctx_vars_cover_def by blast

lemma ctx_vars_cover_enterD [dest]:
  assumes cover: "ctx_vars_cover g succ_ctx rc vars"
  shows "⋀u ctx dst fs as q k. (u, ctx) ∈ vars
     ⟹ (u, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g
     ⟹ (FunctionEntry q, succ_ctx u ctx (CallEdge dst fs as) q) ∈ vars"
  using cover unfolding ctx_vars_cover_def by blast

lemma ctx_vars_cover_combineD [dest]:
  assumes cover: "ctx_vars_cover g succ_ctx rc vars"
  shows "⋀u ctx dst fs as q k. (u, ctx) ∈ vars
     ⟹ (u, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g ⟹ (k, ctx) ∈ vars"
  using cover unfolding ctx_vars_cover_def by blast

text ‹
  Contextual coverage is testable the way the unit one is, with one difference
  that decides the shape: closure quantifies over the pairs the run solved, and
  those are not enumerable from the graph.  So the test walks the solved keys
  against the two edge enumerations rather than walking the graph alone, which
  is why it takes them as the set the solver returns and iterates over it.

  Sufficient rather than equivalent, and deliberately so.  At a call the test
  asks for the continuation at every action shape, while \<^const>‹ctx_vars_cover›
  asks only about ‹CallEdge›; demanding the callee entry off a non-call action
  would need a context the policy never computes, so that one stays guarded.
›

definition ctx_vars_cover_exec ::
    "cfg ⇒ (cfg_node ⇒ 'c ⇒ call_action ⇒ pname ⇒ 'c) ⇒ 'c
       ⇒ (cfg_node × 'c) set ⇒ bool" where
  "ctx_vars_cover_exec g succ_ctx rc vs ⟷
     (cfg_entry g, rc) ∈ vs
   ∧ (∀(u, ctx) ∈ vs.
        list_all (λ(u', a, v). u' ≠ u ∨ (v, ctx) ∈ vs) (cfg_intra_list g)
      ∧ list_all (λ(c, ca, ce, k). c ≠ u ∨ ((k, ctx) ∈ vs
             ∧ (case ce of FunctionEntry q ⇒ (ce, succ_ctx u ctx ca q) ∈ vs
                  | _ ⇒ True)))
          (cfg_calls_list g))"

lemma ctx_vars_cover_of_exec:
  assumes finE: "finite (intra g)" and finC: "finite (calls g)"
    and cover: "ctx_vars_cover_exec g succ_ctx rc (vs :: (cfg_node × 'c) set)"
  shows "ctx_vars_cover g succ_ctx rc vs"
proof (intro ctx_vars_coverI)
  show "(cfg_entry g, rc) ∈ vs"
    using cover unfolding ctx_vars_cover_exec_def by blast
next
  fix u a v ctx
  assume "(u, ctx) ∈ vs" and "(u, a, v) ∈ intra g"
  then show "(v, ctx) ∈ vs"
    using cover unfolding ctx_vars_cover_exec_def
    by (fastforce simp: list_all_iff set_cfg_intra_list [OF finE])
next
  fix u ctx dst fs as q k
  assume "(u, ctx) ∈ vs"
    and "(u, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g"
  then show "(FunctionEntry q, succ_ctx u ctx (CallEdge dst fs as) q) ∈ vs"
    using cover unfolding ctx_vars_cover_exec_def
    by (fastforce simp: list_all_iff set_cfg_calls_list [OF finC])
next
  fix u ctx dst fs as q k
  assume "(u, ctx) ∈ vs"
    and "(u, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g"
  then show "(k, ctx) ∈ vs"
    using cover unfolding ctx_vars_cover_exec_def
    by (fastforce simp: list_all_iff set_cfg_calls_list [OF finC])
qed


subsection ‹Coverage along live dependencies›

text ‹
  \<^const>‹ctx_vars_cover› demands closure from every solved pair, including pairs
  whose solved state is bottom and calls whose entered state is bottom.  A
  demand-driven solver never solves what such a pair would lead to, so the
  unconditional closure fails on dead call sites and on procedures nothing calls,
  while soundness only ever follows a dependency from a state that holds a
  concrete store.  The live form asks for exactly that much.

  ‹live u ctx› says the state solved at ‹(u, ctx)› may hold a store; an intra
  successor is demanded only from a live pair.  ‹succ u ctx ca q› is the callee
  context a call routes to, or ‹None› when the entered state is bottom and the
  call contributes nothing; the callee entry is demanded only when it is
  ‹Some›.  The continuation stays unconditional: a call site is queried only by
  its own continuation's call tree, so a solver never solves the one without the
  other.
›

definition ctx_vars_cover_live ::
    "cfg ⇒ (cfg_node ⇒ 'c ⇒ bool) ⇒ (cfg_node ⇒ 'c ⇒ call_action ⇒ pname ⇒ 'c option)
       ⇒ 'c ⇒ (cfg_node × 'c) set ⇒ bool" where
  "ctx_vars_cover_live g live succ rc vars ⟷
     (cfg_entry g, rc) ∈ vars
   ∧ (∀u a v ctx. (u, ctx) ∈ vars ⟶ live u ctx ⟶ (u, a, v) ∈ intra g
        ⟶ (v, ctx) ∈ vars)
   ∧ (∀u ctx dst fs as q k. (u, ctx) ∈ vars
        ⟶ (u, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g
        ⟶ (k, ctx) ∈ vars
          ∧ (∀ctx'. succ u ctx (CallEdge dst fs as) q = Some ctx'
               ⟶ (FunctionEntry q, ctx') ∈ vars))"

lemma ctx_vars_cover_liveI [intro]:
  assumes "(cfg_entry g, rc) ∈ vars"
    and "⋀u a v ctx. (u, ctx) ∈ vars ⟹ live u ctx ⟹ (u, a, v) ∈ intra g
           ⟹ (v, ctx) ∈ vars"
    and "⋀u ctx dst fs as q k ctx'. (u, ctx) ∈ vars
           ⟹ (u, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g
           ⟹ succ u ctx (CallEdge dst fs as) q = Some ctx'
           ⟹ (FunctionEntry q, ctx') ∈ vars"
    and "⋀u ctx dst fs as q k. (u, ctx) ∈ vars
           ⟹ (u, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g ⟹ (k, ctx) ∈ vars"
  shows "ctx_vars_cover_live g live succ rc vars"
  unfolding ctx_vars_cover_live_def using assms by blast

lemma ctx_vars_cover_live_entryD [dest]:
  "ctx_vars_cover_live g live succ rc vars ⟹ (cfg_entry g, rc) ∈ vars"
  unfolding ctx_vars_cover_live_def by blast

lemma ctx_vars_cover_live_edgeD [dest]:
  "ctx_vars_cover_live g live succ rc vars ⟹ (u, ctx) ∈ vars ⟹ live u ctx
     ⟹ (u, a, v) ∈ intra g ⟹ (v, ctx) ∈ vars"
  unfolding ctx_vars_cover_live_def by blast

lemma ctx_vars_cover_live_enterD [dest]:
  "ctx_vars_cover_live g live succ rc vars ⟹ (u, ctx) ∈ vars
     ⟹ (u, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g
     ⟹ succ u ctx (CallEdge dst fs as) q = Some ctx' ⟹ (FunctionEntry q, ctx') ∈ vars"
  unfolding ctx_vars_cover_live_def by blast

lemma ctx_vars_cover_live_combineD [dest]:
  "ctx_vars_cover_live g live succ rc vars ⟹ (u, ctx) ∈ vars
     ⟹ (u, CallEdge dst fs as, FunctionEntry q, k) ∈ calls g ⟹ (k, ctx) ∈ vars"
  unfolding ctx_vars_cover_live_def by blast

end