[SwayamInSync]

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

Every spec function of a Lean project is opaque cppSpec_f : .... A goal knows f only through the definition instances it states, the finite fuel levels the solver got, so a goal that needs f at another argument, or induction over f, cannot be proved in Lean. On main, for

cppverify::spec int tri(int n)
  cppverify::decreases(n)
{
  return n <= 0 ? 0 : tri(n - 1) + n;
}

cppverify::proof void tri_nonneg(int n) cppverify::post(tri(n) >= 0) {}
cppverify::proof void tri_four() cppverify::post(tri(4) == 10) {}

Specs.lean has opaque cppSpec_fn_5f5a3374726969 : Int -> Int, and neither postcondition can be proved: tri(4) is given one level (tri 4 = tri 3 + 4), and nothing is known of tri at an unknown n. Z3 proves both: the first by its unfolding of tri(4), the second by its automatic induction.

Now tri is a definition, cppverify_auto evaluates tri(4), and tri_nonneg takes a proof by induction with cppSpec_fn_5f5a3374726969.induct.

Design

Decided for 0.2: a real definition when Lean proves termination, opaque otherwise.

• References. Vermilion (read as data) emits every spec fn as a def with termination_by and a decreasing_by ladder, but wraps a recursive body in if 0 ≤ measure then body else default. Where the measure is negative and the body does not recurse, that changes the value; our research flagged it. Lean 4.35 (tested): a recursive call must be reached through a dependent if or a binder whose hypothesis proves the decrease. Under a ∧ f x or a ∨ f x, a is not a hypothesis. Lean generates f.induct.

• The definition is the canonical step definition (leanSpecDefinition), printed with applications of the recursion by name and no let temporaries, since a hoisted application would lose its guard. Every condition that reaches an application is a hypothesis there:

  • if becomes if _h : c;
  • a ∧ b becomes if _h : a then b else False, a ∨ b becomes if _h : a then True else b, and ¬a ∨ b becomes if _h : a then b else True, when b applies a spec;
  • a bounded existential over one guards its body by its range;
  • a universal's range is already its antecedent.

  Each rewrite is a classical equivalence, so the definition has the spec's value at every argument; it is never guarded by the measure as a whole.

• The measure is termination_by ((m1 + 1).toNat, ...) from the spec's decreases. With upper >= 0 && lower < upper, (lower + 1).toNat < (upper + 1).toNat even for lower = -1 (down(n) = n < 0 ? 0 : down(n - 1) + 1), and equal components stay equal. That is the relation the termination check proves, lexicographic.

• Proving the decrease: decreasing_by all_goals cppverify_decreasing, a prelude macro that tries simp_wf; omega, then with the collection and comparison wrappers unfolded, then with cppIntDiv and cppIntRem unfolded and their conditions split (a measure that falls by a constant divisor, log2(n / 2), which omega does not see through cppIntDiv), then simp_all; omega, then decreasing_tactic.

• Groups: strongly connected components of the applications (Tarjan, callees first), each one mutual block, all definitions or all opaque.

• The trial (leanSpecsText, tryLeanSpecs) runs at export: one Lean file importing Auto, the groups in order, #cppverify_axioms after each member. A definition Lean rejects is added with sorryAx (tested), or not at all. A group's verdict is kept only when each callee tried in the same round was accepted; otherwise it is tried again with the rejected callee opaque, until nothing changes.

• The cache: verdicts live in .cppverify/specs/<sha256>, keyed by the toolchain, LeanSpecRevision, the group's text, and what each callee is, so Specs.lean is the same on every run. Without Lean, undecided groups are opaque and nothing is kept. The scratch-pad stays opaque, as does archive replay, whose modules carry no measures.

• Goals and names do not change. A goal states the same definition instances, which a definition makes theorems.

• Verdicts still rest on the termination cpp-verify establishes. In the test, half's own check (combined with an unproved postcondition) is unresolved while Lean accepts its definition, and everything relying on it stays spec.termination. Letting Lean's acceptance establish that fact is left open.

