Op Specs - The Formal Era

Op Specs live in TheFormalEra.Ops (specs/TheFormalEra/Ops/). Each is a noncomputable def over Mathlib’s ℝ. Model Specs instantiate them with constants; a node’s op field names the Op Spec it uses.

Scalar functions

noncomputable def sigmoid (x : ℝ) : ℝ := 1 / (1 + Real.exp (-x))
noncomputable def silu (x : ℝ) : ℝ := x * sigmoid x
noncomputable def softplus (x : ℝ) : ℝ := Real.log (1 + Real.exp x)
/-- Tanh approximation of GELU (`gelu_pytorch_tanh`). -/
noncomputable def geluTanh (x : ℝ) : ℝ :=
  1 / 2 * x * (1 + Real.tanh (Real.sqrt (2 / Real.pi) * (x + 44715 / 1000000 * x ^ 3)))
/-- Soft-capping `c · tanh(x / c)`. -/
noncomputable def softcap (c x : ℝ) : ℝ := c * Real.tanh (x / c)

Normalisation

Op Spec	Formula	Used by
`rmsnorm`	`x / √(mean(x²) + ε) · w`	Qwen3, Granite, Gemma 4
`rmsnormOffset`	`x / √(mean(x²) + ε) · (1 + w)`	Qwen3.8, Muse Glimmer
`rmsnormUnit`	`x / √(mean(x²) + ε)` (no weight)	Gemma 4 value norm, Muse Glimmer q/k and embedding norms
`rmsnormGated`	`w ⊙ x / √(mean(x²) + ε) ⊙ silu(z)`	Gated DeltaNet output
`l2norm`	`x / √(Σ x² + ε)`	Delta-rule queries and keys

noncomputable def rmsnormOffset (eps : ℝ) (x : ι → Fin H → ℝ) (w : Fin H → ℝ) : ι → Fin H → ℝ :=
  fun t h => x t h / Real.sqrt ((∑ j, x t j ^ 2) / (H : ℝ) + eps) * (1 + w h)

The row index type ι is arbitrary: tokens Fin T for a hidden-state norm, or (token, head) pairs for a per-head norm.

Linear maps and feed-forward

Op Spec	Formula
`linear`	`y[t, n] = Σₖ x[t, k] · W[n, k]`: a bias-free `nn.Linear(K, N)`, `W` stored `[N, K]`
`gateUp`	`[x W_gateᵀ ‖ x W_upᵀ]`, gate first
`siluMul`	`y[t, i] = silu(gu[t, i]) · gu[t, I + i]` (SwiGLU on a fused `[gate ‖ up]` row)
`geluMul`	`y[t, i] = geluTanh(gu[t, i]) · gu[t, I + i]` (GeGLU)
`residual`	`y = x + r · h` (`r = 1` except where a model uses a residual multiplier)
`embed`	`y[t] = c · E[tokens[t]]`
`lmHead`	`z = mul · x Wᵀ`, then optionally `softcap c z`

Attention

noncomputable def softmax {L : ℕ} (s : Fin L → ℝ) (visible : Fin L → Prop)
    [DecidablePred visible] : Fin L → ℝ :=
  fun l => if visible l then
    Real.exp (s l) / ∑ m ∈ Finset.univ.filter visible, Real.exp (s m) else 0

noncomputable def causalGQA {S L Hkv G D : ℕ} (scale : ℝ) (pos : Fin S → ℕ)
    (q : Fin S → Fin Hkv → Fin G → Fin D → ℝ)
    (k v : Fin L → Fin Hkv → Fin D → ℝ) : Fin S → Fin Hkv → Fin G → Fin D → ℝ :=
  fun s c g d =>
    let logit : Fin L → ℝ := fun l => scale * ∑ e, q s c g e * k l c e
    ∑ l, softmax logit (fun l => l.val ≤ pos s) l * v l c d

Op Spec	What it is
`causalGQA`	Causal grouped-query attention: KV head `c` serves `G` query heads
`slidingGQA`	The same, where the query at position `p` sees keys `l` with `p − w < l ≤ p`
`decodeGQA`	Decode attention: one query at the last position of `L` cached tokens. Query head `c·G + g` reads KV head `c`.
`sigmoidGate`	Output gate of gated attention: `o ⊙ σ(gate)`

The sliding-window decode nodes of Gemma 4 and Muse Glimmer are labelled slidingDecodeGQA in the compute graph: decode attention over the last w cached positions. In spec 1.0 that label has no Lean definition of its own. The window semantics are defined by slidingGQA, and the conformance oracle evaluates them, but the engine has no Op Spec to prove a sliding-window decode kernel against. Those kernels are UNKNOWN.

Rotary embeddings

noncomputable def invFreq (theta : ℝ) (denom active i : ℕ) : ℝ :=
  if i < active then theta ^ (-(2 * (i : ℝ) / denom)) else 0

rope θ rot denom active rotates pairs (i, i + rot/2) for i < rot/2 by pos · invFreq i, and leaves coordinates ≥ rot unchanged. That one definition covers every variant in the supported models:

Variant	Parameters	Example
Full RoPE	`rot = denom = D`, `active = D/2`	Qwen3-0.6B, Granite
Partial RoPE	`rot = denom < D`	Qwen3.8-27B: 64 of 256 dimensions
Proportional RoPE	`rot = denom = D`, `active < D/2`	Gemma 4 global layers: 64 active frequencies of 256
NoPE	no `attn.rope` node	Muse Glimmer global layers

Gated DeltaNet

/-- State of the gated delta rule (single head):
    S_t = α_t · S_{t-1} · (I − β_t k_t k_tᵀ) + β_t v_t k_tᵀ -/
noncomputable def gdnState {T Dk Dv : ℕ} (α β : Fin T → ℝ)
    (k : Fin T → Fin Dk → ℝ) (v : Fin T → Fin Dv → ℝ) :
    (t : ℕ) → t ≤ T → Matrix (Fin Dv) (Fin Dk) ℝ
  | 0, _ => 0
  | t + 1, h =>
    let i : Fin T := ⟨t, h⟩
    α i • (gdnState α β k v t (Nat.le_of_succ_le h) * (1 - β i • Matrix.vecMulVec (k i) (k i)))
      + β i • Matrix.vecMulVec (v i) (k i)

/-- Output at step t: o_t = S_t q_t -/
noncomputable def gatedDeltaRule {T Dk Dv : ℕ} (α β : Fin T → ℝ)
    (q k : Fin T → Fin Dk → ℝ) (v : Fin T → Fin Dv → ℝ) : Fin T → Fin Dv → ℝ :=
  fun i => (gdnState α β k v (i.val + 1) i.isLt).mulVec (q i)

Op Spec	What it is
`gatedDeltaRule`	The recurrence above; the decode step is `gdnStep` (`gdnState_succ` proves they agree)
`causalConvSilu`	Depthwise causal convolution of width `K` followed by SiLU, with zero left padding

High-performance kernels use the chunk-parallel (WY) form, which looks nothing like this recurrence. chunkDeltaRule_eq proves in Lean that the chunked form equals the recurrence, for every chunk size.

​Scalar functions

​Normalisation

​Linear maps and feed-forward

​Attention

​Rotary embeddings

​Gated DeltaNet

Scalar functions

Normalisation

Linear maps and feed-forward

Attention

Rotary embeddings

Gated DeltaNet