Function body is not available while checking the well-formedness of the postcondition

[pieter-bos]

Contrary to carbon, it seems the function body/result is not available when establishing the well-formedness of the postcondition:

function require_true(x: Bool): Bool
requires x
{ x }

function f(): Bool
ensures require_true(result)
{ true }

reports:

Silicon found 1 error in 2.27s:
  [0] Precondition of function require_true might not hold. Assertion result might not hold. ([email protected])

carbon finished verification successfully in 1.65s.

Of course there is something to be said for requiring contracts to be self-framing, but I am wondering about the difference with carbon :)

[mschwerhoff]

Interesting catch :-) I have the vague feeling this was observed before, and we concluded it's an incompleteness.

[marcoeilers]

I would consider this intentional behavior, especially now that Viper has opaque functions, which means that for individual function applications, the function body may not be known to the verifier. In that case, the postcondition will still be assumed and IMO should still be well-defined.