Function safe_parser 

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

{
    forall |input: Seq<u8>| (
        #[trigger]
        parser(input) matches Some((n, _)) ==> 0 <= n <= input.len()
    )
}

The functional version of SafeParser.