Part of #27. Extractor grows loan/borrow facts; ownership+MIR-loans alias oracle (weak updates); synthetic formal/actual vertices; param_in/param_out at application scope; summary fixpoint with external pass-through self-edges; semantic DDG (prov points-to). Gate: no dangling SDG endpoints; PARAM arity match; known transitive flow has its summary edge; L3 subset-of L4.
Part of #27. Extractor grows loan/borrow facts; ownership+MIR-loans alias oracle (weak updates); synthetic formal/actual vertices; param_in/param_out at application scope; summary fixpoint with external pass-through self-edges; semantic DDG (prov points-to). Gate: no dangling SDG endpoints; PARAM arity match; known transitive flow has its summary edge; L3 subset-of L4.