Option Unwrapping

Sector9 provides two verification-friendly mechanisms for extracting values from option types: the ! operator inside do ? { } blocks and pattern matching with switch. Pattern matching handles both cases explicitly; ! is only legal in the null-propagating do ? context.

The `do ? { }` Block

The do ? { } block creates a context where you can use the ! operator to unwrap options. If any unwrap encounters null, the entire block returns null:

unwrap-do-block.sr9
// Safe option unwrapping with do ? blocks
persistent actor {
  public func add(a : ?Nat, b : ?Nat) : async ?Nat {
    do ? {
      let x = a!;
      let y = b!;
      x + y
    }
  };

  public func test() : async ()
    ensures true;
  {
    let computed = do ? {
      let x = (?5)!;
      let y = (?10)!;
      x + y
    };
    assert computed == ?15;

    let withNull = do ? {
      let x = (?5)!;
      let y : ?Nat = null;
      x + y!
    };
    assert withNull == null;
  };
}

Key behaviors:

Each ! attempts to extract the value from an option
If the option is null, evaluation stops and the block returns null
If all unwraps succeed, the block returns ?result (wrapped in Some)
The block's return type is always an option

Pattern Matching

The standard approach to option unwrapping is pattern matching with switch:

unwrap-switch-pattern.sr9
// Option unwrapping via pattern matching
persistent actor {
  public func unwrapOr(opt : ?Nat, default : Nat) : async Nat
    ensures opt == null ==> result == default;
    ensures opt != null ==> (switch opt { case (?n) result == n; case null false });
  {
    switch (opt) {
      case null { default };
      case (?v) { v };
    }
  };

  public func isNonNull(opt : ?Nat) : async Bool
    ensures result == (opt != null);
  {
    switch (opt) {
      case null { false };
      case (?_) { true };
    }
  };
}

Pattern matching:

Is exhaustive: you must handle both null and ?value cases
Binds the unwrapped value to a variable (v in case (?v))
Works in postconditions to express relationships

For verified code, prefer switch when you need to continue with a non-option result. Refutable let patterns such as let ?x = opt are rejected by the Viper lane because they do not cover null.

Guarded Unwrapping

When you can prove an option is non-null via preconditions, unwrapping becomes safe:

unwrap-guarded.sr9
// Guarded unwrapping with preconditions
persistent actor {
  public func mustUnwrap(opt : ?Nat) : async Nat
    entry_requires opt != null;
    requires opt != null;
  {
    switch opt {
      case (?v) v;
      case null { 0 };
    }
  };

  transient var stored : ?Nat = null;

  public func getStored() : async Nat
    reads stored
    entry_requires stored != null;
    requires stored != null;
  {
    switch stored {
      case (?v) v;
      case null { 0 };
    }
  };

  public func setStored(val : Nat) : async ()
    modifies stored
    ensures stored == ?val;
  {
    stored := ?val;
  };
}

The requires opt != null precondition guarantees the option is non-null. For public actor methods, mirror caller-controlled guards with entry_requires. The verifier translates != null to isSome(opt) internally, so a switch can return a fallback in the null branch while that branch is unreachable under the precondition.

Pure Functions for Options

Pure functions can encapsulate common option patterns and be called in contracts:

unwrap-pure.sr9
// Pure functions for option handling
persistent actor {
  pure func unwrapOr(opt : ?Nat, default : Nat) : Nat {
    switch (opt) {
      case null { default };
      case (?v) { v };
    }
  };

  pure func isSome(opt : ?Nat) : Bool {
    switch (opt) {
      case null { false };
      case (?_) { true };
    }
  };

  pure func map(opt : ?Nat, add : Nat) : ?Nat {
    switch (opt) {
      case null { null };
      case (?v) { ?(v + add) };
    }
  };

  public func test() : async Nat
    ensures result == 15;
  {
    let x = map(?5, 10);
    assert isSome(x);
    unwrapOr(x, 0)
  };
}

Common pure helpers:

unwrapOr: Returns the value or a default
isSome/isNone: Tests for presence
map: Transforms the inner value if present

The verifier inlines these functions, so you can use them in postconditions.

Options in Postconditions

Use switch expressions in ensures clauses to specify behavior for each option case:

