pub proof fn run<'rcu>(tracked s: &mut VmStore<'rcu>, n: nat)Expand description
requires
old(s).inv(),final(s).inv(),Generates a trace of n steps by repeatedly choosing some op that
satisfies super::op_pre against the current store and applying
it via super::step. Preserves VmStore::inv throughout.
This is the soundness story over arbitrary call sequences: no
matter which n operations the system picks (subject only to
op-pre validity at each step), invariants hold.