gHashTag · gHashTag · Sep 12, 2026 · Sep 12, 2026
@@ -30,7 +30,9 @@ jobs:
         run: python3 -m pip install --quiet pyyaml
 
       - name: Merge-critical workflows must not filter pull_request by branch
-        run: python3 scripts/ci/check_pr_branch_filters.py
+        run: |
+          python3 scripts/ci/check_pr_branch_filters.py --self-test
+          python3 scripts/ci/check_pr_branch_filters.py
 
       # A gate that does not fire is one way to get a green that means nothing;
       # a gate that fires and describes itself as deeper than it is, is another.

@@ -37,6 +37,9 @@ jobs:
     steps:
       - uses: actions/checkout@v6
 
+      - name: Install pyyaml for structural workflow extraction
+        run: python3 -m pip install --quiet pyyaml
+
       - name: The Admitted gate reads every file _CoqProject names, or says it could not
         # #3063. grep answers 0 matched / 1 no match / 2 cannot open, and an
         # `if` merges the last two. Runs here rather than in coq-kernel.yml so

@@ -0,0 +1,10 @@
+# NOW -- Restore topology and Admitted CI (2026-09-12)
+
+## Two existing CI failures (Refs #3574)
+
+- Classify Gate Topology and Untrusted Input Gate as merge-critical in the topology checker and lower the unclassified ceiling from 27 to 26. This changes checker coverage, not GitHub branch protection.
+- Exercise the topology checker against disposable positive and negative workflow trees, including branch filters, missing or malformed classified guards, and growth beyond the unclassified ceiling.
+- Extract the named Admitted step structurally from workflow YAML, require its explicit Bash shell and a unique non-empty body, and execute existing file-population fixtures with GitHub's strict Bash flags.
+- Declare PyYAML in Untrusted Input Gate and test extraction across comments, key ordering, indentation, and invalid or ambiguous step definitions.
+- The explicit PyYAML installation adds one runner-shell step: shell census `run: steps` moves 248 to 249 and `the runner does` moves 227 to 228. Update the shell ledger with this intentional population change; no step is removed or hidden.
+- Validation: all local Gate Topology commands and all 11 Untrusted Input Gate check steps pass. Hosted CI is to be verified on the separate PR; no Coq production step, compiler behavior, specification, or branch-protection setting changes.
@@ -43,7 +43,10 @@
 """
 import glob
 import os
+from pathlib import Path
+import subprocess
 import sys
+import tempfile
 
 try:
     import yaml
@@ -80,6 +83,10 @@
     "corpus-ratchet.yml",
     "withdrawn-live-gate.yml",
     "harness-scratch.yml",
+    # These checks guard CI topology and untrusted workflow inputs themselves.
+    # Omitting them would let a branch filter hide either on a stacked PR.
+    "gate-topology.yml",
+    "untrusted-input-gate.yml",
 )
 
 # The two lists above are a partition ONLY of the files they name. Everything
@@ -97,7 +104,9 @@
 # commit that discovers them and a gate that is red on the day it lands teaches
 # everyone to ignore red. It moves DOWN only: classify a file and lower this in
 # the same commit, so the next unclassified workflow cannot hide in the slack.
-MAX_UNCLASSIFIED = 27
+# Classifying the two guards above takes the live population from 28 to 26.
+# Lower the old ceiling (27), rather than raising it to bless the regression.
+MAX_UNCLASSIFIED = 26
 
 # Not merge-critical, and each exclusion is stated with its reason so that a
 # future reader can disagree with the reason rather than guess at the omission.
@@ -284,5 +293,52 @@ def main():
     return 0
 
 
+def self_test():
+    """Exercise the real checker on disposable workflow trees, not this repo."""
+    script = str(Path(__file__).resolve())
+    clean = "on:\n  pull_request:\njobs: {}\n"
+    failures = []
+
+    def probe(label, edits, expected, diagnostic):
+        with tempfile.TemporaryDirectory(prefix="gate-topology-") as root:
+            workflows = Path(root) / ".github/workflows"
+            workflows.mkdir(parents=True)
+            for name in MERGE_CRITICAL:
+                (workflows / name).write_text(clean)
+            for name, content in edits.items():
+                path = workflows / name
+                if content is None:
+                    path.unlink()
+                else:
+                    path.write_text(content)
+            result = subprocess.run(
+                [sys.executable, script], cwd=root, capture_output=True, text=True,
+                timeout=30,
+            )
+            ok = result.returncode == expected and diagnostic in result.stdout
+            print(f"{'ok' if ok else 'FAIL'}: {label}")
+            if not ok:
+                failures.append(label)
+                print(result.stdout + result.stderr)
+
+    probe("clean classified tree passes", {}, 0, "CLEAN:")
+    for name in ("gate-topology.yml", "untrusted-input-gate.yml"):
+        for key in FILTER_KEYS:
+            probe(
+                f"{name} rejects pull_request.{key}",
+                {name: f"on:\n  pull_request:\n    {key}: [master]\njobs: {{}}\n"},
+                1, f"pull_request.{key}",
+            )
+    probe("missing classified guard fails", {"untrusted-input-gate.yml": None},
+          1, "MISSING")
+    probe("malformed classified guard fails", {"gate-topology.yml": "on: [\n"},
+          1, "UNPARSEABLE MERGE-CRITICAL")
+    at_ceiling = {f"unclassified-{i}.yml": clean for i in range(MAX_UNCLASSIFIED)}
+    probe("existing debt at ceiling passes", at_ceiling, 0, "CLEAN:")
+    probe("one new unclassified workflow fails",
+          {**at_ceiling, "one-too-many.yml": clean}, 1, "UNCLASSIFIED ROSE")
+    return 1 if failures else 0
+
+
 if __name__ == "__main__":
-    sys.exit(main())
+    sys.exit(self_test() if "--self-test" in sys.argv else main())
@@ -15,13 +15,14 @@
 """
 
 import os
