Proof: замкнуть single-operation replay

proof/region/v1/PROTOCOL.md

@@ -12,9 +12,10 @@ protocol fixtures и не является evaluator runner. `arb/evaluator` в
 Arb-enclosures и выпускает связанные transcript bytes;
 `SourceBoundArbControllerV1` заново собирает evaluator, запускает его и создаёт
 только provenance receipt. Ни один из этих путей не выполняет независимый
-semantic replay и не создаёт mathematical proof type. MPFI source lock и
-archive admission уже представлены, но MPFI evaluator/source-bound receipt и
-semantic verifier в текущем release отсутствуют.
+semantic replay и не создаёт mathematical proof type. MPFI source lock,
+archive admission и sealed source input (не evaluator replay) уже представлены, но MPFI
+evaluator/source-bound receipt и semantic verifier в текущем release
+отсутствуют.
 
 Structural protocol/admission сам не является математическим proof.
 `DualComparisonCandidateV1` кодирует только structural agreement и не создаёт
@@ -235,16 +236,39 @@ observation. Право на Arb receipt получает не executor, а от
 
 ## Общая граница BUILD
 
-`provenance.materialize_admitted_source_files_v1` повторно допускает один
-admitted archive и выдаёт только exact relative regular files. Он не вводит
-USTAR namespace, recipe или engine semantics. Lane выбирает layout и связывает
-собственный aggregate source capability; общий materializer не создаёт generic
-source closure. `proof/region/v1/build/input.py` принимает уже нормализованные
-lane entries, кодирует один канонический USTAR и владеет точными input bytes.
+Source replay имеет две намеренно разные стадии. Сначала provenance канонически
+перепарсивает source lock, bounded-decompresses и сканирует archive, чтобы
+сверить lock, manifest, tree и compressed bytes. Эта metadata replay не создаёт
+отдельные file-byte buffers. Затем
+`provenance.replay_materialize_admitted_source_v1` из одного такого replay
+создаёт token-closed снимок lock, archive и exact relative regular files.
+Aggregate Arb/MPFI admission владеет только свежими replayed archives; runtime
+получает все три file-byte materializations только через один
+`replay_admitted_source_closure_v1`. Общий leaf не вводит USTAR namespace,
+recipe или engine semantics. Lane выбирает layout и связывает собственный
+aggregate source capability. `proof/region/v1/build/input.py` принимает уже
+нормализованные lane entries, кодирует один канонический USTAR и владеет точными input bytes.
 `SealedInputV1` структурно неизменяем, связывает целостность байтов с opaque
 caller digest и не утверждает recipe либо engine semantics. Resource bounds
 передаёт lane: общий encoder не вводит собственный fixture-specific cap.
 
+`mpfi/input.py` строит `SealedInputV1` только из одного owned replay snapshot
+пары `MpfiSourceLockV1` и `AdmittedMpfiSourcesV1`. Тот же снимок даёт exact
+regular files, aggregate identity и versioned MPFI-only namespace
+`sources/<role>/<relative>` и связывает свежую aggregate source capability с
+exact USTAR bytes. Роль, а не archive root, разделяет три source trees: lock
+не требует уникальности root. Целостность `SealedInputV1` сама по себе не
+доказывает принадлежность MPFI closure; это отдельно перепроверяет MPFI
+source-input binding. Caller передаёт canonical `CanonicalInputLimitsV1`: lane сверяет
+declared exact file count и payload closure до повторной materialization archive
+bytes, а общий encoder сверяет все final USTAR bounds после materialization.
+Limits — operational boundary, не
+координата MPFI source-input binding и не build policy. Для неверного public
+capability boundary возвращается `MpfiSourceInputErrorV1`; failure exact archive
+replay остаётся `ProvenanceErrorV1`, а limits/USTAR rejection — `InputErrorV1`.
+Эта ступень не вводит recipe, Docker policy, BUILD/RUN authority, executable,
+comparator, receipt или semantic verifier.
+
 `proof/region/v1/build/transport.py` владеет immutable Docker policy,
 одноразовым probe→build lease, bounded stdin/stdout observation, cleanup и
 двумя свежими попытками. Доказательные координаты разделены по причинам:
