feat: Tighten specifications on Strings standard library

[robin-aws]

Description

As follow-up from the initial review, this adds a bodiless CharsConsistent lemma to the abstract Std.Strings.ParametricConversion module that ensures chars and charsToDigits are consistent, which is necessary but not sufficient to prove that forall n :: ToInt(OfInt(n)) == n.

Also makes some documentation and naming improvements, adding an IsDigitChar predicate for better readability than c in charsToDigit (which is slightly different from c in chars) and merges the two confusingly-named ToNumberStr and OfNumberStr predicate into one IsNumberStr (with the definition of the former, weaker predicate).

How has this been tested?

Existing tests + verification.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[robin-aws]

I find this fascinating: I couldn't find an {:rlimit} value high enough to keep this from timing out without hitting an overflow exception in Boogie. :) And yet it's totally tractable to just statically evaluate the ensures clause, since there are so few values to test, and this is arguably just as sound a proof as verification!

[alex-chew]

LGTM, though it's not immediately obvious that removing the < base conditions is safe since nothing states that the elements of chars are unique.

[robin-aws]

Thanks Alex! I neglected to call removing the < base conditions in the PR description: they were totally redundant because those were only ever applied to values of type digit, which was already a subtype with that condition.