Unchecked annotation not respected for inlined postconditions

[gsps]

For @synthetic functions we re-assert postconditions at inlined call sites (see

stainless/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala

Line 114 in 3da44e4

Let(postVal, annotated(post, Unchecked),

).

The particular way in which this is done, i.e., by let-binding the post condition and then asserting the bound variable subverts existing machinery for leaving certain parts of postconditions unchecked. Namely, conjuncts annotated with @unchecked are filtered out in TypeChecker (see

stainless/core/src/main/scala/stainless/verification/TypeChecker.scala

Line 1006 in 3da44e4

val filtered = filterUnchecked(e)

), but only if they occur directly in the VC to be checked. The indirection (let pc = @unchecked cond; assert(pc) instead of assert(@unchecked cond)) leads to cond being check nonetheless.

This leads to an issue with correct-by-construction postconditions introduced in lowering phases, such as TypeEncoding. In particular, for generic functions f[T](x: T): T we lower to f(T: Object => Boolean, x: { v: Object | T(v) }): { v: Object | T(v) } where f's postcondition has been strengthened by ... && @unchecked res == f'(x) referring to auxiliary function f'(x: Object): Object = ???. That postcondition holds by construction, but cannot be proven automatically, so the above-described bug leads to spurious counter-examples.

See also #1125 for a related discussion on how to control the unchecked behavior in a more fine-grained way. As far as I can tell the split in that PR won't help us in this case, unfortunately, but I'll try to have a closer look.