Module scc 

Multi-predicate SCC fixpoint evaluator.

Extends the single-target super::evaluate_fixpoint to a mutually-recursive SCC: rules grouped by their target predicate, evaluated jointly so each predicate’s body can reference any other predicate in the SCC. Naive evaluation: one iteration runs every rule for every predicate; convergence is the global “no relation grew this iteration” check.

Pure-Rust, deterministic, set-semantics. Built to be the recursive-multi-predicate WCOJ correctness oracle for PR 5+ mixed-execution kernels. Not optimized — semi-naive delta-driven SCC fixpoint is a separate concern.

Determinism

• Rules grouped under each predicate are evaluated in input order (slice order). Rule order does NOT affect the result (locked by test) — it’s an efficiency knob, not a semantic one.
• Predicates are iterated in BTreeMap’s sorted-by-key order. Predicate order does NOT affect the result (locked by test).
• Output rows for each predicate are sorted lexicographically and deduplicated.

Schema management

Per-predicate schemas are frozen from the first iteration that produces non-empty rows for that predicate. Subsequent iterations validate every newly-produced row’s variants against the frozen schema; mismatches surface as SccFixpointError::InconsistentHeadValueTypes before the row is unioned. Row arity drift surfaces as SccFixpointError::HeadArityMismatch at function entry — checked once per predicate group across its rules.

Enums

SccFixpointError

Errors surfaced by evaluate_scc_fixpoint.

Functions

evaluate_scc_fixpoint

Evaluate a mutually-recursive SCC of predicates to a fixpoint.