Skip to main content

Variant Contracts

Postconditions can specify different guarantees for each variant case, letting you express precise relationships between inputs and outputs based on which constructor is matched.

Per-Case Postconditions​

Use switch expressions in ensures clauses to specify what each variant case should return:

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;
    }
  };
}

The postcondition mirrors the implementation structure. Each case binds the same payload variables and specifies the expected result:

  • #red has no payload and returns a constant
  • #blue x binds x and returns it unchanged
  • #green (a, b) binds a tuple and returns the sum

Result-Style Variants​

A common pattern is the Result type with success and error variants. Use implication to specify behavior based on input conditions:

variant-result-type.sr9
// Variant contracts with Result-style types
persistent actor {
  type Result = { #ok : Nat; #err : Text };

  public func divide(a : Nat, b : Nat) : async Result
    ensures b == 0 ==> result == #err("division by zero");
    ensures b != 0 ==> result == #ok(a / b);
  {
    if (b == 0) { #err("division by zero") } else { #ok(a / b) }
  };
}

The ==> operator connects conditions to outcomes:

  • When b == 0, the result must be the error variant
  • When b != 0, the result must be the success variant with the computed value

The second implication also protects the division in the postcondition: the non-zero divisor fact is available on the right side of ==>. See division safety for the general rule.

Pure Helper Functions​

For complex variant logic, extract predicates into pure functions:

variant-pure-helper.sr9
// Pure helper functions for variant predicates
persistent actor {
  type Status = { #pending; #approved : Nat; #rejected : Text };

  pure func isPending(s : Status) : Bool {
    switch (s) {
      case (#pending) true;
      case (_) false;
    }
  };

  pure func getApprovalId(s : Status) : Nat {
    switch (s) {
      case (#approved id) id;
      case (_) 0;
    }
  };

  public func checkPending(s : Status) : async Bool
    ensures result == isPending(s);
  {
    isPending(s)
  };

  public func extractId(s : Status) : async Nat
    ensures result == getApprovalId(s);
  {
    getApprovalId(s)
  };
}

Pure functions that pattern match on variants can be called in postconditions. The verifier inlines these functions and reasons about each case. This keeps postconditions readable while handling complex variant logic.

State Transitions with Variants​

Variant types work well for modeling state machines. Preconditions restrict which transitions are valid, and postconditions specify the target state:

variant-state-transition.sr9
// Variant contracts with state transitions
persistent actor {
  type Status = { #pending; #approved : Nat; #rejected };

  var status : Status = #pending;

  public func approve(id : Nat) : async ()
    modifies status
    entry_requires status == #pending;
    requires status == #pending;
    ensures status == #approved(id);
  {
    status := #approved(id)
  };

  public func reject() : async ()
    modifies status
    entry_requires status == #pending;
    requires status == #pending;
    ensures status == #rejected;
  {
    status := #rejected
  };

  public func reset() : async ()
    modifies status
    ensures status == #pending;
  {
    status := #pending
  };
}

Key patterns:

  • requires status == #pending restricts transitions to valid source states
  • ensures status == #approved(id) specifies the exact target variant with its payload
  • The reset function can transition from any state, so it has no precondition

For public actor methods, source-state preconditions should also be mirrored with entry_requires when callers control the transition.

Generic Postconditions​

Sometimes you need a property that holds regardless of which variant case is matched:

variant-generic-postcondition.sr9
// Generic postcondition that must hold for all variant cases
persistent actor {
  type Result = { #ok : Nat; #err : Text };

  public func safeValue(r : Result) : async Nat
    ensures result >= 0;
  {
    switch (r) {
      case (#ok n) n;
      case (#err _) 0;
    }
  };

  public func doubleOrZero(r : Result) : async Nat
    ensures (switch (r) {
      case (#ok n) result == n * 2;
      case (#err _) result == 0;
    });
    ensures result >= 0;
  {
    switch (r) {
      case (#ok n) n * 2;
      case (#err _) 0;
    }
  };
}

The safeValue function has a single postcondition that the verifier must prove for all variant cases. The doubleOrZero function combines per-case postconditions with a generic one.

How Variant Contracts Work​

When you write a switch expression in a postcondition, Sector9 translates it to nested conditionals:

ensures switch (c) {
  case (#red) result == 4;
  case (#blue x) result == x;
  case (#green (a, b)) result == a + b;
}

Becomes:

ensures isColor$red(c) ? (result == 4) :
        (isColor$blue(c) ? (result == getColor$blue$0(c)) :
         (result == getColor$green$0(c) + getColor$green$1(c)))

The verifier generates:

  1. Discriminator functions like isColor$red(c) to test which constructor
  2. Getter functions like getColor$blue$0(c) to extract payloads
  3. Exhaustiveness and exclusivity axioms ensuring every value has one constructor tag

Detecting Mismatches​

The verifier catches when postconditions contradict the implementation:

// Generic postcondition that must hold for all variant cases
persistent actor {
  type Result = { #ok : Nat; #err : Text };

  public func safeValue(r : Result) : async Nat
    ensures result >= 0;
  {
    switch (r) {
      case (#ok n) n;
      case (#err _) 0;
    }
  };

  public func doubleOrZero(r : Result) : async Nat
    ensures (switch (r) {
      case (#ok n) result == n * 2;
      case (#err _) result == 0;
    });
    ensures result >= 0;
  {
    switch (r) {
      case (#ok n) n * 2;
      case (#err _) 0;
    }
  };
}

The wrong version claims #ok n returns n + 1, but the implementation returns n. The verifier detects this and reports a postcondition failure.

Using result with Variants​

The result keyword works with variant return types. You can:

  • Compare result to a specific variant: result == #ok(42)
  • Match on result in a switch: switch (result) { case (#ok n) ... }
  • Combine result with input in tuple patterns: switch (input, result) { ... }

Example with tuple pattern:

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

The pattern (opt, result) lets you express the relationship between input and output for each case combination.

Restrictions​

Variant contracts have the same restrictions as other pattern matching in verification:

PatternStatus
Simple variants (#tag)Supported
Variant payloads (#tag x)Supported
Tuple payloads (#tag (a, b))Supported
Wildcards (_)Supported
Or-patterns (case (0 or 1))Frontend supported, Viper-lane unsupported
Refutable let and for patternsViper-lane unsupported

See Exhaustiveness Checking for details on pattern restrictions.

Summary​

  • Use switch in ensures clauses to specify per-case postconditions
  • Payload variables bound in patterns can appear in postcondition expressions
  • Pure helper functions simplify complex variant logic in contracts
  • The ==> operator connects conditions to variant outcomes
  • Variant fields work with state machine patterns using requires/ensures
  • The verifier translates switch expressions to nested conditionals with discriminators
  • Mismatches between implementation and postcondition trigger verification failures