parser: a forall no longer takes its checkable neighbours with it (Refs #2161) - #2740
Merged
Conversation
…Refs #2161) An invariant reading assert g(1) == 111 forall x: i32 . g(x) == x assert g(2) == 222 lost BOTH asserts. Skipping an unbounded `forall` is a defensible language decision -- the compiler says so in its own comment -- but taking the clauses around it is a second loss on top of the defensible one, and nothing recorded that it happened. Clauses lowered BEFORE the unmodellable one are now kept, and the block is MARKED. The mark matters as much as the keeping: the emitter's "NOT CHECKED" notice keys on `children.is_empty()`, so a partial block without it would report as fully verified -- the exact claim W635 exists to stop. Now it carries its assertions AND its notice. Clauses AFTER the `forall` are still skipped: the parser jumps to the next top-level from there, and reaching them is a different change. Measured over 746 tracked specs, before binary vs after: assertions in generated Zig 11,704 -> 11,712 (+8) NOT CHECKED markers 1,068 -> 1,068 specs that LOST an assertion 0 specs that parse 620 -> 620 t27c tests 1629/6 -> 1629/6 RATCHET CLEAN Eight is the honest number. The census that motivated this estimated ~9,400 recoverable tokens, but that counterfactual assumed a different mechanism -- it rewrote the SOURCE, while this keeps what the existing parser already lowered. The eight were silently dropped before and are checked now, and the mechanism is what stops the next `forall` from doing it again. Found with the compiler's own instrument: T27_BDD_DEBUG named the fallback site on the first try, after I had guessed the wrong one and edited it to no effect. FROZEN_HASH resealed in the same commit (M5).
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
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.
An invariant reading
lost both asserts. Skipping an unbounded
forallis a defensible language decision — the compiler says so in its own comment — but taking the clauses around it is a second loss on top of the defensible one, and nothing recorded that it happened.Clauses lowered before the unmodellable one are now kept, and the block is marked.
The mark matters as much as the keeping: the emitter's
NOT CHECKEDnotice keys onchildren.is_empty(), so a partial block without it would report as fully verified — the exact claim W635 exists to stop. Now it carries its assertions and its notice.Clauses after the
forallare still skipped: the parser jumps to the next top-level from there, and reaching them is a different change.Measured over 746 tracked specs
NOT CHECKEDmarkersEight is the honest number. The census that motivated this estimated ~9,400 recoverable tokens, but that counterfactual rewrote the source, while this keeps what the existing parser already lowered. The eight were silently dropped before and are checked now — and the mechanism is what stops the next
forallfrom doing it again.Found with the compiler's own instrument:
T27_BDD_DEBUGnamed the fallback site on the first try, after I had guessed the wrong one, edited it, and watched the probe not move.Refs #2161