proto: integrate with Hax

[mkovaxx]

The main purpose of this PR at this point is to enable discussion over concrete prototype code.

[mkovaxx]

@maximebuyse I think this is getting pretty close.

All the following items used in the hax.rs example are now provided by anodized:

• implies!
• forall
• opaque! (to allow passing through "uninterpreted" expressions to specific backends)
• loop specs are now actually on the for/while

Remaining TODO:

• transform expressions before emitting Hax attributes:
  • forall to ::hax_lib::forall
  • implies! to ::hax_lib::implies
  • unwrap opaque! expressions
  • transform loops to inject loop_invariant/loop_decreases

Are we missing anything?

[maximebuyse]

@maximebuyse I think this is getting pretty close.

All the following items used in the hax.rs example are now provided by anodized:

* `implies!`

* `forall`

* `opaque!` (to allow passing through "uninterpreted" expressions to specific backends)

* loop specs are now actually on the `for`/`while`

Remaining TODO:

* transform expressions before emitting Hax attributes:
  
  * `forall` to `::hax_lib::forall`
  * `implies!` to `::hax_lib::implies`
  * unwrap `opaque!` expressions
  * transform loops to inject `loop_invariant`/`loop_decreases`

Are we missing anything?

@mkovaxx Great! I pushed a small commit to make sure we produce the right calls to the hax macros (limited to the cases of function and trait contracts for now). We can refactor to limit the number of if blocks needed. Something similar needs to be done for loop annotations (but this is already in your list).

For now I am testing by running RUSTFLAGS="--cfg anodized_hax" cargo hax into fstar on a crate containing basically the rust that is added as a test here.

I think your list would cover most of what we need. There will still be a few things missing like refinement types but we're also refactoring our annotations so we'll see what we do with this feature.

[mkovaxx]

@maximebuyse I've refactored this a bit, introducing an anodized_discard_specs setting, which turns spec embedding off, so the Hax-specific guards are no longer necessary.

[mkovaxx]

@maximebuyse The transforms to handle quantifiers, loops, and opaque expressions are now implemented. Please give it a try!

Remaining TODOs:

• implies!(a, b) desugars to if a { b } else { true } internally, which might not work with Hax.
• && and || probably need to be replaced with bitwise ops for Prop to work.

[maximebuyse]

@maximebuyse The transforms to handle quantifiers, loops, and opaque expressions are now implemented. Please give it a try!

Remaining TODOs:

* `implies!(a, b)` desugars to `if a { b } else { true }` internally, which might not work with Hax.

* `&&` and `||` probably need to be replaced with bitwise ops for `Prop` to work.

@mkovaxx Great! I tried quickly and:

• Quantifiers work great!
• I now need to pass the anodized_discard_specs cfg, I imagine this is expected, the cfgs will be inserted by hax itself eventually anyway
• I have a small issue with loop invariants. My example is the following:

pub fn f_loop(x: &[u8]) -> u8 {
    let mut max = 0;
    #[spec(
        maintains: forall(|j: usize| implies!(j < i, x[j] <= max)),
    )]
    for i in 0..x.len() {
        if x[i] > max {
            max = x[i]
        }
    }
    max
}

Here rust cannot infer the type of i in the loop invariant. When we use hax_lib directly we can annotate the closure parameter (hax_lib::loop_invariant!(|i: usize| ..)). One possible way to solve this would be to allow passing a closure instead of an expression (like for post-conditions):

#[spec(
      maintains: |i: &usize| forall(|j: usize| implies!(j < i, x[j] <= max)),
)]
for i in 0..x.len() {
..
}

I imagine we need to take a reference here to make it work with rutnime checks as well, but this can work for hax too.

[mkovaxx]

@maximebuyse Thanks for trying it out and writing down the feedback! :)

I've made the changes so that a for loop's invariants can now be written as closures.

In the long term, I hope that we'd be able to simplify the surface language syntax so that a loop invariant is always a bare expression (as opposed to a closure).

I think moving integration deeper (to Hax's rustc_driver, as opposed to the shallow source-to-source transforms of this prototype) would allow lowering a bare expression into the closure form Hax needs internally, by having access to not only the pattern but also to type information (from THIR), etc.

Can you think of anything about the semantics of Hax's loop invariants that might prevent simplifying the surface language like that?

[maximebuyse]

@mkovaxx Thanks! I'll try this. Closures for loop invariants can be confusing so accepting bare expressions would be an improvement. I think the processing of invariants in the hax engine could recognize the loop index and reconstruct a closure (doing it in the frontend/rustc_driver seems more fragile and we want it to work through charon as well).

[mkovaxx]

@maximebuyse Integrating with Charon is something I'm also considering. I think we could prevent duplicated effort by extending Charon with a notion of specs. I'll allocate some time to build a prototype! :)

CC @Nadrieril

[Nadrieril]

I'm open to that! Do note that a solution based on THIR can't work in Charon, as that would prevent fetching specs from foreign crates.