Adaptations for the upcoming change to the new iterator interface.

[parno]

When we release the new approach to specifying iterators, this PR should get the repo back into a verifying state.

[parno]

@microsoft-github-policy-service agree company="CMU"

[jaylorch]

Thanks! When a vstd crate with this feature is available on crates.io, could you please update this PR to include the requisite updates to the various Cargo.toml files, so they point to that version?

[parno]

I updated the Cargo.toml files. At least on my local version two of the three projects now verify. However, with CapybaraKV, I'm seeing:

capybaraKV/capybarakv $ cargo verus focus --no-default-features

thread '<unnamed>' (12115053) panicked at vir/src/sst_to_air.rs:172:25:
abstract datatype should be boxed Datatype(Path(Path(vstd, ["resource" :: "ghost_var" :: "GhostVar"])), [Datatype(Path(Path(capybarakv, ["kv2" :: "concurrentspec_t" :: "ConcurrentKvStoreView"])), [TypParam("K"), TypParam("I"), TypParam("L")], [])], [])
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread '<unnamed>' (12115053) panicked at rust_verify/src/verifier.rs:424:17:
dropped, expected call to `into_inner` instead

Does that seem at all familiar?

[jaylorch]

It doesn't look familiar to me. Maybe I can recreate it. Are you using Linux or MacOS to get this error?

[jaylorch]

Oh, I'm able to recreate it on Windows.

[jaylorch]

To answer your question, no, it doesn't look familiar to me.

[parno]

I isolated the issue leading to the panic, and pushed a potential fix in this PR. It was a problem with how recommends are handled when a proof fails. With that out of the way, I could see the actual failure, which was a failed loop invariant inside of setup in shardkv_v.rs. In 9cf8ada, I added a spinoff prover directive that seems to nudge things back into a verifying state.

[jaylorch]

Thanks for figuring it out! Now I'm trying to figure out how to fix the error (without spinning off the prover, which masks it). I'm finding that even if I assert or assume the loop condition at the end of the loop (after taking into account the change to idx that's about to occur), I still see the error. And even if I rewrite the loop invariant to avoid using the loop variable idx, I still find I can assume it at the end of the loop and Verus can't verify that the condition is preserved by the loop body. Is there some way I can see the "desugared" form of the new iterator loop so I can see what's happening between the end of the loop body and the end of the desugared loop body?

[jaylorch]

Never mind. It seems to have nothing to do with the loop. I'm investigating the triggering issue.

[jaylorch]

I found the problem. There was a missing invariant in the loop. I'll push my fix to this PR, if it lets me.

[jaylorch]

Hmm, it's not letting me. Here's the diff you need:

diff --git a/capybaraKV/capybarakv/src/kv2/shardkv_v.rs b/capybaraKV/capybarakv/src/kv2/shardkv_v.rs
index 45db90ff..14aaa91e 100644
--- a/capybaraKV/capybarakv/src/kv2/shardkv_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/shardkv_v.rs
@@ -238,7 +238,6 @@ where
         self.inv@.constant().combined_id
     }

-    #[verifier::spinoff_prover]
     exec fn setup(
         nshards: usize,
         Tracked(shard_res): Tracked<Map<int, GhostVar<ConcurrentKvStoreView::<K, I, L>>>>,
@@ -271,6 +270,7 @@ where

         for idx in 0..nshards
             invariant
+                nshards >= 1,
                 pred.shard_ids.len() == idx,
                 pred.combined_id == shardstates.combined.id(),
                 pred.combined_id == combined_res.id(),

[jaylorch]

I wonder why the new iterator system requires this invariant nshards >= 1. After all, nshards doesn't change in the body of the loop.

[jaylorch]

It doesn't seem to need invariants about shard_res_old, such as these that seem useful:

forall |shard| 0 <= shard < nshards ==> #[trigger] shard_res_old.contains_key(shard),
forall |shard| #[trigger] shard_res_old.contains_key(shard) ==> {
    &&& shard_res_old[shard]@.ps == ps
    &&& shard_res_old[shard]@.pm_constants == pm_constants
    &&& shard_res_old[shard]@.kv == RecoveredKvStore::<K, I, L>::init(ps).kv
},

It seems to be able to infer these, as expected, because shard_res_old doesn't change in the body of the loop.

[jaylorch]

The safest, most stable thing to do is to add those invariants about shard_res_old as well, and then we're not dependent on the vagaries of how Verus chooses to treat variables unmodified in the loop body.

[jaylorch]

Thanks!