feat(spec): GF-T softmax+cross-entropy gradient — the backward pass (Refs #1764)

.trinity/seals/ternary_GftSoftmaxGrad4.json

@@ -0,0 +1,11 @@
+{
+  "gen_hash_c": "sha256:550d8c42b95aa1789c03b4a8a97d00bdd6cbf7f037d7222a499e0cff61b33731",
+  "gen_hash_rust": "sha256:1ae267a11f55f4d3dafb9e501de14d3864ad8858b1fcf34b29c88605660ca858",
+  "gen_hash_verilog": "sha256:3d06bd4749a33aa86a8ad7c12ca1d251e88fc191ebb0cd39151a5a306ed85872",
+  "gen_hash_zig": "sha256:c9fa5b6027ab4cf0dd6a0d3d81e9c056d713d508312502db127730d98f3a3265",
+  "module": "GftSoftmaxGrad4",
+  "ring": 12,
+  "sealed_at": "2026-08-06T17:01:15Z",
+  "spec_hash": "sha256:efb7ddf9728f24009405883d4cbd9d9f34d57e8206b36e114cda360bf5a54fd4",
+  "spec_path": "specs/ternary/gft_softmax_grad4.t27"
+}

bootstrap/tests/gft_softmax_grad4.rs

@@ -0,0 +1,80 @@
+// ============================================================================
+// Check for the spec-first GF-T softmax (specs/ternary/gft_softmax_grad4.t27): softmax
+// over four signed GF-T16 logits, base-2, max-stabilized -> p_sel as a positive
+// GF-T16. Composes the verified GF-T primitives (max/sub/exp2/sum/reciprocal/mul).
+// Bit-exact to the committed integer oracle over 1600 vectors
+// (tests/gft_softmax_grad4_vectors.txt); accuracy vs true float softmax <=0.0018 abs vs true p_i-y_i (measured in the oracle harness).
+// ============================================================================
+
+use std::env;
+use std::fs;
+use std::path::PathBuf;
+use std::process::Command;
+
+fn t27c() -> &'static str { env!("CARGO_BIN_EXE_t27c") }
+fn spec_path() -> PathBuf {
+    PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("..").join("specs").join("ternary").join("gft_softmax_grad4.t27")
+}
+fn vectors_path() -> PathBuf {
+    PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("tests").join("gft_softmax_grad4_vectors.txt")
+}
+fn tool_available(t: &str) -> bool {
+    Command::new(t).arg("-V").output().map(|o| o.status.success()).unwrap_or(false)
+}
+
+#[test]
+fn spec_first_gft_softmax_grad4_matches_oracle() {
+    let gen = Command::new(t27c()).arg("gen-verilog").arg(spec_path()).output().expect("gen-verilog");
+    assert!(gen.status.success(), "gen-verilog failed:\n{}", String::from_utf8_lossy(&gen.stderr));
+    let v = String::from_utf8_lossy(&gen.stdout).into_owned();
+    assert!(
+        v.contains("input  wire [31:0] l0") && v.contains("input  wire [7:0] t") && v.contains("input  wire [7:0] sel")
+            && v.contains("output wire [31:0] result"),
+        "softmax_grad4 missing logits/sel -> prob interface:\n{}", v
+    );
+
+    if !tool_available("iverilog") || !tool_available("vvp") {
+        eprintln!("SKIP: iverilog/vvp not on PATH; skipping softmax_grad4 check");
+        return;
+    }
+
+    let vectors = fs::read_to_string(vectors_path()).expect("read vectors");
+    let n = vectors.lines().filter(|l| !l.trim().is_empty()).count();
+    let dir = env::temp_dir().join(format!("t27_smg4_{}", std::process::id()));
+    let _ = fs::remove_dir_all(&dir);
+    fs::create_dir_all(&dir).unwrap();
+    fs::write(dir.join("spec.v"), &gen.stdout).unwrap();
+    fs::write(dir.join("vec.txt"), &vectors).unwrap();
+
+    let tb = format!(
+        r#"`timescale 1ns/1ps
+module tb;
+  reg [31:0] l0,l1,l2,l3; reg [7:0] t,sel; wire [31:0] y;
+  integer fails,nn,fd,code; reg [31:0] exp;
+  GftSoftmaxGrad4 dut(.clk(1'b0),.rst_n(1'b1),.en(1'b1),.l0(l0),.l1(l1),.l2(l2),.l3(l3),.t(t),.sel(sel),.ready(),.result(y));
+  initial begin
+    fails=0; nn=0; fd=$fopen("{}","r");
+    while(!$feof(fd)) begin code=$fscanf(fd,"%h %h %h %h %d %d %h\n",l0,l1,l2,l3,t,sel,exp);
+      if(code==7) begin #1; nn=nn+1;
+        if(y!==exp) begin fails=fails+1; if(fails<=6)$display("FAIL sel=%0d y=%h exp=%h",sel,y,exp); end
+      end end
+    $fclose(fd);
+    if(fails==0)$display("ALL_PASS %0d",nn); else $display("FAILED %0d/%0d",fails,nn);
+    $finish;
+  end
+endmodule
+"#,
+        dir.join("vec.txt").to_str().unwrap()
+    );
+    fs::write(dir.join("tb.v"), tb).unwrap();
+
+    let vvp = dir.join("sim.vvp");
+    let compile = Command::new("iverilog").args(["-g2012", "-o", vvp.to_str().unwrap()])
+        .arg(dir.join("spec.v")).arg(dir.join("tb.v")).output().unwrap();
+    assert!(compile.status.success(), "iverilog compile failed:\n{}", String::from_utf8_lossy(&compile.stderr));
+    let run = Command::new("vvp").arg(&vvp).output().unwrap();
+    let stdout = String::from_utf8_lossy(&run.stdout).into_owned();
+    let _ = fs::remove_dir_all(&dir);
+    assert!(stdout.contains(&format!("ALL_PASS {}", n)), "softmax_grad4 differs from the oracle:\n{}", stdout);
+    assert!(!stdout.contains("FAIL"), "softmax_grad4 mismatch:\n{}", stdout);
+}