Skip to main content

Query Functions

Query functions are public actor methods that skip consensus for faster execution. Use them for read-only APIs. Current Sector9 verification still uses ordinary permission rules for their bodies: list fields you read in reads, and list fields you write in modifies.

Declaration Syntax​

Query functions are declared with public query func inside an actor:

public query func methodName(params) : async ReturnType
  reads field1, field2
  entry_requires runtime_precondition;
  requires precondition;
  ensures postcondition;
{
  // body
}

The query modifier tells the Internet Computer to execute this function without consensus. The async return type is still required because the method is still a shared actor entry point.

Basic Example​

A simple query that reads the current balance:

query-basic.sr9
// Query function: read-only access that skips consensus
persistent actor {
  var balance : Nat = 100;

  // Query function returns async, reads state
  public query func getBalance() : async Nat
    reads balance
    ensures result == balance;
  {
    balance
  };
}

The verifier proves that:

  1. The function only reads balance (no modifications)
  2. The returned value equals the current balance
  3. No state changes occur because the body only has read permission

Why Use Query Functions​

Query functions provide significant performance benefits:

AspectUpdate FunctionQuery Function
ConsensusRequired (all replicas agree)Skipped (single replica)
LatencyHigher (~2 seconds)Lower (~200ms)
State changesPermanentNot consensus-committed; prefer read-only queries
CostHigher (consensus overhead)Lower

Use query functions for:

  • Reading current state
  • Checking balances or status
  • Retrieving data without side effects
  • Any read-only operation

Contracts on Query Functions​

Query functions support the same contract specifications as update functions:

  • entry_requires - Runtime entry guards for exported queries
  • requires - Logical preconditions the verifier assumes after the entry guard
  • ensures - Postconditions guaranteed after execution
  • reads - Fields the function accesses

For read-only queries, use reads. If a query body writes a field, current verification requires a modifies clause just like an update method; do not rely on query execution for durable state changes.

query-with-requires.sr9
// Query function with preconditions
persistent actor {
  var items : [Nat] = [10, 20, 30];

  // Query with requires clause for bounds checking
  public query func getItem(index : Nat) : async Nat
    reads items
    entry_requires index < items.size();
    requires index < items.size();
    ensures result == items[index];
  {
    items[index]
  };
}

The entry guard entry_requires index < items.size() rejects invalid external calls. The matching logical requires clause lets the verifier prove the array access is within bounds.

The reads Clause​

The reads clause declares which actor fields a query function accesses:

public query func getBalance() : async Nat
  reads balance
  ensures result == balance;
{
  balance
};

Rules:

  • List all fields the function reads
  • The verifier uses this for permission checking
  • Accessing a field not listed in reads causes an error

Reading Multiple Fields​

Query functions can read multiple fields:

query-multiple-fields.sr9
// Query function reading multiple fields
persistent actor {
  var x : Int = 10;
  var y : Int = 20;
  var z : Int = 30;

  // Read multiple fields, compute result
  public query func getSum() : async Int
    reads x, y, z
    ensures result == x + y + z;
  {
    x + y + z
  };

  // Read subset of fields
  public query func getXY() : async (Int, Int)
    reads x, y
    ensures result.0 == x;
    ensures result.1 == y;
  {
    (x, y)
  };
}

Each function declares exactly which fields it needs access to.

Calling Pure Functions​

Query functions can call pure helper functions. This is useful for complex computations in contracts:

query-calling-pure.sr9
// Query function calling pure helpers
persistent actor {
  var count : Nat = 5;

  // Pure helper for use in contracts
  pure func double(n : Nat) : Nat {
    n * 2
  };

  // Query uses pure function in postcondition
  public query func getDoubledCount() : async Nat
    reads count
    ensures result == double(count);
  {
    double(count)
  };
}

Pure functions have no side effects and can be used safely within query functions and contracts.

Actor Invariants​

Query functions interact with actor invariants the same way as update functions:

PointBehavior
EntryInvariant is assumed to hold
ExitInvariant is verified
persistent actor {
  var balance : Nat = 0;

  invariant balance <= 1_000_000;

  // Invariant is assumed at entry
  public query func getBalance() : async Nat
    reads balance
    ensures result <= 1_000_000;  // Follows from invariant
  {
    balance
  };
}

Read-only queries preserve invariants trivially. If a query body declares modifies and writes state, the verifier checks invariant preservation for that body.

Return Types​

Query functions must return an async type:

// Returns a value
public query func getValue() : async Nat { ... }

