Spec-driven test generation

Hull generates random well-typed Deep programs by using the typing rules as construction constraints. Each generated program comes paired with its expected type (derived by the reference checker) and its expected value (derived by the reference evaluator). This gives conformance testing at the language level: the compiler is tested against the spec on programs no human wrote.

How it works

Generation proceeds top-down. Hull picks a target type, then works backward through the typing rules to construct a term that inhabits that type. At each choice point (which rule to apply, which subterms to generate), it samples randomly within the space of valid derivations. The result is a well-typed Deep AST term together with a complete typing derivation.

Because the generator uses the same typing rules as the reference checker, every generated program is well-typed by construction. If the compiler rejects one, the compiler has a bug.

Usage

Generate a batch of random programs:

chelis hull generate --count 100

Generate programs targeting a specific type:

chelis hull generate --count 50 --target "Int -> Int"

Each generated program is written to a separate .deep file in the output directory.

Conformance testing

The typical workflow combines generation with comparison:

chelis hull generate --count 100 --out ./generated/
for f in ./generated/*.deep; do
  chelis check "$f" > /tmp/compiler.out
  chelis hull check "$f" > /tmp/spec.out
  diff -q /tmp/compiler.out /tmp/spec.out || echo "DIVERGENCE: $f"
done

This surfaces programs where the compiler and the spec disagree on typing. The same pattern works for evaluation:

for f in ./generated/*.deep; do
  chelis eval "$f" > /tmp/compiler.out
  chelis hull eval "$f" > /tmp/spec.out
  diff -q /tmp/compiler.out /tmp/spec.out || echo "DIVERGENCE: $f"
done

Shrinking

When a divergence is found, Hull can shrink the failing program to a minimal reproducer:

chelis hull shrink failing-program.deep

Shrinking removes subterms while preserving well-typedness and the divergence, producing the smallest program that still triggers the disagreement between spec and compiler.