Nitpick Design by Contract and Formal Verification

Nitpick is distinct from other bare-metal languages because it ships with formal mathematical verification integrated directly into its compiler pipeline, powered by the Z3 SMT solver. This enables you to prove your code’s correctness at compile time, matching the safety guarantees of languages like Ada/SPARK.

1. Value Constraints: limit<Rules>

Nitpick allows you to define constraints on value ranges called Rules. You can then bind these rules to variables using the limit<RuleName> syntax.

// 1. Define a rule for an integer
Rules<int32>:r_positive = { $ > 0i32 };

func:main = int32() {
    // 2. Bind the rule to a variable
    limit<r_positive> int32:x = 5i32;
    exit 0i32;
};

When you compile with --verify, the compiler’s integrated Z3 solver will mathematically prove that the assigned value (5i32) satisfies the constraint ($ > 0). If it cannot prove it statically (for instance, reading user input), it will enforce the check at runtime. If the runtime check fails, it triggers the failsafe handler.

1.1 Rules Composition and Subsumption

Rules can reference other Rules via limit<OtherRule>, creating a constraint hierarchy:

Rules<int32>:r_positive = { $ > 0i32 };
Rules<int32>:r_small_positive = { limit<r_positive>, $ < 100i32 };
// r_small_positive requires: $ > 0 AND $ < 100

The Z3 solver can prove that one Rules subsumes another (e.g., r_small_positive implies r_positive), enabling safe narrowing at call sites.

1.2 Rules and Borrow Checker Integration (v0.66.6)

When limit<Rules>-constrained variables are used as array indices for mutable borrows, the Z3 solver can prove index disjointness to eliminate false-positive aliasing errors:

Rules<int32>:EvenIdx = { $ % 2i32 == 0i32 };
Rules<int32>:OddIdx  = { $ % 2i32 == 1i32 };

func:update = int32(limit<EvenIdx> int32:i, limit<OddIdx> int32:j, int32[100]:arr) {
    $$m int32:a = arr[i];   // mutable borrow at even index
    $$m int32:b = arr[j];   // Z3 proves i != j → borrows are disjoint
    pass(a + b);
};

2. Function Contracts: requires and ensures

Nitpick implements classic Design by Contract (DbC) on function boundaries.

• requires: Preconditions that must be true when the function is called.
• ensures: Postconditions that the function guarantees will be true when it returns. (Use the special result keyword to reference the return value).

func:divide = int32(int32:a, int32:b) 
    requires b != 0i32 
    ensures result > 0i32 
{
    pass 10i32; // Hardcoded for example
};

2.1 Static Verification vs Runtime Enforcement

When you compile with the --verify-contracts flag, the compiler translates these contracts into Z3 assertions to prove they are mathematically valid. Currently, the compiler verifies that the contracts are individually satisfiable.

If you don’t use the static verifier, Nitpick automatically enforces these contracts at runtime.

2.2 The Result<T> Intercept

One of the most powerful features of Nitpick’s DbC implementation is how it interacts with the type system. If a function declares a requires clause, Nitpick implicitly changes its return type to a Result<T>.

If a caller violates the precondition at runtime, the function immediately intercepts execution and returns a Result error rather than crashing or triggering the failsafe. This heavily intertwines contract programming with Nitpick’s sticky error propagation system, forcing the caller to explicitly unwrap or handle potential contract violations using raw, drop, or .is_error.

func:main = int32() {
    // Because `divide` has a `requires` contract, it returns a Result<int32>!
    // We must unwrap it with `raw` or handle the potential failure.
    int32:y = raw divide(10i32, 2i32);
    
    exit 0i32;
};

3. Loop Invariants (invariant)

Loop constructs (loop, while, till, when) support an invariant clause specifying conditions that must hold at every iteration boundary.

func:sum_range = int32(int32:n)
    requires n > 0i32
    ensures result >= 0i32
{
    int32:total = 0i32;
    int32:i = 0i32;
    while (i < n) invariant total >= 0i32, i >= 0i32 {
        total = total + 1i32;
        i = i + 1i32;
    };
    pass(total);
};

When compiled with --verify-contracts, the Z3 solver verifies the inductive step: if the invariant holds at the start of an iteration and the loop condition is true, then the invariant still holds at the end of the iteration.

4. Verification Levels

The --verify-level=N flag controls verification depth: