Modular Verification

Modular verification means verifying components independently rather than as a monolithic whole. This improves verification performance by reducing the scope of each verification task and enables parallel verification of separate modules.

Why Modular Verification Matters

Large actors with many methods can cause verification timeouts. The SMT solver must reason about state, contracts, and interactions for each root it verifies. Modular verification addresses this by:

1. Reducing verification scope: Each module is verified against its contracts, not its callers
2. Enabling parallelism: Independent modules can be verified concurrently
3. Improving cacheability: Unchanged modules don't need re-verification
4. Isolating failures: Contract violations localize to specific boundaries

Approach	Verification Time	Parallelizable	Failure Isolation
Monolithic actor	Slow	No	Poor
Extracted pure helpers	Faster	Yes	Good
Abstract proof-only stubs	Fastest	Yes	Excellent

The Contract Boundary Principle

Modular verification works because the verifier treats function contracts as complete specifications. When verifying a caller:

1. Preconditions are proof obligations at call sites
2. Postconditions are assumptions about the result
3. The callee body is not inlined into the caller's proof

This separation means Module A can rely on Module B's exported contracts instead of re-proving Module B's body at every call site. The imported module still needs to type-check, and you should verify it separately before treating the boundary as established.

Pattern 1: Signature-Only Declarations

Declare ghost abstract functions with contracts but no body. The verifier treats these as temporary specifications for proof-only code:

modular-signature-only.sr9

// Abstract signature-only declarations enable modular verification
// The verifier uses contracts without requiring implementations

module {
  // Abstract signature-only: contract specified, no body
  public ghost abstract func abs(x : Int) : Nat
    requires true;
    ensures result >= 0;
    ensures x >= 0 ==> result == x;
    ensures x < 0 ==> result == -x;

  // Proof-only code can use abs() via its contract.
  public ghost func distance(a : Int, b : Int) : Nat
    ensures result >= 0;
  {
    abs(a - b)
  };
}

How it works: The abs function is marked ghost abstract and has no body. The verifier generates an uninterpreted Viper function with the specified contracts. When the proof-only distance helper calls abs, it:

• Must establish any preconditions (none here)
• May assume the postconditions hold for the result

When to use:

• Verification-Driven Development for ghost helpers and lemmas
• External mathematical facts you trust but don't want to prove yet
• Breaking circular dependencies in proof-only code

Signature-only declarations are not runtime implementations. Runtime code must call functions with bodies; keep declaration-only helpers in ghost/proof-only code. Use abstract for verification-driven placeholders and trusted only for permanent assumptions.

Pattern 2: Trusted Functions

Mark functions as trusted to skip body verification while keeping contracts:

modular-trusted-boundary.sr9

// Trusted functions create verification boundaries
// The body is not verified; contracts are assumed

module {
  // Trusted: body not verified, postcondition assumed
  public trusted func fastHash(data : Nat) : Nat
    requires data < 1_000_000;
    ensures result < 256;
  {
    // Complex implementation the verifier skips
    data % 256
  };

  // Verified caller: must establish precondition
  public func hashIfSmall(n : Nat) : ?Nat
    ensures result == null or n < 1_000_000;
  {
    if (n < 1_000_000) {
      ?fastHash(n)  // Precondition satisfied
    } else {
      null
    }
  };
}

How it works: The trusted modifier tells the verifier:

• Assume the postcondition result < 256 holds
• Skip verification that the body actually achieves this
• Verify that callers satisfy the precondition data < 1_000_000

When to use:

• Complex algorithms that are correct but hard to verify
• Performance-critical code with hand-optimized implementations
• Third-party code you've audited but can't modify

Soundness warning: Trusted functions are assumptions. If the body doesn't actually satisfy the contract, callers may rely on false guarantees. Keep the trusted surface small and auditable; see the trusted computing base design notes.

Pattern 3: Import Chains

Imported modules give callers a contract boundary. Callers reason from exported contracts, not implementation details:

Library Module

modular-mathlib.sr9

// Library module verified independently
// Callers rely on contracts, not implementation details

module MathLib {
  public pure func clamp(x : Nat, lo : Nat, hi : Nat) : Nat
    requires lo <= hi;
    ensures result >= lo;
    ensures result <= hi;
    ensures x < lo ==> result == lo;
    ensures x > hi ==> result == hi;
    ensures x >= lo and x <= hi ==> result == x;
  {
    if (x < lo) { lo }
    else if (x > hi) { hi }
    else { x }
  };

  public pure func max(a : Nat, b : Nat) : Nat
    ensures result >= a;
    ensures result >= b;
    ensures result == a or result == b;
  {
    if (a >= b) { a } else { b }
  };
}

Caller Module

modular-import-contract.sr9

// Verification works across module boundaries via contracts
// Each module is verified independently

import MathLib "./modular-mathlib.sr9";

persistent actor {
  var total : Nat = 0;

  public func addClamped(x : Nat, max : Nat) : async Nat
    modifies total
    entry_requires max > 0;
    requires max > 0;
    ensures result <= max;
    ensures total == old(total) + result;
  {
    // MathLib.clamp's contract guarantees result <= max
    let clamped = MathLib.clamp(x, 0, max);
    total += clamped;
    clamped
  };
}

