Set Operations

Sets are specification-only collections for membership reasoning. They model mathematical sets with union, intersection, and subset operations, useful for tracking permissions, visited states, or unique identifiers.

The core Set module is a ghost API over Sector9's trusted primitive collection model. Sets are proof data, not runtime containers. When runtime code needs a collection, use a runtime module and expose the proof shape through that module's Spec API.

Creating Sets

Create a Set with Set.empty<T>() or Set.singleton(element):

set-basic.sr9

// Creating Sets
persistent actor {
  public func check() : async () {
    ghost {
      // Empty set
      let empty : Set<Nat> = Set.empty<Nat>();
      assert Set.card(empty) == 0;

      // Singleton set
      let single = Set.singleton(42);
      assert Set.card(single) == 1;
      assert Set.contains(42, single);
    };
  };
}

Sets are typed with element type T. Elements must be spec-immutable types, except opaque/token handles by identity.

Core Operations

Set.empty<T>()

Creates an empty Set of type Set<T>:

let empty : Set<Nat> = Set.empty<Nat>();
assert Set.card(empty) == 0;

Set.singleton(e)

Creates a Set containing exactly one element:

let s = Set.singleton(42);
assert Set.card(s) == 1;
assert Set.contains(42, s);

Set.contains(e, s)

Returns true if element e is in Set s:

let s = Set.singleton(1);
assert Set.contains(1, s);       // true
assert not Set.contains(2, s);   // true

Note the argument order: element first, then Set.

Set.card(s)

Returns the cardinality (number of elements) in the Set as an Int:

let s = Set.union(Set.singleton(1), Set.singleton(2));
assert Set.card(s) == 2;

Set.union(s1, s2)

Combines elements from both Sets:

set-union.sr9

// Set union combines elements from both sets
persistent actor {
  public func check() : async () {
    ghost {
      let a = Set.singleton(1);
      let b = Set.singleton(2);
      let combined = Set.union(a, b);

      assert Set.contains(1, combined);  // from a
      assert Set.contains(2, combined);  // from b
      assert Set.card(combined) == 2;
    };
  };
}

Union returns a new Set containing elements from both inputs. The input Sets remain usable afterward. See Set Algebra for the algebraic properties.

Set.intersect(s1, s2)

Returns elements present in both Sets:

set-intersect.sr9

// Set intersection finds common elements
persistent actor {
  public func check() : async () {
    ghost {
      let a = Set.union(Set.singleton(1), Set.singleton(2));
      let b = Set.union(Set.singleton(2), Set.singleton(3));
      let common = Set.intersect(a, b);

      assert Set.contains(2, common);      // in both
      assert not Set.contains(1, common);  // only in a
      assert not Set.contains(3, common);  // only in b
    };
  };
}

Set.minus(s1, s2)

Returns elements in s1 that are not in s2 (set difference):

set-minus.sr9

// Set difference removes elements
persistent actor {
  public func check() : async () {
    ghost {
      let all = Set.union(Set.singleton(1), Set.singleton(2));
      let toRemove = Set.singleton(2);
      let result = Set.minus(all, toRemove);

      assert Set.contains(1, result);      // kept
      assert not Set.contains(2, result);  // removed
    };
  };
}

Set.subset(s1, s2)

Returns true if all elements of s1 are in s2:

set-subset.sr9

// Subset relation
persistent actor {
  public func check() : async () {
    ghost {
      let small = Set.singleton(1);
      let big = Set.union(Set.singleton(1), Set.singleton(2));

      assert Set.subset(small, big);       // small is subset of big
      assert not Set.subset(big, small);   // big is not subset of small

      // Empty set is subset of everything
      let empty = Set.empty<Int>();
      assert Set.subset(empty, small);
    };
  };
}

The empty Set is a subset of all Sets.

Set Algebra

The trusted primitive set model follows standard mathematical set semantics. Use these laws as proof vocabulary, and keep larger algebraic arguments in small lemmas when a contract starts becoming hard to read.

Union:

• Commutative: Set.union(a, b) equals Set.union(b, a)
• Associative: Set.union(a, Set.union(b, c)) equals Set.union(Set.union(a, b), c)
• Idempotent: Set.union(a, a) equals a

Intersection:

• Commutative and associative
• Set.intersect(a, Set.empty()) equals Set.empty()

Difference:

• Set.minus(a, a) equals Set.empty()
• Set.minus(a, Set.empty()) equals a

Value Semantics

Set operations that produce new Sets (union, intersect, minus) are ghost, side-effect-free operations: they return persistent values and leave their inputs usable. Read-only operations (contains, card, subset) can also be repeated freely:

ghost {
  let s = Set.singleton(1);
  let c1 = Set.contains(1, s);   // s still valid
  let c2 = Set.contains(2, s);   // s still valid
  let size = Set.card(s);         // s still valid
};

Ghost Set Fields

Declare ghost Set fields at actor level to track membership state:

set-ghost-field.sr9

// Ghost Set fields track membership
persistent actor {
  ghost var approved : Set<Nat> = Set.empty();

  invariant Set.card(approved) >= 0;

  public func approve(id : Nat) : async ()
    modifies approved
    ensures Set.contains(id, approved);
  {
    ghost {
      approved := Set.union(approved, Set.singleton(id));
    };
  };

  public func revoke(id : Nat) : async ()
    modifies approved
    ensures not Set.contains(id, approved);
  {
    ghost {
      approved := Set.minus(approved, Set.singleton(id));
    };
  };
}

