We do not always get determinism for uninterpreted functions

[msaaltink]

I expected this proof to work:

#[ext(pure)]
fun foo(x: &vector<u8>): u8 {
    if (x.length() > 0) x[0] else 0
}

#[spec(prove, uninterpreted=foo)]
fun test(x: &vector<u8>, y: &vector<u8>) {
    requires(x == y);
    ensures(foo(x) == foo(y));
}

but it does not:

error: prover::ensures does not hold
    ┌─ ./sources/playground.move:10:5
    │
675 │     ensures(foo(x) == foo(y));
    │     ^^^^^^^^^^^^^^^^^^^^^^^^^
    │
    =     at ./sources/playground.move:8: test
    =         x =
    =           <? List([Literal("Vec_21333"), List([Literal("_"), List([Literal("as-array")]), List([Literal("k!12")])]), Literal("0")])>
    =         y =
    =           <? List([Literal("Vec_21333"), List([Literal("_"), List([Literal("as-array")]), List([Literal("k!13")])]), Literal("0")])>
    =     at ./sources/playground.move:674: test

As can be seen, in this example the vectors actually are equal so it seems incredible that the proof fails.

In the BPL we see

function $0_playground_foo$pure(_$t0: Vec (int)) returns ($ret0: int);

and later, in the procedure to be verified

    $t2 := $IsEqual'vec'u8''($t0, $t1);
    call $0_prover_requires($t2);

    $t3 := $0_playgound_foo$pure($t0);
    assume $IsValid'u8'($t3);
    $t4 := $0_playgound_foo$pure($t1);
    assume $IsValid'u8'($t4);
    $t5 := $IsEqual'u8'($t3, $t4);
    assert {:msg "assert_failed(255,12768,12793): prover::ensures does not hold"} $t5;

So I think this issue is this: the assumption $IsEqual'vec'u8''($t0, $t1); which asserts the two vectors to have the same length and same value for valid indices, does not imply that they are equal. So there is no reason for the prover to conclude that foo$pure($t0) equals foo$pure($t1).

This is unfortunate in cases where a complex function is working on a complex type and you want to have the function uninterpreted in a proof, as we no longer get determinism for these functions.

Luckily there is a work-around. In the example I can add the missing axiom

#[spec_only(axiom)]
fun foo_is_deterministic(x: &vector<u8>, y: &vector<u8>): bool {
    if (x == y) foo(x) == foo(y) else true
}

However, it may not be obvious to users (as it was not obvious to me for some time in my actual proof) that the lack of an axiom like this is making their proofs fail. Perhaps it could be added automatically when a function is uninterpreted.