2.3. Artifact two: the executable parser🔗

The readable specification says which strings are valid and what they mean. The generated parser.lean turns that interface into a function that returns a domain value.

2.3.1. The generated parser🔗

def Decimal.parse : String → Option Int64 :=
fun s => gatedParseOfSpec Decimal.IsValid Decimal.computeValue Int64.ofInt s#print Decimal.parse

def Decimal.parse : String → Option Int64 :=
fun s => gatedParseOfSpec Decimal.IsValid Decimal.computeValue Int64.ofInt s

Read this definition as a pipeline:

gatedParseOfSpec uses the generated decision procedure for Decimal.IsValid to check both the grammar and its semantic constraints.
An invalid input returns Option.none.
For a valid input, Decimal.computeValue computes the specification-level Int.
Int64.ofInt converts that value to the parser's Int64 result.

The first two inputs below succeed. The third violates the grammar, while the fourth has the right shape but denotes a value outside the Int64 range:

(some 15000, some (-1500), none, none)#eval
  (Decimal.parse "1.5",
    Decimal.parse "-0.15",
    Decimal.parse "1.x",
    Decimal.parse "922337203685477.5808")

(some 15000, some (-1500), none, none)

2.3.2. Executing validity🔗

The generated decision procedure makes the readable predicates directly executable with decide. This separates a grammar failure from a semantic-constraint failure:

(false, true, false, false)#eval
  let tooLarge := "922337203685477.5808"
  (decide (Decimal.IsWf "3.14159"),
    decide (Decimal.IsWf tooLarge),
    decide (Decimal.SatisfiesConstraints tooLarge),
    decide (Decimal.IsValid tooLarge))

(false, true, false, false)

The first string fails Decimal.IsWf because it has five fraction digits. The second string is well-formed, but it fails Decimal.SatisfiesConstraints, so Decimal.IsValid also returns false.

2.3.3. Decoding the grammar🔗

Before a value can be computed, the generated engine decodes the input into the grammar's named captures:

some [("Sign", ""), ("Natural", "1"), ("Fraction", "5")]#eval decode Decimal.grammar "1.5"

some [("Sign", ""), ("Natural", "1"), ("Fraction", "5")]

This capture map is an engine representation. Ordinary clients use the typed Decimal.View introduced in §2.2 instead of looking up these string keys.

2.3.4. Computing the specification value🔗

Decimal.computeValue decodes the input and evaluates the DSL's value expression. Its result is still the specification-level Int; it neither applies the semantic constraint nor converts the result to Int64:

def Decimal.computeValue : String → Option Int :=
fun s => computeValue Decimal.grammar Decimal.valueExpr s#print Decimal.computeValue

def Decimal.computeValue : String → Option Int :=
fun s => computeValue Decimal.grammar Decimal.valueExpr s

The distinction is visible in these three results. A valid decimal computes normally, the well-formed but out-of-range decimal still computes an Int, and malformed text cannot be decoded:

(some 15000, some 9223372036854775808, none)#eval
  (Decimal.computeValue "1.5",
    Decimal.computeValue "922337203685477.5808",
    Decimal.computeValue "1.x")

(some 15000, some 9223372036854775808, none)

2.3.5. The typed executable view🔗

The engine stores captures in a generic string-keyed map. Without a typed view, every client proof would have to unfold that representation and reason about lookups such as "Natural" ↦ "12" and "Fraction" ↦ "34". The view theorems perform that translation once: client code obtains a Decimal.View and works directly with fields such as v.natural, v.fraction, and v.denotation.

Surface validity is then equivalent to the existence of a valid decoded view, and value computation and parser results factor through that same record:

@Decimal.decodeView_input : ∀ {s : String} {v : Decimal.View}, Decimal.decodeView s = some v → v.input = s#check @Decimal.decodeView_input
Decimal.IsValid_view : ∀ (s : String), Decimal.IsValid s ↔ ∃ v, Decimal.decodeView s = some v ∧ v.Valid#check @Decimal.IsValid_view
Decimal.computeValue_view : ∀ (s : String),
  Decimal.computeValue s = Option.map Decimal.View.denotation (Decimal.decodeView s)#check @Decimal.computeValue_view
Decimal.parse_eq_some_iff_view : ∀ (s : String) (i : Int64),
  Decimal.parse s = some i ↔
    ∃ decodedView, Decimal.decodeView s = some decodedView ∧ decodedView.Valid ∧ Int64.ofInt decodedView.denotation = i#check @Decimal.parse_eq_some_iff_view
Decimal.parse_eq_none_iff_view : ∀ (s : String), Decimal.parse s = none ↔ ¬∃ v, Decimal.decodeView s = some v ∧ v.Valid#check @Decimal.parse_eq_none_iff_view

The generated engine also connects structural derivations to executable decoding. Decimal.Derivation.Decimal.matches proves that a valid derivation matches the root production, and Decimal.Derivation.Decimal.mem_fullParses records its captures as a complete parse of the grammar. The Decimal grammar passes the conservative all-input uniqueness checker, so Decimal.Derivation.Decimal.decode_render proves that the decoder recovers those captures without an ambiguity premise. Finally, Decimal.Derivation.Decimal.decodeView_render proves that decoding recovers the same typed view:

