web: property suite 4/4 on the external corpus (definitional absolutes join the relations); de-flaked test_b2b

web/TEST_RESULTS.md

@@ -43,12 +43,21 @@ so the bug list has a different author than the checks.
 |---|---|---|---|
 | `acc=` instead of `acc+=` | loop | CAUGHT (sensitivity) | CAUGHT |
 | missing bounds guard (mult-of-8) | loop | CAUGHT (nonTriviality) | CAUGHT |
-| dropped constant factor (2×) | math | missed | CAUGHT |
-| wrong leaky-ReLU alpha | math | missed | CAUGHT |
-
-The split is the finding: properties are a **loop-bug detector** (2/2), blind
-to structure-preserving value bugs (0/2). Those are owned by the differential
-gate against the spec-correct mirror. Each check class has an owner.
+| dropped constant factor (2×) | math | CAUGHT (unitScaleAnchor) | CAUGHT |
+| wrong leaky-ReLU alpha | math | CAUGHT (reluRange) | CAUGHT |
+
+**4/4 both oracles** — but the road there is the finding. The first score was
+0/4; adding non-triviality and sensitivity got the loop bugs (2/4). The two
+math bugs are provably invisible to any RELATION — if `out` satisfies every
+relation, so does `c·out` — so no cleverer relation exists. Closing them took
+a different species of check: **definitional absolutes**. `reluRange` (ReLU
+output cannot be negative — a range constraint from the definition) catches
+the leaky alpha; `unitScaleAnchor` (at unit scales dequant is the identity, so
+the output must equal the exact integer dot product, computed with plain
+integer arithmetic — no LUT, no mirror) pins absolute scale and catches the
+uniform 2×. Still no reference implementation anywhere in the property suite;
+the suite is now relations for the loop plus spec-pinned absolutes for the
+values, and the differential gate remains an independent second opinion.
 
 ## Backward rework: bit-identity + GPU wall clock
 

web/test_b2b.js

@@ -44,10 +44,15 @@ const ok = (c, msg) => { console.log(`${c ? "  ok  " : "  FAIL"}  ${msg}`); if (
     }
     ok(bad === 0, `scales from the fused absmax are bit-identical to quantizeRows (${n} rows incl. zero rows)`);
   }
