Lowered Forward Evaluation: Shared Invariants

The shape list records the expected type of every value in the dynamic evaluator table. packedAt and tensorAt recover an in-bounds value and its typed tensor from that invariant; the lookup lemmas connect them to the evaluator's failure-aware interface. Small graph constructors are shared by the local, per-operator evaluation theorems.

Local graph constructors for evaluator lemmas

def NN.Verification.Builtin.Proved.Correctness.IRStep.unaryNodeOut (kind : IR.OpKind) (outShape : Spec.Shape) : IR.Node

A unary node with parent 0 and an explicit output shape.

def NN.Verification.Builtin.Proved.Correctness.IRStep.unaryGraphOut (kind : IR.OpKind) (inShape outShape : Spec.Shape) : IR.Graph

A two-node graph for a unary op with explicit input and output shapes.

def NN.Verification.Builtin.Proved.Correctness.IRStep.unaryGraph (kind : IR.OpKind) (s : Spec.Shape) : IR.Graph

A two-node graph for a unary op whose input and output share the same shape.

def NN.Verification.Builtin.Proved.Correctness.IRStep.binaryNodeOut (kind : IR.OpKind) (outShape : Spec.Shape) : IR.Node

A binary node with parents 0 and 1 and an explicit output shape.

def NN.Verification.Builtin.Proved.Correctness.IRStep.binaryGraphOut (kind : IR.OpKind) (leftShape rightShape outShape : Spec.Shape) : IR.Graph

A three-node graph for a binary op with explicit parent and output shapes.

def NN.Verification.Builtin.Proved.Correctness.IRStep.binaryGraph (kind : IR.OpKind) (s : Spec.Shape) : IR.Graph

A three-node graph for a binary op whose inputs and output share the same shape.

def NN.Verification.Builtin.Proved.Correctness.IRStep.variadicNodeOut (kind : IR.OpKind) (parentShapes : Array Spec.Shape) (outShape : Spec.Shape) : IR.Node

A node consuming every preceding entry of a shape array, in order.

def NN.Verification.Builtin.Proved.Correctness.IRStep.variadicGraphOut (kind : IR.OpKind) (parentShapes : Array Spec.Shape) (outShape : Spec.Shape) : IR.Graph

Graph fixture for an arbitrary-arity evaluator theorem: one input node per parent shape followed by a node whose parent ids are the complete preceding range.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.range_mapM_eq_toList_of_getElem_eq {β : Type} (values : Array β) (get : ℕ → Except String β) (hget : ∀ (i : ℕ) (hi : i < values.size), get i = Except.ok values[i]) : List.mapM get (List.range values.size) = Except.ok values.toList

A failure-aware lookup over List.range reconstructs the array's element list when it succeeds at every valid index.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.rangeArray_mapM_eq_of_getElem_eq {β : Type} (values : Array β) (get : ℕ → Except String β) (hget : ∀ (i : ℕ) (hi : i < values.size), get i = Except.ok values[i]) : Array.mapM get (Array.range values.size) = Except.ok values

A failure-aware lookup reconstructs an array when it succeeds at every valid index.

@[simp]

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.variadicGraphOut_getNode (kind : IR.OpKind) (parentShapes : Array Spec.Shape) (outShape : Spec.Shape) : (variadicGraphOut kind parentShapes outShape).getNode parentShapes.size = Except.ok (variadicNodeOut kind parentShapes outShape)

The final node of a variadic evaluator fixture is its variadic operation node.

