Skip to main content

11. Higher-Order Function Verification

1. Introduction: The Higher-Order Challenge​

In smart contract development, higher-order functions (functions that take other functions as arguments, like map or filter) are essential for abstraction. However, they are notoriously difficult for deductive verifiers:

  • The Callee Problem: When Canister A calls callback(), the verifier doesn't know which function is being called. It cannot "jump" to the callee's source code.
  • The Side-Effect Problem: If a callback modifies state, the verifier must know which state it modifies to maintain sound framing (Subject 2).
  • The Capture Problem: Closures can capture local variables or actor state, creating hidden dependencies.

Sector9 addresses these issues through a Narrow Supported Surface for higher-order logic, combining contract-bearing types with axiomatic dispatch. This research analyzes the implementation in src/viper/ho_contracts.ml and src/viper/callable.ml.

2. Unified Callables: The Ref Abstraction​

In Sector9's Motoko-derived surface, functions, modules, objects, and actors are distinct. In the verification lane, they are unified into the Callable abstraction (callable.ml).

Representation as Function Objects​

Callable identities are represented through Viper references and generated function-object constants. This allows the verifier to treat functions as first-class objects that can be stored in variables or passed as arguments.

type callable_kind = CKFunc | CKObject | CKModule | CKActor

To distinguish between different functions with the same signature, Sector9 generates unique Function Object Constants (Subject 9).

3. Type Contracts: Functional Specifications​

The core of Sector9's higher-order safety is the Type Contract. Sector9 allows contracts on function types:

type Callback = (n : Nat) -> Nat contract {
  requires n > 0;
  ensures result > n;
  reads this.config
};

When a function is used as a Callback, the verifier enforces two obligations:

  1. At the Call Site: The caller must prove the requires clause and must assume the ensures clause after the call.
  2. At the Definition or Coercion: A value flowing into the Callback type must already carry a compatible contract or be checked against one at a supported boundary. Uncontracted named helper coercions remain restricted so hidden effects cannot slip through.

This decouples the caller from the implementation. The verifier only needs to see the Type Contract to reason about the call, solving the "Callee Problem."

4. Contract Enforcement Policy (ho_contracts.ml)​

Sector9 implements a strict enforcement policy to prevent "Impure Leakage."

Rejecting Under-constrained Callbacks​

If a function type has no contract, Sector9 by default assumes it is Pure (no side effects).

let dynamic_module_unknown_effect_msg =
  "dynamic module calls have unknown effects; verified methods must call only pure/trusted targets..."

If a developer attempts to pass a function that modifies state to an uncontracted callback, the verifier rejects it (ImpureNoContracts). This forces the developer to be explicit: either the function is pure, or its effects must be documented in a contract.

Side-Effect Subtyping​

When assigning a function to a contracted type, the verifier checks Effect Inclusion:

if not (String_set.subset actual_modifies expected_modifies) then
  error_contract_effects exp.at info.name_opt ~label:"modifies" ...

The implementation's modifies set must be a subset of the type's modifies set. This ensures that a callback can never "surprise" the system by mutating a field that the caller didn't expect.

5. Axiomatic Dispatch with $apply​

To model the execution of a dynamic call, Sector9 uses Axiomatic Dispatch.

The $apply Domain​

For every function signature, the verifier defines an $apply function.

function $apply$int$int($f: Ref, $arg: Int): Int

If a function literal func(x) { x + 1 } is bound to a variable f, Sector9 emits a Semantic Axiom:

axiom { forall x :: $apply$int$int($func_obj$f(), x) == x + 1 }

This allows the solver to "unwrap" the logic of a specific function if its identity is known, while still allowing for abstract reasoning using the Type Contract if the identity is unknown.

6. Self-Escape and Closure Safety​

Closures are dangerous because they can capture $Self (the actor's state).

Self-Escape Analysis​

The ho_contracts.ml module performs a reachability analysis on free variables.

let func_touches_self (ctxt : Context.ctxt) (pat : M.pat) (body : M.exp) : bool =
  let free = Motoko_walk_free_vars.free_vars ~bound body in
  String_set.exists (fun name -> name_touches_self ctxt name) free

If a function captures $Self, it is marked as SelfBlocked unless it has a Full Contract (including reads/modifies). This prevents "Hidden Reentrancy," where a callback is used to sneakily mutate actor state without the verifier's knowledge.

7. Evaluation & Comparison​

vs. Solidity (Function Pointers)​

Solidity supports function pointers, but they are extremely dangerous as they can point to any code (via assembly). There is no way to specify their effects.

  • Sector9: Uses nominal identity and verifier-enforced contracts so function-pointer calls carry explicit preconditions, postconditions, and effects.

vs. Dafny (Function Specifications)​

Dafny has powerful support for higher-order logic using "Function Specifications" and "Requires/Ensures" clauses.

  • Dafny: Often requires complex "Decreases" clauses for termination proofs of higher-order functions.
  • Sector9: Primarily focuses on Safety and Framing for DeFi. It prioritizes declared effect bounds for callbacks over termination proofs for complex recursive higher-order algorithms.

vs. Move (No Higher-Order Functions)​

Move intentionally excludes higher-order functions to keep its verifier simple and decidable.

  • Move: Forces developers to use flatter, more repetitive code patterns.
  • Sector9: Permits higher-order abstractions but gates them behind strict contract rules. This provides better ergonomics for complex protocols (like pluggable strategies in a DAO) while preserving verifier-enforced permission bounds.

8. Conclusion​

Higher-order function verification in Sector9 is a pragmatic restricted model. By forcing dynamic calls to be mediated by a Type Contract and utilizing Axiomatic Dispatch, Sector9 allows useful abstractions while keeping closure and function-pointer effects explicit. For DeFi, this enables patterns like strategy callbacks or hook modules with proof obligations that those hooks stay within their declared permission bounds.

Strengths:

  1. Decoupling: Type contracts allow reasoning about callbacks without seeing their source.
  2. Safety: Self-escape analysis prevents hidden state mutation via closures.
  3. Efficiency: Axiomatic dispatch is much faster for SMT solvers than complex symbolic execution of dynamic calls.

Weaknesses:

  1. Narrow Surface: Only simple functional postconditions (result == ...) are currently translated into axioms. Complex imperative logic in callbacks still relies purely on the Type Contract.
  2. Annotation Heavy: Developers must write explicit contracts for every higher-order type.