2.3.1. The generated parser🔗

def Decimal.parse : String → Option Int64 :=
fun s => scannerParse Decimal.grammar Decimal.constraints Decimal.valueExpr Int64.ofInt s

Read this definition as a pipeline:

1. scannerParse scans the input once and obtains the named captures.

2. It checks both grammar-derived and semantic constraints against that same capture map.

3. For an accepted input, it evaluates Decimal.valueExpr to the specification-level Int.

4. Int64.ofInt converts that value to the parser's Int64 result; a rejected input returns Option.none.

The generated Decimal.parse_eq_gated theorem proves that this single-scan implementation has exactly the readable behavior “accept when Decimal.IsValid, then return Decimal.computeValue converted by Int64.ofInt.”

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)

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)

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. Scanning the grammar🔗

Before a value can be computed, the generated scanner extracts the grammar's named captures:

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.

The scanner performs ordered search directly and stops at the first complete parse. The archived Triptych.decode definition instead constructs lists of candidate splits; it is kept as a transparent reference semantics. The checked theorem Triptych.scan_eq_decode proves that both select exactly the same capture map on every input, so replacing the runtime engine does not change the readable specification, computed value, or parser contracts.

2.3.4. Computing the specification value🔗

Decimal.computeValue uses the scanner 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 => scannerComputeValue 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)

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:

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:

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:

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

2.3.7. Why the parser is correct by construction🔗

Triptych generates the grammar, constraints, value expression, and scanner parser from the same DSL description. The generic theorem Triptych.scannerParse_eq_surfaceGatedParseOfSpec proves that the one-scan implementation equals the readable Triptych.gatedParseOfSpec contract.

The generated contracts rewrite through Decimal.parse_eq_gated and then apply generic theorems about that contract. For example, the complete soundness proof has this form:

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:

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.