v0.0.5 — Stronger Problems
Strengthens problem descriptions and postconditions to improve benchmark quality.
Changed
Explicit De Bruijn slot ordering in descriptions (issue #13):
- VB-T4-002 (GCD): description states @Nat.0=b (rightmost), @Nat.1=a
- VB-T4-004 (power): description states @Nat.0=exp (rightmost), @Nat.1=base
- VB-T5-003 (safe_div): description states slot mapping for both functions
Stronger postconditions that catch logic bugs (issue #14):
| Problem | New postcondition | Z3 tier |
|---|---|---|
| multiply(a,b) | result == a * b |
Tier 1 |
| div_natural(a,b) | result * b <= a AND (result+1) * b > a |
Tier 1 |
| sum_to_n(n) | result == n * (n+1) / 2 |
Tier 1 |
| gcd(a,b) | result <= a || b > 0 |
Tier 1 |
| counter() | result == 3 |
Tier 3 |
| state_double(x) | result == x * 2 |
Tier 3 |
| state_max(n) | result == n |
Tier 3 |
Tier 4 postconditions are Z3-proved. Tier 5 fall to runtime due to effect handlers.
Impact
A slot-swapped GCD or multiply that previously passed vera verify (because ensures(@Nat.result >= 0) is trivially true) will now fail verification. This makes the verify@1 metric more meaningful.