Add Basic hax extraction setup

[jschneider-bensch]

Hi,

I think I can't push to your PR branch directly so I'm making a PR for your fork instead.

This PR adds a minimal setup for running hax release 0.3.6 on the kmac crate to extract everything to F*.

After you've installed hax (let me know if you need help in setting up hax), you can run

./hax.py extract

to extract the kmac Rust source to F*. Once you've done that, you can run the F* typechecker on the extracted code with

./hax.py prove

If that succeeds without errors then you've shown that the code you extracted does not panic. As it is now, the extraction will work (I commented out two unsupported const blocks), but F* typechecking will fail. There can be different reasons for the typechecking step to fail, most often the following:

1. Your code uses something that is not supported by the F* library that comes with hax, i.e. you'll have a Identifier not found or similar in the output of ./hax.py prove. In this case you can either try to write thing you want to do in a different way on the Rust side, or get in touch about if/how we can extend the hax F* lib.
2. F* can't determine that your code is free of panics, because the necessary pre-conditions are not met everywhere. This means e.g. you have a function with an addition

fn add(a: u32, b: u32) -> u32 {
    a + b
}

but you don't state bounds for a and b that let F* determine that their sum would not overflow u32 which would lead to a panic.
You can add a sufficient pre-condition like so

#[hax_lib::requires(a <= u32::MAX - b)]
fn add(a: u32, b: u32) -> u32 {
    a + b
}

Afterwards you have to run ./hax.py extract and then you can try your luck again with ./hax.py prove.

There are more things to consider, such as which parts of your code you really want to be extracted to F* and which parts should be excluded, but we can look into that once you feel somewhat comfortable with the basic setup.