pub proof fn op_pre_satisfiable<'rcu>(s: VmStore<'rcu>)Expand description
ensures
exists |op: Op| op_pre(s, op),op_pre is always satisfiable: Op::NewVmSpace has no
preconditions, so it’s a witness for any state.