Skip to main content

TrackDrop

vstd_extra::drop_tracking

Trait TrackDrop 

Source 
pub trait TrackDrop: Sized {
    type State;
    type Key;

    // Required methods
    spec fn key(self) -> Self::Key;
    spec fn constructor_requires(self, s: Self::State) -> bool;
    spec fn constructor_ensures(
        self,
        s0: Self::State,
        s1: Self::State,
        obl_key: Self::Key,
    ) -> bool;
    proof fn constructor_spec(self, tracked s: &mut Self::State) -> tracked obl : DropObligation<Self::Key>;
    spec fn drop_requires(self, s: Self::State) -> bool;
    spec fn drop_ensures(
        self,
        s0: Self::State,
        s1: Self::State,
        obl_key: Self::Key,
    ) -> bool;
    spec fn consume_requires(self, s: Self::State, obl_key: Self::Key) -> bool;
    spec fn consume_ensures(
        self,
        s0: Self::State,
        s1: Self::State,
        obl_key: Self::Key,
    ) -> bool;
    proof fn consume_obligation(
        self,
tracked         s: &mut Self::State,
tracked         obl: DropObligation<Self::Key>,
    );
}

Required Associated Types§

Source

type State

Source

type Key

Identifies which obligation this resource holds in the ledger.

Required Methods§

Source

spec fn key(self) -> Self::Key

The ledger key for this instance. Pinned by constructor_spec’s ensures and Drop::drop’s requires.

Source

spec fn constructor_requires(self, s: Self::State) -> bool

Source

spec fn constructor_ensures( self, s0: Self::State, s1: Self::State, obl_key: Self::Key, ) -> bool

Source

proof fn constructor_spec(self, tracked s: &mut Self::State) -> tracked obl : DropObligation<Self::Key>

requires
self.constructor_requires(*old(s)),
ensures
self.constructor_ensures(*old(s), *final(s), obl.value()),
obl.value() == self.key(),
Source

spec fn drop_requires(self, s: Self::State) -> bool

Source

spec fn drop_ensures( self, s0: Self::State, s1: Self::State, obl_key: Self::Key, ) -> bool

Postcondition of Drop::drop. obl_id is the [Loc] of the consumed obligation token — ledger-enforcing impls reference it to pin the ledger transition (e.g. “the entry at obl_id was removed”); ledger-less impls ignore it.

Source

spec fn consume_requires(self, s: Self::State, obl_key: Self::Key) -> bool

Precondition for “consume the obligation without running the destructor” (see [ConsumeDrop]). obl_id is exposed so ledger-enforcing impls can require the entry to be outstanding.

Source

spec fn consume_ensures( self, s0: Self::State, s1: Self::State, obl_key: Self::Key, ) -> bool

Postcondition for consuming an obligation. Encodes any ledger mutation (e.g. redeeming the entry at obl_id). Impls without a ledger keep s0 == s1.

Source

proof fn consume_obligation(self, tracked s: &mut Self::State, tracked obl: DropObligation<Self::Key>)

requires
self.consume_requires(*old(s), obl.value()),
obl.value() == self.key(),
ensures
self.consume_ensures(*old(s), *final(s), obl.value()),

Consume the obligation token without running the destructor body. Used by [ConsumeDrop::new] to discharge the verifier’s linear-drop obligation when the underlying resource is intentionally leaked (or freed via a separate path).

Impls with a real ledger should call a paired redeem axiom here; impls without (Key = ()) can leave the body empty — obl is silently dropped, which is fine because no ledger entry needs to shrink to match.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§