Records

Records are named field collections that group related data together. They are the primary way to structure domain data in Sector9, offering self-documenting field names like { name : Text; age : Nat }. Immutable records behave like values; mutable records introduce heap identity, ownership, and read/write permissions.

Creating Records

Define record types with type and create instances using { field = value } syntax:

record-basic.sr9

// Basic record creation and field access
persistent actor {
  // Define a named record type
  type Point = { x : Int; y : Int };

  // Anonymous inline record type
  var person : { name : Text; age : Nat } = { name = "Alice"; age = 30 };

  // Create records using named types
  public func createPoint(x : Int, y : Int) : async Point
    ensures result.x == x;
    ensures result.y == y;
  {
    { x = x; y = y }
  };

  // Field access with dot notation
  public func getX(p : Point) : async Int
    ensures result == p.x;
  {
    p.x
  };

  // Return inline record type
  public func getInfo() : async { name : Text; age : Nat }
    reads person
    ensures result.name == person.name;
    ensures result.age == person.age;
  {
    person
  };
}

Key points:

• Record types list fields with fieldName : Type separated by semicolons
• Record values use fieldName = value to assign each field
• Access fields with dot notation: record.fieldName
• Named types (type Point = { ... }) create reusable definitions
• Inline types ({ name : Text; age : Nat }) work for one-off structures

Immutable vs Mutable Records

Records come in two forms based on their field declarations:

Aspect	Immutable Record	Mutable Record
Field syntax	x : Int	var x : Int
Creation	{ x = 1 }	{ var x = 1 }
Update	Replace entire record	Assign field with :=
Semantics	Value (copyable)	Reference (single owner)
In collections	Allowed	Not allowed

// Immutable record - update by creating new record
type Point = { x : Int; y : Int };
let p = { x = 1; y = 2 };
let moved = { x = p.x + 1; y = p.y };

// Mutable record - update field in place
type Cell = { var value : Int };
let c = { var value = 0 };
c.value := 10;  // Mutate the field directly

Mutable Records

Use var to declare mutable fields. These records support in-place field updates:

record-mutable.sr9

// Mutable records with var fields
persistent actor {
  // A mutable record type - fields declared with `var`
  type Cell = { var value : Int };

  // Mutable record as actor state
  var counter : Cell = { var value = 0 };

  // Mutate a field with :=
  public func increment() : async ()
    modifies counter
    ensures counter.value == old(counter.value) + 1;
  {
    counter.value := counter.value + 1;
  };

  // Read a mutable field
  public func getValue() : async Int
    reads counter
    ensures result == counter.value;
  {
    counter.value
  };

  // Set a mutable field
  public func setValue(v : Int) : async ()
    modifies counter
    ensures counter.value == v;
  {
    counter.value := v;
  };

  // Pass mutable record as parameter
  private func bump(c : Cell) : ()
    ensures c.value == old(c.value) + 1;
  {
    c.value := c.value + 1;
  };

  public func bumpCounter() : async ()
    modifies counter
    ensures counter.value == old(counter.value) + 1;
  {
    bump(counter);
  };
}

Key points:

• Mutable fields are declared with var fieldName : Type
• Created with { var fieldName = value }
• Mutate with := assignment: record.field := newValue
• Mutable records passed as parameters allow the callee to modify them
• Use old(record.field) in postconditions to reference pre-state values

Record Extension

Extend or update records using the with keyword:

record-extension.sr9

// Record extension with structural update
persistent actor {
  type Point2D = { x : Int; y : Int };
  type Point3D = { x : Int; y : Int; z : Int };

  // Extend a record with new fields using `with`
  public func extendToPoint3D(p : Point2D, z : Int) : async Point3D
    ensures result.x == p.x;
    ensures result.y == p.y;
    ensures result.z == z;
  {
    { p with z = z }
  };

  // Override existing field while preserving others
  public func moveX(p : Point2D, newX : Int) : async Point2D
    ensures result.x == newX;
    ensures result.y == p.y;
  {
    { p with x = newX }
  };

  // Combine multiple extensions
  public func transform(p : Point2D) : async Point3D
    ensures result.x == p.x + 1;
    ensures result.y == p.y;
    ensures result.z == 0;
  {
    { p with x = p.x + 1; z = 0 }
  };
}

The { base with field = value } syntax:

• Copies all fields from base
• Adds or overrides the specified fields
• Creates a new record (does not mutate the original)

Nested Records

Records can contain other records, allowing deep hierarchical structures:

record-nested.sr9

