Skip to main content

Implicit

vest_lib::combinators::implicit

Struct Implicit 

Source 
pub struct Implicit<Head, Tail>(pub Head, pub Tail);
Expand description

Dependent sequential combinator with deterministic key recovery.

Parsing semantics: parse Head to get a key, then parse the body via Tail::apply(key). Only the body value is returned.

The key is recovered via Tail::recover(value) during serialization.

§Consistency

A value v: Tail::Val is consistent with Implicit(Head, Tail) iff

let key = self.1.recover(v);
self.0.consistent(key) && self.1.apply(key).consistent(v)

§Unambiguity

self.0.unambiguous() &&
forall|key: Head::PVal| #[trigger] (self.1.apply(key)).unambiguous()

Tuple Fields§

§0: Head§1: Tail

Trait Implementations§

Source§

impl<Head: Clone, Tail: Clone> Clone for Implicit<Head, Tail>

Source§

exec fn clone(&self) -> cloned : Self

ensures
call_ensures(Head::clone, (&self.0,), cloned.0),
call_ensures(Tail::clone, (&self.1,), cloned.1),
1.0.0 (const: unstable) · Source§

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

Performs copy-assignment from source. Read more
Source§

impl<Head, Tail> Consistency for Implicit<Head, Tail>
where Head: Consistency, Tail: DepCombinator<Key = Head::Val>,

Source§

open spec fn consistent(&self, value: Self::Val) -> bool

{
    let key = self.1.recover(value);
    self.0.consistent(key) && self.1.apply(key).consistent(value)
}
Source§

type Val = <Tail as DepCombinator>::Val

The type of values whose consistency is being checked.
Source§

impl<Head, Nested> DepCombinator for Implicit<Head, Nested>
where Head: Consistency, Nested: DepCombinator<Key = Head::Val>,

Source§

open spec fn apply(&self, key: Self::Key) -> Self::Body

{ self.1.apply(key) }
Source§

open spec fn recover(&self, value: Self::Val) -> Self::Key

{ self.1.recover(value) }
Source§

open spec fn recover_inv(&self) -> bool

{ self.1.recover_inv() }
Source§

proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val)

Source§

type Key = <Head as Consistency>::Val

The type of keys parsed by the head combinator/to be recovered during serialization.
Source§

type Val = <Nested as DepCombinator>::Val

The type of values consumed/produced by the body combinator.
Source§

type Body = <Nested as DepCombinator>::Body

The type of the body combinator produced by apply.
Source§

impl<Head, Tail> EquivSerializers for Implicit<Head, Tail>
where Head: EquivSerializersGeneral, Tail: DepCombinator<Key = Head::SVal>, Tail::Body: EquivSerializers<SVal = Tail::Val>,

Source§

open spec fn equiv_inv(&self) -> bool

{
    &&& self.0.equiv_general_inv()
    &&& forall |key: Head::SVal| #[trigger] self.1.apply(key).equiv_inv()

}
Source§

proof fn lemma_serialize_equiv_on_empty(&self, value: Self::SVal)

Source§

impl<Head, Tail> EquivSerializersGeneral for Implicit<Head, Tail>
where Head: EquivSerializersGeneral, Tail: DepCombinator<Key = Head::SVal>, Tail::Body: EquivSerializersGeneral<SVal = Tail::Val>,

Source§

open spec fn equiv_general_inv(&self) -> bool

{
    &&& self.0.equiv_general_inv()
    &&& forall |key: Head::SVal| #[trigger] self.1.apply(key).equiv_general_inv()

}
Source§

proof fn lemma_serialize_equiv(&self, value: Self::SVal, obuf: Seq<u8>)

Source§

impl<Head, Tail> GoodSerializer for Implicit<Head, Tail>
where Head: GoodSerializer, Tail: DepCombinator<Key = Head::SVal>, Tail::Body: GoodSerializer<T = Tail::Val>,

Source§

open spec fn serialize_inv(&self) -> bool

{
    &&& self.0.serialize_inv()
    &&& forall |key: Head::SVal| #[trigger] self.1.apply(key).serialize_inv()

}
Source§

proof fn lemma_serialize_len(&self, value: Self::SVal)

Source§

impl<Head, Tail> NoLookAhead for Implicit<Head, Tail>
where Head: NoLookAhead, Tail: DepCombinator<Key = Head::PVal>, Tail::Body: NoLookAhead<PVal = Tail::Val>,

Source§

open spec fn no_lookahead_inv(&self) -> bool

{
    &&& self.0.no_lookahead_inv()
    &&& forall |key: Head::PVal| #[trigger] self.1.apply(key).no_lookahead_inv()

}
Source§

proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>)

Source§

fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>)

Read more
Source§

impl<Head, Tail> NonMalleable for Implicit<Head, Tail>
where Head: SoundParser + NonMalleable, Tail: DepCombinator<Key = Head::T>, Tail::Body: SoundParser<T = Tail::Val> + NonMalleable,

Source§

open spec fn nonmal_inv(&self) -> bool

