Verifier panic about expected call to into_inner

[jaylorch]

I encountered the following panic when running the verifier. It's likely related to verifying the following function, since it doesn't panic when it's removed from the storage_map_shard.rs file. See attached zip file for full context.

2024-03-12-18-46-28.zip

pub proof fn create_storage_map_shard<K, V>(m: Map<K, V>) -> (tracked storage: StateMachineStorageMapState<K, V>)
    ensures
        ({
            &&& storage.valid()
            &&& storage.dom() == m.dom()
            &&& forall |k| m.contains_key(k) ==> storage.owns(k) && storage.value(k) == m[k]
        })
{
    let m = Map::new(|k: K| m.contains_key(k),
                     |k: K| VariableShardResource::RightToAccess{ value: m[k] });
    let r = StorageMapShardResource{ m };
    let tracked mut perm = Permission::<StorageMapShardResource<K, V>>::new(r);
    let tracked storage = StateMachineStorageMapState{ perm };
    storage
}

C:\Apps\verus-systems-code\resource-algebra\src>verus main.rs --verify-module storage_map_shard
note: verifying module storage_map_shard

thread '<unnamed>' panicked at rust_verify\src\verifier.rs:806:21:
unexpected output from solver: (error "line 4512 column 51: unknown constant K&.")
stack backtrace:
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
thread '<unnamed>' panicked at rust_verify\src\verifier.rs:331:17:
dropped, expected call to `into_inner` instead
stack backtrace:
   0:     0x7ffe0b9e738a - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h90c22c4185b55f04
   1:     0x7ffe0ba1bb5b - core::fmt::write::h8a7f6edbcadee319
   2:     0x7ffe0b9dcc51 - <std::io::IoSlice as core::fmt::Debug>::fmt::h0ee392ef0f96e369
   3:     0x7ffe0b9e710a - std::sys_common::backtrace::lock::h134eeaadb35136bd
   4:     0x7ffe0b9ea8ca - std::panicking::default_hook::h81d7caaa8c7a40b4
   5:     0x7ffe0b9ea538 - std::panicking::default_hook::h81d7caaa8c7a40b4
   6:     0x7ffe0b9eb03e - std::panicking::rust_panic_with_hook::h8ac326f3b5470b08
   7:     0x7ff6ad69f8e9 - std::sync::once::Once::call_once_force::{{closure}}::hb63ad714e5d051bb
   8:     0x7ff6ad69a889 - std::sys_common::backtrace::__rust_end_short_backtrace::hcc057018e258d62f
   9:     0x7ff6adde7acd - std::panicking::begin_panic::h2134e5b6e01e1a45
  10:     0x7ff6ad6a2456 - core::ptr::drop_in_place<(alloc::sync::Arc<alloc::vec::Vec<alloc::sync::Arc<air::ast::CommandX>>>,alloc::string::String)>::h6998c619cb1a54cd
  11:     0x7ff6ad6da84e - rust_verify::verifier::Verifier::create_log_file::h9fb87b7e9df5ba1e
  12:     0x7ffecac61060 - <unknown>
  13:     0x7ffecac653ea - is_exception_typeof
  14:     0x7ffecac6fb80 - _C_specific_handler
  15:     0x7ffecac645f0 - is_exception_typeof
  16:     0x7ffecac704b1 - _CxxFrameHandler3
  17:     0x7ffee61b449f - _chkstk
  18:     0x7ffee612fd54 - RtlUnwindEx
  19:     0x7ffecac70046 - _C_specific_handler
  20:     0x7ffecac63245 - is_exception_typeof
  21:     0x7ffecac63666 - is_exception_typeof
  22:     0x7ffecac646ec - is_exception_typeof
  23:     0x7ffecac704b1 - _CxxFrameHandler3
  24:     0x7ffee61b441f - _chkstk
  25:     0x7ffee612e466 - RtlFindCharInUnicodeString
  26:     0x7ffee6164475 - RtlRaiseException
  27:     0x7ffee34b5b0c - RaiseException
  28:     0x7ffe0ba43b68 - _umodti3
  29:     0x7ffe0ba022ee - _rust_start_panic
  30:     0x7ffe0b9eb3fd - rust_panic
  31:     0x7ffe0b9eb206 - std::panicking::rust_panic_with_hook::h8ac326f3b5470b08
  32:     0x7ffe0b9eaf2d - <std::panicking::begin_panic_handler::StrPanicPayload as core::panic::BoxMeUp>::get::h353ca2f9698f73b3
  33:     0x7ffe0b9e8049 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h90c22c4185b55f04
  34:     0x7ffe0b9eac30 - rust_begin_unwind
  35:     0x7ffe0ba50d85 - core::panicking::panic_fmt::hb3ce2a19a4187054
  36:     0x7ff6ad6cf214 - rust_verify::verifier::Verifier::create_log_file::h9fb87b7e9df5ba1e
  37:     0x7ff6ad6dbd43 - rust_verify::verifier::Verifier::verify_bucket_outer::ha5ef1eafd9664a1a
  38:     0x7ff6ad7e1712 - std::panicking::try::he17101fe7bb9eb82
  39:     0x7ff6ad69a907 - std::sys_common::backtrace::__rust_begin_short_backtrace::h55957ad33f685633
  40:     0x7ff6ad7e2503 - <&T as core::fmt::Display>::fmt::h131cf157c6cb9e7a
  41:     0x7ffe0b9fe3ec - std::sys::windows::thread::Thread::new::h75a9ed52a5af2748
  42:     0x7ffee3eb257d - BaseThreadInitThunk
  43:     0x7ffee616aa58 - RtlUserThreadStart

[Chris-Hawblitzel]

This appears to be a bug in the AIR -> SMT translation, where the AIR code is valid but the SMT code has error "line 4512 column 51: unknown constant K&.". (Ignore the stack trace and the "dropped, expected call to into_inner instead"; that's unrelated and should be fixed separately.) I would recommend changing this:

        pub closed spec fn dom(self) -> Set<K>
        {
            Set::new(|k| !(#[trigger] self.perm.r().get(k) is Empty))
        }

to this:

        pub closed spec fn dom(self) -> Set<K>
        {
            Set::new(|k| !(self.perm.r().get(k) is Empty))
        }

Like Dafny and F*, Verus generally doesn't need triggers on closure declarations; support for triggers in closures was added by #331 to handle some unusual situations. Apparently, they aren't always translated to SMT correctly.

[Chris-Hawblitzel]

Here's a small repro of the bug that generates the SMT error error "line 813 column 19: unknown constant A&.":

spec fn id<A>(a: A) -> A { a }

struct S<A>(A);
impl<A> S<A> {
    spec fn f() -> (spec_fn(A) -> bool) {
        |a: A| #[trigger] id(a) == a
    }
}

proof fn test() {
    assert(S::f()(true));
}

[Chris-Hawblitzel]

(I'm guessing that the fix is pretty minor: simplify_choose calls enclose_force_hole on each trigger expression, so simplify_lambda probably just has to do the same.)

[tjhance]

Was this fully resolved by #1038 or are there remaining tasks here?

[utaal-b]

I think #1044 captures what's remaining, i.e. that certain errors unwind badly (due to the guard I put in place to avoid dropping diagnostics on the floor) and print a trace with expect call to into_inner in addition to the actual error.

@jaylorch @Chris-Hawblitzel I believe the issue is otherwise fixed, right? (If so, you can close and I'll get back to the issue with the error message.)

[utaal]

Closing on the assumption that this is fixed by #1038, modulo #1044, please reopen if it's still an issue.