[SwayamInSync]

A contract is C++, evaluated where the function is called and where it returns, as C++26 evaluates contracts. On main nothing checks that it is defined there:

Clause	main
a precondition that divides first: pre(a / b == 0)	Verified; only a verified caller checks the division, at its call
a precondition that dereferences first: pre(*p > 0)	Verified
a precondition that reads before it bounds: pre(valid(p, 8) && p[i] == 3)	Verified; a caller passing i = 8 is Verified too
a postcondition that reads past an extent: post(p[i] == old(p[i])), i <= 8	Verified; the same read in the body fails
a loop invariant or cppverify::check that reads past an extent	Verified
a trusted postcondition that divides by its result: post(1000 / result > 0)	never checked

The last one is a wrong result. The logic defines what C++ leaves undefined (x / 0 is 0), so the trusted contract read as excluding a result of 0, and a caller that divided by that result verified:

[[cppverify::trusted]] int read_sensor(int channel)
  cppverify::post(1000 / cppverify::result > 0);

int scaled(int channel)
  cppverify::post(cppverify::result > 0)
{
  int r = read_sensor(channel);
  return 1000 / r;            // main: Verified [trusts=read_sensor]
}

Now:

defined.cpp:2:17: error: verification failed: contract of read_sensor [...::contract::division-by-zero@2:17] (counterexample: result [ssa=__result_1] [type=i32] = 0)
Unresolved: scaled [backend=z3] [reason=callee.contract] (relies on the contract of read_sensor (its clauses are not shown to be defined), which is not established)

Design

How the references handle this:

• Dafny builds a well-formedness procedure for every method and function (CheckWellFormed$$f, BoogieGenerator.cs). It checks each requires and then assumes it, left to right, havocs the heap within modifies and the outputs, and checks each ensures in that state. &&, ==>, ||, and if guard what follows them. It is not rechecked at call sites.
• Verus makes spec code total and keeps partiality soft (recommends, checked after a failure).
• Frama-C: ACSL terms are total for WP; only E-ACSL, at run time, guards annotations.
• C++26 evaluates a contract predicate as C++, so an undefined one is undefined behavior.

This PR takes Dafny's procedure and C++26's meaning, and keeps Verus's totality for specs:

• Preconditions (Passivizer::contract): a module of its own per function, contract of f. The generated preconditions (pointer validity, separation, type invariants) are entry facts. Each written precondition, in order, gets the definedness checks its operations get in a body, and is then assumed. A clause is therefore checked where the clauses before it hold, and within a clause, where the operands of &&, ||, ?: before it allow.
• Postconditions of a verified body (run()): checked in the body's own final state, as C++26 and Verus do, each guarded by the postconditions before it, now with the memory checks too.
• Postconditions of a trusted function or one without a definition: in every state its frame allows, with any result. That is the state its callers assume, built by the same code: the frame part of emitCallStmt is factored into havocFootprints and footprintBytes, unchanged.
• Loop invariants and cppverify::check: the memory checks of the body.
• The checks: the core checks (collectSafety) and, with memory checking, the memory checks of the clause as written. instrumentUBChecks computes them before spec inlining, as it does for the body's accesses, and records them beside each written precondition and postcondition, each loop invariant, and each cppverify::check (VMemoryCheck). Cloning and loop unrolling copy them. A read under old is checked in the entry state, a quantifier's body at every value of its range, and in a pre- or postcondition every parameter is its entry value. In the object model an extent is its pointer's object, so the object checks cover it; a proof function, outside the object model, is checked against its extents. Passivization joins a clause's memory checks to its core checks, one obligation per kind.
• Why before inlining: checking the inlined clause got two things wrong. An inlined spec exposes its own reads, though a spec is total: post(result == cell(p, 7)) with a spec cell that reads p[i] failed at the read. And an inlined lifted helper repeats its arguments' reads under each of its guards: one postcondition of scan_uleb128_1 (llvm_uleb128_decoder_exhaustive.cpp) grew from 183 thousand to 4.1 million lines of passive program.
• As callers see it: the contract module runs on the interface version of the function (UB-instrumented, not spec-inlined), the one call sites use. A lifted constexpr helper's checks are then reported at its call (collectSafety anchors an unfolded helper's checks there).
• Verdicts: quiet when the check holds. A failure is an error at the operation; the contract then establishes nothing, so callers that rely on it are Unresolved with callee.contract, and the check is a producer of the contract fact in the cycle check. The function's own verdict is about its body and does not change. An unresolved check goes through --lean-fallback like any module; under BMC the check is solved by Z3, as spec checks are.
• Specs stay total (Verus, ACSL): no check of their own; recommends stays a warning.
• Lean's readable goals (verify: State each Lean goal as named hypotheses, with a bridge the kernel checks #59): in the contract's check, a clause assumed once it is shown defined is h_pre_<n> or h_post_<n>, and what holds of the state a function without a verified body returns in, its frame and its result, is h_ret_<n>. Without this every hypothesis of these goals was h_fact_<n>.

