Formalize and Verify the Decimal parser - #979
Open
cruisesong7 wants to merge 15 commits into
Open
Conversation
MavenRain
reviewed
Jun 29, 2026
| exact Nat.underscore_not_in_toDigits h | ||
| simpa [String.contains] using h | ||
| split | ||
| · -- "000" ++ toString n, n < 10 |
Contributor
There was a problem hiding this comment.
A have zeropad_ok (pad) (hp) : . . . could cut some duplication between the different cases where the primary discriminant is the number of leading zeros.
MavenRain
reviewed
Jun 29, 2026
| rename_i h2 h1 | ||
| rw [hno_us "00" _ (by simp)] | ||
| simp [String.toNat?, String.Slice.toNat?] | ||
| simp[toDigits_foldl_roundtrip _] |
Contributor
There was a problem hiding this comment.
Nit: missing space between simp and [
MavenRain
approved these changes
Jun 29, 2026
Rewrite the decimal well-formedness predicate and value function so they are
a faithful, direct transcription of the reference grammar's productions,
instead of delegating validity and value to the stdlib string-to-number
parsers. The goal is that the Lean spec reads straight off the grammar block:
Decimal ::= Integer '.' Fraction
Integer ::= ['-'] Digit⁺
Fraction ::= Digit{1,4}
value = int(Integer) × 10⁴ + sign × nat(Fraction) × 10^(4 − |Fraction|)
Changes:
- IsWfStr is now defined via IsDigits / IsWfInt, phrased over Char.isDigit,
so it encodes `['-'] Digit⁺` and `Digit{1,4}` literally and independently of
any parser. The old `left ≠ "-"` and `0 < right.length` side conditions
become structural consequences of `Digit⁺`, removing the stdlib-fragility
that previously required an explicit bare-"-" guard.
- computeValue mirrors the grammar's single-`sign`-factor value function and
returns Option Int (none for malformed input) rather than a junk 0.
- Grammar↔parser bridge lemmas (digit strings ↔ toInt?'/toNat?' acceptance)
connect the re-formalized spec to Decimal.parse; parse_sound,
parse_complete, and parse_eq_none_iff are restated accordingly.
- Grammar.lean holds only definitions; the bridge and toString lemmas live in
Lemmas.lean, split into clearly-segmented sections.
All proofs remain axiom-clean (propext, Classical.choice, Quot.sound).
Signed-off-by: cruisesong7 <csong326@gatech.edu>
Move the character-level `IsDigits` predicate (the grammar's `Digit⁺` production) and its `toNat?'` correspondence bridges out of the decimal grammar and into `Cedar.Thm.Data.String`, so the predicate can be reused by other numeric grammars (e.g. duration) rather than being decimal-specific. - `Cedar.Thm.Data.String` now hosts `IsDigits`, the four digit-string bridges (`no_underscore_of_isDigits`, `isNat_of_isDigits`, `isDigits_of_isNat`, `toNat?'_isSome_of_isDigits`, `isDigits_of_toNat?'_isSome`) and dot-notation projections (`IsDigits.ne_empty`, `.toNat?'_isSome`, `.all_isDigit`), organized into clearly-segmented sections. - Decimal's `Grammar`/`Lemmas` now reuse the shared `IsDigits`; the integer-specific `IsWfInt` bridges remain in the decimal module. No proof content changed; build stays axiom-clean. Signed-off-by: cruisesong7 <csong326@gatech.edu>
Complete the one-to-one correspondence between the reference grammar's
productions and the well-formedness predicates:
Decimal ::= Integer '.' Fraction → IsWfDecimal
Integer ::= ['-'] Digit⁺ → IsWfInt
Fraction ::= Digit{1,4} → IsWfFrac
- Add `IsWfFrac` (`IsDigits s ∧ s.length ≤ DECIMAL_DIGITS`) so the fraction
production is a named predicate rather than spelled inline in `IsWfStr`.
- Rename `IsWfStr` → `IsWfDecimal` (and the lemmas embedding the name:
`isWfDecimal_iff`, `toString_isWfDecimal`, `computeValue_isSome_of_isWfDecimal`,
`parse_some_isWfDecimal`) so the top-level predicate names the `Decimal`
production, mirroring the forthcoming `IsWfDuration`.
No proof content changed; build stays axiom-clean.
Signed-off-by: cruisesong7 <csong326@gatech.edu>
Re-add the `-- ANCHOR: … -- ANCHOR_END: …` comment markers (dropped in an earlier refactor) around IsWfInt, IsWfFrac, IsWfDecimal, and computeValue so the decimal doc can render these definitions from source. Comments only; no proof or definition change. Signed-off-by: cruisesong7 <csong326@gatech.edu>
The Nat-to-Int coercion on the fraction value is inserted implicitly by the arithmetic elaborator, since the surrounding operands are already Int. Signed-off-by: cruisesong7 <csong326@gatech.edu>
parse_sound now concludes only IsWfDecimal s ∧ computeValue s = some d.toInt. The MIN ≤ d.toInt ≤ MAX conjuncts were redundant: d : Decimal = Int64, so d.toInt is in range by construction (Int64.toInt is unconditionally bounded). This matches the "range constraint is implicit" reasoning already used in parse_complete. Proof unchanged apart from dropping the two range obligations. Signed-off-by: cruisesong7 <csong326@gatech.edu>
Restate the decimal grammar in the same shape as the duration and datetime
grammars: one predicate per production (IsWfSign / IsWfNat / IsWfFrac) and
IsWfDecimal s := exists sign natural fraction,
s = sign ++ natural ++ "." ++ fraction and each part well-formed
replacing the split-based phrasing that folded the optional sign into an
IsWfInt integer part. The optional sign now reads as its own production, as in
the grammar itself.
Only the isWfDecimal_iff bridge needed reproving: downstream consumers all
destructure through it, so the surface theorems are untouched. The new
direction needs the split/concat round-trip, so add join_splitToList (converse
of the existing splitToList_eq) to Cedar.Thm.Data.String, plus per-production
no-dot and sign/natural toInt?' bridges.
All decimal theorems still close, sorry-free, standard axioms only.
Signed-off-by: cruisesong7 <csong326@gatech.edu>
IsWfSign (['-'] optional minus) and the digit-width refinements IsFixedDigits
(Digit{n}) / IsDigitsUpTo (Digit{1,n}) are not decimal-specific, so move them
next to the shared IsDigits vocabulary. Decimal now spells Sign and Natural
with the shared predicates directly and keeps only Fraction as a local
definition (an IsDigitsUpTo instance); the IsWfNat alias for IsDigits is gone.
IsFixedDigits is currently duplicated in the datetime grammar; that copy is
replaced by the shared one in a follow-up on cruise-datetime.
Signed-off-by: cruisesong7 <csong326@gatech.edu>
The doc chapters render IsFixedDigits / IsDigitsUpTo / IsWfSign from source via anchor blocks, so mark them like the neighbouring IsDigits. Signed-off-by: cruisesong7 <csong326@gatech.edu>
The docstring cited int(Integer), a production that no longer exists. State the grammar's value function in the factored Sign/Natural form and explain that computeValue implements an equivalent regrouping, since toInt?' reads the sign along with the digits. Signed-off-by: cruisesong7 <csong326@gatech.edu>
Grammars can now name Natural the way they name Sign and Fraction (IsWfSign, IsDigitsUpTo) instead of reaching for IsDigits directly. It is an abbrev, so it is definitionally IsDigits: every existing IsDigits lemma applies without unfolding and no proof needed changing. Signed-off-by: cruisesong7 <csong326@gatech.edu>
The grammar proofs reference both, so they must be visible outside the module: DECIMAL_DIGITS becomes a public abbrev (transparent, so the numeral still reduces in proofs) and the ToString Decimal instance becomes public. Without the latter, toString d resolves to Int64's instance in the proof modules and toString_isWfDecimal no longer typechecks. Signed-off-by: cruisesong7 <csong326@gatech.edu>
cruisesong7
force-pushed
the
cruise-decimal
branch
from
July 29, 2026 18:50
657f357 to
fe449c3
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
IsWfStrdefineswell-formedness (the context-free structure) and
computeValuedefinesthe semantic attribute (the synthesized integer value)
parse_toString_roundtrip:parse ∘ toString = someparse_eq_none_iff: parse fails iff not well-formed or value overflows Int64parse_sound: if parse succeeds then input is well-formed, value isin Int64 range, and the result has exactly that computed value
toString_injective: distinct decimals produce distinct stringsCedar.Thm.Data.StringTest plan
lake buildpasses oncruise-decimal