1.2. One block in, up to three files out🔗

A triptych block has a required grammar and optional value, constraint, external-parser, and printer clauses. Here is the Cedar Decimal input:

Triptych: wrote Decimal → Outputs/Decimal/ [spec.lean, parser.lean] (26 spec + 15 engine + 31 proof + 13 verified-parser + 18 obligation decls)Triptych: Outputs/Decimal/soundness.lean exists — left untouched (it holds your proofs; delete it to re-scaffold)triptych declaration uses `sorry`declaration uses `sorry`declaration uses `sorry`declaration uses `sorry`declaration uses `sorry`Decimal where
  grammar
    Decimal  ::= Sign Natural "." Fraction
    Sign     ::= sign
    Natural  ::= digit+
    Fraction ::= digit{1,4}
  value
    Sign * (nat Natural * 10 ^ 4 + nat Fraction * 10 ^ (4 - len Fraction))
    ofSpec Int64.ofInt
    toSpec Int64.toInt
  constraints
    value ∈ [Int64.MIN, Int64.MAX]
  parser Cedar.Spec.Ext.Decimal.parse
  printer decimalToStr
  to "Outputs/Decimal"

The source lives in cedar-examples/Inputs/Decimal.lean. Its output is split by role:

spec.lean -- what a reviewer reads. It contains the grammar value, per-production IsWf predicates, value and constraint functions, the overall IsValid predicate, a typed View, and typed Derivation trees. It contains no proofs.
parser.lean -- what an application runs and the kernel checks. It contains the generic engine instance, decodeView, computeValue, the specialized parse, and all compiler-discharged reconciliation and parser-contract theorems.
soundness.lean -- the integration boundary. This write-once scaffold appears only for an explicit external parser or serializer. It states the semantic facts that the compiler cannot infer from syntax.

All compiler-generated proofs use only propext, Classical.choice, and Quot.sound. The five shipped Cedar formats also contain completed integration proofs: there are no placeholders in their output or proof modules.