From ad56194366397acdc532960ca962c5e85b17d0b0 Mon Sep 17 00:00:00 2001 From: ahrazzle <38987266+ahrazzle@users.noreply.github.com> Date: Tue, 27 Oct 2026 22:56:39 -0500 Subject: [PATCH 1/2] Check dynamic independent spec reviewers at the current head --- FOUNDING-BRIEF.md | 2 +- MERGE-SOP.md | 2 +- README.md | 2 +- bar/README.md | 11 +++- bar/check.py | 65 ++++++++++--------- bar/reviewers.toml | 11 ---- bar/template/bar.toml | 3 + bar/tests/test_check.py | 132 +++++++++++++++++++++++++++++++++++---- index.html | 2 +- playbook/verified-bar.md | 9 ++- 10 files changed, 181 insertions(+), 58 deletions(-) delete mode 100644 bar/reviewers.toml diff --git a/FOUNDING-BRIEF.md b/FOUNDING-BRIEF.md index f1163a6..22475d7 100644 --- a/FOUNDING-BRIEF.md +++ b/FOUNDING-BRIEF.md @@ -48,7 +48,7 @@ Each project follows the same seven steps. The playbook is public. Each step has A project may use the word verified in public only when all of these hold. The playbook page `playbook/verified-bar.md` says how each one is checked, and `bar/` in this repo holds the checker and the CI workflow every library repo runs. -1. The specification is public, approved by a reviewer on the org's list who did not write it, and pinned. The approval records a hash of the specification, the whole project page, the programs people run, and the tests, and any later change voids it. +1. The specification is public, approved by an independent current repository maintainer, and pinned. The approval records a hash of the specification, the whole project page, the programs people run, and the tests, and any later change voids it. 2. Each public claim names the theorem behind it, and the reviewer has checked that the theorem says what the claim says. 3. One command, `lake comparator --paranoid`, re-checks that the proofs prove exactly the approved statements, with only the standard Lean axioms, under every kernel shipped with Lean. Nothing outside the approved text and the code under proof can change what a statement means. 4. The code that runs is the code that was proved. The programs people run call the proved functions, and project code uses no `implemented_by`, `extern`, `unsafe`, native evaluation, metaprogramming, or `axiom`, and no `sorry` or `admit` outside the statements, except for exceptions the page lists. diff --git a/MERGE-SOP.md b/MERGE-SOP.md index eb88167..ecfb234 100644 --- a/MERGE-SOP.md +++ b/MERGE-SOP.md @@ -5,7 +5,7 @@ A pull request is merged when a maintainer who did not write it approves it. ## Scope This rule applies to every repository in aska-digital, Foundation-0, and Proven-Commons. -Maintainers are the members of the organisation that owns the repository. +Maintainers are repository collaborators with current write, maintain or admin authority. This SOP covers pull requests to main. diff --git a/README.md b/README.md index 00bb792..3ccd63f 100644 --- a/README.md +++ b/README.md @@ -10,7 +10,7 @@ A finished project publishes the library, the specification, a proof a computer A project may use the word verified in public only when all of these hold. The [playbook page](playbook/verified-bar.md) says how each one is checked, and [bar/](bar/) holds the checker, the CI workflow, and a template for a new library. -1. The specification is public, approved by a reviewer on the org's list who did not write it, and pinned. The approval records a hash of the specification, the whole project page, the programs people run, and the tests, and any later change voids it. +1. The specification is public, approved by an independent current repository maintainer, and pinned. The approval records a hash of the specification, the whole project page, the programs people run, and the tests, and any later change voids it. 2. Each public claim names the theorem behind it, and the reviewer has checked that the theorem says what the claim says. 3. One command, `lake comparator --paranoid`, re-checks that the proofs prove exactly the approved statements, with only the standard Lean axioms, under every kernel shipped with Lean. Nothing outside the approved text and the code under proof can change what a statement means. 4. The code that runs is the code that was proved. The programs people run call the proved functions, and project code uses no `implemented_by`, `extern`, `unsafe`, native evaluation, metaprogramming, or `axiom`, and no `sorry` or `admit` outside the statements, except for exceptions the page lists. diff --git a/bar/README.md b/bar/README.md index 0d7008f..248c599 100644 --- a/bar/README.md +++ b/bar/README.md @@ -28,7 +28,7 @@ It prints one row per bar item, with PASS, FAIL, OPEN, or SKIP. It exits 1 if an ## Record an approval -GitHub does not let people approve their own pull requests, so the reviewer approves one that someone else opens: +Reviewers are selected dynamically. An approving reviewer must currently have write, maintain or admin access to the owning repository. They must be neither a listed spec author nor an author or committer of a spec-file commit. The approval pull request must be opened by someone else. There is no fixed reviewer roster. 1. Anyone but the reviewer opens a pull request that adds the approval to `bar.toml`. The hash comes from: @@ -47,7 +47,7 @@ GitHub does not let people approve their own pull requests, so the reviewer appr ``` Until the review lands, item 1 reads OPEN. -2. The reviewer reviews the spec, checks the hash, and approves that pull request on GitHub. The review starts a new run of the check, which confirms it. +2. The reviewer reviews the spec, checks the hash, and approves the current head of that pull request on GitHub. A later commit needs a fresh approval even if the covered hash is unchanged. A later request for changes or dismissal cancels an earlier approval. The review starts a new run of the check, which confirms it. 3. Merge it without pushing anything more to it. A push after the approval leaves the approved text behind, and a branch rule that dismisses stale approvals would dismiss it. ## Run the self-tests @@ -58,3 +58,10 @@ BAR_LEAN=1 python3 -m unittest discover -s bar/tests -k LeanTest -v ``` The second line builds the template and runs `lake comparator` on planted faults: a weakened statement, a `sorry`, and an `implemented_by` that the kernels cannot see but the source rule catches. Run `lake build` in `template/` first. + +The online authority check reads the reviewer's current repository +permission from GitHub. It needs no fixed roster or organisation-wide +membership token. Unknown or unreadable permission never passes item 1; +`--offline` leaves it skipped. The existing spec hash still binds every +covered file, and the approved commit must itself contain the matching +approval record. diff --git a/bar/check.py b/bar/check.py index a775610..516909e 100644 --- a/bar/check.py +++ b/bar/check.py @@ -44,11 +44,6 @@ BAR_VERSION = "2" STANDARD_AXIOMS = {"propext", "Classical.choice", "Quot.sound"} -# People the org has named as spec reviewers, one GitHub login each. Kept -# next to this script so a library cannot add to it; only a change to -# this repo can. -REVIEWERS_FILE = Path(__file__).resolve().parent / "reviewers.toml" - # Limit for each long step (the proof check, the tests), in seconds. CI # sets it so both steps fit inside the job's own limit. STEP_TIMEOUT = int(os.environ.get("BAR_STEP_TIMEOUT_MINUTES", "120")) * 60 @@ -442,7 +437,7 @@ def git_spec_authors(root, files): """Names and emails of everyone who committed to the spec files.""" try: out = subprocess.run( - ["git", "log", "--format=%an%x00%ae", "--", *files], cwd=root, + ["git", "log", "--format=%an%x00%ae%n%cn%x00%ce", "--", *files], cwd=root, capture_output=True, text=True, timeout=60) except (OSError, subprocess.TimeoutExpired): return None @@ -462,7 +457,7 @@ def git_prefix(root): class GitHub: - """The two GitHub API reads the approval check needs.""" + """Live repository authority, review and source checks.""" def get(self, path, raw=False): headers = {"Accept": "application/vnd.github.raw" if raw else "application/vnd.github+json", @@ -475,6 +470,15 @@ def get(self, path, raw=False): body = r.read() return body.decode("utf-8") if raw else json.loads(body) + def pull_request(self, owner, repo, number): + return self.get(f"/repos/{owner}/{repo}/pulls/{number}") + + def is_maintainer(self, owner, repo, login): + """Current repository write authority; no fixed roster or org token.""" + permission = self.get(f"/repos/{owner}/{repo}/collaborators/" + f"{urllib.parse.quote(login, safe='')}/permission") + return isinstance(permission, dict) and permission.get("permission") in {"write", "maintain", "admin"} + def reviews(self, owner, repo, number): found, page = [], 1 while True: @@ -484,12 +488,13 @@ def reviews(self, owner, repo, number): return found page += 1 - def commit_logins(self, owner, repo, path): + def commit_logins(self, owner, repo, path, ref=None): """GitHub logins of the authors and committers of every commit to a path.""" logins, page = set(), 1 + revision = f"&sha={urllib.parse.quote(ref, safe='')}" if ref else "" while True: batch = self.get(f"/repos/{owner}/{repo}/commits?path={urllib.parse.quote(path)}" - f"&per_page=100&page={page}") + f"&per_page=100&page={page}{revision}") for c in batch: for who in ("author", "committer"): login = (c.get(who) or {}).get("login") @@ -567,11 +572,6 @@ def check_spec(root, bar, rep, offline, github): if not reviewer or reviewer.lower() in authors: rep.add(1, "FAIL", f"the approving reviewer '{reviewer}' is listed as a spec author") return - named = reviewer_list() - if reviewer.lower() not in named: - rep.unmet(1, f"'{reviewer}' is not on the org's list of spec reviewers " - f"(bar/reviewers.toml in Proven-Commons/mission, {len(named)} named)") - return committers = git_spec_authors(root, files) or [] if any(re.search(rf"(^|[\x00+]){re.escape(reviewer.lower())}([\x00@]|$)", c.lower()) for c in committers): @@ -595,16 +595,34 @@ def check_spec(root, bar, rep, offline, github): if (github.parent(here) or "").lower() != f"{owner}/{repo}".lower(): rep.add(1, "FAIL", f"{said}; the pull request is not in {here} or the repo it was forked from") return + if not github.is_maintainer(owner, repo, reviewer): + rep.unmet(1, f"{said}; {reviewer} is not a current maintainer of {owner}/{repo}") + return + pull = github.pull_request(owner, repo, number) + if str((pull.get("user") or {}).get("login", "")).lower() == reviewer.lower(): + rep.add(1, "FAIL", f"{said}; the reviewer authored the approval pull request") + return + head = (pull.get("head") or {}).get("sha") + if not head: + rep.add(1, "SKIP", f"{said}; GitHub did not return the pull request head") + return for rel in files: - if reviewer.lower() in github.commit_logins(owner, repo, prefix + rel): + if reviewer.lower() in github.commit_logins(owner, repo, prefix + rel, ref=head): rep.add(1, "FAIL", f"{said}; GitHub shows {reviewer} as an author of a commit to {rel}") return reviews = github.reviews(owner, repo, number) - mine = [r for r in reviews if r.get("state") == "APPROVED" - and str((r.get("user") or {}).get("login", "")).lower() == reviewer.lower()] - if not mine: - rep.unmet(1, f"{said}; GitHub shows no approving review by {reviewer} on that pull request yet") + mine = [r for r in reviews + if str((r.get("user") or {}).get("login", "")).lower() == reviewer.lower() + and r.get("state") in {"APPROVED", "CHANGES_REQUESTED", "DISMISSED"}] + latest = max(enumerate(mine), key=lambda pair: ( + pair[1].get("submitted_at") or "", pair[1].get("id") or 0, pair[0]))[1] if mine else None + if not latest or latest.get("state") != "APPROVED": + rep.unmet(1, f"{said}; GitHub shows no current approving review by {reviewer} on that pull request") + return + if latest.get("commit_id") != head: + rep.unmet(1, f"{said}; the approving review is not on the pull request's current head") return + mine = [latest] # The review must be of this exact text: hash the spec as it was # at the commit the reviewer approved. for r in mine: @@ -626,15 +644,6 @@ def check_spec(root, bar, rep, offline, github): rep.unmet(1, f"{said}; the text {reviewer} approved on GitHub is not the text this hash covers") -def reviewer_list(path=None): - path = Path(path or os.environ.get("BAR_REVIEWERS") or REVIEWERS_FILE) - try: - data = tomllib.loads(read_text(path)) - except (OSError, tomllib.TOMLDecodeError, UnicodeDecodeError): - return set() - return {str(r.get("login", "")).lower() for r in data.get("reviewer", []) if isinstance(r, dict)} - - def backing(rep): """How the person-judged part of an item stands, from item 1.""" row = next((r for r in rep.rows if r["item"] == 1), None) diff --git a/bar/reviewers.toml b/bar/reviewers.toml deleted file mode 100644 index a3ef400..0000000 --- a/bar/reviewers.toml +++ /dev/null @@ -1,11 +0,0 @@ -# The people the org has named as spec reviewers, by GitHub login. A -# spec approval counts only when its reviewer is listed here. Only a -# pull request to this repo can change the list, and the org's head of -# verification approves each change. -# -# The list is empty until the first reviewers are named -# (FOUNDING-BRIEF.md, "Decisions needed now"). -# -# [[reviewer]] -# login = "github-handle" -# since = "2026-11-01" diff --git a/bar/template/bar.toml b/bar/template/bar.toml index ac8f572..aa93b3f 100644 --- a/bar/template/bar.toml +++ b/bar/template/bar.toml @@ -23,6 +23,9 @@ files = ["SPEC.md", "Spec.lean"] code = ["Clamp.clamp"] # Add one entry per approval, in the pull request the reviewer approves. +# Choose an independent current maintainer dynamically, not from a roster. +# The reviewer must approve the current head and must not be a spec author +# or committer, or the author of this approval pull request. # `sha256` is what `python3 check.py --spec-hash ` prints for the # reviewed text. Any later change to that text voids the approval. # diff --git a/bar/tests/test_check.py b/bar/tests/test_check.py index 87a5e26..efc1d89 100644 --- a/bar/tests/test_check.py +++ b/bar/tests/test_check.py @@ -70,13 +70,22 @@ class FakeGitHub: """Reviews on one pull request, each made at a commit whose files are a snapshot of the project.""" - def __init__(self, login, files, state="APPROVED", forks=None, committers=()): + def __init__(self, login, files, state="APPROVED", forks=None, committers=(), maintainer=True, author="example-author", head=None): self.review = {"state": state, "user": {"login": login}, "commit_id": "c0ffee" * 6} self.files = files self.forks = forks or {} self.committers = {c.lower() for c in committers} + self.maintainer = maintainer + self.author = author + self.head = head or self.review["commit_id"] - def commit_logins(self, owner, repo, path): + def is_maintainer(self, owner, repo, login): + return self.maintainer + + def pull_request(self, owner, repo, number): + return {"user": {"login": self.author}, "head": {"sha": self.head}} + + def commit_logins(self, owner, repo, path, ref=None): return self.committers required = {"bar / bar"} @@ -100,6 +109,54 @@ def approved_by(project, login="reviewer-b"): return FakeGitHub(login, project.snapshot()) +class MaintainerAPITest(unittest.TestCase): + def test_write_maintain_and_admin_are_current_maintainers(self): + for role in ("write", "maintain", "admin"): + with self.subTest(role=role): + github = check.GitHub() + github.get = mock.Mock(return_value={"permission": role}) + self.assertTrue(github.is_maintainer("Org", "repo", "Reviewer")) + self.assertEqual(github.get.call_args.args[0], "/repos/Org/repo/collaborators/Reviewer/permission") + + def test_read_triage_and_no_access_cannot_approve(self): + for role in ("read", "triage", "none", "unknown", None): + with self.subTest(role=role): + github = check.GitHub() + github.get = mock.Mock(return_value={"permission": role}) + self.assertFalse(github.is_maintainer("Org", "repo", "reviewer")) + self.assertEqual(github.get.call_count, 1) + + def test_missing_permission_is_not_maintainer_authority(self): + github = check.GitHub() + github.get = mock.Mock(return_value={}) + self.assertFalse(github.is_maintainer("Org", "repo", "reviewer")) + + def test_malformed_permission_response_is_not_authority(self): + github = check.GitHub() + for response in (None, "write", []): + with self.subTest(response=response): + github.get = mock.Mock(return_value=response) + self.assertFalse(github.is_maintainer("Org", "repo", "reviewer")) + + def test_spec_commit_history_uses_the_approved_head(self): + github = check.GitHub() + github.get = mock.Mock(return_value=[]) + github.commit_logins("Org", "repo", "SPEC.md", ref="current-head") + self.assertIn("&sha=current-head", github.get.call_args.args[0]) + + def test_authority_api_errors_do_not_establish_permission(self): + github = check.GitHub() + github.get = mock.Mock(side_effect=OSError("authority API unavailable")) + with self.assertRaises(OSError): + github.is_maintainer("Org", "repo", "reviewer") + + def test_github_commit_logins_include_authors_and_committers(self): + github = check.GitHub() + github.get = mock.Mock(return_value=[{"author": {"login": "Writer"}, + "committer": {"login": "Committer"}}]) + self.assertEqual(github.commit_logins("Org", "repo", "SPEC.md"), {"writer", "committer"}) + + class CheckTest(unittest.TestCase): def setUp(self): self.p = Project() @@ -108,10 +165,6 @@ def setUp(self): env.start() self.addCleanup(env.stop) os.environ.pop("GITHUB_REPOSITORY", None) - # The org's reviewer list, for these tests. - reviewers = Path(self.p.tmp.name) / "reviewers.toml" - reviewers.write_text('[[reviewer]]\nlogin = "reviewer-b"\n[[reviewer]]\nlogin = "example-author"\n') - os.environ["BAR_REVIEWERS"] = str(reviewers) def tearDown(self): self.p.close() @@ -208,13 +261,67 @@ def test_exact_duplicate_section_is_covered(self): secs = check.sections((self.p.root / "README.md").read_text()) self.assertIn("It is also fast.", check.find_section(secs, "What is proved")) - def test_reviewer_not_on_the_org_list_is_open_then_fails(self): + def test_reviewer_without_current_repo_authority_is_open_then_fails(self): self.p.approve(reviewer="sock-puppet") - got = self.p.run(offline=False, github=approved_by(self.p, "sock-puppet")) + got = self.p.run(offline=False, github=FakeGitHub("sock-puppet", self.p.snapshot(), maintainer=False)) self.assertEqual(got[1][0], "OPEN") - self.assertIn("not on the org's list", got[1][1]) + self.assertIn("not a current maintainer", got[1][1]) self.p.edit("bar.toml", 'status = "in-progress"', 'status = "verified"') - self.assertEqual(self.status(1, offline=False, github=approved_by(self.p, "sock-puppet")), "FAIL") + self.assertEqual(self.status(1, offline=False, github=FakeGitHub("sock-puppet", self.p.snapshot(), maintainer=False)), "FAIL") + + def test_static_reviewer_list_environment_has_no_authority(self): + self.p.approve() + with mock.patch.dict(os.environ, {"BAR_REVIEWERS": "/no-such-static-roster"}): + self.assertEqual(self.status(1, offline=False, github=approved_by(self.p)), "PASS") + + def test_any_independent_current_maintainer_can_approve(self): + self.p.approve(reviewer="new-maintainer") + github = FakeGitHub("NEW-MAINTAINER", self.p.snapshot()) + self.assertEqual(self.status(1, offline=False, github=github), "PASS") + + def test_pull_request_author_cannot_approve(self): + self.p.approve() + github = FakeGitHub("reviewer-b", self.p.snapshot(), author="Reviewer-B") + self.assertEqual(self.status(1, offline=False, github=github), "FAIL") + + def test_additional_spec_author_cannot_approve(self): + self.p.edit("bar.toml", 'spec_authors = ["example-author"]', + 'spec_authors = ["example-author", "Reviewer-B"]') + self.p.approve() + self.assertEqual(self.status(1, offline=False, github=approved_by(self.p)), "FAIL") + + def test_approval_on_previous_head_does_not_count_even_with_same_hash(self): + self.p.approve() + github = FakeGitHub("reviewer-b", self.p.snapshot(), head="new-head") + status, detail = self.p.run(offline=False, github=github)[1] + self.assertEqual(status, "OPEN") + self.assertIn("current head", detail) + + def test_later_request_for_changes_overrides_an_approval(self): + self.p.approve() + github = approved_by(self.p) + approved = dict(github.review, id=1) + changed = dict(github.review, id=2, state="CHANGES_REQUESTED") + github.reviews = lambda *args: [changed, approved] + self.assertEqual(self.status(1, offline=False, github=github), "OPEN") + + def test_later_comment_does_not_replace_an_approval_verdict(self): + self.p.approve() + github = approved_by(self.p) + approved = dict(github.review, id=1) + comment = dict(github.review, id=2, state="COMMENTED") + github.reviews = lambda *args: [approved, comment] + self.assertEqual(self.status(1, offline=False, github=github), "PASS") + + def test_local_spec_committer_cannot_approve(self): + import subprocess + git = ["git", "-C", str(self.p.root)] + subprocess.run(git + ["init", "-q"], check=True) + subprocess.run(git + ["add", "SPEC.md"], check=True) + subprocess.run(git + ["-c", "user.name=reviewer-b", "-c", "user.email=reviewer-b@example.org", + "commit", "-q", "--author=Someone ", "-m", "spec"], check=True) + self.p.approve() + self.assertEqual(self.status(1, offline=False, github=approved_by(self.p)), "FAIL") def test_reviewer_who_authored_a_spec_commit_on_github_fails(self): self.p.approve() @@ -258,7 +365,10 @@ def test_github_error_is_skipped_not_passed(self): self.p.approve() class Broken: - def commit_logins(self, owner, repo, path): + def is_maintainer(self, owner, repo, login): + raise OSError("network down") + + def commit_logins(self, owner, repo, path, ref=None): raise OSError("network down") def reviews(self, owner, repo, number): diff --git a/index.html b/index.html index 56f0014..47103c7 100644 --- a/index.html +++ b/index.html @@ -646,7 +646,7 @@

