HOL-Light: Support running proofs on MacOS

[mkannwischer]

Currently the HOL-Light proof added in #640 only works on x86_64 Linux.
First, we need to enable it on AArch64 (#643). However, even when cross compiltation is supported there appears to be an issue (as mentionedin #640:

There is an issue where the x86 bytecode generated on clang ARM Mac is different to that when compiled on a gcc Linux. The clang compiler performs some optimization of instructions by switching the source operands of VPADDD etc. to get a shorter encoding. This means the define_assert_from_elf check will fail when compiled on clang ARM Mac, as the proof is set with the machine code as compiled on gcc Linux (I do have proofs for both). We will have the same issue in mlkem-native when the x86 proofs arrive. So looking for opinions on (1) being okay with the x86 proofs not working on clang ARM Mac environments (2) fix the selective swapping of source operands to VPADDD to "optimise" the instructions down to the shorter size on gcc Linux, so both compile consistently (3) adding both proof types... likely all but (1) is out of scope of this PR -- just keeping notes.

We should make sure the proofs can be reproduced also on MacOS.

[jakemas]

This won't be too bad, essentially, I will need to automate some of the proof to read the size of the machine code and proceed accordingly. Now I've build the autogen byte code functionality, this should be a simple follow up