Tiago Oliveira

> CI is happy. Let’s wait for feedback from Jasmin users. @vbgl @bgregoir, I did some experiments on libjade. I explain the procedure first, and then the results. 1. compile...

After reading this issue I ran some experiments on `compiler/examples/`. You can find some files attached to this message. I extracted each function from each file under this directory (at...

I was about to report the same issue and found this one. To replicate it on libjade: - branch dsprenkels-dilithium (https://github.com/formosa-crypto/libjade/tree/dsprenkels-dilithium) - running `make extract_ct` on `src/crypto_sign/dilithium/dilithium3/amd64/ref` - causes the...

Yes, it does fix the described issue. Then I get `[critical] [sign_ct.ec: line 5788 (11-28)] unknown function: SC.randombytes_32` when running `easycrypt sign_ct.ec` but that is for another topic, I believe.

Hi @vbgl, thanks for the corresponding PR. I just pushed the same modifications for sha256. CI should be green for that example during the afternoon. I also increased the timeout...

Another question, by running `jasminc --help`: ``` -checksafety : automatically check for safety -safetyparam parameter for automatic safety verification: format: "f_1>param_1|f_2>param_2|..." where each param_i is of the form: pt_1,...,pt_n;len_1,...,len_k pt_1,...,pt_n:...

> With `-safetyparam "jade_xof_shake256_amd64_spec>output,input;output_length,input_length"`, the result is more precise (and as fast). Do you know if it is possible to specify the information from the cmd line argument `jade_xof_shake256_amd64_spec>output,input;output_length,input_length` within...

> PR #312 should fix the assertion failures. Thanks!! I updated the CI machine and I will give it a try

If this is the case, I can integrate it as it currently is (using `-safetyparam` option and corresponding syntax), and then I will update the Makefiles/scripts when necessary. Meanwhile, could...

Hi, I merged the safety branch from libjade into the main branch (there's still some work to do regarding parameter generation for the `-safetyparam` option, based on the contents of...