Missing constraints for uninterpreted functions

[msaaltink]

When a function is uninterpreted, its value is not always known to be valid. Here are two simple examples:

#[ext(pure)]
fun sub1(x: u8): u8 {
    if (x > 0) x-1 else 0
}

fun apply() {
    assert!(sub1(1) <= 255, 1);
}

#[spec(prove, uninterpreted=sub1)]
fun apply_spec() {
    apply()
}

The sui-prover does not see that the assertion can never fail:

error: code should not abort
    ┌─ ./sources/playground.move:221:5
    │
221 │     assert!(sub1(1) <= 255, 1);
    │     ^^^^^^^^^^^^^^^^^^^^^^^^^^
    ·
226 │     apply()
    │     ------- abort happened here with code 0x1
    │
    =     at ./sources/playground.move:226: apply_spec
    =         ABORTED

So I suspect that $IsValid'u8' has not been asserted for the result of sub1.

A similar thing happens for vectors:

#[ext(pure)]
fun vex(v: vector<u8>): vector<u8> {
    v
}

fun user() {
    let u = vector[1];
    assert!(vex(u).length() >= 0, 1);
}
    
#[spec(prove, uninterpreted=vex)]
fun user_spec() {
    user();
}

where the prover again claims that the abort can happen:

error: code should not abort
    ┌─ ./sources/playground.move:236:5
    │
236 │     assert!(vex(u).length() >= 0, 1);
    │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    ·
241 │     user();
    │     ------ abort happened here with code 0x1
    │
    =     at ./sources/playground.move:241: user_spec
    =         ABORTED

[andreistefanescu]

fixed in #525.