Expand description
Lazy trace generation: run generates a trace on the fly by
repeatedly stepping with arbitrary-but-valid Ops.
At each iteration run uses choose to pick some Op that
satisfies super::op_pre against the current store. Because
super::Op::NewVmSpace has no precondition, such an op always
exists, so choose is well-defined. The picked op is then
discharged into super::step, and the recursion continues with
the post-state.
Compared to the previous run_trace(trace: Seq<Op>) design, this
avoids needing a valid_trace predicate / step_post spec
function: validity is established at the moment of choice rather
than as a precondition over a pre-built trace.