Tracking: Anneal interactive proofs

We have two conflicting goals:
- Write specifications and proofs inline in `.rs` files
- Enable interactive proving (for humans via IDEs and agents via MCPs or similar)

There are two problems with supporting specifications and proofs inline in `.rs` files:
- Existing interactive tools (the Lean LSP server, the Lean REPL, etc) do not work on `.rs` files
- The `.rs` files don't contain the full expansion of the `.rs` code, meaning that humans/agents need to mentally model the expansion that Aeneas and Anneal are performing in order to understand how edits to `.rs` Anneal annotations correspond to the underlying `.lean` files

## Progress

- [ ] Write agent instructions for using `cargo anneal verify --allow-sorry` to extract `.lean` files, iterate on `.lean` files directly, and then copy complete proofs back to `.rs` files
- [ ] ???
- [ ] TODO: Some sort of LSP passthrough and REPL passthrough for IDE integration and MCP