Public and Private Members

Visibility modifiers control which functions can be called from outside an actor and where verification places actor-invariant boundaries.

Visibility Basics

Actor members have two visibility levels:

Modifier	Access	Verification
public	Callable from outside	Invariants checked at exported method boundaries
(none) or private	Internal only	No automatic invariant boundary

Functions without a visibility modifier are private by default. Use private explicitly for clarity.

Public Functions

Public functions are the actor's external interface. They:

• Can be called from other actors or external clients
• In actors, must return an async type; unawaited fire-and-forget futures are rejected by the verified subset
• Have actor invariants automatically assumed at entry and checked at exit
• Need entry_requires for caller-controlled runtime guards when they also have nontrivial logical requires

persistent actor {
  var count : Nat = 0;

  invariant count <= 100;

  // Public: external callers can invoke this
  public func increment() : async Nat
    modifies count
    entry_requires count < 100;
    requires count < 100;
    ensures result == old(count) + 1;
  {
    count += 1;
    count
  };
}

The verifier ensures that:

1. The invariant count <= 100 holds when increment is called
2. The invariant still holds when increment returns
3. The postcondition result == old(count) + 1 is satisfied

Private Functions

Private functions are internal helpers that cannot be called from outside the actor. They:

• Are not exposed in the actor's public interface
• Do not trigger automatic invariant checking
• Can have their own contracts (requires, ensures, modifies)

persistent actor {
  var count : Nat = 0;

  // Private: only callable within this actor
  func addOne() : Nat
    modifies count
    ensures result == old(count) + 1;
  {
    count += 1;
    count
  };

  public func addTwo() : async Nat
    modifies count
  {
    ignore addOne();
    addOne()
  };
}

Use the private keyword explicitly for clarity:

private func helper() : Nat { 42 };

Complete Example

This example shows public and private functions working together:

visibility-basic.sr9

// Basic visibility example: public vs private functions
persistent actor Counter {
  var count : Nat = 0;

  // Private helper function - not callable from outside
  func increment() : Nat
    modifies count
    ensures result == old(count) + 1;
    ensures count == result;
  {
    count += 1;
    count
  };

  // Public function - callable from outside the actor
  public func add(n : Nat) : async Nat
    modifies count
    entry_requires n <= 100;
    requires n <= 100;
    ensures result == old(count) + n;
  {
    var i : Nat = 0;
    while (i < n) {
      loop:invariant i <= n;
      loop:invariant count == old(count) + i;
      ignore increment();
      i += 1;
    };
    count
  };

  // Public query function - read-only access
  public func getCount() : async Nat
    reads count
    ensures result == count;
  {
    count
  };
}

The private increment function handles the core logic. The public add function provides the external interface and loops over the helper.

Private Helpers with Contracts

Private functions benefit from contracts just like public functions. The verifier uses private function contracts to reason about public function behavior:

visibility-private-helpers.sr9

// Private helper functions with contracts
persistent actor Validator {
  var total : Nat = 0;
  let MAX : Nat = 1000;

  // Private: validate input range
  pure func isValid(amount : Nat) : Bool {
    amount > 0 and amount <= 1000
  };

  // Private: apply validated update
  func applyUpdate(amount : Nat) : ()
    reads MAX
    modifies total
    requires isValid(amount);
    requires total + amount <= MAX;
    ensures total == old(total) + amount;
  {
    total += amount;
  };

  // Public: validates and updates
  public func deposit(amount : Nat) : async Bool
    reads MAX
    modifies total
    ensures result == (old(total) + amount <= MAX and amount > 0 and amount <= MAX);
    ensures result ==> total == old(total) + amount;
    ensures (not result) ==> total == old(total);
  {
    if (isValid(amount) and total + amount <= MAX) {
      applyUpdate(amount);
      true
    } else {
      false
    }
  };

  public func getTotal() : async Nat
    reads total
  {
    total
  };
}

The private isValid and applyUpdate functions have their own contracts. When deposit calls them, the verifier:

1. Checks that deposit satisfies applyUpdate's preconditions
2. Assumes applyUpdate's postconditions hold after the call

This modular approach keeps contracts focused and proofs tractable.

Explicit private Keyword

While functions are private by default, the explicit private keyword improves readability:

visibility-private-explicit.sr9

// Explicit private keyword for clarity
persistent actor Bank {
  var balance : Int = 0;

  invariant balance >= 0;

  // Explicit private - preferred for clarity
  private pure func validateAmount(amount : Nat) : Bool {
    amount > 0 and amount <= 10000
  };

  // Explicit private - internal state update
  private func addToBalance(amount : Nat) : ()
    modifies balance
    requires balance + amount >= 0;
    ensures balance == old(balance) + amount;
  {
    balance += amount;
  };

  public func deposit(amount : Nat) : async Bool
    modifies balance
    entry_requires validateAmount(amount);
    requires validateAmount(amount);
    ensures balance == old(balance) + amount;
    ensures result == true;
  {
    addToBalance(amount);
    true
  };

  public func withdraw(amount : Nat) : async Bool
    modifies balance
    ensures result == (old(balance) >= amount);
    ensures result ==> balance == old(balance) - amount;
    ensures (not result) ==> balance == old(balance);
  {
    if (balance >= amount) {
      balance -= amount;
      true
    } else {
      false
    }
  };
}

Using private makes the intent clear to readers and helps catch accidental exposure.

