Repository navigation
Proof: a certified full-domain run declares the work its decision needs (V5b2d-4a) - #546
Conversation
…ds (V5b2d-4a) Наблюдаемый дефект: полнодоменный RUN 31022375756 оставил 44 точки на RESOURCE_LIMIT_REACHED на обоих движках, и compare_dual_transcripts отвергает такой transcript закрыто (unresolved_transcript). Дуальное доказательство полного домена было недостижимо ни в каком процессе. Корень: corpus.full_domain_job_v1 заимствовал политику у замороженной протокольной фикстуры, а та объявляет намеренно враждебный нулевой грант (controller.py: "frozen zero-grant hostile policy"). Грант проверяется ДО запуска ветви предиката, поэтому точка с нулевым бюджетом не решается ни на какой точности — все 44 лежат на границе региона в около-чёрном углу. Закон: решающая процедура тратит не более одной ветви на сегмент региона, то есть max(1, knot_count - 1) на точку. Граница доказуемо точная, поэтому сертифицированная материализация объявляет ровно её. От базовой политики наследуются только лестница точности и equality release. global_pregrant — абсолютный тотал по ordinal-префиксу, а не ставка, поэтому выводится под сертифицируемый домен. Второй дефект того же класса: lane_window_job_v1 зашивал полосе нулевой pregrant. Это верно только при нулевом полном гранте; полоса обязана стартовать с остатка префикса max(0, pregrant - per_point_work*start). Прежний тест утверждал обратное — что при потраченном гранте полоса законно расходится с монолитом; это противоречит требованию order/shard-независимости и был вакуумен при per_point_work=0. Доказательства (RED -> GREEN): - test_certified_policy_leaves_no_unresolved_point: RED оставлял 8 точек seam-домена на исходе 3, включая 65793 = RGB(1,1,1); - test_the_starved_fixture_policy_cannot_decide_the_same_points: anti-vacuity, фиксирует что домен реально входит в оплачиваемую ветвь; - test_certified_domain_carries_the_region_and_its_complement: регион непуст, INSIDE и OUTSIDE присутствуют; - test_lane_window_job_reconstructs_the_ordinal_prefix_grant и ..._clamps_an_exhausted_prefix_to_zero: RED давали 0 вместо остатка; - test_lane_fragments_match_the_monolithic_stream_under_a_spent_grant: побайтовое совпадение полос с монолитом при потраченном гранте. Замороженная фикстура proof-job-v1.bin НЕ изменена: её нулевой грант остаётся враждебным протокольным входом. Локально: 245 тестов, 7 ошибок — ровно базовые пробелы среды Windows (fcntl / native process cwd), новых нет. Гейты репозитория без дрейфа: verify_point_support_surplus PASS, verify_clean_set_receipt PRODUCT_IDENTITY_VERIFIED.
|
Warning Review limit reachedYou’ve reached a temporary PR review limit under our Fair Usage Limits Policy. Next review available in: 28 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 (10)
WalkthroughPR добавляет сертифицированные work budgets для полного домена. Оконные задачи восстанавливают grant-состояние по ordinal-префиксу. Тесты проверяют бюджеты, semantic replay, побайтовое совпадение lane-фрагментов и арность вызовов. ChangesБюджеты полного домена и оконные lanes
Estimated code review effort: 4 (Complex) | ~45 minutes Sequence Diagram(s)sequenceDiagram
participant full_domain_job_v1
participant certified_work_policy_v1
participant lane_window_job_v1
participant run_window_lane_v1
full_domain_job_v1->>certified_work_policy_v1: строит сертифицированную policy
certified_work_policy_v1-->>full_domain_job_v1: возвращает per-point work и global pregrant
lane_window_job_v1->>lane_window_job_v1: считает точки ordinal-префикса
lane_window_job_v1->>run_window_lane_v1: передаёт восстановленный grant
run_window_lane_v1-->>lane_window_job_v1: формирует lane-фрагмент
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 |
…view fixes) Три находки двух независимых ревью финального состояния, все подтверждены. 1. Граница была недостаточной. Кап "одна ветвь на сегмент" действует на ОДИН вызов decide, но бюджет точки общий на всю лестницу: точка, заплатившая ветвь на нижнем рунге и оставшаяся BOUNDARY_UNPROVEN, приходит на следующий рунг ни с чем. Контрпример воспроизведён на замороженных определении и формуле: лестница (16, 64), грант 1 -> ординалы 65792 и 65794 получают RESOURCE_LIMIT_REACHED; грант 2 решает оба. Граница теперь len(precision_ladder) * max(1, knot_count - 1), достаточность структурная: цикл по рунгам исполняется не более len(ladder) раз и каждый вызов тратит не более segments. Минимальность НЕ утверждается. Клейм "proven tight / necessary and sufficient" был overclaim: доказана была только необходимость. Формулировки исправлены в коде и PROTOCOL.md. 2. PROTOCOL.md утверждал отказ full_domain_job_v1 по invalid_policy, которого в коде нет: конструктор безусловно выводит политику. Ложное утверждение в нормативном контракте убрано, записан фактический закон. 3. Префикс полосы считался по абсолютному ординалу окна, а монолит списывает грант один раз на ТОЧКУ ДОМЕНА в порядке итерации. Совпадает только когда домен покрывает все ординалы ниже окна. На домене ((0,128),(65792,65920)) полоса второго диапазона получала pregrant 0 против 128 у монолита и расходилась на всех 128 точках. Введён domain_points_before_v1; на точном полном манифесте поведение не меняется. Бюджет также стал per-comparator: каждый движок объявляет свою лестницу, а общая константа голодала бы того, кто эскалирует дальше. Доказательства: контрпример закреплён регрессией (test_a_single_rung_budget_starves_points_that_escalate падает при границе 1 и проходит при выведенной); DomainPrefixTests закрывают префикс; намеренный саботаж трёх инвариантов подтверждает чувствительность — каждая мутация делает соответствующий тест красным. Локально: 248 тестов, 7 ошибок — ровно базовые пробелы среды Windows.
… left in code Два дефекта моей же правки по ревью. 1. Смена сигнатуры decision_procedure_work_bound_v1 не была проведена по всем вызовам: test_corpus_shards.py звал старую однопараметрическую форму. Модуль целиком не импортируется на Windows (build/transport требует fcntl), поэтому локальный прогон был зелёным, а CI упал с TypeError. Класс закрыт не только правкой вызова: добавлена механическая AST-проверка арности по всему proof/region/v1, которая ловит рассинхрон независимо от того, грузится ли модуль в конкретной среде. Тест заодно стал точнее — читает границу per-comparator, ровно как её выводит certified_work_policy_v1. 2. Overclaim "The bound is proven tight ... necessary and sufficient" был убран из PROTOCOL.md и из docstring decision_procedure_work_bound_v1, но остался дословно в docstring certified_work_policy_v1, а коммит и тело PR заявляли его исправленным. Заявленное не совпало со сделанным. Соседнее утверждение "budget below the bound leaves EVERY boundary point on RESOURCE_LIMIT_REACHED and no proof can exist" под лестничной границей тоже ложно: бюджет ниже границы решает точки, закрывающиеся на первом рунге. Оба переписаны по факту. Заодно снят риторический перебор "starves exactly the points" / "голодает ровно те точки": контрпримером доказано существование голодающих точек, а не то, что голодают все эскалирующие. Проверки: 28 тестов затронутых модулей OK; AST-арность OK по всему дереву; утверждения FullDomainJobTests и DomainPrefixTests исполнены напрямую в обход неимпортируемого харнеса — PASS; grep по "proven tight|necessary and sufficient|доказуемо точн" — пусто.
…ing it Коммит 179c184 заявлял механическую AST-проверку арности как preventive action, но фактически она была разовым скриптом вне репозитория: corrective action существовала, preventive — нет. Заявленное не совпало со сделанным, находка независимого ревью. Гейт теперь часть набора. Он читает дерево как исходник, а не импортирует его, поэтому исполняется и там, где модули не грузятся — ровно в той среде, где рассинхрон сигнатуры и остался незамеченным (build/transport требует Unix-only модулей, из-за чего test_corpus_shards.py целиком исчезает из Windows-прогона). Разрешение имён точное, а не по голому имени: проверяются только вызовы, чью цель можно установить однозначно — module.function через алиас настоящего import модуля дерева, либо function через настоящий from-import. Метод, локальная переменная и вызываемый атрибут пропускаются, а не угадываются, иначе гейт давал бы ложные срабатывания (первая версия матчила set.add на модульную функцию add — 50 ложных). Доказывается только арность, не типы. Чувствительность проверена против РЕАЛЬНОГО дефекта, а не синтетического: временный возврат вызова к однопараметрической форме даёт "tests/test_corpus_shards.py:287: corpus.decision_procedure_work_bound_v1 called with 1 argument(s), definition takes 2..2". Плюс anti-vacuity: гейт падает, если разрешил меньше 100 вызовов или увидел меньше 30 модулей.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 5
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.py (1)
588-590: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick winОтклоняйте окно, которое не полностью покрывает
full_job.domain.Для разреженного
full_job.domaindomain_points_before_v1считает только точки исходного домена, ноwindow_manifestна Lines 588-590 добавляет все ordinals непрерывного интервала. Например, окно[0, 256)для ranges((0, 128), (65792, 65920))запустит ordinals[128, 256), которых нет в монолитном запуске. Lane artifact не сможет совпасть с его фрагментом.
proof/region/v1/corpus.py#L588-L590: до создания manifest проверьте, что число domain points в окне равноwindow_points; иначе вернитеShardCorpusRejectedV1.proof/region/v1/tests/test_corpus_lanes.py#L147-L157: добавьте случай окна, которое пересекает gap, и проверьте типизированный отказ.Предлагаемое исправление
+ window_end = window_start + window_points + if ( + domain_points_before_v1(full_job.domain, window_end) + - domain_points_before_v1(full_job.domain, window_start) + != window_points + ): + return _reject( + ShardCorpusReasonV1.FOREIGN_INPUT, + "lane window must be fully covered by the job domain", + ) window_manifest = protocol.ReducedDomainManifestV1( - ((window_start, window_start + window_points),), window_points + ((window_start, window_end),), window_points )🤖 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.py` around lines 588 - 590, Reject windows that do not fully cover the sparse full_job.domain: before constructing ReducedDomainManifestV1 in proof/region/v1/corpus.py lines 588-590, compare the domain-point count in the window with window_points and return ShardCorpusRejectedV1 when they differ. Add a test covering a window crossing a domain gap in proof/region/v1/tests/test_corpus_lanes.py lines 147-157 and assert the typed rejection.
🤖 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.py`:
- Around line 402-409: Замените исключения TypeError на типизированный результат
отказа во всех публичных путях decision_procedure_work_bound_v1,
domain_points_before_v1, certified_work_policy_v1 и full_domain_job_v1. В
proof/region/v1/corpus.py:402-409, 426-429, 460-463 и 491-492 возвращайте
соответствующую причину invalid вместо завершения исключением. Обновите проверки
в proof/region/v1/tests/test_corpus_shards.py:268-270, 322-326 и 372-377, чтобы
проверять тип и причину отказа вместо assertRaises(TypeError).
In `@proof/region/v1/tests/test_call_arity.py`:
- Around line 41-42: Update _module_name and the cls.defined construction to
prevent duplicate path.stem values from silently overwriting entries: either key
modules by their path relative to the proof root and update _resolve
accordingly, or explicitly detect duplicate stems and fail the test with a typed
error. Do not retain the current plausible fallback behavior when module names
collide.
- Line 149: В цикле, перебирающем self.trees, удалите неиспользуемую переменную
path, сохранив доступ к каждому tree через итерацию по значениям словаря.
- Around line 71-75: В обработке ast.Import обновите создание aliases, чтобы для
точечного импорта без asname использовалось фактически связанное Python-имя
(корневой пакет), а не полный item.name; сохраняйте имя asname при его наличии.
Убедитесь, что алиас записывается только когда связанное имя совпадает со stem
модуля, чтобы вызовы через корректное имя распознавались.
- Around line 159-169: Keep the planted call in
test_the_gate_catches_a_planted_drift intentionally one argument short of
decision_procedure_work_bound_v1’s required positional signature. Update the
test fixture or assertion so _supplied(call) remains less than signature[0] even
if the function signature changes, preserving detection of an incomplete call.
---
Outside diff comments:
In `@proof/region/v1/corpus.py`:
- Around line 588-590: Reject windows that do not fully cover the sparse
full_job.domain: before constructing ReducedDomainManifestV1 in
proof/region/v1/corpus.py lines 588-590, compare the domain-point count in the
window with window_points and return ShardCorpusRejectedV1 when they differ. Add
a test covering a window crossing a domain gap in
proof/region/v1/tests/test_corpus_lanes.py lines 147-157 and assert the typed
rejection.
🪄 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: 12916705-fac3-480d-a5b6-747f4a47a3db
📒 Files selected for processing (9)
proof/region/v1/PROTOCOL.mdproof/region/v1/corpus.pyproof/region/v1/corpus_lane.pyproof/region/v1/tests/test_call_arity.pyproof/region/v1/tests/test_corpus_lanes.pyproof/region/v1/tests/test_corpus_shards.pyproof/region/v1/tests/test_semantic_replay.pyproof/region/v1/tests/test_verification_assembly.pyproof/region/v1/verification_assembly.py
| if type(definition) is not protocol.ContextualRegionDefinitionV1: | ||
| raise TypeError("a work bound requires a canonical region definition") | ||
| if ( | ||
| type(precision_ladder) is not tuple | ||
| or not precision_ladder | ||
| or any(type(rung) is not int for rung in precision_ladder) | ||
| ): | ||
| raise TypeError("a work bound requires a canonical precision ladder") |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | 🏗️ Heavy lift
Возвращайте типизированный отказ из изменённых public paths.
decision_procedure_work_bound_v1, domain_points_before_v1, certified_work_policy_v1 и full_domain_job_v1 выбрасывают TypeError для invalid input. Публичный путь должен возвращать типизированный отказ. Не завершайте вызывающий путь исключением.
proof/region/v1/corpus.py#L402-L409: заменитеTypeErrorна типизированный результат отказа.proof/region/v1/corpus.py#L426-L429: заменитеTypeErrorна типизированный результат отказа.proof/region/v1/corpus.py#L460-L463: заменитеTypeErrorна типизированный результат отказа.proof/region/v1/corpus.py#L491-L492: заменитеTypeErrorна типизированный результат отказа.proof/region/v1/tests/test_corpus_shards.py#L268-L270: проверяйте тип и причину отказа вместоassertRaises(TypeError).proof/region/v1/tests/test_corpus_shards.py#L322-L326: проверяйте тип и причину отказа вместоassertRaises(TypeError).proof/region/v1/tests/test_corpus_shards.py#L372-L377: проверяйте тип и причину отказа вместоassertRaises(TypeError).
As per coding guidelines: «Новый или изменяемый public path не должен вызывать panic ... invalid, unreachable, unsupported и incomplete context должны возвращаться типизированно».
🧰 Tools
🪛 Ruff (0.16.1)
[warning] 403-403: Avoid specifying long messages outside the exception class
(TRY003)
[warning] 409-409: Avoid specifying long messages outside the exception class
(TRY003)
📍 Affects 2 files
proof/region/v1/corpus.py#L402-L409(this comment)proof/region/v1/corpus.py#L426-L429proof/region/v1/corpus.py#L460-L463proof/region/v1/corpus.py#L491-L492proof/region/v1/tests/test_corpus_shards.py#L268-L270proof/region/v1/tests/test_corpus_shards.py#L322-L326proof/region/v1/tests/test_corpus_shards.py#L372-L377
🤖 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.py` around lines 402 - 409, Замените исключения
TypeError на типизированный результат отказа во всех публичных путях
decision_procedure_work_bound_v1, domain_points_before_v1,
certified_work_policy_v1 и full_domain_job_v1. В
proof/region/v1/corpus.py:402-409, 426-429, 460-463 и 491-492 возвращайте
соответствующую причину invalid вместо завершения исключением. Обновите проверки
в proof/region/v1/tests/test_corpus_shards.py:268-270, 322-326 и 372-377, чтобы
проверять тип и причину отказа вместо assertRaises(TypeError).
Source: Coding guidelines
Находка обоих независимых ревью финального состояния: обобщая фикс префикса, я записал безусловное «полоса побайтно равна тому же окну монолитного прогона при любом бюджете», но lane_window_job_v1 принимала окно поверх дыры редуцированного домена — там монолитного референта не существует вовсе. Утверждение было шире провалидированного. Сделано истинным, а не сужено: окно обязано лежать внутри одного диапазона домена, иначе типизированный отказ. Диапазоны отсортированы и никогда не смежны, поэтому вложенность означает вложенность ровно в один диапазон. Побочно снимается бессмысленный полный реплей внедоменных ординалов, который раньше отбрасывался только на сборке. Поздняя защита сборки СОХРАНЕНА и по-прежнему проверяется: полосы приходят файлами из другого прогона и не обязаны проходить через продюсер. Два теста сборки строят враждебную полосу против другого job — это ближе к реальности, чем прежний вариант, где её производил сам продюсер. Заодно снято уцелевшее «starves exactly those points» в комментарии test_corpus_shards.py. Локально: 252 теста, 7 ошибок — ровно базовые пробелы среды Windows.
Три находки CodeRabbit по гейту, все верные. 1. Идентичность модуля по имени файла теряла коллизии. В дереве ДЕСЯТЬ дублей стемов: receipt.py, formula.py, gate.py, native_gate.py, input.py, runtime.py, full_domain_receipt.py и другие живут и под arb/, и под mpfi/. Словарь по стему молча оставлял один из них, после чего вызов сопоставлялся с сигнатурами ЧУЖОГО движка — ложный или пропущенный дрейф. Для гейта это хуже отсутствия: он отвечал правдоподобно и неверно. Ключ теперь точечный путь; голое имя разрешается только пока стем уникален в дереве. Проверено: arb.receipt (22 функции) и mpfi.receipt (14) — разные ключи, стем receipt не разрешается вовсе. 2. Для `import pkg.mod` без asname Python связывает только `pkg`, а код писал ключ `pkg.mod`, который никогда не совпадёт с ast.Name. Тихая потеря покрытия. Теперь такой импорт алиас не создаёт, а from-import различает подмодуль и функцию. 3. Неиспользуемая переменная цикла убрана. Плюс собственная находка исправленного резолвера: он поймал `build_input.seal_input_v1` с одним аргументом в arb/tests/test_transport.py — намеренно неверный вызов внутри `lambda:`, проверяющий отказ. Гейт, срабатывающий на намеренном коде, будет отключён, поэтому он теперь различает намерение: вызовы внутри lambda и внутри тела assertRaises пропускаются. Это стоит покрытия, что видно по anti-vacuity полу, но не порождает ложных срабатываний. Чувствительность после переписывания перепроверена против РЕАЛЬНОГО дефекта: возврат вызова к однопараметрической форме даёт "tests/test_corpus_shards.py:287: corpus.decision_procedure_work_bound_v1 called with 1 argument(s), definition takes 2..2". Локально: 252 теста, 7 ошибок — ровно базовые пробелы среды Windows.
|
@coderabbitai Спасибо — три находки по Коллизия имён модулей (Major) — подтверждена как ЖИВАЯ, не гипотетическая. В дереве десять дублей стемов: Точечный импорт без asname — подтверждён. Неиспользуемая переменная цикла — убрана. Побочно исправленный резолвер нашёл По В
Замечание при этом не считаю ошибочным: Прошу перепроверить |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
git show --stat --oneline 9e009f6
git show --format=fuller --find-renames --find-copies 9e009f6 -- proof/region/v1/tests/test_call_arity.py
ast-grep outline proof/region/v1/tests/test_call_arity.py --items all
ast-grep outline proof/region/v1/corpus.py --items all --match 'decision_procedure_work_bound_v1|certified_work_policy_v1|domain_points_before_v1|full_domain_job_v1|lane_window_job_v1'
rg -n -C 4 --glob '*.py' \
'def (decision_procedure_work_bound_v1|certified_work_policy_v1|domain_points_before_v1|full_domain_job_v1|lane_window_job_v1)\b|test_full_domain_job_rejects_foreign_input|decision_procedure_work_bound_v1\s*\(|certified_work_policy_v1\s*\(|domain_points_before_v1\s*\(' \
proof
rg -n -C 3 --glob '*.py' \
'def seal_input_v1\b|seal_input_v1\s*\(' \
proof/region/v1/arbLength of output: 29757 🏁 Script executed: #!/bin/bash
set -euo pipefail
sed -n '35,260p' proof/region/v1/tests/test_call_arity.py
sed -n '379,605p' proof/region/v1/corpus.py
sed -n '250,390p' proof/region/v1/tests/test_corpus_shards.py
printf '\n-- dotted imports in proof --\n'
rg -n -P --glob '*.py' '^\s*import\s+[A-Za-z_]\w*(?:\.[A-Za-z_]\w*)+(?:\s+as\s+\w+)?(?:\s*,|$)' proof
printf '\n-- assertRaises context forms in proof --\n'
rg -n -C 2 --glob '*.py' '\bassertRaises(?:Regex)?\s*\(' proof
printf '\n-- calls that resolve through module aliases --\n'
rg -n -P --glob '*.py' '^\s*(?:import|from)\s+.*\b(corpus|build_input)\b' proof/region/v1Length of output: 142808
Три находки по
По
Новых замечаний по этому срезу нет. 🐇 ✏️ Learnings added
You are interacting with an AI system. |
|
@coderabbitai full review |
|
Ревью относилось к коммиту 179c184; с тех пор дерево изменилось дважды. Все три находки закрыты в 9e009f6 и проверяемы: коллизия десяти стемов (arb.receipt 22 функции / mpfi.receipt 14 — теперь разные ключи, голое имя receipt не разрешается), точечный импорт без asname больше не создаёт недостижимый алиас, мёртвая переменная убрана. По TypeError из публичных путей ответ с обоснованием в issuecomment-5202207805: норма признана, миграция вынесена отдельным срезом (меняет контракт full_domain_job_v1 на union, пять вызывающих). CodeRabbit повторно упёрся в лимит ревью и подать новое не может; по действующему порядку лимит не является блокером мержа, компенсация — два независимых гетерогенных ревью финального состояния и мутационная проверка 3/3. CI зелёный: 402 теста proof-слоя в двух режимах плюс verify-fixtures.
1 participant
Наблюдаемый дефект
Полнодоменный RUN
31022375756завершился успехом, обе семантические квитанции запечатаны — но дуальный допуск на этих артефактах невозможен:Счётчики транскриптов обоих движков побитово одинаковы:
(INSIDE=0, OUTSIDE=16777172, BOUNDARY_UNPROVEN=0, RESOURCE_LIMIT_REACHED=44). 44 точки не решены, аregion_proof_protocol.py:1878отвергает такой transcript закрыто — по требованию роадмапа «каждая output-точка обязана быть доказанно inside либо outside».Все 44 лежат в около-чёрном углу (
R,G,B ≤ 13) — это контур границы региона, а свидетельства обоих движков байт-идентичны.Корень
corpus.full_domain_job_v1заимствовал политику у замороженной протокольной фикстуры целиком. Но фикстура объявляет намеренно враждебный нулевой грант —controller.pyтак и называет его:frozen zero-grant hostile policy.Грант проверяется до запуска ветви предиката (
semantic/region.py:202,arb/evaluator/region.c:194), поэтому точка с нулевым бюджетом не решается ни на какой точности. Это не дефект точности и не дефект движка — сертифицирующий прогон работал по враждебному тестовому бюджету.Закон
Один вызов
decideтратит не более одной ветви на сегмент региона, но бюджет точки общий на всю лестницу: точка, заплатившая ветвь на нижнем рунге и оставшаясяBOUNDARY_UNPROVEN, приходит на следующий рунг ни с чем. Поэтому граница:Достаточность структурная: цикл по рунгам исполняется не более
len(ladder)раз и каждый вызов тратит не болееsegments. Минимальность НЕ утверждается — меньший грант может оказаться достаточным, но лишь при численном свойстве конкретного определения, здесь не доказанном.Бюджет выводится per-comparator: каждый движок объявляет свою лестницу, а общая константа голодала бы того, кто эскалирует дальше. Сертифицированная материализация объявляет бюджет сама; от базовой политики наследуются только лестница точности и equality release.
global_pregrant— абсолютный тотал по ordinal-префиксу домена, а не ставка, поэтому выводится под сертифицируемый домен.Второй дефект того же класса
lane_window_job_v1зашивал полосеglobal_pregrant = 0. Это верно только пока полный грант нулевой. Полоса обязана стартовать с остатка префиксаmax(0, pregrant − per_point_work × window_start).Прежний тест
test_lane_regime_follows_the_grant_exhaustion_boundaryутверждал обратное — что при потраченном гранте полоса законно расходится с монолитом. Это противоречит требованию order/shard-независимости полнодоменной материализации, и приper_point_work=0тест был вакуумен: веткаany_consumedнедостижима. Заменён контрактом побайтового совпадения в любом режиме гранта.Доказательства (RED → GREEN)
test_certified_policy_leaves_no_unresolved_point65793 = RGB(1,1,1)test_the_starved_fixture_policy_cannot_decide_the_same_pointstest_certified_domain_carries_the_region_and_its_complementtest_lane_window_job_reconstructs_the_ordinal_prefix_grant0 != 12153test_lane_window_job_clamps_an_exhausted_prefix_to_zero0 != …(клампинг)test_lane_fragments_match_the_monolithic_stream_under_a_spent_grantИзмерение на независимой Python-реплике (том самом верификаторе, что уже сверил 16.7 млн точек): при
per_point_work=1все 44 точки решаются на первом рунге 64 бита за одну ветвь — 43 OUTSIDE, 1 INSIDE. Регион на всём sRGB8 содержит ровно одну точку: RGB(1,1,1).Перекрёстная проверка: нативный движок реализует то же правило гранта (
arb/evaluator/main.c:417-431), поэтому правка согласована на обеих сторонах, а не только в реплике.Что НЕ изменено
Замороженная фикстура
proof-job-v1.binне тронута — её нулевой грант остаётся легитимным враждебным протокольным входом. Пиныcontroller.pyи идентичности вtest_region_proof_protocol.pyне сдвинуты.Последствие
Идентичность сертифицированной полнодоменной задачи меняется:
Бюджет для замороженной лестницы
(64, 128):per_point_work = 2,global_pregrant = 2 × 2^24. Неизрасходованный грант ничего не стоит, поэтому цена нулевая.Это новый proof release по правилу роадмапа «изменение ladder/budget создаёт новый proof release». Существующие evidence и 512 lane-артефактов от RUN
31022375756становятся вытесненными и требуют перевыпуска.Правки по независимому ревью (коммит b419759)
Два независимых ревью финального состояния нашли три подтверждённых дефекта; все закрыты.
(16, 64), грант 1 → ординалы 65792 и 65794 получаютRESOURCE_LIMIT_REACHED, грант 2 решает оба. Прежний клейм «proven tight / necessary and sufficient» был overclaim — доказана была только необходимость. Контрпример закреплён регрессией.PROTOCOL.mdзаявлял отказ поinvalid_policy, которого в коде нет. Ложное утверждение в нормативном контракте убрано.((0,128),(65792,65920))полоса второго диапазона получала pregrant 0 против 128 у монолита и расходилась на всех 128 точках. Введёнdomain_points_before_v1; на точном полном манифесте поведение не меняется.Мутационная чувствительность. Намеренный саботаж трёх инвариантов — каждая мутация делает соответствующий тест красным:
Проверки
fcntl,invalid native process cwd), новых нет. База до правки: 240/7.PYTHONOPTIMIZE=2) плюсcontroller.py verify-fixtures— всё зелёное. Это и есть настоящая проверка тестов, которые не грузятся на Windows.scripts/verify_point_support_surplus.py— PASS.scripts/verify_clean_set_receipt.py product --product-root .— PRODUCT_IDENTITY_VERIFIED.Rollback
git revertодного коммита. Правка чисто вычислительная: артефакты на диске не переписываются, замороженные фикстуры и пины не тронуты.Точность формулировки о локальных свидетельствах
tests/test_corpus_shards.pyцеликом не импортируется на Windows (build/transport.pyпадает на импорте — цепочка предсуществующая, правкой не тронута). Поэтому новые тесты деривации в этом модуле локально не исполнялись как тесты; их утверждения проверены прямым вызовом функций. Настоящую проверку даёт CI, где модуль загружается и исполняется.CodeRabbit
Упёрся в лимит ревью (
Review limit reached) — содержательных ревью ноль, зелёная галка это pass-through лимита. Компенсация по действующему порядку: два независимых гетерогенных ревью, отчёты выше.Summary by CodeRabbit
Новые возможности
Документация
Тесты