Struct Mapped 

pub struct Mapped<Inner, M> {
    pub inner: Inner,
    pub mapper: M,
}

Mapped { inner, mapper } transforms the inner combinator’s value type.

Lossless mappers preserve all format properties including parser soundness and non-malleability, while lossy mappers may introduce malleability.

Fields

inner: Inner

The inner combinator whose values are being transformed.

mapper: M

The mapping between the inner and outer value types.

Trait Implementations

impl<Inner, M, MRev, T> ByteLen<T> for Mapped<Inner, BiMap<M, MRev>>

where T: DeepView, M: SpecMap<Input = MRev::Output, Output = T::V>, MRev: SpecMap<Input = T::V> + for<'x> Map<&'x T>, Inner: for<'x> ByteLen<<MRev as Map<&'x T>>::O>,

open spec fn exec_inv(&self) -> bool

{ self.inner.exec_inv() }

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

impl<Inner: Clone, M: Clone> Clone for Mapped<Inner, M>

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

ensures

call_ensures(Inner::clone, (&self.inner,), cloned.inner),

call_ensures(M::clone, (&self.mapper,), cloned.mapper),

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

Performs copy-assignment from source.

impl<Inner, M, MRev> Consistency for Mapped<Inner, BiMap<M, MRev>>

where Inner: Consistency, M: SpecMap<Input = Inner::Val>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

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

{ self.inner.consistent(self.mapper.1.spec_map(v)) }

type Val = <M as SpecMap>::Output

The type of values whose consistency is being checked.

impl<Inner, M> Consistency for Mapped<Inner, M>

where Inner: Consistency, M: SpecMapper<In = Inner::Val>,

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

{
    &&& self.mapper.wf_out(v)
    &&& self.inner.consistent(self.mapper.spec_map_rev(v))

}

type Val = <M as SpecMapper>::Out

The type of values whose consistency is being checked.

impl<Inner, M, MRev, T> DerOrd<T> for Mapped<Inner, BiMap<M, MRev>>

where T: DeepView, M: SpecMap<Input = MRev::Output, Output = T::V>, MRev: SpecMap<Input = T::V> + for<'x> Map<&'x T>, for<'x> Inner: DerState + DerOrd<<MRev as Map<&'x T>>::O>,

proof fn lemma_der_serialize_len(&self, value: T::V)

open spec fn der_remaining(&self, value: T::V, state: Inner::State) -> Seq<u8>

{ self.inner.der_remaining(self.mapper.1.spec_map(value), state) }

open spec fn der_state_valid(&self, value: T::V, state: Inner::State) -> bool

{ self.inner.der_state_valid(self.mapper.1.spec_map(value), state) }

exec fn der_start(&self, v: &T) -> state : Inner::State

exec fn der_next(&self, v: &T, state: &mut Inner::State) -> next : Option<u8>

fn der_leq(&self, left: &T, right: &T) -> bool

impl<Inner: DerState, M, MRev> DerState for Mapped<Inner, BiMap<M, MRev>>

type State = <Inner as DerState>::State

impl<Inner, M, MRev> EquivSerializers for Mapped<Inner, BiMap<M, MRev>>

where Inner: EquivSerializers, M: SpecMap<Input = Inner::SVal>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn equiv_inv(&self) -> bool

{ self.inner.equiv_inv() }

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

impl<Inner, M> EquivSerializers for Mapped<Inner, M>

where Inner: EquivSerializers, M: SpecMapper<In = Inner::SVal>,

open spec fn equiv_inv(&self) -> bool

{ self.inner.equiv_inv() }

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

impl<Inner, M, MRev> EquivSerializersGeneral for Mapped<Inner, BiMap<M, MRev>>

where Inner: EquivSerializersGeneral, M: SpecMap<Input = Inner::SVal>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn equiv_general_inv(&self) -> bool

{ self.inner.equiv_general_inv() }

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

impl<Inner, M> EquivSerializersGeneral for Mapped<Inner, M>

