Check dynamic independent spec reviewers at the current head

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 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.

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 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.

bar/README.md

@@ -16,7 +16,7 @@ lake build
 python3 <mission>/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
 
@@ -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,14 @@ 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 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.

bar/check.py

@@ -37,18 +37,14 @@
 import subprocess
 import sys
 import tomllib
+import urllib.error
 import urllib.parse
 import urllib.request
 from pathlib import Path
 
 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 +438,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 +458,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 +471,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 +489,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 +573,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 +596,42 @@ 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
+        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():
+            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 +653,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)

bar/template/bar.toml

@@ -23,6 +23,10 @@ files = ["SPEC.md", "Spec.lean"]
 code = ["Clamp.clamp"]
 
 # Add one entry per approval, in the pull request the reviewer approves.
+# 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 <repo>` prints for the
 # reviewed text. Any later change to that text voids the approval.
 #