Verified Forward Fragment: Syntax And Evaluation

The first-order forward language used by the TorchLean verifier bridge, together with its direct value evaluator over the scalar semantics selected by the caller.

@[simp]

theorem NN.Verification.Builtin.Proved.dval_tensor_mk {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (t : TorchLean.Tensor α s) : { shape := s, tensor := t }.tensor = t

Projecting the tensor from a freshly constructed dynamic value is definitionally exact.

@[simp]

theorem NN.Verification.Builtin.Proved.graph_expectShape_mk {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (t : TorchLean.Tensor α s) : IR.Graph.expectShape s { shape := s, tensor := t } = Except.ok t

Shape checking succeeds for a dynamic value constructed with the expected shape tag.

Typed indices

structure NN.Verification.Builtin.Proved.Idx (Γ : List Spec.Shape) (s : Spec.Shape) : Type

An index into a shape context Γ, carrying a proof that it has shape s.

• i : Fin Γ.length

  Position in the context.

• h : Γ.get self.i = s

  Proof that the context entry at i has shape s.

@[simp]

theorem NN.Verification.Builtin.Proved.Idx.mk_eta {Γ : List Spec.Shape} {s : Spec.Shape} (x : Idx Γ s) : { i := x.i, h := ⋯ } = x

Eta rule for Idx: rebuilding from projections gives the same index.

def NN.Verification.Builtin.Proved.Idx.id {Γ : List Spec.Shape} {s : Spec.Shape} (x : Idx Γ s) : ℕ

The underlying numeric index of an Idx.

This is convenient when we store context values in arrays (indexed by Nat) rather than in dependent lists.

Parameter access

def NN.Verification.Builtin.Proved.getParam {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {s : Spec.Shape} (params : TorchLean.TensorPack α paramShapes) (idx : Idx paramShapes s) : TorchLean.Tensor α s

Fetch a parameter tensor from a TensorPack, using a typed index Idx.

This is the bridge between the parameter context paramShapes and the strongly-typed tensor value returned at shape s.

First-order SSA nodes

@[reducible, inline]

abbrev NN.Verification.Builtin.Proved.Ctx (inShape : Spec.Shape) (ss : List Spec.Shape) : List Spec.Shape

Evaluation context shape list.

We always treat the distinguished input as index 0, then append the shapes of previously-produced SSA node outputs (ss).

inductive NN.Verification.Builtin.Proved.MatmulOperation : Spec.Shape → Spec.Shape → Spec.Shape → Type

Typed evidence for matrix multiplication over an arbitrary shared leading shape.

• leading (leading : List ℕ) (m n p : ℕ) : MatmulOperation ((Spec.Shape.ofList leading).concat [m, n]) ((Spec.Shape.ofList leading).concat [n, p]) ((Spec.Shape.ofList leading).concat [m, p])

  Multiply the final two axes independently at every index of leading.

def NN.Verification.Builtin.Proved.MatmulOperation.denote {α : Type} [TorchLean.Storage α] [Context α] {leftShape rightShape outShape : Spec.Shape} (op : MatmulOperation leftShape rightShape outShape) (left : TorchLean.Tensor α leftShape) (right : TorchLean.Tensor α rightShape) : TorchLean.Tensor α outShape

Typed denotation of a supported matrix multiplication operation.

structure NN.Verification.Builtin.Proved.LayerNormOperation (s : Spec.Shape) : Type

Typed evidence for LayerNorm over a suffix of an arbitrary tensor shape.

rows × width is an evaluation view obtained by flattening the dimensions before and after axis; it is not a restriction on the rank or layout of the input tensor.

• axis : ℕ

  First axis included in the normalized suffix.

• rows : ℕ

  Number of independent rows in the flattened evaluation view.

• width : ℕ

  Number of entries normalized in each row.

• matrixDims : IR.OpContracts.layerNormMatrixDims self.axis s = Except.ok (self.rows, self.width)

  The generic IR shape contract computes the recorded matrix dimensions.

• size_eq : s.size = (Spec.Shape.dim self.rows (Spec.Shape.dim self.width Spec.Shape.scalar)).size

  Reshaping to the matrix view preserves the number of elements.

• rows_pos : 0 < self.rows

  Every evaluation view has at least one row.

• width_pos : 0 < self.width

  The normalized suffix is nonempty.

inductive NN.Verification.Builtin.Proved.Node (α : Type) [TorchLean.Storage α] (paramShapes : List Spec.Shape) (inShape : Spec.Shape) (ss : List Spec.Shape) : Spec.Shape → Type

A well-typed SSA node in the verified forward fragment.

Each Node can only reference earlier values (via Idx (Ctx inShape ss) _), ensuring the DAG/SSA discipline by construction.

The constructors match the operator subset for which this file proves lowering correctness into the verifier IR (NN.IR.Graph). Adding a new operator means extending both this syntax and the correctness proof, which keeps the trusted fragment explicit.

• const {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (wf : s.WellFormed) (t : TorchLean.Tensor α s) : Node α paramShapes inShape ss s
• paramConst {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (wf : s.WellFormed) (p : Idx paramShapes s) : Node α paramShapes inShape ss s
• add {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (a b : Idx (Ctx inShape ss) s) : Node α paramShapes inShape ss s
• sub {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (a b : Idx (Ctx inShape ss) s) : Node α paramShapes inShape ss s
• mulElem {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (a b : Idx (Ctx inShape ss) s) : Node α paramShapes inShape ss s
• relu {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (x : Idx (Ctx inShape ss) s) : Node α paramShapes inShape ss s
• exp {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (x : Idx (Ctx inShape ss) s) : Node α paramShapes inShape ss s
• log {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (x : Idx (Ctx inShape ss) s) : Node α paramShapes inShape ss s
• inv {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (x : Idx (Ctx inShape ss) s) : Node α paramShapes inShape ss s
• matmul {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {leftShape rightShape outShape : Spec.Shape} (op : MatmulOperation leftShape rightShape outShape) (a : Idx (Ctx inShape ss) leftShape) (b : Idx (Ctx inShape ss) rightShape) : Node α paramShapes inShape ss outShape
• reshape {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} (inS outS : Spec.Shape) (h : inS.size = outS.size) (x : Idx (Ctx inShape ss) inS) : Node α paramShapes inShape ss outS
• transpose {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s out : Spec.Shape} (axis₁ axis₂ : ℕ) (hOut : IR.OpContracts.inferTransposeOutShape axis₁ axis₂ s = Except.ok out) (x : Idx (Ctx inShape ss) s) : Node α paramShapes inShape ss out
• softmax {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (axis : ℕ) (hAxis : Spec.Shape.AxisInBounds axis s) (x : Idx (Ctx inShape ss) s) : Node α paramShapes inShape ss s
• layerNorm {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (op : LayerNormOperation s) (x : Idx (Ctx inShape ss) s) : Node α paramShapes inShape ss s
• linear {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} (inDim outDim : ℕ) (w : Idx paramShapes (Spec.Shape.dim outDim (Spec.Shape.dim inDim Spec.Shape.scalar))) (b : Idx paramShapes (Spec.Shape.dim outDim Spec.Shape.scalar)) (x : Idx (Ctx inShape ss) (Spec.Shape.dim inDim Spec.Shape.scalar)) : Node α paramShapes inShape ss (Spec.Shape.dim outDim Spec.Shape.scalar)
• conv {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {d : ℕ} (inC outC : ℕ) (kernelShape stride padding inSpatial : TorchLean.Tensor ℕ [d]) (hIn : inC ≠ 0) (hKernel : ∀ (i : Fin d), kernelShape.getScalar i ≠ 0) (hStride : ∀ (i : Fin d), stride.getScalar i ≠ 0) (hInfer : IR.OpContracts.inferConvOutShape "conv" 0 inC outC kernelShape stride padding (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ))) = Except.ok (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernelShape stride padding).to (List ℕ)))) (kernel : Idx paramShapes (Spec.Shape.ofList (outC :: inC :: kernelShape.to (List ℕ)))) (bias : Idx paramShapes (Spec.Shape.dim outC Spec.Shape.scalar)) (x : Idx (Ctx inShape ss) (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) : Node α paramShapes inShape ss (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernelShape stride padding).to (List ℕ)))
• mseLoss {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (yhat target : Idx (Ctx inShape ss) s) : Node α paramShapes inShape ss Spec.Shape.scalar

Forward programs (closed let-chains)

inductive NN.Verification.Builtin.Proved.ForwardLetChain (α : Type) [TorchLean.Storage α] (paramShapes : List Spec.Shape) (inShape : Spec.Shape) : List Spec.Shape → Spec.Shape → Type

Well-typed first-order programs, represented as a forward “let chain”.

The type parameter ss tracks the list of already-produced node output shapes, so every node can only reference earlier values (including the distinguished input at index 0).

• ret {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (y : Idx (Ctx inShape ss) out) : ForwardLetChain α paramShapes inShape ss out
• let1 {α : Type} [TorchLean.Storage α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {mid out : Spec.Shape} : Node α paramShapes inShape ss mid → ForwardLetChain α paramShapes inShape (ss ++ [mid]) out → ForwardLetChain α paramShapes inShape ss out

@[reducible, inline]

abbrev NN.Verification.Builtin.Proved.ForwardProgram (α : Type) [TorchLean.Storage α] (paramShapes : List Spec.Shape) (inShape outShape : Spec.Shape) : Type

A closed program in the proved forward fragment, from inShape to outShape.

Evaluation

def NN.Verification.Builtin.Proved.getValue? {α : Type} [TorchLean.Storage α] [Context α] (vals : Array (Spec.SomeTensor α)) (idx : ℕ) : Except String (Spec.SomeTensor α)

Read a dynamic value from the executable context with a user-facing bounds error.

def NN.Verification.Builtin.Proved.getVal {α : Type} [TorchLean.Storage α] [Context α] {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (vals : Array (Spec.SomeTensor α)) (idx : Idx (Ctx inShape ss) s) : Except String (TorchLean.Tensor α s)

Read a previously computed dynamic value and cast it back to the statically expected shape.

The verified fragment constructs only well-scoped indices, but the executable evaluator stores values in an array, so this check gives a clear error if an implementation bug ever violates the shape discipline.

def NN.Verification.Builtin.Proved.evalNode {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (node : Node α paramShapes inShape ss out) (params : TorchLean.TensorPack α paramShapes) (vals : Array (Spec.SomeTensor α)) : Except String (Spec.SomeTensor α)

Evaluate a single SSA node, given the parameter environment and current value context.

This mirrors the IR denotation for the supported operator subset.

def NN.Verification.Builtin.Proved.evalForwardLetChain {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (g : ForwardLetChain α paramShapes inShape ss out) (params : TorchLean.TensorPack α paramShapes) (vals : Array (Spec.SomeTensor α)) : Except String (TorchLean.Tensor α out)

Evaluate a forward let-chain program, threading an array of dynamic values.

The vals array stores the input and all previously-computed node outputs, so that node evaluation can do simple array lookups by Idx.id.

def NN.Verification.Builtin.Proved.evalForward {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape outShape : Spec.Shape} (p : ForwardProgram α paramShapes inShape outShape) (params : TorchLean.TensorPack α paramShapes) (x : TorchLean.Tensor α inShape) : Except String (TorchLean.Tensor α outShape)

Evaluate a verified forward fragment program.

This is the top-level evaluator for ForwardProgram: it initializes the context with the input value and then interprets the SSA let-chain.