Triptych

3.3. Printer automation🔗

An explicit serializer has one central obligation, encode_view: its output decodes to a valid typed view whose converted denotation is the original domain value.

The automation does not prove arbitrary serializer behavior. Each route starts from evidence that matches how the serializer was developed, then removes the repeated work of constructing the existential view witness.

3.3.1. Existing external parser: triptych_encode🔗

Use triptych_encode when an existing serializer already roundtrips through an external parser and that parser has an agreement theorem. Decimal supplies exactly those facts:

theorem Decimal.encode_view (i : Int64) : ∃ v : Decimal.View, Decimal.decodeView (decimalToStr i) = some v ∧ Decimal.View.Valid v ∧ Int64.ofInt (Decimal.View.denotation v) = i := i:Int64⊢ ∃ v, decodeView (decimalToStr i) = some v ∧ v.Valid ∧ Int64.ofInt v.denotation = i All goals completed! 🐙

The tactic combines Cedar's serializer roundtrip, Decimal parser agreement, the generated view normal forms, and the Int64 conversion inverse. From this one witness, Triptych derives Decimal.parse_toString_roundtrip, serializer injectivity, and normalization results.

3.3.2. Direct generated-spec facts: triptych_encode_direct🔗

Use triptych_encode_direct when there is no external parser to reconcile. Its inputs say directly that the serializer output is accepted by the generated specification and computes the intended value:

private theorem triptychEncodeDirect_identity (n : Nat) : ∃ view, encodeDecodeView (encodePrinter n) = some view ∧ encodeValid view ∧ view.denotation = n := n:Nat⊢ ∃ view, encodeDecodeView (encodePrinter n) = some view ∧ encodeValid view ∧ view.denotation = n All goals completed! 🐙

This regression test has a serializer and generated-spec-style parser but no parser-agreement theorem. The tactic turns the direct acceptance and value facts into the same encode_view obligation expected by downstream roundtrip theorems.

3.3.3. Structural printer: triptych_encode_derivation🔗

Use triptych_encode_derivation when the serializer naturally constructs a grammar derivation. The proof supplies a valid root tree for each domain value; the generated decodeView_render theorem projects that tree to the flat view:

private theorem triptychEncodeDerivation_identity (n : Nat) : ∃ view, encodeDecodeView (encodePrinter n) = some view ∧ encodeValid view ∧ view.denotation = n := n:Nat⊢ ∃ view, encodeDecodeView (encodePrinter n) = some view ∧ encodeValid view ∧ view.denotation = n All goals completed! 🐙

This route avoids separately proving string-level acceptance and value equations, because those facts follow from the valid derivation and its rendering theorem.

3.3.4. Fully synthesized printer: printer auto🔗

printer auto goes one step further: for supported value expressions, Triptych synthesizes the serializer and its Triptych.DerivationPrinter certificate together. The signed-integer syntax test checks both the emitted spelling and the generated roundtrip theorem:

triptych SignedInteger where grammar Root ::= Sign Digits Sign ::= sign Digits ::= digit+ value Sign * nat Digits printer auto #guard SignedInteger.toString 0 = "0" #guard SignedInteger.toString 42 = "42" #guard SignedInteger.toString (-42) = "-42" #guard SignedInteger.parse (SignedInteger.toString (-42)) = some (-42)

Its current proved rule covers total signed decimal integers with no constraints or domain conversion. Unsupported constrained, ofSpec, and opaque value' cases fail with source-located diagnostics instead of emitting an unjustified theorem.