Proof: a dispatched campaign hands the dual proof its lane run ids (V5b2d-4e) - #553
Merged
Conversation
added 2 commits
August 6, 2026 23:22
…5b2d-4e) Наблюдаемый дефект: полное покрытие домена — 512 отдельных прогонов полос (256 на движок), и дуальному доказательству нужен список их идентификаторов. Собрать его нечем: `corpus_dispatch.py` печатает команды `gh workflow run`, а они id не возвращают; сбор по времени создания ломается ровно там, где он и нужен — два движка реплеят одни и те же окна одной evidence-сборки одновременно. Закон: прогон полосы назван своими координатами (`verification-lanes.yml` рендерит `lane <artifact> <start>+<points> of <evidence_run_id>`), поэтому список кампании — запрос по именам, а не догадка по часам. Кампанию отделяют артефакт и evidence run id, не время. Режим `--mode collect` устроен по границе, уже принятой в модуле: - `gh_lane_runs_v1` — единственное нечистое наблюдение. Проекция сделана самим `--jq` в запросе, поэтому в процесс входят ровно три поля (databaseId, displayTitle, conclusion) и ни одно непросмотренное поле ответа API не может попасть ни в решение, ни в лог. Запись, которая не проецируется точно, отвергается, а не угадывается. - `match_lane_runs_v1` — чистое сопоставление имён с планом. Все правила — чья кампания, чей движок, какое заключение считается, что такое полное покрытие — достижимы тестом без сети. - `collect_lane_runs_v1` — шов между ними: недоступный API, отсутствующий токен или нечитаемый ответ становятся типизированным отказом с причиной, а не пустой кампанией; пустая кампания и сломанный запрос ведут оператора к противоположным действиям. Неполный сбор — типизированный отказ `LaneRunCollectionRejectedV1`, а не тихий частичный список: окна без прогона и окна с двумя едут в нём данными (`missing`/`duplicated`), оператор передиспатчит ровно их, а CLI не пишет ничего и выходит 64. Частичный список неотличим от полного для того, кто прочитает его следующим. Парсер имени допускает ровно канонический рендеринг: `int()` принял бы `+7`, `007`, `1_0` и не-ASCII цифры, и каждое из них позволило бы чужому заголовку занять окно плана. Доказательства (WSL, python3 -m unittest): - RED до реализации: 17 ошибок «module 'corpus_dispatch' has no attribute parse_lane_run_name_v1 / match_lane_runs_v1 / collect_lane_runs_v1». - 19 новых тестов; каждый заявленный класс убивает мутацию: порядок плана → порядок наблюдения (M1); дыра терпится (M2); дубль терпится (M3); фильтр артефакта снят (M4); фильтр evidence run снят (M5); заключение игнорируется (M6); ordinals по `isdigit()` (M7); `except Exception` сужен до `OSError` на шве наблюдения (M8). Все восемь падают на финальном коде. - Контакт с реальностью: `gh run list --workflow verification-lanes.yml --json databaseId,displayTitle,conclusion --jq ...` на живом репозитории возвращает реальные записи; `--mode collect` против прогона 31104030757 отказывает с 256 missing и не пишет ничего (в `main` run-name ещё нет — он приходит с V5b2d-4d, до него ни один заголовок не является полосой кампании). - Набор proof: 427 тестов, 3 падения — ровно предсуществующие в test_build на Linux (два golden-digest и post_popen_handler_gap). Связность: режим полагается на `run-name` из `verification-lanes.yml` (V5b2d-4d). Без него сбор не выдумывает совпадений — он отказывает громко.
Independent verification ran mutants and found the same class three times: an invariant stated in code and in the comment beside it, with nothing that would notice its removal. The expensive one is the second engine. Both engines replay the same evidence build, so a listing carries both campaigns — and a collector that hardcoded the first artifact answered an MPFI request with Arb's run ids and exited 0. Half a dual proof, silently wrong, reported as success. Every CLI case used the Arb artifact, so nothing could tell the two apart. The overlap guard was theatre in the literal sense: its docstring calls overlap "the one thing that must not pass", and the refusal suite contained no overlapping plan at all — the case it did contain died on the tuple-shape branch beside it. A plan of two windows sharing an ordinal is in the suite now. Deduplicating by run id had the same shape: a listing that repeats a run must not manufacture a duplicate-cover refusal, and removing the check left everything green. Each is proven by the mutant it kills, one test apiece: the hardcoded artifact at the collect call site, `window[0] < cursor` weakened to a tautology, and the unconditional append. Verified: 31 dispatch tests pass; 429 on Linux with the three pre-existing `test_build` failures that also fail on an untouched tree.
WalkthroughДобавлен режим ChangesКоллекция lane runs
Estimated code review effort: 4 (Сложный) | ~45 минут Sequence Diagram(s)sequenceDiagram
participant CLI as collect CLI
participant GH as gh run list
participant Collector as collect_lane_runs_v1
participant Matcher as match_lane_runs_v1
participant File as lane-runs.json
CLI->>GH: Запрашивает lane runs с лимитом
GH-->>Collector: Возвращает TSV-наблюдения
Collector->>Matcher: Передаёт успешные observations
Matcher-->>Collector: Возвращает коллекцию или отказ
Collector->>File: Записывает JSON при полном покрытии
Possibly related PRs
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✨ Finishing Touches 💡 1📝 Generate docstrings 💡
🧪 Generate unit tests (beta)
Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@proof/region/v1/corpus_dispatch.py`:
- Around line 649-661: В режиме collect добавьте до вызова collect_lane_runs_v1
валидацию положительного значения args.run_limit, положительного
args.evidence_run_id и допустимого значения args.evidence_artifact. При каждой
ошибке сразу выведите сообщение с именем неверного параметра и верните код 64,
не выполняя сетевой запрос; сохраните существующие проверки обязательных
аргументов.
In `@proof/region/v1/tests/test_corpus_dispatch.py`:
- Around line 611-635: Add a CollectCliTests test covering --run-limit: use an
observer that records its limit argument, invoke _with_observer with --run-limit
set to 37, and assert successful execution plus seen == [37]. Keep the existing
collect output assertions unchanged.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: c7773709-db0d-4b6f-a08b-6b9db50a16a6
📒 Files selected for processing (2)
proof/region/v1/corpus_dispatch.pyproof/region/v1/tests/test_corpus_dispatch.py
added 2 commits
August 7, 2026 08:52
Замечание ревью верно по существу: `--mode collect` передавал свои аргументы в `collect_lane_runs_v1` без единой проверки, а тот первым делом делает сетевой вызов. Наблюдённое поведение до правки (WSL, наблюдатель-заглушка вместо `gh`): - `--evidence-run-id 0` и `-1`: запрос выполнен (observer_called=[2000]), отказ гласит «lane run collection cannot observe verification-lanes.yml: …» — вина переложена на workflow, а не на аргумент; - `--evidence-artifact verification-evidence-flint`: то же самое; - `--run-limit 0` и `-5`: значение уходит в `gh run list --limit` дословно, а пустой ответ превращается в отказ «cover is incomplete: missing=…» с 256 окнами — оператор идёт передиспатчивать кампанию, которая цела. Закон: координата, которая будет потрачена на сетевой запрос, проверяется до запроса, и отказ называет виновный аргумент. Код возврата назвать его не может — он 64 у всех соседних отказов, поэтому именно на текст и на отсутствие запроса опираются тесты. Allowlist не продублирован: он рендерится из `EVIDENCE_ARTIFACTS_V1`, так что оператор узнаёт допустимый набор из самого отказа. Тот же инвариант рядом (предсуществующий дефект, закрыт этим же срезом): `--mode verification-dispatch` с непозитивным run id или чужим артефактом обходил построитель команд, тот возвращал типизированный отказ, а `main` обходил его циклом как список команд — оператор получал `TypeError: 'ShardCorpusRejectedV1' object is not iterable` вместо причины. Теперь отказ построителя печатается с его собственной причиной и выходит 64. Доказательства (WSL, python3 -m unittest): - RED до реализации: три падения по заявленной причине («--evidence-run-id» не найден в тексте отказа; «--run-limit» не найден в отказе про неполное покрытие) и одна ошибка TypeError в verification-dispatch. - 8 мутантов, каждый убит: M1/M2/M3 — снятие каждой из трёх проверок; M4 — общий текст «requires valid arguments» вместо имени аргумента (убивает все три теста); M5 — проверки перенесены ПОСЛЕ запроса (observed=[2000] != []); M6 — проверка лимита сделана слишком строгой (`>= 0`), убита тестом на допустимые аргументы; M7 — отказ без причины; M8 — снятие защиты от обхода отказа (тот самый TypeError). - Прежний `test_collect_requires_both_evidence_coordinates` заменён: его наблюдатель звал `self.fail`, а `collect_lane_runs_v1` глотает любое исключение наблюдателя в типизированный отказ с тем же кодом 64 — тест не мог упасть по своей заявленной причине. - Набор proof: 433 теста, 3 падения — ровно предсуществующие в test_build (два golden-digest и post_popen_handler_gap), они же падают на нетронутом дереве (429 тестов, те же три). - Контакт с реальностью: после правки все пять случаев дают observer_called=[], ничего не записано, текст называет аргумент. Rust не затронут: изменены три файла в proof/region/v1.
Independent verification found the class this branch claimed closed was closed only at the zero boundary: a positive but truncating --run-limit spent the query and then reported the campaign incomplete — sending the operator to re-dispatch 256 lanes when the fix is one flag. `gh run list --limit N` drops the oldest runs, so a listing that came back exactly at the limit cannot distinguish a real hole from its own truncation. The refusal now names the flag when the listing is saturated, and keeps blaming the campaign when there is room to spare — the anti-vacuity case, because hiding real damage behind the flag would be the opposite failure. Also corrected here: the comment claiming CalledProcessError.__repr__ drops stderr — measured false on the #555 branch, repr carries every constructor argument; stderr is preferred for legibility, not recovery. Verified: 36 dispatch tests pass, both new ones read the refusal text.
added 2 commits
August 7, 2026 10:33
The interleave was real: git tried to merge the new collect observer into the artifact observer because both begin identically, so the zone was reconstructed programmatically — both sides whole, shared fragments duplicated into each. Resolution by intent: - printing is the default and dispatching is `--execute` (main's polarity); the collect tests lose the flag that no longer exists; - `--run-limit` joins main's argument set; - main's typed not-a-tuple guard and single mid-flight handler stand; the branch's older duplicates go; - the collect block — observation, matching, saturation rule, CLI mode — lands beside the admission chain rather than inside it. Verified: 75 dispatch tests pass, and pass again under PYTHONOPTIMIZE=2.
One conflict, the module docstring: both paragraphs are true — the origin admission from #552 and the collect mode from this branch — so both stand. Everything else, including the provenance chain and its tests, merged clean. Verified: 95 dispatch tests pass, and again under PYTHONOPTIMIZE=2.
There was a problem hiding this comment.
Actionable comments posted: 1
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
proof/region/v1/corpus_dispatch.py (1)
846-862: 🩺 Stability & Availability | 🟠 Major | ⚡ Quick winДобавьте таймаут в
gh run list.Два других наблюдения этого модуля (
gh_run_artifacts_v1,gh_run_provenance_v1) передаютtimeout=OBSERVATION_TIMEOUT_SECONDS_V1. Здесь таймаута нет. Зависшийghостанавливает режимcollectбез ограничения времени, и оператор не отличает зависание от работы. Таймаут также нужен потому, чтоcollect_lane_runs_v1превращает любую ошибку наблюдения в типизированный отказ; без него отказа не будет вовсе.🛠️ Предлагаемая правка
capture_output=True, text=True, check=True, + # Инвариант наблюдений этого модуля: у запроса есть предельный срок, + # иначе зависший `gh` неотличим от работы и отказ никогда не наступит. + timeout=OBSERVATION_TIMEOUT_SECONDS_V1, )🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@proof/region/v1/corpus_dispatch.py` around lines 846 - 862, Update the subprocess.run invocation in collect_lane_runs_v1 to pass timeout=OBSERVATION_TIMEOUT_SECONDS_V1, matching the existing gh_run_artifacts_v1 and gh_run_provenance_v1 observations. Preserve the current command and error propagation behavior so a hung gh run list becomes the existing typed observation failure.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@proof/region/v1/corpus_dispatch.py`:
- Line 844: Исправьте форматирование в match_lane_runs_v1: перенесите
закрывающие тройные кавычки докстроки на отдельную строку, а закрывающую скобку
кортежа аргументов — после значения --jq на отдельную строку, сохранив
содержимое и поведение без изменений.
---
Outside diff comments:
In `@proof/region/v1/corpus_dispatch.py`:
- Around line 846-862: Update the subprocess.run invocation in
collect_lane_runs_v1 to pass timeout=OBSERVATION_TIMEOUT_SECONDS_V1, matching
the existing gh_run_artifacts_v1 and gh_run_provenance_v1 observations. Preserve
the current command and error propagation behavior so a hung gh run list becomes
the existing typed observation failure.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 55ea9f33-2f73-437c-ab90-1ef234b2031b
📒 Files selected for processing (3)
proof/region/v1/corpus_dispatch.pyproof/region/v1/tests/test_corpus_dispatch.pyproof/region/v1/tests/test_verification_dispatch.py
| it saw, without deciding anything. The projection is done by `--jq` in | ||
| the query itself, so no unreviewed field of the API reply ever enters the | ||
| process; which of these runs belongs to a campaign is a rule, and it lives | ||
| in `match_lane_runs_v1` where a test can reach it. """ |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🔵 Trivial | 💤 Low value
Исправьте склеенное форматирование.
В строке 844 закрывающая """ стоит на одной строке с текстом докстроки. В строке 858 закрывающая скобка кортежа аргументов стоит после значения --jq. Обе строки выглядят как результат неудачного слияния и мешают чтению.
♻️ Предлагаемая правка
- in `match_lane_runs_v1` where a test can reach it. """
+ in `match_lane_runs_v1` where a test can reach it.
+ """
@@
- ".[] | [.databaseId, .displayTitle, .conclusion] | `@tsv`", ),
+ ".[] | [.databaseId, .displayTitle, .conclusion] | `@tsv`",
+ ),Also applies to: 858-858
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@proof/region/v1/corpus_dispatch.py` at line 844, Исправьте форматирование в
match_lane_runs_v1: перенесите закрывающие тройные кавычки докстроки на
отдельную строку, а закрывающую скобку кортежа аргументов — после значения --jq
на отдельную строку, сохранив содержимое и поведение без изменений.
Collaborator
Author
|
@coderabbitai Оба замечания закрыты кодом в |
|
Tip For best results, initiate chat on the files or code changes.
Режим 🐇 ✅ ✏️ Learnings added
You are interacting with an AI system. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Что это
Полное покрытие домена — это 512 отдельных прогонов воркфлоу (256 полос на движок). Дуальному доказательству нужен список их идентификаторов, и собрать его было нечем: координатор печатает команды
gh workflow run, которые id не возвращают, а собирать по времени создания ломается, как только пересекаются две кампании.Это прямой блокер запуска доказательства — даже при полностью живом GitHub.
Что добавлено
Режим сбора: по evidence-прогону и плану находит прогоны полос по их именам (в PR #549 полоса получает
run-nameс координатами) и выдаёт машинно-читаемый список в--out.Архитектура — принятая в модуле: нечистое наблюдение отдельно, чистое сопоставление имён с планом отдельно и покрыто тестами, отказ типизированный, наблюдение проецирует белый список полей, а не сырой объект прогона.
Неполный сбор — типизированный отказ, а не тихий частичный список. Ничего не пишется: частичный список идентификаторов читается потребителем ровно как полный. В отказ выводится, каких окон не хватает и какие задвоены.
Что нашла независимая проверка и что исправлено
Проверяющий прогнал 11 мутаций, переживших набор. Три из них — один класс: инвариант объявлен в коде и в комментарии рядом, а теста нет.
Второй движок не проверялся ни разу — самая дорогая находка. Оба движка реплеят одну evidence-сборку, поэтому листинг несёт обе кампании. Мутант с захардкоженным первым артефактом отвечал на запрос MPFI идентификаторами Arb и выходил с кодом 0. Половина дуального доказательства, тихо неверная, отрапортованная как успех. Все CLI-кейсы использовали только Arb, поэтому различить было нечем.
Охранник пересечения окон — театр в буквальном смысле. Его докстринг называет пересечение «единственным, что не должно пройти», а в наборе отказов не было ни одного пересекающегося плана: тот кейс, что был, падал на соседней проверке длины кортежа. Теперь в наборе есть план из двух окон, делящих ординал.
Дедупликация по идентификатору прогона — та же форма: повторяющийся листинг не должен фабриковать отказ «покрытие задвоено», и снятие проверки оставляло набор зелёным.
Каждая починка доказана убитым мутантом, по одному тесту на каждый: захардкоженный артефакт на пути сбора,
window[0] < cursorослабленное до тавтологии, безусловныйappend.Проверки
test_build, воспроизведены на нетронутом дереве.Зависимость
Полезен вместе с #549, где полоса получает
run-nameс координатами. Без него сопоставление по именам не имеет опоры.Откат
Ревертом одного коммита. Новый режим аддитивен, существующие пути не затронуты.
Summary by CodeRabbit
Новые возможности
collectдля поиска успешных verification-запусков и проверки полного покрытия плана.--run-limitдля ограничения количества запрашиваемых запусков.Исправления