Document number: P4423R0
Audience: EWG


Ville Voutilainen
2026-10-23

Strict contracts: conveyor functions and conveyor predicates

Abstract

This paper presents the design and an implementation of strict contracts: contract predicates that are guaranteed by the compiler to be free of side effects and of undefined behavior. It builds on the conveyor functions of P2680 and P3285, and expresses strictness through the control objects of P4324, of which this paper is a companion. It describes two escape hatches, shows how the standard library's hardened preconditions become strict contracts, and describes the static analysis the compiler performs on top of strict contracts, cross-analyzed against the requirements set out in P3362.

Strict contracts are not a toy subset; they are expressive enough for everyday code, and can implement the standard library's hardened preconditions. In the implementation, 478 of the 509 hardened checks of libstdc++ become strict assertions without being rewritten. 60 of those can instead be declared as preconditions on the functions they guard, such as pre<conveyor_assert_v>(n < size()) on vector::operator[], so that calling code is checked against them: a call guarded by if (i < v.size()) is proven to satisfy that precondition.

Motivation

Contract predicates are code. Like any code, they can contain bugs, have side effects, and have undefined behavior. A contract whose predicate can modify state, or invoke undefined behavior, can change the behavior of the program it is supposed to check, and gives neither a reader nor a tool a reliable statement about the program.

A strict contract removes that problem: its predicate is checked by the compiler to have no side effects and no undefined behavior. That makes the predicate a reliable fact, both when it is evaluated at run time and when it is reasoned about at compile time. As P3362 argues, it is also what makes static analysis based on contracts practical.

Background

The design

Strict predicates are selected by the control object

Whether a contract is strict is a property of its control object: a control object type whose is_conveyor() query returns true makes the predicate of every contract that names it strict. The standard control objects for this are std::contracts::conveyor_assert_v and its variants:

int divide(int a, int b) conveyor pre<std::contracts::conveyor_assert_v>(b != 0);

Strict and relaxed contracts therefore coexist, chosen per contract, without new syntax for the distinction. This is why this paper depends on P4324: the way a strict contract is expressed is a choice of control object.

Conveyor functions

A function declared with the trailing function-specifier conveyor is a conveyor function. The specifier is part of the declaration only; it doesn't change the function's type. A strict predicate may only call conveyor functions, and the body of a conveyor function is checked to have no side effects and no undefined behavior. In summary, a conveyor function or strict predicate:

Where P3285 specifies most of these as syntactic first approximations, the last group is checked by flow analysis over the function body, so a guarded division such as if (y != 0) return x / y; is accepted. As in P3285, whose inc(int&) is a conveyor function, a conveyor function may modify its own locals and objects it is given access to through its parameters; that can't affect the evaluation of a predicate, which can't modify anything.

Three further rules make conveyor functions composable:

As in P2680, a compiler-generated or defaulted special member function is conveyor if the corresponding special members of all its bases and members are.

Escape hatches

conveyor(auto). A template can't always know whether its specializations can be conveyor: less<T> is conveyor exactly when T's operator< is. A function template declared conveyor(auto) is conveyor for each specialization that satisfies the rules, and an ordinary function for each that doesn't, much like the deduction of noexcept. A specialization that isn't conveyor is still usable from ordinary code; it just can't be called from a conveyor function.

Never-proven conveyor assertions. Sometimes a programmer knows something the analysis can't establish. A contract_assert with the control object never_proven_conveyor_v has a strict predicate, so it is still checked to be UB-free and side-effect-free, but its claim is not re-proven from the facts already established. It is trusted, and becomes a fact that later code can rely on. Its run-time checking is unaffected.

Symbolic contracts

The implementation also has a second flavor of strict contracts, symbolic contracts, whose predicates are never evaluated and may name functions that are declared but not defined. A fact established by a conveyor contract can discharge a symbolic obligation, but not the other way around. Symbolic contracts are described in a separate paper, P4425R0.

The standard library's hardened preconditions

A hardened standard library checks preconditions such as "the index is less than size()", "the container is not empty", or "the divisor is not zero". The implementation expresses these checks in two ways, selected by an opt-in build mode:

