Function non_malleable_parser 

pub open spec fn non_malleable_parser<T>(parser: ParserFnSpec<T>) -> bool

{
    forall |buf1: Seq<u8>, buf2: Seq<u8>| (
        #[trigger]
        parser_pair_some(
            parser,
            buf1,
            buf2,
        ) matches Some(((n1, v1), (n2, v2))) ==> v1 == v2 ==> buf1[0..n1] == buf2[0..n2]
    )
}

Functional non-malleability for parser functions.