unwrap-postcondition.sr9
// Option handling in postconditions
persistent actor {
  public func next(opt : ?Nat) : async ?Nat
    ensures switch (opt, result) {
      case (null, null) true;
      case (?n, ?m) m == n + 1;
      case (_, _) false;
    };
  {
    switch (opt) {
      case (null) null;
      case (?n) ?(n + 1);
    }
  };

  public func find(arr : [Nat], target : Nat) : async ?Nat
    reads arr
    ensures result != null ==> (switch result { case (?idx) idx < arr.size() and arr[idx] == target; case null false });
  {
    var i : Nat = 0;
    loop:invariant i <= arr.size();
    loop:invariant forall<Nat>(pure func (j : Nat) : Bool =
      j < i ==> arr[j] != target);
    while (i < arr.size()) {
      if (arr[i] == target) {
        return ?i;
      };
      i := i + 1;
    };
    null
  };
}

The tuple pattern (input, result) lets you express the relationship between input option and output option. The wildcard case (_, _) false ensures exhaustiveness.

Nested Options

Double option types (??T) require nested pattern matching:

unwrap-nested.sr9
// Nested option types
persistent actor {
  public func shift(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);
        }
      };
    }
  };
}

Each level of nesting adds complexity to the postcondition. The cases are:

(null, null): Outer null maps to outer null
(?null, ?null): Inner null maps to inner null
(??n, ??m): Doubly-wrapped value is transformed

How Verification Works

When Sector9 translates option operations, it generates:

isSome(opt) / isNone(opt): Discriminator functions to test presence
getSome(opt): Accessor to extract the wrapped value
Some(v) / None(): Constructors for building options

For a switch on options:

switch (opt) {
  case null { default };
  case (?v) { v };
}

The verifier generates:

isNone(opt) ? default : getSome(opt)

With these axioms ensuring soundness:

Exhaustiveness: forall o :: isNone(o) || isSome(o)
Exclusivity: forall o :: !(isNone(o) && isSome(o))
Inverse: forall v :: getSome(Some(v)) == v

Compile-Time Errors

Using ! outside a do ? { } block is rejected at compile time:

Wrong
Correct

// Rejected: bang operator outside do ? block
persistent actor {
  public func wrong() : async Nat {
    let opt : ?Nat = ?5;
    opt!
  };
}

// Safe option unwrapping with do ? blocks
persistent actor {
  public func add(a : ?Nat, b : ?Nat) : async ?Nat {
    do ? {
      let x = a!;
      let y = b!;
      x + y
    }
  };

  public func test() : async ()
    ensures true;
  {
    let computed = do ? {
      let x = (?5)!;
      let y = (?10)!;
      x + y
    };
    assert computed == ?15;

    let withNull = do ? {
      let x = (?5)!;
      let y : ?Nat = null;
      x + y!
    };
    assert withNull == null;
  };
}

Error M0064: misplaced '!' (no enclosing 'do ? { ... }' expression)

The ! operator requires a surrounding do ? { } block that provides the null-propagation context.

Similarly, using ! on a non-option type triggers:

Error M0065: expected option type before '!', but expression produces type T

Null Comparisons

Direct null comparisons translate cleanly:

Expression	Viper Translation
`opt == null`	`isNone(opt)`
`opt != null`	`isSome(opt)`

These work in requires, ensures, assert, and other specification contexts.

Unsupported Patterns

Some option-related patterns are not supported in verification:

Pattern	Status	Error
`!` inside `do ? { }`	Supported	-
Pattern match `case (?v)`	Supported	-
`!` outside `do ? { }`	Rejected	M0064
`!` on non-option	Rejected	M0065
Option pattern in `for`	Viper-lane unsupported	`for-in: pattern with boolean guards not supported`
Option pattern in `let` / tuple `let`	Viper-lane unsupported	`patterns in let bindings must be irrefutable for verification`

For for loops, only simple variable binders are allowed in verified code. Refutable patterns like ?x must use explicit switch inside the loop body. For let, use an exhaustive switch or a do ? block instead of a refutable option pattern.

Summary

Use do ? { } with ! for chained unwrapping with early null return
Use switch pattern matching for explicit handling of both cases
Preconditions with requires opt != null prove safety for switch-based unwrapping
Pure functions encapsulate option logic for use in contracts
The verifier translates options to isSome/isNone/getSome functions
! outside do ? { } is a compile-time error (M0064)
Option patterns in for loops and refutable let bindings are not supported

Exhaustiveness checking for option and variant case coverage
Variant contracts for switch expressions in postconditions
Options for the language-level ?T model
Verified subset limitations for refutable pattern restrictions in verification

The do ? { } Block​

Pattern Matching​

Guarded Unwrapping​

Pure Functions for Options​

Options in Postconditions​

Nested Options​

How Verification Works​

Compile-Time Errors​

Null Comparisons​

Unsupported Patterns​

Summary​

Related Topics​