assert false in CT extraction

[eponier]

The following program

export fn main (reg u64 i) {
  stack u8[2] a;

  a[1] = i;
}

triggers

Fatal error: exception File "src/toEC.ml", line 380, characters 55-61: Assertion failed

when we call the extraction using jasminc test.jazz -CT -ec main. What seems important is that i is unknown.

[eponier]

(this was first observed by Ethan in https://github.com/ethanlee515/jasmin-dilithium)

[tfaoliveira]

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 same error.

Is this something that can be avoided by rewriting the code? Is it possible to print more information about why it fails, or does it need fixing on the extraction?

[vbgl]

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?

[tfaoliveira]

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.

[vbgl]

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