Problems with the trace option

[msaaltink]

sui-prover --trace can give some strange error locations, and can disagree with both plain sui-prover and with Boogie. This does not seem to occur with very simple assertions, but in this example, the quantifier is enough (on my machine) to trigger the issue.

module tracing::tracing;

use prover::prover::{ensures, forall, requires};

#[ext(pure)]
fun is_small(i: u64, v: &vector<u64>): bool {
    i >= v.length() || v[i] <= i
}

fun foo(x: u64): u64 {
    x - 1
}

#[spec(prove, boogie_opt=b"vcsSplitOnEveryAssert",)]
fun baz(v: &mut vector<u64>) {
    requires(v.length() > 20);
    requires(forall!(|i| is_small(*i, v)));
    let v0 = v[0];
    let v2 = v[2]+100;
    let x = foo(v[v0]);
    let y = v.pop_back()-2;
    ensures(forall!(|i| is_small(*i, v)));
}

Running sui-prover gives

✅ funs_abort_check
🔄 tracing::baz_Check
error: code should not abort
   ┌─ ./sources/tracing.move:11:7
   │
11 │     x - 1
   │       ^
   │
   =     at ./sources/tracing.move:15: baz
   =         v =
   =           <? List([Literal("Vec_21333"), List([Literal("_"), List([Literal("as-array")]), List([Literal("k!17")])]), Literal("21")])>
   =     at ./sources/tracing.move:16: baz
   =         v0#1#0 = 0u64
   =     at ./sources/tracing.move:19: baz
   =         x = 0u64
   =     at ./sources/tracing.move:11: foo

❌ tracing::baz_Check (0.9s)
✅ tracing::baz_Assume
✅ tracing::baz_SpecNoAbortCheck

However, sui-prover --trace gives something different:

🔄 funs_abort_check
    ⊢  $0_tracing_is_small$no_abort_check$verify
✅ funs_abort_check
🔄 tracing::baz_Check
    ⊢  $0_tracing_baz$verify
    📌 split 12/12: code should not abort (at ./sources/tracing.move:22)
    ❌ split 7/12: code should not abort (at ./sources/tracing.move:11)
error: unexpected boogie output: `Parsing output/tracing::baz_Check.bpl
Coalescing blocks...
Inlining... ..`
  ┌─ <unknown>:1:1
  │
1 │ <unknown>
  │ ^^^^^^^^^

error: code should not abort
   ┌─ ./sources/tracing.move:11:7
   │
11 │     x - 1
   │       ^
   │
   =     at ./sources/tracing.move:15: baz
   =         v =
   =           <? List([Literal("Vec_21333"), List([Literal("_"), List([Literal("as-array")]), List([Literal("k!17")])]), Literal("21")])>
   =     at ./sources/tracing.move:16: baz
   =         v0#1#0 = 0u64
   =     at ./sources/tracing.move:19: baz
   =         x = 0u64
   =     at ./sources/tracing.move:11: foo

❌ tracing::baz_Check (1.0s)
🔄 tracing::baz_Assume
✅ tracing::baz_Assume
🔄 tracing::baz_SpecNoAbortCheck
    ⊢  $0_tracing_baz$verify
    📌 split 12/12: code should not abort (at ./sources/tracing.move:22)
    ❌ split 7/12: code should not abort (at ./sources/tracing.move:11)
error: unexpected boogie output: `Parsing output/tracing::baz_SpecNoAbortCheck.bpl
Coalescing blocks...
 ..`
  ┌─ <unknown>:1:1
  │
1 │ <unknown>
  │ ^^^^^^^^^

❌ tracing::baz_SpecNoAbortCheck (1.1s)

So why are we now seeing errors for the SpecNoAbortCheck?

Why are we seeing unexpected Boogie output?

Moreover, the flagged line 22 is the final ensures(forall!(|i| is_small(*i, v))); of function baz, and is not where the error lies. On larger specifications I see more examples of this, where an error reported under --trace is nowhere near the actual problem.

[andreistefanescu]

fixed in #527.