Aymeric Fromherz

I'm no expert in cryptography, so I'm not sure I understand perfectly what happens if the scalar is out of bounds (even if the mathematical behaviour is specified in Spec.DH)....

As far as I understand, this `pow` is not just a `pow2`, it takes two arguments `a` and `b` and performs `a ** b`. It indeed seems to be called...

Regarding maximum input length, I had started around a week ago, but I was preempted and it still needs some more work. I'll look at it in the next few...

@ad-l , I pushed a change to fstar-master that doesn't restrict the length of the input or output for the Vale AES-GCM, which should address points 1 and 2. Let...

Thanks for the heads-up about this. The issue stems from an incorrect invariant that we assumed for the Z3 generation: We previously thought that any EMatch would be returning a...

While several components are still not or partially supported, the current encoding is sufficient to handle all variables from the "allocations_familiales" example. I'd suggest extending the current support for the...

@mamonet There were some CI failures due to recent changes in F*, which were fixed in the main branch of HACL*. Could you please merge main in your branch, which...

@mamonet I was looking at the extraction part more deeply today because of another issue (#625) Is the assembly syntax that you are printing OS-independent? Also, as far as I...

Great thanks. Since Linux distros are the target, this means that we will also need to add `.section .note.GNU-stack,"",%progbits` in the generated .S (see https://github.com/cryspen/hacl-packages/issues/196), correct? If so, I can...

My concerns were about reporting errors if, for instance, you print a term inside F* with some options enabled (--ugly, --print_universes for instance) and try to parse it again using...