Skip to content

feat: prove GF-T primitives bit-exact across C + Rust + Verilog + model - #1877

Merged
gHashTag merged 1 commit into
masterfrom
feat/multitarget-bitexact
Aug 7, 2026
Merged

feat: prove GF-T primitives bit-exact across C + Rust + Verilog + model#1877
gHashTag merged 1 commit into
masterfrom
feat/multitarget-bitexact

Conversation

@gHashTag

@gHashTag gHashTag commented Aug 7, 2026

Copy link
Copy Markdown
Owner

Strengthens the one spec → any target, bit-exact thesis from Verilog-only to four targets. verify_multitarget.py emits smul/sadd (the exact functions the trainer's shared datapath uses) via t27c gen-c and gen-rust, compiles both (cc/rustc), and cross-checks against the independent Python GF-T model over 600 random operand pairs each: C == model and Rust == model bit-exact for both. Combined with Verilog == model (verify_emit_bitexact), all of {Verilog, C, Rust, model} agree bit-for-bit. Wired into emit-bitexact-gate (SKIPs if cc/rustc/t27c absent). Refs #1764

Strengthens the one-spec-any-target thesis from Verilog-only to four targets.
verify_multitarget.py emits smul/sadd (the exact functions the trainer's shared
datapath uses) via t27c gen-c and gen-rust, compiles both (cc/rustc), and
cross-checks against the independent Python GF-T model over 600 random operand
pairs each: C == model and Rust == model bit-exact for both. Combined with
Verilog == model (verify_emit_bitexact), all of {Verilog, C, Rust, model} agree
bit-for-bit. Wired into emit-bitexact-gate (SKIPs if cc/rustc/t27c absent).

gen-c emits the spec's test blocks as assert_eq() calls undeclared in C; stubbed
as a no-op macro before include since we call the functions directly.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@github-actions

github-actions Bot commented Aug 7, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-08-07 14:21:49 UTC

Summary

Status Count
Total Open PRs 13
PRs with Failing Checks 1
PRs with All Checks Green 12
READY 5
FAILING 1
PENDING 0

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=4c1aaad5309a != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

@github-actions

github-actions Bot commented Aug 7, 2026

Copy link
Copy Markdown
Contributor

📓 NotebookLM Notebook linked to this PR

This notebook contains session context, decisions, and artifacts for this work.

@gHashTag
gHashTag merged commit 150793a into master Aug 7, 2026
18 checks passed
@gHashTag
gHashTag deleted the feat/multitarget-bitexact branch August 7, 2026 14:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant