The verification specification (spec/06-contracts.md) describes three verification tiers. Tiers 1 and 3 are implemented. Tier 2 is specified but not implemented in the reference compiler.
What Tier 2 covers: Extends the decidable fragment by allowing Z3 to use hints from assert statements (treated as axioms for subsequent verification conditions) and lemma functions — pure functions with Unit bodies whose contracts establish facts for the verifier (see spec section 6.6).
Current behaviour: All contracts that Z3 cannot prove statically fall directly to Tier 3 (runtime check with a warning). The vera verify --json output never reports tier2_hints.
Expected behaviour after this issue:
- assert(expr) statements in function bodies are passed as axioms to Z3 when verifying subsequent contracts
- Calls to lemma functions cause the lemma postcondition to be assumed as an axiom
- vera verify --json reports tier2_hints count
Spec references: sections 6.3.2, 6.4.3, 6.6, 6.8
The verification specification (spec/06-contracts.md) describes three verification tiers. Tiers 1 and 3 are implemented. Tier 2 is specified but not implemented in the reference compiler.
What Tier 2 covers: Extends the decidable fragment by allowing Z3 to use hints from assert statements (treated as axioms for subsequent verification conditions) and lemma functions — pure functions with Unit bodies whose contracts establish facts for the verifier (see spec section 6.6).
Current behaviour: All contracts that Z3 cannot prove statically fall directly to Tier 3 (runtime check with a warning). The vera verify --json output never reports tier2_hints.
Expected behaviour after this issue:
Spec references: sections 6.3.2, 6.4.3, 6.6, 6.8