eclib: set0_{128,256} issue; Jasmin v2022.04.0

[tfaoliveira]

This issue is described in the context of Jasmin v2022.04.0 and EasyCrypt r2022.04.

When extracting to EasyCrypt a Jasmin function that contains #set0_128() or #set0_256(), those statements are extracted to <- set0_128 ; or <- set0_256 ;.

When checking the extracted file with EasyCrypt, I get the error:

This expression has type
   bool * bool * bool * bool * bool * W128.t
but is expected to have type
   W128.t

• set0_XX is defined here:

  jasmin/eclib/JWord.ec

  Line 1482 in 7f67b5b

  op set0_XX = (false,false,false,false,false, of_int 0).

• Theory W256 is defined here:

  jasmin/eclib/JWord.ec

  Line 2520 in 7f67b5b

  theory W256.

I think it is necessary to define set0_128 and set0_256 differently (without returning the flags) for these particular cases.

[fdupress]

Are there any uses of those instructions where the flags are not ignored in the Jasmin source? Instead of defining set0_128 and set0_256 differently, it's probably a better idea to tweak extraction to mimic the source's behaviour w.r.t. ignoring the flags.

[bgregoir]

Hi Tiago, this is clearly a bug in the extraction and the easycrypt model. I will fix this.

[eponier]

Before, set0 for sizes 128 and 256 was called setw0. Maybe this is related to this bug.

[tfaoliveira]

For u128 and u256 flags are not affected. I think this is possible to see in Definition Oset0_instr from

jasmin/proofs/compiler/x86_extra.v

Line 35 in 7906ac9

Definition Oset0_instr sz :=

, and I also double-checked in the Intel developer's manual.

I would risk saying that the extraction is OK and only the eclib needs to be adjusted.

[vbgl]

This has been fixed in #134.

[tfaoliveira]

Tested on libjade; Everything fine :-)