Using Pure Functions in Contracts
Pure functions serve as named predicates in contracts, making specifications more readable and reusable.
Why Use Pure Functions in Contracts
Contracts often contain complex conditions that are hard to read inline. Pure functions let you name these conditions:
// Hard to read inline
public func withdraw(amount : Nat) : async Nat
entry_requires amount > 0 and amount <= balance and balance >= minimumBalance + amount;
requires amount > 0 and amount <= balance and balance >= minimumBalance + amount;
modifies balance
{ ... }
// Clear with named predicate
pure func isValidWithdrawal(amount : Nat, bal : Nat, minBal : Nat) : Bool {
amount > 0 and amount <= bal and bal >= minBal + amount
}
public func withdraw(amount : Nat) : async Nat
entry_requires isValidWithdrawal(amount, balance, minimumBalance);
requires isValidWithdrawal(amount, balance, minimumBalance);
modifies balance
{ ... }
Named predicates are self-documenting. A reader immediately understands what isValidWithdrawal checks without parsing the boolean logic.
Pure Functions in Preconditions
Use pure functions in requires clauses to validate inputs:
pure func inRange(x : Int, lo : Int, hi : Int) : Bool {
x >= lo and x <= hi
}
pure func isPositive(x : Int) : Bool {
x > 0
}
persistent actor {
var temperature : Int = 20;
public func setTemperature(t : Int) : async ()
entry_requires inRange(t, -40, 100);
requires inRange(t, -40, 100);
modifies temperature
{
temperature := t;
}
public func increaseBy(delta : Int) : async ()
entry_requires isPositive(delta);
entry_requires inRange(temperature + delta, -40, 100);
requires isPositive(delta);
requires inRange(temperature + delta, -40, 100);
modifies temperature
{
temperature += delta;
}
}
When you call a pure function in a precondition, the verifier checks that the caller satisfies the pure function's own preconditions if any. Use entry_requires as the exported runtime gate when the same predicate must be checked before a shared update starts.
The same rule applies in every contract position. If an ensures,
invariant, or loop:invariant calls a pure helper, the verifier separately
proves the helper's requires clauses from the surrounding proof context. The
helper precondition is not treated as an implication guard around the contract
fact; a missing bound such as reserve >= fee remains a real proof failure.
Pure Functions in Postconditions
Use pure functions in ensures clauses to describe return values:
pure func max(a : Int, b : Int) : Int {
if (a > b) { a } else { b }
}
pure func min(a : Int, b : Int) : Int {
if (a < b) { a } else { b }
}
pure func clamp(x : Int, lo : Int, hi : Int) : Int {
max(lo, min(x, hi))
}
persistent actor {
var value : Int = 0;
public func clampedSet(x : Int) : async Int
modifies value
ensures result == clamp(x, 0, 100);
ensures value == result;
{
value := clamp(x, 0, 100);
value
}
}
For local pure functions, the verifier can use the function body to prove the
postcondition. Across source imports, pure helpers are contract-only unless the
helper is explicitly exported as inline pure func.
Combining with old()
Pure functions work naturally with old() to describe state changes:
pure func doubled(x : Int) : Int {
x * 2
}
pure func addWithBonus(amount : Int, bonus : Int) : Int {
amount + bonus
}
persistent actor {
var balance : Int = 100;
var bonus : Int = 10;
public func doubleDeposit(amount : Int) : async Int
entry_requires amount >= 0;
requires amount >= 0;
modifies balance
ensures balance == old(balance) + doubled(amount);
ensures result == balance;
{
balance += doubled(amount);
balance
}
public func depositWithBonus(amount : Int) : async Int
entry_requires amount >= 0;
requires amount >= 0;
modifies balance
ensures balance == old(balance) + addWithBonus(amount, bonus);
{
balance += addWithBonus(amount, bonus);
balance
}
}
Note: Pure functions themselves cannot use old() in their own contracts. The old() calls must be in the enclosing method's contract.
Pure Functions in Actor Invariants
Extract complex actor invariant conditions into pure functions:
pure func withinBudget(spent : Nat, limit : Nat) : Bool {
spent <= limit
}
pure func isValidRate(rate : Nat) : Bool {
rate <= 100
}
persistent actor {
var spent : Nat = 0;
var budget : Nat = 10000;
var taxRate : Nat = 5;
invariant withinBudget(spent, budget);
invariant isValidRate(taxRate);
}
This pattern keeps invariants readable even when the conditions are complex.
Pure Functions in Loop Invariants
loop:invariant annotations benefit greatly from pure function helpers:
pure func tri2(n : Nat) : Nat {
n * (n + 1)
}
persistent actor {
public func sumTo(n : Nat) : async Nat
ensures 2 * result == tri2(n);
{
var sum : Nat = 0;
var i : Nat = 0;
while (i < n) {
loop:invariant i <= n;
loop:invariant 2 * sum == tri2(i);
i += 1;
sum += i;
};
sum
}
}
The pure function tri2 gives a name to the closed-form formula, making the loop invariant clear without relying on division in the invariant.
Composing Pure Functions
Pure functions can call other pure functions, enabling layered specifications:
pure func square(x : Int) : Int {
x * x
}
pure func sumOfSquares(a : Int, b : Int) : Int {
square(a) + square(b)
}
persistent actor {
public func computeHypotenuse(a : Int, b : Int) : async Int
ensures result == sumOfSquares(a, b);
{
sumOfSquares(a, b)
}
}
Nested composition also works:
pure func double(x : Int) : Int { x * 2 }
pure func quadruple(x : Int) : Int {
double(double(x))
}
persistent actor {
var value : Int = 0;
public func quadrupleAdd(x : Int) : async Int
modifies value
ensures value == old(value) + quadruple(x);
{
value += quadruple(x);
value
}
}
Module-Level Pure Functions
Define reusable pure predicates in modules:
module Validation {
public pure func isNonNegative(x : Int) : Bool {
x >= 0
}
public pure func isInBounds(x : Int, lo : Int, hi : Int) : Bool {
x >= lo and x <= hi
}
public pure func isValidPercentage(p : Nat) : Bool {
p <= 100
}
}
persistent actor {
var rate : Nat = 5;
public func setRate(r : Nat) : async ()
entry_requires Validation.isValidPercentage(r);
requires Validation.isValidPercentage(r);
modifies rate
{
rate := r;
}
}
Module-qualified calls like Validation.isValidPercentage(r) work in contracts.
Pure Functions with Their Own Contracts
Pure functions can have preconditions and postconditions:
pure func safeDivide(a : Int, b : Int) : Int
requires b != 0;
ensures result * b <= a;
{
a / b
}
pure func safeSubtract(a : Nat, b : Nat) : Nat
requires a >= b;
ensures result == a - b;
{
a - b
}
persistent actor {
var balance : Nat = 100;
public func withdraw(amount : Nat) : async Nat
entry_requires amount <= balance;
requires amount <= balance;
modifies balance
ensures balance == safeSubtract(old(balance), amount);
{
balance := safeSubtract(balance, amount);
balance
}
}
When calling safeSubtract in the contract, the verifier checks that old(balance) >= amount holds.
If that fact is missing, the failure points to the helper dependency in the
contract rather than allowing the postcondition to hold conditionally.
Pattern: Boolean Predicates
Use pure functions to name boolean conditions:
pure func isEmpty(size : Nat) : Bool {
size == 0
}
pure func isFull(size : Nat, capacity : Nat) : Bool {
size >= capacity
}
pure func canAdd(size : Nat, capacity : Nat) : Bool {
not isFull(size, capacity)
}
persistent actor {
var count : Nat = 0;
let capacity : Nat = 100;
public func add() : async ()
entry_requires canAdd(count, capacity);
requires canAdd(count, capacity);
modifies count
{
count += 1;
}
public func remove() : async ()
entry_requires not isEmpty(count);
requires not isEmpty(count);
modifies count
{
count -= 1;
}
}
Pattern: Computation Helpers
Use pure functions to compute expected values:
pure func fee(amount : Nat, rate : Nat) : Nat {
amount * rate / 100
}
pure func netAmount(amount : Nat, rate : Nat) : Nat
requires fee(amount, rate) <= amount;
{
amount - fee(amount, rate)
}
persistent actor {
var balance : Nat = 0;
let feeRate : Nat = 1;
public func deposit(amount : Nat) : async ()
entry_requires amount > 0;
entry_requires fee(amount, feeRate) < amount;
requires amount > 0;
requires fee(amount, feeRate) < amount;
modifies balance
ensures balance == old(balance) + netAmount(amount, feeRate);
{
balance += netAmount(amount, feeRate);
}
}
Pattern: Record Operations
Use pure functions to work with records in specifications:
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
}
persistent actor {
var position : Point = { x = 0; y = 0 };
public func move(delta : Point) : async Int
modifies position
ensures position == addPoints(old(position), delta);
ensures result == manhattan(position);
{
position := addPoints(position, delta);
manhattan(position)
}
}
Pattern: Variant Classification
Use pure functions to classify variant values:
type Status = { #pending; #approved; #rejected };
pure func isPending(s : Status) : Bool {
switch (s) {
case (#pending) { true };
case (_) { false };
}
}
pure func isFinal(s : Status) : Bool {
switch (s) {
case (#approved) { true };
case (#rejected) { true };
case (_) { false };
}
}
persistent actor {
var status : Status = #pending;
public func approve() : async ()
entry_requires isPending(status);
requires isPending(status);
modifies status
ensures isFinal(status);
{
status := #approved;
}
}
What You Cannot Do
Pure functions in contracts have restrictions inherited from pure function rules.
No Recursion in Pure Functions
// WRONG: recursive pure function
pure func factorial(n : Nat) : Nat {
if (n == 0) { 1 }
else { n * factorial(n - 1) } // ERROR: recursive pure functions not supported
}
Use a lemma or pure trusted func instead for recursive specifications.
No old() in Pure Function Contracts
// WRONG: old() in pure function's own contract
pure func bad(x : Nat) : Nat
ensures result == old(x); // ERROR: old() not allowed in pure function contracts
{
x
}
// CORRECT: use parameter directly
pure func good(x : Nat) : Nat
ensures result == x;
{
x
}
The old() expression belongs in the enclosing method's contract, not in the pure function itself.
Higher-Order Pure Functions
// OK: calling a function parameter is allowed when it is pure or lemma
pure func apply(f : Int -> Int, x : Int) : Int {
f(x)
}
// WRONG: passing an impure function value
func impure(x : Int) : Int { x + 1 };
apply(impure, 5); // ERROR M0360
Function parameters can be used in pure functions when the passed function value is pure or has an effect-free contract. Impure function values are rejected with M0360.
Runtime Identity Helpers
Trusted-pure helpers such as Runtime.moduleHash() can appear in pure helpers and contracts when the proof needs stable module identity, for example token or asset IDs. Context-sensitive provenance helpers such as Runtime.callingModuleId() are intentionally limited to executable method bodies and executable method contracts.
Best Practices
- Name conditions clearly:
isValidAmountis better thancheck1 - Keep pure functions small: One concept per function
- Compose for complexity: Build complex predicates from simple ones
- Pass state explicitly: Pure functions receive state as parameters, not through field access
- Use for repeated conditions: If the same condition appears multiple times, extract it
- Document with postconditions: Add
ensuresclauses to pure functions when the computation is non-obvious
Summary
- Pure functions in contracts act as named predicates
- Use in
requires,ensures,invariant, andloop:invariant - Combine with
old()in the enclosing method's contract - Module-level pure functions enable reusable specifications
- Pure functions can have their own contracts that callers must satisfy
- Compose pure functions for layered specifications
- Extract repeated or complex conditions into named pure functions
Related Topics
- The
puremodifier for declaration syntax and basic examples - Pure restrictions for what helpers cannot do
old()basics for combining pure helpers with entry snapshotsentry_requiresfor mirroring named predicates at exported runtime boundaries- Digital asset identity for
Runtime.moduleHash()in token models