{
    &&& self.0.nonmal_inv()
    &&& self.0.sound_inv()
    &&& forall |key: Head::PVal| #[trigger] self.1.apply(key).nonmal_inv()
    &&& forall |key: Head::PVal| #[trigger] self.1.apply(key).sound_inv()
    &&& self.1.recover_inv()

}
Source§

proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)

Source§

impl<Head, Tail> NonTailFmt for Implicit<Head, Tail>
where Head: NonTailFmt, Tail: DepCombinator<Key = Head::SValue>, Tail::Body: NonTailFmt<T = Tail::Val>,

Source§

open spec fn serialize_dps_inv(&self) -> bool

{
    &&& self.0.serialize_dps_inv()
    &&& forall |key: Head::SValue| #[trigger] self.1.apply(key).serialize_dps_inv()

}
Source§

proof fn lemma_serialize_dps_prepend(&self, value: Self::SValue, obuf: Seq<u8>)

Source§

proof fn lemma_serialize_dps_len(&self, value: Self::SValue, obuf: Seq<u8>)

Source§

impl<Head, Tail> Productive for Implicit<Head, Tail>
where Head: Productive, Tail: DepCombinator<Key = Head::PVal>, Tail::Body: Productive<PVal = Tail::Val>,

Source§

open spec fn productive_inv(&self) -> bool

{
    ||| self.0.productive_inv()
    ||| forall |key: Head::PVal| #[trigger] self.1.apply(key).productive_inv()

}
Source§

proof fn lemma_productive(&self, s: Seq<u8>)

Source§

impl<Head, Tail> SPRoundTripDps for Implicit<Head, Tail>
where Head: SPRoundTripDps + NonTailFmt, Tail: DepCombinator<Key = Head::T>, Tail::Body: SPRoundTripDps<T = Tail::Val>,

Source§

open spec fn unambiguous(&self) -> bool

{
    &&& self.0.serialize_dps_inv()
    &&& self.0.unambiguous()
    &&& forall |key: Head::T| #[trigger] self.1.apply(key).unambiguous()

}
Source§

proof fn theorem_serialize_dps_parse_roundtrip(&self, value: Self::T, obuf: Seq<u8>)

Source§

impl<Head, Tail> SafeParser for Implicit<Head, Tail>
where Head: SafeParser, Tail: DepCombinator<Key = Head::PVal>, Tail::Body: SafeParser<PVal = Tail::Val>,

Source§

open spec fn safe_inv(&self) -> bool

{
    &&& self.0.safe_inv()
    &&& forall |key: Head::PVal| #[trigger] self.1.apply(key).safe_inv()

}
Source§

proof fn lemma_parse_safe(&self, ibuf: Seq<u8>)

Source§

impl<Head, Tail> SoundParser for Implicit<Head, Tail>
where Head: SoundParser, Tail: DepCombinator<Key = Head::PVal>, Tail::Body: SoundParser<T = Tail::Val>,

Source§

open spec fn sound_inv(&self) -> bool

{
    &&& self.0.sound_inv()
    &&& forall |key: Head::PVal| #[trigger] self.1.apply(key).sound_inv()
    &&& self.1.recover_inv()

}
Source§

proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>)

Source§

proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>)

Source§

impl<Head, Tail> SpecByteLen for Implicit<Head, Tail>
where Head: SpecByteLen, Tail: DepCombinator<Key = Head::T>, Tail::Body: SpecByteLen<T = Tail::Val>,

Source§

open spec fn byte_len(&self, value: Self::T) -> nat

{
    let key = self.1.recover(value);
    let body = self.1.apply(key);
    self.0.byte_len(key) + body.byte_len(value)
}
Source§

type T = <Tail as DepCombinator>::Val

The type of values whose byte length is being computed.
Source§

impl<Head, Tail> SpecParser for Implicit<Head, Tail>
where Head: SpecParser, Tail: DepCombinator<Key = Head::PVal>, Tail::Body: SpecParser<PVal = Tail::Val>,

Source§

open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)>

{
    match self.0.spec_parse(ibuf) {
        Some((n1, key)) => {
            let body = self.1.apply(key);
            match body.spec_parse(ibuf.skip(n1)) {
                Some((n2, value)) => Some((n1 + n2, value)),
                None => None,
            }
        }
        None => None,
    }
}
Source§

type PVal = <Tail as DepCombinator>::Val

The type of parsed values.
Source§

impl<Head, Tail> SpecSerializer for Implicit<Head, Tail>
where Head: SpecSerializer, Tail: DepCombinator<Key = Head::SVal>, Tail::Body: SpecSerializer<SVal = Tail::Val>,

Source§

open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8>

{
    let key = self.1.recover(value);
    let body = self.1.apply(key);
    self.0.spec_serialize(key) + body.spec_serialize(value)
}
Source§

type SVal = <Tail as DepCombinator>::Val

The type of values to be serialized.
Source§

impl<Head, Tail> SpecSerializerDps for Implicit<Head, Tail>
where Head: SpecSerializerDps, Tail: DepCombinator<Key = Head::SValue>, Tail::Body: SpecSerializerDps<SValue = Tail::Val>,