// Nested records and deep field access
persistent actor {
  type Point = { x : Int; y : Int };
  type Rectangle = { topLeft : Point; bottomRight : Point };

  var rect : Rectangle = {
    topLeft = { x = 0; y = 0 };
    bottomRight = { x = 10; y = 10 }
  };

  // Access nested fields with chained dot notation
  public func getWidth() : async Int
    reads rect
    ensures result == rect.bottomRight.x - rect.topLeft.x;
  {
    rect.bottomRight.x - rect.topLeft.x
  };

  // Create nested structure in one expression
  public func createRect(x1 : Int, y1 : Int, x2 : Int, y2 : Int) : async Rectangle
    ensures result.topLeft.x == x1;
    ensures result.topLeft.y == y1;
    ensures result.bottomRight.x == x2;
    ensures result.bottomRight.y == y2;
  {
    {
      topLeft = { x = x1; y = y1 };
      bottomRight = { x = x2; y = y2 }
    }
  };

  // Update nested structure (whole record replacement)
  public func moveRect(dx : Int, dy : Int) : async ()
    modifies rect
    ensures rect.topLeft.x == old(rect.topLeft.x) + dx;
    ensures rect.topLeft.y == old(rect.topLeft.y) + dy;
    ensures rect.bottomRight.x == old(rect.bottomRight.x) + dx;
    ensures rect.bottomRight.y == old(rect.bottomRight.y) + dy;
  {
    rect := {
      topLeft = { x = rect.topLeft.x + dx; y = rect.topLeft.y + dy };
      bottomRight = { x = rect.bottomRight.x + dx; y = rect.bottomRight.y + dy }
    }
  };
}

Access nested fields by chaining dots: rect.topLeft.x. For immutable nested records, update by reconstructing the entire structure.

Record Spread and Type Operators

Spread syntax merges fields from multiple records or types:

record-spread.sr9

// Record spread and type operators
persistent actor {
  type A = { x : Nat; y : Nat };
  type B = { y : Nat; z : Nat };

  // Type-level spread: merge types
  type AB = { ...A; ...B };  // { x : Nat; y : Nat; z : Nat }

  // Spread multiple records (right-biased: later overrides earlier)
  public func merge() : async AB
    ensures result.x == 1;
    ensures result.y == 20;  // y from b overrides y from a
    ensures result.z == 3;
  {
    let a : A = { x = 1; y = 2 };
    let b : B = { y = 20; z = 3 };
    { ...a; ...b }
  };

  // Mix spread with explicit fields
  public func mergeWithOverride() : async AB
    ensures result.x == 1;
    ensures result.y == 99;  // explicit override
    ensures result.z == 3;
  {
    let a : A = { x = 1; y = 2 };
    let b : B = { y = 20; z = 3 };
    { ...a; ...b; y = 99 }
  };

  // omit removes fields from a type
  type OnlyX = omit A { y };  // { x : Nat }

  // pick selects specific fields
  type OnlyY = pick A { y };  // { y : Nat }

  public func pickFields() : async Nat
    ensures result == 5;
  {
    let full : A = { x = 5; y = 10 };
    let partial : OnlyX = { x = full.x };
    partial.x
  };
}

Key operators:

• { ...A; ...B } - Merge types (later fields override earlier)
• { ...a; ...b } - Merge values (right-biased)
• omit TYPE { fields } - Remove specific fields from a type
• pick TYPE { fields } - Select only specific fields

Pattern Matching

Destructure records to extract fields into variables:

record-pattern.sr9

// Record pattern matching (destructuring)
persistent actor {
  type Point = { x : Int; y : Int };

  // Destructure in let binding
  public func getSum(p : Point) : async Int
    ensures result == p.x + p.y;
  {
    let { x; y } = p;
    x + y
  };

  // Partial destructuring (select specific fields)
  public func getX(p : Point) : async Int
    ensures result == p.x;
  {
    let { x } = p;
    x
  };

  // Rename fields during destructuring
  public func swapped(p : Point) : async Point
    ensures result.x == p.y;
    ensures result.y == p.x;
  {
    let { x = origX; y = origY } = p;
    { x = origY; y = origX }
  };

  // Nested destructuring
  type Rectangle = { topLeft : Point; bottomRight : Point };

  public func getCornerX(r : Rectangle) : async Int
    ensures result == r.topLeft.x;
  {
    let { topLeft = { x } } = r;
    x
  };
}

Pattern syntax:

• let { x; y } = record - Bind fields to same-named variables
• let { x = a; y = b } = record - Bind fields to different names
• let { x } = record - Extract only specific fields

Pure Functions with Records

Pure functions work naturally with immutable records:

record-pure.sr9

