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 ProvedRealEnclosure supplies the separate proof that an exact-real execution is enclosed. Larger graphs use the same artifact-generation and replay path.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.graph : IR.Graph

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.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.interval (lo hi : UInt32) : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32

Build a binary32 interval from two bit patterns.

Every source range in this file is written in hexadecimal rather than as a decimal literal. That keeps the certificate an exact artifact: no decimal-to-binary conversion sits between what is written here and what the checker sees.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.accepted {α : Type} : Except String α → Bool

Did an executable certificate operation return a checked value?

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.sources : Array Proofs.RuntimeApprox.NumericalCertificate.SourceRange

Input and constant assumptions. Hexadecimal endpoints preserve the exact binary32 artifact.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.checked : Except String Proofs.RuntimeApprox.NumericalCertificate.RegistryCheckedCertificate

Generate and replay the range trace and the selected kernel plan.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.payload : IR.Payload (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) payload._proof_1 payload._proof_2 payload._proof_3 payload._proof_4)

Concrete payload used for bit-level replay. The constant is 0.75, which lies in the declared constant range $[0.5,1]$.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.input : Spec.SomeTensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) payload._proof_1 payload._proof_2 payload._proof_3 payload._proof_4)

A concrete input (1.25) inside the declared input interval.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.replay : Except String Proofs.RuntimeApprox.NumericalCertificate.RangeCheckedExecution

Replay the same graph using the bit-level IEEE32 interpreter and check every intermediate.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.tampered : Except String Proofs.RuntimeApprox.NumericalCertificate.GraphNumericalCertificate

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.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.tamperedCheck : Except String Proofs.RuntimeApprox.NumericalCertificate.RegistryCheckedCertificate

Check the deliberately corrupted artifact against the canonical graph transfers.

A complete model pass

The small graph above makes each range easy to inspect. This 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. Kernel selection 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.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpInputShape : Spec.Shape

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpHiddenShape : Spec.Shape

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpFirstWeightShape : Spec.Shape

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpSecondWeightShape : Spec.Shape

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpOutputShape : Spec.Shape

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpGraph : IR.Graph

A two-layer matrix MLP expressed only in the canonical operation IR.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpSources : Array Proofs.RuntimeApprox.NumericalCertificate.SourceRange

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.

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.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpFirstWeightFlat : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) payload._proof_1 payload._proof_2 payload._proof_3 payload._proof_4) [6]

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpHiddenBiasFlat : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) payload._proof_1 payload._proof_2 payload._proof_3 payload._proof_4) [3]

First bias, flat.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpSecondWeightFlat : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) payload._proof_1 payload._proof_2 payload._proof_3 payload._proof_4) [3]

Second weight matrix [3, 1], flat.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpOutputBiasFlat : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) payload._proof_1 payload._proof_2 payload._proof_3 payload._proof_4) [1]

Output bias, a single value.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpPayload : IR.Payload (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) payload._proof_1 payload._proof_2 payload._proof_3 payload._proof_4)

Concrete parameters are payloads of the constant nodes, not special fields in the checker.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpInput : Spec.SomeTensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) payload._proof_1 payload._proof_2 payload._proof_3 payload._proof_4)

The concrete [1, 2] input the full-model replay runs on.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpCertificate : Except String Proofs.RuntimeApprox.NumericalCertificate.RegistryCheckedCertificate

Generate the operation-local range trace and bind it to the checked CPU capsule plan.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.mlpReplay : Except String Proofs.RuntimeApprox.NumericalCertificate.RangeCheckedExecution

Execute the stored graph in the bit-level binary32 interpreter and check every node.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.exampleChecks : Array (String × Bool)

Generate and replay both graphs, and reject the deliberately tampered base artifact.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.usage : String

Help text for the certificate example.

def NN.Examples.DeepDives.Floats.GraphNumericalCertificate.main (args : List String) : IO UInt32

Public runner for the certificate examples. A failed positive check or an accepted negative check produces a nonzero exit code, so this command is also suitable for regression testing.