A trusted contract whose valid marker cannot be read was accepted silently; it is now reported, as it is for a definition.

A flaw in the Z3 race, which this exposed

CI's release job failed twice on certified_failure_attribution.cpp (--jobs=3), past its 20-second limit. Pinned to one core it took 60.33 s, against 0.67 s on main. The cause is in the race between a module's whole query and its obligations (verifyModuleDirect), not in this PR's checks:

• A module without logic functions gives its whole query a 500 ms slice of the budget.
• A model the whole query finds is checked before it is reported (certifyModel), and that check was capped by what was left of the slice. On a loaded core the search took about 460 ms, the check had 41 ms, and the model was left unchecked: no certified failure, so the race went on.
• The postcondition's own query, which this test makes slow on purpose, then ran to the 60 s timeout.
• This PR's three new bounds obligations in that file slow the whole query just enough to expose it.

The race's own comment says a model check has a budget of its own. Now it does: a whole query given a slice of the budget checks a model it finds with the time a check of the module's queries gets, half the module's timeout or --certify-timeout (Z3Encoder::setSearchSlice, solveQuery's Slice). The function's deadline still bounds it.

That was not all: the release job failed again (within_seconds: the command took longer than 20 s with --jobs=3). Reproduced on two loaded cores (taskset -c 2,3 with two busy loops on them): 61 s in each of five runs, against 0.9 s on main. Instrumented, the whole query's 500 ms slice ended unresolved at 581 ms; the 18 easy obligations were proved, the postcondition's ran to its 60 s timeout, and only then did the retry of the whole query, with the full budget, refute the function in 585 ms. On main the smaller query fits its slice even under load, so the order of the fallback never mattered there.

The slice exists to keep the obligations' time when they and the whole query share one worker. Racing, they do not, and the retry waited for them anyway. Now:

• a whole query its slice leaves unresolved is retried as one more task of the race, queued after the obligations: a free worker runs it beside them, and without one the function's own thread runs it after them, exactly as with one job;
• the obligations stop the whole query, or its retry, whenever they settle the module: when one fails, as when they prove all of it.

A first version ran the retry on the function's own thread before helping its group: the verdicts were the same, but loop_frames.cpp took 61 s against 1.3 s, since every worker held a retry while the obligations that would settle the functions waited in their queues; and without the second rule, a retry beside obligations that had already failed ran to its timeout. Measured with the final version, on two loaded cores: certified_failure_attribution.cpp takes 1.2 s with --jobs=3 and with --jobs=1.

The whole query's probe is bounded by work, not time

CI's assertions job then failed certified_failure_attribution.cpp with --jobs=1, past its 20 s limit (the macOS log was not available). Reproduced on an assertions build, on one core shared with two busy loops (taskset -c 0): Unresolved with solver.timeout after 121 s. A module without logic functions gave its whole query 500 ms. This one needs about 700 thousand Z3 resource units, which an assertions build does not do in 500 ms under load. With one job its obligations then ran, the postcondition among them, whose search does not end. More jobs hid it, since the retry then runs beside them. Where the probe stopped depended on the load and on the build.

Now the probe is a fixed amount of work, WholeProbeUnits: 6 million Z3 resource units (rlimit), with the module's timeout as its bound in time.

• Calibration, with an instrumented idle release build over the 413 test sources: 2622 probes decided within 500 ms. 99% of them took less than 200 thousand units; the most, 5.2 million, are the three of the UTF-8 case study. 18 probes did not decide.
• Choosing the failure to report, once the probe refutes the module: each obligation gets the probe's work (UnitsCap), as it had the probe's time before.
• Retry: a probe that its work bound stops is retried with the full budget, as before. One that its timeout stops already had the full budget, so it is not.
• Cost: a probe that does not decide now does its 6 million units: 0.5 to 3 s instead of 0.5 s, since those 18 do 1,900 to 13,000 units a millisecond. With more than one job, the obligations solved beside it stop it once they settle the module.

Measured:

• certified_failure_attribution.cpp on that loaded core: 7 s with --jobs=1 and with --jobs=3 (before: 121 s and 1.5 s). Idle: 2.3 s.
• Two mutants, both killed by the test's 20 s limit: a probe of 100 thousand units (60 s with --jobs=1), and the choice without the work cap (60 s with both).

Tests

