pub proof fn smoke_test<'a, 'rcu>(tracked s: &mut VmStore<'rcu>)Expand description
requires
old(s).inv(),final(s).inv(),Smoke test: applies a chain of step calls and asserts s.inv() at
the end without any intermediate lemma calls. The fact that this
proof fn typechecks is the implicit-induction property — Verus
chains each step’s ensures into the next step’s requires for free,
and the final s.inv() falls out of the last step’s ensures.
The specific ids passed (0) need not match any actual id allocated
during the chain; per-op steps that find no matching id are no-ops,
which still preserve inv().