pub struct DropObligation<R> { /* private fields */ }Expand description
A linear-looking “must drop” obligation tied to a value of type R.
R is the key type used to identify the resource in the State’s
obligation ledger — e.g. Range<Paddr> for a Segment<M>, usize for a
per-slot resource, () for impls that pipe the token through without a
per-instance ledger. Two-layer enforcement (the design that survives
Verus’s affineness):
- Token (this type): an
ExclusiveGhost<R>wrapper. Eachallocproduces a unique [Loc]; two outstanding tokens can be proven distinct viaDropObligation::validate_with_other. No external_body axioms — the allocation is verified byvstd’s resource algebra. - Ledger (in State): optional. For impls that opt in, the State
carries a set/multiset of outstanding keys; mint adds, redeem removes,
and the State’s
clean_inv()(or any boundary predicate) requires the set to be empty (or the per-slot counter to be zero). Combined with1, the linear guarantee is sound: silently dropping the token leaves the ledger non-empty and breaks the boundary check.
Impls that don’t add a per-state ledger still pass tokens through — they get the API uniformity but not the enforcement.
Implementations§
Source§impl<R> DropObligation<R>
impl<R> DropObligation<R>
Sourcepub closed spec fn id(self) -> Loc
pub closed spec fn id(self) -> Loc
Unique identifier of this token. Two outstanding DropObligations
can be proven distinct via Self::validate_with_other.
Sourcepub proof fn tracked_mint(value: R) -> tracked res : DropObligation<R>
pub proof fn tracked_mint(value: R) -> tracked res : DropObligation<R>
res.value() == value,Mint a fresh obligation token. Sound on its own (no axiom — the
allocation goes through vstd’s resource algebra and is verified).
Two legitimate uses:
- Inside an impl that opts out of per-state-ledger enforcement
(e.g.
Key = ()impls): the token is a no-op marker; the trait API stays uniform but noclean_inv()enforcement applies. - As the underlying allocator for a paired mint axiom on
HasObligations— the axiom adds the ledger entry alongside.
Sourcepub proof fn validate_with_other(tracked &mut self, tracked other: &Self)
pub proof fn validate_with_other(tracked &mut self, tracked other: &Self)
*old(self) == *final(self),final(self).id() != other.id(),Two outstanding obligations have distinct Locs.