pub proof fn step<'rcu>(tracked s: &mut VmStore<'rcu>, op: Op)Expand description
requires
old(s).inv(),op_pre(*old(s), op),final(s).inv(),One-step soundness theorem.
op_pre(*old(s), op) is the per-op precondition. Each match arm
extracts the relevant entries from the store, calls the per-op step
(which has neither preconditions nor if-guards on store membership),
and inserts any modified or freshly-produced entries back.