Skip to content
43 changes: 41 additions & 2 deletions proof/region/v1/PROTOCOL.md
Original file line number Diff line number Diff line change
Expand Up @@ -478,13 +478,52 @@ V1 не доказывает independence. Как anti-vacuum declared-diversity
dependency graph; cross-path GMP/MPFR overlap и обязательные distinct edges не
считаются установленными без отдельного MPFI receipt.

### Две идентичности компаратора

`identity` связывает все десять координат, включая `build_identity` и
`test_observation`. Эти две сворачивают наблюдение сборки — docker capability и
digest-ы консольного вывода процессов, — и потому **не воспроизводятся**: два
прогона идентичного дерева исходников на двух раннерах дают одинаковый бинарь и
одинаковые решения, а наблюдения различаются. Замерено на прогонах
`31089986150`/`31090010890`: `binary_identity` равны; внутри `build_identity`
различаются ровно 96 байт (32 docker capability + 2×32 наблюдения процессов), и
отдельно различается `test_observation` у Arb, который сворачивает те же
наблюдения процессов.

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

📐 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


`source_identity` связывает kind и восемь координат, выводимых из источников:
`engine_release`, `upstream_source`, `arithmetic_input_set`, `wrapper_source`,
`evaluator_source`, `operation_allowlist`, `legal_file_set`, `exclusions`.
Лейбл — `labcolors.proof-region.comparator-source-identity.v2`. Это производное
свойство, а не поле wire: грамматика манифеста не меняется.

Разделение проходит по вопросу «может ли решение от этого зависеть»:

- **решающая цепь** связывает `source_identity` — движку передаётся именно она
в `--manifest-identity`, поэтому её несут `DecisionTranscriptV1`,
`RunClaimV1`, accounting-префикс и lane-манифест (ключ
`comparator_source_identity`). Решение точки не зависит от того, какой демон
наблюдал сборку, поэтому полоса, посчитанная под одним прогоном, допускается
под другим прогоном тех же источников. Без этого каждая verification lane
умирала бы вместе с прогоном, выпустившим её evidence, и дуальное
доказательство было бы недостижимо: source-bound квитанции не имеют
wire-формы намеренно, а посчитать 512 полос внутри процесса RUN нельзя;
- **цепь провенанса** связывает полную `identity` — её несут
`DualComparisonClaimV1.comparator_identities`, `SemanticVerificationReceiptV1`
и обе source-bound квитанции. Какая именно сборка произвела каждый движок —
ровно то, что дуальное доказательство и удостоверяет, и эта запись не
ослабляется.

Изменение любой из восьми source-координат меняет `source_identity` и
закрыто отвергает чужую полосу; изменение наблюдения сборки — нет.

Comment thread
coderabbitai[bot] marked this conversation as resolved.
## `DecisionTranscriptV1`

Wire после `LCTRN1\0\0`, по порядку:

1. job identity;
2. domain identity;
3. comparator manifest identity;
3. comparator **source** identity — движку передаётся именно она, и он
echo-ит её в header; см. «Две идентичности компаратора»;
4. point count `u64be`;
5. decision payload `blob`;
6. counters `inside`, `outside`, `boundary_unproven`,
Expand Down Expand Up @@ -566,7 +605,7 @@ counters не превращают его в semantic resolved/proven type.
Wire после `LCRUN1\0\0` содержит шесть digest coordinates:

1. job identity;
2. comparator manifest identity;
2. comparator **source** identity — та же координата, что несёт транскрипт;
3. exact binary identity;
4. exact invocation identity;
5. platform identity;
Expand Down
8 changes: 5 additions & 3 deletions proof/region/v1/arb/receipt.py
Original file line number Diff line number Diff line change
Expand Up @@ -295,8 +295,10 @@ def _run_identity_v1(
executable=build.binary,
argv=(
b"arb-evaluator",
# The engine binds what it is told, and a decision cannot depend
# on the observation of the build: it is told the source identity.
b"--manifest-identity",
build.comparator.identity.hex().encode("ascii"),
build.comparator.manifest.source_identity.hex().encode("ascii"),
b"--job",
b"/dev/stdin",
),
Expand All @@ -323,7 +325,7 @@ def _run_identity_v1(
or transcript.encode() != process.stdout
or transcript.job_identity != request.job.identity
or transcript.domain_identity != request.job.domain.identity
or transcript.comparator_identity != build.comparator.identity
or transcript.comparator_identity != build.comparator.manifest.source_identity
or transcript.point_count != request.job.domain.point_count
):
raise TypeError("controller-observed RUN did not replay")
Expand Down Expand Up @@ -1237,7 +1239,7 @@ def execute(self, request: pipeline.PipelineRequestV1) -> SourceBoundResultV1:
argv=(
b"arb-evaluator",
b"--manifest-identity",
built.comparator.identity.hex().encode("ascii"),
built.comparator.manifest.source_identity.hex().encode("ascii"),
b"--job",
b"/dev/stdin",
),
Expand Down
7 changes: 7 additions & 0 deletions proof/region/v1/arb/tests/full_domain_receipt.py
Original file line number Diff line number Diff line change
Expand Up @@ -90,8 +90,15 @@ def test_full_domain_build_run_seal_and_verification_evidence(self) -> None:
transcript.domain_identity,
protocol.exact_full_domain_manifest_v1().identity,
)
# The engine echoes the coordinate it was told, and it is told the
# comparator's source identity: the decision chain must stay portable
# across runs whose build observations differ.
self.assertEqual(
transcript.comparator_identity,
result.comparator.manifest.source_identity,
)
self.assertNotEqual(
result.comparator.manifest.source_identity,
result.comparator.manifest.identity,
)

