Unsound recursive function encoding with wildcard permissions

[ArquintL]

Having a recursive, terminating function that takes wildcard permissions to the same heap location for all recursive calls seems to trigger an unsoundness.

// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

field f: Int

predicate Mem(x: Ref)
{
    acc(x.f) && 0 <= x.f
}

function recurse(x: Ref, idx: Int): Int
requires acc(Mem(x), wildcard)
requires unfolding acc(Mem(x), wildcard) in 0 <= idx && idx <= x.f
decreases unfolding acc(Mem(x), wildcard) in x.f - idx
{
    unfolding acc(Mem(x), wildcard) in idx == x.f ? 42 : recurse(x, idx + 1)
}

method fooUnsound(x: Ref)
requires Mem(x)
ensures  Mem(x)
ensures  false // succeeds unexpectedly
{
    var oldResult: Int := recurse(x, 0)
    unfold Mem(x)
    x.f := x.f + 1
    fold Mem(x)
    var newResult: Int := recurse(x, 0) // this call triggers the unsoundness
}

Note that replacing all wildcard permission amounts by 1/1 does not result in the unsoundness, i.e., the postcondition fails as expected. Strangely, the type checker warns about 1/1 being treated like wildcard, which is however clearly not the case!

Here is a slightly longer example using sequences but involving the same unsoundness:
unsound.vpr.zip

[ArquintL]

Marking this as critical since this issue is related to the key new feature in the upcoming release

[ArquintL]

Silicon (ea0efee) exhibits this unsoundness while Carbon does not

[ArquintL]

The same unsoundness also occurs with --respectFunctionPrePermAmounts

[ArquintL]

Introducing another reference seems to result in non-termination of Silicon

// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

field f: Int

predicate Mem(x: Ref)
{
    acc(x.f) && 0 <= x.f
}

function recurse(x: Ref, idx: Int): Int
requires acc(Mem(x), wildcard)
requires unfolding acc(Mem(x), wildcard) in 0 <= idx && idx <= x.f
decreases unfolding acc(Mem(x), wildcard) in x.f - idx
{
    unfolding acc(Mem(x), wildcard) in idx == x.f ? 42 : recurse(x, idx + 1)
}

method fooUnsound(x: Ref, y: Ref)
requires Mem(x) && Mem(y)
ensures  Mem(x)
ensures  false // succeeds unexpectedly
{
    var oldResult: Int := recurse(x, 0)
    unfold Mem(x)
    x.f := x.f + 1
    fold Mem(x)
    var newResult: Int := recurse(y, 0) // this call triggers the unsoundness
}