Function equivalent_under 

pub fn equivalent_under(
    a: &SpatialProgram,
    b: &SpatialProgram,
    inputs: &[Inputs],
) -> Result<(), Divergence>

Do a and b compute the same outputs on every input of the corpus?

Ok(()) is the equivalence claim discharged over exactly those points — no more, and the corpus is the caller’s argument for “no less”. Err names the first divergence found, scanning inputs in order and tensors in id order, so the report is deterministic and diffable across runs.

Both programs are evaluated under super::eval::Scheduler::RoundRobin; scheduler independence is a separate property with its own oracle (eval_choreography_confluent) and conflating the two would make a nondeterministic program look like an inequivalent one.

★ WHAT THIS IS NOT. Both sides run under the SAME evaluator, so this validates a REWRITE against the IR’s semantics — never the semantics against the mathematics. A pass that preserves an operator the compiler has always computed wrongly passes here and should: that error belongs to spatial_algebra_semantics_lock, which checks eval_choreography against references written out longhand from each operator’s definition. The two oracles are complementary and neither substitutes.