From 9dcc8d66975970750e456e98d7bdfa563c6f4c98 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 01:40:47 +0700 Subject: [PATCH] spec(nn): make attention.t27 compile and pass with 0 vacuous tests (Closes #10094) The module read constants::PHI_CUBED_INV from math::constants, which t27c does not resolve. It is now self-contained (use base::types only): phi, phi^-3 = 1/phi^3 and the sacred scale 81^(-phi^-3) are local constants, checked by tests against phi^2 = phi + 1, phi^2 + phi^-2 = 3, sqrt(5) - 2 and exp(-gamma ln 81). Math fix: the causal mask set masked scores to 0.0 before the softmax, so future positions still got positive weight. The mask is now a very negative score and future weights are exactly 0.0. The QK-gain ablation module is folded in, with the two empty-bodied functions implemented and the gain applied to Q and K (score x gain^2). Dropped: unused attention types and phase constants, the bench blocks, the BPB training run, and tests that asserted constants against themselves. 35 tests, 35 pass, 0 fail, 0 vacuous; 9 invariants. Five mutants (mask, causal comparison, softmax shift, RoPE sign, QK gain) each fail >= 1 test. Seals re-saved on the lab. Co-Authored-By: Claude Opus 5.5 --- .trinity/seals/SacredAttention.json | 19 +- .trinity/seals/nn_SacredAttention.json | 37 +- specs/nn/attention.t27 | 1692 ++++++++++++------------ 3 files changed, 897 insertions(+), 851 deletions(-) diff --git a/.trinity/seals/SacredAttention.json b/.trinity/seals/SacredAttention.json index 0b3572e43c..c3ee453269 100644 --- a/.trinity/seals/SacredAttention.json +++ b/.trinity/seals/SacredAttention.json @@ -1,14 +1,19 @@ { - "gen_hash_c": "sha256:e75168deb5c7e973eb84215c005b0c7d2469fe9c32db7465698e8605962562b8", - "gen_hash_rust": "sha256:82d7a7f6fdc205ca72ce8e4395d92dbce5f86c273bd4aa0ba90aba4d0d879180", - "gen_hash_verilog": "sha256:495b48a5c98b7c1fccab460f017fcc48da428a1789ba23eaa7691edc1d0d9e13", - "gen_hash_zig": "sha256:292d274755a74b29e942065441a84629a6ce760f21d7ca1ce8e85aed92c4d927", + "gen_hash_c": "sha256:3866e812c08467cfeeddb6ba009beebb164df706e571cc839f79cc0f8b15b34a", + "gen_hash_rust": "sha256:4fc50d64d99e9a5b70d48f7a5f28d91824541ede8d198cfb28359c77894c760c", + "gen_hash_verilog": "sha256:fbdce65faac2e1e185c56b1008b87a00e41a4eaccd6c7e443185ef5fd20494d4", + "gen_hash_zig": "sha256:cd1ad49182a2220333958e2fd58b42d8f6a52005811dbf12c1ee4c3cdf99d80d", "module": "SacredAttention", "ring": 12, - "sealed_at": "2026-10-11T10:43:23Z", - "spec_hash": "sha256:be83d2a916a15957502d6afa4d6eff7ab07d0373e81555704ee842500db47187", + "sealed_at": "2026-10-17T18:39:31Z", + "spec_hash": "sha256:c40795145b0dcc397d9a3d23a7c8fc72dc8144f27afeb6ead112b18cc6045e7a", "spec_path": "specs/nn/attention.t27", "tests": { - "blocked": "does not compile: spec.zig:30:27: error: use of undeclared identifier 'PHI_CUBED_INV'" + "failed": 0, + "failing": [], + "forced": false, + "passed": 35, + "total": 35, + "vacuous": 0 } } \ No newline at end of file diff --git a/.trinity/seals/nn_SacredAttention.json b/.trinity/seals/nn_SacredAttention.json index 6dd82f820a..e142591872 100644 --- a/.trinity/seals/nn_SacredAttention.json +++ b/.trinity/seals/nn_SacredAttention.json @@ -1,41 +1,30 @@ { - "built_by": "t27c-bootstrap@0.5.2+cc19d1fcd", + "built_by": "t27c-bootstrap@0.5.2+efe3c94", "closure": [ - { - "spec": "specs/base/ops.t27", - "spec_hash": "sha256:8e6c6168f64ff2d654a3b276d7f3ceee4fbd408d334590ce03467b1f3aaa68b3" - }, { "spec": "specs/base/types.t27", "spec_hash": "sha256:3c2fb2a2edf20e90bc76798fb5d12690b2f60fc0f5bbf2f6052936e22d6e62e2" - }, - { - "spec": "specs/math/constants.t27", - "spec_hash": "sha256:57187e7afda1d88167b2af0382ad7f0623aa6b269ba020a78e3ffeebba1161bb" - }, - { - "spec": "specs/nn/attention.t27", - "spec_hash": "sha256:be83d2a916a15957502d6afa4d6eff7ab07d0373e81555704ee842500db47187" - }, - { - "spec": "specs/numeric/gf16.t27", - "spec_hash": "sha256:2a33d77db23966331716955924d08e30d12a3af361067da0a2c7072b7f4b7b0d" } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:e75168deb5c7e973eb84215c005b0c7d2469fe9c32db7465698e8605962562b8", - "gen_hash_rust": "sha256:82d7a7f6fdc205ca72ce8e4395d92dbce5f86c273bd4aa0ba90aba4d0d879180", - "gen_hash_verilog": "sha256:495b48a5c98b7c1fccab460f017fcc48da428a1789ba23eaa7691edc1d0d9e13", - "gen_hash_zig": "sha256:292d274755a74b29e942065441a84629a6ce760f21d7ca1ce8e85aed92c4d927", + "gen_hash_c": "sha256:3866e812c08467cfeeddb6ba009beebb164df706e571cc839f79cc0f8b15b34a", + "gen_hash_rust": "sha256:4fc50d64d99e9a5b70d48f7a5f28d91824541ede8d198cfb28359c77894c760c", + "gen_hash_verilog": "sha256:fbdce65faac2e1e185c56b1008b87a00e41a4eaccd6c7e443185ef5fd20494d4", + "gen_hash_zig": "sha256:cd1ad49182a2220333958e2fd58b42d8f6a52005811dbf12c1ee4c3cdf99d80d", "module": "SacredAttention", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-11T10:43:23Z", + "sealed_at": "2026-10-17T18:39:31Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:be83d2a916a15957502d6afa4d6eff7ab07d0373e81555704ee842500db47187", + "spec_hash": "sha256:c40795145b0dcc397d9a3d23a7c8fc72dc8144f27afeb6ead112b18cc6045e7a", "spec_path": "specs/nn/attention.t27", "tests": { - "blocked": "does not compile: spec.zig:30:27: error: use of undeclared identifier 'PHI_CUBED_INV'" + "failed": 0, + "failing": [], + "forced": false, + "passed": 35, + "total": 35, + "vacuous": 0 }, "toolchain": { "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", diff --git a/specs/nn/attention.t27 b/specs/nn/attention.t27 index e7e7583434..11eefbd3d6 100644 --- a/specs/nn/attention.t27 +++ b/specs/nn/attention.t27 @@ -1,943 +1,995 @@ // SPDX-License-Identifier: Apache-2.0 // t27/specs/nn/attention.t27 // Sacred Attention Specification -// Multi-head attention with φ-RoPE and sacred scaling (d_k^(-φ³)) -// φ² + 1/φ² = 3 | TRINITY +// Multi-head causal attention with phi-RoPE and sacred scaling (d_k^(-phi^3)) +// phi^2 + 1/phi^2 = 3 | TRINITY +// +// This spec never compiled: it read constants::PHI_CUBED_INV and +// constants::PHI, which math::constants does not define for t27c ("use of +// undeclared identifier 'constants'"); it computed its scale with a pow() +// that has a negative non-integer exponent; its tests built buffers with +// `AttentionBuffers{...}` and called functions that take a pointer to them; +// and the second module appended below it (AttentionQKGainAblation) had two +// functions with empty bodies, called run_attention_with_gain and +// attention_forward, which exist nowhere, and asserted gain constants against +// themselves. +// +// It is written out now with only `use base::types`: +// - phi, phi^-3 and the sacred scale 81^(-phi^-3) are local constants; the +// tests check them against independent identities (phi^2 = phi + 1, +// phi^2 + phi^-2 = 3, phi^-3 = sqrt(5) - 2, exp(-phi^-3 ln 81)). +// - the buffers are slices the caller owns, so every step can be tested on +// its own; the phi-RoPE tables live in module storage. +// - the causal mask is a very negative score, not 0.0: with 0.0 a masked +// position still received softmax weight exp(0 - max) > 0, so any call +// with seq_len > position + 1 read the future. +// - the QK-gain ablation is one scalar, qk_gain, applied to Q and K before +// the dot product (so it multiplies the score by gain^2), with the +// variants phi^2, 1.0, learned-at-1.0 and sqrt(phi) as constants. +// Dropped, because nothing here implements or measures them: the bidirectional +// and sparse attention types and the six phase constants (no code reads them); +// the ablation's training run (run_attention_with_gain, a BPB measurement); +// the `bench` blocks (their targets named buffers and calls that do not exist, +// and a bench measures nothing the compiler can check); the gf16 type for the +// gains (f64 here). +// +// The kernel is checked on an identity-weight case computed by hand, against a +// two-position case with a closed form, and against a future-poisoned cache. +// The caller runs sacred_attention_init() once before the kernel (tables). module SacredAttention { - // Import base types, operations, and math constants use base::types; - use base::ops; - use math::constants; - // ═════════════════════════════════════════════════════════════════ + // ===================================================================== // 1. Constants - // ═════════════════════════════════════════════════════════════════════════ + // ===================================================================== // TRINITY-based configuration - const NUM_HEADS : usize = 3; // 3 heads (TRINITY) - const HEAD_DIM : usize = 81; // 81 dim per head (3⁴) - const EMBED_DIM : usize = 243; // Total embedding (3 × 81) - const CONTEXT_LEN : usize = 81; // Max sequence length - const ROPE_PAIRS : usize = 40; // 81/2 = 40 pairs (1 unrotated) - - // Sacred scaling: φ⁻³ and d_k^(-φ³) - const SACRED_GAMMA : f64 = constants::PHI_CUBED_INV; // φ⁻³ ≈ 0.236 - const SACRED_SCALE : f64 = pow(81.0, -SACRED_GAMMA); // 81^(-φ⁻³) ≈ 0.354 - - // Attention types - const ATTN_CAUSAL : u8 = 0; // Causal (autoregressive) attention - const ATTN_BIDIR : u8 = 1; // Bidirectional attention - const ATTN_SPARSE : u8 = 2; // Sparse (local) attention - - // Attention phase states - const PHASE_QUERY : u8 = 0; // Compute Q projections - const PHASE_KEY : u8 = 1; // Compute K projections - const PHASE_VALUE : u8 = 2; // Compute V projections - const PHASE_SCORE : u8 = 3; // Compute attention scores - const PHASE_SOFTMAX : u8 = 4; // Apply softmax - const PHASE_WEIGHT : u8 = 5; // Apply to values - - // ═════════════════════════════════════════════════════════════════ - // 2. RoPE Tables - // ═════════════════════════════════════════════════════════════════════════ - - // φ-RoPE tables: [CONTEXT_LEN × ROPE_PAIRS] - // Each entry is precomputed cos(p * θ_i) and sin(p * θ_i) - // where θ_i = φ^(-2i/HEAD_DIM) for i=0..ROPE_PAIRS-1 - struct RoPETables { - cos : [CONTEXT_LEN * ROPE_PAIRS]f64, - sin : [CONTEXT_LEN * ROPE_PAIRS]f64, - } - - var rope_tables : RoPETables; - - // ═════════════════════════════════════════════════════════════════ - // 3. Attention State - // ═════════════════════════════════════════════════════════════════════════ - - // Attention buffers (allocated per forward pass) - struct AttentionBuffers { - q_buffer : [EMBED_DIM]f64, // Query projections - k_buffer : [EMBED_DIM]f64, // Key projections - v_buffer : [EMBED_DIM]f64, // Value projections - scores : [NUM_HEADS * CONTEXT_LEN]f64, // Attention scores - concat : [EMBED_DIM]f64, // Concatenated head outputs - } - - // ═════════════════════════════════════════════════════════════════ - // 4. Initialization - // ═════════════════════════════════════════════════════════════════════════ - - // sacred_attention_init() → void - // Initialize φ-RoPE tables - // θ_i = φ^(-2i/HEAD_DIM) for i=0..ROPE_PAIRS-1 - // For each position p: cos(p*θ_i), sin(p*θ_i) - fn sacred_attention_init() -> void { - var p : usize = 0; - - while (p < CONTEXT_LEN) { - var i : usize = 0; - - while (i < ROPE_PAIRS) { - // Compute freq = φ^(-2i/HEAD_DIM) - const freq_exponent = -2.0 * (i as f64) / (HEAD_DIM as f64); - const freq = pow(constants::PHI, freq_exponent); - - // angle = position * freq - const angle = (p as f64) * freq; - - // cos and sin - const cos_val = cos(angle); - const sin_val = sin(angle); - - // Store in tables - const table_offset = p * ROPE_PAIRS + i; - rope_tables.cos[table_offset] = cos_val; - rope_tables.sin[table_offset] = sin_val; - - i = i + 1; - } - - p = p + 1; + const NUM_HEADS : usize = 3; // 3 heads + const HEAD_DIM : usize = 81; // 81 per head (3^4) + const EMBED_DIM : usize = 243; // total embedding (3 x 81) + const CONTEXT_LEN : usize = 81; // max sequence length + const ROPE_PAIRS : usize = 40; // pairs (i, i + 40) per head; dim 80 unrotated + + // The golden ratio, and phi^-3 = 1 / phi^3 = sqrt(5) - 2 + const PHI : f64 = 1.618033988749895; + const PHI_CUBED_INV : f64 = 1.0 / (PHI * PHI * PHI); + + // Sacred scaling: gamma = phi^-3 and the score scale 81^(-gamma) = 0.3543788557 + const SACRED_GAMMA : f64 = PHI_CUBED_INV; + const SACRED_SCALE : f64 = 0.3543788557382518; + + // A masked score: exp(MASK_SCORE - anything finite) underflows to exactly 0.0 + const MASK_SCORE : f64 = 0.0 - 1.0e30; + + // QK-gain ablation variants (Phase B2): the gain applied to Q and K + const GAIN_PHI_SQ : f64 = 2.618033988749895; // phi^2 = phi + 1 [open conjecture] + const GAIN_STANDARD : f64 = 1.0; // baseline + const GAIN_SQRT_PHI : f64 = 1.272019649514069; // sqrt(phi) [open conjecture] + const GAIN_LEARNED_INIT : f64 = 1.0; // a learned gain starts at 1.0 + + // Variant ids for get_qk_gain + const QK_PHI_SQUARED : u8 = 0; + const QK_STANDARD : u8 = 1; + const QK_LEARNED : u8 = 2; + const QK_SQRT_PHI : u8 = 3; + + // ===================================================================== + // 2. Storage + // ===================================================================== + + // phi-RoPE tables [position][pair]: cos(p * theta_i), sin(p * theta_i), + // theta_i = phi^(-2i / HEAD_DIM) + var rope_cos : [CONTEXT_LEN * ROPE_PAIRS]f64 = undefined; + var rope_sin : [CONTEXT_LEN * ROPE_PAIRS]f64 = undefined; + + // The QK gain: Q and K are scaled by it, so scores by its square + var qk_gain : f64 = 1.0; + + // ===================================================================== + // 3. Kernels + // ===================================================================== + + fn fill(x: []f64, value: f64) -> void { + var i : usize = 0; + while (i < x.len) { + x[i] = value; + i = i + 1; } } - // ═════════════════════════════════════════════════════════════════ - // 5. Main Attention Kernel - // ═════════════════════════════════════════════════════════════════════════ - - // sacred_attention_kernel( - // input: []f32, // [EMBED_DIM] input embeddings - // w_q: []Trit, w_k: []Trit, w_v: []Trit, w_o: []Trit, // Ternary weights - // position: usize, - // seq_len: usize, - // output: []f32, // [EMBED_DIM] output - // cache_k: []f32, cache_v: []f32, // [CONTEXT_LEN][EMBED_DIM] - // ) → void - // Single position forward pass with sacred scaling - fn sacred_attention_kernel( - input: []f64, - w_q: []Trit, w_k: []Trit, w_v: []Trit, w_o: []Trit, - position: usize, - seq_len: usize, - output: []f64, - cache_k: []f64, cache_v: []f64, - ) -> void { - var buffers = AttentionBuffers{ - .q_buffer = [0.0; EMBED_DIM], - .k_buffer = [0.0; EMBED_DIM], - .v_buffer = [0.0; EMBED_DIM], - .scores = [0.0; NUM_HEADS * CONTEXT_LEN], - .concat = [0.0; EMBED_DIM], - }; - - // Step 1: Project Q, K, V via ternary matmul - project_qkv(&buffers, input, w_q, w_k, w_v); - - // Step 2: Apply φ-RoPE to Q and K - apply_rope_qk(&buffers, position); - - // Step 3: Cache K and V - cache_kv(&buffers, position, cache_k, cache_v); - - // Step 4: Compute attention scores (Q @ K^T * SACRED_SCALE) - compute_scores(&buffers, position, seq_len, cache_k); - - // Step 5: Apply softmax to scores - apply_softmax(&buffers, seq_len); - - // Step 6: Weighted sum of values - weighted_values(&buffers, seq_len, cache_v); - - // Step 7: Output projection via W_o - project_output(&buffers, w_o, output); - - // Step 8: Add residual connection - add_residual(output, input); - } - - // ═════════════════════════════════════════════════════════════════ - // 6. Q/K/V Projection - // ═════════════════════════════════════════════════════════════════════════ - - // project_qkv(buffers, input, w_q, w_k, w_v) → void - // Compute Q, K, V projections using ternary matrix multiplication - // Q[i] = Σ_j input[j] * W_q[j][i] - // Using ternary weights: W_q[j][i] ∈ {-1, 0, +1} - fn project_qkv( - buffers: *AttentionBuffers, - input: []f64, - w_q: []Trit, w_k: []Trit, w_v: []Trit, - ) -> void { - // Compute Q - ternary_matmul(input, w_q, &buffers.q_buffer, EMBED_DIM, EMBED_DIM); - - // Compute K - ternary_matmul(input, w_k, &buffers.k_buffer, EMBED_DIM, EMBED_DIM); - - // Compute V - ternary_matmul(input, w_v, &buffers.v_buffer, EMBED_DIM, EMBED_DIM); - } - - // ternary_matmul(input, weights, output, in_dim, out_dim) → void - // Matrix multiplication with ternary weights - fn ternary_matmul( - input: []f64, - weights: []Trit, - output: []f64, - in_dim: usize, - out_dim: usize, - ) -> void { + // output[i] = sum_j input[j] * w[j * out_dim + i], trits as -1 / 0 / +1 + fn ternary_matmul(input: []const f64, weights: []const Trit, output: []f64, in_dim: usize, out_dim: usize) -> void { var i : usize = 0; - while (i < out_dim) { var acc : f64 = 0.0; var j : usize = 0; - while (j < in_dim) { - const weight_val = weights[j * out_dim + i] as i8; - - if (weight_val == 1) { + const w = weights[j * out_dim + i]; + if (w == Trit.pos) { acc = acc + input[j]; - } else if (weight_val == -1) { + } else if (w == Trit.neg) { acc = acc - input[j]; } - j = j + 1; } - output[i] = acc; i = i + 1; } } - // ═════════════════════════════════════════════════════════════════ - // 7. φ-RoPE Application - // ═════════════════════════════════════════════════════════════════════════ + // Fills the phi-RoPE tables and resets the QK gain to 1.0 + fn sacred_attention_init() -> void { + const ln_phi = log(PHI); + var p : usize = 0; + while (p < CONTEXT_LEN) { + var i : usize = 0; + while (i < ROPE_PAIRS) { + const t = 2.0 * @as(f64, @floatFromInt(i)) / @as(f64, @floatFromInt(HEAD_DIM)); + const angle = @as(f64, @floatFromInt(p)) * exp(0.0 - t * ln_phi); + rope_cos[p * ROPE_PAIRS + i] = cos(angle); + rope_sin[p * ROPE_PAIRS + i] = sin(angle); + i = i + 1; + } + p = p + 1; + } + qk_gain = 1.0; + } + + fn set_qk_gain(gain: f64) -> void { + qk_gain = gain; + } + + // The gain of an ablation variant; an unknown id gets the standard gain + fn get_qk_gain(variant: u8) -> f64 { + if (variant == QK_PHI_SQUARED) { + return GAIN_PHI_SQ; + } + if (variant == QK_SQRT_PHI) { + return GAIN_SQRT_PHI; + } + if (variant == QK_LEARNED) { + return GAIN_LEARNED_INIT; + } + return GAIN_STANDARD; + } + + // Score scale of the ablation against plain attention: gain^2 / sqrt(head_dim). + // Q and K both carry the gain, so the dot product picks up gain^2. + fn effective_score_scale(gain: f64, head_dim: f64) -> f64 { + return gain * gain / sqrt(head_dim); + } - // apply_rope_qk(buffers, position) → void - // Apply φ-RoPE rotation to Q and K - // Rotates pairs of dimensions using precomputed tables - fn apply_rope_qk(buffers: *AttentionBuffers, position: usize) -> void { - // `rope_tables.cos` is [CONTEXT_LEN * ROPE_PAIRS] and this reads - // `position * ROPE_PAIRS + pair_idx`. Nothing bounded `position`, so a - // caller past the end read off the end of the table -- a panic in the - // generated Rust, and a silent read in C, where a []T is a bare pointer. + // Rotates pairs (i, i + 40) of every head of x (EMBED_DIM long) by the + // position's angles; inverse rotates the other way (the transpose). + // A position past the tables is left alone: the table is + // [CONTEXT_LEN * ROPE_PAIRS] and nothing else bounds `position`. + fn rope(x: []f64, position: usize, inverse: bool) -> void { if (position >= CONTEXT_LEN) { return; } var h : usize = 0; - while (h < NUM_HEADS) { - const head_offset = h * HEAD_DIM; - var pair_idx : usize = 0; - - while (pair_idx < ROPE_PAIRS) { - const idx0 = head_offset + pair_idx; - const idx1 = head_offset + pair_idx + ROPE_PAIRS; - - const table_offset = position * ROPE_PAIRS + pair_idx; - const cos_val = rope_tables.cos[table_offset]; - const sin_val = rope_tables.sin[table_offset]; - - // Rotate Q - const q0 = buffers.q_buffer[idx0]; - const q1 = buffers.q_buffer[idx1]; - buffers.q_buffer[idx0] = q0 * cos_val - q1 * sin_val; - buffers.q_buffer[idx1] = q0 * sin_val + q1 * cos_val; - - // Rotate K - const k0 = buffers.k_buffer[idx0]; - const k1 = buffers.k_buffer[idx1]; - buffers.k_buffer[idx0] = k0 * cos_val - k1 * sin_val; - buffers.k_buffer[idx1] = k0 * sin_val + k1 * cos_val; - - pair_idx = pair_idx + 1; + var i : usize = 0; + while (i < ROPE_PAIRS) { + const c = rope_cos[position * ROPE_PAIRS + i]; + var s = rope_sin[position * ROPE_PAIRS + i]; + if (inverse) { + s = 0.0 - s; + } + const i0 = h * HEAD_DIM + i; + const i1 = i0 + ROPE_PAIRS; + const x0 = x[i0]; + const x1 = x[i1]; + x[i0] = x0 * c - x1 * s; + x[i1] = x0 * s + x1 * c; + i = i + 1; } - h = h + 1; } } - // ═════════════════════════════════════════════════════════════════ - // 8. KV Caching - // ═════════════════════════════════════════════════════════════════════════ - - // cache_kv(buffers, position, cache_k, cache_v) → void - // Cache K and V at the current position - fn cache_kv( - buffers: *AttentionBuffers, - position: usize, - cache_k: []f64, cache_v: []f64, - ) -> void { - // The shape is stated in a comment on the declaration -- - // `cache_k: []f64, cache_v: []f64, // [CONTEXT_LEN][EMBED_DIM]` -- and - // was enforced nowhere. `position` indexes into that, so an unbounded - // one writes past the end. + // Stores k and v at `position` in the caches ([CONTEXT_LEN][EMBED_DIM]). + // A position past the end writes nothing. + fn cache_kv(k: []const f64, v: []const f64, position: usize, cache_k: []f64, cache_v: []f64) -> void { if (position >= CONTEXT_LEN) { return; } const offset = position * EMBED_DIM; var i : usize = 0; - while (i < EMBED_DIM) { - cache_k[offset + i] = buffers.k_buffer[i]; - cache_v[offset + i] = buffers.v_buffer[i]; + cache_k[offset + i] = k[i]; + cache_v[offset + i] = v[i]; i = i + 1; } } - // ═════════════════════════════════════════════════════════════════ - // 9. Score Computation - // ═════════════════════════════════════════════════════════════════════════ - - // compute_scores(buffers, position, seq_len, cache_k) → void - // Compute attention scores: Q @ K^T * SACRED_SCALE - // For causal attention: only positions <= current position - fn compute_scores( - buffers: *AttentionBuffers, - position: usize, - seq_len: usize, - cache_k: []f64, - ) -> void { - // `buffers.scores` is [NUM_HEADS * CONTEXT_LEN] and the write index is - // `h * CONTEXT_LEN + j` with `j < seq_len`. A `seq_len` above - // CONTEXT_LEN therefore runs off the end of every head's row. + // scores[h * CONTEXT_LEN + j] = (q_h . k_j) * SACRED_SCALE * gain^2 for + // j <= position, MASK_SCORE for j > position (causal), j < seq_len + fn compute_scores(q: []const f64, position: usize, seq_len: usize, cache_k: []const f64, scores: []f64) -> void { var bounded_len : usize = seq_len; if (bounded_len > CONTEXT_LEN) { bounded_len = CONTEXT_LEN; } var h : usize = 0; - while (h < NUM_HEADS) { const head_offset = h * HEAD_DIM; var j : usize = 0; - while (j < bounded_len) { - // Skip if j > position (causal mask) if (j > position) { - buffers.scores[h * CONTEXT_LEN + j] = 0.0; - j = j + 1; - continue; - } - - // Compute dot product: Q_head · K_head[j] - var score : f64 = 0.0; - var d : usize = 0; - - while (d < HEAD_DIM) { - const q_val = buffers.q_buffer[head_offset + d]; - const k_val = cache_k[j * EMBED_DIM + head_offset + d]; - score = score + q_val * k_val; - d = d + 1; + scores[h * CONTEXT_LEN + j] = MASK_SCORE; + } else { + var dot : f64 = 0.0; + var d : usize = 0; + while (d < HEAD_DIM) { + dot = dot + q[head_offset + d] * cache_k[j * EMBED_DIM + head_offset + d]; + d = d + 1; + } + scores[h * CONTEXT_LEN + j] = dot * SACRED_SCALE * qk_gain * qk_gain; } - - // Apply sacred scale - buffers.scores[h * CONTEXT_LEN + j] = score * SACRED_SCALE; j = j + 1; } - h = h + 1; } } - // ═════════════════════════════════════════════════════════════════ - // 10. Softmax - // ═════════════════════════════════════════════════════════════════════════ - - // apply_softmax(buffers, seq_len) → void - // Apply softmax to attention scores for each head - // softmax(x) = exp(x - max) / Σ exp(x - max) - fn apply_softmax(buffers: *AttentionBuffers, seq_len: usize) -> void { + // Softmax of each head's first seq_len scores, in place: + // exp(s - max) / sum exp(s - max) + fn apply_softmax(scores: []f64, seq_len: usize) -> void { + var bounded_len : usize = seq_len; + if (bounded_len > CONTEXT_LEN) { + bounded_len = CONTEXT_LEN; + } var h : usize = 0; - while (h < NUM_HEADS) { - // Find max - var max_score : f64 = -1.0e30; - var j : usize = 0; - - while (j < seq_len) { - const s = buffers.scores[h * CONTEXT_LEN + j]; - if (s > max_score) { - max_score = s; + const row = h * CONTEXT_LEN; + var max_score : f64 = scores[row]; + var j : usize = 1; + while (j < bounded_len) { + if (scores[row + j] > max_score) { + max_score = scores[row + j]; } j = j + 1; } - - // Compute exp and sum var sum_exp : f64 = 0.0; j = 0; - - while (j < seq_len) { - const s = exp(buffers.scores[h * CONTEXT_LEN + j] - max_score); - buffers.scores[h * CONTEXT_LEN + j] = s; - sum_exp = sum_exp + s; + while (j < bounded_len) { + scores[row + j] = exp(scores[row + j] - max_score); + sum_exp = sum_exp + scores[row + j]; j = j + 1; } - - // Normalize j = 0; - while (j < seq_len) { - buffers.scores[h * CONTEXT_LEN + j] = - buffers.scores[h * CONTEXT_LEN + j] / sum_exp; + while (j < bounded_len) { + scores[row + j] = scores[row + j] / sum_exp; j = j + 1; } - h = h + 1; } } - // ═════════════════════════════════════════════════════════════════ - // 11. Weighted Value Sum - // ═════════════════════════════════════════════════════════════════════════ - - // weighted_values(buffers, seq_len, cache_v) → void - // Compute weighted sum of values: output = Σ attention[j] * V[j] - fn weighted_values( - buffers: *AttentionBuffers, - seq_len: usize, - cache_v: []f64, - ) -> void { + // concat[h * HEAD_DIM + d] = sum_j weight[h][j] * v_j[h * HEAD_DIM + d] + fn weighted_values(scores: []const f64, seq_len: usize, cache_v: []const f64, concat: []f64) -> void { + var bounded_len : usize = seq_len; + if (bounded_len > CONTEXT_LEN) { + bounded_len = CONTEXT_LEN; + } var h : usize = 0; - while (h < NUM_HEADS) { const head_offset = h * HEAD_DIM; var d : usize = 0; - while (d < HEAD_DIM) { var weighted_sum : f64 = 0.0; var j : usize = 0; - - while (j < seq_len) { - const weight = buffers.scores[h * CONTEXT_LEN + j]; - const v_val = cache_v[j * EMBED_DIM + head_offset + d]; - weighted_sum = weighted_sum + weight * v_val; + while (j < bounded_len) { + weighted_sum = weighted_sum + scores[h * CONTEXT_LEN + j] * cache_v[j * EMBED_DIM + head_offset + d]; j = j + 1; } - - buffers.concat[head_offset + d] = weighted_sum; + concat[head_offset + d] = weighted_sum; d = d + 1; } - h = h + 1; } } - // ═════════════════════════════════════════════════════════════════ - // 12. Output Projection - // ═════════════════════════════════════════════════════════════════════════ + // output = output + input + fn add_residual(output: []f64, input: []const f64) -> void { + var i : usize = 0; + while (i < output.len) { + output[i] = output[i] + input[i]; + i = i + 1; + } + } + + // One position, causal, with a KV cache. q, k, v = input @ Wq, Wk, Wv; + // phi-RoPE on q and k; k and v go into the cache at `position`; per head, + // softmax(q . k_j * scale) over j <= position weights the v_j; + // output = (context @ Wo) + input. A position past the cache leaves the + // output and the caches untouched. + fn sacred_attention_kernel(input: []const f64, w_q: []const Trit, w_k: []const Trit, w_v: []const Trit, w_o: []const Trit, position: usize, seq_len: usize, output: []f64, cache_k: []f64, cache_v: []f64) -> void { + if (position >= CONTEXT_LEN) { + return; + } + var q : [EMBED_DIM]f64 = undefined; + var k : [EMBED_DIM]f64 = undefined; + var v : [EMBED_DIM]f64 = undefined; + var scores : [NUM_HEADS * CONTEXT_LEN]f64 = undefined; + var concat : [EMBED_DIM]f64 = undefined; + fill(&scores, 0.0); + + ternary_matmul(input, w_q, &q, EMBED_DIM, EMBED_DIM); + ternary_matmul(input, w_k, &k, EMBED_DIM, EMBED_DIM); + ternary_matmul(input, w_v, &v, EMBED_DIM, EMBED_DIM); + rope(&q, position, false); + rope(&k, position, false); + cache_kv(&k, &v, position, cache_k, cache_v); + compute_scores(&q, position, seq_len, cache_k, &scores); + apply_softmax(&scores, seq_len); + weighted_values(&scores, seq_len, cache_v, &concat); + ternary_matmul(&concat, w_o, output, EMBED_DIM, EMBED_DIM); + add_residual(output, input); + } - // project_output(buffers, w_o, output) → void - // Apply output projection: output = concat @ W_o - // Using ternary weights - fn project_output( - buffers: *AttentionBuffers, - w_o: []Trit, - output: []f64, - ) -> void { - ternary_matmul(buffers.concat, w_o, output, EMBED_DIM, EMBED_DIM); + // ===================================================================== + // 4. Probes (the tests call these; each sets up what it reads) + // ===================================================================== + + const SENTINEL : f64 = 7.0; + + var p_wq : [EMBED_DIM * EMBED_DIM]Trit = undefined; + var p_wk : [EMBED_DIM * EMBED_DIM]Trit = undefined; + var p_wv : [EMBED_DIM * EMBED_DIM]Trit = undefined; + var p_wo : [EMBED_DIM * EMBED_DIM]Trit = undefined; + var p_ck : [CONTEXT_LEN * EMBED_DIM]f64 = undefined; + var p_cv : [CONTEXT_LEN * EMBED_DIM]f64 = undefined; + var p_in : [EMBED_DIM]f64 = undefined; + var p_out : [EMBED_DIM]f64 = undefined; + var p_vec : [EMBED_DIM]f64 = undefined; + var p_scores : [NUM_HEADS * CONTEXT_LEN]f64 = undefined; + var p_concat : [EMBED_DIM]f64 = undefined; + + // The constants, read through functions so the tests execute at runtime + fn phi_squared() -> f64 { + return PHI * PHI; } - // ═════════════════════════════════════════════════════════════════ - // 13. Residual Connection - // ═════════════════════════════════════════════════════════════════════════ + fn phi_plus_one() -> f64 { + return PHI + 1.0; + } + + fn phi_identity_total() -> f64 { + const phi_sq = PHI * PHI; + return phi_sq + 1.0 / phi_sq; + } + + fn gamma_times_phi_cubed() -> f64 { + return PHI_CUBED_INV * PHI * PHI * PHI; + } + + fn gamma_value() -> f64 { + return SACRED_GAMMA; + } - // add_residual(output, input) → void - // Add residual connection: output = output + input - fn add_residual(output: []f64, input: []f64) -> void { + fn sqrt_five_minus_two() -> f64 { + return sqrt(5.0) - 2.0; + } + + fn scale_from_gamma() -> f64 { + return exp(0.0 - SACRED_GAMMA * log(81.0)); + } + + fn scale_value() -> f64 { + return SACRED_SCALE; + } + + // A deterministic, non-trivial vector element + fn small(i: usize) -> f64 { + return 0.1 * @as(f64, @floatFromInt((i * 7) % 11)) - 0.5; + } + + // w[j * EMBED_DIM + i] = +1 on the diagonal (sign = +1) or -1 (sign = -1), else 0 + fn set_diagonal(w: []Trit, negate: bool) -> void { + var n : usize = 0; + while (n < EMBED_DIM * EMBED_DIM) { + w[n] = Trit.zero; + n = n + 1; + } var i : usize = 0; + while (i < EMBED_DIM) { + if (negate) { + w[i * EMBED_DIM + i] = Trit.neg; + } else { + w[i * EMBED_DIM + i] = Trit.pos; + } + i = i + 1; + } + } - while (i < output.len()) { - output[i] = output[i] + input[i]; + // Identity Wq, Wk, Wv, Wo (or a negated Wo), empty caches, fresh tables + fn identity_setup(negate_o: bool) -> void { + sacred_attention_init(); + set_diagonal(&p_wq, false); + set_diagonal(&p_wk, false); + set_diagonal(&p_wv, false); + set_diagonal(&p_wo, negate_o); + fill(&p_ck, 0.0); + fill(&p_cv, 0.0); + fill(&p_out, SENTINEL); + } + + fn matmul_probe(negate: bool, index: usize) -> f64 { + const input : [3]f64 = [1.0, 2.0, 3.0]; + var weights : [9]Trit = [Trit.pos, Trit.zero, Trit.zero, Trit.zero, Trit.pos, Trit.zero, Trit.zero, Trit.zero, Trit.pos]; + if (negate) { + var i : usize = 0; + while (i < 9) { + weights[i] = Trit.neg; + i = i + 1; + } + } + var output : [3]f64 = [9.0, 9.0, 9.0]; + ternary_matmul(&input, &weights, &output, 3, 3); + return output[index]; + } + + // A 3 x 2 matrix: output[i] = sum_j input[j] w[j * 2 + i] + fn matmul_rect_probe(index: usize) -> f64 { + const input : [3]f64 = [1.0, 2.0, 3.0]; + const weights : [6]Trit = [Trit.pos, Trit.neg, Trit.zero, Trit.pos, Trit.neg, Trit.neg]; + var output : [2]f64 = [0.0, 0.0]; + ternary_matmul(&input, &weights, &output, 3, 2); + return output[index]; + } + + fn residual_probe(index: usize) -> f64 { + var output : [4]f64 = [5.0, 10.0, 15.0, 20.0]; + const input : [4]f64 = [2.0, 4.0, 6.0, 8.0]; + add_residual(&output, &input); + return output[index]; + } + + // Element i of rope(e_k) for a unit vector e_k, with fresh tables + fn rope_unit(position: usize, k: usize, i: usize) -> f64 { + sacred_attention_init(); + fill(&p_vec, 0.0); + p_vec[k] = 1.0; + rope(&p_vec, position, false); + return p_vec[i]; + } + + // |rope(x)|^2 - |x|^2 for a fixed x + fn rope_norm_change(position: usize) -> f64 { + sacred_attention_init(); + var before : f64 = 0.0; + var i : usize = 0; + while (i < EMBED_DIM) { + p_vec[i] = small(i); + before = before + p_vec[i] * p_vec[i]; + i = i + 1; + } + rope(&p_vec, position, false); + var after : f64 = 0.0; + i = 0; + while (i < EMBED_DIM) { + after = after + p_vec[i] * p_vec[i]; + i = i + 1; + } + return after - before; + } + + // rope then its inverse: the largest deviation from the original + fn rope_round_trip_gap(position: usize) -> f64 { + sacred_attention_init(); + var i : usize = 0; + while (i < EMBED_DIM) { + p_vec[i] = small(i); + i = i + 1; + } + rope(&p_vec, position, false); + rope(&p_vec, position, true); + var gap : f64 = 0.0; + i = 0; + while (i < EMBED_DIM) { + gap = gap + @abs(p_vec[i] - small(i)); + i = i + 1; + } + return gap; + } + + // How far x moved under rope at a position past the tables + fn rope_out_of_range_gap() -> f64 { + sacred_attention_init(); + var i : usize = 0; + while (i < EMBED_DIM) { + p_vec[i] = small(i); + i = i + 1; + } + rope(&p_vec, CONTEXT_LEN, false); + var gap : f64 = 0.0; + i = 0; + while (i < EMBED_DIM) { + gap = gap + @abs(p_vec[i] - small(i)); + i = i + 1; + } + return gap; + } + + // The largest |cos^2 + sin^2 - 1| over the whole table, and the entry at (0, 0) + fn table_unit_gap() -> f64 { + sacred_attention_init(); + var worst : f64 = 0.0; + var n : usize = 0; + while (n < CONTEXT_LEN * ROPE_PAIRS) { + const e = @abs(rope_cos[n] * rope_cos[n] + rope_sin[n] * rope_sin[n] - 1.0); + if (e > worst) { + worst = e; + } + n = n + 1; + } + return worst; + } + + fn table_cos_at(position: usize, pair: usize) -> f64 { + sacred_attention_init(); + return rope_cos[position * ROPE_PAIRS + pair]; + } + + fn table_sin_at(position: usize, pair: usize) -> f64 { + sacred_attention_init(); + return rope_sin[position * ROPE_PAIRS + pair]; + } + + // softmax of (1, 2, 3, 4) + offset in head 0's first four slots; all other + // slots stay 0.0, so heads 1 and 2 are softmaxed over four zeros + fn softmax_probe(offset: f64, head: usize, index: usize) -> f64 { + fill(&p_scores, 0.0); + p_scores[0] = 1.0 + offset; + p_scores[1] = 2.0 + offset; + p_scores[2] = 3.0 + offset; + p_scores[3] = 4.0 + offset; + apply_softmax(&p_scores, 4); + return p_scores[head * CONTEXT_LEN + index]; + } + + fn softmax_row_sum(offset: f64, head: usize) -> f64 { + const unused = softmax_probe(offset, head, 0); + return p_scores[head * CONTEXT_LEN] + p_scores[head * CONTEXT_LEN + 1] + p_scores[head * CONTEXT_LEN + 2] + p_scores[head * CONTEXT_LEN + 3] + 0.0 * unused; + } + + // Head 0: q = e_0, k_j = (j + 1) e_0 for j = 0..3. Position 1 sees j = 0, 1. + // Scores, then softmax, over seq_len 4. + fn causal_probe(index: usize) -> f64 { + sacred_attention_init(); + fill(&p_vec, 0.0); + p_vec[0] = 1.0; + fill(&p_ck, 0.0); + var j : usize = 0; + while (j < 4) { + p_ck[j * EMBED_DIM] = @as(f64, @floatFromInt(j + 1)); + j = j + 1; + } + fill(&p_scores, 0.0); + compute_scores(&p_vec, 1, 4, &p_ck, &p_scores); + apply_softmax(&p_scores, 4); + return p_scores[index]; + } + + // Raw scores (before softmax): head 0 has q[0] = 2, k_0[0] = 3; head 2 has + // q[2 * 81 + 5] = 1, k_0[2 * 81 + 5] = 4 + fn score_probe(head: usize, gain: f64) -> f64 { + sacred_attention_init(); + set_qk_gain(gain); + fill(&p_vec, 0.0); + p_vec[0] = 2.0; + p_vec[2 * HEAD_DIM + 5] = 1.0; + fill(&p_ck, 0.0); + p_ck[0] = 3.0; + p_ck[2 * HEAD_DIM + 5] = 4.0; + fill(&p_scores, 0.0); + compute_scores(&p_vec, 0, 1, &p_ck, &p_scores); + set_qk_gain(1.0); + return p_scores[head * CONTEXT_LEN]; + } + + // Weights (0.25, 0.75) on two positions of head 1; v_0 = 4, v_1 = 8 at the + // head's dim 3 -> 0.25 * 4 + 0.75 * 8 = 7 + fn weighted_probe(index: usize) -> f64 { + fill(&p_scores, 0.0); + p_scores[1 * CONTEXT_LEN] = 0.25; + p_scores[1 * CONTEXT_LEN + 1] = 0.75; + fill(&p_cv, 0.0); + p_cv[HEAD_DIM + 3] = 4.0; + p_cv[EMBED_DIM + HEAD_DIM + 3] = 8.0; + fill(&p_concat, SENTINEL); + weighted_values(&p_scores, 2, &p_cv, &p_concat); + return p_concat[index]; + } + + // cache_kv at a position stores k and v at that row only + fn cache_probe(which: u8, position: usize, index: usize) -> f64 { + fill(&p_ck, 0.0); + fill(&p_cv, 0.0); + var i : usize = 0; + while (i < EMBED_DIM) { + p_vec[i] = @as(f64, @floatFromInt(i + 1)); + p_in[i] = 100.0 + @as(f64, @floatFromInt(i)); + i = i + 1; + } + cache_kv(&p_vec, &p_in, 2, &p_ck, &p_cv); + if (which == 0) { + return p_ck[position * EMBED_DIM + index]; + } + return p_cv[position * EMBED_DIM + index]; + } + + // A position past the cache writes nothing and does not run off the end + fn cache_out_of_range_sum() -> f64 { + fill(&p_ck, 0.0); + fill(&p_cv, 0.0); + fill(&p_vec, 1.0); + cache_kv(&p_vec, &p_vec, CONTEXT_LEN, &p_ck, &p_cv); + var total : f64 = 0.0; + var n : usize = 0; + while (n < CONTEXT_LEN * EMBED_DIM) { + total = total + p_ck[n] + p_cv[n]; + n = n + 1; + } + return total; + } + + // Identity weights, position 0, one token: softmax over one position is 1, + // context = v_0 = x, output = x + x. Returns sum |out - 2x|. + fn kernel_one_position_gap() -> f64 { + identity_setup(false); + var i : usize = 0; + while (i < EMBED_DIM) { + p_in[i] = small(i); + i = i + 1; + } + sacred_attention_kernel(&p_in, &p_wq, &p_wk, &p_wv, &p_wo, 0, 1, &p_out, &p_ck, &p_cv); + var gap : f64 = 0.0; + i = 0; + while (i < EMBED_DIM) { + gap = gap + @abs(p_out[i] - 2.0 * small(i)); + i = i + 1; + } + return gap; + } + + // The same with Wo = -identity: output = x - context = 0 + fn kernel_negated_output_total() -> f64 { + identity_setup(true); + var i : usize = 0; + while (i < EMBED_DIM) { + p_in[i] = small(i); + i = i + 1; + } + sacred_attention_kernel(&p_in, &p_wq, &p_wk, &p_wv, &p_wo, 0, 1, &p_out, &p_ck, &p_cv); + var total : f64 = 0.0; + i = 0; + while (i < EMBED_DIM) { + total = total + @abs(p_out[i]); i = i + 1; } + return total; + } + + // Two tokens, identity weights. x0 = 2 e_0 at position 0, x1 = 1.5 e_0 at + // position 1 (rope angle 1 rad on the pair (0, 40)). Returns output[index] + // of position 1. + fn kernel_two_position(index: usize) -> f64 { + identity_setup(false); + fill(&p_in, 0.0); + p_in[0] = 2.0; + sacred_attention_kernel(&p_in, &p_wq, &p_wk, &p_wv, &p_wo, 0, 1, &p_out, &p_ck, &p_cv); + fill(&p_in, 0.0); + p_in[0] = 1.5; + sacred_attention_kernel(&p_in, &p_wq, &p_wk, &p_wv, &p_wo, 1, 2, &p_out, &p_ck, &p_cv); + return p_out[index]; + } + + // Closed form of kernel_two_position(0): s0 = 1.5 cos(1) 2 S, s1 = 2.25 S, + // w1 = 1 / (1 + exp(s0 - s1)), out = (1 - w1) 2 + w1 1.5 + 1.5 + fn two_position_expected() -> f64 { + const s0 = 1.5 * cos(1.0) * 2.0 * SACRED_SCALE; + const s1 = 2.25 * SACRED_SCALE; + const w1 = 1.0 / (1.0 + exp(s0 - s1)); + return (1.0 - w1) * 2.0 + w1 * 1.5 + 1.5; } - // ═══════════════════════════════════════════════════════════════════════════════════════════════════════ + // Position 0 with garbage in the cache rows 1 and 2: asking for seq_len 3 + // must give what seq_len 1 gives. Returns sum |difference|. + fn kernel_future_gap() -> f64 { + identity_setup(false); + var i : usize = 0; + while (i < EMBED_DIM) { + p_in[i] = small(i); + i = i + 1; + } + sacred_attention_kernel(&p_in, &p_wq, &p_wk, &p_wv, &p_wo, 0, 1, &p_out, &p_ck, &p_cv); + fill(&p_vec, 0.0); + i = 0; + while (i < EMBED_DIM) { + p_vec[i] = p_out[i]; + i = i + 1; + } + identity_setup(false); + i = EMBED_DIM; + while (i < 3 * EMBED_DIM) { + p_ck[i] = 1000.0 + @as(f64, @floatFromInt(i)); + p_cv[i] = 0.0 - 500.0 - @as(f64, @floatFromInt(i)); + i = i + 1; + } + i = 0; + while (i < EMBED_DIM) { + p_in[i] = small(i); + i = i + 1; + } + sacred_attention_kernel(&p_in, &p_wq, &p_wk, &p_wv, &p_wo, 0, 3, &p_out, &p_ck, &p_cv); + var gap : f64 = 0.0; + i = 0; + while (i < EMBED_DIM) { + gap = gap + @abs(p_out[i] - p_vec[i]); + i = i + 1; + } + return gap; + } + + // A position past the cache: the output keeps its sentinel + fn kernel_out_of_range_gap() -> f64 { + identity_setup(false); + var i : usize = 0; + while (i < EMBED_DIM) { + p_in[i] = small(i); + i = i + 1; + } + sacred_attention_kernel(&p_in, &p_wq, &p_wk, &p_wv, &p_wo, CONTEXT_LEN, 1, &p_out, &p_ck, &p_cv); + var gap : f64 = 0.0; + i = 0; + while (i < EMBED_DIM) { + gap = gap + @abs(p_out[i] - SENTINEL); + i = i + 1; + } + return gap; + } + + // Head 1 and head 2 of a 2-position kernel run stay at their residual: + // x has only dim 0 (head 0), so v is zero outside head 0 + fn kernel_other_heads_total() -> f64 { + const unused = kernel_two_position(0); + var total : f64 = 0.0; + var i : usize = HEAD_DIM; + while (i < EMBED_DIM) { + total = total + @abs(p_out[i]); + i = i + 1; + } + return total + 0.0 * unused; + } + + // ================================================================= // TDD-Inside-Spec: Tests and Invariants for SacredAttention - // ═══════════════════════════════════════════════════════════════════════════════════════════════════════ + // ================================================================= - test attn_sacred_scaling_constant - given scale = SACRED_SCALE - and expected = pow(81.0, -0.2360679) - then abs(scale - expected) < 0.001 + // -- Constants -- - test attn_sacred_gamma_is_phi_cubed_inv - given gamma = SACRED_GAMMA - and phi_inv_cubed = pow(constants::PHI_INV, 3.0) - then abs(gamma - phi_inv_cubed) < 0.00001 + test attn_phi_squared_is_phi_plus_one + given lhs = phi_squared() + when rhs = phi_plus_one() + then @abs(lhs - rhs) < 0.000000000001 - test attn_num_heads_is_trinity - given heads = NUM_HEADS - then heads == 3 + test attn_phi_squared_plus_inverse_is_three + given total = phi_identity_total() + then @abs(total - 3.0) < 0.000000000001 - test attn_head_dim_is_three_pow_four - given dim = HEAD_DIM - then dim == 81 // 3^4 + test attn_gamma_is_phi_cubed_inverse + given product = gamma_times_phi_cubed() + when closed_form = sqrt_five_minus_two() + then @abs(product - 1.0) < 0.000000000001 and @abs(gamma_value() - closed_form) < 0.000000000001 - test attn_embed_dim_is_heads_times_head_dim - given embed = EMBED_DIM - and computed = NUM_HEADS * HEAD_DIM - then embed == computed + test attn_sacred_scale_is_81_to_minus_gamma + given expected = scale_from_gamma() + when actual = scale_value() + then @abs(actual - expected) < 0.000000000001 - test attn_rope_pairs_is_context_len_div_two - given pairs = ROPE_PAIRS - and computed = CONTEXT_LEN / 2 - then pairs == computed + // -- Ternary matmul -- test attn_ternary_matmul_identity - given input = [1.0, 2.0, 3.0, 4.0] - and weights = [Trit.pos, Trit.zero, Trit.zero, Trit.zero, - Trit.zero, Trit.pos, Trit.zero, Trit.zero, - Trit.zero, Trit.zero, Trit.pos, Trit.zero, - Trit.zero, Trit.zero, Trit.zero, Trit.pos] - and output = [0.0; 4] - when ternary_matmul(input, weights, output, 4, 4) - then output[0] == 1.0 and output[1] == 2.0 and output[2] == 3.0 and output[3] == 4.0 + given a = matmul_probe(false, 0) + when c = matmul_probe(false, 2) + then a == 1.0 and matmul_probe(false, 1) == 2.0 and c == 3.0 test attn_ternary_matmul_negation - given input = [1.0, 2.0, 3.0, 4.0] - and weights = [Trit.neg, Trit.neg, Trit.neg, Trit.neg, - Trit.neg, Trit.neg, Trit.neg, Trit.neg, - Trit.neg, Trit.neg, Trit.neg, Trit.neg, - Trit.neg, Trit.neg, Trit.neg, Trit.neg] - and output = [0.0; 4] - when ternary_matmul(input, weights, output, 4, 4) - then output[0] == -10.0 and output[1] == -10.0 and output[2] == -10.0 and output[3] == -10.0 - - test attn_add_residual_identity - given output = [5.0, 10.0, 15.0, 20.0] - and input = [2.0, 4.0, 6.0, 8.0] - when add_residual(output, input) - then output[0] == 7.0 and output[1] == 14.0 and output[2] == 21.0 and output[3] == 28.0 - - test attn_softmax_normalization - given scores = [1.0, 2.0, 3.0, 4.0] - and buffers = AttentionBuffers{...} - when buffers.scores[0..4] = scores - and apply_softmax(&buffers, 4) - and sum = buffers.scores[0] + buffers.scores[1] + buffers.scores[2] + buffers.scores[3] - then abs(sum - 1.0) < 0.0001 - - test attn_softmax_positive - given scores = [1.0, -1.0, 2.0, -2.0] - and buffers = AttentionBuffers{...} - when buffers.scores[0..4] = scores - and apply_softmax(&buffers, 4) - and all_positive = (buffers.scores[0] >= 0.0) and - (buffers.scores[1] >= 0.0) and - (buffers.scores[2] >= 0.0) and - (buffers.scores[3] >= 0.0) - then all_positive == true - - test attn_sacred_scale_range - given scale = SACRED_SCALE - then scale > 0.3 and scale < 0.4 - - test attn_rope_tables_initialized - given tables = rope_tables - and sacred_attention_init() - then tables.cos[0] > 0.0 and tables.cos.len() == CONTEXT_LEN * ROPE_PAIRS - - test attn_cache_kv_stores_values - given buffers = AttentionBuffers{...} - and cache_k = [0.0; EMBED_DIM * CONTEXT_LEN] - and cache_v = [0.0; EMBED_DIM * CONTEXT_LEN] - and buffers.k_buffer = [1.0, 2.0, 3.0] - and buffers.v_buffer = [4.0, 5.0, 6.0] - when cache_kv(&buffers, 0, cache_k, cache_v) - then cache_k[0] == 1.0 and cache_k[1] == 2.0 and cache_v[0] == 4.0 and cache_v[1] == 5.0 - - test attn_compute_scores_applies_scale - given buffers = AttentionBuffers{...} - and cache_k = [0.0; EMBED_DIM * CONTEXT_LEN] - and buffers.q_buffer = [1.0, 1.0, 1.0] - and buffers.k_buffer = [1.0, 1.0, 1.0] - and sacred_attention_init() - when cache_kv(&buffers, 0, cache_k, [0.0; EMBED_DIM * CONTEXT_LEN]) - and compute_scores(&buffers, 0, 1, cache_k) - then buffers.scores[0] == 3.0 * SACRED_SCALE - - invariant attn_sacred_gamma_positive - assert SACRED_GAMMA > 0.0 - - invariant attn_sacred_gamma_less_than_one - assert SACRED_GAMMA < 1.0 - - invariant attn_sacred_scale_positive - assert SACRED_SCALE > 0.0 - - invariant attn_sacred_scale_reasonable - assert SACRED_SCALE > 0.3 and SACRED_SCALE < 0.4 - - invariant attn_num_heads_constant - assert NUM_HEADS == 3 - - invariant attn_head_dim_constant - assert HEAD_DIM == 81 - - invariant attn_embed_dim_constant - assert EMBED_DIM == 243 - - invariant attn_context_len_constant - assert CONTEXT_LEN == 81 - - invariant attn_rope_pairs_constant - assert ROPE_PAIRS == 40 - - invariant attn_embed_dim_equals_heads_times_head_dim + given a = matmul_probe(true, 0) + then a == -6.0 and matmul_probe(true, 2) == -6.0 + + // column 0: 1 - 3 = -2 (w = +1, 0, -1); column 1: -1 + 2 - 3 = -2 + test attn_ternary_matmul_row_major_layout + given c0 = matmul_rect_probe(0) + when c1 = matmul_rect_probe(1) + then c0 == -2.0 and c1 == -2.0 + + test attn_add_residual_adds_elementwise + given a = residual_probe(0) + when d = residual_probe(3) + then a == 7.0 and residual_probe(1) == 14.0 and residual_probe(2) == 21.0 and d == 28.0 + + // -- phi-RoPE -- + + test attn_rope_is_identity_at_position_zero + given same = rope_unit(0, 10, 10) + when other = rope_unit(0, 10, 50) + then same == 1.0 and other == 0.0 + + // Pair (10, 50) at position 3: angle 3 phi^(-20/81); dims 80, 161 are unrotated + test attn_rope_rotates_pair_i_with_i_plus_40 + given c = rope_unit(3, 10, 10) + when s = rope_unit(3, 10, 50) + then @abs(c + 0.8880621352130498) < 0.000000000001 and @abs(s - 0.4597234429533031) < 0.000000000001 and rope_unit(3, 80, 80) == 1.0 and rope_unit(3, 161, 161) == 1.0 + + // Head 1 rotates the same pair indices inside its own 81 dims + test attn_rope_rotates_every_head + given head0 = rope_unit(3, 10, 50) + when head1 = rope_unit(3, 81 + 10, 81 + 50) + then @abs(head0 - head1) < 0.000000000001 and rope_unit(3, 81 + 10, 50) == 0.0 + + test attn_rope_preserves_norm_and_inverts + given change = rope_norm_change(19) + when gap = rope_round_trip_gap(19) + then @abs(change) < 0.000000001 and gap < 0.000000001 + + test attn_rope_table_entries_are_unit_circle + given worst = table_unit_gap() + then worst < 0.000000000001 + + // theta_0 = 1: the first pair turns 1 rad per position; pair 39 turns slowest + test attn_rope_table_frequencies + given c1 = table_cos_at(1, 0) + when s2 = table_sin_at(2, 0) + then @abs(c1 - cos(1.0)) < 0.000000000001 and @abs(s2 - sin(2.0)) < 0.000000000001 and table_cos_at(0, 39) == 1.0 + + test attn_rope_past_the_tables_changes_nothing + given gap = rope_out_of_range_gap() + then gap == 0.0 + + // -- Cache -- + + test attn_cache_kv_stores_at_the_position_row + given k = cache_probe(0, 2, 5) + when v = cache_probe(1, 2, 5) + then k == 6.0 and v == 105.0 and cache_probe(0, 1, 5) == 0.0 and cache_probe(1, 3, 5) == 0.0 + + test attn_cache_kv_past_the_end_writes_nothing + given total = cache_out_of_range_sum() + then total == 0.0 + + // -- Scores, mask, softmax -- + + // Head 0: (2 e_0 . 3 e_0) S = 6 S; head 2 reads its own slice: 1 * 4 * S + test attn_scores_are_scaled_dot_products_per_head + given s0 = score_probe(0, 1.0) + when s2 = score_probe(2, 1.0) + then @abs(s0 - 6.0 * SACRED_SCALE) < 0.000000000001 and @abs(s2 - 4.0 * SACRED_SCALE) < 0.000000000001 and score_probe(1, 1.0) == 0.0 + + // Q and K both carry the gain: the score picks up gain^2 + test attn_qk_gain_scales_scores_by_gain_squared + given base = score_probe(0, 1.0) + when scaled = score_probe(0, GAIN_PHI_SQ) + then @abs(scaled / base - GAIN_PHI_SQ * GAIN_PHI_SQ) < 0.000000000001 + + test attn_softmax_row_sums_to_one + given h0 = softmax_row_sum(0.0, 0) + when h2 = softmax_row_sum(0.0, 2) + then @abs(h0 - 1.0) < 0.000000000001 and @abs(h2 - 1.0) < 0.000000000001 + + // softmax(1, 2, 3, 4)[3] = 1 / (1 + e^-1 + e^-2 + e^-3); e^-1 apart in order + test attn_softmax_values + given top = softmax_probe(0.0, 0, 3) + when ratio = softmax_probe(0.0, 0, 0) / softmax_probe(0.0, 0, 1) + then @abs(top - 1.0 / (1.0 + exp(-1.0) + exp(-2.0) + exp(-3.0))) < 0.000000000001 and @abs(ratio - exp(-1.0)) < 0.000000000001 + + test attn_softmax_of_equal_scores_is_uniform + given w = softmax_probe(0.0, 1, 2) + then @abs(w - 0.25) < 0.000000000001 + + // exp(1004) overflows; subtracting the max keeps it finite and the same + test attn_softmax_is_shift_invariant_and_stable + given plain = softmax_probe(0.0, 0, 3) + when shifted = softmax_probe(1000.0, 0, 3) + then @abs(plain - shifted) < 0.000000000001 and shifted > 0.6 and shifted < 0.7 + + // Position 1 sees keys 0 and 1 (scores S and 2 S); positions 2 and 3 are masked + test attn_causal_mask_gives_future_zero_weight + given w2 = causal_probe(2) + when w3 = causal_probe(3) + then w2 == 0.0 and w3 == 0.0 + + test attn_causal_mask_leaves_a_distribution_on_the_past + given w0 = causal_probe(0) + when w1 = causal_probe(1) + then @abs(w0 + w1 - 1.0) < 0.000000000001 and @abs(w1 / w0 - exp(SACRED_SCALE)) < 0.000000000001 + + // -- Weighted values -- + + test attn_weighted_values_mix_values_by_weight + given mixed = weighted_probe(HEAD_DIM + 3) + when other_head = weighted_probe(3) + then @abs(mixed - 7.0) < 0.000000000001 and other_head == 0.0 and weighted_probe(HEAD_DIM + 4) == 0.0 + + // -- Kernel -- + + // Identity weights, one token: context = v_0 = x, output = x + x + test attn_kernel_identity_one_position + given gap = kernel_one_position_gap() + then gap < 0.000000000001 + + // Wo = -identity: output = x - context = 0, so Wo is applied + test attn_kernel_applies_output_projection + given total = kernel_negated_output_total() + then total < 0.000000000001 + + // Two tokens by hand: weights from scores 3 cos(1) S and 2.25 S, values unrotated + test attn_kernel_two_positions_match_closed_form + given out = kernel_two_position(0) + when expected = two_position_expected() + then @abs(out - expected) < 0.000000001 and @abs(kernel_two_position(40)) < 0.000000000001 + + // V is not rotated and x has only dim 0, so every other head stays zero + test attn_kernel_leaves_other_heads_alone + given total = kernel_other_heads_total() + then total < 0.000000000001 + + // seq_len 3 at position 0 with a poisoned future must equal seq_len 1 + test attn_kernel_does_not_read_the_future + given gap = kernel_future_gap() + then gap < 0.000000000001 + + test attn_kernel_past_the_cache_does_nothing + given gap = kernel_out_of_range_gap() + then gap == 0.0 + + // -- QK-gain ablation (Phase B2) -- + + test attn_gain_variants + given phi_sq = get_qk_gain(QK_PHI_SQUARED) + when standard = get_qk_gain(QK_STANDARD) + then @abs(phi_sq - (PHI + 1.0)) < 0.000000000001 and standard == 1.0 and get_qk_gain(QK_LEARNED) == 1.0 and @abs(get_qk_gain(QK_SQRT_PHI) - sqrt(PHI)) < 0.000000000001 and get_qk_gain(99) == 1.0 + + // 1 / sqrt(96), and phi^4 / sqrt(96) = 0.6995 + test attn_effective_score_scale + given standard = effective_score_scale(GAIN_STANDARD, 96.0) + when phi_sq = effective_score_scale(GAIN_PHI_SQ, 96.0) + then @abs(standard - 1.0 / sqrt(96.0)) < 0.000000000001 and @abs(phi_sq * sqrt(96.0) - PHI * PHI * PHI * PHI) < 0.000000001 and phi_sq > 0.69 and phi_sq < 0.71 + + test attn_phi_squared_gain_scales_more_than_standard + given a = effective_score_scale(GAIN_PHI_SQ, 96.0) + when b = effective_score_scale(GAIN_STANDARD, 96.0) + then a > b and a / b > 6.8 and a / b < 6.9 + + // -- Invariants -- + + invariant attn_embed_dim_is_heads_times_head_dim assert EMBED_DIM == NUM_HEADS * HEAD_DIM - invariant attn_rope_pairs_is_half_context_len - assert ROPE_PAIRS == CONTEXT_LEN / 2 - - invariant attn_ternary_matmul_output_dim - given input = [0.0; 10] - and weights = [Trit.zero; 100] - and output = [0.0; 10] - and ternary_matmul(input, weights, output, 10, 10) - assert output.len() == 10 - - invariant attn_add_residual_preserves_dim - given output = [0.0; 100] - and input = [0.0; 100] - and add_residual(output, input) - assert output.len() == 100 - - invariant attn_softmax_output_probability_distribution - given buffers = AttentionBuffers{...} - and buffers.scores = [1.0, 2.0, 3.0, 4.0] - and apply_softmax(&buffers, 4) - and sum = buffers.scores[0] + buffers.scores[1] + buffers.scores[2] + buffers.scores[3] - and all_non_neg = (buffers.scores[0] >= 0.0) and - (buffers.scores[1] >= 0.0) and - (buffers.scores[2] >= 0.0) and - (buffers.scores[3] >= 0.0) - assert abs(sum - 1.0) < 0.001 and all_non_neg - - invariant attn_rope_cos_in_valid_range - given tables = rope_tables - and sacred_attention_init() - and idx = tables.cos.len() / 2 - then assert tables.cos[idx] >= -1.0 and tables.cos[idx] <= 1.0 - - invariant attn_rope_sin_in_valid_range - given tables = rope_tables - and sacred_attention_init() - and idx = tables.sin.len() / 2 - then assert tables.sin[idx] >= -1.0 and tables.sin[idx] <= 1.0 - - bench attn_ternary_matmul_latency - measure: nanoseconds to ternary_matmul([1.0; 243], [Trit.pos; 243*243], [0.0; 243], 243, 243) - target: < 5000ns - - bench attn_apply_rope_latency - measure: nanoseconds to apply_rope_qk(&buffers, 40) - target: < 2000ns - - bench attn_softmax_latency - measure: nanoseconds to apply_softmax(&buffers, 81) - target: < 3000ns - - bench attn_compute_scores_latency - measure: nanoseconds to compute_scores(&buffers, 40, 41, cache_k) - target: < 10000ns - - bench attn_weighted_values_latency - measure: nanoseconds to weighted_values(&buffers, 41, cache_v) - target: < 8000ns - - bench attn_sacred_attention_kernel_latency - measure: nanoseconds for sacred_attention_kernel on single position - target: < 30000ns -} + invariant attn_head_dim_is_three_pow_four + assert HEAD_DIM == 3 * 3 * 3 * 3 -// ===================================================================== -// Phase B2 (epic #181) -- QK-Gain control ablation (appended, separate module) -// gain=phi^2 vs gain=1.0 vs learned. phi^2 [Open conjecture]; phi^2=phi+1 [Verified]. -// ===================================================================== + invariant attn_rope_pairs_leave_one_dim + assert 2 * ROPE_PAIRS + 1 == HEAD_DIM -module AttentionQKGainAblation; - use base::types; - use math::constants; - use numeric::gf16; - use nn::attention; + invariant attn_context_equals_head_dim + assert CONTEXT_LEN == HEAD_DIM - // ========================================================= - // 1. Constants - // ========================================================= - - const PHI : gf16::GF16 = 1.618033988749895; - const PHI_SQ : gf16::GF16 = 2.618033988749895; // phi^2 = phi + 1; [Verified arithmetic] - const PHI_SQ_INV : gf16::GF16 = 0.381966011250105; // phi^(-2); [Verified arithmetic] - - // B2 gain variants - const GAIN_PHI_SQ : gf16::GF16 = PHI_SQ; // phi^2 ~ 2.618 [Open conjecture] - const GAIN_STANDARD : gf16::GF16 = 1.0; // Standard (no extra gain) - const GAIN_SQRT_PHI : gf16::GF16 = 1.272019649514069; // sqrt(phi) ~ 1.272 [Open conjecture] - const GAIN_LEARNED_INIT : gf16::GF16 = 1.0; // Learned gain initialized at 1.0 - - // Attention scaling (kept separate from QK-Gain; standard 1/sqrt(d_k)) - // Sacred scaling from attention.t27: SACRED_SCALE = 81^(-PHI^(-3)) ~ 0.354 - // These are combined: effective_scale = SACRED_SCALE * qk_gain^2 - // (qk_gain is applied to Q and K before dot product -- doubles in the score) - - // ========================================================= - // 2. Types - // ========================================================= - - pub const QKGainVariant = enum { - PhiSquared, // gain = phi^2 ~ 2.618 [Open conjecture] - Standard, // gain = 1.0 (baseline) - Learned, // gain starts at 1.0, optimized by AdamW - SqrtPhi, // gain = sqrt(phi) ~ 1.272 [Open conjecture] - }; - - pub const QKGainConfig = struct { - variant : QKGainVariant, - head_dim : u32, - initial_gain : gf16::GF16, - learnable : bool, // If true, gain is a trained scalar - lr_gain : gf16::GF16, // LR for gain parameter (if learnable) - }; - - pub const QKGainResult = struct { - gain_value : gf16::GF16, // Effective gain applied - score_scale : gf16::GF16, // Combined score scale (gain^2 / sqrt(head_dim)) - }; - - // ========================================================= - // 3. Core Functions - // ========================================================= - - // get_qk_gain(config: QKGainConfig) -> gf16::GF16 - // Returns the effective QK gain scalar for the given variant. - fn get_qk_gain(config: QKGainConfig) -> gf16::GF16 { - // PhiSquared: return GAIN_PHI_SQ - // Standard: return GAIN_STANDARD - // Learned: return config.initial_gain (will be trained) - // SqrtPhi: return GAIN_SQRT_PHI - } - - // effective_score_scale(gain: gf16::GF16, head_dim: u32) -> gf16::GF16 - // Computes the combined score scale = gain^2 / sqrt(head_dim). - // Standard formula uses gain=1: scale = 1/sqrt(head_dim). - // phi^2 formula: scale = phi^4 / sqrt(head_dim). - // Note: igla-peek applies gain to both Q and K, so dot product - // picks up gain^2 vs the standard 1 factor. - fn effective_score_scale(gain: gf16::GF16, head_dim: u32) -> gf16::GF16 { - // return gain * gain / sqrt(head_dim as gf16::GF16) - } - - // ========================================================= - // PHASE B2: Constant-identity tests - // ========================================================= - - // B2-CONST-1: phi^2 = phi + 1 -- [Verified] (L5 corollary) - test b2_phi_sq_equals_phi_plus_one - given phi = 1.618033988749895 - when lhs = phi * phi - and rhs = phi + 1.0 - then approximately_equal(lhs, rhs) // tolerance 1e-12 - - // B2-CONST-2: GAIN_PHI_SQ matches igla-peek PHI_SQ - test b2_gain_phi_sq_matches_trainer_constant - given expected = 1.618033988749895 + 1.0 // phi + 1 = phi^2 - when val = GAIN_PHI_SQ - then approximately_equal(val, expected) // tolerance 1e-9 - - // B2-CONST-3: phi^2 + phi^(-2) = 3 -- [Verified] (Law L5) - test b2_trinity_identity_l5 - given phi = 1.618033988749895 - when lhs = phi * phi + 1.0 / (phi * phi) - then approximately_equal(lhs, 3.0) // tolerance 1e-12 - // [Verified]: the ONLY phi-fact that is Verified in this codebase. - - // B2-CONST-4: Standard gain is distinct from phi^2 - test b2_standard_gain_distinct_from_phi_sq - then GAIN_PHI_SQ != GAIN_STANDARD - and GAIN_PHI_SQ > 2.0 - and GAIN_PHI_SQ < 3.0 - - // B2-CONST-5: sqrt(phi) is in valid range - test b2_sqrt_phi_in_range - given phi = 1.618033988749895 - when expected = sqrt(phi) - then approximately_equal(GAIN_SQRT_PHI, expected) // tolerance 1e-9 - - // ========================================================= - // PHASE B2: Control-test design (QK-Gain ablation) - // - // FALSIFICATION CRITERION: - // If gain=1.0 (standard) or learned gain reaches BPB within - // Monte-Carlo error of gain=phi^2 on equal budget, phi-specificity - // of the QK-gain design is FALSIFIED. - // - // Experimental protocol: - // - Metric: BPB on held-out validation set - // - Budget: equal gradient steps; equal HP tuning for lr_gain - // - Baseline: standard attention (Vaswani 2017, 1/sqrt(d_k)) - // - Three cells: (a) phi^2, (b) 1.0, (c) learned - // - Optional fourth cell: sqrt(phi) to test sqrt-phi hypothesis - // - All cells use identical architecture; only gain differs - // - muP QK scaling (Yang 2022, 2203.03466) is phi-independent: - // use standard 1/sqrt(d_k) after muP transfer (see B3) - // ========================================================= - - // B2a: phi^2 gain [Open conjecture] - test b2_variant_a_phi_sq_config - given config = QKGainConfig{ - .variant = QKGainVariant.PhiSquared, - .head_dim = 96, - .initial_gain = GAIN_PHI_SQ, - .learnable = false, - .lr_gain = 0.0 - } - when gain = get_qk_gain(config) - then approximately_equal(gain, PHI_SQ) // ~ 2.618 - - // B2b: standard gain = 1.0 (baseline; Vaswani 2017) - test b2_variant_b_standard_config - given config = QKGainConfig{ - .variant = QKGainVariant.Standard, - .head_dim = 96, - .initial_gain = GAIN_STANDARD, - .learnable = false, - .lr_gain = 0.0 - } - when gain = get_qk_gain(config) - then approximately_equal(gain, 1.0) - - // B2c: learned gain (starts at 1.0, optimized jointly with model) - // Represents: "let the data decide the gain" - test b2_variant_c_learned_init - given config = QKGainConfig{ - .variant = QKGainVariant.Learned, - .head_dim = 96, - .initial_gain = GAIN_LEARNED_INIT, - .learnable = true, - .lr_gain = 1e-3 - } - when gain_init = get_qk_gain(config) - then approximately_equal(gain_init, 1.0) // starts at 1.0 - // after training, gain may converge toward phi^2 or elsewhere -- - // that outcome would be informative but is not asserted here - - // B2d: Score scale is correctly computed per variant - test b2_score_scale_phi_sq - given gain = GAIN_PHI_SQ - and head_dim = 96 - when scale = effective_score_scale(gain, head_dim) - // phi^4 / sqrt(96) ~ 6.854 / 9.798 ~ 0.7 - then scale > 0.5 and scale < 1.5 - - test b2_score_scale_standard - given gain = GAIN_STANDARD - and head_dim = 96 - when scale = effective_score_scale(gain, head_dim) - // 1 / sqrt(96) ~ 0.102 - then approximately_equal(scale, 1.0 / sqrt(96.0)) // tolerance 1e-6 - - // B2e: Ablation scaffold produces finite BPB for all variants - test b2_control_ablation_all_variants_finite - given n_steps = 500 // mini-run for CI; full run uses 81000 - and seed = 43 - and bpb_a = run_attention_with_gain(QKGainVariant.PhiSquared, n_steps, seed) - and bpb_b = run_attention_with_gain(QKGainVariant.Standard, n_steps, seed) - and bpb_c = run_attention_with_gain(QKGainVariant.Learned, n_steps, seed) - then all_finite([bpb_a, bpb_b, bpb_c]) - and all_positive([bpb_a, bpb_b, bpb_c]) - // NOT asserting bpb_a < bpb_b or bpb_a < bpb_c. - // phi-specificity is FALSIFIED if any non-phi variant - // matches variant (a) within Monte-Carlo error. - - // ========================================================= - // PHASE B2: Invariants - // ========================================================= - - // B2-INV-1: phi^2 gain is in (1, 4) -- plausible range for a score amplifier - invariant b2_phi_sq_gain_valid_range - then GAIN_PHI_SQ > 1.0 - and GAIN_PHI_SQ < 4.0 - - // B2-INV-2: standard gain is exactly 1.0 - invariant b2_standard_gain_is_one - then GAIN_STANDARD == 1.0 - - // B2-INV-3: effective score scale is positive for any positive gain and head_dim - invariant b2_score_scale_positive - given gain = random_gf16_in_range(0.01, 10.0) - and head_dim = 96 - when scale = effective_score_scale(gain, head_dim) - then scale > 0.0 - - // B2-INV-4: phi^2 gain variant gives strictly higher score scale than gain=1 - // (This is a structural invariant -- not a performance claim) - invariant b2_phi_sq_scale_greater_than_standard - given head_dim = 96 - when scale_a = effective_score_scale(GAIN_PHI_SQ, head_dim) - and scale_b = effective_score_scale(GAIN_STANDARD, head_dim) - then scale_a > scale_b - - // B2-INV-5: Trinity identity preserved -- [Verified] (Law L5) - invariant b2_trinity_l5_verified - given phi = 1.618033988749895 - when lhs = phi * phi + 1.0 / (phi * phi) - then approximately_equal(lhs, 3.0) - - // B2-INV-6: Gain variants are numerically distinct - invariant b2_all_gain_variants_distinct - then GAIN_PHI_SQ != GAIN_STANDARD - and GAIN_PHI_SQ != GAIN_SQRT_PHI - and GAIN_STANDARD != GAIN_SQRT_PHI - - // ========================================================= - // PHASE B2: Benchmarks - // ========================================================= - - bench b2_forward_pass_phi_sq_gain - given config = QKGainConfig{.variant = QKGainVariant.PhiSquared, .head_dim = 96, .initial_gain = GAIN_PHI_SQ, .learnable = false, .lr_gain = 0.0} - and seq_len = 64 - when result = attention_forward(config, seq_len) - then elapsed_time_ms < 5 - - bench b2_forward_pass_standard_gain - given config = QKGainConfig{.variant = QKGainVariant.Standard, .head_dim = 96, .initial_gain = GAIN_STANDARD, .learnable = false, .lr_gain = 0.0} - and seq_len = 64 - when result = attention_forward(config, seq_len) - then elapsed_time_ms < 5 - // Both variants must have equal latency (same algorithm, different scalar) - - bench b2_forward_pass_learned_gain - given config = QKGainConfig{.variant = QKGainVariant.Learned, .head_dim = 96, .initial_gain = GAIN_LEARNED_INIT, .learnable = true, .lr_gain = 1e-3} - and seq_len = 64 - when result = attention_forward(config, seq_len) - then elapsed_time_ms < 5 - - // ========================================================= - // Mathematical Notes - // ========================================================= - // - // QK scoring: score(q, k) = (q @ k^T) * scale - // Standard scale: 1 / sqrt(head_dim) (Vaswani 2017) - // igla-peek uses: qk_gain applied to Q and K before dot product, - // then 1/sqrt(head_dim) on the dot product. - // Net score = (gain * q) @ (gain * k)^T / sqrt(head_dim) - // = gain^2 * (q @ k^T) / sqrt(head_dim) - // So QK-Gain = phi^2 is equivalent to scaling by phi^4 / sqrt(head_dim). - // - // Why [Open conjecture] and not [Verified]: - // - phi^2 = phi + 1 is [Verified arithmetic] (L5). - // - That phi^2 is the *optimal* gain for LLM attention is NOT derived - // from any theorem. It is a hypothesis to be tested empirically. - // - muP (Yang 2022, 2203.03466) provides a principled alternative: - // QK scale = 1/sqrt(d_head) after muP initialization. This scale - // is phi-independent (see B3 audit). - // - // Literature: - // Vaswani et al. 2017: standard 1/sqrt(d_k) scaling rationale. - // Yang et al. 2022 (2203.03466): muP LR transfer; QK scale is 1/d_head. - // igla-peek INV-9: current codebase anchors gain to phi^2 as a hypothesis. - // - // ========================================================= + invariant attn_sacred_gamma_range + assert SACRED_GAMMA > 0.2360679 and SACRED_GAMMA < 0.2360680 + + invariant attn_sacred_scale_range + assert SACRED_SCALE > 0.3543788 and SACRED_SCALE < 0.3543789 + + invariant attn_mask_is_below_any_score + assert MASK_SCORE < 0.0 - 1.0e20 + + invariant attn_gain_variants_are_distinct + assert GAIN_PHI_SQ != GAIN_STANDARD and GAIN_PHI_SQ != GAIN_SQRT_PHI and GAIN_STANDARD != GAIN_SQRT_PHI + + invariant attn_gain_variant_ids_are_unique + assert QK_PHI_SQUARED != QK_STANDARD and QK_STANDARD != QK_LEARNED and QK_LEARNED != QK_SQRT_PHI and QK_PHI_SQUARED != QK_LEARNED and QK_PHI_SQUARED != QK_SQRT_PHI and QK_STANDARD != QK_SQRT_PHI +}