pub proof fn step<'a, 'rcu>(tracked s: &mut VmStore<'rcu>, op: Op)
old(s).inv(),
final(s).inv(),
One-step soundness theorem.