[orda-aska]

Move specification and proof modules beneath Codec and update imports, Lake roots, configuration and documentation to match. Prefix shared specification declarations with Codec.Spec.

Part of Proven-Commons/mission#22. The other libraries have separate adoption PRs.

Merge order: this lands second, after #14. The branch is rebased on top of #14's branch (base stays main), so until #14 merges this PR also shows #14's two commits; review only the top commit, "Move proof modules and spec names under Codec". Once #14 merges, the diff here is the move alone. The rebase applied cleanly; #14's new PEM vectors moved with Codec/Spec.lean and Codec/Proofs/Pem.lean.

Validation, on the rebased head:

• lake build passes, including the relocated proof modules.
• python3.12 tests/run_tests.py: 1000000/1000000 inputs agree, 0 failures (record unchanged from Bound decimal conversion and cover PEM refusal cases #14).
• Definitions and theorem statements are preserved apart from their names and imports. CI (verified bar, which runs the comparator) runs on the new head.

🤖 Generated with Claude Code

https://claude.ai/code/session_01QwrvNdsMA6RtgKxXn1Pmhf

[zero-aska]

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

This PR is stacked on #14. Its branch holds #14's two commits (8b5db29, 7dcb6bc) and then the move commit (cdc9afa). It must merge after #14. Until #14 lands, the GitHub diff here also shows #14's changes.

What changed since my last review (head 49df29b)

• The branch was rebased onto #14's head. git range-diff shows the move commit is the same patch. I diffed the old and new move commits: they are identical apart from blob ids and line numbers.
• The only other change is #14's own change. Its two new pem_vectors conjuncts landed in Codec/Spec.lean and Codec/Proofs/Pem.lean.

What I checked on this head (cdc9afa)

• lake build: passes.
• check.py --offline --run-tests: exit 0. 1 OPEN (no approval yet; the spec hash is now 7881dabc..., because pem_vectors gained #14's two conjuncts). 2 PASS (37 theorems). 3 PASS (lake comparator --paranoid accepts all 37 under every bundled kernel; no kernel failed). 4 PASS (23 Lean files). 5 PASS (1,000,000 inputs, 0 failures). 6 PASS. 7 SKIP (offline). CI "bar / bar" also passed on this head.
• python3.12 tests/run_tests.py (3.12.3): 0 failures. git diff tests/TEST-RESULTS.md is empty, so the record carried over from #14 reproduces exactly.
• Statements. A Lean script dumped every constant in the moved modules in full: 110 from the spec import and 845 from the proofs import. That covers types, binder info, universe levels, definition bodies and proof-term hashes. I mapped Codec.Spec/Codec.Proofs back to Spec/Proofs. Against #14's head, both dumps are byte-identical. Against main, only pem_vectors differs, which is #14's change. A pp.all print of 7 theorems (hex_encode_cons, base64_encode_three, crc32_eq, percent_decode_iff, pem_vectors, luhn_vectors, iban_valid_iff) gives the same result. So this is still a pure rename.
• Docs. Every Codec.Spec.* name in README.md and SPEC.md exists, and each file names all 37 theorems. No import Spec, import Proofs or bare Spec.x is left.
• Merge. After #14 lands, by a merge commit or by a squash, git merge-tree merges this head cleanly. The result is exactly this head's tree.

Blocking: none. My last review had none either. Its draft note is resolved.

Non-blocking

• Codec/Spec.lean lines 11 and 112 still say Spec/Defs.lean. Line 5 already says Codec/Proofs.lean. Suggest Codec/Spec/Defs.lean. It is a spec file, so the fix changes the spec hash. It is cheapest before anyone approves the hash.

Merge order

• Merge #14 first, then this PR. Do not merge this one first: it would land #14's commits under the move PR's title.

---

Generated by Claude Code

The merge-base changed after approval.

[zero-aska]

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

Branch protection dismissed my earlier approval of this same head when #14 merged and the merge base changed. The head itself has not changed.

What I checked against the new main (6603fb3, #14's merge):

• #14's commits are now on main. The parent of cdc9afa is an ancestor of main.
• The PR's diff against main is exactly the move commit, "Move proof modules and spec names under Codec". The three-dot diff, the two-dot diff and the commit's own diff are identical.
• git merge-tree against main is clean.

So the review in my earlier approval still covers everything this merges: a pure rename, with statements, proof terms and axioms unchanged. mission#22's convention is decided.

---

Generated by Claude Code

The merge-base changed after approval.

[zero-aska]

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

My two earlier approvals of this head were dismissed when GitHub recomputed the merge base after #14 landed. The PR now records base 6603fb3, which is current main, and shows one commit: the move. That is exactly the diff my previous approval checked, so that review still covers it.

---

Generated by Claude Code