Struct FixWith 

pub struct FixWith<const LIMIT: usize, Body, Param>(pub Body, pub Param);

Bounded fixpoint combinator for parameterized recursive formats.

Param is the starting parameter for the recursive Body. Context-free recursive formats use Param = ().

Tuple Fields

0: Body

1: Param

Implementations

impl<const LIMIT: usize, Body, Param> FixWith<LIMIT, Body, Param>

where Body: SpecRecBody, Param: DeepView<V = Body::Param>,

pub open spec fn byte_len_gas( body: &Body, gas: nat, param: Body::Param, v: Body::T, ) -> nat

{ body.spec_body(param, Self::specs_callback(&body, gas)).byte_len(v) }

pub open spec fn consistent_gas( body: &Body, gas: nat, param: Body::Param, v: Body::T, ) -> bool

{ body.spec_body(param, Self::specs_callback(&body, gas)).consistent(v) }

pub open spec fn spec_parse_gas( body: &Body, gas: nat, param: Body::Param, input: Seq<u8>, ) -> Option<(int, Body::T)>

{ body.spec_body(param, Self::specs_callback(&body, gas)).spec_parse(input) }

pub open spec fn spec_serialize_gas( body: &Body, gas: nat, param: Body::Param, v: Body::T, ) -> Seq<u8>

{ body.spec_body(param, Self::specs_callback(&body, gas)).spec_serialize(v) }

pub open spec fn spec_serialize_dps_gas( body: &Body, gas: nat, param: Body::Param, v: Body::T, obuf: Seq<u8>, ) -> Seq<u8>

{ body.spec_body(param, Self::specs_callback(&body, gas)).spec_serialize_dps(v, obuf) }

pub open spec fn spec_parse_callback( body: &Body, gas: nat, param: Body::Param, ) -> ParserFnSpec<Body::T>

{
    |ibuf: Seq<u8>| {
        if gas > 0 {
            Self::spec_parse_gas(body, (gas - 1) as nat, param, ibuf)
        } else {
            None
        }
    }
}

pub open spec fn consistent_callback( body: &Body, gas: nat, param: Body::Param, ) -> PredFnSpec<Body::T>

{
    |vv: Body::T| {
        if gas > 0 {
            Self::consistent_gas(body, (gas - 1) as nat, param, vv)
        } else {
            false
        }
    }
}

pub open spec fn byte_len_callback( body: &Body, gas: nat, param: Body::Param, ) -> ByteLenFnSpec<Body::T>

{
    |vv: Body::T| {
        if gas > 0 { Self::byte_len_gas(body, (gas - 1) as nat, param, vv) } else { 0 }
    }
}

pub open spec fn spec_serialize_callback( body: &Body, gas: nat, param: Body::Param, ) -> SerializerFnSpec<Body::T>

{
    |vv: Body::T| {
        if gas > 0 {
            Self::spec_serialize_gas(body, (gas - 1) as nat, param, vv)
        } else {
            Seq::empty()
        }
    }
}

pub open spec fn spec_serialize_dps_callback( body: &Body, gas: nat, param: Body::Param, ) -> SerializerDPSFnSpec<Body::T>

{
    |vv: Body::T, obuf: Seq<u8>| {
        if gas > 0 {
            Self::spec_serialize_dps_gas(body, (gas - 1) as nat, param, vv, obuf)
        } else {
            obuf
        }
    }
}

pub open spec fn specs_callback( body: &Body, gas: nat, ) -> ParamRecSpecs<Body::Param, Body::T>

{
    |param: Body::Param| (
        Self::consistent_callback(&body, gas, param),
        Self::byte_len_callback(&body, gas, param),
        Self::spec_parse_callback(&body, gas, param),
        Self::spec_serialize_callback(&body, gas, param),
        Self::spec_serialize_dps_callback(&body, gas, param),
    )
}

Bundled callbacks used when unfolding one recursive level.

impl<const LIMIT: usize, Body, Param> FixWith<LIMIT, Body, Param>

