[SwayamInSync]

std::min and std::max in a contract ended Unresolved: obligation lowering failed: f (missing spec definition: fn_...): they are constexpr templates of the standard library, which the converter applies as specs but never lifts. Now, of two integers, they mean what the standard says, whatever the library, in contracts and in code:

#include <algorithm>

int lower(int a, int b)
  cppverify::post(cppverify::result == std::min(a, b))
  cppverify::post(cppverify::result <= a && cppverify::result <= b)
{
  int m = std::min(a, b);
  return m;
}

long widened(int x)
  cppverify::post(cppverify::result >= 3)
{
  long w = std::max<long>(x, 3L);
  return w;
}

Verified: lower [backend=z3]
Verified: widened [backend=z3]

On the base (#81):

Unresolved: obligation lowering failed: lower (missing spec definition: fn_5f5a5374336d696e496945524b545f53325f53325f)
Unresolved: obligation lowering failed: widened (missing spec definition: fn_5f5a5374336d6178496c45524b545f53325f53325f)

Stacked on #81 (plan item A18, which the plan schedules with B2: lift constexpr template instantiations, or fail closed with a message that names the function).

Design

• A model, not a lift. The plan offered lifting the library's instantiation as any constexpr helper is lifted. But each library writes these functions its own way (libstdc++ with an if and two returns, under a concept-check macro), so a proof that lifted the library's code would rest on the platform's library, and a construct one library uses and the verifier does not support would cost that platform alone. The standard fixes their meaning instead ([alg.min.max]): for scalars, max(a, b) is a < b ? b : a and min(a, b) is b < a ? b : a. stdMinOrMax recognizes the two-argument std::min and std::max of a const reference to an integer, an enumeration, or bool (not the comparison or initializer-list overloads, nor a class with its own operator<), and convertMinOrMax lowers a call to a VConditionalExpr over the arguments, read once each, before the call would become a spec application; it has no definedness condition of its own. A reference bound to the result fails closed, as any reference to a call result does.
• The rest of the standard library is not lifted for the same reason: a non-constant call of any other of its constexpr functions (std::clamp) is an error naming it, std::clamp is not modeled: of the standard library, the verifier knows std::min and std::max of two integers.
• References to const scalars in lifted helpers. The same shape in a user's helper, constexpr const T &larger(const T &a, const T &b), could not be lifted (unsupported C++ type in verification: const int &). A spec is a function of values, and a reference to a const integer, which the helper only reads, stands for the value it refers to, as a parameter and as the result (constScalarReferent; the parameters in ValueReferences are read as values, not loaded). A reference the helper could write through (int &) is still unsupported.
• Helpers that cannot be lifted are named. A failed lift returned nothing, so its users' lowering ended missing spec definition: fn_<hex>; and a helper reading memory through a pointer failed silently. convertConstexprSpec now returns a placeholder that the lifting loop marks unsupported, reporting why at the helper, so the driver's existing check names it in each verdict that relies on it: Unresolved: reads [reason=construct.unsupported] (relies on first, which uses a construct the verifier does not support).

Tests

suite/std_min_max.cpp (Z3, with a check that no proof is vacuous): std::max and std::min in contracts and in code, in an expression, with an explicit template argument, of unsigned long and of an enumeration, and in a spec; a wrong use that fails with a counterexample; std::clamp, std::max of a class with its own operator<, and a reference bound to std::max's result, each an error; a user's constexpr const T & helper lifted and verified; a helper reading through a pointer and one taking int &, each named in its user's verdict.

The test fails on the base: every function using std::min or std::max ends missing spec definition, std::clamp too, and mymax<int> is unsupported C++ type in verification: const int & with its user missing spec definition.

Mutants, each built on an assertions build and run on std_min_max.cpp, function_templates.cpp, z3_calls_fail_closed.cpp, and verify_constexpr_spec_e2e.cpp: 8 of 8 killed.

Mutant	Killed by
no model	std_min_max
min and max swapped	std_min_max (clamp3, wrong)
classes modeled too	std_min_max (newer)
other standard functions not reported	std_min_max (clamped)
const reference parameters read through memory	std_min_max (mine)
references to const integers not values	std_min_max (mymax<int>)
a helper that cannot be lifted dropped	std_min_max (reads, bumps)
references to non-const integers values too	std_min_max (bumped)

Docs

• functions-loops.rst: const references in lifted helpers; std::min and std::max, a checked example; what changed.
• limitations.rst: the standard library's modeled functions. Release notes: "std::min and std::max".
• DESIGN.md: the model and value references. ARCHITECTURE.md: stdMinOrMax, convertMinOrMax, unlifted helpers.

Checked

• The Verify suite on a release build: 468 passed (the exhaustive decoder filtered out), 1231 s with 40 workers.
• The doc pages' examples (functions-loops, limitations, release notes, DESIGN, ARCHITECTURE): 34 checked, 0 failed; docs_examples.test and docs_coverage.test pass in the suite; the site builds with warnings as errors.