A graph numerical certificate #
This example certifies a four-node scalar graph:
x in [1, 2] c in [0.5, 1]
\ /
y = x + c
|
z = y * c
The source intervals are executable binary32 endpoints. The checker propagates them with directed
rounding, rejects non-finite intermediate intervals, and records the backend capsules selected when
the portable CPU profile replans the graph. The resulting range trace is an executable check; a
CheckedRealExecution supplies the separate proof that an exact-real execution is enclosed. This
file demonstrates the artifact-generation and replay path that a larger graph uses.
The example uses scalar nodes so the interval endpoints remain easy to inspect. The certificate machinery itself stores only one scalar hull per tensor and is independent of tensor rank.
Instances For
Input and constant assumptions. Hexadecimal endpoints preserve the exact binary32 artifact.
Instances For
Generate and replay the range trace and the selected backend plan.
Instances For
Concrete payload used for bit-level replay. The constant is 0.75, which lies in the declared
constant range $[0.5,1]$.
Instances For
A concrete input (1.25) inside the declared input interval.
Instances For
Replay the same graph using the bit-level IEEE32 interpreter and check every intermediate.
Instances For
Deliberately replace the addition range with $[0,0]$. This models a corrupted or optimistic external artifact; replay must not accept it merely because $[0,0]$ is itself a valid interval.
Instances For
Check the deliberately corrupted artifact against the canonical graph transfers.
Instances For
A finite interval attached to an arithmetic node is still an invalid source assumption.
Instances For
Registries are deterministic maps: registering a second source contract is rejected.
Instances For
A certificate is bound to the named operation registry used to derive its transfer rows.
Instances For
Coverage before propagation #
Coverage is checked after any architecture has lowered to the common IR. An architecture using only registered primitives needs no architecture-specific checker. A new primitive is rejected with its node id and operation name until a local range contract is registered.
The base graph is completely covered by the built-in range registry.
Instances For
Exponential is executable in the graph IR, but it intentionally has no built-in interval transfer yet. This graph demonstrates that unsupported numerical semantics fail explicitly.
Instances For
Coverage failure occurs before certificate propagation begins.
Instances For
A fixed-order reduction #
Reduction order is part of the backend audit because floating-point addition is not associative.
The portable profile advertises the same left fold used by Tensor.sumSpec, so the checker can
propagate this reduction directly. Native CUDA's implementation-dependent reduction policy is not
silently treated as the same computation.
Matrix accumulation #
The same reduction policy governs matrix multiplication. Each output entry is a fixed-left sum of products in the portable profile, so the checker combines outward-rounded multiplication with the existing sum transfer. CUDA profiles advertise an implementation-dependent accumulation and are not accepted by this particular transfer.
Attempt to use the fixed-left matrix transfer with a CUDA reduction policy.
Instances For
Domain-sensitive square root #
The checker propagates absolute value before checking the square-root domain. Thus an input range
that crosses zero is valid for abs → sqrt, while the same range passed directly to sqrt is
rejected. The square-root endpoints use TorchLean's proved directed binary32 rounders rather than a
host libm call.
A source interval containing negative values does not satisfy the real square-root domain.
Instances For
Layer normalization #
LayerNorm combines several domain-sensitive steps. The certificate follows the implementation: mean, centering, squaring, variance, epsilon stabilization, directed square root, and division. The portable profile fixes the reduction order used by both means.
The same fixed-left LayerNorm transfer is not attributed to an unspecified CUDA reduction.
Instances For
Domain-sensitive activations #
Absolute value converts the signed source range to a nonnegative interval. That discharged domain condition allows the checker to apply the proved directed square-root endpoints. ReLU then preserves the resulting range.
Stable axis softmax #
The real softmax theorem proves that a nonempty row lies in $[0,1]$; the bit-level replay then checks that the executable implementation stayed finite and respected that range for the concrete input.
A complete model pass #
The preceding examples isolate individual numerical rules. This final graph runs the same machinery over a two-layer MLP with matrix weights and explicit bias tensors:
input [1,2]
-> matmul [2,3]
-> add bias [1,3]
-> ReLU
-> matmul [3,1]
-> add bias [1,1]
Nothing in certificate generation is told that this is an MLP. The checker sees ten ordinary IR
nodes and obtains each transfer from GraphRangeRegistry. The backend planner independently chooses
a capsule for every operation. The final replay executes the stored graph with bit-level binary32
semantics and checks all ten intermediate tensors against the regenerated ranges.
A two-layer matrix MLP expressed only in the canonical operation IR.
Instances For
Source ranges cover inputs, both weight matrices, and both bias tensors. A single enclosure per tensor is sufficient for this certificate format; the graph walk remains independent of rank.
Instances For
Constant payloads use the IR's canonical flat storage ABI; node shapes recover the typed matrix view during evaluation. The explicit order below is row-major.
Concrete parameters are payloads of the constant nodes, not special fields in the checker.
Instances For
Generate the operation-local range trace and bind it to the checked CPU capsule plan.
Instances For
Execute the stored graph in the bit-level binary32 interpreter and check every node.
Instances For
Executable acceptance report. Positive cases should be true; deliberately corrupted,
invalid-domain, or wrong-reduction-policy cases should be false. This list exercises range
reconstruction and IEEE replay; it does not construct the separate exact-real enclosure proof.