[SwayamInSync]

A Lean project named each goal by its position: cppverify_one_fn_…_obligation_3_goal, the third obligation of one, its proof in Proofs/Goal_<md5 of that name>.lean, and each spec body by the position of its module in the file (cppSpecBody_m2_…). So a proof stayed with a number, not with what it proves:

Change to the source	main	Now
reorder two postconditions	each proof meets the other's goal; certification fails: Type mismatch: h has type r = BitVec.ofInt 32 1 but is expected to have type cppBvSle (BitVec.ofInt 32 0) r	every proof stays with its statement, no warning
insert a function before others	every later spec body is renamed (cppSpecBody_m2_ → m3_), and every proof that unfolds one stops building	spec bodies are named by their function and keep their names
rename a function	its goals get new names; its proofs stay behind, unused, and the new goals get sorry stubs	its proofs move with it, with the names they use rewritten, and a warning names each move
change a statement	the old proof meets the new goal	the old proof is kept in Stale/ with a note naming the new goal, and the goal gets a stub
remove a function	its proofs stay among the proof files	they are kept in Stale/, and come back when a goal has their statement again

Design

The research for this item (Frama-C WP's per-goal scripts, Vermilion's proof blocks keyed by the hash of their statement, Dafny's and Verus's caches) is in the plan's notes. This takes the identity from Vermilion and the file-per-goal layout from Frama-C, and adds what neither has: proofs follow a renamed function, and a proof is never lost.

• A goal is named by its statement. cppverify_<function>_<h6>_<kind>_<h8>: h6 hashes the function's identity (so overloads differ), h8 begins the SHA-256 hash of the obligation's statement. That hash, obligationStatementHash, covers the goal and the logical declarations it reaches, as the per-obligation semantic hash does, without the function's identity, so a renamed function's goals keep their hashes. Identical goals of one function get _2, _3 in source order. Spec bodies are cppSpecBody_<hash of the function identity>_….
• One proof file per goal, grouped per function: CppVerify/Proofs/<function>/<goal>.lean, starting with a header that records the goal, the stable obligation id, the full hash, the spec-body prefix, and the source. A proof written over its stub (with cp, say) gets the header on the next run.
• Every regeneration gives each goal the proof of its statement: the file at its path; else a proof recorded with its name, from Stale/ too; else a proof of the same statement whose goal is gone, from the function with proofs of the most of this function's goals, so two functions renamed at once each take back their own; else the 0.1 file of its 0.1 name; else a stub. A move rewrites the goal's name and the spec-body names throughout the proof text.
• Nothing of the user's is deleted. A proof no goal takes is moved to Stale/, with a note saying why: its statement changed (naming the goal of the changed obligation), its function has no obligation with that statement any more, or its function is gone. A stub cpp-verify wrote and nobody edited is removed. --lean-prune-stale deletes Stale/ on request.
• A fallback run examines only what its solver leaves unresolved. The exporter records every obligation of an exported function, those the solver proved too, and the driver records the functions it gave the solver. A proof of anything the run did not send to Lean stays where it is.
• 0.1 projects move to the new names. For each goal, the exporter also computes the name 0.1 gave it and the spec-body prefix 0.1 used. A 0.1 proof file is moved to its goal's new file with both rewritten, an unedited 0.1 stub silently. A 0.1 proof of a goal that is gone is kept in Stale/. Together with verify: Pin Lean 4.35.0, move projects 0.1 pinned, and certify with the pinned toolchain #56's pin migration, a 0.1 project certifies again without edits.

The header's source path is escaped as Lean comments need: Generated.lean already did that, but the first header did not, and a path containing /- opened a nested comment, so the proof file did not parse. The test runs from a directory named -src to keep that covered.

Tests

• New suite/lean_identity.test walks one project through every case. It checks the exact warnings and files at each step, and certifies after the renames, after the return, and after the migration:
  • export, then proofs copied over the stubs: they get their headers, and nothing moves;
  • a function inserted before the others, with two postconditions reordered: no warning, and the spec bodies keep their names;
  • two functions renamed at once: each takes its own proofs, True goals included (the same statement in both functions), and the stubs of the removed function are deleted;
  • a changed postcondition: the old proof is kept, with the note;
  • the change reverted: the kept proof comes back by its name;
  • a removed function: its proofs are kept;
  • the first names back: everything returns and certifies;
  • fallback runs: proofs of the functions Z3 settles stay; a removed function's proofs are kept;
  • pruning, and the error without a project;
  • a partial fallback export leaves the proof of the obligation Z3 proved in place;
  • a 0.1 project with six proofs, an unedited stub, and a stray proof and stub, migrated and certified.
• Updated: the other Lean tests for the new names and paths (lean_project, lean_fallback, lean_fallback_partial, lean_fallback_fast, lean_certify, lean_dependencies, lean_semantics), and their proof inputs for the new spec-body names. The fidelity gate's Lean identity check now compares each project goal's (stable id, kind, source) with the scratch and archive export, and checks each proof file's header against its path and name.
• On main, the new test fails from its second check on: the goal names, paths, headers, moves, and messages are all new.

Mutants of Verifier.cpp, LeanBackend.cpp, and ObligationSerialization.cpp, each rebuilt and run against the Lean tests: 27 of 28 killed.

• no move to another goal; a renamed function's goals not moved together, or the last candidate preferred; a kept proof never restored by its name; kept proofs never read;

• the functions the solver settles examined; their modules, or their termination modules, not recorded; the goals left to the solver unknown, not recorded, imported, or certified;

• stubs taken for proofs, or moved like proofs; 0.1 stubs reported as moved, or kept; 0.1 proofs not migrated;

• a proof written over its stub given no header; goal or spec-body names not rewritten in a moved proof; the source in a header unescaped;

• an untaken proof deleted, or kept without its note; emptied directories left; --lean-prune-stale ignored;

• spec bodies named by position; the statement hash including the function's identity.

  The survivor keeps a proof at its goal's path whatever its full hash: the path already carries the hash's first eight digits, so the two differ only on a 32-bit collision within one function and kind. Four of the killed mutants survived a first run and showed gaps in the test, which now has a step for each: a reverted change, a re-export after proofs are copied in, and a function with nothing but stubs.

Docs

• tooling.rst: goal and file names, moves, Stale/, and the 0.1 migration in the --lean-project row; what a fallback run examines; the --lean-prune-stale row and its error.
• Book, ch17: "Proofs that follow their goals", with a rename and a changed statement shown with their exact output; the worked example's goal and file names updated.
• ch16: the proof-file path.
• Release notes: "Lean proofs stay with their goals", and the statement hash under data formats.
• ARCHITECTURE.md: "Project goals and their proofs" (names, records, regeneration, fallback runs, the test). DESIGN.md: the naming and regeneration rules.

Checked

Builds on #56 (the Lean 4.35.0 pin), whose 13 commits come first here until it merges. Checked on a local merge of main 14a7383 with #54, #55, and #56; rebased onto main d7bb472 and the rebased #56, the tree is the same, file for file.

• Lean tests: all 37 lit tests that run Lean pass, lean_identity.test and the fidelity gate included, plus backend_options.cpp. VerifyTests: 62 passed, 1 skipped (EncodingParityTest, which needs archives).
• On main, the table's first row: after reordering two postconditions, certification fails with the type mismatch shown above.
• Solver paths: nothing this changes runs outside Lean export and project regeneration. The statement hash is a new function, and the semantic hash and the archive are unchanged, so no Z3 verdict can change. The full suites are left to CI.
• Docs: the site builds with -W; docs_coverage.test and docs_examples.test pass, and the book's outputs are from this build. clang-format: clean.