SMT Refinements

Paradox uses Z3 (an SMT solver) to verify validation constraints at compile time. This catches logical errors before any code is generated.

What Gets Verified

Overconstrained Detection

If the constraints on a type are logically contradictory, the type has no valid inhabitants. Paradox detects this:

type Person
  age: Integer

valid Person
  age > 21
  age < 18

[error 22]: Overconstrained validation for Person

  7 │ valid Person
  8 │   age > 21
  9 │   age < 18

     │ Note: These constraints make constructing Person impossible

The SMT solver proves that no value of age can simultaneously satisfy age > 21 and age < 18.

Arithmetic Contradictions

Complex arithmetic relationships are also checked:

type BadRectangle
  width: Integer
  height: Integer
  area: Integer

valid BadRectangle
  width > 0
  height > 0
  area = width * height
  area < 0

[error 22]: Overconstrained validation for BadRectangle

     │ Note: These constraints make constructing BadRectangle impossible

If width > 0 and height > 0, then area = width * height > 0, so area < 0 is impossible.

Refinement Violations

When constructing a wrap type, the value must provably satisfy the wrap’s constraint:

wrap PositiveInt: Integer

valid PositiveInt
  unwrap > 0

badZero: PositiveInt
  PositiveInt 0

[error 40]: Refinement type constraint violated

   7 │   unwrap > 0
     •   ╰╸ valid PositiveInt is defined here

  15 │   PositiveInt 0
     •   ╰╸ this value does not satisfy the constraint: unwrap > 0

     │ Hint: The value must satisfy: unwrap > 0

Arithmetic Safety

The solver catches cases where arithmetic might violate constraints:

wrap StockCount: Integer

valid StockCount
  unwrap >= 0

decrementStock: current:StockCount. quantity:Integer. StockCount
  StockCount (current.unwrap - quantity)

[error 40]: Refinement type constraint violated

  10 │   StockCount (current.unwrap - quantity)
     •   ╰╸ this value does not satisfy the constraint: unwrap >= 0

     │ Hint: The value must satisfy: unwrap >= 0

The solver recognizes that current.unwrap - quantity might be negative when quantity > current.unwrap.

Union Variant Violations

Per-variant validation is also checked:

union Status
  approved: Integer
  rejected
  pending

valid Status
  approved: amount. amount > 0

badApproved: Status
  Status.approved: 0

The value 0 does not satisfy amount > 0.

What Gets Checked at Compile Time

Wrap constructors: WrapType value checks value against the wrap’s constraint
Overconstrained types: all constraints on a product type are checked for satisfiability
Function return types: if a function returns a refined type, the body is checked
Conditional branches: refinement checks track through if-then-else
Pattern match branches: each branch is checked independently

Limitations

External functions: If a function’s body calls another function, the solver may not be able to verify the result satisfies a constraint (it doesn’t inline function bodies)
Complex expressions: Very complex arithmetic or deeply nested logic may time out
Runtime values: Values that depend on runtime input cannot be verified at compile time — the refinement still generates runtime validators

How It Works

During type checking, when Paradox encounters a wrap constructor WrapType expr, it:
1. Collects the constraint from valid WrapType
2. Encodes the expression and constraint as an SMT formula
3. Asks Z3 whether the constraint can be violated
4. If Z3 finds a counterexample, reports a refinement violation error
For overconstrained detection:
1. Collects all constraints on a type
2. Asks Z3 whether there exists any value satisfying all constraints simultaneously
3. If unsatisfiable, reports the type as overconstrained

Prerequisites

SMT verification requires Z3 on your PATH. In the Nix development shell (nix develop), Z3 is provided automatically.

Without Z3, Paradox still works but skips compile-time refinement checking. Runtime validators are always generated regardless.