where Body: SafeParserRecBody, Body::Body: SafeParser, Param: DeepView<V = Body::Param>,

pub proof fn lemma_specs_callback_safe_inv(&self, gas: nat, param: Body::Param)

ensures

Self::specs_callback(&self.0, gas)(param).safe_inv(),

impl<const LIMIT: usize, Body, Param> FixWith<LIMIT, Body, Param>

where Body: SoundParserRecBody, Body::Body: SoundParser, Param: DeepView<V = Body::Param>,

pub proof fn sound_parser_by_induction( &self, gas: nat, param: Body::Param, input: Seq<u8>, n: int, v: Body::T, )

ensures

Self::spec_parse_gas(&self.0, gas, param, input) == Some((n, v))
    ==> {
        &&& Self::consistent_gas(&self.0, gas, param, v)
        &&& Self::byte_len_gas(&self.0, gas, param, v) == n

    },

Inductive proof that spec_parse_gas satisfies sound_parser.

impl<const LIMIT: usize, Body, Param> FixWith<LIMIT, Body, Param>

where Body: ProductiveRecBody, Body::Body: Productive, Param: DeepView<V = Body::Param>,

pub proof fn lemma_specs_callback_productive_inv(&self, gas: nat, param: Body::Param)

ensures

Self::specs_callback(&self.0, gas)(param).productive_inv(),

Establishes productivity for one bundled recursive callback.

Trait Implementations

impl<const LIMIT: usize, Body: Clone, Param: Clone> Clone for FixWith<LIMIT, Body, Param>

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

ensures

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

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

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

Performs copy-assignment from source.

impl<const LIMIT: usize, Body, Param> Consistency for FixWith<LIMIT, Body, Param>

where Body: SpecRecBody, Param: DeepView<V = Body::Param>,

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

{ Self::consistent_gas(&self.0, LIMIT as nat, self.1.deep_view(), v) }

type Val = <Body as SpecRecBody>::T

The type of values whose consistency is being checked.

impl<const LIMIT: usize, Body, Param> EquivSerializers for FixWith<LIMIT, Body, Param>

where Body: EquivSerializersGeneralRecBody, Body::Body: EquivSerializersGeneral, Param: DeepView<V = Body::Param>,

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

fn equiv_inv(&self) -> bool

impl<const LIMIT: usize, Body, Param> EquivSerializersGeneral for FixWith<LIMIT, Body, Param>

where Body: EquivSerializersGeneralRecBody, Body::Body: EquivSerializersGeneral, Param: DeepView<V = Body::Param>,

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

fn equiv_general_inv(&self) -> bool

impl<const LIMIT: usize, Body, Param> GoodSerializer for FixWith<LIMIT, Body, Param>

where Body: GoodSerializerRecBody, Body::Body: GoodSerializer, Param: DeepView<V = Body::Param>,

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

fn serialize_inv(&self) -> bool

impl<const N: usize, Body, Param> LeafNonMalleable for FixWith<N, Body, Param>

where Param: DeepView<V = Body::Param>, Body: StrictRecBody, Body::Body: StrictCombinator,

proof fn nonmal_leaf_inv(&self)

impl<const LIMIT: usize, Body, Param> NoLookAhead for FixWith<LIMIT, Body, Param>

where Body: NoLookAheadRecBody, Body::Body: NoLookAhead, Param: DeepView<V = Body::Param>,

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

fn no_lookahead_inv(&self) -> bool

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

impl<const LIMIT: usize, Body, Param> NonMalleable for FixWith<LIMIT, Body, Param>

where Body: NonMalleableRecBody, Body::Body: NonMalleable + SafeParser + SoundParser, Param: DeepView<V = Body::Param>,

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

fn nonmal_inv(&self) -> bool

impl<const LIMIT: usize, Body, Param> NonTailFmt for FixWith<LIMIT, Body, Param>

