Allow cross-checking of HOL-Light proofs

[hanno-becker]

#1323 introduced first HOL-Light proofs for x86_64, alongside the existing AArch64 proofs.

However, at present ./scripts/tests/hol_light will only run the proofs for the architecture matching the host machine.

Task:

• Ensure that HOL-Light proofs can be cross-checked; that is, you should be able to run AArch64 proofs on x86 hosts, and x86 proofs on AArch64 hosts.
• Consider how to exercise this in CI; perhaps cross-check only one of the simple proofs (e.g. basemul), or just do a cross-arch bytecode generation.
• Adjust ./scripts/tests/hol_light to not just run native proofs