A reviewed, pinned specification

- A reviewer on the org's list, who did not write it, approves + An independent current repository maintainer approves what the code is meant to do. The approval records a hash, and any later change voids it.

diff --git a/playbook/verified-bar.md b/playbook/verified-bar.md index b345523..519e946 100644 --- a/playbook/verified-bar.md +++ b/playbook/verified-bar.md @@ -6,7 +6,7 @@ A project may use the word verified in public only when every item below holds. ## The items -1. **The specification is public, approved by a reviewer apart from the author, and pinned.** The specification is `SPEC.md` in plain words and a Lean file of theorem statements with `sorry` where the proofs go, called the challenge file. A reviewer on the org's list of spec reviewers, who wrote neither, approves them. The approval also covers `comparator.json`, the programs people run, the test generator, the list of code under proof, and the whole project page, since a claim anywhere on the page is a public claim. The approval is the reviewer's approving review of the GitHub pull request that records it in `bar.toml`, with the SHA-256 of what was approved. Any later change to any of it voids the approval until a reviewer approves the new text. +1. **The specification is public, approved by a reviewer apart from the author, and pinned.** The specification is `SPEC.md` in plain words and a Lean file of theorem statements with `sorry` where the proofs go, called the challenge file. An independent current maintainer of the owning repository approves them. The reviewer must have write, maintain or admin repository access, and must have neither authored nor committed the spec. No fixed roster is used. The approval also covers `comparator.json`, the programs people run, the test generator, the list of code under proof, and the whole project page, since a claim anywhere on the page is a public claim. The approval is the reviewer's approving review of the GitHub pull request that records it in `bar.toml`, with the SHA-256 of what was approved. Any later change to any of it voids the approval until a reviewer approves the new text. 2. **Each public claim names the theorem behind it, and the theorem says what the claim says.** What is proved is a table of claims in plain words, each with its theorem. The reviewer reads each statement against its claim and tries to write a wrong program that still meets the statement. If one exists, the statement is too weak. A safety statement also holds for a program that does nothing, so the specification pairs each one with a statement that such a program fails, or the page says that usefulness rests on tests alone. @@ -33,7 +33,7 @@ A run exits 1 when an item fails, or when `bar.toml` says `verified` and any ite | Item | What the machine checks | What only a person can judge | |------|-------------------------|------------------------------| -| 1 | The recorded hash equals the hash of what the approval covers now. The reviewer is on `bar/reviewers.toml` in this repo, is not a listed spec author, and is not the GitHub author of any commit to the spec files. GitHub shows the reviewer's approving review of the pull request that added this approval to `bar.toml`, at a commit where the covered text had this same hash. | Whether the specification is right. | +| 1 | The recorded hash equals the hash of what the approval covers now. The reviewer currently has write, maintain or admin access to the owning repository, is not any listed spec author, and is not an author or committer of any commit to the spec files or the author of the approval pull request. GitHub shows the reviewer's approving review of the pull request that added this approval to `bar.toml`, on its current head, where the covered text has this same hash. A later request for changes or dismissal invalidates an earlier approval. | Whether the specification is right. | | 2 | Every theorem in `comparator.json` is named under What is proved. | Whether each statement says what its claim says, whether a wrong program can meet it, and whether a program that does nothing can. | | 3 | `lake comparator --paranoid` passes. Only the three standard axioms are permitted. The challenge file is one of the spec files, and `comparator.json` names every theorem in it. A walk over each statement, in a sandbox, finds no project definition or instance outside the spec files and the code under proof, and finds some code under proof. The toolchain is pinned. | Whether the list of code under proof is right. | | 4 | No forbidden feature or metaprogramming appears outside comments and strings, and `lakefile.toml` uses only allowed keys, except for listed exceptions. It lists the instance declarations outside the challenge file. | Whether the programs people run call the proved functions, and whether an instance changes what a statement means. | @@ -97,3 +97,8 @@ Lean 4.35 ships the tools this bar rests on: `lake comparator` and five kernels - Whether the specification is the right one. That stays a person's judgment, which is why the reviewer must not be the author. - Speed. - The checker itself, and this repo. Every library runs the checker from here, so this repo's main branch needs the same protection as a release, and each library pins the version it runs. + +Choose the spec reviewer for each piece of work from the repository's +current maintainers. A maintainer has write, maintain or admin permission. +The checker reads that permission live; a fixed list in mission does not +grant review authority. Unknown or unreadable permissions do not pass. From 8df261fd3dc042d9dbe0b370b4792d24673424fa Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 29 Oct 2026 19:58:16 +0000 Subject: [PATCH 2/2] Keep MERGE-SOP as is and say who can confirm item 1 MERGE-SOP keeps its definition of a maintainer; the spec reviewer is now described by access instead (current write, maintain or admin access to the library's repository), so the word does not mean two things. A 403 from the collaborator-permission endpoint now gives a SKIP that says a token with push access is needed and to read item 1 from the library's CI run, and bar/README.md says the same. The playbook moves reviewer selection under item 1 and says, under what the bar does not cover, that any repo admin can make an account eligible and that removing access voids that reviewer's approvals. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01QwrvNdsMA6RtgKxXn1Pmhf --- FOUNDING-BRIEF.md | 2 +- MERGE-SOP.md | 2 +- README.md | 2 +- bar/README.md | 12 ++++++++---- bar/check.py | 13 +++++++++++-- bar/template/bar.toml | 3 ++- bar/tests/test_check.py | 14 +++++++++++++- index.html | 2 +- playbook/verified-bar.md | 9 +++------ 9 files changed, 41 insertions(+), 18 deletions(-) diff --git a/FOUNDING-BRIEF.md b/FOUNDING-BRIEF.md index 22475d7..9f07abc 100644 --- a/FOUNDING-BRIEF.md +++ b/FOUNDING-BRIEF.md @@ -48,7 +48,7 @@ Each project follows the same seven steps. The playbook is public. Each step has A project may use the word verified in public only when all of these hold. The playbook page `playbook/verified-bar.md` says how each one is checked, and `bar/` in this repo holds the checker and the CI workflow every library repo runs. -1. The specification is public, approved by an independent current repository maintainer, and pinned. The approval records a hash of the specification, the whole project page, the programs people run, and the tests, and any later change voids it. +1. The specification is public, approved by an independent reviewer with current write, maintain or admin access to the library's repository, and pinned. The approval records a hash of the specification, the whole project page, the programs people run, and the tests, and any later change voids it. 2. Each public claim names the theorem behind it, and the reviewer has checked that the theorem says what the claim says. 3. One command, `lake comparator --paranoid`, re-checks that the proofs prove exactly the approved statements, with only the standard Lean axioms, under every kernel shipped with Lean. Nothing outside the approved text and the code under proof can change what a statement means. 4. The code that runs is the code that was proved. The programs people run call the proved functions, and project code uses no `implemented_by`, `extern`, `unsafe`, native evaluation, metaprogramming, or `axiom`, and no `sorry` or `admit` outside the statements, except for exceptions the page lists. diff --git a/MERGE-SOP.md b/MERGE-SOP.md index ecfb234..eb88167 100644 --- a/MERGE-SOP.md +++ b/MERGE-SOP.md @@ -5,7 +5,7 @@ A pull request is merged when a maintainer who did not write it approves it. ## Scope This rule applies to every repository in aska-digital, Foundation-0, and Proven-Commons. -Maintainers are repository collaborators with current write, maintain or admin authority. +Maintainers are the members of the organisation that owns the repository. This SOP covers pull requests to main. diff --git a/README.md b/README.md index 3ccd63f..0e5ce21 100644 --- a/README.md +++ b/README.md @@ -10,7 +10,7 @@ A finished project publishes the library, the specification, a proof a computer A project may use the word verified in public only when all of these hold. The [playbook page](playbook/verified-bar.md) says how each one is checked, and [bar/](bar/) holds the checker, the CI workflow, and a template for a new library. -1. The specification is public, approved by an independent current repository maintainer, and pinned. The approval records a hash of the specification, the whole project page, the programs people run, and the tests, and any later change voids it. +1. The specification is public, approved by an independent reviewer with current write, maintain or admin access to the library's repository, and pinned. The approval records a hash of the specification, the whole project page, the programs people run, and the tests, and any later change voids it. 2. Each public claim names the theorem behind it, and the reviewer has checked that the theorem says what the claim says. 3. One command, `lake comparator --paranoid`, re-checks that the proofs prove exactly the approved statements, with only the standard Lean axioms, under every kernel shipped with Lean. Nothing outside the approved text and the code under proof can change what a statement means. 4. The code that runs is the code that was proved. The programs people run call the proved functions, and project code uses no `implemented_by`, `extern`, `unsafe`, native evaluation, metaprogramming, or `axiom`, and no `sorry` or `admit` outside the statements, except for exceptions the page lists. diff --git a/bar/README.md b/bar/README.md index 248c599..2682453 100644 --- a/bar/README.md +++ b/bar/README.md @@ -16,7 +16,7 @@ lake build python3 /bar/check.py . --run-tests ``` -It prints one row per bar item, with PASS, FAIL, OPEN, or SKIP. It exits 1 if any item failed, or if `bar.toml` says `verified` and any item did not pass. `--no-lean` skips the proof check, and `--offline` skips asking GitHub to confirm the spec approval. A skipped item is never a pass. +It prints one row per bar item, with PASS, FAIL, OPEN, or SKIP. It exits 1 if any item failed, or if `bar.toml` says `verified` and any item did not pass. `--no-lean` skips the proof check, and `--offline` skips asking GitHub to confirm the spec approval. A skipped item is never a pass. Confirming the approval needs a token with push access to the library (see below), so anyone else reads item 1 from the library's CI run. ## Start a library @@ -59,9 +59,13 @@ BAR_LEAN=1 python3 -m unittest discover -s bar/tests -k LeanTest -v The second line builds the template and runs `lake comparator` on planted faults: a weakened statement, a `sorry`, and an `implemented_by` that the kernels cannot see but the source rule catches. Run `lake build` in `template/` first. -The online authority check reads the reviewer's current repository -permission from GitHub. It needs no fixed roster or organisation-wide -membership token. Unknown or unreadable permission never passes item 1; +The online check of item 1 reads the reviewer's current permission on the +library's repository from GitHub. It needs no fixed roster or +organisation-wide membership token, but GitHub shows a collaborator's +permission only to a token with push access to that repository. The +library's own CI token has it, so read item 1 from the library's CI run. A +run with any other token, a stranger's or a fork's, reports item 1 as SKIP +and says why. Unknown or unreadable permission never passes item 1; `--offline` leaves it skipped. The existing spec hash still binds every covered file, and the approved commit must itself contain the matching approval record. diff --git a/bar/check.py b/bar/check.py index 516909e..d666eae 100644 --- a/bar/check.py +++ b/bar/check.py @@ -37,6 +37,7 @@ import subprocess import sys import tomllib +import urllib.error import urllib.parse import urllib.request from pathlib import Path @@ -595,8 +596,16 @@ def check_spec(root, bar, rep, offline, github): if (github.parent(here) or "").lower() != f"{owner}/{repo}".lower(): rep.add(1, "FAIL", f"{said}; the pull request is not in {here} or the repo it was forked from") return - if not github.is_maintainer(owner, repo, reviewer): - rep.unmet(1, f"{said}; {reviewer} is not a current maintainer of {owner}/{repo}") + try: + maintainer = github.is_maintainer(owner, repo, reviewer) + except urllib.error.HTTPError as e: + if e.code != 403: + raise + rep.add(1, "SKIP", f"{said}; GitHub shows a collaborator's permission only to a token with " + f"push access to {owner}/{repo} (HTTP 403), so read item 1 from the library's CI run") + return + if not maintainer: + rep.unmet(1, f"{said}; {reviewer} has no current write, maintain or admin access to {owner}/{repo}") return pull = github.pull_request(owner, repo, number) if str((pull.get("user") or {}).get("login", "")).lower() == reviewer.lower(): diff --git a/bar/template/bar.toml b/bar/template/bar.toml index aa93b3f..a42e1db 100644 --- a/bar/template/bar.toml +++ b/bar/template/bar.toml @@ -23,7 +23,8 @@ files = ["SPEC.md", "Spec.lean"] code = ["Clamp.clamp"] # Add one entry per approval, in the pull request the reviewer approves. -# Choose an independent current maintainer dynamically, not from a roster. +# Choose an independent reviewer with current write, maintain or admin +# access to this repository; there is no fixed roster. # The reviewer must approve the current head and must not be a spec author # or committer, or the author of this approval pull request. # `sha256` is what `python3 check.py --spec-hash ` prints for the diff --git a/bar/tests/test_check.py b/bar/tests/test_check.py index efc1d89..a33e8c3 100644 --- a/bar/tests/test_check.py +++ b/bar/tests/test_check.py @@ -17,6 +17,7 @@ import shutil import tempfile import unittest +import urllib.error from pathlib import Path from unittest import mock @@ -265,7 +266,7 @@ def test_reviewer_without_current_repo_authority_is_open_then_fails(self): self.p.approve(reviewer="sock-puppet") got = self.p.run(offline=False, github=FakeGitHub("sock-puppet", self.p.snapshot(), maintainer=False)) self.assertEqual(got[1][0], "OPEN") - self.assertIn("not a current maintainer", got[1][1]) + self.assertIn("no current write, maintain or admin access", got[1][1]) self.p.edit("bar.toml", 'status = "in-progress"', 'status = "verified"') self.assertEqual(self.status(1, offline=False, github=FakeGitHub("sock-puppet", self.p.snapshot(), maintainer=False)), "FAIL") @@ -377,6 +378,17 @@ def reviews(self, owner, repo, number): self.assertEqual(got[1][0], "SKIP") self.assertIn("network down", got[1][1]) + def test_permission_hidden_without_push_access_is_skipped_with_the_reason(self): + self.p.approve() + + class NoPush: + def is_maintainer(self, owner, repo, login): + raise urllib.error.HTTPError("https://api.github.com/x", 403, "Forbidden", None, None) + got = self.p.run(offline=False, github=NoPush()) + self.assertEqual(got[1][0], "SKIP") + self.assertIn("push access", got[1][1]) + self.assertIn("CI run", got[1][1]) + def test_record_that_is_not_a_pull_request_fails(self): self.p.approve(record="approved in a call") self.assertEqual(self.status(1, offline=False, github=approved_by(self.p)), "FAIL") diff --git a/index.html b/index.html index 47103c7..99c55a6 100644 --- a/index.html +++ b/index.html @@ -646,7 +646,7 @@