@@ -282,16 +306,30 @@ cleanup, без ложного заявления о reap CLI. `TwoBuildObservat
 валидной session сохраняется весь уже завершённый causal prefix; нарушение
 контракта, выявленное до неё, может не иметь ни session, ни process prefix.
 Transport не знает formula, ELF, comparator или
-source provenance: lane отдельно перепроверяет semantic input binding перед
-каждым process и передаёт output admission. Arb объявляет собственную exact
-policy; MPFI обязан объявить другую, а не заимствовать Arb semantics.
+source provenance: engine lane отдельно перепроверяет свой engine-owned input binding перед
+каждым process и передаёт output admission. MPFI sealed source input ещё не
+является MPFI build policy; будущая policy должна быть объявлена отдельно и не
+может заимствовать Arb semantics.
 
 ## Воспроизведение Arb, связанное с источником
 
-`SourceBoundArbControllerV1` сначала повторно парсит source lock и job,
-повторно допускает exact owned archive/build-input bytes и строит из regular
-files один canonical USTAR с нормализованными metadata. Один immutable bundle
-object дважды передаётся через bounded stdin; каждый свежий контейнер до
+`PipelineRequestV1` до операции отдельно перепроверяет и владеет metadata-only
+source closure: это ранняя integrity boundary для public input, не shared cache
+операции. Затем `SourceBoundArbControllerV1` получает один detached operation
+snapshot: канонический source lock, owned replayed archives и единственные для
+этой операции file-byte materializations, заново допущенные копии build files,
+job и limits. Он передаёт этот же private snapshot в `ControlledPipelineV1`;
+самостоятельный BUILD создаёт snapshot сам до probe/spawn. Внутренний transport
+recheck сверяет только owned snapshot, а public verifier независимо строит
+новый snapshot из request, сохранённого внутри evidence, а не из исходного
+объекта вызывающего. До replay он фиксирует structural projection всех
+evidence coordinates и сверяет каждый используемый protocol identity cache с
+независимо восстановленным canonical wire. Он принимает результат только если
+та же projection на входе, после source replay и после edge replay совпадает.
+Projection сверяет retained bytes, manifests и protocol wire, но не открывает
+вторую source materialization; она доказывает стабильность значения в пределах
+одного вызова, а не неизменность объекта после возврата. Один
+immutable bundle object дважды передаётся через bounded stdin; каждый свежий контейнер до
 распаковки сверяет exact length и SHA-256, распаковывает только в private
 bounded tmpfs, а executable возвращает через stdout. Semantic host bind mounts,
 host output path и повторное открытие результата отсутствуют. Эта граница
@@ -309,9 +347,10 @@ identity без зеркальных промежуточных dataclass:
 2. build identity связывает source identity, versioned Docker capability,
    pipeline policy, trust boundary, один sealed bundle object, два exact
    transfer и два byte-identical executable stdout. Comparator verifier
-   строит свежий canonical manifest из SHA-256 retained preimage bytes и
-   сверяет все его поля и identity с build observation; это проверка retained
-   причинных данных, а не заявление о независимом втором выводе preimages;
+   заново выводит все десять preimage bytes и canonical manifest из того же
+   operation snapshot и retained BUILD observation, затем сверяет все поля и
+   identity с build observation. Это не независимая реализация или semantic
+   replay, а exact re-derivation тех же причинных координат;
 3. run identity впервые связывает canonical job с тем же retained executable
    bytes object, exact argv/env/cwd/stdin/limits, единственной допустимой
    `linux-x86_64` sandbox platform, typed child exit, stdout, canonical