pub trait SafeParser: SpecParser {
// Required method
broadcast proof fn lemma_parse_safe(&self, ibuf: Seq<u8>);
// Provided method
open spec fn safe_inv(&self) -> bool { ... }
}Expand description
Parser safety.
Successful parses never consume bytes out of bounds.
Required Methods§
Sourcebroadcast proof fn lemma_parse_safe(&self, ibuf: Seq<u8>)
broadcast proof fn lemma_parse_safe(&self, ibuf: Seq<u8>)
requires
self.safe_inv(),#[trigger] self.spec_parse(ibuf) matches Some((n, _)) ==> 0 <= n <= ibuf.len(),For any successful parse Some((n, _)), 0 <= n <= ibuf.len().