Struct FnSerializer 

pub struct FnSerializer<Output: OutputBuf, T: DeepView + ?Sized, Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>, Exec: Fn(&T, &mut Output)> {
    pub exec_fn: Exec,
    pub spec_fn: Ghost<Spec>,
    pub _output: PhantomData<Output>,
    pub _marker: PhantomData<T>,
}

Pairs an executable serializer closure with a ghost specification serializer.

Fields

exec_fn: Exec

spec_fn: Ghost<Spec>

_output: PhantomData<Output>

_marker: PhantomData<T>

Implementations

impl<Output, T, Spec, Exec> FnSerializer<Output, T, Spec, Exec>

where Output: OutputBuf, T: DeepView + ?Sized, Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>, Exec: Fn(&T, &mut Output),

pub exec fn new(exec_fn: Exec, Ghost(spec_fn): Ghost<Spec>) -> serializer : Self

requires

forall |v: &T, obuf: &mut Output| {
    (spec_fn.consistent(v.deep_view()) && obuf.fits(spec_fn.byte_len(v.deep_view())))
        ==> #[trigger] call_requires(exec_fn, (v, obuf))
},

forall |v: &T, obuf: &mut Output| {
    (spec_fn.consistent(v.deep_view()) && #[trigger]
        call_ensures(exec_fn, (v, obuf), ()))
        ==> {
            &&& final(obuf)@ == obuf@ + spec_fn.spec_serialize(v.deep_view())
            &&& forall |n| {
                #[trigger] obuf.fits(spec_fn.byte_len(v.deep_view()) + n)
                    <==> final(obuf).fits(n)
            }
            &&& obuf.same_destination(final(obuf))

        }
},

ensures

serializer.exec_inv(),

serializer.spec_fn == spec_fn,

Trait Implementations

impl<Output, T, Spec, Exec> Consistency for FnSerializer<Output, T, Spec, Exec>

where Output: OutputBuf, T: DeepView + ?Sized, Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>, Exec: Fn(&T, &mut Output),

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

{
    let Ghost(spec_fn) = self.spec_fn;
    spec_fn.consistent(v)
}

type Val = <T as DeepView>::V

The type of values whose consistency is being checked.

impl<Output, T, Spec, Exec> GoodSerializer for FnSerializer<Output, T, Spec, Exec>

where Output: OutputBuf, T: DeepView + ?Sized, Spec: GoodSerializer<T = T::V> + Consistency<Val = T::V>, Exec: Fn(&T, &mut Output),

open spec fn serialize_inv(&self) -> bool

{
    let Ghost(spec_fn) = self.spec_fn;
    spec_fn.serialize_inv()
}

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

impl<Output, T, Spec, Exec> Serializer<Output, T> for FnSerializer<Output, T, Spec, Exec>

where Output: OutputBuf, T: DeepView + ?Sized, Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>, Exec: Fn(&T, &mut Output),

open spec fn exec_inv(&self) -> bool

{
    let Ghost(spec_fn) = self.spec_fn;
    &&& forall |v: &T, obuf: &mut Output| {
        (spec_fn.consistent(v.deep_view()) && obuf.fits(spec_fn.byte_len(v.deep_view())))
            ==> #[trigger] call_requires(self.exec_fn, (v, obuf))
    }
    &&& forall |v: &T, obuf: &mut Output| {
        (spec_fn.consistent(v.deep_view()) && #[trigger]
            call_ensures(self.exec_fn, (v, obuf), ()))
            ==> {
                &&& final(obuf)@ == obuf@ + spec_fn.spec_serialize(v.deep_view())
                &&& forall |n| {
                    #[trigger] obuf.fits(spec_fn.byte_len(v.deep_view()) + n)
                        <==> final(obuf).fits(n)
                }
                &&& obuf.same_destination(final(obuf))

            }
    }

}

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

impl<Output, T, Spec, Exec> SpecByteLen for FnSerializer<Output, T, Spec, Exec>

where Output: OutputBuf, T: DeepView + ?Sized, Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>, Exec: Fn(&T, &mut Output),

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

{
    let Ghost(spec_fn) = self.spec_fn;
    spec_fn.byte_len(v)
}

type T = <T as DeepView>::V

The type of values whose byte length is being computed.

impl<Output, T, Spec, Exec> SpecSerializer for FnSerializer<Output, T, Spec, Exec>

where Output: OutputBuf, T: DeepView + ?Sized, Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>, Exec: Fn(&T, &mut Output),

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

{
    let Ghost(spec_fn) = self.spec_fn;
    spec_fn.spec_serialize(v)
}

type SVal = <T as DeepView>::V

The type of values to be serialized.