The Decidability Sweet Spot

This article is part of the Transparent Verification series. It builds on From Double Annotation to Discovery to explain the algebraic foundation that makes zero-annotation verification decidable.

DTS: A Distinct Formal Category

The fundamental advantage of the Dimensional Type System (DTS) is its restriction to a specific algebraic niche that general dependent type systems cannot exploit.

A dimensional type system assigns to each numeric value a dimension drawn from a finitely generated free abelian group. The base dimensions (length, time, mass, temperature, electric current, luminous intensity, amount of substance) generate the group under multiplication, with integer exponents. Formally, let $\mathcal{D} = \mathbb{Z}^n$ be the dimension space. Each dimension $d \in \mathcal{D}$ is a vector of integer exponents:

Dimensional consistency of an arithmetic expression reduces to linear algebra over $\mathbb{Z}$: addition requires operand dimensions to be equal; multiplication adds exponent vectors; division subtracts them; exponentiation scales them. These operations are closed in $\mathbb{Z}^n$ and decidable in $O(n)$ per operation.

This is the critical distinction from dependent types. A dependent type can encode an arbitrary predicate over values. Checking whether two dependent types are equal may require proving an arbitrary theorem. Dimensional consistency checking requires comparing two integer vectors, a constant-time operation per base dimension.

General dependent type systems have decidable type checking when the developer supplies the type, but type inference and proof search are undecidable, which is why production systems built on them require manual annotations, fuel limits, and timeout heuristics during SMT solving. Because DTS constraints reduce to linear algebra over integers, they map to one of Z3’s most well-studied, guaranteed-decidable logic fragments: QF_LIA. CCS is designed to ask Z3 to solve a bounded system of linear equations. Z3 resolves these QF_LIA obligations in microseconds, guaranteeing the polynomial-time inference required for real-time language server responses.

The analogy is to regular expressions and context-free grammars. Regular expressions are a distinct formal class with distinct closure properties, distinct recognition algorithms, and distinct practical applications. DTS occupies an analogous position relative to dependent types: a distinct formal class that happens to overlap in expressive power for a specific domain but differs in every computational property that matters for practical tooling.

Design-Time Verification: The Transparent Z3 Partner

Integrating Z3 directly into CCS to handle decidable SMT proof obligations is what makes transparent verification possible. The verification process is designed to happen continuously at design time. As the developer types, Lattice will traverse the PSG and invoke Z3 in the background. The NTU simultaneously acts as the proof apparatus for Z3, deriving proof obligations from the PSG’s structure. Every arithmetic operation in the PSG produces a Z3 assertion, governed by the fixed rules of dimensional algebra. The developer writes zero proof code.

The Gravitational Force Example

Consider a developer writing a standard gravitational force calculation:

let computeForce mass1 mass2 distance =
    let g = 6.674e-11 // compiler knows this is m^3 * kg^-1 * s^-2
    g * mass1 * mass2 / (distance * distance)

The developer provides no proofs and no dependent-type annotations. Here is what CCS is designed to do silently as it builds the PSG nodes:

Step 1: Variable Assignment. CCS assigns integer dimension vectors to every variable. In SMT-LIB2 format, this would generate:

(declare-const d_m1_kg Int)
(declare-const d_m2_kg Int)
(declare-const d_dist_m Int)

Step 2: Operation Constraints (“Natural Bounds”). When CCS processes distance * distance, it knows multiplication means adding dimensional exponents. It would automatically generate the Z3 constraint:

;; d(denom) = 2 * d(distance)
(assert (= d_denom_m (+ d_dist_m d_dist_m)))

Step 3: Division Constraints. For the final division, CCS knows division means subtracting exponents:

;; d(return) = d(numerator) - d(denom)
(assert (= d_ret_m (- d_num_m d_denom_m)))

Step 4: Boundary Constraints. If the function is called with typed arguments such as mass1 : float<kg>, mass2 : float<kg>, and distance : float<m>, CCS treats those as hard assertions:

(assert (= d_m1_kg 1))
(assert (= d_m2_kg 1))
(assert (= d_dist_m 1))

Z3 then verifies if the inferred constraints (naturally derived from the code operations) match the explicit boundary constraints provided by the developer. The result:

• d_g resolves to m^3 · kg^-1 · s^-2 (the gravitational constant’s natural dimension)
• Return dimension: m^3 · kg^-1 · s^-2 + kg + kg - 2·m = kg · m · s^-2 = newtons

Because this is just basic integer addition and subtraction over a bounded system, Z3 solves it instantly and returns SAT. CCS then stamps the PSG node with its proof certificate. The proof cert is generated before MLIR lowering, with the syntactic footprint of standard F#.

Dimensionally Polymorphic Inference

