Multiset Operations

Multisets (also called bags) are specification-only collections that track element multiplicities. Unlike Sets where each element is either present or absent, Multisets count how many times each element appears. This makes them ideal for modeling inventories, vote counts, or resource pools.

The core Multiset module is a ghost API over Sector9's trusted primitive collection model. Use it when a proof needs quantity without order. If runtime code stores the same facts, keep the runtime structure separate and expose or mirror a ghost model for verification.

Creating Multisets

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

multiset-basic.sr9

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

      // Singleton multiset
      let single = Multiset.singleton(42);
      assert Multiset.card(single) == 1;
      assert Multiset.contains(42, single);
      assert Multiset.count(single, 42) == 1;
    };
  };
}

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

Core Operations

Multiset.empty<T>()

Creates an empty Multiset of type Multiset<T>:

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

Multiset.singleton(e)

Creates a Multiset containing exactly one occurrence of an element:

let m = Multiset.singleton(42);
assert Multiset.count(m, 42) == 1;
assert Multiset.contains(42, m);

Multiset.count(m, e)

Returns the multiplicity (number of occurrences) of element e in Multiset m:

multiset-count.sr9

// Counting multiplicities in Multisets
persistent actor {
  public func check() : async () {
    ghost {
      // Union accumulates multiplicities
      let a = Multiset.singleton<Int>(1);
      let b = Multiset.singleton<Int>(1);
      let m = Multiset.union(a, b);

      // Element 1 appears twice
      assert Multiset.count(m, 1) == 2;
      assert Multiset.card(m) == 2;  // Total cardinality

      // Element 2 has count 0
      assert Multiset.count(m, 2) == 0;
      assert not Multiset.contains(2, m);
    };
  };
}

This is the key operation that distinguishes Multisets from Sets. The count returns an Int; proofs normally establish that counts are non-negative for the cases they use.

Multiset.contains(e, m)

Returns true if element e appears at least once in Multiset m:

let m = Multiset.singleton(1);
assert Multiset.contains(1, m);       // true (count is 1)
assert not Multiset.contains(2, m);   // true (count is 0)

Note the argument order: element first, then Multiset. This operation is equivalent to Multiset.count(m, e) > 0.

Multiset.card(m)

Returns the total cardinality (sum of all multiplicities) in the Multiset:

let a = Multiset.singleton<Int>(1);
let b = Multiset.singleton<Int>(1);
let m = Multiset.union(a, b);
assert Multiset.card(m) == 2;  // Total count, not unique elements

Unlike Set.card which counts unique elements, Multiset.card returns the sum of all element counts.

Multiset.union(m1, m2)

Combines two Multisets by adding multiplicities:

multiset-union.sr9

// Multiset union adds multiplicities
persistent actor {
  public func check() : async () {
    ghost {
      let m = Multiset.singleton<Int>(1);
      let n = Multiset.singleton<Int>(2);
      let u = Multiset.union(m, n);

      // Both elements present
      assert Multiset.contains(1, u);
      assert Multiset.contains(2, u);
      assert Multiset.card(u) == 2;

      // Union with duplicates
      let a = Multiset.singleton<Int>(5);
      let b = Multiset.singleton<Int>(5);
      let c = Multiset.union(a, b);
      assert Multiset.count(c, 5) == 2;  // Counts add
    };
  };
}

Union returns a new Multiset with combined multiplicities. The input Multisets remain usable afterward. See Multiset Algebra for the algebraic properties.

Multiset.intersect(m1, m2)

Returns a Multiset with the minimum count of each element:

multiset-intersect.sr9

// Multiset intersection takes minimum count
persistent actor {
  public func check() : async () {
    ghost {
      let a = Multiset.singleton<Int>(5);
      let b = Multiset.singleton<Int>(5);
      let c = Multiset.intersect(a, b);

      // Intersection of {5} and {5} is {5}
      assert Multiset.count(c, 5) == 1;
      assert Multiset.contains(5, c);

      // Intersection with disjoint elements
      let m = Multiset.singleton<Int>(1);
      let n = Multiset.singleton<Int>(2);
      let empty = Multiset.intersect(m, n);
      assert Multiset.card(empty) == 0;
    };
  };
}