How it works: When verifying TokenActor:

1. MathLib.clamp's body is not inlined into the actor method proof
2. Only the contract is used: ensures result <= hi
3. The caller's proof uses this contract to establish result <= max

When to use: Always structure code this way. Separate concerns into modules with clear contracts.

Pattern 4: Verification-Driven Development

Write proof-helper contracts first, verify ghost callers against stubs, implement later:

modular-vdd-stubs.sr9

// Verification-Driven Development for proof helpers: stubs first, implementation later
// Write contracts, verify proof-only callers, then implement

module {
  // Stage 1: Abstract ghost helper stubs with contracts only
  public ghost abstract func lineTotal(qty : Nat, price : Nat) : Nat
    requires true;
    ensures result == qty * price;

  public ghost abstract func applyDiscount(amount : Nat, rate : Nat) : Nat
    requires rate <= 100;
    ensures result <= amount;
    ensures result == amount - (amount * rate / 100);

  // Stage 2: Verified proof-only function using stubs
  public ghost func computeInvoice(qty : Nat, price : Nat, discountRate : Nat) : Nat
    requires discountRate <= 100;
    ensures result <= qty * price;
  {
    let subtotal = lineTotal(qty, price);
    applyDiscount(subtotal, discountRate)
  };

  // Stage 3: Implement stubs later (not shown)
  // The caller verification already passed using contracts
}

The VDD workflow:

1. Declare stubs: Abstract ghost functions with contracts, no bodies
2. Write ghost callers: Proof-only functions or lemmas that use the stubs
3. Verify callers: They verify against stub contracts
4. Implement stubs: Fill in bodies that satisfy contracts
5. Verify stubs: Confirm implementations meet contracts

Why this helps: You can verify the proof design before committing to implementations. Runtime callers still need helpers with bodies.

Pattern 5: Extract Pure Helpers

Move complex logic into pure functions that can be verified independently:

modular-split-monolith.sr9

// Before: Monolithic actor with slow verification
// After: Extracted pure helpers enable parallel verification

module TokenMath {
  // Verified independently - fast
  public pure func validateTransfer(balance : Nat, amount : Nat) : Bool
    ensures result == (amount <= balance);
  {
    amount <= balance
  };

  public pure func computeFee(amount : Nat, basisPoints : Nat) : Nat
    requires basisPoints <= 10000;
    ensures result <= amount;
  {
    amount * basisPoints / 10000
  };
};

persistent actor TokenActor {
  var balances : [var Nat] = [var];

  // Actor methods use pure helpers
  // Verification leverages helper contracts
  public func transfer(from : Nat, to : Nat, amount : Nat) : async Bool
    modifies balances
    entry_requires from < balances.size() and to < balances.size();
    requires from < balances.size();
    requires to < balances.size();
  {
    if (TokenMath.validateTransfer(balances[from], amount)) {
      balances[from] -= amount;
      balances[to] += amount;
      true
    } else {
      false
    }
  };
}

How it works:

• TokenMath module contains pure helpers with contracts
• TokenActor uses these helpers, relying on their contracts
• Each component verifies faster than the combined whole

Splitting guidelines:

• Extract validation logic into pure predicates
• Move calculations into pure functions
• Keep actor methods focused on state transitions

Diagnosing Modular Verification Opportunities

Signs you need modularization:

• Verification times out on large actors
• Adding unrelated methods slows down existing verification
• Similar logic is duplicated with slight variations

Check verification times:

time XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify large-actor.mo

If verification takes more than 30 seconds, consider extracting modules.

Identify hot spots:

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --viper --deterministic large-actor.mo > output.vpr

Look for methods with many assertions, quantifiers, or array operations. These are extraction candidates.

Performance Comparison

Before	After	Improvement
1 actor, 20 methods, 45s	4 modules, 60s total but parallel	4x with parallel verification
1 file with 10 helpers	Helpers in separate module	Each module verifies in <10s
Trusted inline code	Explicit trusted boundary	Clear soundness scope

Modular Verification Checklist

1. Extract pure helpers - Move calculations and predicates to separate modules
2. Use abstract signature-only stubs only in proof code - Runtime code needs helpers with bodies
3. Mark trusted code explicitly - Don't hide assumptions in implementations
4. Verify imports independently - Each module should verify on its own
5. Minimize cross-module state - Prefer immutable data passing over shared state
6. Document contract boundaries - Make it clear what each module guarantees
7. Test modules in isolation - Verification tests should cover each module separately

See Also

• The trusted Modifier - Detailed trusted function semantics
• Signature-Only Declarations - Abstract placeholders and trusted bodyless assumptions
• Pure Functions - Side-effect free helpers
• Frame Conditions - What contracts guarantee about unchanged state
• Trigger Management - Related quantifier performance issues

Summary

• Modular verification breaks large verification tasks into independent components
• Abstract signature-only declarations let you verify proof-only callers before implementing functions
• Trusted functions create explicit boundaries where the verifier assumes contracts
• Import chains verify each module independently against its contracts
• Verification-Driven Development uses abstract proof-only stubs to validate proof design before implementation
• Extracting pure helpers enables parallel verification and faster iteration
• Contract boundaries are the key mechanism: callers use contracts, not implementations