pub type SpecPair<Fst, Snd> = Pair<Fst, Snd, GhostFn<<Fst as SpecCombinator>::Type, Snd>>;Expand description
Alias for a spec dependent pair combinator.
Aliased Type§
pub struct SpecPair<Fst, Snd> {
pub fst: Fst,
pub _snd: PhantomData<Snd>,
pub snd: FnSpec<(<Fst as SpecCombinator>::Type,), Snd>,
}Fields§
§fst: Fstcombinators 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: FnSpec<(<Fst as SpecCombinator>::Type,), Snd>closure that captures dependencies and maps them to the dependent combinators
Trait Implementations§
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,
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
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>)
proof fn parse_disjoint_on(&self, other: &SpecPair<U2, V2>, buf: Seq<u8>)
Source§impl<Fst, Snd> SecureSpecCombinator for SpecPair<Fst, Snd>where
Fst: SecureSpecCombinator,
Snd: SecureSpecCombinator,
impl<Fst, Snd> SecureSpecCombinator for SpecPair<Fst, Snd>where
Fst: SecureSpecCombinator,
Snd: SecureSpecCombinator,
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§open spec fn is_prefix_secure() -> bool
open spec fn is_prefix_secure() -> bool
{ Fst::is_prefix_secure() && Snd::is_prefix_secure() }Source§proof fn lemma_prefix_secure(&self, buf: Seq<u8>, s2: Seq<u8>)
proof fn lemma_prefix_secure(&self, buf: Seq<u8>, s2: Seq<u8>)
Source§proof fn lemma_parse_length(&self, s: Seq<u8>)
proof fn lemma_parse_length(&self, s: Seq<u8>)
Source§open spec fn is_productive(&self) -> bool
open spec fn is_productive(&self) -> bool
{
||| self.fst.is_productive()
||| forall |v1| #[trigger] ((self.snd)(v1)).is_productive()
}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<Fst, Snd> SpecCombinator for SpecPair<Fst, Snd>where
Fst: SecureSpecCombinator,
Snd: SpecCombinator,
impl<Fst, Snd> SpecCombinator for SpecPair<Fst, Snd>where
Fst: SecureSpecCombinator,
Snd: SpecCombinator,
Source§open spec fn requires(&self) -> bool
open spec fn requires(&self) -> bool
{
&&& Fst::is_prefix_secure()
&&& self.fst.requires()
&&& forall |i: Fst::Type| #[trigger] (self.snd)(i).requires()
}Source§open spec fn wf(&self, v: Self::Type) -> bool
open spec fn wf(&self, v: Self::Type) -> bool
{
&&& self.fst.wf(v.0)
&&& (self.snd)(v.0).wf(v.1)
}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, v1)) = self.fst.spec_parse(s) {
let snd = (self.snd)(v1);
if let Some((m, v2)) = snd.spec_parse(s.skip(n as int)) {
Some((n + m, (v1, v2)))
} else {
None
}
} else {
None
}
}Source§open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8>
open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8>
{
let snd = (self.snd)(v.0);
let buf1 = self.fst.spec_serialize(v.0);
let buf2 = snd.spec_serialize(v.1);
buf1 + buf2
}Source§type Type = (<Fst as SpecCombinator>::Type, <Snd as SpecCombinator>::Type)
type Type = (<Fst as SpecCombinator>::Type, <Snd as SpecCombinator>::Type)
The view of [
Combinator::Result].