feat(t27b): run invariant blocks like tests, report them apart (Refs #5977) - #5992
Merged
Merged
Conversation
An `invariant` block lowers exactly like a `test` (a parameterless body,
the test binding rule) and runs through the same trap machinery. t27c's
Zig backend emits it as `comptime { ... }`, so a broken invariant is a
compile error there; t27b runs it at test time and prints INVARIANT
PASS / INVARIANT FAIL, plus an `invariants N held, M broken, K not
checked` line. An invariant whose body the front-end discarded (a
`forall`, an unparseable clause) is NOT CHECKED, never "held"; a
partially parsed one is rejected, as a partial test already was.
Clause-form blocks carry no line on any node, so their header line is
looked up in the source text.
Corpus: 48 supported (47 pass, 1 spec failure), was 37; 0 mismatches.
Differential: 0 mismatches, 2500 programs per mode.
Refs #5977
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Merged
4 of 5 tasks
Contributor
This was referenced Oct 4, 2026
6 tasks
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.
Summary
invariantblocks are now lowered and run by t27b, natively, through the same machinery astestblocks:invariantblock lowers exactly like atest: a parameterless body under the test binding rule, with the same trap sites.INVARIANT PASS/INVARIANT FAIL, plus a lineinvariants N held, M broken, K not checked.forall, or a clause it could not parse), the invariant is reported as NOT CHECKED. It is never reported as held.unsupported construct InvariantBlockmessage. Partially parsed tests were already rejected this way.t27c's Zig backend emits an invariant as
comptime { ... }, so a broken invariant is a compile error there. t27b runs it at test time instead.Numbers
t27b corpus specs/over 1184 specs:ternary_model, a bug in the spec)The differential test (random programs, JIT vs interpreter) found 0 mismatches over 2500 programs in each overflow mode.
New tests are in
cli/t27b/tests/source.rs. They cover invariants that hold, break, overflow or are quantified, plus the rejection of a partially parsed invariant.Refs #5977. Part of #5905.
🤖 Generated with Claude Code