Triptych

2.5. Independent check against Cedar's test corpus🔗

The generated proof covers every string relative to the Triptych specification. A finite test suite answers a different question: does that authored specification agree with Cedar on the cases Cedar's developers chose to test?

cedar-examples/ConformanceTests.lean carries over every valid and invalid parser case from Cedar's relevant Decimal, Duration, Datetime, and IP address unit-test suites. It also includes IP strings used by Cedar's rendering, loopback, range, equality, and symbolic tests, plus focused grammar-boundary cases.

The suite compares:

  • the generated parser with Cedar's parser for Decimal, Duration, Datetime, IPv4, and IPv6;

  • the readable IsValid specifications with Cedar for IPv4 and IPv6;

  • each runtime-checked Cedar parser with Cedar's original parser, confirming that the runtime check retains every Cedar result in the corpus; and

  • generated and Cedar IPv6 printer roundtrips.

This is 13 suites and 882 checks. All currently pass, and lake build ConformanceTests fails if any comparison diverges.

The corpus has already exposed a distinction that the construction proof cannot. An early Duration grammar put the optional minus sign in an anonymous position. The generated parser was proved correct relative to that grammar, but the grammar computed a negative duration as positive. Cedar's independently authored cases found the value mismatch. The fix made the sign a named production and taught the DSL to reject that unsafe shape.

The two layers therefore support different claims:

  • the Lean proof establishes parser correctness for all inputs relative to the authored specification;

  • the Cedar corpus increases confidence that the authored specification matches Cedar, but it remains finite test evidence rather than a universal proof.