Permission Errors

Understanding and fixing "missing permission" failures.

Overview

Permission errors occur when code accesses actor state without declaring the required reads or modifies clause. The verifier rejects such programs to ensure sound reasoning about state changes.

Tests with _reject, _unsat, or older _noperm-style names demonstrate expected permission failures. These failures fall into two categories:

Error Type	When It Occurs	Error Source
Translation error	Missing reads/modifies declaration	Sector9 frontend
Verification error	Out-of-bounds access or assertion depending on unavailable permission	Viper backend
Await-safety error	A live local may reference actor state across suspension	Sector9 await analysis

Missing Reads Permission

Reading a field without a reads clause causes a translation error:

perm-error-missing-reads_reject.sr9

// Permission error: missing reads clause
persistent actor MissingReads {
  var counter : Nat = 0;

  // ERROR: reads clause missing fields: counter
  public func getCounter() : async Nat {
    counter  // Reading without permission
  };
}

The error message identifies the missing field:

reads clause missing fields: counter; add `reads counter` (or `modifies counter` for written fields)

How to Fix

Add the field to the reads clause:

perm-error-missing-reads-fixed.sr9

// Fixed: added reads clause
persistent actor FixedReads {
  var counter : Nat = 0;

  // Correct: reads counter grants read permission
  public func getCounter() : async Nat reads counter {
    counter
  };
}

Missing Modifies Permission

Writing to a field without a modifies clause causes a translation error:

perm-error-missing-modifies_reject.sr9

// Permission error: missing modifies clause
persistent actor MissingModifies {
  var counter : Nat = 0;

  // ERROR: modifies clause missing fields: counter
  public func increment() : async () {
    counter += 1;  // Writing without permission
  };
}

The error message identifies the missing field:

modifies clause missing fields: counter; add `modifies counter`

How to Fix

Add the field to the modifies clause:

perm-error-missing-modifies-fixed.sr9

// Fixed: added modifies clause
persistent actor FixedModifies {
  var counter : Nat = 0;

  // Correct: modifies counter grants write permission
  public func increment() : async () modifies counter {
    counter += 1;
  };
}

Transitive Permission Errors

If function A calls function B, and B reads or modifies a field, then A must also declare that permission. The verifier tracks field accesses transitively across the call graph.

perm-error-transitive_reject.sr9

// Permission error: missing transitive permission
persistent actor TransitiveError {
  var config : Int = 100;

  // Helper reads config
  private func helper() : Int reads config {
    config
  };

  // ERROR: reads clause missing fields: config
  // Caller must also declare permission for callee's accesses
  public func caller() : async Int {
    helper()
  };
}

Even though caller does not directly access config, it calls helper which does. The error message indicates:

reads clause missing fields: config; add `reads config` (or `modifies config` for written fields)

How to Fix

Declare the transitive permission in the caller:

perm-error-transitive-fixed.sr9

// Fixed: caller declares transitive permission
persistent actor TransitiveFixed {
  var config : Int = 100;

  private func helper() : Int reads config {
    config
  };

  // Correct: caller declares reads config for helper's access
  public func caller() : async Int reads config {
    helper()
  };
}

Permission Errors After Await

When a local variable escapes to actor state, it can be modified by interleaving messages during an await. Current verification mode rejects that shape if the actor-state reference remains live across the await boundary.

perm-error-escaped-local_unsat.sr9

// Permission error: escaped local across await
persistent actor EscapedLocal {
  type Cell = { var x : Int };

  var stored : Cell = { var x = 0 };

  private func bump() : async () modifies stored {
    stored.x := stored.x + 1;
  };

  public func run() : async () modifies stored {
    let local : Cell = { var x = 1 };
    stored := local;           // local escapes to actor state
    let before = local.x;
    try {
      await bump();            // interleaving can mutate stored (== local)
    } catch (_) {};
    assert local.x == before;  // FAILS: insufficient permission
  };
}

This produces an await-safety translation error:

await may not cross references to actor state; drop or copy before await (live: local)

Why This Happens

