Proof: one process that mints both receipts is the only place a dual proof can be sealed (V5b2d-4d)

.github/workflows/dual-proof.yml

@@ -0,0 +1,346 @@
+name: Full-domain dual proof
+
+on:
+  workflow_dispatch:
+    inputs:
+      lane_run_ids:
+        description: comma-separated runs carrying the verification lane artifacts of BOTH engines
+        required: true
+
+permissions:
+  contents: read
+  actions: read
+
+concurrency:
+  group: dual-proof-${{ github.run_id }}
+  cancel-in-progress: false
+
+jobs:
+  dual-proof:
+    name: seal one full-domain dual proof from two live source-bound receipts
+    # Both engines run in ONE job because `join_dual_proof_v1` needs their
+    # source-bound receipts, and those have no wire form by design: only the
+    # process that minted them can hold them.  Measured on run 31116022208 the
+    # native RUNs took 63 min (Arb) and 43 min (MPFI), so the sequential pair
+    # plus both builds fits the envelope below with room to spare.
+    #
+    # The lane covers come from an earlier run's artifacts.  They admit against
+    # these fresh receipts because a lane binds the comparator's *source*
+    # identity, which reproduces across runners; the full identity folds build
+    # observation and does not.
+    runs-on: ubuntu-latest
+    timeout-minutes: 330
+    env:
+      PYTHONDONTWRITEBYTECODE: "1"
+      PYTHONHASHSEED: "0"
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: bind run-local native paths
+        shell: bash
+        run: |
+          set -euo pipefail
+          scope="/sys/fs/cgroup/labcolors-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT"
+          # One observer subtree per engine.  A shared one cannot work here:
+          # its budget is two tasks, the controller stays in the observer it
+          # entered, and the second engine's BUILD would fork into a full
+          # subtree.  The gate returns to `tasks` between engines and points
+          # LABCOLORS_EXECUTOR_CGROUP_V1 at the next subtree itself.
+          {
+            echo "LABCOLORS_CGROUP_SCOPE_V1=$scope"
+            echo "LABCOLORS_DUAL_PROOF_CGROUP_TASKS=$scope/tasks"
+            echo "LABCOLORS_DUAL_PROOF_CGROUP_ARB=$scope/proof-arb"
+            echo "LABCOLORS_DUAL_PROOF_CGROUP_MPFI=$scope/proof-mpfi"
+          } >> "$GITHUB_ENV"
+
+      - name: acquire and hash-check the union of both source closures
+        shell: bash
+        run: |
+          set -euo pipefail
+          # GMP and MPFR are pinned to byte-identical archives by both engine
+          # locks, so the union is fetched once; a future divergence makes the
+          # digest check below fail loudly instead of silently preferring one.
+          source_dir="$RUNNER_TEMP/dual-source-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT"
+          install -d -m 0700 "$source_dir"
+          echo "LABCOLORS_DUAL_SOURCE_DIR=$source_dir" >> "$GITHUB_ENV"
+          export PYTHONPATH="$GITHUB_WORKSPACE/proof/region/v1"
+          python3 - <<'PY' > "$source_dir/lock.tsv"
+          import sys
+
+          import provenance
+
+          seen: dict[str, tuple[str, str, int]] = {}
+          for lock in (provenance.arb_source_lock_v1(), provenance.mpfi_source_lock_v1()):
+              for source in lock.sources:
+                  entry = (
+                      source.archive_url,
+                      source.archive_sha256.hex(),
+                      source.archive_length,
+                  )
+                  previous = seen.setdefault(source.role.name, entry)
+                  if previous != entry:
+                      # One role, two different archives: the engines no longer
+                      # share a source and this job's single fetch would give
+                      # one of them the wrong bytes.
+                      print(f"source role diverged: {source.role.name}", file=sys.stderr)
+                      raise SystemExit(64)
+          for role, (url, digest, length) in sorted(seen.items()):
+              print(role, url, digest, 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" ;;
+              MPFI) echo "LABCOLORS_MPFI_ARCHIVE=$archive" >> "$GITHUB_ENV" ;;
+              *) exit 64 ;;
+            esac
+            count=$((count + 1))
+          done < "$source_dir/lock.tsv"
+          test "$count" -eq 4
+
+      - name: acquire both pinned OCI manifests
+        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"
+          python3 - <<'PY' > images.txt
+          from arb import pipeline
+          from mpfi import build
+
+          print(pipeline.OCI_IMAGE_REFERENCE_V1)
+          print(build.MPFI_BUILD_IMAGE_REFERENCE_V1)
+          PY
+          while read -r image; do
+            test -n "$image"
+            "$docker_path" image inspect "$image" >/dev/null 2>&1 ||
+              /usr/bin/timeout --signal=TERM --kill-after=30s 15m \
+                "$docker_path" pull "$image"
+          done < images.txt
+          rm -f images.txt
+          {
+            echo "LABCOLORS_ARB_PIPELINE_DOCKER=$docker_path"
+            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: download both engines' verification lane covers
+        # Every lane is dispatched as its own run, so the cover spans many
+        # run ids — the same shape `full-domain-corpus.yml` already uses to
+        # assemble lane evidence.  Both engines land in one flat directory:
+        # lane artifact names carry the engine only to keep the files apart,
+        # while which engine a lane serves is decided by the comparator
+        # source identity inside its manifest.
+        #
+        # Each run lands in its own directory first.  Downloading straight
+        # into one would let a re-run of the same window overwrite the
+        # evidence already there — the cover would still look exact while
+        # quietly having used one of two answers.
+        shell: bash
+        env:
+          GH_TOKEN: ${{ github.token }}
+          LANE_RUN_IDS: ${{ inputs.lane_run_ids }}
+        run: |
+          set -euo pipefail
+          mkdir -p lanes-in staged
+          IFS=',' read -r -a RUNS <<< "${LANE_RUN_IDS}"
+          for run in "${RUNS[@]}"; do
+            run="$(echo "${run}" | tr -d '[:space:]')"
+            case "${run}" in
+              ''|*[!0-9]*)
+                echo "lane run id is not a number: ${run}" >&2
+                exit 64
+                ;;
+            esac
+            rm -rf "staged/${run}"
+            mkdir -p "staged/${run}"
+            gh run download "${run}"               --repo '${{ github.repository }}'               --pattern 'verification-lane-*'               --dir "staged/${run}"
+            for lane in "staged/${run}"/*/; do
+              name="$(basename "${lane}")"
+              if [[ -e "lanes-in/${name}" ]]; then
+                echo "two runs claim lane ${name}; one would silently win" >&2
+                exit 64
+              fi
+              mv "${lane}" "lanes-in/${name}"
+            done
+          done
+          rm -rf staged
+          echo "LABCOLORS_DUAL_PROOF_LANES=$GITHUB_WORKSPACE/lanes-in"             >> "$GITHUB_ENV"
+
+      - name: refuse an incomplete cover before anything expensive is built
+        shell: bash
+        run: |
+          set -euo pipefail
+          # Cover arithmetic costs seconds; discovering a missing lane after
+          # both native runs costs the whole job.
+          export PYTHONPATH="$GITHUB_WORKSPACE/proof/region/v1"
+          python3 - <<'PY'
+          import json
+          import sys
+          from collections import defaultdict
+          from pathlib import Path
+
+          import region_proof_protocol as protocol
+
+          domain_points = protocol.OUTPUT_CARDINALITY_V1
+          windows = defaultdict(list)
+          for lane in sorted(Path("lanes-in").iterdir()):
+              manifest_path = lane / "lane-manifest.json"
+              if not manifest_path.is_file():
+                  print(f"not a lane directory: {lane}", file=sys.stderr)
+                  raise SystemExit(64)
+              manifest = json.loads(manifest_path.read_text("ascii"))
+              windows[manifest["comparator_source_identity"]].append(
+                  (manifest["window_start"], manifest["window_points"])
+              )
+          if len(windows) != 2:
+              print(f"expected two engines, found {len(windows)}", file=sys.stderr)
+              raise SystemExit(64)
+          for identity, cover in sorted(windows.items()):
+              cursor = 0
+              for start, points in sorted(cover):
+                  if start != cursor:
+                      print(f"{identity[:16]}: gap or overlap at {cursor}", file=sys.stderr)
+                      raise SystemExit(64)
+                  cursor += points
+              if cursor != domain_points:
+                  print(f"{identity[:16]}: cover ends at {cursor}", file=sys.stderr)
+                  raise SystemExit(64)
+              print(f"{identity[:16]}: {len(cover)} lanes cover the exact domain")
+          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 "$apparmor_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 "$apparmor_userns")" = 0
+          else
+            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"
+          for engine in proof-arb proof-mpfi; do
+            mkdir "$scope/$engine"
+            printf '+memory +pids' > "$scope/$engine/cgroup.subtree_control"
+            printf '2' > "$scope/$engine/pids.max"
+            mkdir "$scope/$engine/observer"
+            grep --fixed-strings --quiet 'memory' "$scope/$engine/cgroup.subtree_control"
+            grep --fixed-strings --quiet 'pids' "$scope/$engine/cgroup.subtree_control"
+            test "$(cat "$scope/$engine/pids.max")" = 2
+          done
+          echo core | sudo tee /proc/sys/kernel/core_pattern >/dev/null
+          test "$(cat /proc/sys/kernel/core_pattern)" = core
+
+      - name: seal the full-domain dual proof
+        shell: bash
+        env:
+          LABCOLORS_DUAL_PROOF_OUT: dual-proof-out
+        run: |
+          set -euo pipefail
+          # Same cgroup admission contract as the single-engine lanes: root
+          # admits the runner into the owned subtree, and every later observer
+          # placement 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/tests/dual_proof_gate.py
+
+      - name: upload the sealed dual proof identity
+        uses: actions/upload-artifact@65c4c4a1ddee5b72f698fdd19549f0f0fb45cf08 # v4.6.0
+        with:
+          name: dual-proof-identity
+          path: dual-proof-out/
+          if-no-files-found: error
+
+      - 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_DUAL_SOURCE_DIR:-}" ]]; then
+            rm -rf -- "$LABCOLORS_DUAL_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-arb/observer proof-arb proof-mpfi/observer proof-mpfi 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"

.github/workflows/verification-lanes.yml

@@ -1,5 +1,13 @@
 name: Verification lane replay
 
+# One lane is one run, so a full-domain cover is 512 of them and the dual
+# proof needs their ids.  Naming the run after its coordinates makes that list
+# a query instead of a guess about creation times.
+run-name: >-
+  lane ${{ inputs.evidence_artifact }}
+  ${{ inputs.window_start }}+${{ inputs.window_points }}
+  of ${{ inputs.evidence_run_id }}
+
 on:
   workflow_dispatch:
     inputs:
@@ -97,8 +105,14 @@ jobs:
             --out lane-out
 
       - name: upload the verification lane wire evidence
+        # The engine belongs in the name because both engines replay the same
+        # window plan: without it every Arb lane and its MPFI twin claim one
+        # artifact name, and a cover gathered from many runs would overwrite
+        # itself down to one engine.  The name is only for keeping the files
+        # apart — which engine a lane actually serves is decided by the
+        # comparator source identity inside its manifest.
         uses: actions/upload-artifact@65c4c4a1ddee5b72f698fdd19549f0f0fb45cf08 # v4.6.0
         with:
-          name: verification-lane-${{ inputs.window_start }}-${{ inputs.window_points }}
+          name: verification-lane-${{ inputs.evidence_artifact }}-${{ inputs.window_start }}-${{ inputs.window_points }}
           path: lane-out/
           if-no-files-found: error