// Pure functions with immutable records
persistent actor {
  type Point = { x : Int; y : Int };

  // Pure function creating a record
  pure func origin() : Point {
    { x = 0; y = 0 }
  };

  // Pure function with record parameter
  pure func translate(p : Point, dx : Int, dy : Int) : Point {
    { x = p.x + dx; y = p.y + dy }
  };

  // Pure function combining records
  pure func add(p1 : Point, p2 : Point) : Point {
    { x = p1.x + p2.x; y = p1.y + p2.y }
  };

  // Pure functions in contracts
  public func testOrigin() : async Point
    ensures result.x == origin().x;
    ensures result.y == origin().y;
  {
    origin()
  };

  public func testTranslate() : async Point
    ensures result.x == 5;
    ensures result.y == 7;
  {
    translate(origin(), 5, 7)
  };

  public func testAdd() : async Point
    ensures result.x == 4;
    ensures result.y == 6;
  {
    add({ x = 1; y = 2 }, { x = 3; y = 4 })
  };
}

Pure record helpers can appear directly in verification contracts (ensures, requires, invariant).

Records in Verification

Contracts on Record Fields

Use dot notation in contracts to specify field properties:

public func setPoint(x : Int, y : Int) : async Point
  ensures result.x == x;
  ensures result.y == y;
{
  { x = x; y = y }
};

Actor State Records

Records stored as actor fields require reads or modifies clauses:

persistent actor {
  var config : { min : Int; max : Int } = { min = 0; max = 100 };

  public func getMin() : async Int
    reads config
    ensures result == config.min;
  {
    config.min
  };

  public func expand(delta : Int) : async ()
    modifies config
    entry_requires delta >= 0;
    requires delta >= 0;
    ensures config.min == old(config.min) - delta;
    ensures config.max == old(config.max) + delta;
  {
    config := { min = config.min - delta; max = config.max + delta };
  };
}

Invariants Over Records

Actor invariants can express relationships between record fields:

persistent actor {
  var range : { min : Int; max : Int } = { min = 0; max = 100 };

  invariant range.min <= range.max;

  public func setRange(newMin : Int, newMax : Int) : async ()
    modifies range
    entry_requires newMin <= newMax;
    requires newMin <= newMax;
    ensures range.min == newMin;
    ensures range.max == newMax;
  {
    range := { min = newMin; max = newMax };
  };
}

Restrictions

Mutable Field Pattern Matching

Cannot pattern-match mutable fields:

type Cell = { var x : Int };
let c : Cell = { var x = 5 };
let { var x } = c;  // ERROR M0120: cannot pattern match mutable field x

Use direct field access instead: let x = c.x.

Mutable Records in Collections

Mutable records cannot be stored in spec collections (Set, Map, Seq, Multiset):

type Cell = { var x : Int };
ghost var cells : Set<Cell> = Set.empty();  // ERROR M0242

Only immutable records (no var fields) are allowed as spec collection elements. This keeps equality and membership stable for Map, Set, Seq, and Multiset.

Arrays of Mutable Records

Arrays containing mutable records have targeted verification support, not a blanket rejection. Fresh local arrays and the current owned/opaque payload lanes are supported; deeply nested or escaping shapes still need careful ownership and aliasing contracts. See mutable record ownership for the proof obligations that show up once references can alias.

type Cell = { var value : Nat };
var cells : [var Cell] = [var { var value = 0 }];
cells[0].value := 1;

Field Mutability Mismatch

Field mutability must match between type and value:

record-mutable-mismatch_reject.sr9

// Type error: mutable field mismatch
persistent actor {
  // Type expects immutable field
  type Immutable = { x : Int };

  // Trying to provide mutable field
  public func wrongMutability() : async Immutable {
    // ERROR M0150: expected immutable field x
    // but found mutable 'var' field (delete 'var'?)
    { var x = 10 }
  };
}

Record vs Tuple

Feature	Record	Tuple
Access	By name (.fieldName)	By position (.0, .1)
Type syntax	{ age : Nat; name : Text }	(Nat, Text)
Self-documenting	Yes	No
Field order	Independent	Matters
Best for	Structured domain data	Quick groupings

Use records when field names add clarity. Use tuples for temporary groupings like swapping values.

Error Codes

Code	Meaning
M0028	Field does not exist in record type
M0120	Cannot pattern match mutable field
M0149	Expected mutable var field, found immutable
M0150	Expected immutable field, found mutable var
M0151	Missing required field from expected type
M0242	Collection element type must be immutable

Summary

• Records group named fields: { name : Text; age : Nat }
• Immutable records use field : Type, mutable use var field : Type
• Access fields with dot notation: record.field
• Extend records with { base with newField = value }
• Spread merges records: { ...a; ...b } (right-biased)
• Destructure with patterns: let { x; y } = record
• Mutable record fields update in place with :=
• Use old(record.field) in postconditions for pre-state values
• Mutable records cannot be stored in spec collections
• Prefer records over tuples when field names improve clarity