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

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

`identity` связывает все десять координат, включая `build_identity` и
`test_observation`. Эти две сворачивают И воспроизводимые входы сборки (байты
build recipe, `build_input_identity`, `formula_support_identity`,
`pipeline_policy_identity`, sha и длину бинаря), И наблюдение сборки — docker
capability и digest-ы консольного вывода процессов. Исключены они потому, что
СОДЕРЖАТ наблюдение, а не потому, что состоят только из него: одна
невоспроизводимая координата делает невоспроизводимым весь фолд.

Отсюда честная цена разделения: решающая цепь перестаёт различать компараторы,
отличающиеся ТОЛЬКО воспроизводимыми входами сборки — тот же исходник, собранный
другим рецептом или давший другой бинарь. Математику это не задевает:
`engine_release`, `upstream_source`, `arithmetic_input_set`, `wrapper_source` и
`evaluator_source` остаются в source-наборе, а полная `identity` с бинарём и
рецептом по-прежнему связывается квитанцией и дуальным клеймом.

Правило, а не измерение: `binary_identity` воспроизводится между прогонами
одинакового дерева исходников, а `build_identity` — нет, потому что сворачивает
наблюдение сборки. У Arb невоспроизводимость затрагивает и `test_observation`,
который сворачивает те же наблюдения процессов; у MPFI координата несёт вложенный
digest, поэтому состав дельты иной. Конкретные прогоны и величины дельты —
история измерения, а не контракт: она живёт в PR и журнале, не здесь.

`source_identity` связывает kind и восемь координат, выводимых из источников:
`engine_release`, `upstream_source`, `arithmetic_input_set`, `wrapper_source`,
`evaluator_source`, `operation_allowlist`, `legal_file_set`, `exclusions`.
Это производное свойство, а не поле wire: грамматика манифеста не меняется.
Преимидж не является top-level artifact, поэтому общая формула identity выше к
нему неприменима; координата вычисляется как

`SHA256("labcolors.proof-region.comparator-source-identity.v2" ||
u64be(payload_length) || u8(kind) || восемь digest-ов подряд)`,

где digest-ы идут в порядке объявления полей манифеста, без magic и без длин:
каждая координата — ровно 32 байта, поэтому склейка однозначна. Состав и
порядок выводятся из схемы (`source_bound_coordinates_v2()`), а не
перечисляются отдельно, поэтому новая координата манифеста попадает в фолд
автоматически.

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

- **решающая цепь** связывает `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 +627,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 Expand Up @@ -739,8 +800,9 @@ replay:
кодируется как `u64be(exponent) || u64be(len) || digits`, а `digits` —
вывод `mpfr_get_str(NULL, &exponent, 16, 0, value, MPFR_RNDN)`;
- accounting digest: домен `labcolors.arb-evaluation-accounting.v1\0` или
`labcolors.mpfi-evaluation-accounting.v1\0`, затем job/domain/policy/comparator
identities и на точку `u32be(ordinal) || u32be(precision) ||
`labcolors.mpfi-evaluation-accounting.v1\0`, затем job identity, domain
identity, policy identity и comparator **source** identity — accounting
принадлежит решающей цепи, — и на точку `u32be(ordinal) || u32be(precision) ||
u64be(consumed) || u8(outcome)`.

Правила допуска по решению:
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
10 changes: 5 additions & 5 deletions proof/region/v1/corpus_assembly.py
Original file line number Diff line number Diff line change
Expand Up @@ -132,15 +132,15 @@ def load_lane_v1(
corpus.ShardCorpusReasonV1.FOREIGN_INPUT,
"lane manifest counters must be a list of integers",
)
if manifest.get("schema") != corpus_lane.LANE_SCHEMA_V1:
if manifest.get("schema") != corpus_lane.LANE_SCHEMA_V2:
return _reject(
corpus.ShardCorpusReasonV1.FOREIGN_INPUT, "foreign lane schema"
)
identities = {
"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
43 changes: 31 additions & 12 deletions proof/region/v1/corpus_lane.py
Original file line number Diff line number Diff line change
Expand Up @@ -32,22 +32,38 @@

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_V2 = "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()
# The manifest takes content addresses, not content: unpacking the dict
# reads as if the bytes went in, so the keys are named at the call site.
addresses = tuple(contents)
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, *addresses
)
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 +191,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 @@ -233,14 +252,14 @@ def write_lane_artifacts_v1(
)
(out / "lane-records.bin").write_bytes(lane.accounting_records)
manifest = {
"schema": LANE_SCHEMA_V1,
"schema": LANE_SCHEMA_V2,
"window_start": lane.window_start,
"window_points": lane.window_points,
"shard_points": shard_points,
"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