Strengthening Preconditions

When verification fails because the verifier cannot prove a callee's precondition at a call site, you need to strengthen preconditions to rule out impossible inputs.

The Problem

A precondition failure looks like this:

[1] Precondition might not hold
  Precondition n > 0 might not hold at this call site.
  method: divide
  at: math.sr9:15:12
  hint:
    - Guard the call or strengthen the callee requires.

This means the caller cannot prove that n > 0 when calling divide. The error is at the call site, not inside the callee.

Debugging Strategy

When you encounter a precondition failure:

Identify the callee's requirement: What condition does the callee expect?
Examine the caller's context: What do you know at the call site?
Choose a fix strategy: Add a guard, strengthen the caller's precondition, or refine the callee.

Fix Strategy 1: Strengthen the Caller's Precondition

The most common fix is to add a requires clause to the caller that implies the callee's requirement. If the caller is an exported actor method, also add matching entry_requires guards for caller-controlled conditions.

strengthen-caller-pre.sr9
// Example: Strengthening the caller's precondition

module {
  // Callee requires x > 0
  public pure func safeDivide(x : Nat, y : Nat) : Nat
    requires x > 0;
    requires y > 0;
    ensures result == x / y;
  {
    x / y
  };

  // WRONG: caller has no precondition - verification fails
  // public func badCaller(n : Nat) : Nat {
  //   safeDivide(n, 2)  // Error: cannot prove n > 0
  // };

  // CORRECT: caller's precondition implies callee's requirement
  public pure func goodCaller(n : Nat) : Nat
    requires n > 0;  // Strengthened: now implies safeDivide's requires x > 0
    ensures result == n / 2;
  {
    safeDivide(n, 2)  // OK: n > 0 satisfies x > 0
  };
}

The caller now requires n > 0, which implies the callee's requires x > 0. Verification succeeds because the caller's precondition matches or exceeds what the callee needs.

When to use: When the condition should be the caller's responsibility. This pushes the obligation up the call chain.

Fix Strategy 2: Add a Guard Before the Call

If the callee's precondition may not always hold, add a conditional guard:

strengthen-callee-guard.sr9
// Example: Adding a guard before the call

module {
  // Callee requires positive input
  public pure func process(x : Nat) : Nat
    requires x > 0;
    ensures result == x * 2;
  {
    x * 2
  };

  // Caller handles both cases with a guard
  public pure func safeProcess(n : Nat) : Nat
    ensures n > 0 ==> result == n * 2;
    ensures n == 0 ==> result == 0;
  {
    if (n > 0) {
      // Inside this branch, the verifier knows n > 0
      process(n)  // OK: guard establishes precondition
    } else {
      // Handle the case where precondition would fail
      0
    }
  };
}

The if statement establishes the callee's precondition within that branch. The verifier knows that inside the if, the condition holds.

When to use: When the call should only happen conditionally. This is defensive programming - you handle the case where the precondition fails.

Fix Strategy 3: Strengthen Division Guards

Division and modulo require explicit non-zero guards. Logical requires clauses are collected for proof, so the important part is that the non-zero fact is present. For exported methods, place executable entry_requires guards before any later entry_requires expression that divides by the same value, so runtime entry checks fail cleanly instead of evaluating a division by zero first.

strengthen-division.sr9
// Example: Division guards

module {
  // WRONG: missing guard for b
  // public pure func missingGuard(a : Nat, b : Nat) : Nat
  //   ensures result == a / b;
  // { a / b };

  // CORRECT: logical guard rules out division by zero
  public pure func guarded(a : Nat, b : Nat) : Nat
    requires b != 0;
    requires a / b > 0;
    ensures result == a / b;
  {
    a / b
  };

  // Multiple divisors - guard each one
  public pure func multiDivisor(a : Nat, b : Nat, c : Nat) : Nat
    requires b != 0;     // Guard for b
    requires c != 0;     // Guard for c
    requires a / b > c;  // Now safe to use both
    ensures result == a / b - c;
  {
    a / b - c
  };
}

For nested division, guard each divisor. A logical guard may appear with the other proof preconditions, while executable entry guards should be ordered from primitive safety facts to derived expressions:

