Subprocess Output Validation🔗

The common process helper is small:

-- Require a successful process and one complete JSON
-- document on stdout.
def runJsonStdoutChecked
    (ctx : String)
    (cmd : String)
    (args : Array String)
    (cwd : Option String := some ".") :
    IO Json := do
  let stdout ← runStdoutChecked ctx cmd args cwd
  match Json.parse stdout with
  | .ok value => pure value
  | .error message =>
      throw <| IO.userError
        s!"{ctx}: JSON parse error: {message}\nstdout:\n{stdout}"

runStdoutChecked starts the process, captures its streams, and rejects a nonzero exit code with the command, arguments, status, and standard error in the diagnostic. runJsonStdoutChecked then requires all of standard output to be one JSON document.

Suppose Python prints:

{"format":"torchlean.bound.v1","lower":0.12,"upper":0.31}

Successful parsing establishes only that this text is valid JSON. A useful checker must still:

1. require the exact format string;

2. require finite numeric fields;

3. establish \mathrm{lower}\leq\mathrm{upper};

4. connect the interval to a particular graph, payload, input set, and output;

5. invoke a sound acceptance theorem.

The helper gives process failures and data failures separate locations. If Python exits with an error, the caller sees that exit status and its standard error rather than attempting to interpret a partial result as a certificate. If Python exits successfully but prints a progress banner before the JSON, the single-document parse fails. A producer using this interface should put diagnostic text on standard error and reserve standard output for the artifact.

The small bound document has no graph identifier, input coordinates, or output index. Even if 0.12 ≤ 0.31 is checked, it remains an interval with no established connection to the requested computation. Binding those fields to a particular query is part of acceptance, not an optional annotation to add after a numerical inequality succeeds.

upper = inf, finite = false

parsed  = {"upper":9.9}
checker read upper = 9.900000

accepted: lo=#[0.100000, 0.200000], hi=#[0.300000, 0.400000]
accepted: lo=#[0.400000, 0.700000], hi=#[0.600000, 0.900000]

rejected: region.hi[0]: expected finite float
rejected: region: invalid interval at coordinate 0: [0.500000, 0.200000]
rejected: region: field `lo` requires a matching `hi` field
rejected: region: endpoint fields (`lo`, `hi`) cannot be combined with `center` or `eps`

PyTorch Graph Capture🔗

Run:

# Capture the maintained Python probes and validate their
# exported IR documents.
lake exe pytorch_export_check

The command asks Python and torch.export to capture several small nn.Modules (Paszke et al., 2019), emits torchlean.ir.v1 JSON, parses each document in Lean, lowers supported values to NN.IR.Graph, and runs the graph validators.

The maintained numerical probes cover TinyMLP, TinyAffineLayerNorm, TinyLayerNormEpsilon, and TinyBatchNormEpsilon. Each captured graph is executed on a deterministic input and compared with PyTorch. Generated-reference and state-dict checks run in the same command:

== PyTorch nn.Module → TorchLean IR runtime check ==
generated Python float bit patterns and tiny epsilon: ok
generated reference code and state-dict round trip: ok
  numerical parity: ok (TinyMLP)
  numerical parity: ok (TinyAffineLayerNorm)
  numerical parity: ok (TinyLayerNormEpsilon)
  numerical parity: ok (TinyBatchNormEpsilon)
pytorch_export_check: ok

The parser's structural theorem is parseGraph_wellShaped. The examples below inspect that statement and exercise malformed documents directly, independently of these numerical probes.

The two epsilon models make small normalization constants observable: a formatter that rounded them to zero could change the computation without changing any shape. Generated-source and state-dictionary checks exercise separate import paths. Each ok records the outcome of its named probe, with the supplied parameters and deterministic input.

Graph Exchange Format🔗

I'll use a three-node graph with one input of shape [1,4]. The second node applies ReLU elementwise, preserving that shape. The third sums all four entries to a scalar, whose shape is []. Parent IDs record that sequence:

That string is a Lean value, so the importer can be run on it directly. One helper reports the verdict:

accepted: nodes=3, input=0, outputs=#[2]

