Module equiv 

equiv — the differential that decides whether two spatial programs MEAN the same thing.

A pass, a legalization, an imported placement, a hand-written lowering: each hands us a second SpatialProgram together with a claim that it computes what the first one computes. equivalent_under is how that claim is discharged — evaluate both under the executable token semantics of super::eval, on the SAME inputs, over a corpus of them, and name the first place the two part company.

★ WHY THIS EXISTS WHEN certify_external_spatial ALREADY HAS THE SHAPE. That function (spatial/certificate.rs:759) looks like the same idea — same tensors, evaluate both, compare — and it cannot validate a rewrite, for two independent reasons, either of which alone is fatal:

1. It is a ONE-POINT differential. It builds dry_inputs(source): the recorded fills, and zeros wherever the data is external. One evaluation, at one point, and that point is the origin. A rewrite that is wrong everywhere except there passes it, and zero is exactly the argument at which dropped terms, swapped operands and lost scale factors are all invisible.
2. It gates on STRUCTURAL stage-kind equality. Before evaluating anything it compares the two programs’ sorted, deduplicated multisets of discriminant(StageKind) — and, for compute stages, discriminant(ComputeOp) — returning None when they differ. Every legalization worth the name violates that BY CONSTRUCTION: expanding one fused ComputeOp::RowReduce into the Elementwise → ReduceRows → RowXform → RowRescale chain changes those discriminants, and changing them IS the rewrite. A validator that refuses precisely the programs it exists to validate can never be called on one. (It has, today, no callers at all.)

This module is the generalization: a CORPUS rather than a point, and no structural precondition whatsoever — only the tensors that come out the other end. The two programs need not share a stage, a buffer, a placement or a schedule. They need only agree on what they compute.

Equality here is Outputs’s own equality, applied element by element so the answer can say WHERE: Value::Int compares exactly, Value::Float compares with == (so a rewrite that turns a number into NaN on both sides is reported as a divergence rather than waved through — fail-closed). steps is deliberately NOT compared: how many rounds a schedule takes is an artifact of the arrangement, not of the meaning, and a rewrite that changes it has changed nothing this module is asked about.

Enums

Divergence

Why two programs are not the same program.

Elem

One element, in whichever numeric tower its tensor lives in — enough to read a divergence without carrying two whole tensors through a panic message.

Side

Which of the two programs a divergence is being reported against.

Constants

APPROX_REL_TOL

The relative tolerance a NumericsClaim::Approx program’s rewrite is discharged against.

CORPUS_MAGNITUDE_CAP

The magnitude a corpus element is capped at.

DEFAULT_ABS_BOUND

The window used for a tensor that declares neither a range nor a bounded fill.

Functions

corpus_prng

The repo’s deterministic hash PRNG — the same mixing crates/logicaffeine_tests/tests/common/spatial.rs uses, restated here because a corpus builder that lives in the compiler cannot reach into the test tree. Same seed, same index, same window ⇒ same value, on every machine and every run.

equivalent_under

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

equivalent_within

equivalent_under, but comparing floats within rel RELATIVE tolerance (falling back to rel as an absolute bound near zero, so a divergence cannot pass merely because both sides are small). Integers are still compared exactly — an approximate claim is about a float datapath, never about an integer one.

seeded_corpus

A corpus: one seeded_inputs per seed, in the order given.

seeded_inputs

One corpus point for p: every tensor the evaluator needs, keyed by TensorId.