Function sound_parser 

pub open spec fn sound_parser<T>(
    parser: ParserFnSpec<T>,
    consistent: PredFnSpec<T>,
    byte_len: ByteLenFnSpec<T>,
) -> bool

{
    forall |input: Seq<u8>| (
        #[trigger]
        parser(
            input,
        ) matches Some(
            (n, v),
        ) ==> {
            &&& consistent(v)
            &&& byte_len(v) == n

        }
    )
}

The functional version of SoundParser.