The report identifies the three accepted nodes, node 0 as the input, and node 2 as the output. This fixture exercises the parser directly from a Lean string without starting Python. In a full capture, the Python producer translates raw FX or ATen names into stable TorchLean tags. The Lean parser recognizes a conservative list, parses operation-specific fields, constructs candidate nodes, and validates the result. The op kind strings come from the fixed v1 table in NN.Runtime.PyTorch.Wire. Its round-trip theorem says that reading the spelling of an operator recovers its NN.IR.OpTag identity.

The complete path separates external capture from the checks Lean performs on its result:

PyTorch module
   ↓ external capture, treated as an untrusted producer
FX/value graph
   ↓ explicit JSON schema
Lean parser
   ↓ checked structural lowering
NN.IR.Graph
   ↓ denotation / verifier / exporter
TorchLean analysis

The first lowering step must preserve more than tensor shapes. For example, nn.MultiheadAttention returns a tuple of attention output and attention weights. Treating that FX node as a single tensor loses the distinction between its components. TorchLean first retains tuple shape metadata, then lowers only supported tensor projections. The later Lean checks apply to the resulting document, so their scope depends on exactly what the parser and graph validators recognize.

Parent identifiers and output identifiers serve different purposes. Parent edges establish the dependencies needed to evaluate a node. The output list chooses which already-recorded values form the external result, in return order. Both need validation because a well-shaped internal node list alone would not make an out-of-range output identifier usable.

The Parser's Structural Guarantee🔗

parseGraph_wellShaped states the structural property of a successful parse:

@parseGraph_wellShaped : ∀ {j : Json} {cg : CapturedGraph}, parseGraph j = Except.ok cg → cg.graph.WellShaped

The conclusion is the property WellShaped, defined by the executable checker's success:

def NN.IR.Graph.WellShaped : NN.IR.Graph → Prop :=
fun g => g.checkShapes = Except.ok ()

If the importer returns a graph, the theorem establishes that the shared shape checker accepts it. Downstream proofs can use this result without re-deriving well-shapedness or assuming that the importer remembered to call the checker. Its premise mentions only the JSON value and successful parsing, so its conclusion concerns that graph's structure. It makes no claim that Python captured the intended module or translated every operator correctly (Necula, 1997).

accepted, output = 4.000000
accepted, output = 1.820822

Import Rejection🔗

Each of the following changes one field in ffiGood, letting us trace the resulting rejection to the check responsible for it:

