HOL-Light: Prove correctness of AArch64 implementation of poly_tobytes

[hanno-becker]

No description provided.

[hanno-becker]

This needs support for ST3 in s2n-bignum first.

[rod-chapman]

Also needs support for "vor" and "shrn2" in both s2n-bignum and SLOTHY.

[hanno-becker]

What is "vor"? If you mean EOR, this has been added by @jargh but is not yet in main I think.

[rod-chapman]

Sorry... it's "orr" in ARM assembly syntax. It's "class vor" in the SLOTHY model.

[hanno-becker]

Where is that being used? I see neither orr nor shrn2 in the repository.

[rod-chapman]

They appear in the code generated by GCC for poly_tobytes(). That code is potentially faster than what we have now because it ends up doing 8 ST3 (16.b) instructions rather than 16 ST3 (8.b) instructions. Measuring now.

[hanno-becker]

Ok. I don't think this should take any priority -- poly_tobytes is already very fast (<100 cycles on Graviton2, for example), so we don't need to spend cycles optimizing it further, esp. if it increases the verification burden by requiring additional instructions.