vest_lib/combinators/preceded/
proof.rs

1//! Correctness proofs for sequential formats discarding their prefix.
2use super::spec::*;
3use crate::{
4    combinators::{mapped::spec::*, Mapped, Pair, Refined, TryMap},
5    core::{proof::*, spec::*},
6};
7use vstd::prelude::*;
8
9verus! {
10
11impl<A, B, const CHECK: bool> SPRoundTripDps for super::Preceded<A, A::SValue, B, CHECK> where
12    A: SPRoundTripDps + NonTailFmt,
13    B: SPRoundTripDps,
14 {
15    open spec fn unambiguous(&self) -> bool {
16        // We know that the `BiMap(|pair: (A, B)| pair.1, |b| (a_val, b))` in `preceded` is always sound (the unambiguous condition
17        // required by `Mapped<Inner, BiMap<M, MRev>>`).
18        // As a result, the unambiguity is equivalent to the unambiguity of the underlying `Pair`.
19        Pair(self.a, self.b).unambiguous()
20    }
21
22    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
23        let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
24        fmt.theorem_serialize_dps_parse_roundtrip(v, obuf);
25    }
26}
27
28impl<A, B> NonMalleable for super::Preceded<A, A::PVal, B, true> where
29    A: SoundParser + NonMalleable,
30    B: SoundParser + NonMalleable,
31 {
32    open spec fn nonmal_inv(&self) -> bool {
33        // When CHECK is true, we check that the value parsed by A is exactly a_val, making the `BiMap` `lossless` (the nonmal_inv condition
34        // required by `Mapped<Inner, BiMap<M, MRev>>`).
35        // As a result, `nonmal_inv` for `Mapped<Inner, BiMap<M, MRev>>` holds as long as `nonmal_inv` for `Inner` holds.
36        &&& Pair(self.a, self.b).sound_inv()
37        &&& Pair(self.a, self.b).nonmal_inv()
38    }
39
40    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
41        let fmt = preceded::<_, _, _, _, true>(self.a, self.b, self.a_val);
42        fmt.lemma_parse_non_malleable(buf1, buf2);
43    }
44}
45
46impl<A, B> NonMalleable for super::Preceded<A, A::PVal, B, false> where
47    A: SoundParser + NonMalleable + AdmitsUniqueVal,
48    B: SoundParser + NonMalleable,
49 {
50    open spec fn nonmal_inv(&self) -> bool {
51        &&& Pair(self.a, self.b).sound_inv()
52        &&& Pair(self.a, self.b).nonmal_inv()
53    }
54
55    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
56        let pair = Pair(self.a, self.b);
57        if let Some((n1, v1)) = self.spec_parse(buf1) {
58            if let Some((n2, v2)) = self.spec_parse(buf2) {
59                if v1 == v2 {
60                    let (_m1, p1) = pair.spec_parse(buf1)->0;
61                    let (_m2, p2) = pair.spec_parse(buf2)->0;
62                    pair.lemma_parse_sound_value(buf1);
63                    pair.lemma_parse_sound_value(buf2);
64                    self.a.lemma_unique_consistent_val(p1.0, p2.0);
65                    pair.lemma_parse_non_malleable(buf1, buf2);
66                }
67            }
68        }
69    }
70}
71
72impl<A, B, const CHECK: bool> NoLookAhead for super::Preceded<A, A::PVal, B, CHECK> where
73    A: NoLookAhead,
74    B: NoLookAhead,
75 {
76    open spec fn no_lookahead_inv(&self) -> bool {
77        let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
78        fmt.no_lookahead_inv()
79    }
80
81    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
82        let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
83        fmt.lemma_no_lookahead(i1, i2);
84    }
85}
86
87impl<A, B> Productive for super::Preceded<A, A::PVal, B, true> where A: Productive, B: Productive {
88    open spec fn productive_inv(&self) -> bool {
89        preceded::<_, _, _, _, true>(self.a, self.b, self.a_val).productive_inv()
90    }
91
92    proof fn lemma_productive(&self, s: Seq<u8>) {
93        preceded::<_, _, _, _, true>(self.a, self.b, self.a_val).lemma_productive(s);
94    }
95}
96
97impl<A, B> Productive for super::Preceded<A, A::PVal, B, false> where A: Productive, B: Productive {
98    open spec fn productive_inv(&self) -> bool {
99        preceded::<_, _, _, _, false>(self.a, self.b, self.a_val).productive_inv()
100    }
101
102    proof fn lemma_productive(&self, s: Seq<u8>) {
103        preceded::<_, _, _, _, false>(self.a, self.b, self.a_val).lemma_productive(s);
104    }
105}
106
107impl<A, B, const CHECK: bool> EquivSerializersGeneral for super::Preceded<
108    A,
109    A::SValue,
110    B,
111    CHECK,
112> where A: EquivSerializersGeneral + Consistency<Val = A::SVal>, B: EquivSerializersGeneral {
113    open spec fn equiv_general_inv(&self) -> bool {
114        let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
115        fmt.equiv_general_inv()
116    }
117
118    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
119        let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
120        fmt.lemma_serialize_equiv(v, obuf);
121    }
122}
123
124impl<A, B, const CHECK: bool> EquivSerializers for super::Preceded<A, A::SValue, B, CHECK> where
125    A: EquivSerializersGeneral + Consistency<Val = A::SVal>,
126    B: EquivSerializers,
127 {
128    open spec fn equiv_inv(&self) -> bool {
129        let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
130        fmt.equiv_inv()
131    }
132
133    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
134        let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
135        fmt.lemma_serialize_equiv_on_empty(v);
136    }
137}
138
139} // verus!
vest_lib/combinators/preceded/proof.rs

vest_lib/combinators/preceded/
proof.rs
