Jonathan Protzenko

I should mention that the error started happening after we upgraded GCC (specifically: mingw) to version 9. We were previously on version 7 and there was no trouble.

Just coming back to this issue after a long while... Are we positive that this is a GCC bug? I can't tell from the previous discussion what the "misbehavior" might...

Your solution seems fine to me @dra27 -- do I understand you correctly that we need both `HAVE_INT128` and `-O0`? Definitely something fishy going on here but I agree that...

@Chris-Hawblitzel you've been working on AES specifications; do you have one already for AES-256, or could you tell us whether this one looks fine?

EverCrypt only exposes the CTR block function. It exposes neither the raw keystream, nor a complete ctr encryption.

My understanding is that you can remove nodes from the beginning of the tree but not at arbitrary positions. Maybe @wintersteiger or @fournet could confirm.

Thanks for the separate PR and the compilation error. So, the Intel manual says this intrinsic is found in nmmintrin.h https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_cmpgt_epi64&ig_expand=1038 I do have nmmintrin.h on both my Linux and...

That's a corresponding F* issue: https://github.com/FStarLang/FStar/issues/432 ... basically, this would have to be a manual wrapper generated by hand, as not all preconditions can be automatically converted by the F\*...

> Thanks for the very rapid response :-) Of course! > > I suppose the way forward is for me to try to port the Dune generation logic to KreMLin...

> I initially wasn't sure how closely linked the two projects are / how problematic it is to need to release them in lockstep There's a way to make your...