Finding
Rule names in spec/10-grammar.md EBNF blocks and vera/grammar.lark have nominal drift. Live state at HEAD 08c1197:
- Spec EBNF rules: 82
- Lark rules: 65
- Common: 59
The bulk of "spec-only" rules are expression-precedence ladders (add_expr, cmp_expr, or_expr, unary_expr, primary_expr, etc.) that Lark inlines via alternation. Those are a deliberate notational choice each tool optimises for; they should be documented in the spec as "represented inline in Lark" but not renamed.
The genuine drift is a small subset of names:
| Spec-only |
Lark equivalent |
Note |
assert_stmt |
assert_expr |
assert/assume return values; the implementation chose _expr. Spec should follow. |
assume_stmt |
assume_expr |
Same. |
module_call |
(no rule) |
Same construct as qualified_call; spec uses both names. |
qualified_call |
(no rule) |
Same. |
| (no rule) |
effect_set, pure_effect, with_clause |
Lark sub-rules with no spec counterpart. Either inline in spec or add to spec EBNF. |
program |
start |
Lark requires start; spec name is conventional. Document as known allowlist exception. |
Suggested fix
A one-pass reconciliation:
- Decide on
_expr vs _stmt for assert/assume and update the spec to match the implementation (the grammar uses _expr, and they return values, so this is the right call)
- Rename
qualified_call → module_call throughout the Lark grammar (DESIGN.md text uses "module-qualified", so module_call is the more natural name)
- Either inline the Lark-only sub-rules (
effect_set, pure_effect, with_clause) into their parents or add them as sub-rules in the spec EBNF
- Add
scripts/check_grammar_alignment.py that re-extracts the rule sets from both files and asserts they agree modulo a documented allowlist (currently {program ↔ start} and the inline-expression-precedence convention)
Scope decision
This issue is scoped to the nominal renames + check script. The expression-precedence "drift" (add_expr / cmp_expr / etc. existing in spec but not Lark) is a deliberate notational choice and out of scope — Lark uses operator-precedence inlining; spec uses precedence ladders. Both notations are correct; reconciling them would be a notational ideology change, not a hygiene fix.
Acceptance criteria
python scripts/check_grammar_alignment.py returns zero with no allowlist exceptions other than program ↔ start and the documented expression-precedence convention- Script runs as a pre-commit hook and in CI
- Spec and Lark agree on assert/assume naming (use
_expr)
- Spec and Lark agree on module-qualified-call naming (use
module_call)
- Lark-only sub-rules (
effect_set, pure_effect, with_clause) either appear in the spec or are inlined in Lark
Estimated effort
Half a day for the renames + check script.
Origin
Surfaced by a strategic compiler review on 2026-05-18 (v0.0.155). Marked P2 (hygiene). Counts independently verified before filing: 82 spec rules / 65 Lark rules with 59 in common; the headline numerical gap is dominated by the precedence-ladder notational difference rather than genuine drift.
Finding
Rule names in
spec/10-grammar.mdEBNF blocks andvera/grammar.larkhave nominal drift. Live state at HEAD08c1197:The bulk of "spec-only" rules are expression-precedence ladders (
add_expr,cmp_expr,or_expr,unary_expr,primary_expr, etc.) that Lark inlines via alternation. Those are a deliberate notational choice each tool optimises for; they should be documented in the spec as "represented inline in Lark" but not renamed.The genuine drift is a small subset of names:
assert_stmtassert_exprassert/assumereturn values; the implementation chose_expr. Spec should follow.assume_stmtassume_exprmodule_callqualified_call; spec uses both names.qualified_calleffect_set,pure_effect,with_clauseprogramstartstart; spec name is conventional. Document as known allowlist exception.Suggested fix
A one-pass reconciliation:
_exprvs_stmtfor assert/assume and update the spec to match the implementation (the grammar uses_expr, and they return values, so this is the right call)qualified_call→module_callthroughout the Lark grammar (DESIGN.md text uses "module-qualified", somodule_callis the more natural name)effect_set,pure_effect,with_clause) into their parents or add them as sub-rules in the spec EBNFscripts/check_grammar_alignment.pythat re-extracts the rule sets from both files and asserts they agree modulo a documented allowlist (currently{program ↔ start}and the inline-expression-precedence convention)Scope decision
This issue is scoped to the nominal renames + check script. The expression-precedence "drift" (
add_expr/cmp_expr/ etc. existing in spec but not Lark) is a deliberate notational choice and out of scope — Lark uses operator-precedence inlining; spec uses precedence ladders. Both notations are correct; reconciling them would be a notational ideology change, not a hygiene fix.Acceptance criteria
python scripts/check_grammar_alignment.pyreturns zero with no allowlist exceptions other thanprogram ↔ startand the documented expression-precedence convention_expr)module_call)effect_set,pure_effect,with_clause) either appear in the spec or are inlined in LarkEstimated effort
Half a day for the renames + check script.
Origin
Surfaced by a strategic compiler review on 2026-05-18 (v0.0.155). Marked P2 (hygiene). Counts independently verified before filing: 82 spec rules / 65 Lark rules with 59 in common; the headline numerical gap is dominated by the precedence-ladder notational difference rather than genuine drift.