-import re
 import shutil
 import subprocess
 import sys
 import tempfile
 from pathlib import Path
 
+import yaml
+
 REPO = Path(__file__).resolve().parents[2]
 WF = REPO / ".github/workflows/coq-kernel.yml"
 STEP = "Verify Kernel PHI layer has no Admitted"
@@ -34,12 +35,79 @@ def check(name, ok, detail=""):
         FAILURES.append(f"{name}: {detail}")
 
 
-def step_body():
-    y = WF.read_text()
-    m = re.search(rf"- name: {re.escape(STEP)}\n        run: \|\n(.*?)(?=\n      - |\n\Z)", y, re.S)
-    if not m:
-        return None
-    return "\n".join(l[10:] if l.startswith(" " * 10) else l for l in m.group(1).split("\n"))
+def step_body(text=None):
+    """Read the actual build step, independent of YAML formatting.
+
+    The old regex required `name` immediately followed by `run`. Adding the
+    required `shell: bash` and its explanation broke extraction. Do not loosen
+    a regex across step boundaries: parse YAML and require one unambiguous step.
+    """
+    doc = yaml.safe_load(WF.read_text() if text is None else text)
+    if not isinstance(doc, dict):
+        raise ValueError("workflow must be a mapping")
+    jobs = doc.get("jobs")
+    build = jobs.get("build") if isinstance(jobs, dict) else None
+    steps = build.get("steps") if isinstance(build, dict) else None
+    if not isinstance(steps, list):
+        raise ValueError("build.steps must be a list")
+    matches = [s for s in steps if isinstance(s, dict) and s.get("name") == STEP]
+    if len(matches) != 1:
+        raise ValueError(f"expected exactly one build step named {STEP!r}, got {len(matches)}")
+    step = matches[0]
+    # The Coq container defaults to sh (dash), which cannot run these arrays.
+    # Running the fixture in bash must not hide a missing workflow shell key.
+    if step.get("shell") != "bash":
+        raise ValueError("the Admitted step must explicitly declare shell: bash")
+    body = step.get("run")
+    if not isinstance(body, str) or not body.strip():
+        raise ValueError("the Admitted step must contain a non-empty run string")
+    return body
+
+
+def extractor_tests():
+    fixture = (
+        "jobs:\n  build:\n    steps:\n"
+        f"      - name: '{STEP}'\n"
+        "        # An explanation between name and run must be harmless.\n"
+        "        shell: bash\n"
+        "        run: |\n"
+        "          printf 'fixture\\n'\n"
+        "      - name: Unrelated sibling\n"
+        "        run: echo not-the-gate\n"
+    )
+    check("comments, quoted names and shell do not hide the body",
+          step_body(fixture) == "printf 'fixture\\n'\n")
+    # A different indentation, key order and block style denote the same step.
+    reordered = {"jobs": {"build": {"steps": [
+        {"run": "echo fixture\n", "shell": "bash", "name": STEP},
+    ]}}}
+    check("key order and indentation do not select another body",
+          step_body(yaml.safe_dump(reordered, indent=4, sort_keys=False)) == "echo fixture\n")
+    step = {"name": STEP, "shell": "bash", "run": "echo fixture"}
+    for label, steps in (
+        ("missing step", []),
+        ("duplicate step", [step, step]),
+        ("missing shell", [{"name": STEP, "run": "echo fixture"}]),
+        ("wrong shell", [{**step, "shell": "sh"}]),
+        ("empty body", [{**step, "run": ""}]),
+        ("non-string body", [{**step, "run": ["echo fixture"]}]),
+    ):
+        rejected = False
+        try:
+            step_body(yaml.safe_dump({"jobs": {"build": {"steps": steps}}}))
+        except ValueError:
+            rejected = True
+        check(f"extractor refuses {label}", rejected)
+    for label, text in (
+        ("malformed YAML", "jobs: ["),
+        ("missing build job", yaml.safe_dump({"jobs": {"other": {"steps": [step]}}})),
+    ):
+        rejected = False
+        try:
+            step_body(text)
+        except (ValueError, yaml.YAMLError):
+            rejected = True
+        check(f"extractor refuses {label}", rejected)
 
 
 # The gate's operand list. Named here rather than taken from `files`, because the
