Put template proof modules and declarations under Clamp

bar/README.md

@@ -21,7 +21,8 @@ It prints one row per bar item, with PASS, FAIL, OPEN, or SKIP. It exits 1 if an
 ## Start a library
 
 1. Copy `template/` into a new repo named for the software it verifies.
-2. Replace `Clamp.lean`, `Spec.lean`, `Proofs.lean`, `Main.lean`, `SPEC.md`, the tests, and the page. Update `lakefile.toml` (library and executable names, `defaultTargets`), the executable path in `tests/run_tests.py`, `comparator.json`, and `bar.toml` (including `[spec] code`) to match.
+2. Replace `Clamp.lean`, `Clamp/Spec.lean`, `Clamp/Proofs.lean`, `Main.lean`, `SPEC.md`, the tests, and the page. Update `lakefile.toml` (library and executable names, `defaultTargets`), the executable path in `tests/run_tests.py`, `comparator.json`, and `bar.toml` (including `[spec] code`) to match.
+   Keep both module paths and declaration names under the library name. For example, rename `Clamp.Spec` and `Clamp.Proofs` to `YourLib.Spec` and `YourLib.Proofs`, and `Clamp.Spec.clamp_of_mem` to `YourLib.Spec.your_theorem`. Keep the matching Lake `roots`, comparator names, spec paths and page claims in step. This avoids collisions when libraries are imported together. Existing libraries need their own migration and review.
 3. Keep `[project] status = "in-progress"` until every item passes.
 4. In `.github/workflows/bar.yml`, pin the workflow and `bar-ref` to the same tag or commit of this repo.
 5. Have the default branch require the `bar / bar` check, which the "verified bar" workflow reports.

bar/template/Clamp/Proofs.lean

@@ -0,0 +1,17 @@
+/-
+  Proofs of the statements in `Clamp/Spec.lean`, under the same names.
+-/
+
+import Clamp
+
+open Clamp
+
+theorem Clamp.Spec.clamp_in_range (lo hi x : Nat) (h : lo ≤ hi) :
+    lo ≤ clamp lo hi x ∧ clamp lo hi x ≤ hi := by
+  unfold clamp
+  omega
+
+theorem Clamp.Spec.clamp_of_mem (lo hi x : Nat) (h₁ : lo ≤ x) (h₂ : x ≤ hi) :
+    clamp lo hi x = x := by
+  unfold clamp
+  omega

bar/template/Spec.lean → bar/template/Clamp/Spec.lean

@@ -2,7 +2,7 @@
   The specification as Lean statements: the challenge file.
 
   A reviewer who did not write this file approves it, and `bar.toml`
-  records the SHA-256 it had then. The proofs live in `Proofs.lean`;
+  records the SHA-256 it had then. The proofs live in `Clamp/Proofs.lean`;
   `lake comparator` checks that each one proves exactly the statement
   written here. The `sorry` below is expected in this file only.
 -/
@@ -12,11 +12,11 @@ import Clamp
 open Clamp
 
 /-- Safety: the result is never outside the range. -/
-theorem Spec.clamp_in_range (lo hi x : Nat) (h : lo ≤ hi) :
+theorem Clamp.Spec.clamp_in_range (lo hi x : Nat) (h : lo ≤ hi) :
     lo ≤ clamp lo hi x ∧ clamp lo hi x ≤ hi := sorry
 
 /-- Usefulness: a value already in range comes back unchanged.
     A function that always returns `lo` passes `clamp_in_range`
     but fails this one. -/
-theorem Spec.clamp_of_mem (lo hi x : Nat) (h₁ : lo ≤ x) (h₂ : x ≤ hi) :
+theorem Clamp.Spec.clamp_of_mem (lo hi x : Nat) (h₁ : lo ≤ x) (h₂ : x ≤ hi) :
     clamp lo hi x = x := sorry

bar/template/README.md

@@ -8,10 +8,10 @@ Status: in progress. The specification has not been approved by a reviewer, so t
 
 | Claim | Theorem |
 |-------|---------|
-| When `lo ≤ hi`, `clamp lo hi x` is never below `lo` or above `hi`. | `Spec.clamp_in_range` |
-| A value already between `lo` and `hi` comes back unchanged. | `Spec.clamp_of_mem` |
+| When `lo ≤ hi`, `clamp lo hi x` is never below `lo` or above `hi`. | `Clamp.Spec.clamp_in_range` |
+| A value already between `lo` and `hi` comes back unchanged. | `Clamp.Spec.clamp_of_mem` |
 
