pub struct Opt<T>(pub T);Expand description
The optional combinator that never fails.
If the inner combinator fails, the result is None.
§Note
One might think that the Opt<T> combinator can be encoded as OrdChoice<T, Success>.
However, this is not the case because one cannot prove that Success is disjoint from T.
In fact, there is a fundamental difference between Opt<T> and OrdChoice<Fst, Snd>:
the Disjoint conditions can be aggregated for OrdChoice, making it “nestable”, while
the “productivity” condition cannot be aggregated for Opt (i.e., Opt<Opt<T>> can never be
constructed).
Tuple Fields§
§0: TImplementations§
Trait Implementations§
Source§impl<'x, I, O, T> Combinator<'x, I, O> for Opt<T>where
I: VestInput,
O: VestOutput<I>,
T: Combinator<'x, I, O, SType = &'x <T as Combinator<'x, I, O>>::Type>,
T::V: SecureSpecCombinator<Type = <T::Type as View>::V>,
T::Type: 'x,
impl<'x, I, O, T> Combinator<'x, I, O> for Opt<T>where
I: VestInput,
O: VestOutput<I>,
T: Combinator<'x, I, O, SType = &'x <T as Combinator<'x, I, O>>::Type>,
T::V: SecureSpecCombinator<Type = <T::Type as View>::V>,
T::Type: 'x,
Source§open spec fn ex_requires(&self) -> bool
open spec fn ex_requires(&self) -> bool
{ self.0.ex_requires() }Source§exec fn serialize(
&self,
v: Self::SType,
data: &mut O,
pos: usize,
) -> res : Result<usize, SerializeError>
exec fn serialize( &self, v: Self::SType, data: &mut O, pos: usize, ) -> res : Result<usize, SerializeError>
Source§type SType = &'x <Opt<T> as Combinator<'x, I, O>>::Type
type SType = &'x <Opt<T> as Combinator<'x, I, O>>::Type
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<T: SecureSpecCombinator> SecureSpecCombinator for Opt<T>
impl<T: SecureSpecCombinator> SecureSpecCombinator for Opt<T>
Source§open spec fn is_prefix_secure() -> bool
open spec fn is_prefix_secure() -> bool
{ false }Source§open spec fn is_productive(&self) -> bool
open spec fn is_productive(&self) -> bool
{ false }Source§proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)
proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)
Source§proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)
proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)
Source§proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
Source§proof fn lemma_parse_length(&self, s: Seq<u8>)
proof fn lemma_parse_length(&self, s: Seq<u8>)
Source§proof fn lemma_parse_productive(&self, s: Seq<u8>)
proof fn lemma_parse_productive(&self, s: Seq<u8>)
Source§fn corollary_parse_surjective(&self, v: Self::Type)
fn corollary_parse_surjective(&self, v: Self::Type)
Source§fn corollary_serialize_injective_contraposition(
&self,
v1: Self::Type,
v2: Self::Type,
)
fn corollary_serialize_injective_contraposition( &self, v1: Self::Type, v2: Self::Type, )
Source§fn lemma_serialize_productive(&self, v: Self::Type)
fn lemma_serialize_productive(&self, v: Self::Type)
Source§impl<T: SecureSpecCombinator> SpecCombinator for Opt<T>
impl<T: SecureSpecCombinator> SpecCombinator for Opt<T>
Source§open spec fn wf(&self, v: Self::Type) -> bool
open spec fn wf(&self, v: Self::Type) -> bool
{
match v {
Some(vv) => self.0.wf(vv),
None => true,
}
}Source§open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)>
open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)>
{
if let Some((n, v)) = self.0.spec_parse(s) {
Some((n, Some(v)))
} else {
Some((0, None))
}
}Source§open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8>
open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8>
{
match v {
Some(v) => self.0.spec_serialize(v),
None => Seq::empty(),
}
}Auto Trait Implementations§
impl<T> Freeze for Opt<T>where
T: Freeze,
impl<T> RefUnwindSafe for Opt<T>where
T: RefUnwindSafe,
impl<T> Send for Opt<T>where
T: Send,
impl<T> Sync for Opt<T>where
T: Sync,
impl<T> Unpin for Opt<T>where
T: Unpin,
impl<T> UnwindSafe for Opt<T>where
T: UnwindSafe,
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
§impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: From<T>,
impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: From<T>,
fn obeys_from_spec() -> bool
fn from_spec(v: T) -> VERUS_SPEC__A
§impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: Into<T>,
impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: Into<T>,
fn obeys_into_spec() -> bool
fn into_spec(self) -> T
§impl<T, U> IntoSpecImpl<U> for Twhere
U: From<T>,
impl<T, U> IntoSpecImpl<U> for Twhere
U: From<T>,
fn obeys_into_spec() -> bool
fn into_spec(self) -> U
Source§impl<T, U> SpecTryInto<U> for Twhere
U: SpecTryFrom<T>,
impl<T, U> SpecTryInto<U> for Twhere
U: SpecTryFrom<T>,
Source§open spec fn spec_try_into(self) -> Result<U, <U as SpecTryFrom<T>>::Error>
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
type Error = <U as SpecTryFrom<T>>::Error
The type returned in the event of a conversion error.