Skip to main content

The result Keyword

The result keyword refers to the return value of a successful function return inside postconditions.

When you write an ensures clause, result is automatically bound to whatever value the function returns. This allows you to specify constraints on the output.

Basic Syntax​

public func add(a : Nat, b : Nat) : async Nat
  ensures result == a + b;
{
  a + b
}

The verifier proves that for all valid inputs, the returned value equals a + b.

Where result Can Appear​

The result keyword is only valid in postconditions (ensures clauses, and phase ensures in the phase-contract subset). Using it anywhere else causes a type error:

ContextValid?
ensures result == ...Yes
requires result == ...No - M0057 "unbound variable"
assert result == ...No - M0057 "unbound variable"
Function bodyNo - M0057 "unbound variable"
invariant result == ...No - M0057 "unbound variable"

The reason: result represents the function's output, which doesn't exist until the function completes. Preconditions run before execution, so result has no meaning there.

Result with Different Types​

Primitive Types​

public func getBalance() : async Nat
  reads balance
  ensures result == balance;
{
  balance
}

public func isPositive(x : Int) : async Bool
  ensures result == (x > 0);
{
  x > 0
}

Unit Return Type​

Functions returning () can still use result:

public func reset() : async ()
  modifies counter
  ensures counter == 0;
  ensures result == ();
{
  counter := 0;
}

In practice, postconditions for unit functions typically focus on state changes rather than result.

Tuples​

Access tuple elements using .0, .1, etc:

public func swap(a : Int, b : Int) : async (Int, Int)
  ensures result.0 == b;
  ensures result.1 == a;
{
  (b, a)
}

public func minMax(a : Int, b : Int) : async (Int, Int)
  ensures result.0 <= result.1;
  ensures result.0 == a or result.0 == b;
  ensures result.1 == a or result.1 == b;
{
  if (a <= b) { (a, b) } else { (b, a) }
}

Records​

Access record fields with dot notation:

type Point = { x : Int; y : Int };

public func origin() : async Point
  ensures result.x == 0;
  ensures result.y == 0;
{
  { x = 0; y = 0 }
}

Options​

Use pattern matching or comparison with null:

public func find(key : Nat) : async ?Nat
  reads data
  ensures key < data.size() ==> result == ?data[key];
  ensures key >= data.size() ==> result == null;
{
  if (key < data.size()) { ?data[key] } else { null }
}

Variants​

Specify which variant is returned:

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

Multiple Postconditions​

You can use result across multiple ensures clauses. All must hold:

public func clamp(x : Int, lo : Int, hi : Int) : async Int
  entry_requires lo <= hi;
  requires lo <= hi;
  ensures result >= lo;
  ensures result <= hi;
  ensures x < lo ==> result == lo;
  ensures x > hi ==> result == hi;
  ensures lo <= x and x <= hi ==> result == x;
{
  if (x < lo) { lo }
  else if (x > hi) { hi }
  else { x }
}

Result with old()​

Combine result with old() to relate return values to pre-state:

public func increment() : async Nat
  modifies count
  ensures count == old(count) + 1;
  ensures result == count;
{
  count += 1;
  count
}

public func pop() : async ?Int
  modifies stack
  ensures old(stack.size()) > 0 ==> result == ?old(stack[stack.size() - 1]);
  ensures old(stack.size()) == 0 ==> result == null;
{
  // implementation
}

Result with Implication​

Use ==> to specify conditional guarantees:

public func sign(x : Int) : async Int
  ensures x > 0 ==> result == 1;
  ensures x < 0 ==> result == -1;
  ensures x == 0 ==> result == 0;
{
  if (x > 0) { 1 } else if (x < 0) { -1 } else { 0 }
}

Common Patterns​

Returning State​

public func getCount() : async Nat
  reads count
  ensures result == count;
{
  count
}

Bounds Checking​

public func saturatingAdd(a : Nat, b : Nat) : async Nat
  ensures result >= a;
  ensures result >= b;
  ensures result <= a + b;
{
  a + b
}

Transformation Guarantees​

public func absolute(x : Int) : async Nat
  ensures result >= 0;
  ensures x >= 0 ==> result == x;
  ensures x < 0 ==> result == -x;
{
  if (x >= 0) { x } else { -x }
}

Preservation Properties​

public func double(x : Nat) : async Nat
  ensures result == 2 * x;
  ensures x > 0 ==> result > x;
{
  x * 2
}

Common Mistakes​

Using result in Preconditions​

// WRONG - won't compile
public func bad(x : Int) : async Int
  requires result > 0;  // Error: M0057 unbound variable result
{
  x
}

Using result in Function Body​

// WRONG - won't compile
public func bad(x : Int) : async Int
  ensures result > 0;
{
  assert result > 0;  // Error: M0057 unbound variable result
  x
}

Forgetting Return Type Mismatch​

If your postcondition doesn't match the return type, verification fails:

// This will fail to verify
public func getOne() : async Nat
  ensures result == -1;  // Nat can't be negative
{
  1
}

Summary​

  • result refers to the function's return value in ensures clauses
  • Only valid in postconditions, nowhere else
  • Works with all return types: primitives, tuples, records, options, variants
  • Use .0, .1 for tuple access, .field for record access
  • Combine with old() to relate output to input state
  • Multiple ensures clauses with result are conjoined (all must hold)