diff --git a/.trinity/seals/ternary_GftLog2.json b/.trinity/seals/ternary_GftLog2.json new file mode 100644 index 000000000..869e68cdd --- /dev/null +++ b/.trinity/seals/ternary_GftLog2.json @@ -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" +} \ No newline at end of file diff --git a/.trinity/seals/ternary_GftNll.json b/.trinity/seals/ternary_GftNll.json new file mode 100644 index 000000000..24c31349d --- /dev/null +++ b/.trinity/seals/ternary_GftNll.json @@ -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" +} \ No newline at end of file diff --git a/bootstrap/tests/gft_log2.rs b/bootstrap/tests/gft_log2.rs new file mode 100644 index 000000000..73e9f8215 --- /dev/null +++ b/bootstrap/tests/gft_log2.rs @@ -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); +} diff --git a/bootstrap/tests/gft_log2_vectors.txt b/bootstrap/tests/gft_log2_vectors.txt new file mode 100644 index 000000000..4337fa693 --- /dev/null +++ b/bootstrap/tests/gft_log2_vectors.txt @@ -0,0 +1,505 @@ +03fe5 15602 +05fc9 055f6 +05a8d 054ad +03e04 1563f +049ba 1531a +05cd1 0553f +05cfd 0554a +03c20 1567a +051f1 04fea +0430c 15532 +048a8 15397 +04aff 1526b +03e12 1563d +04127 155ac +05830 05411 +054bf 05275 +05ddc 05579 +04bf5 15204 +03db9 15647 +05b33 054d7 +05704 05398 +04419 154f7 +065bb 056ba +0614d 0562e +05522 052a6 +04b17 1525f +0565e 0533e +04d04 150d1 +05e51 0559b +04779 1541a +04fe5 14677 +05265 05085 +05299 050c1 +04de6 15013 +051d9 04fc7 +05375 05194 +04b4c 15247 +03f89 1560b +046de 1543d +04a1e 152eb +04e83 14eaf +05a05 05482 +05acb 054be +040f2 155b9 +05455 05239 +05903 0544c +05202 05003 +0639b 05676 +058a5 05434 +05436 05225 +05605 05304 +04394 15515 +05232 05045 +03f3b 15614 +04cab 1512b +04daf 1503d +0411b 155af +0424d 15566 +04a9d 1529d +0646a 05691 +06302 05666 +06415 05684 +06070 05612 +05bc5 054f5 +0606e 05612 +03d46 15653 +05919 05451 +046f9 15437 +06418 05684 +05c86 0552b +055af 052e2 +05d0d 0554e +052c8 050f4 +03c9e 15667 +0653b 056ac +05259 05076 +04146 155a5 +04740 15426 +03f6b 1560f +04477 154d9 +0621a 05645 +04075 155da +0556c 052c6 +06516 056a8 +0509c 04d12 +0553e 052b2 +03e20 1563a +05fe7 055fb +05488 05257 +06273 05653 +06334 0566b +05152 04eed +04153 155a2 +057b9 053e5 +0615c 05630 +04fed 14575 +05bd4 054f8 +04553 154a2 +05187 04f46 +06360 05670 +040bd 155c6 +053fa 051fc +03dbe 15646 +04300 15535 +04c2b 151c5 +04811 153f4 +04334 15529 +0615a 05630 +06245 0564c +04f6a 14ba8 +04659 15462 +055cf 052ee +05010 046d6 +05840 05416 +04171 1559c +04e45 14f45 +04cd0 15104 +05f2a 055d5 +056b6 05370 +05f9e 055ed +042b5 15548 +056e2 05387 +042cf 15541 +040ac 155cb +06286 05655 +06061 05610 +04433 154ee +064ac 0569b +04d02 150d3 +048af 15393 +05b5c 054e0 +05884 0542a +065e0 056bd +04d8f 15056 +04e0a 14fe4 +0649f 05699 +058e9 05445 +05992 0546b +05fd8 055f9 +03d07 1565a +0402c 155f1 +05cde 05543 +06018 05604 +06283 05655 +0499f 15325 +058ce 0543e +04b84 15230 +045e5 15485 +0467f 15457 +06455 0568e +0642f 05688 +04848 153cf +0544e 05234 +05273 05096 +04d76 1506b +04010 155fa +042cc 15542 +042d1 15541 +0616d 05632 +04a80 152ae +0455a 154a1 +0444c 154e6 +05dd2 05578 +06400 05680 +03f4f 15612 +04a9f 1529c +0405b 155e2 +0551a 052a2 +05cd1 0553f +04f4a 14c42 +053d5 051e0 +0596a 05463 +04261 15560 +048a9 15397 +04abe 1528b +03fb1 15607 +05197 04f60 +05c1c 0550a +03f02 1561a +05788 053d2 +0526f 05091 +04c95 15143 +0590f 0544e +05996 0546c +0419d 15593 +0496a 1533b +044e4 154bc +054df 05286 +053f3 051f7 +043f1 15503 +03c69 1566f +04572 1549c +03ea4 15626 +043c0 1550c +04a9c 1529e +05fee 055fd +03faa 15608 +04192 15595 +04425 154f3 +055a7 052de +03de6 15642 +0642f 05688 +040ff 155b5 +0602d 05608 +04c53 15191 +0642c 05688 +0470b 15433 +04790 15415 +05b7d 054e7 +049b8 1531b +05495 0525e +04cea 150ea +046ea 1543a +0632b 0566a +05c0c 05504 +05648 05331 +0588f 0542d +03c3e 15675 +040c4 155c4 +04232 1556f +04819 153ee +04cea 150ea +0645e 05690 +04215 15579 +055df 052f4 +064f0 056a3 +0426e 1555c +06197 05636 +046df 1543d +041d1 15589 +05c50 0551b +057c2 053e9 +04ea0 14e6e +0409b 155cf +04830 153df +05919 05451 +05a81 054aa +06460 05690 +047e3 15405 +05106 04e62 +04453 154e4 +04cd1 15103 +05c00 05500 +064ec 056a3 +04dec 1500f +04b60 1523f +046f5 15438 +05d95 0556c +05405 05204 +045f8 15481 +043bb 1550d +04eab 14e56 +041f7 15582 +05b28 054d4 +042a4 1554d +04c01 151ff +05b39 054d8 +042d6 15540 +05639 05327 +04c7c 15160 +062a3 0565a +04897 153a1 +04edc 14de0 +0600e 05602 +064f7 056a4 +04d1b 150bb +04bc1 15217 +04e25 14f99 +05668 05344 +05c58 0551d +05bf3 054fe +06582 056b4 +04b44 1524b +05b71 054e4 +05586 052d1 +04d7e 15064 +03f0f 15619 +060c0 0561d +05700 05396 +04d3d 1509c +04375 1551b +058de 05443 +04299 15550 +0465d 15461 +05249 05062 +051e2 04fd4 +0548d 0525a +054ba 05272 +04c3a 151b1 +04c3b 151af +04bce 15212 +04ce5 150ef +048f4 15370 +05af6 054c8 +04ae2 15279 +044e5 154bc +05417 05210 +03e04 1563f +047e4 15405 +04017 155f8 +05020 048cc +058bf 0543b +03f87 1560c +05eba 055b9 +05337 0515f +06141 0562d +048c9 15386 +03fec 15602 +03f8d 1560b +04791 15415 +063bf 0567a +051d4 04fbf +042eb 1553a +061fa 0563f +044eb 154ba +05925 05454 +05290 050b7 +06169 05631 +05665 05342 +053aa 051bf +042a4 1554d +050a3 04d31 +04480 154d7 +05522 052a6 +059db 05479 +0422e 15570 +045a6 15491 +063e4 0567d +0488b 153a7 +041dd 15586 +04bf0 15206 +03e6c 1562e +0437c 15519 +05827 0540e +048ce 15383 +04f90 14aac +0446c 154dd +04518 154af +06167 05631 +060a5 0561a +05755 053bd +05f02 055cb +05e99 055b0 +06084 05615 +04dca 15028 +057b0 053e2 +04ea0 14e6e +045f7 15482 +05dff 05580 +04f77 14b51 +05cb7 05538 +0563b 05328 +052a6 050cf +04929 15357 +05f83 055e8 +0586f 05424 +04096 155d1 +03cfd 1565b +03de1 15643 +05fdd 055fa +06137 0562c +06077 05613 +059c1 05474 +04c1b 151da +04af9 1526e +04b34 15252 +041e7 15585 +05ee8 055c5 +0578c 053d4 +057c1 053e9 +03e1f 1563b +03cd3 15660 +04533 154a9 +05be6 054fb +0411f 155ae +0609d 05619 +065c5 056bb +05497 0525f +05393 051ad +0556e 052c7 +05f18 055d1 +0632d 0566b +04c1e 151d6 +047a6 15411 +041b3 1558e +03f31 15615 +0479b 15413 +062e2 05662 +05341 05167 +04b4b 15248 +04d29 150ae +06566 056b1 +05e54 0559c +05d1b 05551 +044b2 154c9 +05b05 054cc +05df5 0557e +04e37 14f69 +05797 053d8 +05f71 055e4 +03ce9 1565d +06353 0566f +03fbb 15606 +06471 05692 +058b4 05438 +0618f 05635 +0626f 05652 +0570f 0539d +046cf 15441 +0435c 15520 +056c0 05376 +05acb 054be +05b4e 054dd +03c41 15675 +056e1 05387 +0537d 0519b +063cf 0567b +0401c 155f6 +05b4b 054dc +06443 0568b +04bbe 15219 +0588a 0542c +04068 155de +05a23 0548c +055cd 052ed +04604 1547f +04e88 14ea4 +05e0f 05585 +064bb 0569d +06360 05670 +06199 05636 +04810 153f5 +0441f 154f5 +05a35 05492 +05aa8 054b4 +03eba 15623 +03ecb 15621 +063d2 0567c +03fff 15600 +057ff 05400 +0463a 1546c +05ce4 05544 +05f60 055e1 +062bd 0565d +0404e 155e6 +044aa 154cb +0565c 0533d +0479d 15413 +06013 05603 +04b9b 15226 +054c3 05277 +0563e 0532a +054a3 05266 +046f9 15437 +05ef8 055c9 +04611 1547a +061e3 0563d +05715 053a0 +04850 153ca +03fad 15608 +04d3c 1509d +05533 052ad +064cc 0569f +051bf 04f9f +0498e 1532c +05e8f 055ad +05ee1 055c3 +041e0 15586 +06058 0560f +03e89 1562a +0449d 154cf +05114 04e7d +05612 0530d +04e3a 14f62 +05296 050be +064eb 056a3 +063c3 0567a +0622f 05648 +063dc 0567d +0469e 1544e +03c52 15672 +06338 0566c +05b3b 054d9 +0557d 052cd +05dab 05570 +0546e 05248 +05eb3 055b7 +03e1c 1563b +03ec7 15622 +054ff 05295 +063de 0567d +05bdb 054f9 +04dde 15019 +04366 1551e +04cc5 15110 +05dd5 05578 +04d20 150b6 +057c3 053e9 +03c83 1566b +04856 153c7 +05000 00000 +05200 05000 +04e00 15000 +05400 05200 +04c00 15200 diff --git a/bootstrap/tests/gft_nll.rs b/bootstrap/tests/gft_nll.rs new file mode 100644 index 000000000..ce067214f --- /dev/null +++ b/bootstrap/tests/gft_nll.rs @@ -0,0 +1,78 @@ +// ============================================================================ +// Check for the spec-first GF-T nll primitive (specs/ternary/gft_nll.t27): +// cross-entropy loss -log2(p) for a probability p; result a positive GF-T16. The missing building +// block for a GF-T softmax. Bit-exact to the committed integer oracle over 606 +// vectors (tests/gft_nll_vectors.txt); the oracle is itself <=1 ULP vs the true +// the log2-composed model (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_nll.t27") +} +fn vectors_path() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("tests").join("gft_nll_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_nll_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] p") && v.contains("output wire [31:0] result"), + "nll missing p -> result interface:\n{}", v + ); + + if !tool_available("iverilog") || !tool_available("vvp") { + eprintln!("SKIP: iverilog/vvp not on PATH; skipping nll 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_nll_{}", 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] p; wire [31:0] y; integer fails,nn,fd,code; reg [31:0] exp; + GftNll dut(.clk(1'b0),.rst_n(1'b1),.en(1'b1),.p(p),.ready(),.result(y)); + initial begin + fails=0; nn=0; fd=$fopen("{}","r"); + while(!$feof(fd)) begin code=$fscanf(fd,"%h %h\n",p,exp); + if(code==2) begin #1; nn=nn+1; + if(y!==exp) begin fails=fails+1; if(fails<=6)$display("FAIL p=%h y=%h exp=%h",p,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)), "nll differs from the oracle:\n{}", stdout); + assert!(!stdout.contains("FAIL"), "nll mismatch:\n{}", stdout); +} diff --git a/bootstrap/tests/gft_nll_vectors.txt b/bootstrap/tests/gft_nll_vectors.txt new file mode 100644 index 000000000..46c99149f --- /dev/null +++ b/bootstrap/tests/gft_nll_vectors.txt @@ -0,0 +1,403 @@ +04d01 050d4 +04643 05469 +04954 05344 +04a56 052c7 +04f05 04d3f +048c9 05386 +04912 05362 +043a4 05511 +05134 14eb8 +045e6 05485 +0482b 053e2 +04378 0551a +04861 053c0 +0413c 055a7 +04ffe 03f00 +046f6 05438 +050ff 14e55 +04f0b 04d28 +04dfb 05004 +03d75 0564d +043c0 0550c +03b9b 0568a +041e4 05585 +03b74 0568e +043de 05506 +047c4 0540b +04993 0532a +03d84 0564c +0439c 05513 +047ad 05410 +04604 0547f +04a9d 0529d +043ad 05510 +04768 0541e +03a51 056b2 +0481b 053ed +04ba5 05222 +04c19 051dd +04eca 04e15 +04692 05452 +0414d 055a3 +047a9 05410 +04232 0556f +045d8 05487 +03f6c 0560e +0407c 055d8 +040c1 055c5 +03db5 05647 +049cf 05312 +0510f 14e74 +03c1b 0567b +04990 0532b +04155 055a2 +040d9 055bf +049a6 05322 +04b7e 05232 +046ae 0544a +04011 055fa +03f0d 05619 +04999 05327 +046e8 0543b +0386e 056ee +03cba 05663 +03b30 05695 +039c7 056c5 +047ba 0540d +03b70 0568e +04cf5 050df +0423b 0556c +04629 05472 +05141 14ecf +04aa3 0529a +04dff 05001 +04d7b 05067 +04787 05417 +0424f 05566 +03c8d 0566a +049ee 05307 +04901 0536a +047b1 0540f +040db 055be +04100 055b5 +04e2d 04f84 +0479c 05413 +04bff 05200 +03a4e 056b3 +03b54 05691 +0390e 056d9 +046e0 0543d +051fc 14ffa +0389e 056e7 +04fe2 046be +03983 056cc +039a3 056c9 +04a11 052f4 +03a42 056b5 +04bb9 0521b +040c4 055c4 +03bc8 05685 +0435b 05520 +04b97 05228 +039c3 056c6 +041b0 0558f +03d41 05653 +0441c 054f6 +051b9 14f96 +04a0b 052f8 +04a2c 052e2 +0512e 14ead +0463b 0546c +03e0e 0563e +03ab0 056a5 +03960 056d0 +04f88 04ae0 +0474f 05423 +046eb 0543a +0478e 05416 +047cc 0540a +04ad6 0527f +051ee 14fe6 +03bf2 05681 +03b6b 0568f +04d22 050b5 +047eb 05404 +04ad4 05280 +0413c 055a7 +04ad1 05282 +04ebe 04e2e +05065 14c14 +049b1 0531e +0444f 054e6 +0412f 055aa +04ad5 05280 +050ab 14d54 +04216 05578 +03fde 05603 +041db 05587 +049cf 05312 +03bc3 05686 +04201 05580 +0455b 054a0 +03e97 05628 +039dc 056c3 +03b5c 05690 +04086 055d5 +03e07 0563f +03a78 056ad +04909 05366 +0409e 055ce +050be 14da5 +038a1 056e7 +04ca9 0512d +03aa3 056a6 +039ba 056c7 +04e86 04ea9 +03f14 05618 +03f49 05612 +04a41 052d4 +03e48 05634 +03f4a 05612 +051ab 14f80 +03cb3 05664 +04c77 05166 +03a33 056b7 +04bed 05207 +0408b 055d4 +04f26 04cc3 +0484d 053cc +045d0 05489 +04239 0556d +04410 054fa +04158 055a1 +04837 053da +03d45 05653 +04a68 052bc +04b93 0522a +03b3e 05693 +04126 055ac +05102 14e5b +04457 054e3 +04573 0549b +0500f 146a9 +0466b 0545d +03986 056cc +03d96 0564a +04b72 05237 +046cb 05442 +047ae 0540f +03c9a 05668 +03ec9 05621 +04270 0555b +03c80 0566b +03e33 05637 +04d6a 05075 +04d5b 05082 +0445e 054e1 +040ba 055c7 +04b6f 05238 +043eb 05504 +0457f 05499 +03c6b 0566e +0384f 056f3 +0424f 05566 +03981 056cc +038a7 056e6 +04c69 05176 +04348 05525 +048c8 05386 +03e9d 05627 +050b7 14d87 +04879 053b2 +04e83 04eaf +04219 05577 +04425 054f3 +04144 055a5 +03c4c 05673 +03997 056ca +03871 056ee +03cfb 0565b +04d2c 050ab +03e27 05639 +050f9 14e49 +03b15 05698 +043fa 05501 +03d49 05652 +039ca 056c5 +04425 054f3 +04aae 05294 +047b4 0540e +04946 0534a +050ee 14e34 +046ef 05439 +04f94 04a92 +04f40 04c66 +04170 0559c +04e7a 04ec4 +03cfe 0565b +04dda 0501c +04e28 04f91 +039da 056c3 +048d0 05382 +03d7e 0564d +03951 056d1 +04e43 04f4a +04987 0532e +049de 0530c +04eaf 04e4e +0443a 054ec +05179 14f2f +0447f 054d7 +041ad 05590 +046f6 05438 +044f2 054b9 +04701 05435 +03b90 0568b +03d53 05651 +040a1 055ce +03b05 0569a +03de4 05643 +0461e 05476 +0472f 0542a +051db 14fca +04d92 05054 +04d7a 05068 +03c84 0566b +04747 05425 +03818 056fc +04cb7 0511e +04d72 0506e +03b23 05696 +03a96 056a8 +04953 05344 +04df9 05005 +04572 0549c +03e5c 05631 +04f2b 04cb1 +04ec0 04e29 +04eb3 04e45 +047d8 05407 +041ea 05584 +0420c 0557c +03fc3 05606 +0480a 053f9 +03a58 056b1 +04339 05528 +04d9e 0504a +0436f 0551c +039a9 056c8 +044d0 054c1 +04d91 05055 +041df 05586 +03aab 056a5 +038c9 056e1 +04330 0552a +03e42 05635 +048a9 05397 +03d24 05656 +04b98 05228 +03bb4 05687 +045d1 05489 +050ef 14e36 +04fcc 04867 +03df7 05641 +046c9 05443 +0421e 05576 +0418e 05596 +0393e 056d3 +0424d 05566 +0458e 05496 +04af8 0526e +04a87 052aa +03cdb 0565f +04092 055d2 +0480d 053f7 +04320 0552e +04d72 0506e +05009 14536 +04803 053fe +05009 14536 +04854 053c8 +05154 14ef0 +05149 14edd +049c1 05317 +04bac 05220 +04c60 05181 +04132 055a9 +0480c 053f7 +03fc9 05605 +0395f 056d0 +04923 0535a +038cb 056e1 +03e4d 05633 +04489 054d4 +0441e 054f6 +0415c 055a0 +04189 05597 +03854 056f2 +03cfb 0565b +04250 05565 +041a0 05592 +04339 05528 +03aa2 056a7 +0500e 1467c +04f4a 04c42 +03cf0 0565d +040f3 055b8 +04878 053b2 +050a8 14d47 +04002 055ff +04f05 04d3f +042b6 05548 +051c1 14fa2 +0402d 055f0 +039a3 056c9 +04bfe 05201 +042c7 05543 +049f9 05303 +0439d 05513 +04cf8 050dc +03d22 05657 +04959 05342 +038e7 056de +04c9f 05138 +049eb 05308 +03dfc 05640 +04256 05563 +047d7 05408 +05022 148f7 +03ad3 056a0 +042a7 0554c +03de7 05642 +04a4c 052cd +05073 14c57 +04cd1 05103 +04bd5 05210 +04365 0551e +04f55 04c1c +04ddc 0501a +05058 14ba9 +03c5e 05670 +04f06 04d3b +04115 055b0 +041d0 05589 +03905 056da +0434b 05524 +04cfe 050d6 +044e8 054bb +04282 05556 +04632 0546f +04420 054f5 +03bf0 05681 +04ad4 05280 +045ae 0548f +03b19 05698 +03e21 0563a +044a5 054cc +03c81 0566b +04ed6 04df8 +04173 0559b +04501 054b5 +05000 00000 +04e00 05000 +04c00 05200 diff --git a/docs/NOW.md b/docs/NOW.md index 36523142c..a3c560765 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,23 @@ +# NOW — feat(spec): GF-T log2 primitive + cross-entropy (NLL) loss (2026-08-06) + +Last updated: 2026-08-06 + +## feat(spec): GF-T log2 + NLL loss — the training-signal primitives (Refs #1764) + +- Branch: `feat/gft-log2-nll` (stacked on `feat/gft-recip-softmax`) + +Deliverable **C** of "все три параллельно" (A = merge queue, infra-blocked; B = softmax synthesizability check). + +### Что легло +- `specs/ternary/gft_log2.t27` (`GftLog2`): a GF-T **log2** primitive — `log2(x)` for a positive GF-T16 → signed GF-T16. **Inverse of exp2.** `log2(x) = (o−40) + log2(1+m/512)`; the fractional part is a Q Horner quartic (coeffs `94274,−44443,21224,−5528`), the integer+fraction real value is then **normalized fixed→GF-T via a flat 31-step priority encoder** (yosys-synthesizable). Accuracy ≤0.008 abs vs true log2 (output-quantization limited). iverilog **505/505** bit-exact. + - **Bug found + fixed (broken-ruler class):** the log2 poly has NEGATIVE coefficients, and t27 emits `>>` as a **logical** shift on signed regs → it filled 0 for negative intermediates instead of arithmetic floor, diverging from the Python model. Fix: an explicit `asr9` helper doing floor-shift with only non-negative shifts. (exp2's poly was all-positive so it never hit this.) +- `specs/ternary/gft_nll.t27` (`GftNll`): GF-T **cross-entropy / negative-log-likelihood** loss for a one-hot label — given the softmax probability `p` of the true class, returns the loss `−log2(p)` as a positive GF-T16 (composes `gft_log2` + sign flip). iverilog **403/403** bit-exact; `p=1→0`, `p=0.5→1.0`, `p=0.25→2.0` (exact cross-entropy). +- Fresh seals for `GftLog2` + `GftNll` (`seal --verify` MATCH). No compiler change. + +**This opens the door from inference to TRAINING on GF-T:** forward `softmax → prob`, then `NLL → loss`, with the inverse pair `exp2`/`log2` both verified. The per-sample training signal is now expressible spec-first. + +--- + # NOW — feat(spec): GF-T reciprocal + full GF-T softmax (2026-08-06) Last updated: 2026-08-06 diff --git a/specs/ternary/gft_log2.t27 b/specs/ternary/gft_log2.t27 new file mode 100644 index 000000000..b5249538b --- /dev/null +++ b/specs/ternary/gft_log2.t27 @@ -0,0 +1,98 @@ +module GftLog2; +// #1764 + GF-T: a GF-T log2 primitive -- log2(x) for a POSITIVE GF-T16 x, result a +// signed GF-T16. Inverse of gft_exp2; the primitive needed for cross-entropy / NLL +// loss (loss = -log2(p)). log2(x) = (o-40) + log2(1+m/512); the fractional part is +// a Q16 quartic in m, then the integer+fraction real value is normalized +// (fixed->GF-T, flat priority-encoder -> yosys-synthesizable) into a signed GF-T16. +// Accuracy: <=0.008 abs vs true log2 (output-quantization limited). x<=0 saturates. +// +// Input: x positive GF-T16 (u32). Output: log2(x) as signed GF-T16 (u32). + +// arithmetic floor-shift by 9 (the poly has negative coefficients, and the +// generated Verilog `>>` on a signed reg is LOGICAL -> would fill 0 for negatives; +// this reproduces Python's floor(x/512) using only non-negative shifts). +fn asr9(v: i32) -> i32 { + if (v >= 0) { return v >> 9; } + return 0 - (((0 - v) + 511) >> 9); +} +// round(65536 * log2(1+m/512)) for m in [0,511], Q Horner with rounded shifts. +fn log2_frac(m: i32) -> i32 { + var p : i32 = 0 - 5528; + p = asr9(p * m + 256) + 21224; + p = asr9(p * m + 256) + (0 - 44443); + p = asr9(p * m + 256) + 94274; + p = asr9(p * m + 256); + return p; +} + +// encode a positive Q16.16 magnitude `mag` (value = mag/2^16) as a GF-T16 with the +// given sign. Flat left-normalization so the leading 1 lands at bit 30. +fn encode(sign: i32, mag: i32) -> u32 { + if (mag == 0) { return 0; } + var acc : i32 = mag; + var e : i32 = 0; + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + // acc now in [2^30, 2^31): mantissa = round((acc - 2^30) / 2^21), off = 54 - e. + var mant : i32 = ((acc - 1073741824) + 1048576) >> 21; + var off : i32 = 54 - e; + if (mant >= 512) { mant = 0; off = off + 1; } + if (off < 1) { off = 1; mant = 0; } + if (off > 80) { off = 80; mant = 511; } + return ((sign << 16) | (off << 9) | mant) as u32; +} + +fn on_comb(x: u32) -> u32 { + // x <= 0 (sign set or zero) is outside the log2 domain -> saturate very negative. + if (x == 0) { return ((1 << 16) | (80 << 9) | 511) as u32; } + if ((x >> 16) == 1) { return ((1 << 16) | (80 << 9) | 511) as u32; } + var o : i32 = ((x >> 9) & 127) as i32; + var m : i32 = (x & 511) as i32; + var intpart : i32 = o - 40; + var frac : i32 = log2_frac(m); + var val : i32 = (intpart << 16) + frac; // signed Q16.16 of log2(x) + if (val == 0) { return 0; } + if (val < 0) { return encode(1, 0 - val); } + return encode(0, val); +} + +// log2(1.0) = 0. +test l1 { assert_eq(on_comb(20480), 0); } +// log2(2.0) = 1.0 (0x5000). +test l2 { assert_eq(on_comb(20992), 20480); } +// log2(0.5) = -1.0 (0x15000). +test lhalf { assert_eq(on_comb(19968), 86016); } +// log2(4.0) = 2.0 (0x5200). +test l4 { assert_eq(on_comb(21504), 20992); } +// log2(0.25) = -2.0 (0x15200). +test lq { assert_eq(on_comb(19456), 86528); } +endmodule diff --git a/specs/ternary/gft_nll.t27 b/specs/ternary/gft_nll.t27 new file mode 100644 index 000000000..336495eb4 --- /dev/null +++ b/specs/ternary/gft_nll.t27 @@ -0,0 +1,102 @@ +module GftNll; +// #1764 + GF-T: GF-T negative-log-likelihood (cross-entropy loss for a one-hot +// label) -- given the softmax probability p of the true class, returns the loss +// -log2(p) as a positive GF-T16. Composes the verified gft_log2 primitive with a +// sign flip. log2(x) = (o-40) + log2(1+m/512); the fractional part is +// a Q16 quartic in m, then the integer+fraction real value is normalized +// (fixed->GF-T, flat priority-encoder -> yosys-synthesizable) into a signed GF-T16. +// Accuracy: <=0.008 abs vs true log2 (output-quantization limited). x<=0 saturates. +// +// Input: x positive GF-T16 (u32). Output: log2(x) as signed GF-T16 (u32). + +// arithmetic floor-shift by 9 (the poly has negative coefficients, and the +// generated Verilog `>>` on a signed reg is LOGICAL -> would fill 0 for negatives; +// this reproduces Python's floor(x/512) using only non-negative shifts). +fn asr9(v: i32) -> i32 { + if (v >= 0) { return v >> 9; } + return 0 - (((0 - v) + 511) >> 9); +} +// round(65536 * log2(1+m/512)) for m in [0,511], Q Horner with rounded shifts. +fn log2_frac(m: i32) -> i32 { + var p : i32 = 0 - 5528; + p = asr9(p * m + 256) + 21224; + p = asr9(p * m + 256) + (0 - 44443); + p = asr9(p * m + 256) + 94274; + p = asr9(p * m + 256); + return p; +} + +// encode a positive Q16.16 magnitude `mag` (value = mag/2^16) as a GF-T16 with the +// given sign. Flat left-normalization so the leading 1 lands at bit 30. +fn encode(sign: i32, mag: i32) -> u32 { + if (mag == 0) { return 0; } + var acc : i32 = mag; + var e : i32 = 0; + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + if (acc < 1073741824) { acc = acc << 1; e = e + 1; } + // acc now in [2^30, 2^31): mantissa = round((acc - 2^30) / 2^21), off = 54 - e. + var mant : i32 = ((acc - 1073741824) + 1048576) >> 21; + var off : i32 = 54 - e; + if (mant >= 512) { mant = 0; off = off + 1; } + if (off < 1) { off = 1; mant = 0; } + if (off > 80) { off = 80; mant = 511; } + return ((sign << 16) | (off << 9) | mant) as u32; +} + +fn log2v(x: u32) -> u32 { + if (x == 0) { return ((1 << 16) | (80 << 9) | 511) as u32; } + if ((x >> 16) == 1) { return ((1 << 16) | (80 << 9) | 511) as u32; } + var o : i32 = ((x >> 9) & 127) as i32; + var m : i32 = (x & 511) as i32; + var intpart : i32 = o - 40; + var frac : i32 = log2_frac(m); + var val : i32 = (intpart << 16) + frac; + if (val == 0) { return 0; } + if (val < 0) { return encode(1, 0 - val); } + return encode(0, val); +} +fn neg(v: u32) -> u32 { + if (v == 0) { return 0; } + return v ^ 65536; +} +// cross-entropy loss for one class: -log2(p), p a probability in (0,1]. +fn on_comb(p: u32) -> u32 { + return neg(log2v(p)); +} + +// p = 1.0 -> loss 0 (perfect prediction). +test perfect { assert_eq(on_comb(20480), 0); } +// p = 0.5 -> loss -log2(0.5) = +1.0 (0x5000). +test half { assert_eq(on_comb(19968), 20480); } +// p = 0.25 -> loss 2.0 (0x5200). +test quarter { assert_eq(on_comb(19456), 20992); } +endmodule