Ownership Predicates

Ownership predicates are the verification mechanism that tracks permissions for mutable records. They bundle field permissions into a single token that the verifier manages automatically at call boundaries and field accesses.

What Are Ownership Predicates

When you define a mutable record type like { var x : Int }, the verifier generates an ownership predicate that bundles permissions for all fields. This predicate:

Grants access to the record's fields
Must be held to read or write any field
Transfers temporarily when passing the record to a function
Returns to the caller when the function completes

The naming convention is Owned$MutRec$HASH, where HASH is derived from the type structure. You never write these names directly, but you may see them in error messages.

Basic Ownership

When a function accepts a mutable record parameter, it temporarily receives ownership:

ownership-basic.sr9
// Basic ownership predicate demonstration
// Shows how the verifier tracks permissions for mutable records

persistent actor OwnershipBasic {
  type Cell = { var x : Int };

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

  // Increment requires ownership of the cell
  private func incr(c : Cell) : ()
    ensures c.x == old(c.x) + 1;
  {
    c.x := c.x + 1;
  };

  // Reading also requires ownership (to access the field)
  private func getValue(c : Cell) : Int
    ensures result == c.x;
  {
    c.x
  };

  // Actor methods declare which fields they access
  public func increment() : async ()
    modifies cell
    ensures cell.x == old(cell.x) + 1;
  {
    incr(cell);
  };

  public func read() : async Int
    reads cell
    ensures result == cell.x;
  {
    getValue(cell)
  };
}

Key points:

The incr function receives ownership of c for its duration
While incr executes, it has exclusive access to c.x
When incr returns, ownership flows back to the caller
Actor methods declare their field access via modifies or reads

Fold and Unfold

Under the hood, ownership predicates use fold and unfold operations:

Unfold: Opens the predicate to access individual field permissions
Fold: Closes the predicate, bundling permissions back together

The verifier inserts these automatically. You write code normally, and the verifier manages the permission bookkeeping:

ownership-fold-unfold.sr9
// Demonstrates fold/unfold semantics for ownership predicates
// The verifier automatically manages these operations

persistent actor OwnershipFoldUnfold {
  type Point = { var x : Int; var y : Int };

  var origin : Point = { var x = 0; var y = 0 };

  // Each field access temporarily unfolds the ownership predicate
  // Multiple accesses in sequence work correctly
  private func translate(p : Point, dx : Int, dy : Int) : ()
    ensures p.x == old(p.x) + dx;
    ensures p.y == old(p.y) + dy;
  {
    // First access: unfold, read x, fold
    // Second access: unfold, write x, fold
    // Third access: unfold, read y, fold
    // Fourth access: unfold, write y, fold
    // The verifier inserts these automatically
    p.x := p.x + dx;
    p.y := p.y + dy;
  };

  public func moveOrigin(dx : Int, dy : Int) : async ()
    modifies origin
    ensures origin.x == old(origin.x) + dx;
    ensures origin.y == old(origin.y) + dy;
  {
    translate(origin, dx, dy);
  };
}

For the translate function, the generated Viper code includes:

unfold Owned$MutRec$...(p)  // Get permission for p.x
p.x := p.x + dx
fold Owned$MutRec$...(p)    // Release permission
unfold Owned$MutRec$...(p)  // Get permission for p.y
p.y := p.y + dy
fold Owned$MutRec$...(p)    // Release permission

This is invisible in your Sector9 code but explains the verification mechanics.

Opaque Owner Transactions

Opaque types with payload invariants use the same ownership machinery, but with one extra rule: inside the owner module, a mutator may temporarily break the opaque invariant while it updates several payload fields. The verifier keeps the owner carrier open, marks it dirty, and closes it once at a stable boundary.

Stable boundaries include:

returning from the owner method
crossing an await
calling another method with the dirty owner or one of its projected children
an internal explicit owner close point

That means this pattern is allowed when the method repairs the invariant before the boundary:

public type Pair = opaque {
  var left : Nat;
  var right : Nat;
  invariant left == right
};

public pure func model(pair : Pair) : Nat
  requires true;
  ensures result == pair.left;
{
  pair.left
};

public func bump(pair : Pair, amount : Nat) : ()
  ensures model(pair) == old(model(pair)) + amount;
{
  pair.left += amount;
  pair.right += amount;
}

If the method returns, awaits, or calls out while left == right is still broken, verification fails when the owner carrier is closed. The OP4 regression fixtures test/viper/op4/opaque_owner_two_field_transaction_sat.mo, test/viper/op4/opaque_owner_dirty_exit_unsat.mo, and test/viper/op4/opaque_owner_dirty_await_boundary_unsat.mo pin this behavior.

Nested Ownership

When mutable records are nested, each level has its own ownership predicate. Accessing a deeply nested field requires unfolding each level:

ownership-nested.sr9
// Nested ownership predicates for nested mutable records
// Each level has its own Owned predicate

persistent actor OwnershipNested {
  type Inner = { var value : Int };
  type Outer = { inner : Inner };

  var data : Outer = { inner = { var value = 42 } };

  // Accessing nested mutable field requires unfolding both predicates
  private func readDeep(o : Outer) : Int
    ensures result == o.inner.value;
  {
    // Unfolds Outer predicate to access inner
    // Unfolds Inner's Owned predicate to read value
    o.inner.value
  };

  private func writeDeep(o : Outer, v : Int) : ()
    ensures o.inner.value == v;
  {
    o.inner.value := v;
  };

  public func update(v : Int) : async ()
    modifies data
    ensures data.inner.value == v;
  {
    writeDeep(data, v);
  };

  public func read() : async Int
    reads data
    ensures result == data.inner.value;
  {
    readDeep(data)
  };
}

