Skip to content

Commit 05bdd16

Browse files
marcelolynchmarcelolynch
committed
feat(cache): restructure cache tool server-side storage layout (leanprover-community#40035)
This PR significantly restructures the cache back-end storage layout to address some security issues and as a side benefit improve auditing, garbage collection, provenance. 1) Instead of setting the cache-universe boundary to the repository, we scope it to particular commit SHAs. This means a review of the changes in a PR does give you confidence in pulling from the cache at that commit. 2) Split the cache universes from master, forks, and nightly-testing at the infrastructure level, using different azure containers. This has other benefits in management, like better auditing, the possibility of targeted garbage collection, etc. See `SECURITY.md` for the motivation and explanation of the trust model implemented here. Also added cache tool tests, and changed a bunch of the messages output to users to surface security concerns more clearly. Extra details: ### Trust model - Five containers — `master`, `forks`, `nightly-testing`, `pr-toolchain-tests`, and `legacy` (the original bare `mathlib4` bucket) — each mapped to a dedicated Azure container. Every trust level has its own writer identity. Azure RBAC on the OIDC token is the enforced write boundary, not the workflow logic. - Reads use a per-repo, trust-ordered chain (most-trusted first, stop at first hit - URL layout is fixed per container, not per repo: `master` is flat (`/f/{hash}`), multi-writer containers namespace by repo (`/f/{repo}/{hash}`), `legacy` preserves its historical mixed layout for older clients. ### Per-commit scoping & discovery - Fork uploads are scoped to their commit SHA (`/f/{repo}/{sha}/{hash}`), so a closed/hidden PR's artifacts can't be served to a later honest PR on the same fork. A marker blob (`/m/{repo}/{sha}`) is written after a successful upload. - New `cache query [REF]`: walks history to the merge-base with master and HEAD- probes markers to report the most recent cached commit (or a boolean probe for a single ref). `cache get --scope=<sha>` then reads that commit's namespace. - `cache get --unsafe` folds that discovery into the download itself: it walks history for the most recent cached fork commit and reads it as a scope automatically, instead of you copying a SHA into `--scope`. `--unsafe-window=N` widens this to the `N` most recent (default `1`). It always prints the security notice, since it trusts whoever built those commits. - `cache get` prints a security notice whenever a read leaves the repo's default trust boundary (a scope, a widened `--cache-from`, or a `--repo` that diverges from the git remote), plus a hint pointing uncached fork HEADs at `cache query`. ### CLI / env surface - New flags: `--cache-from=LIST`, `--container=NAME`, `--scope=REF`, `--unsafe`, `--unsafe-window=N`; new command `cache query`. - New env: `MATHLIB_CACHE_FROM`, `MATHLIB_CACHE_REPO_SCOPE`. `MATHLIB_CACHE_GET_URL` / `_PUT_URL` retained as single-URL escape hatches; `MATHLIB_CACHE_USE_CLOUDFLARE` removed. ### CI wiring - New composite action `cache-trust-dispatch` is the single source mapping `(repo, branch) → (write container, read chain, per-commit scope)`; `build.yml`, `bors.yml`, and `build_template.yml` consult it. Trust policy lives in YAML, not in the Lean tool. - During migration, master CI dual-writes to `legacy` so older cache clients keep working; forks/nightly never write to `legacy`. ### Code organization & testing - Backend split into focused modules: `Cache.Infra` (container model), `Cache.Cli` (option parsing), `Cache.Marker`, `Cache.Query`, `Cache.Warning`; `Cache.Init` folded away. - New standalone `lake exe cache-test` (`Cache.Test`) unit-tests the pure logic — container model, URL construction, per-repo read chains, flag parsing, and the warning conditions — without building Mathlib.
1 parent 3cd5cf9 commit 05bdd16

18 files changed

Lines changed: 3030 additions & 358 deletions

File tree

‎.github/actions/cache-trust-dispatch/action.yml‎

