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

.github/actionlint.yaml

@@ -1,6 +1,7 @@
 self-hosted-runner:
   labels:
     - labpics-ci-gvisor-v1
+    - labcolors-ephemeral
 paths:
   .github/workflows/mutation.yml:
     # actionlint 1.7.12 отстаёт от текущей GitHub-схемы concurrency.queue;

.github/workflows/arb.yml

@@ -0,0 +1,305 @@
+name: Arb evaluator build and runtime
+
+on:
+  workflow_dispatch:
+  push:
+    branches: [main]
+    paths:
+      - .github/workflows/arb.yml
+      - crates/labcolors-core/contracts/contextual-region-formula-v1.lcir
+      - proof/region/v1/**
+permissions:
+  contents: read
+
+concurrency:
+  group: arb-evaluator-build-runtime-${{ github.run_id }}
+  cancel-in-progress: false
+
+jobs:
+  diagnostic-build-runtime:
+    name: two offline builds and runtime tests (no artifact)
+    # Docker is root-equivalent, so this label is provisioned only on a fresh
+    # one-job VM whose runner group is bound to this exact workflow revision.
+    runs-on: [self-hosted, Linux, X64, labcolors-ephemeral]
+    timeout-minutes: 360
+    env:
+      PYTHONDONTWRITEBYTECODE: "1"
+      PYTHONHASHSEED: "0"
+    steps:
+      - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        with:
+          persist-credentials: false
+
+      - name: complete fast Arb contract with exact skip manifest
+        shell: bash
+        run: |
+          set -euo pipefail
+          python3 proof/region/v1/arb/tests/gate.py
+          PYTHONOPTIMIZE=2 python3 proof/region/v1/arb/tests/gate.py
+
+      - name: complete fast MPFI source contract with exact inventory
+        shell: bash
+        run: |
+          set -euo pipefail
+          python3 proof/region/v1/mpfi/tests/gate.py
+          PYTHONOPTIMIZE=2 python3 proof/region/v1/mpfi/tests/gate.py
+
+      - name: bind run-local native paths after the fast gate
+        shell: bash
+        run: |
+          set -euo pipefail
+          scope="/sys/fs/cgroup/labcolors-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT"
+          {
+            echo "LABCOLORS_CGROUP_SCOPE_V1=$scope"
+            echo "LABCOLORS_EXECUTOR_CGROUP_V1=$scope/proof"
+          } >> "$GITHUB_ENV"
+
+      - name: acquire and hash-check exact source archives
+        shell: bash
+        run: |
+          set -euo pipefail
+          source_dir="$RUNNER_TEMP/arb-source-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT"
+          install -d -m 0700 "$source_dir"
+          echo "LABCOLORS_ARB_SOURCE_DIR=$source_dir" >> "$GITHUB_ENV"
+          export PYTHONPATH="$GITHUB_WORKSPACE/proof/region/v1"
+          python3 - <<'PY' > "$source_dir/lock.tsv"
+          import provenance
+
+          for source in provenance.arb_source_lock_v1().sources:
+              print(
+                  source.role.name,
+                  source.archive_url,
+                  source.archive_sha256.hex(),
+                  source.archive_length,
+                  sep="\t",
+              )
+          PY
+          count=0
+          while IFS=$'\t' read -r role url digest length; do
+            archive="$source_dir/${role}.archive"
+            curl --fail --location --silent --show-error \
+              --connect-timeout 30 --max-time 600 --retry 3 --retry-all-errors \
+              "$url" --output "$archive"
+            test "$(stat --format=%s "$archive")" = "$length"
+            echo "$digest  $archive" | sha256sum --check --strict
+            case "$role" in
+              GMP) echo "LABCOLORS_GMP_ARCHIVE=$archive" >> "$GITHUB_ENV" ;;
+              MPFR) echo "LABCOLORS_MPFR_ARCHIVE=$archive" >> "$GITHUB_ENV" ;;
+              FLINT_ARB) echo "LABCOLORS_FLINT_ARCHIVE=$archive" >> "$GITHUB_ENV" ;;
+              *) exit 64 ;;
+            esac
+            count=$((count + 1))
+          done < "$source_dir/lock.tsv"
+          test "$count" -eq 3
+
+      - name: acquire and hash-check exact MPFI source closure
+        shell: bash
+        run: |
+          set -euo pipefail
+          source_dir="${LABCOLORS_ARB_SOURCE_DIR:?}"
+          export PYTHONPATH="$GITHUB_WORKSPACE/proof/region/v1"
+          python3 - <<'PY' > "$source_dir/mpfi-lock.tsv"
+          import provenance
+
+          for source in provenance.mpfi_source_lock_v1().sources:
+              print(
+                  source.role.name,
+                  source.archive_url,
+                  source.archive_sha256.hex(),
+                  source.archive_length,
+                  sep="\t",
+              )
+          PY
+          count=0
+          while IFS=$'\t' read -r role url digest length; do
+            case "$role" in
+              GMP)
+                archive="${LABCOLORS_GMP_ARCHIVE:?}"
+                ;;
+              MPFR)
+                archive="${LABCOLORS_MPFR_ARCHIVE:?}"
+                ;;
+              MPFI)
+                archive="$source_dir/MPFI.archive"
+                curl --fail --location --silent --show-error \
+                  --connect-timeout 30 --max-time 600 --retry 3 --retry-all-errors \
+                  "$url" --output "$archive"
+                echo "LABCOLORS_MPFI_ARCHIVE=$archive" >> "$GITHUB_ENV"
+                ;;
+              *) exit 64 ;;
+            esac
+            test "$(stat --format=%s "$archive")" = "$length"
+            echo "$digest  $archive" | sha256sum --check --strict
+            count=$((count + 1))
+          done < "$source_dir/mpfi-lock.tsv"
+          test "$count" -eq 3
+
+      - name: acquire the exact pinned OCI manifest
+        shell: bash
+        run: |
+          set -euo pipefail
+          export PYTHONPATH="$GITHUB_WORKSPACE/proof/region/v1"
+          docker_path="$(realpath "$(command -v docker)")"
+          test -f "$docker_path"
+          test ! -L "$docker_path"
+          image="$(python3 - <<'PY'
+          from arb import pipeline
+          print(pipeline.OCI_IMAGE_REFERENCE_V1)
+          PY
+          )"
+          "$docker_path" image inspect "$image" >/dev/null 2>&1 ||
+            /usr/bin/timeout --signal=TERM --kill-after=30s 15m \
+              "$docker_path" pull "$image"
+          echo "LABCOLORS_ARB_PIPELINE_DOCKER=$docker_path" >> "$GITHUB_ENV"
+
+      - name: acquire the exact pinned MPFI OCI manifest
+        shell: bash
+        run: |
+          set -euo pipefail
+          export PYTHONPATH="$GITHUB_WORKSPACE/proof/region/v1"
+          docker_path="${LABCOLORS_ARB_PIPELINE_DOCKER:?}"
+          image="$(python3 - <<'PY'
+          from mpfi import build
+          print(build.MPFI_BUILD_IMAGE_REFERENCE_V1)
+          PY
+          )"
+          "$docker_path" image inspect "$image" >/dev/null 2>&1 ||
+            /usr/bin/timeout --signal=TERM --kill-after=30s 15m \
+              "$docker_path" pull "$image"
+          echo "LABCOLORS_MPFI_DOCKER=$docker_path" >> "$GITHUB_ENV"
+
+      - name: require the exact diagnostic Docker boundary
+        shell: bash
+        run: |
+          set -euo pipefail
+          export PYTHONPATH="$GITHUB_WORKSPACE/proof/region/v1"
+          export LABCOLORS_ARB_PIPELINE_DOCKER
+          python3 - <<'PY'
+          import os
+          import sys
+          from pathlib import Path
+
+          from arb import pipeline
+          from build import transport as build_transport
+
+          docker = build_transport.NativeDockerBuildBackendV1(
+              Path(os.environ["LABCOLORS_ARB_PIPELINE_DOCKER"]),
+              pipeline.ARB_BUILD_TRANSPORT_POLICY_V1,
+          ).probe()
+          print(repr(docker))
+          if type(docker) is not build_transport.DockerSupportedV1:
+              sys.exit(78)
+          PY
+
+      - name: delegate one disposable cgroup subtree
+        shell: bash
+        run: |
+          set -euo pipefail
+          apparmor_userns=/proc/sys/kernel/apparmor_restrict_unprivileged_userns
+          if [[ -f "$apparmor_userns" ]]; then
+            original_userns="$(cat /proc/sys/kernel/apparmor_restrict_unprivileged_userns)"
+            case "$original_userns" in
+              0|1) ;;
+              *) exit 78 ;;
+            esac
+            echo "LABCOLORS_APPARMOR_USERNS_V1=$original_userns" >> "$GITHUB_ENV"
+            sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0
+            test "$(cat /proc/sys/kernel/apparmor_restrict_unprivileged_userns)" = 0
+          else
+            # The restriction sysctl exists only on kernels carrying the
+            # AppArmor userns mediation; its absence is proof that there is
+            # nothing to lift, and the cleanup restore stays a no-op.
+            echo "LABCOLORS_APPARMOR_USERNS_V1=" >> "$GITHUB_ENV"
+          fi
+          scope="$LABCOLORS_CGROUP_SCOPE_V1"
+          sudo mkdir "$scope"
+          sudo chown "$(id -u):$(id -g)" \
+            "$scope" \
+            "$scope/cgroup.procs" \
+            "$scope/cgroup.threads" \
+            "$scope/cgroup.subtree_control"
+          printf '+memory +pids' > "$scope/cgroup.subtree_control"
+          mkdir "$scope/tasks" "$scope/proof"
+          printf '+memory +pids' > "$scope/proof/cgroup.subtree_control"
+          printf '2' > "$scope/proof/pids.max"
+          mkdir "$scope/proof/observer"
+          grep --fixed-strings --quiet 'memory' "$scope/proof/cgroup.subtree_control"
+          grep --fixed-strings --quiet 'pids' "$scope/proof/cgroup.subtree_control"
+          test "$(cat "$scope/proof/pids.max")" = 2
+
+      - name: one source-bound BUILD to RUN receipt and evaluator runtime
+        shell: bash
+        run: |
+          set -euo pipefail
+          # The kernel admits a cgroup migration only with write access to the
+          # common ancestor of the source and destination groups; the runner
+          # cgroup is root-owned, so root admits this step into the owned
+          # subtree first and the controller's observer placement then stays a
+          # proven self-migration between delegated groups.
+          echo "$$" | sudo tee \
+            "$LABCOLORS_CGROUP_SCOPE_V1/tasks/cgroup.procs" >/dev/null
+          exec python3 proof/region/v1/arb/tests/native_gate.py receipt
+
+      - name: one source-bound MPFI BUILD to RUN receipt and evaluator runtime
+        shell: bash
+        run: |
+          set -euo pipefail
+          # Identical admission contract as the Arb receipt lane above.
+          echo "$$" | sudo tee \
+            "$LABCOLORS_CGROUP_SCOPE_V1/tasks/cgroup.procs" >/dev/null
+          exec python3 proof/region/v1/mpfi/tests/native_gate.py receipt
+
+      - name: native containment under an atomic two-task subtree
+        shell: bash
+        run: |
+          set -euo pipefail
+          echo "$$" | sudo tee \
+            "$LABCOLORS_EXECUTOR_CGROUP_V1/observer/cgroup.procs" >/dev/null
+          exec python3 proof/region/v1/arb/tests/native_gate.py executor
+
+      # No upload step: the static binary is an ephemeral observation until a
+      # linker/member inventory plus notices/source/relink distribution gate exists.
+
+      - name: remove disposable inputs and cgroup
+        if: always()
+        shell: bash
+        run: |
+          set -uo pipefail
+          status=0
+          record_failure() {
+            local code="$?"
+            if (( status == 0 )); then
+              status="$code"
+            fi
+          }
+          if [[ -n "${LABCOLORS_ARB_SOURCE_DIR:-}" ]]; then
+            rm -rf -- "$LABCOLORS_ARB_SOURCE_DIR" || record_failure
+          fi
+          if [[ -n "${LABCOLORS_CGROUP_SCOPE_V1:-}" && \
+                -d "$LABCOLORS_CGROUP_SCOPE_V1" ]]; then
+            if [[ -f "$LABCOLORS_CGROUP_SCOPE_V1/cgroup.kill" ]]; then
+              echo 1 | sudo tee "$LABCOLORS_CGROUP_SCOPE_V1/cgroup.kill" \
+                >/dev/null || record_failure
+            fi
+            if [[ -f "$LABCOLORS_CGROUP_SCOPE_V1/cgroup.events" ]]; then
+              for _ in {1..100}; do
+                grep --fixed-strings --quiet 'populated 0' \
+                  "$LABCOLORS_CGROUP_SCOPE_V1/cgroup.events" && break
+                sleep 0.01
+              done
+              grep --fixed-strings --quiet 'populated 0' \
+                "$LABCOLORS_CGROUP_SCOPE_V1/cgroup.events" || record_failure
+            fi
+            for child in proof/observer proof tasks; do
+              if [[ -d "$LABCOLORS_CGROUP_SCOPE_V1/$child" ]]; then
+                sudo rmdir "$LABCOLORS_CGROUP_SCOPE_V1/$child" || record_failure
+              fi
+            done
+            sudo rmdir "$LABCOLORS_CGROUP_SCOPE_V1" || record_failure
+          fi
+          if [[ -n "${LABCOLORS_APPARMOR_USERNS_V1:-}" ]]; then
+            sudo sysctl -w \
+              "kernel.apparmor_restrict_unprivileged_userns=$LABCOLORS_APPARMOR_USERNS_V1" \
+              >/dev/null || record_failure
+          fi
+          exit "$status"

README.md

@@ -236,9 +236,12 @@ anchors
 
 ## Runtime и фон
 
-### `effectiveBackground`
+### Наблюдение фона (внутренняя граница)
 
-Текущая функция — вспомогательная эталонная оценка для поддерживаемой цепочки CSS-цветов, а не доказательство того, что пользователь видит именно этот пиксель.
+Вспомогательные функции с областью видимости пакета разбирают поддерживаемую
+цепочку CSS-цветов для runtime-контроллеров. Это не функция публичного
+корневого API и не доказательство того, что пользователь видит именно этот
+пиксель.
 
 Критические ограничения:
 
@@ -247,7 +250,9 @@ anchors
 - отсутствие непрозрачной базы, предел обхода и ошибка style API должны рассматриваться как неизвестный контекст, а не как белый или чёрный fallback;
 - эмитированные движком значения предпочтительно передавать байтами, а не повторно декодировать из CSS-строки.
 
-Текущий helper совместимости ещё не реализует весь строгий типизированный контракт наблюдения. Его bare hex нельзя использовать как сертификат браузера или дисплея.
+Результат внутренней границы наблюдения нельзя использовать как сертификат
+браузера или дисплея. Неподдерживаемый или неизвестный контекст остаётся
+типизированным `Unknown`, а не превращается в правдоподобный цвет.
 
 ### `watchTheme`
 

docs/whitepaper.md

@@ -193,13 +193,15 @@ display-measured evidence без соответствующего измерен
 после устойчивого относительного снижения запускает новый resolve и переход к его
 результату.
 
-`effectiveBackground` — reference estimate поддерживаемой цепочки CSS-цветов,
-не наблюдение пикселя. Image, gradient, video, filter, blend mode и
+Внутренняя граница наблюдения использует вспомогательные функции с областью
+видимости пакета для разбора поддерживаемой цепочки CSS-цветов; это опорная
+оценка, а не наблюдение пикселя. Image, gradient, video, filter, blend mode и
 `backdrop-filter` требуют явных образцов или другого источника фактов. Строгий
-occurrence-контракт не вправе заменять неизвестный фон белым или чёрным. Текущий
-legacy helper всё ещё использует белую базу по умолчанию и пропускает
-неподдерживаемые CSS-слои, поэтому его результат — только compatibility estimate,
-не evidence; для обязательной проверки caller передаёт явный фон или samples.
+контракт наблюдения не вправе заменять неизвестный фон белым или чёрным: если
+непрозрачная база не доказана и вызывающая сторона не объявила `canvas`,
+наблюдение имеет типизированный исход `Unknown`. Для обязательной проверки
+вызывающая сторона передаёт явный фон или образцы; неподдерживаемые слои и
+эффекты не отбрасываются молча.
 
 ## Доказательный статус
 

packages/colors/bench/wasm.json

@@ -27,12 +27,12 @@
     ]
   },
   "measurement": {
-    "source": "github-actions-run-30790916413",
+    "source": "github-actions-run-30864842276",
     "platform": "linux-x64",
-    "rawBytes": 376554
+    "rawBytes": 376907
   },
   "policy": {
-    "maxRawBytes": 376554,
+    "maxRawBytes": 376907,
     "basis": "generic-exact-point-representation",
     "gzip": "diagnostic-only"
   }