Ensures

ensures clauses are function postconditions. They describe facts that must be true for the function's successful return value and can be propagated to callers.

Syntax

Use ensures after the function signature and before the body:

func:seven = int32()
    ensures result == 7i32
{
    pass(7i32);
};

The result pseudo-variable names the successful return value. It is available only inside ensures clauses.

Result scope

result is not a normal local variable. It is rejected outside ensures:

func:bad = int32() {
    // error: ARIA-070 / ARIA-RESULT-OUT-OF-SCOPE
    int32:x = result;
    pass(x);
};

Valid use:

func:make_positive = int32(int32:x)
    requires x >= 0i32, x < 1000i32
    ensures result > 0i32
{
    pass(x + 1i32);
};

Propagation to downstream calls

A caller may rely on an ensures fact when proving a later requires clause:

func:need_positive = int32(int32:x)
    requires x > 0i32
{
    pass(x);
};

func:chain = int32(int32:x)
    requires x >= 0i32, x < 1000i32
{
    int32:y = raw make_positive(x);
    pass(raw need_positive(y));
};

The v0.34.3 suite locks this with bug692_contract_ensures_chain_z3_pass.npk.

Failure modes

A postcondition fails when the body cannot establish it on every success path:

func:bad_abs = int32(int32:x)
    ensures result >= 0i32
{
    pass(x); // not valid for negative x
};

When Z3 finds a counterexample, compile-time verification reports the contract failure instead of silently trusting the annotation.

Purity of clauses