rejected: PyTorch graph import: unsupported format `torchlean.ir.v2` (expected `torchlean.ir.v1`)
rejected: PyTorch graph import: node[1]: unsupported TorchLean IR op kind `sort`
rejected: IR graph: node 1: outShape mismatch: inferred=[1, 4], declared=[1, 5] (Node(id=1, kind=relu, parents=#[0], outShape=[1, 5]))
rejected: PyTorch graph import: node[1]: parent id 2 is not < 1

The errors identify four stages of validation:

• the format rejection comes from the schema check, before any node is looked at;

• the op kind rejection comes from the conservative operator table, which is why adding torch.sort to the Python side without touching the Lean parser produces an explicit unsupported-operation failure rather than a partial import;

• the shape mismatch comes from checkShapes, which reports both the inferred and the declared shape, helping locate a mismatch without proving which side introduced it;

• the parent id rejection comes from the id discipline, and it is the one that keeps cycles out: a node may only refer to strictly earlier nodes, so a candidate containing a forward reference is rejected.

The four messages above were rewrapped to fit the page; the runtime prints each on one line.

The command's successful captures do not test every unsupported translation. Reflect padding could become zero padding, scaled addition could lose its scale, a dtype cast could disappear, or training-mode BatchNorm could be read as eval-mode BatchNorm. Each substitution can yield a graph with correct shapes and different values. A producer must either implement the intended semantics or reject the case, and that behavior needs tests in addition to the Lean shape check. Replacing an unsupported node with an identity or silently dropping attention weights would have the same problem.

State Dictionaries And Graphs🔗

A state_dict supplies named tensors. It does not describe data flow. A graph capture supplies operations and edges. It may refer to parameters without carrying the full checkpoint provenance.

Round-trip import therefore has two obligations:

Run:

# Generate the default family artifacts for joint inspection
# of model and payload.
lake exe torchlean pytorch_roundtrip

This writes the generated MLP PyTorch artifacts under NN/Examples/Interop/PyTorch/MLP/. Open the generated model and parameter files together: neither one is a complete description of the executable network by itself. A graph with a well-shaped convolution node contains no weights, and a checkpoint full of correctly shaped weights says nothing about the order the operations run in. Reconstructing the network requires matching the graph's parameter references to the tensors in the state dictionary.

Semantic Guarantees For Imported Graphs🔗

For an imported model, distinguish these three claims:

1. Python produced a document and exited successfully.

2. Lean parsed the document into a well-shaped supported graph.

3. The graph's denotation equals the original PyTorch module on all admissible inputs.

The capture experiment and parseGraph_wellShaped establish the second proposition, conditional on the bytes received. The third needs a translation theorem for the supported producer or an explicit trust assumption about capture and lowering.

Numerical parity tests provide execution evidence for that assumption. The deterministic linear and normalization probes above can expose transposes, axis errors, and missing biases. Checking mask translation would require an attention probe. Their conclusions concern the tested cases, with no universal quantification over parameters and inputs. Coverage-guided fuzzing (Odena et al., 2019) and generated well-typed graphs (Liu et al., 2023) extend this approach by exploring cases beyond a fixed collection of hand-written examples; both have found defects in production frameworks.

A graph/payload mismatch can survive both kinds of structural checks. Two checkpoints may supply all the same names and dimensions but contain different learned values. Pairing the captured graph with the wrong one then runs a well-shaped network whose prediction is unrelated to the intended training artifact. Numerical probes can expose that mismatch, while a semantic claim must specify which payload its graph denotation uses. The empty payload in ffiDenote is sufficient only because its input, activation, and sum require no stored parameters.

ONNX Import🔗

NN.Runtime.PyTorch.Export.ONNX emits a Python adapter for a conservative static-shape ONNX fragment. The producer handles elementwise operations, rank-two and limited batched matmul, reductions, softmax, reshape and flatten, concat, selected transposes, Gemm, inference BatchNorm, and ungrouped, undilated convolution with the layouts represented by the current IR. It writes the same torchlean.ir.v1 document consumed by parseGraph, so both producers use the same Lean parser and structural checks.

ONNX protobuf parsing and shape inference therefore remain outside Lean. Lean checks the smaller IR artifact it receives. Graph initializers and payload-backed nodes still need a matching payload import; a well-shaped convolution node by itself does not contain authenticated weights.

Native FFI And Memory Ownership🔗

The parsed graph is ordinary Lean data. A CUDA buffer instead holds an opaque reference to memory that native code can allocate, mutate, alias, or free. Parsing cannot establish that such an allocation remains live.

The CUDA buffer boundary in Buffer.lean contains declarations such as:

-- These declarations expose native ownership operations
-- without exposing pointer storage.
@[never_extract, extern "torchlean_cuda_buffer_of_float_array_io"]
opaque ofFloatArrayIO (a : @& FloatArray) : IO Buffer

@[never_extract, extern "torchlean_cuda_buffer_to_float_array_io"]
opaque toFloatArrayIO (b : @& Buffer) : IO FloatArray

@[never_extract, extern "torchlean_cuda_buffer_release_with_token"]
private opaque releaseWithToken (b : @& Buffer) (token : UInt32) : UInt32

The annotations control three aspects of the boundary: access to the representation, reference ownership, and compiler treatment of calls.

Returning an opaque Buffer, including through IO Buffer, keeps the native pointer representation hidden from Lean callers. The C implementation still determines whether allocation, copying, finalization, and release are correct. Hiding the representation prevents Lean callers from manipulating the pointer directly; it does not verify the native implementation.

@& marks a borrowed argument (Ullrich and de Moura, 2019). Lean's compiler uses reference counting, and a borrowed parameter is one the callee may inspect during the call without owning: native code must not consume the borrowed reference. Retaining it beyond the call requires taking its own reference, with the matching release later. Getting this wrong produces a use-after-free or a leak that no type in the Lean source mentions. Native translation units also repeat critical length and geometry checks. The file-to-symbol map in NN.Runtime.Autograd.Engine.Cuda.Trusted identifies the native implementations behind these declarations.

never_extract prevents closed-term extraction and common-subexpression elimination for calls to the marked declaration. It does not turn a pure signature into an effect type or establish unique ownership. Cleanup also needs a live result dependency or an explicit effectful boundary.

AnyBuffer.validate : AnyBuffer → Result AnyBuffer

Allocation Effects In IO🔗

Native allocation also raises a question about how the compiler may reuse a result. Compare the pure primitive with the checked IO entry point for the same host upload:

Buffer.ofFloatArray : FloatArray → Buffer

Buffer.ofFloatArrayIO : FloatArray → IO Buffer

The first signature does not express allocation effects or release-sensitive identity. It says the result is a function of the input array, so Lean is entitled to treat two uploads of the same array as one value: common subexpression elimination is sound for pure functions. Allocation combined with explicit release cannot safely be treated that way without ownership rules. Two uploads of the same host array must produce independently owned buffers, or releasing one invalidates the other.

The effectful entry point declares the native call itself in IO:

-- Sequence the native upload and its allocation result in IO.
@[never_extract, extern "torchlean_cuda_buffer_of_float_array_io"]
opaque ofFloatArrayIO (a : @& FloatArray) : IO Buffer

ofFloatArrayIO a describes an action. Executing it performs the upload at that point in the surrounding IO sequence. Executing it again with the same host array allocates a separate buffer. The allocation effect belongs to this native call, rather than to a pure upload evaluated inside pure. The borrowed host array remains available to the caller.

Failure is also part of the call's result. When device allocation runs out of memory, the allocator releases unused cached blocks and retries. If that retry also runs out of memory, the action throws IO.Error.resourceExhausted, which the caller can handle through the usual IO exception mechanism. The call has returned no new buffer, and the caller retains its host array and existing device buffers. This is the checked upload contract; the IO type makes sequencing and failure visible, while correct allocation and ownership still depend on the native implementation.

The release wrapper releaseIO still uses a token. It is called only at an ownership boundary where no alias will be used again; session caches atomically remove their published alias before calling it, and the native finalizer stays safe after explicit release because the implementation nulls the pointer.

Both upload entry points copy the same host values, rounding each element to float32. The checked IO entry point additionally exposes when allocation happens and how allocation failure returns to the caller. These effects do not change the tensor's shape or intended contents. They also do not establish unique ownership of the returned handle: Lean references to a Buffer remain copyable.

After explicit release, every alias still refers to the native object whose payload was retired. Copying a Lean reference does not bring the allocation back. The index in Tensor α s constrains rank and dimensions, so it cannot detect use of a stale cached handle. Session code must remove that handle before release, and consumers must respect the same lifetime.

Workspaces And Backward🔗

Some forward kernels produce an output plus intermediates needed by their VJP. TorchLean represents that ownership explicitly:

-- Retain the intermediates needed by backward alongside the
-- forward value.
structure WithWorkspace where
  value : Buffer
  workspace : Array Buffer := #[]

The tape node retains the workspace until backward has consumed it. Afterwards the cleanup is threaded through a value that is still used:

Buffer.WithWorkspace.releaseWorkspaceThen : Buffer.WithWorkspace → Buffer → Buffer

Buffer.WithWorkspace.releaseAllThen : Buffer.WithWorkspace → Buffer → Buffer

Each helper takes a result-with-workspace and a buffer to keep, then returns the kept buffer. Callers thread that return value into their next computation, keeping the release on a path whose result is still needed. The type does not force callers to invoke the helper: they already have the keep buffer and could use it directly. Cleanup therefore remains an ownership protocol that the caller must follow, using a result dependency to retain the release operation.

For long training runs this prevents two forms of growth:

• GPU allocations waiting for Lean external-object finalizers;

• tape closures retaining workspaces after their VJP has run.

Allocator counters report live and peak bytes, allocation and free counts, wrapper counts, and device free memory. These measurements help test the cleanup protocol: for example, live bytes should not grow indefinitely when a fixed workload repeatedly releases its temporaries. The measurements describe that run and do not prove the absence of native leaks.

The two workspace helpers retire different ownership sets. releaseWorkspaceThen keeps the result's own value alive while releasing its auxiliaries. releaseAllThen also retires that value, so the returned keep must belong to storage the caller can still use. Neither type proves that those ownership sets are disjoint; the surrounding operation must establish the protocol.

Allocator telemetry can help distinguish retained payloads from retained Lean wrappers. A wrapper may remain alive after explicit payload release, while a device allocator may retain freed blocks in a cache. Looking only at driver free memory can therefore hide which layer retained memory. Live payload bytes, wrapper counts, and cache behavior need to be interpreted together for the particular repeated workload being inspected.

Host Profiling🔗

LeanProfiler records named IO spans and writes both a Perfetto-compatible trace and a JSON timing summary. It can sit around an existing TorchLean runner after adding the separate LeanProfiler package dependency:

-- Instrument the existing IO runner; device completion
-- needs its own synchronization.
import LeanProfiler
open LeanProfiler

def main : IO Unit :=
  profileFromEnvironment "training" do
    span "model.run" runModel

With LEAN_PROFILE=1, the trace shows nesting and order while the summary groups repeated spans and records process counters. The comparison command checks a new summary against a baseline with explicit absolute and relative tolerances.

A host timer does not automatically measure asynchronous device work. The TorchLean integration can wait for device completion before closing a span; that number is completion latency, not per-kernel CUDA or CUPTI time. A short host call may merely queue a much longer GPU operation, so a short host span can hide device work. It can also mean the relevant host work was not instrumented; measure completion before assigning the cause.

External Oracles And Certificates🔗

TorchLean also calls arbitrary-precision or interval tools to propose bounds. A typical workflow is:

Lean writes an exact query
        ↓
Arb / python-flint computes an enclosure
        ↓
Lean parses rational midpoint-radius data
        ↓
a checker validates the enclosure or treats it as oracle evidence

The rational midpoint and radius preserve the returned numbers without an extra binary64 conversion at ingestion. This avoids the conversion step that overflowed in the 1e999 example. It does not verify the external interval algorithm. That question belongs to the last step in the diagram: if a proved checker replays and accepts the result, its theorem supplies the corresponding proposition. If the result is only compared in a test, it remains oracle evidence.

The same producer and checker distinction applies to α,β-CROWN leaf dumps, PINN residual artifacts, ODE enclosures, and geometry certificates. The external search may use a large implementation, while a checker validates only the returned artifact. The schema determines what information crosses the boundary; the acceptance theorem determines what can be concluded from it.

For each artifact, the report should identify the proposition the checker established and the assumptions connecting its inputs to the requested computation. Exact midpoint-radius data preserves the proposed interval; the acceptance theorem must still justify its enclosure claim.

Evidence For Boundary Contracts🔗

A useful boundary report may say:

• shape: proved by a typed constructor;

• layout: guarded by length and row-major checks;

• value: compared by a regression suite;

• VJP: delegated to a trusted external provider;

• provenance: native symbol torchlean_cuda_buffer_matmul.

A proof of shape safety supplies no arithmetic conclusion, and a source-file link identifies an implementation without validating its behavior. Recording evidence field by field keeps each claim attached to the check, test, or assumption that supports it.

Boundary Failure Tests🔗

The live blocks above exercise numeric parsing, region validation, graph acceptance, and graph rejection during the page build. To exercise the external capture process and a CUDA training call, run:

# Exercise external graph capture and a separately
# configured CUDA runtime call.
lake exe pytorch_export_check
lake -R -K cuda=true exe torchlean quickstart_mlp \
  --device cuda --steps 2 --show-backend

Then deliberately break one condition:

1. add an unsupported PyTorch operation and observe import rejection;

2. change a JSON shape and observe checkShapes reject it;

3. request CUDA from a stub build and observe runtime availability rejection;

4. pass a wrong-size Q buffer to the LibTorch SDPA test and observe the Lean and native guard reject it.

The live blocks illustrate the first two rejection paths using JSON strings. The last two depend on the build configuration and native library: availability is checked when the CUDA session is created, and buffer dimensions are checked at the Lean and native call boundaries. Testing these failures confirms where execution stops when an input violates a boundary condition.