Implements

From Structure to Implementation

A structure declares what operations exist. An implements block provides the actual definitions:

structure Addable(T) {
    operation add : T × T → T
}

implements Addable(ℝ) {
    operation add(x, y) = x + y
}

implements Addable(ℤ) {
    operation add(x, y) = x + y
}

Full Example: Complex Numbers

// Declare the structure
structure Complex(T) {
    re : ℝ
    im : ℝ
    
    operation add : Complex(T) → Complex(T)
    operation mul : Complex(T) → Complex(T)
    operation conj : Complex(T)
    operation mag : ℝ
}

// Implement the operations (parenthesized type argument required)
implements Complex(ℝ) {
    operation add(z, w) = builtin_complex_add
    operation mul(z, w) = builtin_complex_mul
    operation conj(z) = builtin_complex_conj
    operation mag(z) = sqrt(re(z)^2 + im(z)^2)
}

Parametric Implementations

Implement structures with type parameters:

structure Stack(T) {
    operation push : T → Stack(T)
    operation pop : Stack(T)
    operation top : T
    operation empty : Bool
}

implements Stack(ℤ) {
    operation push = builtin_stack_push
    operation pop = builtin_stack_pop
    operation top = builtin_stack_top
    operation empty = builtin_stack_empty
}

Multiple Implementations

The same structure can have multiple implementations:

structure Orderable(T) {
    operation compare : T × T → Ordering
}

// Natural ordering
implements Orderable(ℤ) {
    operation compare = builtin_int_compare
}

Implementing Extended Structures

When a structure extends another, implement all operations:

structure Monoid(M) {
    operation e : M
    operation mul : M × M → M
}

structure Group(G) extends Monoid(G) {
    operation inv : G → G
}

// Must implement both Monoid and Group operations
implements Group(ℤ) {
    operation e = 0
    operation mul(x, y) = x + y
    operation inv(x) = -x
}

Builtin Operations

Some operations can’t be defined in pure Kleis — they need native code. The builtin_ prefix connects Kleis to underlying implementations:

implements Matrix(m, n, ℝ) {
    operation transpose = builtin_transpose
    operation add = builtin_matrix_add
    operation mul = builtin_matrix_mul
}

When Kleis sees operation add = builtin_add, the builtin_add name is stored as metadata in the type registry. At runtime, operations are dispatched by their semantic names (e.g., plus, add, abs) in the evaluator’s builtin table, not by stripping the builtin_ prefix. The builtin_* names serve as an implementation marker connecting structure declarations to native Rust code.

For Z3 verification, operations are translated using their structure operation names (e.g., plus maps to Z3’s +). The builtin name is not involved in the Z3 path.

This architecture enables:

Performance: Native BLAS for matrix operations
Hardware access: GPUs, network cards, sensors
System calls: File I/O, networking, threading
FFI: Calling existing libraries

The Vision: Hardware as Structures

Imagine:

structure NetworkInterface(N) {
    operation send : Packet → Result(Unit, Error)
    operation receive : Unit → Result(Packet, Error)
    
    axiom delivery : ∀(p : Packet).
        connected → eventually(delivered(p))
}

implements NetworkInterface(EthernetCard) {
    operation send = builtin_eth_send
    operation receive = builtin_eth_receive
}

The axioms define the contract. The builtins provide the implementation. Z3 can verify that higher-level protocols satisfy their specifications given the hardware axioms.

This is how Kleis becomes a universal verification platform — not just for math, but for any system with verifiable properties.

Verification of Implementations

Kleis + Z3 can verify that implementations satisfy axioms:

structure Monoid(M) {
    e : M
    operation mul : M × M → M
    
    axiom identity : ∀(x : M). mul(e, x) = x ∧ mul(x, e) = x
    axiom associative : ∀(x : M)(y : M)(z : M).
        mul(mul(x, y), z) = mul(x, mul(y, z))
}

implements Monoid(String) {
    element e = ""
    operation mul = builtin_concat
}

// Kleis can verify:
// 1. concat("", s) = s for all s ✓
// 2. concat(s, "") = s for all s ✓
// 3. concat(concat(a, b), c) = concat(a, concat(b, c)) ✓

What’s Next?

Learn about Z3 verification in depth!

→ Next: Z3 Verification

The Kleis Manual