Vincent Laporte

This is certainly a bug in `toEC.ml`. I’ve proposed a fix in #229. Tiago, can you please double-check that it solves your current issue?

Thanks for testing. Indeed, you’ll need to specify the `randombytes` system calls in EasyCrypt (contributions to `eclib/` welcome!).

Well spotted. There is at least a weird behavior in register-allocation: variables `res` (first argument of `#ADD_64`) and `test` (result of the same) are merged (due to architectural constraints) but...

The instructions descriptors should be slightly redesigned to explicitly document what sizes they support: currently this information is spread in the instruction syntax, semantics, parsing rules etc. Would it also...

In this case, the annotation is not ignored. It qualifies the argument to the intrinsic (here expression “x”). The result is always a `u128`, hence the error message. If the...

I’ve tried to improved on this in f4decb8bb00eddd237093cb3e3a36699fbb02bbb (branch `glob_array3`).

Exactly, I just moved things around. Many of these proofs indeed need to be reworked and the compiler-proof file is a big work-in-progress (in that branch).

Is this still relevant?

This also prints the “usage” help message; is this expected?

Also, do not forget to rebase on top of a recent version of `main`.