Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions .trinity/seals/ternary_GftLog2.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
{
"gen_hash_c": "sha256:75f978e51e511e9603498ceb9967300792995873b502aae0e9148b96b41327ae",
"gen_hash_rust": "sha256:687edcb0c65a118086b8da89051a8edc7a52b6891babcefb3bfb88f33f623ea0",
"gen_hash_verilog": "sha256:8c42bac8470c8b36d6546e9e95f2d503cf50d6d3a2d40bbdcf0cfaec6fb43685",
"gen_hash_zig": "sha256:139c0ab8aed1018c7c9e478eb7068cf63348eb93af0cb5fd1109490178c6549c",
"module": "GftLog2",
"ring": 12,
"sealed_at": "2026-08-06T16:54:52Z",
"spec_hash": "sha256:8eb008b250b93d3ec404e36be81a8e02c58a0495ba6f5e370e6f3f8361761644",
"spec_path": "specs/ternary/gft_log2.t27"
}
11 changes: 11 additions & 0 deletions .trinity/seals/ternary_GftNll.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
{
"gen_hash_c": "sha256:4bef3df4b957ee8318850b0b83458701ac68e4935bdda7c57e4df4174cf529c7",
"gen_hash_rust": "sha256:bfd7eddf7132aa036fab731cf279f7eacbad0ecbc60e95296207167b2f1fecc4",
"gen_hash_verilog": "sha256:98fb953a267e09ad50d80f7c087d0125decca93a2e67508220f6baa123e25f33",
"gen_hash_zig": "sha256:847e7b618dd89cbbf71a89a21e59a042fc09d644ce92f5e5196dad7563a92c25",
"module": "GftNll",
"ring": 12,
"sealed_at": "2026-08-06T16:54:52Z",
"spec_hash": "sha256:17e2121ad5a409fe247a3829ab0c46936fd4e374eb6cccc220a6c45311ca419c",
"spec_path": "specs/ternary/gft_nll.t27"
}
78 changes: 78 additions & 0 deletions bootstrap/tests/gft_log2.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,78 @@
// ============================================================================
// Check for the spec-first GF-T log2 primitive (specs/ternary/gft_log2.t27):
// log2(x) for a positive GF-T16, result a signed GF-T16. The missing building
// block for a GF-T softmax. Bit-exact to the committed integer oracle over 606
// vectors (tests/gft_log2_vectors.txt); the oracle is itself <=1 ULP vs the true
// true log2 (<=0.008 abs) (measured in the prototype).
// ============================================================================

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_log2.t27")
}
fn vectors_path() -> PathBuf {
PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("tests").join("gft_log2_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_log2_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] x") && v.contains("output wire [31:0] result"),
"log2 missing x -> result interface:\n{}", v
);

if !tool_available("iverilog") || !tool_available("vvp") {
eprintln!("SKIP: iverilog/vvp not on PATH; skipping log2 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_log2_{}", 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] x; wire [31:0] y; integer fails,nn,fd,code; reg [31:0] exp;
GftLog2 dut(.clk(1'b0),.rst_n(1'b1),.en(1'b1),.x(x),.ready(),.result(y));
initial begin
fails=0; nn=0; fd=$fopen("{}","r");
while(!$feof(fd)) begin code=$fscanf(fd,"%h %h\n",x,exp);
if(code==2) begin #1; nn=nn+1;
if(y!==exp) begin fails=fails+1; if(fails<=6)$display("FAIL x=%h y=%h exp=%h",x,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)), "log2 differs from the oracle:\n{}", stdout);
assert!(!stdout.contains("FAIL"), "log2 mismatch:\n{}", stdout);
}
Loading
Loading