Analysis: `assume_specification` centralization for `SmallVec` in `ostd/src/cpu/set.rs`

[Marsman1996]

Date: 2026-09-11
Subject: Can the #[verifier::external_body] accessor TCB in cpu::set be eliminated by specifying SmallVec directly via assume_specification (per the coding guidelines)?
Bottom line: Partially. SmallVec can be given assume_specifications (the earlier "blocked by const-generics" claim was wrong), and a centralized spec module for the unobstructed operations compiles. But full elimination of cpu::set's external_body accessors is not achievable in the current Verus: two SmallVec methods that cpu::set needs (resize, and the IndexMut write path) hit concrete Verus obstacles that the guidelines themselves say justify retaining a wrapper.

---

1. Background: what's currently in place

ostd/src/cpu/set.rs is proven at "A1": the bit-masking logic of add/remove/contains/From::from is genuinely verified over a Seq<u64> model (bits_seq), bridged to the real SmallVec<[u64; 2]> field by five small #[verifier::external_body] accessor methods:

bits_len / bits_get / bits_set / bits_resize / bits_fill   (external_body, on CpuSet)

• cargo dv focus --targets ostd -- --verify-only-module cpu::set → 6 verified, 0 errors
• Full cargo dv verify --targets ostd → 1517 verified, 0 errors (no regression)

The external_body accessors are the TCB. The question was whether the guideline-preferred assume_specification on SmallVec's own methods could replace them (centralizing the TCB in vstd_extra, "direct form" over wrappers).

---

2. Correction: SmallVec is not blocked by const-generics

My earlier claim — "SmallVec is foreign + const-generic, so no external_type_specification" — was wrong.

• array_ptr.rs:384's TODO is about const params (ArrayPtr<V, N> where N is a const).
• SmallVec<A>'s A is a type parameter (A: smallvec::Array), not a const.

The real obstacle (surmountable) is that the foreign smallvec::Array trait (with associated type Item) must be declared to Verus first. Verus says so itself:

