Cycles and Resources

Cycles are the computational currency of the Internet Computer. Every operation your canister performs costs cycles, and cycle exhaustion is a runtime resource concern outside Sector9's proof model.

What Are Cycles

Cycles measure computational resources on the IC:

Resource	Cycles Cost
CPU instructions	Per instruction
Memory usage	Per byte stored
Inter-canister calls	Per message
HTTP outcalls	Per request
Cryptographic operations	Per signature

Your canister maintains a cycle balance. As it executes, the IC deducts cycles. If the balance is insufficient for execution or storage, runtime calls can fail and canister operation can be interrupted by the IC.

The Cycles API

Sector9 exposes the current cycle helpers through mo:core/Cycles. The module wraps IC cycle primitives but does not give the verifier a model of cycle accounting.

Core Functions

import Cycles "mo:core/Cycles";

// Query your canister's current cycle balance
let myBalance : Nat = Cycles.balance();

// Check cycles received in the current call
let received : Nat = Cycles.available();

// Accept cycles from the caller
let accepted : Nat = Cycles.accept<system>(10_000_000);

// Check cycles refunded from the last await
let refund : Nat = Cycles.refunded();

// Burn cycles intentionally
let burned : Nat = Cycles.burn<system>(1_000_000);

Function Reference

Function	Signature	Purpose
balance()	() -> Nat	Current canister cycle balance
available()	() -> Nat	Cycles received in this call (minus accepted)
accept<system>(n)	Nat -> Nat	Transfer cycles from available to balance
refunded()	() -> Nat	Cycles returned from last await
burn<system>(n)	Nat -> Nat	Burn cycles intentionally

The <system> capability marker indicates these functions interact with IC system state.

Cycle Transfer Semantics

Cycles flow between canisters through a push model:

Sending Cycles

try { await (with cycles = 15_000_000) targetCanister.operation(); } catch (_) {};

The parenthetical syntax (with cycles = amount) attaches cycles to a specific call. Legacy primitive add/call patterns exist in low-level Motoko tests, but new Sector9 code should use the parenthetical syntax.

Receiving Cycles

public func acceptDonation() : async Nat {
  let offered = Cycles.available();
  let accepted = Cycles.accept<system>(offered);
  accepted
}

Refund Mechanism

Unaccepted cycles automatically return to the caller:

public func sendWithRefund() : async Nat {
  try { await (with cycles = 10_000_000) targetCanister.operation(); } catch (_) {};  // accepts 3_000_000
  Cycles.refunded()  // returns 7_000_000
}

If the callee rejects or traps before accepting cycles, the attached cycles are refunded. Cycles already accepted by the callee follow IC runtime rules and should not be treated as proof-visible state.

Cycle Flow Diagram

Caller                           Callee
------                           ------
balance = 100M                   balance = 50M
  │
  ├── await (with cycles = 20M) operation()
  │                          ──────► available() = 20M
  │   balance now 80M             │
  │                               ├── accept<system>(15M)
  │                               │   balance now 65M
  │                               │
  │   ◄────────────────────────── return
  │
  ├── refunded() = 5M
  │   balance now 85M
  │

Cost Estimation

The IC provides cost estimation functions for planning:

import Prim "mo:⛔";

// Estimate cost to create a new canister
let createCost : Nat = Prim.costCreateCanister();

// Estimate cost for an inter-canister call
let callCost : Nat = Prim.costCall(methodNameLength, payloadSize);

// Estimate cost for HTTP outcall
let httpCost : Nat = Prim.costHttpRequest(requestSize, maxResponseBytes);

These estimates help ensure you attach sufficient cycles before operations. Sector9 does not prove the estimates are sufficient.

Cycle Limits

Cycle amounts use 128-bit unsigned integers. The maximum is 2^128 - 1:

// This traps or rejects: exceeds maximum
await (with cycles = 0x1_00000000_00000000_00000000_00000000) target.operation();
// Error: "cannot add more than 2^128 cycles"

Attempting to add more than the maximum causes an immediate trap.

Verification and Cycles

Sector9 does not model cycle accounting. Cycles are explicitly outside the verification boundary.

What Sector9 Verifies

• Contract preconditions and postconditions
• Actor invariants
• Loop invariants
• Assertion correctness
• Permission and framing

What Sector9 Does Not Verify

• Cycle balance sufficiency
• Cycle exhaustion
• Cost estimation accuracy
• Refund handling correctness

Why Cycles Are Out of Scope

The verification model focuses on algebraic reasoning about values, state, and control flow. Cycle accounting depends on:

• Runtime execution costs (unpredictable)
• IC infrastructure pricing (external)
• Canister memory usage (dynamic)
• Network conditions (variable)

These factors are outside what SMT-based verification can reason about.

Cycles Operations in Verification

When the verifier encounters core cycle operations, it treats them as trusted runtime calls with opaque return values:

public func deposit() : async ()
  modifies savings
  requires true;  // No cycle-related preconditions
{
  let amount = Cycles.available();  // Verifier: opaque Nat
  let accepted = Cycles.accept<system>(amount);  // Verifier: opaque Nat
  savings += accepted;  // Verifier: normal arithmetic
}

The verifier does not prove relationships such as "accepted cycles are less than available cycles" or "balance increased by the accepted amount" unless you model those relationships explicitly in your own state and contracts.

Best Practices

1. Check Balance Before Expensive Operations

public func performExpensive() : async () {
  if (Cycles.balance() < minimumRequired) {
    trap true "Insufficient cycles";
  };
  // Proceed with operation
}

2. Accept Cycles Explicitly

Always accept the cycles you need, not more:

public func acceptPayment(required : Nat) : async Bool {
  let available = Cycles.available();
  if (available < required) {
    return false;  // Reject: insufficient payment
  };
  let _ = Cycles.accept<system>(required);  // Accept exactly what's needed
  true  // Excess refunds automatically
}

3. Use Parenthetical Syntax

Prefer the new syntax for clarity:

// Clear: cycles attached to specific call
try { await (with cycles = 10_000_000) target.method(); } catch (_) {};

4. Handle Refunds

Check refunds after calls to understand actual costs:

public func transferWithCost() : async Nat {
  let sent = 10_000_000;
  try { await (with cycles = sent) target.operation(); } catch (_) {};
  let refund = Cycles.refunded();
  sent - refund  // Actual cost
}

Common Pitfalls

Forgetting to Accept

Cycles available in a call are not automatically credited:

// Wrong: cycles are lost (refunded to caller)
public func badDeposit() : async () {
  // Cycles.available() > 0 but we never accept
}

// Correct: explicitly accept cycles
public func goodDeposit() : async () {
  let _ = Cycles.accept<system>(Cycles.available());
}

Overflow on Attached Cycles

Cycle amounts are bounded:

await (with cycles = largeAmount) target.method();

Summary

• Cycles are the IC's computational currency that powers canister execution
• The mo:core/Cycles module provides balance, accept, burn, and refund operations
• Cycles transfer uses a push model: sender attaches cycles, receiver accepts them
• Unaccepted cycles automatically refund to the caller
• Sector9 does not verify cycle sufficiency - it is a runtime concern
• Use the parenthetical syntax (with cycles = n) for clarity
• Always explicitly accept cycles you need

See Also

• Trap Behavior - State rollback on failure
• At-Most-Once Delivery - Message delivery guarantees
• Runtime limitations - Verification boundaries
• Cycles module - Core API reference