feat: GF-T standalone smul + sadd datapath cores (microsequencer)

docs/NOW.md

@@ -1,7 +1,15 @@
-# NOW — feat: GF-T fused weight-update primitive (2026-08-07)
+# NOW — feat: GF-T standalone smul/sadd datapath cores (2026-08-07)
 
 Last updated: 2026-08-07
 
+## feat: GF-T standalone smul + sadd cores (microsequencer datapath) (Refs #1764)
+
+- **NEW** specs `specs/ternary/gft_smul.t27` (signed GF-T16 multiply a*b) and `specs/ternary/gft_sadd.t27` (signed GF-T16 add a+b) — the two GF-T ops exposed as standalone modules (previously only helper fns inside larger specs)
+- `test` blocks 3/3 each PASS
+- Purpose: the shared datapath cores for a MICROSEQUENCED full 2-layer backprop. Instead of instantiating many multipliers (which pushes the naive backprop to ~22M, over the ~17M ceiling), an FSM feeds operands cycle-by-cycle and reuses ONE smul + ONE sadd core + `gft_madd` (the fused update) -> tiny area. Forward computed once, intermediates in registers, updates sequenced
+- Sequencer state plan: LOAD -> [MUL(w,x) x4 for logits] -> [ADD] -> RELU -> [MUL for grads] -> [MADD x6 for updates], one op per few cycles, ~20 states
+- Spec-only; no `gen/`/`coq/` edits; no new `*.sh`; Refs #1764
+
 ## feat: GF-T madd -- fused weight update for stored-intermediates backprop (Refs #1764)
 
 - **NEW** spec `specs/ternary/gft_madd.t27` — `on_comb(w,factor,xin,k) = w - (factor*xin)*2^-k`: the single shared UPDATE datapath (one multiply + power-of-2 eta exponent-shift + subtract) for a stored-intermediates backprop, reused per weight across frames so a full 2-layer backprop fits under the ~17M correctness ceiling

specs/ternary/gft_sadd.t27

