Skip to main content

op_pre

ostd::specs::mm::embedding

Function op_pre 

Source 
pub open spec fn op_pre<'rcu>(s: VmStore<'rcu>, op: Op) -> bool
Expand description
{
    match op {
        Op::NewVmSpace => true,
        Op::DropVmSpace { vs } => {
            s.vm_spaces.dom().contains(vs)
                && (forall |c: CursorId| {
                    #[trigger] s.cursors.dom().contains(c)
                        ==> s.cursors[c].vm_space != vs
                })
                && (forall |v: VmIoId| {
                    #[trigger] s.vm_ios.dom().contains(v)
                        ==> s.vm_ios[v].vm_space != Some(vs)
                })
        }
        Op::OpenCursor { vs, va: _ } => s.vm_spaces.dom().contains(vs),
        Op::OpenCursorMut { vs, va: _ } => s.vm_spaces.dom().contains(vs),
        Op::DropCursor { c } => s.cursors.dom().contains(c),
        Op::Query { c } => s.cursors.dom().contains(c),
        Op::FindNext { c, len: _ } => s.cursors.dom().contains(c),
        Op::Jump { c, va: _ } => s.cursors.dom().contains(c),
        Op::VirtAddr { c } => s.cursors.dom().contains(c),
        Op::Map { c, fid, prop: _ } => {
            s.cursors.dom().contains(c) && s.frames.dom().contains(fid)
        }
        Op::Unmap { c, len: _ } => s.cursors.dom().contains(c),
        Op::ProtectNext { c, len: _ } => s.cursors.dom().contains(c),
        Op::NewReader { vs, vaddr: _, len: _ } => s.vm_spaces.dom().contains(vs),
        Op::NewWriter { vs, vaddr: _, len: _ } => s.vm_spaces.dom().contains(vs),
        Op::NewKernelReader { vaddr: _, len: _ } => true,
        Op::NewKernelWriter { vaddr: _, len: _ } => true,
        Op::DropReader { vio } => s.vm_ios.dom().contains(vio),
        Op::DropWriter { vio } => s.vm_ios.dom().contains(vio),
        Op::ReaderReadVal { source } => s.vm_ios.dom().contains(source),
        Op::ReaderCollect { source } => s.vm_ios.dom().contains(source),
        Op::ReaderLimit { vio, max: _ } => s.vm_ios.dom().contains(vio),
        Op::ReaderSkip { vio, n: _ } => s.vm_ios.dom().contains(vio),
        Op::ReaderQuery { vio } => s.vm_ios.dom().contains(vio),
        Op::WriterWriteVal { writer } => s.vm_ios.dom().contains(writer),
        Op::WriterFillZeros { vio, len: _ } => s.vm_ios.dom().contains(vio),
        Op::WriterLimit { vio, max: _ } => s.vm_ios.dom().contains(vio),
        Op::WriterSkip { vio, n: _ } => s.vm_ios.dom().contains(vio),
        Op::WriterQuery { vio } => s.vm_ios.dom().contains(vio),
        Op::Read { source, dest } => {
            s.vm_ios.dom().contains(source) && s.vm_ios.dom().contains(dest)
                && source != dest && s.vm_ios[source].is_kernel_reader()
                && s.vm_ios[dest].is_kernel_writer()
        }
        Op::Write { source, dest } => {
            s.vm_ios.dom().contains(source) && s.vm_ios.dom().contains(dest)
                && source != dest && s.vm_ios[source].is_kernel_reader()
                && s.vm_ios[dest].is_kernel_writer()
        }
        Op::FrameFromUnused { paddr: _ } => true,
        Op::FrameFromInUse { paddr: _ } => true,
        Op::FrameDrop { fid } => {
            s.frames.dom().contains(fid)
                && segment_cover_count(s.segments, s.frames[fid].paddr) == 0
        }
        Op::SegmentFromUnused { range } => {
            range.start % PAGE_SIZE == 0 && range.end % PAGE_SIZE == 0
                && range.start < range.end && range.end <= MAX_PADDR
                && forall |paddr: Paddr| {
                    (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
                        ==> s
                            .regions
                            .slot_owners[frame_to_index(paddr)]
                            .inner_perms
                            .ref_count
                            .value() == REF_COUNT_UNUSED
                }
        }
        Op::SegmentDrop { sid } => s.segments.dom().contains(sid),
        Op::SegmentSplit { sid, offset } => {
            s.segments.dom().contains(sid) && offset % PAGE_SIZE == 0 && 0 < offset
                && offset < (s.segments[sid].range.end - s.segments[sid].range.start)
        }
        Op::SegmentNext { sid } => s.segments.dom().contains(sid),
    }
}

Per-op precondition — the conjunction of facts about the store that must hold for an Op to be applied. Encodes id-existence, distinctness, cross-store ref-integrity, and the expressible portion of the exec-method preconditions (per-op requires from the verus_spec annotations). MODEL GAPS (handle inv/wf, tlb_model.inv() is in VmStore::inv, closure preconditions on protect_next, size_of::<T>() range bounds on read_val/write_val/collect) are documented in [super::cursor] and super::io axiom comments.

step requires op_pre(*old(s), op). Callers must establish the precondition for the specific Op variant they’re about to apply.

SOUNDNESS: when we’re done building this model, op_pre must be permissive enough to permit every possible call trace. That means that these conditions should reduce to “the relevant objects exist in the store”.