public func nested(a : Nat, b : Nat, c : Nat) : async Nat
  entry_requires b != 0;
  entry_requires c != 0;
  entry_requires b / c != 0;
  requires b != 0;
  requires c != 0;
  requires b / c != 0;
  ensures result == a / (b / c);
{
  a / (b / c)
}

Key rule: include a logical non-zero guard for every divisor. On exported methods, write the matching entry_requires guard before any executable entry_requires clause that performs the division.

Strengthening Across Call Chains

When functions call other functions, preconditions must account for the entire chain:

strengthen-chain.sr9
// Example: Strengthening preconditions across call chains

module {
  // Inner function requires x < 1000
  public pure func increment(x : Nat) : Nat
    requires x < 1000;
    ensures result == x + 1;
  {
    x + 1
  };

  // WRONG: x < 1000 is not strong enough for two calls
  // public pure func badDouble(x : Nat) : Nat
  //   requires x < 1000
  // {
  //   let first = increment(x);      // OK: x < 1000
  //   increment(first)               // Error: first = x + 1, might be 1000
  // };

  // CORRECT: account for the intermediate value
  public pure func doubleIncrement(x : Nat) : Nat
    requires x < 999;   // Strengthened: x + 1 < 1000 for second call
    ensures result == x + 2;
  {
    let first = increment(x);      // OK: x < 999 implies x < 1000
    increment(first)               // OK: first = x + 1 < 1000
  };

  // Even stronger for triple increment
  public pure func tripleIncrement(x : Nat) : Nat
    requires x < 998;   // x + 2 < 1000 for third call
    ensures result == x + 3;
  {
    let first = increment(x);
    let second = increment(first);
    increment(second)
  };
}

The doubleIncrement function needs x < 999 (not just x < 1000) because after the first increment, the value becomes x + 1, which must still satisfy < 1000 for the second call.

Pattern: When chaining calls, trace through the values and compute what the outer function must require.

Bounds Preconditions for Numeric Types

Fixed-width types like Nat64 require overflow prevention:

strengthen-bounds.sr9
// Example: Bounds preconditions for fixed-width types

persistent actor {
  var counter : Nat64 = 0;

  private func incrementChecked() : Nat64
    modifies counter
    requires counter < 18446744073709551615;  // Max Nat64 - 1
    ensures result == counter;
    ensures counter == old(counter) + 1;
  {
    counter += 1;
    counter
  };

  // Precondition prevents overflow
  public func increment() : async Nat64
    modifies counter
    entry_requires counter < 18446744073709551615;
    requires counter < 18446744073709551615;
    ensures result == counter;
    ensures counter == old(counter) + 1;
  {
    incrementChecked()
  };

  // Add by arbitrary amount - need stronger guard
  public func addAmount(amount : Nat64) : async Nat64
    modifies counter
    entry_requires counter <= 18446744073709551615 - amount;
    requires counter <= 18446744073709551615 - amount;  // Room for addition
    ensures result == counter;
    ensures counter == old(counter) + amount;
  {
    counter += amount;
    counter
  };

  // Caller must ensure room exists
  public func safeIncrement() : async ?Nat64
    modifies counter
    ensures counter < 18446744073709551615 ==> result != null;
  {
    if (counter < 18446744073709551615) {
      // Guard establishes precondition
      ?incrementChecked()
    } else {
      null
    }
  };
}

For signed types, guard both bounds:

public func decrement(x : Int8) : async Int8
  entry_requires x > -128;  // Prevent underflow
  requires x > -128;
  ensures result == x - 1;
{
  x - (1 : Int8)
}

Using Counterexamples to Find Weak Preconditions

Run with --counterexample to see concrete values that violate the precondition:

sector9 --verify --counterexample file.sr9

This requires the Viper server backend. If model extraction is unavailable, use --json or --toon to inspect the failing call site first.

Output:

Counterexample summary
  entry:
    n = 0
  call site: process(n)
    requires n > 0 might not hold

This tells you exactly which input value causes the failure. Use this to understand what precondition is missing.

Common Patterns

Array Bounds

public func get(arr : [Nat], i : Nat) : async Nat
  entry_requires i < arr.size();  // Prevent out-of-bounds access
  requires i < arr.size();
  ensures result == arr[i];
{
  arr[i]
}

Option Unwrapping

