Theory Voblint_Routing.Compiled_Routed_Equations

theory Compiled_Routed_Equations
  imports
    "Voblint_Framework.Routed_Context"
    "Voblint_Compile.Compile_Wellformed"
    "HOL-Library.RBT"
begin

section ‹Executable routed equations for a compiled program›

text ‹
  A routed configuration chooses the key a node buffers its own global part at,
  the key each global name is read and published at, a seed-key constructor, a
  routing function, a D/G specification, an initial local state and an initial
  global state. The remaining equation-system wiring is fixed: predecessor
  enumeration, edge execution, static call resolution, seed publication, and
  bottom initialization of every other unknown.

  A context-insensitive analysis is this constructor at the unit context:
  ‹Analysis_Global ()› as the only global key, ‹Activation_Seed› as the seed
  constructor and ‹route_unit› as the routing function. There is no second
  unit-context generator.

  Solver policy is deliberately outside this constructor. Always-join,
  per-origin, and warrowing instances can solve the same equations without
  hiding that choice here.

  The enumerations the equations read are stated over the edge relations and
  answer every query by re-enumerating a whole relation. The code equation at
  the end answers them from indexes built once per graph instead, so a solver
  step costs a lookup rather than a scan and sort of every edge.
›

definition compiled_routed_eqs_for ::
    "'K
      ⇒ ('N ⇒ 'K)
      ⇒ (pp ⇒ 'C ⇒ 'K)
      ⇒ (pp ⇒ 'C ⇒ 'D ⇒ call_action ⇒ 'C)
      ⇒ (pp × 'C, 'K, 'N,
           'D::bounded_semilattice_sup_bot, 'G::bounded_semilattice_sup_bot) dg_spec
      ⇒ cfg
      ⇒ 'D
      ⇒ 'G
      ⇒ (pp × 'C, 'K, ('D, 'G) dg_state) eqsT"
where
  "compiled_routed_eqs_for global global_of seed route S g initial initial_global =
     routed_node_rhs_buffered intra_predecessor_addr_list call_site_list
       (λ_. global) route
       (λctx' src a. dg_spec_edge_program S a src global_of)
       (routed_call_program S global_of seed (static_resolve g) (λd. d = bot))
       (routed_entry_seed_programs seed)
       g bot initial initial_global"

subsection ‹Per-node edge indexes›

text ‹
  ‹group_by_key key_of f xs› files each element ‹f› accepts under its key,
  keeping list order within a key. A lookup is therefore the order-preserving
  filter of ‹xs› at that key, which is what lets it replace an enumeration
  inside a fold that observes order.
›

definition group_lookup :: "('k::linorder, 'y list) rbt ⇒ 'k ⇒ 'y list" where
  "group_lookup m k = (case RBT.lookup m k of None ⇒ [] | Some ys ⇒ ys)"

definition group_by_key ::
    "('x ⇒ 'k::linorder) ⇒ ('x ⇒ 'y option) ⇒ 'x list ⇒ ('k, 'y list) rbt" where
  "group_by_key key_of f xs =
     foldr (λx m. case f x of
                None ⇒ m
              | Some y ⇒ RBT.insert (key_of x) (y # group_lookup m (key_of x)) m)
       xs RBT.empty"

lemma group_lookup_group_by_key:
  "group_lookup (group_by_key key_of f xs) k
     = List.map_filter (λx. if key_of x = k then f x else None) xs"
  by (induction xs) (auto simp: group_by_key_def group_lookup_def split: option.splits)

definition intra_predecessor_index ::
    "cfg ⇒ (cfg_node, (cfg_node × edge_action) list) rbt" where
  "intra_predecessor_index g =
     group_by_key (λ(u, a, w). w) (λ(u, a, w). Some (u, a)) (cfg_intra_list g)"

lemma group_lookup_intra_predecessor_index:
  "group_lookup (intra_predecessor_index g) v = intra_predecessor_list g v"
proof -
  have "List.map_filter
          (λx. if (λ(u, a, w). w) x = v then (λ(u, a, w). Some (u, a)) x else None) es
          = map (λ(u, a, w). (u, a)) (filter (λ(u, a, w). w = v) es)"
    for es :: "(cfg_node × edge_action × cfg_node) list"
    by (induction es) auto
  then show ?thesis
    unfolding intra_predecessor_index_def intra_predecessor_list_def group_lookup_group_by_key
    by simp
qed

lemma map_group_lookup_intra_predecessor_index:
  "map (λ(u, a). (Inl (u, ctx), a)) (group_lookup (intra_predecessor_index g) v)
     = intra_predecessor_addr_list g v ctx"
  by (simp add: intra_predecessor_addr_list_def group_lookup_intra_predecessor_index)

definition call_target_index ::
    "cfg ⇒ (cfg_node, (cfg_node × call_action × pname) list) rbt" where
  "call_target_index g =
     group_by_key (λ(c, ca, ce, k). k) (λ(c, ca, ce, k). call_target_at k (c, ca, ce, k))
       (cfg_calls_list g)"

lemma group_lookup_call_target_index:
  "group_lookup (call_target_index g) v = call_target_list g v"
proof -
  have "(if (λ(c, ca, ce, k). k) e = v
         then (λ(c, ca, ce, k). call_target_at k (c, ca, ce, k)) e else None)
          = call_target_at v e" for e :: "cfg_node × call_action × cfg_node × cfg_node"
  proof -
    obtain c ca ce k where e: "e = (c, ca, ce, k)" by (cases e) auto
    show ?thesis by (cases ce) (auto simp: e)
  qed
  then show ?thesis
    unfolding call_target_index_def call_target_list_def group_lookup_group_by_key
    by simp
qed

text ‹
  The indexes are let-bound outside the equation system, so a solver holding
  the system evaluates them once. The three selectors restate
  \<^const>‹intra_predecessor_addr_list›, \<^const>‹call_site_list› and
  \<^const>‹static_resolve› over a lookup in place of the enumeration. They
  ignore their graph argument, which is sound only because the generator
  applies every selector at the one graph it is given.
›

lemma compiled_routed_eqs_for_code [code]:
  "compiled_routed_eqs_for global global_of seed route S g initial initial_global =
     (let preds = intra_predecessor_index g; targets = call_target_index g
      in routed_node_rhs_buffered
           (λ_ v ctx. map (λ(u, a). (Inl (u, ctx), a)) (group_lookup preds v))
           (λ_ v. remdups (map (λ(c, ca, p). (c, ca)) (group_lookup targets v)))
           (λ_. global) route
           (λctx' src a. dg_spec_edge_program S a src global_of)
           (routed_call_program S global_of seed
              (λv cc ca d. map (λ(c, a, p). p)
                 (filter (λ(c, a, p). c = cc ∧ a = ca) (group_lookup targets v)))
              (λd. d = bot))
           (routed_entry_seed_programs seed)
           g bot initial initial_global)"
proof -
  note preds = map_group_lookup_intra_predecessor_index
  have sites: "remdups (map (λ(c, ca, p). (c, ca)) (group_lookup (call_target_index g) v))
      = call_site_list g v" for v
    by (simp add: call_site_list_def group_lookup_call_target_index)
  have resolve: "(λv cc ca d. map (λ(c, a, p). p)
                   (filter (λ(c, a, p). c = cc ∧ a = ca) (group_lookup (call_target_index g) v)))
      = static_resolve g"
    by (intro ext) (simp add: static_resolve_def static_targets_def group_lookup_call_target_index)
  show ?thesis
    unfolding compiled_routed_eqs_for_def routed_node_rhs_buffered_def
      routed_contribution_programs_def Let_def
    by (simp only: preds sites resolve)
qed

end