The trusted Modifier

The trusted modifier marks a deliberate verification boundary: callers must prove the function's preconditions, and the verifier assumes its postconditions without proving the implementation.

Overview

Sometimes you need the verifier to accept a function's contract without proving the body. The trusted modifier tells Sector9: assume this function's ensures clauses hold when its requires clauses are met, but do not generate proof obligations for the implementation.

This is useful for:

• Complex mathematical functions that are difficult to verify directly
• External code, runtime APIs, or core-library wrappers with known behavior
• Performance-critical code where the executable body is tested but not verified
• Long-lived proof assumptions that should be visible in the trusted base

For temporary proof scaffolding, prefer abstract declarations. trusted should communicate that the assumption is intentional.

Syntax

The trusted keyword appears before func in the function header:

public trusted func name(params) : ReturnType
  requires precondition;
  ensures postcondition;
{
  body
}

Trusted functions must still expose a spec surface:

• At least one requires and ensures clause (use requires true / ensures true if needed)
• reads / modifies if an impure trusted function is inside an actor

This keeps the trusted boundary explicit for callers. The body is still parsed and type-checked, but the Viper proof translation treats the function as a contract boundary instead of verifying the body statements.

Basic Example

trusted-basic.sr9

// Basic trusted function - body is not verified, contract is assumed
module {
  public trusted func double(x : Nat) : Nat
    requires x < 1000;
    ensures result == x * 2;
  {
    x * 2
  };

  // Verified caller relies on trusted function's contract
  public func useDouble(n : Nat) : Nat
    requires n < 1000;
    ensures result == n * 2;
  {
    double(n)
  };
}

In this example:

• double is a trusted function with a postcondition result == x * 2
• The verifier does NOT check that the body satisfies this postcondition
• useDouble is verified normally and can rely on double's postcondition

What Gets Verified vs Assumed

Aspect	Verified	Assumed
Preconditions at call sites	Yes	-
Postconditions hold	-	Yes
Body implements contract	-	Yes
Type correctness and syntax	Yes	-
Actor footprints for impure trusted helpers	Yes	-

The verification boundary:

1. Callers must satisfy preconditions - The verifier checks that requires clauses hold at every call site
2. Postconditions are assumed - After a call, the verifier assumes all ensures clauses are true
3. Body proof is skipped - the source body is still checked as Sector9 code, but Viper does not prove it against the postconditions

Caller Responsibilities

Callers must still establish preconditions before calling a trusted function:

trusted-caller.sr9

// Verified function calling trusted function
module {
  public trusted func safeDivide(a : Nat, b : Nat) : Nat
    requires b > 0;
    ensures result == a / b;
  {
    a / b
  };

  // Verified caller establishes precondition, uses postcondition
  public func average(x : Nat, y : Nat) : Nat
    ensures result == (x + y) / 2;
  {
    safeDivide(x + y, 2)  // 2 > 0 is trivially true
  };
}

The average function verifies successfully because:

• It calls safeDivide(x + y, 2)
• The precondition b > 0 is satisfied since 2 > 0 is trivially true
• The postcondition result == (x + y) / 2 is assumed, matching average's own postcondition

Precondition Violations Are Still Detected

The verifier rejects calls that violate a trusted function's preconditions:

trusted-precondition-fail_unsat.sr9

// Verification fails: caller does not satisfy trusted function precondition
module {
  public trusted func requiresPositive(x : Nat) : Nat
    requires x > 10;
    ensures result >= x;
  {
    x + 5
  };

  // ERROR: n might be <= 10, violating the precondition
  public func badCaller(n : Nat) : Nat
    ensures result >= n;
  {
    requiresPositive(n)  // Verification fails here
  };
}

The verifier reports an error because badCaller cannot guarantee n > 10. Trusted does not mean "trust every call" - it only means the callee implementation is outside the proof.

Multiple Contract Clauses

Trusted functions support multiple requires and ensures clauses:

trusted-complex.sr9