• cppverify_auto revision 3 appends _eval: it rewrites with the equations of every spec CppVerify.Specs defines, and with cppIntDiv and cppIntRem, which closes a goal at known arguments. Then _div: grind [cppIntDiv, cppIntRem], for a contract that divides by a constant (a / 2 >= 2 for a >= 4), which needs no spec definition. A spec's own termination goal states the decrease its definition's decreasing_by proves, so log2's is proved the same way. Both come after every other step, so a goal an earlier step proves keeps its proof.

Measured

Every source of the suite exported with this branch (375 sources, 9259 goals), each goal tried by revision 2 (a replica of its steps) and by revision 3:

	revision 2	revision 3
the 5582 goals Z3 proves	5210 (93.3%)	5301 (95.0%)
all 9259 goals	8078	8194
goals neither proves, mean time	3.1 s	4.4 s

None is proved by revision 2 and not by revision 3. The replica of revision 2 gives exactly LS2's figures on LS2's exports (5210), so the definitions change no goal an earlier step proved. In the five sources with the most new proofs, 48 of their 61 are _div's (pointer differences divide by the element size; binary search halves an interval) and 13 _eval's (the factorial constants of mvp_factorial.cpp).

The trial makes 213 of the suite's 293 spec functions definitions. Of the 80 opaque: 69 have no definition to try (20 choose, 47 heights and witnesses of inductive predicates, 2 unspecified); 11 do not terminate (diverge, loop, loopy, swing, loops, sum_diverges, diverges_at_one) or terminate only by their own postcondition (g, m91, nested) or a choice's axiom (pick). The census found three that terminate by C++ division (span_sum, log2, log2_below), which the first ladder missed since omega does not see through cppIntDiv; the division rung of cppverify_decreasing and _div come from that.

Tests

suite/lean_spec_definitions.test, on:

• tri; even/odd (mutual, calls under || and &&); ack (lexicographic); half;
• steps, whose termination rests on half's postcondition: Lean rejects it, and it stays opaque;
• count_steps, which calls steps: rejected in the first round through steps' rejected definition, accepted against the opaque one;
• down, whose call has measure -1 where its caller's is 0;
• log2, whose measure falls by C++ division, and log2_eight (log2(8) == 3), proved by _eval;
• reaches, with a call under a bounded existential.

It checks:

• each definition's text and the opaque one;
• that a rerun tries nothing and writes no file;
• tri_four, even_four, small_ack, log2_eight proved by cppverify_auto, and tri_nonneg by a proof by induction (Inputs/lean_spec_definitions_tri_nonneg.lean), all Certified;
• count_steps still spec.termination through half;
• that without Lean every spec is opaque.

suite/lean_division.test: two contracts that divide by constants, proved by _div and Certified.

Updated: lean_modules.test and lean_collections.test expect definitions in Specs.lean; lean_automation.test and lean_collections.test expect revision 3. lean_fallback.test now runs with --no-lean-auto: the new step certifies fibo_six too, and the test is about fallback projects and their proofs, so its expectations are main's again.

Docs

• ch17: a new section, "Spec functions in Lean", with a checked example, the definition, the trial, and a proof by induction. Also: the Specs.lean description, the collections section (induction over total), and cppverify_auto's steps and revision.
• tooling.rst: --lean-project's specs.
• Release notes: "Spec functions as Lean definitions".
• DESIGN.md, ARCHITECTURE.md: the design above.

Checked

• lean_spec_definitions.test and lean_division.test fail on main (no definitions; no _div step).
• Mutants, each killed: every spec opaque; every candidate taken untried; conditions not hypotheses; a conjunction not a condition; a disjunction not a condition; an existential's range not a condition; a measure without its one; verdicts not kept; a verdict kept though a callee was rejected; no evaluation step; no division in the decreasing ladder; evaluation without division; no division step.
• Every lit test that runs Lean or names a Lean option (44) and docs_examples.test (34 examples, 0 failed): all pass. VerifyTests: 62 passed, 1 skipped (the parity test, which needs archives).
• git clang-format clean.