Module Definitions

Modules are stateless containers for organizing related functions, types, constants, and proof helpers into reusable units. They are the right place for reusable pure functions and typed interfaces that actors can call.

Overview

A module groups related definitions together under a single namespace. Unlike actors, modules have no mutable state and cannot have async methods. This makes them ideal for:

• Library functions - reusable utilities shared across actors
• Type definitions - custom types used throughout your codebase
• Pure functions - predicates and helpers for use in requires and ensures
• Constants - named values like configuration limits

Basic Syntax

The basic module syntax uses the module keyword followed by an optional name and a body:

module ModuleName {
  // public members are accessible to importers
  public func add(a : Nat, b : Nat) : Nat { a + b };

  // private members are internal only
  func helper(n : Nat) : Nat { n * 2 };

  // public constants
  public let MAX : Nat = 1000;

  // public types
  public type Id = Nat;
};

Named Modules

Named modules define a namespace that other code can reference directly:

module-basic.sr9

// Basic module with public function
module MathLib {
  public func double(n : Nat) : Nat
    ensures result == n * 2;
  {
    n * 2
  };

  public func square(n : Nat) : Nat
    ensures result == n * n;
  {
    n * n
  };
};

// Using the module
persistent actor {
  public func test() : async Nat
    ensures result == 50;
  {
    MathLib.double(MathLib.square(5))
  };
}

The actor accesses module functions using dot notation: MathLib.double(...).

Anonymous Modules

When a file contains only a module with no actor, you can omit the name. This is the common pattern for library files:

module-anonymous.sr9

// Anonymous module (top-level library pattern)
module {
  public func increment(n : Nat) : Nat
    ensures result == n + 1;
  {
    n + 1
  };

  public func decrement(n : Nat) : Nat
    requires n >= 1;
    ensures result == n - 1;
  {
    n - 1
  };
}

When imported, the module takes on the name given in the import statement:

import Utils "./module-anonymous";

// Now use as Utils.increment(...)

Visibility: Public vs Private

Module members are private by default. Use public to expose them:

module-visibility.sr9

// Module with public and private members
module Counter {
  // Private helper - not accessible outside
  func clamp(n : Nat) : Nat {
    if (n > 100) 100 else n
  };

  // Public interface
  public func increment(n : Nat) : Nat
    ensures result <= 100;
    ensures result >= n or result == 100;
  {
    clamp(n + 1)
  };

  // Public constant
  public let MAX : Nat = 100;
};

persistent actor {
  public func test() : async Nat
    ensures result <= 100;
  {
    Counter.increment(50)
  };
}

Visibility rules:

• public func - callable from outside the module
• public let - readable constant from outside
• public type - usable type from outside
• No modifier - private, internal to the module only

Nested Modules

Modules can contain other modules for hierarchical organization:

module-nested.sr9

// Module with nested submodules
module Math {
  public module Arithmetic {
    public func add(a : Int, b : Int) : Int
      ensures result == a + b;
    {
      a + b
    };

    public func subtract(a : Int, b : Int) : Int
      ensures result == a - b;
    {
      a - b
    };
  };

  public module Comparison {
    public pure func max(a : Int, b : Int) : Int {
      if (a > b) a else b
    };

    public pure func min(a : Int, b : Int) : Int {
      if (a < b) a else b
    };
  };
};

persistent actor {
  public func test() : async Int
    ensures result == 7;
  {
    Math.Comparison.max(
      Math.Arithmetic.add(3, 4),
      Math.Arithmetic.subtract(10, 5)
    )
  };
}

Access nested modules with chained dot notation: Math.Arithmetic.add(...).

Exporting Types

Modules commonly export type definitions for use across your codebase:

module-types.sr9

// Module exporting types and constants
module Types {
  // Type alias
  public type UserId = Nat;

  // Record type
  public type User = {
    id : UserId;
    name : Text;
    active : Bool;
  };

  // Variant type
  public type Status = {
    #pending;
    #approved;
    #rejected;
  };