For type Outer = { inner : Inner } where Inner = { var value : Int }:

Owned$Outer contains permission for the inner field (which is a reference)
Owned$Inner contains permission for inner.value
Accessing o.inner.value requires unfolding both predicates

The verifier tracks this hierarchy and unfolds as needed.

Ownership Transfer

Ownership transfers temporarily when you pass a mutable record to a function:

ownership-transfer.sr9
// Ownership transfer between caller and callee
// The callee receives temporary ownership

persistent actor OwnershipTransfer {
  type Counter = { var count : Nat };

  var counter : Counter = { var count = 0 };

  // This function receives ownership of the counter
  // Caller gives up ownership during the call
  // Caller regains ownership when function returns
  private func bumpAndGet(c : Counter) : Nat
    ensures c.count == old(c.count) + 1;
    ensures result == c.count;
  {
    c.count := c.count + 1;
    c.count
  };

  // Multiple sequential calls work correctly
  // Ownership flows: caller -> bump1 -> caller -> bump2 -> caller
  public func bumpTwice() : async Nat
    modifies counter
    ensures counter.count == old(counter.count) + 2;
    ensures result == counter.count;
  {
    ignore bumpAndGet(counter);  // First bump: 0 -> 1
    bumpAndGet(counter)          // Second bump: 1 -> 2
  };
}

The ownership flow for bumpTwice is:

bumpTwice has ownership of counter (via modifies counter)
First call: ownership transfers to bumpAndGet
bumpAndGet returns: ownership returns to bumpTwice
Second call: ownership transfers again
bumpAndGet returns: ownership returns to bumpTwice
bumpTwice returns: ownership returns to actor state

This transfer-and-return pattern enables modular verification while preserving the caller's frame. It is the mutable-record version of the same call-site discipline described in framing and permissions.

Ownership and Await

Ownership predicates interact importantly with await boundaries. Across an await, other messages may run and any public write effect on actor state must be accounted for:

ownership-error_unsat.sr9
// Demonstration of ownership predicate violation
// This example fails verification due to missing ownership

persistent actor OwnershipError {
  type Cell = { var x : Int };

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

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

  // This fails: after await, cell's value may have changed
  // The ownership predicate is not preserved across await
  public func broken() : async ()
    modifies cell
    ensures cell.x == old(cell.x) + 1;  // FAILS
  {
    let before = cell.x;
    try {
      await bump();
    } catch (_) {};
    // At this point, cell could have any value due to interference
    // The ensures clause cannot be proven
    assert cell.x == before + 1;
  };
}

This example wraps await in try/catch, as required by the async safety rule, but still fails verification because:

Before the await, cell.x has some value
The await introduces an interference point
Another call path may modify the same actor field
After the await, the verifier cannot prove the postcondition from the saved local value alone

The verifier correctly rejects this because the ensures clause cannot be proven. See Async Verification for patterns that work across await.

Understanding Error Messages

When verification fails due to ownership issues, you may see messages like:

Insufficient permission to access Owned$MutRec$2eb11964

This means:

The code tried to access a mutable record field
The required ownership predicate was not available
The 2eb11964 is the type hash (ignore it)

Common causes:

Missing modifies clause for actor fields
Missing reads for field reads
Missing modifies for field writes
Passing aliased records to a contract that assumes distinct objects
Keeping an alias to actor state live across await

The Allocation Method

When you create a mutable record, the verifier generates an allocation method that establishes the ownership predicate:

let cell : Cell = { var x = 42 };

Becomes (conceptually):

$r := $alloc_MutRec$HASH(42)
// Postcondition: Owned$MutRec$HASH($r) && $r.x == 42

The allocation method:

Creates a new reference
Initializes fields to the provided values
Grants the caller the ownership predicate

This is why freshly created records are immediately usable without explicit permission declarations.

MemBlock Predicates

For advanced scenarios, the verifier also generates $MemBlock$MutRec$HASH predicates. These support internal proof steps such as:

$mem_block_split: Unfolds the predicate to expose raw field permissions
$mem_block_join: Folds raw permissions back into the predicate

You do not use these directly, but they enable the verifier to handle complex permission patterns internally.

Snapshot Domains

For old() expressions on mutable records, the verifier generates snapshot domains. When you write:

ensures c.x == old(c.x) + 1

The verifier captures the pre-state value using an immutable snapshot type Snap$MutRec$HASH. This allows comparing values across state changes without permission complications.

Summary

Ownership predicates bundle permissions for mutable record fields
The naming convention is Owned$MutRec$HASH
Fold/unfold operations are inserted automatically to access fields
Opaque owner transactions allow temporary invariant breaks inside the owner module, but the owner carrier is rechecked before stable boundaries
Nested records have hierarchical ownership predicates
Ownership transfers temporarily to callees and returns after
Await boundaries can invalidate facts about actor-owned records
Error messages mentioning Owned$ indicate permission issues
Allocation establishes fresh ownership predicates

Mutable record types for syntax and restrictions
Aliasing restrictions for same-object parameters
Local vs shared state for await and escape behavior

What Are Ownership Predicates​

Basic Ownership​

Fold and Unfold​

Opaque Owner Transactions​

Nested Ownership​

Ownership Transfer​

Ownership and Await​

Understanding Error Messages​

The Allocation Method​

MemBlock Predicates​

Snapshot Domains​

Summary​

Related Topics​