Struct Subset 

pub struct Subset<T: InhabitedInvariant>(/* private fields */);

A subset type.

This the same as T, with one exception: the invariant for T will also be verified in logic.

Example

struct Pair(i32);
impl Invariant for Pair {
    #[logic] fn invariant(self) -> bool { self.0 % 2 == 0 }
}
impl InhabitedInvariant for Pair {
    #[logic]
    #[ensures(result.invariant())]
    fn inhabits() -> Self { Self(0i32) }
}

#[logic]
fn pair_in_logic(x: Subset<Pair>) {
    proof_assert!(x.0 % 2 == 0);
}

Implementations

impl<T: InhabitedInvariant> Subset<T>

pub fn new_logic(x: T) -> Self

Create a new element of Subset<T> in logic.

As per the documentation of Subset, the returned value will satisfy T’s type invariant.

(opaque)

requires

x.invariant()

ensures

result@ == x

pub fn view_inj(self, other: Self)

Characterize that Subset<T> indeed contains a T (and only a T).

Example

#[requires(x == y@)]
fn foo<T: InhabitedInvariant>(x: T, y: Subset<T>) {
    let x = Subset::new(x);
    let _ = snapshot!(Subset::<T>::view_inj);
    proof_assert!(x == y);
}

(opaque)

requires

self@ == other@

ensures

self == other

pub fn new(x: T) -> Self

Create a new element of Subset<T>.

Example

// Use the `Pair` type defined in `Subset`'s documentation

let p = Subset::new(Pair(0));
proof_assert!(p@.0 == 0i32);

terminates

ghost

ensures

result == Self::new_logic(x)

pub fn into_inner(self) -> T

Unwrap the Subset to get the inner value.

Example

// Use the `Pair` type defined in `Subset`'s documentation

fn changes_pair(p: &mut Subset<Pair>) { /* ... */ }

let mut p = Subset::new(Pair(0));
changes_pair(&mut p);
let inner = p.into_inner();
proof_assert!(inner.0 % 2 == 0);

terminates

ghost

ensures

result == self@

Trait Implementations

impl<T: InhabitedInvariant + Clone> Clone for Subset<T>

fn clone(&self) -> Self

ensures

T::clone.postcondition((&(self@),), result@)

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<T: InhabitedInvariant + DeepModel> DeepModel for Subset<T>

fn deep_model(self) -> T::DeepModelTy

(inline)

type DeepModelTy = <T as DeepModel>::DeepModelTy

impl<T: InhabitedInvariant> Deref for Subset<T>

fn deref(&self) -> &Self::Target

terminates

ghost

ensures

*result == self@

type Target = T

The resulting type after dereferencing.

impl<T: InhabitedInvariant> DerefMut for Subset<T>

fn deref_mut(&mut self) -> &mut Self::Target

terminates

ghost

ensures

*result == self@

ensures

^result == (^self)@

impl<T: InhabitedInvariant + DeepModel + PartialEq> PartialEq for Subset<T>

fn eq(&self, rhs: &Self) -> bool

ensures

result == (self.deep_model() == rhs.deep_model())

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<T: InhabitedInvariant> Resolve for Subset<T>

fn resolve(self) -> bool

(open, prophetic, inline)

pearlite! { resolve(self@) }

fn resolve_coherence(self)

(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<T: InhabitedInvariant> View for Subset<T>

fn view(self) -> T

(opaque)

ensures

result.invariant()

type ViewTy = T

impl<T: InhabitedInvariant + Copy> Copy for Subset<T>

impl<T: InhabitedInvariant + DeepModel + Eq> Eq for Subset<T>