Put each library's Spec and Proofs modules and names under the library's own namespace #22

Problem

The anthology in Foundation-0/proven-commons builds the 18 Proven-Commons libraries that have a lakefile on their default branch, in one Lake workspace. One file can import every library's main module, but no file can import two libraries' proofs. Both reasons below hold on each library's default branch today.

1. Module names. One Lean file cannot import two modules with the same name, and these names repeat across libraries:

   • Proofs: 14 libraries (bencode, codec, csv, dns, ip, json, pep440, png, protobuf, rfc, semver, toml, utf, uuid)
   • Spec and Spec.Defs: 6 libraries (bencode, codec, protobuf, rfc, semver, utf)
   • Submodules: Proofs.RoundTrip (csv, dns, json, pep440, png, uuid), Proofs.Main (protobuf, rfc, semver, utf), Proofs.Examples (pep440, uuid), Proofs.Format (rfc, semver), Proofs.Verify (dns, png)

2. Declaration names. The 6 libraries with a comparator.json state their theorems as Spec.<name> and define what the statements use as Spec.<name> too. The Proofs module tree proves the theorems under the same names, as comparator.json expects. 16 of these names are declared by more than one library:

   • Theorems: Spec.decode_encode, Spec.decode_iff and Spec.encode_eq (protobuf, utf); Spec.reject_vectors (protobuf, semver, utf); Spec.isValid_iff (protobuf, rfc); Spec.parse_iff, Spec.parse_print, Spec.parse_valid, Spec.print_eq and Spec.print_parse (rfc, semver)
   • Definitions: Spec.ascii (bencode, codec); Spec.decimal (codec, semver); Spec.encode (protobuf, utf); Spec.Digit, Spec.Valid and Spec.render (rfc, semver)

   So renaming the modules alone is not enough.

bar/template uses a top-level Spec and Proofs too, so each new library repeats the pattern. The branches that will bring bech32, cbor, hostname, http and punycode to main all do.

The cost: no single build checks every proof in the org, and no single #print axioms pass can cover the collection. The anthology works around this by building and auditing each library on its own.

Proposal

Move both under the library's main module name, <Lib>: Bencode, Codec, Csv, Dns, Ip, Json, Pep440, Png, Protobuf, Rfc3339, SemVer, Toml or Uuid. utf has two main modules, Utf8 and Utf16, so it needs a choice (see below).

• Modules: everything under Spec and Proofs moves under <Lib>. Spec becomes <Lib>.Spec, Spec.X becomes <Lib>.Spec.X, Proofs becomes <Lib>.Proofs, and Proofs.X becomes <Lib>.Proofs.X. The files move from Spec.lean, Spec/, Proofs.lean and Proofs/ to the same names under <Lib>/. Every import of a moved module changes, including three outside those folders: rfc/Main.lean (import Spec.Ixdtf), and pep440/Pep440/Verify.lean and uuid/Uuid/Verify.lean (import Proofs, import Proofs.Examples).
• Declaration names: Spec.<name> becomes <Lib>.Spec.<name>, for theorems and definitions alike, in the statement, definition and proof files.
• Lake: keep one lean_lib each for the spec and the proofs, with roots set to the new module, for example name = "BencodeProofs" and roots = ["Bencode.Proofs"]. List them in defaultTargets. bencode's defaultTargets currently list only its executable.
• comparator.json: challenge_module becomes <Lib>.Spec, solution_module becomes <Lib>.Proofs, and theorem_names take the new names.
• bar.toml: [spec] files take the moved paths, for example Bencode/Spec.lean.
• README and SPEC.md: "What is proved" gives each theorem's full new name, because the bar's claim check looks for each comparator.json name verbatim. Both pages take the new file paths wherever they name Spec.lean, Spec/, Proofs.lean or Proofs/.

Across the 14 libraries, that is 92 files to move and 152 import lines to change. Most of it falls in rfc (22 files) and utf (17). The 8 libraries with a Proofs module and no comparator.json (csv, dns, ip, json, pep440, png, toml, uuid) need only the module moves. Their theorems are already in their own namespaces, such as Csv.Proofs and Ip. toml's proofs are unnamed examples.

Why both renames, and why nested names:

• Renaming only the declarations leaves problem 1, because Lean takes a module's name from its file path.
• Flat module names, such as BencodeProofs, would avoid the nesting. But the anthology recognizes a proof library by a root whose last part is Proofs.

Notes

• The checker: bar/check.py needs no change. It reads module names from comparator.json and paths from bar.toml, and maps a dotted module name to its path.
• The template: bar/template should change the same way, to Clamp.Spec and Clamp.Proofs, so that new libraries start under their own name. The same mission PR has to update what describes the old layout: bar/tests/test_check.py (which builds and edits the template), step 2 of "Start a library" in bar/README.md, and the layout in playbook/verified-bar.md. The five libraries still on branches can adopt it before they merge.
• Approvals: the spec approval hash covers the spec files, comparator.json, the entry points, the test files, the project page and the [spec] code list. This rename changes several of those, so it would void a recorded approval. No library has one yet (every bar.toml says in-progress), so the rename costs least now.
• Tests and CI: no change needed. The test scripts build the executable or run lake build, and the bar workflow names neither module. A few test files mention a Spec. name in a comment, and those take the new name.
• Checking a rename: each library's PR should be a pure rename. lake comparator --paranoid and the bar check should pass, and #print of each named theorem should differ from before only by the <Lib>. prefix.

What the anthology does

Foundation-0/proven-commons#7 (open) adds AnthologyProofs. It imports a library's proof library once every top-level module name that library uses is unique in the workspace and the joint build succeeds with it. Once that PR merges, each library that moves all its Spec and Proofs modules joins the joint proof build in the anthology's next daily sync pull request, with no change to the anthology's code. This is tracked in Foundation-0/proven-commons#4.

Decision

Decided on 2026-10-30 by two maintainers, recorded in #22 (comment). The owner can still overrule it.

• Convention: agreed as proposed above.
• utf's prefix: a new Utf (folder Utf/, no Utf.lean).
• PRs: one per library, and one for bar/template (mission#23). Libraries that reached main after this issue was written adopt the convention in their own PRs.

Current work

• Template: mission#23.
• The fourteen library PRs: 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. Each merges on its own approval on its current head.
• Stacked PRs: codec#15, rfc#10, toml#6 and utf#9 each wait for the PR under them: codec#14, rfc#9, toml#5 and utf#8.