Add unsafe versions of inlining macros

[W95Psp]

Closes #825.

(note: replace BACKEND by fstar, coq, etc. in the text of this PR)

This PR:

• adds hax_lib::inline_unsafe function, hidden in documentation, that allows to inline BACKEND code of any type directly as an expression. This is an internal function, it not supposed to be used directly. It exists only when compiling through hax (see my last reverted commit). The body of this function is an unreachable!.
• adds a hax_lib_macro:BACKEND_unsafe_expr macro (exposed as hax_lib::BACKEND_unsafe_expr, hidden in doc) which leverages inline_unsafe to produce inlined BACKEND code of any type.
• exposes hax_lib_macro:BACKEND_unsafe_expr locally as BACKEND in pre and post conditions. Thus we can use e.g. fstar!("forall x. ...") in ensures and requires clauses.
• Disallow future(...) within a quote (e.g. fstar!("... ${future(arg)} ...")): due to the way macros expand in a fixed sequence (the fstar!("...") expands after requires expands, so the requires macro cannot rewrite future nodes in "..." -- note that will be the same thing, but with old instead of future, when Pre/post &mut argument: remove future in favor of old #773 will be fixed)
• adds tests

Example of what you can do:

/// `ensures` and `requires` with inlined code (issue #825)
mod inlined_code_ensures_requires {
    #[hax_lib::requires(fstar!("forall i. FStar.Seq.index $v i <. ${254u8}"))]
    #[hax_lib::ensures(|()| {
        let future_v = future(v);
        fstar!("forall i. FStar.Seq.index ${future_v} i >. ${0u8}")
    })]
    fn increment_array(v: &mut [u8; 4]) {
        v[0] += 1;
        v[1] += 1;
        v[2] += 1;
        v[3] += 1;
    }
}

https://hax-playground.cryspen.com/#fstar/88b4821690/gist=49d80be217020e9fd41f9e0a6a23714e

[karthikbhargavan]

Very useful, but it croaks when you use hax_lib::fstar instead of fstar in the requires/ensures. Would this be easy to fix?

I see that future cannot be used within F*, which may also be confusing for people. In a future PR, let's figure out the recommended style for this, once we have some experience.

[W95Psp]

Thanks!

• for future, it is OK to use it with fstar!, you just need to put it in a let (the macro signals that to the user, if you fstar!("${future(x)}"), you get a message saying you need to put future(x) in a let binding an use the binding instead of future(x) directly, see https://hax-playground.cryspen.com/#fstar/88b4821690/gist=9b5b4923c0717cca519a323176fbe2b3)
• I could make it work for hax_lib::fstar, but it is going to be a bit odd. Maybe I should rename the local fstar! of ensures/requires to something else?