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.
/// ```anneal, rust
/// is_valid = |p| p.x > 0
/// ```
struct Positive {
x: usize,
}
/// ```anneal, rust
/// is_safe = std::mem::align_of::<Self>() == 1
/// ```
unsafe trait Unaligned {}
Lower to Lean using Charon/Aeneas and treat these as equivalent to specifications written directly in Lean.
Possible examples, using the
anneal, rustinfo string to denote specs written in Rust.