diff --git a/.trinity/seals/ternary_GftSgdStep.json b/.trinity/seals/ternary_GftSgdStep.json new file mode 100644 index 000000000..a1e68cd0f --- /dev/null +++ b/.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" +} \ No newline at end of file diff --git a/bootstrap/tests/gft_sgd_step.rs b/bootstrap/tests/gft_sgd_step.rs new file mode 100644 index 000000000..17df580f7 --- /dev/null +++ b/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); +} diff --git a/bootstrap/tests/gft_sgd_step_vectors.txt b/bootstrap/tests/gft_sgd_step_vectors.txt new file mode 100644 index 000000000..f95bc417d --- /dev/null +++ b/bootstrap/tests/gft_sgd_step_vectors.txt @@ -0,0 +1,500 @@ +1496f 155ed 04a00 04f7f +04e2e 1594a 04c00 05590 +05806 158d0 04c00 058ba +05635 15410 04c00 05677 +15231 04c0a 04e00 15252 +1563d 14859 04c00 1563c +159ba 05506 05000 15a3e +055bb 04e5e 05000 0556f +04933 156c7 04a00 050fa +05027 054de 04c00 14cdc +05248 04d82 05000 051b0 +14a5e 058f3 04c00 15506 +056fa 159af 04a00 057e6 +04c53 14aa1 04e00 04cfb +04caf 048cf 05000 04bf6 +057a4 149c9 04a00 057a5 +053fe 057af 04a00 05226 +056e1 1517f 05000 05751 +14bbe 15799 04c00 0535d +158fe 14b08 04e00 158fb +14c92 159ac 04c00 05583 +057ac 04eea 04a00 057a6 +05727 14d4e 04e00 05734 +05703 15895 05000 05a0b +152fa 04b61 04a00 15301 +14a02 1578c 04c00 0536c +05437 0597a 04a00 04fd0 +04860 1573a 05000 0573f +05214 05129 04e00 05094 +14a16 05916 04a00 15337 +04c20 15735 04c00 05379 +15386 04f94 04c00 153bf +053c9 1480b 04c00 053cd +04cbd 05925 04c00 154f9 +05549 05496 04a00 054f6 +05693 05926 04a00 05593 +14e33 15121 04e00 04bb8 +14bc0 154c7 05000 054a9 +0570c 14d1e 04c00 05712 +14d86 04a4f 04a00 14dab +04a81 05587 05000 15573 +04c1b 15814 04c00 05436 +14dae 1592d 04e00 05710 +154aa 059f2 04a00 15652 +049bb 055c4 04a00 14f4d +14e36 14d3f 04a00 14e02 +054ea 14b62 04e00 054f8 +1538f 04d66 04c00 153aa +14a77 14be4 05000 048da +155cc 0545a 04e00 1567c +159a3 05261 04c00 159b6 +14b0a 15981 04a00 05350 +15620 14aab 05000 15615 +1504c 14d90 04a00 15030 +057bf 05951 05000 156e3 +14b72 14ef7 05000 04e1a +157fe 0556a 05000 158da +14ec1 14f02 05000 04808 +1533d 153af 04a00 152c7 +05954 04f59 05000 05939 +0538f 04f9f 04c00 05355 +15815 04ded 04a00 15817 +056a8 04b88 04a00 056a6 +05279 14dbc 04c00 05297 +14e2f 0495b 04c00 14e4a +15207 050eb 04a00 15236 +05172 04baf 04e00 05137 +1512d 1483d 04e00 1511b +04d3c 154d2 04a00 05038 +155e6 0495e 04a00 155e8 +14fdf 0523d 04a00 1507f +14d94 14d25 04e00 14c02 +04f25 05100 04a00 04e65 +04c8f 04eb2 05000 14cd5 +154a3 14fc4 04c00 15485 +1539d 148ea 04c00 15397 +14af3 05543 04a00 15000 +04b7b 04875 04a00 04b54 +157c8 15026 05000 15783 +04b7e 15029 05000 05099 +148f7 14e1d 04e00 04abe +14ac1 0530c 04c00 14fbc +14d10 14ff7 04c00 14a29 +056ad 04894 04e00 056aa +14f7f 15794 04c00 052b4 +04e83 04fb5 04a00 04e0c +158d3 149e8 04a00 158d3 +1505b 155bd 04c00 04ec4 +1536f 14d29 05000 1530a +0480f 148b2 04e00 04968 +14fde 15743 04c00 0524c +150c4 14fd8 05000 14d60 +05029 04b73 05000 04f75 +05493 049f4 04c00 0548f +14854 14881 04c00 14768 +14c6d 0481d 04a00 14c7e +051f6 04d7a 04e00 05187 +04e37 151e9 04a00 04f31 +057f1 05306 05000 05730 +058e4 1503c 04c00 058ed +0504f 14bdd 05000 050cb +04d85 14c6b 05000 04ef8 +055c9 051e3 04a00 055aa +15573 15103 04e00 15513 +04a1b 14d97 04a00 04b01 +148b9 04867 04c00 14953 +05330 157ba 04e00 056a9 +14bd0 15659 04c00 0521c +14bb0 049aa 05000 14cc2 +04ac4 14e7d 04e00 04ddf +04d0e 14c1c 04a00 04d52 +056fd 14adc 04c00 05700 +056a2 1483d 04e00 056a4 +04950 05144 05000 1510f +15383 14d9f 05000 1530f +14d2e 05512 04c00 151de +155e8 04a2d 05000 155f9 +15891 05993 04a00 15903 +153ac 1560a 04a00 152a7 +1497c 04ce0 04c00 14b2e +055c2 14bc4 04a00 055c6 +14f04 1541f 04c00 04c74 +15519 152f5 05000 1533d +1566d 05348 04a00 15687 +15835 05690 04c00 15887 +04a03 05627 04c00 15207 +056cb 04c3f 05000 056b9 +05715 053a8 04a00 056f8 +14e0b 1533f 04a00 1495c +04e8a 15165 05000 05255 +056f9 1543c 04e00 05788 +157c6 157e0 04e00 155ac +04f75 04a3f 04a00 04f63 +15010 157d1 04a00 04f82 +05560 148d0 04c00 05563 +14ef4 156d5 05000 056a6 +04b95 14bd9 04a00 04c08 +150e0 14b94 04e00 150a7 +156d0 14e45 04c00 156c7 +150dc 05614 05000 15670 +15418 1592b 04e00 0561f +04b91 0518f 04e00 14eab +15633 05519 04e00 156f9 +15468 159af 04e00 0567b +04bdf 04fec 05000 14ef4 +153cb 148a5 04a00 153c8 +048cd 14f7e 05000 04fd8 +14cb1 152b4 04a00 03d00 +04f90 14f6f 05000 05180 +0486d 1590d 04e00 05712 +04e85 151f5 05000 0529c +055f2 150f9 04e00 05629 +055ca 04844 04a00 055c9 +05621 15377 04e00 05690 +14cf7 14c41 05000 148d8 +04cd8 05481 05000 15454 +15232 149ab 04c00 1522b +04f30 153b7 04e00 052a8 +14c13 14aea 04c00 14b6c +05521 052eb 04c00 054c4 +1572a 15388 04a00 1570e +155af 05772 04e00 15790 +15046 14fd8 05000 14ad0 +157c8 04cac 05000 157dd +05332 04e5d 05000 0529b +056ba 05042 04a00 056b1 +1485a 14ccf 04e00 04944 +04d38 14c01 04c00 04db8 +152ee 1532d 04e00 150af +058a4 04a89 05000 0589f +15806 14a45 04e00 15804 +1569d 04ebc 05000 156c9 +151c2 052d7 04c00 15297 +14ba8 057e9 05000 157f8 +1554a 04834 04a00 1554b +14afd 15383 04e00 05123 +056ee 1521d 04c00 05710 +14bfe 04883 04e00 14c4f +051aa 14bfc 05000 05215 +04d8b 0521e 05000 15159 +14ad1 04b20 04e00 14c30 +057da 04c40 05000 057c8 +1558f 057f3 04c00 156c4 +151d8 04e92 05000 15290 +155dc 051cf 05000 15668 +057c9 0509e 04a00 057bf +14c1c 14bfe 04a00 14bb8 +0557a 14f40 04a00 05587 +15427 1571d 05000 0560a +14a4b 04a76 04c00 14ae8 +14be0 0567e 04a00 150fa +14b0f 15380 04a00 04bf1 +15601 04df0 05000 15620 +14c56 059e4 04a00 15417 +14ec9 157f8 04c00 05346 +048cc 15236 04c00 04e90 +0595d 1499a 04a00 0595d +14c08 153b8 05000 05377 +05352 149c5 05000 05370 +05199 1555a 04e00 05493 +14eb3 159aa 04c00 05554 +04aba 15715 05000 05720 +14c1d 05184 05000 15206 +05675 14f8c 04c00 05683 +15122 151eb 04c00 15027 +059d7 05558 04a00 059bc +051dd 04b3f 04e00 051a9 +148bc 0539c 05000 153b2 +14f93 0540f 04a00 150d1 +15177 0593e 04e00 157ad +05027 14efa 04e00 050e6 +05682 052cd 04e00 05628 +1514e 15939 04a00 05124 +15596 050b8 05000 15622 +153e6 155a1 05000 0535c +0499a 14b00 05000 04c66 +04ffc 04c3a 05000 04edf +0550f 157aa 04a00 055fa +1511c 04ca0 04c00 15146 +04c55 04df5 04e00 046d4 +0570e 057a0 04e00 0547c +14d62 14ea1 04e00 14904 +05761 05444 04e00 056d0 +056df 14cdb 04a00 056e2 +055fa 157ce 04a00 05677 +14d80 0507e 05000 1515e +154b3 04e13 04c00 154c4 +14cdc 14b2a 05000 14a8e +059ae 15895 05000 05b22 +15943 04e97 04e00 1594d +055a6 0534e 04a00 05571 +04f68 14b94 04e00 04fda +14e3a 04804 04a00 14e42 +151da 1562c 04c00 04bf0 +1593e 04b22 04a00 1593f +151ad 14b5c 04c00 15192 +04d9a 05912 04e00 156f5 +15963 14f71 04e00 15955 +04879 158d6 05000 058d8 +059b4 149dc 04c00 059b5 +149dc 050f6 05000 15134 +1517f 051ef 04c00 1523d +0494a 05407 04e00 151d9 +15358 14a4e 04c00 1534f +04fe0 053ad 04e00 14f7a +05393 05158 04e00 052bd +159ce 05635 04a00 159f1 +14d22 15353 05000 052ef +14ab4 15721 04a00 050ca +04f66 150dc 04e00 05121 +04c8c 0569c 04e00 15473 +05829 05521 04c00 057ee +1566f 159f6 05000 058be +14d05 14958 04e00 14c9a +04b89 14a43 05000 04ce6 +058eb 04b94 04a00 058ea +1538d 05098 04a00 153b6 +1514d 05648 05000 156b2 +15128 04828 04c00 15131 +0595b 05083 04a00 05956 +04b0b 156a4 05000 056b0 +14c71 153d3 04e00 05137 +152a9 0541b 04e00 15462 +14992 04c67 05000 14d4c +0589e 04849 04a00 0589e +157d1 05556 04a00 15803 +051ac 1548e 04c00 0531d +1547d 04ca9 04c00 15488 +054ed 15672 04e00 056b0 +14e78 04b65 04c00 14eae +150c6 059c0 05000 159ec +05690 053f0 04c00 05651 +04e55 04ff7 04a00 04dac +151d8 14baf 05000 15162 +1556e 04f0b 04a00 1557a +15756 14bc6 04a00 15754 +155fd 05166 04a00 1560c +04b2d 04b88 05000 144d8 +14abe 04804 04e00 14b3f +14c56 04d6a 04e00 14e06 +14cff 0517d 04c00 14f3e +04d81 055af 05000 15577 +148ce 155a4 04c00 05177 +14f79 14f7f 04c00 14e99 +14f2f 0576d 04e00 155d3 +14c70 156bb 05000 056a8 +050d8 1522c 04a00 05163 +156b7 158b2 04e00 14880 +0531d 0535e 04a00 052b1 +152c3 0562b 04e00 1558c +154da 04de6 05000 15518 +0591b 14d85 04c00 0591f +15286 1542f 04e00 14cb8 +04bae 04e7d 05000 14d23 +153f6 15948 04a00 14eb8 +153f4 04ff5 04c00 1541a +04e2e 15500 05000 05546 +059e2 056c5 05000 05880 +149ee 15093 04e00 04e15 +04c00 1504e 04e00 04f4e +057ae 049bf 05000 057a7 +057ff 05387 05000 0571d +05994 05562 04e00 05928 +157f0 05326 04c00 15811 +14efd 059c6 04a00 15443 +05833 053c0 04c00 05815 +04c3e 155b9 04c00 05224 +053b6 050a5 04c00 05361 +156dc 14a65 04c00 156da +15313 15007 04c00 152d2 +0522e 152aa 04a00 05283 +14aaa 14c89 04e00 14210 +05091 04923 04c00 05084 +1523a 153ea 05000 05160 +14d5a 159be 04c00 05588 +04b6c 0520c 04a00 146b0 +04942 055f7 04e00 153dd +04cce 048df 05000 04c16 +049e4 051f8 04e00 14f7c +1599e 15003 04a00 1599a +14864 052b0 04a00 14d49 +152a1 0528c 04c00 15344 +05621 056c8 04c00 054de +1504f 14ba2 04e00 15015 +04f98 0491b 04e00 04f66 +1568e 04952 04a00 1568f +05077 14f72 04a00 050ae +15905 151ad 05000 158ca +05738 15634 04e00 05829 +05835 052b7 04e00 0580a +05542 1556a 04a00 055af +14990 155e3 04e00 053c6 +156eb 1492b 04a00 156ea +05295 1495c 04e00 052a2 +056f2 14889 04a00 056f3 +150fd 15436 05000 052ee +05894 15679 04c00 058e3 +1554e 04953 04a00 15550 +1595d 14982 04c00 1595c +15218 057d3 04e00 15670 +1485d 04816 04c00 148e2 +15248 14c6e 04c00 15235 +05624 1583c 04a00 056b3 +05481 04c1a 04a00 0547d +04e09 14cde 05000 04f78 +0566d 1538e 04c00 056a6 +04e7a 0487c 04c00 04e66 +0493c 05742 04a00 1510e +049a6 158f1 05000 058f5 +153b2 153d3 04a00 15338 +154a7 04b8a 04a00 154ab +0521b 15609 04c00 05412 +155b4 04c11 04c00 155bc +0523d 14a5c 04a00 05242 +1524c 14bf4 05000 1520d +14c88 1500c 05000 04ed4 +1543b 1503c 04c00 15417 +05414 15784 04c00 055d6 +05444 04b71 05000 05428 +04aed 15094 04e00 04f4f +053be 154f8 04c00 0549d +148fb 054de 04c00 1510e +059d7 14800 05000 059d9 +14ba6 04903 04c00 14c03 +05371 1488c 04e00 0537b +04851 055b8 04c00 15193 +0560b 04990 04a00 0560a +057cb 04af5 04c00 057c8 +154a6 057e6 04c00 1564c +14a36 14a6a 04e00 14802 +1576d 153bb 04a00 1574f +159e1 14963 04c00 159e0 +151ae 057e1 05000 1582b +14ed0 05851 04c00 154ab +057d7 050ba 05000 05780 +1591c 050a7 04c00 15927 +15068 14a49 04c00 15056 +054f3 1524a 05000 0560c +14fba 150f1 05000 04e28 +151af 04e78 04e00 15226 +14f4a 150cf 04a00 14e96 +04cd8 048eb 04a00 04cc1 +04f50 14886 04a00 04f5a +14d43 05814 04a00 1527c +15196 152b3 04c00 1503c +14e5d 058f5 04c00 15541 +14fc2 15304 04a00 14e40 +0557b 04bb3 05000 0555d +059c7 04d1a 04c00 059c4 +14df1 15024 05000 04e50 +1534f 04d06 04c00 15367 +0595d 154a1 04c00 05987 +14aae 14cde 04e00 04300 +1568e 056d5 05000 158b2 +056a0 155b5 04e00 0578d +04904 054f0 04a00 14e90 +14d91 059ab 04a00 1540f +05827 04f45 04a00 05824 +14cbd 14869 04c00 14c96 +0570b 0510a 04c00 056f3 +15368 04928 04a00 1536b +15833 159bf 04a00 15776 +04f4c 05275 04e00 14d3c +15334 156a6 05000 055b2 +04a9f 04d81 04e00 14788 +04bcf 1581f 04c00 0543d +14ed3 04c39 04c00 14f1a +1575f 05802 04e00 158b0 +1533c 04cda 05000 15397 +04f4b 15457 04c00 051fc +0525b 1563d 04a00 0537a +04e85 1588e 04a00 0532f +1504e 14d1d 05000 14f0e +059cf 04e94 05000 059ba +05159 04d87 05000 05077 +056e0 053fc 04e00 05660 +14dcb 050ea 04c00 14f5a +051b6 14b22 04e00 051e8 +158c1 149f2 05000 158bd +1502e 1553e 04c00 04e20 +0485b 1516e 04e00 04fb9 +0588c 04aaa 05000 05887 +15294 15810 05000 0577b +156df 05440 04a00 15703 +15451 157e7 04e00 0532c +14c18 14826 04c00 14beb +05719 158dd 04a00 057d0 +15298 150d8 04a00 1526a +057ac 1515c 05000 0580c +0503d 15505 04e00 05412 +14fa6 149fb 04c00 14f86 +14d6f 049f7 04e00 14dee +1522c 04bb5 04a00 15233 +0495b 04eb9 05000 14e4e +156d0 1546a 04a00 156a9 +052fb 159a5 05000 05a02 +05849 04c5d 05000 05840 +053c4 0520d 04a00 05382 +04d61 04b4a 05000 04b78 +1598f 0545d 04e00 159db +05714 15439 05000 05818 +058a6 04bb2 04c00 058a4 +159c1 14f68 04c00 159ba +051b1 0548c 05000 15340 +050b6 14a34 04e00 050d9 +14f4b 05768 05000 1579d +04bd6 049b1 04a00 04b9b +04c13 15709 04a00 0518e +1543d 05284 04a00 15465 +14876 15548 04c00 05121 +0570e 04bf9 04c00 0570a +14cdb 14c3f 05000 14870 +04eb9 1513f 04c00 0502c +14847 1491a 04a00 147c8 +14e30 158be 05000 058ac +058c6 05022 04a00 058c2 +14ea5 14f4f 04c00 14da2 +14a79 04b85 05000 14cff +04869 055c6 04e00 153b3 +052e4 150f3 04e00 053a1 +149a4 059bb 04e00 157c2 +051ed 14cbe 04a00 05201 +04b2e 054cd 04a00 14e02 +0587e 05395 04a00 05870 +05704 14d63 04e00 05712 +04d18 05630 04c00 1519a +056ea 05524 04e00 05621 +0521a 14943 05000 05234 +150da 04c66 04a00 150ed +15569 148d3 04a00 15568 +152bc 14c31 05000 15276 +14849 14f48 04c00 04a24 +15666 14d31 05000 1564c +15394 04bea 05000 153d3 +05916 05946 04e00 056e6 +04e1c 04e28 05000 14300 +0502a 0596f 04c00 154e4 +15384 04e30 05000 15408 +15490 15065 04e00 15443 +14bf4 04f14 04a00 14cbf +15650 1532c 04c00 1561d +04ba2 14bfb 04c00 04c50 +0557b 0549e 05000 05174 +04b29 04db1 04e00 14620 +04948 15024 04e00 04e8d +04c99 058d1 04a00 1527e +14b15 1589e 04c00 05485 +04a21 14af5 04c00 04ade +1564e 04e51 04c00 15657 +05560 05444 04e00 0543e +154e4 156bd 04a00 15435 +15897 053de 04a00 158a6 +150dd 0559c 04e00 15485 +14fbc 05878 05000 15896 +1561e 04f33 04e00 15638 +14957 04e81 04c00 14c16 +1511c 05410 04a00 15212 +0525c 0531b 04c00 0512a +0480d 05926 04a00 15316 +051c6 04df9 05000 050c8 diff --git a/docs/NOW.md b/docs/NOW.md index af6997694..4e459abdf 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,20 @@ +# NOW — feat(spec): GF-T SGD weight update — training loop closed (2026-08-07) + +Last updated: 2026-08-07 + +## feat(spec): GF-T SGD step w' = w − η·g — the on-device training loop is complete (Refs #1764) + +- Branch: `feat/gft-sgd-step` (stacked on `feat/gft-softmax-grad`) + +### Что легло +- `specs/ternary/gft_sgd_step.t27` (`GftSgdStep`): a GF-T **SGD weight update** `w' = w − η·g` — the final brick of an on-device training step. `η` positive learning rate, `g` the (signed) gradient, `w` the (signed) weight. Composes a **signed** multiply `smul` (sign = XOR of signs, magnitude = the verified RNE magnitude mul) with subtract (`sadd`+`neg`). Bit-exact to the integer oracle **500/500** (iverilog); accuracy to GF-T16 precision (≤1 ULP, ~0.03 abs at the largest magnitudes). Spot: `w=1,g=0.5,η=0.5 → 0.75` exact; `g=0 → w` unchanged; `w=1,g=−1,η=1 → 2.0` (ascent) exact. +- Fresh seal for `GftSgdStep` (`seal --verify` MATCH). No compiler change. + +**The full on-device training loop is now expressible spec-first on GF-T:** +`logits → softmax → prob → NLL loss` (forward) → `gradient p−y` (backward) → `w' = w − η·g` (**update**). Every stage iverilog-verified bit-exact. Combined with the BitNet×GF-T layers/MLP/classifier, GF-T now spans a complete train+infer stack in synthesizable spec-first hardware. + +--- + # NOW — feat(spec): GF-T softmax+cross-entropy gradient (backward pass) (2026-08-07) Last updated: 2026-08-07 diff --git a/specs/ternary/gft_sgd_step.t27 b/specs/ternary/gft_sgd_step.t27 new file mode 100644 index 000000000..d851f3632 --- /dev/null +++ b/specs/ternary/gft_sgd_step.t27 @@ -0,0 +1,121 @@ +module GftSgdStep; +// #1764 + GF-T: a GF-T SGD weight update -- w' = w - eta * g, the final brick of an +// on-device training step (forward softmax -> loss -> gradient g -> THIS update). +// eta is the (positive) learning rate; g the gradient (signed); w the weight (signed). +// Composes the verified primitives: signed multiply (smul over the RNE magnitude +// mul) + subtract (sadd + neg). Bit-exact to the integer oracle; accuracy is to +// GF-T16 precision (<=1 ULP; ~0.03 abs at the largest magnitudes). +// +// Inputs: w, g, eta signed GF-T16 (u32). Output: updated weight w' GF-T16 (u32). + +fn magadd(a: i32, b: i32) -> i32 { + var ao : i32 = a >> 9; var am : i32 = a & 511; + var bo : i32 = b >> 9; var bm : i32 = b & 511; + var ho : i32 = bo; var hm : i32 = bm; var lo : i32 = ao; var lm : i32 = am; + if (ao >= bo) { ho = ao; hm = am; lo = bo; lm = bm; } + var hs : i32 = 512 + hm; var ls : i32 = 512 + lm; + var d : i32 = ho - lo; if (d > 11) { d = 11; } + var losh : i32 = ls >> d; var rem : i32 = ls - (losh << d); + var s : i32 = hs + losh; var off : i32 = ho; var mant : i32 = s - 512; + if (s >= 1024) { + var g : i32 = s & 1; var pre : i32 = s >> 1; mant = pre - 512; + if (g == 1) { if (rem > 0) { mant = mant + 1; } else { if ((pre & 1) == 1) { mant = mant + 1; } } } + off = ho + 1; if (off >= 80) { off = 80; } + } else { + var t : i32 = rem << 1; var hf : i32 = 1 << d; + if (t > hf) { mant = mant + 1; } else { if (t == hf) { if ((s & 1) == 1) { mant = mant + 1; } } } + } + if (mant >= 512) { mant = 0; off = off + 1; if (off >= 80) { off = 80; } } + return (off << 9) | mant; +} + +fn magsub(hi: i32, lo: i32) -> i32 { + if (hi == lo) { return 0; } + var ho : i32 = hi >> 9; var hm : i32 = hi & 511; + var lo_o : i32 = lo >> 9; var lm : i32 = lo & 511; + var d : i32 = ho - lo_o; var hs : i32 = (512 + hm) << 14; + var la : i32 = 0; var sticky : i32 = 0; + if (d >= 26) { la = 0; sticky = 1; } + else { var ls : i32 = (512 + lm) << 14; la = ls >> d; if ((ls - (la << d)) > 0) { sticky = 1; } } + var diff : i32 = hs - la; var off : i32 = ho; + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + var q : i32 = diff >> 14; var rem : i32 = diff - (q << 14); var half : i32 = 8192; var mant : i32 = q - 512; + if (rem > half) { mant = mant + 1; } + else { if (rem == half) { if (sticky == 1) { mant = mant + 1; } else { if ((q & 1) == 1) { mant = mant + 1; } } } } + if (mant >= 512) { mant = 0; off = off + 1; if (off >= 80) { off = 80; } } + return (off << 9) | mant; +} + +fn sadd(a: u32, b: u32) -> u32 { + if (a == 0) { return b; } + if (b == 0) { return a; } + var sa : i32 = (a >> 16) as i32; var ma : i32 = (a & 65535) as i32; + var sb : i32 = (b >> 16) as i32; var mb : i32 = (b & 65535) as i32; + if (sa == sb) { return ((sa << 16) | magadd(ma, mb)) as u32; } + var bsign : i32 = sa; + var r : i32 = magsub(ma, mb); + if (ma < mb) { r = magsub(mb, ma); bsign = sb; } + if (r == 0) { return 0; } + return ((bsign << 16) | r) as u32; +} + +fn neg(v: u32) -> u32 { + if (v == 0) { return 0; } + return v ^ 65536; +} + +fn magmul(a16: i32, b16: i32) -> i32 { + var ao : i32 = a16 >> 9; var am : i32 = a16 & 511; + var bo : i32 = b16 >> 9; var bm : i32 = b16 & 511; + var prod : i32 = (512 + am) * (512 + bm); + var carry : i32 = 0; if (prod >= 524288) { carry = 1; } + var q : i32 = prod >> 9; var r : i32 = prod & 511; var half : i32 = 256; + if (carry == 1) { q = prod >> 10; r = prod & 1023; half = 512; } + var mant : i32 = q - 512; + if (r > half) { mant = mant + 1; } + if (r == half) { if ((q & 1) == 1) { mant = mant + 1; } } + var sm : i32 = ao + bo + carry; + var out_off : i32 = 0; + if (sm >= 40) { var res : i32 = sm - 40; if (res >= 80) { out_off = 80; } else { out_off = res; } } + if (mant >= 512) { mant = 0; out_off = out_off + 1; if (out_off >= 80) { out_off = 80; } } + return (out_off << 9) | mant; +} + +// softmax: p_sel = 2^(l_sel - M) / sum_i 2^(l_i - M), M = max logit. + +// signed GF-T multiply: sign = xor of signs, magnitude = RNE magnitude mul. +fn smul(a: u32, b: u32) -> u32 { + if (a == 0) { return 0; } + if (b == 0) { return 0; } + var sgn : i32 = ((a >> 16) & 1) as i32; + var sb : i32 = ((b >> 16) & 1) as i32; + if (sgn != sb) { sgn = 1; } else { sgn = 0; } + var mag : i32 = magmul((a & 65535) as i32, (b & 65535) as i32); + if (mag == 0) { return 0; } + return ((sgn << 16) | mag) as u32; +} + +// w' = w - eta*g. +fn on_comb(w: u32, g: u32, eta: u32) -> u32 { + var delta : u32 = smul(eta, g); + return sadd(w, neg(delta)); +} + +// w=+1.0, g=+0.5, eta=0.5 -> 1 - 0.25 = 0.75 (offset39,mant256 = 0x4f00 = 20224). +test step { assert_eq(on_comb(20480, 19968, 19968), 20224); } +// g=0 -> weight unchanged. +test nograd { assert_eq(on_comb(20480, 0, 19968), 20480); } +// w=+1.0, g=-1.0, eta=1.0 -> 1 - (1*-1) = 2.0 (offset41 = 0x5200 = 20992). +test ascend { assert_eq(on_comb(20480, 86016, 20480), 20992); } +endmodule