-The statements are in `Spec.lean`, the proofs in `Proofs.lean`. The command-line tool in `Main.lean` calls the proved `Clamp.clamp` directly.
+The statements are in `Clamp/Spec.lean`, the proofs in `Clamp/Proofs.lean`. The command-line tool in `Main.lean` calls the proved `Clamp.clamp` directly.
 
 ## What is not proved
 
@@ -35,13 +35,13 @@ lake comparator --paranoid
 python3 tests/run_tests.py
 ```
 
-`lake comparator --paranoid` builds the project in a sandbox, checks that each theorem in `Proofs.lean` proves exactly the statement in `Spec.lean`, checks that it uses only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean. The test script compares the tool with the oracle on a million inputs and rewrites `tests/TEST-RESULTS.md`.
+`lake comparator --paranoid` builds the project in a sandbox, checks that each theorem in `Clamp/Proofs.lean` proves exactly the statement in `Clamp/Spec.lean`, checks that it uses only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean. The test script compares the tool with the oracle on a million inputs and rewrites `tests/TEST-RESULTS.md`.
 
 ## Layout
 
 - `Clamp.lean`: the code under proof.
-- `Spec.lean`: the statements, with `sorry` for proofs. This is the file a reviewer approves.
-- `Proofs.lean`: the proofs, under the same names.
+- `Clamp/Spec.lean`: the statements, with `sorry` for proofs. This is the file a reviewer approves.
+- `Clamp/Proofs.lean`: the proofs, under the same names.
 - `Main.lean`: the command-line tool used by the tests.
 - `lakefile.toml`: the build. It names the libraries and the executable, and sets nothing else.
 - `comparator.json`: which theorems `lake comparator` checks, and which axioms it allows.

bar/template/SPEC.md

@@ -1,6 +1,6 @@
 # Specification: clamp
 
-This is the template's specification. Replace it with the real one. A reviewer who did not write it approves it together with `Spec.lean` and the page sections listed in `bar.toml`.
+This is the template's specification. Replace it with the real one. A reviewer who did not write it approves it together with `Clamp/Spec.lean` and the page sections listed in `bar.toml`.
 
 ## Scope
 
@@ -12,12 +12,12 @@ Every input is valid. The function is total and has no error case.
 
 ## What must always hold
 
-Each property below is a theorem in `Spec.lean`.
+Each property below is a theorem in `Clamp/Spec.lean`.
 
 | Property | Theorem |
 |----------|---------|
-| With `lo ≤ hi`, the result is at least `lo` and at most `hi`. | `Spec.clamp_in_range` |
-| A value already in the range comes back unchanged. | `Spec.clamp_of_mem` |
+| With `lo ≤ hi`, the result is at least `lo` and at most `hi`. | `Clamp.Spec.clamp_in_range` |
+| A value already in the range comes back unchanged. | `Clamp.Spec.clamp_of_mem` |
 
 The first is a safety property. A function that always returns `lo` meets it, so the second is there to rule that function out.
 

bar/template/bar.toml

@@ -15,8 +15,8 @@ entry_points = ["Main.lean"]
 
 [spec]
 # What a reviewer approves, together with the whole page named above.
-# Spec.lean is the challenge module named in comparator.json.
-files = ["SPEC.md", "Spec.lean"]
+# Clamp/Spec.lean is the challenge module named in comparator.json.
+files = ["SPEC.md", "Clamp/Spec.lean"]
 # The code under proof: the definitions the statements are about. Any
 # other project definition a statement uses must sit in the spec files,
 # so that the approval fixes what the statement means.

bar/template/comparator.json

@@ -1,6 +1,6 @@
 {
-  "challenge_module": "Spec",
-  "solution_module": "Proofs",
-  "theorem_names": ["Spec.clamp_in_range", "Spec.clamp_of_mem"],
+  "challenge_module": "Clamp.Spec",
+  "solution_module": "Clamp.Proofs",
+  "theorem_names": ["Clamp.Spec.clamp_in_range", "Clamp.Spec.clamp_of_mem"],
   "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"]
 }

bar/template/lakefile.toml

@@ -1,15 +1,17 @@
 name = "clamp"
 version = "0.1.0"
-defaultTargets = ["Clamp", "Spec", "Proofs", "clamp"]
+defaultTargets = ["Clamp", "ClampSpec", "ClampProofs", "clamp"]
 
 [[lean_lib]]
 name = "Clamp"
 
 [[lean_lib]]
-name = "Spec"
+name = "ClampSpec"
+roots = ["Clamp.Spec"]
 
 [[lean_lib]]
-name = "Proofs"
+name = "ClampProofs"
+roots = ["Clamp.Proofs"]
 
 [[lean_exe]]
 name = "clamp"

bar/tests/test_check.py

@@ -121,6 +121,20 @@ def status(self, item, **kw):
 
     # The template as shipped.
 
+    def test_template_uses_library_owned_modules_and_declarations(self):
+        import json
+        import tomllib
+        cfg = json.loads((self.p.root / "comparator.json").read_text())
+        lake = tomllib.loads((self.p.root / "lakefile.toml").read_text())
+        self.assertEqual(cfg["challenge_module"], "Clamp.Spec")
+        self.assertEqual(cfg["solution_module"], "Clamp.Proofs")
+        self.assertTrue(all(n.startswith("Clamp.Spec.") for n in cfg["theorem_names"]))
+        self.assertFalse((self.p.root / "Spec.lean").exists())
+        self.assertFalse((self.p.root / "Proofs.lean").exists())
+        roots = {lib["name"]: lib.get("roots") for lib in lake["lean_lib"]}
+        self.assertEqual(roots["ClampSpec"], ["Clamp.Spec"])
+        self.assertEqual(roots["ClampProofs"], ["Clamp.Proofs"])
+
     def test_template_has_no_failures(self):
         got = self.p.run()
         self.assertEqual(got[1][0], "OPEN")
@@ -145,7 +159,7 @@ def test_approval_offline_is_skipped_not_passed(self):
     def test_changing_a_statement_voids_the_approval(self):
         self.p.approve()
         github = approved_by(self.p)
-        self.p.edit("Spec.lean", "lo ≤ clamp lo hi x ∧", "lo ≤ clamp lo hi x ∨")
+        self.p.edit("Clamp/Spec.lean", "lo ≤ clamp lo hi x ∧", "lo ≤ clamp lo hi x ∨")
         got = self.p.run(offline=False, github=github)
         self.assertEqual(got[1][0], "OPEN")
         self.assertIn("changed after the last approval", got[1][1])
@@ -181,7 +195,7 @@ def test_changing_files_outside_the_spec_and_page_keeps_the_approval(self):
 
     def test_line_endings_do_not_change_the_hash(self):
         before, _ = check.spec_hash(self.p.root, check.load_bar(self.p.root))
-        path = self.p.root / "Spec.lean"
+        path = self.p.root / "Clamp/Spec.lean"
         path.write_bytes(path.read_bytes().replace(b"\n", b"\r\n"))
         after, _ = check.spec_hash(self.p.root, check.load_bar(self.p.root))
         self.assertEqual(before, after)
@@ -232,7 +246,7 @@ def test_approving_a_pull_request_that_does_not_record_the_approval_does_not_cou
         self.assertEqual(got[1][0], "OPEN")
 
     def test_each_reviewed_file_voids_the_approval(self):
-        for rel, old, new in [("comparator.json", '"Spec.clamp_of_mem"', '"Spec.clamp_of_mem" '),
+        for rel, old, new in [("comparator.json", '"Clamp.Spec.clamp_of_mem"', '"Clamp.Spec.clamp_of_mem" '),
                               ("Main.lean", "It calls the proved function", "It calls the function"),
                               ("tests/run_tests.py", "default=20261024", "default=1")]:
             with self.subTest(rel):
@@ -287,7 +301,7 @@ def test_review_of_other_text_does_not_count(self):
         # spec said something else, and the author recorded the hash of
         # text the reviewer never saw.
         before = approved_by(self.p)
-        self.p.edit("Spec.lean", "lo ≤ clamp lo hi x ∧", "lo ≤ clamp lo hi x ∨")
+        self.p.edit("Clamp/Spec.lean", "lo ≤ clamp lo hi x ∧", "lo ≤ clamp lo hi x ∨")
         self.p.approve()
         got = self.p.run(offline=False, github=before)
         self.assertEqual(got[1][0], "OPEN")
@@ -310,11 +324,11 @@ def test_verified_project_without_approval_fails(self):
     # Item 2: claims name theorems.
 
     def test_theorem_missing_from_claims_is_open(self):
-        self.p.edit("README.md", "| `Spec.clamp_of_mem` |", "| (see Spec.lean) |")
+        self.p.edit("README.md", "| `Clamp.Spec.clamp_of_mem` |", "| (see Clamp/Spec.lean) |")
         self.assertEqual(self.status(2), "OPEN")
 
     def test_theorem_name_must_match_whole(self):
-        self.p.edit("README.md", "`Spec.clamp_of_mem`", "`Spec.clamp_of_mem_aux`")
+        self.p.edit("README.md", "`Clamp.Spec.clamp_of_mem`", "`Clamp.Spec.clamp_of_mem_aux`")
         self.assertEqual(self.status(2), "OPEN")
 
     # Item 3: proof configuration.
@@ -324,7 +338,7 @@ def test_extra_permitted_axiom_fails(self):
         self.assertEqual(self.status(3), "FAIL")
 
     def test_challenge_file_must_be_approved(self):
-        self.p.edit("bar.toml", 'files = ["SPEC.md", "Spec.lean"]', 'files = ["SPEC.md"]')
+        self.p.edit("bar.toml", 'files = ["SPEC.md", "Clamp/Spec.lean"]', 'files = ["SPEC.md"]')
         got = self.p.run()
         self.assertEqual(got[3][0], "FAIL")
         self.assertIn("not one of the approved spec files", got[3][1])
@@ -461,13 +475,13 @@ def test_decide_native_fails(self):
         self.assertEqual(self.status(4), "FAIL")
 
     def test_unfinished_proofs_are_open_in_progress_and_fail_once_verified(self):
-        self.assertEqual(self.status(4), "PASS")  # Spec.lean is full of sorry
-        self.p.edit("Proofs.lean", "  unfold clamp\n  omega\n\ntheorem Spec.clamp_of_mem",
-                    "  sorry\n\ntheorem Spec.clamp_of_mem")
+        self.assertEqual(self.status(4), "PASS")  # Clamp/Spec.lean is full of sorry
+        self.p.edit("Clamp/Proofs.lean", "  unfold clamp\n  omega\n\ntheorem Clamp.Spec.clamp_of_mem",
+                    "  sorry\n\ntheorem Clamp.Spec.clamp_of_mem")
         self.p.edit("Clamp.lean", "end Clamp", "theorem t2 : 1 = 1 := by admit\n\nend Clamp")
         status, detail = self.p.run()[4]
         self.assertEqual(status, "OPEN")
-        self.assertIn("Proofs.lean:", detail)
+        self.assertIn("Clamp/Proofs.lean:", detail)
         self.assertIn("admit", detail)
         self.p.edit("bar.toml", 'status = "in-progress"', 'status = "verified"')
         self.assertEqual(self.status(4), "FAIL")
@@ -682,15 +696,15 @@ def test_template_proofs_pass(self):
         self.assertEqual(self.p.run(no_lean=False)[3][0], "PASS")
 
     def test_weaker_statement_fails(self):
-        self.p.edit("Proofs.lean", "    lo ≤ clamp lo hi x ∧ clamp lo hi x ≤ hi := by\n  unfold clamp\n  omega",
+        self.p.edit("Clamp/Proofs.lean", "    lo ≤ clamp lo hi x ∧ clamp lo hi x ≤ hi := by\n  unfold clamp\n  omega",
                     "    lo ≤ clamp lo hi x ∨ clamp lo hi x ≤ hi := by\n  unfold clamp\n  omega")
         status, detail = self.p.run(no_lean=False)[3]
         self.assertEqual(status, "FAIL")
         self.assertIn("do not match", detail)
 
     def test_sorry_proof_fails_once_verified(self):
-        self.p.edit("Proofs.lean", "  unfold clamp\n  omega\n\ntheorem Spec.clamp_of_mem",
-                    "  sorry\n\ntheorem Spec.clamp_of_mem")
+        self.p.edit("Clamp/Proofs.lean", "  unfold clamp\n  omega\n\ntheorem Clamp.Spec.clamp_of_mem",
+                    "  sorry\n\ntheorem Clamp.Spec.clamp_of_mem")
         self.p.edit("bar.toml", 'status = "in-progress"', 'status = "verified"')
         got = self.p.run(no_lean=False)
         self.assertEqual(got[3][0], "FAIL")
@@ -701,9 +715,9 @@ def walk(self, extra_theorems=()):
         import json
         path = self.p.root / "comparator.json"
         cfg = json.loads(path.read_text())
-        cfg["theorem_names"] = ["Spec.clamp_in_range", "Spec.clamp_of_mem", *extra_theorems]
+        cfg["theorem_names"] = ["Clamp.Spec.clamp_in_range", "Clamp.Spec.clamp_of_mem", *extra_theorems]
         path.write_text(json.dumps(cfg, indent=2))
-        subprocess.run(["lake", "build", "Spec"], cwd=self.p.root, capture_output=True, check=True)
+        subprocess.run(["lake", "build", "ClampSpec"], cwd=self.p.root, capture_output=True, check=True)
         bar = check.load_bar(self.p.root)
         cmp_cfg, _ = check.load_comparator(self.p.root)
         return check.statement_dependencies(self.p.root, bar, cmp_cfg)[0]
@@ -713,42 +727,42 @@ def test_walk_passes_the_template(self):
 
     def test_instance_in_the_code_that_changes_a_statement_fails(self):
         # The comparator sees the same instance on both sides, so only the
-        # walk can tell that `≤` in Spec.lean no longer means Nat.le.
+        # walk can tell that `≤` in Clamp/Spec.lean no longer means Nat.le.
         self.p.edit("Clamp.lean", "end Clamp",
                     "instance (priority := high) sneaky : LE Nat := ⟨fun _ _ => True⟩\n\nend Clamp")
         problems = self.walk()
         self.assertTrue(any("Clamp.sneaky" in p for p in problems), problems)
 
     def test_predicate_in_the_code_fails_and_in_the_spec_passes(self):
         self.p.edit("Clamp.lean", "end Clamp", "def Good (n : Nat) : Prop := n = n\n\nend Clamp")
-        self.p.append("Spec.lean", "\ntheorem Spec.good (lo hi x : Nat) : Clamp.Good (clamp lo hi x) := sorry\n")
-        problems = self.walk(["Spec.good"])
+        self.p.append("Clamp/Spec.lean", "\ntheorem Clamp.Spec.good (lo hi x : Nat) : Clamp.Good (clamp lo hi x) := sorry\n")
+        problems = self.walk(["Clamp.Spec.good"])
         self.assertTrue(any("Clamp.Good" in p for p in problems), problems)
 
         self.p.edit("Clamp.lean", "def Good (n : Nat) : Prop := n = n\n", "")
-        self.p.edit("Spec.lean", "theorem Spec.good (lo hi x : Nat) : Clamp.Good",
-                    "def Spec.Good (n : Nat) : Prop := n = n\n\ntheorem Spec.good (lo hi x : Nat) : Spec.Good")
-        self.assertEqual(self.walk(["Spec.good"]), [])
+        self.p.edit("Clamp/Spec.lean", "theorem Clamp.Spec.good (lo hi x : Nat) : Clamp.Good",
+                    "def Clamp.Spec.Good (n : Nat) : Prop := n = n\n\ntheorem Clamp.Spec.good (lo hi x : Nat) : Clamp.Spec.Good")
+        self.assertEqual(self.walk(["Clamp.Spec.good"]), [])
 
     def test_theorem_left_out_of_comparator_json_fails(self):
         # Found in review: a claimed theorem could be dropped from
         # comparator.json, and so from the proof check, after approval.
-        self.p.append("Spec.lean", "\ntheorem Spec.clamp_le_hi (lo hi x : Nat) (h : lo ≤ hi) : "
+        self.p.append("Clamp/Spec.lean", "\ntheorem Clamp.Spec.clamp_le_hi (lo hi x : Nat) (h : lo ≤ hi) : "
                       "clamp lo hi x ≤ hi := sorry\n")
         problems = self.walk()
-        self.assertTrue(any("does not name these theorems" in p and "Spec.clamp_le_hi" in p
+        self.assertTrue(any("does not name these theorems" in p and "Clamp.Spec.clamp_le_hi" in p
                             for p in problems), problems)
 
     def test_unfinished_proof_is_open_in_progress(self):
-        self.p.edit("Proofs.lean", "  unfold clamp\n  omega\n\ntheorem Spec.clamp_of_mem",
-                    "  sorry\n\ntheorem Spec.clamp_of_mem")
+        self.p.edit("Clamp/Proofs.lean", "  unfold clamp\n  omega\n\ntheorem Clamp.Spec.clamp_of_mem",
+                    "  sorry\n\ntheorem Clamp.Spec.clamp_of_mem")
         got = self.p.run(no_lean=False)
         self.assertEqual(got[3][0], "OPEN", got[3][1])
         self.assertEqual(got[4][0], "OPEN")
 
     def test_statement_without_code_fails(self):
-        self.p.append("Spec.lean", "\ntheorem Spec.trivial : 1 + 1 = 2 := sorry\n")
-        problems = self.walk(["Spec.trivial"])
+        self.p.append("Clamp/Spec.lean", "\ntheorem Clamp.Spec.trivial : 1 + 1 = 2 := sorry\n")
+        problems = self.walk(["Clamp.Spec.trivial"])
         self.assertTrue(any("mentions no code under proof" in p for p in problems), problems)
 
     def test_implemented_by_passes_the_kernels_so_the_source_rule_must_catch_it(self):