-  // 2) the respec moves an int8 by at most ONE step
+  // 2) the respec moves an int8 by at most ONE step — and must move at least
+  //    one somewhere, or every "bit-identical to the mirror" claim downstream
+  //    is untested. Boundary hits are ~1 in 10^5 values, so scan ADAPTIVELY:
+  //    keep drawing until one is found (a fixed small sample made this test
+  //    flip a coin — it failed 2 runs in 3, which is its own lesson about
+  //    asserting the existence of rare events from bounded randomness).
   {
     let maxd = 0, diff = 0, n = 0;
-    for (let t = 0; t < 200; t++) {
+    while (diff === 0 && n < 3_000_000) {
       const rows = 1 + (Math.random() * 30 | 0), cols = 1 + (Math.random() * 70 | 0);
       const X = rnd(rows * cols);
       const old = V.quantizeRows(X, rows, cols);
@@ -60,10 +65,8 @@ const ok = (c, msg) => { console.log(`${c ? "  ok  " : "  FAIL"}  ${msg}`); if (
         if (d > maxd) maxd = d;
       }
     }
-    ok(maxd <= 1, `respecced quantize differs by at most 1 step (max ${maxd}; ${diff}/${n} = ${(100 * diff / n).toFixed(3)}% of values moved)`);
-    // and it must differ SOMEWHERE: if the respec silently became the old
-    // spec, every "bit-identical to the mirror" claim downstream is untested
-    ok(diff > 0, `the respec is a real change (${diff} boundary values moved) — the mirror equivalence is not vacuous`);
+    ok(maxd <= 1, `respecced quantize differs by at most 1 step (max ${maxd} over ${n} values)`);
+    ok(diff > 0, `the respec is a real change (${diff} boundary value(s) in ${n} scanned) — the mirror equivalence is not vacuous`);
   }
   // 3) chain == its parts, and gemm1 is byte-identical to the un-chained GEMM
   {

web/test_corpus.js

@@ -129,6 +129,36 @@ function propertySuite(K) {
       if (!moved) return `sensitivity(A[.,${p}] ignored)`;
     }
   }
+  // RELU RANGE. relu(x) >= 0 is part of the kernel's DEFINITION when the
+  // fused ReLU is on — a range constraint, not a relation between calls.
+  // This is what catches a wrong negative slope: the structure survives a
+  // leak, the sign does not.
+  {
+    const d = { ...SHAPES, relu: true };
+    const A = randf(d.m * d.k), B = randf(d.k * d.n);
+    const o = call(K, A, B, d);
+    for (let i = 0; i < o.length; i++) if (o[i] < 0) return "reluRange";
+  }
+  // UNIT-SCALE ANCHOR. With rs = cs = 1 the dequant is the identity, so the
+  // definition pins ABSOLUTE values: out must equal the exact integer dot
+  // product (f32-exact far below 2^24). No RELATION can do this — if out
+  // satisfies every relation, so does c*out — so the suite needs one point
+  // where the spec fixes the scale. Expected values come from plain integer
+  // arithmetic: no reference implementation, no LUT, no mirror.
+  {
+    const d = { m: 3, k: 5, n: 4, batch: 1 };
+    const Xq = new Int8Array(d.m * d.k), Wq = new Int8Array(d.k * d.n);
+    for (let i = 0; i < Xq.length; i++) Xq[i] = ((i * 37 + 11) % 25) - 12;
+    for (let i = 0; i < Wq.length; i++) Wq[i] = ((i * 53 + 7) % 25) - 12;
+    const rs = new Float32Array(d.m).fill(1), cs = new Float32Array(d.n).fill(1);
+    const o = K(Xq, Wq, rs, cs, d);
+    for (let i = 0; i < d.m; i++)
+      for (let j = 0; j < d.n; j++) {
+        let dot = 0;
+        for (let p = 0; p < d.k; p++) dot += Xq[i * d.k + p] * Wq[p * d.n + j];
+        if (o[i * d.n + j] !== dot) return "unitScaleAnchor";
+      }
+  }
   // zero row of A -> zero row out
   {
     const d = { ...SHAPES };

web/test_metamorphic.js

@@ -12,6 +12,17 @@
 // the behaviour is wrong, regardless of which side is "right". They hold exactly
 // (not approximately) because per-row/per-column quantization commutes with
 // permutation, and because int32 accumulation is exactly associative.
+//
+// The suite is TWO species of check, and the distinction matters:
+//   RELATIONS (permutation, zero-row, batch, sensitivity) — compare calls to
+//     each other. Provably blind to value bugs: if out satisfies every
+//     relation, so does c·out. An external bug corpus scored exactly this
+//     hole (2/2 on loop bugs, 0/2 on math bugs).
+//   DEFINITIONAL ABSOLUTES (reluRange, unitScaleAnchor) — points where the
+//     spec pins the value itself: ReLU output cannot be negative, and at unit
+//     scales the output IS the integer dot product. Still no reference
+//     implementation anywhere — the expected values are plain integer
+//     arithmetic — but they close the value-bug hole the relations cannot.
 const fs = require("fs");
 const path = require("path");
 const V = require("./public/verified_core.js");
@@ -60,6 +71,16 @@ function makeKernel(bug) {
       if (m > 1) for (let j = 0; j < n; j++) { const t = out[0 * n + j]; out[0 * n + j] = out[1 * n + j]; out[1 * n + j] = t; }
       return out;
     }
+    if (bug === "factor2") {              // corpus: gelu_triton_buggy — uniform 2x
+      const out = V.bgemmJS(x.q, wq, x.s, ws, d, L);
+      for (let i = 0; i < out.length; i++) out[i] = Math.fround(out[i] * 2);
+      return out;
+    }
+    if (bug === "leakyAlpha") {           // corpus: leaky_relu_buggy — leaks instead of clamping
+      const out = V.bgemmJS(x.q, wq, x.s, ws, { ...d, relu: false }, L);
+      if (d.relu) for (let i = 0; i < out.length; i++) if (out[i] < 0) out[i] = Math.fround(out[i] * 0.1);
+      return out;
+    }
     return V.bgemmJS(x.q, wq, x.s, ws, d, L);
   };
 }
@@ -104,6 +125,39 @@ const PROPS = {
     }
     return null;
   },
