Io restoration

[SNoAnd]

This PR restores parity with io.rs and fixes some incomplete verification issues in that file. I've streamlined the model a bit as well, and added part of the top-level soundness proof in embedding, mainly to help convince myself that the new model is sufficient.

The other interesting thing I'd like to point out is the tarball in vtrace. This is the static version of a code difference tracker we've been working on here: https://github.com/CertiKProject/dv-verus-rewrite-tracker. It documents all of the differences between this branch and the original phaseII/mainline code, subject to predefined equivalence relations. The idea is to expand the equivalences where possible, or else manually approve intentional differences. Segment and io have up-to-date triage in the static copy.

[Marsman1996]

There are several extra files (i.e., vtrace?) uploaded, may need to remove.

[SNoAnd]

Done! Also found a couple of redundant preconditions on the cursor and removed them.

[rikosellic]

I'm reconsidering whether this design is good for verification. When we call align_up in another function now, we will get the align condition for free in its post-condition, which means we will never discover an overflow bug in the future! Worse still, if we call this function on arguments that do not satisfy the condition, it will imply false and we can prove any statement.

[rikosellic]

Maybe we still need the panic condition in the precondition to detect incorrect calls to the verified function. We can do something like this:

fn exec_f()
requires
   !panic_condition()
ensures
   normal_post_condition(),
   panic_condition() ==> false,