where Inner: EquivSerializersGeneral, M: SpecMapper<In = Inner::SVal>,

open spec fn equiv_general_inv(&self) -> bool

{ self.inner.equiv_general_inv() }

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

impl<Inner, M, MRev> GoodSerializer for Mapped<Inner, BiMap<M, MRev>>

where Inner: GoodSerializer, M: SpecMap<Input = Inner::SVal>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn serialize_inv(&self) -> bool

{ self.inner.serialize_inv() }

proof fn lemma_serialize_len(&self, v: M::Output)

impl<Inner, M> GoodSerializer for Mapped<Inner, M>

where Inner: GoodSerializer, M: SpecMapper<In = Inner::SVal>,

open spec fn serialize_inv(&self) -> bool

{ self.inner.serialize_inv() }

proof fn lemma_serialize_len(&self, v: M::Out)

impl<Inner, Mapper, Reverse> HasAsn1Start for Mapped<Inner, BiMap<Mapper, Reverse>>

where Inner: HasAsn1Start, Mapper: SpecMap<Input = Inner::PVal>, Reverse: SpecMap<Input = Mapper::Output, Output = Mapper::Input>,

BiMap mapping does not change the accepted byte domain.

open spec fn asn1_start(&self) -> Asn1StartDomain

{ self.inner.asn1_start() }

proof fn lemma_parse_implies_asn1_start(&self, input: Seq<u8>)

impl<Inner, Mapper> HasAsn1Start for Mapped<Inner, Mapper>

where Inner: HasAsn1Start, Mapper: SpecMapper<In = Inner::PVal>,

Semantic mapping does not change the accepted byte domain.

open spec fn asn1_start(&self) -> Asn1StartDomain

{ self.inner.asn1_start() }

proof fn lemma_parse_implies_asn1_start(&self, input: Seq<u8>)

impl<Inner, M, MRev> MinMaxByteLen for Mapped<Inner, BiMap<M, MRev>>

where Inner: MinMaxByteLen, M: SpecMap<Input = Inner::T>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn min(&self) -> nat

{ self.inner.min() }

open spec fn max(&self) -> nat

{ self.inner.max() }

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

impl<Inner, M> MinMaxByteLen for Mapped<Inner, M>

where Inner: MinMaxByteLen, M: SpecMapper<In = Inner::T>,

open spec fn min(&self) -> nat

{ self.inner.min() }

open spec fn max(&self) -> nat

{ self.inner.max() }

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

impl<Inner, M, MRev> NoLookAhead for Mapped<Inner, BiMap<M, MRev>>

where Inner: NoLookAhead, M: SpecMap<Input = Inner::PVal>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn no_lookahead_inv(&self) -> bool

{ self.inner.no_lookahead_inv() }

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

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

impl<Inner, M> NoLookAhead for Mapped<Inner, M>

where Inner: NoLookAhead, M: SpecMapper<In = Inner::PVal>,

open spec fn no_lookahead_inv(&self) -> bool

{ self.inner.no_lookahead_inv() }

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

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

impl<Inner, Out> NonMalleable for Mapped<Inner, FnSpecMapper<Inner::PVal, Out>>

where Inner: SoundParser + NonMalleable,

open spec fn nonmal_inv(&self) -> bool

{
    &&& self.inner.nonmal_inv()
    &&& self.inner.sound_inv()
    &&& forall |v: Inner::PVal| {
        #[trigger] self.inner.consistent(v) ==> (self.mapper.1)((self.mapper.0)(v)) == v
    }

}

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

impl<Inner, M, MRev> NonMalleable for Mapped<Inner, BiMap<M, MRev>>

where Inner: SoundParser + NonMalleable, M: SpecMap<Input = Inner::PVal>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn nonmal_inv(&self) -> bool

{
    &&& self.inner.nonmal_inv()
    &&& self.inner.sound_inv()
    &&& forall |i: Inner::T| self.inner.consistent(i) ==> self.mapper.lossless(i)

}

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

