Triptych

5.3. Broader grammar coverage🔗

The first two tracks improve formats that Triptych already supports. Grammar work changes the accepted DSL itself, so it should proceed incrementally. Each step removes a different current restriction and asks more of the parser backend and proof generator:

  1. Broader static certificates. The conservative Triptych.Grammar.staticUnique checker certifies deterministic fragments such as Graph and Decimal. Shared-prefix alternatives, nullable sequences, and more repetition shapes need broader capture-functionality certificates before they can receive the same premise-free roundtrip theorems.

  2. Character classes and repetition. General Base64 needs user-defined finite character classes or unseparated repetition of a 64-way symbol, together with quartet and padding constraints. The value tier can already host a decoder once the grammar can split and validate the text.

  3. Dependent field boundaries. Constraints can reject a decoded string but cannot change how it was split. Graph6 is a representative next case because its header determines the length of the following payload.

  4. Recursive productions. JSON, s-expressions, and Cedar policies require recursive grammar support. Until it exists, these formats need a hand-written parser and a separately proved specification.

Recursive productions are the point where Triptych may need a different parsing model rather than another local grammar extension. The design study should compare three relevant systems:

  • The verified LL(1) generator, A Verified LL(1) Parser Generator (Lasser et al., ITP 2019), restricts the grammar to obtain deterministic parsing and termination.

  • CoStar, CoStar: A Verified ALL(*) Parser (Lasser et al., PLDI 2021), generates verified parsers for recursive grammars.

  • CoStar++, Verified ALL(*) Parsing with Semantic Actions and Dynamic Input Validation (Lasser et al., NFM 2023), also incorporates semantic actions and dynamic input-validation predicates.

The comparison should evaluate grammar coverage, generated-parser performance, extraction and integration costs, the trust boundary for user-supplied semantics, and whether an approach can verify an existing parser rather than only the parser it generates.