[SwayamInSync]

Stacked on #66 (LS3, on #65, #62, and #63), whose commits show here until they merge; merge after #66. The runs quoted below as on main (with LS3) are on #66's branch.

An obligation archive reached Lean only as the unchecked scratch-pad: --obligation-in rejected --lean-project, --lean-certify, and automation, and every Lean path rejected a bounded (BMC) module. Archives also dropped what a project needs: spec measures (so every replayed spec was opaque, LS3) and where each assumption of a goal comes from (so a replayed readable goal named no hypothesis, and a proof written for the source did not build). On main (with LS3), for suite/Inputs/lean_replay.cpp:

$ cpp-verify --obligation-in=a.cpv --lean-project=rep
error: archive replay supports Lean scratch-pad export with --lean-out, not Lean project generation or certification
$ cpp-verify --obligation-in=b.cpv --backend=lean --lean-out=b.lean      # b.cpv from --backend=bmc --unroll=3
error: Lean scratch export cannot replay a BMC-transformed obligation archive

Now the replayed project has the goals, Specs.lean, and proof files of a source run (diff -r empty), the proof of tri_nonneg by induction written for the source certifies the archive's goal, and a bounded module states its bound and aggregates as BMC does.

Design

Decided for 0.2 (LS6): archive replay and BMC provenance in Lean.

• References. Frama-C WP sessions and Why3 replay keep proofs by goal, independent of how the goals were produced; Vermilion (read as data) keeps proofs by statement hash. LM3 already names goals by obligationStatementHash and their group (function name and a hash of its identity), both archived, so the same obligation has the same goal name and proof file from source or archive. What was missing was the producer path and two pieces of data.
• One owner of Lean projects. The project code moves out of Verifier into LeanProject (initialize, write modules and the spec trial, finalize with moves and quarantine, automation, certification), which collects warnings instead of pushing diagnostics. Source verification and verify::replayLeanProject both drive it; there is no second implementation. The move is verbatim apart from the warnings and the automation count, and the 12 lean_*.test pass unchanged on it.
• Replay results. Replay checks each module alone, as with a solver: a module whose goals all certify is Proved obligations ... [backend=lean] (status Verified in replay, JSON proved-obligations), never Certified, which would claim the dependency fixpoint. Automation, moving and keeping proofs, --lean-prune-stale, and --jobs work as in source mode; --lean-fallback stays source-only.
• Schema v3 (cppverify.obligation/3, reads v1 and v2):
  • each logical function's Decreases, validated like its definition (integer terms over its parameters, every call resolved, every variable in scope), never hashed: a measure changes no meaning (Lean checks termination itself; an induction descends by a well-founded relation whatever the measure);
  • with source metadata, LogicExpr::Premise on each Or (where an assumption comes from), which names a readable goal's hypothesis, never hashed.
• Canonicalization keeps a measure's callees. A declaration depends on what its definition and its measures apply; before, a spec only a measure applied was removed, so the measure could not be printed (or validated). This changes the module hash of a module whose specs' measures apply other specs; per-obligation hashes and proof-cache keys do not change.
• Bounded modules. Lean accepts them in scratch and project mode. The goals of each state the bound (/- bound: N loop iterations, by unrolling: ... -/), and LeanProjectGoal::Unwinding marks the unwinding goals. Every goal certified, unwinding included, is Proved obligations ... [backend=lean, bound=N]; every goal but some unwinding goal certified is BoundedSafe (bmc.incomplete-bound). Lean proves and never refutes, so a Lean BoundedSafe says the unwinding is not certified, not that it fails; what BoundedSafe claims, that no execution within the bound fails, is exactly what the safety goals state. Unresolving it instead would leave Lean no bounded verdict for the modules BMC exists for, whose unwinding fails. Goal names stay statement names: an identical statement is the same theorem at any bound.

Found while writing it: a spec whose measure applies another spec (decreases(size(n))) was never even a candidate for a Lean definition, since its module had dropped size. With this PR it is tried; cppverify_decreasing does not unfold size, so Lean still rejects it (noted as open in the LS3 design note).

Tests

suite/lean_replay.test, on Inputs/lean_replay.cpp (tri, tri_nonneg, size/down, inc) and Inputs/lean_replay_loops.cpp (sum_small, count_up):

• source and replay projects: diff -r of Goals/, Specs.lean, and Proofs/ empty; tri defined, size kept for down's measure; inc's readable goal names h_pre_1;
• the source's induction proof of tri_nonneg certifies the replay: Proved obligations for every module; JSON lean_automatic;
• a v2 record (mutate_obligation_archive.py schema-v2): tri opaque, no h_pre;
• bounded: the scratch-pad states both bounds and the unwinding kind; certification gives Proved obligations: sum_small [backend=lean, bound=2] and lean_replay_loops.cpp:19:3: BoundedSafe: count_up (every goal is certified but the unwinding: ...) [backend=lean, bound=3] [reason=bmc.incomplete-bound];
• a replay that drops a goal keeps the edited proof in Stale/ with its warning, and one that brings the goal back takes the proof back, its warning a JSON record in a JSON run (as source runs print warnings);
• option errors.

Updated: obligation_archive.test (version 3 accepted, 4 rejected; a v2 record replays; a measure with a free variable is rejected), obligation_ir.cpp (schema name), Inputs/mutate_obligation_archive.py (schema 3: measures and premises; schema-v2, measure-free-variable).

Mutants, each killed (13 of 13): measures not archived; premises not archived; measures not read; schema 2 read with measures; measure callees not kept; measures not validated; no bound with the goals; unwinding goals not marked; bounded safety not reported; replay never certified; replay counts no automatic proof; bounded modules solved under Lean; project warnings dropped.

Docs

• ch17: "Archives in a Lean project", with the replay and bounded outputs and a checked example of the two loops; the archive section's schema v3, canonicalization, and BMC paragraphs.
• tooling.rst: --obligation-in's Lean projects; schema v3; what hashes omit.
• Release notes: "Lean projects from archives"; data formats.
• DESIGN.md, ARCHITECTURE.md: the design above.

Checked

• lean_replay.test fails on LS3 (replay into a project is an error there).
• The whole Verify lit suite but the exhaustive uleb128 file: 445 tests, all pass. VerifyTests: 62 passed, 1 skipped (the parity test, which needs archives).
• Verdict differential against LS3 over the 413 suite sources (--diagnostics-format=json, one job each): 0 files with different results, 0 with a time change (1295 s, 1285 s).
• Replay differential: the 359 archives LS3 writes (schema 2), replayed by LS3 and by this branch: 0 changes (1222 proved-obligations, 496 failed, 82 unresolved).
• git clang-format clean.