def NN.Verification.Builtin.Proved.Correctness.evalForwardLetChainVals {α : 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 (Array (Spec.SomeTensor α))

Evaluate a typed forward let-chain while accumulating every intermediate dynamic value.

theorem NN.Verification.Builtin.Proved.Correctness.expectShape_eq_ok {α : Type} [TorchLean.Storage α] [Context α] {expected : Spec.Shape} (v : Spec.SomeTensor α) (h : v.shape = expected) : IR.Graph.expectShape expected v = Except.ok (v.cast h)

Graph.expectShape returns the stored tensor when the dynamic shape tag matches.

theorem NN.Verification.Builtin.Proved.Correctness.shape_eq_of_expectShape_eq_ok {α : Type} [TorchLean.Storage α] [Context α] {expected : Spec.Shape} {v : Spec.SomeTensor α} {t : TorchLean.Tensor α expected} (h : IR.Graph.expectShape expected v = Except.ok t) : v.shape = expected

A successful shape check certifies the shape stored by the packed tensor.

theorem NN.Verification.Builtin.Proved.Correctness.eq_mk_of_expectShape_eq_ok {α : Type} [TorchLean.Storage α] [Context α] {expected : Spec.Shape} {v : Spec.SomeTensor α} {t : TorchLean.Tensor α expected} (h : IR.Graph.expectShape expected v = Except.ok t) : v = { shape := expected, tensor := t }

A successful shape check identifies the packed value with the typed tensor it returned.

theorem NN.Verification.Builtin.Proved.Correctness.getVal_eq_ok {α : Type} [TorchLean.Storage α] [Context α] {inShape : Spec.Shape} {ss : List Spec.Shape} {expected : Spec.Shape} (vals : Array (Spec.SomeTensor α)) (idx : Idx (Ctx inShape ss) expected) (v : Spec.SomeTensor α) (hSome : vals[idx.id]? = some v) (h : v.shape = expected) : getVal vals idx = Except.ok (v.cast h)

getVal returns the indexed tensor when the runtime value carries the expected shape tag.

theorem NN.Verification.Builtin.Proved.Correctness.shapesOfVals_get?_eq {α : Type} [TorchLean.Storage α] [Context α] (vals : Array (Spec.SomeTensor α)) (i : ℕ) : (shapesOfVals vals)[i]? = Option.map (fun (v : Spec.SomeTensor α) => v.shape) vals[i]?

Shape lookup through shapesOfVals agrees with looking up the dynamic value first.

@[simp]

theorem NN.Verification.Builtin.Proved.Correctness.shapesOfVals_length {α : Type} [TorchLean.Storage α] [Context α] (vals : Array (Spec.SomeTensor α)) : (shapesOfVals vals).length = vals.size

shapesOfVals has one entry per runtime value.

theorem NN.Verification.Builtin.Proved.Correctness.index_lt_of_shapesOfVals_eq {α : Type} [TorchLean.Storage α] [Context α] {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (vals : Array (Spec.SomeTensor α)) (idx : Idx (Ctx inShape ss) s) (hShapes : shapesOfVals vals = Ctx inShape ss) : idx.id < vals.size

A shape-context invariant proves that a typed index is in bounds for the value array.

def NN.Verification.Builtin.Proved.Correctness.packedAt {α : Type} [TorchLean.Storage α] [Context α] {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (vals : Array (Spec.SomeTensor α)) (idx : Idx (Ctx inShape ss) s) (hShapes : shapesOfVals vals = Ctx inShape ss) : Spec.SomeTensor α

The packed runtime value selected by a typed index and a matching shape context.

theorem NN.Verification.Builtin.Proved.Correctness.getElem?_eq_some_packedAt {α : Type} [TorchLean.Storage α] [Context α] {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (vals : Array (Spec.SomeTensor α)) (idx : Idx (Ctx inShape ss) s) (hShapes : shapesOfVals vals = Ctx inShape ss) : vals[idx.id]? = some (packedAt vals idx hShapes)

Safe array lookup returns the packed value selected by packedAt.

@[simp]

theorem NN.Verification.Builtin.Proved.Correctness.packedAt_shape {α : Type} [TorchLean.Storage α] [Context α] {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (vals : Array (Spec.SomeTensor α)) (idx : Idx (Ctx inShape ss) s) (hShapes : shapesOfVals vals = Ctx inShape ss) : (packedAt vals idx hShapes).shape = s

The packed value selected by a typed index carries the statically expected shape.

def NN.Verification.Builtin.Proved.Correctness.tensorAt {α : Type} [TorchLean.Storage α] [Context α] {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (vals : Array (Spec.SomeTensor α)) (idx : Idx (Ctx inShape ss) s) (hShapes : shapesOfVals vals = Ctx inShape ss) : TorchLean.Tensor α s

The typed tensor selected by an index into a runtime context with the expected shapes.

theorem NN.Verification.Builtin.Proved.Correctness.ofTensor_tensorAt_eq_packedAt {α : Type} [TorchLean.Storage α] [Context α] {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (vals : Array (Spec.SomeTensor α)) (idx : Idx (Ctx inShape ss) s) (hShapes : shapesOfVals vals = Ctx inShape ss) : Spec.SomeTensor.ofTensor (tensorAt vals idx hShapes) = packedAt vals idx hShapes

Packing the typed tensor recovered from a well-shaped context returns the original value.

theorem NN.Verification.Builtin.Proved.Correctness.expectShape_packedAt_eq_ok {α : Type} [TorchLean.Storage α] [Context α] {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (vals : Array (Spec.SomeTensor α)) (idx : Idx (Ctx inShape ss) s) (hShapes : shapesOfVals vals = Ctx inShape ss) : IR.Graph.expectShape s (packedAt vals idx hShapes) = Except.ok (tensorAt vals idx hShapes)

Shape checking succeeds for the typed tensor extracted from a well-shaped context.

theorem NN.Verification.Builtin.Proved.Correctness.getVal_eq_ok_of_shapesOfVals_eq {α : Type} [TorchLean.Storage α] [Context α] {inShape : Spec.Shape} {ss : List Spec.Shape} {expected : Spec.Shape} (vals : Array (Spec.SomeTensor α)) (idx : Idx (Ctx inShape ss) expected) (hShapes : shapesOfVals vals = Ctx inShape ss) : getVal vals idx = Except.ok (tensorAt vals idx hShapes)

getVal succeeds from a well-shaped executable context.

This is the proof layer form of getVal_eq_ok: callers use the semantic invariant shapesOfVals vals = Ctx inShape ss, and the lemma derives the array-bounds fact internally.