Skip to content

feat(spec): GF-T reciprocal + complete GF-T softmax (Refs #1764) - #1804

Merged
gHashTag merged 1 commit into
feat/gft-exp2-layer4-synthfrom
feat/gft-recip-softmax
Aug 6, 2026
Merged

feat(spec): GF-T reciprocal + complete GF-T softmax (Refs #1764)#1804
gHashTag merged 1 commit into
feat/gft-exp2-layer4-synthfrom
feat/gft-recip-softmax

Conversation

@gHashTag

@gHashTag gHashTag commented Aug 6, 2026

Copy link
Copy Markdown
Owner

Stacked on #1803 (needs its exp2 primitive). Base will be retargeted to master once #1803 merges.

gft_recip.t27 — GF-T reciprocal 1/x (the last softmax primitive)

Closed form, no polynomial: 1/(1+m/512) = 512/(512+m), written in GF-T form gives 512+m' = round(524288/(512+m)), off' = 79−o (+renorm). One rounded integer divide → EXACT (0 ULP) vs true 1/x (30000 samples). iverilog 506/506 bit-exact; spot checks exact (1/1=1, 1/2=0.5, 1/0.5=2, 1/−1=−1, 1/4=0.25).

gft_softmax4.t27 — the complete GF-T softmax

Softmax over 4 signed GF-T16 logits, base-2, max-stabilized:

p_i = 2^(l_i − M) / Σ_j 2^(l_j − M),   M = max_j l_j

Returns p_sel. Composes all the now-verified GF-T primitives: max (gt), subtract (sadd+neg), exp2 (≤1 ULP), sum (sadd), reciprocal (exact), multiply (RNE).

  • Bit-exact to the integer oracle 2000/2000 (iverilog).
  • Accuracy ≤ 0.0017 absolute probability vs true float softmax. Sum-of-probs ∈ [0.9982, 1.0018]; uniform logits → 0.25 exact; [2,1,1,1] → 0.40.

Fresh seals for GftRecip + GftSoftmax4 (seal --verify → MATCH). No compiler change.

This completes the GF-T classifier head: activations → MLP → logits → {argmax → class} OR {softmax → calibrated probabilities}.

Refs #1764

⚠️ GitHub Actions infra incident still ongoing (jobs stuck queued). All verification above is local (iverilog + seals).

🤖 Generated with Claude Code

gft_recip.t27 (GftRecip): 1/x for a signed GF-T16 -- the last missing softmax
primitive. Closed form (no polynomial): 512+m' = round(524288/(512+m)),
off' = 79-o (+renorm). One rounded integer divide -> EXACT (0 ULP) vs true 1/x.
iverilog 506/506 bit-exact.

gft_softmax4.t27 (GftSoftmax4): the complete GF-T softmax over 4 signed GF-T16
logits, base-2, max-stabilized: p_i = 2^(l_i-M) / sum 2^(l_j-M), returns p_sel.
Composes the verified primitives -- max (gt), subtract (sadd+neg), exp2 (<=1 ULP),
sum (sadd), reciprocal (exact), multiply (RNE). Bit-exact to the integer oracle
2000/2000 (iverilog); accuracy <=0.0017 abs probability vs true float softmax
(sum-of-probs in [0.9982,1.0018]; uniform -> 0.25 exact).

Completes the GF-T classifier head: activations -> MLP -> logits ->
{argmax -> class} or {softmax -> calibrated probabilities}.

Fresh seals for GftRecip + GftSoftmax4 (seal --verify MATCH). No compiler change.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gHashTag

gHashTag commented Aug 6, 2026

Copy link
Copy Markdown
Owner Author

Synthesizability confirmed (yosys). read_verilog → hierarchy → proc → flatten → opt → techmap → opt → stat completes cleanly on GftSoftmax4:

  • 132,981 cells (42324 \$_AND_, 36994 \$_MUX_, 24918 \$_OR_, 14724 \$_XOR_, 14017 \$_NOT_), 49817 wires. ~54s, 2.3 GB peak.
  • No Function can only be called with constant arguments error — the nested runtime-arg composition (exp2(sadd(l_i, neg(mx))), recip, magmul) synthesizes fine (combinational, no latches). This retires the earlier open question about whether nested GF-T primitive calls are synthesizable.

Area is large (deep GF-T arith trees × 4 logits + the exp2 poly + recip divide), as expected for a full softmax — it is a candidate for pipelining/sharing before a board run, but it is synthesizable today.

@gHashTag
gHashTag merged commit 908a578 into feat/gft-exp2-layer4-synth Aug 6, 2026
6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant