Proof: the decision chain binds what the sources produce, not who watched the build (V5b2d-4b)

proof/region/v1/PROTOCOL.md

@@ -478,6 +478,42 @@ 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` равны, различаются ровно 96 байт
+внутри `build_identity` (32 docker capability + 2×32 наблюдения процессов).
+
+`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` и
+закрыто отвергает чужую полосу; изменение наблюдения сборки — нет.
+
 ## `DecisionTranscriptV1`
 
 Wire после `LCTRN1\0\0`, по порядку:

proof/region/v1/arb/receipt.py

@@ -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",
         ),
@@ -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")
@@ -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",
                 ),

proof/region/v1/corpus.py

@@ -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
@@ -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),

proof/region/v1/corpus_assembly.py

@@ -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))
@@ -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(
@@ -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:
@@ -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,

proof/region/v1/corpus_lane.py

@@ -175,15 +175,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"
@@ -240,7 +243,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,

proof/region/v1/mpfi/receipt.py

@@ -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)
         ):
@@ -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",
                 ),

proof/region/v1/region_proof_protocol.py

@@ -57,6 +57,22 @@
 POLICY_ID_LABEL_V1 = b"labcolors.proof-region.policy.v1\0"
 JOB_ID_LABEL_V1 = b"labcolors.proof-region.job.v1\0"
 MANIFEST_ID_LABEL_V2 = b"labcolors.proof-region.comparator-manifest.v2\0"
+COMPARATOR_SOURCE_ID_LABEL_V2 = (
+    b"labcolors.proof-region.comparator-source-identity.v2\0"
+)
+# The two manifest coordinates left out of the source identity fold in the
+# build observation, which records the environment rather than the sources:
+# see `ComparatorManifestV2.source_identity`.
+SOURCE_BOUND_COORDINATES_V2 = (
+    "engine_release",
+    "upstream_source",
+    "arithmetic_input_set",
+    "wrapper_source",
+    "evaluator_source",
+    "operation_allowlist",
+    "legal_file_set",
+    "exclusions",
+)
 TRANSCRIPT_ID_LABEL_V1 = b"labcolors.proof-region.transcript.v1\0"
 RUN_CLAIM_ID_LABEL_V1 = b"labcolors.proof-region.run-claim.v1\0"
 PROVENANCE_CLAIM_ID_LABEL_V1 = b"labcolors.proof-region.evaluator-provenance-claim.v1\0"
@@ -854,6 +870,33 @@ def encode(self) -> bytes:
     def identity(self) -> bytes:
         return _identity(MANIFEST_ID_LABEL_V2, self.encode())
 
+    @cached_property
+    def source_identity(self) -> bytes:
+        """Identity of everything the comparator derives from its sources.
+
+        The full identity also binds `build_identity` and `test_observation`,
+        and those two coordinates fold in the build observation — the docker
+        capability and the build processes' console digests.  That is a
+        deliberate provenance record, but it is not reproducible: two runs of
+        the identical source tree on two runners produce identical binaries
+        and identical decisions while their observations differ.
+
+        A decision the engine reaches does not depend on which daemon watched
+        the build, so the decision chain binds this coordinate instead: the
+        engine's transcript, its accounting and the replay lanes stay portable
+        across runs, while the receipt keeps the full identity and loses
+        nothing about the environment it was built in.
+        """
+
+        return _identity(
+            COMPARATOR_SOURCE_ID_LABEL_V2,
+            bytes((int(self.kind),))
+            + b"".join(
+                getattr(self, name) for name in SOURCE_BOUND_COORDINATES_V2
+            ),
+        )
+
+
 @dataclass(frozen=True, init=False)
 class ContentResolvedComparatorManifestV2:
     manifest: ComparatorManifestV2
@@ -926,6 +969,10 @@ def admit(
     def identity(self) -> bytes:
         return self.manifest.identity
 
+    @cached_property
+    def source_identity(self) -> bytes:
+        return self.manifest.source_identity
+
 
 class DecisionV1(IntEnum):
     INSIDE = 0
@@ -1440,7 +1487,9 @@ def from_decisions(
         result = cls(
             job.identity,
             job.domain.identity,
-            comparator.identity,
+            # A transcript records what the engine was told the comparator is,
+            # and the engine is told the source identity.
+            comparator.source_identity,
             job.domain.point_count,
             decision_bits,
             counters,
@@ -1597,9 +1646,22 @@ def for_transcript(
         invocation_identity: bytes,
         platform_identity: bytes,
     ) -> "RunClaimV1":
-        if transcript.job_identity != job.identity or transcript.comparator_identity != comparator.identity:
+        # The transcript carries what the engine was told the comparator is,
+        # and the engine is told the source identity: a decision cannot depend
+        # on the observation of the build that produced the evaluator.
+        if (
+            transcript.job_identity != job.identity
+            or transcript.comparator_identity != comparator.source_identity
+        ):
             _fail("run-claim-v1", 0, ProtocolReasonV1.FOREIGN_BINDING, "transcript binding mismatch")
-        return cls(job.identity, comparator.identity, binary_identity, invocation_identity, platform_identity, transcript.identity)
+        return cls(
+            job.identity,
+            comparator.source_identity,
+            binary_identity,
+            invocation_identity,
+            platform_identity,
+            transcript.identity,
+        )
 
     @classmethod
     def parse(cls, data: bytes) -> "RunClaimV1":
@@ -1851,8 +1913,15 @@ def compare_dual_transcripts(
     job_identity = job.identity
     domain_identity = job.domain.identity
     policy_identity = job.policy.identity
+    # Two different coordinates, on purpose.  The transcript and run claim
+    # bind the reproducible source identity, because a decision cannot depend
+    # on the observation of the build.  The dual claim keeps the full
+    # identity, because which build produced each engine is exactly what the
+    # dual proof attests.
     first_comparator_identity = first_manifest.identity
     second_comparator_identity = second_manifest.identity
+    first_source_identity = first_manifest.source_identity
+    second_source_identity = second_manifest.source_identity
     first_transcript_identity = first_transcript.identity
     second_transcript_identity = second_transcript.identity
     _admit_transcript(
@@ -1862,7 +1931,7 @@ def compare_dual_transcripts(
         first_run,
         job_identity=job_identity,
         domain_identity=domain_identity,
-        comparator_identity=first_comparator_identity,
+        comparator_identity=first_source_identity,
         transcript_identity=first_transcript_identity,
     )
     _admit_transcript(
@@ -1872,7 +1941,7 @@ def compare_dual_transcripts(
         second_run,
         job_identity=job_identity,
         domain_identity=domain_identity,
-        comparator_identity=second_comparator_identity,
+        comparator_identity=second_source_identity,
         transcript_identity=second_transcript_identity,
     )
     if first_transcript.counters[2] or first_transcript.counters[3] or second_transcript.counters[2] or second_transcript.counters[3]: