Hax-lib[-macros]: cfg(hax), cfg(debug_assert) and release mode policy

[W95Psp]

hax-lib and hax-lib-macros provide hax-related features that are relevant only when extracting though hax (and maybe in some scenarios in debug mode, but this is not entirely clear yet)

The constraint here is production code. When we introduce a dependency to hax-lib in production code, we want (if not cfg(hax)):

• as few as possible dependencies (from hax-lib);
• all macros from hax-lib should be no-ops.

Solution: add a dummy hax-lib-dummy crate that is an empty shell, providing the same interface to hax-lib, but with macros being no-ops. Then hax-lib, with a cfg, either includes the real library or the dummy one.

Actions:

• Rename hax-lib into hax-lib-impl, move it inside a brand new hax-lib crate
• Create a hax-lib-dummy crate
• Make hax-lib expose either the dummy one or the lib one
• Move all docstrings to external files so that the dummy and impl crate have the same documentation
• Feature-gate the refinement_type macro
• Ensure correct handling of bounded integers (Bounded integers #642)

Note: some work exists in wip-toward-639

[franziskuskiefer]

Putting this into separate crates requires publishing both, hence more complexity.
How about clearly separate modules instead of different crates?

[github-actions]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

Still needed

[W95Psp]

I´'ve been looking at that the last two hours or so:

• we need two crates for hax-lib-macros: a real one and an impl one. We can't do two modules included conditionally: macros need to live in the top level module.
• I'm not sure yet about what to do with the refinements. In hax-lib-macros, we have refinements and ints.
  • we should have a feature refinement and a feature int
  • in the dummy crate, such macros should generate simple wrappers, or maybe type synonym
• I use cargo-public-api to make sure hax-lib[-macros] dummy VS non-dummy expose the same API
• I opened a draft PR there feat(hax-lib): intro. hax feature #983