7.1. Constrained types🔗

A constrained type refines an existing type with a predicate, so that a fact established once travels through the program as part of the type instead of being re-proved at each use. It is declared with a base type, a where predicate, and a witness value that shows the constraint is inhabited.

constrained nat = x: int where x >= 0 witness 0

The property that matters for reducing proof effort is that the fact survives flow through code that knows nothing about it. Consider a polymorphic identity, which returns its argument unchanged for any type T:

// syntax illustrative — generics are still in progress
procedure identity<T>(x: T) returns (r: T) { return x };

procedure usesIdentity() {
  var n: nat := 5;
  var m: nat := identity(n);
  assert m >= 0            // still available: the `nat` constraint survived the round-trip
};

identity is verified once, generically, with no knowledge of nat or its predicate. Yet because the constraint rides along with the type, instantiating T with nat lets the caller recover m >= 0 on the result with no extra annotation or proof at the call site. The fact is neither dropped when the value enters the generic procedure nor re-derived when it leaves. That is what lets constrained types cut proof effort across a whole program: a property proved at one point remains available everywhere the constrained value flows, even through procedures that are entirely agnostic to the constraint.