Import Syntax

Imports bring modules, types, and functions from other files into scope. In verified code, imports are also a modular proof boundary: callers prove imported preconditions and rely on imported postconditions instead of reopening the imported body.

Basic Import Syntax

The basic import statement binds a module to a local name:

import ModuleName "path/to/module"

The path is relative to the importing file. File extensions (.sr9 or .mo) are omitted.

Library Module

import-basic-lib.sr9

// A simple library module to import
module MathLib {
  public func double(n : Nat) : Nat
    ensures result == n * 2;
  {
    n * 2
  };

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

Importing Actor

import-basic.sr9

// Import a local module
import MathLib "./import-basic-lib";

persistent actor Calculator {
  public func compute(n : Nat) : async Nat
    ensures result == n * 6;
  {
    MathLib.triple(MathLib.double(n))
  };
}

Access imported members using dot notation: MathLib.double(n).

Import Placement

Imports must appear at the top of the file, before any other declarations:

import A "./module_a";
import B "./module_b";

// All other declarations come after imports
persistent actor MyActor {
  // ...
}

Selective Imports

Import specific members directly into scope using destructuring syntax:

import { member1; member2 } "path/to/module"

Library Module

import-selective-lib.sr9

// Module with multiple exports for selective import
module Utils {
  public func inc(n : Nat) : Nat
    ensures result == n + 1;
  {
    n + 1
  };

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

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

Selective Import

import-selective.sr9

// Import only specific functions from a module
import { inc; square } "./import-selective-lib";

persistent actor SelectiveDemo {
  public func compute(n : Nat) : async Nat
    ensures result == (n + 1) * (n + 1);
  {
    // Use imported functions directly without module prefix
    square(inc(n))
  };
}

With selective imports, you use the function names directly (inc, square) instead of qualifying them with a module prefix.

Importing Types

Modules can export type definitions that you reference through the import alias:

Types Module

import-types-lib.sr9

// Module exporting types
module Types {
  public type Point = { x : Int; y : Int };
  public type Size = { width : Nat; height : Nat };

  public pure func origin() : Point {
    { x = 0; y = 0 }
  };
};

Using Types

import-types.sr9

// Import a module and use its types
import Types "./import-types-lib";

persistent actor Geometry {
  var position : Types.Point = Types.origin();

  public func moveTo(x : Int, y : Int) : async ()
    modifies position
    ensures position.x == x;
    ensures position.y == y;
  {
    position := { x = x; y = y };
  };
}

Reference imported types as ModuleName.TypeName (e.g., Types.Point).

Anonymous Modules

When a module file contains an anonymous module (no name after module), it takes the name of the import alias:

Anonymous Module

import-anonymous-lib.sr9

// Anonymous module - takes the import alias name
module {
  public let VERSION : Nat = 1;

  public func greet() : Text {
    "Hello"
  };
};

Import Alias

import-anonymous.sr9

// Anonymous modules take their name from the import alias
import Config "./import-anonymous-lib";

persistent actor App {
  public func getVersion() : async Nat {
    // Access via the import alias "Config"
    Config.VERSION
  };
}

The anonymous module is accessed through the alias Config.

Nested Module Access

When a module contains nested submodules, access them through chained dot notation:

Nested Modules

import-nested-lib.sr9

// Module with nested submodules
module Outer {
  public module Inner {
    public func compute(n : Nat) : Nat
      ensures result == n + 10;
    {
      n + 10
    };
  };

  public let CONSTANT : Nat = 42;
};

Accessing Nested

import-nested.sr9

// Access nested modules through dot notation
import Outer "./import-nested-lib";

persistent actor NestedDemo {
  public func example(n : Nat) : async Nat
    ensures result == n + 10 + 42;
  {
    // Access nested module via chained dot notation
    Outer.Inner.compute(n) + Outer.CONSTANT
  };
}

Core and System Imports

Import the verified core library with the mo:core prefix:

import Debug "mo:core/Debug"; // Debug utilities
import Text "mo:core/Text";   // Text operations
import Nat "mo:core/Nat";     // Numeric helpers

The mo:core/... modules are the normal user-facing standard library for verified Sector9 code. Primitive paths such as mo:prim or mo:⛔ exist for compiler/core-library internals and legacy Motoko code, but application code should prefer core wrappers. Package imports such as mo:base/... only work when that package is configured for the build.

Import URL Formats

Format	Description	Example
"./path"	Relative path from current file	"./utils"
"../path"	Parent directory relative path	"../shared/types"
"mo:core/path"	Sector9 core library import	"mo:core/Text"
"mo:package/path"	Configured package import	"mo:base/Array"
"mo:prim" / "mo:⛔"	Primitive/internal import	"mo:prim"

Path Resolution

When you import "./math", Sector9 searches for:

1. ./math.sr9 (preferred)
2. ./math.mo (legacy)
3. ./math/lib.sr9 (directory with lib module)
4. ./math/lib.mo (legacy directory)

This allows both single-file modules and directory-based module organization.

Verification with Imports

Imports work with verification. When you call an imported executable function:

• Preconditions become proof obligations at the call site
• Postconditions become assumptions about the result
• Implementation is not re-opened - the caller verifies against contracts only

This enables modular verification where each module is verified independently. It also means imported helpers need useful contracts; a body that proves facts locally does not automatically teach importers those facts.

import MathLib "./math";

persistent actor Caller {
  public func use(n : Nat) : async Nat
    entry_requires n < 100;
    requires n < 100;           // Caller's precondition
    ensures result == n * 2;    // Relies on MathLib.double's contract
  {
    MathLib.double(n)           // MathLib.double's postcondition assumed
  };
}

Imported runtime pure/spec helpers follow the same contract-only rule by default. If a proof library intentionally wants callers to use a helper's body across an import boundary, mark that helper inline pure func. Imported ghost/lemma helpers remain proof-only and can expose definitional proof bodies.

Run --check over imported libraries to catch type, legality, and contract-surface issues even when no actor root is being verified.

Common Errors

Error Code	Meaning
M0009	File does not exist for import path
M0010	Package not defined (for mo: imports)
M0020	Unresolved import
M0141	Non-import declarations before/after main actor

Summary

• Use import Name "path" to import a module with an alias
• Use import { a; b } "path" to import specific members directly
• Imports must appear at the top of the file
• Paths are relative and omit file extensions
• Access imported members with dot notation: Module.member
• Core library modules use the mo:core/... path
• Imported function contracts are used for modular verification

Related Topics

• Module definitions for authoring importable modules
• Pure functions for inline pure helpers
• Differences from Motoko for Sector9 import and verification differences