vest_lib/core/exec/
fns.rs

1//! Executable fn traits.
2use crate::combinators::mapped::spec::{SpecMap, SpecMapper};
3use crate::core::exec::output::*;
4use crate::core::exec::parser::*;
5use crate::core::exec::{
6    output::OutputBuf,
7    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
8};
9use crate::core::proof::Productive;
10use crate::core::spec::*;
11use core::marker::PhantomData;
12use vstd::prelude::*;
13
14verus! {
15
16/// Executable counterpart of [`crate::core::spec::SpecPred`].
17///
18/// The executable method takes `&T` so callers can validate parsed values without moving them.
19pub trait Pred<T: DeepView>: SpecPred<T::V> {
20    fn test(&self, value: &T) -> (ok: bool)
21        ensures
22            ok == self.apply(value.deep_view()),
23    ;
24}
25
26impl<T, P> Pred<T> for &P where T: DeepView, P: Pred<T> {
27    fn test(&self, value: &T) -> (ok: bool) {
28        (*self).test(value)
29    }
30}
31
32/// Pairs an executable predicate closure with a ghost spec predicate.
33pub struct FnPred<T: DeepView, Exec: Fn(&T) -> bool, Spec: SpecPred<T::V>> {
34    exec_fn: Exec,
35    spec_fn: Ghost<Spec>,
36    marker: PhantomData<T>,
37}
38
39impl<T, Exec, Spec> FnPred<T, Exec, Spec> where
40    T: DeepView,
41    Exec: Fn(&T) -> bool,
42    Spec: SpecPred<T::V>,
43 {
44    #[verifier::type_invariant]
45    spec fn wf(&self) -> bool {
46        &&& forall|v: &T| #[trigger] call_requires(self.exec_fn, (v,))
47        &&& forall|v: &T, ok: bool| #[trigger]
48            call_ensures(self.exec_fn, (v,), ok) ==> ok == {
49                let Ghost(spec_pred) = self.spec_fn;
50                spec_pred.apply(v.deep_view())
51            }
52    }
53
54    pub fn new(exec_fn: Exec, Ghost(spec): Ghost<Spec>) -> (pred: Self)
55        requires
56            forall|v: &T| #[trigger] call_requires(exec_fn, (v,)),
57            forall|v: &T, ok: bool| #[trigger]
58                call_ensures(exec_fn, (v,), ok) ==> ok == spec.apply(v.deep_view()),
59    {
60        Self { exec_fn, spec_fn: Ghost(spec), marker: PhantomData }
61    }
62}
63
64impl<T, Exec, Spec> SpecPred<T::V> for FnPred<T, Exec, Spec> where
65    T: DeepView,
66    Exec: Fn(&T) -> bool,
67    Spec: SpecPred<T::V>,
68 {
69    closed spec fn apply(&self, value: T::V) -> bool {
70        let Ghost(spec_pred) = self.spec_fn;
71        spec_pred.apply(value)
72    }
73}
74
75impl<T, Exec, Spec> Pred<T> for FnPred<T, Exec, Spec> where
76    T: DeepView,
77    Exec: Fn(&T) -> bool,
78    Spec: SpecPred<T::V>,
79 {
80    fn test(&self, value: &T) -> (ok: bool) {
81        proof {
82            use_type_invariant(self);
83        }
84        (self.exec_fn)(value)
85    }
86}
87
88pub trait Map<I>: SpecMap where I: DeepView<V = Self::Input> {
89    type O: DeepView<V = Self::Output>;
90
91    fn map(&self, i: I) -> (o: Self::O)
92        ensures
93            self.spec_map(i.deep_view()) == o.deep_view(),
94    ;
95}
96
97pub trait MapRef<I>: SpecMap<Output = Self::O> where I: DeepView<V = Self::Input> {
98    type O;
99
100    fn map(&self, i: &I) -> (o: Self::O)
101        ensures
102            self.spec_map(i.deep_view()) == o,
103    ;
104}
105
106// pub trait MapRef<I> where I: DeepView {
107//     type O;
108//     open spec fn pre(&self, i: &I) -> bool {
109//         true
110//     }
111//     spec fn post(&self, i: &I, o: Self::O) -> bool;
112//     fn map(&self, i: &I) -> (o: Self::O)
113//         requires
114//             self.pre(i),
115//         ensures
116//             self.post(i, o),
117//     ;
118// }
119// pub type ClsWithSpec<I, O, F> = (F, Ghost<spec_fn(I) -> O>);
120// // implement MapRef for any `Fn(&I) -> O` that satisfies the pre/post conditions
121// impl<I, O, F> MapRef<I> for ClsWithSpec<I, O, F> where I: DeepView, F: Fn(&I) -> O {
122//     type O = O;
123//     open spec fn pre(&self, i: &I) -> bool {
124//         call_requires(self.0, (i,))
125//     }
126//     open spec fn post(&self, i: &I, o: O) -> bool {
127//         call_ensures(self.0, (i,), o)
128//     }
129//     fn map(&self, i: &I) -> (o: O) {
130//         (self.0)(i)
131//     }
132// }
133// impl<I, O, F> SpecMap for ClsWithSpec<I, O, F> where I: DeepView, F: Fn(&I) -> O {
134//     type Input = I;
135//     type Output = O;
136//     open spec fn spec_map(&self, i: I) -> O {
137//         let Ghost(spec_fn) = self.1;
138//         spec_fn(i)
139//     }
140// }
141/// Pairs an executable predicate closure with a ghost spec predicate.
142#[verifier::reject_recursive_types(O)]
143pub struct FnMap<
144    I: DeepView,
145    O: DeepView,
146    Exec: Fn(I) -> O,
147    Spec: SpecMap<Input = I::V, Output = O::V>,
148> {
149    exec_fn: Exec,
150    spec_fn: Ghost<Spec>,
151    _marker: PhantomData<(I, O)>,
152}
153
154impl<I: DeepView, O: DeepView, Exec: Fn(I) -> O, Spec: SpecMap<Input = I::V, Output = O::V>> FnMap<
155    I,
156    O,
157    Exec,
158    Spec,
159> {
160    #[verifier::type_invariant]
161    spec fn wf(&self) -> bool {
162        &&& forall|i: I| #[trigger] call_requires(self.exec_fn, (i,))
163        &&& forall|i: I, o: O| #[trigger]
164            call_ensures(self.exec_fn, (i,), o) ==> o.deep_view() == {
165                let Ghost(spec_fn) = self.spec_fn;
166                spec_fn.spec_map(i.deep_view())
167            }
168    }
169
170    pub fn new(exec_fn: Exec, Ghost(spec_fn): Ghost<Spec>) -> (fnmap: Self)
171        requires
172            forall|i: I| #[trigger] call_requires(exec_fn, (i,)),
173            forall|i: I, o: O| #[trigger]
174                call_ensures(exec_fn, (i,), o) ==> o.deep_view() == spec_fn.spec_map(i.deep_view()),
175    {
176        Self { exec_fn, spec_fn: Ghost(spec_fn), _marker: PhantomData }
177    }
178}
179
180impl<I, O, Exec, Spec> SpecMap for FnMap<I, O, Exec, Spec> where
181    I: DeepView,
182    O: DeepView,
183    Exec: Fn(I) -> O,
184    Spec: SpecMap<Input = I::V, Output = O::V>,
185 {
186    type Input = I::V;
187
188    type Output = O::V;
189
190    closed spec fn spec_map(&self, i: Self::Input) -> Self::Output {
191        let Ghost(spec_fn) = self.spec_fn;
192        spec_fn.spec_map(i)
193    }
194}
195
196impl<I, O, Exec, Spec> Map<I> for FnMap<I, O, Exec, Spec> where
197    I: DeepView,
198    O: DeepView,
199    Exec: Fn(I) -> O,
200    Spec: SpecMap<Input = I::V, Output = O::V>,
201 {
202    type O = O;
203
204    fn map(&self, i: I) -> (o: Self::O) {
205        proof {
206            use_type_invariant(self);
207        }
208        (self.exec_fn)(i)
209    }
210}
211
212/// Pairs an executable parser closure with a ghost specification parser.
213#[verifier::reject_recursive_types(O)]
214pub struct FnParser<
215    I: View<V = Seq<u8>>,
216    O: DeepView,
217    Spec: SpecParser<PVal = O::V>,
218    Exec: Fn(&I) -> PResult<O>,
219> {
220    pub exec_fn: Exec,
221    pub spec_fn: Ghost<Spec>,
222    pub _marker: PhantomData<(I, O)>,
223}
224
225impl<I, O, Spec, Exec> FnParser<I, O, Spec, Exec> where
226    I: View<V = Seq<u8>>,
227    O: DeepView,
228    Spec: Productive<PVal = O::V>,
229    Exec: Fn(&I) -> PResult<O>,
230 {
231    /// Constructs a safe, productive parser callback with a ghost specification.
232    pub fn new(exec_fn: Exec, Ghost(spec_fn): Ghost<Spec>) -> (parser: Self)
233        requires
234            spec_fn.safe_inv(),
235            spec_fn.productive_inv(),
236            forall|i: &I| #[trigger] call_requires(exec_fn, (i,)),
237            forall|i: &I, r: PResult<O>| #[trigger]
238                call_ensures(exec_fn, (i,), r) ==> parse_matches_spec(r, spec_fn.spec_parse(i@)),
239        ensures
240            parser.exec_inv(),
241            parser.safe_inv(),
242            parser.productive_inv(),
243            parser.spec_fn == spec_fn,
244    {
245        Self { exec_fn, spec_fn: Ghost(spec_fn), _marker: PhantomData }
246    }
247}
248
249impl<I, O, Spec, Exec> SpecParser for FnParser<I, O, Spec, Exec> where
250    I: View<V = Seq<u8>>,
251    O: DeepView,
252    Spec: SpecParser<PVal = O::V>,
253    Exec: Fn(&I) -> PResult<O>,
254 {
255    type PVal = O::V;
256
257    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
258        let Ghost(spec_fn) = self.spec_fn;
259        spec_fn.spec_parse(ibuf)
260    }
261}
262
263pub proof fn lemma_ref_fn_parser_spec_parse<I, O, Spec, Exec>(
264    parser: &FnParser<I, O, Spec, Exec>,
265    ibuf: Seq<u8>,
266) where I: View<V = Seq<u8>>, O: DeepView, Spec: SpecParser<PVal = O::V>, Exec: Fn(&I) -> PResult<O>
267    ensures
268        (&parser).spec_parse(ibuf) == parser.spec_fn@.spec_parse(ibuf),
269{
270}
271
272impl<I, O, Spec, Exec> SafeParser for FnParser<I, O, Spec, Exec> where
273    I: View<V = Seq<u8>>,
274    O: DeepView,
275    Spec: SafeParser<PVal = O::V>,
276    Exec: Fn(&I) -> PResult<O>,
277 {
278    open spec fn safe_inv(&self) -> bool {
279        let Ghost(spec_fn) = self.spec_fn;
280        spec_fn.safe_inv()
281    }
282
283    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
284        let Ghost(spec_fn) = self.spec_fn;
285        spec_fn.lemma_parse_safe(ibuf);
286    }
287}
288
289impl<I, O, Spec, Exec> Productive for FnParser<I, O, Spec, Exec> where
290    I: View<V = Seq<u8>>,
291    O: DeepView,
292    Spec: Productive<PVal = O::V>,
293    Exec: Fn(&I) -> PResult<O>,
294 {
295    open spec fn productive_inv(&self) -> bool {
296        let Ghost(spec_fn) = self.spec_fn;
297        spec_fn.productive_inv()
298    }
299
300    proof fn lemma_productive(&self, input: Seq<u8>) {
301        let Ghost(spec_fn) = self.spec_fn;
302        spec_fn.lemma_productive(input);
303    }
304}
305
306impl<I, O, Spec, Exec> Parser<I> for FnParser<I, O, Spec, Exec> where
307    I: View<V = Seq<u8>>,
308    O: DeepView,
309    Spec: SpecParser<PVal = O::V>,
310    Exec: Fn(&I) -> PResult<O>,
311 {
312    type PT = O;
313
314    open spec fn exec_inv(&self) -> bool {
315        &&& forall|i: &I| #[trigger] call_requires(self.exec_fn, (i,))
316        &&& forall|i: &I, r: PResult<O>| #[trigger]
317            call_ensures(self.exec_fn, (i,), r) ==> {
318                let Ghost(spec_fn) = self.spec_fn;
319                parse_matches_spec(r, spec_fn.spec_parse(i@))
320            }
321    }
322
323    fn parse(&self, ibuf: &I) -> (r: PResult<O>) {
324        (self.exec_fn)(ibuf)
325    }
326}
327
328/// Pairs an executable serializer closure with a ghost specification serializer.
329#[verifier::reject_recursive_types(T)]
330pub struct FnSerializer<
331    Output: OutputBuf,
332    T: DeepView + ?Sized,
333    Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>,
334    Exec: Fn(&T, &mut Output),
335> {
336    pub exec_fn: Exec,
337    pub spec_fn: Ghost<Spec>,
338    pub _output: PhantomData<Output>,
339    pub _marker: PhantomData<T>,
340}
341
342impl<Output, T, Spec, Exec> FnSerializer<Output, T, Spec, Exec> where
343    Output: OutputBuf,
344    T: DeepView + ?Sized,
345    Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>,
346    Exec: Fn(&T, &mut Output),
347 {
348    pub fn new(exec_fn: Exec, Ghost(spec_fn): Ghost<Spec>) -> (serializer: Self)
349        requires
350            forall|v: &T, obuf: &mut Output|
351                (spec_fn.consistent(v.deep_view()) && obuf.fits(spec_fn.byte_len(v.deep_view())))
352                    ==> #[trigger] call_requires(exec_fn, (v, obuf)),
353            forall|v: &T, obuf: &mut Output|
354                (spec_fn.consistent(v.deep_view()) && #[trigger] call_ensures(
355                    exec_fn,
356                    (v, obuf),
357                    (),
358                )) ==> {
359                    &&& final(obuf)@ == obuf@ + spec_fn.spec_serialize(v.deep_view())
360                    &&& forall|n| #[trigger]
361                        obuf.fits(spec_fn.byte_len(v.deep_view()) + n) <==> final(obuf).fits(n)
362                    &&& obuf.same_destination(final(obuf))
363                },
364        ensures
365            serializer.exec_inv(),
366            serializer.spec_fn == spec_fn,
367    {
368        Self { exec_fn, spec_fn: Ghost(spec_fn), _output: PhantomData, _marker: PhantomData }
369    }
370}
371
372impl<Output, T, Spec, Exec> SpecSerializer for FnSerializer<Output, T, Spec, Exec> where
373    Output: OutputBuf,
374    T: DeepView + ?Sized,
375    Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>,
376    Exec: Fn(&T, &mut Output),
377 {
378    type SVal = T::V;
379
380    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
381        let Ghost(spec_fn) = self.spec_fn;
382        spec_fn.spec_serialize(v)
383    }
384}
385
386impl<Output, T, Spec, Exec> SpecByteLen for FnSerializer<Output, T, Spec, Exec> where
387    Output: OutputBuf,
388    T: DeepView + ?Sized,
389    Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>,
390    Exec: Fn(&T, &mut Output),
391 {
392    type T = T::V;
393
394    open spec fn byte_len(&self, v: Self::T) -> nat {
395        let Ghost(spec_fn) = self.spec_fn;
396        spec_fn.byte_len(v)
397    }
398}
399
400impl<Output, T, Spec, Exec> GoodSerializer for FnSerializer<Output, T, Spec, Exec> where
401    Output: OutputBuf,
402    T: DeepView + ?Sized,
403    Spec: GoodSerializer<T = T::V> + Consistency<Val = T::V>,
404    Exec: Fn(&T, &mut Output),
405 {
406    open spec fn serialize_inv(&self) -> bool {
407        let Ghost(spec_fn) = self.spec_fn;
408        spec_fn.serialize_inv()
409    }
410
411    proof fn lemma_serialize_len(&self, v: Self::SVal) {
412        let Ghost(spec_fn) = self.spec_fn;
413        spec_fn.lemma_serialize_len(v)
414    }
415}
416
417impl<Output, T, Spec, Exec> Consistency for FnSerializer<Output, T, Spec, Exec> where
418    Output: OutputBuf,
419    T: DeepView + ?Sized,
420    Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>,
421    Exec: Fn(&T, &mut Output),
422 {
423    type Val = T::V;
424
425    open spec fn consistent(&self, v: Self::Val) -> bool {
426        let Ghost(spec_fn) = self.spec_fn;
427        spec_fn.consistent(v)
428    }
429}
430
431impl<Output, T, Spec, Exec> Serializer<Output, T> for FnSerializer<Output, T, Spec, Exec> where
432    Output: OutputBuf,
433    T: DeepView + ?Sized,
434    Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>,
435    Exec: Fn(&T, &mut Output),
436 {
437    #[verifier::prophetic]
438    open spec fn exec_inv(&self) -> bool {
439        let Ghost(spec_fn) = self.spec_fn;
440        &&& forall|v: &T, obuf: &mut Output|
441            (spec_fn.consistent(v.deep_view()) && obuf.fits(spec_fn.byte_len(v.deep_view())))
442                ==> #[trigger] call_requires(self.exec_fn, (v, obuf))
443        &&& forall|v: &T, obuf: &mut Output|
444            (spec_fn.consistent(v.deep_view()) && #[trigger] call_ensures(
445                self.exec_fn,
446                (v, obuf),
447                (),
448            )) ==> {
449                &&& final(obuf)@ == obuf@ + spec_fn.spec_serialize(v.deep_view())
450                &&& forall|n| #[trigger]
451                    obuf.fits(spec_fn.byte_len(v.deep_view()) + n) <==> final(obuf).fits(n)
452                &&& obuf.same_destination(final(obuf))
453            }
454    }
455
456    fn serialize_into(&self, v: &T, obuf: &mut Output) {
457        (self.exec_fn)(v, obuf)
458    }
459}
460
461/// Pairs an executable preparation closure with its consistency and byte-length specification.
462#[verifier::reject_recursive_types(T)]
463pub struct FnPrepare<
464    T: DeepView + ?Sized,
465    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
466    Exec: Fn(&T) -> Result<usize, PreSerializeError>,
467> {
468    pub exec_fn: Exec,
469    pub spec_fn: Ghost<Spec>,
470    pub _marker: PhantomData<T>,
471}
472
473impl<T, Spec, Exec> FnPrepare<T, Spec, Exec> where
474    T: DeepView + ?Sized,
475    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
476    Exec: Fn(&T) -> Result<usize, PreSerializeError>,
477{
478    pub fn new(exec_fn: Exec, Ghost(spec_fn): Ghost<Spec>) -> (prepare: Self)
479        requires
480            forall|value: &T| #[trigger] call_requires(exec_fn, (value,)),
481            forall|value: &T, result: Result<usize, PreSerializeError>|
482                #[trigger] call_ensures(exec_fn, (value,), result) ==> (
483                    result matches Ok(len) ==> {
484                        &&& spec_fn.consistent(value.deep_view())
485                        &&& len == spec_fn.byte_len(value.deep_view())
486                    }
487                ),
488        ensures
489            prepare.exec_inv(),
490            prepare.spec_fn == spec_fn,
491    {
492        Self { exec_fn, spec_fn: Ghost(spec_fn), _marker: PhantomData }
493    }
494}
495
496impl<T, Spec, Exec> Consistency for FnPrepare<T, Spec, Exec> where
497    T: DeepView + ?Sized,
498    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
499    Exec: Fn(&T) -> Result<usize, PreSerializeError>,
500{
501    type Val = T::V;
502
503    open spec fn consistent(&self, value: Self::Val) -> bool {
504        self.spec_fn@.consistent(value)
505    }
506}
507
508impl<T, Spec, Exec> SpecByteLen for FnPrepare<T, Spec, Exec> where
509    T: DeepView + ?Sized,
510    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
511    Exec: Fn(&T) -> Result<usize, PreSerializeError>,
512{
513    type T = T::V;
514
515    open spec fn byte_len(&self, value: Self::T) -> nat {
516        self.spec_fn@.byte_len(value)
517    }
518}
519
520impl<T, Spec, Exec> Prepare<T> for FnPrepare<T, Spec, Exec> where
521    T: DeepView + ?Sized,
522    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
523    Exec: Fn(&T) -> Result<usize, PreSerializeError>,
524{
525    open spec fn exec_inv(&self) -> bool {
526        &&& forall|value: &T| #[trigger] call_requires(self.exec_fn, (value,))
527        &&& forall|value: &T, result: Result<usize, PreSerializeError>|
528            #[trigger] call_ensures(self.exec_fn, (value,), result) ==> (
529                result matches Ok(len) ==> {
530                    &&& self.spec_fn@.consistent(value.deep_view())
531                    &&& len == self.spec_fn@.byte_len(value.deep_view())
532                }
533            )
534    }
535
536    fn prepare(&self, value: &T) -> Result<usize, PreSerializeError> {
537        (self.exec_fn)(value)
538    }
539}
540
541/// Pairs an executable byte-length closure with its specification.
542#[verifier::reject_recursive_types(T)]
543pub struct FnByteLen<
544    T: DeepView + ?Sized,
545    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
546    Exec: Fn(&T) -> usize,
547> {
548    pub exec_fn: Exec,
549    pub spec_fn: Ghost<Spec>,
550    pub _marker: PhantomData<T>,
551}
552
553impl<T, Spec, Exec> FnByteLen<T, Spec, Exec> where
554    T: DeepView + ?Sized,
555    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
556    Exec: Fn(&T) -> usize,
557{
558    pub fn new(exec_fn: Exec, Ghost(spec_fn): Ghost<Spec>) -> (length: Self)
559        requires
560            forall|value: &T|
561                spec_fn.byte_len(value.deep_view()) <= usize::MAX ==> #[trigger]
562                    call_requires(exec_fn, (value,)),
563            forall|value: &T, len: usize| #[trigger]
564                call_ensures(exec_fn, (value,), len) ==> len == spec_fn.byte_len(
565                    value.deep_view(),
566                ),
567        ensures
568            length.exec_inv(),
569            length.spec_fn == spec_fn,
570    {
571        Self { exec_fn, spec_fn: Ghost(spec_fn), _marker: PhantomData }
572    }
573}
574
575impl<T, Spec, Exec> Consistency for FnByteLen<T, Spec, Exec> where
576    T: DeepView + ?Sized,
577    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
578    Exec: Fn(&T) -> usize,
579{
580    type Val = T::V;
581
582    open spec fn consistent(&self, value: Self::Val) -> bool {
583        self.spec_fn@.consistent(value)
584    }
585}
586
587impl<T, Spec, Exec> SpecByteLen for FnByteLen<T, Spec, Exec> where
588    T: DeepView + ?Sized,
589    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
590    Exec: Fn(&T) -> usize,
591{
592    type T = T::V;
593
594    open spec fn byte_len(&self, value: Self::T) -> nat {
595        self.spec_fn@.byte_len(value)
596    }
597}
598
599impl<T, Spec, Exec> ByteLen<T> for FnByteLen<T, Spec, Exec> where
600    T: DeepView + ?Sized,
601    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
602    Exec: Fn(&T) -> usize,
603{
604    open spec fn exec_inv(&self) -> bool {
605        &&& forall|value: &T|
606            self.spec_fn@.byte_len(value.deep_view()) <= usize::MAX ==> #[trigger]
607                call_requires(self.exec_fn, (value,))
608        &&& forall|value: &T, len: usize| #[trigger]
609            call_ensures(self.exec_fn, (value,), len) ==> len == self.spec_fn@.byte_len(
610                value.deep_view(),
611            )
612    }
613
614    fn length(&self, value: &T) -> usize {
615        (self.exec_fn)(value)
616    }
617}
618
619} // verus!
vest_lib/core/exec/fns.rs

vest_lib/core/exec/
fns.rs
