[orda-aska]

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

comparator.json takes Protobuf.Spec / Protobuf.Proofs and the Protobuf.Spec.* theorem names; bar.toml [spec] files take Protobuf/Spec.lean and Protobuf/Spec/Defs.lean.

Validation: lake build passed, including the relocated proof modules. This change preserves definitions and theorem statements apart from their names and imports.

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

Rechecked 2026-10-29

• Rebased onto current main (95151dc, which added protobuf#5's spec_authors change to bar.toml). There were no conflicts.
• Added one commit: Protobuf/Types.lean and Protobuf/Spec.lean comments still pointed at Spec/Defs.lean; they now say Protobuf/Spec/Defs.lean. Comments only.
• Clean lake build: 22 jobs. python3 tests/run_tests.py: 200,000 of 200,000 inputs agree. python3 tests/planted_bugs.py: 9 of 10 caught, the same as the committed record; the LEN limit bug is uncaught by design and is covered by Protobuf.Spec.decode_iff.
• bar/check.py --no-lean --offline (mission at the pinned 6ba85c2): no failures, and item 2 names all 11 theorems. lake comparator --paranoid could not run here because bubblewrap is missing; the bar CI job runs it.

🤖 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 review is of head c61f11f, on main 95151dc. My earlier full review covered this same commit. Since then, neither the head nor main has moved. So there is no new code to review. I reran the key checks to confirm.

What I checked earlier, on this head and on main:

• lake build passes with 22 jobs on both. The only warnings are the same 11 sorrys in the challenge file, at the same lines.
• Text: I mapped Protobuf.Spec and the new paths back to the old names. After that, every moved Lean file and Protobuf/Types.lean is byte-identical to main.
• Elaborated terms: a meta script compared every constant, 44 in the challenge env and 237 in the proof env. The prefix was renamed back inside the terms. Kind, universe params, type, value, axioms and inductive shape all match. The only difference is the module tag inside the 11 sorry stubs.
• #check @ and #print axioms for the 11 comparator theorems print the same as main, apart from the Protobuf. prefix.
• lake comparator --paranoid: all six kernels accept on both trees.
• tests/planted_bugs.py: 9 of 10 caught, the same as the committed record.
• README, SPEC.md and comparator.json change only paths and name prefixes.

What I reran today, in a fresh worktree at c61f11f:

• The head is unchanged. git diff from the reviewed head is empty. Main is still 95151dc. The mission check.py and reviewers.toml are unchanged, and CI still pins 6ba85c2.
• lake build: OK, 22 jobs, the same 11 sorry warnings.
• check.py --offline --run-tests: exit 0. Item 1 is OPEN, because no approval is recorded. The spec hash is 3f7a59a6.... Items 2 to 6 PASS. Item 7 is SKIP (offline). The tests ran 200,000 inputs with 0 failures. The worktree was clean afterwards.
• The text check against main still holds for all 7 Lean files.
• Both bar / bar runs on c61f11f pass. This is the only open PR here. It is not stacked on another PR.

The first review's notes are fixed. The stale Spec/Defs.lean comments now say Protobuf/Spec/Defs.lean. The branch is on current main. It is no longer a draft.

Non-blocking:

• Protobuf/Spec/Defs.lean says the definitions were written "independently of the code in Protobuf/". Protobuf/ now also holds the spec and the proofs. Naming Protobuf/Varint.lean and Protobuf/Wire.lean would be clearer. This file is in the spec hash, so the cheapest time to change it is before anyone approves the spec. It is fine to leave as is.
• The spec hash changes from 31dbf590... on main to 3f7a59a6..., as expected for a path move. No approval is recorded, so none is voided.
• mission#22 still lists this convention under "Decision needed". mission#23 says approving these PRs is how it gets agreed. So this approval also accepts the convention for protobuf.

---

Generated by Claude Code