// Trusted function with multiple contract clauses
module {
  public trusted func clamp(x : Nat, lo : Nat, hi : Nat) : Nat
    requires lo <= hi;
    requires x <= 10000;
    ensures result >= lo;
    ensures result <= hi;
    ensures (x >= lo and x <= hi) ==> result == x;
  {
    if (x < lo) { lo }
    else if (x > hi) { hi }
    else { x }
  };

  // All postconditions are assumed without verification
  public func boundedValue(n : Nat) : Nat
    requires n <= 10000;
    ensures result >= 0;
    ensures result <= 100;
  {
    clamp(n, 0, 100)
  };
}

All postconditions are assumed simultaneously when the preconditions are met.

Combining with pure

You can combine trusted with pure to create trusted pure functions. This enables recursive specification helpers that ordinary verified pure functions do not support:

trusted-pure.sr9

// Pure trusted function for complex math
module {
  // Complex calculation assumed correct - allows recursion
  pure trusted func factorial(n : Nat) : Nat
    requires n <= 12;
    ensures result >= 1;
    ensures n == 0 ==> result == 1;
  {
    if (n == 0) { 1 }
    else { n * factorial(n - 1) }
  };

  // Use in contracts
  public func computeFactorial(n : Nat) : Nat
    requires n <= 12;
    ensures result == factorial(n);
  {
    factorial(n)
  };
}

Regular pure functions cannot be recursive because the verifier treats their definitions as transparent specification code. Marking a recursive pure function as trusted makes the contract the verification boundary instead.

Actor State and Footprints

An impure trusted function in an actor must declare its state footprint:

private trusted func bump() : Nat
  reads x
  modifies x
  requires true;
  ensures result == old(x) + 1;
{
  x += 1;
  x
};

Without reads or modifies, verification rejects the trusted actor helper. The verifier cannot inspect the body to infer the boundary, so the trusted signature must state what actor fields it may read or write. Use pure trusted only when the function has no state effects.

Comparison with Related Features

Feature	Access State	Modify State	Use old()	Recursive	Body Proved
pure func	No	No	No	No	Yes
lemma	With declared footprints when needed	With declared footprints when needed	Yes	Supported as proof calls	Yes
trusted func	Yes, with footprints in actors	Yes, with footprints in actors	In postconditions	Yes	No
Regular func	Yes	Yes	N/A	Yes	Yes

Use trusted when:

• You need a function's contract assumed without proof
• The function is too complex to verify directly
• You need recursive pure functions

Use lemmas when:

• You want to establish proof facts that ARE verified
• You need old() in a verified context
• The proof can be expressed as calls, assertions, and local ghost reasoning

When to Use Trusted Functions

Appropriate uses:

• Mathematical functions with known correctness (e.g., standard library functions)
• Wrapping external calls where you trust the implementation
• Complex algorithms verified by other means (testing, formal proofs elsewhere)
• Bootstrapping: proving easier properties first, trusting harder ones temporarily
• Core-library boundaries where the executable behavior is backed by runtime implementation and tests

Avoid when:

• The function is simple enough to verify directly
• You can express the property as a lemma instead
• The contract is speculative or untested

Soundness Implications

Every trusted function is part of your trusted base. If a trusted function's contract is wrong, the verifier may prove false properties about your code. Keep the trusted base minimal:

• Prefer verification over trust when feasible
• Test trusted functions thoroughly
• Document why each function is trusted
• Review trusted contracts carefully during code review
• Track trusted declarations separately from temporary abstract proof obligations

See The Trusted Base for more on soundness boundaries.

Summary

• trusted marks functions whose contracts are assumed, not verified
• Preconditions are still checked at call sites
• Postconditions are assumed true after calls
• The function body is parsed and type-checked, but its proof obligations are skipped
• Impure trusted actor helpers must declare reads or modifies
• Combine with pure to enable recursive helper functions
• Keep trusted functions minimal to maintain verification soundness

Related Topics

• Signature-only declarations for abstract placeholders and trusted bodyless declarations
• Abstract functions for VDD stubs that should be refined later
• Footprints for trusted actor state boundaries
• Runtime limitations for what cannot ship as executable code