From 8573799a6b819549808489436e0883f398467e38 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Fri, 7 Aug 2026 17:20:07 +0700 Subject: [PATCH] feat: GF-T 2-layer backprop with scale_q eta (power-of-2, -2M fasm) gft_xorbp2.t27: the full 2-layer XOR backprop step with scale_q applied to the weight updates -- eta=0.125=2^-3 folded into an exponent-offset shift, removing the 6 eta-multipliers. In-spec PASS; GF-T sim converges XOR 4/4 with eta=0.125. Size: single-core-with-sel backprop 23.7M -> 21.7M with scale_q, still over the ~17M ceiling (all 3 sel-branches synthesize into hardware). Finding: a stored-intermediates FSM is needed to fit -- forward once (store h,e,z,dz,x), then per-weight update frames reuse one shared update datapath. The sequential/coordinate backprop dynamic converges (verified in sim). Refs #1764 Co-Authored-By: Claude Opus 4.8 --- docs/NOW.md | 9 +- specs/ternary/gft_xorbp2.t27 | 159 +++++++++++++++++++++++++++++++++++ 2 files changed, 167 insertions(+), 1 deletion(-) create mode 100644 specs/ternary/gft_xorbp2.t27 diff --git a/docs/NOW.md b/docs/NOW.md index 5323316c69..e0c457d9d7 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,7 +1,14 @@ -# NOW — feat: GF-T full 2-layer XOR backprop step (2026-08-07) +# NOW — feat: GF-T backprop with power-of-2 eta (scale_q) (2026-08-07) Last updated: 2026-08-07 +## feat: GF-T 2-layer backprop, scale_q eta optimization (Refs #1764) + +- **NEW** spec `specs/ternary/gft_xorbp2.t27` — the full 2-layer XOR backprop step (`gft_xorbp`) with `scale_q` applied to the weight updates: eta=0.125=2^-3 folded into an exponent-offset shift, removing the 6 eta-multipliers. In-spec test PASS; GF-T sim converges XOR 4/4 with eta=0.125 +- Size: single-core-with-sel backprop is fasm 23.7M -> 21.7M with scale_q -- STILL over the ~17M correctness ceiling (all 3 sel-branches synthesize into hardware since sel is a runtime input). Design finding: a stored-intermediates FSM is needed to fit -- run the forward ONCE (store h,e,z,dz,x in registers), then per-weight update frames reuse a single shared update datapath +- The sequential/coordinate backprop dynamic (update one weight-pair per frame, recompute forward) converges -- verified in the GF-T sim +- Spec-only; no `gen/`/`coq/` edits; no new `*.sh`; Refs #1764 + ## feat: GF-T full 2-layer backprop (learnable hidden + output) (Refs #1764) - **NEW** spec `specs/ternary/gft_xorbp.t27` — full 2-layer XOR backprop step: hidden W(2x2) AND output v(2) BOTH trainable (fixed biases c=[0,-1], b=0). Forward z_j=W_j.x+c_j, h_j=relu(z_j), y=v.h; MSE backprop e=y-t, dv_j=e*h_j, dz_j=e*v_j*relu'(z_j), dW_jk=dz_j*x_k. Returns the updated weight-PAIR by `sel` (u64: 0->hidden0, 1->hidden1, 2->output) diff --git a/specs/ternary/gft_xorbp2.t27 b/specs/ternary/gft_xorbp2.t27 new file mode 100644 index 0000000000..58d4c8b8f5 --- /dev/null +++ b/specs/ternary/gft_xorbp2.t27 @@ -0,0 +1,159 @@ +module GftXorBp2; +// #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; +} + +// GF-T ReLU: max(0,z) — zero if z is zero or has the sign bit set, else z. +fn relu(z: u32) -> u32 { + if (z == 0) { return 0; } + if (((z >> 16) & 1) == 1) { return 0; } + return z; +} +// ReLU derivative as a GF-T gate: 1.0 (=20480) if z>0, else 0. +fn relu_prime(z: u32) -> u32 { + if (z == 0) { return 0; } + if (((z >> 16) & 1) == 1) { return 0; } + return 20480; +} +// FULL 2-layer XOR backprop step. Hidden W (2x2) with fixed biases c=[0,-1], +// output v (2) with fixed b=0. Forward z_j=W_j.x+c_j, h_j=relu(z_j), y=v.h. +// Backprop (MSE): e=y-t; dv_j=e*h_j; dz_j=e*v_j*relu'(z_j); dW_jk=dz_j*x_k. +// Returns the updated weight-PAIR selected by sel (u64): 0 -> (w00',w01'), +// 1 -> (w10',w11'), 2 -> (v0',v1'). Wrapper holds 6 regs, instantiates 3 cores. +fn scale_q(x: u32, k: i32) -> u32 { + if (x == 0) { return 0; } + var sign : i32 = ((x >> 16) & 1) as i32; + var off : i32 = ((x >> 9) & 127) as i32; + var mant : i32 = (x & 511) as i32; + off = off - k; + if (off < 1) { return 0; } + return ((sign << 16) | (off << 9) | mant) as u32; +} +fn on_comb(w00: u32, w01: u32, w10: u32, w11: u32, v0: u32, v1: u32, + x0: u32, x1: u32, t: u32, eta: u32, sel: u32) -> u64 { + var z0 : u32 = sadd(sadd(smul(w00, x0), smul(w01, x1)), 0); // c0 = 0 + var z1 : u32 = sadd(sadd(smul(w10, x0), smul(w11, x1)), 86016); // c1 = -1.0 + var h0 : u32 = relu(z0); + var h1 : u32 = relu(z1); + var y : u32 = sadd(smul(v0, h0), smul(v1, h1)); + var e : u32 = sadd(y, neg(t)); + if (sel == 2) { + var v0n : u32 = sadd(v0, neg(scale_q(smul(e, h0), 3))); + var v1n : u32 = sadd(v1, neg(scale_q(smul(e, h1), 3))); + return ((v0n as u64) << 32) | (v1n as u64); + } + if (sel == 0) { + var dz0 : u32 = smul(smul(e, v0), relu_prime(z0)); + var w00n : u32 = sadd(w00, neg(scale_q(smul(dz0, x0), 3))); + var w01n : u32 = sadd(w01, neg(scale_q(smul(dz0, x1), 3))); + return ((w00n as u64) << 32) | (w01n as u64); + } + var dz1 : u32 = smul(smul(e, v1), relu_prime(z1)); + var w10n : u32 = sadd(w10, neg(scale_q(smul(dz1, x0), 3))); + var w11n : u32 = sadd(w11, neg(scale_q(smul(dz1, x1), 3))); + return ((w10n as u64) << 32) | (w11n as u64); +} +// smoke: near-solution W=[[1,1],[1,1]], v=[1,-2]; corner (1,1),t=0. output sel=2. +// forward y = 1*relu(2) + (-2)*relu(1) = 2-2 = 0 = t -> e=0 -> v unchanged (1,-2). +test out_noupdate { assert_eq(on_comb(20480,20480,20480,20480,20480,86528, 20480,20480,0,19456, 2), 87960930308608); }