If element e has count 3 in m1 and count 2 in m2, it has count 2 in the intersection.

Multiset.minus(m1, m2)

Subtracts multiplicities, returning a new Multiset:

multiset-minus.sr9

// Multiset minus subtracts multiplicities
persistent actor {
  public func check() : async () {
    ghost {
      // Create multiset with element 1 appearing twice
      let a = Multiset.singleton<Int>(1);
      let b = Multiset.singleton<Int>(1);
      let m = Multiset.union(a, b);
      assert Multiset.count(m, 1) == 2;

      // Remove one occurrence
      let m2 = Multiset.minus(m, Multiset.singleton<Int>(1));
      assert Multiset.count(m2, 1) == 1;

      // Remove last occurrence
      let m3 = Multiset.minus(m2, Multiset.singleton<Int>(1));
      assert Multiset.count(m3, 1) == 0;
      assert not Multiset.contains(1, m3);
    };
  };
}

Counts are floored at 0. If m1 has count 2 and m2 has count 5 for an element, the result has count 0.

Multiset Algebra

The trusted primitive multiset model follows standard bag algebra semantics. Use these facts to state conservation and accounting properties; when a proof needs several algebraic rewrites, put them behind a small lemma.

Union:

• Adds multiplicities: count(union(a, b), e) == count(a, e) + count(b, e)
• Commutative: Multiset.union(a, b) equals Multiset.union(b, a)
• Associative: union order does not matter

Intersection:

• Takes minimum: count(intersect(a, b), e) == min(count(a, e), count(b, e))
• Commutative and associative
• Multiset.intersect(a, Multiset.empty()) equals Multiset.empty()

Difference:

• Subtracts counts: count(minus(a, b), e) == max(0, count(a, e) - count(b, e))
• Multiset.minus(a, a) equals Multiset.empty()
• Multiset.minus(a, Multiset.empty()) equals a

Value Semantics

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

ghost {
  let m = Multiset.singleton(1);
  let c1 = Multiset.count(m, 1);   // m still valid
  let c2 = Multiset.count(m, 2);   // m still valid
  let has = Multiset.contains(1, m);  // m still valid
  let size = Multiset.card(m);     // m still valid
};

Ghost Multiset Fields

Declare ghost Multiset fields at actor level to track multiplicity state:

multiset-ghost-field.sr9

// Ghost Multiset fields track multiplicities
persistent actor {
  ghost var inventory : Multiset<Nat> = Multiset.empty();

  invariant Multiset.card(inventory) >= 0;

  public func stock(item : Nat) : async ()
    modifies inventory
  {
    ghost {
      inventory := Multiset.union(inventory, Multiset.singleton(item));
      assert Multiset.contains(item, inventory);
    };
  };

  public func sell(item : Nat) : async ()
    modifies inventory
  {
    ghost {
      inventory := Multiset.minus(inventory, Multiset.singleton(item));
    };
  };
}

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

Using Multisets in Invariants

Multisets work well in actor invariants for resource tracking and conservation laws:

ghost {
  let maxSupply : Nat = 10;
  let to : Nat = 1;
  var tokens : Multiset<Nat> = Multiset.empty();

  assert Multiset.card(tokens) < maxSupply;
  tokens := Multiset.union(tokens, Multiset.singleton(to));
  assert Multiset.count(tokens, to) == 1;
}

Quantifiers with Multisets

Combine Multisets with quantifiers for expressive specifications:

multiset-quantifiers.sr9

// Quantifiers with Multisets
persistent actor {
  ghost var votes : Multiset<Nat> = Multiset.empty();

  public func check() : async () {
    ghost {
      // Create multiset with votes for options 1 and 2
      let v1 = Multiset.union(
        Multiset.singleton<Nat>(1),
        Multiset.singleton<Nat>(1)
      );
      let v2 = Multiset.singleton<Nat>(2);
      votes := Multiset.union(v1, v2);

      // All elements have positive count
      assert forall<Nat>(pure func (x : Nat) : Bool =
        Multiset.contains(x, votes) ==> Multiset.count(votes, x) > 0);

      // There exists an element with count 2
      assert exists<Nat>(pure func (x : Nat) : Bool =
        Multiset.count(votes, x) == 2);
    };
  };
}

