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§
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)
Dyn Compatibility§
This trait is dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety".