Support writing Anneal specifications in Rust

Lower to Lean using Charon/Aeneas and treat these as equivalent to specifications written directly in Lean.

Possible examples, using the `anneal, rust` info string to denote specs written in Rust.

```rust
/// ```anneal, rust
/// is_valid = |p| p.x > 0
/// ```
struct Positive {
x: usize,
}

/// ```anneal, rust
/// is_safe = std::mem::align_of::() == 1
/// ```
unsafe trait Unaligned {}
```