// Returns a tuple
public query func getPair() : async (Nat, Nat) { ... }

Error M0036: If you omit async, the verifier rejects the function:

// Error M0036: shared query function must have return type 'async <typ>'
public query func bad() : Nat { 42 };

Restrictions​

Query functions have important restrictions enforced by the type system.

Writes Require modifies​

Current Sector9 verification permits a query body to write actor fields, but the write must be declared with modifies. Prefer read-only query APIs unless you are intentionally modeling query-execution-local mutation.

// Query function that writes state must declare a modifies clause
persistent actor {
  var counter : Nat = 0;

  // Prefer read-only queries for public APIs, but current verification permits
  // query bodies to write fields when the writes are declared.
  public query func incrementInQueryExecution() : async Nat
    modifies counter
    ensures result == counter;
  {
    counter += 1;
    counter
  };
}

Cannot Call Update Functions​

Query functions cannot call other shared functions (update or oneway):

// Query function cannot call update functions - this is rejected
persistent actor {
  var count : Nat = 0;

  public func increment() : async ()
    modifies count
  {
    count += 1;
  };

  // Error M0188: cannot call shared function from query
  public query func badQuery() : async Nat
    reads count
  {
    await increment();  // Not allowed!
    count
  };
}

Error M0188: The verifier reports "send capability required, but not available (cannot call a shared function from a query function)".

Cannot Use await Directly​

Query functions cannot contain await expressions in their body:

// Error M0038: misplaced await
public query func badQuery() : async Nat {
  await someCall();  // Not allowed in query body
  42
};

This restriction exists because await implies inter-canister calls that could have side effects.

Composite Query Functions​

For queries that need to call other queries on the same subnet, use composite query:

public composite query func aggregateData() : async Nat {
  let a = try { await* otherCanister.getData() } catch (_) { 0 };
  let b = try { await* anotherCanister.getData() } catch (_) { 0 };
  a + b
};

Composite queries:

  • Can call other query and composite query functions
  • Still cannot call update functions (Error M0187)
  • Cannot be called from regular update functions (Error M0186)

Composite queries are a query-specific use of await*. The await* keyword itself is not limited to composite queries; it consumes async* computations. In update code, async* helpers still run as part of the update flow, and only an ordinary await reached inside that computation creates an interleaving boundary.

Shared Type Restrictions​

Like update functions, query parameters and return types must be shared types:

Allowed:

  • Primitives: Nat, Int, Bool, Text, Float, Principal, Blob
  • Containers: ?T, [T], tuples, records, variants (if elements are shared)
  • Actor references whose interface contains only shared functions

Not allowed:

  • Functions (cannot serialize closures)
  • Mutable arrays ([var T] in parameters)
  • Modules
// Error M0031: shared function has non-shared return type
public query func bad() : async (Nat -> Nat) { ... };

// Correct: use only shared types
public query func good() : async Nat { 42 };

Common Mistakes​

Forgetting reads Clause​

Accessing a field without declaring it in reads:

// Error: permission violation
persistent actor {
  var balance : Nat = 0;

  public query func getBalance() : async Nat
    // Missing: reads balance
  {
    balance  // No permission to read!
  };
}

Fix: Add reads balance to the function header.

Using modifies When You Only Read​

Read-only query functions should declare what they read:

// Avoid: this grants write permission even though the body only reads
public query func getValue() : async Nat
  modifies value
{ value };

// Correct
public query func getValue() : async Nat
  reads value
{ value };

Trying to Await in Query Body​

Query functions cannot await directly:

// Error M0038
public query func bad() : async Nat {
  await someAsyncCall();  // Not allowed
  42
};

If you need to await, either:

  • Use a composite query function (for query calls only)
  • Use a regular update function

Query vs Update: Decision Guide​

Use query functions when:

  • Reading current state
  • No state changes needed
  • Performance matters (lower latency)
  • Checking conditions or retrieving data

Use update functions when:

  • Modifying state
  • Calling other canisters with side effects
  • Changes must be persisted
  • Atomic transactions required

Summary​

  • Query functions are public query func methods intended for fast read APIs
  • They skip consensus, providing faster execution (~10x faster than updates)
  • Use reads to declare which fields the function accesses
  • Query functions support entry_requires, requires, and ensures contracts
  • Restrictions: no calling update functions and no direct await; writes still require modifies
  • Use composite query when you need to call other queries
  • Actor invariants are checked at entry and exit; read-only queries preserve them trivially
  • Parameters and return types must be shared (serializable) types