Macros: preconditions that generates an debug_assert!

[W95Psp]

We would like a specialized version of hax_lib::requires that also inserts at the top of the function a assert_debug.

Having this as a separate version let the users write non-Rust code in the hax_lib::requires clauses (e.g. something that would break borrow checking or something that uses fstar!). In the debug version, the user can write only valid Rust code.