Pure Function Restrictions

Pure functions are side-effect free mathematical functions. This page documents all restrictions, their error codes, and workarounds.

Why Restrictions Exist

The verifier can inline pure function bodies at local call sites. Across source imports, runtime pure/spec helpers are contract-only by default unless written as inline pure func. For local body reasoning to be sound, pure functions must:

• Always return the same output for the same inputs
• Have no observable side effects
• Translate to expression-style verifier definitions
• Not depend on mutable state

These properties let the verifier treat f(x) as identical wherever it appears in the same proof context.

Complete Restriction Reference

No State Access (M0317)

Pure functions cannot read actor or module fields.

persistent actor {
  var count : Nat = 0;

  pure func bad() : Nat {
    count  // ERROR M0317
  }
}

Error message: pure function cannot access field 'count'; pure functions can only use their parameters and other pure functions

Why: State can change between calls. If f() reads a field, two calls to f() could return different values, breaking referential transparency.

Workaround: Pass state as a parameter:

persistent actor {
  var count : Nat = 0;

  pure func addTo(c : Nat, amount : Nat) : Nat {
    c + amount
  }

  public func increment(n : Nat) : async Nat
    modifies count
    ensures count == addTo(old(count), n);
  {
    count := addTo(count, n);
    count
  }
}

No State Modification (M0240)

Pure functions cannot assign to variables, update mutable fields, or declare mutable variables.

module {
  var total : Nat = 0;

  pure func tick() : Nat {
    total := total + 1;  // ERROR M0240
    total
  }
}

Error message: pure or lemma functions may not write state

Why: Side effects break the mathematical function model. A function that modifies state is not a function in the mathematical sense.

Workaround: Return a new value instead of mutating:

pure func increment(n : Nat) : Nat {
  n + 1  // Returns new value, no mutation
}

No Await (M0240)

Pure functions cannot perform async operations.

pure func bad() : async Nat {
  await someCall()  // ERROR M0240
}

Error message: pure or lemma functions may not await

Why: Await suspends execution and introduces non-determinism. The result depends on external state and timing.

Workaround: Use a regular function for async operations, then call pure functions on the result:

pure func process(value : Nat) : Nat { value * 2 }

public func fetch() : async Nat {
  let raw = try { await externalCall() } catch (_) { 0 };
  process(raw)  // Pure function processes the result
}

No Assertions or Traps (M0240)

Pure functions cannot contain assert, runtime:assert, or trap.

pure func validate(x : Nat) : Nat {
  assert x > 0;  // ERROR M0240
  x
}

pure func check(x : Nat) : Nat {
  runtime:assert x > 0;  // ERROR M0240
  x
}

pure func guard(x : Nat) : Nat {
  trap (x == 0);  // ERROR M0240
  x
}

Error message: pure or lemma functions may not contain assertions or traps (assert, trap, runtime:assert, Prim.trap, Runtime.trap)

Why: Assertions and traps can abort execution, which is an effect. A mathematical function always returns a value.

Workaround: Use requires clauses to express preconditions:

pure func safeDivide(a : Nat, b : Nat) : Nat
  requires b > 0;
{
  a / b
}

The caller must prove the precondition. The verifier rejects calls that violate it.

No Recursion

Pure functions cannot be directly or mutually recursive. This is checked at verification time.

pure func factorial(n : Nat) : Nat {
  if (n == 0) { 1 }
  else { n * factorial(n - 1) }  // ERROR at verification
}

Error message: recursive pure functions are not supported by the verifier; use a method/lemma or mark as trusted

Mutual recursion is also rejected:

pure func isEven(n : Nat) : Bool {
  if (n == 0) { true }
  else { isOdd(n - 1) }  // ERROR
}

pure func isOdd(n : Nat) : Bool {
  if (n == 0) { false }
  else { isEven(n - 1) }  // ERROR
}

Why: The verifier inlines local pure function bodies. Recursion would create infinite inlining, and termination proofs are not implemented.

Workaround: Use a lemma for recursive mathematical properties, or use pure trusted func when you need to assume a recursive definition:

// Pure function for the closed form
pure func triangular(n : Nat) : Nat {
  n * (n + 1) / 2
}

// Lemma establishes the inductive step
public lemma triangularStep(i : Nat) : ()
  ensures triangular(i) + (i + 1) == triangular(i + 1);
{
}

// Use in loop invariant
public func sumTo(n : Nat) : async Nat
  ensures result == triangular(n);
{
  var acc : Nat = 0;
  var i : Nat = 0;
  while (i < n) {
    loop:invariant acc == triangular(i);
    triangularStep(i);
    i += 1;
    acc += i;
  };
  acc
}

No old() in Contracts (M0313)

Pure functions cannot use old() in their own requires or ensures clauses.

pure func bad(x : Nat) : Nat
  ensures result == old(x);  // ERROR M0313
{
  x
}

Error message: old() expression can only be used in ghost context (ghost let/block, verification assertions, or lemma)

Why: Pure functions have no notion of "previous state" since they don't access state. The value of x never changes within the function.

Workaround: Use old() in the enclosing method's contract:

pure func doubled(x : Nat) : Nat {
  x * 2
}

persistent actor {
  var balance : Nat = 100;

  public func deposit(amount : Nat) : async Nat
    modifies balance
    ensures balance == old(balance) + doubled(amount);  // old() here is valid
  {
    balance += doubled(amount);
    balance
  }
}

