The `decreases()` contract clause is parsed and stored in the AST but the verifier never checks that the termination metric actually decreases across recursive calls. All `decreases` clauses fall back to Tier 3 with a warning.
Current behaviour (`vera/verifier.py:436-450`):
Every `decreases` clause produces a Tier 3 warning: "Termination metric cannot be statically verified yet."
Expected behaviour:
For recursive functions with a `decreases(expr)` clause, the verifier should check that `expr` is strictly smaller at each recursive call site, using Z3 to prove the decrease. This would allow recursive functions like `factorial` to have their termination statically verified.
Complexity: Requires identifying recursive call sites within the function body, substituting the callee arguments into the decreases expression, and proving that the substituted expression is strictly less than the original.
The `decreases()` contract clause is parsed and stored in the AST but the verifier never checks that the termination metric actually decreases across recursive calls. All `decreases` clauses fall back to Tier 3 with a warning.
Current behaviour (`vera/verifier.py:436-450`):
Every `decreases` clause produces a Tier 3 warning: "Termination metric cannot be statically verified yet."
Expected behaviour:
For recursive functions with a `decreases(expr)` clause, the verifier should check that `expr` is strictly smaller at each recursive call site, using Z3 to prove the decrease. This would allow recursive functions like `factorial` to have their termination statically verified.
Complexity: Requires identifying recursive call sites within the function body, substituting the callee arguments into the decreases expression, and proving that the substituted expression is strictly less than the original.