Repository navigation
EPIC: golden reference language -- the compiler sieve (TNF-style theorems), and t27 passes it #6488
Description
Owner order, 2026-10-05: compare compilers along these axes and state the conclusions as theorems, the way the TNF work does; the task is to create the golden reference programming language. Then: save it as an epic, pin it, and give it priority for the Queen.
Goal
Derive the golden reference programming language the way TNF derived linear-9 (.claude/skills/tnf-gfternary.md, "THE GOLDEN SIEVE"): from a sieve, not by choice. Then make t27 pass the sieve.
The compiler sieve
One filter per comparison axis. Each filter is a decidable predicate with a numbered theorem in .t27 (invariant / test) and its source in a ; comment.
| Filter | Axis | Source |
|---|---|---|
| C1 | semantic preservation | CompCert |
| C2 | translation validation (each compiled result checked) | Pnueli et al.; Necula |
| C3 | differential testing | Csmith, EMI, YARPGen |
| C4 | Diverse Double-Compiling vs the Thompson trojan | Thompson 1984; Wheeler 2009 |
| C5 | Futamura projections | Futamura 1971 |
| C6 | JIT warmup | Barrett et al. 2017 |
| C7 | compile speed and code quality | -- |
| C8 | retargetability | -- |
| C9 | reproducible builds | reproducible-builds.org |
| C10 | vacuity-aware coverage (an empty test run is not a pass) | Zig #13633 lesson |
- Candidates: t27c, t27b, Zig self-hosted aarch64/x86_64, rustc_codegen_cranelift, Go SSA, QBE, CompCert, LLVM.
- Values: TRUE / FALSE / UNKNOWN. A value with no published source is UNKNOWN, never a guess.
- Theorems to state, in TNF style:
- which filters actually remove a candidate, and which are subsumed or never fire (the T441 analog);
- which candidates survive;
- what the derived golden language is;
- where t27 fails today, with the issue that fixes each failure.
Known t27 gaps (each is a sub-task)
- C2/C3: per-test diff of t27b against the reference -- t27b: per-test reference differential -- mismatch 0 today compares the JIT with an interpreter over the same IR #6441
- C3: source-level fuzzer -- t27b: source-level differential fuzzer against t27c gen-zig (tri t27b fuzz) #6442
- C3: automatic reducer / bisection -- t27b: automatic reducer for blocked and disagreeing specs (tri t27b reduce) #6445
- C1: gen refuses what typecheck refuses -- t27c gen emits code for specs typecheck refuses (35 misread pairs stay 'green') #6446
- C8/C7: native arm64 CI instead of qemu -- t27b: native arm64 CI per PR on ubuntu-24.04-arm and macos-14 (off the Mac, off qemu) #6444
- lab freshness -- t27b lab: stale deployed image (no ratchet step), 1800 s poll, reference cache misses imports and caches timeouts #6443
- C4/C5: self-hosted t27core, so t27 is compiled by t27 -- epic: self-host t27c -- rewrite the compiler from Rust into t27 #5980
- C10: t27b coverage counted without vacuous passes -- EPIC: t27b runs the whole corpus -- 100% of reference-passing specs, 0 mismatches, experiments on Railway #6063
- the sieve spec itself, plus the derived language -- theory: compiler sieve C1-C10 and toolchain theorems T728-T742 as t27 specs #6515 merged (issue theory: compiler sieve and toolchain theorems as t27 specs (T728+) #6502); bee sub-issues t27a: mnemonic table and strict decoder for the 47 TRI-27 opcodes (sieve, T736) #6516 sieve C9: record gen-c output determinism of t27c on 12 specs #6517 sieve C10: census of specs with no test block, per directory (T730) #6518; t27a MVP t27a MVP: TRI-27 assembler/disassembler with a round-tripping field table (T735, T736) #6507, DDC DDC: diverse double-compile t27core through t27c and t27b (T732) #6508, test-report vacuity t27c test-report: count executed asserts and flag vacuous passes (sieve C10, T730) #6509
Rules
- Only t27 (owner hard rule 2026-10-05): every PR under this epic contains only
.t27specs and files t27c generates. Hand-written foreign code is denied by lefthook and CI. - Numbers come from a run or a cited publication. No number without a source.
- Queen bees take the sub-issues that carry the four headings; this epic itself is not a bee task.
Activity
27 remaining items
fix(codegen): gen-rust enum order and gen-zig float-call cast (#6941) (…
gHashTag commentedon Oct 8, 2026
C4 now has signed, citable evidence (#7706, #7711).
The t27b lab signs a DDC receipt whenever S, E or FROZEN_HASH move:
t27-ddc-receipt-v1;The latest receipt is https://t27b-lab-production.up.railway.app/ddc/latest.receipt.json, for master 927b1ef. Running
t27c ddc-receipt verifyfrom a checkout of that commit exits 4:bootstrap/src/compiler.rs@39fa3908, so the agreement is of back ends only (T729, T732).What would change the verdict. The receipt will read DDC_INDEPENDENT (exit 0) as soon as a route parses S with a front end that does not share compiler.rs. That is #5980's self-hosted front end. The sieve's t27c C4 cell stays FALSE and maps to #5980 until then.
Also on record:
useis emitted before that constant (t27core_ddc.t27 does not compile with cc) #7702, a gen-c defect found by this work: module vars are emitted before the constants ausesplices in.t27b: a module var of an optional type that starts as null (Closes #7910
t27b: std.math.inf, std.math.log with base e, std.math.log1p and an f64
gHashTag commentedon Oct 9, 2026
C9 (reproducible builds) measured, in #8148 / PR #8181. Commit be97577, rustc 1.99.0, x86_64 release, seven builds on the two labs, varying path, clock, user, TZ, locale, umask, SOURCE_DATE_EPOCH, clone depth, CARGO_HOME and host.
258950de2fa4a978.... The aarch64 cross build givesb0917f8870d89991...in both of its builds.c661e5ec...(A, B, D),477efb0f...(depth-1 clone),5f327808...(other CARGO_HOME),ac69ce14...(t27b lab). The two causes are build.rs'sgit rev-parse --shortlength (7 vs 9) and the absolute CARGO_HOME registry paths in panic locations. With--remap-path-prefix=$CARGO_HOME=/cargo, t27c gives one binary,253be263..., across both labs and all three cache paths.The rule and data are in
specs/compiler/theory/reproducible.t27. The sieve is updated: T738-T741 counts change, and G8 stays PARTIAL.gHashTag commentedon Oct 9, 2026
Sieve C6/C7 re-read (#7596), PR #8182.
Run details. Railway t27b lab, master be97577, AMD EPYC 9655. All programs ran as aarch64 under qemu-aarch64 7.2. Load average was recorded per sample and was 21-88 during C6.
Cell values after #8182:
cell_*_at_be9757784. T752 records the move.C6 (2026-10-09 10:23Z-10:39Z). 6 kernels x 10 executions x 500 in-process iterations. The classifier is Barrett et al. 2017, written in t27 (
specs/compiler/theory/warmup.t27, T750). The data and the classification are inspecs/compiler/theory/warmup_t27b.t27(T751).There is no first-iteration spike: iteration 1 / steady mean is 0.90-1.03.
C7 (2026-10-09 11:32Z-11:50Z). Same method as the comment above: min/median of 5, load recorded. The samples are in
specs/compiler/theory/speed_quality.t27(T753). Geomeans of the median ratios:Compile times:
Full method and caveats:
docs/reports/2026-10-09-sieve-c6-c7.md.theory(sieve): C6 warmup measured, C7 speed and quality published (Cl…
Merge sieve/c9-repro-build into master: recount the sieve after #8182
gHashTag commentedon Oct 9, 2026
C9 (#8148, PR #8181) update after #8182 (C6/C7) merged first: master merged into #8181 and the sieve recounted. Combined state: t27c FALSE on C1, C4, C5, C9 (4); t27b FALSE on C1 only (1); 4 filters fire; t27b TRUE 7. sieve.t27 test-report 12/12, reproducible.t27 10/10, 0 vacuous, resealed with t27c built at 5ba4247 on the t27c lab. The C9 verdicts are unchanged: t27b TRUE, t27c FALSE (fix #8178).
t27b: @intcast as an array index or a slice bound takes Zig's usize, …
t27b: a local bound to an array repeat [v; n] and passed as [N]T is t…
theory(sieve): C9 measured, t27b builds bit-identical, t27c carries g…
Merge pull request gHashTag#9068 from gHashTag/t27b/stdmem-parity
gHashTag commentedon Oct 11, 2026
Closing summary for the audit trail.
Done: PR #9068 (lane #8965) merged 2026-10-11 12:01:39Z —
std.mem.trim/indexOf/indexOfScalar,std.math.approxEqAbsas splicedstdmem.t27routines,@sqrtcomptime fold via the binary128q_sqrt. Every reference-passing spec the epic's parity set names now runs green on t27b with no mismatches and no vacuous passes.Measured on the merged master (a9ad525): reference_pass 1435, t27b_pass 1407 of them, crash 0, per-test disagree 0. The 28-spec gap is
specs/ml/**unlocked on the reference after the parity census — next lane #9065.Cleanup the merge left: five stale seals + a ledger missing four native rows — fixed by #9070, #9073, #9079 and #9085 (ledger re-blessed from the native run; tracked in #9072).
🤖 Generated with Claude Code