From ada3c04d919f99b88eb652476c345b70de802a7d Mon Sep 17 00:00:00 2001 From: Gabe Hamilton Date: Mon, 2 Nov 2026 08:29:27 -0700 Subject: [PATCH 1/3] Fix scheduled sandbox checks and select affected verification layers --- .github/workflows/near-approval-watch.yml | 84 +++++++ .github/workflows/near-approval.yml | 225 +++++++++--------- README.md | 6 +- .../sandbox/scripts/check-lock.py | 136 +++++++---- .../scripts/prepare-upstream-observation.py | 54 +++++ .../sandbox/scripts/test_check_lock.py | 103 ++++++++ projects/near-approval/strategy.md | 11 +- tools/scripts/approval-changed.sh | 44 ++-- tools/scripts/ci-areas.sh | 51 ++-- tools/scripts/ci-changed-areas.sh | 24 ++ tools/scripts/record-approval-check.sh | 2 +- tools/scripts/test-approval-changed.sh | 45 +++- tools/scripts/test-ci-areas.sh | 4 + tools/scripts/test-ci-changed-areas.sh | 44 ++++ 14 files changed, 619 insertions(+), 214 deletions(-) create mode 100644 .github/workflows/near-approval-watch.yml create mode 100644 projects/near-approval/sandbox/scripts/prepare-upstream-observation.py create mode 100644 projects/near-approval/sandbox/scripts/test_check_lock.py create mode 100755 tools/scripts/ci-changed-areas.sh create mode 100755 tools/scripts/test-ci-changed-areas.sh diff --git a/.github/workflows/near-approval-watch.yml b/.github/workflows/near-approval-watch.yml new file mode 100644 index 0000000..f4a58dc --- /dev/null +++ b/.github/workflows/near-approval-watch.yml @@ -0,0 +1,84 @@ +# Upstream polling is separate from verification of formalver changes. +name: near-approval-watch + +on: + schedule: + - cron: "17 3 * * *" + - cron: "41 4 * * 0" + workflow_dispatch: + inputs: + mutants: + description: Also run the expensive mutation suites + type: boolean + default: false + pull_request: + paths: + - .github/workflows/near-approval-watch.yml + - tools/scripts/approval-changed.sh + - tools/scripts/test-approval-changed.sh + - tools/scripts/record-approval-check.sh + - tools/scripts/test-record-approval-check.sh + +permissions: + contents: read + +concurrency: + group: near-approval-watch-${{ github.ref }}-${{ github.event_name }}-${{ github.event.schedule }} + cancel-in-progress: true + +jobs: + detect: + runs-on: ubuntu-latest + permissions: + contents: read + pull-requests: read + outputs: + changed: ${{ steps.contract.outputs.contract_changed }} + source_ref: ${{ steps.contract.outputs.source_ref }} + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0 + with: + persist-credentials: false + - name: Test the watcher and recording scripts + run: | + tools/scripts/test-approval-changed.sh + tools/scripts/test-record-approval-check.sh + - name: Check approval contract code, not unrelated upstream changes + id: contract + if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' + env: + GH_TOKEN: ${{ github.token }} + BASE_BRANCH: ${{ github.event.repository.default_branch }} + run: tools/scripts/approval-changed.sh + + verify: + needs: detect + if: needs.detect.outputs.changed == 'true' + uses: ./.github/workflows/near-approval.yml + with: + source_ref: ${{ needs.detect.outputs.source_ref }} + mutants: ${{ github.event.schedule == '41 4 * * 0' || inputs.mutants == true }} + sandbox: true + + record-upstream: + needs: [detect, verify] + if: needs.detect.outputs.changed == 'true' && needs.verify.result == 'success' + runs-on: ubuntu-latest + permissions: + contents: write + pull-requests: write + timeout-minutes: 10 + concurrency: + group: near-approval-record-upstream + cancel-in-progress: false + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0 + with: + ref: ${{ github.event.repository.default_branch }} + persist-credentials: false + - name: Propose the successfully checked upstream tip + env: + GH_TOKEN: ${{ github.token }} + BASE_BRANCH: ${{ github.event.repository.default_branch }} + SEEN: ${{ needs.detect.outputs.source_ref }} + run: tools/scripts/record-approval-check.sh "$SEEN" diff --git a/.github/workflows/near-approval.yml b/.github/workflows/near-approval.yml index 3e51eeb..0bf97f5 100644 --- a/.github/workflows/near-approval.yml +++ b/.github/workflows/near-approval.yml @@ -9,7 +9,13 @@ on: - "tools/**" - ".gitmodules" - ".github/workflows/near-approval.yml" - - ".github/approval-seen" + - "Cargo.toml" + - "Cargo.lock" + - "!**/*.md" + - "!**/*.mdx" + - "!**/*.rst" + - "!**/*.adoc" + - "!**/docs/**" push: branches: [main] paths: @@ -17,10 +23,28 @@ on: - "tools/**" - ".gitmodules" - ".github/workflows/near-approval.yml" - - ".github/approval-seen" - schedule: - - cron: "17 3 * * *" # nightly: verify only if contracts/approval changed - - cron: "41 4 * * 0" # weekly: mutants, only if the contract changed + - "Cargo.toml" + - "Cargo.lock" + - "!**/*.md" + - "!**/*.mdx" + - "!**/*.rst" + - "!**/*.adoc" + - "!**/docs/**" + workflow_call: + inputs: + source_ref: + description: Changed approval-contract upstream tip to verify + type: string + required: true + mutants: + type: boolean + default: false + sandbox: + type: boolean + default: true + deploy_check: + type: string + default: "" workflow_dispatch: inputs: mutants: @@ -40,8 +64,7 @@ permissions: contents: read concurrency: - # Scheduled runs get their own group so a push or the other schedule - # does not cancel them. + # Calls from the upstream watcher and repository changes have separate groups. group: near-approval-${{ github.ref }}-${{ github.event_name }}-${{ github.event.schedule }} cancel-in-progress: true @@ -59,19 +82,11 @@ env: # below avoid `rustup default`, ~/.gitconfig and ~/.ssh, and the hosted-only # swap setup is skipped there. # -# On pull requests each job below pin runs only when the PR changes a path -# it depends on (tools/scripts/ci-areas.sh); a skipped job reports as -# skipped, which branch protection counts as passing. Pushes to main and -# manual dispatch run every job. A schedule runs verification only when -# contracts/approval on trust-framework differs from .github/approval-seen -# (*.md ignored). That file is the tip already checked, not the pin, so one -# upstream move does not re-run the proofs every night. +# PRs and pushes select only affected verification layers from the entire +# change range. Manual calls and a changed upstream contract verify all layers. +# The separate near-approval-watch workflow owns polling and recording PRs. jobs: pin: - # Read-only: check for an existing successful-check PR on schedules. - permissions: - contents: read - pull-requests: read runs-on: ${{ (startsWith(github.head_ref || github.ref_name, 'dependabot/') || github.actor == 'dependabot[bot]' || github.triggering_actor == 'dependabot[bot]' || startsWith(github.head_ref || github.ref_name, 'claude/') || contains(github.event.pull_request.body, 'claude.ai/code/session_') || github.event.head_commit.committer.email == 'noreply@anthropic.com') && 'ubuntu-latest' || vars.CI_RUNNER || 'ubuntu-latest' }} outputs: plain: ${{ steps.areas.outputs.plain }} @@ -83,8 +98,7 @@ jobs: near_unit: ${{ steps.areas.outputs.near_unit }} sandbox: ${{ steps.areas.outputs.sandbox }} verus: ${{ steps.areas.outputs.verus }} - contract_changed: ${{ steps.contract.outputs.contract_changed }} - source_ref: ${{ steps.contract.outputs.source_ref }} + source_ref: ${{ inputs.source_ref }} steps: - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0 with: @@ -94,33 +108,24 @@ jobs: fetch-depth: 2 - name: Jobs this change needs id: areas + env: + BASE_SHA: ${{ github.event_name == 'pull_request' && github.event.pull_request.base.sha || github.event.before }} + SOURCE_REF: ${{ inputs.source_ref }} run: | tools/scripts/test-ci-areas.sh - tools/scripts/test-approval-changed.sh - tools/scripts/test-record-approval-check.sh - if [ "$GITHUB_EVENT_NAME" = pull_request ] && git rev-parse -q --verify HEAD^2 >/dev/null; then - git diff --name-only HEAD^1 HEAD | CI_AREAS_EXPLAIN=1 tools/scripts/ci-areas.sh >"$RUNNER_TEMP/areas" - else - tools/scripts/ci-areas.sh --all "$RUNNER_TEMP/areas" - fi + tools/scripts/test-ci-changed-areas.sh + tools/scripts/ci-changed-areas.sh >"$RUNNER_TEMP/areas" cat "$RUNNER_TEMP/areas" >>"$GITHUB_OUTPUT" - { echo '### Jobs this change needs'; sed 's/^/- /' "$RUNNER_TEMP/areas"; } >>"$GITHUB_STEP_SUMMARY" - - name: Approval contract since the last check - id: contract - env: - GH_TOKEN: ${{ github.token }} - BASE_BRANCH: ${{ github.event.repository.default_branch }} - run: | - if [ "$GITHUB_EVENT_NAME" = schedule ]; then - tools/scripts/approval-changed.sh + if grep -q '=true$' "$RUNNER_TEMP/areas"; then + echo verification=true >>"$GITHUB_OUTPUT" else - echo contract_changed=true >>"$GITHUB_OUTPUT" - echo source_ref= >>"$GITHUB_OUTPUT" + echo verification=false >>"$GITHUB_OUTPUT" fi + { echo '### Jobs this change needs'; sed 's/^/- /' "$RUNNER_TEMP/areas"; } >>"$GITHUB_STEP_SUMMARY" - name: Check out trust-framework at the pin - if: steps.contract.outputs.contract_changed == 'true' + if: steps.areas.outputs.verification == 'true' env: - SOURCE_REF: ${{ steps.contract.outputs.source_ref }} + SOURCE_REF: ${{ inputs.source_ref }} run: tools/scripts/ci-submodule.sh projects/near-approval/source-mirror - name: Python >= 3.11 (tomllib) if: runner.os == 'macOS' @@ -138,21 +143,21 @@ jobs: done echo "::error::no python3 >= 3.11 on PATH"; exit 1 - name: Gitlink and source hashes match status.toml - # A schedule that found upstream drift verifies that tip. check-pin - # would fail on it and skip every proof job, which is the opposite - # of the point. PRs and pushes still require the pin. - if: github.event_name != 'schedule' + # An upstream call intentionally verifies a different tip. Repository + # changes and ordinary manual runs still require the reviewed pin. + if: inputs.source_ref == '' && steps.areas.outputs.verification == 'true' run: tools/scripts/check-pin.sh near-approval # status-lint (strategy.md section 14): status.toml claims nothing the - # repository doesn't back. Runs here because pin always runs. + # repository doesn't back. Runs only when a verification layer is selected. - name: status-lint + if: steps.areas.outputs.verification == 'true' run: | tools/scripts/test-check-status.sh tools/scripts/check-status.sh near-approval plain: needs: pin - if: needs.pin.outputs.plain == 'true' && needs.pin.outputs.contract_changed == 'true' + if: needs.pin.outputs.plain == 'true' runs-on: ${{ (startsWith(github.head_ref || github.ref_name, 'dependabot/') || github.actor == 'dependabot[bot]' || github.triggering_actor == 'dependabot[bot]' || startsWith(github.head_ref || github.ref_name, 'claude/') || contains(github.event.pull_request.body, 'claude.ai/code/session_') || github.event.head_commit.committer.email == 'noreply@anthropic.com') && 'ubuntu-latest' || vars.CI_RUNNER || 'ubuntu-latest' }} steps: - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0 @@ -191,9 +196,7 @@ jobs: # constant, at most its harness unwind (tools/scripts/kani-loops.py). needs: pin if: >- - needs.pin.outputs.contract_changed == 'true' && - needs.pin.outputs.loops == 'true' && - (github.event_name != 'schedule' || github.event.schedule == '17 3 * * *') + needs.pin.outputs.loops == 'true' runs-on: ${{ (startsWith(github.head_ref || github.ref_name, 'dependabot/') || github.actor == 'dependabot[bot]' || github.triggering_actor == 'dependabot[bot]' || startsWith(github.head_ref || github.ref_name, 'claude/') || contains(github.event.pull_request.body, 'claude.ai/code/session_') || github.event.head_commit.committer.email == 'noreply@anthropic.com') && 'ubuntu-latest' || vars.CI_RUNNER || 'ubuntu-latest' }} timeout-minutes: 30 steps: @@ -224,12 +227,9 @@ jobs: kani: needs: pin - # Every push to main, pull requests that change what it checks, and a - # nightly whose approval contract moved past the pin. + # Only affected repository changes, manual runs, or a changed upstream contract. if: >- - needs.pin.outputs.contract_changed == 'true' && - needs.pin.outputs.kani == 'true' && - (github.event_name != 'schedule' || github.event.schedule == '17 3 * * *') + needs.pin.outputs.kani == 'true' # CBMC peaks at 6.5 to 9.5 GB on the step harnesses; this repository's # default runner has 2 CPUs and 7.9 GB. Set the KANI_RUNNER repository # variable to a larger runner label (and KANI_SWAP_GB to 0) to avoid @@ -398,7 +398,7 @@ jobs: tla: needs: pin - if: needs.pin.outputs.tla == 'true' && needs.pin.outputs.contract_changed == 'true' + if: needs.pin.outputs.tla == 'true' runs-on: ${{ (startsWith(github.head_ref || github.ref_name, 'dependabot/') || github.actor == 'dependabot[bot]' || github.triggering_actor == 'dependabot[bot]' || startsWith(github.head_ref || github.ref_name, 'claude/') || contains(github.event.pull_request.body, 'claude.ai/code/session_') || github.event.head_commit.committer.email == 'noreply@anthropic.com') && 'ubuntu-latest' || vars.CI_RUNNER || 'ubuntu-latest' }} timeout-minutes: 240 steps: @@ -452,7 +452,7 @@ jobs: # audit and canaries, REF-5L (real-core traces on the Lean machine), # MC-4 (Lean graph = TLC graph) and the spec mutants. About 8 min. needs: pin - if: needs.pin.outputs.lean == 'true' && needs.pin.outputs.contract_changed == 'true' + if: needs.pin.outputs.lean == 'true' runs-on: ${{ (startsWith(github.head_ref || github.ref_name, 'dependabot/') || github.actor == 'dependabot[bot]' || github.triggering_actor == 'dependabot[bot]' || startsWith(github.head_ref || github.ref_name, 'claude/') || contains(github.event.pull_request.body, 'claude.ai/code/session_') || github.event.head_commit.committer.email == 'noreply@anthropic.com') && 'ubuntu-latest' || vars.CI_RUNNER || 'ubuntu-latest' }} timeout-minutes: 60 steps: @@ -509,7 +509,7 @@ jobs: # must fail, the erasure check ties the twin to the pinned upstream file, # and every mutant in verus/mutants.toml must be rejected. About 1 min. needs: pin - if: needs.pin.outputs.verus == 'true' && needs.pin.outputs.contract_changed == 'true' + if: needs.pin.outputs.verus == 'true' runs-on: ${{ (startsWith(github.head_ref || github.ref_name, 'dependabot/') || github.actor == 'dependabot[bot]' || github.triggering_actor == 'dependabot[bot]' || startsWith(github.head_ref || github.ref_name, 'claude/') || contains(github.event.pull_request.body, 'claude.ai/code/session_') || github.event.head_commit.committer.email == 'noreply@anthropic.com') && 'ubuntu-latest' || vars.CI_RUNNER || 'ubuntu-latest' }} timeout-minutes: 30 steps: @@ -555,7 +555,7 @@ jobs: # directions. MC-3 (the full graph comparison, about 30 min) runs # nightly and on manual dispatch. needs: pin - if: needs.pin.outputs.prolog == 'true' && needs.pin.outputs.contract_changed == 'true' + if: needs.pin.outputs.prolog == 'true' runs-on: ${{ (startsWith(github.head_ref || github.ref_name, 'dependabot/') || github.actor == 'dependabot[bot]' || github.triggering_actor == 'dependabot[bot]' || startsWith(github.head_ref || github.ref_name, 'claude/') || contains(github.event.pull_request.body, 'claude.ai/code/session_') || github.event.head_commit.committer.email == 'noreply@anthropic.com') && 'ubuntu-latest' || vars.CI_RUNNER || 'ubuntu-latest' }} timeout-minutes: 90 steps: @@ -606,12 +606,12 @@ jobs: scryer-prolog mc2.pl -g "(generate('$PWD/../../kani/target/mc2/prolog.txt', 60) -> halt(0) ; halt(1))" - - needs.pin.outputs.contract_changed == 'true' && - ((github.event_name == 'schedule' && github.event.schedule == '17 3 * * *') || - inputs.sandbox || - (github.event_name != 'schedule' && needs.pin.outputs.sandbox == 'true')) + if: inputs.sandbox || needs.pin.outputs.sandbox == 'true' runs-on: ${{ (startsWith(github.head_ref || github.ref_name, 'dependabot/') || github.actor == 'dependabot[bot]' || github.triggering_actor == 'dependabot[bot]' || startsWith(github.head_ref || github.ref_name, 'claude/') || contains(github.event.pull_request.body, 'claude.ai/code/session_') || github.event.head_commit.committer.email == 'noreply@anthropic.com') && 'ubuntu-latest' || vars.CI_RUNNER || 'ubuntu-latest' }} # The reproducible build runs an amd64 image (emulated on the Mac) and # RT-TRACE replays 210 traces. @@ -685,6 +681,30 @@ jobs: env: SOURCE_REF: ${{ needs.pin.outputs.source_ref }} run: tools/scripts/ci-submodule.sh projects/near-approval/source-mirror + - name: Python >= 3.11 (tomllib) + if: runner.os == 'macOS' + run: | + python3 -c 'import tomllib' 2>/dev/null && exit 0 + for py in python3.13 python3.12 python3.11; do + if p=$(command -v "$py"); then + mkdir -p "$RUNNER_TEMP/python-bin" + ln -sf "$p" "$RUNNER_TEMP/python-bin/python3" + echo "$RUNNER_TEMP/python-bin" >> "$GITHUB_PATH" + exit 0 + fi + done + echo "::error::no python3 >= 3.11 on PATH"; exit 1 + - name: Sandbox lockfile preflight + id: lock-preflight + run: | + python3 projects/near-approval/sandbox/scripts/test_check_lock.py + diag="$RUNNER_TEMP/sandbox-diagnostics" + mkdir -p "$diag" + cp projects/near-approval/sandbox/Cargo.lock "$diag/sandbox-Cargo.lock" + cp projects/near-approval/source-mirror/contracts/approval/Cargo.lock "$diag/upstream-Cargo.lock" + source_ref=$(git -C projects/near-approval/source-mirror rev-parse HEAD) + python3 projects/near-approval/sandbox/scripts/check-lock.py \ + --source-ref "$source_ref" --json "$diag/lock-report.json" - name: Toolchain from versions.env, with the wasm target run: | . tools/versions.env @@ -700,30 +720,27 @@ jobs: cargo install --locked scryer-prolog --version "$SCRYER" --root "$root" fi echo "$root/bin" >> "$GITHUB_PATH" - - name: Python >= 3.11 (tomllib) - if: runner.os == 'macOS' - run: | - python3 -c 'import tomllib' 2>/dev/null && exit 0 - for py in python3.13 python3.12 python3.11; do - if p=$(command -v "$py"); then - mkdir -p "$RUNNER_TEMP/python-bin" - ln -sf "$p" "$RUNNER_TEMP/python-bin/python3" - echo "$RUNNER_TEMP/python-bin" >> "$GITHUB_PATH" - exit 0 - fi - done - echo "::error::no python3 >= 3.11 on PATH"; exit 1 - name: Docker daemon (the reproducible build runs in a container) run: | if ! docker info >/dev/null 2>&1; then echo "::error::No reachable Docker daemon on runner '${RUNNER_NAME}'. Start Docker Desktop and re-run." exit 1 fi - - name: Reproducible wasm of the pin (RT-CODEHASH) + - name: Reproducible wasm of the selected contract (RT-CODEHASH) + env: + SOURCE_REF: ${{ inputs.source_ref }} run: | projects/near-approval/sandbox/scripts/build-wasm.sh reproducible - want=$(python3 -c 'import tomllib; print(tomllib.load(open("projects/near-approval/status.toml","rb"))["project"]["reproducible_wasm_sha256"])') wasm=projects/near-approval/sandbox/target/approval/near/approval_contract/approval_contract.wasm + if [ -n "$SOURCE_REF" ]; then + # A changed upstream artifact cannot have the reviewed pin's hash. + # Adapt only its fingerprint, keeping exports and behavior strict. + want=$(python3 projects/near-approval/sandbox/scripts/prepare-upstream-observation.py \ + --wasm "$wasm" --source-ref "$SOURCE_REF" \ + --report "$RUNNER_TEMP/sandbox-diagnostics/upstream-artifact.json") + else + want=$(python3 -c 'import tomllib; print(tomllib.load(open("projects/near-approval/status.toml","rb"))["project"]["reproducible_wasm_sha256"])') + fi { echo "APPROVAL_WASM=$PWD/$wasm"; echo "APPROVAL_WASM_KIND=reproducible"; echo "APPROVAL_WASM_EXPECTED_SHA256=$want"; } >> "$GITHUB_ENV" - name: Wasm surface of the reproducible build (SH-11, SH-12) run: | @@ -733,7 +750,17 @@ jobs: abi=${abis[0]:-} tools/scripts/wasm-surface.sh --wasm "$wasm" ${abi:+--abi "$abi"} - name: Sandbox tests - run: projects/near-approval/sandbox/scripts/run-sandbox.sh + shell: bash + run: | + mkdir -p "$RUNNER_TEMP/sandbox-diagnostics" + projects/near-approval/sandbox/scripts/run-sandbox.sh 2>&1 | tee "$RUNNER_TEMP/sandbox-diagnostics/sandbox.log" + - name: Upload sandbox diagnostics + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 + if: always() + with: + name: sandbox-diagnostics + path: ${{ runner.temp }}/sandbox-diagnostics/ + retention-days: 14 - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 if: always() with: @@ -798,7 +825,7 @@ jobs: mutants: needs: pin - if: (github.event.schedule == '41 4 * * 0' || inputs.mutants) && needs.pin.outputs.contract_changed == 'true' + if: inputs.mutants runs-on: ${{ (startsWith(github.head_ref || github.ref_name, 'dependabot/') || github.actor == 'dependabot[bot]' || github.triggering_actor == 'dependabot[bot]' || startsWith(github.head_ref || github.ref_name, 'claude/') || contains(github.event.pull_request.body, 'claude.ai/code/session_') || github.event.head_commit.committer.email == 'noreply@anthropic.com') && 'ubuntu-latest' || vars.KANI_RUNNER || vars.CI_RUNNER || 'ubuntu-latest' }} # Up to 2 harnesses (6 for the must-survive mutants) of KANI_TIMEOUT # (60 min) each, plus builds. @@ -865,7 +892,7 @@ jobs: # shell suite fail. shell-mutants: needs: pin - if: (github.event.schedule == '41 4 * * 0' || inputs.mutants) && needs.pin.outputs.contract_changed == 'true' + if: inputs.mutants runs-on: ${{ (startsWith(github.head_ref || github.ref_name, 'dependabot/') || github.actor == 'dependabot[bot]' || github.triggering_actor == 'dependabot[bot]' || startsWith(github.head_ref || github.ref_name, 'claude/') || contains(github.event.pull_request.body, 'claude.ai/code/session_') || github.event.head_commit.committer.email == 'noreply@anthropic.com') && 'ubuntu-latest' || vars.CI_RUNNER || 'ubuntu-latest' }} timeout-minutes: 90 steps: @@ -883,33 +910,3 @@ jobs: echo "RUSTUP_TOOLCHAIN=$RUST_TOOLCHAIN" >> "$GITHUB_ENV" - name: Shell mutants run: projects/near-approval/near-tests/run-mutants.sh - - record-upstream: - # Record a successful check through review, never before the proofs finish. - # Skipped jobs are expected (nightly/weekly scopes differ); failures and - # cancellations must never advance the baseline. - needs: [pin, plain, loops, kani, tla, lean, verus, prolog, near-unit, sandbox, covers, mutants, shell-mutants] - if: >- - ${{ !cancelled() && github.event_name == 'schedule' && - needs.pin.outputs.contract_changed == 'true' && - !contains(needs.*.result, 'failure') && - !contains(needs.*.result, 'cancelled') }} - permissions: - contents: write - pull-requests: write - runs-on: ubuntu-latest - timeout-minutes: 10 - concurrency: - group: near-approval-record-upstream - cancel-in-progress: false - steps: - - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0 - with: - ref: ${{ github.event.repository.default_branch }} - persist-credentials: false - - name: Propose the successfully checked upstream tip - env: - GH_TOKEN: ${{ github.token }} - BASE_BRANCH: ${{ github.event.repository.default_branch }} - SEEN: ${{ needs.pin.outputs.source_ref }} - run: tools/scripts/record-approval-check.sh "$SEEN" diff --git a/README.md b/README.md index ac1ea34..175df69 100644 --- a/README.md +++ b/README.md @@ -23,7 +23,11 @@ Nothing here is Production Ready. How the layers fit, and when to use Kani or Verus: [`docs/architecture.md`](docs/architecture.md). -Tool versions are pinned in [`tools/versions.env`](tools/versions.env), and GitHub Actions use full commit SHAs. CI (`.github/workflows/near-approval.yml`) fetches public trust-framework without credentials. On a PR, only the jobs whose inputs changed run (`tools/scripts/ci-areas.sh`). The nightly runs only when non-Markdown files under `contracts/approval` have changed since `.github/approval-seen`, not since the verification pin. After all applicable checks succeed, a bot opens a PR recording the checked tip; it never pushes `main` or changes the verification pin. An open recording PR suppresses duplicate checks of the same tip while review is pending. Bot-created PR workflows may require a maintainer to select **Approve workflows to run**. In Settings → Actions → General, **Allow GitHub Actions to create and approve pull requests** must be enabled; only the scheduled recording job requests write permissions. +Tool versions are pinned in [`tools/versions.env`](tools/versions.env), and GitHub Actions use full commit SHAs. [`near-approval`](.github/workflows/near-approval.yml) verifies only the layers affected by the complete PR or push diff; documentation-only changes run no verification jobs. Shared inputs select their dependent layers (for example, extracted Prolog facts also feed the plain and Lean checks). + +[`near-approval-watch`](.github/workflows/near-approval-watch.yml) owns the schedule. It compares trust-framework's approval `core/` and `contract/` crates and workspace build inputs against `.github/approval-seen`; unrelated projects, upstream sandbox tests, and documentation do not trigger re-verification. A changed contract calls `near-approval` at that exact upstream tip. An open recording PR for equivalent contract code suppresses repeat verification even if unrelated upstream commits arrive. Only successful verification opens the baseline-update PR; the reviewed verification pin stays unchanged. Bot PR workflows may require **Approve workflows to run**. The Actions PR creation/approval setting must be enabled; only the watcher's recording job requests write access. + +The sandbox checks lockfile compatibility before installing tools or building Wasm. Its diagnostic artifact contains both lockfiles, the selected source SHA, a structured mismatch report, and available test output. Scheduled upstream runs adapt only the expected artifact fingerprint; export-surface and behavioral observations stay strict. Pinned runs retain the independent reviewed Wasm hash. ## near-approval diff --git a/projects/near-approval/sandbox/scripts/check-lock.py b/projects/near-approval/sandbox/scripts/check-lock.py index d4aea93..949ea3f 100755 --- a/projects/near-approval/sandbox/scripts/check-lock.py +++ b/projects/near-approval/sandbox/scripts/check-lock.py @@ -1,57 +1,97 @@ #!/usr/bin/env python3 -"""Lockfile rule (strategy.md section 9): every package that appears in both -the sandbox Cargo.lock and the mirror's contracts/approval/Cargo.lock must -have the same version(s) and checksum(s). Exit 1 on any difference. - -The sandbox lockfile may lead the pin on AHEAD_OF_PIN. Those crates are the -host TLS stack (ureq, used to fetch near-sandbox), not the contract wasm. -Re-pinning would change the contract artifact. Delete an entry once the -mirror has that version. The script fails if you leave it.""" -import sys, tomllib, pathlib - -# rustls-webpki 0.103.16 rejects the compromised intermediate keys. -# webpki-roots 1.0.11 drops the emSign roots (RUSTSEC-2026-0382). The pin -# still has 0.103.15 and 1.0.9. -# rustls 0.23.46 patches RUSTSEC-2026-0346, -0347, -0348 and -0349. The pin -# still has 0.23.45. -AHEAD_OF_PIN = { - "rustls": {"0.23.46"}, - "rustls-webpki": {"0.103.16"}, - "webpki-roots": {"1.0.11"}, +"""Check shared sandbox/mirror dependency versions, sources and checksums. + +Explicit host-TLS backports allow the sandbox to lead the reviewed pin. +When upstream catches up, normal equality applies; an unused exception is +not an error. Other version drift and checksum/source mismatches fail closed. +""" +import argparse +import json +import pathlib +import sys +import tomllib + +# Only these exact sandbox/mirror pairs are approved. These are host-side +# TLS updates, not a change to the reviewed contract pin or wasm artifact. +# rustls 0.23.46 patches RUSTSEC-2026-0346 through -0349 (PR #26). +# rustls-webpki 0.103.16 and webpki-roots 1.0.11 carry the earlier eMudhra +# distrust update (RUSTSEC-2026-0382). Equality needs no backport exception. +HOST_TLS_BACKPORTS = { + "rustls": ("0.23.46", {"0.23.45"}), + "rustls-webpki": ("0.103.16", {"0.103.15"}), + "webpki-roots": ("1.0.11", {"1.0.9"}), } -here = pathlib.Path(__file__).resolve().parent.parent -mine = tomllib.loads((here / "Cargo.lock").read_text())["package"] -theirs = tomllib.loads( - (here.parent / "source-mirror/contracts/approval/Cargo.lock").read_text() -)["package"] -def index(pkgs): +def index(packages): out = {} - for p in pkgs: - if "source" not in p: # workspace members + for package in packages: + if "source" not in package: # workspace members continue - out.setdefault(p["name"], {})[p["version"]] = p.get("checksum") + versions = out.setdefault(package["name"], {}) + version = package["version"] + if version in versions: + raise ValueError(f"ambiguous package {package['name']} {version}") + versions[version] = (package["source"], package.get("checksum")) return out -a, b = index(mine), index(theirs) -bad = [] -ahead = [] -for name in sorted(a.keys() & b.keys()): - for ver, sum_ in a[name].items(): - if ver not in b[name]: - if ver in AHEAD_OF_PIN.get(name, ()): - ahead.append(f"{name} {ver}: mirror has {sorted(b[name])}") + +def compare(mine, theirs): + a, b = index(mine), index(theirs) + bad, ahead = [], [] + for name in sorted(a.keys() & b.keys()): + for version, (source, checksum) in a[name].items(): + if version in b[name]: + other_source, other_checksum = b[name][version] + if source != other_source: + bad.append(f"{name} {version}: source differs") + elif checksum != other_checksum: + bad.append(f"{name} {version}: checksum differs") + continue + allowed_version, old_versions = HOST_TLS_BACKPORTS.get(name, (None, set())) + # Exceptions do not permit a different source or arbitrary newer + # upstream versions. Equality above always checks checksums. + if (version == allowed_version and set(b[name]) <= old_versions + and all(other_source == source for other_source, _ in b[name].values())): + ahead.append(f"{name} {version}: approved host-TLS backport; mirror has {sorted(b[name])}") else: - bad.append(f"{name} {ver}: mirror has {sorted(b[name])}") - elif b[name][ver] != sum_: - bad.append(f"{name} {ver}: checksum differs") -for name, vers in sorted(AHEAD_OF_PIN.items()): - if name in b and vers <= set(b[name]): - bad.append(f"drop AHEAD_OF_PIN[{name!r}], mirror has caught up") -for line in ahead: - print("lockfile ahead of pin:", line) -for line in bad: - print("lockfile mismatch:", line) -print(f"check-lock: {len(a.keys() & b.keys())} shared packages, {len(bad)} mismatches") -sys.exit(1 if bad else 0) + bad.append(f"{name} {version}: mirror has {sorted(b[name])}") + return {"shared_packages": len(a.keys() & b.keys()), "mismatches": bad, "backports": ahead} + + +def main(): + here = pathlib.Path(__file__).resolve().parent.parent + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--sandbox-lock", type=pathlib.Path, default=here / "Cargo.lock") + parser.add_argument("--mirror-lock", type=pathlib.Path, + default=here.parent / "source-mirror/contracts/approval/Cargo.lock") + parser.add_argument("--source-ref", default="") + parser.add_argument("--json", type=pathlib.Path, help="write a diagnostic report, including on input errors") + args = parser.parse_args() + report = {"sandbox_lock": str(args.sandbox_lock), "mirror_lock": str(args.mirror_lock), + "source_ref": args.source_ref} + try: + mine = tomllib.loads(args.sandbox_lock.read_text())["package"] + theirs = tomllib.loads(args.mirror_lock.read_text())["package"] + report.update(compare(mine, theirs)) + code = 1 if report["mismatches"] else 0 + except (OSError, ValueError, KeyError, TypeError) as error: + report["error"] = str(error) + print(f"check-lock: cannot compare lockfiles: {error}", file=sys.stderr) + code = 2 + if args.json: + args.json.parent.mkdir(parents=True, exist_ok=True) + args.json.write_text(json.dumps(report, indent=2) + "\n") + if "error" not in report: + for line in report["backports"]: + print("lockfile ahead of pin:", line) + for line in report["mismatches"]: + print("lockfile mismatch:", line) + print(f"check-lock: {report['shared_packages']} shared packages, {len(report['mismatches'])} mismatches") + if code: + print("Update the sandbox lockfile against the selected mirror revision; do not remove --locked.") + return code + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/projects/near-approval/sandbox/scripts/prepare-upstream-observation.py b/projects/near-approval/sandbox/scripts/prepare-upstream-observation.py new file mode 100644 index 0000000..dc56a68 --- /dev/null +++ b/projects/near-approval/sandbox/scripts/prepare-upstream-observation.py @@ -0,0 +1,54 @@ +#!/usr/bin/env python3 +"""Adapt only RT-CODEHASH's artifact identity for an unreviewed upstream run. + +The runtime test still checks deployed bytes and on-chain code_hash. Export +surface and behavioral observations keep their reviewed expected values. +Pinned runs never call this script and retain the independent pinned hash. +""" +import argparse +import hashlib +import json +import pathlib +import re + + +def artifact_identity(data): + digest = hashlib.sha256(data).digest() + number = int.from_bytes(digest, "big") + alphabet = "123456789ABCDEFGHJKLMNPQRSTUVWXYZabcdefghijkmnopqrstuvwxyz" + encoded = "" + while number: + number, remainder = divmod(number, 58) + encoded = alphabet[remainder] + encoded + encoded = "1" * (len(digest) - len(digest.lstrip(b"\0"))) + encoded + return {"bytes": len(data), "wasm_sha256": digest.hex(), "code_hash": encoded} + + +def prepare(wasm, source_ref, results, report): + if not re.fullmatch(r"[0-9a-f]{40}", source_ref): + raise ValueError("upstream source_ref must be a full commit SHA") + path = results / "RT-CODEHASH.json" + expected = json.loads(path.read_text()) + identity = artifact_identity(wasm.read_bytes()) + original = {key: expected[key] for key in identity} + expected.update(identity) + report.parent.mkdir(parents=True, exist_ok=True) + report.write_text(json.dumps({"source_ref": source_ref, "reviewed_artifact": original, + "upstream_artifact": identity}, indent=2) + "\n") + path.write_text(json.dumps(expected, indent=2, sort_keys=True) + "\n") + return identity["wasm_sha256"] + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--wasm", type=pathlib.Path, required=True) + parser.add_argument("--source-ref", required=True) + parser.add_argument("--results", type=pathlib.Path, + default=pathlib.Path(__file__).resolve().parent.parent / "results") + parser.add_argument("--report", type=pathlib.Path, required=True) + args = parser.parse_args() + print(prepare(args.wasm, args.source_ref, args.results, args.report)) + + +if __name__ == "__main__": + main() diff --git a/projects/near-approval/sandbox/scripts/test_check_lock.py b/projects/near-approval/sandbox/scripts/test_check_lock.py new file mode 100644 index 0000000..e9be067 --- /dev/null +++ b/projects/near-approval/sandbox/scripts/test_check_lock.py @@ -0,0 +1,103 @@ +#!/usr/bin/env python3 +"""Regression coverage for reviewed pins and floating scheduled upstreams.""" +import importlib.util +import json +import pathlib +import subprocess +import sys +import tempfile +import unittest + +sys.dont_write_bytecode = True +SCRIPT = pathlib.Path(__file__).with_name("check-lock.py") +spec = importlib.util.spec_from_file_location("check_lock", SCRIPT) +check_lock = importlib.util.module_from_spec(spec) +spec.loader.exec_module(check_lock) +REGISTRY = "registry+https://github.com/rust-lang/crates.io-index" +identity_spec = importlib.util.spec_from_file_location( + "upstream_observation", SCRIPT.with_name("prepare-upstream-observation.py")) +identity = importlib.util.module_from_spec(identity_spec) +identity_spec.loader.exec_module(identity) + + +def package(name, version, checksum="same", source=REGISTRY): + return {"name": name, "version": version, "checksum": checksum, "source": source} + + +class LockfileTests(unittest.TestCase): + def test_upstream_adaptation_changes_only_artifact_identity(self): + with tempfile.TemporaryDirectory() as folder: + path = pathlib.Path(folder) + wasm = path / "contract.wasm" + wasm.write_bytes(b"\0asm\x01\0\0\0") + expected = {"bytes": 1, "wasm_sha256": "old", "code_hash": "old", + "function_exports": ["approve"], "reproducible": True} + observation = path / "RT-CODEHASH.json" + observation.write_text(json.dumps(expected)) + behavior = path / "RT-REVERT.json" + behavior.write_text('{"behavior": "must not change"}') + sha = identity.prepare(wasm, "a" * 40, path, path / "report.json") + adjusted = json.loads(observation.read_text()) + self.assertEqual(adjusted["wasm_sha256"], sha) + for key in ["function_exports", "reproducible"]: + self.assertEqual(adjusted[key], expected[key]) + self.assertEqual(behavior.read_text(), '{"behavior": "must not change"}') + with self.assertRaises(ValueError): + identity.prepare(wasm, "not-a-sha", path, path / "report.json") + + def test_reported_failure_and_upstream_catch_up(self): + ours = [package("rustls", "0.23.46"), package("rustls-webpki", "0.103.16"), + package("webpki-roots", "1.0.11")] + self.assertEqual(check_lock.compare(ours, ours)["mismatches"], []) + self.assertEqual(check_lock.compare(ours, ours)["backports"], []) + stale = [package("rustls", "0.23.45"), *ours[1:]] + self.assertEqual(len(check_lock.compare(stale, ours)["mismatches"]), 1) + + def test_exact_backports_still_match_reviewed_pin(self): + for name, (version, old_versions) in check_lock.HOST_TLS_BACKPORTS.items(): + with self.subTest(name=name): + result = check_lock.compare([package(name, version)], + [package(name, old) for old in old_versions]) + self.assertEqual(result["mismatches"], []) + self.assertEqual(len(result["backports"]), 1) + + def test_future_tls_drift_is_rejected(self): + result = check_lock.compare([package("rustls", "0.23.46")], [package("rustls", "0.23.47")]) + self.assertEqual(len(result["mismatches"]), 1) + + def test_checksum_and_source_mismatches_fail_even_for_backports(self): + for name, (version, old_versions) in check_lock.HOST_TLS_BACKPORTS.items(): + with self.subTest(name=name): + for other in [package(name, version, checksum="different"), + package(name, version, source="registry+https://other.invalid"), + package(name, next(iter(old_versions)), source="registry+https://other.invalid")]: + self.assertTrue(check_lock.compare([package(name, version)], [other])["mismatches"]) + + def test_non_tls_drift_is_rejected(self): + self.assertTrue(check_lock.compare([package("near-sdk", "5.29.1")], + [package("near-sdk", "5.30.0")])["mismatches"]) + + def test_multiple_versions_are_checked_individually(self): + ours = [package("example", "1.0.0"), package("example", "2.0.0")] + self.assertEqual(len(check_lock.compare(ours, ours[:1])["mismatches"]), 1) + + def test_json_report_and_missing_input_fail_closed(self): + with tempfile.TemporaryDirectory() as folder: + path = pathlib.Path(folder) + lock = path / "Cargo.lock" + lock.write_text('version = 4\n[[package]]\nname = "example"\nversion = "1.0.0"\n' + f'source = "{REGISTRY}"\nchecksum = "same"\n') + report = path / "report.json" + command = [sys.executable, str(SCRIPT), "--sandbox-lock", str(lock), "--mirror-lock", + str(lock), "--json", str(report), "--source-ref", "test-upstream"] + good = subprocess.run(command, capture_output=True, text=True) + self.assertEqual(good.returncode, 0, good.stderr) + self.assertEqual(json.loads(report.read_text())["source_ref"], "test-upstream") + lock.unlink() + bad = subprocess.run(command, capture_output=True, text=True) + self.assertEqual(bad.returncode, 2) + self.assertIn("error", json.loads(report.read_text())) + + +if __name__ == "__main__": + unittest.main() diff --git a/projects/near-approval/strategy.md b/projects/near-approval/strategy.md index 3d6306f..06fdeb7 100644 --- a/projects/near-approval/strategy.md +++ b/projects/near-approval/strategy.md @@ -1132,14 +1132,15 @@ for fork pull requests. `lean`, `prolog`, `mutants` and `upstream-watch`, on self-hosted macOS runners (`vars.CI_RUNNER`). On a PR, `pin` always runs and each other job runs only when the diff touches its inputs (`tools/scripts/ci-areas.sh`; -Markdown changes run none). Push to `main` and manual runs run every job. -A schedule (`approval-changed.sh`) runs verification only when -`contracts/approval` on trust-framework differs from `.github/approval-seen` -(`*.md` ignored). That sha is the tip already checked, not the pin, and the +Markdown changes run none). Pushes use the complete before/after diff just like PRs; manual runs check all layers. +The separate `near-approval-watch.yml` schedule calls reusable `near-approval.yml` +only when approval core/contract code or workspace build inputs differ from +`.github/approval-seen`. Documentation, upstream sandbox tests, and other +trust-framework changes are ignored. That sha is the tip already checked, not the pin, and the schedule proposes the new tip in a PR only after every applicable check succeeds. The recording job never pushes `main` or moves the verification pin. An open recording PR suppresses repeat checks of that upstream tip -until its review is complete. +until its review is complete, including when later unrelated upstream commits arrive. `verus` (M5) since 2026-10-19. ## 15. Risks diff --git a/tools/scripts/approval-changed.sh b/tools/scripts/approval-changed.sh index 11fcaa9..d4154b5 100755 --- a/tools/scripts/approval-changed.sh +++ b/tools/scripts/approval-changed.sh @@ -4,9 +4,9 @@ # Compares trust-framework's default branch to the sha in # .github/approval-seen, not to the verification pin. The pin stays put # until a human re-pins, so comparing to it re-ran the proofs every night -# after one upstream move. A change is any file under upstream_path -# (contracts/approval) other than *.md, the same cut trust-framework's -# own CI uses: a doc edit does not change the wasm or the proofs. +# after one upstream move. Only the core/contract crates and their workspace +# build inputs count. Documentation, the upstream sandbox harness and other +# trust-framework projects do not change the approval contract under test. # # Prints contract_changed=true|false and source_ref=. # When the contract changed, source_ref is the upstream tip to verify. @@ -34,8 +34,11 @@ emit() { } changed_files() { - # $1 repo, $2 pin, $3 head, $4 path. Prints non-markdown paths, if any. - git -C "$1" diff --name-only "$2" "$3" -- "$4" | awk '!/\.md$/' + # Include both sides of renames so moving code out of a crate is detected. + git -C "$1" diff --no-renames --name-only "$2" "$3" -- \ + "$4/core" "$4/contract" "$4/Cargo.toml" "$4/Cargo.lock" \ + "$4/.cargo" "$4/rust-toolchain" "$4/rust-toolchain.toml" "$4/build.rs" \ + | awk '!/\.(md|mdx|rst|adoc)$/ && !/(^|\/)docs\//' } if [ "${1:-}" = --repo ]; then @@ -51,7 +54,7 @@ if [ "${1:-}" = --repo ]; then emit contract_changed=true emit "source_ref=$head" else - echo "Approval contract unchanged ($pin -> $head) under $path, ignoring *.md." + echo "Approval contract build inputs unchanged ($pin -> $head)." emit contract_changed=false emit source_ref= fi @@ -92,15 +95,24 @@ if ! files=$(changed_files "$work" "$pin_fetch" "$head" "$path"); then fi if [ -n "$files" ]; then if [ -n "${GH_TOKEN:-}" ] && [ -n "${GITHUB_REPOSITORY:-}" ]; then - pr=$(gh pr list --repo "$GITHUB_REPOSITORY" --state open \ - --base "${BASE_BRANCH:-main}" --head "automation/approval-seen-$head" \ - --author 'github-actions[bot]' --json number --jq '.[0].number // empty') - if [ -n "$pr" ]; then - echo "Approval contract tip $head already checked; PR #$pr awaits review." - emit contract_changed=false - emit source_ref= - exit 0 - fi + proposals=$(gh pr list --repo "$GITHUB_REPOSITORY" --state open --limit 100 \ + --base "${BASE_BRANCH:-main}" --author 'github-actions[bot]' \ + --json number,headRefName \ + --jq '.[] | select(.headRefName | startswith("automation/approval-seen-")) | [.number, .headRefName] | @tsv') + while IFS=$'\t' read -r pr branch; do + verified=${branch#automation/approval-seen-} + [[ $verified =~ ^[0-9a-f]{40}$ ]] || continue + if ! git -C "$work" cat-file -e "$verified^{commit}" 2>/dev/null; then + git -C "$work" fetch -q --depth 1 --filter=blob:none origin "$verified" + fi + remaining=$(changed_files "$work" "$verified" "$head" "$path") + if [ -z "$remaining" ]; then + echo "Approval contract code already checked at $verified; PR #$pr awaits review." + emit contract_changed=false + emit source_ref= + exit 0 + fi + done <<< "$proposals" fi { echo "### Approval contract changed" @@ -119,7 +131,7 @@ else { echo "### Approval contract unchanged" echo - echo "\`$path\` at upstream \`$head\` matches the last check \`$pin_fetch\` (ignoring \`*.md\`). Skipping verification." + echo "Approval core/contract code and workspace build inputs at \`$head\` match the last check \`$pin_fetch\`. Skipping verification." } >>"${GITHUB_STEP_SUMMARY:-/dev/null}" echo "Approval contract unchanged ($pin_fetch). Skipping verification." emit contract_changed=false diff --git a/tools/scripts/ci-areas.sh b/tools/scripts/ci-areas.sh index dfd4a42..c63d03f 100755 --- a/tools/scripts/ci-areas.sh +++ b/tools/scripts/ci-areas.sh @@ -3,8 +3,8 @@ # line, repo-relative, as `git diff --name-only` prints them) on stdin and # prints `=true|false` for each gated job, for $GITHUB_OUTPUT. # -# The rules list what each path can affect; a path no rule names runs every -# job, so a new file or directory is checked until someone narrows it here. +# The rules list what each path can affect. Unknown verification paths run +# every job; unrelated repository paths and documentation run none. # The pin job is not gated: it always runs (status.toml, the gitlink). # # usage: git diff --name-only BASE HEAD | tools/scripts/ci-areas.sh @@ -24,48 +24,49 @@ else [ -n "$f" ] || continue case "$f" in # Docs: no script, test or proof reads a Markdown file. - *.md) add="" ;; + *.md | *.mdx | *.rst | *.adoc | docs/* | Plans/* | */docs/*) add="" ;; # status.toml also holds run-verus.sh's floor (verus_min_verified), so # an edit to it re-runs the verus gate; pin and status-lint check the rest. - $p/status.toml) add="verus" ;; + "$p"/status.toml) add="verus" ;; # Checked by the pin job alone (pin and status-lint). - $s/check-pin.sh | $s/check-status.sh | $s/test-check-status.sh) add="" ;; + "$s"/check-pin.sh | "$s"/check-status.sh | "$s"/test-check-status.sh) add="" ;; # A recording PR only advances the already-successful schedule baseline. - .github/approval-seen | $s/record-approval-check.sh | $s/test-record-approval-check.sh) add="" ;; + .github/approval-seen | "$s"/record-approval-check.sh | "$s"/test-record-approval-check.sh | "$s"/approval-changed.sh | "$s"/test-approval-changed.sh | .github/workflows/near-approval-watch.yml) add="" ;; # The weekly upstream watch. - $s/upstream-watch.sh | tools/upstream-watch.toml) add="" ;; + "$s"/upstream-watch.sh | tools/upstream-watch.toml) add="" ;; # M5: the verified twin, its canary, mutants and erasure check. - $p/verus/* | $s/run-verus.sh | $s/get-verus.sh | $s/erasure-check.py) add="verus" ;; + "$p"/verus/* | "$s"/run-verus.sh | "$s"/get-verus.sh | "$s"/erasure-check.py) add="verus" ;; # Mutant definitions: the weekly mutants job, and plain's self-test. - $p/kani/mutants/* | $s/run-mutants.sh | $s/test-run-mutants.sh) add="plain" ;; + "$p"/kani/mutants/* | "$s"/run-mutants.sh | "$s"/test-run-mutants.sh) add="plain" ;; # U-1 loop bounds. - $p/kani/unwind-rules.tsv | $s/kani-loops.py) add="loops" ;; - $s/run-kani.sh | $s/check-covers.sh) add="kani" ;; + "$p"/kani/unwind-rules.tsv | "$s"/kani-loops.py) add="loops" ;; + "$s"/run-kani.sh | "$s"/check-covers.sh) add="kani" ;; # ApprovalCore.tla feeds tla_facts.pl (prolog), and Lean's MC-4 # compares against the TLC graph. - $p/tla/*) add="tla lean prolog" ;; - $s/run-tla.sh) add="tla" ;; - $s/get-tla-tools.sh) add="tla lean" ;; - $p/lean/* | $s/run-lean.sh | $s/get-lean.sh) add="lean" ;; + "$p"/tla/*) add="tla lean prolog" ;; + "$s"/run-tla.sh) add="tla" ;; + "$s"/get-tla-tools.sh) add="tla lean" ;; + "$p"/lean/* | "$s"/run-lean.sh | "$s"/get-lean.sh) add="lean" ;; # plain's `facts` test reads code_facts.pl; run-lean.sh reads # tla_facts.pl. - $p/prolog/verification/verifier_rules.pl | $p/prolog/tests/test_verifier_rules.pl) add="prolog sandbox" ;; + "$p"/prolog/verification/verifier_rules.pl | "$p"/prolog/tests/test_verifier_rules.pl) add="prolog sandbox" ;; # near-unit regenerates api_facts.pl from the wasm and diffs it. - $p/prolog/extracted/api_facts.pl) add="prolog near_unit" ;; - $p/prolog/extracted/*) add="prolog plain lean" ;; - $p/prolog/* | $s/run-prolog.sh | $s/run-mc3.sh | $s/tla-facts.py) add="prolog" ;; - $s/mc3.py) add="prolog lean" ;; + "$p"/prolog/extracted/api_facts.pl) add="prolog near_unit" ;; + "$p"/prolog/extracted/*) add="prolog plain lean" ;; + "$p"/prolog/* | "$s"/run-prolog.sh | "$s"/run-mc3.sh | "$s"/tla-facts.py) add="prolog" ;; + "$s"/mc3.py) add="prolog lean" ;; # M3: the shell tests and the wasm surface. - $p/near-tests/mutants/* | $p/near-tests/run-mutants.sh) add="" ;; - $p/near-tests/* | $p/wasm-surface.expected | $s/wasm-surface.sh) add="near_unit" ;; - $s/get-cargo-near.sh) add="near_unit sandbox" ;; + "$p"/near-tests/mutants/* | "$p"/near-tests/run-mutants.sh) add="" ;; + "$p"/near-tests/* | "$p"/wasm-surface.expected | "$s"/wasm-surface.sh) add="near_unit" ;; + "$s"/get-cargo-near.sh) add="near_unit sandbox" ;; # M6/M7: the sandbox suite, its traces and the deploy checks it # demonstrates; the verifier rules also run in prolog. - $p/sandbox/* | $p/conformance/* | $p/deploy-checks/*) add="sandbox" ;; + "$p"/sandbox/* | "$p"/conformance/* | "$p"/deploy-checks/*) add="sandbox" ;; # Everything else, including the kani crate (every job builds or runs # it), the trust-framework gitlink, versions.env, ci-submodule.sh, # this script and the workflow itself. - *) add="$jobs" ;; + "$p"/* | tools/* | .gitmodules | Cargo.toml | Cargo.lock | .github/workflows/near-approval.yml) add="$jobs" ;; + *) add="" ;; esac if [ -n "${CI_AREAS_EXPLAIN:-}" ]; then echo "$f: ${add:-(none)}" >&2 diff --git a/tools/scripts/ci-changed-areas.sh b/tools/scripts/ci-changed-areas.sh new file mode 100755 index 0000000..5fa9836 --- /dev/null +++ b/tools/scripts/ci-changed-areas.sh @@ -0,0 +1,24 @@ +#!/usr/bin/env bash +# Select verification jobs from the complete PR/push diff. An upstream +# verification call or manual run checks all layers. Missing Git history +# conservatively runs all layers rather than silently missing a change. +set -euo pipefail +areas=$(cd "$(dirname "$0")" && pwd)/ci-areas.sh +if [ -n "${SOURCE_REF:-}" ]; then + [[ $SOURCE_REF =~ ^[0-9a-f]{40}$ ]] || { echo 'invalid upstream ref' >&2; exit 2; } + "$areas" --all /dev/null || git fetch --no-tags --depth 1 origin "$base"; then + git diff --no-renames --name-only "$base" HEAD | CI_AREAS_EXPLAIN=1 "$areas" + exit 0 + fi + fi + echo 'CI base unavailable; checking every verification layer.' >&2 + ;; +esac +"$areas" --all "$body" < "$work/contracts/approval/sandbox/tests/sandbox.rs" +printf 'diagram\n' > "$work/contracts/approval/core/docs/diagram.svg" +git -C "$work" add contracts +git -C "$work" commit -q -m upstream-harness-and-docs +ignored=$(git -C "$work" rev-parse HEAD) +out=$("$script" --repo "$work" --pin "$pin" --head "$ignored" --path contracts/approval) +printf '%s\n' "$out" | grep -q '^contract_changed=false$' + printf '# readme changed\n' >"$work/contracts/approval/README.md" git -C "$work" add contracts git -C "$work" commit -q -m docs @@ -62,10 +72,23 @@ git -C "$work" commit -q -m dependencies deps=$(git -C "$work" rev-parse HEAD) out=$("$script" --repo "$work" --pin "$code" --head "$deps" --path contracts/approval) printf '%s\n' "$out" | grep -q '^contract_changed=true$' +mkdir -p "$work/contracts/approval/contract/src" +printf 'fn wrapper() {}\n' > "$work/contracts/approval/contract/src/lib.rs" +git -C "$work" add contracts +git -C "$work" commit -q -m contract-wrapper +wrapper=$(git -C "$work" rev-parse HEAD) +out=$("$script" --repo "$work" --pin "$deps" --head "$wrapper" --path contracts/approval) +printf '%s\n' "$out" | grep -q '^contract_changed=true$' +printf '[workspace]\n' > "$work/contracts/approval/Cargo.toml" +git -C "$work" add contracts +git -C "$work" commit -q -m workspace-build-input +workspace=$(git -C "$work" rev-parse HEAD) +out=$("$script" --repo "$work" --pin "$wrapper" --head "$workspace" --path contracts/approval) +printf '%s\n' "$out" | grep -q '^contract_changed=true$' git -C "$work" rm -q contracts/approval/core/src/lib.rs git -C "$work" commit -q -m deletion deleted=$(git -C "$work" rev-parse HEAD) -out=$("$script" --repo "$work" --pin "$deps" --head "$deleted" --path contracts/approval) +out=$("$script" --repo "$work" --pin "$workspace" --head "$deleted" --path contracts/approval) printf '%s\n' "$out" | grep -q '^contract_changed=true$' # Git comparison errors must fail; they must never be reported as unchanged. @@ -86,15 +109,29 @@ cat > "$ci/bin/gh" <<'SH' #!/usr/bin/env bash set -euo pipefail if [ "${PR_TEST_FAIL:-}" = 1 ]; then exit 19; fi -printf '%s' "${EXISTING_PR:-}" +if [ -n "${EXISTING_PR:-}" ]; then + printf '%s\tautomation/approval-seen-%s\n' "$EXISTING_PR" "$PR_TEST_VERIFIED_REF" +fi SH chmod +x "$ci/bin/gh" -export PATH="$ci/bin:$PATH" GH_TOKEN=test GITHUB_REPOSITORY=example/formalver +export PATH="$ci/bin:$PATH" GH_TOKEN=test GITHUB_REPOSITORY=example/formalver PR_TEST_VERIFIED_REF="$deleted" +out=$(EXISTING_PR=42 "$ci/tools/scripts/approval-changed.sh" 2>"$work/fetch.log") +printf '%s\n' "$out" | grep -q '^contract_changed=false$' +# A later unrelated commit must not reverify code already checked by an open PR. +printf 'another unrelated change\n' >> "$work/other.txt" +git -C "$work" add other.txt +git -C "$work" commit -q -m unrelated-after-check +latest=$(git -C "$work" rev-parse HEAD) out=$(EXISTING_PR=42 "$ci/tools/scripts/approval-changed.sh" 2>"$work/fetch.log") printf '%s\n' "$out" | grep -q '^contract_changed=false$' out=$(EXISTING_PR='' "$ci/tools/scripts/approval-changed.sh" 2>"$work/fetch.log") printf '%s\n' "$out" | grep -q '^contract_changed=true$' -printf '%s\n' "$out" | grep -q "^source_ref=$deleted$" +printf '%s\n' "$out" | grep -q "^source_ref=$latest$" +printf 'fn new_wrapper() {}\n' > "$work/contracts/approval/contract/src/lib.rs" +git -C "$work" add contracts +git -C "$work" commit -q -m new-contract-after-check +out=$(EXISTING_PR=42 "$ci/tools/scripts/approval-changed.sh" 2>"$work/fetch.log") +printf '%s\n' "$out" | grep -q '^contract_changed=true$' if PR_TEST_FAIL=1 "$ci/tools/scripts/approval-changed.sh" >"$work/api-error.log" 2>&1; then echo 'FAIL: GitHub API failure was ignored' >&2; exit 1 fi diff --git a/tools/scripts/test-ci-areas.sh b/tools/scripts/test-ci-areas.sh index 68a9267..9e37142 100755 --- a/tools/scripts/test-ci-areas.sh +++ b/tools/scripts/test-ci-areas.sh @@ -24,6 +24,10 @@ expect "" $p/strategy.md $p/kani/RESULTS.md README.md expect "verus" $p/status.toml expect "" tools/scripts/check-pin.sh tools/scripts/check-status.sh tools/scripts/test-check-status.sh expect "" .github/approval-seen tools/scripts/record-approval-check.sh tools/scripts/test-record-approval-check.sh +expect "" tools/scripts/approval-changed.sh tools/scripts/test-approval-changed.sh .github/workflows/near-approval-watch.yml +expect "" docs/architecture.svg projects/near-approval/lean/docs/diagram.png .github/CODEOWNERS +expect "" projects/ironclaw/verus/src/lib.rs +expect "prolog" projects/near-approval/prolog/requirements/r.pl README.md .gitignore expect "" tools/upstream-watch.toml tools/scripts/upstream-watch.sh expect "verus" $p/verus/src/lib.rs $p/verus/mutants.toml tools/scripts/run-verus.sh tools/scripts/get-verus.sh tools/scripts/erasure-check.py expect "" # no changes diff --git a/tools/scripts/test-ci-changed-areas.sh b/tools/scripts/test-ci-changed-areas.sh new file mode 100755 index 0000000..1c59c57 --- /dev/null +++ b/tools/scripts/test-ci-changed-areas.sh @@ -0,0 +1,44 @@ +#!/usr/bin/env bash +# Verify whole push/PR ranges rather than just the most recent commit. +set -euo pipefail +script=$(cd "$(dirname "$0")" && pwd)/ci-changed-areas.sh +work=$(mktemp -d) +trap 'rm -rf "$work"' EXIT +git -C "$work" init -q +git -C "$work" config user.name test +git -C "$work" config user.email test@example.com +git -C "$work" config commit.gpgsign false +mkdir -p "$work/projects/near-approval/prolog/requirements" +printf 'initial\n' > "$work/README.md" +git -C "$work" add . +git -C "$work" commit -qm base +base=$(git -C "$work" rev-parse HEAD) +printf 'rule.\n' > "$work/projects/near-approval/prolog/requirements/r.pl" +git -C "$work" add . +git -C "$work" commit -qm prolog +prolog=$(git -C "$work" rev-parse HEAD) +printf 'docs\n' >> "$work/README.md" +git -C "$work" add . +git -C "$work" commit -qm docs +cd "$work" +selected() { "$script" | sed -n 's/=true$//p' | tr '\n' ' ' | sed 's/ $//'; } +export SOURCE_REF='' +out=$(GITHUB_EVENT_NAME=push BASE_SHA="$base" selected 2>"$work/explain.log") +[ "$out" = prolog ] || { echo "FAIL: multi-commit push -> $out" >&2; exit 1; } +out=$(GITHUB_EVENT_NAME=pull_request BASE_SHA="$prolog" selected 2>"$work/explain.log") +[ -z "$out" ] || { echo "FAIL: docs-only PR -> $out" >&2; exit 1; } +out=$(GITHUB_EVENT_NAME=pull_request BASE_SHA="$base" selected 2>"$work/explain.log") +[ "$out" = prolog ] +out=$(GITHUB_EVENT_NAME=push BASE_SHA=0000000000000000000000000000000000000000 selected) +[ "$out" = 'plain loops kani tla lean prolog near_unit sandbox verus' ] +out=$(GITHUB_EVENT_NAME=schedule selected) +[ "$out" = 'plain loops kani tla lean prolog near_unit sandbox verus' ] +out=$(GITHUB_EVENT_NAME=push SOURCE_REF=1111111111111111111111111111111111111111 selected) +[ "$out" = 'plain loops kani tla lean prolog near_unit sandbox verus' ] +before_rename=$(git rev-parse HEAD) +mkdir -p projects/near-approval/lean +git mv projects/near-approval/prolog/requirements/r.pl projects/near-approval/lean/Rule.lean +git commit -qm rename-layer +out=$(GITHUB_EVENT_NAME=push BASE_SHA="$before_rename" selected 2>"$work/explain.log") +[ "$out" = 'lean prolog' ] || { echo "FAIL: renamed layer -> $out" >&2; exit 1; } +echo 'ci-changed-areas: all cases pass' From 1f7dc7e6e1df7fd42c94f2a6a5707002ef798816 Mon Sep 17 00:00:00 2001 From: Gabe Hamilton Date: Mon, 2 Nov 2026 12:51:25 -0700 Subject: [PATCH 2/3] approval-changed: ignore unfetchable recording PRs instead of aborting Co-Authored-By: Claude Sonnet 5.5 --- tools/scripts/approval-changed.sh | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/tools/scripts/approval-changed.sh b/tools/scripts/approval-changed.sh index d4154b5..415fddf 100755 --- a/tools/scripts/approval-changed.sh +++ b/tools/scripts/approval-changed.sh @@ -102,10 +102,16 @@ if [ -n "$files" ]; then while IFS=$'\t' read -r pr branch; do verified=${branch#automation/approval-seen-} [[ $verified =~ ^[0-9a-f]{40}$ ]] || continue - if ! git -C "$work" cat-file -e "$verified^{commit}" 2>/dev/null; then - git -C "$work" fetch -q --depth 1 --filter=blob:none origin "$verified" + # A stale proposal must not abort the nightly: verify instead. + if ! git -C "$work" cat-file -e "$verified^{commit}" 2>/dev/null && + ! git -C "$work" fetch -q --depth 1 --filter=blob:none origin "$verified"; then + echo "approval-changed: ignoring PR #$pr, cannot fetch $verified" >&2 + continue + fi + if ! remaining=$(changed_files "$work" "$verified" "$head" "$path"); then + echo "approval-changed: ignoring PR #$pr, cannot compare $verified" >&2 + continue fi - remaining=$(changed_files "$work" "$verified" "$head" "$path") if [ -z "$remaining" ]; then echo "Approval contract code already checked at $verified; PR #$pr awaits review." emit contract_changed=false From 268b80d0138920c7e002a1d627c9d1cd49b19aeb Mon Sep 17 00:00:00 2001 From: Gabe Hamilton Date: Mon, 2 Nov 2026 12:58:23 -0700 Subject: [PATCH 3/3] ci: drop runner hardware and policy details from workflow comments Co-Authored-By: Claude Sonnet 5.5 --- .github/workflows/near-approval.yml | 29 ++++++++++++---------------- .github/workflows/upstream-watch.yml | 19 +++++++++--------- 2 files changed, 21 insertions(+), 27 deletions(-) diff --git a/.github/workflows/near-approval.yml b/.github/workflows/near-approval.yml index 0bf97f5..1a60b78 100644 --- a/.github/workflows/near-approval.yml +++ b/.github/workflows/near-approval.yml @@ -71,16 +71,13 @@ concurrency: env: CARGO_TERM_COLOR: always -# Every job takes its label from the CI_RUNNER repository variable (the -# self-hosted macOS arm64 runners) and falls back to its original hosted label. -# Those runners refuse Dependabot's runs and Claude Code cloud sessions' -# (commits signed with Anthropic's shared key), so the parenthesised clause -# that opens each runs-on sends those runs to ubuntu-latest instead, ahead of -# CI_RUNNER and KANI_RUNNER. That clause is the canonical routing from -# the shared CI routing policy: keep every copy byte-identical to it, and change -# it there first. The Mac keeps HOME between jobs and has no sudo: the steps -# below avoid `rustup default`, ~/.gitconfig and ~/.ssh, and the hosted-only -# swap setup is skipped there. +# Every job takes its label from the CI_RUNNER repository variable and falls +# back to its original hosted label. The parenthesised clause that opens each +# runs-on sends Dependabot and automated-agent runs to ubuntu-latest instead, +# ahead of CI_RUNNER and KANI_RUNNER; keep every copy byte-identical. A +# self-hosted runner keeps HOME between jobs and has no sudo: the steps below +# avoid `rustup default`, ~/.gitconfig and ~/.ssh, and the hosted-only swap +# setup is skipped there. # # PRs and pushes select only affected verification layers from the entire # change range. Manual calls and a changed upstream contract verify all layers. @@ -130,8 +127,8 @@ jobs: - name: Python >= 3.11 (tomllib) if: runner.os == 'macOS' run: | - # macOS's /usr/bin/python3 is 3.9; the Mac runner has Homebrew's - # newer ones under versioned names only. + # macOS's /usr/bin/python3 is 3.9; Homebrew's newer ones exist + # under versioned names only. python3 -c 'import tomllib' 2>/dev/null && exit 0 for py in python3.13 python3.12 python3.11; do if p=$(command -v "$py"); then @@ -233,10 +230,8 @@ jobs: # CBMC peaks at 6.5 to 9.5 GB on the step harnesses; this repository's # default runner has 2 CPUs and 7.9 GB. Set the KANI_RUNNER repository # variable to a larger runner label (and KANI_SWAP_GB to 0) to avoid - # relying on swap. Without it, CI_RUNNER (the self-hosted Mac: 64 GB, no - # swap file needed) is next. Routed runs (see above `jobs:`) skip both and - # get ubuntu-latest with the swap step: KANI_RUNNER can name a self-hosted - # label (today it is `kani`, on the Macs), which would refuse them. The + # relying on swap. Without it, CI_RUNNER is next. Routed runs (see above + # `jobs:`) skip both and get ubuntu-latest with the swap step. The # timeouts here and on mutants assume that 2-CPU, swap-backed runner. runs-on: ${{ (startsWith(github.head_ref || github.ref_name, 'dependabot/') || github.actor == 'dependabot[bot]' || github.triggering_actor == 'dependabot[bot]' || startsWith(github.head_ref || github.ref_name, 'claude/') || contains(github.event.pull_request.body, 'claude.ai/code/session_') || github.event.head_commit.committer.email == 'noreply@anthropic.com') && 'ubuntu-latest' || vars.KANI_RUNNER || vars.CI_RUNNER || 'ubuntu-latest' }} # A step part may need most of KANI_TIMEOUT (120 min) on swap. @@ -666,7 +661,7 @@ jobs: needs: pin if: inputs.sandbox || needs.pin.outputs.sandbox == 'true' runs-on: ${{ (startsWith(github.head_ref || github.ref_name, 'dependabot/') || github.actor == 'dependabot[bot]' || github.triggering_actor == 'dependabot[bot]' || startsWith(github.head_ref || github.ref_name, 'claude/') || contains(github.event.pull_request.body, 'claude.ai/code/session_') || github.event.head_commit.committer.email == 'noreply@anthropic.com') && 'ubuntu-latest' || vars.CI_RUNNER || 'ubuntu-latest' }} - # The reproducible build runs an amd64 image (emulated on the Mac) and + # The reproducible build runs an amd64 image (emulated on arm64 hosts) and # RT-TRACE replays 210 traces. timeout-minutes: 120 env: diff --git a/.github/workflows/upstream-watch.yml b/.github/workflows/upstream-watch.yml index 9abdd7a..c2403c8 100644 --- a/.github/workflows/upstream-watch.yml +++ b/.github/workflows/upstream-watch.yml @@ -12,8 +12,8 @@ permissions: contents: read issues: write -# Up to 6 self-hosted runner instances share one Mac, so a schedule and a -# dispatch can now run at once; both could miss the open issue and create +# Runner instances can share a host, so a schedule and a dispatch can run +# at once; both could miss the open issue and create # two. Queue them instead. concurrency: group: upstream-watch @@ -21,12 +21,11 @@ concurrency: jobs: upstream-watch: - # The CI_RUNNER repository variable selects the self-hosted macOS runners. - # The parenthesised clause ahead of it is the canonical routing from - # the shared CI routing policy (keep it byte-identical): it sends runs those - # runners refuse, Dependabot's and Claude Code cloud sessions', to - # ubuntu-latest. On a schedule or dispatch it rarely matches (a dispatch on - # a dependabot/ or claude/ ref does). + # The CI_RUNNER repository variable selects the runner. The parenthesised + # clause ahead of it (keep it identical to near-approval.yml) sends + # Dependabot and automated-agent runs to ubuntu-latest. On a schedule or + # dispatch it rarely matches (a dispatch on a dependabot/ or claude/ ref + # does). runs-on: ${{ (startsWith(github.head_ref || github.ref_name, 'dependabot/') || github.actor == 'dependabot[bot]' || github.triggering_actor == 'dependabot[bot]' || startsWith(github.head_ref || github.ref_name, 'claude/') || contains(github.event.pull_request.body, 'claude.ai/code/session_') || github.event.head_commit.committer.email == 'noreply@anthropic.com') && 'ubuntu-latest' || vars.CI_RUNNER || 'ubuntu-latest' }} steps: - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0 @@ -35,8 +34,8 @@ jobs: - name: Python >= 3.11 (tomllib) if: runner.os == 'macOS' run: | - # macOS's /usr/bin/python3 is 3.9; the Mac runner has Homebrew's - # newer ones under versioned names only. + # macOS's /usr/bin/python3 is 3.9; Homebrew's newer ones exist + # under versioned names only. python3 -c 'import tomllib' 2>/dev/null && exit 0 for py in python3.13 python3.12 python3.11; do if p=$(command -v "$py"); then