pub trait NoLookAhead: SafeParser {
// Required method
proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>);
// Provided methods
open spec fn no_lookahead_inv(&self) -> bool { ... }
fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>) { ... }
}Expand description
No-lookahead property for parsers.
Intuitively: the parser’s behavior does not depend on “future” bytes beyond the consumed prefix (i.e., it does not need to “look ahead”/“peek” at them to decide how to parse the prefix).
Formally: if two buffers share a common prefix that successfully parses, then they parse to the same value.
Required Methods§
Sourceproof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>)
proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>)
requires
self.safe_inv(),self.no_lookahead_inv(),self
.spec_parse(
i1,
) matches Some(
(n, v),
) ==> 0 <= n <= i2.len()
==> (i2.take(n) == i1.take(n) ==> self.spec_parse(i2) == Some((n, v))),Provided Methods§
Sourceopen spec fn no_lookahead_inv(&self) -> bool
open spec fn no_lookahead_inv(&self) -> bool
{ true }Sourceproof fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>)
proof fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>)
requires
self.safe_inv(),self.no_lookahead_inv(),self.spec_parse(i1) matches Some((n, v)) ==> self.spec_parse(i1 + i2) == Some((n, v)),