RFC: SHA-isolated `lake cache get` via configurable revision discovery

Proposal

lake cache get walks git history to the nearest cached ancestor when the current commit has no cache (Main.lean:574-589). For a low-trust source such as fork-PR artifacts, that walk breaks isolation: a build can be served a different commit's cache. This conflicts with the security model that projects like mathlib, with open outside contributions that should be assumed malicious for threat modelling purposes.

This RFC proposes adding a per-service revDiscovery policy so a service can be pinned to the current commit's mapping, with no walk, giving the invariant "gets are isolated by SHA" — safe by default and without a per-call flag.

Background: cache poisoning and trust segregation

A cache writable by low-trust jobs (e.g., PR CI with arbitrary elaboration code) is open to poisoning: a malicious build publishes an input/output mapping and corrupted artifact. Lake content-addresses artifacts and verifies hashes on download (Cache.lean:553-561, 778-783), which protects transfer integrity but not mapping authenticity.

Defending against this means segregating reads and writes by trust level into separate endpoints/scopes, enforced by storage credentials (S3/OIDC). Consumers can then choose to consume from the different endpoints according to different situations.

mathlib4 has restructured its build cache this way; see leanprover-community/mathlib4#40035. Trust-segregated containers (master, forks, others), each with its own write credentials, read through an ordered fallback chain with per-commit scoping.

For fork artifacts it enforces a per-SHA isolation invariant: a build is only served the cache of the specific commit it is on, so a closed or hidden PR's artifacts cannot be served to a later honest PR. This RFC brings that invariant to lake cache.

The invariant: gets isolated by SHA

Content-addressing already pins artifact integrity (Cache.lean:778-783): whatever endpoint serves a hash, the bytes must match it or are rejected. So the only thing that decides what a build consumes is which mapping it reads. A mapping is {rev}.jsonl, keyed by commit SHA, and SHAs are globally unique. Reading only the current commit's mapping binds consumption to that commit's vouched outputs; a different or closed PR's mapping is a file you never fetch. The unbounded walk to an ancestor is exactly what breaks this, so the "fix" is to not perform this walk. This requires lakeside support, here in the form of a configuration of the endpoint itself.

Current state

cache get --rev <sha> already fetches exactly that rev's mapping with no walk, erroring if absent (Main.lean:535-538). But it must be passed on every call. With no --rev, the default is to walk (Main.lean:574-589).

The change

Per-service revDiscovery:

• nearest: walk ancestors, take the first revision cached. (current behavior, default)
• head: current commit only, no walk. Enforces SHA isolation.

A service marked revDiscovery = "head" makes a bare lake cache get against it isolated by default, with no --rev to remember and no SHA to compute.

Configuration sketch

[[cache.service]]
name = "forks"
kind = "s3"
artifactEndpoint = "https://…/forks/artifacts"
revisionEndpoint = "https://…/forks/revisions"
revDiscovery = "head"            # only the current commit's mapping; no walk

lake cache get --service forks then fetches only the current commit's mapping and the artifacts it names, all hash-verified.

Interaction with other flags

• --max-revs: ignored with a warning for a head service. We want the configuration to be always respected here, especially since revDiscovery = head has some security implications. --fail-level (--wfail/--iofail) can escalate that warning
• --rev: still acts as an override, as it is explicitly a "no-walk" pin
• an explicit mappings file (lake cache get <file>) bypasses revision discovery entirely so revDiscovery does not apply

Security

The trust boundary preventing poisoning is publish-side: which endpoint a job can write to, enforced by CI credentials and storage IAM (e.g., only master CI holds the master key). cache put and write-credential handling (Main.lean:591-619) are unchanged.

On the read side, revDiscovery = "head" is the mechanism for the SHA invariant: the build reads only the current commit's mapping, so a low-trust source can only serve the build of the exact commit it is on. Artifacts are verified against their content hash regardless of endpoint, so the mapping source is the only thing that must be trusted (or head-pinned).

Alternatives considered

• Per-call --rev <sha> (status quo): the no-walk mechanism exists (Main.lean:535-538) but is flag-dependent: a forgetful caller or a bare lake cache get still walks. This RFC makes it a safe-by-default per-service policy.
• Per-commit/per-repo artifact path scoping (mathlib4's /f/{repo}/{sha}/{hash}.art). Redundant for read isolation, which the SHA-keyed mapping already provides, and it fragments cross-commit reuse. It remains useful publish-side (write-IAM, GC).

Backwards compatibility

Additive. revDiscovery defaults to nearest, today's behavior. head is opt-in per service; existing flags including --rev are unaffected.

User Experience

A service is marked no-walk once in config, so a bare lake cache get against it is SHA-isolated. The caller does not remember --rev, compute a SHA, or pass a scope.

Beneficiaries

Projects that consume low-trust (fork/PR) caches and need the assurance that a build only sees its own commit's artifacts. Immediate driver: mathlib4's migration of its multi-container cache (leanprover-community/mathlib4#40035) to lake cache, which needs this invariant for fork fetches.

Maintainability

Small surface. revDiscovery = "nearest" is the existing walk; head reuses the existing no-walk --rev path. No new transport or storage.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start in src/lake/Lake/CLI/Main.lean at the cache get revision-discovery paths around lines 535-589, then inspect cache configuration and verification in src/lake/Lake/Config/Cache.lean. The change is complete when a service can select head or nearest discovery, head avoids ancestor walking, existing --rev behavior remains intact, and the stated warning and explicit-mapping cases are preserved.