Skip to main content

Contract Subtyping and Escaping Functions

Function values are only safe in verification when their behavior is summarized by contracts. This page explains how contract subtyping works and when contracts are required.

Why Contracts Matter for Function Values​

When you pass a function as a value (higher-order) or store it in data structures, the verifier often cannot see the body at the call site. The only sound summary is the type contract:

  • Prove requires before the call
  • Assume ensures after the call
  • Apply reads/modifies for framing

Without a contract, function values are treated as pure. Impure function values are rejected unless the callback type supplies a contract.

Subtyping Rules for Contracts​

Contracts are checked by logical implication:

  • requires is contravariant
  • ensures is covariant

A function value can be used at a contract type when its precondition is no stronger than the expected precondition and its postcondition is at least as strong as the expected postcondition.

type Weak = (x : Nat) -> Nat contract {
  requires x > 0;
  ensures result >= x;
};

type Strong = (x : Nat) -> Nat contract {
  requires x > 0;
  ensures result > x;
};

let strong : Strong = ...;
let weak : Weak = strong;  // OK

If the implication does not hold, the verifier rejects the coercion. This prevents callers from losing required input checks or assuming result facts the function does not guarantee.

Escaping Functions and $Self​

When a function value can escape (returned, stored, or passed out), the verifier must know its effects on actor state.

  • If a function may touch $Self, its type contract must include full reads/modifies along with requires/ensures.
  • trusted functions must still provide these contracts before they can escape as values.

This ensures callers get an explicit effect summary, even when the body is not verified.