pub trait NonMalleable: SafeParser {
// Required method
proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>);
// Provided method
open spec fn nonmal_inv(&self) -> bool { ... }
}Expand description
Parser non-malleability.
If two buffers parse to equal values, their consumed bytes are identical—i.e., each semantic value has a unique byte-level representation.
Required Methods§
Sourceproof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)
proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)
requires
self.safe_inv(),self.nonmal_inv(),self
.spec_parse(
buf1,
) matches Some(
(n1, v1),
) ==> self
.spec_parse(
buf2,
) matches Some((n2, v2)) ==> v1 == v2 ==> buf1.take(n1) == buf2.take(n2),Provided Methods§
Sourceopen spec fn nonmal_inv(&self) -> bool
open spec fn nonmal_inv(&self) -> bool
{ true }Optional invariant (used by spec-function combinators; struct-based combinators
typically leave this as true)