ForwardScale

Forward scale propagation over SSA/DAG graphs.

This optional module mirrors NN.Proofs.RuntimeApprox.Graph.ForwardApprox, but for scale bounds (nonnegative bounds on linf_norm) rather than eps error bounds.

PyTorch analogue: users often track activation magnitudes (for normalization, stability, or analysis). Here we make that tracking explicit and compositional at the proof level.

structure Proofs.RuntimeApprox.FwdNodeScale {α : Type} (toSpec : α → Spec.SpecScalar) (Γ : List Spec.Shape) (τ : Spec.Shape) extends Proofs.RuntimeApprox.FwdNode toSpec Γ τ : Type

A forward node augmented with a scale bound function and a soundness lemma.

• forwardSpec : TList Spec.SpecScalar Γ → Spec.SpecTensor τ
• forwardRuntime : TList α Γ → Spec.Tensor α τ
• bound : EList Γ → TList α Γ → Spec.SpecScalar
• sound (xS : TList Spec.SpecScalar Γ) (xR : TList α Γ) (eps : EList Γ) : approxCtx toSpec xS xR eps → approxT toSpec (self.forwardSpec xS) (self.forwardRuntime xR) (self.bound eps xR)
• scaleBound : BList Γ → TList α Γ → NNReal
• scaleSound (ctxS : TList Spec.SpecScalar Γ) (ctxR : TList α Γ) (epsCtx : EList Γ) (bCtx : BList Γ) : approxCtx toSpec ctxS ctxR epsCtx → scaleCtx toSpec ctxS ctxR bCtx → scaleT toSpec (self.forwardSpec ctxS) (self.forwardRuntime ctxR) (self.scaleBound bCtx ctxR)

inductive Proofs.RuntimeApprox.FwdGraphScale {α : Type} (toSpec : α → Spec.SpecScalar) (Γ : List Spec.Shape) : List Spec.Shape → Type

Forward graph with scale-aware nodes.

• nil {α : Type} {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} : FwdGraphScale toSpec Γ []
• snoc {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} {τ : Spec.Shape} : FwdGraphScale toSpec Γ ss → FwdNodeScale toSpec (Γ ++ ss) τ → FwdGraphScale toSpec Γ (ss ++ [τ])

def Proofs.RuntimeApprox.FwdGraphScale.toFwdGraph {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} : FwdGraphScale toSpec Γ ss → FwdGraph toSpec Γ ss

Forget the scale annotations on nodes, producing an ordinary FwdGraph.

def Proofs.RuntimeApprox.FwdGraphScale.evalSpec {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : FwdGraphScale toSpec Γ ss) (x : TList Spec.SpecScalar Γ) : TList Spec.SpecScalar (Γ ++ ss)

Evaluate the forward pass on spec values, returning the extended context Γ ++ ss.

def Proofs.RuntimeApprox.FwdGraphScale.evalRuntime {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : FwdGraphScale toSpec Γ ss) (x : TList α Γ) : TList α (Γ ++ ss)

Evaluate the forward pass on runtime values, returning the extended context Γ ++ ss.

def Proofs.RuntimeApprox.FwdGraphScale.evalBounds {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : FwdGraphScale toSpec Γ ss) (epsIn : EList Γ) (xR : TList α Γ) : EList (Γ ++ ss)

Forward-pass error bounds for all intermediate nodes, computed from input bounds epsIn.

def Proofs.RuntimeApprox.FwdGraphScale.evalScales {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : FwdGraphScale toSpec Γ ss) (bIn : BList Γ) (xR : TList α Γ) : BList (Γ ++ ss)

Forward-pass scale bounds for all intermediate nodes, computed from input bounds bIn.

theorem Proofs.RuntimeApprox.FwdGraphScale.eval_scale {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : FwdGraphScale toSpec Γ ss) (xS : TList Spec.SpecScalar Γ) (xR : TList α Γ) (epsIn : EList Γ) (bIn : BList Γ) : approxCtx toSpec xS xR epsIn → scaleCtx toSpec xS xR bIn → scaleCtx toSpec (g.evalSpec xS) (g.evalRuntime xR) (g.evalScales bIn xR)