1. The fresh local { var x = 1 } is initially stable across await
2. Assigning stored := local causes the local to escape to actor state
3. The awaited call is a suspension point where other public methods may write actor state
4. The verifier rejects the live reference because it would carry actor-state reachability across the boundary

How to Fix

There are two approaches:

Option 1: Do not escape the local Keep the local separate from actor state if you need to preserve its value:

public func run() : async () modifies stored {
  let local : Cell = { var x = 1 };
  let before = local.x;
  try { await bump(); } catch (_) {};
  assert local.x == before;  // OK: local never escaped
};

Option 2: Use actor invariants If escaping is necessary, do not keep the mutable reference live across await. Snapshot primitive facts before suspension and use actor invariants to constrain the actor state:

invariant stored.x >= 0

Array Permission Errors

Array accesses require permission for the specific index. If an index is out of bounds, the verifier cannot prove permission exists.

perm-error-array-bounds_unsat.sr9

// Permission error: array out-of-bounds access
persistent actor ArrayBounds {
  var arr : [var Nat] = [var 1, 2, 3];

  invariant arr.size() == 3;

  // FAILS: insufficient permission to access index 5
  // The invariant guarantees only indices 0, 1, 2 are valid
  public func accessOutOfBounds() : async Nat modifies arr {
    arr[5]
  };
}

The invariant arr.size() == 3 only grants permission for indices 0, 1, and 2. Accessing index 5 fails:

There might be insufficient permission to access $loc($Self.fld$arr, 5)

How to Fix

Guard array access with bounds checking:

public func safeAccess(i : Nat) : async Nat
  reads arr
  entry_requires i < arr.size();
  requires i < arr.size();
{
  arr[i]  // OK: precondition ensures i is in bounds
};

Reading Error Messages

Permission errors come in two formats depending on when they are detected:

Translation Errors (Frontend)

Detected before Viper verification. Format:

<file>:<line>.<col>-<line>.<col>: viper error [0], translation to viper failed:
<reads|modifies> clause missing fields: fld$<fieldname>

These are the most common permission errors. The fix is always to add the missing field to the appropriate clause.

Verification Errors (Backend)

Detected by the Viper/Silicon verifier. Format:

{
  "msg": "Assert might fail. There might be insufficient permission to access ...",
  "fix_hints": [
    "Add proof steps or strengthen preconditions to establish the assertion.",
    "Add missing reads/modifies or ensure permissions are in scope."
  ]
}

These errors indicate more complex permission issues:

• Out-of-bounds array access
• Aliased state with interleaving
• Assertions that depend on facts lost at await boundaries

Debugging Checklist

When you encounter a permission error:

1. Check the error location: The line and column point to the access that lacks permission

2. Identify the field: The error message names the missing field (e.g., fld$counter)

3. Add the declaration:

   • For reads: add reads fieldname to the function signature
   • For writes: add modifies fieldname to the function signature

4. Check transitive accesses: If you call helper functions, add their permissions to your function

5. Check for escaping: If the error is near await, check if a live local can reach actor state

6. Check array bounds: For array access errors, ensure index is within bounds via preconditions or guards

Common Patterns

Pattern	Error	Fix
Reading field without reads	reads clause missing fields: x	Add reads x
Writing field without modifies	modifies clause missing fields: x	Add modifies x
Calling helper that accesses field	reads/modifies clause missing fields: x	Add permission to caller
Local escapes to actor state	await may not cross references to actor state	Avoid escape, drop the reference, or snapshot values
Array index out of bounds	insufficient permission to access $loc(...)	Add bounds precondition

Summary

• Permission errors occur when code accesses state without declaring reads or modifies
• Translation errors are caught early and identify the exact missing field
• Verification errors indicate complex issues like bounds violations or assertions that depend on unavailable permissions
• Transitive permissions must be declared: if A calls B, A needs B's permissions
• Locals that can reach actor state must not remain live across await
• Array access requires permission for the specific index, guarded by bounds checks

Related Topics

• Read vs write permissions for the permission hierarchy
• Local vs shared state for escaped locals across await
• Await frames for facts lost or preserved across suspension
• Debugging verification errors for interpreting frontend and backend diagnostics