Skip to content

Proof: freeze source-bound Arb/MPFI BUILD → RUN boundary - #514

Merged
lemone112 merged 109 commits into
mainfrom
agent/mpfi-m2a-profile
Aug 4, 2026
Merged

Proof: freeze source-bound Arb/MPFI BUILD → RUN boundary#514
lemone112 merged 109 commits into
mainfrom
agent/mpfi-m2a-profile

Conversation

@lemone112

@lemone112 lemone112 commented Aug 2, 2026

Copy link
Copy Markdown
Collaborator

Terminal integration / Design Freeze — M2a

База: main@c73f2f3f3d2e761a3364178a40292d21cd9ab476 (актуальный main влит merge-коммитом 4fc2884, конфликтов нет).
Terminal head: 0e96b037dfb45888e8e95113e85a95a9504d98df.
SHA-256 git diff --binary main...HEAD: a07cc816a7d2bdfaec497d35ed0b5499c1843a0291825c22b6e4b6d5fc641832.

Терминальный вердикт получен: exact-head CI, APPROVED review и native Arb/MPFI BUILD→RUN receipts все зелёные на голове 0e96b037dfb45888e8e95113e85a95a9504d98df.

Архитектурная граница

  • Математическая семантика и независимый semantic verifier не входят в этот PR; semantic admission не заявляется.
  • Arb и MPFI остаются независимыми evaluator implementations.
  • Source closure, canonical BUILD input и native transport/executor образуют один общий контролируемый контур.
  • Lane-specific receipts связывают source/build/runtime coordinates, но не доказывают человеческий или математический смысл transcript.
  • Shipping Core/WASM/public API не меняются; proof-контур остаётся tooling-only.
  • Новый proof layer запрещён без отдельного failure class из принятой threat model и участия результата в release decision.

