A statement may stand where a clause head is expected - #2779
Merged
Conversation
W699 rung 9, and the instrument that found it.
INSTRUMENT: `parse-complete --fallbacks`. `bdd-block-fallback` is 93% of
everything this parser discards, and it is EIGHT call sites sharing one name.
Recording which one fired, and on which clause, split it in one pass:
events specs why clause
594 35 quantified invariant (forall) forall
269 29 unmodelled clause head forall
69 21 stopped mid-clause for
41 14 stopped mid-clause while
863 of 1 034 events are `forall` in two spellings -- one owner decision, #2774.
The 110 `for`/`while` events were the only actionable row, and they are this
commit.
RUNG 9: `for` and `while` are keywords, so at clause position they are neither a
clause head nor a block boundary, and the loop fell through to the whole-block
fallback -- taking every assertion after them.
discarded tokens 30408 -> 25093 (-5 315, the largest rung so far)
specs discarding 86 -> 77
TWO BACKEND DEFECTS THE RECOVERED CODE EXPOSED, both older than this change:
* `gen_c_invariant` emits at MODULE SCOPE, which is right for the
`_Static_assert` it is built around and invalid for anything else. A body
with statements now goes in a function, as `gen_c_test` already does.
("while loop outside of a function", and `vals` redefined per invariant.)
* `@as(usize, x)` printed its TYPE argument as an expression -- `(usize)(x)`,
"use of undeclared identifier 'usize'". Every other site maps through
`type_to_c`; this one printed the identifier it found.
cc accepts it 158 -> 163
ALL FOUR 63 -> 66
AND ONE ASSERTION THAT FAILS ON ITS OWN MERITS, filed as #2778.
`specs/base/ternary_encoding.t27` asserts a round trip over 0..16 that does not
hold. Zig evaluates it at comptime now and stops. Every backend reported that
spec as fine for as long as the block was discarded. Nine rungs in, this is the
first recovered assertion that is simply FALSE -- which is what the line was for.
Zig 217 -> 214: those three specs are ones whose assertions now RUN. One is
#2778; the other two are shape complaints (`value of type 'usize' ignored`,
`use of undefined value`) and are named there as follow-ups.
A CORRECTION. I first labelled one fallback arm "clause head not an identifier".
The comment above it says the opposite -- it fires for an identifier that is not
a CLAUSE -- so the table read as though `forall` lexed as something other than an
Ident. Renamed to "unmodelled clause head". A mislabelled bucket is worse than no
bucket: it invents an explanation.
parse-conform 22/22, new case load-bearing
cargo test --no-fail-fast 2432 passed, 0 failed
suite --ratchet RATCHET: CLEAN, ledger 177 -> 168
check_elab_ratchet.py 176 = baseline, exit 0
check_specs_generate.py exit 0
check_seal_coverage.py exit 0 (168 re-sealed, 172 twins synced)
Skill 170-172.
Refs #2754, #2778
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-29 04:14:10 UTC
Summary
Seal Status
|
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.
Refs #2754, #2778
The instrument first:
parse-complete --fallbacksbdd-block-fallbackis 93% of everything this parser discards — one bucket, no direction. It is eight call sites sharing one name. Recording which one fired, and on which clause, split it in a single pass:863 of 1 034 events are
forallin two spellings — one owner decision, #2774. The 110for/whileevents were the only actionable row, and they are this PR.Rung 9
forandwhileare keywords, so at clause position they are neither a clause head nor a block boundary, and the loop fell through to the whole-block fallback — taking every assertion after them.Two backend defects the recovered code exposed, both older than this change
gen_c_invariantemits at module scope — right for the_Static_assertit is built around, invalid for anything else.while loop outside of a function, andvalsredefined once per invariant. A body with statements now goes in a function, asgen_c_testalready does.@as(usize, x)printed its type argument as an expression —(usize)(x), use of undeclared identifier 'usize'. Every other site in that backend maps throughtype_to_c; this one printed the identifier it found.And one assertion that fails on its own merits
#2778.
specs/base/ternary_encoding.t27assertstrits_to_bits(bits_to_trits(i)) == iover0..16. It does not hold. Zig evaluates it at comptime now and stops.Every backend reported that spec as fine for as long as the block was discarded. Nine rungs in, this is the first recovered assertion that is simply false — which is what the whole line was for.
Zig 217 → 214: those three specs are the ones whose assertions now run. One is #2778; the other two are shape complaints (
value of type 'usize' ignored,use of undefined value) and are named there as follow-ups. Read the column falling only after opening each spec — five other specs went the other way once the backend defects they exposed were fixed.A correction
I first labelled one fallback arm
"clause head not an identifier". The comment directly above it says the opposite — it fires for an identifier that is not a clause — so the table read as thoughforalllexed as something other than anIdent. Renamed to"unmodelled clause head". A mislabelled bucket is worse than no bucket: it invents an explanation.🤖 Generated with Claude Code