Lines changed: 157 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,157 @@
1+
# Single source of truth mapping (repo, branch) → (upload container,
2+
# read fallback chain) for Mathlib's multi-container cache.
3+
#
4+
# Called by build, upload_cache, and post_steps in build_template.yml so
5+
# trust classification is decided in exactly one place. Lean-side cache
6+
# logic stays branch-agnostic; this composite is the seam where CI-only
7+
# trust policy lives.
8+
9+
name: Cache trust dispatch
10+
description: Compute the cache container target and read fallback for this job.
11+
12+
inputs:
13+
repo:
14+
description: GitHub repo full name (`owner/name`).
15+
required: true
16+
branch:
17+
description: Branch name (`github.head_ref || github.ref_name`).
18+
required: true
19+
head-sha:
20+
description: |
21+
Head commit SHA for the ref being built. Used as the per-commit cache
22+
namespace (`MATHLIB_CACHE_REPO_SCOPE`) for fork-trust uploads, so a
23+
closed/hidden PR's poisoned artifacts cannot be served to a later
24+
honest PR from the same fork.
25+
required: true
26+
27+
# Outputs are mirrored to $GITHUB_ENV inside the step, which is what
28+
# downstream `cache get` / `cache put-staged` calls actually read. We
29+
# also expose them as action outputs for callers that need them in
30+
# `with:` blocks (e.g. constructing further `if:` conditions).
31+
outputs:
32+
primary:
33+
description: Container name for uploads (master, forks, nightly-testing, pr-toolchain-tests).
34+
value: ${{ steps.dispatch.outputs.primary }}
35+
read-chain:
36+
description: |
37+
Comma-separated read fallback chain for `MATHLIB_CACHE_FROM`. Empty
38+
when the job should use the cache tool's repo-level default.
39+
value: ${{ steps.dispatch.outputs.read-chain }}
40+
repo-scope:
41+
description: |
42+
Per-commit namespace suffix for `MATHLIB_CACHE_REPO_SCOPE`. Set to
43+
the head SHA when uploading to fork-trust containers; empty for
44+
master / nightly / pr-toolchain-tests uploads where scoping isn't
45+
applied.
46+
value: ${{ steps.dispatch.outputs.repo-scope }}
47+
48+
runs:
49+
using: composite
50+
steps:
51+
- name: Compute trust dispatch
52+
id: dispatch
53+
shell: bash
54+
run: |
55+
REPO="${{ inputs.repo }}"
56+
BRANCH="${{ inputs.branch }}"
57+
HEAD_SHA="${{ inputs.head-sha }}"
58+
PRIMARY=""
59+
READ_CHAIN=""
60+
REPO_SCOPE=""
61+
62+
# Security note: this dispatch is NOT the trust boundary for writes.
63+
# The real enforcement is the OIDC bearer token minted in upload_cache:
64+
# the token is scoped to a specific container, so a malicious actor
65+
# rewriting this case to `--container=master` from a fork build would
66+
# be 403'd by Azure regardless. The dispatch exists so the workflow
67+
# does the right thing in the honest case; defence in depth is RBAC.
68+
69+
case "$REPO" in
70+
"leanprover-community/mathlib4")
71+
case "$BRANCH" in
72+
"master"|"staging")
73+
# Master / staging are the only writers that feed `master`
74+
# (`staging` is bors's merge candidate, which fast-forwards to
75+
# `master`). Read `master` only, not the default [master,
76+
# legacy]: files the read chain serves are skipped at stage
77+
# time, so keeping `legacy` would leave legacy-only files out of
78+
# `master` for good. Reading `master` alone turns them into
79+
# misses that get rebuilt and uploaded, so `master` fills itself
80+
# into a standalone cache. (Only PRIMARY=master does this; other
81+
# runs write to `forks` and keep the wider chain.)
82+
PRIMARY="master"
83+
READ_CHAIN="master"
84+
;;
85+
*)
86+
# `bors trying`, `ci-dev/*`, maintainer dev branches on the
87+
# canonical repo: trust level is fork-equivalent (the OIDC
88+
# token's RBAC scopes them to `forks`). Reads must widen
89+
# past the default [master, legacy] so the post-build
90+
# verification finds the just-uploaded fork-trust artifacts.
91+
PRIMARY="forks"
92+
READ_CHAIN="master,forks,legacy"
93+
;;
94+
esac
95+
;;
96+
"leanprover-community/mathlib4-nightly-testing")
97+
case "$BRANCH" in
98+
"nightly-testing"|"nightly-testing-green"|"staging"|bump/*)
99+
# Trusted nightly refs use the default [nightly-testing, legacy].
100+
# It excludes `pr-toolchain-tests` so an upload from a
101+
# `lean-pr-testing-*` branch never reaches a trusted-nightly
102+
# consumer.
103+
PRIMARY="nightly-testing"
104+
;;
105+
*)
106+
# `lean-pr-testing-*`, `batteries-pr-testing-*`, etc.:
107+
# least-trusted (can build with arbitrary toolchains). Widen
108+
# reads to recover this branch's own previously-uploaded
109+
# artifacts; trusted-nightly stays preferred where hash
110+
# spaces happen to align.
111+
PRIMARY="pr-toolchain-tests"
112+
READ_CHAIN="pr-toolchain-tests,nightly-testing,legacy"
113+
;;
114+
esac
115+
;;
116+
*)
117+
# Foreign fork. The cache tool's default chain for a fork repo
118+
# is [master, forks, legacy] (master-first): master supplies the
119+
# bulk of unchanged upstream deps, forks supplies PR-specific
120+
# files. No widening needed, so MATHLIB_CACHE_FROM stays unset.
121+
PRIMARY="forks"
122+
;;
123+
esac
124+
125+
# Per-commit cache namespace, only for fork-trust uploads. Closes the
126+
# within-fork temporal replay attack: each commit's CI run gets its
127+
# own /f/{repo}/{sha}/... namespace, so artifacts from a closed/
128+
# hidden PR cannot be served to a later honest build on the same
129+
# fork. Master / nightly / pr-toolchain-tests uploads stay un-scoped:
130+
# master has a single writer (no replay risk), and the per-toolchain
131+
# hash partitioning isolates nightly and toolchain-test classes via
132+
# their root-hash inputs.
133+
if [ "$PRIMARY" = "forks" ]; then
134+
REPO_SCOPE="$HEAD_SHA"
135+
fi
136+
137+
echo "primary=$PRIMARY" >> "$GITHUB_OUTPUT"
138+
echo "read-chain=$READ_CHAIN" >> "$GITHUB_OUTPUT"
139+
echo "repo-scope=$REPO_SCOPE" >> "$GITHUB_OUTPUT"
140+
echo "MATHLIB_CACHE_PRIMARY=$PRIMARY" >> "$GITHUB_ENV"
141+
if [ -n "$READ_CHAIN" ]; then
142+
echo "MATHLIB_CACHE_FROM=$READ_CHAIN" >> "$GITHUB_ENV"
143+
fi
144+
if [ -n "$REPO_SCOPE" ]; then
145+
echo "MATHLIB_CACHE_REPO_SCOPE=$REPO_SCOPE" >> "$GITHUB_ENV"
146+
fi
147+
# Visible in CI logs so a glance at any cache-touching step shows
148+
# what trust class the job is operating under.
149+
SCOPE_NOTE=""
150+
if [ -n "$REPO_SCOPE" ]; then
151+
SCOPE_NOTE=", MATHLIB_CACHE_REPO_SCOPE=$REPO_SCOPE"
152+
fi
153+
if [ -n "$READ_CHAIN" ]; then
154+
echo "cache-trust-dispatch: REPO=$REPO BRANCH=$BRANCH → container=$PRIMARY, MATHLIB_CACHE_FROM=$READ_CHAIN$SCOPE_NOTE"
155+
else
156+
echo "cache-trust-dispatch: REPO=$REPO BRANCH=$BRANCH → container=$PRIMARY, MATHLIB_CACHE_FROM=<default>$SCOPE_NOTE"
157+
fi

‎.github/actions/get-tools/action.yml‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,15 @@ inputs:
3636
description: Destination directory for the tools.
3737
required: false
3838
default: tools-branch
39+
source_dir:
40+
description: >
41+
Optional path to a local checkout under test. When set and the artifact
42+
fast path is in play, the action compares this checkout's tool sources
43+
against the artifact's `master` baseline; if they differ it skips the
44+
prebuilt artifact and builds from source, so a branch that changes the
45+
tool is tested with its own tool. Empty disables the comparison.
46+
required: false
47+
default: ''
3948
runs:
4049
using: composite
4150
steps:
@@ -56,6 +65,23 @@ runs:
5665
--workflow "${{ inputs.artifact_workflow }}" \
5766
--branch master --status success --event push \
5867
--limit 1 --json databaseId --jq '.[0].databaseId // empty' 2>/dev/null || true)
68+
69+
# If a local checkout under test is provided and its tool sources differ
70+
# from the artifact's master baseline, the prebuilt tool would mask the
71+
# change — drop it and build from source. Local git only; no API call.
72+
# These are the source paths that determine the bundled tools (the
73+
# `cache` binary and the build-helper scripts in publish_tools.yml); they
74+
# live here so callers don't have to duplicate the list.
75+
if [[ -n "$run_id" && -n "${{ inputs.source_dir }}" ]]; then
76+
git -C "${{ inputs.source_dir }}" fetch --no-tags --depth=1 \
77+
"https://github.com/${{ inputs.artifact_repo }}.git" master || true
78+
# Fail safe toward building: a failed fetch/diff leaves $? non-zero.
79+
if ! git -C "${{ inputs.source_dir }}" diff --quiet FETCH_HEAD -- \
80+
Cache scripts/lake-build-with-retry.sh scripts/lake-build-wrapper.py; then
81+
echo "Tool sources in '${{ inputs.source_dir }}' differ from master; building from source."
82+
run_id=""
83+
fi
84+
fi
5985
fi
6086
echo "Resolved publisher run_id: '${run_id}'"
6187
echo "run_id=${run_id}" >> "$GITHUB_OUTPUT"

‎.github/workflows/bors.yml‎

Lines changed: 40 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -27,13 +27,46 @@ jobs:
2727
with:
2828
concurrency_group: ${{ github.workflow }}-${{ github.ref }}-${{ github.run_id }}
2929
pr_branch_ref: ${{ github.sha }}
30-
# Use the MASTER cache key only when merging into mathlib4 (staging branch);
31-
# 'bors try' runs (trying branch) and nightly-testing use NON_MASTER
32-
cache_application_id: ${{ github.ref_name == 'staging' && github.repository == 'leanprover-community/mathlib4' && vars.CACHE_MASTER_WRITER_AZURE_APP_ID || vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
33-
# Track the cache_application_id choice above; the environment fixes the OIDC subject the Azure app trusts.
34-
# nightly-testing is intentionally left without an environment ('') so it keeps its existing ref-based trust.
35-
# TODO: give mathlib4-nightly-testing its own cache-upload environment + federated credential.
36-
cache_environment: ${{ github.repository == 'leanprover-community/mathlib4' && (github.ref_name == 'staging' && 'cache-upload-master' || 'cache-upload-forks') || '' }}
30+
# Trust-level dispatch for the cache writer app (bors runs on
31+
# `staging` = real merge candidate; `trying` = experimental).
32+
# Each case is spelled out so the trust mapping is unambiguous:
33+
# - mathlib4/staging → MASTER writer
34+
# - mathlib4/trying → NON_MASTER (FORKS) writer
35+
# (explicitly NOT master-trust)
36+
# - mathlib4-nightly-testing/staging → NIGHTLY_TESTING writer
37+
# - mathlib4-nightly-testing/trying → PR_TOOLCHAIN_TESTS writer
38+
# (least-trust on the nightly repo)
39+
# - any other ref on either repo → NON_MASTER (FORKS) writer
40+
cache_application_id: >-
41+
${{
42+
(github.repository == 'leanprover-community/mathlib4'
43+
&& github.ref_name == 'staging')
44+
&& vars.CACHE_MASTER_WRITER_AZURE_APP_ID
45+
|| (github.repository == 'leanprover-community/mathlib4'
46+
&& github.ref_name == 'trying')
47+
&& vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID
48+
|| (github.repository == 'leanprover-community/mathlib4-nightly-testing'
49+
&& github.ref_name == 'staging')
50+
&& vars.CACHE_NIGHTLY_TESTING_WRITER_AZURE_APP_ID
51+
|| (github.repository == 'leanprover-community/mathlib4-nightly-testing'
52+
&& github.ref_name == 'trying')
53+
&& vars.CACHE_PR_TOOLCHAIN_TESTS_WRITER_AZURE_APP_ID
54+
|| vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID
55+
}}
56+
# OIDC environment binding for the upload_cache job. MUST track the cache_application_id
57+
# mapping above so the minted token's `:environment:` subject matches the writer app's
58+
# federated credential. mathlib4-nightly-testing intentionally uses branch/ref-scoped
59+
# trust instead of an environment: each nightly writer app is RBAC-isolated to its own
60+
# container, so branch scoping is sufficient there.
61+
cache_environment: >-
62+
${{
63+
(github.repository == 'leanprover-community/mathlib4'
64+
&& github.ref_name == 'staging')
65+
&& 'cache-upload-master'
66+
|| (github.repository == 'leanprover-community/mathlib4')
67+
&& 'cache-upload-forks'
68+
|| ''
69+
}}
3770
# bors runs should build the tools from their commit-under-test: after all, we are trying to
3871
# test 'what would happen if this was merged', so we need to use the 'would-be-post-merge' tools
3972
tools_branch_ref: ${{ github.sha }}

‎.github/workflows/build.yml‎

Lines changed: 34 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -36,11 +36,39 @@ jobs:
3636
with:
3737
concurrency_group: ${{ github.workflow }}-${{ github.ref }}-${{ (github.event_name == 'push' && github.ref == 'refs/heads/master' && github.run_id) || '' }}
3838
pr_branch_ref: ${{ github.sha }}
39-
# Use the MASTER cache key only on mathlib4/master; nightly-testing and other branches use NON_MASTER
40-
cache_application_id: ${{ github.repository == 'leanprover-community/mathlib4' && github.ref == 'refs/heads/master' && vars.CACHE_MASTER_WRITER_AZURE_APP_ID || vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
41-
# Track the cache_application_id choice above; the environment fixes the OIDC subject the Azure app trusts.
42-
# nightly-testing is intentionally left without an environment ('') so it keeps its existing ref-based trust.
43-
# TODO: give mathlib4-nightly-testing its own cache-upload environment + federated credential.
44-
cache_environment: ${{ github.repository == 'leanprover-community/mathlib4' && (github.ref == 'refs/heads/master' && 'cache-upload-master' || 'cache-upload-forks') || '' }}
39+
# Trust-level dispatch for the cache writer app:
40+
# - mathlib4/master → MASTER writer
41+
# - mathlib4-nightly-testing/(nightly-testing | nightly-testing-green | bump/*)
42+
# → NIGHTLY_TESTING writer
43+
# - mathlib4-nightly-testing/(anything else) → PR_TOOLCHAIN_TESTS writer
44+
# - everything else (dev branches on mathlib4, etc.) → NON_MASTER (forks) writer
45+
cache_application_id: >-
46+
${{
47+
(github.repository == 'leanprover-community/mathlib4'
48+
&& github.ref_name == 'master')
49+
&& vars.CACHE_MASTER_WRITER_AZURE_APP_ID
50+
|| (github.repository == 'leanprover-community/mathlib4-nightly-testing'
51+
&& (github.ref_name == 'nightly-testing'
52+
|| github.ref_name == 'nightly-testing-green'
53+
|| startsWith(github.ref_name, 'bump/')))
54+
&& vars.CACHE_NIGHTLY_TESTING_WRITER_AZURE_APP_ID
55+
|| (github.repository == 'leanprover-community/mathlib4-nightly-testing')
56+
&& vars.CACHE_PR_TOOLCHAIN_TESTS_WRITER_AZURE_APP_ID
57+
|| vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID
58+
}}
59+
# OIDC environment binding for the upload_cache job. MUST track the cache_application_id
60+
# mapping above so the minted token's `:environment:` subject matches the writer app's
61+
# federated credential. mathlib4-nightly-testing intentionally uses branch/ref-scoped
62+
# trust instead of an environment: each nightly writer app is RBAC-isolated to its own
63+
# container, so branch scoping is sufficient there.
64+
cache_environment: >-
65+
${{
66+
(github.repository == 'leanprover-community/mathlib4'
67+
&& github.ref_name == 'master')
68+
&& 'cache-upload-master'
69+
|| (github.repository == 'leanprover-community/mathlib4')
70+
&& 'cache-upload-forks'
71+
|| ''
72+
}}
4573
runs_on: pr
4674
secrets: inherit

0 commit comments

Comments
 (0)