  // Constructor function
  public func makeUser(id : UserId, name : Text) : User {
    { id = id; name = name; active = true }
  };
};

persistent actor {
  public func createUser() : async Types.User {
    Types.makeUser(1, "Alice")
  };
}

Reference exported types with the module prefix: Types.User, Types.Status.

Pure Functions for Contracts

Modules are an excellent place to define pure functions that can appear in verification contracts:

module-pure.sr9

// Module with pure functions for use in contracts
module Validators {
  public pure func isPositive(n : Int) : Bool {
    n > 0
  };

  public pure func inRange(n : Int, lo : Int, hi : Int) : Bool {
    n >= lo and n <= hi
  };

  public pure func clamp(n : Int, lo : Int, hi : Int) : Int {
    if (n < lo) lo
    else if (n > hi) hi
    else n
  };
};

persistent actor {
  var value : Int = 0;

  public func setValue(n : Int) : async ()
    modifies value
    requires Validators.isPositive(n);
    requires Validators.inRange(n, 1, 100);
    ensures value == Validators.clamp(n, 1, 100);
  {
    value := Validators.clamp(n, 1, 100);
  };
}

Pure functions in modules:

• Can be used in requires and ensures clauses
• Cannot have side effects or mutable state
• Are used symbolically by the verifier; imported pure helpers are contract-only unless declared inline pure

Modules vs Actors

Feature	Module	Actor
Mutable state (var)	No	Yes
Async methods	No	Yes
Invariants	No	Yes
Persistence	N/A	Yes
Use case	Libraries	Services

Key distinction: Modules have no actor identity, no durable state, and no message queue. Actors are runtime entities with persistent state and async entry points.

Restrictions

No Mutable State

Modules cannot declare mutable fields. All module content must be static (compile-time evaluable):

Wrong

module-mutable-state_reject.sr9

// ERROR: Modules cannot have mutable state
module BadModule {
  var counter : Nat = 0;  // Rejected: non-static

  public func bump() : Nat
    modifies counter
  {
    counter += 1;
    counter
  };
};

Error: M0014 - non-static expression in library, module or migration expression

Correct

// Use an actor for mutable state
persistent actor Counter {
var counter : Nat = 0;

public func bump() : async Nat
  modifies counter
  ensures result == old(counter) + 1;
{
  counter += 1;
  counter
};
}

Static Expressions Only

Module bodies can only contain static declarations and expressions:

• Function definitions
• Type definitions
• Immutable let bindings
• Nested modules and immutable objects

The following are rejected in modules:

• Mutable variables (var)
• Async expressions
• Function calls that have side effects
• Mutable array literals

No Invariants

Since modules have no mutable state, invariant declarations are not allowed. Use actor invariants in actors instead.

Common Patterns

Library Module

A self-contained utility library:

module StringUtils {
  public func isEmpty(s : Text) : Bool { s == "" };
  public func length(s : Text) : Nat { s.size() };
  public let EMPTY : Text = "";
};

Type Provider Module

A module that only exports types:

module Domain {
  public type UserId = Nat;
  public type Amount = Nat;
  public type Timestamp = Int;

  public type Transaction = {
    from : UserId;
    to : UserId;
    amount : Amount;
    time : Timestamp;
  };
};

Validator Module

Pure functions for use in contracts:

module Validate {
  public pure func nonZero(n : Nat) : Bool { n > 0 };
  public pure func inBounds(n : Nat, max : Nat) : Bool { n <= max };
  public pure func validId(id : Nat) : Bool { id > 0 and id < 1_000_000 };
};

Related Topics

• Import syntax for bringing modules from other files into scope
• Module types for structural interfaces
• First-class modules for passing modules as values
• Pure functions for spec-callable helpers
• Ghost modules for verification-only abstractions

Summary

• Modules group related functions, types, and constants into reusable units
• Use public to expose members; members are private by default
• Modules are stateless - no var fields or async methods allowed
• Nested modules provide hierarchical organization
• Anonymous modules (no name) are common for library files
• Pure functions in modules can be used in verification contracts
• Use modules for libraries; use actors for services with state