Prove

prove(expr); is a hard compile-time proof directive. If a proof cannot be discharged, compilation fails.

Syntax

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

func:check = NIL(int32:x) {
    limit<Percentage> int32:pct = x;
    prove(pct >= 0i32);
    prove(pct <= 100i32);
    pass(NIL);
};

prove statements are erased after successful verification and have no runtime cost.

Automatic verification

As of v0.34.5, a module containing prove statements enters the verification pass even if the user did not explicitly pass --verify. This keeps prove from becoming a silent no-op.

Z3 outcome mapping

The compiler asks Z3 whether axioms ∧ ¬condition is satisfiable:

Z3 outcome	Meaning for `prove`	Compiler behavior
`UNSAT`	no counterexample exists	proof succeeds; statement erases
`SAT`	counterexample exists	compile error ARIA-073
`UNKNOWN` / translation failure	solver could not discharge	compile error ARIA-074

Diagnostics:

ARIA-073: ARIA-PROVE-UNSAT: prove() assertion is not valid
ARIA-074: ARIA-PROVE-TIMEOUT: prove() obligation timed out or could not be discharged

The historical mnemonic UNSAT in ARIA-PROVE-UNSAT is source-facing release language for an invalid proof/counterexample result.

SMT-LIB dumps

Use --debug-z3 to print the solver query for prove and assert_static obligations. This is useful when a proof that looks obvious to a person is too complex or unsupported for the current encoder.

npkc program.npk --debug-z3

The dump is emitted from the compiler's VerifyOutcome::smtlib capture, so it matches the exact query the verifier sent to Z3.

When to use `prove`

Use prove for facts that are part of correctness, not just debugging:

array/index facts that must be true before unsafe-looking arithmetic;
range facts after limit<Rules> bindings;
assumptions you want CI to reject if a later edit invalidates them.

If a fact is helpful but can fall back to runtime checking, prefer assert_static.