Discovered while completing the #597 walker-completeness audit (PR for that ships v0.0.151).
vera/smt.py::translate_expr currently lists three Expr subclasses in its WALKER_COVERAGE checklist as latent gaps:
| Subclass |
Gap |
| FloatLit |
Z3 supports floats natively. Contracts could embed float predicates if the parser allowed them. |
| ArrayLit |
SMT array theory exists. Contract grammar would need extension to accept array-literal predicates. |
| IndexExpr |
requires(@Array.0[0] > 0) is a useful contract shape. Same grammar-extension dependency as ArrayLit. |
Each requires:
- Extending the contract grammar (
grammar.lark) to accept the predicate shape.
- Adding a translation case to
SmtContext.translate_expr returning a Z3 expression.
- Type-checker rules ensuring the predicate's structure stays well-formed.
Each is mostly independent of the others; can be tackled one at a time.
Today these are masked by the contract grammar — the parser rejects predicates containing these shapes before the SMT translator ever sees them. The audit surfaces them so the gap is visible for future work rather than relying on the parser rejection forever.
Discovered in: PR #597 walker-completeness audit (v0.0.151).
Pairs with: #427 (Tier 2 verification — both would benefit from richer SMT coverage).
Discovered while completing the #597 walker-completeness audit (PR for that ships v0.0.151).
vera/smt.py::translate_exprcurrently lists threeExprsubclasses in its WALKER_COVERAGE checklist as latent gaps:requires(@Array.0[0] > 0)is a useful contract shape. Same grammar-extension dependency as ArrayLit.Each requires:
grammar.lark) to accept the predicate shape.SmtContext.translate_exprreturning a Z3 expression.Each is mostly independent of the others; can be tackled one at a time.
Today these are masked by the contract grammar — the parser rejects predicates containing these shapes before the SMT translator ever sees them. The audit surfaces them so the gap is visible for future work rather than relying on the parser rejection forever.
Discovered in: PR #597 walker-completeness audit (v0.0.151).
Pairs with: #427 (Tier 2 verification — both would benefit from richer SMT coverage).