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.

Great timing of the bot, this should also go on https://github.com/cryspen/home/issues/95 I suppose @W95Psp

Basic support was added in #867.
I suppose now the question is: what do we do with unsafe blobs? Shall we just extract them as is? That's probably fine, unsafe is just a marker, at the end, performing an unsafe operation resolve to (1) calling unsafe functions or (2) raw pointers. We still reject raw pointers right away, and unsafe functions are just normal functions that usually make strong assumptions, which we can model precisely with strong preconditions

I wonder if we should just turn the unsafe feature on in the F* backend then. Wdyt @franziskuskiefer?

Sure, let's turn it on for F* and see what happens.
Is more needed than the basic support? If so, please update the issue on what remains unsupported and what's supported. If not, let's close this.

No, more advanced support would mean library support in the backends, so we should close that issue.
Ok! Will push a PR, it's gonna be a very small PR.