Triptych

6.2. Broader grammar coverage🔗

Automation improves 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 Decimal. Shared-prefix alternatives, nullable sequences such as the lowered dependent-width Graph payload, and more repetition shapes need broader capture-functionality certificates before they can receive the same premise-free roundtrip theorems.

  2. Character classes and repetition. Inclusive ASCII ranges are now supported. General Base64 still needs arbitrary finite classes or unseparated repetition of a 64-way symbol, together with quartet and padding constraints.

  3. Dependent field boundaries. The public dependent-width form now generates the complete artifact family for one delimiter-bounded final payload, as exercised by the sized upper-triangular graph. The verified Triptych.scanDependent architecture handles the broader header-selected-tail model, and Graph6 exercises that path. The next step is lowering delimiter-free and internal dependent fields to that staged engine while retaining the same readable predicates, views, derivations, and parser contracts.

  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.