Conditionals

Conditionals let runtime code and specifications split facts into explicit cases. In verified code, each branch is a proof path: postconditions, actor invariants, and declared effects must hold no matter which branch runs.

Basic Syntax

The if/else construct is an expression in Sector9, meaning it returns a value. The basic form is:

if (condition) { thenExpr } else { elseExpr }

The condition must be of type Bool. Both branches return values, and the overall type is the common supertype of both branch types.

cond-basic.sr9
// Basic if/else expressions
module {
  // If/else returns a value
  pure func max(a : Int, b : Int) : Int {
    if (a >= b) { a } else { b }
  };

  // If without else returns unit
  public func maybeLog(shouldLog : Bool) : async () {
    if (shouldLog) {
      // side effect would go here
    };
  };
}

If Without Else

When you omit the else branch, the expression returns unit ():

if (condition) {
  // side effect
};

This is useful for conditional side effects where you don't need a return value.

Chained Conditionals

Use else if to chain multiple conditions:

cond-chain.sr9
// Chained if/else if/else
module {
  pure func sign(x : Int) : Int {
    if (x > 0) {
      1
    } else if (x < 0) {
      -1
    } else {
      0
    }
  };

  pure func grade(score : Nat) : Text {
    if (score >= 90) { "A" }
    else if (score >= 80) { "B" }
    else if (score >= 70) { "C" }
    else if (score >= 60) { "D" }
    else { "F" }
  };
}

Chained conditionals are evaluated top-to-bottom. The first branch whose condition is true executes, and remaining branches are skipped.

Type Requirements

Condition Type

The condition expression must be exactly Bool. There are no implicit conversions:

// Correct
if (x > 0) { ... }
if (flag) { ... }
if (a == b) { ... }

// Wrong - these are not Bool
// if (x) { ... }      // x is Int, not Bool
// if (count) { ... }  // count is Nat, not Bool

Branch Types

Branch types don't need to match exactly. The compiler computes the least upper bound (LUB) of both types:

let x : Int = if (flag) { 5 } else { -3 };  // Both Int
let y = if (flag) { 1 } else { 2 };         // Inferred as Int

If branch types are incompatible, the compiler issues warning M0081 and infers an opaque supertype. Prefer explicit type annotations or matching branch types.

Nested Conditionals

Conditionals can be nested arbitrarily deep:

cond-nested.sr9
// Nested conditionals
module {
  pure func quadrant(x : Int, y : Int) : Nat {
    if (x >= 0) {
      if (y >= 0) { 1 } else { 4 }
    } else {
      if (y >= 0) { 2 } else { 3 }
    }
  };

  // Combining with boolean operators is often cleaner
  pure func quadrantAlt(x : Int, y : Int) : Nat {
    if (x >= 0 and y >= 0) { 1 }
    else if (x < 0 and y >= 0) { 2 }
    else if (x < 0 and y < 0) { 3 }
    else { 4 }
  };
}

For complex conditions, consider boolean operators (and, or) or switch expressions so the value shape is visible in the code.

Conditionals in Pure Functions

Pure functions can use conditionals for side-effect-free case analysis:

cond-pure.sr9
// Conditionals in pure functions
module {
  // Pure functions with conditionals for case analysis
  pure func abs(x : Int) : Int {
    if (x < 0) { -x } else { x }
  };

  pure func clamp(x : Int, lo : Int, hi : Int) : Int {
    if (x < lo) { lo }
    else if (x > hi) { hi }
    else { x }
  };

  // Using pure conditionals in contracts
  pure func isValid(x : Nat) : Bool {
    x > 0 and x < 1000
  };
}

Pure conditional functions are callable from requires and ensures clauses, making them useful for reusable predicates.

Verification with Conditionals

Postconditions with Implication

When a function's behavior depends on a condition, implication (==>) is often clearer than a nested conditional:

cond-contract.sr9
// Conditionals with verification contracts
persistent actor {
  var balance : Nat = 100;

  // Postconditions use implication for branch-dependent behavior
  public func withdraw(amount : Nat) : async Bool
    modifies balance
    ensures amount <= old(balance) ==> result == true;
    ensures amount <= old(balance) ==> balance == old(balance) - amount;
    ensures amount > old(balance) ==> result == false;
    ensures amount > old(balance) ==> balance == old(balance);
  {
    if (amount <= balance) {
      balance -= amount;
      true
    } else {
      false
    }
  };
}

The verifier proves each implication under the branch fact on the left side. Use this when different input regions imply different result facts.

Invariant Preservation

When conditionals appear in methods, every branch that can reach the end of the method must re-establish actor invariants:

persistent actor {
  var balance : Nat = 0;
  invariant balance <= 1000;

  public func adjust(delta : Int) : async ()
    modifies balance
    entry_requires balance + delta >= 0;
    entry_requires balance + delta <= 1000;
    requires balance + delta >= 0;
    requires balance + delta <= 1000;
  {
    if (delta > 0) {
      balance += delta;  // Must preserve: balance <= 1000
    } else {
      balance -= (-delta);  // Must preserve: balance <= 1000
    };
  };
}

The verifier checks that the invariant holds after both branches.

Conditional Effects

When a field is written in only one branch, it's still included in the effects summary:

private func maybeIncrement(flag : Bool) : () modifies counter {
  if (flag) {
    counter += 1;
  };
  // counter is in effects even though it's conditionally written
};

Fields not written in any branch can be framed as unchanged. Use modifies to make conditional writes explicit in the method contract.

Common Patterns

Guard Pattern

Check a condition before proceeding:

public func process(x : Nat) : async Nat
  entry_requires x > 0;
  requires x > 0;
{
  if (x == 0) {
    return 0;  // Early return (though precondition already guards this)
  };
  // Main logic
  x * 2
};

Conditional Assignment

Select between values:

let status = if (count > 0) { #active } else { #inactive };

Null Checking

For option types, prefer switch over if:

// Prefer switch for options
switch (maybeValue) {
  case (?v) { /* use v */ };
  case null { /* handle null */ };
};

// Rather than
if (maybeValue != null) { ... }

Restrictions

Contract Style

Prefer implications or switch expressions in contracts because they keep each proof case explicit:

// Correct - use implication
ensures x > 0 ==> result > 0;

// Also valid when a true value expression is clearer
ensures if (x > 0) { result > 0 } else { true };

No Allocation in Loop Conditions

Array or object literals cannot appear in while conditions:

// Rejected
while (([] : [Nat]).size() == 0) { ... }

// Use a variable instead
let arr : [Nat] = [];
while (arr.size() == 0) { ... }

Summary

if/else is an expression that returns a value
The condition must be Bool; no implicit conversions
Branch types are unified via least upper bound
if without else returns unit ()
Use ==> or switch in contracts when a proof splits into cases
Both branches must preserve invariants
Prefer switch for option types and pattern matching

Pattern matching for variants, options, and richer case analysis
Requires and ensures for branch-dependent specifications
Actor invariants for branch obligations over persistent state

Basic Syntax​

If Without Else​

Chained Conditionals​

Type Requirements​

Condition Type​

Branch Types​

Nested Conditionals​

Conditionals in Pure Functions​

Verification with Conditionals​

Postconditions with Implication​

Invariant Preservation​

Conditional Effects​

Common Patterns​

Guard Pattern​

Conditional Assignment​

Null Checking​

Restrictions​

Contract Style​

No Allocation in Loop Conditions​

Summary​

Related Topics​