Triptych

 Triptych🔗

Triptych. Parser, spec, and soundness: one grammar, three panels.

Triptych is a Lean 4 grammar-to-parser compiler for flat, non-recursive string formats.

A triptych block -- a grammar plus optional value, constraint, external-parser, and printer clauses -- generates a coherent family of artifacts:

  • a readable surface specification with typed syntax derivations,

  • a verified executable parser and typed decoded view, and

  • machine-checked reconciliation, parser-contract, and printer theorems.

Compiler-generated proofs depend only on propext, Classical.choice, and Quot.sound. The shipped Cedar examples also discharge every format-specific external-parser and printer obligation.

The chapters follow the compiler from its source DSL through executable parsing, generated correctness proofs, checks against Cedar's test corpus, proof automation, current scope, and next steps.

Contents

  1. 1. Introduction: one grammar, a coherent parser stack
  2. 2. Walkthrough: the Decimal format, end to end
  3. 3. Automation: discharging proof obligations
  4. 4. Scope: supported tiers and current boundaries
  5. 5. Next steps
  6. 6. Demo