trait default spec fns stopped working

[jonhnet]

In this reduced example, Trait::foo has a default body. Struct::test can't see that definition. If we copy the default body of foo into the impl Trait for Struct (commented out below), the verification succeeds.

use builtin_macros::*;

verus! {

pub trait Trait {
    spec fn hidden(&self) -> bool
        ;

    open spec fn foo(&self) -> bool
    {
        self.hidden()
    }

    proof fn test(&self);
}

pub struct Struct {
}

impl Trait for Struct {
    open spec fn hidden(&self) -> bool
    {
        true
    }

//     open spec fn foo(&self) -> bool
//     {
//         self.hidden()
//     }

    proof fn test(&self) {
        assert(self.foo() == self.hidden());
    }
}

}

2024-06-06-11-56-10.zip

(severity: I can work around this with a tedious degree of copy-pasting.)

[jonhnet]

Here is a perhaps-related issue: it's not about a trait default, but it's another case of an open spec fn's definition suddenly being unavailable in a proof. In this recording, the first two assertion failures on 441 & 443:

error: assertion failed
   --> src/marshalling/UniformSizedSeq_v.rs:441:25
    |
441 |                 assert( result.deepv().len() == result.len() );
    |                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ assertion failed

error: assertion failed
   --> src/marshalling/UniformSizedSeq_v.rs:443:21
    |
443 | ...   result.deepv() == Seq::new(result.len() as nat, |i: int| result[i].deepv()) );
    |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ assertion failed

These assertions should follow easily from the definition of deepv on Vec at Marshalling:22:

impl<DVE, Elt: Deepview<DVE>> Deepview<Seq<DVE>> for Vec<Elt> {
    open spec fn deepv(&self) -> Seq<DVE> {
        Seq::new(self.len() as nat, |i: int| self[i].deepv())
    }
}

I've had proofs working this way, but recently (perhaps with a recent verus update?) I'm encountering these new failures on what should be simple properties.

2024-06-06-14-32-31.zip

[jonhnet]

Okay, I think some sort of triggering plumbing went really haywire. Here's another very weird behavior (that happens to be in a trait impl): exec_set has a postcondition in the trait. I can assert that postcondition at the end of the impl, but I still get the postcondition not satisfied error. I can even add it as an additional ensures on the impl fn, and that ensures works, but the ensures declared on the trait still fails.

I'm pretty sure this is a Verus bug because if there's one thing I should be able to in a Dafny/Verus-like language, it's copy a failing postcondition into an assert/assume and make the postcondition error disappear.

2024-06-06-18-01-31.zip

[Chris-Hawblitzel]

Can you try with the latest commit?

[Chris-Hawblitzel]

I'll address the second problem separately. Here's a minimized repro:

trait T {
    spec fn f() -> int;
}

struct S<A>(A);

impl<A: T> T for S<A> {
    spec fn f() -> int { 3 }
}

trait U {
    type X: T;
}

proof fn test2<Z: U>() {
    assert(<S<Z::X> as T>::f() == 3);
}

I suspect that the trait bound axiom for X: T is missing.

[Chris-Hawblitzel]

Ok, the second problem should be fixed too.

[jonhnet]

Thanks for your speedy work! I just tried at the current main commit 78a7e67, and got a panic:

+ /home/jonh/verus/source/target-verus/release/verus --time src/marshalling_test.rs
thread '<unnamed>' panicked at rust_verify/src/verifier.rs:522:17:
internal error: ill-typed AIR code: error 'error 'use of undeclared function proj%%marshalling_test!marshalling.Marshalling_v.Marshal./U' in expression '(proj%%marshalling_test!marshalling.Marshalling_v.Marshal./U Self%&. Self%&)'' in expression '(tr_bound%marshalling_test!marshalling.Marshalling_v.Deepview. (proj%%marshalling_test!marshalling.Marshalling_v.Marshal./U
  Self%&. Self%&
 ) (proj%marshalling_test!marshalling.Marshalling_v.Marshal./U Self%&. Self%&) (proj%%marshalling_test!marshalling.Marshalling_v.Marshal./DV
  Self%&. Self%&
 ) (proj%marshalling_test!marshalling.Marshalling_v.Marshal./DV Self%&. Self%&)
)'
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread '<unnamed>' panicked at rust_verify/src/verifier.rs:1950:29:

2024-06-07-20-09-51.zip

[Chris-Hawblitzel]

Can you try now?

[jonhnet]

Nice! I just tried commit d1c6065: No panic, and I was able to delete all the workarounds in my code that I had marked 'issue 1157'. Things seem much happier now. Thank you!