impl<Inner, M> NonMalleable for Mapped<Inner, M>

where Inner: SoundParser + NonMalleable, M: LosslessMapper<In = Inner::PVal>,

open spec fn nonmal_inv(&self) -> bool

{
    &&& self.inner.nonmal_inv()
    &&& self.inner.sound_inv()
    &&& forall |v: Inner::T| self.inner.consistent(v) ==> self.mapper.wf_in(v)

}

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

impl<Inner, M, MRev> NonTailFmt for Mapped<Inner, BiMap<M, MRev>>

where Inner: NonTailFmt, M: SpecMap<Input = Inner::SValue>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn serialize_dps_inv(&self) -> bool

{ self.inner.serialize_dps_inv() }

proof fn lemma_serialize_dps_prepend(&self, v: M::Output, obuf: Seq<u8>)

proof fn lemma_serialize_dps_len(&self, v: M::Output, obuf: Seq<u8>)

impl<Inner, M> NonTailFmt for Mapped<Inner, M>

where Inner: NonTailFmt, M: SpecMapper<In = Inner::SValue>,

open spec fn serialize_dps_inv(&self) -> bool

{ self.inner.serialize_dps_inv() }

proof fn lemma_serialize_dps_prepend(&self, v: M::Out, obuf: Seq<u8>)

proof fn lemma_serialize_dps_len(&self, v: M::Out, obuf: Seq<u8>)

impl<I, Inner, M, MRev> Parser<I> for Mapped<Inner, BiMap<M, MRev>>

where I: View<V = Seq<u8>>, Inner: Parser<I>, M: Map<Inner::PT, Input = Inner::PVal>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn exec_inv(&self) -> bool

{ self.inner.exec_inv() }

exec fn parse(&self, ibuf: &I) -> PResult<Self::PT>

type PT = <M as Map<<Inner as Parser<I>>::PT>>::O

Executable value returned by this parser.

impl<Inner, M, MRev, T> Prepare<T> for Mapped<Inner, BiMap<M, MRev>>

where T: DeepView, M: SpecMap<Input = MRev::Output, Output = T::V>, MRev: SpecMap<Input = T::V> + for<'x> Map<&'x T>, Inner: for<'x> Prepare<<MRev as Map<&'x T>>::O>,

open spec fn exec_inv(&self) -> bool

{ self.inner.exec_inv() }

exec fn prepare(&self, v: &T) -> Result<usize, PreSerializeError>

impl<Inner, M, MRev> Productive for Mapped<Inner, BiMap<M, MRev>>

where Inner: Productive, M: SpecMap<Input = Inner::PVal>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn productive_inv(&self) -> bool

{ self.inner.productive_inv() }

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

impl<Inner: Productive, Out> Productive for Mapped<Inner, FnSpec<(Inner::PVal,), Out>>

open spec fn productive_inv(&self) -> bool

{ self.inner.productive_inv() }

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

impl<Inner, M> Productive for Mapped<Inner, M>

where Inner: Productive, M: SpecMapper<In = Inner::PVal>,

open spec fn productive_inv(&self) -> bool

{ self.inner.productive_inv() }

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

impl<F, M> Retaggable for Mapped<F, M>

where F: Retaggable, M: Copy,

Allows a semantic mapping to remain attached when its underlying ASN.1 format is retagged.

Retagging is delegated to the inner format and the mapper is preserved.

open spec fn spec_retagged(&self, tag: Tag) -> Self

{
    Mapped {
        inner: self.inner.spec_retagged(tag),
        mapper: self.mapper,
    }
}

exec fn retagged(&self, tag: Tag) -> Self

impl<Inner: SPRoundTripDps, Out> SPRoundTripDps for Mapped<Inner, FnSpecMapper<Inner::T, Out>>

open spec fn unambiguous(&self) -> bool

{
    &&& self.inner.unambiguous()
    &&& forall |o: Out| {
        #[trigger] self.consistent(o) ==> (self.mapper.0)((self.mapper.1)(o)) == o
    }

}

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

