Skip to main content

The pure Modifier

The pure modifier declares a function as side-effect free, enabling its use in verification specifications like contracts and invariants.

Basic Syntax​

pure func double(x : Int) : Int {
  x * 2
}

The pure keyword appears before func. Pure functions can use their parameters, immutable locals, fields of parameter values, and other pure or trusted-pure helpers. They cannot read actor/module state, declare mutable locals, modify state, await, assert, trap, or produce side effects.

What Pure Functions Mean​

Pure functions are mathematical functions: given the same inputs, they always return the same output. The verifier uses this property to reason about specifications.

pure func max(a : Int, b : Int) : Int {
  if (a > b) { a } else { b }
}

persistent actor {
  var value : Int = 0;

  public func clampedSet(x : Int) : async ()
    modifies value
    ensures value == max(0, x);
  {
    value := max(0, x);
  }
}

Because max is pure, the verifier knows max(0, x) in the ensures clause equals max(0, x) in the body.

Declaring Pure Functions​

In Modules​

module Math {
  public pure func abs(x : Int) : Int {
    if (x < 0) { -x } else { x }
  }

  public pure func min(a : Int, b : Int) : Int {
    if (a < b) { a } else { b }
  }

  public pure func clamp(x : Int, lo : Int, hi : Int) : Int {
    max(lo, min(x, hi))
  }
}

Pure functions can be private or public. Public pure functions can be called from other modules in contracts.

In Actors​

persistent actor {
  var balance : Int = 100;

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

  public func addDoubled(amount : Int) : async Int
    modifies balance
    ensures result == old(balance) + doubled(amount);
  {
    balance := balance + doubled(amount);
    balance
  }
}

Pure functions in actors cannot access actor fields. They operate only on their parameters.

Pure Functions with Contracts​

Pure functions can have requires and ensures clauses:

pure func safeSub(a : Int, b : Int) : Int
  requires a >= b;
  ensures result == a - b;
{
  a - b
}

pure func safeDivide(a : Int, b : Int) : Int
  requires b > 0;
  ensures result * b <= a;
{
  a / b
}

When you call a pure function, including from another contract clause, the verifier checks its preconditions at that call site.

Calling Pure Functions​

Pure Calling Pure​

Pure functions can call other pure functions:

pure func square(x : Int) : Int {
  x * x
}

pure func sumOfSquares(a : Int, b : Int) : Int {
  square(a) + square(b)
}

pure func quadruple(x : Int) : Int {
  double(double(x))  // Nested pure calls
}

Pure in Regular Functions​

Regular functions can call pure functions:

persistent actor {
  var counter : Int = 0;

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

  public func addTwice(n : Int) : async Int
    modifies counter
    ensures counter == old(counter) + doubled(n);
  {
    counter += doubled(n);
    counter
  }
}

What Pure Functions Cannot Do​

Pure functions are restricted to ensure referential transparency.

Cannot Access State​

persistent actor {
  var total : Int = 0;

  // WRONG: accesses actor field
  pure func bad() : Int {
    total  // ERROR: pure function cannot access field 'total'
  }

  // CORRECT: take state as parameter
  pure func good(t : Int) : Int {
    t
  }
}

Cannot Modify State​

module {
  var counter : Nat = 0;

  // WRONG: modifies module state
  pure func tick() : Nat {
    counter := counter + 1;  // ERROR: pure or lemma functions may not write state
    counter
  }
}

Cannot Use Assertions or Traps​

// WRONG: contains assert
pure func bad1(x : Nat) : Nat {
  assert x > 0;  // ERROR: pure or lemma functions may not contain assertions
  x
}

// WRONG: contains trap
pure func bad2(x : Nat) : Nat {
  trap (x == 0);  // ERROR: pure or lemma functions may not contain assertions or traps
  x
}

// WRONG: contains runtime:assert
pure func bad3(x : Nat) : Nat {
  runtime:assert x > 0;  // ERROR
  x
}

Cannot Await​

// WRONG: async operations not allowed
pure func bad() : async Int {
  await someCall()  // ERROR: pure or lemma functions may not await
}

Cannot Use Statement-Style Loops​

// WRONG: statement loop in a pure body
pure func bad(x : Nat) : Nat {
  while (false) {
  };
  x
}

Pure bodies used by the verifier must translate as specification expressions. Use conditionals, pattern matching, small algebraic helpers, lemmas, or trusted pure helpers instead of imperative loops.

Cannot Be Recursive​

// WRONG: direct recursion
pure func factorial(n : Nat) : Nat {
  if (n == 0) { 1 }
  else { n * factorial(n - 1) }  // ERROR: recursive pure functions not supported
}

// WRONG: mutual recursion
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) }
}

Use a lemma or pure trusted func for recursive specifications.

Cannot Use old()​

// WRONG: old() in pure function contract
pure func bad(x : Nat) : Nat
  ensures result == old(x);  // ERROR: old() not allowed in pure function contracts
{
  x
}

Pure functions have no notion of "previous state" since they don't access state.

Cannot Index Arrays​

// WRONG: array indexing
pure func bad(arr : [Nat], i : Nat) : Nat {
  arr[i]  // ERROR: pure function cannot index arrays
}

