Repository navigation
feat(sieve): DDC of t27core through t27c and t27b (Closes #6508) - #6825
Merged
Merged
Conversation
Diverse Double-Compiling of the self-hosted core (theorem T732, epics #6488 and #5980). specs/compiler/core/t27core_ddc.t27 imports t27core through `use`, carries S (t27core.t27) and E (`t27c gen-c S`) as data, and has one test: S's compile on S must write E byte for byte, and one flipped byte must be found. Each backend that builds the module runs its own stage 2: gen-c + cc core_selfhost.rs fixpoint (core(S) == gen-c(S)) t27b AArch64 t27b test --check: PASS, 7 runtime asserts Zig reference t27c test-report: PASS `t27b corpus specs/compiler/core --blockers --reference <t27c>` runs the t27b and Zig routes and compares them test by test: 2 files, 0 disagree. t27core changes so three compilers can build it: buffers of 65536 elements (t27b's repeat cap), usize indexes and unsigned division (Zig), fresh test locals instead of reassignment, brace and bracket character literals as K_* constants (use_resolve counts them), and advance() instead of a repeated `p = p + 1` (gen-zig CSE miscompile #6292, found by this harness). Fixpoint and the 59-spec corpus differential still hold. Hex data words lost digits in the front end (#6802), so the data is decimal. Limitation (T729), stated in the harness: t27b mounts compiler.rs's parser and type checker, so all three routes share one front end; the diversity is in the back ends only. core_selfhost.rs ignores the closed pipe when the core refuses a spec longer than SRC_MAX (owner-approved-foreign on #6508). Refs #6488 #5980 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
gHashTag
added
the
owner-approved-foreign
gHashTag
enabled auto-merge (squash)
October 6, 2026 13:00
This was referenced Oct 6, 2026
Merged
Merged
Merged
This was referenced Oct 6, 2026
Port scripts/tri_loop/claims.py (Python, 1 function) to specs/port/scripts/tri_loop/claims.t27
#6842
Merged
Conflict in tools/policy/foreign-exceptions.txt: both entries kept (core_selfhost.rs for #6508, test_report.rs and main.rs for #6509). compiler.rs, use_resolve.rs and specs/compiler/core are unchanged on master, so S, E and their sha256 sums in t27core_ddc.t27 still hold. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This was referenced Oct 6, 2026
Contributor
gHashTag
added a commit
that referenced
this pull request
Oct 6, 2026
T732 said the Diverse Double-Compiling check of t27core "cannot run" because t27b was BLOCKED on t27core.t27. PR #6825 makes it run: the harness specs/compiler/core/t27core_ddc.t27 builds a stage-1 core on three back ends (gen-c + cc, t27b AArch64, Zig reference) and each stage 2 equals t27c gen-c of S byte for byte (lab records cited in the spec). The text now states that result, the two defects the run found (#6292, #6802), and keeps the T729 limit: the front end is shared, so the agreement is of back ends only. The model gains the verdict rule over routes (cannot run / miscompile / back-end agreement / independent agreement), with the shared-front-end flag taken from T729's shared() rather than restated. Tests check the three recorded runs (before #6825, the first Zig run of #6292, commit 0fbd183), an exhaustive enumeration over every route mask, and a negative control: the self-host fixpoint alone passes the run DDC flags. Mutation check on the lab: dropping the miscompile branch fails all three new tests. Seal: t27c seal --save on the Railway t27c lab (t27c built from this tree), tests 20/20. Refs #6488 #6508 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
gHashTag
added a commit
that referenced
this pull request
Oct 6, 2026
T732 said the Diverse Double-Compiling check of t27core "cannot run" because t27b was BLOCKED on t27core.t27. PR #6825 makes it run: the harness specs/compiler/core/t27core_ddc.t27 builds a stage-1 core on three back ends (gen-c + cc, t27b AArch64, Zig reference) and each stage 2 equals t27c gen-c of S byte for byte (lab records cited in the spec). The text now states that result, the two defects the run found (#6292, #6802), and keeps the T729 limit: the front end is shared, so the agreement is of back ends only. The model gains the verdict rule over routes (cannot run / miscompile / back-end agreement / independent agreement), with the shared-front-end flag taken from T729's shared() rather than restated. Tests check the three recorded runs (before #6825, the first Zig run of #6292, commit 0fbd183), an exhaustive enumeration over every route mask, and a negative control: the self-host fixpoint alone passes the run DDC flags. Mutation check on the lab: dropping the miscompile branch fails all three new tests. Seal: t27c seal --save on the Railway t27c lab (t27c built from this tree), tests 20/20. Refs #6488 #6508 Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #6508
Refs #6488 #5980
Diverse Double-Compiling of the self-hosted core (theorem T732).
What lands
specs/compiler/core/t27core_ddc.t27(new). It imports t27core throughuseand carries S (t27core.t27) and E (t27c gen-c S) as tool-packed data, with sha256 sums pinned next to the lengths. Its one test runs S'scompileon S and checks that the output is E byte for byte. It then flips one byte and requires the comparison to find exactly that byte. Each backend that builds this module builds a stage-1 core, and running the test is that core's stage 2.specs/compiler/core/t27core.t27: changes so all three compilers can build it.as usizeandput_intdivides unsigned, both for Zig.{ } [ ]character literals becameK_*constants, becauseuse_resolvecounts brackets inside character literals and cut functions short.advance()instead of a repeatedp = p + 1. The repeated form triggers the gen-zig CSE miscompile in gen-zig CSE hoistscount + 1abovevar countand across its reassignment #6292.bootstrap/tests/core_selfhost.rs: one line.run_coreno longer panics on the closed pipe when the core refuses a spec longer than SRC_MAX. With the smaller buffers, 24 corpus specs are longer than that.tools/policy/foreign-exceptions.txt: entry for that test file.Stage 2 on each route (lab evidence, commit 0fbd183)
core(S) == gen-c(S), own tests 8/8, corpus differentialcargo test --release -p t27c --test core_selfhoston the t27c lab: okThe comparison is one command. It runs routes B and C and compares their verdicts test by test:
Lab records:
The t27b lab runs the same t27b and reference comparison over all of
specs/on every master commit, so after merge both files are covered there too. The t27b and t27c binaries are the lab's master build; this PR changes no t27b or t27c source.t27core.t27under the Zig reference: 8/8 PASS. Under t27btest --check: 8/8, 19 runtime asserts.The core_selfhost corpus differential still accepts 59 specs, the same set as master, with 0 mismatches against gen-c. That was measured with the cc-built core, outside cargo.
Found by the harness
count + 1abovevar countand across its reassignment #6292: gen-zig CSE hoistedp + 1above a write topinparse_array,parse_fnandparse_if, so the Zig-built core failed on S. The other two routes passed. That is the DDC working. S now avoids the shape; the compiler bug stays open in gen-zig CSE hoistscount + 1abovevar countand across its reassignment #6292.f16,f32orf64loses those digits in the shared front end. The data words are decimal because of it.Limitation (T729), stated next to the result
t27b mounts
bootstrap/src/compiler.rs's parser and type checker through#[path], and gen-c and gen-zig run behind the same parser. A front-end defect is therefore common mode: all three routes can agree on it. The diversity here is in the back ends only (C via cc, AArch64 via t27b, Zig via zig). Wheeler's independence also requires a second front end, which is not removed here.The harness header states two more limits:
Foreign code
The owner added the label
owner-approved-foreignto #6508 on 2026-10-06. Under that approval this PR edits one line of an existing Rust test,bootstrap/tests/core_selfhost.rs, and lists the file intools/policy/foreign-exceptions.txt. No new foreign file is added.bootstrap/src/compiler.rsis not touched.Not done here
specs/compiler/theory/toolchain.t27T732 still says "Today it cannot run". Updating that text would make its seal stale, so it needs a reseal on the lab and is left for a follow-up.🤖 Generated with Claude Code