Sequence Operations

Sequences are specification-only ordered collections for verification reasoning. They model mathematical sequences with indexing, slicing, and concatenation, useful for tracking event logs, message histories, or ordered data.

The core Seq module is a ghost API over Sector9's trusted primitive collection model. Use it to describe ordering in contracts and invariants. For runtime storage, use arrays, buffers, or sequence-backed runtime modules and connect them to Seq with Spec.model contracts.

Creating Sequences

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

seq-basic.sr9

// Basic Seq operations: empty, singleton, len, get, concat
persistent actor {
  public func demo() : async () {
    ghost {
      // Create sequences
      let empty : Seq<Nat> = Seq.empty();
      let one = Seq.singleton<Nat>(42);

      // Length
      assert Seq.len(empty) == 0;
      assert Seq.len(one) == 1;

      // Element access
      assert Seq.get(one, 0) == 42;

      // Concatenation
      let s1 = Seq.singleton<Nat>(1);
      let s2 = Seq.singleton<Nat>(2);
      let s3 = Seq.concat(s1, s2);
      assert Seq.len(s3) == 2;
      assert Seq.get(s3, 0) == 1;
      assert Seq.get(s3, 1) == 2;
    };
  };
}

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

Core Operations

Seq.empty<T>()

Creates an empty Seq of type Seq<T>:

let empty : Seq<Nat> = Seq.empty();
assert Seq.len(empty) == 0;

Seq.singleton<T>(e)

Creates a Seq containing exactly one element:

let s = Seq.singleton<Nat>(42);
assert Seq.len(s) == 1;
assert Seq.get(s, 0) == 42;

Seq.len(s)

Returns the length of the sequence as an Int:

let s = Seq.concat(Seq.singleton(1), Seq.singleton(2));
assert Seq.len(s) == 2;

Seq.get(s, i)

Returns the element at index i (0-based). The index must be within bounds:

let s = Seq.singleton<Nat>(42);
assert Seq.get(s, 0) == 42;

Out-of-bounds access fails verification. Ensure 0 <= i and i < Seq.len(s).

Seq.concat(s1, s2)

Joins two sequences into one:

let s1 = Seq.singleton<Nat>(1);
let s2 = Seq.singleton<Nat>(2);
let s3 = Seq.concat(s1, s2);
assert Seq.len(s3) == 2;
assert Seq.get(s3, 0) == 1;
assert Seq.get(s3, 1) == 2;

Concatenation follows the trusted primitive sequence model, including the usual length, indexing, and associativity behavior. For non-trivial proofs over several concatenations, isolate the argument in a lemma instead of burying it in a public method body.

Seq.contains(e, s)

Returns true if element e is in the sequence:

seq-contains.sr9

// Seq.contains checks membership
persistent actor {
  public func demo() : async () {
    ghost {
      let s = Seq.concat(
        Seq.singleton<Nat>(1),
        Seq.singleton<Nat>(2));

      assert Seq.contains(1, s);
      assert Seq.contains(2, s);
      assert not Seq.contains(3, s);
      assert not Seq.contains(0, s);
    };
  };
}

Note the argument order: element first, then sequence.

Slicing Operations

Seq.take(s, n)

Returns the first n elements of the sequence:

let s = Seq.concat(Seq.singleton(1), Seq.singleton(2));
let first = Seq.take(s, 1);
assert Seq.len(first) == 1;
assert Seq.get(first, 0) == 1;

Seq.drop(s, n)

Returns the sequence with the first n elements removed:

let s = Seq.concat(Seq.singleton(1), Seq.singleton(2));
let rest = Seq.drop(s, 1);
assert Seq.len(rest) == 1;
assert Seq.get(rest, 0) == 2;

Seq.slice(s, i, j)

Returns elements from index i (inclusive) to j (exclusive):

seq-slicing.sr9