The key observation is that the hardened preconditions of the standard library are, by nature, free of side effects and of undefined behavior. They compare sizes, test for emptiness, and compare against zero. That makes them natural strict predicates. Turning them into strict contracts mostly required declaring the functions they call, such as size() and empty(), conveyor, not rewriting the checks. In the implementation, 478 out of 509 of the library's hardened assertions become strict assertions under this mode; 31 do not, because they have conditions that call functions that can't be conveyor (in the atomics, unique_ptr, filesystem paths, the copy-on-write string, <future>, <latch> and <text_encoding>); those keep using an ordinary control object.

One consequence should be stated plainly: under this mode, the implicit is_object_address preconditions of the library's conveyor member functions apply to every call. A reference parameter of an ordinary, non-conveyor function is not trusted to refer to an object, since it might dangle, so calling a member function through it can't be proven. Code that uses the strict mode makes its own functions conveyor, which gives their reference parameters the same implicit precondition.

Arithmetic in strict predicates

C++26's saturation arithmetic functions std::saturating_add, std::saturating_sub, std::saturating_mul and std::saturating_cast are declared conveyor. They can't have undefined behavior: they clamp to the representable range instead of overflowing. std::saturating_div can still divide by zero, so it is declared conveyor together with the precondition pre<conveyor_assert_v>(y != 0).

That gives strict predicates a way to do arithmetic. Built-in arithmetic in a strict predicate must be provably free of overflow, which for arbitrary arguments it isn't. The saturating functions are free of it by construction:

void f(int a, int b) pre<conveyor_assert_v>(a + b < 100);                    // error: not provably free of overflow
void g(int a, int b) pre<conveyor_assert_v>(std::saturating_add(a, b) < 100); // OK
void h(int a, int b) pre<conveyor_assert_v>(b != 0 && std::saturating_div(a, b) > 0); // OK
void k(int a, int b) pre<conveyor_assert_v>(std::saturating_div(a, b) > 0);  // error: b not provably nonzero

For a comparison against a value in range, as here, the saturated result gives the same answer as the mathematical one, so g's predicate means what it says. A predicate that calls saturating_div must establish its precondition itself, as h does with its first conjunct. Without it, as in k, the predicate is rejected: a call from a strict predicate, or from a conveyor function, to a conveyor function must establish that function's preconditions, since its freedom from undefined behavior depends on them.

Static analysis based on conveyors

What the compiler checks

Because a strict predicate is guaranteed to be side-effect-free and UB-free, it can be treated as a fact: after a call, the callee's strict postcondition holds; before a call, the callee's strict precondition must hold. The compiler uses this to check call sites against the callee's declaration:

Two separate guarantees are involved, and they shouldn't be confused. The UB-freedom of conveyor code is mandatory. Proving that a precondition actually holds at a call site covers the implicit is_object_address preconditions by default; for other predicates, it is enabled per contract by the control object (lenient "analyzed" or strict "proven" variants) or by a compiler option. The analysis is about values established by the program. Besides ranges of values, it tracks comparisons of a value with another value or with the result of a conveyor accessor, possibly offset by a constant, as in v.size() - i > 10; it doesn't reason about arbitrary relations between variables. Arithmetic that is composed to establish a fact is only trusted where its result is representable: a bound that would overflow is unknown, not assumed.

The implementation has two independent analysis engines, selected with -fcontract-analysis-engine=ast, gimple or both: one over the front end's abstract syntax trees, and one over GIMPLE, GCC's intermediate representation, before optimization. Both read the declared contracts directly. The GIMPLE engine works on the compiler's own control-flow graph and SSA form, and uses its value range analysis, so loops, branches and conversions are handled exactly as the compiler sees them; the AST engine works on the program as written, which keeps its diagnostics close to the source. The two engines agree on the implementation's entire contracts test suite, and differ only in precision: where one proves more than the other, both are sound. Running them side by side has been a strong check of each: several soundness bugs were found by one engine disagreeing with the other.

Cross-analysis against P3362