Ghost Sets are updated inside ghost { } blocks using assignment. Include ghost Set fields in modifies clauses.

Using Sets in Invariants

Sets work well in actor invariants for membership properties:

persistent actor {
  ghost var admins : Set<Nat> = Set.singleton(0);

  invariant Set.card(admins) >= 1;  // Always at least one admin

  public func addAdmin(p : Nat) : async ()
    modifies admins
    ensures Set.contains(p, admins)
  {
    ghost {
      admins := Set.union(admins, Set.singleton(p));
    };
  };
}

Quantifiers with Sets

Combine Sets with quantifiers for expressive specifications:

set-quantifiers.sr9

// Using quantifiers with Sets
persistent actor {
  public func check() : async () {
    ghost {
      let s = Set.union(Set.singleton(1), Set.singleton(2));

      // All elements in s are positive
      assert forall<Int>(pure func (x : Int) : Bool =
        Set.contains(x, s) ==> x > 0);

      // There exists an element equal to 2
      assert exists<Int>(pure func (x : Int) : Bool =
        Set.contains(x, s) and x == 2);
    };
  };
}

Common patterns:

• Use forall with a Set.contains guard to express properties of all members.
• Use exists to assert at least one element satisfies a condition.
• Combine Set.contains with ==> for conditional membership properties.

Sets with Map.domain

Sets integrate with Maps through the Map.domain operation:

ghost {
  let m = Map.update(Map.empty<Nat, Int>(), 1, 100);
  let keys = Map.domain(m);  // Returns Set<Nat>

  assert forall<Nat>(pure func (k : Nat) : Bool =
    Set.contains(k, keys) ==> Map.contains(k, m));
};

Element Type Restrictions

Set elements must be spec-immutable types. The following are rejected:

• Mutable records (with var fields)
• Mutable arrays ([var T])
• Functions (T -> U)
• Actors and modules
• Async types

Opaque/token handles may be set elements by identity. The set stores the handle, not a snapshot of its owner payload.

set-immutable-reject_reject.sr9

// Set element types must be spec-immutable
persistent actor {
  type MutableCell = { var value : Int };  // Has var field

  public func check() : async () {
    ghost {
      // ERROR: Mutable record cannot be Set element
      let s : Set<MutableCell> = Set.empty();
    };
  };
}

Allowed types include primitives (Nat, Int, Bool, Text), immutable records, tuples, variants, and options with immutable element types.

Operation Reference

Operation	Signature	Mutates/Consumes Input	Description
Set.empty<T>()	Set<T>	-	Create empty Set
Set.singleton(e)	Set<T>	-	Create single-element Set
Set.contains(e, s)	Bool	No	Check membership
Set.card(s)	Int	No	Count of elements
Set.union(s1, s2)	Set<T>	No	Combine elements
Set.intersect(s1, s2)	Set<T>	No	Common elements
Set.minus(s1, s2)	Set<T>	No	Difference (s1 - s2)
Set.subset(s1, s2)	Bool	No	Check subset relation

Common Patterns

Permission Tracking

persistent actor {
  ghost var permissions : Set<Nat> = Set.empty();

  public func grant(user : Nat) : async ()
    modifies permissions
    ensures Set.contains(user, permissions);
  {
    ghost {
      permissions := Set.union(permissions, Set.singleton(user));
    };
  };

  public func revoke(user : Nat) : async ()
    modifies permissions
    ensures not Set.contains(user, permissions);
  {
    ghost {
      permissions := Set.minus(permissions, Set.singleton(user));
    };
  };
}

Visited State Tracking

ghost {
  var visited : Set<Nat> = Set.empty();
  let id : Nat = 42;

  assert not Set.contains(id, visited);
  visited := Set.union(visited, Set.singleton(id));
  assert Set.contains(id, visited);
}

Unique Identifiers

ghost var used : Set<Nat> = Set.empty();

public func allocate(id : Nat) : async Bool
  modifies used
  ensures result == not Set.contains(id, old(used))
  ensures result ==> Set.contains(id, used)
{
  if (Set.contains(id, used)) {
    false
  } else {
    ghost {
      used := Set.union(used, Set.singleton(id));
    };
    true
  }
}

Summary

• Sets are specification-only membership collections
• Set operations are ghost proof operations over a trusted primitive collection model
• Create with Set.empty<T>() or Set.singleton(element)
• Query with Set.contains, Set.card, Set.subset
• Combine with Set.union, Set.intersect, Set.minus
• Set algebra operations return new Sets; inputs remain usable
• Elements must be spec-immutable (no mutable fields, arrays, or functions), except opaque/token handles by identity
• Use ghost Set fields with modifies clauses for actor-level tracking
• Combine with quantifiers and Map.domain for expressive invariants

Related Topics

• Map operations for Map.domain and key sets
• Collection restrictions for spec-immutable element rules
• Ghost variables for actor-level permission sets
• Quantifier patterns for membership-guarded properties
• Trusted base for the soundness boundary behind primitive collections