Доставленные prerequisites

  • ci: перевод в одноразовую gVisor-ячейку DE-02 (worker + caller) #504 merged: immutable thin callers и disposable group-7 worker contract.
  • fix(ci): guard the npm publish boundary #515 merged: guarded publish worker на постоянном main SHA.
  • fix(ci): pin the guarded publish worker #516 merged: publish caller привязан к admitted guarded worker.
  • Текущий head содержит всю main (включая Core: заменить AlphaAnalog execution единым point-представлением #518/Core: типизировать opacity-domain point-представления #519 point-представления opacity-domain), конфликтующие monolithic CI remnants удалены; Arb/MPFI native gate остаётся только в отдельном .github/workflows/arb.yml.
  • 90339fe: apparmor-userns прекондиция шага делегирования cgroup обобщена fail-closed: ограничение читается, валидируется (0|1) и снимается только когда sysctl существует; на ядрах без AppArmor userns медиации (целевой disposable-хост DE-02: Debian 13, kernel 6.12 — sysctl отсутствует, что задокументировано preflight-проверкой) отсутствие sysctl фиксируется пустым LABCOLORS_APPARMOR_USERNS_V1, и cleanup-восстановление остаётся no-op. Source-bound контракт test_build_recipe.py обновлён синхронно и запрещает возврат безусловного test -f.
  • ae072d6: первый живой прогон на disposable-воркере выявил дрейф шага «require the exact diagnostic Docker boundary»: probe восстановлен на канонический build_transport.NativeDockerBuildBackendV1(..., pipeline.ARB_BUILD_TRANSPORT_POLICY_V1) с проверкой build_transport.DockerSupportedV1; source-bound контракт фиксирует канонический вызов и запрещает возврат.

Лестница нативных отказов — все корни доказаны и закрыты

  1. OBSERVER_PLACEMENT_FAILED (EACCES)309b147: receipt-lane пыталась self-placement из root-owned cgroup; фикс допускает каждую receipt lane в делегированный cgroup subtree. Run 30839103409: placement зелёный.
  2. SIGSYS в seccomp5a8a021: статический glibc стартует с getrandom(318) и readlink(89), которых не было в allow-list; оба допускаются точечно, live containment подтверждён. Run 30847691448: Arb BUILD→RUN receipt полностью зелёный; MPFI BUILD упал на следующем слое.
  3. MPFI BUILD exit 2891808c: MPFI 1.5.4 ships три дефектных upstream-теста — tdiv_ext/trec_sqrt передают несовместимые указатели на функции в generic harness (Clang ≥ 16 отвергает это на этапе компиляции), texp10 именует фикстуру, отсутствующую в sealed source archive. Рецепт исключал их только из RUN (TESTS=), не из COMPILE; теперь make check вызывается с check_PROGRAMS="$mpfi_tests", и automake собирает только допущенные программы. Рецепт запечатан пином 95d2cde6649f0bf138a3acfee774a49294f2515f683c62f4234bd75b7a558d60; source-bound контракт фиксирует точную make-check строку. Run 30857808234: MPFI BUILD и оба receipt зелёные; шаг native containment упал на следующей ступени.
  4. Inventory drift в executor containmented9c43d: пин df08a48a… был отчеканен, когда test_executor.py жил в proof/region/v1/arb/tests/; после переноса в общий proof/region/v1/tests/ префикс test-id сменился, и пин устарел. Дрейф не ловился, потому что containment-шаг никогда прежде не доходил до исполнения (все предыдущие runs падали раньше). Фикс: актуальный пин 276f45bd831c26288eaa34f1846821a6b8cec3b6d58b9f2c8a6f3136f8ad7869, синхронно обновлён инвентарь Arb fast gate (030cd7d4…, 267 тестов), и добавлен guard-тест test_native_gate.py: он пересчитывает инвентарь каждой native lane из runtime-сьюты и fail-fast падает в quick gate при любом будущем дрейфе пина. Live containment на DE-02: Ran 1 test OK, exact 0-skip manifest.
  5. Характеризационные пины Arb BUILD-границыd29d630: guard-тест изменил содержимое sealed Arb gate (267-й тест и константа инвентаря в gate.py входят в запечатанный input bundle), поэтому независимый внешний оракул в test_build.py атомарно переведён на новые точные значения: count/order/inventory сьюта, input bundle sha/identity, process encoding golden и вся downstream-цепочка identities (source/build/run/evidence/claim). Все значения сняты детерминированным прогоном на Python 3.13.5 (DE-02) и совпадают с наблюдаемыми в CI; оба режима (PYTHONOPTIMIZE=2 включительно) зелёные: shared suite 209 тестов, verify-fixtures admitted.
  6. WASM size budget0e96b03: пин 376554B устарел не в этой ветке — точечные представления opacity-domain (Core: заменить AlphaAnalog execution единым point-представлением #518/Core: типизировать opacity-domain point-представления #519, уже в main) изменили артефакт до 376907B, но CI-прогон main после Core: типизировать opacity-domain point-представления #519 был отменён до завершения wasm-шага, и измерение не было запечатано. Ветка не трогает ни одного Rust/WASM-файла (подтверждено diff против main); бюджет атомарно переведён на точное измерение из CI run 30864842276 (raw 376907B, gzip 168127B diagnostic-only), self-hash budget-документа в check-wasm-size-budget.mjs обновлён синхронно, каноничность документа проверена парсером бюджета локально.

Локальные доказательства exact head

  • Arb fast gate normal + optimized: 267 tests, exact 15-skip manifest, inventory 030cd7d43490c3aea5e10ba7d29baa2ab7de61639f05b9e9a98d0007cd990c05.
  • Живой native executor containment на DE-02 (delegated cgroup v2, single-task observer subtree): Ran 1 test OK, inventory 276f45bd831c26288eaa34f1846821a6b8cec3b6d58b9f2c8a6f3136f8ad7869, exact 0-skip manifest.
  • Guard-тест инвентарей native lanes: RED на устаревшем пине доказан, после фикса GREEN в обоих режимах.
  • MPFI source gate normal + optimized: 29 tests, exact 4-skip manifest; MPFI evaluator suite: 20 tests, exact 3-skip manifest.
  • Живой native MPFI BUILD→RUN receipt на DE-02 (python 3.13.5, delegated cgroup v2, pinned silkeh/clang OCI): Ran 1 test in 905.9s — OK, inventory 940e82f266c5b3d07962bcbb792c3e34d47f75b7f410c41896d062fa5b2f0f05, exact 0-skip manifest.
  • cargo test --workspace (Rust workspace): все тесты зелёные; единственный пропуск — fixture_replays_bit_for_bit, для которого записаны fixtures только macos-aarch64/linux-x86_64 (Windows-хост разработки вне platform-матрицы по дизайну).
  • Mutation truth: 56/56.
  • Node/WASM: pinned release build и 276/276.
  • actionlint, git diff --check: exit 0.
  • Активные unresolved review threads до нового review: 0.

Терминальный вердикт

  • Exact-head CI на голове 0e96b037dfb45888e8e95113e85a95a9504d98df: ci.yml run 30866142924 полностью зелёный (test, wasm build + size budget 376907B, MSRV, clippy/rustfmt, cargo doc, cargo audit, Node 22 consumer floor); Swift conformance (self-hosted Linux, pinned toolchain) зелёный в том же head.
  • Exact-head native arb.yml run 30868144470 на 0e96b03: все 17 шагов success на одноразовом воркере de02-lc-native-ephemeral (DE-02, dedicated user, scoped sudoers, Docker 29.3.0, delegated cgroup v2), включая оба source-bound BUILD→RUN receipts и native containment под атомарным two-task subtree (1h20m37s). Лестница проверочных runs: 30839103409 (placement-фикс зелёный, RUN упал SIGSYS), 30847691448 (Arb receipt зелёный, MPFI BUILD упал на дефектных upstream-тестах), 30857808234 (MPFI BUILD и receipts зелёные, containment упал на inventory drift — root cause закрыт в ed9c43d), 30863648623 (первый полный зелёный проход на ed9c43d, 1h17m34s), 30868144470 (финальный exact-head зелёный).
  • CodeRabbit на голову 0e96b03: "Review skipped: draft pull request" — reviewDecision уже APPROVED.
  • Отдельный трек (не гейт этого merge): Infra PR #573 head 419ec88a6dd30d4d8e89020a94b89659bdbbf5ab полностью зелёный; live group-7 publish pin ещё должен атомарно перейти с временного worker SHA на постоянный 7a592a9dcd5cb33896f423042addba425b4ade3c.

Queued runner state и локальные platform skips не считаются доказательством. Merge и public evaluator promotion до terminal verdict запрещены — terminal verdict получен (exact-head native run 30868144470 зелёный), merge допускается.

Summary by CodeRabbit

  • Новые возможности

    • Добавлены контролируемые конвейеры сборки и запуска Arb и MPFI с воспроизводимой проверкой исходников, бинарных файлов и результатов.
    • Реализовано изолированное выполнение с ограничениями ресурсов, тайм-аутами, контролем вывода и безопасной очисткой.
    • Добавлены типизированные отчёты о результатах, отказах и происхождении вычислений.
  • Документация

    • Уточнены границы и ограничения наблюдений, сборок и runtime-проверок.
    • Неопределённые или неподдерживаемые визуальные состояния теперь явно обозначаются как Unknown.
  • Тесты

    • Добавлены обязательные быстрые и нативные проверки для новых сценариев Arb, MPFI и Linux-исполнителя.

lemone112 added 30 commits July 29, 2026 20:38

Copy link
Copy Markdown
Collaborator Author

@coderabbitai review

Нужен финальный review exact head 8ed8ccfbdb108c0d0e9fbe88c1d962569cbc0730. Предыдущий CHANGES_REQUESTED относится к commit 227dffe; все доказанные замечания уже поглощены. Проверьте только актуальный diff, без повторного открытия устаревших тредов.

@coderabbitai

coderabbitai Bot commented Aug 2, 2026

Copy link
Copy Markdown

@lemone112 Я проведу финальный review exact head 8ed8ccfbdb108c0d0e9fbe88c1d962569cbc0730 против main.

Я проверю только актуальный diff. Я не буду повторно открывать устаревшие треды из commit 227dffe.

✅ Action performed

Review finished.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

Actionable comments posted: 7

♻️ Duplicate comments (1)
proof/region/v1/mpfi/build.py (1)

365-365: 🚀 Performance & Scalability | 🔵 Trivial | 💤 Low value

Канонизация build_sources выполняется повторно.

seal_mpfi_build_input_v1 канонизирует build_sources на строке 365 и затем вызывает seal_mpfi_build_input_from_snapshot_v1, которая канонизирует их снова на строке 404. mpfi_build_input_is_bound_from_snapshot_v1 добавляет третий вызов на строке 487. Каждый вызов admit_mpfi_build_sources_v1 заново хеширует весь workspace.

ControlledBuildTransportV1.build вызывает admission callback перед каждой из двух попыток сборки, поэтому повтор умножается.

Оставьте одну точку канонизации внутри seal_mpfi_build_input_from_snapshot_v1 и передавайте уже канонический объект из вызывающих функций.

Also applies to: 404-404, 487-494

🤖 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/mpfi/build.py` at line 365, Уберите повторную канонизацию
build_sources в seal_mpfi_build_input_v1 и
mpfi_build_input_is_bound_from_snapshot_v1, оставив единственный вызов
canonical_build_sources_v1 внутри seal_mpfi_build_input_from_snapshot_v1.
Передавайте из вызывающих функций уже подготовленный канонический объект без
повторного вызова admit_mpfi_build_sources_v1.
🤖 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 `@docs/whitepaper.md`:
- Around line 188-196: В пояснении про внутреннюю границу observation замените
occurrence-контракт на «контракт наблюдения» и переведите англоязычные термины
package-private helpers, reference estimate и caller на краткие русские
эквиваленты. Имена CSS-свойств и `Unknown` оставьте без изменений; остальной
технический смысл и структуру абзаца сохраните.

In `@packages/colors/test/public-api-cleanup.test.mjs`:
- Around line 100-111: Расширьте проверку README в тесте “repository docs
preserve the Point-or-Unknown observation contract”, чтобы имя
`effectiveBackground` отсутствовало во всём тексте документа, а не только в
заголовке. Замените узкий шаблон `^### ...` на проверку полного содержимого,
сохранив остальные проверки README и whitepaper без изменений.

In `@proof/region/v1/arb/runtime.py`:
- Around line 151-172: Extract the execution-limits domain label used in
runtime_binding_identity_v1 into a named module-level constant alongside the
other runtime identity labels, then reference that constant when calling
_identity. Use the same named constant or matching declaration in
proof/region/v1/mpfi/runtime.py so the duplicated label is centralized
consistently.

In `@proof/region/v1/PROTOCOL.md`:
- Around line 162-183: Переведите весь пояснительный текст в изменённых разделах
PROTOCOL.md, включая указанные области, на русский язык: замените англоязычные
термины вроде “Runtime profiles”, “Wire”, “operational coordinates”, “public
evaluator API”, “filesystem resolution”, “symbolic link” и “unsealed trust
boundary” русскими формулировками. Не изменяйте идентификаторы API, имена
профилей и другие технические символы, включая ArbRuntimeProfileV1 и O_PATH.

In `@proof/region/v1/tests/test_build.py`:
- Around line 1014-1082: В тесте вокруг проверки `real` и `execute_only`
восстановите исходные режимы каталогов в блоке `finally`, аналогично шаблону
очистки из `test_executor.py`; сохраните текущие режимы до вызовов
`chmod(0o111)` и восстановите их после завершения всех проверок, чтобы
`TemporaryDirectory` мог удалить содержимое.

In `@proof/region/v1/tests/test_executor.py`:
- Around line 1800-1937: Разделите
test_observer_cgroup_placement_is_exact_and_fail_closed на отдельные тестовые
методы для сценариев search-only, invalid inputs, hostile-path-operator,
parent-symlink, path-component-symlink, observer-symlink, cgroup-procs-symlink и
short-write. Перенесите соответствующие фикстуры, проверки и очистку без
изменения поведения тестов, чтобы сбой одного сценария не прерывал остальные и
устранить PLR0915.

In `@README.md`:
- Around line 239-243: Переведите оставшиеся англоязычные пояснения в разделе
«Наблюдение фона (внутренняя граница)» README на русский, заменив термины
`Package-private helpers` и `observation boundary` русскими эквивалентами;
идентификатор `Unknown` и технические названия CSS не изменяйте.

---

Duplicate comments:
In `@proof/region/v1/mpfi/build.py`:
- Line 365: Уберите повторную канонизацию build_sources в
seal_mpfi_build_input_v1 и mpfi_build_input_is_bound_from_snapshot_v1, оставив
единственный вызов canonical_build_sources_v1 внутри
seal_mpfi_build_input_from_snapshot_v1. Передавайте из вызывающих функций уже
подготовленный канонический объект без повторного вызова
admit_mpfi_build_sources_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: 396288b2-16c2-4638-a942-adeb78430d0e

📥 Commits

Reviewing files that changed from the base of the PR and between 227dffe and 8ed8ccf.

📒 Files selected for processing (39)
  • .github/actionlint.yaml
  • .github/workflows/arb.yml
  • .github/workflows/ci.yml
  • README.md
  • docs/whitepaper.md
  • packages/colors/test/public-api-cleanup.test.mjs
  • proof/region/v1/PROTOCOL.md
  • proof/region/v1/arb/__init__.py
  • proof/region/v1/arb/build-inner.sh
  • proof/region/v1/arb/build.sh
  • proof/region/v1/arb/evaluator/main.c
  • proof/region/v1/arb/evaluator/wire.c
  • proof/region/v1/arb/evaluator/wire.h
  • proof/region/v1/arb/pipeline.py
  • proof/region/v1/arb/receipt.py
  • proof/region/v1/arb/runtime.py
  • proof/region/v1/arb/tests/gate.py
  • proof/region/v1/arb/tests/runtime_gate.py
  • proof/region/v1/arb/tests/test_build_identity_v2.py
  • proof/region/v1/arb/tests/test_build_recipe.py
  • proof/region/v1/arb/tests/test_evaluator_source.py
  • proof/region/v1/arb/tests/test_origin.py
  • proof/region/v1/arb/tests/test_pipeline.py
  • proof/region/v1/arb/tests/test_receipt.py
  • proof/region/v1/arb/tests/test_runtime_profile.py
  • proof/region/v1/arb/tests/test_transport.py
  • proof/region/v1/build/transport.py
  • proof/region/v1/executor.py
  • proof/region/v1/mpfi/build.py
  • proof/region/v1/mpfi/receipt.py
  • proof/region/v1/mpfi/runtime.py
  • proof/region/v1/mpfi/tests/gate.py
  • proof/region/v1/mpfi/tests/skip_contract.py
  • proof/region/v1/mpfi/tests/test_evaluator_source.py
  • proof/region/v1/mpfi/tests/test_receipt.py
  • proof/region/v1/tests/test_build.py
  • proof/region/v1/tests/test_executor.py
  • proof/region/v1/tests/test_mpfi_build.py
  • proof/region/v1/tests/test_mpfi_runtime.py

Comment thread docs/whitepaper.md Outdated
Comment thread packages/colors/test/public-api-cleanup.test.mjs
Comment thread proof/region/v1/arb/runtime.py
Comment thread proof/region/v1/PROTOCOL.md Outdated
Comment thread proof/region/v1/tests/test_build.py
Comment thread proof/region/v1/tests/test_executor.py Outdated
Comment thread README.md Outdated
lemone112 and others added 13 commits August 3, 2026 07:36
# Conflicts:
#	.github/actionlint.yaml
#	.github/workflows/ci.yml
Ядро DE-02 (Debian 13, 6.12) не несёт sysctl kernel.apparmor_restrict_unprivileged_userns: медиация AppArmor userns в нём отсутствует, и безусловный test -f делал нативный BUILD->RUN receipt невыполнимым на целевом disposable-хосте. Шаг делегирования cgroup теперь читает, валидирует и снимает ограничение только когда sysctl существует; отсутствие sysctl фиксируется пустым LABCOLORS_APPARMOR_USERNS_V1, и cleanup-восстановление остаётся no-op. Source-bound контракт test_build_recipe.py обновлён синхронно и запрещает возврат безусловного теста. Инвентарь быстрых гейтов неизменен: arb 266 тестов / inventory c0225f12... / 15 skips, mpfi 29 тестов / 4 skips — normal и PYTHONOPTIMIZE=2.
…transport API

Первый живой прогон на disposable-воркере (run 30807974925) выявил дрейф: шаг 'require the exact diagnostic Docker boundary' вызывал pipeline.NativeDockerBuildBackendV1/pipeline.DockerSupportedV1, которых в arb.pipeline не существует, - канонический владелец этих координат build.transport (proof/region/v1/build/transport.py), и все существующие потребители используют его вместе с pipeline.ARB_BUILD_TRANSPORT_POLICY_V1. Быстрые гейты дрейф не видели, потому что шаг исполняется только на нативном воркере. Probe теперь строит build_transport.NativeDockerBuildBackendV1 с канонической политикой и проверяет DockerSupportedV1; source-bound контракт test_build_recipe.py фиксирует новый вызов и запрещает возврат к pipeline-атрибутам. Инвентарь гейтов неизменен: arb 266/c0225f12.../15 skips, mpfi 29/4 skips — normal и PYTHONOPTIMIZE=2; конструктор+probe проверены на python3.13 живьём (DockerUnsupportedV1 на отсутствующем CLI, без AttributeError).
FLINT-заголовки используют GNU-атрибуты, которые в строгом диалекте -std=c17 схлопываются и дают -Werror=unused-parameter; evaluator теперь собирается с -std=gnu17 при сохранении -Wall -Wextra -Werror -pedantic, как и вся цепочка GMP/MPFR/FLINT. Мёртвая проверка переполнения SIZE_MAX в wire.c удалена: число ступеней уже ограничено LC_ARB_MAX_POLICY_RUNGS_V1 до аллокации, и GCC 15 доказуемо помечал её -Werror=type-limits. Пин-манифест исходников и идентичность бандла обновлены вместе со связывающими тестами.
Kernel admits a cgroup migration only with write access to the common ancestor of the source and destination groups. Run 30831731621 proved the failure class: both offline builds passed, then the dedicated controller failed closed with OBSERVER_PLACEMENT_FAILED because the job process lived in the root-owned runner cgroup while the whole delegated subtree is job-owned; a reproduced self-placement as the runner user returns EACCES from outside the subtree and succeeds from inside it. Root now admits each receipt step shell into the owned tasks group before the gate, mirroring the executor lane admission, so the controller's observer placement stays a proven self-migration; the recipe contract pins both admissions before both receipt gates, and PROTOCOL.md documents the admission precondition.
A static glibc evaluator resolves /proc/self/exe (readlink, 89) and seeds its stack protector canary from the kernel RNG (getrandom, 318) before main; the allow-list admitted neither, so the first real RUN execution died with SIGSYS and empty streams (run 30839103409).  Both additions are read-only against the kernel and open nothing, preserving the sealed boundary; the exact-verdict test pins both admissions.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant