Create a Boogie AST crate

[zhassan-aws]

Description of changes:

Introduce a Boogie AST crate and translate a small subset of MIR to Boogie. The current translation can handle simple programs involving integers and booleans and asserts (using kani::assert), e.g.:

#[kani::proof]
fn main() {
    let x = true;
    kani::assert(x, "");
}

and

#[kani::proof]
fn main() {
    let x = 1;
    let y = x;
    kani::assert(y == 1, "");
}

Resolved issues:

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

I've been testing the output by running it with boogie manually. The next step would be to install boogie as part of the setup process and run it on the output file via a script.

Testing:

• How is this change tested? Testing manually for now

• Is this a refactor change? No

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

Thanks for working on this. When do you think you'll be able to add a few tests?

[zhassan-aws]

When do you think you'll be able to add a few tests?

I've been testing this manually on a few small programs via running Boogie on them locally.

I looked into adding a script that installs Boogie, but found out that it'll take some effort because of the need to install .NET, so I decided to push this to a future PR.

It should be possible to add tests for the writer though, which I can do in this PR or a follow-up one.

[celinval]

Mostly some code cleaning suggestions, but not blockers.