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.take(n1) == buf2.take(n2)
    )
}

Functional non-malleability for parser functions.