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 {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise addition.

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

noncomputable def Proofs.RuntimeApprox.NFBackend.subNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise subtraction (wraps approxTensor_sub_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.mulNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise multiplication (wraps approxTensor_mul_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.safeDivNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest 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 approxTensor_safeDiv_spec to obtain an unconditional bound.

noncomputable def Proofs.RuntimeApprox.NFBackend.scaleNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) (c : FloatLib.Floats.Formats.Flocq.NF β fexp rnd) : FwdNode toSpec Γ s

FwdNode for scaling by a runtime constant c.

Wraps approxTensor_scale_spec.

noncomputable def Proofs.RuntimeApprox.NFBackend.negNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise negation (wraps approxTensor_neg_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.absNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise absolute value (wraps approxTensor_abs_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.expNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise exponentiation (wraps approxTensor_exp_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.softplusNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise softplus (wraps approxTensor_softplus_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.safeLogNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest 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 approxTensor_safeLog_spec.

noncomputable def Proofs.RuntimeApprox.NFBackend.safeLogSoftplusNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) (ε : ℝ) (hε : 0 < ε) : FwdNode toSpec Γ s

FwdNode for the smooth safeLog activation.

Requires hε : 0 < ε and wraps approxTensor_safe_log_spec.

noncomputable def Proofs.RuntimeApprox.NFBackend.tanhNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise tanh (wraps approxTensor_tanh_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.sigmoidNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

FwdNode for elementwise sigmoid (wraps approxTensor_sigmoid_spec).

noncomputable def Proofs.RuntimeApprox.NFBackend.reluNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

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

noncomputable def Proofs.RuntimeApprox.NFBackend.softmaxNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ s

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

noncomputable def Proofs.RuntimeApprox.NFBackend.sumNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : FwdNode toSpec Γ Spec.Shape.scalar

FwdNode for sum reduction (sumSpec).

This reduces a tensor to a scalar and uses approxTensor_sum_spec with the accumulated sumBound.