Proof: the MPFI engine's source identity is answerable before its build (V5b2d-4j) - #556
Conversation
…ld (V5b2d-4j) A coverage pre-check can show cheaply that a set of lanes carries exactly the two distinct comparator source identities a dual proof requires, but not that those identities belong to the engines the job will build. Arb can already answer that from admitted inputs alone. MPFI could not, so the binding still cost a native Docker build to discover and the cheap check could bind only one engine of the pair. `expected_comparator_source_identity_v1` derives the MPFI answer from the request's own snapshot, with no build, daemon or binary in reach. It is not a second statement of the coordinates: `_source_bound_preimages_v1` is the single derivation the build path now consumes too, and `source_bound_identity_v2` is the single fold both the pre-check and the built manifest go through. The boundary is narrow on purpose. Two things are established: the pre-check and the build agree because they physically run one derivation, and the answer is invariant to every build observation. That the derivation computes the *correct* coordinates is NOT established — no pinned expected identity and no second implementation exist in this repository. The Arb half carries exactly the same limitation. Two asymmetries between the engines are recorded rather than changed: `source_bound_coordinates_v2()` serves both because the manifest grammar is single and `kind` is a discriminator field, not a schema switch; and MPFI folds the runtime binding into its comparator while Arb does not, which costs MPFI the lane portability across runtime limits that the source identity exists to provide.
The docstring claimed the MPFI receipt never catches _SharedDerivationProbe, but the controller's broad `except Exception` blocks do catch it and convert it into a REPLAY_BINDING_FAILED rejection; the test itself asserts `built.detail == marker`. State the actual mechanism.
The Arb half's final review found one branch of the construction guard that nothing could see, and the MPFI half shipped with the same hole: the field order is checked against the protocol rather than trusted, but both sides read one declaration, so deleting the check left every suite green — including the neighbour test whose docstring calls the invariant proven. The drift is now injected at the protocol seam (reversed order, extra coordinate) exactly as the Arb suite does it, so the branch is reachable and the guard tests carry all three refusals plus the anti-vacuity case. Inventory pin recomputed by running the gate, not by hand: 43 tests, 2c422736... The Arb gate is untouched by this slice and still reports its own 284 / 3284dccf..., which is main's value.
|
Warning Review limit reachedYou’ve reached a temporary PR review limit under our Fair Usage Limits Policy. Next review available in: 46 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 (3)
Comment |
1 participant
Что это
MPFI-половина статической source-идентичности движка. Парная к Arb-половине (#554), форма и границы совпадают с ней намеренно.
expected_comparator_source_identity_v1отвечает на вопрос «какая source-идентичность будет у MPFI-компаратора» из уже допущенного запроса: без сборки, без демона Docker, без бинарника. Это не второе изложение координат —_source_bound_preimages_v1теперь единственная деривация, которую физически потребляет и путь сборки, и предсборочная проверка, аprotocol.source_bound_identity_v2— единственная свёртка, через которую проходят обе стороны.Дефект
Дешёвая coverage-проверка умеет показать, что набор лейнов несёт ровно две различные source-идентичности компараторов, но не то, что эти идентичности принадлежат движкам, которые задание собирается собрать. Arb отвечал на это из допущенных входов после #554. MPFI — нет: единственным производителем идентичности был
ComparatorManifestV2, существующий только после сборки. То есть привязка стоила нативной сборки MPFI, и дешёвая проверка могла связать лишь один движок из пары.Что доказано
_MUTANT_SECOND_BINDING_V1 = _source_bound_preimages_v1), после чего подмена одной стороны перестаёт валить другую —test_the_build_and_the_pre_check_share_one_source_bound_derivationкраснеет (1 failure). Тест эмулирует именно дубликат-алиас, а не отсутствие функции.build_identityвместоengine_release) краснит 6 подслучаев, включая все три backend'а.kind. Мутант M4 (убраноbytes((int(kind),))из прообраза) краснитtest_the_fold_separates_the_two_engines_on_identical_coordinates.test_the_source_bound_preimage_set_cannot_drift_from_the_manifestостаётся зелёным — это и есть доказательство, что ветка была недостижима ничем другим.Все четыре мутанта применялись скриптом с обязательным совпадением якоря ровно один раз (иначе abort), дерево восстанавливалось
git checkout --с проверкой чистоты.Анти-вакуумность: точная форма конструируется (
test_the_exact_shape_constructs), иначе защита, отвергающая всё, удовлетворила бы все тесты на отказ.Что НЕ доказано — прямо
ArbBuildIdentityCharacterizationTestsвtests/test_build.pyдержит характеризационные пины на Arb-координатах. MPFI-эквивалента нет ни одного — проверено поиском по дереву. То есть для MPFI не закреплено даже характеризационно, на синтетической фикстуре.expected_comparator_source_identity_v1не вызывается ниоткуда, кроме тестов — ни в MPFI-половине, ни в Arb-половине на main. Предсборочная coverage-проверка, ради которой деривация существует, в дереве отсутствует;tests/dual_proof_gate.pyсравнивает source-идентичности уже собранных движков. Срез делает ответ выводимым, но не подключает его. Это отдельный следующий срез, статус тот же, что у Arb.runtime_binding_identity_v1вarithmetic_input_set, Arb не читает runtime-биндинг вовсе. Из-за этого замена лимита executor'а двигает MPFI-идентичность и не двигает Arb-идентичность, то есть переносимость лейнов между запусками, ради которойsource_identityи существует, для MPFI не выполняется. Какая сторона права — решение семантики протокола, здесь не решается. ТестComparatorRuntimeBindingAsymmetryTestsсуществует, чтобы ни одну сторону нельзя было изменить не нарочно.Проверки (WSL, python 3.12.3)
proof/region/v1/tests: 497 тестов, 3 падения.origin/main, распакованном отдельно (test_build: 45 тестов, те же 3 FAIL). То есть они pre-existing и не внесены этим срезом. По записи в Proof: the engine's source identity is answerable before its build (V5b2d-4f) #554 это падения, специфичные для локального 3.12 и отсутствующие на CI-3.14 — здесь это не проверялось, проверено только совпадение с нетронутой базой.PYTHONOPTIMIZE=2: тот же результат, 497 тестов, те же 3 падения.proof/region/v1/mpfi/tests/gate.py: OK, 43 теста, 4 skip. В обоих режимах.proof/region/v1/arb/tests/gate.py: OK, 284 теста, 15 skip, inventory3284dccf...— значение main, срез его не двигает. В обоих режимах.Пины инвентаря
Пересчитаны исполнением гейта, не рукой: MPFI
EXPECTED_TEST_COUNT = 43,EXPECTED_TEST_INVENTORY_SHA256 = 2c422736047106ab082955d2330d120c199ad1bb70e81321ca93c0dd2b2dbd4c.Внешний оракул
tests/test_build.py(ARB_*) иarb/tests/gate.pyне трогались: срез добавляет тест только вmpfi/tests, который arb-гейт не обходит. Это подтверждено зелёным arb-гейтом на исходном значении main.Слияние
origin/mainвлит. Конфликтов не было: обе половины внесли вregion_proof_protocol.pyпобайтово одинаковое изменение (source_bound_identity_v2+ переключениеComparatorManifestV2.source_identityна неё), git свёл их как одинаковую правку. Результат проверенast.parseпо всем затронутым файлам плюс проверка на дублирование определений — единственные повторы имён это дандеры разных классов.Откат
git revert -m 1мерж-коммита, либо удаление ветки без merge. Публичных контрактов срез не меняет:source_bound_identity_v2уже на main из #554, новая функция потребителей не имеет, единственная правка вне тестов — расщепление_derive_comparator_v1на source-bound часть и наблюдения сборки, которое проверяется существующим набором.Незакрытые гейты
Независимое review финального состояния не выполнено — только самопроверка и мутационные доказательства выше.