Five checks that had stopped describing the code they guard - #2744
Merged
Conversation
All five were red, and in every one the behaviour was right and the check was stale. None of them is a behaviour change. - `lowers_only_first_of_two_modules_characterization` counted the substring "module " and found two: the second is inside the emitted comment "this module cannot move a value across its boundary". It counts declarations now -- a line whose first token is `module`. - `local_array_named_after_a_verilog_keyword_is_escaped` pinned the SHAPE of the lowering, `reg [15:0] \buf [0:3];` with per-element initialisers. The emitter packs the array into one vector now, so the assertion failed while the escaping it exists to protect was working. W643 is about escaping, so the requirement is stated over every occurrence: no mention of `buf` may appear unescaped, wherever the emitter puts it. Stricter than the two literals it replaces. Confirmed load-bearing by renaming the local to a non-keyword, which makes the escaping stop and the assertion fire. - `array_param_bound_from_test_block` and `test_block_emits_real_function_call` asked `gen-verilog` for a lowered test block. That backend deliberately does not lower one: it emits synthesizable RTL and names the test under "NOT LOWERED BY THIS BACKEND", because yosys turns `$display` into a `$print` cell nextpnr has no BEL to place. Test blocks are carried by `gen-verilog-for-simulation`, which emits exactly what these ask for. Asked of the other backend they could only ever fail. - The same test pinned `if (!(` for assert_eq; the emitter writes the comparison directly now, `if (((x) != (43981)))`. Stated as what a real check must do: branch on the expected value AND emit the failure path, since a comparison that cannot fail is not a check. - Two lexer conformance rows described `#` as an unrecognised character dropped without a diagnostic. That mechanism is not there -- `#` opens a comment to end of line, deliberately, measured at 42 occurrences in struct field positions across 8 specs. The rows assert the decided behaviour now, and the real hazard is written down instead of inferred from a wrong cause: a Rust attribute `#[test]` takes its whole line with it. Main binary: 1635 passed, 0 failed, 2 ignored. Refs #2735 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Refs #2743 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-27 23:06:35 UTC
Summary
Seal Status
|
An assert inside a loop over a corpus reports one defect and reads like a count -- 1 of 73. Forty of those 73 were theorems about an empty module. Three stale rows described mechanisms that no longer exist, which is worse than merely failing. Rulers break: a substring count found the emitter's own comment, and two tests pinned shapes the emitter had moved past. The suite was green while six specs regressed, so the control is a per-spec corpus diff between the before and after binaries. $? after a pipeline, for the third time. And a partial fix that cut errors 7 -> 2 while leaving a module that looks complete was reverted, not shipped. Refs #2743 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-27 23:16:55 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 #2743
Five checks were red. In every one the behaviour was right and the check was stale, so nothing here changes what the compiler does.
lowers_only_first_of_two_modules_characterizationv.matches("module ").count() == 1modulelocal_array_named_after_a_verilog_keyword_is_escapedreg [15:0] \buf [0:3];and\buf [0] =bufis escaped, wherever the emitter puts itarray_param_bound_from_test_blockgen-veriloglowers a test blockgen-verilog-for-simulation, which doestest_block_emits_real_function_callif (!(lexer_matches_its_conformance_table(2 rows)#is a dropped unknown character#opens a comment, which is what the lexer deliberately doesThree of these are rulers that broke, not code that broke:
buftest failed because the emitter started packing arrays into one vector (reg [63:0] \buf ;, indexed\buf [31:16]) instead of an unpacked array. The escaping — the thing W643 exists to protect — was working the whole time. The replacement is stricter: no mention of the keyword-named local may appear unescaped anywhere in the output, not just at two literal spellings. Confirmed load-bearing by renaming the local to a non-keyword, which stops the escaping and fires the assertion.#as "an unrecognised character DISCARDED with no diagnostic". That mechanism is not in the lexer:#runs to end of line as a comment, on purpose, and the decision carries its measurement — 42 occurrences in struct field positions across 8 specs, plus files with a.t27extension whose contents are Markdown headings. The rows had been failing while describing a cause that does not exist. They now assert the decided behaviour, and the hazard they were reaching for is written down rather than inferred:#[test]takes its whole line with it.The two
w459tests askedgen-verilogto lower a test block. That backend deliberately does not — it emits synthesizable RTL and names the test under "NOT LOWERED BY THIS BACKEND", because yosys turns each$displayinto a$printcell nextpnr has no BEL to place.gen-verilog-for-simulationemits exactly what they ask for, down toset(1, 43981);. Asked of the other backend they could only ever fail.Measured
The earlier numbers in this session were read off the main binary alone; the 12-binary figure is the honest total and is stated here so the two are not confused.
The one that remains
bitnet_layerfails, and failed before #2742 — verified by rebuilding at9fa5eedeand getting byte-identical iverilog errors. It is a real defect, not a stale check, so it is not touched here: filed as #2743 with its root cause, and with the measurement of the partial fix I implemented and reverted (errors 7 → 2, corpus acceptance unmoved at 217 / 157 / 194, andlayer2left calling a function that was refused — a module that looks complete and is not).🤖 Generated with Claude Code