5.1. Grammar🔗

The grammar language is a strict subclass of the regular languages:

concatenation and finite alternatives;
optional items and the dedicated sign terminal;
built-in digit, hexDigit, and bit runs with {n}, {lo,hi}, or + lengths;
inclusive ASCII ranges such as ascii[63,126]{1};
separated repetition such as rep H16 sepBy ":" {8}.
a final named terminal such as Cells ::= bit{upperTriangleSize Order}, when a literal delimiter fixes its boundary and the start rule captures Order first.

Triptych checks the complete nonterminal graph during elaboration. If it detects a cycle, for example A -> B -> A, it rejects the declaration and reports the cycle. This check enforces the current non-recursive boundary. With an acyclic graph and field boundaries fixed by grammar structure, Triptych can emit readable predicates, executable decoding, and their equivalence mechanically.

5.1.1. Sized final payloads🔗

The first dependent surface form covers a common binary and SAT/SMT layout: a header declares the exact size of the final payload.

def upperTriangleSize (order : String) : Nat :=
  let vertices := Triptych.readNat order
  vertices * (vertices - 1) / 2

def toGraph (order cells : String) : Nat × String :=
  (Triptych.readNat order, cells)

triptych Graph where
  grammar
    Graph ::= Order ":" Cells
    Order ::= digit+
    Cells ::= bit{upperTriangleSize Order}
  value'
    toGraph Order Cells

For "3:101", Order is "3" and the required payload width is three. "3:10" and "3:1010" are rejected. Triptych represents the lexical payload as zero-or-more bits and generates the exact-width equation as part of IsWf. It therefore emits the same readable specification, typed View, structural Derivation, executable parser, parser contracts, and search-cost theorem as for an ordinary declaration. The derivation's structural validity checks the lexical bit shape; the generated IsWf and View.Valid additionally enforce the dependent width.

The width function is specification code: Lean checks its type and definition, while the author is responsible for ensuring that it expresses the intended format rule. The current surface form is deliberately limited to one final, delimiter-bounded payload. Formats in which width validation must make the parser reconsider the header use the staged architecture API described in the scanner chapter.