pub trait SoundParser:
SpecByteLen
+ SpecParser<PVal = Self::T>
+ Consistency<Val = Self::T> {
// Required methods
proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>);
broadcast proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>);
// Provided method
open spec fn sound_inv(&self) -> bool { ... }
}Expand description
Parser soundness.
This trait specifies semantic soundness w.r.t. the format spec, independent
from the orthogonal safety property captured by SafeParser.
Required Methods§
Sourceproof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>)
proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>)
requires
self.sound_inv(),self.spec_parse(ibuf) matches Some((n, v)) ==> n == self.byte_len(v),For any successful parse Some((n, v)), n == self.byte_len(v).
Sourcebroadcast proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>)
broadcast proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>)
requires
self.sound_inv(),#[trigger] self.spec_parse(ibuf) matches Some((_, v)) ==> self.consistent(v),For any successful parse Some((_, v)), v is consistent with the format’s spec.
Provided Methods§
Implementations on Foreign Types§
Source§impl<SpecP, Cnstcy, Blen> SoundParser for (SpecP, Cnstcy, Blen)
impl<SpecP, Cnstcy, Blen> SoundParser for (SpecP, Cnstcy, Blen)
Source§open spec fn sound_inv(&self) -> bool
open spec fn sound_inv(&self) -> bool
{
let (p, c, b) = *self;
let (p_fn, c_fn, b_fn) = (
|ibuf| p.spec_parse(ibuf),
|v| c.consistent(v),
|v| b.byte_len(v),
);
sound_parser(p_fn, c_fn, b_fn)
}