1.1. Where this came from🔗

Triptych grew out of verifying the Cedar authorization language's extension-type parsers: hand-written Lean functions that parse strings such as "-12.34", "1d2h3m", and "2024-10-15T11:38:02Z".

Proving a parser correct forces an uncomfortable question first: correct against what? A correctness theorem needs a specification that is independent of the parser — otherwise the theorem is circular. So for each format we wrote one by hand: a predicate saying which strings are well-formed, and a function saying what value a well-formed string denotes, both phrased as direct transcriptions of the format's grammar.

Doing that three times revealed two things. First, the hand-written spec is itself a place for bugs to hide — a mis-transcribed field width or a forgotten sign case produces a theorem that is provable and wrong. Second, the specs were almost entirely mechanical. Each one had the same shape: an existential decomposition of the string into named fields, per-field character-class predicates, numeric range constraints, and a value function over the captured fields. The shape was dictated by the grammar; only the grammar itself carried information.

Anything mechanical should be generated. That is Triptych.