Pure functions can receive array parameters but cannot index into them.

Allowed in Pure Functions​

ExpressionExample
Parametersx, a + b
Arithmeticx * 2, a / b
Comparisonsx > 0, a == b
Logical operatorsa and b, not x
Conditionalsif (x > 0) { x } else { -x }
Local let bindingslet y = x + 1; y * 2
Pure function callsdouble(x), max(a, b), Runtime.moduleHash()
Record construction{ x = 1; y = 2 }
Record field accesspoint.x
Tuple construction(a, b, c)
Variant construction#red, #some(42)
Pattern matchingswitch (v) { case (#a) 1; case (#b) 2 }

Common Use Cases​

Specification Helpers​

persistent actor {
  pure func tri2(n : Nat) : Nat {
    n * (n + 1)
  }

  public func sumTo(n : Nat) : async Nat
    ensures 2 * result == tri2(n);
  {
    var total : Nat = 0;
    var i : Nat = 0;

    while (i < n) {
      loop:invariant i <= n;
      loop:invariant 2 * total == tri2(i);
      total += i + 1;
      i += 1;
    };

    total
  }
}

Named Predicates​

pure func isValidAmount(amount : Nat, balance : Nat) : Bool {
  amount > 0 and amount <= balance
}

persistent actor {
  var balance : Nat = 100;

  public func withdraw(amount : Nat) : async Nat
    entry_requires isValidAmount(amount, balance);
    requires isValidAmount(amount, balance);
    modifies balance
    ensures balance == old(balance) - amount;
  {
    balance -= amount;
    balance
  }
}

Invariant Helpers​

persistent actor {
  var minted : Nat = 0;
  var burned : Nat = 0;

  pure func withinSupply(minted : Nat, burned : Nat, cap : Nat) : Bool {
    burned <= minted and minted - burned <= cap
  }

  invariant withinSupply(minted, burned, 1_000_000);
}

Record Computations​

type Point = { x : Int; y : Int };

pure func origin() : Point {
  { x = 0; y = 0 }
}

pure func addPoints(p1 : Point, p2 : Point) : Point {
  { x = p1.x + p2.x; y = p1.y + p2.y }
}

pure func manhattan(p : Point) : Int {
  let ax = if (p.x < 0) { -p.x } else { p.x };
  let ay = if (p.y < 0) { -p.y } else { p.y };
  ax + ay
}

Variant Pattern Matching​

type Color = { #red; #green; #blue };

pure func colorCode(c : Color) : Int {
  switch (c) {
    case (#red) { 1 };
    case (#green) { 2 };
    case (#blue) { 3 };
  }
}

pure func isRed(c : Color) : Bool {
  switch (c) {
    case (#red) { true };
    case (_) { false };
  }
}
FeatureCan Access StateCan Modify StateUse in SpecsVerified Body
pure funcNoNoYesYes
lemma funcVia parametersNoProof stepsYes
pure trusted funcNoNoYesTrusted
Regular funcYesYesNoYes

Error Messages​

ErrorCause
"pure function cannot access field"Accessing actor/module field
"pure or lemma functions may not write state"Assignment in pure function
"pure or lemma functions may not await"Async operation
"pure or lemma functions may not contain assertions or traps"assert, trap, or runtime:assert
"recursive pure functions are not supported"Direct or mutual recursion
"old() is not allowed in pure function contracts"Using old() in requires/ensures
"pure function cannot index arrays"Array element access
"pure expression contains statementful source expression"Statement loop in a pure body

Common Mistakes​

Accessing Actor State​

persistent actor {
  var count : Nat = 0;

  // WRONG: reads actor field
  pure func withCount(x : Nat) : Nat {
    x + count  // ERROR
  }

  // CORRECT: pass state as parameter
  pure func addTo(x : Nat, c : Nat) : Nat {
    x + c
  }
}

Using Assertions for Validation​

// WRONG: using assert in pure function
pure func safeSqrt(x : Nat) : Nat {
  assert x >= 0;  // ERROR
  // ...
}

// CORRECT: use requires clause
pure func safeSqrt(x : Nat) : Nat
  requires x >= 0;
{
  // ...
}

Expecting Runtime Checks​

// Pure functions have no runtime effect
pure func validate(x : Nat) : Bool {
  x > 0
}

public func process(x : Nat) : async Nat {
  // This does NOT check at runtime - pure calls are specification-only
  if (validate(x)) { x } else { 0 }  // OK but no runtime trap
}

Pure function calls in runtime code are compiled normally. They can branch and compute values, but they cannot contain runtime checks such as runtime:assert or trap.

Summary​

  • pure declares a function as side-effect free
  • Pure functions can use parameters, immutable locals, parameter fields, and pure or trusted-pure helpers
  • Cannot access actor/module state, modify state, await, assert, trap, use statement loops in verifier-visible bodies, or recurse
  • Cannot use old() in contracts
  • Use pure functions for specification helpers, named predicates, and invariant computations
  • Pure functions can have requires and ensures clauses
  • Callers and enclosing contracts must satisfy pure function preconditions
  • For recursive specifications, use lemmas or pure trusted func instead