From e4dd210fc3ef0c661717349bf119b85de1d7a704 Mon Sep 17 00:00:00 2001 From: Claude Code Date: Fri, 7 Aug 2026 20:10:02 +0300 Subject: [PATCH] Proof: the corpus lane refuses a campaign it does not belong to (V5b2d-4m) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Гвард в координаторе не защищает устаревший координатор: старый файл несёт старый контракт целиком. Сегодня это стоило двух массовых диспатчей — 133 прогона от забытого `--dry-run` и 69 от исполнения чекаута, где полярность флага была прежней. Оба раза правило существовало и оба раза не исполнялось той копией, которая отправляла диспатчи. Поэтому инвариант переносится туда, где код всегда свежий. `full-domain-corpus.yml` объявляет вход `expect_lanes` как required без default: GitHub отвергает диспатч без него ДО создания прогона, и координатор, который такого входа не знает, кампанию не начнёт вовсе. Первым шагом полосы, до checkout и до любой дорогой работы, стоит арифметика: 16777216 делится на `window_points` нацело, частное равно `expect_lanes`, а `window_start` — каноническая десятичная запись внутри домена и на шве покрова этой ширины. Сравнения — по сырым байтам через `case`: `[ -eq ]` и `int()` принимают окружающие пробельные символы, а `$(( ))` читает ведущий ноль как восьмеричную запись, из-за чего `0200000` был бы 65536 для гварда и 200000 для `corpus_lane.py` — один диспатч, два разных окна. Длина координаты ограничена восемью цифрами домена до арифметики: `$(( ))` молча переполняется на 2^64, где `18446744073709551616` выглядит идеально выровненным нулём. У этого workflow есть второй режим — ограниченный префиксный зонд без окна. Он не полоса кампании, и единственный истинный для него размер — ноль; диспатч, который называет кампанию и не несёт окна, запустил бы один и тот же зонд по разу на полосу и отчитался бы зелёным. `dispatch_commands_v1` добавляет `-f expect_lanes=` в каждую команду. Тесты ИСПОЛНЯЮТ shell гварда, извлечённый из YAML: текстовая проверка на `-ne` ничего не говорит о том, что делает оболочка, и обезвреженное сравнение оставляло такие проверки зелёными. Co-authored-by: Claude Code --- .github/workflows/full-domain-corpus.yml | 102 ++++++ proof/region/v1/corpus_dispatch.py | 7 + .../v1/tests/test_corpus_campaign_guard.py | 317 ++++++++++++++++++ 3 files changed, 426 insertions(+) create mode 100644 proof/region/v1/tests/test_corpus_campaign_guard.py diff --git a/.github/workflows/full-domain-corpus.yml b/.github/workflows/full-domain-corpus.yml index 3f0dee76..a5162502 100644 --- a/.github/workflows/full-domain-corpus.yml +++ b/.github/workflows/full-domain-corpus.yml @@ -19,6 +19,20 @@ on: description: lane window width (packing-aligned multiple of shard_points) required: false default: "" + expect_lanes: + description: >- + lanes in the full-domain campaign this dispatch belongs to + (2^24 / window_points, or 0 for a dispatch that is not a lane) + # The coordinator's `--expect-lanes` lives in the coordinator, so a + # checkout older than that flag carries the older contract whole: + # this project has twice turned one mistake into a campaign — 133 + # runs, then 69 — while reading rules the running copy did not have. + # No guard added to the client protects a stale client. Declared + # required and without a default, this coordinate is refused by + # GitHub before a run exists, so a coordinator that does not know it + # cannot dispatch at all, and one that does has to state the scale + # of what it is about to start. + required: true lane_run_ids: description: comma-separated lane run ids to assemble (empty skips assembly) required: false @@ -43,6 +57,94 @@ jobs: PYTHONDONTWRITEBYTECODE: "1" PYTHONHASHSEED: "0" steps: + # First, and before the checkout on purpose: a dispatch whose + # coordinates cannot describe a lane of the cover must cost nothing, + # and this guard must not be a copy of the repository whose age is + # exactly what is in doubt. Everything it reads is declared on the + # step itself, so the guard is one self-contained object to review. + - name: refuse a dispatch that does not belong to a coherent campaign + shell: bash + env: + WINDOW_START: ${{ inputs.window_start }} + WINDOW_POINTS: ${{ inputs.window_points }} + EXPECT_LANES: ${{ inputs.expect_lanes }} + run: | + set -euo pipefail + # Arithmetic, not a token: a lane is admissible only if its own + # width tiles the full sRGB8 domain exactly into the campaign the + # dispatcher claims. An older coordinator cannot satisfy this by + # accident, and nothing here needs the repository to be read. + domain=16777216 + # `case` compares raw bytes. `[ -eq ]` and Python's `int()` both + # accept surrounding whitespace, so either would admit a + # coordinate carrying the carriage return a Windows shell leaves + # behind; and `$(( ))` reads a leading zero as octal, so `0200000` + # would be 65536 here and 200000 in the lane runner — one dispatch + # describing two different windows, the guard's arithmetic then + # saying nothing about the window that actually replays. + case "${EXPECT_LANES}" in + ''|*[!0-9]*) echo "expect_lanes must be a canonical decimal" >&2; exit 64;; + esac + if [ -z "${WINDOW_POINTS}" ]; then + # No window is the bounded prefix probe, which is not a lane of + # any cover: the only campaign size true of it is none. A + # dispatch that claims a campaign and carries no window would + # run that same bounded probe once per lane and report every one + # of them green. + if [ "${EXPECT_LANES}" != "0" ]; then + echo "a dispatch without window_points is the bounded probe and" \ + "belongs to no campaign: expect_lanes must be 0" >&2 + exit 64 + fi + if [ -n "${WINDOW_START}" ]; then + echo "window_start ${WINDOW_START} names a lane, and a lane needs" \ + "window_points: this dispatch would replay the bounded probe" >&2 + exit 64 + fi + exit 0 + fi + case "${WINDOW_POINTS}" in + ''|*[!0-9]*|0) echo "window_points must be a positive integer" >&2; exit 64;; + 0*) echo "window_points must not carry leading zeros" >&2; exit 64;; + esac + case "${WINDOW_START}" in + ''|*[!0-9]*) echo "window_start must be a canonical decimal" >&2; exit 64;; + 0) ;; + 0*) echo "window_start must not carry leading zeros" >&2; exit 64;; + esac + # Both coordinates are bounded by the domain and the domain is + # eight digits, so anything longer is out of range by + # construction — and it has to be refused before the arithmetic + # rather than by it: `$(( ))` wraps silently at 2^64, where + # `18446744073709551616` reads as a perfectly aligned zero, and + # `[ -ge ]` answers "not greater" for a value it cannot parse. + if [ "${#WINDOW_POINTS}" -gt 8 ] || [ "${#WINDOW_START}" -gt 8 ]; then + echo "window ${WINDOW_START}+${WINDOW_POINTS} is outside the sRGB8 domain" >&2 + exit 64 + fi + if [ $(( domain % WINDOW_POINTS )) -ne 0 ]; then + echo "window_points ${WINDOW_POINTS} does not tile the full domain" >&2 + exit 64 + fi + lanes=$(( domain / WINDOW_POINTS )) + # Compared as bytes, because both sides are canonical decimals by + # now and a numeric comparison is the one that can answer "equal" + # about something it failed to read. + if [ "${lanes}" != "${EXPECT_LANES}" ]; then + echo "campaign size ${EXPECT_LANES} contradicts the plan: a" \ + "${WINDOW_POINTS}-point window covers the domain in ${lanes} lanes" >&2 + exit 64 + fi + if [ "${WINDOW_START}" -ge "${domain}" ]; then + echo "window_start ${WINDOW_START} is outside the sRGB8 domain" >&2 + exit 64 + fi + if [ $(( WINDOW_START % WINDOW_POINTS )) -ne 0 ]; then + echo "window_start ${WINDOW_START} is not a seam of a" \ + "${WINDOW_POINTS}-point cover" >&2 + exit 64 + fi + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false diff --git a/proof/region/v1/corpus_dispatch.py b/proof/region/v1/corpus_dispatch.py index 88a9a15d..558e71ad 100644 --- a/proof/region/v1/corpus_dispatch.py +++ b/proof/region/v1/corpus_dispatch.py @@ -195,6 +195,13 @@ def dispatch_commands_v1( f"window_points={points}", "-f", f"shard_points={shard_width}", + "-f", + # The campaign's size travels with every lane so the workflow can + # check it against arithmetic on its own side. `--expect-lanes` + # guards the operator's intent here, where a stale checkout makes + # the guard stale with it; this coordinate guards the same + # invariant in the one place that is always current. + f"expect_lanes={len(plan)}", ) for start, points in plan ) diff --git a/proof/region/v1/tests/test_corpus_campaign_guard.py b/proof/region/v1/tests/test_corpus_campaign_guard.py new file mode 100644 index 00000000..eab155fc --- /dev/null +++ b/proof/region/v1/tests/test_corpus_campaign_guard.py @@ -0,0 +1,317 @@ +#!/usr/bin/env python3 +"""The corpus campaign contract, asserted where a stale checkout cannot move it. + +A guard that lives only in the coordinator cannot protect a checkout older +than the guard: the old file carries the old contract whole. That is how +this project dispatched 133 runs from a forgotten flag and then 69 from an +older checkout whose polarity was the opposite one. So `full-domain-corpus.yml` +asserts the campaign invariant itself — as a required input GitHub refuses to +dispatch without, and as arithmetic in the lane's first step, before the +checkout exists. + +These tests bind the two sides. The coordinator's command must carry the +coordinate the workflow demands, and the workflow's guard must admit exactly +the campaigns the coordinator can produce. The guard is *executed*, not read: +asserting that its text says `-ne` proves nothing about what the shell does +with it, and a neutered comparison left every text assertion green. +""" + +from __future__ import annotations + +import os +import re +import shutil +import subprocess +import sys +import unittest +from pathlib import Path + +PROOF = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(PROOF)) +REPO = PROOF.parents[2] + +import corpus # noqa: E402 +import corpus_dispatch # noqa: E402 + +WORKFLOW_V1 = REPO / ".github" / "workflows" / "full-domain-corpus.yml" +GUARD_STEP_V1 = "refuse a dispatch that does not belong to a coherent campaign" +_STEP_START_V1 = re.compile(r"^ - ", re.MULTILINE) +_INPUT_KEY_V1 = re.compile(r"^ [A-Za-z0-9_-]+:\s*$", re.MULTILINE) +REFUSED_V1 = 64 + + +class CorpusCampaignContractTests(unittest.TestCase): + """The lane's own campaign guard and the coordinator's command, together.""" + + def setUp(self) -> None: + self.text = WORKFLOW_V1.read_text(encoding="utf-8") + + # --- the declaration ------------------------------------------------ + + def test_the_campaign_size_is_a_required_input_without_a_default(self) -> None: + # Required and without a default is the whole mechanism: GitHub + # refuses the dispatch before a runner exists, so a coordinator that + # predates this coordinate cannot start a campaign at all. A default + # would restore exactly what the incident was — an omission that + # silently means something. + block = self.text[self.text.index(" expect_lanes:") :] + # The declaration ends where the next one begins; slicing to the + # first step instead would drag a neighbour's `default:` in and make + # this assertion answer about the wrong input. + following = _INPUT_KEY_V1.search(block, 1) + self.assertIsNotNone(following) + block = block[: following.start()] + self.assertIn("\n required: true\n", block) + self.assertNotIn("default:", block) + + # --- the coordinator side ------------------------------------------- + + def test_every_dispatched_command_carries_the_campaign_size(self) -> None: + plan = corpus_dispatch.lane_plan_v1() + commands = corpus_dispatch.dispatch_commands_v1( + plan, corpus_dispatch.DEFAULT_SHARD_WIDTH + ) + self.assertIs(type(commands), tuple) + self.assertEqual(len(commands), 256) + for command in commands: + self.assertEqual(command[3], corpus_dispatch.WORKFLOW_V1) + coordinate = f"expect_lanes={len(commands)}" + self.assertIn(coordinate, command) + # Membership is not a dispatch: `gh` reads a coordinate only when + # `-f` introduces it, and a bare element is an unrecognised + # positional argument the campaign discovers 256 times over. + self.assertEqual(command[command.index(coordinate) - 1], "-f") + + def test_a_rejected_plan_still_produces_no_command(self) -> None: + # The coordinate is derived from the plan's length, so it must not + # turn a typed refusal into an attribute error on the way out. + result = corpus_dispatch.dispatch_commands_v1( + corpus.ShardCorpusRejectedV1( + corpus.ShardCorpusReasonV1.FOREIGN_INPUT, "foreign" + ), + corpus_dispatch.DEFAULT_SHARD_WIDTH, + ) + self.assertIs(type(result), corpus.ShardCorpusRejectedV1) + + # --- the guard, executed -------------------------------------------- + + def _guard_script_v1(self) -> str: + """The guard's own shell, lifted out of the step that carries it.""" + + start = self.text.index(GUARD_STEP_V1) + body = self.text.index(" run: |", start) + len(" run: |\n") + end = body + _STEP_START_V1.search(self.text[body:]).start() + script = "\n".join( + line[10:] if line.startswith(" " * 10) else line + for line in self.text[body:end].splitlines() + ) + # Anti-vacuity: an extraction that silently found nothing would make + # every refusal below pass for the wrong reason. + self.assertIn("16777216", script) + self.assertGreater(len(script.splitlines()), 20) + return script + + def _run_guard_v1( + self, + window_points: str, + expect_lanes: str, + window_start: str = "0", + ) -> int: + bash = shutil.which("bash") + if bash is None: + self.skipTest("the lane guard is shell and needs a shell to run") + completed = subprocess.run( + (bash, "-c", self._guard_script_v1()), + capture_output=True, + text=True, + env={ + **os.environ, + "WINDOW_POINTS": window_points, + "EXPECT_LANES": expect_lanes, + "WINDOW_START": window_start, + }, + ) + return completed.returncode + + def test_the_guard_admits_every_seam_of_the_cover(self) -> None: + # The whole plan has to survive its own guard, seam by seam: a guard + # that refused one of them would refuse a correct campaign. + for width in (1 << 16, 1 << 23): + lanes = corpus_dispatch.FULL_DOMAIN // width + for start in range(0, corpus_dispatch.FULL_DOMAIN, width): + self.assertEqual( + self._run_guard_v1(str(width), str(lanes), str(start)), + 0, + (width, start), + ) + + def test_the_guard_admits_exactly_what_the_coordinator_dispatches(self) -> None: + # The two sides bound end to end: whatever the coordinator writes on + # a command line is fed to the guard as the runner would receive it. + for lane_width in (1 << 16, 1 << 20, 1 << 23): + plan = corpus_dispatch.lane_plan_v1(lane_width=lane_width) + self.assertIs(type(plan), tuple, lane_width) + commands = corpus_dispatch.dispatch_commands_v1( + plan, corpus_dispatch.DEFAULT_SHARD_WIDTH + ) + sampled = (commands[0], commands[len(commands) // 2], commands[-1]) + for command in sampled: + coordinates = dict( + item.split("=", 1) for item in command if "=" in item + ) + self.assertEqual( + self._run_guard_v1( + coordinates["window_points"], + coordinates["expect_lanes"], + coordinates["window_start"], + ), + 0, + command, + ) + + def test_the_guard_refuses_a_campaign_that_contradicts_its_width(self) -> None: + # The defect this exists to stop is a dispatch whose claimed scale and + # whose window disagree — including off by one, which is what a + # half-updated coordinator produces. + for width, lanes in ( + (1 << 16, 255), + (1 << 16, 257), + (1 << 16, 1), + (1 << 20, 256), + (1 << 23, 256), + ): + self.assertEqual( + self._run_guard_v1(str(width), str(lanes)), REFUSED_V1, (width, lanes) + ) + + def test_the_guard_refuses_a_width_that_cannot_tile_the_domain(self) -> None: + # A width that does not divide the domain has no lane count at all, so + # it must stop before the division rather than round into one. + for width in (1000, 65537, (1 << 24) + 1): + self.assertEqual( + self._run_guard_v1(str(width), "256"), REFUSED_V1, width + ) + + # These refuse for the divisibility rule alone. Every width above is + # also caught by the size comparison downstream, so deleting the + # divisibility check leaves this test green without these two: 65535 + # windows of 256 lanes leave 256 points of the domain uncovered while + # integer division still answers exactly 256. + for width, lanes in ((65535, 256), (65534, 256)): + self.assertEqual(corpus_dispatch.FULL_DOMAIN // width, lanes, width) + self.assertNotEqual(corpus_dispatch.FULL_DOMAIN % width, 0, width) + self.assertEqual( + self._run_guard_v1(str(width), str(lanes)), + REFUSED_V1, + (width, lanes), + ) + + def test_the_guard_refuses_what_is_not_a_positive_integer(self) -> None: + # A hand-typed dispatch is the realistic source of these, and an empty + # campaign size is what a coordinator would leave behind if this input + # ever gained a default. + for width, lanes in ( + ("65536", ""), + ("65536", "0"), + ("0", "256"), + ("-65536", "256"), + ("65536", "-256"), + ("65536", "256x"), + ("65536", "2 56"), + ("65 536", "256"), + ("65536\r", "256"), + ("65536", "256\r"), + ): + self.assertEqual( + self._run_guard_v1(width, lanes), REFUSED_V1, (width, lanes) + ) + + def test_the_guard_refuses_a_coordinate_that_is_not_a_canonical_decimal( + self, + ) -> None: + # A coordinate generated on Windows carries a carriage return; one + # typed by hand carries a space or a sign. Neither `[ -eq ]` nor + # `int()` objects to surrounding whitespace, and the lane runner would + # replay a window whose spelling no longer matches the guard's. + for start in ( + "65536\r", + "65536\n", + " 65536", + "65536 ", + "+65536", + "-65536", + "0x10000", + "6553 6", + "", + ): + self.assertEqual( + self._run_guard_v1("65536", "256", start), REFUSED_V1, repr(start) + ) + + # A leading zero is not cosmetic: `$(( ))` reads it as octal, so + # `0200000` is 65536 to this guard and 200000 to the lane runner's + # `int()`. The guard would then admit a window the run never + # replays. Every other spelling above is caught downstream too, so + # deleting the leading-zero arm leaves this test green without this + # case: 0200000 lands on the seam and inside the domain. + self.assertEqual(int("0200000"), 200000) + self.assertEqual(self._run_guard_v1("65536", "256", "0200000"), REFUSED_V1) + # Same class on the width: octal 0100000 is 32768, which tiles the + # domain into 512 lanes, while the runner replays 100000 points. + self.assertEqual(int("0100000"), 100000) + self.assertEqual(self._run_guard_v1("0100000", "512", "0"), REFUSED_V1) + + def test_the_guard_refuses_a_start_off_the_seam_or_off_the_domain(self) -> None: + # A start inside a window belongs to no plan and one past the end + # belongs to no domain; both replay something the cover never asked + # for. + for start in ("1", "65535", "65537", "16777216", "16842752"): + self.assertEqual( + self._run_guard_v1("65536", "256", start), REFUSED_V1, start + ) + + # Past the shell's own integer the comparisons stop answering: `[ -ge ]` + # reports "not greater" for what it cannot parse and `$(( ))` wraps, + # so 2^64 is a perfectly aligned zero. Deleting the width bound + # leaves this test green without this case. + self.assertEqual(18446744073709551616 % 65536, 0) + self.assertEqual( + self._run_guard_v1("65536", "256", "18446744073709551616"), REFUSED_V1 + ) + self.assertEqual( + self._run_guard_v1("18446744073709617152", "256", "0"), REFUSED_V1 + ) + + # --- the dispatch that is not a lane -------------------------------- + + def test_the_guard_admits_the_bounded_probe_as_no_campaign(self) -> None: + # The bounded prefix probe is this workflow's other mode; it is not a + # lane of any cover, and the only campaign size true of it is none. + self.assertEqual(self._run_guard_v1("", "0", ""), 0) + + def test_the_guard_refuses_a_campaign_claim_without_a_window(self) -> None: + # The half-updated coordinator: it names the campaign but drops the + # window, so every one of its dispatches would run the same bounded + # probe and report it green. + for lanes in ("1", "256", "16777216"): + self.assertEqual(self._run_guard_v1("", lanes, ""), REFUSED_V1, lanes) + + def test_the_guard_refuses_a_start_with_no_window_to_start(self) -> None: + # A start without a width is silently ignored by the probe branch, so + # the operator reads a green run as the lane they asked for. + self.assertEqual(self._run_guard_v1("", "0", "65536"), REFUSED_V1) + + # --- where the guard sits ------------------------------------------- + + def test_the_guard_runs_before_anything_is_fetched_or_replayed(self) -> None: + # A refusal that costs a checkout and an hour of replay is not the + # refusal this guard exists to be. + guard = self.text.index(GUARD_STEP_V1) + checkout = self.text.index("actions/checkout@") + replay = self.text.index("python3 proof/region/v1/corpus_") + self.assertLess(guard, checkout) + self.assertLess(guard, replay) + + +if __name__ == "__main__": + unittest.main(verbosity=2)