Verified Forward Fragment: Graph Structure

The structural part of lowering correctness: every graph produced by lowerForwardProgramToIR satisfies the verifier IR well-formedness checks.

def NN.Verification.Builtin.Proved.Correctness.shapesOfVals {α : Type} [TorchLean.Storage α] [Context α] (vals : Array (Spec.SomeTensor α)) : List Spec.Shape

Extract the list of shapes from an array of dynamic values.

theorem NN.Verification.Builtin.Proved.Correctness.shapesOfVals_push {α : Type} [TorchLean.Storage α] [Context α] (vals : Array (Spec.SomeTensor α)) (v : Spec.SomeTensor α) : shapesOfVals (vals.push v) = shapesOfVals vals ++ [v.shape]

shapesOfVals commutes with pushing an element onto the value array.

theorem NN.Verification.Builtin.Proved.Correctness.getNode_push_lt (g : IR.Graph) (n : IR.Node) {i : ℕ} (hi : i < g.nodes.size) : { nodes := g.nodes.push n }.getNode i = g.getNode i

Pushing a node onto g.nodes does not affect getNode for earlier indices.

theorem NN.Verification.Builtin.Proved.Correctness.wellFormed_push (g : IR.Graph) (n : IR.Node) (hWF : g.wellFormed = true) (hId : n.id = g.nodes.size) (hArity : n.hasValidArity = true) (hParentsBelow : n.parentsBelow = true) : { nodes := g.nodes.push n }.wellFormed = true

Preservation of Graph.wellFormed under pushing a new node with the right id, arity, and parent discipline.

theorem NN.Verification.Builtin.Proved.Correctness.idx_id_lt_length {Γ : List Spec.Shape} {s : Spec.Shape} (x : Idx Γ s) : x.id < Γ.length

Any typed index Idx Γ s points to a position strictly below Γ.length.

theorem NN.Verification.Builtin.Proved.Correctness.idx_id_lt_ctxLen {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (x : Idx (Ctx inShape ss) s) : x.id < ss.length + 1

Specialized bound for indices into Ctx inShape ss = inShape :: ss.

theorem NN.Verification.Builtin.Proved.Correctness.lowerNode_hasValidArity {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (id : ℕ) (node : Node α paramShapes inShape ss out) (params : TorchLean.TensorPack α paramShapes) (ps : MLTheory.CROWN.Graph.ParamStore α) : (lowerNode id node params ps).1.hasValidArity = true

Lowered nodes always satisfy the IR arity check.

theorem NN.Verification.Builtin.Proved.Correctness.lowerNode_parentsBelow {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (params : TorchLean.TensorPack α paramShapes) (ps : MLTheory.CROWN.Graph.ParamStore α) (id : ℕ) (hId : id = (Ctx inShape ss).length) (node : Node α paramShapes inShape ss out) : (lowerNode id node params ps).1.parentsBelow = true

Lowered nodes satisfy parentsBelow when lowered at the next fresh id. Typed parent indices ensure parent ids are below the id of the newly-pushed node.

theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_wellFormed {α : 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) (c : LoweredIR α) (hSize : c.graph.nodes.size = (Ctx inShape ss).length) (hWF : c.graph.wellFormed = true) : (lowerForwardLetChain g params c).graph.wellFormed = true

Lowering preserves Graph.wellFormed while threading the lowering pass accumulator through a forward let-chain.

theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardProgramToIR_wellFormed {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape outShape : Spec.Shape} (p : ForwardProgram α paramShapes inShape outShape) (params : TorchLean.TensorPack α paramShapes) : (lowerForwardProgramToIR p params).graph.wellFormed = true

Graphs produced by lowerForwardProgramToIR satisfy the IR structural discipline (Graph.wellFormed = true).