where Body: NonTailFmtRecBody, Body::Body: NonTailFmt, Param: DeepView<V = Body::Param>,

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>)

fn serialize_dps_inv(&self) -> bool

impl<const LIMIT: usize, Body, Param, I> Parser<I> for FixWith<LIMIT, Body, Param>

where I: InputBuf, Param: DeepView<V = Body::Param>, Body: ParserRecBody<I, EP = Param> + ProductiveRecBody, Body::Body: Productive,

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

type PT = <Body as ParserRecBody<I>>::O

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl<T, const LIMIT: usize, Body, Param> Prepare<T> for FixWith<LIMIT, Body, Param>

where T: DeepView<V = Body::T>, Param: DeepView<V = Body::Param>, Body: PrepareRecBody<T, EP = Param>,

open spec fn exec_inv(&self) -> bool

{ true }

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

impl<const LIMIT: usize, Body, Param> Productive for FixWith<LIMIT, Body, Param>

where Body: ProductiveRecBody, Body::Body: Productive, Param: DeepView<V = Body::Param>,

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

fn productive_inv(&self) -> bool

impl<const LIMIT: usize, Body, Param> SPRoundTripDps for FixWith<LIMIT, Body, Param>

where Body: SPRoundTripDpsRecBody + NonTailFmtRecBody, Body::Body: SPRoundTripDps + NonTailFmt, Param: DeepView<V = Body::Param>,

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

fn unambiguous(&self) -> bool

impl<const LIMIT: usize, Body, Param> SafeParser for FixWith<LIMIT, Body, Param>

where Body: SafeParserRecBody, Body::Body: SafeParser, Param: DeepView<V = Body::Param>,

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

fn safe_inv(&self) -> bool

impl<Output: OutputBuf, T, const LIMIT: usize, Body, Param> Serializer<Output, T> for FixWith<LIMIT, Body, Param>

where T: DeepView<V = Body::T>, Param: DeepView<V = Body::Param>, Body: SerializerRecBody<Output, T, EP = Param>,

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

fn exec_inv(&self) -> bool

impl<const LIMIT: usize, Body, Param> SoundParser for FixWith<LIMIT, Body, Param>

where Body: SoundParserRecBody, Body::Body: SoundParser, Param: DeepView<V = Body::Param>,

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

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

fn sound_inv(&self) -> bool

impl<const LIMIT: usize, Body, Param> SpecByteLen for FixWith<LIMIT, Body, Param>

where Body: SpecRecBody, Param: DeepView<V = Body::Param>,

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

{ Self::byte_len_gas(&self.0, LIMIT as nat, self.1.deep_view(), v) }

type T = <Body as SpecRecBody>::T

The type of values whose byte length is being computed.

impl<const LIMIT: usize, Body, Param> SpecParser for FixWith<LIMIT, Body, Param>

where Body: SpecRecBody, Param: DeepView<V = Body::Param>,

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

{ Self::spec_parse_gas(&self.0, LIMIT as nat, self.1.deep_view(), input) }

type PVal = <Body as SpecRecBody>::T

The type of parsed values.

impl<const LIMIT: usize, Body, Param> SpecSerializer for FixWith<LIMIT, Body, Param>

where Body: SpecRecBody, Param: DeepView<V = Body::Param>,

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

{ Self::spec_serialize_gas(&self.0, LIMIT as nat, self.1.deep_view(), v) }

type SVal = <Body as SpecRecBody>::T

The type of values to be serialized.

impl<const LIMIT: usize, Body, Param> SpecSerializerDps for FixWith<LIMIT, Body, Param>

where Body: SpecRecBody, Param: DeepView<V = Body::Param>,

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

{ Self::spec_serialize_dps_gas(&self.0, LIMIT as nat, self.1.deep_view(), v, obuf) }

type SValue = <Body as SpecRecBody>::T

The type of values to be serialized.

impl<const LIMIT: usize, Body: Copy, Param: Copy> Copy for FixWith<LIMIT, Body, Param>