Unsoundness: Wildcards and/or taken permission variables in function axioms are constrained independently of arguments

[marcoeilers]

So the following verifies (all three assert falses go through) with MCE (haven't tested without yet) because either the wildcard variables or the amount-taken-from-a-specific-chunk-during-wildcard-consume-variables are constrained once-and-for-all, they should be functions instead s.t. we can constrain applications of those functions for specific arguments.

field f: Int

function foo1(x: Ref, y: Ref, z: Ref, b: Bool): Int
  requires b ? acc(x.f) : acc(y.f)
  requires b ? z == x : z == y
  requires bar(z) > 2
{5}

function foo2(x: Ref, y: Ref, z: Ref, b: Bool): Int
  requires acc(x.f) && acc(y.f)
  requires z == x || z == y
  requires bar(z) > 2
{5}

function foo3(x: Ref, y: Ref, z: Ref, b: Bool): Int
  requires acc(x.f, b ? write : none) && acc(y.f, b ? none : write)
  requires (z == x && b && z != y) || (z == y && !b && z != x)
  requires bar(z) > 2
{5}


function bar(x: Ref): Int
  requires acc(x.f, wildcard)
{
  5
}

method caller1(x: Ref, y: Ref)
{
  inhale acc(x.f) && acc(y.f)
  var res: Int
  res := foo1(x, y, x, true)
  res := foo1(x, y, y, false)
  assert false
}

method caller2(x: Ref, y: Ref)
{
  inhale acc(x.f) && acc(y.f)
  var res: Int
  res := foo2(x, y, x, true)
  res := foo2(x, y, y, false)
  assert false
}

method caller3(x: Ref, y: Ref)
{
  inhale acc(x.f) && acc(y.f)
  var res: Int
  res := foo3(x, y, x, true)
  res := foo3(x, y, y, false)
  assert false
}

[marcoeilers]

Same issue in quantifier evaluation, vars should be functions that depend on quantified variables. The following verifies:

field f: Int

method foo(x: Ref, y: Ref)
{
  inhale acc(x.f) && acc(y.f)
  
  var myseq: Seq[Ref] := Seq(x, y)

  assert forall r: Ref :: r in myseq ==> fn(r) > 2

  assert false


}

function fn(x: Ref): Int
  requires acc(x.f, wildcard)
{5}

[marcoeilers]

And the problem probably doesn't exist without MCE because I need disjunctive aliasing to make it happen at all, and also the amount-taken-from-a-specific-chunk-during-wildcard-consume-variables only exist with MCE.

[marcoeilers]

Fixed in PR #895