Definitions of function applications in postconditions of recursively called functions available too late
marcoeilers opened this issue · 1 comments
marcoeilers commented
The following verifies in Carbon but not in Silicon:
function fac(i: Int): Int
ensures ge(result, 1)
{
i <= 1 ? 1 : i * fac(i - 1)
}
function ge(i1: Int, i2: Int): Bool
{
i1 >= i2
}
The issue is that the precondition propagation axiom for fac
(which states that if the precondition of fac
is satisfied, then the precondition of ge
in its postcondition is also satisfied) is not available while verifying the body of fac
, and thus the definition of ge
cannot be used when learning the postcondition of the recursive call.
marcoeilers commented
Fixed in PR #745