We can explicitly express the panic condition with panic_condition() ==> false, indicating that the function can never reach its end when the panic condition is met. And this condition is still inferred by your vstd::assert! macro. There may be more overflow checks enforced by Verus (e.g., self + (align - 1) <= $uint_type::MAX preserved in align_up's precondition), we can insert more vstd::assert!s so that the panic_condition can cover those cases. (This is a direct contradiction) When we found that the panic condition is not fully described in the documentation, we should report it to the dev group.

[rikosellic]

@SNoAnd @hiroki-chen What do you think?

[hiroki-chen]

Well I think it's necessary to make any situation that may cause runtime panic explicit in the verification conditions just to avoid potential mistakes.

[rikosellic]

The current design is equivalent to the explicit requires true ensures panic_condition() ==> false. But we can not rely on Verus to detect any misuse then.

[rikosellic]

but it holds trivially if we also include requires !panic_condition()

Yeah, I also realized this shortly after my reply. So the current situation is somehow embarrassing: if we include the panic condition in the precondition, then our vstd::assert mechanism will have no effect. If we do not include it, then we can not propagate the panic condition to the call site automatically and may fail to identify undocumented panics.

The addition semantic mismatch may be a smaller issue. We can add more constraints in the Verus condition to describe it more precisely.

[SNoAnd]

My worry is that the addition semantic mismatch might not be the only one. Turning panics and unexpected behavior into preconditions is a common Verus idiom.

I need to think harder about it, but maybe we can use the opaqueness idea on the requires side instead. The caller provides the non-panic predicate, but its content is only accessible once it's independently enforced by the assert!.

[SNoAnd]

I think I have a good solution. Panic diverge can take an uninterp spec fn may_panic() token in its requires. Functions that have the possibility of panicking must provide that token via their own requires. We write !P || may_panic() or P ==> may_panic() in the requires block, and propagate it back to the API surface.

This is framed as a "may" because the token on its own does nothing if the code doesn't actually reach a panic_diverge. If there is a single condition P, we can turn it into a total condition:

requires
    P <==> may_panic()
ensures
    !may_panic()

Working on implementation.

[rikosellic]

@SNoAnd Sounds like a great idea!

To my understanding, do you mean something like {may_panic} panic_diverge {false}.

Then we have:
assert!(P)
is equivalent to:
{!P ==> may_panic()} if (P) {skip} else {panic_diverge()} {P}

I'm not very sure whether we should use P<==> may_panic() or just P==>may_panic() though.

[SNoAnd]

Yes, exactly! I think that requires !P ==> may_panic() and ensures P is actually sufficient, and much easier to work with. The leftward implication gets unpleasant when functions have multiple conditions that might trigger in different nested callees.

[Copilot]

Pull request overview

This PR refactors and strengthens the VM I/O and virtual-memory verification model to restore parity with io.rs, relax some overly-strong preconditions (notably in_locked_range) while preserving soundness via explicit divergence modeling, and introduces a deeper embedding layer to structure top-level soundness arguments.

Changes:

• Introduces UnwrapOrPanic (diverging unwrap) and updates cursor/pop modeling to treat real Rust panics as sound divergence rather than precondition failures.
• Refactors VM I/O tracked types/axioms into ostd/specs/mm/io.rs, expands slice/int external specs, and updates VmReader/VmWriter construction and method contracts accordingly.
• Adds a new deep embedding (ostd/specs/mm/embedding/*) with store/step semantics to support top-level soundness reasoning across arbitrary operation traces.

Reviewed changes

Copilot reviewed 35 out of 35 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
vstd_extra/src/panic.rs	Adds diverging unwrap_or_panic abstraction for modeling real panics.
vstd_extra/src/external/slice.rs	Extends slice specs (raw parts, range helpers, overflow axiom).
vstd_extra/src/external/mod.rs	Exposes new int_specs module.
vstd_extra/src/external/int_specs.rs	Adds is_power_of_two specs for common unsigned integer types.
vstd_extra/src/drop_tracking.rs	Simplifies drop-tracking traits by removing drop_tracked from TrackDrop.
ostd/src/mm/vm_space.rs	Switches to specs::mm::virt_mem/specs::mm::io types and tightens ensures.
ostd/src/mm/page_table/mod.rs	Adds regions-invariant preservation ensure in user PT creation.
ostd/src/mm/page_table/cursor/mod.rs	Relaxes in_locked_range preconditions, re-derives conditions post-guards, updates jump/pop modeling.
ostd/src/mm/io.rs	Refactors VM I/O contracts, moves tracked owner/view logic to specs, updates fallible/infallible behaviors and defaults.
ostd/src/mm/frame/untyped.rs	Updates imports to new virt_mem and specs::mm::io::VmIoOwner.
ostd/src/mm/frame/segment.rs	Updates to new virt_mem::MemView path.
ostd/src/mm/frame/mod.rs	Strengthens Frame drop ensures around refcount/identity preservation.
ostd/src/mm/frame/linked_list.rs	Removes large drop_tracked proof implementation (now handled differently).
ostd/src/mm/dma/dma_stream.rs	Updates VM I/O imports and removes obsolete read_byte impl using removed array ptr API.
ostd/specs/mm/vm_space.rs	Updates to specs::mm::io tracked types and new virt_mem module.
ostd/specs/mm/virt_mem.rs	Adds byte-sequence read/write specs and updates volatile read/write contracts.
ostd/specs/mm/pod.rs	Introduces pod_bytes spec and axioms to relate typed values to byte sequences.
ostd/specs/mm/page_table/owners.rs	Initializes new borrowed field in EntryOwner default.
ostd/specs/mm/page_table/node/mod.rs	Removes drop_tracked implementation from PageTableGuard tracking.
ostd/specs/mm/page_table/node/entry_owners.rs	Adds borrowed translation-only entry variant and associated invariants/constructors.
ostd/specs/mm/page_table/cursor/va_lemmas.rs	Clears popped_too_high on reposition and tightens related preconditions.
ostd/specs/mm/page_table/cursor/owners.rs	Adjusts cursor-owner invariants and lock-range reasoning to match new model.
ostd/specs/mm/page_table/cursor/cursor_steps.rs	Updates proof obligations after relaxing in_locked_range and lock bounds.
ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs	Updates comments/spec intent for panic/unwrap modeling.
ostd/specs/mm/mod.rs	Renames/restructures modules (virt_mem_newer → virt_mem, vm_space_embedding → embedding).
ostd/specs/mm/io.rs	Moves/expands tracked VM I/O owner/view types and trust-boundary axioms into specs.
ostd/specs/mm/frame/unique.rs	Removes drop_tracked implementation from UniqueFrame tracking.
ostd/specs/mm/frame/segment.rs	Updates to new virt_mem::MemView path and removes empty drop_tracked.
ostd/specs/mm/embedding/vm_space.rs	Adds embedded axioms/steps for VmSpace::new and drop.
ostd/specs/mm/embedding/trace.rs	Adds lazy trace generation proof (choose-based stepping).
ostd/specs/mm/embedding/mod.rs	Introduces deep embedding: store, ops, op-preconditions, step dispatcher, helpers.
ostd/specs/mm/embedding/io.rs	Embeds VM I/O operations and mirrors exec contracts via _embedded axioms.
ostd/specs/mm/embedding/frame.rs	Embeds frame lifecycle operations and ties them to regions/refcount semantics.
ostd/specs/mm/embedding/cursor.rs	Embeds cursor operations and mirrors relaxed exec preconditions.
ostd/libs/align_ext/src/lib.rs	Makes align_up/align_down panic-enforce power-of-two alignment requirements.

Comments suppressed due to low confidence (1)

ostd/specs/mm/virt_mem.rs:846

• VirtPtr::copy_nonoverlapping no longer requires the source and destination ranges to be non-overlapping, but the operation is modeled as a memcpy-style copy (and the runtime arch primitive used elsewhere is also memcpy-like). Allowing overlap makes the spec too permissive and can let proofs rely on behavior that is undefined/incorrect for overlapping copies. Consider restoring the original non-overlap precondition (src.vaddr + n <= dst.vaddr || dst.vaddr + n <= src.vaddr) or renaming/re-specifying this API as an overlap-tolerant copy (memmove/snapshot semantics) and ensuring callers use the appropriate primitive.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[hiroki-chen]

One thing about adding axiom fn for creating tracked objects to mimic their spec definitions: the current codebase uses #[verifier::external_body] pub proof fn tracked_[fn_name]. Can we please make the code style consistent @SNoAnd ?

[SNoAnd]

@rikosellic, @hiroki-chen: This is another place where the panic discussion is relevant. Like with overflow arithmetic, Verus replaces the panic in unwrap() with a precondition, but ostd sometimes relies on the panic behavior.

[rikosellic]

This design is absolutely sound, as both we and the devs agree that panic diverge is a sound behaviour. The question is that not all panics are expected or preferred, which are also considered bugs (the fuzzing work by @Marsman1996 has found dozens of them).

As a result, we may fail to identify that the following function may unexpectedly panic because Verus will no longer raise any verification errors:

pub fn api() {
       let x = None;
       x.unwrap_or_panic()
}

To prevent this, any function that is called in a verified caller should have the panic condition in its requires clause. For public APIs, we may keep the current design because they will not be called in a verification context in the near future.

[rikosellic]

@SNoAnd, please merge the latest main branch. We have enabled the global format check again!

[rikosellic]

@SNoAnd Thanks for your contribution! Left a small comment in vstd_extra. Please also format the code (you may have to run cargo dv bootstrap --upgrade to get the latest version). I will merge it then.

[rikosellic]

@hiroki-chen Is it valid to delete read_byte in dma_stream?

[rikosellic]

There are is_pow2 and is_pow2_exists defined in vstd::arithmetic::power2, we can reuse those definitions.

[rikosellic]

We can also write a macro_rule to simplify this file.

[hiroki-chen]

@hiroki-chen Is it valid to delete read_byte in dma_stream?

I think this is fine. The unverified ostd uses the default trait implementation and in the initial version I just marked this function as a placeholder.

[SNoAnd]

One thing about adding axiom fn for creating tracked objects to mimic their spec definitions: the current codebase uses #[verifier::external_body] pub proof fn tracked_[fn_name]. Can we please make the code style consistent @SNoAnd ?

Missed this in the shuffle, but yeah, we can do that.

[rikosellic]

Thanks for your contribution! I think we can leave the minor improvements in another PR. I will merge it now.