Source§

open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8>

{
    let key = self.1.recover(value);
    let body = self.1.apply(key);
    self.0.spec_serialize_dps(key, body.spec_serialize_dps(value, obuf))
}
Source§

type SValue = <Tail as DepCombinator>::Val

The type of values to be serialized.
Source§

impl<Head, Tail> StaticByteLen for Implicit<Head, Tail>
where Head: StaticByteLen, Tail: DepCombinator<Key = Head::T>, Tail::Body: StaticByteLen<T = Tail::Val>,

Source§

open spec fn static_byte_len() -> nat

{ Head::static_byte_len() + Tail::Body::static_byte_len() }
Source§

proof fn lemma_static_len_matches_byte_len(&self, v: Self::T)

Source§

impl<Head, Tail> ValueByteLen for Implicit<Head, Tail>
where Head: StaticByteLen, Tail: DepCombinator<Key = Head::T>, Tail::Body: ValueByteLen<T = Tail::Val>,

Source§

open spec fn value_byte_len(value: Self::T) -> nat

{ Head::static_byte_len() + Tail::Body::value_byte_len(value) }
Source§

proof fn lemma_value_len_matches_byte_len(&self, value: Self::T)

Source§

impl<Head: Copy, Tail: Copy> Copy for Implicit<Head, Tail>

Auto Trait Implementations§

§

impl<Head, Tail> Freeze for Implicit<Head, Tail>
where Head: Freeze, Tail: Freeze,

§

impl<Head, Tail> RefUnwindSafe for Implicit<Head, Tail>
where Head: RefUnwindSafe, Tail: RefUnwindSafe,

§

impl<Head, Tail> Send for Implicit<Head, Tail>
where Head: Send, Tail: Send,

§

impl<Head, Tail> Sync for Implicit<Head, Tail>
where Head: Sync, Tail: Sync,

§

impl<Head, Tail> Unpin for Implicit<Head, Tail>
where Head: Unpin, Tail: Unpin,

§

impl<Head, Tail> UnsafeUnpin for Implicit<Head, Tail>
where Head: UnsafeUnpin, Tail: UnsafeUnpin,

§

impl<Head, Tail> UnwindSafe for Implicit<Head, Tail>
where Head: UnwindSafe, Tail: 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> CloneToUninit for T
where T: Clone,

Source§

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)
Performs copy-assignment from self to dest. Read more
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 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<C> NonAmbiguous for C
where C: SPRoundTrip,

Source§

open spec fn nonamb_inv(&self) -> bool

{ self.sp_roundtrip_inv() }
Source§

proof fn lemma_serialize_injective( &self, v1: <C as Consistency>::Val, v2: <C as Consistency>::Val, )

Source§

fn corollary_serialize_injective_contrapositive( &self, v1: Self::Val, v2: Self::Val, )

Read more
Source§

impl<C> PSRoundTrip for C
where C: SPRoundTrip + NonMalleable + SoundParser,

Source§

open spec fn ps_roundtrip_inv(&self) -> bool

{ self.safe_inv() && self.sound_inv() && self.nonmal_inv() && self.sp_roundtrip_inv() }
Source§

proof fn theorem_parse_serialize_roundtrip(&self, ibuf: Seq<u8>)

Source§

fn corollary_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)

Read more
Source§

impl<C> SPRoundTrip for C
where C: SPRoundTripDps + GoodSerializer + EquivSerializers,

Source§

open spec fn sp_roundtrip_inv(&self) -> bool

{ self.serialize_inv() && self.equiv_inv() && self.unambiguous() }
Source§

proof fn theorem_serialize_parse_roundtrip(&self, v: <C as SpecByteLen>::T)

Source§

impl<T, S> SerializerExt<T> for S
where S: SpecByteLen<T = <T as DeepView>::V> + SpecSerializer<SVal = <T as DeepView>::V> + Consistency<Val = <T as DeepView>::V>, T: DeepView + ?Sized,

Source§

fn serialize<'a>(&self, v: &T, obuf: &'a mut [u8])
where Self: Serializer<OutputSlice<'a>, T>,

Read more
Source§

fn serialize_with_vec(&self, v: &T, obuf: &mut Vec<u8>)
where Self: Serializer<Vec<u8>, T>,

Read more
Source§

impl<T> ToOwned for T
where T: Clone,

Source§

type Owned = T

The resulting type after obtaining ownership.
Source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
Source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
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 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>

Source§

impl<T> SpecCombinator for T
where T: SpecParser<PVal = <T as SpecByteLen>::T> + SpecByteLen + SpecSerializer<SVal = <T as SpecByteLen>::T> + Consistency<Val = <T as SpecByteLen>::T> + SpecSerializerDps<SValue = <T as SpecByteLen>::T>,

§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A

Source§

impl<Body> StrictCombinator for Body
where Body: SafeParser + Productive + SoundParser + NonMalleable + GoodSerializer + NonTailFmt + SPRoundTripDps + EquivSerializersGeneral,