Common patterns:

• Use forall with a Multiset.contains guard to express properties of all present elements.
• Use exists to assert at least one element has a specific count.
• Combine Multiset.count with arithmetic in predicates for balances, votes, and inventory limits.

Element Type Restrictions

Multiset 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 multiset elements by identity. Multiplicity facts count handles, not owner payload snapshots.

multiset-immutable-reject_reject.sr9

// Multiset 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 Multiset element
      let m : Multiset<MutableCell> = Multiset.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
Multiset.empty<T>()	Multiset<T>	-	Create empty Multiset
Multiset.singleton(e)	Multiset<T>	-	Create single-element Multiset
Multiset.count(m, e)	Int	No	Get element multiplicity
Multiset.contains(e, m)	Bool	No	Check if count > 0
Multiset.card(m)	Int	No	Sum of all multiplicities
Multiset.union(m1, m2)	Multiset<T>	No	Add multiplicities
Multiset.intersect(m1, m2)	Multiset<T>	No	Minimum multiplicities
Multiset.minus(m1, m2)	Multiset<T>	No	Subtract multiplicities

Common Patterns

Inventory Tracking

ghost {
  var inventory : Multiset<Nat> = Multiset.empty();
  let item : Nat = 7;
  let qty : Nat = 3;

  var i = 0;
  while (i < qty) loop:invariant i <= qty {
    inventory := Multiset.union(inventory, Multiset.singleton(item));
    i := i + 1;
  };

  assert Multiset.count(inventory, item) >= qty;
}

ghost {
  let item : Nat = 7;
  var inventory : Multiset<Nat> = Multiset.singleton(item);

  assert Multiset.contains(item, inventory);
  inventory := Multiset.minus(inventory, Multiset.singleton(item));
  assert not Multiset.contains(item, inventory);
}

Vote Counting

ghost var votes : Multiset<Nat> = Multiset.empty();

public func vote(option : Nat) : async ()
  modifies votes
  ensures Multiset.count(votes, option) == Multiset.count(old(votes), option) + 1
{
  ghost {
    votes := Multiset.union(votes, Multiset.singleton(option));
  };
}

public func getVotes(option : Nat) : async Int
  reads votes
  ensures result == Multiset.count(votes, option)
{
  Multiset.count(votes, option)
}

Resource Pool

ghost var pool : Multiset<Nat> = Multiset.empty();

invariant Multiset.card(pool) <= MAX_RESOURCES;

public func acquire(resource : Nat) : async Bool
  modifies pool
  ensures result == Multiset.contains(resource, old(pool))
  ensures result ==> Multiset.count(pool, resource) == Multiset.count(old(pool), resource) - 1
{
  if (Multiset.contains(resource, pool)) {
    ghost {
      pool := Multiset.minus(pool, Multiset.singleton(resource));
    };
    true
  } else {
    false
  }
}

Multiset vs Set

Use Multisets when you need to track quantities. Use Sets when you only need presence/absence:

Property	Multiset	Set
Duplicates	Allowed (counts accumulate)	Not allowed
Count semantics	count(m, e) returns 0, 1, 2, ...	Implicit: 0 or 1
Cardinality	Sum of all counts	Number of unique elements
Use cases	Inventory, votes, resources	Permissions, visited states

Summary

• Multisets are specification-only collections that track element multiplicities
• Multiset operations are ghost proof operations over a trusted primitive collection model
• Create with Multiset.empty<T>() or Multiset.singleton(element)
• Query with Multiset.count, Multiset.contains, Multiset.card
• Combine with Multiset.union (add counts), Multiset.intersect (min counts), Multiset.minus (subtract counts)
• Algebra operations return new Multisets; inputs remain usable
• Elements must be spec-immutable (no mutable fields, arrays, or functions), except opaque/token handles by identity
• Use ghost Multiset fields with modifies clauses for actor-level tracking
• Combine with quantifiers for expressive invariants about multiplicities

Related Topics

• Set operations for presence/absence models
• Sequence operations for ordered histories
• Collection restrictions for spec-immutable element rules
• Quantifier patterns for multiplicity invariants
• Trusted base for the soundness boundary behind primitive collections