Skip to main content

7. SMT Solver Engineering & Stability

1. Introduction: The "SMT Heat" Problem​

Automated verifiers like Sector9 rely on SMT solvers (Z3) to check the validity of Hoare-logic obligations. However, SMT solvers are not "magic boxes." As a protocol grows in complexity—adding more state, more invariants, and more complex data structures—the solver must explore an exponentially increasing search space.

This often leads to SMT Heat: a state where the solver consumes 100% CPU for minutes or hours before timing out (or worse, returning "Unknown"). For DeFi developers, this is a major productivity killer. If verification takes 10 minutes, you can't iterate.

Sector9 employs a variety of SMT Engineering techniques to improve stability and performance. It focuses on reducing "Quantifier Heat" and keeping the generated Viper code solver-friendly. This research analyzes the implementation in src/viper/lower_exp.ml and src/viper/mvir_trigger_helpers.ml.

2. Trigger Inference: Taming the Quantifiers​

The most common cause of solver timeouts is Matching Loops caused by universal quantifiers (forall). To instantiate a forall, Z3 uses Matching Patterns (Triggers). If a trigger is too broad, Z3 instantiates the axiom too many times, leading to a loop.

Sector9 implements a sophisticated Trigger Inference Engine in mvir_trigger_helpers.ml, inspired by the Prusti (Rust) verifier.

Heuristic-Based Selection​

Instead of letting Z3 guess triggers, Sector9's engine analyzes the body of the quantifier and picks the most stable terms:

  1. Priority 1: Access Terms. MutRecArrayElemE, AddrAsRefE, and ArrayLocE. These are specific to data access and are highly stable.
  2. Priority 2: Lookup Terms. ArrayReadE, SeqIndexE, and ArraySnapReadE.
  3. Priority 3: Function Calls. Pure function calls (CallE) and field accesses (FldAcc).

Trigger Coverage​

The engine ensures that the chosen trigger set covers all binders in the quantifier.

let rec loop () =
  (* ... *)
  let best = candidates |> List.map (fun t -> (t, binder_coverage t))
  (* ... pick the term that covers the most uncovered binders *)

By providing explicit, minimal trigger sets, Sector9 reduces the chance of Z3 entering matching loops and can substantially reduce verification time for complex collection proofs (Subject 5).

3. Selective Lowering and "Pure Contexts"​

In lower_exp.ml, Sector9 implements a strict separation between executable code and specification logic through Pure Contexts.

Statement Lifting​

Sector9's source language allows expressions to have side effects (e.g., let x = (a := 1; 2)). If these side effects were translated directly into logic formulas, the solver would have to model the entire heap state inside a simple equality. Sector9's lower_exp.ml rejects statementful expressions in pure contexts:

let reject_statementful_pure_entry (ctxt : ctxt) (e : M.exp) : unit =
  Value_helpers.reject_statementful ~mode:Value_helpers.Pure_context ...

By forcing side effects to be "lifted" to the statement level (Viper assign or call), Sector9 ensures that the logic formulas passed to the SMT solver are purely functional, making them much easier to solve.

Arithmetic Truncation​

Computer arithmetic (fixed-width) is tricky for solvers. Sector9 implements Checked Arithmetic via partial axioms (Subject 5) and uses Truncating Division/Modulus in the lowering phase (trunc_div, trunc_mod). The division/modulus lowering aligns signed arithmetic with runtime behavior; fixed-width overflow is handled separately by checked operations and partial axioms.

4. Domain-Aware Constraints​

The SMT solver treats all Int as infinite-precision mathematical integers. However, Sector9's Nat type is restricted to non-negative values.

If the verifier says forall (n : Int) :: balance[n] >= 0, the solver might try to instantiate n = -1 and get stuck. Sector9 solves this by automatically injecting Domain Constraints:

let domain_constraint_for_binder at (binder, motoko_typ) =
  if is_nat_like_type motoko_typ then
    Some (!!! at (GeCmpE (n, 0)))

When a developer quantifies over a Nat in Sector9, the verifier emits forall n: Int :: n >= 0 ==> ... in Viper. This guides the solver's search space and prevents it from spending effort on values that are outside the source type's domain.

5. Axiom Partiality and "Opaque Stubs"​

Soundness is often at odds with performance. A "Total Axiom" (one that covers all inputs) is easy to use but hard to solve.

Sector9 uses Partial Axioms for its fixed-width arithmetic.

axiom { forall a, b :: a + b <= MAX ==> add(a, b) == a + b }

If the verifier cannot prove a + b <= MAX, the add(a, b) function becomes Uninterpreted (a black box). This prevents the solver from making dangerous assumptions about overflows, while also keeping the "Search Surface" small—the solver only "unwraps" the axiom when it has a proof that it's safe to do so.

6. Evaluation & Comparison​

vs. Solidity (Symbolic Execution)​

Tools like Manticore or Mythril use Symbolic Execution, which explores paths one by one.

  • Solidity: Suffers from "Path Explosion."
  • Sector9: Uses Deductive Verification (Hoare Logic), which uses a single formula for the entire function. Sector9's challenge is "Quantifier Heat," but trigger engineering can make large state spaces more tractable than path-by-path symbolic execution.

vs. Dafny​

Dafny is the "gold standard" for SMT-based verification.

  • Dafny: Often requires developers to manually write {:trigger} annotations to fix performance issues.
  • Sector9: Automates trigger inference. This makes Sector9 much more approachable for "Smart Contract Engineers" who aren't SMT experts.

vs. F* / Lean​

Dependent type systems use proof assistants (interactive).

  • F / Lean:* No timeouts (because a human is helping), but incredibly slow developer experience.
  • Sector9: Aims for the "Push-Button" experience. Its SMT engineering is what makes the "One Codebase, Four Views" goal practical for production.

7. Conclusion​

Sector9's SMT solver engineering is what makes push-button verification practical for the target protocol subset. By automating trigger inference, enforcing pure contexts, and using domain-aware constraints, it aims to keep common DeFi verification jobs fast enough for normal development. For the Internet Computer, where protocol updates are frequent and high-stakes, this stability is part of a secure development lifecycle.

Strengths:

  1. Automation: Trigger inference removes a major source of developer frustration.
  2. Stability: Domain constraints and lifted statements lead to highly predictable solver behavior.
  3. Soundness: Partial axioms provide a "fail-safe" for complex arithmetic.

Weaknesses:

  1. Heuristic Risk: Triggers are still based on heuristics. In rare cases, the engine might miss a necessary trigger, requiring explicit forallWith triggers, helper lemmas, or intermediate assert steps from the developer.
  2. Z3 Dependency: Ultimately, Sector9 is still bound by the performance and bugs of the underlying Z3 solver.