feat(spec): GF-T SGD weight update w'=w-eta*g — training loop closed (Refs #1764)

.trinity/seals/ternary_GftSgdStep.json

@@ -0,0 +1,11 @@
+{
+  "gen_hash_c": "sha256:5515d0ea89d404f1f3b4cf2a3cddff4696c15054a9805cdfd22714c42884e36b",
+  "gen_hash_rust": "sha256:5385f7872c428856cf7dd8404a3624ddbbb556fcea1829963ec4f6ea31e70b2a",
+  "gen_hash_verilog": "sha256:688a6551ea442bf503fcc1d7baa3a7532f2474d774b0b59142cc0d5cf9dd20fc",
+  "gen_hash_zig": "sha256:395ba1306710fa36de41e2e57910c0c0dd262040d49f69c5bb9719b99e85d576",
+  "module": "GftSgdStep",
+  "ring": 12,
+  "sealed_at": "2026-08-06T17:05:04Z",
+  "spec_hash": "sha256:21db83ed35b6b0627dc77997430eaf7739126aeff07ea0120b917421eda29108",
+  "spec_path": "specs/ternary/gft_sgd_step.t27"
+}

bootstrap/tests/gft_sgd_step.rs

@@ -0,0 +1,73 @@
+// ============================================================================
+// Check for the spec-first GF-T SGD weight update (specs/ternary/gft_sgd_step.t27):
+// w' = w - eta*g, the final brick of an on-device training step. Bit-exact to the
+// integer oracle over 500 vectors (tests/gft_sgd_step_vectors.txt).
+// ============================================================================
+
+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_sgd_step.t27")
+}
+fn vectors_path() -> PathBuf {
+    PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("tests").join("gft_sgd_step_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_sgd_step_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] w") && v.contains("input  wire [31:0] eta")
+            && v.contains("output wire [31:0] result"),
+        "sgd_step missing w/g/eta -> result interface:\n{}", v
+    );
+    if !tool_available("iverilog") || !tool_available("vvp") {
+        eprintln!("SKIP: iverilog/vvp not on PATH; skipping sgd_step 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_sgd_{}", 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] w,g,eta; wire [31:0] y; integer fails,nn,fd,code; reg [31:0] exp;
+  GftSgdStep dut(.clk(1'b0),.rst_n(1'b1),.en(1'b1),.w(w),.g(g),.eta(eta),.ready(),.result(y));
+  initial begin
+    fails=0; nn=0; fd=$fopen("{}","r");
+    while(!$feof(fd)) begin code=$fscanf(fd,"%h %h %h %h\n",w,g,eta,exp);
+      if(code==4) begin #1; nn=nn+1;
+        if(y!==exp) begin fails=fails+1; if(fails<=6)$display("FAIL w=%h g=%h eta=%h y=%h exp=%h",w,g,eta,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)), "sgd_step differs from the oracle:\n{}", stdout);
+    assert!(!stdout.contains("FAIL"), "sgd_step mismatch:\n{}", stdout);
+}