vest_lib/cbor/
format.rs

1//! Recursive generic-CBOR format specifications, proofs, and execution.
2//!
3//! [`CborFmt`] uses [`FixWith`] for its pure
4//! recursive grammar and bounded executable parsing. Its `DET` parameter
5//! selects general or deterministic head and container encodings.
6use alloc::{boxed::Box, string::String, vec::Vec};
7
8use crate::asn1::Utf8StringFmt;
9use crate::combinators::{
10    bytes::ExactLen,
11    mapped::spec::{FnSpecMapper, LosslessMapper, LossyMapper, SpecMapper},
12    recursive::{
13        BundledSpecs, EquivSerializersGeneralRecBody, GoodSerializerRecBody, NonMalleableRecBody,
14        NonTailFmtRecBody, ParamRecSpecs, ParserRecBody, PrepareRecBody, ProductiveRecBody,
15        SPRoundTripDpsRecBody, SafeParserRecBody, SerializerRecBody, SoundParserRecBody,
16        SpecRecBody,
17    },
18    Bind, Empty, FixWith, Mapped, Pair, Repeat, RepeatN, Sum, Tail, Void,
19};
20use crate::core::exec::{
21    fns::{FnByteLen, FnParser, FnPrepare, FnSerializer},
22    input::{InputBuf, InputSlice},
23    output::OutputBuf,
24    parser::*,
25    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
26    ParseError,
27};
28use crate::core::{proof::*, spec::*};
29use crate::Never;
30use vstd::assert_seqs_equal;
31use vstd::prelude::*;
32use vstd::string::StringSliceAdditionalSpecFns;
33
34use super::{
35    CborBytes, CborFloat, CborHead, CborHeadFmt, CborHeadValue, CborText, CborValue, CborValueSpec,
36    MajorType, BREAK, MAX_RECURSION_DEPTH,
37};
38use Sum::Inl as L;
39use Sum::Inr as R;
40
41use super::chunk::{flatten_byte_chunks, flatten_text_chunks, ByteChunkFmt, TextChunkFmt};
42
43verus! {
44
45type CborWire = (
46    CborHead,
47    Sum<
48        (),
49        Sum<
50            (),
51            Sum<
52                Seq<u8>,
53                Sum<
54                    (Seq<Seq<u8>>, u8),
55                    Sum<
56                        Seq<char>,
57                        Sum<
58                            (Seq<Seq<char>>, u8),
59                            Sum<
60                                Seq<CborValueSpec>,
61                                Sum<
62                                    (Seq<CborValueSpec>, u8),
63                                    Sum<
64                                        Seq<(CborValueSpec, CborValueSpec)>,
65                                        Sum<
66                                            (Seq<(CborValueSpec, CborValueSpec)>, u8),
67                                            Sum<CborValueSpec, Sum<(), Never>>,
68                                        >,
69                                    >,
70                                >,
71                            >,
72                        >,
73                    >,
74                >,
75            >,
76        >,
77    >,
78);
79
80type CborBranches<Rec, const DET: bool> = Sum<
81    Empty,
82    Sum<
83        Empty,
84        Sum<
85            ExactLen<Tail, u64>,
86            Sum<
87                Repeat<ByteChunkFmt<DET>, super::BreakFmt>,
88                Sum<
89                    ExactLen<Utf8StringFmt, u64>,
90                    Sum<
91                        Repeat<TextChunkFmt<DET>, super::BreakFmt>,
92                        Sum<
93                            RepeatN<Rec, u64>,
94                            Sum<
95                                Repeat<Rec, super::BreakFmt>,
96                                Sum<
97                                    RepeatN<Pair<Rec, Rec>, u64>,
98                                    Sum<
99                                        Repeat<Pair<Rec, Rec>, super::BreakFmt>,
100                                        Sum<Rec, Sum<Empty, Void>>,
101                                    >,
102                                >,
103                            >,
104                        >,
105                    >,
106                >,
107            >,
108        >,
109    >,
110>;
111
112type CborParseBodyInnerFmt<Rec, const DET: bool> = Mapped<
113    Bind<CborHeadFmt<DET>, spec_fn(CborHead) -> CborBranches<Rec, DET>>,
114    CborMapper<DET>,
115>;
116
117type NormalizedOnly<T> = Mapped<Void, FnSpecMapper<Never, T>>;
118
119pub open spec fn normalized_only<T>() -> NormalizedOnly<T> {
120    Mapped {
121        inner: Void("indefinite-length form is not emitted"),
122        mapper: (|_never: Never| arbitrary(), |_value: T| arbitrary()),
123    }
124}
125
126type CborNormalizedBranches<Rec, const DET: bool> = Sum<
127    Empty,
128    Sum<
129        Empty,
130        Sum<
131            ExactLen<Tail, u64>,
132            Sum<
133                NormalizedOnly<(Seq<Seq<u8>>, u8)>,
134                Sum<
135                    ExactLen<Utf8StringFmt, u64>,
136                    Sum<
137                        NormalizedOnly<(Seq<Seq<char>>, u8)>,
138                        Sum<
139                            RepeatN<Rec, u64>,
140                            Sum<
141                                NormalizedOnly<(Seq<CborValueSpec>, u8)>,
142                                Sum<
143                                    RepeatN<Pair<Rec, Rec>, u64>,
144                                    Sum<
145                                        NormalizedOnly<(Seq<(CborValueSpec, CborValueSpec)>, u8)>,
146                                        Sum<Rec, Sum<Empty, Void>>,
147                                    >,
148                                >,
149                            >,
150                        >,
151                    >,
152                >,
153            >,
154        >,
155    >,
156>;
157
158type CborNormalizedBodyInnerFmt<Rec, const DET: bool> = Mapped<
159    Bind<CborHeadFmt<DET>, spec_fn(CborHead) -> CborNormalizedBranches<Rec, DET>>,
160    CborMapper<DET>,
161>;
162
163pub open spec fn cbor_value_valid(value: CborValueSpec) -> bool {
164    match value {
165        CborValueSpec::Integer(value) => {
166            &&& value as int >= -1 - u64::MAX as int
167            &&& value as int <= u64::MAX as int
168        },
169        CborValueSpec::Bytes(bytes) => bytes.len() <= u64::MAX,
170        CborValueSpec::Text(text) => vstd::utf8::encode_utf8(text).len() <= u64::MAX,
171        CborValueSpec::Array(values) => values.len() <= u64::MAX,
172        CborValueSpec::Map(entries) => entries.len() <= u64::MAX,
173        CborValueSpec::Simple(value) => value <= 19u8 || value >= 32u8,
174        _ => true,
175    }
176}
177
178pub open spec fn cbor_wire_valid<const DET: bool>(wire: CborWire) -> bool {
179    #[verusfmt::skip]
180    match wire {
181        (CborHead { major: MajorType::Unsigned, value: CborHeadValue::Argument(_) }, L(())) => true,
182        (CborHead { major: MajorType::Negative, value: CborHeadValue::Argument(_) }, R(L(()))) => true,
183        (CborHead { major: MajorType::Bytes, value: CborHeadValue::Argument(len) }, R(R(L(bytes)))) => len == bytes.len(),
184        (CborHead { major: MajorType::Bytes, value: CborHeadValue::Indefinite }, R(R(R(L(_))))) => !DET,
185        (CborHead { major: MajorType::Text, value: CborHeadValue::Argument(len) }, R(R(R(R(L(text)))))) => len == vstd::utf8::encode_utf8(text).len(),
186        (CborHead { major: MajorType::Text, value: CborHeadValue::Indefinite }, R(R(R(R(R(L(_))))))) => !DET,
187        (CborHead { major: MajorType::Array, value: CborHeadValue::Argument(len) }, R(R(R(R(R(R(L(values)))))))) => len == values.len(),
188        (CborHead { major: MajorType::Array, value: CborHeadValue::Indefinite }, R(R(R(R(R(R(R(L(_))))))))) => !DET,
189        (CborHead { major: MajorType::Map, value: CborHeadValue::Argument(len) }, R(R(R(R(R(R(R(R(L(entries)))))))))) => len == entries.len(),
190        (CborHead { major: MajorType::Map, value: CborHeadValue::Indefinite }, R(R(R(R(R(R(R(R(R(L(_))))))))))) => !DET,
191        (CborHead { major: MajorType::Tag, value: CborHeadValue::Argument(_) }, R(R(R(R(R(R(R(R(R(R(L(_)))))))))))) => true,
192        (CborHead { major: MajorType::Simple, value }, R(R(R(R(R(R(R(R(R(R(R(L(()))))))))))))) => match value {
193            CborHeadValue::Float(_) => true,
194            CborHeadValue::Simple(value) => value <= 23u8 || value >= 32u8,
195            _ => false,
196        },
197        _ => false,
198    }
199}
200
201pub open spec fn decode_cbor_wire(wire: CborWire) -> CborValueSpec {
202    let head = wire.0;
203    #[verusfmt::skip]
204    match wire.1 {
205        L(()) => match head.value {
206            CborHeadValue::Argument(value) => CborValueSpec::Integer(value as i128),
207            _ => arbitrary(),
208        },
209        R(L(())) => match head.value {
210            CborHeadValue::Argument(value) => CborValueSpec::Integer((-1 - value as int) as i128),
211            _ => arbitrary(),
212        },
213        R(R(L(bytes))) => CborValueSpec::Bytes(bytes),
214        R(R(R(L((chunks, _break))))) => CborValueSpec::Bytes(chunks.flatten()),
215        R(R(R(R(L(text))))) => CborValueSpec::Text(text),
216        R(R(R(R(R(L((chunks, _break))))))) => CborValueSpec::Text(chunks.flatten()),
217        R(R(R(R(R(R(L(values))))))) => CborValueSpec::Array(values),
218        R(R(R(R(R(R(R(L((values, _break))))))))) => CborValueSpec::Array(values),
219        R(R(R(R(R(R(R(R(L(entries))))))))) => CborValueSpec::Map(entries),
220        R(R(R(R(R(R(R(R(R(L((entries, _break))))))))))) => CborValueSpec::Map(entries),
221        R(R(R(R(R(R(R(R(R(R(L(value))))))))))) => match head.value {
222            CborHeadValue::Argument(tag) => CborValueSpec::Tag(tag, Box::new(value)),
223            _ => arbitrary(),
224        },
225        R(R(R(R(R(R(R(R(R(R(R(L(())))))))))))) => match head.value {
226            CborHeadValue::Float(value) => CborValueSpec::Float(value),
227            CborHeadValue::Simple(20) => CborValueSpec::Bool(false),
228            CborHeadValue::Simple(21) => CborValueSpec::Bool(true),
229            CborHeadValue::Simple(22) => CborValueSpec::Null,
230            CborHeadValue::Simple(23) => CborValueSpec::Undefined,
231            CborHeadValue::Simple(value) => CborValueSpec::Simple(value),
232            _ => arbitrary(),
233        },
234        _ => arbitrary(),
235    }
236}
237
238pub open spec fn encode_cbor_value(value: CborValueSpec) -> CborWire {
239    #[verusfmt::skip]
240    match value {
241        CborValueSpec::Integer(value) if value >= 0 => (
242            CborHead { major: MajorType::Unsigned, value: CborHeadValue::Argument(value as u64) },
243            L(()),
244        ),
245        CborValueSpec::Integer(value) => (
246            CborHead {
247                major: MajorType::Negative,
248                value: CborHeadValue::Argument((-1 - value as int) as u64),
249            },
250            R(L(())),
251        ),
252        CborValueSpec::Bytes(bytes) => (
253            CborHead {
254                major: MajorType::Bytes,
255                value: CborHeadValue::Argument(bytes.len() as u64),
256            },
257            R(R(L(bytes))),
258        ),
259        CborValueSpec::Text(text) => (
260            CborHead {
261                major: MajorType::Text,
262                value: CborHeadValue::Argument(vstd::utf8::encode_utf8(text).len() as u64),
263            },
264            R(R(R(R(L(text))))),
265        ),
266        CborValueSpec::Array(values) => (
267            CborHead {
268                major: MajorType::Array,
269                value: CborHeadValue::Argument(values.len() as u64),
270            },
271            R(R(R(R(R(R(L(values))))))),
272        ),
273        CborValueSpec::Map(entries) => (
274            CborHead {
275                major: MajorType::Map,
276                value: CborHeadValue::Argument(entries.len() as u64),
277            },
278            R(R(R(R(R(R(R(R(L(entries))))))))),
279        ),
280        CborValueSpec::Tag(tag, value) => (
281            CborHead { major: MajorType::Tag, value: CborHeadValue::Argument(tag) },
282            R(R(R(R(R(R(R(R(R(R(L(*value))))))))))),
283        ),
284        CborValueSpec::Float(value) => (
285            CborHead { major: MajorType::Simple, value: CborHeadValue::Float(value) },
286            R(R(R(R(R(R(R(R(R(R(R(L(())))))))))))),
287        ),
288        CborValueSpec::Bool(value) => (
289            CborHead {
290                major: MajorType::Simple,
291                value: CborHeadValue::Simple(if value { 21 } else { 20 }),
292            },
293            R(R(R(R(R(R(R(R(R(R(R(L(())))))))))))),
294        ),
295        CborValueSpec::Null => (
296            CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(22) },
297            R(R(R(R(R(R(R(R(R(R(R(L(())))))))))))),
298        ),
299        CborValueSpec::Undefined => (
300            CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(23) },
301            R(R(R(R(R(R(R(R(R(R(R(L(())))))))))))),
302        ),
303        CborValueSpec::Simple(value) => (
304            CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(value) },
305            R(R(R(R(R(R(R(R(R(R(R(L(())))))))))))),
306        ),
307    }
308}
309
310#[derive(Clone, Copy)]
311pub struct CborMapper<const DET: bool>;
312
313impl<const DET: bool> SpecMapper for CborMapper<DET> {
314    type In = CborWire;
315
316    type Out = CborValueSpec;
317
318    open spec fn spec_map(&self, wire: Self::In) -> Self::Out {
319        decode_cbor_wire(wire)
320    }
321
322    open spec fn spec_map_rev(&self, value: Self::Out) -> Self::In {
323        encode_cbor_value(value)
324    }
325
326    open spec fn wf_in(&self, wire: Self::In) -> bool {
327        cbor_wire_valid::<DET>(wire)
328    }
329
330    open spec fn wf_out(&self, value: Self::Out) -> bool {
331        cbor_value_valid(value)
332    }
333}
334
335impl<const DET: bool> LossyMapper for CborMapper<DET> {
336    proof fn lemma_sound_mapper(&self, value: Self::Out) {
337    }
338
339    proof fn lemma_mapper_wf_out_in(&self, value: Self::Out) {
340    }
341}
342
343impl LosslessMapper for CborMapper<true> {
344    proof fn lemma_lossless_mapper(&self, wire: Self::In) {
345        assert(cbor_wire_valid::<true>(wire));
346        assert(encode_cbor_value(decode_cbor_wire(wire)) == wire);
347    }
348
349    proof fn lemma_mapper_wf_in_out(&self, wire: Self::In) {
350    }
351}
352
353#[doc(hidden)]
354pub open spec fn cbor_parse_body<const DET: bool>(
355    rec: ParamRecSpecs<(), CborValueSpec>,
356) -> CborParseBodyInnerFmt<BundledSpecs<CborValueSpec>, DET> {
357    let child = rec(());
358    #[verusfmt::skip]
359    Mapped {
360        inner: Bind(
361            CborHeadFmt::<DET>,
362            |head: CborHead|
363                match head {
364                    CborHead { major: MajorType::Unsigned, value: CborHeadValue::Argument(_) } => L(Empty),
365                    CborHead { major: MajorType::Negative, value: CborHeadValue::Argument(_) } => R(L(Empty)),
366                    CborHead { major: MajorType::Bytes, value: CborHeadValue::Argument(len) } => R(R(L(ExactLen(len, Tail)))),
367                    CborHead { major: MajorType::Bytes, value: CborHeadValue::Indefinite } => R(R(R(L(Repeat(ByteChunkFmt::<DET>, BREAK))))),
368                    CborHead { major: MajorType::Text, value: CborHeadValue::Argument(len) } => R(R(R(R(L(ExactLen(len, Utf8StringFmt)))))),
369                    CborHead { major: MajorType::Text, value: CborHeadValue::Indefinite } => R(R(R(R(R(L(Repeat(TextChunkFmt::<DET>, BREAK))))))),
370                    CborHead { major: MajorType::Array, value: CborHeadValue::Argument(len) } => R(R(R(R(R(R(L(RepeatN(len, child)))))))),
371                    CborHead { major: MajorType::Array, value: CborHeadValue::Indefinite } => R(R(R(R(R(R(R(L(Repeat(child, BREAK))))))))),
372                    CborHead { major: MajorType::Map, value: CborHeadValue::Argument(len) } => R(R(R(R(R(R(R(R(L(RepeatN(len, Pair(child, child))))))))))),
373                    CborHead { major: MajorType::Map, value: CborHeadValue::Indefinite } => R(R(R(R(R(R(R(R(R(L(Repeat(Pair(child, child), BREAK))))))))))),
374                    CborHead { major: MajorType::Tag, value: CborHeadValue::Argument(_) } => R(R(R(R(R(R(R(R(R(R(L(child))))))))))),
375                    CborHead { major: MajorType::Simple, value } if value != CborHeadValue::Break => R(R(R(R(R(R(R(R(R(R(R(L(Empty)))))))))))),
376                    _ => R(R(R(R(R(R(R(R(R(R(R(R(Void("invalid CBOR head/value combination"))))))))))))),
377                },
378        ),
379        mapper: CborMapper::<DET>,
380    }
381}
382
383#[doc(hidden)]
384pub open spec fn cbor_normalized_body<const DET: bool>(
385    rec: ParamRecSpecs<(), CborValueSpec>,
386) -> CborNormalizedBodyInnerFmt<BundledSpecs<CborValueSpec>, DET> {
387    let child = rec(());
388    #[verusfmt::skip]
389    Mapped {
390        inner: Bind(
391            CborHeadFmt::<DET>,
392            |head: CborHead|
393                match head {
394                    CborHead { major: MajorType::Unsigned, value: CborHeadValue::Argument(_) } => L(Empty),
395                    CborHead { major: MajorType::Negative, value: CborHeadValue::Argument(_) } => R(L(Empty)),
396                    CborHead { major: MajorType::Bytes, value: CborHeadValue::Argument(len) } => R(R(L(ExactLen(len, Tail)))),
397                    CborHead { major: MajorType::Bytes, value: CborHeadValue::Indefinite } => R(R(R(L(normalized_only())))),
398                    CborHead { major: MajorType::Text, value: CborHeadValue::Argument(len) } => R(R(R(R(L(ExactLen(len, Utf8StringFmt)))))),
399                    CborHead { major: MajorType::Text, value: CborHeadValue::Indefinite } => R(R(R(R(R(L(normalized_only())))))),
400                    CborHead { major: MajorType::Array, value: CborHeadValue::Argument(len) } => R(R(R(R(R(R(L(RepeatN(len, child)))))))),
401                    CborHead { major: MajorType::Array, value: CborHeadValue::Indefinite } => R(R(R(R(R(R(R(L(normalized_only())))))))),
402                    CborHead { major: MajorType::Map, value: CborHeadValue::Argument(len) } => R(R(R(R(R(R(R(R(L(RepeatN(len, Pair(child, child))))))))))),
403                    CborHead { major: MajorType::Map, value: CborHeadValue::Indefinite } => R(R(R(R(R(R(R(R(R(L(normalized_only())))))))))),
404                    CborHead { major: MajorType::Tag, value: CborHeadValue::Argument(_) } => R(R(R(R(R(R(R(R(R(R(L(child))))))))))),
405                    CborHead { major: MajorType::Simple, value } if value != CborHeadValue::Break => R(R(R(R(R(R(R(R(R(R(R(L(Empty)))))))))))),
406                    _ => R(R(R(R(R(R(R(R(R(R(R(R(Void("invalid CBOR head/value combination"))))))))))))),
407                },
408        ),
409        mapper: CborMapper::<DET>,
410    }
411}
412
413proof fn lemma_normalized_parse_implies_parse<const DET: bool>(
414    rec: ParamRecSpecs<(), CborValueSpec>,
415    input: Seq<u8>,
416)
417    ensures
418        cbor_normalized_body::<DET>(rec).spec_parse(input) matches Some((n, value))
419            ==> cbor_parse_body::<DET>(rec).spec_parse(input) == Some((n, value)),
420{
421}
422
423proof fn lemma_parse_normalized_consistency<const DET: bool>(
424    rec: ParamRecSpecs<(), CborValueSpec>,
425    value: CborValueSpec,
426)
427    ensures
428        cbor_parse_body::<DET>(rec).consistent(value) == cbor_normalized_body::<DET>(
429            rec,
430        ).consistent(value),
431{
432}
433
434proof fn lemma_parse_normalized_byte_len<const DET: bool>(
435    rec: ParamRecSpecs<(), CborValueSpec>,
436    value: CborValueSpec,
437)
438    ensures
439        cbor_parse_body::<DET>(rec).byte_len(value) == cbor_normalized_body::<DET>(rec).byte_len(
440            value,
441        ),
442{
443}
444
445/// One recursive CBOR unfolding with a permissive parser and normalized serializer semantics.
446#[doc(hidden)]
447pub struct CborBodyFmt<const DET: bool> {
448    pub rec: Ghost<ParamRecSpecs<(), CborValueSpec>>,
449}
450
451pub open spec fn cbor_body<const DET: bool>(rec: ParamRecSpecs<(), CborValueSpec>) -> CborBodyFmt<
452    DET,
453> {
454    CborBodyFmt { rec: Ghost(rec) }
455}
456
457pub struct CborRecBody<const DET: bool>;
458
459impl<const DET: bool> SpecRecBody for CborRecBody<DET> {
460    type Param = ();
461
462    type T = CborValueSpec;
463
464    type Body = CborBodyFmt<DET>;
465
466    open spec fn spec_body(&self, _param: (), rec: ParamRecSpecs<(), CborValueSpec>) -> Self::Body {
467        cbor_body::<DET>(rec)
468    }
469}
470
471fn parse_cbor_with_child<'i, const DET: bool, P>(
472    Ghost(spec_rec): Ghost<ParamRecSpecs<(), CborValueSpec>>,
473    child: &P,
474    input: &&'i [u8],
475) -> (result: PResult<CborValue<'i>>) where
476    P: Parser<&'i [u8], PT = CborValue<'i>, PVal = CborValueSpec> + Productive,
477
478    requires
479        child.exec_inv(),
480        child.safe_inv(),
481        child.productive_inv(),
482        parser_congruent(child, spec_rec(())),
483    ensures
484        parse_matches_spec(result, cbor_body::<DET>(spec_rec).spec_parse(input@)),
485{
486    use crate::combinators::congruence::*;
487    use crate::core::exec::bridge_lemmas::*;
488
489    broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
490    broadcast use lemma_parser_congruent_reflexive;
491
492    let _ = input.len();
493    let (head_len, head) = CborHeadFmt::<DET>.parse(input)?;
494    proof {
495        CborHeadFmt::<DET>.lemma_parse_safe(input@);
496    }
497    let rest = input.skip(head_len);
498
499    let ghost child_spec = spec_rec(());
500    proof {
501        lemma_ref_parser_exec_inv::<&'i [u8], _>(child);
502        lemma_ref_safe_productive_inv(child);
503    }
504
505    match head {
506        CborHead { major: MajorType::Unsigned, value: CborHeadValue::Argument(value) } => {
507            Ok((head_len, CborValue::Integer(value as i128)))
508        },
509        CborHead { major: MajorType::Negative, value: CborHeadValue::Argument(value) } => {
510            Ok((head_len, CborValue::Integer(-1i128 - value as i128)))
511        },
512        CborHead { major: MajorType::Bytes, value: CborHeadValue::Argument(len) } => {
513            let (content_len, bytes) = ExactLen(len, Tail).parse(&rest)?;
514            Ok((head_len + content_len, CborValue::Bytes(CborBytes::Definite(bytes))))
515        },
516        CborHead { major: MajorType::Bytes, value: CborHeadValue::Indefinite } => {
517            let repeated = Repeat(ByteChunkFmt::<DET>, BREAK);
518            let (content_len, (chunks, _break)) = repeated.parse(&rest)?;
519            let bytes = flatten_byte_chunks(chunks);
520            Ok((head_len + content_len, CborValue::Bytes(CborBytes::Indefinite(bytes))))
521        },
522        CborHead { major: MajorType::Text, value: CborHeadValue::Argument(len) } => {
523            let (content_len, text) = ExactLen(len, Utf8StringFmt).parse(&rest)?;
524            Ok((head_len + content_len, CborValue::Text(CborText::Definite(text))))
525        },
526        CborHead { major: MajorType::Text, value: CborHeadValue::Indefinite } => {
527            let repeated = Repeat(TextChunkFmt::<DET>, BREAK);
528            let (content_len, (chunks, _break)) = repeated.parse(&rest)?;
529            let text = flatten_text_chunks(chunks);
530            Ok((head_len + content_len, CborValue::Text(CborText::Indefinite(text))))
531        },
532        CborHead { major: MajorType::Array, value: CborHeadValue::Argument(len) } => {
533            let repeated = RepeatN(len, child);
534            proof {
535                lemma_repeat_n_parser_exec_inv::<&'i [u8], _, _>(&repeated);
536                lemma_repeat_n_parser_congruence(repeated, RepeatN(len, child_spec));
537                lemma_parser_congruent_apply(repeated, RepeatN(len, child_spec), rest@);
538            }
539            let (content_len, values) = repeated.parse(&rest)?;
540            let value = CborValue::Array(values);
541            proof {
542                super::value::lemma_collection_value_view(&value);
543            }
544            Ok((head_len + content_len, value))
545        },
546        CborHead { major: MajorType::Array, value: CborHeadValue::Indefinite } => {
547            let repeated = Repeat(child, BREAK);
548            proof {
549                lemma_repeat_parser_exec_inv::<&'i [u8], _, _>(&repeated);
550                lemma_repeat_parser_congruence(child, child_spec, BREAK, BREAK);
551                lemma_parser_congruent_apply(repeated, Repeat(child_spec, BREAK), rest@);
552            }
553            let (content_len, (values, _break)) = repeated.parse(&rest)?;
554            let value = CborValue::Array(values);
555            proof {
556                super::value::lemma_collection_value_view(&value);
557            }
558            Ok((head_len + content_len, value))
559        },
560        CborHead { major: MajorType::Map, value: CborHeadValue::Argument(len) } => {
561            let entry = Pair(child, child);
562            let repeated = RepeatN(len, entry);
563            proof {
564                lemma_pair_parser_exec_inv::<&'i [u8], _, _>(&entry);
565                lemma_pair_parser_congruence(child, child_spec, child, child_spec);
566                lemma_repeat_n_parser_exec_inv::<&'i [u8], _, _>(&repeated);
567                lemma_repeat_n_parser_congruence(
568                    repeated,
569                    RepeatN(len, Pair(child_spec, child_spec)),
570                );
571                lemma_parser_congruent_apply(
572                    repeated,
573                    RepeatN(len, Pair(child_spec, child_spec)),
574                    rest@,
575                );
576            }
577            let (content_len, entries) = repeated.parse(&rest)?;
578            let value = CborValue::Map(entries);
579            proof {
580                super::value::lemma_collection_value_view(&value);
581            }
582            Ok((head_len + content_len, value))
583        },
584        CborHead { major: MajorType::Map, value: CborHeadValue::Indefinite } => {
585            let entry = Pair(child, child);
586            let repeated = Repeat(entry, BREAK);
587            proof {
588                lemma_pair_parser_exec_inv::<&'i [u8], _, _>(&entry);
589                lemma_pair_parser_congruence(child, child_spec, child, child_spec);
590                lemma_repeat_parser_exec_inv::<&'i [u8], _, _>(&repeated);
591                lemma_repeat_parser_congruence(entry, Pair(child_spec, child_spec), BREAK, BREAK);
592                lemma_parser_congruent_apply(
593                    repeated,
594                    Repeat(Pair(child_spec, child_spec), BREAK),
595                    rest@,
596                );
597            }
598            let (content_len, (entries, _break)) = repeated.parse(&rest)?;
599            let value = CborValue::Map(entries);
600            proof {
601                super::value::lemma_collection_value_view(&value);
602            }
603            Ok((head_len + content_len, value))
604        },
605        CborHead { major: MajorType::Tag, value: CborHeadValue::Argument(tag) } => {
606            proof {
607                lemma_parser_congruent_apply(child, child_spec, rest@);
608            }
609            let (content_len, value) = child.parse(&rest)?;
610            Ok((head_len + content_len, CborValue::Tag(tag, Box::new(value))))
611        },
612        CborHead { major: MajorType::Simple, value: CborHeadValue::Float(value) } => {
613            Ok((head_len, CborValue::Float(value)))
614        },
615        CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(20) } => {
616            Ok((head_len, CborValue::Bool(false)))
617        },
618        CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(21) } => {
619            Ok((head_len, CborValue::Bool(true)))
620        },
621        CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(22) } => {
622            Ok((head_len, CborValue::Null))
623        },
624        CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(23) } => {
625            Ok((head_len, CborValue::Undefined))
626        },
627        CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(value) } => {
628            Ok((head_len, CborValue::Simple(value)))
629        },
630        _ => Err(ParseError::custom("invalid CBOR head/value combination")),
631    }
632}
633
634#[verifier::rlimit(50)]
635fn serialize_cbor_with_child<'i, Output, const DET: bool, Exec>(
636    Ghost(spec_rec): Ghost<ParamRecSpecs<(), CborValueSpec>>,
637    exec_rec: Exec,
638    value: &CborValue<'i>,
639    out: &mut Output,
640) where Output: OutputBuf, Exec: Fn(&(), &CborValue<'i>, &mut Output)
641    requires
642        cbor_body::<DET>(spec_rec).consistent(value.deep_view()),
643        old(out).fits(cbor_body::<DET>(spec_rec).byte_len(value.deep_view())),
644        forall|pp: &(), vv: &CborValue<'i>, output: &mut Output|
645            {
646                &&& spec_rec(pp.deep_view()).0(vv.deep_view())
647                &&& output.fits(spec_rec(pp.deep_view()).1(vv.deep_view()))
648            } ==> call_requires(exec_rec, (pp, vv, output)),
649        forall|pp: &(), vv: &CborValue<'i>, output: &mut Output|
650            call_ensures(exec_rec, (pp, vv, output), ()) ==> {
651                &&& final(output)@ == output@ + spec_rec(pp.deep_view()).3(vv.deep_view())
652                &&& forall|n|
653                    output.fits(spec_rec(pp.deep_view()).1(vv.deep_view()) + n)
654                        <==> #[trigger] final(output).fits(n)
655                &&& output.same_destination(final(output))
656            },
657    ensures
658        final(out)@ == old(out)@ + cbor_body::<DET>(spec_rec).spec_serialize(value.deep_view()),
659        forall|n|
660            old(out).fits(cbor_body::<DET>(spec_rec).byte_len(value.deep_view()) + n)
661                <==> #[trigger] final(out).fits(n),
662        old(out).same_destination(final(out)),
663{
664    use crate::combinators::congruence::*;
665    use crate::core::exec::bridge_lemmas::*;
666    broadcast use crate::core::exec::output::outbuf_lemmas;
667
668    reveal(<crate::combinators::Star<_> as Consistency>::consistent);
669    reveal(<crate::combinators::Star<_> as SpecByteLen>::byte_len);
670    reveal(<crate::combinators::Star<_> as SpecSerializer>::spec_serialize);
671
672    let ghost child_spec = spec_rec(());
673    let child_exec = |child_value: &CborValue<'i>, output: &mut Output| -> ()
674        requires
675            child_spec.consistent(child_value.deep_view()),
676            old(output).fits(child_spec.byte_len(child_value.deep_view())),
677        ensures
678            final(output)@ == old(output)@ + child_spec.spec_serialize(child_value.deep_view()),
679            forall|n|
680                old(output).fits(child_spec.byte_len(child_value.deep_view()) + n)
681                    <==> #[trigger] final(output).fits(n),
682            old(output).same_destination(final(output)),
683        { exec_rec(&(), child_value, output) };
684    let child: FnSerializer<Output, CborValue<'i>, BundledSpecs<CborValueSpec>, _> =
685        FnSerializer::new(child_exec, Ghost(child_spec));
686    proof {
687        lemma_ref_serializer_exec_inv::<Output, _, CborValue<'i>>(&child);
688        lemma_ref_fn_serializer_congruence(&child);
689    }
690
691    match value {
692        CborValue::Integer(integer) => {
693            let head = if *integer >= 0 {
694                CborHead {
695                    major: MajorType::Unsigned,
696                    value: CborHeadValue::Argument(*integer as u64),
697                }
698            } else {
699                CborHead {
700                    major: MajorType::Negative,
701                    value: CborHeadValue::Argument((-1i128 - *integer) as u64),
702                }
703            };
704            CborHeadFmt::<DET>.serialize_into(&head, out);
705        },
706        CborValue::Bytes(CborBytes::Definite(bytes)) => {
707            let head = CborHead {
708                major: MajorType::Bytes,
709                value: CborHeadValue::Argument(bytes.len() as u64),
710            };
711            CborHeadFmt::<DET>.serialize_into(&head, out);
712            Tail.serialize_into(bytes, out);
713        },
714        CborValue::Bytes(CborBytes::Indefinite(bytes)) => {
715            let head = CborHead {
716                major: MajorType::Bytes,
717                value: CborHeadValue::Argument(bytes.len() as u64),
718            };
719            CborHeadFmt::<DET>.serialize_into(&head, out);
720            Tail.serialize_into(bytes.as_slice(), out);
721        },
722        CborValue::Text(CborText::Definite(text)) => {
723            let head = CborHead {
724                major: MajorType::Text,
725                value: CborHeadValue::Argument(text.as_bytes().len() as u64),
726            };
727            CborHeadFmt::<DET>.serialize_into(&head, out);
728            Utf8StringFmt.serialize_into(text, out);
729        },
730        CborValue::Text(CborText::Indefinite(text)) => {
731            let head = CborHead {
732                major: MajorType::Text,
733                value: CborHeadValue::Argument(text.as_str().as_bytes().len() as u64),
734            };
735            CborHeadFmt::<DET>.serialize_into(&head, out);
736            Utf8StringFmt.serialize_into(text, out);
737        },
738        CborValue::Array(values) => {
739            proof {
740                super::value::lemma_collection_value_view(value);
741            }
742            let count = values.len();
743            let head = CborHead {
744                major: MajorType::Array,
745                value: CborHeadValue::Argument(count as u64),
746            };
747            CborHeadFmt::<DET>.serialize_into(&head, out);
748            let repeated = RepeatN(count as u64, &child);
749            let ghost repeated_spec = RepeatN(count as u64, child_spec);
750            proof {
751                lemma_repeat_n_serializer_exec_inv::<Output, _, _, CborValue<'i>>(&repeated);
752                lemma_repeat_n_serializer_congruence(repeated, repeated_spec);
753                lemma_serializer_congruent_prepare(repeated, repeated_spec);
754                lemma_prepare_congruent_consistent(repeated, repeated_spec, values.deep_view());
755                lemma_prepare_congruent_byte_len(repeated, repeated_spec, values.deep_view());
756                lemma_serializer_congruent_serialize(repeated, repeated_spec, values.deep_view());
757            }
758            repeated.serialize_into(values.as_slice(), out);
759        },
760        CborValue::Map(entries) => {
761            proof {
762                super::value::lemma_collection_value_view(value);
763            }
764            let count = entries.len();
765            let head = CborHead {
766                major: MajorType::Map,
767                value: CborHeadValue::Argument(count as u64),
768            };
769            CborHeadFmt::<DET>.serialize_into(&head, out);
770            let entry = Pair(&child, &child);
771            let ghost entry_spec = Pair(child_spec, child_spec);
772            let repeated = RepeatN(count as u64, entry);
773            let ghost repeated_spec = RepeatN(count as u64, entry_spec);
774            proof {
775                lemma_pair_serializer_congruence(entry, entry_spec);
776                lemma_pair_serializer_exec_inv::<Output, _, _, CborValue<'i>, CborValue<'i>>(
777                    &entry,
778                );
779                lemma_repeat_n_serializer_exec_inv::<Output, _, _, (CborValue<'i>, CborValue<'i>)>(
780                    &repeated,
781                );
782                lemma_repeat_n_serializer_congruence(repeated, repeated_spec);
783                lemma_serializer_congruent_prepare(repeated, repeated_spec);
784                lemma_prepare_congruent_consistent(repeated, repeated_spec, entries.deep_view());
785                lemma_prepare_congruent_byte_len(repeated, repeated_spec, entries.deep_view());
786                lemma_serializer_congruent_serialize(repeated, repeated_spec, entries.deep_view());
787            }
788            repeated.serialize_into(entries.as_slice(), out);
789        },
790        CborValue::Tag(tag, inner) => {
791            let head = CborHead { major: MajorType::Tag, value: CborHeadValue::Argument(*tag) };
792            proof {
793                assert(child_spec.consistent((**inner).deep_view()));
794                lemma_serializer_congruent_prepare(&child, child_spec);
795                lemma_prepare_congruent_consistent(&child, child_spec, (**inner).deep_view());
796                lemma_prepare_congruent_byte_len(&child, child_spec, (**inner).deep_view());
797                lemma_serializer_congruent_serialize(&child, child_spec, (**inner).deep_view());
798                lemma_fn_serializer_specs(&child, (**inner).deep_view());
799            }
800            CborHeadFmt::<DET>.serialize_into(&head, out);
801            child.serialize_into(&**inner, out);
802        },
803        CborValue::Float(float) => {
804            let head = CborHead { major: MajorType::Simple, value: CborHeadValue::Float(*float) };
805            CborHeadFmt::<DET>.serialize_into(&head, out);
806        },
807        CborValue::Bool(boolean) => {
808            let head = CborHead {
809                major: MajorType::Simple,
810                value: CborHeadValue::Simple(
811                    if *boolean {
812                        21
813                    } else {
814                        20
815                    },
816                ),
817            };
818            CborHeadFmt::<DET>.serialize_into(&head, out);
819        },
820        CborValue::Null => {
821            let head = CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(22) };
822            CborHeadFmt::<DET>.serialize_into(&head, out);
823        },
824        CborValue::Undefined => {
825            let head = CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(23) };
826            CborHeadFmt::<DET>.serialize_into(&head, out);
827        },
828        CborValue::Simple(simple) => {
829            let head = CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(*simple) };
830            CborHeadFmt::<DET>.serialize_into(&head, out);
831        },
832    }
833}
834
835fn checked_add_lengths(left: usize, right: usize) -> (result: Result<usize, PreSerializeError>)
836    ensures
837        result matches Ok(total) ==> total as nat == left as nat + right as nat,
838{
839    match left.checked_add(right) {
840        Some(total) => Ok(total),
841        None => Err(PreSerializeError::length_too_large()),
842    }
843}
844
845fn prepare_cbor_with_child<'i, const DET: bool, Exec>(
846    Ghost(spec_rec): Ghost<ParamRecSpecs<(), CborValueSpec>>,
847    exec_rec: Exec,
848    value: &CborValue<'i>,
849) -> (result: Result<usize, PreSerializeError>) where
850    Exec: Fn(&(), &CborValue<'i>) -> Result<usize, PreSerializeError>,
851
852    requires
853        forall|pp: &(), vv: &CborValue<'i>| call_requires(exec_rec, (pp, vv)),
854        forall|pp: &(), vv: &CborValue<'i>, rr: Result<usize, PreSerializeError>|
855            call_ensures(exec_rec, (pp, vv), rr) ==> (rr matches Ok(len) ==> {
856                &&& spec_rec(pp.deep_view()).0(vv.deep_view())
857                &&& len == spec_rec(pp.deep_view()).1(vv.deep_view())
858            }),
859    ensures
860        result matches Ok(len) ==> {
861            &&& cbor_body::<DET>(spec_rec).consistent(value.deep_view())
862            &&& len == cbor_body::<DET>(spec_rec).byte_len(value.deep_view())
863        },
864{
865    use crate::combinators::congruence::*;
866    use crate::core::exec::bridge_lemmas::*;
867
868    let ghost child_spec = spec_rec(());
869    let child_exec = |child_value: &CborValue<'i>| -> (child_result: Result<
870        usize,
871        PreSerializeError,
872    >)
873        ensures
874            child_result matches Ok(len) ==> {
875                &&& child_spec.consistent(child_value.deep_view())
876                &&& len == child_spec.byte_len(child_value.deep_view())
877            },
878        { exec_rec(&(), child_value) };
879    let child: FnPrepare<CborValue<'i>, BundledSpecs<CborValueSpec>, _> = FnPrepare::new(
880        child_exec,
881        Ghost(child_spec),
882    );
883    proof {
884        lemma_ref_prepare_exec_inv(&child);
885        lemma_ref_fn_prepare_congruence(&child);
886    }
887
888    match value {
889        CborValue::Integer(integer) => {
890            if *integer < -1i128 - u64::MAX as i128 || *integer > u64::MAX as i128 {
891                return Err(PreSerializeError::custom("CBOR integer is out of range"));
892            }
893            let head = if *integer >= 0 {
894                CborHead {
895                    major: MajorType::Unsigned,
896                    value: CborHeadValue::Argument(*integer as u64),
897                }
898            } else {
899                CborHead {
900                    major: MajorType::Negative,
901                    value: CborHeadValue::Argument((-1i128 - *integer) as u64),
902                }
903            };
904            CborHeadFmt::<DET>.prepare(&head)
905        },
906        CborValue::Bytes(CborBytes::Definite(bytes)) => {
907            let head = CborHead {
908                major: MajorType::Bytes,
909                value: CborHeadValue::Argument(bytes.len() as u64),
910            };
911            let head_len = CborHeadFmt::<DET>.prepare(&head)?;
912            let content_len = Tail.prepare(bytes)?;
913            checked_add_lengths(head_len, content_len)
914        },
915        CborValue::Bytes(CborBytes::Indefinite(bytes)) => {
916            let head = CborHead {
917                major: MajorType::Bytes,
918                value: CborHeadValue::Argument(bytes.len() as u64),
919            };
920            let head_len = CborHeadFmt::<DET>.prepare(&head)?;
921            let content_len = Tail.prepare(bytes.as_slice())?;
922            checked_add_lengths(head_len, content_len)
923        },
924        CborValue::Text(CborText::Definite(text)) => {
925            let head = CborHead {
926                major: MajorType::Text,
927                value: CborHeadValue::Argument(text.as_bytes().len() as u64),
928            };
929            let head_len = CborHeadFmt::<DET>.prepare(&head)?;
930            let content_len = Utf8StringFmt.prepare(text)?;
931            checked_add_lengths(head_len, content_len)
932        },
933        CborValue::Text(CborText::Indefinite(text)) => {
934            let head = CborHead {
935                major: MajorType::Text,
936                value: CborHeadValue::Argument(text.as_str().as_bytes().len() as u64),
937            };
938            let head_len = CborHeadFmt::<DET>.prepare(&head)?;
939            let content_len = Utf8StringFmt.prepare(text)?;
940            checked_add_lengths(head_len, content_len)
941        },
942        CborValue::Array(values) => {
943            proof {
944                super::value::lemma_collection_value_view(value);
945            }
946            let count = values.len();
947            let head = CborHead {
948                major: MajorType::Array,
949                value: CborHeadValue::Argument(count as u64),
950            };
951            let repeated = RepeatN(count as u64, &child);
952            let ghost repeated_spec = RepeatN(count as u64, child_spec);
953            proof {
954                lemma_repeat_n_prepare_exec_inv::<_, _, CborValue<'i>>(&repeated);
955                lemma_repeat_n_prepare_congruence(repeated, repeated_spec);
956            }
957            let head_len = CborHeadFmt::<DET>.prepare(&head)?;
958            let content_len = repeated.prepare(values.as_slice())?;
959            proof {
960                lemma_prepare_congruent_consistent(repeated, repeated_spec, values.deep_view());
961                lemma_prepare_congruent_byte_len(repeated, repeated_spec, values.deep_view());
962            }
963            checked_add_lengths(head_len, content_len)
964        },
965        CborValue::Map(entries) => {
966            proof {
967                super::value::lemma_collection_value_view(value);
968            }
969            let count = entries.len();
970            let head = CborHead {
971                major: MajorType::Map,
972                value: CborHeadValue::Argument(count as u64),
973            };
974            let entry = Pair(&child, &child);
975            let ghost entry_spec = Pair(child_spec, child_spec);
976            let repeated = RepeatN(count as u64, entry);
977            let ghost repeated_spec = RepeatN(count as u64, entry_spec);
978            proof {
979                lemma_pair_prepare_exec_inv::<_, _, CborValue<'i>, CborValue<'i>>(&entry);
980                lemma_pair_prepare_congruence(entry, entry_spec);
981                lemma_repeat_n_prepare_exec_inv::<_, _, (CborValue<'i>, CborValue<'i>)>(&repeated);
982                lemma_repeat_n_prepare_congruence(repeated, repeated_spec);
983            }
984            let head_len = CborHeadFmt::<DET>.prepare(&head)?;
985            let content_len = repeated.prepare(entries.as_slice())?;
986            proof {
987                lemma_prepare_congruent_consistent(repeated, repeated_spec, entries.deep_view());
988                lemma_prepare_congruent_byte_len(repeated, repeated_spec, entries.deep_view());
989            }
990            checked_add_lengths(head_len, content_len)
991        },
992        CborValue::Tag(tag, inner) => {
993            let head = CborHead { major: MajorType::Tag, value: CborHeadValue::Argument(*tag) };
994            let head_len = CborHeadFmt::<DET>.prepare(&head)?;
995            let content_len = child.prepare(&**inner)?;
996            proof {
997                lemma_prepare_congruent_consistent(&child, child_spec, (**inner).deep_view());
998                lemma_prepare_congruent_byte_len(&child, child_spec, (**inner).deep_view());
999                lemma_fn_prepare_specs(&child, (**inner).deep_view());
1000            }
1001            checked_add_lengths(head_len, content_len)
1002        },
1003        CborValue::Float(float) => CborHeadFmt::<DET>.prepare(
1004            &CborHead { major: MajorType::Simple, value: CborHeadValue::Float(*float) },
1005        ),
1006        CborValue::Bool(boolean) => CborHeadFmt::<DET>.prepare(
1007            &CborHead {
1008                major: MajorType::Simple,
1009                value: CborHeadValue::Simple(
1010                    if *boolean {
1011                        21
1012                    } else {
1013                        20
1014                    },
1015                ),
1016            },
1017        ),
1018        CborValue::Null => CborHeadFmt::<DET>.prepare(
1019            &CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(22) },
1020        ),
1021        CborValue::Undefined => CborHeadFmt::<DET>.prepare(
1022            &CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(23) },
1023        ),
1024        CborValue::Simple(simple) => {
1025            if *simple > 19 && *simple < 32 {
1026                Err(PreSerializeError::custom("reserved CBOR simple value"))
1027            } else {
1028                CborHeadFmt::<DET>.prepare(
1029                    &CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(*simple) },
1030                )
1031            }
1032        },
1033    }
1034}
1035
1036fn length_cbor_with_child<'i, const DET: bool, Exec>(
1037    Ghost(spec_rec): Ghost<ParamRecSpecs<(), CborValueSpec>>,
1038    exec_rec: Exec,
1039    value: &CborValue<'i>,
1040) -> (len: usize) where Exec: Fn(&(), &CborValue<'i>) -> usize
1041    requires
1042        cbor_body::<DET>(spec_rec).byte_len(value.deep_view()) <= usize::MAX,
1043        forall|pp: &(), vv: &CborValue<'i>|
1044            spec_rec(pp.deep_view()).1(vv.deep_view()) <= usize::MAX ==> call_requires(
1045                exec_rec,
1046                (pp, vv),
1047            ),
1048        forall|pp: &(), vv: &CborValue<'i>, child_len: usize|
1049            call_ensures(exec_rec, (pp, vv), child_len) ==> child_len == spec_rec(pp.deep_view()).1(
1050                vv.deep_view(),
1051            ),
1052    ensures
1053        len == cbor_body::<DET>(spec_rec).byte_len(value.deep_view()),
1054{
1055    use crate::combinators::congruence::*;
1056    use crate::core::exec::bridge_lemmas::*;
1057
1058    let ghost child_spec = spec_rec(());
1059    let child_exec = |child_value: &CborValue<'i>| -> (child_len: usize)
1060        requires
1061            child_spec.byte_len(child_value.deep_view()) <= usize::MAX,
1062        ensures
1063            child_len == child_spec.byte_len(child_value.deep_view()),
1064        { exec_rec(&(), child_value) };
1065    let child: FnByteLen<CborValue<'i>, BundledSpecs<CborValueSpec>, _> = FnByteLen::new(
1066        child_exec,
1067        Ghost(child_spec),
1068    );
1069    proof {
1070        lemma_ref_fn_byte_len_congruence(&child);
1071        lemma_ref_byte_len_exec_inv::<_, CborValue<'i>>(&child);
1072    }
1073
1074    match value {
1075        CborValue::Integer(integer) => {
1076            let head = if *integer >= 0 {
1077                CborHead {
1078                    major: MajorType::Unsigned,
1079                    value: CborHeadValue::Argument(*integer as u64),
1080                }
1081            } else {
1082                CborHead {
1083                    major: MajorType::Negative,
1084                    value: CborHeadValue::Argument((-1i128 - *integer) as u64),
1085                }
1086            };
1087            CborHeadFmt::<DET>.length(&head)
1088        },
1089        CborValue::Bytes(CborBytes::Definite(bytes)) => {
1090            let head = CborHead {
1091                major: MajorType::Bytes,
1092                value: CborHeadValue::Argument(bytes.len() as u64),
1093            };
1094            CborHeadFmt::<DET>.length(&head) + Tail.length(bytes)
1095        },
1096        CborValue::Bytes(CborBytes::Indefinite(bytes)) => {
1097            let head = CborHead {
1098                major: MajorType::Bytes,
1099                value: CborHeadValue::Argument(bytes.len() as u64),
1100            };
1101            CborHeadFmt::<DET>.length(&head) + Tail.length(bytes.as_slice())
1102        },
1103        CborValue::Text(CborText::Definite(text)) => {
1104            let head = CborHead {
1105                major: MajorType::Text,
1106                value: CborHeadValue::Argument(text.as_bytes().len() as u64),
1107            };
1108            CborHeadFmt::<DET>.length(&head) + Utf8StringFmt.length(text)
1109        },
1110        CborValue::Text(CborText::Indefinite(text)) => {
1111            let head = CborHead {
1112                major: MajorType::Text,
1113                value: CborHeadValue::Argument(text.as_str().as_bytes().len() as u64),
1114            };
1115            CborHeadFmt::<DET>.length(&head) + Utf8StringFmt.length(text)
1116        },
1117        CborValue::Array(values) => {
1118            proof {
1119                super::value::lemma_collection_value_view(value);
1120            }
1121            let count = values.len();
1122            let head = CborHead {
1123                major: MajorType::Array,
1124                value: CborHeadValue::Argument(count as u64),
1125            };
1126            let repeated = RepeatN(count as u64, &child);
1127            let ghost repeated_spec = RepeatN(count as u64, child_spec);
1128            proof {
1129                lemma_repeat_n_prepare_congruence(repeated, repeated_spec);
1130                lemma_prepare_congruent_byte_len(repeated, repeated_spec, values.deep_view());
1131                lemma_repeat_n_byte_len_exec_inv::<_, _, CborValue<'i>>(&repeated);
1132            }
1133            CborHeadFmt::<DET>.length(&head) + repeated.length(values.as_slice())
1134        },
1135        CborValue::Map(entries) => {
1136            proof {
1137                super::value::lemma_collection_value_view(value);
1138            }
1139            let count = entries.len();
1140            let head = CborHead {
1141                major: MajorType::Map,
1142                value: CborHeadValue::Argument(count as u64),
1143            };
1144            let entry = Pair(&child, &child);
1145            let ghost entry_spec = Pair(child_spec, child_spec);
1146            let repeated = RepeatN(count as u64, entry);
1147            let ghost repeated_spec = RepeatN(count as u64, entry_spec);
1148            proof {
1149                lemma_pair_prepare_congruence(entry, entry_spec);
1150                lemma_repeat_n_prepare_congruence(repeated, repeated_spec);
1151                lemma_prepare_congruent_byte_len(repeated, repeated_spec, entries.deep_view());
1152                lemma_pair_byte_len_exec_inv::<_, _, CborValue<'i>, CborValue<'i>>(&entry);
1153                lemma_repeat_n_byte_len_exec_inv::<_, _, (CborValue<'i>, CborValue<'i>)>(&repeated);
1154            }
1155            CborHeadFmt::<DET>.length(&head) + repeated.length(entries.as_slice())
1156        },
1157        CborValue::Tag(tag, inner) => {
1158            proof {
1159                lemma_prepare_congruent_byte_len(&child, child_spec, (**inner).deep_view());
1160                lemma_fn_byte_len_specs(&child, (**inner).deep_view());
1161            }
1162            let head = CborHead { major: MajorType::Tag, value: CborHeadValue::Argument(*tag) };
1163            CborHeadFmt::<DET>.length(&head) + child.length(&**inner)
1164        },
1165        CborValue::Float(float) => CborHeadFmt::<DET>.length(
1166            &CborHead { major: MajorType::Simple, value: CborHeadValue::Float(*float) },
1167        ),
1168        CborValue::Bool(boolean) => CborHeadFmt::<DET>.length(
1169            &CborHead {
1170                major: MajorType::Simple,
1171                value: CborHeadValue::Simple(
1172                    if *boolean {
1173                        21
1174                    } else {
1175                        20
1176                    },
1177                ),
1178            },
1179        ),
1180        CborValue::Null => CborHeadFmt::<DET>.length(
1181            &CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(22) },
1182        ),
1183        CborValue::Undefined => CborHeadFmt::<DET>.length(
1184            &CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(23) },
1185        ),
1186        CborValue::Simple(simple) => CborHeadFmt::<DET>.length(
1187            &CborHead { major: MajorType::Simple, value: CborHeadValue::Simple(*simple) },
1188        ),
1189    }
1190}
1191
1192fn cbor_length_gas<'i, const DET: bool, const LIMIT: usize>(
1193    gas: usize,
1194    value: &CborValue<'i>,
1195) -> (len: usize)
1196    requires
1197        FixWith::<LIMIT, CborRecBody<DET>, ()>::byte_len_gas(
1198            &CborRecBody::<DET>,
1199            gas as nat,
1200            (),
1201            value.deep_view(),
1202        ) <= usize::MAX,
1203    ensures
1204        len == FixWith::<LIMIT, CborRecBody<DET>, ()>::byte_len_gas(
1205            &CborRecBody::<DET>,
1206            gas as nat,
1207            (),
1208            value.deep_view(),
1209        ),
1210    decreases gas,
1211{
1212    let ghost body = CborRecBody::<DET>;
1213    let ghost spec_rec = FixWith::<LIMIT, CborRecBody<DET>, ()>::specs_callback(&body, gas as nat);
1214    let exec_rec = |_param: &(), child: &CborValue<'i>| -> (child_len: usize)
1215        requires
1216            spec_rec(()).byte_len(child.deep_view()) <= usize::MAX,
1217        ensures
1218            child_len == spec_rec(()).byte_len(child.deep_view()),
1219        {
1220            if gas > 0 {
1221                cbor_length_gas::<DET, LIMIT>((gas - 1) as usize, child)
1222            } else {
1223                0
1224            }
1225        };
1226    length_cbor_with_child::<DET, _>(Ghost(spec_rec), exec_rec, value)
1227}
1228
1229fn parse_cbor_rec_body<'i, const DET: bool, Exec>(
1230    param: &(),
1231    Ghost(spec_rec): Ghost<ParamRecSpecs<(), CborValueSpec>>,
1232    exec_rec: Exec,
1233    input: &&'i [u8],
1234) -> (result: PResult<CborValue<'i>>) where Exec: Fn(&(), &&'i [u8]) -> PResult<CborValue<'i>>
1235    requires
1236        forall|p: ()| #[trigger] spec_rec(p).safe_inv(),
1237        forall|p: ()| #[trigger] spec_rec(p).productive_inv(),
1238        forall|pp: &(), i: &&'i [u8]| call_requires(exec_rec, (pp, i)),
1239        forall|pp: &(), i: &&'i [u8], rr: PResult<CborValue<'i>>|
1240            call_ensures(exec_rec, (pp, i), rr) ==> parse_matches_spec(
1241                rr,
1242                spec_rec(pp.deep_view()).2(i@),
1243            ),
1244    ensures
1245        parse_matches_spec(result, cbor_body::<DET>(spec_rec).spec_parse(input@)),
1246{
1247    let ghost child_spec = spec_rec(());
1248    let child_exec = |child_input: &&'i [u8]| -> (result: PResult<CborValue<'i>>)
1249        ensures
1250            parse_matches_spec(result, child_spec.2(child_input@)),
1251        { exec_rec(param, child_input) };
1252    let child: FnParser<&'i [u8], CborValue<'i>, BundledSpecs<CborValueSpec>, _> = FnParser::new(
1253        child_exec,
1254        Ghost(child_spec),
1255    );
1256    proof {
1257        crate::combinators::congruence::lemma_ref_fn_parser_congruence(&child);
1258    }
1259    parse_cbor_with_child::<DET, _>(Ghost(spec_rec), &child, input)
1260}
1261
1262// Verus currently loses the inherited higher-order `Exec` contract on a const-generic
1263// `ParserRecBody` impl. Keep only these mode-specific trait shims; all logic remains in the
1264// const-generic helper above.
1265impl<'i> ParserRecBody<&'i [u8]> for CborRecBody<false> where
1266    CborRecBody<false>: SpecRecBody<Param = (), T = CborValueSpec, Body = CborBodyFmt<false>>,
1267 {
1268    type EP = ();
1269
1270    type O = CborValue<'i>;
1271
1272    fn parse_body<Exec>(
1273        &self,
1274        param: &(),
1275        spec_rec: Ghost<ParamRecSpecs<(), CborValueSpec>>,
1276        exec_rec: Exec,
1277        input: &&'i [u8],
1278    ) -> PResult<Self::O> where Exec: Fn(&(), &&'i [u8]) -> PResult<Self::O> {
1279        parse_cbor_rec_body::<false, _>(param, spec_rec, exec_rec, input)
1280    }
1281}
1282
1283impl<'i> ParserRecBody<&'i [u8]> for CborRecBody<true> where
1284    CborRecBody<true>: SpecRecBody<Param = (), T = CborValueSpec, Body = CborBodyFmt<true>>,
1285 {
1286    type EP = ();
1287
1288    type O = CborValue<'i>;
1289
1290    fn parse_body<Exec>(
1291        &self,
1292        param: &(),
1293        spec_rec: Ghost<ParamRecSpecs<(), CborValueSpec>>,
1294        exec_rec: Exec,
1295        input: &&'i [u8],
1296    ) -> PResult<Self::O> where Exec: Fn(&(), &&'i [u8]) -> PResult<Self::O> {
1297        parse_cbor_rec_body::<true, _>(param, spec_rec, exec_rec, input)
1298    }
1299}
1300
1301impl<'i, Output: OutputBuf, const DET: bool> SerializerRecBody<
1302    Output,
1303    CborValue<'i>,
1304> for CborRecBody<DET> {
1305    type EP = ();
1306
1307    fn serialize_body<Exec>(
1308        &self,
1309        _param: &(),
1310        Ghost(spec_rec): Ghost<ParamRecSpecs<(), CborValueSpec>>,
1311        exec_rec: Exec,
1312        value: &CborValue<'i>,
1313        out: &mut Output,
1314    ) where Exec: Fn(&(), &CborValue<'i>, &mut Output) {
1315        serialize_cbor_with_child::<Output, DET, _>(Ghost(spec_rec), exec_rec, value, out)
1316    }
1317}
1318
1319// The corresponding const-generic `PrepareRecBody` impl has the same Verus callback-contract
1320// limitation. Both shims delegate to `prepare_cbor_with_child`.
1321impl<'i> PrepareRecBody<CborValue<'i>> for CborRecBody<false> where
1322    CborRecBody<false>: SpecRecBody<Param = (), T = CborValueSpec, Body = CborBodyFmt<false>>,
1323 {
1324    type EP = ();
1325
1326    fn prepare_body<Exec>(
1327        &self,
1328        _param: &(),
1329        spec_rec: Ghost<ParamRecSpecs<(), CborValueSpec>>,
1330        exec_rec: Exec,
1331        value: &CborValue<'i>,
1332    ) -> Result<usize, PreSerializeError> where
1333        Exec: Fn(&(), &CborValue<'i>) -> Result<usize, PreSerializeError>,
1334     {
1335        prepare_cbor_with_child::<false, _>(spec_rec, exec_rec, value)
1336    }
1337}
1338
1339impl<'i> PrepareRecBody<CborValue<'i>> for CborRecBody<true> where
1340    CborRecBody<true>: SpecRecBody<Param = (), T = CborValueSpec, Body = CborBodyFmt<true>>,
1341 {
1342    type EP = ();
1343
1344    fn prepare_body<Exec>(
1345        &self,
1346        _param: &(),
1347        spec_rec: Ghost<ParamRecSpecs<(), CborValueSpec>>,
1348        exec_rec: Exec,
1349        value: &CborValue<'i>,
1350    ) -> Result<usize, PreSerializeError> where
1351        Exec: Fn(&(), &CborValue<'i>) -> Result<usize, PreSerializeError>,
1352     {
1353        prepare_cbor_with_child::<true, _>(spec_rec, exec_rec, value)
1354    }
1355}
1356
1357/// A complete generic CBOR data item with bounded nesting.
1358#[derive(Clone, Copy)]
1359pub struct CborFmt<const DET: bool, const LIMIT: usize = MAX_RECURSION_DEPTH>;
1360
1361pub open spec fn cbor_fmt<const DET: bool, const LIMIT: usize>() -> FixWith<
1362    LIMIT,
1363    CborRecBody<DET>,
1364    (),
1365> {
1366    FixWith(CborRecBody::<DET>, ())
1367}
1368
1369impl<'i, const DET: bool, const LIMIT: usize> Parser<&'i [u8]> for CborFmt<DET, LIMIT> where
1370    CborRecBody<DET>: SpecRecBody<
1371        Param = (),
1372        T = CborValueSpec,
1373        Body = CborBodyFmt<DET>,
1374    > + ParserRecBody<&'i [u8], EP = (), O = CborValue<'i>>,
1375    <CborRecBody<DET> as SpecRecBody>::Body: Productive,
1376 {
1377    type PT = CborValue<'i>;
1378
1379    fn parse(&self, input: &&'i [u8]) -> PResult<Self::PT> {
1380        FixWith::<LIMIT, _, _>(CborRecBody::<DET>, ()).parse(input)
1381    }
1382}
1383
1384impl<'i, Output: OutputBuf, const DET: bool, const LIMIT: usize> Serializer<
1385    Output,
1386    CborValue<'i>,
1387> for CborFmt<DET, LIMIT> {
1388    fn serialize_into(&self, value: &CborValue<'i>, out: &mut Output) {
1389        FixWith::<LIMIT, _, _>(CborRecBody::<DET>, ()).serialize_into(value, out)
1390    }
1391}
1392
1393impl<'i, const DET: bool, const LIMIT: usize> Prepare<CborValue<'i>> for CborFmt<DET, LIMIT> where
1394    CborRecBody<DET>: SpecRecBody<
1395        Param = (),
1396        T = CborValueSpec,
1397        Body = CborBodyFmt<DET>,
1398    > + PrepareRecBody<CborValue<'i>, EP = ()>,
1399 {
1400    fn prepare(&self, value: &CborValue<'i>) -> Result<usize, PreSerializeError> {
1401        FixWith::<LIMIT, _, _>(CborRecBody::<DET>, ()).prepare(value)
1402    }
1403}
1404
1405impl<'i, const DET: bool, const LIMIT: usize> ByteLen<CborValue<'i>> for CborFmt<DET, LIMIT> {
1406    fn length(&self, value: &CborValue<'i>) -> usize {
1407        cbor_length_gas::<DET, LIMIT>(LIMIT, value)
1408    }
1409}
1410
1411mod derived_specs {
1412    use super::*;
1413
1414    impl<const DET: bool> SpecParser for CborBodyFmt<DET> {
1415        type PVal = CborValueSpec;
1416
1417        open spec fn spec_parse(&self, input: Seq<u8>) -> Option<(int, Self::PVal)> {
1418            cbor_parse_body::<DET>(self.rec@).spec_parse(input)
1419        }
1420    }
1421
1422    impl<const DET: bool> Consistency for CborBodyFmt<DET> {
1423        type Val = CborValueSpec;
1424
1425        open spec fn consistent(&self, value: Self::Val) -> bool {
1426            cbor_normalized_body::<DET>(self.rec@).consistent(value)
1427        }
1428    }
1429
1430    impl<const DET: bool> SpecSerializerDps for CborBodyFmt<DET> {
1431        type SValue = CborValueSpec;
1432
1433        open spec fn spec_serialize_dps(&self, value: Self::SValue, out: Seq<u8>) -> Seq<u8> {
1434            cbor_normalized_body::<DET>(self.rec@).spec_serialize_dps(value, out)
1435        }
1436    }
1437
1438    impl<const DET: bool> SpecSerializer for CborBodyFmt<DET> {
1439        type SVal = CborValueSpec;
1440
1441        open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8> {
1442            cbor_normalized_body::<DET>(self.rec@).spec_serialize(value)
1443        }
1444    }
1445
1446    impl<const DET: bool> SpecByteLen for CborBodyFmt<DET> {
1447        type T = CborValueSpec;
1448
1449        open spec fn byte_len(&self, value: Self::T) -> nat {
1450            cbor_normalized_body::<DET>(self.rec@).byte_len(value)
1451        }
1452    }
1453
1454    impl<const DET: bool, const LIMIT: usize> SpecParser for CborFmt<DET, LIMIT> {
1455        type PVal = CborValueSpec;
1456
1457        open spec fn spec_parse(&self, input: Seq<u8>) -> Option<(int, Self::PVal)> {
1458            cbor_fmt::<DET, LIMIT>().spec_parse(input)
1459        }
1460    }
1461
1462    impl<const DET: bool, const LIMIT: usize> Consistency for CborFmt<DET, LIMIT> {
1463        type Val = CborValueSpec;
1464
1465        open spec fn consistent(&self, value: Self::Val) -> bool {
1466            cbor_fmt::<DET, LIMIT>().consistent(value)
1467        }
1468    }
1469
1470    impl<const DET: bool, const LIMIT: usize> SpecSerializerDps for CborFmt<DET, LIMIT> {
1471        type SValue = CborValueSpec;
1472
1473        open spec fn spec_serialize_dps(&self, value: Self::SValue, out: Seq<u8>) -> Seq<u8> {
1474            cbor_fmt::<DET, LIMIT>().spec_serialize_dps(value, out)
1475        }
1476    }
1477
1478    impl<const DET: bool, const LIMIT: usize> SpecSerializer for CborFmt<DET, LIMIT> {
1479        type SVal = CborValueSpec;
1480
1481        open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8> {
1482            cbor_fmt::<DET, LIMIT>().spec_serialize(value)
1483        }
1484    }
1485
1486    impl<const DET: bool, const LIMIT: usize> SpecByteLen for CborFmt<DET, LIMIT> {
1487        type T = CborValueSpec;
1488
1489        open spec fn byte_len(&self, value: Self::T) -> nat {
1490            cbor_fmt::<DET, LIMIT>().byte_len(value)
1491        }
1492    }
1493
1494}
1495
1496mod recursive_proofs {
1497    use super::*;
1498
1499    impl<const DET: bool> SafeParserRecBody for CborRecBody<DET> {
1500        proof fn lemma_body_safe_inv_preservation(
1501            &self,
1502            _param: (),
1503            _rec: ParamRecSpecs<(), CborValueSpec>,
1504        ) {
1505        }
1506    }
1507
1508    impl<const DET: bool> ProductiveRecBody for CborRecBody<DET> {
1509        proof fn lemma_body_productive_inv_preservation(
1510            &self,
1511            _param: (),
1512            _rec: ParamRecSpecs<(), CborValueSpec>,
1513        ) {
1514        }
1515    }
1516
1517    impl SoundParserRecBody for CborRecBody<true> {
1518        proof fn lemma_body_sound_inv_preservation(
1519            &self,
1520            _param: (),
1521            _rec: ParamRecSpecs<(), CborValueSpec>,
1522        ) {
1523        }
1524    }
1525
1526    impl NonMalleableRecBody for CborRecBody<true> {
1527        proof fn lemma_body_nonmal_inv_preservation(
1528            &self,
1529            _param: (),
1530            _rec: ParamRecSpecs<(), CborValueSpec>,
1531        ) {
1532        }
1533    }
1534
1535    impl<const DET: bool> GoodSerializerRecBody for CborRecBody<DET> {
1536        proof fn lemma_s_body_serialize_inv_preservation(
1537            &self,
1538            _param: (),
1539            _rec: ParamRecSpecs<(), CborValueSpec>,
1540        ) {
1541        }
1542    }
1543
1544    impl<const DET: bool> NonTailFmtRecBody for CborRecBody<DET> {
1545        proof fn lemma_s_body_dps_serialize_dps_inv_preservation(
1546            &self,
1547            _param: (),
1548            _rec: ParamRecSpecs<(), CborValueSpec>,
1549        ) {
1550        }
1551    }
1552
1553    impl<const DET: bool> SPRoundTripDpsRecBody for CborRecBody<DET> {
1554        proof fn lemma_body_sp_roundtrip_dps_inv_preservation(
1555            &self,
1556            _param: (),
1557            _rec: ParamRecSpecs<(), CborValueSpec>,
1558        ) {
1559        }
1560    }
1561
1562    impl<const DET: bool> EquivSerializersGeneralRecBody for CborRecBody<DET> {
1563        proof fn lemma_s_body_equiv_general_inv_preservation(
1564            &self,
1565            _param: (),
1566            _rec: ParamRecSpecs<(), CborValueSpec>,
1567        ) {
1568        }
1569    }
1570
1571}
1572
1573mod derived_proofs {
1574    use super::*;
1575
1576    impl<const DET: bool> SafeParser for CborBodyFmt<DET> {
1577        open spec fn safe_inv(&self) -> bool {
1578            cbor_parse_body::<DET>(self.rec@).safe_inv()
1579        }
1580
1581        proof fn lemma_parse_safe(&self, input: Seq<u8>) {
1582            cbor_parse_body::<DET>(self.rec@).lemma_parse_safe(input);
1583        }
1584    }
1585
1586    impl<const DET: bool> Productive for CborBodyFmt<DET> {
1587        open spec fn productive_inv(&self) -> bool {
1588            cbor_parse_body::<DET>(self.rec@).productive_inv()
1589        }
1590
1591        proof fn lemma_productive(&self, input: Seq<u8>) {
1592            cbor_parse_body::<DET>(self.rec@).lemma_productive(input);
1593        }
1594    }
1595
1596    impl SoundParser for CborBodyFmt<true> {
1597        open spec fn sound_inv(&self) -> bool {
1598            cbor_parse_body::<true>(self.rec@).sound_inv()
1599        }
1600
1601        proof fn lemma_parse_sound_consumption(&self, input: Seq<u8>) {
1602            cbor_parse_body::<true>(self.rec@).lemma_parse_sound_consumption(input);
1603            if let Some((_n, value)) = self.spec_parse(input) {
1604                lemma_parse_normalized_byte_len::<true>(self.rec@, value);
1605            }
1606        }
1607
1608        proof fn lemma_parse_sound_value(&self, input: Seq<u8>) {
1609            cbor_parse_body::<true>(self.rec@).lemma_parse_sound_value(input);
1610            if let Some((_n, value)) = self.spec_parse(input) {
1611                lemma_parse_normalized_consistency::<true>(self.rec@, value);
1612            }
1613        }
1614    }
1615
1616    impl<const DET: bool> GoodSerializer for CborBodyFmt<DET> {
1617        open spec fn serialize_inv(&self) -> bool {
1618            cbor_normalized_body::<DET>(self.rec@).serialize_inv()
1619        }
1620
1621        proof fn lemma_serialize_len(&self, value: Self::SVal) {
1622            cbor_normalized_body::<DET>(self.rec@).lemma_serialize_len(value);
1623        }
1624    }
1625
1626    impl<const DET: bool> NonTailFmt for CborBodyFmt<DET> {
1627        open spec fn serialize_dps_inv(&self) -> bool {
1628            cbor_normalized_body::<DET>(self.rec@).serialize_dps_inv()
1629        }
1630
1631        proof fn lemma_serialize_dps_prepend(&self, value: Self::SValue, out: Seq<u8>) {
1632            cbor_normalized_body::<DET>(self.rec@).lemma_serialize_dps_prepend(value, out);
1633        }
1634
1635        proof fn lemma_serialize_dps_len(&self, value: Self::SValue, out: Seq<u8>) {
1636            cbor_normalized_body::<DET>(self.rec@).lemma_serialize_dps_len(value, out);
1637        }
1638    }
1639
1640    impl<const DET: bool> SPRoundTripDps for CborBodyFmt<DET> {
1641        open spec fn unambiguous(&self) -> bool {
1642            cbor_normalized_body::<DET>(self.rec@).unambiguous()
1643        }
1644
1645        proof fn theorem_serialize_dps_parse_roundtrip(&self, value: Self::T, out: Seq<u8>) {
1646            let normalized = cbor_normalized_body::<DET>(self.rec@);
1647            normalized.theorem_serialize_dps_parse_roundtrip(value, out);
1648            lemma_normalized_parse_implies_parse::<DET>(
1649                self.rec@,
1650                normalized.spec_serialize_dps(value, out),
1651            );
1652        }
1653    }
1654
1655    impl NonMalleable for CborBodyFmt<true> {
1656        open spec fn nonmal_inv(&self) -> bool {
1657            cbor_parse_body::<true>(self.rec@).nonmal_inv()
1658        }
1659
1660        proof fn lemma_parse_non_malleable(&self, left: Seq<u8>, right: Seq<u8>) {
1661            cbor_parse_body::<true>(self.rec@).lemma_parse_non_malleable(left, right);
1662        }
1663    }
1664
1665    impl<const DET: bool> EquivSerializersGeneral for CborBodyFmt<DET> {
1666        open spec fn equiv_general_inv(&self) -> bool {
1667            cbor_normalized_body::<DET>(self.rec@).equiv_general_inv()
1668        }
1669
1670        proof fn lemma_serialize_equiv(&self, value: Self::SVal, out: Seq<u8>) {
1671            cbor_normalized_body::<DET>(self.rec@).lemma_serialize_equiv(value, out);
1672        }
1673    }
1674
1675    impl<const DET: bool> EquivSerializers for CborBodyFmt<DET> {
1676        open spec fn equiv_inv(&self) -> bool {
1677            cbor_normalized_body::<DET>(self.rec@).equiv_inv()
1678        }
1679
1680        proof fn lemma_serialize_equiv_on_empty(&self, value: Self::SVal) {
1681            cbor_normalized_body::<DET>(self.rec@).lemma_serialize_equiv_on_empty(value);
1682        }
1683    }
1684
1685    impl<const DET: bool, const LIMIT: usize> SafeParser for CborFmt<DET, LIMIT> {
1686        proof fn lemma_parse_safe(&self, input: Seq<u8>) {
1687            cbor_fmt::<DET, LIMIT>().lemma_parse_safe(input);
1688        }
1689    }
1690
1691    impl<const DET: bool, const LIMIT: usize> Productive for CborFmt<DET, LIMIT> {
1692        proof fn lemma_productive(&self, input: Seq<u8>) {
1693            cbor_fmt::<DET, LIMIT>().lemma_productive(input);
1694        }
1695    }
1696
1697    impl<const LIMIT: usize> SoundParser for CborFmt<true, LIMIT> {
1698        proof fn lemma_parse_sound_consumption(&self, input: Seq<u8>) {
1699            cbor_fmt::<true, LIMIT>().lemma_parse_sound_consumption(input);
1700        }
1701
1702        proof fn lemma_parse_sound_value(&self, input: Seq<u8>) {
1703            cbor_fmt::<true, LIMIT>().lemma_parse_sound_value(input);
1704        }
1705    }
1706
1707    impl<const DET: bool, const LIMIT: usize> GoodSerializer for CborFmt<DET, LIMIT> {
1708        proof fn lemma_serialize_len(&self, value: Self::SVal) {
1709            cbor_fmt::<DET, LIMIT>().lemma_serialize_len(value);
1710        }
1711    }
1712
1713    impl<const DET: bool, const LIMIT: usize> NonTailFmt for CborFmt<DET, LIMIT> {
1714        proof fn lemma_serialize_dps_prepend(&self, value: Self::SValue, out: Seq<u8>) {
1715            cbor_fmt::<DET, LIMIT>().lemma_serialize_dps_prepend(value, out);
1716        }
1717
1718        proof fn lemma_serialize_dps_len(&self, value: Self::SValue, out: Seq<u8>) {
1719            cbor_fmt::<DET, LIMIT>().lemma_serialize_dps_len(value, out);
1720        }
1721    }
1722
1723    impl<const DET: bool, const LIMIT: usize> SPRoundTripDps for CborFmt<DET, LIMIT> {
1724        proof fn theorem_serialize_dps_parse_roundtrip(&self, value: Self::T, out: Seq<u8>) {
1725            cbor_fmt::<DET, LIMIT>().theorem_serialize_dps_parse_roundtrip(value, out);
1726        }
1727    }
1728
1729    impl<const LIMIT: usize> NonMalleable for CborFmt<true, LIMIT> {
1730        proof fn lemma_parse_non_malleable(&self, left: Seq<u8>, right: Seq<u8>) {
1731            cbor_fmt::<true, LIMIT>().lemma_parse_non_malleable(left, right);
1732        }
1733    }
1734
1735    impl<const DET: bool, const LIMIT: usize> EquivSerializersGeneral for CborFmt<DET, LIMIT> {
1736        proof fn lemma_serialize_equiv(&self, value: Self::SVal, out: Seq<u8>) {
1737            cbor_fmt::<DET, LIMIT>().lemma_serialize_equiv(value, out);
1738        }
1739    }
1740
1741    impl<const DET: bool, const LIMIT: usize> EquivSerializers for CborFmt<DET, LIMIT> {
1742        proof fn lemma_serialize_equiv_on_empty(&self, value: Self::SVal) {
1743            cbor_fmt::<DET, LIMIT>().lemma_serialize_equiv_on_empty(value);
1744        }
1745    }
1746
1747}
1748
1749} // verus!
vest_lib/cbor/format.rs

vest_lib/cbor/
format.rs