impl<Inner, M, MRev> SPRoundTripDps for Mapped<Inner, BiMap<M, MRev>>

where Inner: SPRoundTripDps, M: SpecMap<Input = Inner::T>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn unambiguous(&self) -> bool

{
    &&& self.inner.unambiguous()
    &&& forall |o: M::Output| self.consistent(o) ==> self.mapper.sound(o)

}

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

impl<Inner, M> SPRoundTripDps for Mapped<Inner, M>

where Inner: SPRoundTripDps, M: LossyMapper<In = Inner::T>,

open spec fn unambiguous(&self) -> bool

{ self.inner.unambiguous() }

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

impl<Inner, M, MRev> SafeParser for Mapped<Inner, BiMap<M, MRev>>

where Inner: SafeParser, M: SpecMap<Input = Inner::PVal>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn safe_inv(&self) -> bool

{ self.inner.safe_inv() }

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

impl<Inner: SafeParser, Out> SafeParser for Mapped<Inner, FnSpec<(Inner::PVal,), Out>>

open spec fn safe_inv(&self) -> bool

{ self.inner.safe_inv() }

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

impl<Inner, M> SafeParser for Mapped<Inner, M>

where Inner: SafeParser, M: SpecMapper<In = Inner::PVal>,

open spec fn safe_inv(&self) -> bool

{ self.inner.safe_inv() }

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

impl<Output: OutputBuf, Inner, M, MRev, T> Serializer<Output, T> for Mapped<Inner, BiMap<M, MRev>>

where T: DeepView, M: SpecMap<Input = MRev::Output, Output = T::V>, MRev: SpecMap<Input = T::V> + for<'x> Map<&'x T>, Inner: for<'x> Serializer<Output, <MRev as Map<&'x T>>::O>,

open spec fn exec_inv(&self) -> bool

{ self.inner.exec_inv() }

exec fn serialize_into(&self, v: &T, obuf: &mut Output)

impl<Inner: SoundParser, Out> SoundParser for Mapped<Inner, FnSpecMapper<Inner::PVal, Out>>

open spec fn sound_inv(&self) -> bool

{
    &&& self.inner.sound_inv()
    &&& forall |v: Inner::T| {
        #[trigger] self.inner.consistent(v) ==> (self.mapper.1)((self.mapper.0)(v)) == v
    }

}

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

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

impl<Inner, M, MRev> SoundParser for Mapped<Inner, BiMap<M, MRev>>

where Inner: SoundParser, M: SpecMap<Input = Inner::PVal>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn sound_inv(&self) -> bool

{
    &&& self.inner.sound_inv()
    &&& forall |i: Inner::T| {
        #[trigger] self.inner.consistent(i) ==> self.mapper.lossless(i)
    }

}

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

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

impl<Inner, M> SoundParser for Mapped<Inner, M>

where Inner: SoundParser, M: LosslessMapper<In = Inner::PVal>,

open spec fn sound_inv(&self) -> bool

{
    &&& self.inner.sound_inv()
    &&& forall |v: Inner::T| self.inner.consistent(v) ==> self.mapper.wf_in(v)

}

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

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

impl<Inner, M, MRev> SpecByteLen for Mapped<Inner, BiMap<M, MRev>>

where Inner: SpecByteLen, M: SpecMap<Input = Inner::T>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

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

{ self.inner.byte_len(self.mapper.1.spec_map(v)) }

type T = <M as SpecMap>::Output

The type of values whose byte length is being computed.

impl<Inner, M> SpecByteLen for Mapped<Inner, M>

where Inner: SpecByteLen, M: SpecMapper<In = Inner::T>,

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

{ self.inner.byte_len(self.mapper.spec_map_rev(v)) }

type T = <M as SpecMapper>::Out

The type of values whose byte length is being computed.

impl<Inner, M, MRev> SpecParser for Mapped<Inner, BiMap<M, MRev>>

