Enum Sum 

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

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

Variants

Left(L)

Right(R)

Implementations

impl<L, R> Sum<L, R>

pub fn arrow_Left_0(self) -> L

pub fn arrow_Right_0(self) -> R

impl<L, R> Sum<L, R>

pub open spec fn left(self) -> L

{ self->Left_0 }

pub open spec fn right(self) -> R

{ self->Right_0 }

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

returns

Self::Left(left),

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

returns

Self::Right(right),

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

requires

self is Left,

returns

self->Left_0,

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

requires

self is Right,

returns

self->Right_0,

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

requires

self is Left,

ensures

*res == self->Left_0,

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

requires

self is Right,

ensures

*res == self->Right_0,

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

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

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

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

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,

*final(self) is Left,

final(self)->Left_0 == new_left,

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,

*final(self) is Right,

final(self)->Right_0 == new_right,

Trait Implementations

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

open spec fn inv(self) -> bool

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

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

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

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

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

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

open spec fn unit() -> Self

{ SumSP::Unit }

proof fn commutative(a: Self, b: Self)

proof fn associative(a: Self, b: Self, c: Self)

proof fn op_unit(a: Self)

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

open spec fn view(&self) -> Self::V

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

type V = Sum<<L as View>::V, <R as View>::V>