suite/contract_wellformedness.cpp, three runs (Z3, --no-check-ub, BMC):

• Preconditions, each kind: division, dereference, an index past an extent, one object, a member array, a lifted helper's argument conversion, and a division inside a lifted helper (reported at the call). Each failing clause has a defined twin that is quiet.
• Order: clauses (ordered holds, reversed fails), ||, ?:, a quantifier's range (all_positive holds, one_more fails), behaviors.
• Postconditions of bodies: a read past the extent fails; a later clause is guarded by the earlier ones; a read under old is checked in the entry state (take); a parameter the body reassigns is its entry value (advance).
• Invariants and checks: a read at p[n] fails in each.
• Trusted and bodiless contracts: a division by the result, a dereference of a result that may be null, a frame that keeps *q (holds) and one that writes it (fails), a contract without a definition.
• Callers: demoted with the new message; a caller of a defined trusted contract verifies. A trusted contract whose valid marker cannot be read is an error, and its caller is demoted (main: Verified).
• Parameters at entry: a precondition, and a postcondition, reading p[2] (which is q[0]) are checked against p's own object, though the body reassigns p.
• Ghost code: a cppverify::check in a ghost block gets the memory checks too.
• The cycle rule: a contract is established by its function's proof and by its well-formedness check, so the check takes part in the cycle rule. A trusted lemma whose precondition is defined only through a spec's postcondition, which that postcondition's proof block uses, is proof.cycle (main: Verified); with measures that every use lowers (a cluster), both verify.
• Proof functions against their extents. Specs stay total: a spec division by zero in a precondition, and a postcondition applying a spec that reads outside the object, are quiet.
• --no-check-ub: core checks only, so second (one object) passes and at fails its dereference.
• BMC: a postcondition's and a check's memory checks survive unrolling; invariants, which BMC does not use, get none.