@@ -0,0 +1,112 @@
+module GftSadd;
+// #1764 + GF-T: a GF-T SGD weight update -- w' = w - eta * g, the final brick of an
+// on-device training step (forward softmax -> loss -> gradient g -> THIS update).
+// eta is the (positive) learning rate; g the gradient (signed); w the weight (signed).
+// Composes the verified primitives: signed multiply (smul over the RNE magnitude
+// mul) + subtract (sadd + neg). Bit-exact to the integer oracle; accuracy is to
+// GF-T16 precision (<=1 ULP; ~0.03 abs at the largest magnitudes).
+//
+// Inputs: w, g, eta signed GF-T16 (u32). Output: updated weight w' GF-T16 (u32).
+
+fn magadd(a: i32, b: i32) -> i32 {
+    var ao : i32 = a >> 9; var am : i32 = a & 511;
+    var bo : i32 = b >> 9; var bm : i32 = b & 511;
+    var ho : i32 = bo; var hm : i32 = bm; var lo : i32 = ao; var lm : i32 = am;
+    if (ao >= bo) { ho = ao; hm = am; lo = bo; lm = bm; }
+    var hs : i32 = 512 + hm; var ls : i32 = 512 + lm;
+    var d : i32 = ho - lo; if (d > 11) { d = 11; }
+    var losh : i32 = ls >> d; var rem : i32 = ls - (losh << d);
+    var s : i32 = hs + losh; var off : i32 = ho; var mant : i32 = s - 512;
+    if (s >= 1024) {
+        var g : i32 = s & 1; var pre : i32 = s >> 1; mant = pre - 512;
+        if (g == 1) { if (rem > 0) { mant = mant + 1; } else { if ((pre & 1) == 1) { mant = mant + 1; } } }
+        off = ho + 1; if (off >= 80) { off = 80; }
+    } else {
+        var t : i32 = rem << 1; var hf : i32 = 1 << d;
+        if (t > hf) { mant = mant + 1; } else { if (t == hf) { if ((s & 1) == 1) { mant = mant + 1; } } }
+    }
+    if (mant >= 512) { mant = 0; off = off + 1; if (off >= 80) { off = 80; } }
+    return (off << 9) | mant;
+}
+
+fn magsub(hi: i32, lo: i32) -> i32 {
+    if (hi == lo) { return 0; }
+    var ho : i32 = hi >> 9; var hm : i32 = hi & 511;
+    var lo_o : i32 = lo >> 9; var lm : i32 = lo & 511;
+    var d : i32 = ho - lo_o; var hs : i32 = (512 + hm) << 14;
+    var la : i32 = 0; var sticky : i32 = 0;
+    if (d >= 26) { la = 0; sticky = 1; }
+    else { var ls : i32 = (512 + lm) << 14; la = ls >> d; if ((ls - (la << d)) > 0) { sticky = 1; } }
+    var diff : i32 = hs - la; var off : i32 = ho;
+    var cap : i32 = 12; if (off - 1 < cap) { cap = off - 1; } if (cap < 0) { cap = 0; }
+    var sh : i32 = 0;
+    if (diff != 0) {
+        var t : i32 = diff;
+        if (t < 65536) { if (sh + 8 <= cap) { t = t << 8; sh = sh + 8; } }
+        if (t < 1048576) { if (sh + 4 <= cap) { t = t << 4; sh = sh + 4; } }
+        if (t < 4194304) { if (sh + 2 <= cap) { t = t << 2; sh = sh + 2; } }
+        if (t < 8388608) { if (sh + 1 <= cap) { t = t << 1; sh = sh + 1; } }
+    }
+    diff = diff << sh; off = off - sh;
+    var q : i32 = diff >> 14; var rem : i32 = diff - (q << 14); var half : i32 = 8192; var mant : i32 = q - 512;
+    if (rem > half) { mant = mant + 1; }
+    else { if (rem == half) { if (sticky == 1) { mant = mant + 1; } else { if ((q & 1) == 1) { mant = mant + 1; } } } }
+    if (mant >= 512) { mant = 0; off = off + 1; if (off >= 80) { off = 80; } }
+    return (off << 9) | mant;
+}
+
+fn sadd(a: u32, b: u32) -> u32 {
+    if (a == 0) { return b; }
+    if (b == 0) { return a; }
+    var sa : i32 = (a >> 16) as i32; var ma : i32 = (a & 65535) as i32;
+    var sb : i32 = (b >> 16) as i32; var mb : i32 = (b & 65535) as i32;
+    if (sa == sb) { return ((sa << 16) | magadd(ma, mb)) as u32; }
+    var bsign : i32 = sa;
+    var r : i32 = magsub(ma, mb);
+    if (ma < mb) { r = magsub(mb, ma); bsign = sb; }
+    if (r == 0) { return 0; }
+    return ((bsign << 16) | r) as u32;
+}
+
+fn neg(v: u32) -> u32 {
+    if (v == 0) { return 0; }
+    return v ^ 65536;
+}
+
+fn magmul(a16: i32, b16: i32) -> i32 {
+    var ao : i32 = a16 >> 9; var am : i32 = a16 & 511;
+    var bo : i32 = b16 >> 9; var bm : i32 = b16 & 511;
+    var prod : i32 = (512 + am) * (512 + bm);
+    var carry : i32 = 0; if (prod >= 524288) { carry = 1; }
+    var q : i32 = prod >> 9; var r : i32 = prod & 511; var half : i32 = 256;
+    if (carry == 1) { q = prod >> 10; r = prod & 1023; half = 512; }
+    var mant : i32 = q - 512;
+    if (r > half) { mant = mant + 1; }
+    if (r == half) { if ((q & 1) == 1) { mant = mant + 1; } }
+    var sm : i32 = ao + bo + carry;
+    var out_off : i32 = 0;
+    if (sm >= 40) { var res : i32 = sm - 40; if (res >= 80) { out_off = 80; } else { out_off = res; } }
+    if (mant >= 512) { mant = 0; out_off = out_off + 1; if (out_off >= 80) { out_off = 80; } }
+    return (out_off << 9) | mant;
+}
+
+// softmax: p_sel = 2^(l_sel - M) / sum_i 2^(l_i - M), M = max logit.
+
+// signed GF-T multiply: sign = xor of signs, magnitude = RNE magnitude mul.
+fn smul(a: u32, b: u32) -> u32 {
+    if (a == 0) { return 0; }
+    if (b == 0) { return 0; }
+    var sgn : i32 = ((a >> 16) & 1) as i32;
+    var sb : i32 = ((b >> 16) & 1) as i32;
+    if (sgn != sb) { sgn = 1; } else { sgn = 0; }
+    var mag : i32 = magmul((a & 65535) as i32, (b & 65535) as i32);
+    if (mag == 0) { return 0; }
+    return ((sgn << 16) | mag) as u32;
+}
+
+// Standalone signed GF-T16 add (a+b). The shared adder datapath for a
+// microsequenced backprop (see gft_smul). Reused across cycles by the FSM.
+fn on_comb(a: u32, b: u32) -> u32 { return sadd(a, b); }
+test a1 { assert_eq(on_comb(20480, 20480), 20992); }      // 1+1=2
+test a2 { assert_eq(on_comb(20480, 86016), 0); }          // 1+(-1)=0
+test a3 { assert_eq(on_comb(19968, 19968), 20480); }      // 0.5+0.5=1

