[SwayamInSync]

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

The Lean backend refuses every function that uses a spec collection. On main, --backend=lean on a file of a proof function over each kind:

Unresolved: sequences [backend=lean] [reason=logic.unsupported] (backend 'lean' does not support required logic features: sequences)
Unresolved: sets [backend=lean] [reason=logic.unsupported] (backend 'lean' does not support required logic features: collections)
Unresolved: multisets [backend=lean] [reason=logic.unsupported] (backend 'lean' does not support required logic features: collections)
Unresolved: maps [backend=lean] [reason=logic.unsupported] (backend 'lean' does not support required logic features: collections)

Now each is exported, cppverify_auto proves its goals, and certification gives Certified.

Design

Representation. Core Lean types, with Mathlib left opt-in as decided for 0.2:

<cppverify.h>	Lean
seq	List Int
set	Int → Bool, its membership test
multiset	Int → Nat, its counts
map	Int → Option Int, the value at each key it holds

• A set is its membership test, not a finite set, since a set of <cppverify.h> may be infinite. Vermilion's mirror of vstd (read as data) uses Mathlib's Finset and Multiset, which fit vstd's finite sets but not ours.
• Every observation is decidable, so decide evaluates membership, counts, reads, and sequence equality at constants. Equality of sets, multisets, and maps is equality of functions.

Operations. Each is a prelude function (LeanCollectionPrelude): cppSeqEmpty, cppSeqUnit, cppSeqLength, cppSeqAt, cppSeqPush, cppSeqConcat, cppSeqSubrange, cppSeqContains, cppSet*, cppMultiset*, cppMap*. Each has the certifier's total semantics (Certify.cpp):

• a read outside a sequence, or outside a map's domain, is 0;
• a subrange is S[From..To), with From = max 0 (min lo len) and To = max From (min hi len);
• a multiset removal of a count of 0 leaves 0, by Nat subtraction.

update and reverse stay specs over these, as for the solvers.

Membership. The three membership predicates are defs with Decidable instances. A first version made them abbrevs, so that instance search would see s x = true. But then cppverify_norm's Boolean simp lemmas rewrote cppSetContains s x to s x = true, and no lemma stated on cppSetContains matched any more.

Lemmas. As Vermilion states each vstd operation for its ladder, the prelude states each operation's meaning in @[simp, grind =] lemmas, all proved in core Lean 4.35:

• cppSeqAt_push, _concat, _subrange, _unit; cppSeqLength_*; cppSeqContains_push, _concat, _unit;
• cppSeqSubrange_all, _push, _concat_left, _concat_right;
• cppSetContains_*, cppSetSubset_iff, cppMultisetCount_*, cppMapContains_*, cppMapGet_*;
• extensionality: cppSeq_ext, cppSet_ext, cppMultiset_ext, cppMap_ext.

Lengths and counts are not negative, stated through grind_pattern. With a plain @[grind], grind took the normalized inequality -1 * count m x ≤ 0 as the pattern, which no goal contains.

Automation. cppverify_auto revision 2 appends three steps after the five of revision 1, so that every goal an earlier step proves keeps its proof. They come from probing candidate steps on every collection goal of the suite:

• cppverify_auto_bveq: equalities of machine values, such as x != y for two keys, and sign extensions become integer facts too (← BitVec.toInt_inj, toInt_signExtend_of_le with omega for its side condition);
• cppverify_auto_ext: a collection equality is proved by the kind's extensionality lemma;
• cppverify_auto_unfold: the definition instances a goal states are unfolded by the bodies they name (cppSpecBody_…). A body names only lower levels of its definition, so the unfolding ends. Tagging the bodies for grind instead would have changed every earlier step.

A stub that revision 1 wrote is tried again, as LS1 designed for a new revision.

Measured over LS1's probe set (375 exported sources, 9259 goals), each ladder as cppverify_auto runs it, with a step budget of its own:

	revision 1	revision 2
goals Z3 proves (5582)	5044 (90.4%)	5210 (93.3%)
those over collections (112)	86	104
a goal it proved that the other did not	—	0 lost
mean time on a goal neither proves	1.4 s	2.8 s

• _bveq is not subsumed by _unfold. I ran each step alone on the 242 sources where revision 1 leaves a goal unproved. On 37 goals of roundtrip_uleb128 (llvm_uleb128.cpp), unfolding the lifted helpers' bodies exhausts the heartbeats, and _bveq proves them.
• What is left: most of the remaining collection goals need induction over a recursive spec (reverse, sums over concatenation). Lean knows a recursive spec only through the definition instances a goal states, so those wait for real spec definitions in Lean (LS3).

Tests

• suite/lean_collections.test exports a proof function over each kind and a recursive spec over a sequence and over a set. It checks:

  • the export: every true goal is automatic, and the false claim keeps a stub;
  • the declarations in Specs.lean: List Int -> Int and (Int → Bool) -> Int -> Int;
  • the prelude's definitions;
  • the goals' binders and terms;
  • certification of every true function, with a proof by hand of total(s.push(x)) == total(s) + x in place of its automatic one, and the false claim Unresolved;
  • the scratch-pad.

• CertifyTest.AgreesWithLeanEvaluation gains collections:

  • 80 random chains of operations, read by length, index, membership, count, and key;
  • 20 sequence equalities;
  • each operation where it matters: every clamp of a subrange of [1, 2, 3] for lo, hi in [-1, 4], reads at -1 and past the end, membership of an element inserted and removed, each combination of two sets, a multiset removal of a count of 0, 1, and 2, a key written over and removed.

  A first version had only the random chains, and printing set removal as insertion passed it.

• lean_automation.test, lean_modules.test: revision 2 in the headers. lean_modules.test's goals over tri are now automatic, and a rerun after its proofs by hand counts them as the user's.

• lean_toolchain.test (verify: Try cppverify_auto on each new Lean goal, and certify it faster #61's) is unchanged.

Docs

• ch17: a new section, "Collections in Lean", with the representation, the operations, the lemmas, a checked example, and a proof by hand. "Proofs cppverify_auto finds" now covers revision 2's steps and figures.
• ch13, limitations.rst, tooling.rst: collections in Lean.
• Release notes: "Collections in Lean".
• DESIGN.md, ARCHITECTURE.md: the design above.

Checked

• Lean tests: the 42 Verify tests that mention Lean, lean_collections.test among them, and the docs tests pass. VerifyTests: 62 passed, 1 skipped; AgreesWithLeanEvaluation takes 11 s.
• lean_fallback.test: fibo_step is now certified with no proof by hand. _unfold proves its postcondition from the definition instances the goal states. The test's certification failure and its JSON case now use fibo_six, whose postcondition still needs a proof.
• Docs: check-doc-examples.py passes on every page this changes (72 examples, 23 against the verdicts their pages show), the new checked export included.
• Mutation: 11 mutants, all killed:
  • collections unsupported again; the set sort printed without parentheses; set removal printed as insertion (killed by the unit test);
  • no _ext, no _bveq (killed by the check of the step that proves each goal), no _unfold; the revision not bumped;
  • no grind_pattern for counts; set membership as an abbrev; membership of a concatenation, or the subrange of a push, not stated as a lemma.
• On main: every function of Inputs/lean_collections.cpp is Unresolved with logic.unsupported, as quoted above.