P3362's claim or requirementWhat the implementation shows
For func_b(func_a()), a strict pred lets the proof be built from declarations and call sites alone. A strict postcondition of one call discharges the strict precondition of the next; only the declarations are used.
If pred is defined in another translation unit, P2900 offers no proof ("game over"). The callees in the examples below are declared but not defined; the proofs work from their declarations.
A virtual pred requires finding and analyzing the final overrider under P2900. An override of a conveyor virtual function must be conveyor, so a proof doesn't depend on which override runs.
Each conveyor function is checked once, and the result reused by any number of analyses. A conveyor body is checked once, when it is compiled; call sites consult only declarations.
The analysis is light enough to run during builds or in an IDE. The conveyor rules, including freedom from undefined behavior, are checked in every compilation. The correctness proofs at call sites are opt-in (-fcontract-conveyor-proofs, or per contract through its control object), and run within the compilation too, from declarations only: no separate tool, and no whole-program pass.
Strict contracts don't replace relaxed ones; both are needed. Both coexist, selected per contract by its control object.
Protection should hold regardless of whether other UB protections are enabled. The conveyor restrictions are mandatory whenever a strict control object is used, independent of any other mode.

Examples

Conveyor function bodies

bool less(int x, int y) conveyor { return x < y; }          // OK
int guarded(int x, int y) conveyor
{ if (y != 0) return x / y; return 0; }                      // OK: the divisor is guarded

int bump(int x) conveyor { counter = x; return 0; }          // error: modifies a global
int fresh() conveyor { int* p = new int(1); return 0; }      // error: new-expression
int peek(int* p) conveyor { int v = *p; return v; }          // error: p not provably an object
int quot(int x, int y) conveyor { int q = x / y; return q; } // error: divisor not provably nonzero
int calls(int x) conveyor { int r = helper(x); return r; }   // error: callee not conveyor

Call sites checked against declarations

// Definitions may be in another translation unit.
int divide(int a, int b) conveyor pre<sc::analyzed_conveyor_v>(b != 0);
int nonzero_hash(int x) conveyor post<sc::conveyor_assert_v>(r: r != 0);

int guarded(int x)   { if (x != 0) return divide(10, x); return 0; } // proven
int chained(int x)   { return divide(10, nonzero_hash(x)); }         // proven from the postcondition
int unchecked(int x) { return divide(10, x); }                       // warning: cannot verify
int zero()           { return divide(10, 0); }                       // error: provably violates

The implicit soundness precondition

int value(const int& r) conveyor { return r; }   // implicitly: pre(is_object_address(&r))

int local()         { int x = 1; return value(x); } // proven: &x is an object
int through(int* p) { return value(*p); }           // error: *p not provably an object

conveyor(auto)

template <class T>
bool less(const T& a, const T& b) conveyor(auto) { return a < b; }

bool use_plain(const Plain& a, const Plain& b) conveyor
{ return less(a, b); }                 // less<Plain> is conveyor
bool use_logged(const Logged& a, const Logged& b)
{ return less(a, b); }                 // less<Logged> is an ordinary function: fine here
bool strict(const Logged& a, const Logged& b) conveyor
{ bool r = less(a, b); return r; }     // error: less<Logged> isn't conveyor

A never-proven conveyor assertion

int f(int x)
{
  int c = checksum(x) | 1;                              // odd, so never zero
  contract_assert<sc::never_proven_conveyor_v>(c != 0); // UB-free, trusted, not re-proven
  return divide(100, c);                                // proven from the trusted fact
}

A hardened standard library precondition

std::vector<int> v{1, 2, 3};
if (i < v.size())
  return v[i];   // proven: pre(n < size()) on vector::operator[]
return v[i];     // warning: cannot verify

Implementation experience

The design is implemented in a GCC branch, together with P4324's control objects, and applied to libstdc++: 204 functions and function templates across 44 headers are declared conveyor or conveyor(auto), 478 of its 509 hardened checks become strict assertions, and 60 of those can instead be declared as preconditions. The examples above are available on Compiler Explorer with the "x86-64 gcc (P4324 contracts, and profiles)" compiler, using -std=c++26 -fcontracts -fcontract-control-objects:

Wording

To be supplied.