Requires

requires clauses are function preconditions. They describe facts that callers must satisfy before the function body runs. The compiler can use those facts as Z3 assumptions when verifying the body and call sites.

Syntax

Contract clauses appear after the function signature and before the body:

func:divide = int32(int32:a, int32:b)
    requires b != 0i32
{
    pass(a / b);
};

Multiple clauses are comma-separated and are treated as conjunctions:

func:clamp_to_byte = int32(int32:value)
    requires value >= 0i32, value <= 255i32
{
    pass(value);
};

Caller obligations

A caller must prove the callee's requires clause from local facts. Facts may come from:

the caller's own requires clauses;
local limit<Rules> bindings;
facts from previous ensures clauses;
simple guards and assignments the verifier can encode.

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

func:caller = int32(int32:y)
    requires y > 0i32
{
    pass(raw need_positive(y));
};

Contradictions are errors

The compiler rejects impossible preconditions because no caller can satisfy them:

func:impossible = int32(int32:x)
    requires x > 0i32, x < 0i32
{
    pass(x);
};

This pattern is covered by bug693_contract_contradictory_requires_z3_fail.npk.

Good boundary pattern

Use requires where data crosses an API boundary, then use narrower local limit<Rules> bindings only where code needs named range evidence:

Rules:Percentage = { $ >= 0, $ <= 100 };

func:store_percentage = NIL(int32:value)
    requires value >= 0i32, value <= 100i32
{
    limit<Percentage> int32:pct = value;
    prove(pct <= 100i32);
    pass(NIL);
};

Diagnostics and validation

Unsatisfied call-site requirements are contract verification failures.
Contradictory requires clauses are rejected by Z3.
Recursive or nested call expressions inside contract clauses are deliberately restricted by the v0.34.3 purity scan.