// Seq slicing: take, drop, slice
persistent actor {
  public func demo() : async () {
    ghost {
      // Build a sequence [1, 2, 3, 4]
      let s = Seq.concat(Seq.concat(Seq.concat(
        Seq.singleton<Nat>(1),
        Seq.singleton<Nat>(2)),
        Seq.singleton<Nat>(3)),
        Seq.singleton<Nat>(4));

      // Take first n elements
      let first2 = Seq.take(s, 2);
      assert Seq.len(first2) == 2;
      assert Seq.get(first2, 0) == 1;
      assert Seq.get(first2, 1) == 2;

      // Drop first n elements
      let last2 = Seq.drop(s, 2);
      assert Seq.len(last2) == 2;
      assert Seq.get(last2, 0) == 3;
      assert Seq.get(last2, 1) == 4;

      // Slice from i to j (exclusive)
      let mid = Seq.slice(s, 1, 3);
      assert Seq.len(mid) == 2;
      assert Seq.get(mid, 0) == 2;
      assert Seq.get(mid, 1) == 3;
    };
  };
}

The relation between these operations:

• Seq.take(s, n) is equivalent to Seq.slice(s, 0, n)
• Seq.drop(s, n) is equivalent to Seq.slice(s, n, Seq.len(s))

Updating Elements

Seq.update(s, i, v)

Returns a new sequence with the element at index i replaced by v:

seq-update.sr9

// Seq.update creates a new sequence with a modified element
persistent actor {
  public func demo() : async () {
    ghost {
      let s1 = Seq.concat(
        Seq.singleton<Nat>(10),
        Seq.singleton<Nat>(20));

      // Update returns a new sequence
      let s2 = Seq.update(s1, 0, 99);

      // Original unchanged; updates return new values.
      // s2 has the modified element
      assert Seq.get(s2, 0) == 99;
      assert Seq.get(s2, 1) == 20;
      assert Seq.len(s2) == 2;
    };
  };
}

Update preserves length and changes only the selected position in the trusted sequence model. Prove 0 <= i and i < Seq.len(s) before updating or reading by index.

Sequence Properties

Seq.sorted(s)

Returns true if a Seq<Nat> is sorted in ascending order:

seq-sorted.sr9

// Seq.sorted checks if a Seq<Nat> is in ascending order
persistent actor {
  public func demo() : async () {
    ghost {
      // Empty and singleton sequences are sorted
      let empty = Seq.empty<Nat>();
      let one = Seq.singleton<Nat>(42);
      assert Seq.sorted(empty);
      assert Seq.sorted(one);

      // Sorted sequence
      let ascending = Seq.concat(
        Seq.singleton<Nat>(1),
        Seq.singleton<Nat>(2));
      assert Seq.sorted(ascending);
    };
  };
}

This operation only works with Seq<Nat>, not generic sequences.

Seq.permutes(a, b)

Returns true if sequence b is a permutation of sequence a:

seq-permutes.sr9

// Seq.permutes checks if two sequences are permutations
persistent actor {
  public func demo() : async () {
    ghost {
      let s = Seq.singleton<Nat>(1);
      let t = Seq.singleton<Nat>(2);

      // Every sequence is a permutation of itself
      assert Seq.permutes(s, s);

      // Permutations have equal length
      assert (Seq.permutes(s, t) ==> (Seq.len(s) == Seq.len(t)));
    };
  };
}

Properties:

• Reflexive: Seq.permutes(s, s) is always true
• Permutations have equal length: Seq.permutes(a, b) ==> Seq.len(a) == Seq.len(b)
• Permutations preserve element multiplicity: duplicates are counted, not treated as a set

Ghost Seq Fields

Declare ghost Seq fields at actor level to track ordered state:

seq-ghost-field.sr9

// Using Seq as a ghost field for event logging
persistent actor {
  ghost var events : Seq<Nat> = Seq.empty();

  invariant Seq.len(events) >= 0;

  public func log(eventId : Nat) : async ()
    modifies events
    ensures Seq.len(events) == Seq.len(old(events)) + 1;
    ensures Seq.get(events, Seq.len(events) - 1) == eventId;
  {
    ghost {
      events := Seq.concat(events, Seq.singleton(eventId));
    };
  };
}

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

Quantifiers with Sequences

Combine Seqs with quantifiers for expressive specifications:

seq-quantifiers.sr9

// Quantifiers with Seq
persistent actor {
  public func demo() : async () {
    ghost {
      let s = Seq.concat(
        Seq.singleton<Nat>(10),
        Seq.singleton<Nat>(20));
      let n = Seq.len(s);

      // All elements are positive
      assert forall<Int>(pure func (i : Int) : Bool =
        (0 <= i and i < n) ==> (Seq.get(s, i) > 0));

      // Element exists in sequence
      assert exists<Int>(pure func (i : Int) : Bool =
        (0 <= i and i < n) and (Seq.get(s, i) == 10));
    };
  };
}

