Struct FnPrepare 

pub struct FnPrepare<T: DeepView + ?Sized, Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>, Exec: Fn(&T) -> Result<usize, PreSerializeError>> {
    pub exec_fn: Exec,
    pub spec_fn: Ghost<Spec>,
    pub _marker: PhantomData<T>,
}

Pairs an executable preparation closure with its consistency and byte-length specification.

Fields

exec_fn: Exec

spec_fn: Ghost<Spec>

_marker: PhantomData<T>

Implementations

impl<T, Spec, Exec> FnPrepare<T, Spec, Exec>

where T: DeepView + ?Sized, Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>, Exec: Fn(&T) -> Result<usize, PreSerializeError>,

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

requires

forall |value: &T| #[trigger] call_requires(exec_fn, (value,)),

forall |value: &T, result: Result<usize, PreSerializeError>| {
    #[trigger] call_ensures(exec_fn, (value,), result)
        ==> (result matches Ok(
            len,
        ) ==> {
            &&& spec_fn.consistent(value.deep_view())
            &&& len == spec_fn.byte_len(value.deep_view())

        })
},

ensures

prepare.exec_inv(),

prepare.spec_fn == spec_fn,

Trait Implementations

impl<T, Spec, Exec> Consistency for FnPrepare<T, Spec, Exec>

where T: DeepView + ?Sized, Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>, Exec: Fn(&T) -> Result<usize, PreSerializeError>,

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

{ self.spec_fn@.consistent(value) }

type Val = <T as DeepView>::V

The type of values whose consistency is being checked.

impl<T, Spec, Exec> Prepare<T> for FnPrepare<T, Spec, Exec>

where T: DeepView + ?Sized, Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>, Exec: Fn(&T) -> Result<usize, PreSerializeError>,

open spec fn exec_inv(&self) -> bool

{
    &&& forall |value: &T| #[trigger] call_requires(self.exec_fn, (value,))
    &&& forall |value: &T, result: Result<usize, PreSerializeError>| {
        #[trigger] call_ensures(self.exec_fn, (value,), result)
            ==> (result matches Ok(
                len,
            ) ==> {
                &&& self.spec_fn@.consistent(value.deep_view())
                &&& len == self.spec_fn@.byte_len(value.deep_view())

            })
    }

}

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

impl<T, Spec, Exec> SpecByteLen for FnPrepare<T, Spec, Exec>

where T: DeepView + ?Sized, Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>, Exec: Fn(&T) -> Result<usize, PreSerializeError>,

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

{ self.spec_fn@.byte_len(value) }

type T = <T as DeepView>::V

The type of values whose byte length is being computed.