Decimal.Derivation.Decimal.matches : ∀ (qual : String) (fuel : Nat) (d : Decimal.Derivation.Decimal),
  d.Valid →
    ProdMatch Decimal.grammar qual (fuel + 2)
      { name := "Decimal",
        alts :=
          [[{ sym := Sym.ref "Sign" }, { sym := Sym.ref "Natural" }, { sym := Sym.lit "." },
              { sym := Sym.ref "Fraction" }]] }
      d.render (Decimal.Derivation.Decimal.capturesWith qual d)#check @Decimal.Derivation.Decimal.matches
Decimal.Derivation.Decimal.mem_fullParses : ∀ (d : Decimal.Derivation.Decimal),
  d.Valid → Decimal.Derivation.Decimal.capturesWith "" d ∈ fullParses Decimal.grammar d.render#check @Decimal.Derivation.Decimal.mem_fullParses
Decimal.Derivation.Decimal.decode_render : ∀ (d : Decimal.Derivation.Decimal),
  d.Valid → decode Decimal.grammar d.render = some (Decimal.Derivation.Decimal.capturesWith "" d)#check @Decimal.Derivation.Decimal.decode_render
Decimal.Derivation.Decimal.decodeView_render : ∀ (d : Decimal.Derivation.Decimal),
  d.Valid → Decimal.decodeView d.render = some d.toView#check @Decimal.Derivation.Decimal.decodeView_render
"-12.34"#eval
  CedarExamples.Decimal.Decimal.Derivation.Decimal.render
    CedarExamples.Decimal.decimalDerivation

2.3.6. Generated parser contracts🔗

Beyond the executable function, parser.lean contains machine-checked contracts emitted and proved automatically. Every success is valid and correctly valued, every valid input with a matching value succeeds, and rejection is exactly invalidity:

Decimal.parse_sound : ∀ (s : String) (i : Int64),
  Decimal.parse s = some i → Decimal.IsValid s ∧ Option.map Int64.ofInt (Decimal.computeValue s) = some i#check @Decimal.parse_sound
Decimal.parse_complete : ∀ (s : String) (i : Int64),
  Decimal.IsValid s → Option.map Int64.ofInt (Decimal.computeValue s) = some i → Decimal.parse s = some i#check @Decimal.parse_complete
Decimal.parse_reject : ∀ (s : String), Decimal.parse s = none ↔ ¬Decimal.IsValid s#check @Decimal.parse_reject

Compiler-generated theorems use only propext, Classical.choice, and Quot.sound.

2.3.7. Why the parser is correct by construction🔗

Triptych does not generate a format-specific parsing algorithm and then ask the user to prove it correct. It generates Decimal.IsValid and Decimal.computeValue from the same DSL description, then instantiates the already-proved Triptych.gatedParseOfSpec combinator with those two definitions.

The generated contracts are direct applications of generic theorems about that combinator. For example, the complete proof of the generated parser's soundness has this form:

example (s : String) (i : Int64) :
    Decimal.parse s = some i →
      Decimal.IsValid s ∧
        (Decimal.computeValue s).map Int64.ofInt = some i :=
  Triptych.gatedParseOfSpec_sound _ _ _ s i

The same construction supplies completeness and rejection. When the generated file builds, Lean checks the parser definition and each proof term together. If the emitted parser no longer has the behavior required by a generic theorem, the proof does not typecheck.

Here, correct by construction has a precise boundary: for every input, the generated parser implements the authored Triptych validity and value specification. It does not by itself prove that the human-authored grammar is an accurate transcription of Cedar's intended format. The independent corpus check at the end of this chapter addresses that separate question.

2.3.8. The runtime-checked Cedar parser🔗

Before any format-specific proof about Cedar's implementation, parser.lean generates Decimal.checkedExtParse. It first runs Cedar's parser. If Cedar returns a value, the checked parser keeps that result only when Decimal.IsValid accepts the same input and Decimal.computeValue computes the same value after conversion; otherwise it returns Option.none:

Decimal.checkedExtParse : String → Option Cedar.Spec.Ext.Decimal#check @Decimal.checkedExtParse
Decimal.checkedExtParse_eq_some_iff : ∀ (s : String) (d : Cedar.Spec.Ext.Decimal),
  Decimal.checkedExtParse s = some d ↔
    Cedar.Spec.Ext.Decimal.parse s = some d ∧ Decimal.IsValid s ∧ Decimal.computeValue s = some (Int64.toInt d)#check @Decimal.checkedExtParse_eq_some_iff
Decimal.checkedExtParse_sound_view : ∀ (s : String) (d : Cedar.Spec.Ext.Decimal),
  Decimal.checkedExtParse s = some d → ∃ v, Decimal.decodeView s = some v ∧ v.Valid ∧ v.denotation = Int64.toInt d#check @Decimal.checkedExtParse_sound_view

This provides runtime soundness without first proving Cedar's parser correct. It does not repair a false rejection: if Cedar returns Option.none, the checked parser also returns Option.none.