Visibility and Invariant Checking

A key difference between public and private functions is invariant handling:

Function Type	Entry	Exit
Public	Invariant assumed	Invariant verified
Private	No assumption	No verification

Private functions can temporarily violate actor invariants, as long as public functions restore them before returning or before another invariant boundary such as an await:

visibility-verification.sr9

// Visibility affects verification: invariants on public methods only
persistent actor Auction {
  var highBid : Nat = 0;
  var bidCount : Nat = 0;

  // Actor invariant - checked at public method boundaries
  invariant bidCount > 0 ==> highBid > 0;

  // Private: may temporarily violate invariant
  func resetBidCount() : ()
    modifies bidCount
  {
    bidCount := 0;
    // Here invariant might be violated: bidCount=0 but highBid>0
    // This is allowed because private functions don't check invariants
  };

  // Private: completes the reset
  func resetHighBid() : ()
    modifies highBid
  {
    highBid := 0;
    // Now invariant holds again: bidCount=0 and highBid=0
  };

  // Public: must restore invariant before returning
  public func reset() : async ()
    modifies highBid, bidCount
    ensures highBid == 0;
    ensures bidCount == 0;
  {
    resetBidCount();
    resetHighBid();
    // Invariant verified here at public boundary
  };

  public func bid(amount : Nat) : async Bool
    modifies highBid, bidCount
    entry_requires amount > 0;
    requires amount > 0;
    ensures result == (amount > old(highBid));
    ensures result ==> highBid == amount;
    ensures result ==> bidCount == old(bidCount) + 1;
  {
    if (amount > highBid) {
      highBid := amount;
      bidCount += 1;
      true
    } else {
      false
    }
  };
}

In this example:

• resetBidCount sets bidCount to 0, potentially violating the invariant
• resetHighBid restores the invariant by setting highBid to 0
• The public reset function calls both, and the invariant is verified at exit

This flexibility lets you decompose complex state updates into helper functions without requiring each helper to maintain global invariants. Give helpers focused contracts when their effects should be reused by callers.

Query Functions

The query modifier creates fast public functions that skip consensus. Query functions:

• Are best used for read-only APIs
• Still use verifier permissions: reads for fields read, modifies for fields written
• Execute faster because they skip consensus
• Are still public and have invariants checked

persistent actor {
  var balance : Nat = 0;

  // Query: read-only, faster execution
  public query func getBalance() : async Nat
    reads balance
  {
    balance
  };

  // Update: can modify state, goes through consensus
  public func deposit(amount : Nat) : async ()
    modifies balance
  {
    balance += amount;
  };
}

Use query for read-only operations to improve performance. If a query body writes actor fields, current verification requires a modifies clause; do not rely on query execution for durable state changes.

System Visibility

The system visibility is reserved for special actor lifecycle methods:

persistent actor {
  system func timer() : async () {
    // Called by the system at regular intervals
  };

  system func heartbeat() : async () {
    // Called on every subnet round
  };
}

System functions:

• Are called by the Internet Computer runtime, not by external callers
• Have fixed signatures that the compiler checks
• Cannot be called directly from other code

Common Mistakes

Shared Functions Cannot Be Private

Public actor functions are implicitly shared (callable across the network). You cannot make a shared function private:

// Error M0126: a shared function cannot be private
persistent actor {
  private shared func bad() : async () { };
}

Remove either private or shared:

persistent actor {
  private func helper() : () { };          // Private local function
  public func entry() : async () { };      // Public shared function
}

Public Fields Must Be Functions

Actors expose functionality through functions, not direct field access:

// Error M0125: public actor field needs to be a manifest function
persistent actor {
  public var counter : Nat = 0;  // Wrong
}

Use a getter function instead:

persistent actor {
  var counter : Nat = 0;  // Private field

  public func getCounter() : async Nat  // Public accessor
    reads counter
  {
    counter
  };
}

Calling Private Functions from Outside

Private functions cannot be called from other actors or modules:

// From another actor:
let result = try { await myActor.privateHelper() } catch (_) { 0 };  // Error: not in interface

Only public functions appear in the actor's type and can be called externally.

Forgetting async on Public Functions

Public actor functions must return async types:

// Error M0041: public actor function has non-async result type
persistent actor {
  public func bad() : Nat { 42 };
}

Add async to the return type:

persistent actor {
  public func good() : async Nat { 42 };
}

Module Visibility

Modules follow similar visibility rules, but without the async requirement:

module Math {
  // Public: accessible as Math.add
  public func add(a : Nat, b : Nat) : Nat { a + b };

  // Private: internal helper
  func clamp(n : Nat, max : Nat) : Nat {
    if (n > max) max else n
  };

  // Public constant
  public let PI : Float = 3.14159;
}

Module members are private by default. Use public to export them.

Related Topics

• Update methods and query methods for exported method forms
• Entry requires for runtime guards on public methods
• Actor invariant preservation for public boundary checks
• Private helper contracts for modular internal proofs

Summary

• Functions without visibility modifiers are private by default
• Use public to expose functions as the actor's external interface
• Use private explicitly for clarity on internal helpers
• Public functions have actor invariants checked at entry and exit
• Private functions can temporarily violate invariants
• Private functions can have their own contracts for modular verification
• Use query for read-only public functions
• system visibility is for runtime lifecycle hooks
• Public actor functions must return async types