diff --git a/.github/workflows/anneal-release.yml b/.github/workflows/anneal-release.yml index 09ac36a4a2..d316deccdb 100644 --- a/.github/workflows/anneal-release.yml +++ b/.github/workflows/anneal-release.yml @@ -16,14 +16,6 @@ on: - 'anneal/Cargo.toml' workflow_dispatch: inputs: - zstd_level: - description: 'Zstd compression level (1-22)' - required: false - default: '19' - aeneas_version: - description: 'Aeneas version to roll to' - required: false - default: 'PROMPT: Enter Aeneas version' version: description: 'Anneal version' required: true @@ -42,6 +34,8 @@ jobs: check-version: name: Check if version was updated runs-on: ubuntu-latest + permissions: + contents: read # required to compare the checked-out commit with HEAD^ # Don't run this on forks. Also skip it on workflow_dispatch because that # trigger is specifically for creating the version-bumping PR, not for # checking if it was already done. @@ -70,11 +64,11 @@ jobs: if [ "$CUR_VER" != "$PREV_VER" ]; then echo "Version change detected." - echo "changed=true" >> $GITHUB_OUTPUT - echo "version=$CUR_VER" >> $GITHUB_OUTPUT + echo "changed=true" >> "$GITHUB_OUTPUT" + echo "version=$CUR_VER" >> "$GITHUB_OUTPUT" else echo "Version unchanged." - echo "changed=false" >> $GITHUB_OUTPUT + echo "changed=false" >> "$GITHUB_OUTPUT" fi release: @@ -117,7 +111,7 @@ jobs: git config user.name "Google PR Creation Bot" git config user.email "github-pull-request-creation-bot@google.com" git tag -a "$TAG" -m "Release $TAG" - git push https://x-access-token:$GH_TOKEN@github.com/$GH_REPO.git "$TAG" + git push "https://x-access-token:${GH_TOKEN}@github.com/${GH_REPO}.git" "$TAG" - name: Create GitHub Release env: @@ -128,166 +122,312 @@ jobs: TAG="anneal-v$VERSION" gh release create "$TAG" --generate-notes - create-release: - name: Create Release for Artifacts + prepare-release-source: + name: Prepare release source patch if: github.event_name == 'workflow_dispatch' runs-on: ubuntu-latest permissions: - contents: write # required to create a GitHub release + contents: read outputs: - tag_name: ${{ steps.tag.outputs.tag_name }} + base_sha: ${{ steps.prepare.outputs.base_sha }} + short_base_sha: ${{ steps.prepare.outputs.short_base_sha }} steps: - name: Checkout uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 with: + ref: ${{ github.event.inputs.branch }} persist-credentials: false + fetch-depth: 0 + + - name: Prepare version bump patch + id: prepare + env: + VERSION: ${{ github.event.inputs.version }} + run: | + set -eo pipefail + BASE_SHA="$(git rev-parse HEAD)" + SHORT_BASE_SHA="${BASE_SHA:0:12}" + + ./ci/release_anneal_version.sh "$VERSION" + + python3 anneal/tools/check-release-pr-files.py \ + --context "Release version bump" \ + --include-untracked \ + --allowed anneal/Cargo.lock \ + --allowed anneal/Cargo.toml \ + --allowed anneal/README.md \ + --required anneal/Cargo.toml + + git diff --binary > anneal-release-source.patch + if [ ! -s anneal-release-source.patch ]; then + echo "::error::Release version bump produced an empty patch." + exit 1 + fi + + echo "base_sha=${BASE_SHA}" >> "$GITHUB_OUTPUT" + echo "short_base_sha=${SHORT_BASE_SHA}" >> "$GITHUB_OUTPUT" + + - name: Upload release source patch + uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0 + with: + name: anneal-release-source-patch + path: anneal-release-source.patch + if-no-files-found: error + retention-days: 1 + + create-release: + name: Create toolchain artifact release + needs: prepare-release-source + if: github.event_name == 'workflow_dispatch' + runs-on: ubuntu-latest + permissions: + contents: write # required to create a GitHub release + outputs: + tag_name: ${{ steps.tag.outputs.tag_name }} + steps: - name: Create Release id: tag env: GH_TOKEN: ${{ github.token }} - GITHUB_SHA: ${{ github.sha }} + VERSION: ${{ github.event.inputs.version }} + GH_REPO: ${{ github.repository }} + GITHUB_RUN_ID: ${{ github.run_id }} + BASE_SHA: ${{ needs.prepare-release-source.outputs.base_sha }} + SHORT_BASE_SHA: ${{ needs.prepare-release-source.outputs.short_base_sha }} run: | set -eo pipefail - TAG_NAME="build-$(date +'%Y.%m.%d.%H%M%S')-$GITHUB_SHA" - gh release create "$TAG_NAME" --generate-notes --draft --prerelease - echo "tag_name=${TAG_NAME}" >> $GITHUB_OUTPUT + TAG_NAME="anneal-toolchains-v${VERSION}-${GITHUB_RUN_ID}-${SHORT_BASE_SHA}" + gh release create "$TAG_NAME" \ + --repo "$GH_REPO" \ + --target "$BASE_SHA" \ + --title "$TAG_NAME" \ + --notes "Machine-generated Anneal toolchain artifacts for cargo-anneal ${VERSION}, built from ${BASE_SHA} after applying the generated release version-bump patch." \ + --prerelease \ + --latest=false + echo "tag_name=${TAG_NAME}" >> "$GITHUB_OUTPUT" publish-artifacts: - name: Publish Artifacts (${{ matrix.target }}) - needs: [check-version, release, create-release] - # We use `always()` to ensure this job runs even if the `release` job is - # skipped (which happens on PRs). We still require `check-version` to - # succeed to avoid running on failures. - if: always() && (needs.check-version.result == 'success' || needs.create-release.result == 'success') + name: Publish toolchain artifact (${{ matrix.target }}) + needs: [prepare-release-source, create-release] + if: github.event_name == 'workflow_dispatch' permissions: + actions: read # Required to download the release source patch. contents: write # This is required to upload assets to a release. runs-on: ${{ matrix.os }} strategy: + fail-fast: false matrix: include: - os: ubuntu-latest target: linux-x86_64 - rust_triple: x86_64-unknown-linux-gnu + cargo_os: linux + cargo_arch: x86_64 - os: ubuntu-24.04-arm target: linux-aarch64 - rust_triple: aarch64-unknown-linux-gnu + cargo_os: linux + cargo_arch: aarch64 - os: macos-15-intel target: macos-x86_64 - rust_triple: x86_64-apple-darwin + cargo_os: macos + cargo_arch: x86_64 - os: macos-latest target: macos-aarch64 - rust_triple: aarch64-apple-darwin + cargo_os: macos + cargo_arch: aarch64 steps: - name: Checkout uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 with: + ref: ${{ needs.prepare-release-source.outputs.base_sha }} persist-credentials: false - - name: Extract Metadata - id: meta + - name: Download release source patch + uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 # v7.0.0 + with: + name: anneal-release-source-patch + path: . + + - name: Apply release source patch run: | set -eo pipefail - cd anneal - AENEAS_TAG=$(sed -n 's/^tag = "\(.*\)"/\1/p' Cargo.toml | head -n 1) - RUST_DATE=$(sed -n 's/^date = "\(.*\)"/\1/p' Cargo.toml | head -n 1) - echo "aeneas_tag=$AENEAS_TAG" >> $GITHUB_OUTPUT - echo "rust_date=$RUST_DATE" >> $GITHUB_OUTPUT + git apply --check anneal-release-source.patch + git apply anneal-release-source.patch - - name: Install elan + - name: Free up disk space + if: runner.os == 'Linux' run: | - set -eo pipefail - curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none - echo "$HOME/.elan/bin" >> $GITHUB_PATH + df -h + sudo rm -rf /usr/local/lib/android + sudo rm -rf /usr/share/dotnet + sudo rm -rf /usr/local/share/boost + df -h - - name: Install zstd (macOS) - if: runner.os == 'macOS' - run: brew install zstd + - name: Install Nix + uses: DeterminateSystems/determinate-nix-action@441b9e401ac050c38a07d8313748c5c2d17e8aff # v3.6.1 - - name: Download and Package - env: - RUST_TRIPLE: ${{ matrix.rust_triple }} - ANNEAL_ZSTD_LEVEL: ${{ github.event.inputs.zstd_level || 19 }} - run: | - set -eo pipefail - cd anneal - - STAGING_DIR="dist_staging" - mkdir -p "$STAGING_DIR" - - ./tools/build-prebuilt.sh "$RUST_TRIPLE" - - - name: Upload Artifact - if: github.event_name == 'workflow_dispatch' || (github.event_name != 'pull_request' && needs.release.result == 'success') + # On Ubuntu 24.04 (currently `ubuntu-latest`), AppArmor restricts unprivileged user namespaces by default. + # The Nix build sandbox uses `bubblewrap` for Linux FHS execution, which requires creating a user namespace. + - name: Enable unprivileged user namespaces (Ubuntu 24.04) + if: runner.os == 'Linux' + run: sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0 + + - name: Build and publish toolchain artifact env: GH_TOKEN: ${{ github.token }} - VERSION: ${{ needs.check-version.outputs.version }} - AENEAS_VERSION: ${{ github.event.inputs.aeneas_version }} - TARGET: ${{ matrix.target }} - EVENT_NAME: ${{ github.event_name }} + GH_REPO: ${{ github.repository }} TAG_NAME: ${{ needs.create-release.outputs.tag_name }} + TARGET: ${{ matrix.target }} + CARGO_OS: ${{ matrix.cargo_os }} + CARGO_ARCH: ${{ matrix.cargo_arch }} run: | - if [ "$EVENT_NAME" = "workflow_dispatch" ]; then - TAG="$TAG_NAME" - else - TAG="anneal-v$VERSION" + set -eo pipefail + ARCHIVE_NAME="anneal-toolchain-${TARGET}.tar.zst" + MAX_GITHUB_RELEASE_ASSET_SIZE=2147483647 + mkdir -p anneal/v2/target anneal/release-download-check anneal/release-metadata + + nix build ./anneal/v2#omnibus-archive-ci --out-link "anneal/v2/target/${ARCHIVE_NAME}" + cp -L "anneal/v2/target/${ARCHIVE_NAME}" "anneal/${ARCHIVE_NAME}" + ARCHIVE_SIZE="$(python3 -c 'import os, sys; print(os.path.getsize(sys.argv[1]))' "anneal/${ARCHIVE_NAME}")" + printf 'Built %s (%s bytes)\n' "$ARCHIVE_NAME" "$ARCHIVE_SIZE" + if [ "$ARCHIVE_SIZE" -gt "$MAX_GITHUB_RELEASE_ASSET_SIZE" ]; then + echo "::error::${ARCHIVE_NAME} is ${ARCHIVE_SIZE} bytes, which exceeds GitHub's ${MAX_GITHUB_RELEASE_ASSET_SIZE}-byte release asset limit." + exit 1 fi - gh release upload "$TAG" anneal/anneal-toolchain-$TARGET.tar.zst --clobber - finalize-release: - name: Finalize Release - needs: [publish-artifacts, create-release] - if: always() && needs.publish-artifacts.result == 'success' && github.event_name == 'workflow_dispatch' - runs-on: ubuntu-latest - permissions: - contents: write # required to publish the release - steps: - - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + gh release upload "$TAG_NAME" "anneal/${ARCHIVE_NAME}" --repo "$GH_REPO" --clobber + gh release download "$TAG_NAME" \ + --repo "$GH_REPO" \ + --pattern "$ARCHIVE_NAME" \ + --dir anneal/release-download-check \ + --clobber + cmp "anneal/${ARCHIVE_NAME}" "anneal/release-download-check/${ARCHIVE_NAME}" + + url="https://github.com/${GH_REPO}/releases/download/${TAG_NAME}/${ARCHIVE_NAME}" + python3 anneal/tools/collect-release-archive-metadata.py \ + --archive "anneal/release-download-check/${ARCHIVE_NAME}" \ + --target "$TARGET" \ + --os "$CARGO_OS" \ + --arch "$CARGO_ARCH" \ + --url "$url" \ + --out "anneal/release-metadata/${TARGET}.json" + + - name: Restore AppArmor restriction + if: always() && runner.os == 'Linux' + run: sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=1 + + - name: Upload toolchain metadata + uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0 with: - persist-credentials: false - - name: Publish Release - env: - GH_TOKEN: ${{ github.token }} - TAG_NAME: ${{ needs.create-release.outputs.tag_name }} - run: | - gh release edit "$TAG_NAME" --draft=false + name: anneal-toolchain-metadata-${{ matrix.target }} + path: anneal/release-metadata/${{ matrix.target }}.json + if-no-files-found: error + retention-days: 1 release-version-action: # This job handles manual release triggers. It updates version numbers and - # creates a PR for review. It does not perform actual publishing. - name: Release new Anneal versions + # exocrate archive metadata, then creates a PR for review. + name: Release new Anneal version + needs: [prepare-release-source, create-release, publish-artifacts] if: github.event_name == 'workflow_dispatch' permissions: - contents: read + actions: read # Required to download toolchain metadata artifacts. + contents: write # Required by the fork-only create-pull-request fallback. + issues: write # Required to label the generated release PR. pull-requests: write # Required to create pull requests runs-on: ubuntu-latest steps: - name: Checkout code uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 with: - ref: ${{ github.event.inputs.branch }} + ref: ${{ needs.prepare-release-source.outputs.base_sha }} persist-credentials: false - - name: Overwrite Anneal files + + - name: Download release source patch + uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 # v7.0.0 + with: + name: anneal-release-source-patch + path: . + + - name: Apply release source patch + run: | + set -eo pipefail + git apply --check anneal-release-source.patch + git apply anneal-release-source.patch + + - name: Download toolchain metadata + uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 # v7.0.0 + with: + pattern: anneal-toolchain-metadata-* + path: anneal/release-metadata + merge-multiple: true + + - name: Update Anneal archive metadata env: - VERSION: ${{ github.event.inputs.version }} - run: ./ci/release_anneal_version.sh "$VERSION" + TAG_NAME: ${{ needs.create-release.outputs.tag_name }} + run: | + set -eo pipefail + python3 anneal/tools/update-exocrate-metadata.py \ + --cargo-toml anneal/Cargo.toml \ + --metadata-dir anneal/release-metadata \ + --expected-release-tag "$TAG_NAME" \ + --require-all + + rm -f anneal-release-source.patch + rm -rf anneal/release-metadata + + python3 anneal/tools/check-release-pr-files.py \ + --context "Release workflow" \ + --include-untracked \ + --allowed anneal/Cargo.lock \ + --allowed anneal/Cargo.toml \ + --allowed anneal/README.md \ + --required anneal/Cargo.toml - name: Submit PR - id: submit-pr + id: submit-pr-upstream + if: github.repository == 'google/zerocopy' uses: peter-evans/create-pull-request@c0f553fe549906ede9cf27b5156039d195d2ece0 # v8.1.0 # zizmor: ignore[superfluous-actions] with: commit-message: "Release Anneal ${{ github.event.inputs.version }}" author: Google PR Creation Bot committer: Google PR Creation Bot title: "Release Anneal ${{ github.event.inputs.version }}" + base: ${{ github.event.inputs.branch }} branch: anneal-release-${{ github.event.inputs.version }} + add-paths: | + anneal/Cargo.lock + anneal/Cargo.toml + anneal/README.md push-to-fork: google-pr-creation-bot/zerocopy token: ${{ secrets.GOOGLE_PR_CREATION_BOT_TOKEN }} # zizmor: ignore[secrets-outside-env] + - name: Submit PR (fork test) + id: submit-pr-fork + if: github.repository != 'google/zerocopy' + uses: peter-evans/create-pull-request@c0f553fe549906ede9cf27b5156039d195d2ece0 # v8.1.0 # zizmor: ignore[superfluous-actions] + with: + commit-message: "Release Anneal ${{ github.event.inputs.version }}" + author: Google PR Creation Bot + committer: Google PR Creation Bot + title: "Release Anneal ${{ github.event.inputs.version }}" + base: ${{ github.event.inputs.branch }} + branch: anneal-release-${{ github.event.inputs.version }} + add-paths: | + anneal/Cargo.lock + anneal/Cargo.toml + anneal/README.md + token: ${{ github.token }} + - name: Add labels - if: steps.submit-pr.outputs.pull-request-operation == 'created' + if: steps.submit-pr-upstream.outputs.pull-request-operation == 'created' env: GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} - PR_NUMBER: ${{ steps.submit-pr.outputs.pull-request-number }} + PR_NUMBER: ${{ steps.submit-pr-upstream.outputs.pull-request-number }} run: gh pr edit "$PR_NUMBER" --add-label "hide-from-release-notes" + - name: Add labels (fork test) + if: steps.submit-pr-fork.outputs.pull-request-operation == 'created' + env: + GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + PR_NUMBER: ${{ steps.submit-pr-fork.outputs.pull-request-number }} + run: gh pr edit "$PR_NUMBER" --add-label "hide-from-release-notes" diff --git a/.github/workflows/anneal.yml b/.github/workflows/anneal.yml index 6070d766db..5f07ba693d 100644 --- a/.github/workflows/anneal.yml +++ b/.github/workflows/anneal.yml @@ -30,6 +30,44 @@ env: jobs: + static_checks: + name: Anneal Static Checks + runs-on: ubuntu-latest + permissions: + contents: read + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + with: + persist-credentials: false + + - name: Install stable Rust + uses: dtolnay/rust-toolchain@e97e2d8cc328f1b50210efc529dca0028893a2d9 # zizmor: ignore[superfluous-actions] + with: + toolchain: stable + + - name: Test Anneal support scripts + run: | + set -euo pipefail + export PYTHONDONTWRITEBYTECODE=1 + python3 -m py_compile \ + anneal/tools/check-release-pr-files.py \ + anneal/tools/test_exocrate_metadata_helpers.py \ + anneal/tools/test_release_pr_files.py \ + anneal/tools/collect-release-archive-metadata.py \ + anneal/tools/update-exocrate-metadata.py \ + anneal/v2/tests/test_prune_lake_cache.py \ + anneal/v2/prune-lake-cache.py \ + anneal/v2/rewrite-lake-vendor.py + python3 -m unittest discover -s anneal/tools -p 'test_*.py' + python3 -m unittest discover -s anneal/v2/tests -p 'test_*.py' + bash anneal/tools/check-release-flow-dry-run.sh + + - name: Install Nix + uses: DeterminateSystems/determinate-nix-action@441b9e401ac050c38a07d8313748c5c2d17e8aff # v3.6.1 + + - name: Check V2 flake evaluation + run: bash anneal/v2/check-flake-eval.sh + anneal_tests: name: Anneal Tests runs-on: ubuntu-latest @@ -285,6 +323,14 @@ jobs: archive="$(readlink -f target/anneal-exocrate.tar.zst)" rm target/anneal-exocrate.tar.zst cp "$archive" target/anneal-exocrate.tar.zst + archive_size="$(python3 -c 'import os, sys; print(os.path.getsize(sys.argv[1]))' target/anneal-exocrate.tar.zst)" + max_github_release_asset_size=2147483647 + printf 'Built anneal-exocrate.tar.zst (%s bytes)\n' "$archive_size" + if [ "$archive_size" -gt "$max_github_release_asset_size" ]; then + echo "::error::anneal-exocrate.tar.zst is ${archive_size} bytes, which exceeds GitHub's ${max_github_release_asset_size}-byte release asset limit." + exit 1 + fi + nix build "${nix_args[@]}" .#omnibus-archive-layout-check --no-link working-directory: anneal/v2 # Re-enable the AppArmor namespace restriction to restore the runner host's default security posture. @@ -388,7 +434,7 @@ jobs: # https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/collaborating-on-repositories-with-code-quality-features/troubleshooting-required-status-checks#handling-skipped-but-required-checks if: failure() runs-on: ubuntu-latest - needs: [anneal_tests, verify_examples, v2_nix_cache, v2] + needs: [static_checks, anneal_tests, verify_examples, v2_nix_cache, v2] steps: - name: Mark the job as failed run: exit 1 diff --git a/anneal/Cargo.toml b/anneal/Cargo.toml index c20b7da954..2e0d0d370a 100644 --- a/anneal/Cargo.toml +++ b/anneal/Cargo.toml @@ -107,60 +107,6 @@ aeneas_rev = "42c0e90dacf486f7d3ed5b6cde3a9a81f04915a4" # The Lean toolchain version to use. This must match the version of Lean used # by Aeneas in the `lean-toolchain` file in the commit above. lean_toolchain = "leanprover/lean4:v4.30.0-rc2" - -# The Rust toolchain required by Charon. -# -# FIXME(#3165): -# - Roll this from `tools/roll-pinned-prebuilts.py` -# - Auto-install via `rustup` during `cargo anneal setup` -charon_rust_toolchain = "nightly-2026-02-07" - -[package.metadata.anneal.dependencies.aeneas] -# The per-commit release tag from AeneasVerif/charon -tag = "build-2026.04.07.112215-42c0e90dacf486f7d3ed5b6cde3a9a81f04915a4" - -[package.metadata.anneal.dependencies.aeneas.checksums] -linux-aarch64 = "a250ef38be509f69ff4c5fb35eded165255fae6f659172837cd3053978de863f" -linux-x86_64 = "a448682a154590e65b0794c42487583352375fc04bdd6b2418324f6ecafcc94f" -macos-aarch64 = "1dbeaafe875bec173e0d2cf3c6bbfa63d6c591d3ec554bafb0d2c3c52e1ded6d" -macos-x86_64 = "e977c28b72ec041d4f13df0acc77ab59040743a9659b4eefffb71eb420cd5df6" - -[package.metadata.anneal.dependencies.rust] -tag = "nightly-2026-02-07" -date = "2026-02-07" - -[package.metadata.anneal.dependencies.rust.checksums] -linux-x86_64-rustc = "f58a30c9fa9add81d0e99209fd960aa429f0a4ff7a37f9044e5d9eb1a598c925" -linux-x86_64-rust-std = "1b06ef4654bcacd06c4f14094ca9bfe8d8bd4129c96b6b6594e3a9cf0d0214d2" -linux-x86_64-rustc-dev = "7f120343b7153e166261558b07efb8081781cfdd617e5a59ac0e144cbbe9b3df" -linux-x86_64-llvm-tools-preview = "4ca90ae6805121c591bb35998c12c69e6f77f9f7cc93edd72a26dfc017f0c098" -linux-x86_64-miri-preview = "c90b56d0c094d6599f827b5feebb6a105af536b3540924fa373356a38f296d33" -linux-x86_64-cargo = "414e784933c550d7b7c88bbaaa0578609c2c618c9d664ae9a966ce914c54b383" - -linux-aarch64-rustc = "cd781f03a07803fa6048e9848992c88d5b7311a5570e702754b8fc271e780a79" -linux-aarch64-rust-std = "c7e9d1d54ccd6a9426be2de7b1e22d5a6eb4c0e18d0cff5c2dfe5e6a836d1e61" -linux-aarch64-rustc-dev = "552302886c5a3ff8f97d55838efd48ec7876ccfc544f334affa6da59a159fc57" -linux-aarch64-llvm-tools-preview = "1aa7233de3856fb213b7c1927e3d3378b5484a18adbb631bc116ff63fbbb151e" -linux-aarch64-miri-preview = "de65c893bbcf186150204c27de29b408d6bbc59a49b6327119461cefafbc1b42" -linux-aarch64-cargo = "c85804bd8644035d7981b28e3832ac54f7cbcce1e406319b32dff6ca55d0305c" - -macos-x86_64-rustc = "c17ebb6d433fd9cd09b6ca59c2e8c18114e0fd54917997a1b6dcaa1187d0dd23" -macos-x86_64-rust-std = "8d3f34cc047d2daa578615e9ade5b9e80cda2b1a9d14677f1d901d52e840ea35" -macos-x86_64-rustc-dev = "817b2b71d70b07f3f5dfb897b47598b1d64d2d789a71a1250d2123d53262adc5" -macos-x86_64-llvm-tools-preview = "506df88302ff5bb3e652b743ceda9284e7a7fb96fd4c2b3c159a4bdacd815f22" -macos-x86_64-miri-preview = "19f717a65f4c07065b732f43bd14e10303108fc68194e3b7d8d2d574736e4735" -macos-x86_64-cargo = "3ee21dcd2266293458d58c417d3b0aa351bb4d567d20ed15552f992a6f2f3fe5" - -macos-aarch64-rustc = "7f3e916728eaecf5e32ec98a132d21aa677f2f9a9c08527ebbd1025755fda537" -macos-aarch64-rust-std = "888548770827ece8c90fdc8efcb3a3fab0c38823d1f163535aaeec2f325c8001" -macos-aarch64-rustc-dev = "3bed787e9d2b8dc21691bcb33ded3fe9b45f57f46d50fc82c4e2d7c6ea35f519" -macos-aarch64-llvm-tools-preview = "df48a63ebccf2b983b450390908a58e8955bb6d38f8a84ad68dbcef3815aa9c9" -macos-aarch64-miri-preview = "c99b5930e32cdddaa10fb08af3235fec9fede2327b9e4704591bae41c9e329d7" -macos-aarch64-cargo = "6615a0d863d962e2479ce49b3312516abdbdf2403fd3796590cc5823f35d2202" - -rust-src = "404582b3ef31783b3ee390382e149736cc5d49e5b04d4d1ac39d1371a4ddedca" - - [[test]] name = "integration" harness = false diff --git a/anneal/build.rs b/anneal/build.rs index dbbacebd99..19506668b7 100644 --- a/anneal/build.rs +++ b/anneal/build.rs @@ -28,12 +28,7 @@ fn main() { .and_then(|m| m.get("build_rs")) .expect("Cargo.toml must have [package.metadata.build_rs] section"); - // Key in `Cargo.toml` -> Environment variable name - let vars = [ - ("aeneas_rev", "ANNEAL_AENEAS_REV"), - ("lean_toolchain", "ANNEAL_LEAN_TOOLCHAIN"), - ("charon_rust_toolchain", "ANNEAL_CHARON_RUST_TOOLCHAIN"), - ]; + let vars = [("aeneas_rev", "ANNEAL_AENEAS_REV"), ("lean_toolchain", "ANNEAL_LEAN_TOOLCHAIN")]; for (key, env_var) in vars { let value = build_rs_metadata @@ -44,39 +39,6 @@ fn main() { println!("cargo:rustc-env={}={}", env_var, value); } - // Parse [package.metadata.anneal.dependencies] - if let Some(anneal_metadata) = cargo_toml - .get("package") - .and_then(|p| p.get("metadata")) - .and_then(|m| m.get("anneal")) - .and_then(|h| h.get("dependencies")) - .and_then(|d| d.as_table()) - { - for (dep_name, dep_meta) in anneal_metadata { - let dep_upper = dep_name.to_uppercase(); - if let Some(tag) = dep_meta.get("tag").and_then(|t| t.as_str()) { - println!("cargo:rustc-env=ANNEAL_{}_TAG={}", dep_upper, tag); - } - - if let Some(date) = dep_meta.get("date").and_then(|t| t.as_str()) { - println!("cargo:rustc-env=ANNEAL_{}_DATE={}", dep_upper, date); - } - - if let Some(checksums) = dep_meta.get("checksums").and_then(|c| c.as_table()) { - for (platform, checksum) in checksums { - if let Some(hash) = checksum.as_str() { - // Standardize platform name for env var (dashes -> underscores, upper case) - let env_platform = platform.replace('-', "_").to_uppercase(); - println!( - "cargo:rustc-env=ANNEAL_{}_CHECKSUM_{}={}", - dep_upper, env_platform, hash - ); - } - } - } - } - } - if let Some(exocrate_metadata) = cargo_toml .get("package") .and_then(|p| p.get("metadata")) diff --git a/anneal/tools/build-prebuilt.sh b/anneal/tools/build-prebuilt.sh deleted file mode 100755 index 415e9a880e..0000000000 --- a/anneal/tools/build-prebuilt.sh +++ /dev/null @@ -1,150 +0,0 @@ -#!/bin/bash -# Copyright 2026 The Zerocopy Authors -# -# Licensed under the Apache License, Version 2.0 (the "License"); -# you may not use this file except in compliance with the License. -# You may obtain a copy of the License at -# -# https://www.apache.org/licenses/LICENSE-2.0 -# -# Unless required by applicable law or agreed to in writing, software -# distributed under the License is distributed on an "AS IS" BASIS, -# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -# See the License for the specific language governing permissions and -# limitations under the License. - -set -eo pipefail - -# This script builds the precompiled artifacts for the Anneal toolchain. -# It downloads dependencies, pre-compiles the Lean library, and packages the -# artifact for the specified host platform. -# -# It is used in the release workflow and can also be run by developers to -# verify changes locally. - -# Ensure we are in the anneal directory. -cd "$(dirname "$0")/.." - -STAGING_DIR="dist_staging" -if [ -d "$STAGING_DIR" ]; then - chmod -R +w "$STAGING_DIR" -fi -rm -rf "$STAGING_DIR" -mkdir -p "$STAGING_DIR" - -# Extract metadata from Cargo.toml. -# We use sed to parse the TOML file. This is brittle but avoids external -# dependencies like toml-cli. -AENEAS_TAG=$(sed -n 's/^tag = "\(.*\)"/\1/p' Cargo.toml | head -n 1) -RUST_DATE="2026-02-07" -RUST_VERSION="nightly-2026-02-07" - -echo "Detected Aeneas Tag: $AENEAS_TAG" -echo "Detected Rust Date: $RUST_DATE" -echo "Detected Rust Version: $RUST_VERSION" - -HOST_TRIPLE="${1:-x86_64-unknown-linux-gnu}" -echo "Using Host Triple: $HOST_TRIPLE" - -case "$HOST_TRIPLE" in - "x86_64-unknown-linux-gnu") AENEAS_TARGET="linux-x86_64" ;; - "aarch64-unknown-linux-gnu") AENEAS_TARGET="linux-aarch64" ;; - "x86_64-apple-darwin") AENEAS_TARGET="macos-x86_64" ;; - "aarch64-apple-darwin") AENEAS_TARGET="macos-aarch64" ;; - *) echo "Unsupported host triple: $HOST_TRIPLE"; exit 1 ;; -esac - -# Download Aeneas prebuilts. -# We download from the upstream repository to repackage them. -AENEAS_URL="https://github.com/AeneasVerif/aeneas/releases/download/${AENEAS_TAG}/aeneas-${AENEAS_TARGET}.tar.gz" -echo "Downloading Aeneas from $AENEAS_URL..." -curl -L "$AENEAS_URL" -o "$STAGING_DIR/aeneas.tar.gz" - -# Download Rust toolchain components. -# We download specific nightly components required by Charon. -download_rust_component() { - local component=$1 - local url="https://static.rust-lang.org/dist/${RUST_DATE}/${component}-nightly-${HOST_TRIPLE}.tar.gz" - echo "Downloading $component from $url..." - curl -L "$url" -o "$STAGING_DIR/${component}.tar.gz" -} - -download_rust_component "rustc" -download_rust_component "rust-std" -download_rust_component "rustc-dev" -download_rust_component "llvm-tools" -download_rust_component "miri" - -# We also need rust-src which is platform independent. -RUST_SRC_URL="https://static.rust-lang.org/dist/${RUST_DATE}/rust-src-nightly.tar.gz" -echo "Downloading rust-src from $RUST_SRC_URL..." -curl -L "$RUST_SRC_URL" -o "$STAGING_DIR/rust-src.tar.gz" - -# Unpack everything. -echo "Unpacking artifacts..." -cd "$STAGING_DIR" -tar -xzf aeneas.tar.gz - -mkdir -p rust -tar -xzf rustc.tar.gz -C rust --strip-components=2 -tar -xzf rust-std.tar.gz -C rust --strip-components=2 -tar -xzf rustc-dev.tar.gz -C rust --strip-components=2 -tar -xzf llvm-tools.tar.gz -C rust --strip-components=2 -tar -xzf miri.tar.gz -C rust --strip-components=2 -tar -xzf rust-src.tar.gz -C rust --strip-components=2 - -# Move charon and charon-driver to rust/bin to sit alongside rustc -# This allows them to find shared libraries in ../lib relative to themselves. -mv charon charon-driver rust/bin/ - -# Nix preserves read-only permissions from the store, so we must make files -# writable. -chmod -R +w . -cd .. - -# Pre-compile Lean Library. -# We need to make sure we use the correct Lean version and fetch Mathlib cache. -# We assume elan is installed on the system. -echo "Pre-compiling Lean library..." -cd "$STAGING_DIR/backends/lean" - -# Ensure we use the correct Lean version specified by Aeneas. -LEAN_VERSION=$(cat lean-toolchain) -elan default "$LEAN_VERSION" - -# Fetch pre-compiled Mathlib binaries to avoid hours of compilation. -lake exe cache get - -# Force precompilation by unsetting CI environment variable. -# This ensures that shared libraries required for plugin loading are generated. -# Remove tests from AeneasMeta to avoid users compiling them -rm -f AeneasMeta/Async/Test.lean -rm -f AeneasMeta/Async/TestTactics.lean -# Remove imports of these tests from Async.lean -sed '/import AeneasMeta.Async.Test/d' AeneasMeta/Async.lean > AeneasMeta/Async.lean.tmp && mv AeneasMeta/Async.lean.tmp AeneasMeta/Async.lean - -# Remove Mathlib tests to keep the artifact small -rm -rf .lake/packages/mathlib/MathlibTest - -env -u CI lake build - -# Generate the dependency graph -lake exe graph imports.dot --to Aeneas,Aeneas.Std.Core,Aeneas.Std.WP,Aeneas.Tactic.Solver.ScalarTac,Aeneas.Std.Scalar.Core --include-deps - -# Prune Mathlib based on the graph -python3 ../../../tools/prune_mathlib.py imports.dot .lake/packages/mathlib - -# Clean up the graph file -rm imports.dot - -cd ../.. # Back to dist_staging - -# Repackage the artifact. -echo "Repackaging artifact..." -# We remove the original archives before repackaging. -rm -f aeneas.tar.gz rustc.tar.gz rust-std.tar.gz rustc-dev.tar.gz llvm-tools.tar.gz miri.tar.gz rust-src.tar.gz -ZSTD_LEVEL="${ANNEAL_ZSTD_LEVEL:-19}" -tar -cf - * | zstd -"$ZSTD_LEVEL" > ../anneal-toolchain-${AENEAS_TARGET}.tar.zst - -cd .. # Back to anneal directory -echo "Precompiled artifacts built successfully." diff --git a/anneal/tools/check-release-flow-dry-run.sh b/anneal/tools/check-release-flow-dry-run.sh new file mode 100644 index 0000000000..118e4057b2 --- /dev/null +++ b/anneal/tools/check-release-flow-dry-run.sh @@ -0,0 +1,142 @@ +#!/usr/bin/env bash +# +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +set -euo pipefail + +ROOT="$(git rev-parse --show-toplevel)" +TMP_ROOT="$(mktemp -d "${TMPDIR:-/tmp}/anneal-release-dry-run.XXXXXXXX")" +WORKTREE="$TMP_ROOT/worktree" +PATCH="$TMP_ROOT/anneal-release-source.patch" + +cleanup() { + git -C "$ROOT" worktree remove --force "$WORKTREE" >/dev/null 2>&1 || rm -rf "$TMP_ROOT" +} +trap cleanup EXIT + +VERSION="${ANNEAL_RELEASE_DRY_RUN_VERSION:-999.0.0-alpha.0}" +TAG_NAME="anneal-toolchains-v${VERSION}-dry-run" + +git -C "$ROOT" worktree add --detach "$WORKTREE" HEAD >/dev/null +cd "$WORKTREE" + +./ci/release_anneal_version.sh "$VERSION" + +python3 anneal/tools/check-release-pr-files.py \ + --context "Release dry-run version bump" \ + --include-untracked \ + --allowed anneal/Cargo.lock \ + --allowed anneal/Cargo.toml \ + --allowed anneal/README.md \ + --required anneal/Cargo.toml + +git diff --binary > "$PATCH" +if [ ! -s "$PATCH" ]; then + echo "Release dry-run version bump produced an empty patch." >&2 + exit 1 +fi + +git reset --hard HEAD >/dev/null +git clean -fdx >/dev/null +git apply --check "$PATCH" +git apply "$PATCH" + +python3 anneal/tools/check-release-pr-files.py \ + --context "Release dry-run applied source patch" \ + --include-untracked \ + --allowed anneal/Cargo.lock \ + --allowed anneal/Cargo.toml \ + --allowed anneal/README.md \ + --required anneal/Cargo.toml + +mkdir -p anneal/release-metadata +for target in linux-x86_64 linux-aarch64 macos-x86_64 macos-aarch64; do + case "$target" in + linux-x86_64) + cargo_os=linux + cargo_arch=x86_64 + ;; + linux-aarch64) + cargo_os=linux + cargo_arch=aarch64 + ;; + macos-x86_64) + cargo_os=macos + cargo_arch=x86_64 + ;; + macos-aarch64) + cargo_os=macos + cargo_arch=aarch64 + ;; + *) + echo "unexpected release dry-run target: $target" >&2 + exit 1 + ;; + esac + + sha256="$(python3 -c 'import hashlib, sys; print(hashlib.sha256(sys.argv[1].encode()).hexdigest())' "$target")" + url="https://github.com/google/zerocopy/releases/download/${TAG_NAME}/anneal-toolchain-${target}.tar.zst" + cat > "anneal/release-metadata/${target}.json" <, Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +"""Check that release automation only changed expected files.""" + +from __future__ import annotations + +import argparse +import subprocess +from collections.abc import Iterable + + +def parse_porcelain_status_paths(status: str) -> list[str]: + paths = [] + for line in status.splitlines(): + if not line: + continue + path = line[3:] + if " -> " in path: + old, new = path.split(" -> ", 1) + paths.extend([old, new]) + else: + paths.append(path) + return paths + + +def tracked_diff_paths() -> list[str]: + output = subprocess.check_output(["git", "diff", "--name-only"], text=True) + return [line for line in output.splitlines() if line] + + +def working_tree_status_paths() -> list[str]: + output = subprocess.check_output( + ["git", "status", "--porcelain=v1", "--untracked-files=all"], text=True + ) + return parse_porcelain_status_paths(output) + + +def unexpected_paths(paths: Iterable[str], allowed: Iterable[str]) -> list[str]: + return sorted(set(paths) - set(allowed)) + + +def validation_errors(paths: Iterable[str], allowed: Iterable[str], required: Iterable[str]) -> list[str]: + path_set = set(paths) + errors = [] + unexpected = unexpected_paths(path_set, allowed) + if unexpected: + errors.append("Unexpected files changed:\n" + "\n".join(unexpected)) + missing_required = sorted(set(required) - path_set) + if missing_required: + errors.append("Required files were not changed:\n" + "\n".join(missing_required)) + return errors + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--allowed", action="append", default=[], required=True) + parser.add_argument("--required", action="append", default=[]) + parser.add_argument("--include-untracked", action="store_true") + parser.add_argument("--context", default="release workflow") + args = parser.parse_args() + + paths = working_tree_status_paths() if args.include_untracked else tracked_diff_paths() + errors = validation_errors(paths, args.allowed, args.required) + if errors: + print(f"::error::{args.context} changed unexpected files or missed required updates.") + for error in errors: + print(error) + raise SystemExit(1) + + +if __name__ == "__main__": + main() diff --git a/anneal/tools/extract_minimal_toml.py b/anneal/tools/extract_minimal_toml.py deleted file mode 100644 index 9663d058e0..0000000000 --- a/anneal/tools/extract_minimal_toml.py +++ /dev/null @@ -1,41 +0,0 @@ -import json -import tomllib - -def to_toml_inline_table(d): - items = [] - for k, v in d.items(): - items.append(f"{k} = {json.dumps(v)}") - return "{ " + ", ".join(items) + " }" - -with open("Cargo.toml", "rb") as f: - data = tomllib.load(f) - -print("[package]") -print(f'name = {json.dumps(data["package"]["name"])}') -print(f'version = {json.dumps(data["package"]["version"])}') -print(f'edition = {json.dumps(data["package"]["edition"])}') - -deps = data["dependencies"] -print("[dependencies]") -for dep in ["anyhow", "flate2", "sha2", "tar", "fs2", "log", "reqwest", "dirs"]: - val = deps[dep] - if isinstance(val, dict): - print(f"{dep} = {to_toml_inline_table(val)}") - else: - print(f"{dep} = {json.dumps(val)}") - -print("[build-dependencies]") -print(f'toml = {json.dumps(data["build-dependencies"]["toml"])}') - -print("[package.metadata.build_rs]") -for k, v in data["package"]["metadata"]["build_rs"].items(): - print(f"{k} = {json.dumps(v)}") - -print("[package.metadata.anneal.dependencies.aeneas]") -for k, v in data["package"]["metadata"]["anneal"]["dependencies"]["aeneas"].items(): - if k != "checksums": - print(f"{k} = {json.dumps(v)}") - -print("[package.metadata.anneal.dependencies.aeneas.checksums]") -for k, v in data["package"]["metadata"]["anneal"]["dependencies"]["aeneas"]["checksums"].items(): - print(f"{k} = {json.dumps(v)}") diff --git a/anneal/tools/roll-pinned-prebuilts.py b/anneal/tools/roll-pinned-prebuilts.py deleted file mode 100755 index e633012e4c..0000000000 --- a/anneal/tools/roll-pinned-prebuilts.py +++ /dev/null @@ -1,474 +0,0 @@ -#!/usr/bin/env python3 - -import requests -import json -import os -import hashlib -import tarfile -import tempfile -import sys -import argparse -import subprocess -import platform -import re -import stat -from datetime import datetime, timedelta -from pathlib import Path -import tomlkit -from requests.exceptions import RequestException - - -class CompatibilityError(Exception): - """Raised when a release is found but is not compatible with our requirements.""" - pass - -# Default timeout for all network requests in seconds. -DEFAULT_TIMEOUT = 30 - -# Configuration for the Aeneas and Charon repositories. These are used to discover -# releases and fetch metadata from the AeneasVerif organization on GitHub. -AENEAS_REPO = "AeneasVerif/aeneas" -CHARON_REPO = "AeneasVerif/charon" - -# The set of platforms that Anneal supports for pre-built binaries. The script -# will download and checksum artifacts for each of these triples. -PLATFORMS = ["linux-x86_64", "linux-aarch64", "macos-aarch64", "macos-x86_64"] - -# Path to the Cargo.toml file where toolchain metadata is stored. This is -# resolved relative to the script's location to allow invocation from anywhere in -# the repository. -CARGO_TOML_PATH = (Path(__file__).parent.parent / "Cargo.toml").resolve() - - -def github_get(url): - """Performs an authenticated GET request to the GitHub API if a token is present. - - This function automatically uses the 'GITHUB_TOKEN' environment variable if - set to avoid API rate limits. It also enforces a standard timeout. - """ - headers = {} - token = os.environ.get("GITHUB_TOKEN") - if token: - headers["Authorization"] = f"token {token}" - - try: - response = requests.get(url, headers=headers, timeout=DEFAULT_TIMEOUT) - response.raise_for_status() - return response - except RequestException as e: - print(f"ERROR: GitHub request failed: {url}") - print(f" {e}") - sys.exit(1) - - -def get_automated_releases(repo): - """Fetches automated build releases from the GitHub API. - - This function assumes that releases representing automated CI builds are - prefixed with 'build-'. It fetches the first 100 releases to ensure we have - enough history to find compatible pairs. - """ - url = f"https://api.github.com/repos/{repo}/releases?per_page=100" - response = github_get(url) - return [r for r in response.json() if r["tag_name"].startswith("build-")] - - -def get_release_by_tag(repo, tag): - """Fetches metadata for a specific release identified by a tag. - - This is used when a user provides an explicit tag override, bypassing the - automated discovery logic. - """ - url = f"https://api.github.com/repos/{repo}/releases/tags/{tag}" - response = github_get(url) - return response.json() - - -def release_has_assets(release, repo_name): - """Returns True if the release contains all expected assets for our platforms.""" - repo_slug = repo_name.split("/")[-1] - asset_names = {a["name"] for a in release.get("assets", [])} - for platform in PLATFORMS: - expected_asset = f"{repo_slug}-{platform}.tar.gz" - if expected_asset not in asset_names: - return False - return True - - -def get_commit_from_tag(tag): - """Extracts the git commit hash from a build tag. - - This function assumes the tag follows the 'build-YYYY.MM.DD.HHMMSS-' - format used by the AeneasVerif automated build infrastructure. - """ - return tag.split("-")[-1] - - -def fetch_file_content(repo, commit, path): - """Returns the text content of a file from human-readable GitHub raw URLs. - - If the file does not exist (404), this returns None instead of raising an - error, allowing caller logic to try fallback paths. - """ - url = f"https://raw.githubusercontent.com/{repo}/{commit}/{path}" - try: - response = requests.get(url, timeout=DEFAULT_TIMEOUT) - if response.status_code == 404: - return None - response.raise_for_status() - return response.text - except RequestException as e: - print(f"ERROR: Failed to fetch file content: {url}") - print(f" {e}") - sys.exit(1) - - -def get_charon_pin(aeneas_commit): - """Discovers the Charon commit pinned by a specific Aeneas version (in the `charon-pin` file).""" - content = fetch_file_content(AENEAS_REPO, aeneas_commit, "charon-pin") - if content: - for line in content.splitlines(): - line = line.strip() - if line and not line.startswith("#"): - return line - return None - - -def calculate_sha256(data): - return hashlib.sha256(data).hexdigest() - - -def get_host_platform(): - """Detects the current host platform in the format used by Anneal.""" - system = platform.system().lower() - machine = platform.machine().lower() - - if system == "linux": - if machine == "x86_64": - return "linux-x86_64" - elif machine in ["aarch64", "arm64"]: - return "linux-aarch64" - elif system == "darwin": - if machine in ["arm64", "aarch64"]: - return "macos-aarch64" - elif machine == "x86_64": - return "macos-x86_64" - return None - - -def get_asset_checksums(release, repo_name): - """Downloads all platform archives and calculates required checksums. - - Anneal requires two levels of verification: - 1. The checksum of the downloaded '.tar.gz' archive itself. - 2. The checksum of the primary binaries contained within the archive (e.g., - 'aeneas', 'charon'). - - The latter allows Anneal to detect and repair corruption of individual - binaries in a local toolchain installation. - - Also extracts the `charon` binary for the host platform to query the - Rust toolchain version it was built against. - """ - checksums = {} - host_platform = get_host_platform() - if host_platform is None: - print(f"ERROR: Unsupported host platform: {platform.system()} {platform.machine()}") - sys.exit(1) - - charon_rust_toolchain = None - - with tempfile.TemporaryDirectory() as tmp_dir: - tmp_path = Path(tmp_dir) - for platform in PLATFORMS: - asset_name = f"{repo_name.split('/')[-1]}-{platform}.tar.gz" - asset = next( - (a for a in release["assets"] if a["name"] == asset_name), None - ) - if not asset: - print( - f"Warning: Asset {asset_name} not found in release {release['tag_name']}" - ) - continue - - print(f" Downloading {asset_name}...") - try: - resp = requests.get( - asset["browser_download_url"], timeout=DEFAULT_TIMEOUT - ) - resp.raise_for_status() - data = resp.content - except RequestException as e: - raise CompatibilityError(f"Failed to download asset {asset_name}: {e}") - - checksums[platform] = calculate_sha256(data) - - # Write to a temporary file to allow processing with tarfile. - archive_path = tmp_path / asset_name - archive_path.write_bytes(data) - - try: - with tarfile.open(archive_path, "r:gz") as tar: - found_binaries = set() - for member in tar.getmembers(): - # We extract and checksum only the primary binaries that - # Anneal needs to verify individually. - name = Path(member.name).name - if name in ["charon", "charon-driver", "aeneas"]: - f = tar.extractfile(member) - if f is None: - print( - f"Warning: Could not extract {name} from {asset_name} (likely not a regular file)" - ) - continue - binary_data = f.read() - checksums[f"{platform}-{name}"] = calculate_sha256( - binary_data - ) - found_binaries.add(name) - - # If this is charon on the host platform, extract it to disk to query its rustc version. - if platform == host_platform and name in ["charon", "charon-driver"]: - bin_path = tmp_path / name - bin_path.write_bytes(binary_data) - bin_path.chmod(bin_path.stat().st_mode | stat.S_IEXEC) - - # Now that all binaries are extracted for the host platform, run charon. - if platform == host_platform: - charon_bin_path = tmp_path / "charon" - if charon_bin_path.exists(): - try: - print(" Querying charon rustc version...") - # charon internally calls charon-driver, so they must both be extracted. - # Add the temp directory to PATH so charon can find charon-driver - env = os.environ.copy() - env["PATH"] = f"{tmp_path}:{env.get('PATH', '')}" - result = subprocess.run( - [str(charon_bin_path), "rustc", "--", "--version"], - capture_output=True, - text=True, - env=env - ) - if result.returncode != 0: - # It might fail because rustc is not actually installed correctly, - # or because of some missing library, but charon might still print - # its version to stderr or stdout before failing. - pass - version_output = result.stdout.strip() or result.stderr.strip() - match = re.search(r'rustc .* \(.* (\d{4}-\d{2}-\d{2})\)', version_output) - if not match: - raise CompatibilityError( - f"Could not parse rustc version from charon output: '{version_output}'" - ) - date_str = match.group(1) - date_obj = datetime.strptime(date_str, "%Y-%m-%d") - toolchain_date = date_obj + timedelta(days=1) - charon_rust_toolchain = f"nightly-{toolchain_date.strftime('%Y-%m-%d')}" - print(f" Found Charon Rust toolchain: {charon_rust_toolchain}") - except subprocess.CalledProcessError as e: - raise CompatibilityError(f"Failed to execute charon to get rustc version: {e}") - except FileNotFoundError as e: - raise CompatibilityError(f"Failed to execute charon to get rustc version: {e}") - - # Verify that we found the expected binaries for this repo. - expected = ["aeneas", "charon", "charon-driver"] - missing = [b for b in expected if b not in found_binaries] - if missing: - raise CompatibilityError( - f"Release {release['tag_name']} for {platform} is missing expected binaries: {', '.join(missing)}" - ) - - # Copy the verified archive into our testdata directory for offline mock tests. - # This ensures that our integration tests always validate against the exact - # physical payload expected by Cargo.toml. - import shutil - testdata_dir = Path(__file__).parent.parent / "testdata" / "setup" - testdata_dir.mkdir(parents=True, exist_ok=True) - shutil.copy2(archive_path, testdata_dir / asset_name) - - except tarfile.TarError as e: - raise CompatibilityError(f"Failed to extract archive {asset_name}: {e}") - - if charon_rust_toolchain is None: - raise CompatibilityError( - f"Could not find charon binary for host platform {host_platform} in releases." - ) - - return checksums, charon_rust_toolchain - - -def update_cargo_toml(aeneas_meta, charon_meta, dry_run=False): - """Writes the updated toolchain metadata to Anneal's Cargo.toml. - - This function uses tomlkit to parse and modify the document, which ensures - that all existing comments and formatting in the original file are - preserved. - """ - if not CARGO_TOML_PATH.exists(): - print(f"ERROR: Cargo.toml not found at {CARGO_TOML_PATH}") - sys.exit(1) - - if dry_run: - print("\n[DRY RUN] Would update Cargo.toml with:") - print(f" Aeneas Tag: {aeneas_meta['tag']}") - print(f" Lean Toolchain: {aeneas_meta['lean_toolchain']}") - print(f" Charon Version: {charon_meta['version']}") - print(f" Charon Rust Toolchain: {charon_meta['rust_toolchain']}") - return - - print(f"Updating {CARGO_TOML_PATH}...") - try: - content = CARGO_TOML_PATH.read_text() - doc = tomlkit.parse(content) - except Exception as e: - print(f"ERROR: Failed to parse Cargo.toml: {e}") - sys.exit(1) - - try: - metadata = doc["package"]["metadata"] - - # Update the build_rs section, which defines the environment variables - # injected into the Anneal build process. - metadata["build_rs"]["aeneas_rev"] = aeneas_meta["commit"] - metadata["build_rs"]["lean_toolchain"] = aeneas_meta["lean_toolchain"] - metadata["build_rs"]["charon_version"] = charon_meta["version"] - metadata["build_rs"]["charon_rust_toolchain"] = charon_meta["rust_toolchain"] - - # Update the anneal.dependencies section, which defines the download URLs - # and checksums used by the 'cargo anneal setup' command. - deps = metadata["anneal"]["dependencies"] - - # Remove separate Charon metadata if it exists. - if "charon" in deps: - del deps["charon"] - - # Update Aeneas metadata. - deps["aeneas"]["tag"] = aeneas_meta["tag"] - deps["aeneas"]["checksums"] = tomlkit.table() - for k, v in sorted(aeneas_meta["checksums"].items()): - deps["aeneas"]["checksums"][k] = v - except KeyError as e: - print(f"ERROR: Cargo.toml missing expected metadata section: {e}") - sys.exit(1) - - try: - CARGO_TOML_PATH.write_text(tomlkit.dumps(doc)) - except Exception as e: - print(f"ERROR: Failed to write to Cargo.toml: {e}") - sys.exit(1) - - -def main(): - parser = argparse.ArgumentParser( - description="Roll Aeneas and Charon toolchain versions in Cargo.toml" - ) - parser.add_argument( - "--aeneas-tag", help="Force a specific Aeneas tag (skips discovery)" - ) - parser.add_argument( - "--charon-tag", help="Force a specific Charon tag (skips discovery)" - ) - parser.add_argument( - "--dry-run", action="store_true", help="Don't write to Cargo.toml" - ) - args = parser.parse_args() - - target_aeneas_release = None - - if args.aeneas_tag and args.charon_tag: - print(f"Using forced tags: Aeneas={args.aeneas_tag}, Charon={args.charon_tag}") - target_aeneas_release = get_release_by_tag(AENEAS_REPO, args.aeneas_tag) - a_commit = get_commit_from_tag(args.aeneas_tag) - lean_toolchain = fetch_file_content(AENEAS_REPO, a_commit, "backends/lean/lean-toolchain") - if lean_toolchain: - lean_toolchain = lean_toolchain.strip() - print(f" Fetching checksums from Aeneas artifact...") - a_checksums, charon_rust_toolchain = get_asset_checksums(target_aeneas_release, AENEAS_REPO) - target_aeneas_meta = { - "tag": args.aeneas_tag, - "commit": a_commit, - "lean_toolchain": lean_toolchain, - "checksums": a_checksums, - "version": args.charon_tag, - "charon_rust_toolchain": charon_rust_toolchain, - } - else: - print("Fetching releases from GitHub...") - aeneas_releases = get_automated_releases(AENEAS_REPO) - - print("Searching for the latest stable Aeneas release...") - target_aeneas_release = None - target_aeneas_meta = None - - for a_rel in aeneas_releases: - a_tag = a_rel["tag_name"] - if a_tag.startswith("build-"): - if args.aeneas_tag and a_tag != args.aeneas_tag: - continue - - if not release_has_assets(a_rel, AENEAS_REPO): - print(f"Skipping {a_tag}: missing prebuilt assets.") - continue - - a_commit = get_commit_from_tag(a_tag) - c_commit = get_charon_pin(a_commit) - - if not c_commit: - print(f"Skipping {a_tag}: could not find charon-pin file.") - continue - - # We still need to fetch the Charon version pinned by Aeneas to update - # Cargo.toml accurately. This ensures Anneal knows which LLBC format it - # expects. - print(f"Checking {a_tag}...") - charon_cargo = fetch_file_content(CHARON_REPO, c_commit, "charon/Cargo.toml") - charon_version = tomlkit.parse(charon_cargo)["package"]["version"] - - # Fetch additional metadata required for the Anneal build process and the - # 'setup' command. - lean_toolchain = fetch_file_content( - AENEAS_REPO, a_commit, "backends/lean/lean-toolchain" - ) - if not lean_toolchain: - print(f"Skipping {a_tag}: missing lean-toolchain.") - continue - lean_toolchain = lean_toolchain.strip() - - print(f" Fetching checksums from Aeneas artifact...") - try: - a_checksums, charon_rust_toolchain = get_asset_checksums(a_rel, AENEAS_REPO) - except CompatibilityError as e: - print(f" Skipping {a_tag}: {e}") - continue - - target_aeneas_release = a_rel - target_aeneas_meta = { - "tag": a_tag, - "commit": a_commit, - "lean_toolchain": lean_toolchain, - "checksums": a_checksums, - "version": charon_version, - "charon_rust_toolchain": charon_rust_toolchain, - } - break - - if not target_aeneas_release: - print("\nERROR: Could not find a suitable Aeneas release.") - sys.exit(1) - - print(f"\nTargeting:") - print(f" Aeneas Tag: {target_aeneas_meta['tag']}") - print(f" Charon Version: {target_aeneas_meta['version']}") - print(f" Charon Rust Toolchain: {target_aeneas_meta['charon_rust_toolchain']}") - - charon_meta = { - "version": target_aeneas_meta["version"], - "rust_toolchain": target_aeneas_meta["charon_rust_toolchain"], - } - update_cargo_toml(target_aeneas_meta, charon_meta, dry_run=args.dry_run) - if not args.dry_run: - print("\nSuccessfully rolled toolchain updates!") - - -if __name__ == "__main__": - main() diff --git a/anneal/tools/test_release_pr_files.py b/anneal/tools/test_release_pr_files.py new file mode 100644 index 0000000000..9f261c51bc --- /dev/null +++ b/anneal/tools/test_release_pr_files.py @@ -0,0 +1,47 @@ +#!/usr/bin/env python3 +# +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +"""Unit tests for check-release-pr-files.py.""" + +from __future__ import annotations + +import importlib.util +import unittest +from pathlib import Path + + +SCRIPT = Path(__file__).resolve().parent / "check-release-pr-files.py" +SPEC = importlib.util.spec_from_file_location("check_release_pr_files", SCRIPT) +assert SPEC is not None and SPEC.loader is not None +check_release_pr_files = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(check_release_pr_files) + + +class ReleasePrFileTests(unittest.TestCase): + def test_porcelain_status_paths_include_untracked_and_renames(self) -> None: + status = " M anneal/Cargo.toml\n?? anneal/release-metadata/linux.json\nR old/path -> anneal/README.md\n" + self.assertEqual( + check_release_pr_files.parse_porcelain_status_paths(status), + ["anneal/Cargo.toml", "anneal/release-metadata/linux.json", "old/path", "anneal/README.md"], + ) + + def test_validation_catches_unexpected_and_missing_files(self) -> None: + errors = check_release_pr_files.validation_errors( + ["anneal/Cargo.toml", "anneal/release-metadata/linux.json"], + ["anneal/Cargo.toml", "anneal/Cargo.lock", "anneal/README.md"], + ["anneal/Cargo.toml", "anneal/README.md"], + ) + self.assertEqual(len(errors), 2) + self.assertIn("anneal/release-metadata/linux.json", errors[0]) + self.assertIn("anneal/README.md", errors[1]) + + +if __name__ == "__main__": + unittest.main() diff --git a/ci/release_anneal_version.sh b/ci/release_anneal_version.sh index 2cbbb8b2c0..f28d0ef285 100755 --- a/ci/release_anneal_version.sh +++ b/ci/release_anneal_version.sh @@ -28,6 +28,8 @@ sed -i -e "s/cargo install cargo-anneal@[0-9a-zA-Z\.-]*/cargo install cargo-anne # Update Cargo.lock to reflect the version change in Cargo.toml. We must run # this in the anneal subdirectory because it is a separate workspace with its -# own lockfile. +# own lockfile. Use `cargo update` on the local package itself instead of +# regenerating the entire lockfile; the release version bump should not also +# roll dependency versions. cd anneal -cargo generate-lockfile +cargo update -p cargo-anneal --precise "$VERSION"