error: trait `smallvec::Array` not declared to Verus
(hint: use #[verifier::external_trait_specification] to declare the trait)

Declaring it compiles:

#[verifier::external_trait_specification]
pub trait ExArray {
    type ExternalTraitSpecificationFor: smallvec::Array;
    type Item;
}

---

3. Stage 1 deliverable: centralized SmallVec spec module (compiles)

Built at verified_libs/vstd_extra/src/external/smallvec.rs (added smallvec = "1.13.2" to vstd_extra/Cargo.toml; registered pub mod smallvec; + pub use smallvec::*; in external/mod.rs).

cargo dv verify --targets vstd_extra → 567 verified, 0 errors.

Contents:

// Declare the foreign Array trait (assoc type Item).
#[verifier::external_trait_specification]
pub trait ExArray { type ExternalTraitSpecificationFor: smallvec::Array; type Item; }

// SmallVec<A> as an opaque external type (generic <A> — concrete SmallVec<[u64;2]>
// is REJECTED by "expected generics to match"; no-bound <A> fails rustc E0277).
#[verifier::external_type_specification]
#[verifier::external_body]
#[verifier::reject_recursive_types(A)]
pub struct ExSmallVec<A: Array>(SmallVec<A>);

// View as Seq<A::Item>. Cannot `impl vstd::View for SmallVec` — View is private
// (E0603) AND orphan rule (both foreign). Use a custom local trait, like btree's
// CursorMutAdditionalSpecFns.
pub trait SmallVecSpecFns<A: Array> { spec fn view(&self) -> Seq<A::Item>; }
impl<A: Array> SmallVecSpecFns<A> for SmallVec<A> { uninterp spec fn view(&self) -> Seq<A::Item>; }

// Direct assume_specifications (generics go BEFORE [path]; old(s)/final(s) for &mut).
pub assume_specification<A: Array>[ SmallVec::<A>::new ]() -> (ret: SmallVec<A>)
    ensures ret.view() == Seq::empty();
pub assume_specification<A: Array>[ SmallVec::<A>::with_capacity ](capacity: usize) -> (ret: SmallVec<A>)
    ensures ret.view() == Seq::empty();
pub assume_specification<A: Array>[ SmallVec::<A>::len ](s: &SmallVec<A>) -> (ret: usize)
    ensures ret == s.view().len();

This validates the full "direct form" the guideline prefers for new / with_capacity / len.

---

4. Concrete obstacles preventing full elimination

Per the guideline "test the direct form, record any concrete obstacle, then add a wrapper", the following are recorded obstacles that justify retaining wrappers:

4.1 SmallVec::resize — where A::Item: Clone (TESTED, confirmed blocker)

Real signature:

pub fn resize(&mut self, new_len: usize, value: A::Item) where A::Item: Clone

(resize clones value into each new slot, so it requires A::Item: Clone at compile time.)

• Without the bound in the assume_spec: rustc E0599: trait bound '<A as Array>::Item: Clone' not satisfied.
• With where A::Item: Clone, appended after ensures: Verus error: expected an expression — assume_specification does not accept a where clause.
• A::Item: Clone is a bound on an associated type, which can only appear in a where clause, not in the <A: Array> generic list (you can bound a generic param there, not an assoc type). btree's <A: Allocator + Clone> bounds the param A, which is different.

⇒ No place to express A::Item: Clone in an assume_specification ⇒ resize cannot be spec'd ⇒ the bits_resize wrapper must stay.

4.2 Index::index / IndexMut::index_mut — reference returns (INFERRED from btree precedent; not directly tested)

• Index<usize>::index(&self, i) -> &A::Item (read; self.bits[i])
• IndexMut<usize>::index_mut(&mut self, i) -> &mut A::Item (write; self.bits[i] = v)

cpu::set's add/remove write via self.bits[i] = v, i.e. IndexMut, which hands back a &mut A::Item that the caller writes through after the call. Faithfully specifying "writing through the returned &mut changes self.view()[i]" requires the prophetic / permission machinery (the repo's btree model uses final_map / final(value) for exactly this — BTreeMap::get_mut returning &'a mut Value). It is not expressible as a one-line ensures *ret == ....

• The read path Index::index (returns &A::Item) may be more tractable (btree returns borrowed values elsewhere) — not tested.
• The write path IndexMut::index_mut (returns &mut A::Item) is the genuinely hard one — inferred obstacle, not directly tested.

⇒ The bits_get (read) and especially bits_set (write) wrappers stay unless one invests in prophetic specs (advanced, btree-get_mut-scale).

4.3 AtomicU64 atomic ops (separate concern)

AtomicCpuSet uses SmallVec<[AtomicU64; 2]> and fetch_or/fetch_and/load/store. Faithful atomic-memory modeling is a separate, harder problem (concurrent state), independent of the SmallVec-spec question. AtomicCpuSet stays external_body regardless.

4.4 Consumption requires moving CpuSet into verus!

Even to consume the unobstructed assume_specs (len/new/with_capacity) directly in cpu::set, bits_seq(s) would need to be s.bits.view(). But s.bits (a field of CpuSet) is only spec-accessible if CpuSet is a Verus struct inside verus!; an external_type_specification'd CpuSet is opaque (fields inaccessible). Moving CpuSet into verus! brings #[derive(Clone, Debug, Default)]-handling risk for ~1 eliminated accessor (bits_len) while §4.1/§4.2 wrappers must stay anyway — poor cost/benefit.

---

5. Summary: spec'd vs. wrapper-kept

SmallVec op used by cpu::set	Obstacle	Outcome
new	none	assume_spec ✅ (in vstd_extra module)
with_capacity	none	assume_spec ✅
len	none	assume_spec ✅
resize	where A::Item: Clone (TESTED)	external_body wrapper (bits_resize) stays
index (Index, read)	reference return (likely tractable; not tested)	external_body wrapper (bits_get) stays
index_mut (IndexMut, write)	&mut return + write effect (prophetic; inferred)	external_body wrapper (bits_set) stays
fill	via Deref to slice (no inherent)	avoid (rewrite) or wrapper
AtomicU64::fetch_or/...	atomic memory model	AtomicCpuSet stays external_body

Net: the two SmallVec entry points cpu::set actually uses to mutate (resize, index_mut) are exactly the ones blocked from assume_spec — so full elimination of external_body accessors is not achievable in the current Verus.

---

6. Files / verification state

Current (uncommitted) changes:

• ostd/src/lib.rs — re-enabled pub mod cpu; (scoped cpu-module port).
• ostd/src/cpu/mod.rs — scoped port (CpuId/num_cpus/all_cpus kept; local/arch::cpu/atomic_mode/init deferred as comments).
• ostd/src/cpu/set.rs — A1 (verifies; 6 verified, 0 errors).
• verified_libs/vstd_extra/Cargo.toml — added smallvec = "1.13.2".
• verified_libs/vstd_extra/src/external/smallvec.rs — new centralized module (§3).
• verified_libs/vstd_extra/src/external/mod.rs — registered smallvec module.

Verification:

• cargo dv focus --targets ostd -- --verify-only-module cpu::set → 6 verified, 0 errors (A1, still green after vstd_extra changes).
• cargo dv verify --targets vstd_extra → 567 verified, 0 errors (smallvec module compiles).
• cargo dv verify --targets ostd → 1517 verified, 0 errors (no regression at the A1 checkpoint; the vstd_extra module is not yet consumed by ostd).

Note: the vstd_extra smallvec module is currently not consumed by cpu::set (consumption is blocked by §4.1/§4.2/§4.4).

---

7. Recommendation

1. Keep A1 in ostd/src/cpu/set.rs. Its external_body accessors are guideline-justified: the direct assume_spec form was tested and the obstacles (§4.1 where; §4.2 reference-return) were recorded, so a wrapper is the prescribed fallback. Trust surface is equivalent either way (both are TCB).
2. vstd_extra smallvec module: it is real and guideline-compliant but currently unconsumed.
   • Revert it (preferred for a clean repo) — the trust/reuse benefit doesn't materialize while cpu::set can't consume it; drop smallvec from vstd_extra and remove the module. The working pattern (Array-trait declaration + custom SmallVecSpecFns view + assume_spec for <A: Array>) is preserved in memory for when Verus adds where-clause / mutable-borrow-spec support.
   • Or keep it as dormant infrastructure — costs a vstd_extra smallvec dep + a dead module until consumption is unblocked.
3. If Index::index (read) is wanted: a quick assume_spec test is cheap and could potentially eliminate the bits_get wrapper (the read path may be tractable, unlike index_mut). Not done in this analysis; can be a follow-up.
4. Deeper unblockers (future Verus): assume_specification where-clause support (unblocks resize) and a first-class story for &mut-returning method specs (unblocks index_mut / bits_set) would let the centralization complete.

---

8. Key references

• docs/coding-guidelines/proof-engineering.md — "Prefer assume_specification… test the direct form… record any concrete obstacle"; "Centralize trusted boundaries under verified_libs/vstd_extra/src/external/"; "Restrict generic trusted models" (PR prove: id-alloc asterinas/vostd#742 bitvec model is the precedent for a foreign collection).
• verified_libs/vstd_extra/src/external/btree.rs — ExCursorMut<'a,K,V,A> (generic external_type_specification with reject_recursive_types), CursorMutAdditionalSpecFns (custom view trait on a foreign type — the pattern copied here for SmallVecSpecFns), assume_specification<…>[ Path::method ], and get_mut's prophetic final_map (the reference-return precedent).
• verified_libs/vstd_extra/src/array_ptr.rs:384 — TODO "external_type_specification: Const params not yet supported" (the const-param blocker I originally misapplied to SmallVec).
• Memory: vostd-cpu-set-smallvec-tcb-proof.md (A1 proof + full SmallVec findings), vostd-cpu-module-scoped-port.md.