The Decidability Sweet Spot

DTS: A Distinct Formal Category

The Dimensional Type System (DTS) is restricted 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.

Dependent types differ here. A dependent type can encode an arbitrary predicate over values, so checking whether two dependent types are equal may require proving an arbitrary theorem. Dimensional consistency checking is only a comparison of 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 same fragment carries the eBPF target’s admissibility obligations, where the Linux kernel’s own verifier re-derives at load what CCS discharged at design time.

The analogy is to regular expressions and context-free grammars. Regular expressions form their own formal class, with closure properties, recognition algorithms, and applications unlike those of the grammars above them. DTS occupies the analogous position relative to dependent types, a separate formal class that overlaps in expressive power for a specific domain but differs in the computational properties practical tooling depends on: decidability, inference completeness, and runtime cost.

The decidability holds because every quantity in the paragraphs above lives in a finitely-generated free abelian group, where the order of composition never changes the result and consistency reduces to comparing integer vectors. The check stays cheap because composition commutes, and that commutativity holds only inside a boundary. Concurrent work whose crossing order the runtime can observe does not commute, and the group governing its rearrangement is the non-abelian braid group $B_n$, not $\mathbb{Z}^n$. Ordinary code remains inside the abelian interior with no additional obligation. The abelian projection of a crossing, its writhe, stays a Tier 1 quantity decided by the same integer linear algebra, and only observable crossing structure carries a heavier obligation, one discharged by reusing proofs the dual-pass has already produced. The braid as a fourth sheaf is the proposed, non-normative design for that boundary: the sweet spot is the abelian interior, and the non-abelian edge is something we are taking some care to treat appropriately.

Design-Time Verification

Transparent verification is achieved by integrating Z3 directly into CCS to discharge decidable SMT obligations. 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 above maps onto two standard constructions in program verification: weakest-precondition computation for the design-time pass, and Hoare’s consequence rule for the compile-time re-discharge.

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 and the solver derives the precondition. That 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.

Compositionality of the pipeline then 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. That design is deliberately open: any number of compatible sheaves can sit over the same poset and be checked at the same edges, and the non-abelian crossing structure of concurrent work is a proposed fourth such sheaf, assembled by the same dual-pass discharge with a different stalk category.