Anneal tracking issue

## Milestones

### Milestone 1

In a dummy project that lives in the Anneal directory in the repo, prove the panic-freedom of a single, small codebase. Enforce this in CI.

### Milestone 2

Land a single annotation in zerocopy, enforced in CI

## Workstreams

### Workstream A: Prepare for external contribution

Get the implementation and infrastructure into a state where external contributors can:
- Easily navigate the codebase
- Be assured that code will not undergo radical restructuring over the short term
- Add code/tests and be confident that CI infrastructure will prevent bugs or regressions
- Work quickly (ie, `cargo anneal` subcommands execute quickly)

#### Tasks
- Prevent Lake from re-downloading (source) or re-building anything
- Figure out where (if anywhere) to use Docker vs non-Dockerized workflows for local dev/CI
- Reduce work done during `cargo anneal setup`
- Pre-build as much as possible in CI and host as artifacts on GitHub
- Prune Mathlib artifacts so we only download/install what is needed

### Workstream B: Formalizing Rust programs "manually"

Use `cargo anneal expand` or `cargo anneal generate` as the starting point. Given `.lean` files, iterate in situ. Experiment to figure out what Lean code we eventually want Aeneas and Anneal to be able to auto-generate.

### Workstream C: Aeneas support for separation logic

### Workstream D: User-facing syntax

- How do users write Anneal annotations?
- How do users write proofs?
- Where do proofs live?
- Can users write annotations in Rust syntax?

### Workstream E: Internal code organization

- Rewrite code generation (`src/generate.rs`) using a Lean macro