Skip to main content

Runtime Entry Guards with entry_requires

entry_requires is the runtime-facing counterpart to requires for public actor methods. It checks whether an external message is allowed to enter the verified method body.

Use it for facts controlled by the external caller: argument bounds, authorization checks, non-null options, array bounds, division guards, and other conditions that must be enforced at the canister boundary.

Basic Pattern​

For a public actor method, pair caller-controlled logical preconditions with matching runtime entry guards:

public func deposit(amount : Nat) : async ()
  modifies balance
  entry_requires amount > 0;
  requires amount > 0;
  ensures balance == old(balance) + amount;
{
  balance += amount;
}

The entry_requires clause is checked before the external call enters the method. The matching requires clause is still the logical fact the verifier uses inside the method and at internal call sites.

entry-requires-basic.sr9
// Runtime entry guards for public actor methods.
persistent actor {
  var owner : ?Principal = null;
  var balance : Nat = 0;

  public shared({caller}) func claimOwner() : async ()
    modifies owner
    entry_requires owner == null;
    requires owner == null;
    ensures owner == ?caller;
  {
    owner := ?caller;
  };

  public func deposit(amount : Nat) : async ()
    modifies balance
    entry_requires amount > 0;
    requires amount > 0;
    ensures balance == old(balance) + amount;
  {
    balance += amount;
  };

  public shared({caller}) func withdraw(amount : Nat) : async ()
    reads owner
    modifies balance
    entry_requires owner == ?caller;
    entry_requires amount <= balance;
    requires owner == ?caller;
    requires amount <= balance;
    ensures balance == old(balance) - amount;
  {
    balance -= amount;
  };
}

entry_requires vs requires​

ClauseRuntime checkVerifier meaningMain use
entry_requiresYes, for public actor entrypointsMust be strong enough to justify logical preconditionsDefend external boundaries
requiresNoCaller obligation and function assumptionReason about verified calls

For public actor methods, a nontrivial requires without entry_requires is rejected in Viper mode. Otherwise the verifier would trust an external caller to satisfy a precondition that runtime did not check.

// Rejected: external callers are not runtime-checked.
public query func bad(n : Nat) : async Nat
  requires n <= 10;
  ensures result <= 10;
{
  n
}

// Correct: runtime guard proves the logical precondition.
public query func good(n : Nat) : async Nat
  entry_requires n <= 10;
  requires n <= 10;
  ensures result <= 10;
{
  n
}

Strong Enough Guards​

entry_requires is not a way to trust requires. The verifier checks that the entry guards imply the logical preconditions before the body runs.

// Rejected: n <= 20 does not prove n <= 10.
public query func tooWeak(n : Nat) : async Nat
  entry_requires n <= 20;
  requires n <= 10;
  ensures result <= 10;
{
  n
}

The guard may be exactly the same as requires, or stronger:

public query func strongEnough(n : Nat) : async Nat
  entry_requires n <= 5;
  requires n <= 10;
  ensures result <= 10;
{
  n
}

Use entry_requires true; only when no caller-controlled runtime fact is needed. This is useful when actor invariants alone justify the logical requires, but it does not prove parameter bounds by itself.

Access Control​

Use shared({caller}) for caller identity and compare the Principal in entry_requires:

persistent actor {
  var owner : ?Principal = null;

  public shared({caller}) func transferOwnership(newOwner : Principal) : async ()
    reads owner
    modifies owner
    entry_requires owner == ?caller;
    requires owner == ?caller;
    ensures owner == ?newOwner;
  {
    owner := ?newOwner;
  };
}

Do not pass caller identity as a plain argument. The caller is bound by the shared method pattern and has type Principal.

What Can Appear in entry_requires​

Allowed:

  • Parameters and shared caller bindings such as caller
  • Current actor fields covered by reads or modifies
  • Pure runtime-safe helper calls
  • Comparisons, Boolean logic, switch expressions, records, options, arrays, variants, tuples, and quantifiers
  • Division or modulo only after a suitable non-zero guard

Not allowed:

  • old(...)
  • result
  • Local variables from the function body
  • Ghost variables, ghost functions, lemmas, or spec-only helpers
  • Impure method calls or any expression with side effects

If an entry guard reads actor state, declare the footprint:

persistent actor {
  var limit : Nat = 10;

  public query func bounded(n : Nat) : async Nat
    reads limit
    entry_requires n <= limit;
    requires n <= limit;
    ensures result == n;
  {
    n
  };
}

Where It Is Allowed​

entry_requires is for concrete public actor entrypoints:

  • public func
  • public query func
  • public shared({caller}) func
  • Public methods in actor classes

Do not use it on private helpers, module helpers, pure functions, ghost functions, lemmas, abstract declarations, or bodyless trusted declarations. Those are not executable external entrypoints.

Async Boundary Note​

Parameter facts and shared({caller}) facts established by entry_requires remain stable across await. Actor-state facts may not remain true after await unless an invariant re-establishes them.

public shared({caller}) func stableCaller(expected : Principal) : async Principal
  entry_requires caller == expected;
  requires caller == expected;
  ensures result == expected;
{
  caller
}

For state that must hold after await, express the stable part as an actor invariant or re-check it after the await.

Summary​

  • entry_requires is the runtime guard for public actor methods.
  • Pair it with requires when the verifier needs the same fact in the body.
  • Public actor methods with nontrivial requires need an entry_requires guard in Viper mode.
  • Entry guards must be strong enough to prove the logical requires.
  • Use shared({caller}) and Principal for caller-based access control.
  • Do not use ghost state, old(), result, or impure calls in entry_requires.