Options

Options represent values that may or may not exist. The type ?T means "either a value of type T or nothing." Options eliminate null pointer errors by forcing you to explicitly handle the missing case with switch, do ?, or a proven precondition.

Creating Options

Use ?value to wrap a value, and null for the empty case:

option-basic.sr9

// Basic option types
persistent actor {
  // Option type declaration
  transient var maybeCount : ?Nat = null;
  transient var maybeName : ?Text = null;
  transient var maybeScore : ?Int = ?100;

  // Constructing options
  public func setCount(n : Nat) : async ()
    modifies maybeCount
    ensures maybeCount == ?n;
  {
    maybeCount := ?n;
  };

  public func clearCount() : async ()
    modifies maybeCount
    ensures maybeCount == null;
  {
    maybeCount := null;
  };

  // Null checking in contracts
  public func hasCount() : async Bool
    reads maybeCount
    ensures result == (maybeCount != null);
  {
    maybeCount != null
  };
}

Key points:

• ?T is the option type containing values of type T
• ?value constructs an option with a value (the "some" case)
• null represents no value (the "none" case)
• null is a subtype of all option types: you can assign null to any ?T

Pattern Matching with switch

Use switch to safely extract values from options:

option-switch.sr9

// Pattern matching on options
persistent actor {
  transient var stored : ?Nat = null;

  // Basic switch pattern
  public func getOrDefault(default : Nat) : async Nat
    reads stored
    ensures stored == null ==> result == default;
  {
    switch (stored) {
      case null { default };
      case (?v) { v };
    }
  };

  // Transform option value
  public func double() : async ?Nat
    reads stored
    ensures switch (stored, result) {
      case (null, null) true;
      case (?n, ?m) m == n * 2;
      case (_, _) false;
    };
  {
    switch (stored) {
      case null { null };
      case (?v) { ?(v * 2) };
    }
  };

  // Switch extracting to local variable
  public func process() : async Nat
    reads stored
  {
    let x = switch (stored) {
      case null { 0 };
      case (?v) { v + 1 };
    };
    x
  };
}

Pattern matching rules:

• case null matches the empty case
• case (?v) matches a value, binding it to v
• case (?_) matches a value without binding
• All cases must be covered (exhaustiveness is checked at compile time)

Null Comparisons

Compare options directly with null and other options:

option-null.sr9

// Null value and comparisons
persistent actor {
  transient var value : ?Nat = null;

  // Return null explicitly
  public func nothing() : async ?Nat
    ensures result == null;
  {
    null
  };

  // Null comparison in preconditions
  public func mustHaveValue() : async Nat
    reads value
    requires value != null;
  {
    switch (value) {
      case (?v) { v };
      case null { 0 };  // unreachable due to requires
    }
  };

  // Null comparison in postconditions
  public func clearIfZero() : async ()
    modifies value
    ensures old(value) == ?0 ==> value == null;
    ensures old(value) != ?0 ==> value == old(value);
  {
    switch (value) {
      case (?0) { value := null };
      case _ { () };
    }
  };

  // Compare two options
  public func equals(a : ?Nat, b : ?Nat) : async Bool
    ensures result == (a == b);
  {
    a == b
  };
}

Null comparison patterns:

• opt != null - checks if option has a value
• opt == null - checks if option is empty
• opt == ?5 - checks if option equals a specific wrapped value
• a == b - compares two options for equality

Chained Unwrapping with do ?

The do ? { } block provides ergonomic chaining of option operations. Use ! to unwrap values inside the block:

option-do-block.sr9

// do ? blocks for chained unwrapping
persistent actor {
  // Chain multiple optional operations
  public func addOptions(a : ?Nat, b : ?Nat) : async ?Nat {
    do ? {
      let x = a!;
      let y = b!;
      x + y
    }
  };

  // Early return on null
  public func test() : async ()
    ensures true;
  {
    // Both values present
    let sum = do ? {
      let x = (?5)!;
      let y = (?10)!;
      x + y
    };
    assert sum == ?15;

    // One value is null - returns null
    let failed = do ? {
      let x = (?5)!;
      let y : ?Nat = null;
      x + y!  // stops here, returns null
    };
    assert failed == null;
  };

  // Complex chains
  public func tripleAdd(a : ?Nat, b : ?Nat, c : ?Nat) : async ?Nat {
    do ? {
      a! + b! + c!
    }
  };
}

How do ? works:

• The block returns ?T where T is the type of the final expression
• Inside the block, opt! unwraps opt and continues if it has a value
• If any ! encounters null, the entire block returns null immediately
• This is similar to the ? operator in Rust or ?. chaining in other languages

The ! operator is only valid inside do ? { } blocks. Using it elsewhere causes error M0064.

Pure Functions with Options

Define reusable option helpers as pure functions for use in contracts:

option-pure.sr9

// Pure functions for option handling
persistent actor {
  // Extract value or return default
  pure func unwrapOr(opt : ?Nat, default : Nat) : Nat {
    switch (opt) {
      case null { default };
      case (?v) { v };
    }
  };

  // Check if option has value
  pure func isSome(opt : ?Nat) : Bool {
    switch (opt) {
      case null { false };
      case (?_) { true };
    }
  };

  // Check if option is empty
  pure func isNone(opt : ?Nat) : Bool {
    switch (opt) {
      case null { true };
      case (?_) { false };
    }
  };

  // Transform the inner value
  pure func map(opt : ?Nat, add : Nat) : ?Nat {
    switch (opt) {
      case null { null };
      case (?v) { ?(v + add) };
    }
  };

  // Use pure functions in contracts
  public func compute(input : ?Nat) : async Nat
    ensures result == unwrapOr(map(input, 10), 0);
  {
    unwrapOr(map(input, 10), 0)
  };
}

