============================================================================================ # Grammar ↔ parser bridge lemmas
`IsDecimalValue` is phrased over the grammar's productions (`IsWfSign`/`IsNatural`/`IsWfFrac`)
as a rendering `sign ++ natural ++ "." ++ fraction`, with the value read off those three
fields. `Decimal.parse` instead splits on `'.'` first and parses the signed left field through
`toInt?'`. These lemmas connect the views: the rendering splits back into its parts, a digit
string is exactly one the stdlib parser accepts, and the two value expressions agree. Together
they reduce `Decimal.parse s` on a string with a value to a single `Int64` range check
(`parse_eq_decimal?_of_isDecimalValue`), which is what the soundness/completeness proofs
consume.
The `IsDigits` predicate and its `toNat?'` bridges (`no_underscore_of_isDigits`,
`isNat_of_isDigits`, `isDigits_of_isNat`, `toNat?'_isSome_of_isDigits`,
`isDigits_of_toNat?'_isSome`) are shared with the duration grammar and live in
`Cedar.Thm.Data.String`; the integer-specific lemmas below build on them.
============================================================================================
The value spec is single-valued: a string has at most one value. Because the grammar puts
exactly one '.' in the rendering and Natural is a non-empty digit run, the decomposition a
witness supplies is forced, so IsDecimalValue is a function in relational clothing.
============================================================================================
# toString well-formedness and value
============================================================================================
The canonical string representation of a decimal is well-formed and denotes exactly that
decimal's value. Together with parse_toString_roundtrip this is what rules out a vacuously
satisfiable spec.
The string produced by toString d is well-formed for parsing.