+  // relu(x) >= 0 is part of the DEFINITION when the fused ReLU is on — a range
+  // constraint, not a relation. Catches a wrong negative slope, which every
+  // relation survives (the structure of a leak is fine; its sign is not).
+  async reluRange(K) {
+    const d = { m: 6, k: 32, n: 5, batch: 1, relu: true };
+    const out = await K(randf(d.m * d.k), randf(d.k * d.n), d);
+    for (let i = 0; i < out.length; i++)
+      if (out[i] < 0) return `negative output ${out[i]} at [${(i / d.n) | 0},${i % d.n}] under fused ReLU`;
+    return null;
+  },
+  // With unit scales the dequant is the identity, so the definition pins
+  // ABSOLUTE values: out must equal the exact integer dot product. No RELATION
+  // can catch a uniform c× — if out satisfies every relation, c·out does too —
+  // so the suite needs one point where the spec fixes the scale. Inputs are
+  // floats that quantize exactly (row/col absmax = 127 ⇒ scale 1), and the
+  // expected values are plain integer arithmetic: no reference implementation.
+  async unitScaleAnchor(K) {
+    const d = { m: 2, k: 4, n: 2, batch: 1 };
+    const A = Float32Array.from([127, 1, -2, 3,
+                                 0, 5, -127, 2]);
+    const B = Float32Array.from([127, 3,        // k×n, each COLUMN has absmax 127
+                                 -1, 127,
+                                 2, -5,
+                                 0, 1]);
+    const out = await K(A, B, d);
+    for (let i = 0; i < d.m; i++)
+      for (let j = 0; j < d.n; j++) {
+        let dot = 0;
+        for (let p = 0; p < d.k; p++) dot += A[i * d.k + p] * B[p * d.n + j];
+        if (out[i * d.n + j] !== dot) return `unit-scale output [${i},${j}] = ${out[i * d.n + j]}, definition says ${dot}`;
+      }
+    return null;
+  },
   // a zero row of A must produce a zero row of output, whatever the scales are
   async zeroRow(K) {
     const d = { m: 6, k: 32, n: 5, batch: 1 };
@@ -182,6 +236,12 @@ const PROPS = {
   const accPerm = await PROPS.rowPermutation(makeKernel("accOverwrite"));
   ok(accSens !== null, `sensitivity catches acc= instead of acc+=  (${accSens || "MISSED"})`);
   console.log(`  note   rowPermutation vs that same acc= bug: ${accPerm ? "caught" : "missed — it is structure-preserving, which is the whole trap"}`);
+  // value bugs: invisible to every RELATION (c·out satisfies whatever out
+  // does), caught by the definitional absolutes — range and unit-scale anchor
+  const leakBad = await PROPS.reluRange(makeKernel("leakyAlpha"));
+  ok(leakBad !== null, `reluRange catches a wrong leaky slope  (${leakBad || "MISSED"})`);
+  const facBad = await PROPS.unitScaleAnchor(makeKernel("factor2"));
+  ok(facBad !== null, `unitScaleAnchor catches a uniform 2x  (${facBad || "MISSED"})`);
 
   console.log(pass ? "\nMETAMORPHIC TEST PASSED" : "\nMETAMORPHIC TEST FAILED");
   process.exit(pass ? 0 : 1);