Tensor gradient utilities (spec layer)

These are small, generic helpers that operate on gradient tensors:

• norm-based clipping (clip_gradients_spec)
• value-based clipping (clip_by_value_spec)
• percentile-based clipping (clip_by_percentile_spec)

They are defined at the spec layer so they can be used both:

• in executable training examples (instantiated at Float / NF backends), and
• in proofs (instantiated at ℝ).

Why clipping utilities belong in the spec layer:

• Gradient clipping is part of the algorithmic definition of many training loops. To reason about "the training step we ran," clipping must be part of the pure model of that step.
• We also want to reuse the same clipping logic across scalar backends: Float for executable runs, and proof-friendly scalars (ℝ, NF, etc.) for theorems and approximation statements.

Design note:

• These definitions are written for clarity and reuse across scalar backends. Backend-specific implementations (for example, fused kernels) belong in the runtime layer.

def Spec.clipGradientsSpec {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {s : Shape} (gradients : Tensor α s) (max_norm : α) : Tensor α s

Clip gradients by L2 norm (global norm over all elements).

This implements the common "global norm clipping" used in many optimizers:

1. compute $\lVert g\rVert_2$
2. if it exceeds max_norm, rescale $g$ so that $\lVert g\rVert_2=\mathtt{max\_norm}$.

Implementation detail:

• We compare squared norms first so we only compute sqrt in the clipping branch.
• We treat max_norm as a magnitude, so we use abs max_norm as the threshold.

def Spec.clipByValueSpec {α : Type} [Context α] {s : Shape} (gradients : Tensor α s) (min_val max_val : α) : Tensor α s

Clip gradients by value (elementwise clamp).

PyTorch analogy: torch.clamp(g, min=min_val, max=max_val).

def Spec.clipByPercentileSpec {α : Type} [Context α] {s : Shape} (gradients : Tensor α s) (pct : ℕ) [DecidableLT α] : Tensor α s

Clip gradients by percentile of absolute values.

This is a value clipping rule driven by the data:

• Flatten abs(g) to an array.
• Take the pct percentile (0..100) as a bound b.
• Return clamp(g, -b, b).

Notes:

• This definition sorts values, so it requires decidable comparison (DecidableLT α).
• In practice this is meant for executable scalars like Float or IEEE32Exec.

PyTorch analogy (conceptual): compute $b=\operatorname{quantile}(\lvert g\rvert,\mathtt{pct}/100)$ and clamp to $[-b,b]$.