Repository navigation
Proof: собрать Arb evaluator из точных входов #499
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Closed
Closed
Changes from all commits
Commits
Show all changes
14 commits
Select commit
Hold shift + click to select a range
a8c38b3
Proof: добавить точный Arb evaluator и входы сборки
lemone112 2ae2514
Proof: связать comparator с двумя сборками
lemone112 9fdce2d
Proof: закрепить диалект зависимостей на GNU C17
lemone112 178a72a
Proof: нормализовать время source snapshot
lemone112 5852638
Proof: связать snapshot policy с наблюдением
lemone112 592c74a
Provide private scratch for locked FLINT tests
lemone112 3cceea3
Run Arb gate on an ephemeral hosted VM
lemone112 acb8355
Clarify the diagnostic Arb boundary
lemone112 5137840
Proof: замкнуть диагностический Arb runtime
lemone112 49629d2
CI: вывести Arb gate из карантина
lemone112 aedb4e1
CI: закрепить новый путь Arb gate
lemone112 8fe2532
Proof: закрыть fail-open замечания ревью
lemone112 de1a7cf
Proof: закрыть финальный review gate
lemone112 9f1f1a7
Docs: scope proof wire codecs
lemone112 File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,3 @@ | ||
| self-hosted-runner: | ||
| labels: | ||
| - labcolors-ephemeral |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,230 @@ | ||
| 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/** | ||
| pull_request: | ||
| 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.event_name == 'pull_request' && github.event.pull_request.number || github.run_id }} | ||
| cancel-in-progress: ${{ github.event_name == 'pull_request' }} | ||
|
|
||
| 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: 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" | ||
| binary="$RUNNER_TEMP/arb-native-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT" | ||
| { | ||
| echo "LABCOLORS_CGROUP_SCOPE_V1=$scope" | ||
| echo "LABCOLORS_EXECUTOR_CGROUP_V1=$scope/proof" | ||
| echo "LABCOLORS_ARB_NATIVE_BINARY=$binary" | ||
| } >> "$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 the exact pinned OCI manifest | ||
| shell: bash | ||
| run: | | ||
| set -euo pipefail | ||
| export PYTHONPATH="$GITHUB_WORKSPACE/proof/region/v1:$GITHUB_WORKSPACE/proof/region/v1/arb" | ||
| docker_path="$(realpath "$(command -v docker)")" | ||
| test -f "$docker_path" | ||
| test ! -L "$docker_path" | ||
| image="$(python3 - <<'PY' | ||
| 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: require the exact diagnostic Docker boundary | ||
| shell: bash | ||
| run: | | ||
| set -euo pipefail | ||
| export PYTHONPATH="$GITHUB_WORKSPACE/proof/region/v1:$GITHUB_WORKSPACE/proof/region/v1/arb" | ||
| export LABCOLORS_ARB_PIPELINE_DOCKER | ||
| python3 - <<'PY' | ||
| import os | ||
| import sys | ||
| from pathlib import Path | ||
|
|
||
| import pipeline | ||
|
|
||
| docker = pipeline.NativeDockerBuildBackendV1( | ||
| Path(os.environ["LABCOLORS_ARB_PIPELINE_DOCKER"]) | ||
| ).probe() | ||
| print(repr(docker)) | ||
| if type(docker) is not pipeline.DockerSupportedV1: | ||
| sys.exit(78) | ||
| PY | ||
|
|
||
| - name: delegate one disposable cgroup subtree | ||
| shell: bash | ||
| run: | | ||
| set -euo pipefail | ||
| test -f /proc/sys/kernel/apparmor_restrict_unprivileged_userns | ||
| 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 | ||
|
coderabbitai[bot] marked this conversation as resolved.
|
||
| 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: two fresh offline builds and evaluator runtime | ||
| shell: bash | ||
| run: | | ||
| set -euo pipefail | ||
| echo "$$" | sudo tee \ | ||
| "$LABCOLORS_CGROUP_SCOPE_V1/tasks/cgroup.procs" >/dev/null | ||
| python3 proof/region/v1/arb/tests/native_gate.py build | ||
| test -f "$LABCOLORS_ARB_NATIVE_BINARY" | ||
| test "$(stat --format=%a "$LABCOLORS_ARB_NATIVE_BINARY")" = 400 | ||
|
|
||
| - 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_ARB_NATIVE_BINARY:-}" ]]; then | ||
| rm -f -- "$LABCOLORS_ARB_NATIVE_BINARY" || 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" | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.