Function applications with `unfolding` not inferred to be equal

[bobismijnnaam]

I'm using functions to unfold predicates where necessary. Unfortunately, it seems that silicon does not notice that two fields dereferences are equal, even though their object references are equal. In the example below, I'd expect all asserts to verify, but the last two don't.

field f: Int

predicate wrap(r: Ref, obj: Ref) {
    acc(obj.f)
}

function read_f(r: Ref, obj: Ref): Int 
requires acc(wrap(r, obj), wildcard)
{
    unfolding acc(wrap(r, obj), wildcard) in obj.f
}

method m(r1: Ref, r2: Ref, obj: Ref) 
requires acc(wrap(r1, obj), 1/2)
requires acc(wrap(r2, obj), 1/2)
{
    // Makes it verify:
    // assert 
    //     unfolding acc(wrap(r1, obj), wildcard) in 
    //     unfolding acc(wrap(r2, obj), wildcard) in obj.f == obj.f

    // Makes it verify:
    // assert 
    //     unfolding acc(wrap(r1, obj), wildcard) in 
    //     unfolding acc(wrap(r2, obj), wildcard) in 
    //         read_f(r1, obj) == read_f(r2, obj)

    // Makes it verify:
    // unfold acc(wrap(r1, obj), 1/2)
    // unfold acc(wrap(r2, obj), 1/2)
    // fold acc(wrap(r1, obj), 1/2)
    // fold acc(wrap(r2, obj), 1/2)

    // Doesn't verify
    assert (unfolding acc(wrap(r1, obj), wildcard) in obj.f) 
        == 
        (unfolding acc(wrap(r2, obj), wildcard) in obj.f)

    // Doesn't verify
    assert 
        read_f(r1, obj) == read_f(r2, obj)
}

It seems that silicon really needs to observe both predicates open at the same time, before it concludes that read_f(r1, obj) == read_f(r2, obj). Carbon verifies all asserts. Is this an inherent limitation in silicon, or could it be improved?

[marcoeilers]

I'd say this is pretty much an inherent limitation of Silicon's heap model. I think (can't try right now) the separate unfoldings should also work if you have separate permission to obj.f in the method (so e.g. 1/3 permission to obj.f directly, and 1/3 to each of the predicates) (the function version shouldn't work even in that scenario I think). But without that, there is just nothing representing the value of obj.f that one could assume the unfolding's values to be equal to, whereas Carbon can always refer to that heap location internally.

[bobismijnnaam]

Thanks for your quick response! Unfortunate, but it makes sense.