Reduce single-problem evaluation latency without weakening the sandbox

[kim-em]

Problem

The production launch canary's single-problem evaluation spends roughly 42 minutes inside the sandboxed workspace build. This is launch-path latency, not theorem checking or nanoda latency.

Measured on staging run 33577385219, job 100099543632:

• evaluate_submission.py began at 01:03:06 UTC.
• lake update plus lake exe cache get finished around 01:03:21; the cache reported no downloads and 8,691 files already decompressed.
• The trusted evaluator/tool build finished around 01:03:47.
• The sandboxed generated-workspace build then traversed about 8,709 jobs and completed around 01:44:50.
• The official Lean-kernel and nanoda acceptance checks completed essentially immediately afterward.

The production canary in run 33588498880 is showing the same phase shape. Do not cancel or restart that run for this issue.

Desired outcome

Reduce ordinary one-problem submission latency substantially while preserving the current trust boundary:

• never precompile Submission.lean or any target transitively importing it outside landrun;
• retain comparator's theorem-match check;
• retain both the official Lean kernel and nanoda checks;
• retain the network-denied sandbox and environment allowlist probes;
• do not reintroduce persistent qualification machinery or make historical replay a launch dependency.

Suggested first investigation

Profile why the per-problem workspace does not cheaply reuse the already-restored Mathlib artifacts despite the shared .lake/packages tree and successful cache restore. Compare the live GitHub Actions workspace layout with the authoritative replay image's preprimed workspace layout. Any proposed cache or prebuild must document why it cannot include attacker-controlled Submission imports.

Definition of done

• A representative accepted one-problem submission is benchmarked before and after.
• The slow phase is identified with timestamps or comparator phase metrics.
• The improvement is covered by focused tests and the existing sandbox probes.
• Security documentation is updated if the trusted/precompiled boundary changes.

This is an internal performance follow-up and should not delay the already-running production launch canary.