Validate the analyzed domain, not just one compiled answer

An IR verifier can reject mismatched operand types, invalid region structure, or definitions that violate dominance. These checks are valuable because downstream passes rely on well-formed input. A verifier does not generally know whether replacing a multiply with an add preserves the original function, or whether a layout guard omitted a required stride condition. Keep structural tests alongside semantic tests rather than treating either as a complete replacement for the other.

Compatibility is another separate claim. A versioned portable representation can define which producers and consumers accept an artifact, while backend support and numerical behavior require additional checks. StableHLO's compatibility documentation states a versioned portability policy; it is not a promise that all devices execute every program with bit-identical floating-point results. Record producer, IR dialect or artifact version, backend, numerical flags, and relevant device conditions so a regression can be reproduced against the contract actually tested.

A differential fixture compares a reference program with the transformed program under controlled initial state. Use noncontiguous two-dimensional views to test indexing, alias-positive and copy cases to test mutation, changed static values to test specialization, and nonuniform cotangents to test derivative reductions. Include expected rejected or fallback inputs. If an outside-domain call should not reach the specialized kernel, merely checking a numerically lucky result is weaker than verifying the dispatch event.

For supported finite numerical outputs, an absolute-plus-relative tolerance can handle small magnitudes and scale-dependent deviations. Specify which value supplies the scale and evaluate special values separately. NaN equality policy, infinities, signed zero, integer exactness, and state effects are not resolved by a single allclose call. A very large tolerance can conceal a wrong transpose or stale parameter, so derive acceptable error from the application and operations rather than increasing it until every test passes.

One valid counterexample disproves a universal equivalence claim over a domain containing that case. Passing many tests does not prove the universal statement. A bounded formal check can be powerful, but its result applies to the modeled operations, dimensions, value ranges, flags, and memory assumptions. A proof using mathematical integers does not automatically cover overflowing machine arithmetic; a proof excluding aliases does not cover an aliased input. Preserve those restrictions in the validation report instead of turning a bounded result into an unrestricted slogan.

The probability lab quantifies one testing limit under a deliberately hypothetical independent sampling model. Reset, set both defect-trigger probability p=0.1 and trials n=20, predict the no-trigger probability 0.9²⁰≈0.1216, then Play or Step. Reset and set both p=0.1,n=30 for about 0.0424. The displayed binomial bars are exact model probabilities; playback highlights outcomes rather than drawing samples. Real compiler bugs do not come with known independent trigger rates, so deliberate boundary fixtures remain necessary and this lab cannot certify equivalence.