Make entire Anneal annotation a single Lean AST?

Currently, Anneal annotations have the following structure:

```
:
:
:
```

E.g.:

```
requires: x > 0
ensures: ret > 0
```

Each `` block is mapped verbatim into a `.lean` file, but there is extra scaffolding *between* different `` blocks. We've found that agents find this mapping confusing, and that it's a leaky abstraction (reasoning about how to write a Anneal annotation requires understanding the "hidden" parts of the mapping).

Instead, what if we made the entire annotation a *single* Lean AST? We already have `Pre` and `Post` structures for pre-conditions and post-conditions. Perhaps we could combine these into a single `Spec` structure, along with proofs, and have the Anneal annotation simply be an instantiation of `Spec`.