TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Verification.Builtin.Proved.Correctness.Eval.LoweringPrefix

Lowered Forward Evaluation: Prefix Preservation #

Lowering a forward let-chain only appends IR nodes and only inserts payload at fresh node ids. These lemmas record that every node and payload entry below the starting graph size is unchanged by lowering the rest of the chain.

source
def NN.Verification.Builtin.Proved.Correctness.lowerStep {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {mid : Spec.Shape} (node : Node α paramShapes inShape ss mid) (params : TorchLean.TensorPack α paramShapes) (c : LoweredIR α) :
LoweredIR α

The lowering accumulator after appending the lowering of one node at the fresh id.

Instances For
    source
    theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_let1 {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {mid out : Spec.Shape} (node : Node α paramShapes inShape ss mid) (gNext : ForwardLetChain α paramShapes inShape (ss ++ [mid]) out) (params : TorchLean.TensorPack α paramShapes) (c : LoweredIR α) :
    lowerForwardLetChain (ForwardLetChain.let1 node gNext) params c = lowerForwardLetChain gNext params (lowerStep node params c)

    Lowering a let1 chain lowers the head node and continues from the extended accumulator.

    source
    theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_ps_constVals_get?_lt {α : 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 α) {k : ℕ} (hk : k < c.graph.nodes.size) :
    (lowerForwardLetChain g params c).ps.constVals.get? k = c.ps.constVals.get? k

    Lowering a let-chain does not change ps.constVals entries for keys < c.graph.nodes.size. Lowering only inserts payload at the fresh node id, so older keys are unchanged.

    source
    theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_ps_linearWB_get?_lt {α : 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 α) {k : ℕ} (hk : k < c.graph.nodes.size) :
    (lowerForwardLetChain g params c).ps.linearWB.get? k = c.ps.linearWB.get? k

    Lowering a let-chain does not change ps.linearWB entries for keys < c.graph.nodes.size. Lowering only inserts linear payload at the fresh node id, so older keys are unchanged.

    source
    theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_ps_convCfg_get?_lt {α : 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 α) {k : ℕ} (hk : k < c.graph.nodes.size) :
    (lowerForwardLetChain g params c).ps.convCfg.get? k = c.ps.convCfg.get? k

    Lowering a let-chain does not change ps.convCfg entries for keys < c.graph.nodes.size. Lowering only inserts convolution payloads at fresh node ids, so older keys are unchanged.

    source
    theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_ps_batchNormEval_get?_lt {α : 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 α) {k : ℕ} (hk : k < c.graph.nodes.size) :
    (lowerForwardLetChain g params c).ps.batchNormEval.get? k = c.ps.batchNormEval.get? k

    Lowering a let-chain does not change ps.batchNormEval entries for keys below the starting graph size. Eval-mode BatchNorm payloads enter through the broader IR/import bridge, not through this proved first-order fragment.

    source
    theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_ps_layerNorm_get?_lt {α : 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 α) {k : ℕ} (hk : k < c.graph.nodes.size) :
    (lowerForwardLetChain g params c).ps.layerNorm.get? k = c.ps.layerNorm.get? k

    Lowering a let-chain preserves LayerNorm payloads below the starting graph size.

    A payload-free LayerNorm step erases only its own fresh id, preventing stale future entries from changing the source fragment's unit-affine semantics.

    source
    theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_getNode_lt {α : 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 α) {i : ℕ} (hi : i < c.graph.nodes.size) :
    (lowerForwardLetChain g params c).graph.getNode i = c.graph.getNode i

    lowerForwardLetChain does not change existing nodes at indices < c.graph.nodes.size. Lowering only appends nodes, so getNode agrees on the prefix.

    source
    theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_nodesSize_le {α : 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 α) :
    c.graph.nodes.size ≤ (lowerForwardLetChain g params c).graph.nodes.size

    lowerForwardLetChain is monotone in graph.nodes.size (it only appends nodes).