where Inner: SpecParser, M: SpecMap<Input = Inner::PVal>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

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

{
    match self.inner.spec_parse(ibuf) {
        Some((n, v)) => Some((n, self.mapper.0.spec_map(v))),
        None => None,
    }
}

type PVal = <M as SpecMap>::Output

The type of parsed values.

impl<Inner: SpecParser, Out> SpecParser for Mapped<Inner, FnSpec<(Inner::PVal,), Out>>

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

{
    match self.inner.spec_parse(ibuf) {
        Some((n, v)) => Some((n, (self.mapper)(v))),
        None => None,
    }
}

type PVal = Out

The type of parsed values.

impl<Inner, M> SpecParser for Mapped<Inner, M>

where Inner: SpecParser, M: SpecMapper<In = Inner::PVal>,

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

{
    match self.inner.spec_parse(ibuf) {
        Some((n, v)) => Some((n, self.mapper.spec_map(v))),
        None => None,
    }
}

type PVal = <M as SpecMapper>::Out

The type of parsed values.

impl<Inner, M, MRev> SpecSerializer for Mapped<Inner, BiMap<M, MRev>>

where Inner: SpecSerializer, M: SpecMap<Input = Inner::SVal>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn spec_serialize(&self, v: M::Output) -> Seq<u8>

{ self.inner.spec_serialize(self.mapper.1.spec_map(v)) }

type SVal = <M as SpecMap>::Output

The type of values to be serialized.

impl<Inner: SpecSerializer, Out> SpecSerializer for Mapped<Inner, FnSpec<(Out,), Inner::SVal>>

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

{ self.inner.spec_serialize((self.mapper)(v)) }

type SVal = Out

The type of values to be serialized.

impl<Inner, M> SpecSerializer for Mapped<Inner, M>

where Inner: SpecSerializer, M: SpecMapper<In = Inner::SVal>,

open spec fn spec_serialize(&self, v: M::Out) -> Seq<u8>

{ self.inner.spec_serialize(self.mapper.spec_map_rev(v)) }

type SVal = <M as SpecMapper>::Out

The type of values to be serialized.

impl<Inner, M, MRev> SpecSerializerDps for Mapped<Inner, BiMap<M, MRev>>

where Inner: SpecSerializerDps, M: SpecMap<Input = Inner::SValue>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn spec_serialize_dps(&self, v: M::Output, obuf: Seq<u8>) -> Seq<u8>

{ self.inner.spec_serialize_dps(self.mapper.1.spec_map(v), obuf) }

type SValue = <M as SpecMap>::Output

The type of values to be serialized.

impl<Inner: SpecSerializerDps, Out> SpecSerializerDps for Mapped<Inner, FnSpec<(Out,), Inner::SValue>>

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

{ self.inner.spec_serialize_dps((self.mapper)(v), obuf) }

type SValue = Out

The type of values to be serialized.

impl<Inner, M> SpecSerializerDps for Mapped<Inner, M>

where Inner: SpecSerializerDps, M: SpecMapper<In = Inner::SValue>,

open spec fn spec_serialize_dps(&self, v: M::Out, obuf: Seq<u8>) -> Seq<u8>

{ self.inner.spec_serialize_dps(self.mapper.spec_map_rev(v), obuf) }

type SValue = <M as SpecMapper>::Out

The type of values to be serialized.

impl<Inner, M, MRev> StaticByteLen for Mapped<Inner, BiMap<M, MRev>>

where Inner: StaticByteLen, M: SpecMap<Input = Inner::T>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

open spec fn static_byte_len() -> nat

{ Inner::static_byte_len() }

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

impl<Inner, M> StaticByteLen for Mapped<Inner, M>

where Inner: StaticByteLen, M: SpecMapper<In = Inner::T>,

open spec fn static_byte_len() -> nat

{ Inner::static_byte_len() }

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

impl<Inner: Copy, M: Copy> Copy for Mapped<Inner, M>