Skip to main content

Contracts in Function Types

When a function is passed as a value (higher-order), the verifier cannot always see its body at the call site. Function type contracts provide a summary the verifier can rely on.

Call-Site Reasoning​

For a call through a function value, the verifier:

  1. Proves the type contract's requires holds
  2. Assumes the type contract's ensures after the call
module {
  public func run(
    f : (x : Nat) -> Nat contract {
      requires x > 0;
      ensures result > x;
    }
  ) : Nat {
    f(1)  // Requires x > 0, then assumes result > 1
  };
}

If the target is unknown (dynamic module values, higher-order parameters, imported helpers, or escaping closures), the type contract is the only reliable summary.

Effects and Framing​

Type contracts can include reads and modifies. These are authoritative for framing:

persistent actor {
  var counter : Nat = 0;

  public func apply(
    f : (n : Nat) -> Nat contract {
      requires n >= 0;
      ensures result == n;
      modifies counter
    }
  ) : async Nat
    modifies counter
  {
    let before = counter;
    let out = f(0);
    // counter may have changed because f modifies it
    out
  };
}

If a type contract says modifies counter, the verifier treats counter as potentially changed after the call, even if the implementation is pure.

When a callback type includes a contract, the passed function value must also carry a contract so the verifier can check its effect summary.

When You Must Use Type Contracts​

Use function type contracts when you:

  • Pass impure functions as values
  • Store functions in variables or data structures
  • Accept dynamic module values with callable fields
  • Let trusted functions escape as values

Without a contract type, higher-order calls are treated as pure: the passed value must be pure (or have an effect-free contract). Impure callbacks therefore require contract-typed parameters.

Restrictions​

Type contracts follow normal contract rules:

  • No await in contract expressions
  • No old() in requires
  • Only result is allowed in ensures

Contracts in types are verification-only; they do not add runtime checks.