specs/ternary/gft_smul.t27

@@ -0,0 +1,113 @@
+module GftSmul;
+// #1764 + GF-T: a GF-T SGD weight update -- w' = w - eta * g, the final brick of an
+// on-device training step (forward softmax -> loss -> gradient g -> THIS update).
+// eta is the (positive) learning rate; g the gradient (signed); w the weight (signed).
+// Composes the verified primitives: signed multiply (smul over the RNE magnitude
+// mul) + subtract (sadd + neg). Bit-exact to the integer oracle; accuracy is to
+// GF-T16 precision (<=1 ULP; ~0.03 abs at the largest magnitudes).
+//
+// Inputs: w, g, eta signed GF-T16 (u32). Output: updated weight w' GF-T16 (u32).
+
+fn magadd(a: i32, b: i32) -> i32 {
+    var ao : i32 = a >> 9; var am : i32 = a & 511;
+    var bo : i32 = b >> 9; var bm : i32 = b & 511;
+    var ho : i32 = bo; var hm : i32 = bm; var lo : i32 = ao; var lm : i32 = am;
+    if (ao >= bo) { ho = ao; hm = am; lo = bo; lm = bm; }
+    var hs : i32 = 512 + hm; var ls : i32 = 512 + lm;
+    var d : i32 = ho - lo; if (d > 11) { d = 11; }
+    var losh : i32 = ls >> d; var rem : i32 = ls - (losh << d);
+    var s : i32 = hs + losh; var off : i32 = ho; var mant : i32 = s - 512;
+    if (s >= 1024) {
+        var g : i32 = s & 1; var pre : i32 = s >> 1; mant = pre - 512;
+        if (g == 1) { if (rem > 0) { mant = mant + 1; } else { if ((pre & 1) == 1) { mant = mant + 1; } } }
+        off = ho + 1; if (off >= 80) { off = 80; }
+    } else {
+        var t : i32 = rem << 1; var hf : i32 = 1 << d;
+        if (t > hf) { mant = mant + 1; } else { if (t == hf) { if ((s & 1) == 1) { mant = mant + 1; } } }
+    }
+    if (mant >= 512) { mant = 0; off = off + 1; if (off >= 80) { off = 80; } }
+    return (off << 9) | mant;
+}
+
+fn magsub(hi: i32, lo: i32) -> i32 {
+    if (hi == lo) { return 0; }
+    var ho : i32 = hi >> 9; var hm : i32 = hi & 511;
+    var lo_o : i32 = lo >> 9; var lm : i32 = lo & 511;
+    var d : i32 = ho - lo_o; var hs : i32 = (512 + hm) << 14;
+    var la : i32 = 0; var sticky : i32 = 0;
+    if (d >= 26) { la = 0; sticky = 1; }
+    else { var ls : i32 = (512 + lm) << 14; la = ls >> d; if ((ls - (la << d)) > 0) { sticky = 1; } }
+    var diff : i32 = hs - la; var off : i32 = ho;
+    var cap : i32 = 12; if (off - 1 < cap) { cap = off - 1; } if (cap < 0) { cap = 0; }
+    var sh : i32 = 0;
+    if (diff != 0) {
+        var t : i32 = diff;
+        if (t < 65536) { if (sh + 8 <= cap) { t = t << 8; sh = sh + 8; } }
+        if (t < 1048576) { if (sh + 4 <= cap) { t = t << 4; sh = sh + 4; } }
+        if (t < 4194304) { if (sh + 2 <= cap) { t = t << 2; sh = sh + 2; } }
+        if (t < 8388608) { if (sh + 1 <= cap) { t = t << 1; sh = sh + 1; } }
+    }
+    diff = diff << sh; off = off - sh;
+    var q : i32 = diff >> 14; var rem : i32 = diff - (q << 14); var half : i32 = 8192; var mant : i32 = q - 512;
+    if (rem > half) { mant = mant + 1; }
+    else { if (rem == half) { if (sticky == 1) { mant = mant + 1; } else { if ((q & 1) == 1) { mant = mant + 1; } } } }
+    if (mant >= 512) { mant = 0; off = off + 1; if (off >= 80) { off = 80; } }
+    return (off << 9) | mant;
+}
+
+fn sadd(a: u32, b: u32) -> u32 {
+    if (a == 0) { return b; }
+    if (b == 0) { return a; }
+    var sa : i32 = (a >> 16) as i32; var ma : i32 = (a & 65535) as i32;
+    var sb : i32 = (b >> 16) as i32; var mb : i32 = (b & 65535) as i32;
+    if (sa == sb) { return ((sa << 16) | magadd(ma, mb)) as u32; }
+    var bsign : i32 = sa;
+    var r : i32 = magsub(ma, mb);
+    if (ma < mb) { r = magsub(mb, ma); bsign = sb; }
+    if (r == 0) { return 0; }
+    return ((bsign << 16) | r) as u32;
+}
+
+fn neg(v: u32) -> u32 {
+    if (v == 0) { return 0; }
+    return v ^ 65536;
+}
+
+fn magmul(a16: i32, b16: i32) -> i32 {
+    var ao : i32 = a16 >> 9; var am : i32 = a16 & 511;
+    var bo : i32 = b16 >> 9; var bm : i32 = b16 & 511;
+    var prod : i32 = (512 + am) * (512 + bm);
+    var carry : i32 = 0; if (prod >= 524288) { carry = 1; }
+    var q : i32 = prod >> 9; var r : i32 = prod & 511; var half : i32 = 256;
+    if (carry == 1) { q = prod >> 10; r = prod & 1023; half = 512; }
+    var mant : i32 = q - 512;
+    if (r > half) { mant = mant + 1; }
+    if (r == half) { if ((q & 1) == 1) { mant = mant + 1; } }
+    var sm : i32 = ao + bo + carry;
+    var out_off : i32 = 0;
+    if (sm >= 40) { var res : i32 = sm - 40; if (res >= 80) { out_off = 80; } else { out_off = res; } }
+    if (mant >= 512) { mant = 0; out_off = out_off + 1; if (out_off >= 80) { out_off = 80; } }
+    return (out_off << 9) | mant;
+}
+
+// softmax: p_sel = 2^(l_sel - M) / sum_i 2^(l_i - M), M = max logit.
+
+// signed GF-T multiply: sign = xor of signs, magnitude = RNE magnitude mul.
+fn smul(a: u32, b: u32) -> u32 {
+    if (a == 0) { return 0; }
+    if (b == 0) { return 0; }
+    var sgn : i32 = ((a >> 16) & 1) as i32;
+    var sb : i32 = ((b >> 16) & 1) as i32;
+    if (sgn != sb) { sgn = 1; } else { sgn = 0; }
+    var mag : i32 = magmul((a & 65535) as i32, (b & 65535) as i32);
+    if (mag == 0) { return 0; }
+    return ((sgn << 16) | mag) as u32;
+}
+
+// Standalone signed GF-T16 multiply (a*b). One shared multiply datapath for a
+// microsequenced backprop: the FSM feeds operands cycle-by-cycle and reuses this
+// one core instead of instantiating many, keeping area under the ceiling.
+fn on_comb(a: u32, b: u32) -> u32 { return smul(a, b); }
+test m1 { assert_eq(on_comb(20480, 20480), 20480); }      // 1*1=1
+test m2 { assert_eq(on_comb(20480, 86016), 86016); }      // 1*(-1)=-1
+test m3 { assert_eq(on_comb(20992, 19968), 20480); }      // 2*0.5=1