Pair

vest_lib::regular::sequence

Struct Pair 

Source 
pub struct Pair<Fst, Snd, Cont> {
    pub fst: Fst,
    pub _snd: PhantomData<Snd>,
    pub snd: Cont,
}
Expand description

Combinator that sequentially applies two combinators, where the second combinator depends on the first one.

Fields§

§fst: Fst

combinators that contain dependencies

§_snd: PhantomData<Snd>

phantom data representing the second combinator (it really should be private, but this is a workaround for Verus’s conservative treatment of opaque types, which doesn’t allow field access of opaque types in open spec functions)

§snd: Cont

closure that captures dependencies and maps them to the dependent combinators

Implementations§

Source§

impl<Fst, Snd, Cont> Pair<Fst, Snd, Cont>
where Fst: View, Snd: View, Cont: View<V = GhostFn<<Fst::V as SpecCombinator>::Type, Snd::V>>, Fst::V: SecureSpecCombinator, Snd::V: SpecCombinator,

Source

pub exec fn new(fst: Fst, snd: Cont) -> o : Self

ensures
o.fst == fst,
o.snd == snd,
o@ == Pair::spec_new(fst@, snd@),

Creates a new Pair combinator.

Source§

impl<Fst, Snd> Pair<Fst, Snd, GhostFn<Fst::Type, Snd>>
where Fst: SecureSpecCombinator, Snd: SpecCombinator,

Source

pub open spec fn spec_new(fst: Fst, snd: GhostFn<Fst::Type, Snd>) -> Self

{
    Pair {
        fst,
        _snd: core::marker::PhantomData,
        snd,
    }
}

Creates a new Pair combinator.

Trait Implementations§

Source§

impl<'x, I, O, Fst, Snd, Cont> Combinator<'x, I, O> for Pair<Fst, Snd, Cont>
where I: VestInput, O: VestOutput<I>, Fst: Combinator<'x, I, O>, Snd: Combinator<'x, I, O>, Fst::V: SecureSpecCombinator<Type = <Fst::Type as View>::V>, Snd::V: SecureSpecCombinator<Type = <Snd::Type as View>::V>, Fst::SType: Copy, Cont: for<'a> Continuation<POrSType<&'a Fst::Type, Fst::SType>, Output = Snd> + View<V = GhostFn<<Fst::Type as View>::V, Snd::V>>, <Fst as Combinator<'x, I, O>>::Type: 'x,

Source§

exec fn length(&self, v: Self::SType) -> usize

Source§

open spec fn ex_requires(&self) -> bool

{
    let spec_snd_dep = self.snd@;
    &&& self.fst.ex_requires()
    &&& forall |i| #[trigger] self.snd.requires(i)
    &&& forall |i, snd| {
        #[trigger] self.snd.ensures(i, snd)
            ==> snd.ex_requires() && snd@ == spec_snd_dep(i@)
    }

}
Source§

exec fn parse(&self, s: I) -> res : Result<(usize, Self::Type), ParseError>

Source§

exec fn serialize( &self, v: Self::SType, data: &mut O, pos: usize, ) -> res : Result<usize, SerializeError>

Source§

type Type = (<Fst as Combinator<'x, I, O>>::Type, <Snd as Combinator<'x, I, O>>::Type)

The result type of parsing
Source§

type SType = (<Fst as Combinator<'x, I, O>>::SType, <Snd as Combinator<'x, I, O>>::SType)

The input type of serialization, often a reference to Self::Type. For “structural” formats though (e.g., crate::regular::sequence::Pair and crate::regular::variant::Choice), this is the tuple/sum of the corresponding Combinator::SType types.
Source§

impl<U1, U2, V1, V2> DisjointFrom<Pair<U2, V2, FnSpec<(<U2 as SpecCombinator>::Type,), V2>>> for SpecPair<U1, V1>
where U1: DisjointFrom<U2> + SecureSpecCombinator, U2: SecureSpecCombinator, V1: SpecCombinator, V2: SpecCombinator,

Source§

open spec fn disjoint_from(&self, other: &SpecPair<U2, V2>) -> bool

{ self.fst.disjoint_from(&other.fst) }
Source§

proof fn parse_disjoint_on(&self, other: &SpecPair<U2, V2>, buf: Seq<u8>)

Source§

impl<Fst, Snd, Cont> View for Pair<Fst, Snd, Cont>
where Fst: View, Snd: View, Cont: View<V = GhostFn<<Fst::V as SpecCombinator>::Type, Snd::V>>, Fst::V: SecureSpecCombinator, Snd::V: SpecCombinator,

Source§

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

{ Pair::spec_new(self.fst@, self.snd@) }
Source§

type V = Pair<<Fst as View>::V, <Snd as View>::V, FnSpec<(<<Fst as View>::V as SpecCombinator>::Type,), <Snd as View>::V>>

Auto Trait Implementations§

§

impl<Fst, Snd, Cont> Freeze for Pair<Fst, Snd, Cont>
where Fst: Freeze, Cont: Freeze,

§

impl<Fst, Snd, Cont> RefUnwindSafe for Pair<Fst, Snd, Cont>
where Fst: RefUnwindSafe, Cont: RefUnwindSafe, Snd: RefUnwindSafe,

§

impl<Fst, Snd, Cont> Send for Pair<Fst, Snd, Cont>
where Fst: Send, Cont: Send, Snd: Send,

§

impl<Fst, Snd, Cont> Sync for Pair<Fst, Snd, Cont>
where Fst: Sync, Cont: Sync, Snd: Sync,

§

impl<Fst, Snd, Cont> Unpin for Pair<Fst, Snd, Cont>
where Fst: Unpin, Cont: Unpin, Snd: Unpin,

§

impl<Fst, Snd, Cont> UnwindSafe for Pair<Fst, Snd, Cont>
where Fst: UnwindSafe, Cont: UnwindSafe, Snd: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T
where T: View, <T as View>::V: SpecFrom<<T as View>::V>,

Source§

exec fn ex_from(t: T) -> res : T

Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where T: View, U: View + From<T>, <U as View>::V: SpecFrom<<T as View>::V>,

Source§

exec fn ex_into(self) -> U

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> T

§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

impl<T> SpecFrom<T> for T

Source§

open spec fn spec_from(t: T) -> T

{ t }
Source§

impl<T, U> SpecInto<U> for T
where U: SpecFrom<T>,

Source§

open spec fn spec_into(self) -> U

{ U::spec_from(self) }
Source§

impl<T, U> SpecTryInto<U> for T
where U: SpecTryFrom<T>,

Source§

open spec fn spec_try_into(self) -> Result<U, <U as SpecTryFrom<T>>::Error>

{ U::spec_try_from(self) }
Source§

type Error = <U as SpecTryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

§

fn obeys_try_from_spec() -> bool

§

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where T: View, U: View + TryFrom<T>, <U as View>::V: SpecTryFrom<<T as View>::V>,

Source§

exec fn ex_try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>