Cache pinned Lean dependencies without weakening formal qualification

[bordumb]

Problem

The PR formal-translation implementation job routinely takes 90–100 minutes even when the pinned Lean dependency graph has not changed.

Measured successful run: 31985090743 / job 95259249353

Stage	Duration
Build pinned Aeneas and Charon	10m41s
Reproduce/update and qualify the translation	73m25s
Semantic and bounded post-checks	10m30s
Install Lean itself	10s
Whole job	96m55s

A second successful run showed the same shape: roughly 11 minutes for Aeneas/Charon, 70 minutes for qualification, and 11 minutes for post-checks.

The Lean installer is not the problem. The workflow restores no formal/.lake dependency build cache. The lake build nested inside qualification therefore recompiles pinned Mathlib and transitive dependencies on a fresh runner. In a representative checkout, formal/.lake is 7.9 GiB; Mathlib accounts for 6.9 GiB, including 6.4 GiB of compiled build output, while Auths' own Lean build output is about 166 MiB.

Relevant code:

• .github/workflows/ci.yml: formal-translation-run
• .github/actions/setup-lean/action.yml: installs Lean but restores no Lake/Mathlib artifacts
• xtask/src/formal_qualification.rs::qualify: deliberately performs two complete translation reproductions
• xtask/src/formal.rs::build_and_audit_formal: invokes lake build
• xtask/src/formal.rs::run_formal_semantic_checks: runs vectors, Rust refinement tests, and Kani after qualification

Goal

Reduce warm PR formal-translation time substantially without weakening:

• two byte-identical Charon/Aeneas reproductions;
• compilation of the current Auths/generated Lean sources;
• the compiled assurance audit;
• exact pinned Lake dependency identity and clean-worktree checks;
• Rust refinement vectors and the complete Kani harness inventory; or
• protected release evidence.

Recommended design

1. Add a trusted Lean dependency cache

Cache only the pinned third-party Lake package tree and its compiled dependency outputs, initially:

formal/.lake/packages

Do not cache:

• formal/.lake/build (Auths' own proof output);
• formal/qualification/aeneas/generated/**;
• qualification evidence;
• source-closure output; or
• any generated Auths semantic vector.

Use an exact cache key containing:

• cache schema version;
• runner OS and architecture;
• hash of formal/lean-toolchain;
• hash of formal/lake-manifest.json; and
• hash of formal/lakefile.toml.

Use no prefix/fallback restore keys.

2. Make cache provenance fail closed

PR jobs may restore the dependency cache but must never publish or overwrite it.

Only a protected default-branch or dedicated trusted workflow may create the cache, and only after a successful cold formal build from the pinned sources. A release/scheduled qualification must retain a cold-build path.

On restore:

• validate every git dependency HEAD against lake-manifest.json;
• reject dirty dependency worktrees;
• record cache key, hit/miss, producer/provenance, and dependency identity in the job summary/evidence;
• ignore or fail a cache whose exact identity does not match; and
• demonstrate with a mutation test that changing the Lean toolchain or any Lake manifest revision causes a miss.

If GitHub Actions cache provenance cannot be made sufficiently strong for imported .olean files, use a signed repository-controlled artifact, OCI image, or Cachix product created by the trusted cold-build workflow instead. Do not silently make a mutable PR cache part of the proof trust base.

3. Cache the pinned translation tools separately

The exact Aeneas/Charon Nix build currently costs another 10–12 minutes per run despite the public substitute. Publish the exact Nix derivation to a repository-controlled signed Cachix cache, or an equivalent immutable verified artifact, keyed by the pinned commits in formal/translation-toolchain.lock.

Keep the existing version and commit checks.

4. Expose internal timing

The 70+ minute qualification step currently hides several different costs. Report separate durations for:

1. Charon/Aeneas reproduction 1;
2. Charon/Aeneas reproduction 2;
3. output comparison and synchronization;
4. lake build;
5. assurance audit;
6. qualification cases;
7. Rust refinement tests; and
8. each Kani package.

Include cache hit/miss and transferred size in the step summary.

Security constraints

• Do not enable RUSTC_WRAPPER or sccache for Charon extraction; the formal environment deliberately rejects compiler wrappers and semantic Cargo environment overrides.
• Do not reduce the two reproduction passes to one.
• Do not skip lake build, the assurance audit, or Kani on a cache hit.
• Do not trust a cache created by pull-request code.
• Do not use broad restore keys that could select a different Lean or dependency graph.
• Do not let cached third-party output prevent current Auths/generated Lean files from compiling.
• Preserve a cold protected/release build so cached PR checks are not the sole evidence.

Acceptance criteria

• A warm PR run does not rebuild Mathlib or transitive Lake dependencies from source.
• The PR job restores only an exact, trusted cache and cannot save it.
• A cache miss performs the existing cold build and remains green.
• Changes to lean-toolchain, lake-manifest.json, or lakefile.toml cannot reuse the old cache.
• Dirty or wrong-revision dependency worktrees still fail before assurance succeeds.
• Auths' own Lean project and freshly generated Aeneas files are compiled on every formal run.
• Both translation reproductions, byte comparison, assurance audit, refinement tests, and complete Kani inventory still run.
• A protected scheduled/release path performs a cold dependency build from pinned source.
• Cache provenance and detailed phase timing are present in uploaded formal evidence or the job summary.
• Mutation tests protect the restore-only PR boundary, exact cache key, and cold release path.
• Warm-job timing improves by at least 30 minutes over the approximately 97-minute baseline, with before/after measurements recorded.
• Existing workflow-structure and formal-boundary tests prevent later weakening of these constraints.

Non-goals

• Changing theorem statements or formal semantics.
• Hand-editing generated Aeneas output.
• Removing clean reproducibility.
• Making ordinary PR caches a new unaudited trust root.
• Optimizing the 10-second Lean installer or 12-second Kani installer before the dominant costs are fixed.