Struct Refined 

pub struct Refined<Inner, Predicate>(pub Inner, pub Predicate);

Value refinement combinator: filters values through a predicate.

Consistency

inner.consistent(v) && predicate.apply(v).

Tuple Fields

0: Inner

1: Predicate

Trait Implementations

impl<A, PredFn, T> ByteLen<T> for Refined<A, PredFn>

where T: DeepView, A: ByteLen<T>, PredFn: Pred<T>,

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

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

impl<Inner: Clone, Predicate: Clone> Clone for Refined<Inner, Predicate>

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

ensures

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

call_ensures(Predicate::clone, (&self.1,), cloned.1),

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

Performs copy-assignment from source.

impl<A, Pred> Consistency for Refined<A, Pred>

where A: Consistency, Pred: SpecPred<A::Val>,

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

{ self.0.consistent(v) && self.1.apply(v) }

type Val = <A as Consistency>::Val

The type of values whose consistency is being checked.

impl<Inner, P, T> DerOrd<T> for Refined<Inner, P>

where T: DeepView, Inner: DerOrd<T>, P: Pred<T>,

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.0.der_remaining(value, state) }

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

{ self.0.der_state_valid(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, P> DerState for Refined<Inner, P>

type State = <Inner as DerState>::State

impl<A, Pred> EquivSerializers for Refined<A, Pred>

where A: EquivSerializers, Pred: SpecPred<A::SVal>,

open spec fn equiv_inv(&self) -> bool

{ self.0.equiv_inv() }

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

impl<A, Pred> EquivSerializersGeneral for Refined<A, Pred>

where A: EquivSerializersGeneral, Pred: SpecPred<A::SVal>,

open spec fn equiv_general_inv(&self) -> bool

{ self.0.equiv_general_inv() }

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

impl<A, Pred> GoodSerializer for Refined<A, Pred>

where A: GoodSerializer, Pred: SpecPred<A::SVal>,

open spec fn serialize_inv(&self) -> bool

{ self.0.serialize_inv() }

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

impl<Inner: HasAsn1Start, Predicate: SpecPred<Inner::PVal>> HasAsn1Start for Refined<Inner, Predicate>

Refinement can only narrow an accepted input domain.

open spec fn asn1_start(&self) -> Asn1StartDomain

{ self.0.asn1_start() }

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

impl<A, Pred> MinMaxByteLen for Refined<A, Pred>

where A: MinMaxByteLen, Pred: SpecPred<A::T>,

open spec fn min(&self) -> nat

{ self.0.min() }

open spec fn max(&self) -> nat

{ self.0.max() }

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

impl<A: NoLookAhead, Pred: SpecPred<A::PVal>> NoLookAhead for Refined<A, Pred>

open spec fn no_lookahead_inv(&self) -> bool

{ self.0.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<A: NonMalleable, Pred: SpecPred<A::PVal>> NonMalleable for Refined<A, Pred>

open spec fn nonmal_inv(&self) -> bool

{ self.0.nonmal_inv() }

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

impl<A, Pred> NonTailFmt for Refined<A, Pred>

where A: NonTailFmt, Pred: SpecPred<A::SValue>,

open spec fn serialize_dps_inv(&self) -> bool

{ self.0.serialize_dps_inv() }

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

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

impl<I, A, PredFn> Parser<I> for Refined<A, PredFn>

where I: View<V = Seq<u8>>, A: Parser<I>, PredFn: Pred<A::PT>,

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

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

type PT = <A as Parser<I>>::PT

Executable value returned by this parser.

impl<A, PredFn, T> Prepare<T> for Refined<A, PredFn>

where T: DeepView, A: Prepare<T>, PredFn: Pred<T>,

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

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

impl<A: Productive, Pred: SpecPred<A::PVal>> Productive for Refined<A, Pred>

open spec fn productive_inv(&self) -> bool

{ self.0.productive_inv() }

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

impl<F, P> Retaggable for Refined<F, P>

where F: Retaggable, P: Copy,

Allows a value constraint to remain attached when its underlying ASN.1 format is retagged.

Retagging is delegated to the inner format and the refinement predicate is preserved.

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

{ Refined(self.0.spec_retagged(tag), self.1) }

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

impl<A, Pred> SPRoundTripDps for Refined<A, Pred>

where A: SPRoundTripDps, Pred: SpecPred<A::PVal>,

open spec fn unambiguous(&self) -> bool

{ self.0.unambiguous() }

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

impl<A, Pred> SafeParser for Refined<A, Pred>

where A: SafeParser, Pred: SpecPred<A::PVal>,

open spec fn safe_inv(&self) -> bool

{ self.0.safe_inv() }

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

impl<Output: OutputBuf, A, PredFn, T> Serializer<Output, T> for Refined<A, PredFn>

where T: DeepView, A: Serializer<Output, T>, PredFn: SpecPred<T::V>,

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

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

impl<A, Pred> SoundParser for Refined<A, Pred>

where A: SoundParser, Pred: SpecPred<A::PVal>,

open spec fn sound_inv(&self) -> bool

{ self.0.sound_inv() }

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

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

impl<A, Pred> SpecByteLen for Refined<A, Pred>

where A: SpecByteLen, Pred: SpecPred<A::T>,

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

{ self.0.byte_len(v) }

type T = <A as SpecByteLen>::T

The type of values whose byte length is being computed.

impl<A, Pred> SpecParser for Refined<A, Pred>

where A: SpecParser, Pred: SpecPred<A::PVal>,

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

{
    match self.0.spec_parse(ibuf) {
        Some((n, v)) if self.1.apply(v) => Some((n, v)),
        _ => None,
    }
}

type PVal = <A as SpecParser>::PVal

The type of parsed values.

impl<A, Pred> SpecSerializer for Refined<A, Pred>

where A: SpecSerializer, Pred: SpecPred<A::SVal>,

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

{ self.0.spec_serialize(v) }

type SVal = <A as SpecSerializer>::SVal

The type of values to be serialized.

impl<A, Pred> SpecSerializerDps for Refined<A, Pred>

where A: SpecSerializerDps, Pred: SpecPred<A::SValue>,

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

{ self.0.spec_serialize_dps(v, obuf) }

type SValue = <A as SpecSerializerDps>::SValue

The type of values to be serialized.

impl<A, Pred> StaticByteLen for Refined<A, Pred>

where A: StaticByteLen, Pred: SpecPred<A::T>,

open spec fn static_byte_len() -> nat

{ A::static_byte_len() }

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

impl<A, Pred> ValueByteLen for Refined<A, Pred>

where A: ValueByteLen, Pred: SpecPred<A::T>,

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

{ A::value_byte_len(v) }

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

impl<Inner: Copy, Predicate: Copy> Copy for Refined<Inner, Predicate>