ostd/specs/mm/embedding/
trace.rs

1//! Lazy trace generation: [`run`] generates a trace on the fly by
2//! repeatedly stepping with arbitrary-but-valid Ops.
3//!
4//! At each iteration `run` uses `choose` to pick *some* `Op` that
5//! satisfies [`super::op_pre`] against the current store. Because
6//! [`super::Op::NewVmSpace`] has no precondition, such an op always
7//! exists, so `choose` is well-defined. The picked op is then
8//! discharged into [`super::step`], and the recursion continues with
9//! the post-state.
10//!
11//! Compared to the previous `run_trace(trace: Seq<Op>)` design, this
12//! avoids needing a `valid_trace` predicate / `step_post` spec
13//! function: validity is established at the moment of choice rather
14//! than as a precondition over a pre-built trace.
15use vstd::prelude::*;
16use vstd_extra::ownership::*;
17
18use super::{Op, VmStore, op_pre, step};
19
20verus! {
21
22/// `op_pre` is always satisfiable: [`Op::NewVmSpace`] has no
23/// preconditions, so it's a witness for any state.
24pub proof fn op_pre_satisfiable<'rcu>(s: VmStore<'rcu>)
25    ensures
26        exists|op: Op| op_pre(s, op),
27{
28    assert(op_pre(s, Op::NewVmSpace));
29}
30
31/// Generates a trace of `n` steps by repeatedly choosing some op that
32/// satisfies [`super::op_pre`] against the current store and applying
33/// it via [`super::step`]. Preserves [`VmStore::inv`] throughout.
34///
35/// This is the soundness story over arbitrary call sequences: no
36/// matter which `n` operations the system picks (subject only to
37/// op-pre validity at each step), invariants hold.
38pub proof fn run<'rcu>(tracked s: &mut VmStore<'rcu>, n: nat)
39    requires
40        old(s).inv(),
41    ensures
42        final(s).inv(),
43    decreases n,
44{
45    if n > 0 {
46        op_pre_satisfiable(*s);
47        let op: Op = choose|op: Op| op_pre(*s, op);
48        step(s, op);
49        run(s, (n - 1) as nat);
50    }
51}
52
53} // verus!
ostd/specs/mm/embedding/trace.rs

ostd/specs/mm/embedding/
trace.rs