@@ -69,7 +137,10 @@ def arm(body, files, named=OPERANDS):
         for f, c in files.items():
             with open(os.path.join(d, "coq/Kernel", f), "w") as fh:
                 fh.write(c)
-        r = subprocess.run(["bash", "-c", body], capture_output=True, text=True, cwd=d)
+        r = subprocess.run(
+            ["bash", "--noprofile", "--norc", "-eo", "pipefail", "-c", body],
+            capture_output=True, text=True, cwd=d, timeout=30,
+        )
         return r.returncode, r.stdout + r.stderr
     finally:
         shutil.rmtree(d, ignore_errors=True)
@@ -80,12 +151,14 @@ def arm(body, files, named=OPERANDS):
 
 
 def main():
-    body = step_body()
-    check("the step body was found in the workflow", body is not None,
-          f"no step named {STEP!r} with a literal run block -- this test would assert nothing")
-    if body is None:
-        print("\nFAILED:\n  - extractor")
+    FAILURES.clear()
+    extractor_tests()
+    try:
+        body = step_body()
+    except (OSError, ValueError, yaml.YAMLError) as error:
+        print(f"\nFAILED:\n  - extractor: {error}")
         return 1
+    check("the unique bash step body was found in the workflow", True)
 
     rc, out = arm(body, {"Phi.v": CLEAN, "PhiFloat.v": CLEAN})
     check("both files present and clean passes", rc == 0 and "OK: no Admitted" in out, f"rc={rc} out={out!r}")

@@ -2,10 +2,10 @@ WHICH INTERPRETER EACH GATE STEP IS HANDED TO, AND WHO SAYS SO
 
   workflow files read           51
   jobs                          72
-  run: steps                    248
+  run: steps                    249
 
   who names the shell:
-    the runner does             227   no container, so bash -eo pipefail
+    the runner does             228   no container, so bash -eo pipefail
     a `shell:` key does         6
     NOBODY                      15   a container and no `shell:` key