Checking the equivalence of two functions with side effects

[Timmmm]

The SMT $counterexample feature can be used to check the equivalence of two pure functions quite easily:

$counterexample
function prop(foo : bits(128)) -> bool = a(foo) == b(foo)

That works fine, but how would you do this for impure functions that write to registers? For example:

register v1 : bits(128)
register v2 : bits(128)
register v3 : bits(128)

function vector_and() -> unit = {
    v3 = v2 & v1;
}

function vector_and_2() -> unit = {
    foreach (i from 0 to 100) {
        v3[i] = if v2[i] == bitone & v1[i] == bitone then bitone else bitzero;
    }
}

$counterexample
function prop() -> bool = {
  vector_and() == vector_and_2()
}

Obviously this isn't correct because it's just checking () == (). Is there a way to make it actually work? Maybe this can be done with the Coq output?

[Alasdair]

Would be possible to do, but would probably require a new way of asking for this to be checked because vector_and() == vector_and_2() will be evaluated left to right meaning the update to v3 will take place twice. We could have something like:

$equivalent vector_and vector_and_2

as a separate top-level check it could do

[Alasdair]

There's also the very manual:

let (i1, i2, i3) = (v1, v2, v3);
vector_and();
let (out1, out2, out3) = (v1, v2, v3);
(v1, v2, v3) = (i1, i2, i3)
vector_and_2();
out1 == v1 & out2 == v2 & out3 == v3

Not sure if there's any good way to make that more automatic though.

[Timmmm]

$equivalent vector_and vector_and_2

This would be very nice!