No Statement Loops in Verifier-Visible Bodies

Pure bodies are intended to translate as specification expressions. A body that contains an imperative while or for loop may pass ordinary parsing and type checking when it has no side effects, but Viper translation rejects it as a statementful pure expression.

pure func bad(x : Nat) : Nat {
  while (false) {
  };
  x
}

Error message: pure expression contains statementful source expression in spec context

Workaround: Use expression-level conditionals and pattern matching for small helpers. For iterative reasoning, put the loop in the verified method and state a loop:invariant. For reusable math facts, use a lemma or a trusted pure helper with an explicit contract.

No Array Indexing in Named Pure Helpers (M0317)

Named pure functions cannot index into arrays.

pure func getFirst(arr : [Nat]) : Nat {
  arr[0]  // ERROR M0317
}

Error message: pure function cannot index arrays; pure functions can only use their parameters and other pure functions

Why: Array indexing requires heap access. Arrays are mutable structures with heap permissions, which complicates the inlining model. Quantifier predicates in specification contexts commonly mention arr[i], but that is different from defining a reusable named pure helper that indexes an array.

Workaround: Pass the element as a parameter, or use the array in the enclosing method:

pure func process(element : Nat) : Nat {
  element * 2
}

public func processFirst(arr : [Nat]) : async Nat
  entry_requires arr.size() > 0;
  requires arr.size() > 0;
{
  process(arr[0])  // Index in method, pass to pure function
}

No Impure Calls (M0240)

Pure functions can only call other pure functions.

func impure() : Nat { 42 }

pure func bad() : Nat {
  impure()  // ERROR M0240
}

Error message: impure call 'impure' inside pure/lemma function

Why: Calling an impure function would allow side effects to leak in.

Workaround: Make the called function pure, or restructure to call impure functions in the enclosing method:

pure func helper() : Nat { 42 }

pure func good() : Nat {
  helper()  // OK: helper is pure
}

Higher-Order Calls Require Pure Parameters

Pure functions may call function parameters when the passed function value is pure (or has an effect-free contract). Impure function values are rejected with M0360.

pure func apply(f : Nat -> Nat, x : Nat) : Nat {
  f(x)  // OK when f is pure/lemma
}

func impure(x : Nat) : Nat { x + 1 };
apply(impure, 5);  // ERROR M0360

Error message: higher-order function values must be pure

Why: Calling an impure function would allow side effects to leak in.

Workaround: Mark the function value pure, or call it outside the pure function (possibly via a contract-typed callback):

pure func process(value : Nat) : Nat {
  value * 2
}

public func useWithCallback(f : Nat -> Nat, x : Nat) : async Nat {
  let intermediate = f(x);  // Call in method
  process(intermediate)     // Pure function on result
}

Allowed Operations

Pure functions can use:

Operation	Example
Parameters	x, a + b
Arithmetic	x * 2, a / b, n % m
Comparisons	x > 0, a == b, n != 0
Logical operators	a and b, not x, a or b
Implication	a ==> b, a <==> b
Conditionals	if (x > 0) { x } else { -x }
Local let bindings	let y = x + 1; y * 2
Pure function calls	double(x), max(a, b), Runtime.moduleHash()
Record construction	{ x = 1; y = 2 }
Record field access	point.x, config.timeout
Tuple construction	(a, b, c)
Variant construction	#red, #some(42)
Pattern matching	switch (v) { case (#a) 1; case (#b) 2 }

Error Summary

Error Code	Message	Cause
M0317	"pure function cannot access field"	Reading actor/module field
M0317	"pure function cannot index arrays"	Array element access
M0240	"pure or lemma functions may not await"	Async operation
M0240	"pure or lemma functions may not write state"	Assignment or var declaration
M0240	"pure or lemma functions may not contain assertions or traps"	assert, trap, runtime:assert
M0240	"impure call inside pure/lemma function"	Calling impure function
M0313	"old() expression can only be used in ghost context"	old() in pure function contract
(verifier)	"recursive pure functions are not supported"	Direct or mutual recursion
(translator)	"pure expression contains statementful source expression"	while or for in a pure body

Comparison with Related Features

Feature	Access State	Modify State	Use old()	Recursive	Use in Specs
pure func	No	No	No	No	Yes
lemma func	Via params	No	Yes	No	Proof steps
pure trusted func	No	No	No	Trusted	Yes
Regular func	Yes	Yes	N/A	Yes	No

Use lemma when you need proof steps, ghost reasoning, or old() in the helper body. Use pure trusted func when you need to assume correctness without inlining the body. Use pure for simple mathematical helpers that can be inlined.

Summary

• Pure functions are mathematical: same inputs always produce same outputs
• Cannot access or modify state, await, assert, trap, recurse, use statement loops in verifier-visible bodies, or use old()
• Cannot index arrays or call impure functions
• Use requires for preconditions instead of assertions
• Pass state as parameters instead of reading fields
• Use old() in enclosing method contracts, not pure function contracts
• Use lemmas for recursive mathematical properties

Related Topics

• The pure modifier for the basic mental model
• Pure functions in contracts for reusable predicates
• Assertions restrictions for why assert, runtime:assert, and trap are rejected
• Imported contract helpers for inline pure across source imports
• Loop invariants for moving iterative reasoning out of pure helpers