Struct FnByteLen 

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

Pairs an executable byte-length closure with its specification.

Fields

exec_fn: Exec

spec_fn: Ghost<Spec>

_marker: PhantomData<T>

Implementations

impl<T, Spec, Exec> FnByteLen<T, Spec, Exec>

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

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

requires

forall |value: &T| {
    spec_fn.byte_len(value.deep_view()) <= usize::MAX ==> #[trigger]
        call_requires(exec_fn, (value,))
},

forall |value: &T, len: usize| {
    #[trigger] call_ensures(exec_fn, (value,), len)
        ==> len == spec_fn.byte_len(value.deep_view())
},

ensures

length.exec_inv(),

length.spec_fn == spec_fn,

Trait Implementations

impl<T, Spec, Exec> ByteLen<T> for FnByteLen<T, Spec, Exec>

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

open spec fn exec_inv(&self) -> bool

{
    &&& forall |value: &T| (
        self.spec_fn@.byte_len(value.deep_view()) <= usize::MAX ==> #[trigger]
            call_requires(self.exec_fn, (value,))
    )
    &&& forall |value: &T, len: usize| {
        #[trigger] call_ensures(self.exec_fn, (value,), len)
            ==> len == self.spec_fn@.byte_len(value.deep_view())
    }

}

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

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

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

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> SpecByteLen for FnByteLen<T, Spec, Exec>

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

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.