diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index a3fe744..8a2adff 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -59,13 +59,18 @@ ENV PATH=/home/vscode/.nix-profile/bin:/home/vscode/.npm-global/bin:$PATH # - gh → GitHub CLI for PRs/issues/auth; global so it's usable # from anywhere. Auth is persisted across rebuilds via a # named volume on ~/.config/gh (see devcontainer.json). +# - cachix → required by scripts/deploy.sh `nix-cache` to push the +# build closure to the k-framework cache. kup (the other +# half of that deploy step) is fetched via nix at run +# time, so only cachix needs provisioning here. RUN . /home/vscode/.nix-profile/etc/profile.d/nix.sh \ && nix registry add nixpkgs github:NixOS/nixpkgs/nixos-25.05 \ && nix profile install \ nixpkgs#direnv \ nixpkgs#nix-direnv \ nixpkgs#nodejs_22 \ - nixpkgs#gh + nixpkgs#gh \ + nixpkgs#cachix # Claude Code CLI — installed to a per-user prefix so root isn't required. RUN . /home/vscode/.nix-profile/etc/profile.d/nix.sh \ diff --git a/.devcontainer/devcontainer-lock.json b/.devcontainer/devcontainer-lock.json new file mode 100644 index 0000000..5c99099 --- /dev/null +++ b/.devcontainer/devcontainer-lock.json @@ -0,0 +1,9 @@ +{ + "features": { + "ghcr.io/devcontainers/features/docker-in-docker:2": { + "version": "2.17.0", + "resolved": "ghcr.io/devcontainers/features/docker-in-docker@sha256:25b9f05705ffba7dbe503230ac76081419306f8c8bc88e0ce78c4ecd99a0c78c", + "integrity": "sha256:25b9f05705ffba7dbe503230ac76081419306f8c8bc88e0ce78c4ecd99a0c78c" + } + } +} diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 8dd1c06..3605b7e 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -3,6 +3,13 @@ "build": { "dockerfile": "Dockerfile" }, + // An isolated Docker daemon inside the container, so `scripts/deploy.sh docker` + // can build and push the release image without touching the host's Docker. The + // feature adds the docker CLI, runs dockerd, and puts `vscode` in the docker + // group; it also marks the container privileged, which dockerd requires. + "features": { + "ghcr.io/devcontainers/features/docker-in-docker:2": {} + }, "remoteUser": "vscode", "workspaceFolder": "/workspace", "workspaceMount": "source=${localWorkspaceFolder},target=/workspace,type=bind", diff --git a/.dockerignore b/.dockerignore index 4ab3cf6..e027727 100644 --- a/.dockerignore +++ b/.dockerignore @@ -15,3 +15,16 @@ cov-* result result-* state.kore + +# Never ship local secrets. The build context is the whole repo, and the +# Dockerfile does `COPY . komet-node`, so any credential file sitting here +# would be baked into a published image layer (a later `rm` does not remove +# it from history). deploy.sh is run by hand with tokens exported, often via a +# direnv `.envrc` or a `.env`, so keep those and any key/token files out. +.envrc +.env +.env.* +*.pem +*.key +*.token +secrets* diff --git a/.github/scripts/check-cachix-pin.sh b/.github/scripts/check-cachix-pin.sh index 936c66e..48d73d8 100755 --- a/.github/scripts/check-cachix-pin.sh +++ b/.github/scripts/check-cachix-pin.sh @@ -2,7 +2,7 @@ set -euo pipefail # Verifies that `kup publish` actually pushed AND pinned komet-node in the -# private k-framework-binary cache. Cachix has intermittently dropped the +# k-framework-binary cache. Cachix has intermittently dropped the # `cachix pin` requests kup makes under the hood, so we confirm both the pin # (visible via the pin API) and the narinfo (the pushed store path) before # treating the publish as successful. diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 62759bd..7860a35 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -40,38 +40,16 @@ jobs: ref: ${{ github.sha }} fetch-depth: 0 - # Build the komet-node derivation once, then push it to both the public - # k-framework cache (full build closure, via `cachix push`) and the - # private k-framework-binary cache (the kup-installable binary, via - # `kup publish`). Both pushes reuse the build output already present in - # this runner's Nix store, so the derivation is never built twice. + # The build-and-publish logic lives in scripts/deploy.sh so CI and manual + # deployments stay in sync (single source of truth). See CONTRIBUTING.md. - name: 'Build and publish komet-node to both Nix caches' shell: bash env: - GC_DONT_GC: '1' - # Enable flakes for every nix invocation in this step (the initial - # build, the kup build, and the builds kup runs internally) so the - # job does not depend on flakes being globally enabled on the runner. - NIX_CONFIG: 'extra-experimental-features = nix-command flakes' CACHIX_PUBLIC_TOKEN: '${{ secrets.CACHIX_PUBLIC_TOKEN }}' CACHIX_PRIVATE_KFB_TOKEN: '${{ secrets.CACHIX_PRIVATE_KFB_TOKEN }}' OWNER_REPO: '${{ github.repository }}' REV: '${{ github.sha }}' - run: | - KOMET_NODE=$(nix build .#komet-node --no-link --print-out-paths) - DRV=$(nix-store --query --deriver "${KOMET_NODE}") - - # Push the full build closure to the public k-framework cache. - export CACHIX_AUTH_TOKEN="${CACHIX_PUBLIC_TOKEN}" - nix-store --query --requisites --include-outputs "${DRV}" | cachix push k-framework - - # Publish the binary to the private k-framework-binary cache. kup - # reuses the store paths built above. - export CACHIX_AUTH_TOKEN="${CACHIX_PRIVATE_KFB_TOKEN}" - export PATH="$(nix build github:runtimeverification/kup --no-link --print-out-paths)/bin:$PATH" - kup publish k-framework-binary .#komet-node --keep-days 180 - # Cachix has not been responding to 'cachix pin' requests made under the hood by kup. Verify the push and pin manually. - bash .github/scripts/check-cachix-pin.sh + run: ./scripts/deploy.sh nix-cache - name: 'On failure, delete drafted release' if: failure() @@ -96,32 +74,12 @@ jobs: ref: ${{ github.sha }} fetch-depth: 0 - - name: 'Set environment' - run: | - KOMET_NODE_VERSION=$(cat package/version) - TAG=runtimeverificationinc/komet-node:ubuntu-jammy-${KOMET_NODE_VERSION} - echo "TAG=${TAG}" >> ${GITHUB_ENV} - - - name: 'Build Docker image' - run: | - K_VERSION=$(cat deps/k_release) - docker build . --no-cache --tag ${TAG} --build-arg K_VERSION=${K_VERSION} - - - name: 'Run Docker image' - run: docker run --rm ${TAG} komet-node --help - - - name: 'Push Docker image to Docker Hub' + # Build, smoke-test, and push logic lives in scripts/deploy.sh so CI and + # manual deployments stay in sync (single source of truth). See CONTRIBUTING.md. + - name: 'Build, test, and push Docker image to Docker Hub' env: - DOCKERHUB_USERNAME: rvdockerhub DOCKERHUB_PASSWORD: ${{ secrets.DOCKERHUB_PASSWORD }} - DOCKERHUB_NAMESPACE: runtimeverificationinc - DOCKERHUB_REPO: komet-node - run: | - # Log in to Docker Hub - echo "${DOCKERHUB_PASSWORD}" | docker login --username "${DOCKERHUB_USERNAME}" --password-stdin - - # Push the image - docker image push ${TAG} + run: ./scripts/deploy.sh docker - name: 'On failure, delete drafted release' if: failure() diff --git a/.gitignore b/.gitignore index 6caff64..2a43feb 100644 --- a/.gitignore +++ b/.gitignore @@ -2,6 +2,7 @@ __pycache__/ .coverage .direnv/ +.env # Runtime artifacts written by the server / interpreter in the io dir metadata.json diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 0000000..5976a91 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,143 @@ +# Contributing to Komet Node + +## Development environment + +This repository ships a [devcontainer](.devcontainer/) that provisions the full +toolchain (Nix, the flake's `nix develop` shell, the Claude Code CLI, and the +GitHub CLI). Open the repo in a devcontainer-aware editor and everything below is +available out of the box. + +## Using the GitHub CLI (`gh`) + +`gh` is preinstalled in the devcontainer for creating pull requests, reviewing +issues, and other GitHub tasks from the terminal. + +### Authenticating + +Authenticate once with a personal access token: + +```bash +gh auth login +``` + +Choose **GitHub.com** → **HTTPS** → **Paste an authentication token** when +prompted, then paste the token you create below. + +Your credentials are stored in `~/.config/gh` inside the container, which is +backed by a named volume. This means **your token survives container rebuilds** — +you only need to authenticate once, not every time the container is recreated. + +To check or reset your authentication at any time: + +```bash +gh auth status # show the current login +gh auth logout # remove stored credentials +``` + +### Creating a token with minimal permissions + +Create a **fine-grained** personal access token at **GitHub → Settings → Developer +settings → [Fine-grained personal access tokens](https://github.com/settings/personal-access-tokens/new)** +with the least privilege for your work: + +- **Repository access** → *Only select repositories* → `runtimeverification/komet-node` +- **Contents** → *Read and write* +- **Pull requests** → *Read and write* +- **Issues** → *Read and write* (only if you triage issues) + +`Metadata → Read` is selected automatically; leave everything else at *No access*. + +## Signing commits + +To sign commits made with `git`, add an SSH or GPG key of type **Signing key** to +your GitHub account. + +> [!WARNING] +> Never place an SSH key registered as an **Authentication key** in the container. +> An authentication key grants full account-wide git access and would bypass the +> minimal permissions of your fine-grained PAT. Use a **signing-only** key here. + +## Deploying a release + +`scripts/deploy.sh` builds and publishes the komet-node release artifacts. It is +the single source of truth for the deployment steps: the `Release` workflow +(`.github/workflows/release.yml`) invokes its subcommands, and you run the same +subcommands by hand when CI is unavailable. + +### What it does + +The script has three subcommands: + +| Subcommand | Action | +| ----------- | ------ | +| `nix-cache` | Builds `.#komet-node`, pushes the full build closure to the `k-framework` Cachix cache, publishes the kup-installable binary to the `k-framework-binary` cache, then verifies the push and pin. Both caches are public; `binary` is a historical name, not an access level. | +| `docker` | Builds the runtime image from `Dockerfile`, runs `komet-node --help` in it as a smoke test, then pushes it to Docker Hub. | +| `all` | Runs `nix-cache` then `docker`. | + +The image tag is `runtimeverificationinc/komet-node:ubuntu-jammy-`, +where `` comes from `package/version`. + +### Prerequisites + +Both subcommands run from a checkout of the revision you are releasing, with the +following tools on `PATH`: + +- `nix-cache` needs `nix` and `cachix`. It fetches `kup` from + `github:runtimeverification/kup` itself, so you do not install kup separately. +- `docker` needs `docker`. + +Each subcommand checks its tools up front and exits with a clear message if one +is missing, before starting the build. + +The devcontainer provides all of these: `nix` and `cachix` are installed into the +Nix profile, and the docker-in-docker feature supplies `docker`. If you added +these to an existing container, rebuild it ("Dev Containers: Rebuild Container") +so the new tools are present. + +Provide the secrets as environment variables. Everything else has a default (see +the `Shared configuration` block in `deploy.sh`), so a normal checkout needs no +further setup. + +| Subcommand | Required environment variables | +| ----------- | ------------------------------ | +| `nix-cache` | `CACHIX_PUBLIC_TOKEN`, `CACHIX_PRIVATE_KFB_TOKEN` | +| `docker` | `DOCKERHUB_PASSWORD` | + +`OWNER_REPO` and `REV` default to the current checkout's `origin` remote and +`HEAD`. Override them if you are publishing a revision other than the one checked +out. `DOCKERHUB_USERNAME`, `DOCKERHUB_NAMESPACE`, and `DOCKERHUB_REPO` default to +the release account and repository; override them only to publish elsewhere. + +Both subcommands refuse to run if the working tree is not clean. CI builds from a +fresh checkout, so a manual build must too: uncommitted changes and untracked +files would otherwise be baked into the published image or flake build without +matching the `REV` they are published under. Commit, stash, or clean the tree +first. `git status --porcelain` ignores `.gitignore`d paths, so runtime artifacts +and dev caches do not count. Set `ALLOW_DIRTY=1` to override the check when you +deliberately want to publish an uncommitted state. + +### Manual release while CI is down + +The workflow also drafts, cleans up, and finalizes the GitHub release around the +deployment jobs. When you deploy by hand, run those `gh` steps yourself in this +order. `nix-cache` runs once per architecture (the workflow uses an `x86_64` and +an `ARM64` runner), so run it on a machine of each architecture that should be +cached. + +```sh +VERSION=v$(cat package/version) + +# 1. Draft the release. +gh release create "$VERSION" --draft --title "$VERSION" --target "$(git rev-parse HEAD)" + +# 2. Deploy. Export the secrets first (see the table above). +# Run nix-cache once per architecture; docker once. +./scripts/deploy.sh nix-cache +./scripts/deploy.sh docker + +# 3. Finalize the release once every deployment has succeeded. +gh release edit "$VERSION" --draft=false + +# If a deployment fails, remove the draft instead: +# gh release delete "$VERSION" --yes --cleanup-tag +``` diff --git a/CONTRIBUTOR.md b/CONTRIBUTOR.md deleted file mode 100644 index ce4d40f..0000000 --- a/CONTRIBUTOR.md +++ /dev/null @@ -1,58 +0,0 @@ -# Contributing to Komet Node - -## Development environment - -This repository ships a [devcontainer](.devcontainer/) that provisions the full -toolchain (Nix, the flake's `nix develop` shell, the Claude Code CLI, and the -GitHub CLI). Open the repo in a devcontainer-aware editor and everything below is -available out of the box. - -## Using the GitHub CLI (`gh`) - -`gh` is preinstalled in the devcontainer for creating pull requests, reviewing -issues, and other GitHub tasks from the terminal. - -### Authenticating - -Authenticate once with a personal access token: - -```bash -gh auth login -``` - -Choose **GitHub.com** → **HTTPS** → **Paste an authentication token** when -prompted, then paste the token you create below. - -Your credentials are stored in `~/.config/gh` inside the container, which is -backed by a named volume. This means **your token survives container rebuilds** — -you only need to authenticate once, not every time the container is recreated. - -To check or reset your authentication at any time: - -```bash -gh auth status # show the current login -gh auth logout # remove stored credentials -``` - -### Creating a token with minimal permissions - -Create a **fine-grained** personal access token at **GitHub → Settings → Developer -settings → [Fine-grained personal access tokens](https://github.com/settings/personal-access-tokens/new)** -with the least privilege for your work: - -- **Repository access** → *Only select repositories* → `runtimeverification/komet-node` -- **Contents** → *Read and write* -- **Pull requests** → *Read and write* -- **Issues** → *Read and write* (only if you triage issues) - -`Metadata → Read` is selected automatically; leave everything else at *No access*. - -## Signing commits - -To sign commits made with `git`, add an SSH or GPG key of type **Signing key** to -your GitHub account. - -> [!WARNING] -> Never place an SSH key registered as an **Authentication key** in the container. -> An authentication key grants full account-wide git access and would bypass the -> minimal permissions of your fine-grained PAT. Use a **signing-only** key here. diff --git a/scripts/deploy.sh b/scripts/deploy.sh new file mode 100755 index 0000000..2e3bcd5 --- /dev/null +++ b/scripts/deploy.sh @@ -0,0 +1,181 @@ +#!/usr/bin/env bash +set -euo pipefail + +# NOTE: do not run this script under `set -x` / `bash -x`: the cachix and Docker +# Hub tokens flow through the environment and the `docker login` pipe, and shell +# tracing would print them to the logs. + +# deploy.sh -- build and publish komet-node release artifacts. +# +# This is the single source of truth for the deployment steps that the Release +# workflow (.github/workflows/release.yml) performs. The workflow calls the +# subcommands below, and you can run the exact same steps by hand when CI is +# unavailable. See CONTRIBUTING.md ("Deploying a release") for the runbook. +# +# Subcommands: +# nix-cache Build komet-node and push it to both Nix caches (the +# k-framework closure + the k-framework-binary kup binary). +# docker Build the Docker image, smoke-test it, and push to Docker Hub. +# all Run nix-cache then docker. +# +# Usage: +# scripts/deploy.sh + +REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +cd "${REPO_ROOT}" + +# --- Shared configuration -------------------------------------------------- +# Defaults live here (not in the workflow) so the manual and CI paths stay +# identical. Anything already set in the environment wins, which lets the +# workflow inject secrets and lets a developer override values locally. + +# Keep the Nix daemon from garbage-collecting store paths mid-build, and enable +# flakes for every nix invocation (the build, the kup build, and the builds kup +# runs internally) so we do not depend on flakes being globally enabled. +export GC_DONT_GC="${GC_DONT_GC:-1}" +export NIX_CONFIG="${NIX_CONFIG:-extra-experimental-features = nix-command flakes}" + +# owner/repo and revision, used by kup publish + the cachix pin check. Default +# to the current checkout so manual runs work without extra setup. The first +# sed clause strips any `user:token@` userinfo from an https remote before +# parsing, so a credential embedded in the remote URL never ends up in +# OWNER_REPO (which is later echoed into the deploy log by check-cachix-pin.sh). +OWNER_REPO="${OWNER_REPO:-$(git remote get-url origin | sed -E 's#^[a-z]+://[^@/]*@#https://#; s#(git@github.com:|https://github.com/)##; s#\.git$##')}" +REV="${REV:-$(git rev-parse HEAD)}" +export OWNER_REPO REV + +# Docker Hub coordinates. Only DOCKERHUB_PASSWORD is a secret. +DOCKERHUB_USERNAME="${DOCKERHUB_USERNAME:-rvdockerhub}" +DOCKERHUB_NAMESPACE="${DOCKERHUB_NAMESPACE:-runtimeverificationinc}" +DOCKERHUB_REPO="${DOCKERHUB_REPO:-komet-node}" + +KOMET_NODE_VERSION="$(cat package/version)" + +# Fail early with a clear message if a required secret is missing. +require_env() { + local missing=0 var + for var in "$@"; do + if [ -z "${!var:-}" ]; then + echo "error: required environment variable '${var}' is not set" >&2 + missing=1 + fi + done + [ "${missing}" -eq 0 ] || exit 1 +} + +# Fail before the (long) build if a required tool is not on PATH, so a missing +# dependency surfaces immediately rather than after minutes of building. kup is +# not checked here: nix-cache fetches it via `nix build` at run time. +require_cmd() { + local missing=0 cmd + for cmd in "$@"; do + if ! command -v "${cmd}" >/dev/null 2>&1; then + echo "error: required command '${cmd}' not found on PATH" >&2 + missing=1 + fi + done + [ "${missing}" -eq 0 ] || exit 1 +} + +# CI always builds from a fresh checkout at a known revision. A manual run +# builds from your working tree, so uncommitted changes to tracked files (which +# a dirty flake build embeds) and untracked files (which `docker build .` copies +# into the image) would silently end up in the published artifacts -- and would +# not match the REV they are published under. Require a clean tree so a manual +# deploy is byte-for-byte what CI would produce. `git status --porcelain` skips +# .gitignored paths, so runtime artifacts and dev caches do not trip this. +require_clean_worktree() { + [ -n "${ALLOW_DIRTY:-}" ] && return 0 + if [ -n "$(git status --porcelain)" ]; then + echo "error: working tree is not clean." >&2 + echo "CI deploys from a fresh checkout; these changes would be baked into the" >&2 + echo "published artifacts but would not match REV (${REV}):" >&2 + git status --short >&2 + echo "Commit, stash, or clean them -- or set ALLOW_DIRTY=1 to override." >&2 + exit 1 + fi +} + +# --- nix-cache ------------------------------------------------------------- +# Build the komet-node derivation once, then push it to both Nix caches: the +# k-framework cache (full build closure, via `cachix push`) and the +# k-framework-binary cache (the kup-installable binary, via `kup publish`). +# Both caches are public; "binary" is a historical name, not an access level. +# Both pushes reuse the build output already present in this machine's Nix +# store, so the derivation is never built twice. +deploy_nix_cache() { + require_cmd nix nix-store cachix git curl jq + require_clean_worktree + require_env CACHIX_PUBLIC_TOKEN CACHIX_PRIVATE_KFB_TOKEN + + local komet_node drv + komet_node="$(nix build .#komet-node --no-link --print-out-paths)" + drv="$(nix-store --query --deriver "${komet_node}")" + + # Push the full build closure to the public k-framework cache. + echo ":: pushing build closure to the public k-framework cache" + export CACHIX_AUTH_TOKEN="${CACHIX_PUBLIC_TOKEN}" + nix-store --query --requisites --include-outputs "${drv}" | cachix push k-framework + + # Publish the binary to the k-framework-binary cache. kup reuses the + # store paths built above. + echo ":: publishing komet-node binary to the k-framework-binary cache" + export CACHIX_AUTH_TOKEN="${CACHIX_PRIVATE_KFB_TOKEN}" + export PATH="$(nix build github:runtimeverification/kup --no-link --print-out-paths)/bin:${PATH}" + kup publish k-framework-binary .#komet-node --keep-days 180 + + # Cachix has not been reliably honoring the `cachix pin` requests kup makes + # under the hood. Verify the push and pin explicitly. + bash .github/scripts/check-cachix-pin.sh +} + +# --- docker ---------------------------------------------------------------- +# Build the runtime image, smoke-test it, then push it to Docker Hub. +deploy_docker() { + require_cmd docker git + require_clean_worktree + require_env DOCKERHUB_PASSWORD + + local tag k_version + tag="${DOCKERHUB_NAMESPACE}/${DOCKERHUB_REPO}:ubuntu-jammy-${KOMET_NODE_VERSION}" + k_version="$(cat deps/k_release)" + + echo ":: building Docker image ${tag} (K ${k_version})" + docker build . --no-cache --tag "${tag}" --build-arg K_VERSION="${k_version}" + + echo ":: smoke-testing the image" + docker run --rm "${tag}" komet-node --help + + echo ":: pushing ${tag} to Docker Hub" + # Log out on the way out (success or failure) so the base64 credential + # `docker login` writes to ~/.docker/config.json does not linger on the + # self-hosted runner or on the operator's machine. EXIT (not RETURN) so it + # still fires when `set -e` aborts on a failed login or push. + trap 'docker logout >/dev/null 2>&1 || true' EXIT + echo "${DOCKERHUB_PASSWORD}" | docker login --username "${DOCKERHUB_USERNAME}" --password-stdin + docker image push "${tag}" +} + +usage() { + sed -n '8,22p' "${BASH_SOURCE[0]}" | sed 's/^# \{0,1\}//' +} + +main() { + case "${1:-}" in + nix-cache) deploy_nix_cache ;; + docker) deploy_docker ;; + all) deploy_nix_cache; deploy_docker ;; + -h | --help | help | "") + usage + [ -n "${1:-}" ] # exit non-zero when no subcommand was given + ;; + *) + echo "error: unknown subcommand '${1}'" >&2 + echo >&2 + usage >&2 + exit 1 + ;; + esac +} + +main "$@"