Skip to content
Weltenwanderer Weltenwanderer

ADR-004: Two-Level Verification Architecture

Context

Verification can be applied at two different artifacts: the .ddd source model and the generated TypeScript code. These serve different purposes. A single verification layer that operates on generated code cannot catch model errors without running a generator first. Conversely, a single layer on the model cannot verify that the generator preserves semantics.

The question is how to structure verification so that both concerns are addressed without conflating them.

Decision

Two independent verification levels:

Level 1 — Domain Verification (platform-independent)

Operates on the AST before code generation. Checks include:

  • Exhaustiveness: every Command × State pair is covered by a decide branch
  • Evolve totality: every Event × State pair is handled by an evolve branch
  • Guard consistency: no two require guards are simultaneously satisfiable with contradictory outcomes
  • Postcondition derivability: ensure conditions follow from the evolve definition via the fusion law
  • Dead code detection: unreachable decide branches
  • Terminal state enforcement: no commands accepted in terminal states

Rules specified in packages/language/specs/validation-*.allium.

Level 2 — Generator Verification

Operates on generated TypeScript output. Uses property-based testing (fast-check) to assert that the generated code preserves the semantics guaranteed by Level 1. Each generator target has its own Level 2 test suite.

Rules specified in packages/generator-emmett/specs/codegen.allium.

Consequences

Positive

  • Level 1 provides fast feedback before any code is produced; domain errors surface at model authoring time.
  • Adding a new generator target requires only Level 2 tests; Level 1 is reused unchanged.
  • Level 1 and Level 2 can be developed and maintained independently.
  • Property-based testing at Level 2 provides higher confidence than example-based tests for the combinatorial space of generated code.

Negative

  • Level 1 checks are bounded by decidability: Turing-complete flow compositions cannot be fully verified statically (see specs/theory.allium for the three-layer decidability boundary).
  • Two verification passes add latency to the compile pipeline; generator verification requires running fast-check suites.
  • Maintaining semantic equivalence between Level 1 rules and Level 2 property definitions requires discipline.