Expand Down
9 changes: 7 additions & 2 deletions proof/region/v1/corpus.py
Original file line number Diff line number Diff line change
Expand Up @@ -167,8 +167,11 @@ def __init__(
retain_records: bool = False,
) -> None:
self._replay = semantic_replay.SemanticReplay(job, comparator)
# The accounting stream belongs to the decision chain, so it binds
# the reproducible source identity: a lane replayed against another
# run of the same sources must produce the same digest.
self._accounting = semantic_replay.accounting_prefix_v1(
comparator.manifest.kind, job, comparator.identity
comparator.manifest.kind, job, comparator.source_identity
)
if evidence_job_identity is None:
evidence_job_identity = job.identity
Expand Down Expand Up @@ -358,7 +361,9 @@ def assemble_transcript_from_shards_v1(
transcript = protocol.DecisionTranscriptV1(
job.identity,
domain.identity,
comparator.identity,
# Byte-identical to the engine's own transcript, so it records the
# same comparator coordinate the engine was told.
comparator.source_identity,
domain.point_count,
decision_bits,
tuple(counters),
Expand Down
8 changes: 4 additions & 4 deletions proof/region/v1/corpus_assembly.py
Original file line number Diff line number Diff line change
Expand Up @@ -140,7 +140,7 @@ def load_lane_v1(
"job_identity": job.identity,
"domain_identity": job.domain.identity,
"policy_identity": job.policy.identity,
"comparator_identity": comparator.identity,
"comparator_source_identity": comparator.source_identity,
}
for key, expected in identities.items():
value = _parse_hex_identity(manifest.get(key))
Expand Down Expand Up @@ -197,7 +197,7 @@ def load_lane_v1(
if type(window_job) is not protocol.ProofJobV1:
return window_job
window_accounting = semantic_replay.accounting_prefix_v1(
comparator.manifest.kind, window_job, comparator.identity
comparator.manifest.kind, window_job, comparator.source_identity
)
window_accounting.update(records)
if window_accounting.digest().hex() != manifest.get(
Expand Down Expand Up @@ -327,7 +327,7 @@ def assemble_lanes_v1(
cursor = current_range[0]
shards: list[corpus.ShardArtifactV1] = []
accounting = semantic_replay.accounting_prefix_v1(
comparator.manifest.kind, job, comparator.identity
comparator.manifest.kind, job, comparator.source_identity
)
for lane in lanes:
if type(lane) is not AdmittedLaneV1:
Expand Down Expand Up @@ -417,7 +417,7 @@ def main(argv: list[str] | None = None) -> int:
"job_identity": job.identity.hex(),
"domain_identity": job.domain.identity.hex(),
"policy_identity": job.policy.identity.hex(),
"comparator_identity": comparator.identity.hex(),
"comparator_source_identity": comparator.source_identity.hex(),
"transcript_identity": transcript.identity.hex(),
"accounting_digest": transcript.accounting_digest.hex(),
"point_count": transcript.point_count,
Expand Down
38 changes: 27 additions & 11 deletions proof/region/v1/corpus_lane.py
Original file line number Diff line number Diff line change
Expand Up @@ -32,22 +32,35 @@

FIXTURE_JOB_V1 = PROOF / "fixtures" / "proof-job-v1.bin"
DEFAULT_SHARD_POINTS = 1 << 14
LANE_SCHEMA_V1 = "corpus-lane-v1"
# v2 renamed the comparator coordinate and changed what it means: a lane now
# binds the comparator source identity. An unchanged version string would let
# a v1 lane be rejected as a foreign comparator instead of an older grammar,
# which is a misleading diagnosis for an artifact that was never wrong.
LANE_SCHEMA_V1 = "corpus-lane-v2"
RECORD_BYTES_V1 = 17


def lane_comparator_v1() -> protocol.ContentResolvedComparatorManifestV2:
def lane_comparator_contents_v1() -> dict[bytes, bytes]:
"""Content map of the lane comparator, keyed by its manifest addresses.

One source of truth for the coordinates: anything that needs to rebuild
the bundle reads it here instead of restating the generator, where a
second copy would drift and surface as an unresolved content address
rather than as the mismatch it really is.
"""

contents = tuple(
f"corpus-lane-coordinate-{index}".encode("ascii") for index in range(10)
)
return {hashlib.sha256(content).digest(): content for content in contents}


def lane_comparator_v1() -> protocol.ContentResolvedComparatorManifestV2:
contents = lane_comparator_contents_v1()
manifest = protocol.ComparatorManifestV2(
protocol.ComparatorKindV1.ARB,
*(hashlib.sha256(content).digest() for content in contents),
)
return protocol.ContentResolvedComparatorManifestV2.admit(
manifest,
{hashlib.sha256(content).digest(): content for content in contents}.get,
protocol.ComparatorKindV1.ARB, *contents
)
return protocol.ContentResolvedComparatorManifestV2.admit(manifest, contents.get)
Comment thread
coderabbitai[bot] marked this conversation as resolved.


BUNDLE_MANIFEST_NAME_V1 = "comparator-manifest-v2.bin"
Expand Down Expand Up @@ -175,15 +188,18 @@ def fail(detail: str) -> NoReturn:
" transcript")
if type(run_claim) is not protocol.RunClaimV1:
fail("verification evidence requires the engine's sealed run claim")
# The engine is told the comparator's source identity, so that is what its
# transcript and run claim carry; the bundle below still ships the full
# manifest, so the environment record travels with the evidence.
if (
transcript.job_identity != job.identity
or transcript.comparator_identity != resolved.identity
or transcript.comparator_identity != resolved.source_identity
):
fail("verification evidence transcript does not bind the receipt's"
" job and comparator")
if (
run_claim.job_identity != job.identity
or run_claim.comparator_identity != resolved.identity
or run_claim.comparator_identity != resolved.source_identity
or run_claim.transcript_identity != transcript.identity
):
fail("verification evidence run claim does not bind the receipt's"
Expand Down Expand Up @@ -240,7 +256,7 @@ def write_lane_artifacts_v1(
"job_identity": job.identity.hex(),
"domain_identity": job.domain.identity.hex(),
"policy_identity": job.policy.identity.hex(),
"comparator_identity": comparator.identity.hex(),
"comparator_source_identity": comparator.source_identity.hex(),
"counters": list(lane.counters),
"witness_count": lane.witness_count,
"record_count": lane.window_points,
Expand Down
5 changes: 3 additions & 2 deletions proof/region/v1/mpfi/receipt.py
Original file line number Diff line number Diff line change
Expand Up @@ -707,7 +707,8 @@ def replay_mpfi_evidence_is_well_bound_v1(value: object) -> bool:
return False
if (
value.transcript.job_identity != snapshot.request.job.identity
or value.transcript.comparator_identity != value.build.comparator.identity
or value.transcript.comparator_identity
!= value.build.comparator.manifest.source_identity
or value.process.stderr
or not executor.result_matches_request_v1(value.process, value.invocation)
):
Expand Down Expand Up @@ -991,7 +992,7 @@ def execute(self, request: MpfiPipelineRequestV1) -> MpfiSourceBoundResultV1:
argv=(
b"mpfi-evaluator",
b"--manifest-identity",
build.comparator.identity.hex().encode("ascii"),
build.comparator.manifest.source_identity.hex().encode("ascii"),
b"--job",
b"/dev/stdin",
),
Expand Down
7 changes: 7 additions & 0 deletions proof/region/v1/mpfi/tests/full_domain_receipt.py
Original file line number Diff line number Diff line change
Expand Up @@ -111,8 +111,15 @@ def test_full_domain_build_run_seal_and_verification_evidence(self) -> None:
transcript.domain_identity,
protocol.exact_full_domain_manifest_v1().identity,
)
# The engine echoes the coordinate it was told, and it is told the
# comparator's source identity: the decision chain must stay portable
# across runs whose build observations differ.
self.assertEqual(
transcript.comparator_identity,
result.comparator.manifest.source_identity,
)
self.assertNotEqual(
result.comparator.manifest.source_identity,
result.comparator.manifest.identity,
)

Expand Down
Loading
Loading