Without any type annotations at all, the function remains dimensionally polymorphic. The DTS inference assigns dimension variables 'd_g, 'd_m1, 'd_m2, 'd_dist and propagates constraints through the expression tree via extended Hindley-Milner unification. The inferred return type is float<'d_g + 'd_m1 + 'd_m2 - 2 * 'd_dist>, a parametric family. Only when the function is called with concrete dimensional types does unification resolve the full system.

A function let scale factor value = factor * value infers type float<'d1> -> float<'d2> -> float<'d1 * 'd2> without any annotation. The inference is complete (every dimensionally consistent program can be typed without annotation), principal (the inferred type is the most general), and decidable (the constraint system is finite and the solution algorithm terminates). These properties are shared with standard Hindley-Milner inference and are not shared with dependent type inference in general.

Deprecating the “Double Annotation”

If a developer were to attempt a dependent-type-style annotation in Clef, something like [<Requires(dim_a = dim_b + dim_c)>], the DTS would make it redundant. CCS would have already generated that exact constraint from the arithmetic operations in the code.

If a developer explicitly annotates a boundary (the “push model”), like (m1: float<kg>), CCS treats that as a hard assertion in Z3: (assert (= d_m1_kg 1)). Z3 then verifies whether the inferred constraints naturally derived from the code operations match the explicit boundary constraints. If they conflict, Z3 returns UNSAT, and Lattice will highlight the exact line of code where the physics broke down.

By making the NTU responsible for translating standard arithmetic operators into SMT linear equations, the developer is isolated from theorem proving entirely.

From UNSAT Cores to Actionable Diagnostics

Because the SMT proofs are resolved at design time within the saturated PSG, Lattice will be able to exploit them for precise diagnostics.

When Z3 returns UNSAT for a set of constraints, the plan is for Lattice to produce an unsat core, the exact subset of conflicting constraints. CCS translates that mathematical core back into the specific PSG edges that caused the conflict.

If an engineer attempts to accumulate gradients of dimension $\langle \text{newtons} / \text{meters} \rangle$ with $\langle \text{joules} / \text{seconds} \rangle$, Lattice will highlight the exact operation and explain the physical impossibility, backed by a formal mathematical proof, all without leaving the editor.

Closure Under Differentiation

This capability extends naturally to auto-differentiation. The dimensional algebra is closed under differentiation: if $f : \mathbb{R}^{\langle d_1 \rangle} \to \mathbb{R}^{\langle d_2 \rangle}$, then:

The gradient of a loss function with dimension $\langle \text{loss} \rangle$ with respect to a parameter with dimension $\langle d \rangle$ carries dimension $\langle \text{loss} \cdot d^{-1} \rangle$. This follows from the abelian group structure: differentiation is division in the dimensional algebra, and division is closed in $\mathbb{Z}^n$. The inference algorithm extends to auto-differentiation graphs without modification. In a physics-informed model where the loss function includes terms with physical units (force residuals in newtons, energy conservation violations in joules), DTS would verify that gradient accumulation respects dimensional consistency, decidably, without annotation, and with no runtime overhead for the verified properties.

The Hoare Logic View

The mechanism described above has a precise reading in the language of program verification, and stating it in those terms makes the dual-pass architecture’s role clearer.

The design-time Z3 pass is weakest-precondition computation in Dijkstra’s sense. Each PSG node carries a postcondition (the dimensional constraint the node’s output must satisfy), and Z3 works backward through the constraint chain to compute the weakest precondition that suffices for the postcondition to hold. Hoare’s assignment axiom and sequential composition rule are the local steps; the QF_LIA decision procedure discharges each step in microseconds. The engineer writes the program; the solver derives the precondition; the inference is decidable, complete, and principal because the underlying logic is QF_LIA.

The compile-time MLIR re-discharge at each lowering pass is the consequence rule. Hoare’s consequence rule states that if $P' \to P$, $\{P\}\, C\, \{Q\}$, and $Q \to Q'$, then $\{P'\}\, C\, \{Q'\}$. At each lowering, the lowering pass is the command $C$ that transforms one program representation into the next; the framework’s obligation is to verify that the precondition established at the higher dialect implies the precondition required at the lower dialect, and that the postcondition delivered by the lower dialect entails the postcondition the higher dialect promised. Both implications are themselves QF_LIA statements, and Z3 discharges them. The dual-pass is the consequence rule applied at every lowering boundary.

This framing has a useful consequence: the compositionality of the entire pipeline reduces to local checks at each lowering, with no global re-verification required at the binary stage. The compilation sheaf design document makes that compositionality categorical, treating the design-time and compile-time passes together as the witnessing mechanism for a global section over the compilation poset.

The next article extends the transparent verification model from dimensional constraints to memory safety.