Clarify and simplify Anneal's Lake integration

*Written by an agent based on a prompt to summarize all work and discussions around Anneal's use of lake.*

Anneal relies on Lake in several distinct roles:

1. We use Lake while [building the Anneal toolchain archive](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/flake.nix).
2. Anneal v1 [generates a Lake workspace and invokes Lake during verification](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/src/aeneas.rs).
3. Both [v1](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/tests/integration.rs) and [v2](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/src/main.rs) test that a fresh workspace can consume the prebuilt archive without rebuilding or mutating it.
4. We increasingly rely on Lake metadata and build artifacts for [interactive Lean tooling](https://github.com/google/zerocopy/pull/3485) as well as batch compilation.

This integration has accumulated substantial machinery around Lake's model of packages, workspaces, configuration, build artifacts, traces, and caches. Some of that machinery is necessary. Some may encode workarounds for older Lake behavior. Some may now be replaceable by [better Lake interfaces](https://leanprover.zulipchat.com/#narrow/channel/236449-Program-verification/topic/Rust.20Verification.20.2B.20Lake.20Tooling/near/592135972).

We should make the contract explicit, then decide which parts Anneal should continue to own and which parts Lake should provide directly.

## What Anneal needs from Lake

The motivating workload is not one large parallel Lake build. Anneal runs [many independent verification jobs, including many integration-test sandboxes](https://github.com/google/zerocopy/pull/3305). They should [share expensive immutable prerequisites without sharing mutable per-job state](https://leanprover.zulipchat.com/#narrow/channel/236449-Program-verification/topic/Rust.20Verification.20.2B.20Lake.20Tooling/near/592135972).

The desired model is roughly:

```text
prepared once
│
▼
┌─────────────────────┐
│ immutable toolchain │
│ │
│ Lean │
│ Aeneas │
│ dependency sources │
│ compiled artifacts │
│ config/traces │
└─────────────────────┘
▲ ▲ ▲
│ │ │
read-only │ │ │ read-only
│ │ │
┌─────┘ │ └─────┐
│ │ │
workspace A workspace B workspace C
mutable mutable mutable
```

A fresh workspace should be able to use the prepared toolchain:

- without network access;
- without resolving dependencies again;
- without cloning dependencies again;
- without rebuilding unchanged dependencies;
- without mutating the installed toolchain;
- concurrently with other workspaces doing the same thing;
- after the toolchain archive has moved from its build-time path to its installation path;
- for ordinary builds and the language-server/InfoView setup path; and
- with enough validation that a cache hit cannot silently change the verification result relative to a clean build.

These requirements concern several resources that we should keep separate:

- **dependency identity**: which source revisions form the dependency graph;
- **source materialization**: where those sources live;
- **compiled artifacts**: `.olean`, `.ilean`, native outputs, etc.;
- **package configuration**: the compiled/configured interpretation of each Lake package;
- **workspace state**: state which belongs to one generated verification workspace;
- **artifact provenance**: which inputs produced a reusable artifact;
- **coordination**: which locations multiple processes may safely access concurrently.

A content-addressed artifact store solves only some of these problems.

## Historical implementation

### Original model: let each generated workspace behave like a normal Lake project

Early Hermes/Anneal generated a `lakefile.lean` whose [Aeneas dependency ultimately came from source](https://github.com/google/zerocopy/issues/3233). In practice this meant that verification could cause Lake to download dependencies and build Aeneas and its transitive Lean dependencies.

[Issue #3233](https://github.com/google/zerocopy/issues/3233) recorded the resulting costs:

- verification latency;
- complicated caching;
- build noise;
- complicated local-development and CI infrastructure; and
- large cold-cache penalties.

The first response was therefore to [move expensive work out of verification and into setup](https://github.com/google/zerocopy/pull/3236).

[Aeneas #921](https://github.com/AeneasVerif/aeneas/pull/921) changed the Aeneas release pipeline to run `lake build` and ship the compiled Lean library alongside the binaries. That was the first producer-side version of the model: build Aeneas once and distribute the result.

### Prebuilding was not sufficient

A prebuilt library does not by itself tell a downstream Lake workspace how to reuse it.

Several approaches explored that problem.

#### Explicitly pin every transitive package

[#3255](https://github.com/google/zerocopy/pull/3255) read Aeneas's `lake-manifest.json` and generated a `require ... from ""` for every package in the installed toolchain.

The idea was straightforward: construct a generated Lake project whose dependency graph points entirely at already-materialized packages.

This avoided some resolution and downloads, but it also required Anneal to reproduce Lake's resolved dependency graph in a second representation.

#### Share Lake's artifact cache

Sebastian's [#3297](https://github.com/google/zerocopy/pull/3297) replaced Anneal's test worker-cache cloning machinery with Lake's content-addressed artifact cache. Setup populated a stable `LAKE_CACHE_DIR`; tests consumed it read-only.

[#3298](https://github.com/google/zerocopy/pull/3298) extended the same experiment to generated workspaces. It:

- populated the artifact cache during setup;
- copied the toolchain's `lake-manifest.json`;
- manually injected Aeneas into that manifest; and
- symlinked the toolchain's `.lake/packages` into the generated workspace.

The [PR itself calls the manifest injection a hack](https://github.com/google/zerocopy/pull/3298/files): running `lake update` would re-resolve and clone dependencies, while simply copying the manifest did not contain an entry for the new root Aeneas dependency.

This experiment exposed the important distinction between **sharing artifacts** and **sharing mutable package/workspace state**.

### Concurrent readers were not actually read-only

The preserved Lean Zulip discussion records the original concurrency problem more precisely.

Anneal's integration suite runs many independent Lake invocations. Mac distinguished the dedicated artifact store from dependency repositories and other `.lake` state. Sebastian later localized racing writes to shared dependency `.lake/config` directories. Mac suggested comparing configuration traces and dependency ordering rather than assuming identical dependency URLs implied identical configurations.

The important conclusion was not that Lake's artifact cache was corrupt. It was that sharing an immutable artifact cache did not make the other shared Lake state immutable.

That led to [#3304](https://github.com/google/zerocopy/pull/3304).

Instead of exposing one installed filesystem package directly as a path dependency, setup initialized Aeneas as a local Git repository. Generated workspaces depended on a `file://` Git remote. Each workspace could therefore own its checkout while still sharing the content-addressed build artifacts.

This changed **ownership**, not merely caching.

[#3305](https://github.com/google/zerocopy/pull/3305) then removed the old flock-guarded worker pools and smart-cloned caches. A reported integration run with roughly 100 workers had consumed roughly 100 GB; moving shared products out of per-worker clones eliminated that architecture.

[#3306](https://github.com/google/zerocopy/pull/3306) extended the same idea recursively: setup turned transitive Lean dependencies into local Git repositories so that later Lake clones came from the local filesystem rather than the network.

This architecture isolated mutable checkout state, but we still paid to materialize it repeatedly.

### Copy less, symlink more

By [#3344](https://github.com/google/zerocopy/pull/3344), verification was copying a roughly 5 GB dependency tree containing roughly 5,000 `.olean` files into each generated workspace.

The next design copied only files Lake might need to mutate and shared the large immutable build artifacts. The installed toolchain was made recursively read-only so an unexpected Lake write would fail instead of silently introducing a cross-workspace race.

This was a useful invariant:

> The installed toolchain should be a read-only object. If normal verification needs to mutate it, our integration contract is wrong.

But determining which Lake files were mutable remained difficult.

[#3341](https://github.com/google/zerocopy/pull/3341) illustrates how far this went. It experimented with copying precompiled `.lake/config` state, renaming Aeneas's `[anonymous]` configuration to `aeneas`, rewriting trace contents, and incrementing package indices because injecting Aeneas changed the package ordering.

This produced a [measured `run_lake` improvement in that experiment](https://github.com/google/zerocopy/pull/3341), but it also demonstrated that Lake's cached configuration encodes identities which are not naturally relocatable or composable by downstream tools.

### Move preparation into a Nix-built omnibus archive

V2 changed the producer side substantially.

[#3438](https://github.com/google/zerocopy/pull/3438) moved both v1 and v2 onto the same Nix-built omnibus archive. Rather than install Aeneas and then reconstruct/cache its Lake environment at runtime, CI/Nix constructs the whole toolchain ahead of time.

[#3444](https://github.com/google/zerocopy/pull/3444) made that archive portable across supported platforms. It also seeded vendored Lake packages from upstream Mathlib artifacts and built against them.

The current archive pipeline does more than copy dependency sources:

- [`rewrite-lake-vendor.py`](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/rewrite-lake-vendor.py) rewrites Git dependencies in `lakefile.lean`, `lakefile.toml`, and manifests into local path dependencies;
- it can also [strip or rewrite absolute prefixes embedded in `.trace` files](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/rewrite-lake-vendor.py);
- [`prune-lake-cache.py`](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/prune-lake-cache.py) computes the reachable Mathlib module closure and removes unused source/build artifacts; and
- the [Nix build prepares the corresponding Lake caches](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/flake.nix) before the archive becomes read-only.

This gives us a single distributable dependency universe instead of reconstructing one during every `cargo anneal setup`.

### `--old` was useful but not sufficient

[#3443](https://github.com/google/zerocopy/pull/3443) normalized vendored source/config mtimes so that `lake --old` would accept existing artifacts instead of invalidating them.

That solved one invalidation mechanism, but not the full problem.

The key architectural change came in [#3450](https://github.com/google/zerocopy/pull/3450).

The investigation found that:

- `lake --old` still depends on source/config mtimes;
- without a complete root manifest, Lake may reconfigure path dependencies;
- that reconfiguration writes lock/config state into package directories;
- those package directories are intentionally read-only; and
- Lake accepts manifest paths relative to the generated workspace.

V1 therefore stopped materializing a mutable facsimile of Aeneas and its packages.

Instead it now:

1. writes a generated [`lakefile.lean` whose Aeneas dependency points directly into the installed archive](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/src/aeneas.rs#L270-L310);
2. [reads the archive's Aeneas `lake-manifest.json`](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/src/aeneas.rs#L363-L389);
3. [constructs a complete root `lake-manifest.json`](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/src/aeneas.rs#L363-L443);
4. records Aeneas and all of its dependencies as path packages;
5. [makes their paths relative to the final generated workspace](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/src/aeneas.rs#L340-L443);
6. marks inherited packages appropriately; and
7. lets all of those dependencies remain in the read-only archive.

The generated workspace [preserves only its own `.lake` directory across regeneration](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/src/aeneas.rs#L314-L335).

This is the cleanest architecture Anneal has had so far because it separates the two ownership domains directly:

```text
archive: immutable dependency graph + prepared dependency artifacts
workspace: generated source + workspace-owned Lake state
```

[#3453](https://github.com/google/zerocopy/pull/3453) encoded this as a regression test. Both v1 and v2 install the Nix archive, assert that Aeneas is read-only, create a fresh generated workspace with a complete relative manifest, and run:

```text
lake --keep-toolchain --old build Generated
lake --keep-toolchain env lean --json generated/Generated.lean
```

against that archive.

## Current v1 behavior

The retained [`anneal/v1`](https://github.com/google/zerocopy/tree/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1) is still the implementation that [performs verification](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/src/main.rs).

Its [generated project](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/src/aeneas.rs) contains:

- a generated `lean-toolchain`;
- generated Aeneas output;
- Anneal's Lean support code;
- user proof files;
- a generated `lakefile.lean`; and
- a generated complete `lake-manifest.json`.

The main [dependency-build invocation](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/src/aeneas.rs#L520-L529) is:

```text
lake --keep-toolchain --old build Generated Anneal
```

with [the bundled toolchain's environment configured by `configure_lake_command`](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/src/aeneas.rs#L700-L757).

Anneal then [checks individual generated specification files](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/src/aeneas.rs#L590-L645) with:

```text
lake --keep-toolchain env lean --json
```

The distinction matters. Lake builds the shared generated libraries, but each specification is ultimately checked through `lake env lean`, which supplies the environment and invokes Lean directly.

V1's [`generate` command](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/src/main.rs#L82-L98) exposes essentially the same environment for manual experimentation.

## Current v2 behavior

The current top-level [`anneal` crate](https://github.com/google/zerocopy/tree/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal) is not a second complete verification driver. Its [CLI exposes only `setup`](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/src/main.rs#L29-L35).

It [installs the Nix-built archive through Exocrate](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/src/main.rs#L61-L84).

V2 does, however, encode the same Lake consumption contract in its tests. Its [archive-reuse test](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/src/main.rs):

1. installs the archive;
2. checks that Aeneas has no write bits;
3. creates a fresh Lake workspace;
4. writes a relative manifest pointing into the archive;
5. runs `lake --old build Generated`; and
6. runs `lake env lean --json`.

Thus v1 and v2 currently share the **toolchain/archive architecture**, while only retained v1 contains the end-to-end verification implementation.

We should preserve this distinction when discussing “Anneal v2 support.”

## The remaining interactive-tooling problem

Batch compilation is not the whole contract.

The open [#3485](https://github.com/google/zerocopy/pull/3485) and [#3486](https://github.com/google/zerocopy/pull/3486) stack extends the archive work to the language-server setup graph.

### #3485: prime traces through the real server traversal

Previous archive construction promoted `.trace.nobuild` state iteratively. [#3485](https://github.com/google/zerocopy/pull/3485) instead adds a [Lake script](https://github.com/google/zerocopy/blob/26fa0d68f318b987e7712a0c39729e9160e25d6e/anneal/prime-lakefile.lean) which traverses the language-server setup graph once, then rehashes and publishes the resulting package-qualified traces only after the traversal succeeds.

It also takes care [not to let Nix post-processing alter native artifacts after Lake has hashed them](https://github.com/google/zerocopy/blob/26fa0d68f318b987e7712a0c39729e9160e25d6e/anneal/flake.nix).

The [installed-archive regression](https://github.com/google/zerocopy/blob/26fa0d68f318b987e7712a0c39729e9160e25d6e/anneal/v1/tests/integration.rs) then consumes the actual server setup and checks that every referenced artifact belongs to the toolchain.

This is important because “`lake build` did not rebuild anything” is weaker than “the editor can open this project without discovering missing/stale artifacts or escaping the installed toolchain.”

### #3486: compare the optimized archive with a clean build

[#3486](https://github.com/google/zerocopy/pull/3486) adds a [seed-free reference build alongside the normal cache-seeded fast build](https://github.com/google/zerocopy/blob/a52492a733a1532aa36ebd6d3d38c72a5b1548c2/anneal/flake.nix).

It [compares](https://github.com/google/zerocopy/blob/a52492a733a1532aa36ebd6d3d38c72a5b1548c2/anneal/compare-toolchain-archives.py):

- the rewritten source tree;
- the toolchain;
- Lake build outputs;
- raw ILean reference usages;
- hash sidecars;
- stable trace dependency/output hashes; and
- the [normalized InfoView setup contract](https://github.com/google/zerocopy/blob/a52492a733a1532aa36ebd6d3d38c72a5b1548c2/anneal/v1/tests/integration.rs).

The expensive comparison [runs nightly rather than on every PR](https://github.com/google/zerocopy/blob/a52492a733a1532aa36ebd6d3d38c72a5b1548c2/.github/workflows/anneal-archive-equivalence.yml).

This gives us a useful correctness pattern:

> Optimize normal builds aggressively, but continuously compare the result against an independently constructed clean build.

That is stronger than merely checking that Lake accepts our cached state.

## What upstream Lake has already changed

The April discussion should not be treated as a permanent description of Lake.

[Lean 4.31](https://lean-lang.org/doc/reference/latest/releases/v4.31.0/) [moved compiled Lake package configurations from dependency-local `.lake/config` directories into the workspace's `.lake/config`](https://github.com/leanprover/lean4/pull/13683). This directly addresses the class of cross-workspace ownership problem that Anneal encountered: two workspaces can share a dependency without both trying to own that dependency's compiled configuration.

That change does not solve every problem above. In particular, it does not automatically provide:

- a relocatable frozen dependency graph;
- a read-only prepared package universe;
- portable configuration/build traces;
- an explicit producer/consumer archive format; or
- a guarantee that every server/build operation is non-mutating outside the workspace.

But we should distinguish current Lake requirements from workarounds that were necessary only for older versions.

## Possible future directions

I think there are several separable directions. We do not need to choose only one.

### 1. Make the current contract explicit and test it directly

Today much of the contract is implicit in the [archive builder](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/flake.nix) and [regression tests](https://github.com/google/zerocopy/pull/3453).

We should document one invariant:

> After setup, Anneal's installed toolchain is immutable. Any per-project or per-invocation state that Lake needs to mutate belongs to the generated workspace.

Then tests should deliberately enforce it for every Lake-facing operation we support:

- batch build;
- `lake env lean`;
- server setup / InfoView;
- clean and warm workspaces;
- repeated invocations;
- concurrent independent workspaces;
- relocated installations; and
- offline operation.

Where practical, run with the archive physically read-only rather than merely assuming code will not write to it.

### 2. Stop depending on mtimes as soon as Lake exposes a stronger freshness contract

[`--old` is useful because our archive builder knows that the shipped artifacts correspond to the shipped sources](https://github.com/google/zerocopy/pull/3444). We currently encode that knowledge partly by [arranging mtimes](https://github.com/google/zerocopy/pull/3443).

That is a weak transport for a strong fact.

Ideally Lake would support a mode like:

```text
use these existing artifacts if their recorded input identities match;
never rebuild or reconfigure dependencies;
fail if reuse is impossible
```

rather than requiring the producer to manipulate timestamps so that ordinary freshness heuristics reach the desired result.

Anneal could then stop treating mtimes as part of the archive format.

### 3. Give Lake an explicit “frozen dependency universe” interface

Our [generated relative `lake-manifest.json`](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/src/aeneas.rs#L340-L443) is currently the closest thing to this interface.

Anneal knows that its archive contains a fully resolved dependency graph. It should not need Lake to resolve that graph again.

A first-class Lake operation or manifest mode could mean:

- this graph is complete;
- every package already has a materialized source directory;
- package sources are immutable;
- no package may be downloaded or replaced;
- dependency configuration belongs to the consuming workspace;
- existing build products may be reused;
- missing/stale products either fail or build only into workspace-owned state, depending on policy.

That would turn the architecture established by [#3450](https://github.com/google/zerocopy/pull/3450) from an Anneal convention into a supported Lake contract.

### 4. Make prepared Lake artifacts relocatable

The archive has repeatedly encountered paths embedded in manifests and traces.

We have tried or currently use:

- [manifest rewriting](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/rewrite-lake-vendor.py);
- [relative path generation](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/v1/src/aeneas.rs#L340-L463);
- [trace-prefix rewriting](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/rewrite-lake-vendor.py);
- [install-time fixups](https://github.com/google/zerocopy/pull/3436);
- [package-index rewriting](https://github.com/google/zerocopy/pull/3341);
- [anonymous-package renaming](https://github.com/google/zerocopy/pull/3341); and
- [careful preservation of bytes that Lake hashes](https://github.com/google/zerocopy/pull/3485).

This is a strong signal that a reusable Lake package/build image wants a canonical relocation model.

Possible designs include:

- trace paths relative to a package/workspace identity rather than an absolute filesystem root;
- a relocatable placeholder understood by Lake itself;
- an explicit rebase operation which rewrites all affected metadata atomically; or
- a serialization format for prepared package state which is independent of its eventual extraction directory.

Anneal should not independently understand every path-bearing Lake artifact.

### 5. Separate producer state from consumer state in Lake's model

Anneal's archive builder is effectively a **producer**. Generated workspaces are **consumers**.

The producer wants to say:

```text
resolve this graph;
materialize these sources;
build these targets;
prepare server metadata;
package the reusable result.
```

A consumer wants to say:

```text
use exactly this prepared graph;
do not mutate it;
put anything project-specific here.
```

Making [those roles explicit](https://leanprover.zulipchat.com/#narrow/channel/236449-Program-verification/topic/Rust.20Verification.20.2B.20Lake.20Tooling/near/592313730) would clarify which `.lake` files belong in a distributable archive and which should never be shipped.

It would also simplify [Exocrate](https://github.com/google/zerocopy/tree/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/exocrate) and similar tools which want to distribute prebuilt Lean environments without becoming experts in Lake's internal cache layout.

### 6. Expose machine-readable reuse/fallback information

A successful Lake command does not tell Anneal whether it:

- reused the intended artifact;
- rebuilt it;
- restored it from a cache;
- reconfigured a package;
- cloned a dependency; or
- silently fell back to source.

For ordinary development these distinctions may be implementation details. For a verification tool distributing a prebuilt trusted environment, they matter.

A [structured event stream or final report](https://leanprover.zulipchat.com/#narrow/channel/236449-Program-verification/topic/Rust.20Verification.20.2B.20Lake.20Tooling/near/592313730) could let Anneal assert things such as:

```text
network accesses: 0
dependency resolutions: 0
dependency source writes: 0
dependency configurations rebuilt: 0
dependency modules rebuilt: 0
workspace modules built: N
```

This would make our regression tests much less dependent on filesystem inference.

### 7. Define the language-server preparation contract alongside `lake build`

[#3485](https://github.com/google/zerocopy/pull/3485) suggests that preparing a project for `lake build` and preparing it for editor/InfoView use are not identical operations.

If Lake considers the [language-server setup graph](https://github.com/google/zerocopy/blob/26fa0d68f318b987e7712a0c39729e9160e25d6e/anneal/prime-lakefile.lean) a stable concept, it may be worth exposing an explicit producer operation:

```text
lake prepare-server-artifacts ...
```

or an equivalent API.

A toolchain producer could run it once, archive the result, and later ask Lake to validate that the installed environment is complete.

This seems preferable to downstream tools discovering the necessary trace graph experimentally.

### 8. Keep the clean-build oracle

Even if Lake gains better APIs, [#3486's basic approach](https://github.com/google/zerocopy/pull/3486) is valuable.

The optimized producer path will always be more complicated than:

```text
start from sources
build everything cleanly
```

We should retain a periodic independent construction and compare the semantically relevant result.

The comparison should be narrow enough to tolerate intentionally non-semantic differences but broad enough to catch stale cached state. The current work on [source trees, ILean references, artifact hashes, and traces](https://github.com/google/zerocopy/blob/a52492a733a1532aa36ebd6d3d38c72a5b1548c2/anneal/compare-toolchain-archives.py), and [normalized InfoView setup](https://github.com/google/zerocopy/blob/a52492a733a1532aa36ebd6d3d38c72a5b1548c2/anneal/v1/tests/integration.rs), is a good foundation.

### 9. Re-evaluate which current workarounds modern Lake has made obsolete

Before adding more Anneal-side machinery, test the [current pinned Lake version](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/flake.nix) against each historical workaround.

In particular:

- Is [local-Git indirection](https://github.com/google/zerocopy/pull/3304) still necessary now that [package configuration is workspace-owned](https://github.com/leanprover/lean4/pull/13683)?
- Which inputs still require `--old`?
- Which [trace-prefix rewrites](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/rewrite-lake-vendor.py) remain necessary?
- Can current Lake consume a read-only path dependency graph directly with only a locked root manifest?
- Which package/config artifacts must actually be present in the archive?
- Does current server setup still require the [trace priming that #3485 implements](https://github.com/google/zerocopy/blob/26fa0d68f318b987e7712a0c39729e9160e25d6e/anneal/prime-lakefile.lean)?
- Can the dedicated artifact cache replace any of the archive's copied build state without reintroducing mutable shared paths?

We should delete obsolete complexity rather than preserving it as folklore.

## A useful target architecture

The simplest end state I can see is:

### Toolchain build

Lake (or a thin supported API around Lake):

1. resolves the dependency graph;
2. materializes sources;
3. builds the dependency closure;
4. prepares editor/server metadata;
5. emits a relocatable, immutable description of the prepared environment.

Nix packages that result without understanding Lake's internal trace format.

### `cargo anneal setup`

Exocrate:

1. downloads the archive;
2. verifies it;
3. extracts it atomically; and
4. leaves it read-only.

No Lake-specific fixup should ideally be necessary here.

### Verification

Anneal:

1. generates its project-local Lean files;
2. creates a small mutable Lake workspace;
3. points that workspace at the prepared environment;
4. invokes Lake/Lean;
5. fails if Lake would need to resolve, download, mutate, or rebuild the immutable dependency environment.

All state produced specifically for that verification remains below the generated workspace.

### Validation

CI:

1. exercises the above with an actually read-only archive;
2. exercises multiple workspaces concurrently;
3. exercises editor/InfoView setup;
4. exercises archive relocation and offline use; and
5. periodically compares the optimized prepared environment with a clean source build.

This architecture preserves what [#3450](https://github.com/google/zerocopy/pull/3450) got right while removing Anneal's need to understand more and more of Lake's internal serialization.

## Concrete next steps

On the Anneal side:

- [ ] Document the immutable-toolchain / mutable-workspace contract.
- [ ] Land or otherwise resolve the [#3485 server-setup work](https://github.com/google/zerocopy/pull/3485).
- [ ] Land or otherwise resolve the [#3486 clean-build equivalence oracle](https://github.com/google/zerocopy/pull/3486).
- [ ] Add an explicit concurrent-many-workspaces regression if we no longer have one exercising the current architecture.
- [ ] Test relocation and network isolation explicitly.
- [ ] Inventory every remaining Lake metadata rewrite in [`flake.nix`](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/flake.nix), [`rewrite-lake-vendor.py`](https://github.com/google/zerocopy/blob/ec74bc161ec76c43a7f298a1f8bd98fafb6ea51e/anneal/rewrite-lake-vendor.py), and related setup code and record the precise Lake behavior that requires it.
- [ ] Re-test those requirements against the currently pinned Lean/Lake revision and delete obsolete workarounds.

With the Lake maintainers:

- [ ] Agree on the intended way to distribute a pre-resolved, prebuilt, read-only dependency universe.
- [ ] Determine whether a complete locked manifest plus read-only path dependencies is intended to be that interface.
- [ ] Discuss replacing mtime-driven `--old` reuse with an explicit “reuse or fail” policy.
- [ ] Discuss a relocatable representation for traces/configuration/build state.
- [ ] Discuss a supported producer/consumer boundary for prebuilt Lake environments.
- [ ] Discuss machine-readable reporting of cache reuse, rebuilds, configuration, resolution, and network fallback.
- [ ] Include language-server/InfoView preparation in that design rather than treating it as a separate downstream reverse-engineering problem.

The goal is not to make Lake special-case Anneal. The goal is to identify a [general interface for tools that want to prepare a Lean dependency environment once and consume it many times](https://leanprover.zulipchat.com/#narrow/channel/236449-Program-verification/topic/Rust.20Verification.20.2B.20Lake.20Tooling/near/592135972), cheaply and read-only.

Anneal has implemented enough versions of that interface itself that we now have concrete evidence for what it needs.

Start with anneal/flake.nix, anneal/v1/src/aeneas.rs, anneal/v1/tests/integration.rs, and anneal/src/main.rs to trace archive creation and workspace consumption. Then read rewrite-lake-vendor.py and prune-lake-cache.py alongside the linked integration work. Done means the Lake contract, ownership boundaries, and remaining Anneal machinery are explicitly documented and actionable.

Written by the indexing model from the issue text.