Proof: independent semantic verifier replays engine transcripts and seals receipts (V5b2c) - #521
Merged
Merged
Conversation
added 4 commits
August 4, 2026 07:39
Third verifier re-parses the immutable formula bytes with its own strict reader (ssa.py), re-derives every decision through rigorous interval arithmetic (intervalmath.py) and the driver rules (region.py), and replays the claimed transcript decision by decision (replay.py). A clean replay seals SemanticVerificationReceiptV1; any mismatch, witness defect or accounting drift rejects with a closed rejection reason before or during replay. Run binding: the verifier admits a run only when its job, comparator and transcript coordinates match the verified objects. binary_identity, invocation_identity and platform_identity stay declared execution coordinates - their source->build->executable causality belongs to the source-bound controller and the semantic verifier never re-declares that anchor. Interval arithmetic keeps exact rational endpoints and gains adaptive Taylor remainders: series stop as soon as a rigorous tail bound clears the guard target, ln(2)/pi enclosures are cached, and odd-power partial sums evaluate through one integer Horner pass. Point lift drops from 9.65 s to 0.028 s; every enclosure was cross-checked against mpmath dps=200 truth values. Gates: 17 semantic tests including a positive full-domain replay that seals a receipt, protocol suite 39 OK, compileall clean.
pow_nn no longer proves exact zero when the exponent crosses zero, and root3 enforces its nonnegative domain grammar, matching both engines' DOMAIN_UNPROVEN fallback. exp rejects arguments beyond the V1 reduction range and bounds its branch loop, so hostile binary64 inputs terminate in typed rejection instead of overflow or runaway reduction. verify_transcript rejects transcripts whose point count drifts from the bound domain before replay. Diversity stays enforced by the AST boundary test; the unused diversity_violation rejection reason leaves the closed sum. PROTOCOL.md documents the operator domain guards and the deliberate sign strictness. New regression tests: point-count drift, operator domain contracts, and rational-window soundness checks pinning every transcendental enclosure around 20-digit truth values. Gates: 56 tests OK, compileall clean.
|
Warning Review limit reachedYou’ve reached a temporary PR review limit under our Fair Usage Limits Policy. Next review available in: 42 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)
WalkthroughДобавлена независимая stdlib-only semantic verification boundary для V1 transcript-ов. Она разбирает SSA, выполняет точный replay region decisions, проверяет witness-ы и accounting, затем создаёт sealed receipt или typed rejection. ChangesSemantic verification V1
Estimated code review effort: 5 (Critical) | ~120 минут Sequence Diagram(s)sequenceDiagram
participant Transcript
participant verify_transcript
participant SemanticReplay
participant SSA_EvaluationContext
participant SemanticVerificationReceiptV1
Transcript->>verify_transcript: submit job, comparator, run, transcript
verify_transcript->>SemanticReplay: initialize canonical replay
SemanticReplay->>SSA_EvaluationContext: parse formula and evaluate region programs
SSA_EvaluationContext-->>SemanticReplay: point decision and resource result
SemanticReplay-->>verify_transcript: replay result and accounting record
verify_transcript->>SemanticVerificationReceiptV1: seal after all checks pass
SemanticVerificationReceiptV1-->>verify_transcript: receipt or typed rejection
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 |
Collaborator
Author
|
@coderabbitai review |
✅ Action performedReview finished.
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 29
🤖 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 733-742: Исправьте опечатку в описании доменных guard’ов
операторов: замените латинскую букву `t` в начале слова «tочный» на
кириллическую «т», чтобы получилось «точный».
In `@proof/region/v1/semantic/__init__.py`:
- Around line 8-20: Замените абсолютные импорты в пакете semantic на
относительные, сохранив импорт символов из receipt, rejected-типов и
verify_transcript из verifier при импорте как proof.region.v1.semantic. Также
отсортируйте элементы __all__ в порядке, требуемом RUF022.
In `@proof/region/v1/semantic/intervalmath.py`:
- Around line 506-526: Ограничьте перебор в _reduce_quadrant, чтобы большие
аргументы не приводили к неограниченным вычислениям: введите явный
типизированный отказ при превышении допустимого числа кандидатов или величины
value и корректно распространите его через пути sin и cos. Зафиксируйте
выбранный предел и поведение отказа в PROTOCOL.md рядом с ограничением reduction
range для exp; не используйте panic или приблизительный fallback.
- Around line 529-574: Remove the remainder-out-of-range fallback branches from
sin and cos; do not return Interval(-1, 1). Let _reduce_quadrant’s invariant
stand, and preserve the existing lo > hi checks to report missing quadrant
coverage through UnresolvedError.
In `@proof/region/v1/semantic/receipt.py`:
- Around line 69-81: Prevent subclassing of SemanticVerificationReceiptV1 by
enforcing sealed-type inheritance restrictions in addition to the _RECEIPT_TOKEN
check. Ensure any attempted subclass definition is rejected, so only
verify_transcript can create receipts with the inherited binds, encode, and
identity behavior.
- Around line 112-181: Add a regression test that compares
resolved_decision_digest_v1(...) with candidate.claim.decision_digest when both
use identical decision_bits, matching the domain and field ordering used by
compare_dual_transcripts and PROTOCOL.md. Keep the implementations tested
independently while asserting their digest outputs are equal.
In `@proof/region/v1/semantic/region.py`:
- Around line 164-174: Добавьте проверку пустого `region.knots` в начале
соответствующего пути перед обращением к `region.knots[0]` и `region.knots[-1]`,
возвращая типизированный отказ `DecisionResult` вместо допуска `IndexError`;
сохраните существующую обработку одиночного узла через `_evaluate_singleton` и
последующую логику для регионов с узлами.
- Around line 247-252: Переместите распаковку `outputs["jp"]`, `outputs["ap"]` и
`outputs["bp"]` в защищённый блок вокруг вызова `ssa.evaluate` в проверке
point-программы. Обработайте отсутствующие выходы так же, как
`intervalmath.UnresolvedError` и `SemanticFormulaError`, возвращая
типизированный `DecisionResult(BOUNDARY_UNPROVEN, 0, False, 0)` вместо
распространения `KeyError`.
- Around line 41-43: Export a public `dyadic_to_fraction` helper from the
protocol module and replace all three `protocol._dyadic` usages in
`Region.from_definition` and its surrounding logic with that API. Also remove
the unnecessary quotes from the `-> "Region"` return annotation, leaving it as
`-> Region` under postponed annotations.
- Around line 193-229: Update the grant-exhaustion check in the surrounding
segment-processing loop to use a greater-than-or-equal comparison, so consumed
budgets at or beyond grant immediately return RESOURCE_LIMIT_REACHED. Preserve
the existing DecisionResult values and subsequent processing for budgets that
remain available.
- Around line 19-22: Замените локальные числовые коды INSIDE, OUTSIDE,
BOUNDARY_UNPROVEN и RESOURCE_LIMIT_REACHED ссылками на соответствующие члены
protocol.DecisionV1, сохранив доступные имена для verifier.py и тестов.
Убедитесь, что значения вычисляются из канонического перечисления при загрузке
модуля, чтобы несовпадение с DecisionV1 сразу приводило к ошибке.
- Around line 109-112: Обновите путь `_predicate_decision` → `decide` →
`evaluate_rgb` и внешний цикл `verify_transcript`, чтобы ошибки
`SemanticFormulaError` и отсутствующая программа (`KeyError`) не выходили через
публичную границу проверки. Перехватите их вместе с существующими
`intervalmath.UnresolvedError` и `replay.ReplayIntegrityError`, сохранив typed
rejection вместо panic для программ `singleton` и `segment`.
- Around line 40-54: Перед семантическим replay в verify_transcript зафиксируйте
исходный ProofJobV1 через protocol.snapshot_proof_job_v1 и используйте
полученный snapshot дальше. Обработайте IndexError и ProtocolErrorV1 при
построении Region через from_definition как типизированный отказ, сохранив
текущий путь успешной проверки.
In `@proof/region/v1/semantic/replay.py`:
- Around line 129-138: Обновите создание PointReplay в данном участке так, чтобы
все восемь аргументов передавались по именам полей, включая consumed,
point_grant, resource_scope и exact_branch. Сохраните существующее соответствие
каждого значения одноимённому полю и не меняйте остальную логику.
- Around line 89-91: Замените материализацию `job.domain.iter_ordinals()` в
инициализации `self._ordinals` на ленивый итератор, сохранив последовательное
чтение ординалов в `next_point`. Уберите логику, предполагающую наличие кортежа
или произвольный доступ по индексу, но сохраните существующее поведение курсора
и обработки исчерпания домена.
- Around line 141-147: Добавьте аннотацию возврата -> None к
ReplayIntegrityError.__init__ и переместите объявление ReplayIntegrityError выше
SemanticReplay, чтобы исключение было объявлено до его использования в
next_point; остальное поведение класса сохраните.
- Around line 109-111: Validate that budget.precision_ladder is non-empty in the
relevant __init__ method before verify_transcript can access ladder[0], and
reject an empty ladder with the established typed validation error. Preserve
normal initialization and verification behavior for non-empty ladders, including
the existing final_precision setup.
- Around line 50-61: Update accounting_prefix_v1 to handle unsupported
ComparatorKindV1 values explicitly instead of allowing
ACCOUNTING_DOMAINS_V1[kind] to raise KeyError. Raise the repository’s
established typed validation/error type with a clear unsupported-comparator
message, so verify_transcript receives a typed failure at its public boundary.
- Around line 39-70: Добавьте независимый тестовый вектор для digest,
формируемого через accounting_prefix_v1 и account_record: зафиксируйте engine
transcript bytes и ожидаемый digest, затем сравните их с результатом
replay-реализации. Не ограничивайтесь test_replayed_transcript_seals_a_receipt,
поскольку он использует те же функции; проверьте соответствие доменов, порядка
полей и ширин 4/4/8/1.
In `@proof/region/v1/semantic/ssa.py`:
- Around line 199-212: Согласуйте ветку проверки оператора eq в проверке
семантики с ограничениями _evaluate_node: разрешайте сравнение только одинаковых
дискретных типов, исключив real и decode_table. Сохраните требование ровно двух
аргументов и одинаковости их типов, чтобы неподдерживаемые сравнения отклонялись
при разборе через SemanticFormulaError.
- Around line 360-392: Вынесите создание значений литералов из горячего пути:
добавьте кеш декодированных `Interval` в `SemanticFormula`, рассчитанный один
раз для `self.formula.literals`, и в `evaluate` используйте его вместо
повторного вызова `binary64_to_fraction` и `intervalmath.exact`. Сохраните
текущее сопоставление имён литералов и их значений.
In `@proof/region/v1/semantic/verifier.py`:
- Around line 42-48: Update verify_transcript’s canonical object validation to
return a SemanticVerificationRejectedV1 with a new INVALID_INPUT reason instead
of raising TypeError, ensuring every noncanonical argument remains within the
VerificationResultV1 result path.
In `@proof/region/v1/tests/test_semantic_diversity.py`:
- Around line 21-37: Strengthen the independence scan by updating
SEMANTIC_SOURCES to recurse with rglob, and revise _imported_roots() to inspect
every import-path component, including names in relative ImportFrom nodes with
no module. Extend the AST checks to reject dynamic imports through both
__import__ and importlib.import_module, then add negative tests covering nested
modules, relative executor imports, qualified proof.region.v1.executor imports,
and both dynamic-import forms.
In `@proof/region/v1/tests/test_semantic_intervalmath.py`:
- Around line 124-168: Добавьте в OperatorDomainContractTests тесты для
публичного ratio0, проверив особое поведение 0/0 и отклонение нулевого либо
неопределённо знакового делителя, а также тесты для sin и cos с аргументом за
пределами допустимого диапазона редукции, ожидающие UnresolvedError. Используйте
существующие helper call, CAP и стили проверок класса.
In `@proof/region/v1/tests/test_semantic_replay.py`:
- Around line 223-287: Расширьте тестовый модуль фикстурой транскрипта,
созданного реальным semantic replay engine, вместо построения decisions,
witnesses и accounting через те же функции, которые проверяет verify_transcript.
В test_replayed_transcript_seals_a_receipt используйте эту engine-produced
fixture с run_claim и подтвердите выдачу SemanticVerificationReceiptV1 и
корректную привязку к job, comparator, run и transcript; формат фикстуры должен
явно содержать engine-generated decisions, witnesses и accounting digest.
- Around line 205-216: Update the packed-decision byte length in the
DecisionTranscriptV1 fixture construction to round drifted_count up for four
decisions per byte, preserving the declared count even when it is not divisible
by four. Keep the existing byte-fill pattern and drift-count setup unchanged.
- Around line 229-273: Update the test loop around decisions and witnesses to
assert that the fixture produces each witness-producing outcome: exact-boundary
INSIDE, BOUNDARY_UNPROVEN, and RESOURCE_LIMIT_REACHED, before constructing the
transcript. Replace the untyped witnesses list with a union of
ExactZeroSignalTraceV1, BoundaryUnprovenWitnessV1, and ResourceLimitWitnessV1.
- Around line 138-145: Update test_saturate_all_inside_transcript_fails_replay
to assert the specific expected result.reason for saturation-induced replay
failure, matching the explicit reason checks used by the neighboring tests,
rather than only checking SemanticVerificationRejectedV1.
- Around line 121-136: Update
test_two_identical_wrong_transcripts_both_fail_replay to assert that both
rejected results have a reason other than FOREIGN_BINDING, while preserving the
existing checks for deterministic rejection and matching ordinals.
🪄 Autofix (Beta)
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: 4fa8b195-d912-44a5-b06d-f6c6d896d7fe
📒 Files selected for processing (12)
proof/region/v1/PROTOCOL.mdproof/region/v1/semantic/__init__.pyproof/region/v1/semantic/intervalmath.pyproof/region/v1/semantic/receipt.pyproof/region/v1/semantic/region.pyproof/region/v1/semantic/replay.pyproof/region/v1/semantic/ssa.pyproof/region/v1/semantic/verifier.pyproof/region/v1/tests/test_semantic_diversity.pyproof/region/v1/tests/test_semantic_intervalmath.pyproof/region/v1/tests/test_semantic_receipt.pyproof/region/v1/tests/test_semantic_replay.py
- intervalmath: sin/cos unresolved beyond the 2^12 V1 reduction range; drop the unreachable hull fallbacks - region: bind outcome codes to DecisionV1, typed empty-knot rejection, widen predicate catch, guarded output unpack, >= grant check, public dyadic_field_v1 - replay: ReplayIntegrityError moved above its raiser, empty ladder + unknown kind + exhausted ordinals are typed errors, streaming ordinals, keyword PointReplay - verifier: noncanonical inputs reject as invalid_input instead of raising; init/loop catches cover IndexError, ProtocolErrorV1 and ReplayIntegrityError - receipt: INVALID_INPUT reason, final type guard - ssa: eq admits discrete operands only at parse; literal environment cached once per formula - semantic/__init__: relative imports, sorted __all__ - PROTOCOL.md: typo fix, sin/cos guard rule, invalid_input + final documented - tests: hardened diversity checker with synthetic negative cases, dual admission digest parity, independent accounting vector, ratio0/sin/cos domain tests, tighter rejection assertions
Collaborator
Author
|
@coderabbitai review |
✅ Action performedReview finished.
|
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/region_proof_protocol.py`:
- Around line 265-268: Обновите public-функцию dyadic_field_v1, чтобы до вызова
_dyadic она проверяла, что bits имеет тип bytes, и для любого другого входа
возвращала ProtocolErrorV1 через существующий механизм _fail вместо передачи
значения в len. Сохраните текущую обработку корректных bytes без изменений.
In `@proof/region/v1/tests/test_semantic_diversity.py`:
- Around line 33-41: Update the Import handling in the AST root-collection logic
to add every component of alias.name, not only the first component, while
preserving the existing ImportFrom behavior. Extend the relevant
semantic-diversity test with a negative case for `import
proof.region.v1.executor`, ensuring this dependency is rejected and the
verifier’s independence check covers the AST import path.
In `@proof/region/v1/tests/test_semantic_replay.py`:
- Around line 343-364: Добавьте в тест рядом с существующим вектором ARB
независимую проверку для ComparatorKindV1.MPFI: создайте MPFI-компаратор,
вручную соберите ожидаемый SHA-256 с MPFI domain identity и теми же полями
записей, затем сравните его с digest, полученным через accounting_prefix_v1 и
account_record. Не переиспользуйте ожидаемый digest или внутренний результат
accounting_prefix_v1 для вычисления эталона.
🪄 Autofix (Beta)
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: 35714452-d03d-48a5-937d-48a8ae84e847
📒 Files selected for processing (13)
proof/region/v1/PROTOCOL.mdproof/region/v1/region_proof_protocol.pyproof/region/v1/semantic/__init__.pyproof/region/v1/semantic/intervalmath.pyproof/region/v1/semantic/receipt.pyproof/region/v1/semantic/region.pyproof/region/v1/semantic/replay.pyproof/region/v1/semantic/ssa.pyproof/region/v1/semantic/verifier.pyproof/region/v1/tests/test_semantic_diversity.pyproof/region/v1/tests/test_semantic_intervalmath.pyproof/region/v1/tests/test_semantic_receipt.pyproof/region/v1/tests/test_semantic_replay.py
This was referenced Aug 4, 2026
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.
Срез
Третий независимый верификатор региона: stdlib-only Python-пакет
proof/region/v1/semantic/, который самостоятельно replay'ит один engine transcript и запечатываетSemanticVerificationReceiptV1либо возвращает типизированный отказ. Узел correctness-цепи из #228: semantic verifier → DualProofReceiptV1 (V5b2d) → full-domain materialisation.Что внутри
ssa.py— строгий повторный разбор committed ASCII SSA spec собственным reader'ом (release-pinned digest), без доверия engine-парсеру.intervalmath.py— строгая интервальная арифметика на exact dyadicFraction: ряды с рациональными хвостами (atanh/atan), Лагранж для exp, редукция против рациональных огораживаний ln 2 и π (формула Мэчина), outward-округление на dyadic сетку. Адаптивные остатки: ряд останавливается, когда строгая граница хвоста достигает guard-цели; подъём точки 9.65 s → 0.028 s.region.py/replay.py— повторный вывод решений региона (INSIDE/OUTSIDE/BOUNDARY_UNPROVEN/RESOURCE_LIMIT_REACHED), exact-zero trace replay и accounting digest по общим wire-грамматикам.verifier.py+receipt.py— sealed receipt (module-owned token), закрытая сумма причин отказа, binding-проверки до replay.Принятые решения
binary_identity/invocation_identity/platform_identity— заявленные execution coordinates; их причинность source → build → executable доказывает source-bound controller, верификатор не дублирует anchor (совместимо с productionRunClaimV1.for_transcript, где передаётсяbinary_sha256 ≠ manifest.build_identity).root3/logнеразрешимы на отрицательных и пересекающих ноль интервалах,pow_nnдоказывает точный ноль только при строго положительной экспоненте,expнеразрешим за пределами V1 reduction range — по грамматикам операторов и паритету с обоими двигателями (DOMAIN_UNPROVEN →BoundaryUnproven).signуводит точку вBoundaryUnproven— сознательное ужесточение относительно продолжения engine с hull[-1, 1].arb//mpfi//evaluator paths); неиспользуемая причинаdiversity_violationудалена из закрытой суммы.Доказательства
b654824: hostile-replay контракт, 5 тестов падали на заглушке.test_region_proof_protocol,test_semantic_replay+ positive-path full-domain receipt,test_semantic_receipt,test_semantic_diversity,test_semantic_intervalmath— рациональные окна вокруг 20-значных истин для каждого трансцендентного огораживания),compileallчист.pow_nn,root3) и 2 robustness-находки (point_count drift, exp overflow) воспроизведены исполнением и закрыты регрессионными тестами вc93d15f.Гейты
CI (ci-worker pinned) + CodeRabbit на head. PROTOCOL.md дополнен секцией semantic verification.
Summary by CodeRabbit
Новые возможности
Тесты