4.2. Values and constraints🔗

The analyzable value DSL computes an Int from sign, magnitude, length, and count readers. The analyzable constraints DSL narrows the grammar with arithmetic comparisons, lengths, numeric values, canonical decimal spelling, and count X.

For semantics outside those DSLs, value' accepts an ordinary Lean function returning any type, while constraints' accepts any Boolean Lean predicate. Both can receive scalar captures or repeated-capture List String arguments.

The Cedar-independent Graph example uses both escapes:

structure Graph where
  order : Nat
  edges : List (Nat × Nat)

triptych Graph where
  grammar
    Adj   ::= Cells
    Cells ::= bit+
  value'
    toGraph Cells
  constraints'
    isTriangular Cells

The grammar accepts any nonempty bit string. isTriangular : String -> Bool restricts its length to n(n-1)/2, so the final accepted language is non-regular even though the grammar is regular. toGraph : String -> Graph constructs the vertex count and edge list. For example, "101" denotes a path on three vertices, while "11" is rejected because length two is not triangular.

With value' or constraints', Triptych still proves grammar reconciliation, decidability, typed-view equations, and generated-parser contracts against the supplied functions. Those functions become part of the trusted specification: Lean checks their definitions, but users must ensure that they correctly represent the intended value and constraint.