hardware-rust-crypto 1.0.1

name: Build proof image

# Builds the pinned F* / hax toolchain into a container image on GHCR, so the
# release gate (fstar.yml) runs the proof inside it - no from-source build or
# network at release time. Rebuild ON PURPOSE: bump a pin in
# .github/docker/fstar-proof.Dockerfile (and IMAGE_TAG below + the container ref
# in fstar.yml), then run this workflow.
on:
  workflow_dispatch:
  push:
    branches: [main]
    paths:
      - ".github/docker/fstar-proof.Dockerfile"
      - ".github/workflows/proof-image.yml"
  # Rebuild when a PR changes the image definition (e.g. advancing a pin), so the
  # change is validated and the new tag is available before merge.
  pull_request:
    paths:
      - ".github/docker/fstar-proof.Dockerfile"
      - ".github/workflows/proof-image.yml"

permissions:
  contents: read
  packages: write

env:
  # Advance in lockstep with the Dockerfile ARGs and the fstar.yml container ref.
  IMAGE_TAG: hax-a914ac7-fstar-v2026.03.24

jobs:
  build:
    name: build + push fstar-proof image
    runs-on: ubuntu-24.04
    steps:
      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
      - name: Log in to GHCR
        run: echo "${{ secrets.GITHUB_TOKEN }}" | docker login ghcr.io -u "${{ github.actor }}" --password-stdin
      - name: Build and push
        run: |
          set -euo pipefail
          img="ghcr.io/${{ github.repository }}/fstar-proof"
          img="${img,,}"   # GHCR requires a lowercase image path
          echo "image: $img:${IMAGE_TAG}"
          # The Dockerfile pulls everything itself (no COPY), so the build context
          # is just the docker dir - keeps it tiny.
          docker build \
            -f .github/docker/fstar-proof.Dockerfile \
            -t "$img:${IMAGE_TAG}" -t "$img:latest" \
            .github/docker
          docker push "$img:${IMAGE_TAG}"
          docker push "$img:latest"