Exhaustiveness Checking

Sector9 ensures that switch expressions cover all possible values of a type, then gives the verifier a complete case split to reason about.

Two Proof Stages

Pattern matching participates in two proof stages:

1. Compile time: The type checker ensures all cases are covered and warns about unreachable branches.
2. Verification time: Supported switches are lowered to discriminator-based branch expressions, so postconditions can be proven case by case.

The compiler rejects non-exhaustive patterns before verification begins. This means you cannot accidentally miss a case. The Viper lane then applies an additional verified-subset check: some patterns accepted by the language frontend, such as or-patterns, are still rejected during verification lowering.

Basic Variant Matching

When you match on a variant type, each constructor must have a case:

exhaustive-basic.sr9

// Basic exhaustive pattern matching on variants
persistent actor {
  type Status = { #pending; #approved; #rejected };

  public func statusCode(s : Status) : async Nat
    ensures switch (s) {
      case (#pending) result == 0;
      case (#approved) result == 1;
      case (#rejected) result == 2;
    };
  {
    switch (s) {
      case (#pending) 0;
      case (#approved) 1;
      case (#rejected) 2;
    }
  };
}

The Status type has three variants, and the switch covers all three. The postcondition uses the same switch syntax to specify what each case should return.

Variants with Payloads

Variant constructors can carry data. Pattern matching extracts payloads into bound variables:

exhaustive-payload.sr9

// Exhaustive matching with variant payloads
persistent actor {
  type Color = { #red; #blue : Nat; #green : (Nat, Nat) };

  public func colorValue(c : Color) : async Nat
    ensures switch (c) {
      case (#red) result == 4;
      case (#blue x) result == x;
      case (#green (a, b)) result == a + b;
    };
  {
    switch (c) {
      case (#red) 4;
      case (#blue x) x;
      case (#green (a, b)) a + b;
    }
  };
}

Each case binds variables that can be used in both the implementation and the postcondition:

• #red carries no payload
• #blue x binds x : Nat
• #green (a, b) binds a tuple payload

Option Types

The built-in option type ?T has exactly two cases: null and ?value:

exhaustive-option.sr9

// Exhaustive matching on option types
persistent actor {
  public func increment(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);
    }
  };
}

The postcondition uses a tuple pattern (opt, result) to express the relationship between input and output for each case. The wildcard case (_, _) false keeps the postcondition exhaustive while making impossible combinations fail if the implementation ever produces them.

Nested Pattern Matching

You can nest switches to handle combinations of variant types:

exhaustive-nested.sr9

// Nested exhaustive pattern matching
persistent actor {
  type Shape = { #circle : Nat; #square : Nat };
  type Color = { #red; #blue : Nat };

  public func describe(s : Shape, c : Color) : async Nat
    ensures switch (s, c) {
      case ((#circle r), (#red)) result == r;
      case ((#circle r), (#blue k)) result == r + k;
      case ((#square a), (#red)) result == a * 4;
      case ((#square a), (#blue k)) result == a * 4 + k;
    };
  {
    switch (s) {
      case (#circle r) {
        switch (c) {
          case (#red) r;
          case (#blue k) r + k;
        }
      };
      case (#square a) {
        switch (c) {
          case (#red) a * 4;
          case (#blue k) a * 4 + k;
        }
      };
    }
  };
}

The implementation uses nested switch statements, while the postcondition uses a single switch with tuple patterns. Both approaches are valid and must cover all combinations.

How Verification Works

When Sector9 translates supported switch expressions to the verification backend, it generates:

1. Discriminator functions for each variant constructor (e.g., isStatus$pending, isStatus$approved)
2. Exhaustiveness and exclusivity axioms ensuring every value has one constructor tag
3. Nested if-then-else chains with an unreachable fallback

For a type with constructors #a, #b, #c, the verifier knows:

forall v : Type :: isType$a(v) || isType$b(v) || isType$c(v)

These axioms let the SMT solver reason about which branch is taken and verify that postconditions hold.

Detecting Wrong Postconditions

The verifier catches mismatches between implementation and postcondition:

Wrong

// Wrong postcondition: claims #red returns 5, but code returns 4
persistent actor {
  type Color = { #red; #blue : Nat; #green : (Nat, Nat) };

  public func pick(c : Color) : async Nat
    ensures switch (c) {
      case (#red) result == 5;  // WRONG: actual returns 4
      case (#blue x) result == x;
      case (#green (a, b)) result == a + b;
    };
  {
    switch (c) {
      case (#red) 4;
      case (#blue x) x;
      case (#green (a, b)) a + b;
    }
  };
}

Correct

// Exhaustive matching with variant payloads
persistent actor {
  type Color = { #red; #blue : Nat; #green : (Nat, Nat) };

  public func colorValue(c : Color) : async Nat
    ensures switch (c) {
      case (#red) result == 4;
      case (#blue x) result == x;
      case (#green (a, b)) result == a + b;
    };
  {
    switch (c) {
      case (#red) 4;
      case (#blue x) x;
      case (#green (a, b)) a + b;
    }
  };
}

The wrong version claims #red returns 5, but the implementation returns 4. The verifier detects this contradiction and reports a verification failure.

Compile-Time Errors

If you miss a case, the compiler rejects the program before verification:

// REJECTED: missing #rejected case
switch (status) {
  case (#pending) 0;
  case (#approved) 1;
}

Error M0145: this pattern of type Status does not cover value #rejected

Similarly, unreachable patterns trigger warnings:

// WARNING: second #pending is never matched
switch (status) {
  case (#pending) 0;
  case (#pending) 1;  // unreachable
  case (#approved) 2;
  case (#rejected) 3;
}

Warning M0146: this pattern is never matched

Unsupported Patterns

Some pattern features are not supported in verification:

Pattern	Status	Example
Simple variants	Supported	case (#red)
Variant payloads	Supported	case (#blue x)
Tuple patterns	Supported	case (a, b)
Option patterns	Supported	case (?n)
Wildcards	Supported	case (_)
Or-patterns	Frontend supported, Viper-lane unsupported	case (0 or 1)
Refutable let patterns	Viper-lane unsupported	let ?x = opt
Refutable for patterns	Viper-lane unsupported	for (?x in xs.vals())
Mutable record field patterns	Syntax unsupported	case ({ var x = n })

Attempting to use unsupported verified patterns results in a translation error such as patterns in let bindings must be irrefutable for verification or for-in: pattern with boolean guards not supported.

Summary

• Pattern exhaustiveness is checked at compile time, then used as a complete case split during verification
• All variant constructors must have matching cases
• Postconditions can use switch expressions to specify per-case behavior
• The verifier generates exhaustiveness axioms for SMT reasoning
• Missing cases are compile-time errors (M0145)
• Unreachable patterns trigger warnings (M0146)
• Or-patterns, refutable let patterns, and refutable for patterns are not supported in the Viper verification lane

Related Topics

• Variant contracts for per-case postconditions
• Option unwrapping for ?T, null, and do ?
• Language pattern matching for the general syntax
• Verified subset limitations for source forms accepted by the frontend but rejected by verification