[SwayamInSync]

Stacked on #67 (LS6, on #66, #65, #62, and #63), whose commits show here until they merge; merge after #67.

A counterexample the solver finds is a failure once cpp-verify's certifier has evaluated the goal at it, and nothing else checks it: no Lean user can see in their project that the goal is false, and the release gate's Lean row checks names, hashes, and replay, but no verdict, so a translation that made every goal true, or every goal false, would pass it. LM1 left exactly this for later.

Now a fallback project holds the refutation of each certified failure, which --lean-certify checks with the kernel. On the gate's matrix (Inputs/backend_fidelity_matrix.cpp), main prints the 12 failures as Z3 found them; this branch prints each one (confirmed in Lean), and the gate's new row requires Lean to certify every valid case and refute every invalid one.

Design

Decided for 0.2 (LM1, semantic agreement): replay certified counterexamples in Lean; a decisive Lean row in the fidelity gate.

• References. Why3 (Frama-C WP's prover layer) treats a prover's model as evidence only after its interpreter runs the program on it (check-ce); Isabelle's Quickcheck and Nitpick show a counterexample by evaluating the conjecture at concrete values; Dafny turns counterexamples into tests. Here the certifier is that evaluator for the solver, and Lean's kernel, evaluating the generated goal at the model, is a second one, independent of both. Vermilion (read as data) has no counterexamples in Lean.
• The values. Where the adapter attributes a certified counterexample to an obligation, it keeps the model's value of every free variable of that goal, read through the certifier's CandidateModel::constant, so they are the values it evaluated (counterexampleAssignment, VerifyResult::Assignment). It reads a copy of the model: Z3's evaluation with completion adds what it chooses to the model it evaluates, and the first version, reading the reported model, printed a value for every variable of a failing goal, also those the diagnostics leave unknown because the goal does not depend on them (MachineIntegerEncodingTest.IrrelevantVariablesStayUnknown caught it under the bit-vector encoding).
• The refutation (exportLeanRefutation): a module stating the failing goal and the bodies it unfolds as the project would (its specs join Specs, so the LS3 trial may define them), then theorem <goal>_refuted : ¬ <goal>: the goal applied to the values in the order it binds them (BitVec.ofInt; a heap or collection by its runs of equal cells as nested ifs), closed by cppverify_refute, whose evaluation also proves the definition instances the goal states as premises (they hold of the spec functions Lean defines).
• cppverify_refute (Auto.lean): decide; then evaluation by the bodies, the spec equations, memory reads, and machine comparisons, closed by decide or by grind with the heap definitions, since a store relation quantifies over every address. When both fail it tries to show the instance true, in a context without the goal (which would prove any instance of itself: the first version of this probe did, and turned pick_one into a false disagreement), and says why: Lean decides the goal true at the counterexample, or Lean cannot decide the goal.
• Budgets. Each attempt of cppverify_refute, and the probe, gets the heartbeats of a step of cppverify_auto (cppverify.autoBudget) and catches the runtime exceptions it raises (withinBudget, tryCatchRuntimeEx), as the steps of cppverify_auto do: running out of heartbeats or of recursion depth is a "no", and the next attempt starts with a budget of its own. The module lifts the heartbeat limit only for the goal's definitions (section Goal); the theorem keeps Lean's, which also bounds the kernel's check of the proof the attempts build (with set_option maxHeartbeats 1000, decide +kernel on a slow Nat recursion ends in (kernel) deterministic timeout). The first version had no limit at all, and the refutation of an inductive predicate at -5000 ran for over two hours.
• Only failures that stand. The refutations are reported once the verdicts settle: a counterexample checked with a spec's postcondition that is not established is no failure (spec.post), and nothing is said of its refutation.
• Bounded quantifiers over Int have no Decidable instance in core; the prelude decides one by trying each integer of its range (cppIntBallDecidable, cppIntBexDecidable, through core's Nat instances). forall(i, 0, 4, i < 3) needed it.
• Where: a fallback project, the mode where a solver runs beside Lean. CppVerify/Refutations/<group>/<goal>.lean, rewritten by every run, removed with its failure. Certification builds them with the proofs, and the checker takes them as refutation entries: the theorem must state exactly Not <goal> of the goal its own module defines, with Lean's foundations alone.
• Verdicts. A refutation that checks adds (confirmed in Lean) (JSON lean_refuted). One Lean cannot decide (a goal applying a cppverify::choose, which is opaque in Lean) leaves the failure as it was, with a warning. One Lean decides true would be two evaluators of one goal disagreeing: the function is Unresolved, backend.inconsistent-results, as when two solvers disagree, never Failed.
• The gate's Lean row: a project certifies the 16 valid cases and hidden_spec_true (which Z3 leaves spec.hidden, and which Lean sees the definition of), with one proof by hand, Inputs/backend_fidelity_proofs, for the postcondition of heap_spec_read, the one goal cppverify_auto does not prove; a fallback project confirms the counterexample of all 12 invalid ones.

Measured

Every Verify source (468 files, the exhaustive decoder left out), each run with --lean-fallback=DIR --lean-certify and one job: 622 certified failures in 226 files. Each refutation module builds, and none is a disagreement.

• 460 confirmed in Lean (74%).
• 98 with the warning that Lean cannot decide the goal:
  • most in programs with dynamic or local storage, or pointers into objects (dynamic_storage_fail.cpp 18, local_array_lowering.cpp 13, reference_local_object_lowering.cpp 6, modular_ownership_fail.cpp 5, and others). Their goals chain stores into the allocation memories, each an equation between functions over every address (h' = fun q => ...), which Lean settles only by extensionality; decide cannot, and grind does not within a step's heartbeats.
  • 9 apply a cppverify::choose, opaque in Lean (choose_axioms.cpp 5, choose_identity.cpp 4), and the rest apply an inductive predicate, quantify over a large range or all integers, or read collections.
  • One by design: below_a_billion of the test's input.
• 64 without a refutation. They are failures of modules a fallback project does not hold, and they keep their solver failure as before: contract well-formedness checks (contract of f) and checks of spec functions (termination, postconditions, their inductions, reads).

The whole run takes 4466 s of single-job time.

Memory

The first push of this PR shut down CI's 16 GB Linux runners 22 to 28 minutes into check-clang (exit 143), as #69's did after it. lean_refutation.test peaked at 56 GB: compiling the refutation of below_a_billion, forall(i, 0, 1000000000, i < 999999999), one Lean process reached 58.6 GB before failing with maximum recursion depth has been reached. The prelude's cppIntBallDecidable reduces a range of integers to core's Nat.decidableBallLT, one level of recursion per integer, and the generated files allow a depth of 100000. Heartbeats do not count that memory: under a step's 50000 heartbeats, a range of 1000 is decided in 1.9 GB, one of 4000 runs out of heartbeats at 2.7 GB, one of 16000 at 16.1 GB, and one of 64000 reaches the depth limit at 58.7 GB. Lean's -M limit does not bound it either: it is checked only at the interpreter's checkpoints, and the process aborted with an uncaught memory_exception at 58.7 GB.

The prelude now tries each integer of a range of at most 4096, as many as the certifier expands (CertifyLimits::DirectExpansion), and gives a larger range the classical instance, which decide cannot evaluate. lean_refutation.test now peaks at 4.0 GB (the other Lean tests: 2.8 to 3.8 GB), and below_a_billion stays undecided at once. No refutation is lost: none over more than about 4000 integers fit a step's heartbeats before. Four in certified_quantifier_ranges.cpp used to stop Lean at the recursion limit and stay undecided; with decide failing at once, cppverify_evaluate reaches grind, which proves them, and the file takes 34 s instead of 354 s.

lean_refutation_memory.test (Linux) runs the budget input under peak_memory.py: its largest process must stay below 4096 MB, and below_a_thousand, a range of 1000, must still be confirmed. Mutants: without the bound it fails at 58 GB, and with a bound of 100 the thousand is no longer confirmed (both killed).

Assertions build

The second push's Linux assertions job failed lean_toolchain.test: with a lake that fails, certification failed and the driver aborted with Expected<T> must be checked before access or destruction. The driver took the error of certifyLeanProject's result, then, choosing what the refutations rest on, tested the result again, and an Expected holding an error that is tested again is unchecked once more. Archive replay (#67) made the same second test of its result, which no test reached. Both now move the result into an std::optional once. lean_toolchain.test also replays an archive into a project with that lake and checks the failed certification is a verdict; on an assertions build with replay's old code it aborts.

Tests

suite/lean_refutation.test, on Inputs/lean_refutation.cpp:

• a contract (add_one), a bounded quantifier (below_three), a store to memory (zero_first), and a spec Lean defines (tri_three): each (confirmed in Lean); pick_one, whose goal applies a choice: a failure, with the warning;
• the refutation's text; JSON lean_refuted and the warning record;
• a failure that is gone takes its refutation with it;
• the checker rejects a refutation module whose theorem does not state the negation of its goal (proves True, not Not ...);
• cppverify_refute on an instance that holds says Lean decides it true, and on one over every integer that Lean cannot decide it (Inputs/lean_refutation_tactic.lean);
• the refutation's text lifts the heartbeat limit inside section Goal only;
• Inputs/lean_refutation_budget.cpp: below_a_billion (forall(i, 0, 1000000000, i < 999999999)), which Lean would decide by trying a billion integers, ends undecided with the warning; far, whose counterexample rests on a postcondition of ge that is not established, is Unresolved (spec.post), and nothing is said of its refutation.

suite/backend_fidelity_gate.test: the new row, PASS: decisive Lean verdicts: valid cases certified, counterexamples refuted.

Mutants, each built and run on lean_refutation.test and backend_fidelity_gate.test (the last three on lean_refutation.test): on the final code 19 of 21 are killed; a 22nd mutated a step that is now gone. A first run of the three budget mutants reported all three surviving: llvm-lit --timeout fails at once without Python's psutil, and the script read the missing failure as a survivor; they ran again under coreutils' timeout.

Mutant	Killed by
no assignment from an obligation's query	both
an assignment without its values (counterexampleAssignment keeps none)	both
heaps print their default only	both
machine integers print as zero	both
a refutation's statement not checked (the checker accepts any type)	lean_refutation
refutations not written	both
stale refutations kept	lean_refutation
refutations not certified	lean_refutation
confirmation not reported	lean_refutation
no lean_refuted in JSON	both
bounded quantifiers undecided (no prelude instances)	both
no heap evaluation (decide in place of grind)	both
evaluation without spec definitions	both
no refutation exported for a certified counterexample	both
a true instance said undecided	lean_refutation
the probe sees the goal (mkFreshExprMVar in the refutation's context)	lean_refutation
no definition instances (the separate step that proved them dropped)	survived; the step is gone
attempts without a budget (maxHeartbeats := 0 in withinBudget)	lean_refutation (timeout after 900 s)
refutations reported for verdicts that do not stand	lean_refutation
the refutation theorem with unlimited heartbeats	lean_refutation
no assignment from a whole query	survives
a disagreement taken for a failure	survives

• Two first-round survivors changed the design. With "no definition instances" (the refutation proved the definition instances a goal states in a separate step, and the mutant dropped that step) every test still passed, because the evaluation proves them anyway. The step is gone: the evaluation is the one place they are proved. With "evaluation without spec definitions", the first evaluation attempt survived having its spec equations removed, since a second attempt (the same with grind) evaluated them too. The two attempts are now one, cppverify_evaluate, closed by decide or grind, and the mutant is killed.
• "No assignment from a whole query": the assignment is also taken when a counterexample comes from the module's whole query, which races the obligations' own queries when workers are spare. Which query answers first depends on load, so no test can fix the path; the code is the same counterexampleAssignment call as the obligation path, which is killed.
• "A disagreement taken for a failure": it fires only when Lean decides a goal true at a counterexample the certifier evaluated false, which no input reaches unless one of the two evaluators is wrong. The tactic's side, reporting "Lean decides the goal true", is tested (Inputs/lean_refutation_tactic.lean); the verdict it leads to (Unresolved, backend.inconsistent-results) is the one two disagreeing solvers already get.
• lean_refutation_memory.test (Linux): the budget input's largest process stays below 4096 MB, and a quantifier over a thousand integers is still refuted.

Docs

• ch17: "Counterexamples in Lean", with a checked example and its refutation; the fallback paragraph.
• tooling.rst: --lean-fallback's refutations.
• Release notes: "Counterexamples confirmed in Lean".
• DESIGN.md, ARCHITECTURE.md: the design above, and the gate's Lean row.

Checked

• The 47 Verify tests that mention Lean (outside Inputs/), docs_coverage.test, and docs_examples.test pass (564 s, 16 workers), on the branch with the budgets.
• With the range bound: every Lean test, the release gate, and docs_examples.test pass (30 tests, 481 s, 16 workers), and the suite-wide run under Measured is with that binary.
• With the certification fix, on an assertions build: the 29 Lean tests and the gate pass.