suite/lean_contract_certify.test (#60's certification): a trusted contract whose second precondition divides, and a caller. Its check is exported as contract of sensor; with proofs of its goal and the caller's, both are Certified (reading [trusts=sensor]); with the check's proof left a stub, the check is Unresolved and so is reading, with callee.contract.

suite/lean_readable.cpp: the trusted pick may write *p, so its postcondition 100 / *p > 0 may divide by zero. The test checks every hypothesis of that goal in order: h_entry_1, h_null_1, h_null_2, h_object_1, h_pre_1, h_ret_1 (the frame), h_ret_2 (the result's validity), h_post_1.

Existing tests whose contracts were undefined:

• dynamic_storage_fail.cpp: unsafe_forwarded_read's postcondition reads old(source[1]) through a one-object pointer. It now fails there instead of being demoted for its callee.
• certified_quantifier_ranges.cpp: its preconditions read p[i] up to two million through a one-object pointer. They now declare the extent, valid(p, n); every verdict the test checks is unchanged.
• Seven more functions, in five tests, now report a contract that is undefined, each correctly. The tests still check what they were written for, so they are unchanged: offset_precondition forms source + 1 with source possibly null; slen_bad, sound_quant_needs_nonalias_fail's f, and sound_store_changed_fail's f read s[n - 1], s[i], and p[2] through a one-object pointer; unsafe_difference_precondition forms p + (count + 1), past the end; missing_extent_pointer_forward forms p + 2 from one object; the trusted before forms result + 1 with a result that may be null.

Docs

• functions-loops.rst: a new section, "Contracts must be defined", with the checked example above, and how the check is exported and certified under Lean.
• ch18: "Contracts are C++ too", with a checked example.
• ch17: the hypothesis names of a contract's check.
• pointers.rst, limitations.rst, integers.rst, tooling.rst: contracts get the checks; the contract of f label and its obligation IDs.
• Release notes: an entry under "Wrong results fixed", and "Results that depended on load" under "Running cpp-verify".
• tooling.rst: the probe of a complete query is a fixed amount of solver work.
• DESIGN.md, ARCHITECTURE.md, UB-CHECKING.md: the design above.

Checked

Rebased onto main at f861d01 (with #46 and #49). The one conflict, in release-notes.rst, is #49's entry and this PR's "Results that depended on load" added at the same place; both are kept. Before that, on 62af455 (with #54, #55, #56, #58, #59, and #60). On this tree: the 39 Lean tests, contract_wellformedness.cpp, certified_failure_attribution.cpp, the docs tests, and the new lean_contract_certify.test pass. Earlier, on 85f0b90: The one conflict, in Passivize.cpp, is #59's label of each entry assumption: A32 skips the written preconditions there in the contract's check, so the label comes from the precondition's index.

• Verify lit suite: 438 passed on a release build, including the docs tests, with llvm_uleb128_decoder_exhaustive.cpp excluded (lit never runs it). Before this rebase, at 14a7383 with the race fix: 433 passed and 1 unsupported on an assertions build.

• VerifyTests: 62 passed, 1 skipped.

• certified_failure_attribution.cpp pinned to one core (taskset -c 0): passed five of five runs, 2.2 s each under lit.

• The race retry, on assertions builds of this branch before and after it: a verdict differential over 413 test sources with --jobs=4 (the exhaustive ULEB128 file left out, as lit does): no verdict differs; total 742 s → 568 s, llvm_uleb128.cpp 129 s → 56 s, no file slower. The 21 tests that pass --jobs above 1 pass. On two loaded cores, certified_failure_attribution.cpp takes 1.2 s with --jobs=3 and with --jobs=1 (61 s and 1.3 s before).

• The work-bounded probe, on assertions builds of this branch before the race fix and with the probe: a verdict differential over the 413 test sources with --jobs=4 and with --jobs=1. No verdict differs. With --jobs=4, the total is 729 s → 561 s, and llvm_uleb128.cpp 127 s → 52 s (the race fix). With --jobs=1, 1321 s → 1331 s; loop_frames.cpp 3.6 s → 8.8 s, since its five failing functions each spend 1.4 s on a probe that never decides. On the same build, lit runs the 25 tests that pass --jobs above 1 or that this PR adds or changes: all pass.

• On main: each of the three RUN lines of contract_wellformedness.cpp fails.

• Verdict differential against main (573c171 plus verify: Bound pointers into a record by the array, field, or record they point into #53, before the rebase): 440 test sources. Verdicts differ in the new test, in verify: Bound pointers into a record by the array, field, or record they point into #53's subobject_pointers.cpp, in the six tests above whose contracts are undefined (dynamic_storage_fail.cpp and the five with the seven functions), and in the exhaustive file below. Total time 3536 s → 3732 s. Nearly all of it is llvm_uleb128_decoder_exhaustive.cpp (UNSUPPORTED, which lit never runs): 1601 s → 1875 s run alone, and its decode_uleb128_length_10 and _11 reach the timeout. Each has about 12 new bounds checks, one per postcondition, of reads at constant indexes (buffer[3] in valid(buffer, 11)). Deciding such accesses without the solver is a separate item for the body and contracts alike. The case study llvm_uleb128.cpp takes 311 s against 330 s. inductive_rules.cpp showed one 33 s run in the differential, a load stall that main shows too (one 34 s run in 16 parallel runs).

• Mutation: 29 mutants; 28 are killed by the tests:

  • preconditions unchecked, not assumed after their check, or all assumed at entry;
  • recorded memory checks ignored, unrecorded for preconditions, for checks in ghost code, or computed after spec inlining;
  • checks dropped by cloning or by loop unrolling;
  • body postconditions without memory checks; checks and invariants without them;
  • a read under old checked in the final state; quantifier bodies unchecked; proof functions unchecked against their extents; a clause's parameters taken as reassigned;
  • external contracts' postconditions unchecked; their post-state writing the whole heap, or keeping it; result validity not assumed;
  • a lifted helper's checks reported inside it;
  • the check skipped for bodied or external contracts; success printed; an undefined contract still established; the check not a producer of the contract fact; the message not naming the cause; an unreadable marker on a trusted contract accepted.

  The surviving mutant drops the guard that checks a body's postcondition where the ones before it hold. It is equivalent for verdicts: only the first failure in source order is reported, and a later clause's failure under a failing earlier one is never that.

• Readable-goal labels: four mutants, all killed by lean_readable.cpp: no pre, ret, or post label in the contract's check, and an entry assumption labeled by its position among the entry assumptions rather than among the preconditions (which names the extent's fact h_pre_1).

• Docs: check-doc-examples.py passes on every page this changes (74 examples, 25 against the verdicts their pages show).

• Merges: clean with verify: Send crash reports to cpp-verify's issue tracker #46, docs: Publish the documentation of each release, and of main at /dev/ #49, verify: Print Lean goals that mean what their obligations mean #54, verify: Settle what a Lean proof rests on, as a solver's, after certifying it first #55, and verify: Pin Lean 4.35.0, move projects 0.1 pinned, and certify with the pinned toolchain #56. It conflicts with verify: Bound what a run builds and what its solvers allocate #48 in Passivize.cpp: this moves the end of Passivizer::run() into finish(), shared with the contract check, so verify: Bound what a run builds and what its solvers allocate #48's NodeBudget check of the spec facts belongs in finish() (with no return P;), where the contract check gets it too. Whichever lands second takes that resolution.