Jonathan Protzenko

I also forgot to mention that dist/gcc-compatible/configure is auto-generated and that you should edit this one but also dist/configure (the reference one)

@CraigFe anything I can do to help with this?

@CraigFe hey, I was wondering if you had had any chance to make progress on this? we're hoping to switch the build of kremlin itself to dune, and there's a...

I see that https://github.com/ocaml/dune/pull/3905 was merged and there is now very nice documentation here: https://dune.readthedocs.io/en/latest/foreign-code.html#ctypes-stubgen Is there any chance we could try to use this to simplify our build?

@beurdouche I took a look and I couldn't see the non-null precondition here: did you find it somewhere? https://github.com/project-everest/hacl-star/blob/master/code/chacha20poly1305/Hacl.Impl.Chacha20Poly1305.fst#L151 I should have given an update on this: we took a...

I agree that adding a disclaimer for now pointing to this issue would be good. Apologies once again for not responding: I was leading a big effort to try to...

I found a copy of the message I had written on Slack -- apparently I had saved it somewhere knowing it would eventually disappear. I'm pasting a copy for reference...

Yeah, I guess a hotfix for hashes would be good, too, actually. Do you have an exhaustive list of all the places where this specific UB happens?

Thanks Maamoun, that's really neat! To follow up on this: - can you attach a patch for the generated C code so that we can see precisely what needs to...

Thanks @mamonet that looks great. Just to clarify, do you plan on submitting PRs that implement these two changes or are you just filing bugs in the hope that someone...