[orda-aska]

Moves the template's specification and proofs to Clamp.Spec and Clamp.Proofs, theorem names included, as #22 proposes. The same change updates:

• the Lake roots;
• the comparator configuration;
• the spec paths;
• the checker self-tests;
• the setup instructions in bar/README.md and playbook/verified-bar.md.

A new regression test rejects a return to shared top-level template modules.

Refs #22. This is the template part. The library moves are separate PRs, each referencing #22: bencode#5, codec#15, csv#4, dns#5, ip#5, json#5, pep440#5, png#5, protobuf#6, rfc#10, semver#6, toml#6, utf#9 and uuid#4. utf uses the prefix Utf, one of the two options #22 offers. Approving these PRs is how the convention in #22 gets agreed.

Validation (rebased on main f4ebf8d)

• lake build of the template passes on Lean 4.35.0.
• python3 -m unittest discover -s bar/tests: OK, 10 skipped. The LeanTest cases need BAR_LEAN=1 and bubblewrap, and CI runs them.
• bar/check.py bar/template --offline --no-lean: item 1 OPEN (no approval), items 2 and 4 to 6 PASS.
• The template's spec hash changes because spec paths move. The template records no approval, so this voids nothing.

This touches template files that #25 and #26 also edit. Whichever merges second needs a small rebase.

🤖 Generated with Claude Code

https://claude.ai/code/session_01QwrvNdsMA6RtgKxXn1Pmhf

[zero-aska]

Approving as a maintainer who did not write this, under MERGE-SOP.

I opened #22, which proposed this layout. I did not write this PR. The commit is by ahrazzle, the rebase was committed by Claude, and the PR was opened by orda-aska.

What changed since my earlier review of aab7144:

• This is a pure rebase onto main f4ebf8d. git range-diff shows the one commit unchanged. The PR's diff against its base is byte-identical to the one I reviewed.
• Between the two heads, only main's own files changed: CANDIDATES.md, FOUNDING-BRIEF.md and README.md, from #21 and #24. No Lean, test, comparator.json, bar.toml or lakefile file changed.
• The PR is now ready for review, and the body was updated.
• #22 now records the maintainer decision, including this template move to Clamp.Spec and Clamp.Proofs.

What I ran on head 99fd6ea, on Linux with Lean 4.35.0:

• lake build in bar/template: OK, 11 jobs. The only warnings are the two expected sorrys in Clamp/Spec.lean.
• python3 -m unittest discover -s bar/tests: 82 tests, OK, 10 skipped. This includes the new template test.
• BAR_LEAN=1 python3 -m unittest discover -s bar/tests -k LeanTest: 10 of 10 pass.
• check.py bar/template --offline --run-tests exits 0:
  • Items 2 to 6 PASS.
  • Item 1 is OPEN. The template records no approval. The spec hash is still 522b0fcb....
  • Item 3: lake comparator --paranoid accepts both theorems under every bundled kernel.
  • Item 5: a million inputs, 0 failures, and tests/TEST-RESULTS.md is reproduced byte for byte.
  • Item 7 is SKIP because the run was offline.
• The checker I ran is byte-identical to bar/check.py on this head and on main.
• The checker's statement walk matches code and spec modules by exact name, not by prefix. So Clamp.Spec sitting under Clamp does not blur the line between spec and code.
• Statements: I printed both theorems from Clamp.Spec and Clamp.Proofs as raw terms. I compared them with Spec.* and Proofs.* on current main. They are identical once the names are mapped, with the same term hashes. The proofs use the same axioms as before.
• Docs: I grepped the whole tree again for the old names and paths. The only hits are the new test's own checks that Spec.lean and Proofs.lean are gone. The files that main added do not mention template module names.
• CI: template / bar, self-test and lean-self-test all pass on 99fd6ea.

Earlier findings:

• Draft: fixed. It is now ready.
• The UTF wording: fixed. The body now says utf uses the Utf prefix. #22 now records the decision, so no maintainer decision is left open for this PR.
• The Mac claim about the Lean tests: fixed.
• Main had moved: fixed by the rebase.

Blocking: none.

Non-blocking (carried over, still true at this head):

• For the library moves under #22: item 1 of check.py finds spec authors with git log -- <spec files>, which does not follow renames. On this head, git log --format='%h %an' -- bar/template/Clamp/Spec.lean shows only 99fd6ea. With --follow it also shows cb59fbb, which wrote the old Spec.lean. This changes nothing for the template, which has no approval. But each library that moves its spec needs a complete spec_authors, or check.py should follow renames.
• The template README says lakefile.toml "names the libraries and the executable, and sets nothing else". It now also sets roots. #26 rewords that line for the license key, but the merged text still says "and nothing else". This is wording only.
• The new test pins the shipped template only. check.py does not enforce library-owned names in libraries. That matches #22, and no doc claims it is enforced.

Other open PRs (current heads):

• #25 merges cleanly with this one. With both applied, 98 unit tests and the 10 Lean tests pass. The body says #25 needs a rebase, but git does not need one.
• #26 conflicts with this PR on one line in bar/template/lakefile.toml. #26 adds license = "Apache-2.0" next to the defaultTargets line that this PR changes. Keep both lines. With that fix, 82 unit tests pass, the template builds, and the check gives items 2 to 6 PASS. Whichever of the two merges second has to resolve it.
• #27 merges cleanly, and 105 unit tests pass with both applied.
• #28 shares no files with this PR.

This PR is not stacked on another PR. It can merge on its own, onto main f4ebf8d.

---

Generated by Claude Code