1.2. Formal Specification🔗

Following the readable specification generated by Triptych, we separate the grammar production, well-formedness, and denotation. DecimalProduction relates a string to its grammar fields, IsWfDecimal hides those fields existentially, and IsDecimalValue s v extends the same witness with its value. Cedar already has the executable Decimal.parse, so the theorem layer does not define a second operational computeValue decoder.

The building block is IsDigits, which captures Digit⁺ — a non-empty string all of whose characters satisfy Char.isDigit. It lives at the root namespace in Cedar.Thm.Data.String, shared with the duration and datetime grammars:

public def IsDigits (s : String) : Prop :=
  0 < s.length ∧ ∀ c ∈ s.toList, c.isDigit = true

Sign ::= ['-'] is the optional leading minus, common to the signed numeric grammars:

public def IsWfSign (s : String) : Prop :=
  s = "-" ∨ s = ""

And Digit{1,n} refines IsDigits by bounding the run's width from above:

public def IsAtMostNDigits (n : Nat) (s : String) : Prop :=
  IsDigits s ∧ s.length ≤ n

These three predicates — IsDigits, IsWfSign, and IsAtMostNDigits — are the shared vocabulary. The names for the decimal grammar's Natural and Fraction productions stay in its own grammar module.

Natural ::= Digit⁺ is IsDigits under the production's name for readability:

public abbrev IsNatural (s : String) : Prop := IsDigits s

The fraction production is the bounded-digits predicate at the grammar's width, Fraction ::= Digit{1,4}:

public def IsWfFrac (s : String) : Prop :=
  IsAtMostNDigits DECIMAL_DIGITS s

A decimal production relates the rendered string to its well-formed component fields:

public def DecimalProduction (s sign natural fraction : String) : Prop :=
  s = sign ++ natural ++ "." ++ fraction ∧
  IsWfSign sign ∧
  IsNatural natural ∧
  IsWfFrac fraction

Well-formedness existentially hides those component witnesses:

public def IsWfDecimal (s : String) : Prop :=
  ∃ sign natural fraction, DecimalProduction s sign natural fraction

The value formula uses the shared string-level readers natOf, signOf, and lenOf, matching the grammar notation directly:

public def natOf (s : String) : Nat := (toNat?' s).getD 0public def signOf (s : String) : Int := if s.startsWith "-" then -1 else 1public def lenOf (s : String) : Int := s.length

public def value (sign natural fraction : String) : Int :=
  signOf sign *
    ((natOf natural : Int) * Int.pow 10 DECIMAL_DIGITS
     + (natOf fraction : Int) * Int.pow 10 ((DECIMAL_DIGITS : Int) - lenOf fraction).toNat)

The relational value specification extends the same grammar witnesses with their denotation:

public def IsDecimalValue (s : String) (v : Int) : Prop :=
  ∃ sign natural fraction,
    DecimalProduction s sign natural fraction ∧
    v = value sign natural fraction

The existential supplies the decomposition, so nothing here splits or slices a string: no String.front, no String.drop, no String.splitToList, and no Option for a "the fields did not parse" case. IsWfFrac fraction bounds lenOf fraction ≤ 4, so the 4 - |Fraction| exponent cannot underflow. Beyond the shared value readers, the definition talks only about digit characters; it does not mention the string-to-number parser toInt?' the implementation uses, which keeps the specification independent of the parsing implementation.

The syntax and value views agree: every well-formed rendering has a value, and every value witness contains a well-formed rendering.

theorem

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

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

Phrasing the value as a relation raises the question of whether it pins down a function at all. It does: a string has at most one value, because the grammar puts exactly one '.' in the rendering and a Natural cannot begin with '-', so the decomposition a witness supplies is forced.

theorem

Cedar.Thm.Decimal.isDecimalValue_unique {s : String} {v₁ v₂ : Int}
  (h₁ : IsDecimalValue s v₁) (h₂ : IsDecimalValue s v₂) : v₁ = v₂
Cedar.Thm.Decimal.isDecimalValue_unique
  {s : String} {v₁ v₂ : Int}
  (h₁ : IsDecimalValue s v₁)
  (h₂ : IsDecimalValue s v₂) : v₁ = v₂

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.