Proof: add independent MPFI evaluator closure

[lemone112]

Что изменено

Добавлен независимый M1.5-путь MPFI для proof/region/v1:

• отдельные MPFI interval/region/wire/hash/evaluator исходники;
• отдельный parser/emitter exact-real SSA без импорта Arb/FLINT;
• source-level operation allowlist с запретом опасных MPFI операций; ELF symbol parser нормализует только ABI-leading underscores и не смешивает GMP ABI names с разрешёнными MPFI calls;
• дополнительная проверка undefined symbols на реально скомпилированных object-файлах: macro, function-pointer, assembler alias и token-paste обходы не проходят линковочную границу;
• воспроизводимый офлайн build recipe на Clang 19, GMP → MPFR → MPFI; source-owned build.sh dispatches the inner recipe only through the trusted transport's clean child; standalone wrapper is not a source-bound execution authority;
• ELF static/no-dynamic проверка fail-closed при любой ошибке самой проверки;
• явный LC-MPFI-RUNTIME-V1 profile: job ≤16 MiB, precision ≤4096 bits, ≤32 policy rung-ов, ≤1024 knots, transcript ≤16 MiB; лимиты не расширяют математическую wire grammar;
• oversized input/precision/policy/knots отклоняются до MPFI allocation; переполнение transcript получает отдельную типизированную причину output_limit;
• обязательный MPFI anti-vacuum gate с точным inventory/digest в обоих proof workflows;
• RED/hostile tests для формулы, allowlist, alias/indirection, linked-symbol closure, ELF inspection, runtime profile, отсутствия compatibility-layer и canonical transcript;
• PROTOCOL.md уточняет границу: evaluator implementation закрыта, но source-bound BUILD/RUN receipt и semantic verifier ещё не admitted.

Корневая причина

До этого #511 запечатывал только MPFI source input. Начинать M2a без собственного evaluator/build path означало бы создать scaffold или ложный receipt. Этот PR закрывает именно отсутствующую implementation boundary; receipt намеренно не добавляется.

Hostile review выявил и исправил: обход regex allowlist непрямым именем операции, fail-open трактовку exit code 2 от grep, замаскированную ошибку MPFI inventory через make -pn | awk, fail-open compiler --version probe, подменяемый LC_MPFI_BUILD_ENV_V1 sentinel (теперь structural outer entrypoint с hostile environment test) и неограниченное чтение/накопление job/output. Новые лимиты являются operational admission profile и должны быть заново привязаны к immutable executor limits в M2a.

Проверки

Локально:

• cargo fmt --all -- --check;
• cargo test --workspace --all-targets: 1012 passed, 7 ignored;
• RUSTDOCFLAGS=-D warnings cargo doc --workspace --no-deps;
• cargo clippy --workspace --all-targets --all-features -- -D warnings;
• MPFI source gate: 20 тестов, 17 passed, 3 ожидаемо skipped без контролируемого внешнего C17 бинаря; normal и PYTHONOPTIMIZE=2;
• независимая Linux/amd64 reconstruction той же границы: GMP/MPFR upstream checks прошли, MPFI — 156/156 после точного исключения только трёх дефектных тестов upstream (tdiv_ext, texp10, trec_sqrt); evaluator статически собран Clang 19, source/undefined-symbol/ELF gates зелёные;
• runtime evaluator: 16/16 passed на frozen transcript, exact-zero witness и input-limit, включая PYTHONOPTIMIZE=2; локальный бинарный SHA-256: 1cbab9cb27878a38075cbb0d748a95b4d404c9358fe4df6ae93737a0a354d071;
• общий region-proof suite: 177 OK, 1 skip;
• sh -n, shellcheck и git diff --check без новых ошибок; временная VM остановлена после прогона.

Последняя проверка — 2026-08-02

• Новый head b464b8792d0005e126ed3abf543c774e2d8f6004 содержит структурный source-owned MPFI dispatcher и честно сужает claim: clean environment/source-bound execution authority принадлежит trusted transport, а не standalone wrapper.
• Path resolution выполняется только в clean child; hostile environment test и structural ordering test проходят.
• MPFI source gate остаётся 20 tests, 17 passed, 3 exact skips; normal и PYTHONOPTIMIZE=2 зелёные. Source-bound BUILD/RUN receipt и M2a этим PR не заявляются.
• External exact-head jobs 30727180033, 30727180037, 30727180049 пока queued; CodeRabbit success относится к draft и не заменяет полный review.

[coderabbitai]

Warning

Review limit reached

You’ve reached a temporary PR review limit under our Fair Usage Limits Policy.

Your recent review volume is higher than typical usage, so adaptive limits are currently applied.

Next review available in: 29 minutes

Enable usage-based reviews in Billing to review now. Otherwise, wait until the next included review is available.
You're only billed for reviews past your plan's rate limits ($0.25/file).

How can I continue?

After more reviews become available, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews.

How do review limits work?

CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability.

For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window.

Please refer docs for additional details.

Review details

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: d280a881-9b7c-4cd6-a517-540e75ca0d62

📥 Commits

Reviewing files that changed from the base of the PR and between 931c432 and b464b87.

📒 Files selected for processing (20)

• .github/workflows/arb.yml
• .github/workflows/ci.yml
• proof/region/v1/PROTOCOL.md
• proof/region/v1/mpfi/build-inner.sh
• proof/region/v1/mpfi/build.sh
• proof/region/v1/mpfi/evaluator/formula.h
• proof/region/v1/mpfi/evaluator/formula.py
• proof/region/v1/mpfi/evaluator/hash.c
• proof/region/v1/mpfi/evaluator/hash.h
• proof/region/v1/mpfi/evaluator/interval.c
• proof/region/v1/mpfi/evaluator/interval.h
• proof/region/v1/mpfi/evaluator/main.c
• proof/region/v1/mpfi/evaluator/region.c
• proof/region/v1/mpfi/evaluator/region.h
• proof/region/v1/mpfi/evaluator/wire.c
• proof/region/v1/mpfi/evaluator/wire.h
• proof/region/v1/mpfi/operations.py
• proof/region/v1/mpfi/tests/gate.py
• proof/region/v1/mpfi/tests/test_evaluator_source.py
• proof/region/v1/tests/test_mpfi_input.py

---

_{Comment @coderabbitai help to get the list of available commands.}

[lemone112]

@coderabbitai review

Проверьте текущий exact head b464b87: MPFI source-owned dispatcher, clean-child ordering, source/build claim boundaries and anti-vacuum tests. Не расширяйте review на Actions/runner infrastructure.

[coderabbitai]

@lemone112 Принято. Проверю exact head b464b8792d0005e126ed3abf543c774e2d8f6004 только в указанной области. Actions и runner infrastructure не буду включать в review.

✅ 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.

[lemone112]

Этот MPFI evaluator-срез поглощён терминальным PR #514 (base main, exact head 6e8bb6445cf5564bad1b590690a43a235f4dbfbd). Реализация сохранена, а BUILD/RUN receipt вынесен в отдельную терминальную границу с честным native/semantic stop. Закрываю как superseded; код не удалён.