Enum Sum

Source

pub enum Sum<L, R> {
    Left(L),
    Right(R),
}

Expand description

The Sum Type, corresponding to the Either type in Rust.

Variants§

§

Left(L)

§

Right(R)

Implementations§

Source §

pub open spec fn left(self) -> L

{ self->Left_0 }

Source

pub open spec fn right(self) -> R

{ self->Right_0 }

Source

pub proof fn new_left(tracked left: L) -> tracked res : Self

returns

Self::Left(left),

Source

pub proof fn new_right(tracked right: R) -> tracked res : Self

returns

Self::Right(right),

Source

pub proof fn tracked_take_left(tracked self) -> tracked res : L

requires

self is Left,

returns

self->Left_0,

Source

pub proof fn tracked_take_right(tracked self) -> tracked res : R

requires

self is Right,

returns

self->Right_0,

Source

pub proof fn tracked_borrow_left(tracked &self) -> tracked res : &L

requires

self is Left,

ensures

*res == self->Left_0,

Source

pub proof fn tracked_borrow_right(tracked &self) -> tracked res : &R

requires

self is Right,

ensures

*res == self->Right_0,

Source

pub open spec fn lift_map_left<K>(m: Map<K, L>) -> Map<K, Self>

{ m.map_values(|w| Sum::<L, R>::Left(w)) }

Source

pub open spec fn lift_map_right<K>(m: Map<K, R>) -> Map<K, Self>

{ m.map_values(|v| Sum::<L, R>::Right(v)) }

Source

pub proof fn tracked_swap_left(tracked &mut self, tracked new_left: L) -> tracked res : L

requires

*old(self) is Left,

ensures

res == old(self)->Left_0,

*self is Left,

self->Left_0 == new_left,

Source

pub proof fn tracked_swap_right(tracked &mut self, tracked new_right: R) -> tracked res : R

requires

*old(self) is Right,

ensures

res == old(self)->Right_0,

*self is Right,

self->Right_0 == new_right,

Trait Implementations§

Source §

impl<L: Inv, R: Inv> Inv for Sum<L, R>

Source §

open spec fn inv(self) -> bool

{
    match self {
        Self::Left(left) => left.inv(),
        Self::Right(right) => right.inv(),
    }
}

Source §

impl<A, B, const TOTAL: u64> Protocol<(), Sum<A, B>> for CsumP<A, B, TOTAL>

Source §

open spec fn op(self, other: Self) -> Self

{
    match (self, other) {
        (CsumP::Unit, x) => x,
        (x, CsumP::Unit) => x,
        (CsumP::Cinl(ov1, n1, b1), CsumP::Cinl(ov2, n2, b2)) => {
            if !self.is_valid() || !other.is_valid() || n1 + n2 > TOTAL || b1 && b2
                || ov1 is Some && ov2 is Some
            {
                CsumP::CsumInvalid
            } else {
                CsumP::Cinl(if ov1 is Some { ov1 } else { ov2 }, n1 + n2, b1 || b2)
            }
        }
        (CsumP::Cinr(ov1, n1, b1), CsumP::Cinr(ov2, n2, b2)) => {
            if !self.is_valid() || !other.is_valid() || n1 + n2 > TOTAL || b1 && b2
                || ov1 is Some && ov2 is Some
            {
                CsumP::CsumInvalid
            } else {
                CsumP::Cinr(if ov1 is Some { ov1 } else { ov2 }, n1 + n2, b1 || b2)
            }
        }
        _ => CsumP::CsumInvalid,
    }
}

Source §

open spec fn rel(self, s: Map<(), Sum<A, B>>) -> bool

{
    match self {
        CsumP::Unit => s.is_empty(),
        CsumP::Cinl(None, n, true) => 0 <= n <= TOTAL && s.is_empty(),
        CsumP::Cinl(Some(a), n, true) => {
            0 <= n <= TOTAL && s.contains_key(()) && s[()] == Sum::<A, B>::Left(a)
        }
        CsumP::Cinr(None, n, true) => 0 <= n <= TOTAL && s.is_empty(),
        CsumP::Cinr(Some(b), n, true) => {
            0 <= n <= TOTAL && s.contains_key(()) && s[()] == Sum::<A, B>::Right(b)
        }
        _ => false,
    }
}