proto: integrate with Aeneas

[mkovaxx]

DO NOT MERGE
Only for comparison.

[mkovaxx]

@oliver-butterley Here's the summary of this first iteration.

Given a function with a spec like this:

#[spec(
    requires: [
        n > 0,
        n < 42,
    ],
    ensures: *output == 1,
)]
pub fn collatz(n: int) -> int {
    todo!()
}

The following two other functions are generated to embed the spec:

pub fn __anodized_fn_requires_collatz(n: int) -> bool {
    let __anodized_clause_1 = (|| -> bool { n > 0 })();
    let __anodized_clause_2 = (|| -> bool { n < 42 })();
    __anodized_clause_1 && __anodized_clause_2
}

pub fn __anodized_fn_ensures_collatz(n: int, __anodized_output: &int) -> bool {
    let __anodized_clause_1 = (|output: &int| -> bool { *output == 1 })(__anodized_output);
    __anodized_clause_1
}