Summary

Audit every isinstance(expr, ast.X) dispatch chain in the codebase and verify each one explicitly handles or explicitly skips every Expr subclass. Build a per-walker checklist of every Expr in vera/ast.py and document the disposition in code comments.

Discovered the need while diagnosing #588: _walk_free_vars in vera/wasm/closures.py was missing eight Expr subclass branches (IndexExpr, ArrayLit, InterpolatedString, HandleExpr, AssertExpr, AssumeExpr, ForallExpr/ExistsExpr, ModuleCall). When the walker hit one of those expressions inside a closure body, it silently fell through, missed any captured slot references inside the sub-expressions, and the closure-lift produced a broken WAT module that failed validation or trapped at runtime.

The fix was mechanical (~50 lines), but the bug class is systemic: the original _walk_free_vars walked the obvious shapes (BinaryExpr, FnCall, MatchExpr) and missed the long tail of less-common expression types. We don't know how many other walkers in the codebase have the same shape of incompleteness.

Why now

The stabilisation discussion identified this as an unknown: was _walk_free_vars the worst offender, or is it representative? We have at least these AST-walker-shaped functions in the codebase:

• vera/wasm/closures.py::_walk_free_vars — recently audited, was the trigger
• vera/wasm/context.py::_is_void_expr — handles QualifiedCall, UnitLit, FnCall, AssertExpr/AssumeExpr, MatchExpr, IfExpr, Block, HandleExpr. Missing IndexExpr / ArrayLit / etc.? Unknown.
• vera/wasm/inference.py::_infer_expr_wasm_type — large dispatch chain
• vera/wasm/inference.py::_infer_vera_type — parallel dispatch chain
• vera/codegen/... translate_expr family
• vera/checker.py synth/check dispatch
• vera/verifier.py SMT encoding dispatch
• vera/ast.py::format_expr — pretty-printer dispatch (less critical — format failures are visible)

Each of these is a candidate for the same bug class. Until audited, "the walkers are complete" is unverified.

Proposed approach

For each walker:

1. Enumerate every Expr subclass in vera/ast.py that the walker COULD plausibly receive
2. Cross-reference against the walker's if isinstance(expr, ...) chain
3. For each subclass, classify as one of:
   • Handled (walker has an explicit branch)
   • Intentionally ignored (e.g. literals have no sub-expressions to walk; document with a comment)
   • Cannot occur (e.g. OldExpr / NewExpr only appear in contracts, not closure bodies; document the invariant)
   • MISSING (file a bug, add the branch)
4. Add a checklist comment at the top of each walker enumerating every Expr subclass and how it's handled

Example (post-fix shape for _walk_free_vars in #588):

# AST coverage — every Expr subclass listed here, with disposition:
#   SlotRef          → leaf case, captures recorded if outer-scope
#   BinaryExpr       → walks left + right
#   IndexExpr        → walks collection + index   (added #588)
#   ArrayLit         → walks each element         (added #588)
#   InterpolatedString → walks Expr parts         (added #588)
#   ...
#   IntLit/BoolLit/UnitLit/FloatLit → no sub-expressions, intentionally skipped
#   OldExpr/NewExpr → only in contracts, never in closure bodies
def _walk_free_vars(self, expr, ...):
    ...

The checklist comment makes the next missing-branch bug a visible omission rather than a silent one. A new Expr subclass added to ast.py will hit the comment first when someone audits the dispatch.

Tooling option

A small scripts/check_walker_coverage.py that:

• Parses vera/ast.py to extract all Expr subclasses
• Parses each known walker function to extract the isinstance(..., ast.X) calls
• Reports walkers that don't mention every Expr subclass

Run this in pre-commit. If a new Expr subclass is added to AST, every walker is forced to either handle it or explicitly skip it (with a comment). This is the durable form of the audit — the per-walker checklist comment is the human-readable part; the script is the automated guard.

This is similar to how _TRAP_FIX_PARAGRAPHS in vera/codegen/api.py is asserted complete by test_fix_paragraph_table_covers_every_known_kind in tests/test_runtime_traps.py — the test fails if a new trap kind is added without a Fix paragraph.

Acceptance

• Audit complete for every walker in the table above. Per-walker outcome: either "all branches accounted for" (with checklist comment) or "missing branches filed as separate bugs".
• Optional but recommended: scripts/check_walker_coverage.py integrated into pre-commit.
• Any missing-branch bugs found during the audit are filed and fixed before this issue closes.
• Walker-coverage convention documented in vera/README.md (the compiler architecture doc) so future walkers follow it.

Out of scope

• Refactoring walkers into a visitor-pattern base class — too invasive; the per-walker checklist + script approach gives most of the benefit without the rewrite cost.
• Auditing handlers in tests/ — test code is allowed to handle a subset of expressions.
• Auditing pretty-printers (format_expr) — failure mode is "string output is wrong", not "compiled artifact is broken". Lower priority.

Related

• #588 — the trigger; closure-lift's _walk_free_vars was missing 8 branches.
• #584 — _is_void_expr was missing FnCall to user-Unit-returning fns. Same shape of bug from the same walker class.
• The stabilisation discussion that generated this issue.