15 — Level 3, stages 5–7: summaries, SCC fixpoints & SDG assembly

[rahlk]

Part of #9. Phase 3 — native dataflow. The whole-program summit — the hardest issue on the
ladder. Take it in three PRs if needed (oracle+SCC / summaries / SDG).

Learning goals

Tarjan's SCC in Rust (iterative, not recursive — stack discipline), monotone fixpoints and WHY
k-limiting guarantees termination, the Horwitz–Reps–Binkley SDG construction, and large-scale
data design: summaries that are cheap to clone/compose (Arc sharing where it counts).

Task

• Stage 5 — oracles (both FROZEN: read answers, never fork internals): (a) the call graph
  you built in issue 06, condensed into SCCs (Tarjan) — the condensation DAG is the bottom-up
  order; (b) the may-alias oracle: type-based MVP (two paths may alias iff types are
  compatible), explicitly strengthened by ownership: &mut paths alias nothing else live, moves
  end liveness. Document the oracle's API surface: may_alias(p1, p2), targets(callsite).
• Stage 6 — summaries: hammock-region decomposition of each CFG (loop bodies, arms);
  summarize innermost-first as entry-facts → exit-facts edges (one exit set per exit kind:
  normal / panic / return) + a statics read/write footprint; compose function summaries
  bottom-up over the condensation DAG; within an SCC (mutual recursion) iterate members to a
  monotone fixpoint — k-limiting + bounded label sets = termination. Statics/module state ride
  as extra summary inputs/outputs. Unmodeled externals: conservative pass-through (every arg
  and reachable heap flows to the return and to external state).
• Stage 7 — SDG: per call site actual-in/actual-out nodes; per callable formal-in/formal-out;
  edges CALL (callsite → callee ENTRY), PARAM_IN, PARAM_OUT, and SUMMARY edges
  (actual-in → actual-out, encoding the callee's transitive flow — what makes later slicing
  context-sensitive without re-descending).

Gate (summary + SDG gates)

• Composed summary routes a parameter to the return across a fixture call chain a → b → c.
• Two mutually recursive fixture functions reach fixpoint (terminate!) with identical summaries
  across two runs.
• SDG: no dangling (signature, node_id) endpoints; actual/formal arity matches; at least one
  SUMMARY edge for a known transitive flow, asserted by name.