Skip to main content

TrackDrop

vstd_extra::drop_tracking

Trait TrackDrop 

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

    // Required methods
    spec fn tracked_redeem_requires(self, s: Self::State) -> bool;
    spec fn tracked_redeem_ensures(
        self,
        s0: Self::State,
        s1: Self::State,
        obl: Self::Obligation,
    ) -> bool;
    proof fn tracked_redeem(self, tracked s: &mut Self::State) -> tracked obl : Self::Obligation;
    spec fn drop_requires(self, s: Self::State, obl: Self::Obligation) -> bool;
    spec fn drop_ensures(
        self,
        s0: Self::State,
        s1: Self::State,
        obl: Self::Obligation,
    ) -> bool;
}
Expand description

A protocol for associating a value with a permission used by its verified drop implementation.

This trait only defines the shape of the protocol. Implementing it does not by itself guarantee that TrackDrop::Obligation is linear, unforgeable, or authoritatively tied to TrackDrop::State. In particular, an implementation may intentionally use a trivial obligation and perform no drop-permission checking.

Implementations that rely on this protocol for safety are responsible for establishing all of the following properties in their concrete specifications and proofs:

  • an issued obligation is associated with the value for which it was issued;
  • the obligation cannot be forged or duplicated;
  • the state records enough authoritative information to detect a lost outstanding obligation; and
  • Drop::drop consumes the obligation and performs the corresponding state transition exactly once.

Required Associated Types§

Source

type State

A ghost state that originally holds the authoritative drop permission.

Source

type Obligation

The type of the drop permission.

This permission does not necessarily represent the full permission to drop the value, as TrackDrop::drop_requires still takes a TrackDrop::State parameter.

Required Methods§

Source

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

Source

spec fn tracked_redeem_ensures( self, s0: Self::State, s1: Self::State, obl: Self::Obligation, ) -> bool

Source

proof fn tracked_redeem(self, tracked s: &mut Self::State) -> tracked obl : Self::Obligation

requires
self.tracked_redeem_requires(*old(s)),
ensures
self.tracked_redeem_ensures(*old(s), *final(s), obl),

Gives the drop permission to the value.

Source

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

Precondition of Drop::drop.

Source

spec fn drop_ensures( self, s0: Self::State, s1: Self::State, obl: Self::Obligation, ) -> bool

Postcondition of Drop::drop.

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§