feat(data/buffer/parser/*): expand parser properties (#6339)
Add several new properties to parsers:
`static`
`err_static`
`step`
`prog`
`bounded`
`unfailing`
`conditionally_unfailing`.
Most of these properties hold cleanly for existing core parsers, and are provided as classes. This allows nice derivation for any parsers that are made using parser combinators.
This PR is towards proving that the `nat` parser provides the maximal possible natural.
Other API lemmas are introduced for `string`, `buffer`, `char`, and `array`.
