Proof: the engine's source identity is answerable before its build (V5b2d-4f) - #554
Merged
Conversation
added 2 commits
August 7, 2026 00:27
…5b2d-4f) A coverage pre-check can prove cheaply that a lane set carries exactly two distinct comparator source identities, but not that those identities belong to the engines the job is about to build. The identity had one producer — ComparatorManifestV2, which only exists after the build — so a foreign but internally consistent lane set passed the cheap check and broke only after both native runs, which is the price the pre-check exists to avoid. The eight source-bound coordinates never needed the build: they are a function of the source lock, the admitted upstream closure and the pinned build sources. They now live in one derivation that the build path and a pre-build check both consume, folded by one protocol-owned fold that ComparatorManifestV2 itself uses. Two answers to the same question cannot drift apart, because there is only one statement of it. Boundary this does not cross: three coordinates read per-file data — the tree identity, the archive file manifest and each legal file's mode — that the release lock only commits to through archive_sha256. A caller holding the checkout alone would have to invert a digest, so the pre-check still admits the locked archives first; a test pins that boundary so a later lock revision carrying those coordinates is considered deliberately.
…vable Independent verification found two blocks of defensive code that no test could notice the loss of. `source_bound_identity_v2` validates its kind, its arity and every coordinate, and both callers in the tree validate before they call — so deleting the whole block left the suite green. Removing it would be wrong: it is a public protocol entry point, and refusing malformed input is what every entry point here does. What was missing is the third caller, so these tests stand in for one. They live in their own module because `test_region_proof_protocol.py` carries domain separators with delicate bytes, and a mechanical edit to it introduced corruption that only the parser caught. `ArbSourceBoundPreimagesV1.__post_init__` had the same shape: its neighbour test compares the field order against the protocol directly, which proves the invariant and not the guard. Construction with an empty value, a foreign type, and two coordinates sharing bytes is now refused provably — the last of those matters most, since two coordinates folding to the same bytes would make the identity blind to whichever of them changed. Both suites carry an anti-vacuity case: a guard that refused everything would satisfy the refusal tests and be worthless, so the exact shape must still pass. Proven by the mutant: stripping the fold's validation reddens several of the new tests at once. Both inventory pins recomputed by running the gate, not by hand: 279 tests, inventory abdc4341…, order 4bd4ae23… The outer oracle in `test_build.py` is deliberately independent of `gate.py`, so both had to move. Verified on Linux: fast gate OK with its exact 15-skip manifest, outer oracle OK, 412 tests with the three pre-existing `test_build` failures that also fail on an untouched tree.
|
Warning Review limit reachedYou’ve reached a temporary PR review limit under our Fair Usage Limits Policy. Next review available in: 37 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 (6)
Comment |
added 2 commits
August 7, 2026 09:23
… is pinned Final-state review proved two of my claims false by execution and found the one branch of the construction guard that nothing could see. THE BRANCH. The field-order check against the protocol was unreachable by mutation: both sides read one declaration, so deleting the check left every suite green — exactly the class this slice declares closed, in the block its docstring calls proven. The drift is now injected at the protocol seam (reversed order, extra coordinate), and the mutant that deletes the check reddens both subcases. THE FALSE CLAIMS. I measured mutations on python 3.12, where the strongest anchor — ArbBuildIdentityCharacterizationTests — dies before its subtests, and concluded that a changed domain separator reddens nothing and that coordinate content is pinned nowhere. On 3.13, and in CI's pinned 3.14 container, both are false: the fold's label and order are pinned by the committed COMPARISON_IDENTITY golden, and wrapper/evaluator content is pinned by a semantic oracle plus five golden subtests. What remains true, and is now stated instead: there is no anchor from real GMP/MPFR/FLINT anywhere, and six of the eight coordinates are pinned only characterizationally on a synthetic fixture — self-consistency without semantics. The same measurement error produced the "three pre-existing failures" baseline: they are 3.12-only and do not exist in CI. The guard tests' docstring was a status note about a past defect; it now states the contract. Both inventory pins recomputed by running the gate: 280 tests, inventory cc497572…, order 3a6c3170… Both gates verified green on Linux.
Both sides of the pin conflict were stale by construction — main pinned the join-gate's suite, this branch pinned its own — so neither side was taken. The union was computed by running the gate on the merged tree: 284 tests, 267 base + 4 from the merged executor tests + 13 from this branch, inventory 3284dccf…, order 3625426e… Both pin sites updated; both gates verified green on Linux with the exact 15-skip manifest.
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.
Что это
Дешёвая предпроверка покрытия полос в #549 доказывает, что покрытие — два точных домена, но не что эти две идентичности принадлежат движкам, которые job сейчас соберёт. Чужое, но внутренне согласованное покрытие проходит предпроверку и разбивается только после обоих нативных прогонов — через два часа.
Причина: source-идентичность компаратора была доступна только из манифеста, а манифест появляется после сборки.
Что добавлено
Вывод ожидаемой source-идентичности движка из чекаута, без docker и без сборки. Ключевое свойство: пре-чек и сборочный путь физически идут через одну деривацию и одну свёртку — это стережёт отдельный тест, чувствительность которого доказана честной эмуляцией дубликата на обеих половинах.
Граница доказанного — исправлена по финальному ревью
Первая редакция этого текста содержала два утверждения, опровергнутых исполнением. Я мерил мутации на python 3.12, где сильнейший якорь (
ArbBuildIdentityCharacterizationTests) мёртв до подтестов, а CI гоняет закреплённый python 3.14. Честная граница такова:Закреплено уже сейчас: метка и порядок свёртки — закоммиченным golden
COMPARISON_IDENTITY(подмена домен-сепаратора свёртки и перестановка координат внутри неё краснят); содержимоеwrapper_source/evaluator_source— семантическим оракулом, пересчитывающим оба преимиджа из build-источников по имени, плюс пятью golden-подтестами характеризации.Не закреплено: якоря от реальных GMP/MPFR/FLINT в репозитории не существует — ни архивов, ни закоммиченной квитанции, ни golden от настоящей сборки. Содержимое шести из восьми координат закреплено только характеризационно на синтетической фикстуре: самосогласованность без семантики. «Не доказано, что деривация считает правильные координаты» — верно в этой формулировке, а не в более сильной из первой редакции.
Побочный результат того же замера: «три предсуществующих падения test_build» — специфика python 3.12; на 3.13 и в CI их не существует.
Стражи, все ветви доказаны
Финальное ревью нашло третью ветвь стража конструирования с нулевой чувствительностью: проверка порядка полей против протокола, чью потерю не видел ни один набор — обе стороны читают одну декларацию. Дрейф теперь инжектируется на шве протокола (обратный порядок, лишняя координата), и мутант с удалённой проверкой краснит оба подкейса. Остальные ветви обоих стражей и все ветви публичной свёртки убиты мутациями поимённо, с anti-vacuity в каждом наборе.
Названо и не спрятано
arb.ymlтриггерится только на push в main, поэтому SSOT-страж и стражи преимиджей проверяются только после мержа (per-PR исполняются четыре теста свёртки и пересчёт инвентаря). Раскладка предсуществующая, но этот срез кладёт своё главное доказательство в отложенную половину.expected_comparator_source_identity_v1может поднять голыйTypeErrorиз внутренних путей — две конвенции ошибок на двух публичных входах; дёшево закрывается отдельным срезом.Проверки
test_build.ExistingArbGateTests: OK.Откат
Ревертом. Поведение существующих путей не меняется — деривация вынесена, сборка идёт через неё же.