Uninterpreted functions: postconditions vs axioms

[fpoli]

Related to #479, I found that the first program below does not work, but the second does. Is the semantics of the two encodings of rd() the same? I'm wondering if the postcondition and the domain axiom are encoded in semantically different ways or if the difference is just because of heuristics of Z3. If the latter is more reliable we might e.g. switch to it in Prusti.

Not working:

field f: Ref

function rd(): Perm
    ensures none < result && result < write
    ensures none < result * result && result * result < result // Workaround for Silicon issue #479

predicate Q(self: Ref)

predicate P(self: Ref) {
    acc(self.f, rd()) && Q(self.f)
}

method test(x: Ref)
    requires acc(P(x), rd())
{
    unfold acc(P(x), rd())  // ERROR: Unfolding P(x) might fail. There might be insufficient permission to access self.f 
    inhale acc(x.f, rd() - rd() * rd())
    assert perm(x.f) == rd()
}

Working:

field f: Ref

domain MyPermissions {
    function rd(): Perm

    axiom { none < rd() && rd() < write }
    axiom { none < rd() * rd() && rd() * rd() < rd() } // Workaround for Silicon issue #479
}

predicate Q(self: Ref)

predicate P(self: Ref) {
    acc(self.f, rd()) && Q(self.f)
}

method test(x: Ref)
    requires acc(P(x), rd())
{
    unfold acc(P(x), rd())
    inhale acc(x.f, rd() - rd() * rd())
    assert perm(x.f) == rd()
}

[marcoeilers]

The first version is encoded to something that is essentially equivalent to this:

domain Snap {
  function Snap_unit(): Snap
}
domain Internal {
  function rd_limited(s: Snap): Perm
  function rd_pre(s: Snap): Bool
  axiom {
    forall s: Snap :: { rd_limited(s) } rd_pre(s) ==> 
      let result == (rd_limited(s)) in none < result && result < write && none < result * result && result * result < result
  }
}

Then, wherever rd() is used in the Viper program, Silicon first emits the assumption rd_pre(Snap_unit()) and then encodes rd() as rd_limited(Snap_unit()).

So: There is a difference in the encoding; when using the non-domain function, Z3 will have to instantiate a quantifier to learn the postcondition. However, that quantifier is definitely triggered, and Z3 gets the same information. But I guess it's easy to imagine that some Z3 heuristics have an easier time dealing with the first scenario.

[fpoli]

Thanks! Running Z3 on the SMT2 log of the non-domain formulation, Z3 version 4.8.12 manages to prove the property while Z3 version 4.8.7 does not.