Common patterns:

• Use forall with bounds guard 0 <= i and i < Seq.len(s) to express properties of all elements.
• Use exists to assert at least one element satisfies a condition.
• Combine Seq.get with index predicates so the verifier sees every access is in bounds.
• If indexed properties time out, review trigger patterns.

Element Type Restrictions

Seq 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 sequence elements by identity. Sequence equality does not prove the owner models of those handles are unchanged.

seq-immutable-reject_reject.sr9

// ERROR: Seq elements must be immutable
persistent actor {
  type MutArr = [var Int];

  public func demo() : async () {
    ghost {
      // This is rejected - mutable arrays cannot be Seq elements
      let s : Seq<MutArr> = Seq.empty();
      assert true;
    };
  };
}

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

Operation Reference

Operation	Signature	Description
Seq.empty<T>()	Seq<T>	Create empty sequence
Seq.singleton<T>(e)	Seq<T>	Create single-element sequence
Seq.len(s)	Int	Get sequence length
Seq.get(s, i)	T	Get element at index
Seq.concat(s1, s2)	Seq<T>	Join two sequences
Seq.append(s, e)	Seq<T>	Append one element
Seq.update(s, i, v)	Seq<T>	Replace element at index
Seq.take(s, n)	Seq<T>	First n elements
Seq.drop(s, n)	Seq<T>	Remove first n elements
Seq.slice(s, i, j)	Seq<T>	Elements from i to j-1
Seq.contains(e, s)	Bool	Check membership
Seq.sorted(s)	Bool	Check if sorted (Nat only)
Seq.permutes(a, b)	Bool	Check permutation relation

Common Patterns

Event Logging

ghost var log : Seq<Nat> = Seq.empty();

public func recordEvent(id : Nat) : async ()
  modifies log
  ensures Seq.len(log) == Seq.len(old(log)) + 1;
  ensures Seq.get(log, Seq.len(log) - 1) == id;
{
  ghost {
    log := Seq.concat(log, Seq.singleton(id));
  };
}

History Tracking

ghost var history : Seq<Int> = Seq.empty();

public func update(newValue : Int) : async ()
  modifies history
  ensures Seq.contains(newValue, history);
{
  ghost {
    history := Seq.concat(history, Seq.singleton(newValue));
  };
}

Ordered Invariants

ghost {
  var timestamps : Seq<Nat> = Seq.empty();
  let t : Nat = 100;

  assert Seq.sorted(timestamps);
  assert Seq.len(timestamps) == 0 or
    Seq.get(timestamps, Seq.len(timestamps) - 1) <= t;
  timestamps := Seq.concat(timestamps, Seq.singleton(t));
}

Seq vs Arrays

Seq is a specification-only type for verification, while arrays are runtime structures:

Aspect	Seq	Array
Runtime	No (ghost only)	Yes
Mutability	Immutable	Can be mutable
Purpose	Verification reasoning	Runtime data
Index type	Int	Nat

Use Seq when you need to reason about ordered collections in specifications. Use arrays when you need actual runtime storage. If you need both, keep a runtime structure and a ghost Seq model in sync, then compare pre-state and post-state with old().

Summary

• Sequences are specification-only ordered collections
• Seq operations are ghost proof operations over a trusted primitive collection model
• Create with Seq.empty<T>() or Seq.singleton(element)
• Access with Seq.len, Seq.get, Seq.contains
• Combine with Seq.concat, modify with Seq.update
• Slice with Seq.take, Seq.drop, Seq.slice
• Check properties with Seq.sorted (Nat only) and Seq.permutes
• Elements must be spec-immutable (no mutable fields, arrays, or functions), except opaque/token handles by identity
• Use ghost Seq fields with modifies clauses for actor-level tracking
• Combine with quantifiers for expressive invariants and postconditions

Related Topics

• Multiset operations for order-insensitive counts
• Collection snapshots for runtime BSeq and map-entry enumeration bridges
• Collection restrictions for spec-immutable element rules
• Old collection snapshots for comparing histories across method calls
• Quantifier patterns for indexed sequence properties
• Trusted base for the soundness boundary behind primitive collections
• BSeq for runtime sequence utilities with Seq proof models