Common pure helpers:

• unwrapOr(opt, default) - returns value or default
• isSome(opt) - returns true if option has value
• isNone(opt) - returns true if option is empty
• map(opt, f) - applies function to inner value if present

These pure functions can appear in ensures and requires clauses, making contracts readable.

Nested Options

Options can nest: ??T means "optionally an optional T":

option-nested.sr9

// Nested option types
persistent actor {
  // Double-nested option
  public func unwrapOuter(opt : ??Nat) : async ?Nat
    ensures switch (opt, result) {
      case (null, null) true;
      case (?inner, r) r == inner;
      case (_, _) false;
    };
  {
    switch (opt) {
      case null { null };
      case (?inner) { inner };
    }
  };

  // Full nested handling
  public func increment(opt : ??Nat) : async ??Nat
    ensures switch (opt, result) {
      case (null, null) true;
      case (?null, ?null) true;
      case (??n, ??m) m == n + 1;
      case (_, _) false;
    };
  {
    switch (opt) {
      case null { null };
      case (?inner) {
        switch (inner) {
          case null { ?null };
          case (?n) { ??(n + 1) };
        }
      };
    }
  };
}

Nested option cases for ??Nat:

• null - outer is empty
• ?null - outer has value, inner is empty
• ??5 - both present with value 5

Use nested pattern matching to handle all cases.

Options in Contracts

Options work naturally in verification contracts:

public func find(key : Nat) : async ?Nat
  ensures result == null ==> not contains(key);
  ensures result != null ==> switch (result) {
    case (?v) isValid(v);
    case null false;
  };
{
  // body omitted
}

Common contract patterns:

• requires opt != null - caller must provide a value
• ensures result == ?expected - postcondition on wrapped value
• ensures result == null ==> ... - handle empty case
• switch in postconditions for case-by-case specs

Use tuple patterns for input-output relationships:

ensures switch (input, result) {
  case (null, null) true;
  case (?n, ?m) m == n + 1;
  case (_, _) false;
};

Verification Behavior

The verifier translates options to a domain with constructors and discriminators:

Motoko	Viper Translation
?value	Some(value)
null	None()
opt != null	isSome(opt)
opt == null	isNone(opt)
Extract from ?v	getSome(opt)

The verifier generates axioms ensuring:

• Exhaustiveness: every option is either None or Some
• Exclusivity: an option cannot be both None and Some
• Inverse: getSome(Some(v)) == v
• Injectivity: Some(v1) == Some(v2) implies v1 == v2

Restrictions

Refutable Patterns

Option patterns in let bindings must use else:

// Correct: handle the null case
let ?x = opt else return null;

// Incorrect: refutable pattern without else
let (?x, y) = pair;  // ERROR: pattern might not match

For-In Loops

Option patterns cannot be used in for-in loops:

// NOT SUPPORTED
for (?x in arr.values()) { ... }

Filter options before iteration or use explicit switch inside the loop.

Bang Operator Scope

The ! operator only works inside do ? { } blocks:

// Correct
let result = do ? { opt! + 1 };

// Incorrect - causes error M0064
let x = opt!;

Type Constraints

When extracting from ?Nat, the verifier tracks that the value is a Nat (non-negative). However, complex extraction chains may require explicit assertions to preserve type information.

Error Detection

The verifier catches missing null guards:

option-missing-guard_unsat.sr9

// Verification failure: missing null guard
persistent actor {
  transient var stored : ?Nat = null;

  // BUG: Tries to access stored without null check in precondition
  public func unsafeGet() : async Nat
    reads stored
    ensures result >= 0;  // Fails: stored might be null
  {
    switch (stored) {
      case (?v) { v };
      case null { 0 };  // This case is possible!
    }
  };
}

Without a caller-facing entry_requires and internal requires guard, the verifier cannot prove the postcondition because stored might be null.

Option vs Variant

Feature	Option (?T)	Variant
Syntax	?T	{ #none; #some : T }
Construction	?value, null	#some(value), #none
Pattern	case (?v), case null	case (#some v), case (#none)
Custom names	No	Yes
Multiple empties	No	Yes

Use ?T for simple nullable values. Use variants when you need custom tag names or multiple "empty" states.

Error Codes

Code	Meaning
M0064	Misplaced ! (no enclosing do ? { } expression)
M0065	Expected option type before !, but got different type
M0145	Pattern does not cover all cases (missing null or ?v)

Summary

• ?T represents optional values of type T
• Construct with ?value (some) or null (none)
• Use switch with case null and case (?v) for safe extraction
• Use do ? { } blocks with ! for chained unwrapping
• Compare with opt == null, opt != null, or opt == ?value
• Define pure helpers like unwrapOr and isSome for readable contracts
• Nested options (??T) require nested pattern matching
• Options translate to Some/None constructors in verification
• The verifier requires explicit null guards in preconditions
• Use ?T for nullability; use variants for richer alternatives