Proof: the decision chain binds what the sources produce, not who watched the build (V5b2d-4b) - #547
Merged
Merged
Conversation
…ched the build (V5b2d-4b) Наблюдаемый дефект: два прогона идентичного main дают РАЗНУЮ `comparator.identity`, поэтому полосы, посчитанные против одного RUN, не принимаются свежим RUN. Дуальное доказательство становится недостижимым: source-bound квитанции wire-формы не имеют намеренно, значит join обязан идти в процессе RUN, а посчитать там 512 полос нельзя (~46 ч реплики против конверта 8 ч). Замер на прогонах 31089986150/31090010890: `binary_identity` РАВНЫ — сборка из закреплённых исходников байт-воспроизводима между раннерами. Различаются ровно 96 байт внутри `build_identity` (32 docker capability + 2×32 наблюдения процессов сборки) и `test_observation` у Arb. Восемь координат из десяти, выводимых из источников, совпадают. Закон: у компаратора две идентичности, и граница проходит по вопросу «может ли решение от этого зависеть». - Решающая цепь связывает `source_identity` (kind + восемь source-координат). Движку передаётся именно она в `--manifest-identity`, поэтому её несут транскрипт, run claim, accounting-префикс и lane-манифест. Ключ манифеста полосы ПЕРЕИМЕНОВАН в `comparator_source_identity`, чтобы старые артефакты отвергались закрыто, а не переинтерпретировались. - Цепь провенанса связывает полную `identity`: дуальный клейм, семантическая квитанция и обе source-bound квитанции. Какая сборка произвела каждый движок — ровно то, что дуальное доказательство удостоверяет; запись не ослаблена. `source_identity` — производное свойство, wire-грамматика манифеста не меняется. Наблюдение среды остаётся в бандле компаратора, который едет вместе с evidence. Доказательства: `test_a_lane_survives_another_run_of_the_same_sources` — компараторы, различающиеся ТОЛЬКО в исключённых координатах, имеют разные полные идентичности, равные source-идентичности, и полоса одного допускается под другим. Anti-vacuity: `test_a_lane_still_dies_on_a_different_source_closure` — смена `evaluator_source` по-прежнему отвергает полосу закрыто. Локально: 254 теста, 7 ошибок — ровно базовые пробелы среды Windows. Слой arb/mpfi локально не грузится, его проверяет CI.
|
Warning Review limit reachedYou’ve reached a temporary PR review limit under our Fair Usage Limits Policy. Next review available in: 55 minutes Enable usage-based reviews in Billing to review now. Otherwise, wait until the next included review is available. How can I continue?After more reviews become available, a review can be triggered using the To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews. How do review limits work?CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability. For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window. Please refer docs for additional details. Review details⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Plus Run ID: 📒 Files selected for processing (5)
WalkthroughИзменение разделяет полную ChangesSource-bound identity
Estimated code review effort: 4 (Complex) | ~60 minutes Sequence Diagram(s)sequenceDiagram
participant ComparatorManifestV2
participant ShardCorpusRunnerV1
participant LaneAssembly
participant Evaluator
ComparatorManifestV2->>ShardCorpusRunnerV1: source_identity
ShardCorpusRunnerV1->>LaneAssembly: transcript и accounting с source_identity
LaneAssembly->>Evaluator: comparator_source_identity
Evaluator->>LaneAssembly: проверка transcript и run claim
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: 7
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (2)
proof/region/v1/corpus_assembly.py (2)
135-151: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winРассмотрите поднятие версии
LANE_SCHEMA_V1вместе с переименованием ключа.Ключ манифеста изменён с
comparator_identityнаcomparator_source_identity, но значениеschemaосталось прежним. Артефакт, созданный предыдущей версией, проходит проверку схемы на строке 135 и отвергается позже какlane manifest binds a foreign comparator_source_identity. Причина отказа при этом — устаревший формат, а не чужой компаратор.Если поднять версию схемы, отказ станет точным (
foreign lane schema), и старые lane-каталоги будут отличимы от подделанных.🤖 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_assembly.py` around lines 135 - 151, Поднимите версию схемы, используемую при проверке в assembly flow вокруг LANE_SCHEMA_V1, одновременно с переименованием manifest-ключа comparator_identity в comparator_source_identity. Обновите все связанные определения и генерацию манифеста так, чтобы старые lane-каталоги отвергались на проверке schema с причиной FOREIGN_INPUT/"foreign lane schema", а не на проверке identities.
415-431: 🗄️ Data Integrity & Integration | 🟡 Minor | ⚡ Quick winСохраните совместимость
assembly-receipt.json.
ASSEMBLY_SCHEMA_V1не изменился, но ключcomparator_identityзаменён наcomparator_source_identity. Сохранитеcomparator_identityсо значениемcomparator.identityили выпустите новую версию схемы с миграцией потребителей.🤖 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_assembly.py` around lines 415 - 431, В формировании receipt рядом с comparator_source_identity восстановите ключ comparator_identity со значением comparator.identity, сохранив совместимость assembly-receipt.json при неизменном ASSEMBLY_SCHEMA_V1; не заменяйте его новой схемой без миграции потребителей.
🤖 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/PROTOCOL.md`:
- Around line 499-516: Согласуйте списки wire-полей с новым разделом: в
описаниях третьего поля DecisionTranscriptV1 и второго поля RunClaimV1 замените
«comparator manifest identity» на «comparator source identity». Другие поля и
утверждения не изменяйте.
In `@proof/region/v1/region_proof_protocol.py`:
- Around line 873-897: Update source_identity to encode the ordered coordinate
count and each coordinate’s length in the folded preimage before the existing
coordinate bytes, using SOURCE_BOUND_COORDINATES_V2 and the values retrieved
from self. Preserve the current identity domain label, kind binding, and
coordinate order while making future variable-length coordinates unambiguous.
- Around line 60-75: Добавьте в proof/region/v1/region_proof_platform.py в
области BUILD_OBSERVATION_COORDINATES_V2 инвариант, проверяющий, что объединение
build- и source-координат в точности совпадает с полями ComparatorManifestV2 без
kind; сохраните SOURCE_BOUND_COORDINATES_V2 синхронизированным со схемой. В
proof/region/v1/tests/test_region_proof_protocol.py:1289-1294 добавьте проверки,
что source_identity не меняется при изменении build_identity и test_observation,
но меняется при изменении каждой из восьми source-координат.
In `@proof/region/v1/semantic/verifier.py`:
- Line 121: В цикле вокруг transcript.point_count переименуйте неиспользуемую
переменную expected_index в _expected_index, не изменяя остальную логику цикла.
In `@proof/region/v1/tests/test_corpus_assembly.py`:
- Around line 114-120: Move the lane comparator content map into corpus_lane as
a shared LANE_COMPARATOR_CONTENTS_V1 symbol, use it when constructing
lane_comparator_v1, and update _lane_bundle_contents in test_corpus_assembly.py
to return that map instead of recreating the coordinate literals and range.
In `@proof/region/v1/tests/test_semantic_replay.py`:
- Around line 363-377: Update both accounting grammar tests, including
test_mpfi_accounting_digest_matches_independent_packing, to use
comparator.source_identity instead of comparator.identity in the expected manual
packing and accounting_prefix_v1 call. Keep the rest of the digest construction
unchanged.
In `@proof/region/v1/tests/test_verification_evidence.py`:
- Around line 255-265: Replace receipt.comparator.manifest.identity with
receipt.comparator.manifest.source_identity in all three manually constructed
DecisionTranscriptV1 and RunClaimV1 instances referenced here, including the
cases around the foreign job identity and transcript binding tests. Preserve the
intended setup so each rejection test differs in only the single coordinate it
is designed to invalidate.
---
Outside diff comments:
In `@proof/region/v1/corpus_assembly.py`:
- Around line 135-151: Поднимите версию схемы, используемую при проверке в
assembly flow вокруг LANE_SCHEMA_V1, одновременно с переименованием
manifest-ключа comparator_identity в comparator_source_identity. Обновите все
связанные определения и генерацию манифеста так, чтобы старые lane-каталоги
отвергались на проверке schema с причиной FOREIGN_INPUT/"foreign lane schema", а
не на проверке identities.
- Around line 415-431: В формировании receipt рядом с comparator_source_identity
восстановите ключ comparator_identity со значением comparator.identity, сохранив
совместимость assembly-receipt.json при неизменном ASSEMBLY_SCHEMA_V1; не
заменяйте его новой схемой без миграции потребителей.
🪄 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: b5f50a31-887e-4b8e-b913-061c6c9329bd
📒 Files selected for processing (16)
proof/region/v1/PROTOCOL.mdproof/region/v1/arb/receipt.pyproof/region/v1/corpus.pyproof/region/v1/corpus_assembly.pyproof/region/v1/corpus_lane.pyproof/region/v1/mpfi/receipt.pyproof/region/v1/region_proof_protocol.pyproof/region/v1/semantic/verifier.pyproof/region/v1/tests/test_comparator_wire.pyproof/region/v1/tests/test_corpus_assembly.pyproof/region/v1/tests/test_corpus_lanes.pyproof/region/v1/tests/test_corpus_shards.pyproof/region/v1/tests/test_dual_proof.pyproof/region/v1/tests/test_region_proof_protocol.pyproof/region/v1/tests/test_semantic_replay.pyproof/region/v1/tests/test_verification_evidence.py
Comment on lines
+873
to
+897
| @cached_property | ||
| def source_identity(self) -> bytes: | ||
| """Identity of everything the comparator derives from its sources. | ||
|
|
||
| The full identity also binds `build_identity` and `test_observation`, | ||
| and those two coordinates fold in the build observation — the docker | ||
| capability and the build processes' console digests. That is a | ||
| deliberate provenance record, but it is not reproducible: two runs of | ||
| the identical source tree on two runners produce identical binaries | ||
| and identical decisions while their observations differ. | ||
|
|
||
| A decision the engine reaches does not depend on which daemon watched | ||
| the build, so the decision chain binds this coordinate instead: the | ||
| engine's transcript, its accounting and the replay lanes stay portable | ||
| across runs, while the receipt keeps the full identity and loses | ||
| nothing about the environment it was built in. | ||
| """ | ||
|
|
||
| return _identity( | ||
| COMPARATOR_SOURCE_ID_LABEL_V2, | ||
| bytes((int(self.kind),)) | ||
| + b"".join( | ||
| getattr(self, name) for name in SOURCE_BOUND_COORDINATES_V2 | ||
| ), | ||
| ) |
There was a problem hiding this comment.
🔒 Security & Privacy | 🔵 Trivial | 💤 Low value
Кодируйте порядок и длину координат явно.
source_identity конкатенирует восемь digest-ов фиксированной длины 32 байта, поэтому текущая склейка однозначна. Однако _require_digest проверяет длину только в __post_init__, а домен-разделение опирается на неизменность набора координат. Зафиксируйте количество координат в префиксе фолда, чтобы будущее добавление координаты переменной длины не создало неоднозначного preimage.
Это не текущий дефект, а защита от дрейфа. Решение остаётся за вами.
🤖 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/region_proof_protocol.py` around lines 873 - 897, Update
source_identity to encode the ordered coordinate count and each coordinate’s
length in the folded preimage before the existing coordinate bytes, using
SOURCE_BOUND_COORDINATES_V2 and the values retrieved from self. Preserve the
current identity domain label, kind binding, and coordinate order while making
future variable-length coordinates unambiguous.
added 4 commits
August 6, 2026 15:07
Пин run_identity сдвинулся: run claim теперь связывает source-идентичность компаратора. Обновлён по замеру CI. Блок перестроен на subTest по координатам: характеризационный пин, падающий на первом несовпадении, скрывает, какая часть цепи реально сдвинулась, — а цепь и есть то, что этот тест характеризует. Диагностическая ценность падения теперь равна полному срезу цепи, а не одной строке.
Сдвиг цепи объяснён полностью и проверен арифметикой, а не принят на веру: evidence.identity = H(label, source_identity, build_identity, run_identity), и локальный пересчёт с НЕИЗМЕННЫМИ source_identity/build_identity и новой run_identity даёт ровно то значение, которое сообщил CI (f4a4431f2f9a92070e1ad2ada94bf7f9fc83a4b8c7c0d7c26a2e30e80567e2f9). Значит посторонних сдвигов нет: из шести характеризуемых координат четыре совпали, включая comparator.identity (полную) и build_identity — провенанс не тронут, как и заявлено. Сдвинулись ровно две производные от run claim, который теперь связывает source-идентичность компаратора.
…ail after six hours Две независимые линзы ревью дали FAIL. Находки закрыты. 1. КРИТИЧНОЕ. arb/tests/full_domain_receipt.py и mpfi/tests/full_domain_receipt.py сравнивали transcript.comparator_identity с ПОЛНОЙ идентичностью манифеста — после перехода решающей цепи на source-идентичность это вечно ложно. Оба модуля исполняются только диспатчем native_gate.py full-domain-receipt: ни локальный набор, ни PR-CI их не запускают, поэтому прогон на 2^24 упал бы в самом конце, потеряв и RUN, и весь последующий диспатч полос. Добавлена парная anti-vacuity: две идентичности обязаны различаться, иначе проверка сравнивала бы значение с самим собой. 2. Версия схемы полосы поднята до corpus-lane-v2. Грамматика манифеста изменилась (ключ и семантика значения), а версия-строка называла обе несовместимые грамматики одним именем: старые полосы отвергались как «чужой компаратор» вместо честного отказа по версии — вводящий в заблуждение диагноз для артефакта, который никогда не был неверным. 3. PROTOCOL.md противоречил сам себе: wire-разделы DecisionTranscriptV1 и RunClaimV1 по-прежнему называли координату «comparator manifest identity», тогда как соседний раздел и код кладут туда source-идентичность. Имплементатор по этим разделам отверг бы каждый текущий транскрипт. 4. Негативные фикстуры в test_verification_evidence.py и test_verification_assembly.py строились с полной идентичностью, поэтому отказ срабатывал на посторонней координате раньше заявленной: при регрессии проверок job_identity или transcript_identity тесты остались бы зелёными. Прицел восстановлен. 5. Уточнено утверждение о замере: «ровно 96 байт» относится к build_identity, отдельно различается test_observation у Arb. Локально: 254 теста, 7 ошибок — ровно базовые пробелы среды Windows.
…and-kept list Находка CodeRabbit (Major), подтверждена: `SOURCE_BOUND_COORDINATES_V2` был свободным списком строк, а протокольные тесты проверяли только полную `identity`. Потерянная или переименованная координата молча выпала бы из фолда `source_identity`, и решающая цепь перестала бы различать компараторы, отличающиеся по ней. Ни один тест этого не заметил бы. Закрыто выводом, а не заплаткой: перечисляются ДВЕ координаты наблюдения сборки (`BUILD_OBSERVATION_COORDINATES_V2`), а source-bound набор выводится из `fields(ComparatorManifestV2)` как всё остальное. Новая координата манифеста теперь попадает в фолд автоматически, а не ускользает из него молча. Порядок объявления совпадает с прежним ручным списком, поэтому значения не сдвинулись — перепинивать нечего (проверено на артефактах обоих прогонов). Защита сделана настоящей четырьмя тестами: разбиение покрывает манифест точно и без пересечения; КАЖДАЯ source-координата сдвигает source_identity (subTest по координатам); обе координаты наблюдения сдвигают только полную identity; kind связан — полоса под бюджетом чужого движка не пройдёт. Прочее из того же ревью: B007 в semantic/verifier.py; координаты lane-компаратора больше не дублируются в тесте — вынесены в `lane_comparator_contents_v1()`, и обе стороны читают один источник (дубль дрейфовал бы и всплывал как «unresolved content address», пряча настоящую причину). Замечание про длину-префикс в фолде отклоняю обоснованно: элементы — digest-ы фиксированных 32 байт, а набор теперь выводится из схемы, поэтому склейка однозначна и без счётчика; добавление сдвинуло бы все идентичности решающей цепи без выигрыша. Локально: 258 тестов, 7 ошибок — ровно базовые пробелы среды Windows.
Collaborator
Author
|
@coderabbitai Все находки обработаны в
Защита сделана проверяемой четырьмя тестами ( Противоречие нового раздела с wire-списками (Minor) — уже закрыто в B007 в Дублирование координат lane-компаратора — согласен, две копии одной истины. Вынесено в Длина/порядок координат в префиксе фолда (Trivial) — отклоняю обоснованно. Элементы фолда — digest-ы фиксированных 32 байт ( Цена при этом реальная: префикс сдвинул бы Прошу перепроверить |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
git show --no-ext-diff --format=fuller --stat afd4593
printf '\n--- changed paths ---\n'
git diff-tree --no-commit-id --name-only -r afd4593
printf '\n--- target symbols ---\n'
ast-grep outline proof/region/v1/region_proof_protocol.py --items all --match 'ComparatorManifestV2|BUILD_OBSERVATION_COORDINATES_V2|SOURCE_BOUND_COORDINATES_V2|source_identity|identity' --view expanded || true
ast-grep outline proof/region/v1/corpus_lane.py --items all --match 'lane_comparator_contents_v1' --view expanded || true
ast-grep outline proof/region/v1/tests/test_region_proof_protocol.py --items all --match 'ComparatorSourceIdentityTests' --view expanded || true
printf '\n--- relevant diff ---\n'
git show --no-ext-diff --format= --unified=100 afd4593 -- \
proof/region/v1/region_proof_protocol.py \
proof/region/v1/corpus_lane.py \
proof/region/v1/tests/test_region_proof_protocol.py \
proof/region/v1/tests/test_corpus_assembly.py \
proof/region/v1/semantic/verifier.py \
proof/region/v1/PROTOCOL.mdLength of output: 64874 The first inspection confirms the schema-derived partition and fixed-width invariant. I will make one consistency check across the decision chain and protocol text. You are interacting with an AI system. |
Правки писались через write_text(newline="\n"), из-за чего четыре файла, хранящиеся в репозитории с CRLF, переписались целиком: diff показывал 1028 и 620 изменённых строк там, где содержательных изменений единицы. Ревьюер и человек теряют способность увидеть настоящую правку. Содержимое не менялось — только окончания строк возвращены к тому виду, в котором файлы лежат в репозитории.
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 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_lane.py`:
- Around line 58-63: Make the address unpacking explicit in lane_comparator_v1
by passing the keys from contents to protocol.ComparatorManifestV2 rather than
relying on implicit dictionary iteration. Preserve the generator-defined
ordering and keep the existing admit call unchanged.
In `@proof/region/v1/PROTOCOL.md`:
- Around line 488-491: Удалите из документации временные benchmark-данные:
идентификаторы прогонов, значение «96 байт» и конкретные детали наблюдений из
описанного фрагмента. Замените их кратким нормативным правилом о том, что build
observations могут различаться, но не изменяют source_identity.
In `@proof/region/v1/tests/test_region_proof_protocol.py`:
- Around line 105-115: В тесте test_the_split_covers_the_manifest_exactly
добавьте проверки, что observation не пуст и строго меньше полного набора
coordinates. Сохраните существующие проверки покрытия и непересечения без
изменений.
🪄 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: fab2d975-130b-472c-9b30-5040745894db
📒 Files selected for processing (14)
proof/region/v1/PROTOCOL.mdproof/region/v1/arb/tests/full_domain_receipt.pyproof/region/v1/corpus_lane.pyproof/region/v1/mpfi/tests/full_domain_receipt.pyproof/region/v1/region_proof_protocol.pyproof/region/v1/semantic/verifier.pyproof/region/v1/tests/test_build.pyproof/region/v1/tests/test_corpus_assembly.pyproof/region/v1/tests/test_corpus_lanes.pyproof/region/v1/tests/test_dual_proof.pyproof/region/v1/tests/test_region_proof_protocol.pyproof/region/v1/tests/test_semantic_replay.pyproof/region/v1/tests/test_verification_assembly.pyproof/region/v1/tests/test_verification_evidence.py
Comment on lines
+488
to
+491
| `31089986150`/`31090010890`: `binary_identity` равны; внутри `build_identity` | ||
| различаются ровно 96 байт (32 docker capability + 2×32 наблюдения процессов), и | ||
| отдельно различается `test_observation` у Arb, который сворачивает те же | ||
| наблюдения процессов. |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Удалите временный benchmark dump из протокольной документации.
Идентификаторы прогонов 31089986150/31090010890 и измерение 96 байт не являются стабильным протокольным контрактом. Оставьте краткое нормативное правило: build observations могут различаться, но не меняют source_identity.
As per coding guidelines: «временный benchmark dump … не коммитятся».
🤖 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/PROTOCOL.md` around lines 488 - 491, Удалите из документации
временные benchmark-данные: идентификаторы прогонов, значение «96 байт» и
конкретные детали наблюдений из описанного фрагмента. Замените их кратким
нормативным правилом о том, что build observations могут различаться, но не
изменяют source_identity.
Source: Coding guidelines
added 2 commits
August 6, 2026 17:58
… preimage Находки двух независимых линз ревью. Линза корректности дала PASS, линза правдивости — FAIL по одному пункту; все закрыты. 1. Раздел «Две идентичности компаратора» утверждал, что build_identity и test_observation сворачивают наблюдение сборки. Неполно: они сворачивают И воспроизводимые входы (байты build recipe, build_input_identity, formula_support_identity, pipeline_policy_identity, sha и длину бинаря). Исключены они потому, что СОДЕРЖАТ наблюдение, а не потому что состоят только из него. Отсюда цена разделения, которую документ обязан назвать прямо: решающая цепь перестаёт различать компараторы, отличающиеся ТОЛЬКО воспроизводимыми входами сборки — тот же исходник, собранный другим рецептом или давший другой бинарь. Математику это не задевает (пять source-координат остаются), а полная identity с бинарём и рецептом по-прежнему связывается квитанцией и дуальным клеймом. 2. Замер «ровно 96 байт» был Arb-специфичен. У MPFI координата несёт вложенный digest, состав дельты иной, а test_observation между прогонами совпал. Общее для обоих движков — только невоспроизводимость build_identity. Скоуп проставлен. 3. Reference заявлял source_identity, но не задавал её преимидж, а общая формула identity покрывает только top-level artifacts с magic. Независимая реализация не воспроизвела бы координату, которую теперь несёт каждый транскрипт и run claim. Преимидж выписан точно. 4. Accounting-грамматика в разделе верификатора говорила «job/domain/policy/ comparator identities» без уточнения, какая из двух. Имплементатор, читающий только этот буллет, свернул бы полную identity и получил вечный ACCOUNTING_REPLAY_MISMATCH. Тот же класс, что уже исправлялся в wire-разделах. 5. LANE_SCHEMA_V1 = "corpus-lane-v2": имя утверждало V1 при значении v2. Переименовано в LANE_SCHEMA_V2 — долг, внесённый прошлым исправлением. 6. Два grammar-теста accounting подавали полную identity — последний след старой цепи в тестах. Вердикт они не искажали (обе стороны сверки брали одно значение), но переиспользование как оракула молча разошлось бы с продакшном. ВЫНЕСЕНО отдельным срезом, не смешиваю: у mpfi/tests нет аналога arb/tests/test_native_gate.py, поэтому пины режимов MPFI пересчитываются только при dispatch-запуске — тот же класс «гейт падает после часов работы». Разрыв предсуществующий, моей правкой не задет; его закрытие сдвинет собственный инвентарный пин быстрого гейта MPFI и требует круга CI. Локально: 258 тестов, 7 ошибок — ровно базовые пробелы среды Windows.
Второй круг CodeRabbit, три находки, все верные. 1. Я поместил в нормативный reference историю замера — номера прогонов 31089986150/31090010890 и величину «ровно 96 байт». AGENTS.md прямо запрещает коммитить временный benchmark dump, и по делу: контракт должен говорить, ЧТО обязано выполняться, а не как это однажды измерили. Номера прогонов устареют, дельта изменится с версией docker, а правило — `binary_identity` воспроизводится, `build_identity` нет — останется. История измерения живёт в PR и журнале. 2. Анти-вакуумность собственного гейта разбиения: проверки проходили и при ПУСТОМ BUILD_OBSERVATION_COORDINATES_V2, а тогда цикл по координатам наблюдения не исполнил бы ни одного subTest. Разбиение выглядело бы доказанным, не проверяя ничего. Непустота обоих множеств закреплена. 3. `*contents` распаковывал ключи словаря, то есть контент-адреса, но из вызова читалось так, будто в манифест уходит содержимое. Адреса названы явно. Локально: 258 тестов, 7 ошибок — ровно базовые пробелы среды Windows.
lemone112
added a commit
that referenced
this pull request
Aug 7, 2026
…proof can be sealed (V5b2d-4d) (#549) * Proof: one process that mints both receipts is the only place a dual proof can be sealed (V5b2d-4d) `join_dual_proof_v1` needs five evidence chains, and two of them — the engines' source-bound receipts — have no wire form by design: a receipt that could be parsed from bytes would let foreign code mint provenance. So the join has no valid two-job topology at all; it can only happen inside a process that minted both receipts itself. This adds that process. `tests/dual_proof_gate.py` builds and runs both engines over the full manifest back to back, re-seals each engine's semantic receipt from the verification lanes, and seals the dual proof. The lane cover comes from an earlier run and admits here only because a lane binds the comparator's source identity (#547); the same identity sorts the cover by engine, so nothing trusts an artifact's name. Both engine lane modules now expose `seal_full_domain_receipt_v1`, so the gate mints the same receipt those lanes do instead of restating the build coordinates — two copies would drift, and the drift would surface as an unrelated admission failure an hour into a native run. The gate fails, never skips, on an incomplete environment: it is only ever invoked deliberately, so a silent pass would be a proof that did not happen. Measured, not assumed: - both engines' source locks pin byte-identical GMP and MPFR, so one job can serve both without an env collision; a future divergence exits 64 - the native RUNs took 63 min (Arb) and 43 min (MPFI) on run 31116022208, so the sequential pair fits one job's envelope - executor cgroups are named per process with a counter and removed on close, so two sequential executions do not collide `test_decorator_placement.py` closes the class of defect this change itself introduced: extracting the helper put it between the module's env gate and the class that gate guarded, which silently made the helper uncallable and left the native test ungated. Syntax checks and the fast suite both saw nothing — the lane modules live outside the `test_*.py` inventory. The new gate reads the tree as source, like the arity gate beside it. * Proof: the dual-proof job could not have run — two blockers found by review Two independent reviews of the final state found that the job this branch added could never have sealed anything. Both are fixed here. CONTAINMENT. The controller that observes a BUILD to RUN enters the observer group and stays there: non-test code writes `cgroup.procs` in exactly two places — the observer placement and the executed child's attach — and neither walks it back. With one shared subtree at `pids.max=2`, the second engine's BUILD forks docker into a saturated budget and dies, an hour into the run. The single-engine lanes never met this because `arb.yml` puts the engines in separate steps and `full-domain-run.yml` in separate jobs; one process for both engines happens first here, and the dual proof admits no other topology. So each engine now gets its own observer subtree, and `enter_task_cgroup_v1` returns the controller to the unconstrained group between them — where a fresh process would have started. No run's containment widens: the observer budget still governs each execution. DELIVERY. A lane is one dispatch, one run, one artifact, so a full-domain cover is spread across 512 runs while the job read a single `run-id` — and the input was declared `lane_run_ids` but read as `lane_run_id`. Worse, lane artifacts carried no engine in their name, so an Arb lane and its MPFI twin claimed one name and could not coexist under one root. The cover now spans many runs through the shape `full-domain-corpus.yml` already uses, and the artifact name carries the engine. Which engine a lane serves is still decided by the comparator source identity in its manifest, never by a name. A cover that is short, overlapping, or single-engine is now refused in seconds, before the first build, instead of after both native runs. Also from review: - the anti-vacuity check was theatre: receipt identity seals job, comparator, run and transcript and never the cover, so two engines could not collide in it by construction. Replaced with the property it claimed — the two covers are disjoint sets of lane directories. - the preflight listed 4 of the 10 variables the seal functions read, so a partial environment surfaced as a bare KeyError instead of the refusal this gate promises. - `seal_full_domain_receipt_v1` returns a union; an unchecked rejection became `AttributeError` two hours in, losing the reason. Typed now. - the gate skipped the hostile `replay_evidence_is_well_bound_v1` check its single-engine lanes run, and this is the only place a full-domain receipt is ever sealed. Restored, with the transcript's domain and comparator coordinates. - module resolution across the engines' five colliding stems was correct only by the order of two loads. Asserted instead of assumed. Verified: 260 local tests, 7 errors — the exact Windows baseline, unchanged. The new `enter_task_cgroup_v1` tests cannot run here at all: `test_executor` needs `fcntl`. CI is the only place they execute. * Proof: pin the workflow contract the expensive job was missing The dispatch workflows are pinned by the coordinates they must carry, which catches a missing coordinate but not a misspelt one — and a misspelt one is what happened: the dual-proof input was declared `lane_run_ids` and read as `lane_run_id`. GitHub expands an undeclared input to the empty string, so nothing fails until the job has run. On this job that is two hours of native execution before noticing the lane cover was empty. `test_every_referenced_input_is_declared` closes the class for every workflow at once, reading the declarations by indentation rather than parsing: the proof tree carries no YAML dependency. Proven red on the real drift, not a mock — reintroducing exactly `inputs.lane_run_id` into the live workflow makes the gate name it undeclared, and the fixed file is clean. It covers three workflows and eleven references today, with an anti-vacuity floor so a gate that stopped finding anything cannot pass quietly. `DualProofContainmentContractTests` pins the two properties whose absence made the job unrunnable: each engine owns its observer subtree (a shared one admits two tasks, and the second engine's BUILD forks into it), and the cover is gathered from many runs rather than one `run-id`. It also pins that the cover is checked before the first build, so the cheap refusal cannot drift back behind the expensive work. * Proof: the containment fix shipped a red CI and a second tautology Re-review of the final state found that the previous commit would have failed CI deterministically and that one of its own repairs repeated the defect it replaced. THE RED. `arb/tests/gate.py` pins the exact inventory of the fast suite, and that suite includes `tests/test_executor.py` through its shared patterns. Adding three tests there moved the hash and left the pin behind, so the first step of `arb.yml` would have printed inventory drift and returned 1 before building anything. Recomputed independently with an AST replica of the gate's own algorithm — the replica reproduces the parent commit's pinned value byte for byte, which is what makes its answer for HEAD trustworthy: 270 tests, b1bc948c… None of this is observable here; the gate needs `fcntl`, so the machine that wrote the drift could not run the check that catches it. THE SECOND TAUTOLOGY. Replacing the theatre assert with "the two covers are disjoint" was theatre again: `_lane_cover_v1` partitions by comparator source identity, and the two engines cannot share one — the sets are disjoint by construction, and the line could not fail in any state the gate reaches. What is genuinely unguaranteed is that the partition consumed the whole cover: a lane of a third identity is foreign to both engines and disappears silently. The union of both covers must now equal every lane directory present. Also from review: - the MPFI hostile check was vacuous — that receipt's constructor already requires the predicate, so the assert could not fail. Only Arb's remains, where the constructor binds something narrower. The previous commit claimed to restore both; it restored one. - `enter_task_cgroup_v1` took the caller's word for where it landed. The observer placement is always followed by a budget probe; this one now verifies its own post-condition, because the path arrives from configuration and a wrong one silently moves where the next BUILD runs. - the module-collision guard treated an absent import as safety. Absence retires the check instead of failing it, so it is a refusal now. - PROTOCOL.md still called the observer placement the only versioned cross-module placement operation. There are two, and the second is documented with why it cannot widen a run's containment. Verified: 265 local tests, 7 errors — the exact Windows baseline, unchanged. The recomputed inventory now equals the pin. * Proof: name a lane run after the coordinates it replays A full-domain cover is 512 separate runs, and the dual proof needs their ids. Without a name carrying the coordinates the only way to collect them is a guess about creation times, which breaks the moment two campaigns overlap. The run name makes the list a query — and makes a lane identifiable in the UI, where 512 identically-named runs are otherwise indistinguishable. * Proof: compare the entered group by inode, the way the observer probe does The post-condition added a moment earlier compared paths by spelling, while every other placement check in this module compares by inode — `fstat` on both descriptors — precisely because one group can be reached by more than one name. A false refusal here is not a cheap failure: it aborts a job two hours into two native runs, which is the same cost as having no check at all. * Proof: verify on the Linux that was here all along, and fix what it showed The last two rounds shipped a red CI each because the checks that catch inventory drift cannot run on Windows — and WSL, a real Linux where this whole layer imports, was available the entire time. Everything below was measured by running it there, not derived. MY OWN TEST WAS RED. The post-condition added last round refuses when the process is not in the named group, and the test I wrote for that placement builds a fake cgroup in a temporary directory — where no fixture can move this process. It now patches the current-cgroup reader the way the observer probe test beside it already does, and the post-condition finally has a test that proves it fires: an invariant added without one was exactly the omission the reviews keep finding. THE SECOND PIN. `tests/test_build.py` keeps an independent outer oracle of the same inventory — count, inventory digest and discovery-order digest — on purpose, so a coordinated edit to the gate cannot hide drift. Updating only the gate left it stale, and the oracle did its job by failing. All three constants now carry values the gate actually printed on Linux: 271 tests, inventory 86c723aa…, order fe5a3419… The order digest is over discovery order and cannot honestly be derived by hand; it was read off a run. Both gates verified green there: the fast Arb gate reports 271 tests with its exact 15-skip manifest, and the outer oracle passes. PROTOCOL.md's new paragraph was mechanically spliced — a 200-column line, an orphaned clause whose "this descriptor protocol" had drifted onto the wrong subject, and wording describing a string comparison the code no longer does. Rewritten as its own paragraph. Verified on Linux: 419 tests, 3 failures. All three are pre-existing and mine only by proximity — I reproduced them on a worktree whose proof tree is untouched `main`, where the same three fail identically. Windows still gives 265 tests and 7 load errors; that is the platform's ceiling, not a result. * Proof: two runs claiming one lane must not resolve by whoever downloaded last The cover is gathered from many runs into one directory, so a re-run of the same window overwrites the evidence already there. The result still looks exact — the window is present once, the arithmetic adds up — while one of two answers silently won, and nothing records which. Each run now lands in its own staging directory and the move into the flat cover refuses a name that is already taken. Lane run ids are validated as numbers, the way `verification-lanes.yml` already validates its own: an element starting with `-` would be read by `gh` as a flag rather than a run. Both are pinned by the workflow contract tests, so they cannot drift back. Verified: 7 contract tests pass; the workflow still parses to 11 steps. Left open and named rather than hidden: the cheap preflight proves the cover is two exact domains, but not that those two identities belong to the engines this job is about to build. Closing that needs the comparator's source identity derived from the checkout without building — the coordinates are all static, but no such derivation is exposed today. --------- Co-authored-by: Claude Code <daniilerosov12@gmail.com>
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.
Наблюдаемый дефект
Два прогона идентичного
main(31089986150,31090010890) дают разнуюcomparator.identity. Полосы, посчитанные против одного RUN, не принимаются свежим RUN — а значит дуальное доказательство недостижимо в принципе:Что показал замер
binary_identitybuild_identitytest_observation(Arb)То есть математика доказательства воспроизводима целиком; не воспроизводится только наблюдение среды сборки, замешанное в идентичность.
Закон
У компаратора две идентичности, и граница проходит по вопросу «может ли решение от этого зависеть».
Решающая цепь связывает
source_identity= kind +engine_release,upstream_source,arithmetic_input_set,wrapper_source,evaluator_source,operation_allowlist,legal_file_set,exclusions. Движку передаётся именно она в--manifest-identity, поэтому её несут транскрипт, run claim, accounting-префикс и lane-манифест.Цепь провенанса связывает полную
identity: дуальный клейм, семантическая квитанция и обе source-bound квитанции. Какая сборка произвела каждый движок — ровно то, что дуальное доказательство удостоверяет, и эта запись не ослаблена.Почему не наоборот — почему не вынести наблюдение из идентичности вообще: оно там намеренно,
arb/tests/test_build_identity_v2.py:476-481явными ассертами требует участияdocker_capability_identity. Это решение о провенансе, а не недосмотр, и правка аддитивна.source_identity— производное свойство. Wire-грамматика манифеста не меняется, бандл компаратора по-прежнему едет вместе с evidence.Ключ lane-манифеста переименован в
comparator_source_identity: старые артефакты обязаны отвергаться закрыто, а не переинтерпретироваться.Доказательства
test_a_lane_survives_another_run_of_the_same_sources— компараторы, различающиеся ТОЛЬКО в исключённых координатах, имеют разные полные идентичности, равные source-идентичности, и полоса одного допускается под другим.test_a_lane_still_dies_on_a_different_source_closure— anti-vacuity: сменаevaluator_sourceпо-прежнему отвергает полосу закрыто.Проверки
fcntl/invalid native process cwd), новых нет.arb//mpfi/локально не импортируется, его проверяет CI.Rollback
git revertодного коммита. Изменение чисто вычислительное: замороженные фикстуры и пиныcontroller.pyне тронуты, wire-грамматика не менялась.Что открывает
После мержа: новый RUN → 512 полос → полосы переживают повторный RUN → in-process join →
DualProofReceiptV1(full_domain=True)и mint-гейт. Exit-критерии V5b2d №1 и №2 уже закрыты замером (counters=(1, 16777215, 0, 0), decision_bits побайтно идентичны у обоих движков).Summary by CodeRabbit
Новые возможности
Исправления
Тесты