From 99fd6eae9929f6210655f63b0abb9b89f02d11cd Mon Sep 17 00:00:00 2001 From: ahrazzle <38987266+ahrazzle@users.noreply.github.com> Date: Tue, 27 Oct 2026 22:47:54 -0500 Subject: [PATCH] Put template proof modules and declarations under Clamp --- bar/README.md | 3 +- bar/template/Clamp/Proofs.lean | 17 ++++++++ bar/template/{ => Clamp}/Spec.lean | 6 +-- bar/template/Proofs.lean | 17 -------- bar/template/README.md | 12 ++--- bar/template/SPEC.md | 8 ++-- bar/template/bar.toml | 4 +- bar/template/comparator.json | 6 +-- bar/template/lakefile.toml | 8 ++-- bar/tests/test_check.py | 70 ++++++++++++++++++------------ playbook/verified-bar.md | 4 +- 11 files changed, 86 insertions(+), 69 deletions(-) create mode 100644 bar/template/Clamp/Proofs.lean rename bar/template/{ => Clamp}/Spec.lean (72%) delete mode 100644 bar/template/Proofs.lean diff --git a/bar/README.md b/bar/README.md index 0d7008f..9ef0289 100644 --- a/bar/README.md +++ b/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. diff --git a/bar/template/Clamp/Proofs.lean b/bar/template/Clamp/Proofs.lean new file mode 100644 index 0000000..2973d8d --- /dev/null +++ b/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 diff --git a/bar/template/Spec.lean b/bar/template/Clamp/Spec.lean similarity index 72% rename from bar/template/Spec.lean rename to bar/template/Clamp/Spec.lean index 41d22b9..9a38c05 100644 --- a/bar/template/Spec.lean +++ b/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 diff --git a/bar/template/Proofs.lean b/bar/template/Proofs.lean deleted file mode 100644 index 7ca07e6..0000000 --- a/bar/template/Proofs.lean +++ /dev/null @@ -1,17 +0,0 @@ -/- - Proofs of the statements in `Spec.lean`, under the same names. --/ - -import Clamp - -open Clamp - -theorem 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 Spec.clamp_of_mem (lo hi x : Nat) (h₁ : lo ≤ x) (h₂ : x ≤ hi) : - clamp lo hi x = x := by - unfold clamp - omega diff --git a/bar/template/README.md b/bar/template/README.md index 8c5be07..c06fc1c 100644 --- a/bar/template/README.md +++ b/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. diff --git a/bar/template/SPEC.md b/bar/template/SPEC.md index 287dec6..b83fcfb 100644 --- a/bar/template/SPEC.md +++ b/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. diff --git a/bar/template/bar.toml b/bar/template/bar.toml index ac8f572..2cd33a5 100644 --- a/bar/template/bar.toml +++ b/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. diff --git a/bar/template/comparator.json b/bar/template/comparator.json index 2c5df63..dbe0e0f 100644 --- a/bar/template/comparator.json +++ b/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"] } diff --git a/bar/template/lakefile.toml b/bar/template/lakefile.toml index f78204e..004c5d9 100644 --- a/bar/template/lakefile.toml +++ b/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" diff --git a/bar/tests/test_check.py b/bar/tests/test_check.py index 87a5e26..2cc2faa 100644 --- a/bar/tests/test_check.py +++ b/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,7 +727,7 @@ 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() @@ -721,34 +735,34 @@ def test_instance_in_the_code_that_changes_a_statement_fails(self): 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): diff --git a/playbook/verified-bar.md b/playbook/verified-bar.md index b345523..09d82a1 100644 --- a/playbook/verified-bar.md +++ b/playbook/verified-bar.md @@ -50,8 +50,8 @@ Copy [bar/template](../bar/template) to start. It passes every item except the a - `lean-toolchain` and `lake-manifest.json`, so `lake comparator` builds what was checked. - `lakefile.toml`: the libraries and the executable, and nothing else. - The code under proof, for example `Clamp.lean`. -- The challenge file, `Spec.lean`: the statements, with `sorry`, and any definition they need besides the code under proof. -- `Proofs.lean`: the proofs, under the same names. +- The challenge file, `Clamp/Spec.lean`: the statements, with `sorry`, and any definition they need besides the code under proof. +- `Clamp/Proofs.lean`: the proofs, under the same names. - `comparator.json`: the challenge and solution modules, every theorem in the challenge file, and the three permitted axioms. - `SPEC.md`: the specification in plain words, including a table from each property to its theorem. - `bar.toml`: the project's status, its page, its spec authors and files, its entry points, the code under proof, each approval, its tests, and any exception to item 4.