Binary Data

Blob for raw bytes and Principal for IC identity. Both are opaque in verification, with equality, ordering comparisons, selected core library contracts, and explicit user contracts as the practical proof surface.

Overview

Blob represents arbitrary binary data (a sequence of bytes), while Principal represents an Internet Computer identity (user, canister, or system component). Both types are modeled mostly as opaque integer-like values in the verifier: equality, ordering comparisons, selected library contracts, and explicit user contracts are useful, but raw byte/principal structure is not exposed for proof.

blob-basic.sr9

// Blob basic operations
module {
  // Compare two blobs for equality
  public func compareBlob(a : Blob, b : Blob) : Bool
    ensures result == (a == b);
  {
    a == b
  };

  // Return input blob unchanged
  public func identityBlob(data : Blob) : Blob
    ensures result == data;
  {
    data
  };

  // Blob reflexivity - every blob equals itself
  public func blobSelfEqual(data : Blob) : Bool
    ensures result == true;
  {
    data == data
  };
}

Blob

Blob Literals

Blob literals are written as text prefixed with a type annotation:

let data : Blob = "\00\01\02\FF";  // Raw bytes
let empty : Blob = "";             // Empty blob

Escape sequences in blob literals represent byte values in hexadecimal (\XX where XX is 00-FF).

Blob Methods

The Blob type provides these methods at runtime:

Method	Return Type	Description
size()	Nat	Number of bytes
get(index)	Nat8	Byte at given index
keys()	Iter<Nat>	Iterator over indices (0 to size-1)
vals()	Iter<Nat8>	Iterator over byte values
values()	Iter<Nat8>	Iterator over byte values (alias for vals)

These methods work at runtime but have limited verification support. Prefer the core Blob functions in verified contracts: Blob.size, Blob.empty, Blob.fromArray, Blob.fromVarArray, Blob.toArray, and Blob.toVarArray expose trusted size facts. Arbitrary byte contents and indexing are not a general proof surface. Prefer equality, explicit contracts, or a higher-level model when the bytes carry protocol meaning.

Blob in Contracts

You can verify equality-based properties on blobs:

blob-select.sr9

// Blob selection with equality postconditions
module {
  // Select between two blobs based on condition
  public func selectBlob(useFirst : Bool, first : Blob, second : Blob) : Blob
    ensures useFirst ==> result == first;
    ensures (not useFirst) ==> result == second;
  {
    if (useFirst) { first } else { second }
  };
}

Principal

Principal Basics

Principal represents an IC identity - the cryptographic identifier for users, canisters, and system components. Every actor on the IC has a unique principal.

principal-basic.sr9

// Principal basic operations
module {
  // Compare two principals for equality
  public func samePrincipal(a : Principal, b : Principal) : Bool
    ensures result == (a == b);
  {
    a == b
  };

  // Principal reflexivity - every principal equals itself
  public func principalSelfEqual(p : Principal) : Bool
    ensures result == true;
  {
    p == p
  };

  // Return input principal unchanged
  public func identityPrincipal(p : Principal) : Principal
    ensures result == p;
  {
    p
  };
}

Principal Literals

Principal literals use the actor syntax:

let mgmt : actor {} = actor "aaaaa-aa";  // Management canister

The string form uses a base32-like encoding with check digits. At runtime, Sector9 inherits primitive conversions between Principal and Blob, but the verified lane treats principal structure opaquely; rely on equality, storage, and explicit contracts rather than parsing facts.

Principal Selection

Conditional selection based on principal comparison verifies correctly:

principal-select.sr9

// Principal selection with equality postconditions
module {
  // Select between two principals based on condition
  public func selectPrincipal(cond : Bool, a : Principal, b : Principal) : Principal
    ensures cond ==> result == a;
    ensures (not cond) ==> result == b;
  {
    if (cond) { a } else { b }
  };
}

Principal in Spec Collections

Principal can be used as a key in ghost collections since it supports equality. Use that for proof models of permissions, roles, and ownership; deployable access control still needs runtime state:

principal-in-collection.sr9

module {
  public ghost func isAdmin(admins : Set<Principal>, p : Principal) : Bool
    ensures result == Set.contains(p, admins);
  {
    Set.contains(p, admins)
  };

  public ghost func addAdmin(admins : Set<Principal>, p : Principal) : Set<Principal>
    ensures Set.contains(p, result);
  {
    Set.union(admins, Set.singleton(p))
  };
}

