Conditions on entry and return

A stock update has two obligations: the requested quantity must be available, and the remaining quantity must account for every unit removed. Put those conditions next to the function signature.

// A checkout must conserve the requested quantity and never overdraw stock.

fn remaining_stock(available: int, requested: int) -> int
    requires available >= 0
    requires requested >= 0 && requested <= available
    ensures result >= 0 && result + requested == available
{
    if requested == 0 { return available }
    available - requested
}

let remaining = remaining_stock(12, 5)
assert(remaining == 7)
assert(remaining_stock(12, 0) == 12)
print("Remaining stock: {remaining}")

requires runs before the body. ensures runs after a normal return and reads its value through result. Each condition must be Boolean. A false condition raises an error naming the function, condition and source location.

A condition cannot return or propagate with ? out of the checked function. Use an inner callback or attempt for local control flow inside a condition.

A tail expression, return and ? all pass through the return checks exactly once. Body cleanup finishes before those checks. Returning Result::Err through ? is still a normal return; a panic or failed task skips ensures. In an async fn, result is the completed value, and checks finish before its Future completes.

Write all requires clauses before ensures. Conditions can read parameters and surrounding bindings; body-local variables are outside their scope. Contracts are available on functions, methods and trait methods with a default body. Generator contracts are rejected because a yield is not a completed return. Asynchronous checked functions cannot execute at comptime.