theorem Cedar.Thm.Decimal.wf_iff_exists_value {s : String} : IsWfDecimal s ↔ ∃ (v : Int), IsDecimalValue s v

Well-formed decimal syntax is exactly syntax to which the grammar assigns some value.

theorem Cedar.Thm.Decimal.parse_complete (s : String) (d : Spec.Ext.Decimal) (hval : IsDecimalValue s (Int64.toInt d)) : Spec.Ext.Decimal.parse s = some d

Completeness of Decimal.parse: if the grammar assigns s the value d.toInt, then parsing accepts the string as d. Well-formedness is not a separate hypothesis — IsDecimalValue already asserts that s is a rendering of the grammar's productions.

theorem Cedar.Thm.Decimal.parse_sound (s : String) (d : Spec.Ext.Decimal) (h : Spec.Ext.Decimal.parse s = some d) : IsDecimalValue s (Int64.toInt d)

Soundness of Decimal.parse: if parsing succeeds, then the input is a well-formed rendering whose grammar value is exactly the returned decimal's value. (The value is automatically in Int64 range, since d : Decimal = Int64, so no range conjunct is stated.)

theorem Cedar.Thm.Decimal.parse_eq_some_iff_isDecimalValue (s : String) (d : Spec.Ext.Decimal) : Spec.Ext.Decimal.parse s = some d ↔ IsDecimalValue s (Int64.toInt d)

Exact parser characterization: parsing succeeds with d precisely when the declarative grammar relation assigns the input the value d.toInt.

theorem Cedar.Thm.Decimal.parse_toString_roundtrip (d : Spec.Ext.Decimal) : Spec.Ext.Decimal.parse (toString d) = some d

Parsing the canonical string representation of a decimal returns the same decimal.

theorem Cedar.Thm.Decimal.parse_eq_none_iff (s : String) : Spec.Ext.Decimal.parse s = none ↔ ¬IsWfDecimal s ∨ ∃ (v : Int), IsDecimalValue s v ∧ (v < Int64.MIN ∨ v > Int64.MAX)

Failure characterization for Decimal.parse: parsing rejects exactly malformed strings and well-formed strings whose grammar value overflows the Int64 range. The value relation is total on well-formed syntax, so these cases are exhaustive and mutually exclusive.

theorem Cedar.Thm.Decimal.toString_injective (d d' : Spec.Ext.Decimal) (h : toString d = toString d') : d = d'

toString is injective: distinct decimals produce distinct strings.

theorem Cedar.Thm.Decimal.normalize_eq_iff_parse_eq (s s' : String) : normalize s = normalize s' ↔ Spec.Ext.Decimal.parse s = Spec.Ext.Decimal.parse s'

Equal normal form iff equal value: normalization decides decimal equality.