Access Control Pattern

A common use of Principal is access control - restricting who can call certain functions:

principal-access-control.sr9

// Principal for access control
persistent actor {
  var owner : ?Principal = null;

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

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

  public func getOwner() : async ?Principal
    reads owner
    ensures result == owner;
  {
    owner
  };

  public func isOwner(p : Principal) : async Bool
    reads owner
    ensures result == (owner == ?p);
  {
    owner == ?p
  };
}

Use shared({caller}) to bind the function caller in verified contracts, or Runtime.callerId() to read the current runtime caller in a method body.

Verification Model

Both Blob and Principal are modeled as opaque integer-like values in the Viper verification backend:

• Equality works correctly - same values compare equal, different values compare unequal
• Ordering comparisons exist - the core Blob.compare and Principal.compare contracts connect #less, #equal, and #greater to the backend ordering relation
• Limited size facts - Blob.size() can appear in contracts, but it remains symbolic unless a core Blob contract gives more facts
• No content analysis - the verifier cannot reason about arbitrary blob contents or principal structure
• Usable in collections - both can serve as keys/values in ghost Map, Set, Seq, and Multiset

This means you can verify:

• Blob and Principal equality and inequality
• ordering wrapper functions such as Blob.compare and Principal.compare
• Passing values through functions unchanged
• Using them in variant types and collections
• Role-based access control patterns with shared({caller}) and entry_requires

But you cannot verify:

• Arbitrary byte contents or indexing facts
• Principal hierarchy or relationships beyond equality
• Semantic relationships between Blob and Principal conversions unless written and trusted as contracts

Limitations

For-In Over Blob Iterators

Blob iterators are supported in verification as long as the iterator's next() method has a type contract. The built-in values()/vals() and keys() satisfy this:

blob-iteration.sr9

// For-in loop over blob.values()
persistent actor {
  public func scan(b : Blob) : async () {
    for (x in b.values()) {
      let _ = x;
    };
  };
}

Note: the verifier still treats blob contents as opaque, so iterating does not let you prove facts about byte values without additional abstraction.

No Byte Content Verification

The verifier can carry symbolic Blob.size() facts and trusted constructor facts, but it cannot inspect raw bytes or derive arbitrary length/content facts from a literal:

// Cannot verify - verifier doesn't model arbitrary indexing
public func firstByte(b : Blob) : Nat8
  requires b.size() > 0
  ensures result == b.get(0);  // Not verifiable
{ b.get(0) }

Candid Serialization

to_candid and from_candid work at runtime but are treated as uninterpreted operations in verification:

persistent actor {
  public func serialize() : async Blob {
    let b : Blob = to_candid (1, true);  // Works but not reasoned about
    b
  };

  public func deserialize(b : Blob) : async ?Nat {
    let x : ?Nat = from_candid b;  // Works but not reasoned about
    x
  };
}

The verifier does not model the relationship between serialized and deserialized values.

Common Patterns

Proof-Only Principal Sets

persistent actor {
  ghost var seen : Set<Principal> = Set.empty<Principal>();

  func markSeen(p : Principal) : ()
    modifies seen
    ensures Set.contains(p, seen);
  {
    ghost {
      seen := Set.union(seen, Set.singleton(p));
    };
  };
}

Role-Based Access

persistent actor {
  var admin : ?Principal = null;

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

  public shared({caller}) func adminOnly() : async ()
    reads admin
    entry_requires admin == ?caller;
    requires admin == ?caller;
  {
    // Only admins can reach here
  };
}

Ownership Tracking

persistent actor {
  var owner : ?Principal = null;

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

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

Summary

• Blob represents arbitrary binary data; Principal represents IC identities
• Both types support equality-based verification via opaque verifier values
• Principal can be used in ghost collections (Map, Set) for proof models, but runtime access control must use runtime state and entry_requires
• The verifier can carry symbolic Blob.size() facts, but not arbitrary blob contents or byte-level operations
• for-in loops over blob iterators are supported, but contents remain opaque
• Candid serialization (to_candid/from_candid) works at runtime but is not modeled in verification
• Common uses include access control, ownership tracking, and identity comparison in contracts