eclib: no matching operator, named `VMOVSHDUP_4u64'

[tfaoliveira]

I'm integrating this implementation in libjade.

When checking the extracted file with easycrypt I get the following error:

[critical] [sign_s.ec: line 2564 (14-28)] no matching operator, named `VMOVSHDUP_4u64', for the following parameters' type:
  [1]: W256.t
[-] [5972] 100.0 % (-1.0B / [frag -1.0B])

It seems that a def. for VMOVSHDUP_4u64 is missing in JModel.ec around line 673.

[vbgl]

That’s unfortunate, but the VMOVSHDUP_4u64 has no semantics in Jasmin. For the time being, you can rename it into …_8u32.
IMHO, this syntactic flexibility (many variants are accepted by the parser, but only a few make sense) is misleading, hence the related PR. What do you think?

[tfaoliveira]

I think it's OK. Once PR is merged, I can update the libajde code. Thanks.