NF Forward Graph Nodes

FwdNode constructors for the NF backend. These package the operation, runtime implementation, bound computation, and soundness theorem so larger SSA/DAG graphs can compose the primitive proofs.

noncomputable def Proofs.RuntimeApprox.NFBackend.addNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise addition.

This packages approxT_add_spec so addition can be used inside larger verified FwdGraphs.

noncomputable def Proofs.RuntimeApprox.NFBackend.subNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise subtraction (wraps approxT_sub_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.mulNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise multiplication (wraps approxT_mul_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.safeDivNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) (ε : ℝ) (hε : 0 < ε) : FwdNode toSpec Γ s

FwdNode for clamped division safeDiv.

Requires a proof hε : 0 < ε and uses approxT_safeDiv_spec to obtain an unconditional bound.

noncomputable def Proofs.RuntimeApprox.NFBackend.scaleNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) (c : TorchLean.Floats.NF β fexp rnd) : FwdNode toSpec Γ s

FwdNode for scaling by a runtime constant c.

Wraps approxT_scale_spec.

noncomputable def Proofs.RuntimeApprox.NFBackend.negNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise negation (wraps approxT_neg_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.absNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise absolute value (wraps approxT_abs_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.expNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise exponentiation (wraps approxT_exp_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.softplusNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise softplus (wraps approxT_softplus_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.safeLogNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) (ε : ℝ) (hε : 0 < ε) : FwdNode toSpec Γ s

FwdNode for clamped log safeLog.

Requires a proof hε : 0 < ε and wraps approxT_safeLog_spec.

noncomputable def Proofs.RuntimeApprox.NFBackend.safeLogSoftplusNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) (ε : ℝ) (hε : 0 < ε) : FwdNode toSpec Γ s

FwdNode for the smooth safe_log activation.

Requires hε : 0 < ε and wraps approxT_safe_log_spec.

noncomputable def Proofs.RuntimeApprox.NFBackend.tanhNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise tanh (wraps approxT_tanh_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.sigmoidNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise sigmoid (wraps approxT_sigmoid_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.reluNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise ReLU (max · 0, wraps approxT_relu_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.softmaxNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for the scalar logistic-form softmax node (wraps approxT_softmax_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.sumNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ Spec.Shape.scalar

FwdNode for sum reduction (sum_spec).

This reduces a tensor to a scalar and uses approxT_sum_spec with the accumulated sum_bound.