Static Contract Verification

Calor supports static contract verification using Microsoft's Z3 SMT (Satisfiability Modulo Theories) solver. This enables proving contracts at compile time, potentially eliding runtime checks for proven contracts.

Overview

When you write contracts in Calor:

§F{f001:Square:pub}
  §I{i32:x}
  §O{i32}
  §Q (>= x 0)
  §S (>= result 0)
  §R (* x x)
§/F{f001}

The compiler can use Z3 to prove that the postcondition (>= result 0) always holds when the precondition (>= x 0) is satisfied. This is mathematically provable: the square of a non-negative number is always non-negative.

Enabling Static Verification

Use the --verify flag when compiling:

calor -i MyModule.calr -o MyModule.g.cs --verify

Verification Spectrum

Contracts fall into four categories after verification:

Proven

The contract is mathematically proven to always hold. The runtime check can be safely elided.

// PROVEN: Postcondition statically verified: (result >= 0)

Unproven

Z3 couldn't determine if the contract always holds (timeout, complexity limit, or non-linear arithmetic). The runtime check is preserved.

Disproven

Z3 found a counterexample showing the contract can be violated. A warning is emitted with the counterexample, and the runtime check is preserved.

warning Calor0702: Postcondition may be violated in function 'BadFunc'.
  Counterexample: x=0, b=1

Unsupported

The contract contains constructs Z3 doesn't support (function calls, strings, floating-point). The runtime check is silently preserved.

Supported Constructs

Z3 verification supports:

Supported types: i32, i64, bool

Unsupported: Function calls, strings, floating-point, arrays, objects

How It Works

The verification process for postconditions:

1. Declare all parameters as symbolic Z3 variables
2. Assume all preconditions hold
3. Assert the negation of the postcondition
4. Check satisfiability:
   • UNSAT: No counterexample exists → Proven
   • SAT: Found counterexample → Disproven
   • UNKNOWN: Timeout or too complex → Unproven

This approach proves correctness by showing there's no way for the contract to be violated when preconditions are met.

Timeouts

Z3 verification has a 5-second timeout per function. Complex contracts with non-linear arithmetic may timeout and be marked as "Unproven".

Limitations

No Function Call Support

Contracts referencing other functions cannot be verified:

§S (> (strlen s) 0)  ; Unsupported - function call

Integer Only

Floating-point contracts aren't verified due to Z3's floating-point theory complexity.

No Array Support

Array operations and loop invariants are not supported.

Bounded Verification

Z3 uses arbitrary-precision integers, so it doesn't model 32-bit overflow. A contract proven correct in Z3 could theoretically fail at runtime due to integer overflow.

Best Practices

Keep Contracts Simple

Simple arithmetic and comparison contracts verify quickly:

§Q (>= x 0)
§S (>= result 0)

Separate Concerns

Split complex contracts into multiple simpler ones:

; Instead of:
§S (and (>= result 0) (< result 100))

; Use:
§S (>= result 0)
§S (< result 100)

Accept Unproven Contracts

Not all contracts can be statically proven. An "Unproven" result doesn't mean the code is wrong—it means Z3 couldn't prove it within time limits.

Comparison with Runtime-Only Enforcement

Static verification complements runtime checking—it doesn't replace it. Unproven and unsupported contracts still have runtime checks.

What Calor Is Not

Calor is not a proof assistant like LEAN, Isabelle, or Rocq. The distinction matters:

No Proofs Required

In LEAN, proving a function returns a positive number requires explicit proof:

theorem sqrt_positive (x : ℝ) (h : x ≥ 0) : √x ≥ 0 := by
  exact Real.sqrt_nonneg x

In Calor, you declare the contract and Z3 handles verification automatically:

§F{f001:Sqrt}(x: f64) -> f64
  §Q (>= x 0.0)
  §S (>= result 0.0)
  (* x x)
§/F{}

If Z3 can't prove it, the runtime check remains. Your code compiles and runs safely.

Lightweight by Design

Calor's verification is deliberately bounded:

• 5-second timeout per contract (configurable via --verification-timeout)
• Arithmetic and boolean logic (not arbitrary math)
• Graceful degradation to runtime checks

This is a feature, not a limitation. Verification never blocks your build indefinitely, and you don't need expertise in formal methods to benefit from it.

Z3 Installation

Z3 is bundled with the Calor compiler via the Microsoft.Z3 NuGet package. No separate installation is required.

If Z3 native libraries are missing on your platform, the compiler will:

1. Log an informational message
2. Skip static verification
3. Continue compilation normally with all runtime checks

Verification Caching

Z3 verification results are automatically cached to disk. When you recompile a file with unchanged contracts, the compiler retrieves cached results instead of re-running Z3. This provides:

• Faster incremental builds: Unchanged contracts verify in milliseconds instead of seconds
• Reduced CI load: Build servers benefit from cached results across runs
• Deterministic results: Same contract always produces same verification outcome

The cache is keyed by a SHA256 hash of the contract expression and parameter types. When you modify a contract, its hash changes, and the cache misses—ensuring correctness.

To disable caching (e.g., for debugging), use --no-cache. To clear the cache, use --clear-cache.

Beyond Contracts: Refinement Types

Contracts verify behavior — preconditions and postconditions on function boundaries. Refinement types extend this to type-level constraints: instead of asserting (>= x 0) as a precondition, you declare the parameter as §I{i32:x} | (>= # INT:0) and the constraint becomes part of the type itself.

The obligation engine is an evolution of the assume-negate-check pattern described above:

1. Generation — The compiler creates verification obligations for every refined parameter and §PROOF statement
2. Solving — Each obligation goes through the same Z3 pipeline: assume preconditions, negate the condition, check satisfiability
3. Guard Discovery — For failed obligations, the engine discovers the simplest guard that would discharge them, validated by Z3
4. Policy — Configurable policies (default, strict, permissive) control whether failures are errors, warnings, or runtime guards

Where contracts are function-level assertions, refinement types are type-level invariants that propagate across function boundaries. A parameter typed Port (an i32 between 1 and 65535) carries its constraint everywhere it flows — no manual validation at each call site.

• Refinement Types Reference
• Dependent Types Tutorial

See Also

• Contracts in Calor
• Compile Command
• Z3 Prover