error: expression has mode proof, expected mode exec when using pervasive::map

[marshtompsxd]

Hi Verus developers,

Thanks for building verus and I am currently using it to verify some programs I wrote before. But I encountered some confusing errors and need some help from you.

I was running verus (./tools/rust-verify.sh rust_verify/example/myexample.rs) on the following program:

#[allow(unused_imports)]
mod pervasive;
use pervasive::map::*;

#[exec]
pub enum Myenum {
    S1,
    S2,
}

#[exec]
pub fn myfun(map: Map<i32, i32>) -> Myenum {
    if map.dom().contains(10) {
        return Myenum::S1;
    } else {
        return Myenum::S2;
    }
}

#[exec]
fn main() { }

and verus reports the error

error: expression has mode proof, expected mode exec
  --> rust_verify/example/mini.rs:14:16
   |
14 |         return Myenum::S1;
   |                ^^^^^^^^^^

error: aborting due to previous error

If I remove the usage of Map, the error will disappear. I am confused about why this error can happen as I have annotated every function and every enum with exec as shown in the code, and why it is related to the pervasive::map. I have read this doc: https://github.com/secure-foundations/verus/blob/main/source/docs/design/modes.md but still do not know what is the root cause of the error. Could you please let me know what is the best way to address this error?

Thank you

[parno]

Thanks for your interest in the project! The issue is that map is only intended for specifications. In your example, you're using dom, which is defined via fndecl: https://github.com/secure-foundations/verus/blob/fdb8c37d1e409e5eb51fcb7ca5533c4cfa729d69/source/pervasive/map.rs#L29 which declares dom() to be [#spec]: https://github.com/secure-foundations/verus/blob/fdb8c37d1e409e5eb51fcb7ca5533c4cfa729d69/source/builtin_macros/src/fndecl.rs#L7 Similarly, the Set that dom returns has contains declared as spec.

Eventually, we should have an exec map (e.g., wrapping HashMap) which would be specified in terms of map, in a similar way to how the exec vec is defined in terms of the spec seq. Verus is still very much a work in progress!

[marshtompsxd]

Hi @parno , thanks for your reply!

I tried to find some workaround and interestingly verus does not report any error if I change myfun to the following:

#[exec]
pub fn myfun(map: Map<i32, i32>) -> Myenum {
    let mut b = false;
    if map.dom().contains(10) {
        b = true;
    }
    if b {
        return Myenum::S1;
    }
    else {
        return Myenum::S2;
    }
}

Is this a valid workaround that allows us to return different values according to map, or it is actually a bug?

[Chris-Hawblitzel]

Good catch -- that's a bug. This should fix it: ef62f0d

[tjhance]

Should we also make it an error to use Map (and other spec/proof-only types) as an exec variable in the first place?

[Chris-Hawblitzel]

Ultimately, the error for something like fn myfun(map: Map<i32, i32>) will be that you can't actually allocate an exec mode Map<i32, i32> value, so you can't call myfun. We might also try to flag map: Map<i32, i32> as an error directly, as an additional sanity check. It may be hard to be complete with this check, though, since you can declare something like fn myfun<A>(map: A) and then instantiate A with Map<i32, i32>. Catching the instantiation of A = Map<i32, i32>, and similar instantiations, might require more elaborate traits. Maybe a warning would be good enough, in cases where a parameter or datatype field clearly can never be instantiated?

[tjhance]

I didn't think about the generics, but I think error/warning in this situation will always be helpful and result in a more relevant span (and help new users in situations like this one). I've frequently found it surprising when these errors wouldn't caught and I would end up getting an error while trying to call a function that had a parameter accidentally marked as exec.

For the generics, I think we could catch it when it's instantiated, like when we instantiate myfun::<Map<i32, i32>> we see that this is a function that takes an exec argument of proof type. (Or we could just rely on the fact that the user just won't be able to call that function without another mode error occurring earlier).

[utaal]

I've made a discussion to track the possible warning feature, #170

I'm going to close this as resolved otherwise; feel free to reopen if you have follow-up questions.