A reviewed, pinned specification

- An independent current repository maintainer approves + An independent reviewer with write access to the repository approves what the code is meant to do. The approval records a hash, and any later change voids it.

diff --git a/playbook/verified-bar.md b/playbook/verified-bar.md index 519e946..e8fcf99 100644 --- a/playbook/verified-bar.md +++ b/playbook/verified-bar.md @@ -6,7 +6,7 @@ A project may use the word verified in public only when every item below holds. ## The items -1. **The specification is public, approved by a reviewer apart from the author, and pinned.** The specification is `SPEC.md` in plain words and a Lean file of theorem statements with `sorry` where the proofs go, called the challenge file. An independent current maintainer of the owning repository approves them. The reviewer must have write, maintain or admin repository access, and must have neither authored nor committed the spec. No fixed roster is used. The approval also covers `comparator.json`, the programs people run, the test generator, the list of code under proof, and the whole project page, since a claim anywhere on the page is a public claim. The approval is the reviewer's approving review of the GitHub pull request that records it in `bar.toml`, with the SHA-256 of what was approved. Any later change to any of it voids the approval until a reviewer approves the new text. +1. **The specification is public, approved by a reviewer apart from the author, and pinned.** The specification is `SPEC.md` in plain words and a Lean file of theorem statements with `sorry` where the proofs go, called the challenge file. An independent reviewer approves them: someone with current write, maintain or admin access to the owning repository, who has neither authored nor committed the spec. No fixed roster is used, and the checker reads that access live, so choose the reviewer for each piece of work from the people who have it. Unknown or unreadable access does not pass. The approval also covers `comparator.json`, the programs people run, the test generator, the list of code under proof, and the whole project page, since a claim anywhere on the page is a public claim. The approval is the reviewer's approving review of the GitHub pull request that records it in `bar.toml`, with the SHA-256 of what was approved. Any later change to any of it voids the approval until a reviewer approves the new text. 2. **Each public claim names the theorem behind it, and the theorem says what the claim says.** What is proved is a table of claims in plain words, each with its theorem. The reviewer reads each statement against its claim and tries to write a wrong program that still meets the statement. If one exists, the statement is too weak. A safety statement also holds for a program that does nothing, so the specification pairs each one with a statement that such a program fails, or the page says that usefulness rests on tests alone. @@ -97,8 +97,5 @@ Lean 4.35 ships the tools this bar rests on: `lake comparator` and five kernels - Whether the specification is the right one. That stays a person's judgment, which is why the reviewer must not be the author. - Speed. - The checker itself, and this repo. Every library runs the checker from here, so this repo's main branch needs the same protection as a release, and each library pins the version it runs. - -Choose the spec reviewer for each piece of work from the repository's -current maintainers. A maintainer has write, maintain or admin permission. -The checker reads that permission live; a fixed list in mission does not -grant review authority. Unknown or unreadable permissions do not pass. +- Who may review. Any admin of a library repository can make an account, an agent's included, eligible to approve its spec by giving it write access. No change to this repo is needed for that. +- Approvals after access ends. Item 1 reads the reviewer's access when the check runs, so removing a reviewer's write access later voids every approval they gave, and a library marked verified then fails its CI until someone with access approves again.