public func unwrap(opt : ?Nat) : async Nat
  entry_requires opt != null;  // Guard against null
  requires opt != null;
{
  switch opt {
    case (?v) v;
    case null { 0 };  // Unreachable but required for type
  }
}

Structural Constraints

public func between(x : Int, lo : Int, hi : Int) : async Bool
  entry_requires lo <= hi;  // Structural validity
  requires lo <= hi;
  ensures result == (x >= lo and x <= hi);
{
  x >= lo and x <= hi
}

Invariant Preservation

persistent actor {
  var value : Int = 0;
  invariant value >= 0;

  // Precondition ensures invariant is maintained
  public func setValue(newVal : Int) : async ()
    entry_requires newVal >= 0;  // Matches invariant
    requires newVal >= 0;
    modifies value
    ensures value == newVal;
  {
    value := newVal;
  }
}

Diagnosis Checklist

When a precondition fails:

Check the callee's requires: What does the callee expect?
Check the caller's requires: Does the caller's precondition imply the callee's?
Check for guards: Is there an if that establishes the condition?
Check for intermediate operations: Did an operation change the value between establishing the condition and the call?
Run with --counterexample: What concrete value fails?

Multiple Preconditions

When a callee has multiple requires clauses, all must be satisfied:

public func process(x : Nat, y : Nat) : async Nat
  entry_requires x > 0;
  entry_requires y > 0;
  entry_requires x + y < 1000;
  requires x > 0;
  requires y > 0;
  requires x + y < 1000;
  ensures result == x * y;
{
  x * y
}

public func caller(a : Nat, b : Nat) : async Nat
  entry_requires a > 0;
  entry_requires b > 0;
  entry_requires a + b < 1000;
  requires a > 0;        // Satisfies first
  requires b > 0;        // Satisfies second
  requires a + b < 1000; // Satisfies third
  ensures result > 0;
{
  process(a, b)
}

Multiple requires clauses are conjoined (AND-ed). The caller must establish all of them.

Pure Helpers Inside Contracts

A precondition failure can also come from a pure helper used inside an ensures, invariant, or loop:invariant. The verifier proves the helper's own requires clauses as separate obligations at that contract position.

pure func safeSub(a : Nat, b : Nat) : Nat
  requires b <= a;
  ensures result == a - b;
{
  a - b
}

public func charge(balance : Nat, fee : Nat) : async Nat
  entry_requires fee <= balance;
  requires fee <= balance;
  ensures result == safeSub(balance, fee);
{
  balance - fee
}

If fee <= balance is missing, the postcondition does not become conditional. Verification fails because the contract calls safeSub without proving its precondition. When source mapping is available, the diagnostic points at the contract position and may name safeSub as the helper whose requires clause was not established.

When Not to Strengthen

Sometimes the error indicates a real bug:

Logic error: You are calling the function with genuinely invalid inputs
Wrong function: You should be calling a different function
Missing validation: You need runtime validation before this point

Do not blindly add preconditions - understand why the condition fails first.

Summary

Precondition failures occur at call sites when the caller cannot prove the callee's requirements
Strategy 1: Add requires to the caller that implies the callee's requirement
Strategy 2: Add a guard (if) before the call to conditionally establish the requirement
Strategy 3: For division, include non-zero guards; order executable entry_requires guards before derived divisions
Pure helper preconditions are checked even when the helper call appears in a postcondition or invariant
For call chains, outer functions need stronger preconditions to account for intermediate operations
Use --counterexample to find the concrete input that fails
Common patterns: array bounds, null guards, overflow prevention, structural constraints
For exported methods, mirror caller-controlled requires with entry_requires

The Problem​

Debugging Strategy​

Fix Strategy 1: Strengthen the Caller's Precondition​

Fix Strategy 2: Add a Guard Before the Call​

Fix Strategy 3: Strengthen Division Guards​

Strengthening Across Call Chains​

Bounds Preconditions for Numeric Types​

Using Counterexamples to Find Weak Preconditions​

Common Patterns​

Array Bounds​

Option Unwrapping​

Structural Constraints​

Invariant Preservation​

Diagnosis Checklist​

Multiple Preconditions​

Pure Helpers Inside Contracts​

When Not to Strengthen​

Summary​