Unexpected loc SpannedTyped

[maeiik]

I was trying to verify the following (minimized) program using Verus on the main branch (commit edb8f53):

use vstd::prelude::*;
verus! {
    fn proof_add_one(heap: &mut verus_heap::Heap, head: Option< verus_heap::Addr >) {
        *(verus_heap::cast::<i32>(verus_heap::heap_borrow(heap, head))) += 1 as i32;
    }

    mod verus_heap {
        use vstd::prelude::*;
        pub struct Addr;
        pub struct Val;
        pub type Heap = Map< Addr, Val >;

        #[verifier(external_body)]
        pub fn heap_borrow<'a>(heap: &'a Heap, key: Option<Addr>) -> (v: &'a Val) {
            unimplemented!()
        }

        #[verifier(external_body)]
        pub fn cast<'a, T>(v: &'a Val) -> (r: &'a T)     {
            unimplemented!()
        }
    }

    fn main();
}

Unfortunately, Verus panics when run with this example:

thread 'rustc' panicked at vir/src/modes.rs:645:13:
unexpected loc SpannedTyped { span: Span { raw_span: "ANY", id: 6, data: [15845129045879692381, 541165879484], as_string: "foo44_minimal_failing.rs:4:10: 4:72 (#0)" }, typ: Int(I(32)), x: Call(Fun(Static, FunX { path: PathX { krate: Some("foo44_minimal_failing"), segments: ["verus_heap", "cast"] } }, [Int(I(32))], [], Final), [SpannedTyped { span: Span { raw_span: "ANY", id: 5, data: [15845129045879692381, 648540061882], as_string: "foo44_minimal_failing.rs:4:35: 4:70 (#0)" }, typ: Decorate(Ref, Datatype(PathX { krate: Some("foo44_minimal_failing"), segments: ["verus_heap", "Val"] }, [], [])), x: Call(Fun(Static, FunX { path: PathX { krate: Some("foo44_minimal_failing"), segments: ["verus_heap", "heap_borrow"] } }, [], [], Final), [SpannedTyped { span: Span { raw_span: "ANY", id: 3, data: [15845129045879692381, 751619276979], as_string: "foo44_minimal_failing.rs:4:59: 4:63 (#0)" }, typ: Decorate(Ref, Datatype(PathX { krate: Some("vstd"), segments: ["map", "Map"] }, [Datatype(PathX { krate: Some("foo44_minimal_failing"), segments: ["verus_heap", "Addr"] }, [], []), Datatype(PathX { krate: Some("foo44_minimal_failing"), segments: ["verus_heap", "Val"] }, [], [])], [])), x: Var(VarIdent("heap", RustcId(2))) }, SpannedTyped { span: Span { raw_span: "ANY", id: 4, data: [15845129045879692381, 777389080761], as_string: "foo44_minimal_failing.rs:4:65: 4:69 (#0)" }, typ: Datatype(PathX { krate: Some("core"), segments: ["option", "Option"] }, [Datatype(PathX { krate: Some("foo44_minimal_failing"), segments: ["verus_heap", "Addr"] }, [], [])], []), x: Var(VarIdent("head", RustcId(4))) }]) }]) }

Our expectation for this example is that Verus would reject this program with a verification error, due to a possible overflow in function proof_add_one.

verus version:

Verus
  Version: 0.2024.06.26.c3dbf1c.dirty
  Profile: release
  Platform: macos_aarch64
  Toolchain: 1.76.0-aarch64-apple-darwin

[maeiik]

@jcp19

[utaal]

Thank you for the report. My first guess is that this is an unsupported feature (but we should be giving you a better error message). But let's diagnose.

What's the signature and body of verus_heap::cast?

[maeiik]

It's defined on line 12:

#[verifier(external_body)]
pub fn cast<'a, T>(v: &'a Val) -> (r: &'a T) {
    unimplemented!()
}

[utaal]

Sorry I should have read the snippet more carefully.

I need to double check when I'm not on mobile, but I think this is an invalid program, but for a different reason: due to the assignment to an immutable reference. It's unfortunate (and indeed a bug) that we panic before we emit that error.

I have upcoming changes that should reduce the number of corner cases and make this better.