The LABLE SIZE is 16, and we just truncate the 32-byte output to 16 by getting the higher half. It's not safe.
Code: https://github.com/GOATNetwork/bitvm2-gc/blob/main/garbled-snark-verifier/src/core/utils.rs#L53.
One option: AES NI. It's efficient, but there is no precompile yet.