HOL-Light: Add hol-server for interactive proof development #1500

mkannwischer · 2026-01-20T08:23:25Z

Integrates hol_server (https://github.com/monadius/hol_server) to enable TCP-based communication with HOL Light. This allows sending commands programmatically via netcat or the VS Code extension.

Usage: hol-server [port] # default port is 2012

Update documentation accordingly.

Ported from Add hol-server for programmatic HOL Light communication mldsa-native#883

oqs-bot · 2026-01-20T09:02:43Z

CBMC Results (ML-KEM-512)

Full Results (139 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1183s	1226s	-3.5%
`mlk_indcpa_enc`	✅	187s	204s	-8%
`mlk_indcpa_keypair_derand`	✅	178s	182s	-2%
`mlk_keccak_squeezeblocks_x4`	✅	137s	133s	+3%
`mlk_rej_uniform_c`	✅	91s	82s	+11%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	✅	46s	46s	+0%
`mlk_poly_rej_uniform`	✅	34s	37s	-8%
`mlk_ntt_layer`	✅	25s	25s	+0%
`poly_ntt_native`	✅	21s	29s	-28%
`polyvec_basemul_acc_montgomery_cached_native`	✅	21s	22s	-5%
`keccakf1600x4_permute_native_x4`	✅	19s	18s	+6%
`mlk_poly_reduce_native`	✅	18s	14s	+29%
`mlk_poly_sub`	✅	11s	11s	+0%
`mlk_indcpa_dec`	✅	10s	11s	-9%
`mlk_poly_frombytes_native`	✅	10s	10s	+0%
`mlk_polyvec_add`	✅	10s	10s	+0%
`mlk_keccak_absorb_once_x4`	✅	9s	11s	-18%
`mlk_ntt_butterfly_block`	✅	8s	8s	+0%
`mlk_keccak_squeeze_once`	✅	7s	8s	-12%
`mlk_poly_rej_uniform_x4`	✅	7s	8s	-12%
`keccakf1600_permute_native`	✅	6s	6s	+0%
`kem_dec`	✅	6s	6s	+0%
`mlk_fqmul`	✅	6s	7s	-14%
`mlk_keccak_squeezeblocks`	✅	6s	7s	-14%
`mlk_poly_frommsg`	✅	6s	8s	-25%
`mlk_polymat_permute_bitrev_to_custom`	✅	6s	8s	-25%
`mlk_check_pct`	✅	5s	3s	+67%
`mlk_polyvec_decompress_du`	✅	5s	4s	+25%
`mlk_scalar_compress_d10`	✅	5s	3s	+67%
`ntt_native_aarch64`	✅	5s	2s	+150%
`intt_native_aarch64`	✅	4s	2s	+100%
`kem_enc_derand`	✅	4s	3s	+33%
`mlk_ct_sel_uint8`	✅	4s	3s	+33%
`mlk_invntt_layer`	✅	4s	6s	-33%
`mlk_keccak_absorb_once`	✅	4s	6s	-33%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	4s	4s	+0%
`mlk_poly_compress_du`	✅	4s	4s	+0%
`mlk_poly_decompress_du`	✅	4s	2s	+100%
`mlk_poly_decompress_dv`	✅	4s	4s	+0%
`mlk_poly_getnoise_eta1122_4x`	✅	4s	3s	+33%
`mlk_poly_getnoise_eta1_4x`	✅	4s	6s	-33%
`mlk_poly_getnoise_eta1_4x_native`	✅	4s	2s	+100%
`mlk_poly_mulcache_compute_native`	✅	4s	5s	-20%
`mlk_poly_tomont`	✅	4s	1s	+300%
`mlk_poly_tomont_native`	✅	4s	3s	+33%
`mlk_scalar_compress_d4`	✅	4s	2s	+100%
`mlk_scalar_compress_d5`	✅	4s	2s	+100%
`mlk_scalar_decompress_d11`	✅	4s	2s	+100%
`mlk_shake256`	✅	4s	3s	+33%
`mlk_shake256x4`	✅	4s	5s	-20%
`poly_tobytes_native_aarch64`	✅	4s	3s	+33%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	✅	4s	4s	+0%
`keccak_f1600_x1_native_aarch64`	✅	3s	3s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	✅	3s	2s	+50%
`kem_check_pk`	✅	3s	3s	+0%
`kem_check_sk`	✅	3s	1s	+200%
`mlk_ct_cmask_nonzero_u8`	✅	3s	2s	+50%
`mlk_ct_get_optblocker_u32`	✅	3s	2s	+50%
`mlk_keccakf1600_permute`	✅	3s	7s	-57%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	3s	2s	+50%
`mlk_keccakf1600x4_permute`	✅	3s	1s	+200%
`mlk_matvec_mul`	✅	3s	2s	+50%
`mlk_montgomery_reduce`	✅	3s	1s	+200%
`mlk_poly_getnoise_eta2`	✅	3s	3s	+0%
`mlk_poly_invntt_tomont`	✅	3s	3s	+0%
`mlk_poly_invntt_tomont_c`	✅	3s	1s	+200%
`mlk_poly_mulcache_compute`	✅	3s	3s	+0%
`mlk_poly_reduce`	✅	3s	2s	+50%
`mlk_poly_tobytes_native`	✅	3s	2s	+50%
`mlk_poly_tomont_c`	✅	3s	2s	+50%
`mlk_poly_tomsg`	✅	3s	3s	+0%
`mlk_polyvec_ntt`	✅	3s	3s	+0%
`mlk_polyvec_permute_bitrev_to_custom`	✅	3s	1s	+200%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	3s	4s	-25%
`mlk_polyvec_reduce`	✅	3s	4s	-25%
`mlk_polyvec_tobytes`	✅	3s	4s	-25%
`mlk_polyvec_tomont`	✅	3s	2s	+50%
`mlk_scalar_signed_to_unsigned_q`	✅	3s	1s	+200%
`mlk_value_barrier_u32`	✅	3s	2s	+50%
`mlk_value_barrier_u8`	✅	3s	2s	+50%
`poly_getnoise_eta1122_4x_native`	✅	3s	3s	+0%
`poly_invntt_tomont_native`	✅	3s	3s	+0%
`poly_tomont_native_aarch64`	✅	3s	3s	+0%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	3s	3s	+0%
`rej_uniform_native`	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v84a`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	1s	+100%
`kem_enc`	✅	2s	2s	+0%
`kem_keypair`	✅	2s	3s	-33%
`kem_keypair_derand`	✅	2s	3s	-33%
`mlk_barrett_reduce`	✅	2s	2s	+0%
`mlk_ct_cmask_neg_i16`	✅	2s	6s	-67%
`mlk_ct_cmov_zero`	✅	2s	2s	+0%
`mlk_ct_get_optblocker_u8`	✅	2s	1s	+100%
`mlk_ct_memcmp`	✅	2s	5s	-60%
`mlk_gen_matrix_serial`	✅	2s	2s	+0%
`mlk_keccakf1600_extract_bytes`	✅	2s	2s	+0%
`mlk_keccakf1600_xor_bytes`	✅	2s	2s	+0%
`mlk_keccakf1600x4_extract_bytes`	✅	2s	1s	+100%
`mlk_poly_add`	✅	2s	4s	-50%
`mlk_poly_cbd_eta1`	✅	2s	2s	+0%
`mlk_poly_cbd_eta2`	✅	2s	2s	+0%
`mlk_poly_mulcache_compute_c`	✅	2s	1s	+100%
`mlk_poly_ntt_c`	✅	2s	2s	+0%
`mlk_poly_reduce_c`	✅	2s	3s	-33%
`mlk_poly_tobytes_c`	✅	2s	2s	+0%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	2s	4s	-50%
`mlk_polyvec_frombytes`	✅	2s	4s	-50%
`mlk_polyvec_invntt_tomont`	✅	2s	3s	-33%
`mlk_scalar_compress_d11`	✅	2s	3s	-33%
`mlk_scalar_decompress_d10`	✅	2s	3s	-33%
`mlk_scalar_decompress_d5`	✅	2s	3s	-33%
`mlk_sha3_512`	✅	2s	2s	+0%
`mlk_shake128_absorb_once`	✅	2s	2s	+0%
`mlk_shake128x4_absorb_once`	✅	2s	3s	-33%
`mlk_shake128x4_squeezeblocks`	✅	2s	2s	+0%
`poly_mulcache_compute_native_aarch64`	✅	2s	1s	+100%
`poly_reduce_native_aarch64`	✅	2s	3s	-33%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	2s	5s	-60%
`rej_uniform_native_aarch64`	✅	2s	5s	-60%
`sys_check_capability`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	1s	2s	-50%
`mlk_ct_cmask_nonzero_u16`	✅	1s	1s	+0%
`mlk_ct_get_optblocker_i32`	✅	1s	4s	-75%
`mlk_ct_sel_int16`	✅	1s	2s	-50%
`mlk_gen_matrix`	✅	1s	6s	-83%
`mlk_keccakf1600x4_xor_bytes`	✅	1s	2s	-50%
`mlk_poly_compress_dv`	✅	1s	4s	-75%
`mlk_poly_frombytes`	✅	1s	3s	-67%
`mlk_poly_frombytes_c`	✅	1s	1s	+0%
`mlk_poly_ntt`	✅	1s	5s	-80%
`mlk_poly_tobytes`	✅	1s	3s	-67%
`mlk_polyvec_compress_du`	✅	1s	2s	-50%
`mlk_polyvec_mulcache_compute`	✅	1s	2s	-50%
`mlk_rej_uniform`	✅	1s	1s	+0%
`mlk_scalar_compress_d1`	✅	1s	3s	-67%
`mlk_scalar_decompress_d4`	✅	1s	2s	-50%
`mlk_sha3_256`	✅	1s	3s	-67%
`mlk_shake128_squeezeblocks`	✅	1s	2s	-50%
`mlk_value_barrier_i32`	✅	1s	1s	+0%

oqs-bot · 2026-01-20T09:05:25Z

CBMC Results (ML-KEM-1024)

Full Results (139 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1745s	1777s	-1.8%
`mlk_indcpa_enc`	✅	368s	355s	+4%
`mlk_indcpa_keypair_derand`	✅	268s	270s	-1%
`mlk_keccak_squeezeblocks_x4`	✅	130s	136s	-4%
`mlk_polyvec_add`	✅	128s	132s	-3%
`polyvec_basemul_acc_montgomery_cached_native`	✅	123s	125s	-2%
`mlk_rej_uniform_c`	✅	80s	89s	-10%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	✅	53s	53s	+0%
`poly_ntt_native`	✅	41s	48s	-15%
`mlk_poly_rej_uniform`	✅	38s	44s	-14%
`mlk_poly_decompress_dv`	✅	37s	33s	+12%
`mlk_ntt_layer`	✅	29s	27s	+7%
`mlk_indcpa_dec`	✅	19s	21s	-10%
`keccakf1600x4_permute_native_x4`	✅	18s	20s	-10%
`mlk_poly_reduce_native`	✅	16s	14s	+14%
`mlk_poly_sub`	✅	10s	8s	+25%
`mlk_gen_matrix`	✅	9s	9s	+0%
`mlk_ntt_butterfly_block`	✅	9s	10s	-10%
`mlk_poly_frommsg`	✅	9s	8s	+12%
`mlk_keccak_absorb_once_x4`	✅	8s	10s	-20%
`mlk_poly_frombytes_native`	✅	8s	10s	-20%
`mlk_poly_rej_uniform_x4`	✅	8s	10s	-20%
`mlk_fqmul`	✅	7s	8s	-12%
`mlk_keccak_squeezeblocks`	✅	7s	7s	+0%
`mlk_poly_compress_du`	✅	7s	8s	-12%
`intt_native_aarch64`	✅	6s	2s	+200%
`kem_dec`	✅	6s	6s	+0%
`mlk_gen_matrix_serial`	✅	6s	8s	-25%
`mlk_keccak_squeeze_once`	✅	6s	8s	-25%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	6s	4s	+50%
`keccakf1600_permute_native`	✅	5s	5s	+0%
`mlk_keccak_absorb_once`	✅	5s	3s	+67%
`mlk_keccakf1600_permute`	✅	5s	3s	+67%
`mlk_polymat_permute_bitrev_to_custom`	✅	5s	6s	-17%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	5s	4s	+25%
`mlk_shake256x4`	✅	5s	4s	+25%
`kem_enc_derand`	✅	4s	5s	-20%
`mlk_invntt_layer`	✅	4s	5s	-20%
`mlk_poly_cbd_eta2`	✅	4s	3s	+33%
`mlk_poly_ntt_c`	✅	4s	3s	+33%
`mlk_poly_reduce`	✅	4s	2s	+100%
`mlk_polyvec_decompress_du`	✅	4s	3s	+33%
`mlk_polyvec_mulcache_compute`	✅	4s	3s	+33%
`mlk_polyvec_permute_bitrev_to_custom`	✅	4s	2s	+100%
`mlk_polyvec_reduce`	✅	4s	3s	+33%
`mlk_scalar_decompress_d4`	✅	4s	2s	+100%
`mlk_scalar_decompress_d5`	✅	4s	3s	+33%
`mlk_shake128x4_squeezeblocks`	✅	4s	4s	+0%
`ntt_native_aarch64`	✅	4s	2s	+100%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	4s	1s	+300%
`rej_uniform_native`	✅	4s	4s	+0%
`keccak_f1600_x1_native_aarch64`	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	3s	1s	+200%
`mlk_ct_cmask_nonzero_u16`	✅	3s	5s	-40%
`mlk_ct_cmov_zero`	✅	3s	2s	+50%
`mlk_ct_sel_int16`	✅	3s	2s	+50%
`mlk_keccakf1600_extract_bytes`	✅	3s	3s	+0%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	3s	3s	+0%
`mlk_keccakf1600x4_extract_bytes`	✅	3s	3s	+0%
`mlk_keccakf1600x4_permute`	✅	3s	2s	+50%
`mlk_keccakf1600x4_xor_bytes`	✅	3s	3s	+0%
`mlk_montgomery_reduce`	✅	3s	1s	+200%
`mlk_poly_frombytes_c`	✅	3s	2s	+50%
`mlk_poly_getnoise_eta1_4x_native`	✅	3s	3s	+0%
`mlk_poly_invntt_tomont`	✅	3s	2s	+50%
`mlk_poly_invntt_tomont_c`	✅	3s	3s	+0%
`mlk_poly_mulcache_compute`	✅	3s	4s	-25%
`mlk_poly_mulcache_compute_native`	✅	3s	2s	+50%
`mlk_poly_tobytes`	✅	3s	2s	+50%
`mlk_poly_tomont`	✅	3s	1s	+200%
`mlk_poly_tomont_c`	✅	3s	3s	+0%
`mlk_poly_tomsg`	✅	3s	3s	+0%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	3s	4s	-25%
`mlk_polyvec_frombytes`	✅	3s	2s	+50%
`mlk_polyvec_tobytes`	✅	3s	2s	+50%
`mlk_polyvec_tomont`	✅	3s	2s	+50%
`mlk_scalar_compress_d10`	✅	3s	1s	+200%
`mlk_scalar_compress_d11`	✅	3s	2s	+50%
`mlk_scalar_decompress_d10`	✅	3s	4s	-25%
`mlk_scalar_decompress_d11`	✅	3s	2s	+50%
`mlk_sha3_256`	✅	3s	3s	+0%
`mlk_sha3_512`	✅	3s	2s	+50%
`mlk_value_barrier_u8`	✅	3s	2s	+50%
`poly_reduce_native_aarch64`	✅	3s	2s	+50%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	✅	3s	3s	+0%
`sys_check_capability`	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	1s	+100%
`kem_check_pk`	✅	2s	4s	-50%
`kem_check_sk`	✅	2s	4s	-50%
`kem_enc`	✅	2s	3s	-33%
`kem_keypair`	✅	2s	3s	-33%
`mlk_barrett_reduce`	✅	2s	4s	-50%
`mlk_check_pct`	✅	2s	5s	-60%
`mlk_ct_cmask_neg_i16`	✅	2s	4s	-50%
`mlk_ct_get_optblocker_i32`	✅	2s	1s	+100%
`mlk_ct_get_optblocker_u32`	✅	2s	2s	+0%
`mlk_poly_add`	✅	2s	2s	+0%
`mlk_poly_cbd_eta1`	✅	2s	2s	+0%
`mlk_poly_compress_dv`	✅	2s	1s	+100%
`mlk_poly_getnoise_eta2`	✅	2s	2s	+0%
`mlk_poly_mulcache_compute_c`	✅	2s	4s	-50%
`mlk_poly_ntt`	✅	2s	2s	+0%
`mlk_poly_tobytes_c`	✅	2s	1s	+100%
`mlk_poly_tobytes_native`	✅	2s	3s	-33%
`mlk_poly_tomont_native`	✅	2s	1s	+100%
`mlk_polyvec_compress_du`	✅	2s	3s	-33%
`mlk_polyvec_invntt_tomont`	✅	2s	3s	-33%
`mlk_polyvec_ntt`	✅	2s	3s	-33%
`mlk_rej_uniform`	✅	2s	2s	+0%
`mlk_scalar_compress_d1`	✅	2s	3s	-33%
`mlk_scalar_compress_d4`	✅	2s	3s	-33%
`mlk_scalar_compress_d5`	✅	2s	2s	+0%
`mlk_scalar_signed_to_unsigned_q`	✅	2s	2s	+0%
`mlk_shake128_absorb_once`	✅	2s	3s	-33%
`mlk_shake128_squeezeblocks`	✅	2s	2s	+0%
`mlk_value_barrier_u32`	✅	2s	1s	+100%
`poly_getnoise_eta1122_4x_native`	✅	2s	3s	-33%
`poly_invntt_tomont_native`	✅	2s	4s	-50%
`poly_tobytes_native_aarch64`	✅	2s	3s	-33%
`poly_tomont_native_aarch64`	✅	2s	2s	+0%
`rej_uniform_native_aarch64`	✅	2s	5s	-60%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	3s	-67%
`kem_keypair_derand`	✅	1s	3s	-67%
`mlk_ct_cmask_nonzero_u8`	✅	1s	2s	-50%
`mlk_ct_get_optblocker_u8`	✅	1s	2s	-50%
`mlk_ct_memcmp`	✅	1s	3s	-67%
`mlk_ct_sel_uint8`	✅	1s	4s	-75%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	1s	3s	-67%
`mlk_keccakf1600_xor_bytes`	✅	1s	2s	-50%
`mlk_matvec_mul`	✅	1s	1s	+0%
`mlk_poly_decompress_du`	✅	1s	4s	-75%
`mlk_poly_frombytes`	✅	1s	3s	-67%
`mlk_poly_getnoise_eta1122_4x`	✅	1s	3s	-67%
`mlk_poly_getnoise_eta1_4x`	✅	1s	1s	+0%
`mlk_poly_reduce_c`	✅	1s	2s	-50%
`mlk_shake128x4_absorb_once`	✅	1s	1s	+0%
`mlk_shake256`	✅	1s	2s	-50%
`mlk_value_barrier_i32`	✅	1s	1s	+0%
`poly_mulcache_compute_native_aarch64`	✅	1s	3s	-67%

oqs-bot · 2026-01-20T09:07:06Z

CBMC Results (ML-KEM-768)

Full Results (139 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1540s	1754s	-12.2%
`mlk_indcpa_keypair_derand`	✅	385s	404s	-5%
`mlk_indcpa_enc`	✅	236s	238s	-1%
`mlk_keccak_squeezeblocks_x4`	✅	125s	169s	-26%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	✅	81s	110s	-26%
`mlk_rej_uniform_c`	✅	78s	117s	-33%
`polyvec_basemul_acc_montgomery_cached_native`	✅	58s	72s	-19%
`poly_ntt_native`	✅	50s	69s	-28%
`mlk_poly_rej_uniform`	✅	39s	48s	-19%
`mlk_ntt_layer`	✅	28s	37s	-24%
`keccakf1600x4_permute_native_x4`	✅	20s	19s	+5%
`mlk_indcpa_dec`	✅	19s	23s	-17%
`mlk_poly_reduce_native`	✅	16s	16s	+0%
`mlk_keccak_absorb_once_x4`	✅	10s	11s	-9%
`mlk_keccak_squeeze_once`	✅	9s	5s	+80%
`mlk_keccak_squeezeblocks`	✅	9s	10s	-10%
`mlk_ntt_butterfly_block`	✅	9s	14s	-36%
`mlk_poly_sub`	✅	9s	11s	-18%
`mlk_polyvec_add`	✅	9s	15s	-40%
`mlk_fqmul`	✅	8s	9s	-11%
`mlk_poly_rej_uniform_x4`	✅	8s	9s	-11%
`mlk_poly_frombytes_native`	✅	7s	14s	-50%
`mlk_poly_frommsg`	✅	7s	8s	-12%
`kem_dec`	✅	6s	7s	-14%
`mlk_polymat_permute_bitrev_to_custom`	✅	6s	7s	-14%
`mlk_gen_matrix_serial`	✅	5s	4s	+25%
`mlk_invntt_layer`	✅	5s	7s	-29%
`mlk_keccak_absorb_once`	✅	5s	5s	+0%
`mlk_matvec_mul`	✅	5s	2s	+150%
`mlk_poly_compress_dv`	✅	5s	3s	+67%
`mlk_shake256x4`	✅	5s	7s	-29%
`keccak_f1600_x1_native_aarch64_v84a`	✅	4s	3s	+33%
`keccakf1600_permute_native`	✅	4s	6s	-33%
`kem_enc_derand`	✅	4s	3s	+33%
`mlk_check_pct`	✅	4s	2s	+100%
`mlk_gen_matrix`	✅	4s	6s	-33%
`mlk_poly_cbd_eta1`	✅	4s	3s	+33%
`mlk_poly_tobytes`	✅	4s	2s	+100%
`mlk_poly_tomsg`	✅	4s	2s	+100%
`mlk_polyvec_decompress_du`	✅	4s	3s	+33%
`mlk_polyvec_permute_bitrev_to_custom`	✅	4s	4s	+0%
`mlk_scalar_compress_d5`	✅	4s	4s	+0%
`mlk_scalar_decompress_d10`	✅	4s	2s	+100%
`mlk_scalar_decompress_d11`	✅	4s	2s	+100%
`mlk_sha3_512`	✅	4s	2s	+100%
`poly_invntt_tomont_native`	✅	4s	2s	+100%
`intt_native_aarch64`	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	4s	-25%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	3s	3s	+0%
`kem_check_pk`	✅	3s	3s	+0%
`kem_check_sk`	✅	3s	5s	-40%
`kem_keypair`	✅	3s	3s	+0%
`kem_keypair_derand`	✅	3s	2s	+50%
`mlk_barrett_reduce`	✅	3s	1s	+200%
`mlk_ct_cmov_zero`	✅	3s	1s	+200%
`mlk_ct_get_optblocker_u32`	✅	3s	1s	+200%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	3s	2s	+50%
`mlk_keccakf1600_permute`	✅	3s	7s	-57%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	3s	1s	+200%
`mlk_keccakf1600x4_extract_bytes`	✅	3s	3s	+0%
`mlk_poly_compress_du`	✅	3s	4s	-25%
`mlk_poly_frombytes`	✅	3s	2s	+50%
`mlk_poly_frombytes_c`	✅	3s	3s	+0%
`mlk_poly_getnoise_eta1_4x`	✅	3s	2s	+50%
`mlk_poly_getnoise_eta1_4x_native`	✅	3s	4s	-25%
`mlk_poly_invntt_tomont_c`	✅	3s	3s	+0%
`mlk_poly_mulcache_compute_native`	✅	3s	1s	+200%
`mlk_poly_reduce_c`	✅	3s	1s	+200%
`mlk_poly_tobytes_c`	✅	3s	2s	+50%
`mlk_poly_tomont`	✅	3s	1s	+200%
`mlk_poly_tomont_c`	✅	3s	4s	-25%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	3s	3s	+0%
`mlk_polyvec_invntt_tomont`	✅	3s	2s	+50%
`mlk_polyvec_mulcache_compute`	✅	3s	3s	+0%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	3s	2s	+50%
`mlk_polyvec_reduce`	✅	3s	3s	+0%
`mlk_polyvec_tobytes`	✅	3s	2s	+50%
`mlk_rej_uniform`	✅	3s	3s	+0%
`mlk_scalar_compress_d10`	✅	3s	1s	+200%
`mlk_scalar_compress_d11`	✅	3s	1s	+200%
`mlk_scalar_signed_to_unsigned_q`	✅	3s	5s	-40%
`mlk_value_barrier_i32`	✅	3s	3s	+0%
`poly_getnoise_eta1122_4x_native`	✅	3s	2s	+50%
`poly_mulcache_compute_native_aarch64`	✅	3s	1s	+200%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	3s	2s	+50%
`rej_uniform_native`	✅	3s	3s	+0%
`rej_uniform_native_aarch64`	✅	3s	4s	-25%
`sys_check_capability`	✅	3s	2s	+50%
`keccak_f1600_x1_native_aarch64`	✅	2s	1s	+100%
`kem_enc`	✅	2s	3s	-33%
`mlk_ct_cmask_neg_i16`	✅	2s	2s	+0%
`mlk_ct_cmask_nonzero_u8`	✅	2s	2s	+0%
`mlk_ct_get_optblocker_i32`	✅	2s	2s	+0%
`mlk_ct_get_optblocker_u8`	✅	2s	3s	-33%
`mlk_ct_memcmp`	✅	2s	1s	+100%
`mlk_ct_sel_int16`	✅	2s	2s	+0%
`mlk_ct_sel_uint8`	✅	2s	2s	+0%
`mlk_keccakf1600_xor_bytes`	✅	2s	3s	-33%
`mlk_keccakf1600x4_permute`	✅	2s	4s	-50%
`mlk_montgomery_reduce`	✅	2s	3s	-33%
`mlk_poly_add`	✅	2s	3s	-33%
`mlk_poly_cbd_eta2`	✅	2s	1s	+100%
`mlk_poly_decompress_du`	✅	2s	5s	-60%
`mlk_poly_decompress_dv`	✅	2s	2s	+0%
`mlk_poly_getnoise_eta1122_4x`	✅	2s	4s	-50%
`mlk_poly_getnoise_eta2`	✅	2s	3s	-33%
`mlk_poly_invntt_tomont`	✅	2s	1s	+100%
`mlk_poly_reduce`	✅	2s	2s	+0%
`mlk_poly_tobytes_native`	✅	2s	2s	+0%
`mlk_poly_tomont_native`	✅	2s	2s	+0%
`mlk_polyvec_compress_du`	✅	2s	2s	+0%
`mlk_scalar_compress_d1`	✅	2s	3s	-33%
`mlk_scalar_compress_d4`	✅	2s	1s	+100%
`mlk_scalar_decompress_d4`	✅	2s	2s	+0%
`mlk_scalar_decompress_d5`	✅	2s	1s	+100%
`mlk_sha3_256`	✅	2s	2s	+0%
`mlk_shake128_absorb_once`	✅	2s	3s	-33%
`mlk_shake128_squeezeblocks`	✅	2s	4s	-50%
`mlk_shake128x4_absorb_once`	✅	2s	2s	+0%
`mlk_shake128x4_squeezeblocks`	✅	2s	3s	-33%
`mlk_shake256`	✅	2s	3s	-33%
`mlk_value_barrier_u32`	✅	2s	3s	-33%
`ntt_native_aarch64`	✅	2s	3s	-33%
`poly_reduce_native_aarch64`	✅	2s	3s	-33%
`poly_tobytes_native_aarch64`	✅	2s	3s	-33%
`poly_tomont_native_aarch64`	✅	2s	4s	-50%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	2s	4s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	1s	3s	-67%
`mlk_ct_cmask_nonzero_u16`	✅	1s	2s	-50%
`mlk_keccakf1600_extract_bytes`	✅	1s	1s	+0%
`mlk_keccakf1600x4_xor_bytes`	✅	1s	2s	-50%
`mlk_poly_mulcache_compute`	✅	1s	3s	-67%
`mlk_poly_mulcache_compute_c`	✅	1s	4s	-75%
`mlk_poly_ntt`	✅	1s	4s	-75%
`mlk_poly_ntt_c`	✅	1s	4s	-75%
`mlk_polyvec_frombytes`	✅	1s	2s	-50%
`mlk_polyvec_ntt`	✅	1s	2s	-50%
`mlk_polyvec_tomont`	✅	1s	2s	-50%
`mlk_value_barrier_u8`	✅	1s	1s	+0%

hanno-becker · 2026-01-22T05:45:08Z

I tried the PR locally.

Entered hol_light nix shell and started hol-server
Opened VS Code and connected to hol-server
Opened AArch64 poly_tobytes proof file and processed in one go -- SUCCESS
Opened x86_64 poly_tobytes proof file and processed in one go -- FAIL

The failure looks a bit odd, as if the hol-light or s2n-bignum version aren't right. But then the CI shouldn't be happy either?

Exception: Failure "new_specification: Assumptions not allowed in theorem".
Error in included file /nix/store/fjm9sg8dd3m84j9czn2yrfp6x20ws0lf-s2n_bignum-2e7d839720869abdff49e2da7fa6f46718e2c3b0/x86/proofs/x86.ml

- : unit = ()

File "/nix/store/fjm9sg8dd3m84j9czn2yrfp6x20ws0lf-s2n_bignum-2e7d839720869abdff49e2da7fa6f46718e2c3b0/x86/proofs/base.ml", line 61, characters 39-57:
61 | extra_word_CONV := [GEN_REWRITE_CONV I READ_YMM_SSE_EQUIV] @ !extra_word_CONV;;
                                            ^^^^^^^^^^^^^^^^^^
Error: Unbound value READ_YMM_SSE_EQUIV

I need to take a closer look. @mkannwischer Any idea from the top of your head?

Integrates hol_server (https://github.com/monadius/hol_server) to enable TCP-based communication with HOL Light. This allows sending commands programmatically via netcat or the VS Code extension. Usage: hol-server [port] # default port is 2012 Update documentation accordingly. - Ported from pq-code-package/mldsa-native#883 Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

mkannwischer · 2026-01-22T06:11:08Z

I tried the PR locally.

Entered hol_light nix shell and started hol-server

Opened VS Code and connected to hol-server

Opened AArch64 poly_tobytes proof file and processed in one go -- SUCCESS

Opened x86_64 poly_tobytes proof file and processed in one go -- FAIL

The failure looks a bit odd, as if the hol-light or s2n-bignum version aren't right. But then the CI shouldn't be happy either?
Exception: Failure "new_specification: Assumptions not allowed in theorem".
Error in included file /nix/store/fjm9sg8dd3m84j9czn2yrfp6x20ws0lf-s2n_bignum-2e7d839720869abdff49e2da7fa6f46718e2c3b0/x86/proofs/x86.ml

- : unit = ()

File "/nix/store/fjm9sg8dd3m84j9czn2yrfp6x20ws0lf-s2n_bignum-2e7d839720869abdff49e2da7fa6f46718e2c3b0/x86/proofs/base.ml", line 61, characters 39-57:
61 | extra_word_CONV := [GEN_REWRITE_CONV I READ_YMM_SSE_EQUIV] @ !extra_word_CONV;;
                                            ^^^^^^^^^^^^^^^^^^
Error: Unbound value READ_YMM_SSE_EQUIV
I need to take a closer look. @mkannwischer Any idea from the top of your head?

Running just the x86_64 poly_tobytes proof works fine for me with the hol-server in this branch.
I don't think you can do

needs "x86/proofs/base.ml";;
needs "arm/proofs/base.ml";;

in a single HOL-Light session which is what you would need to do if you want to run both an AArch64 and x86_64 proof.
Doing so also gives some error that sounds pretty bad for me:

Exception:
Failure "new_constant: constant registers has already been declared".
Error in included file /nix/store/fjm9sg8dd3m84j9czn2yrfp6x20ws0lf-s2n_bignum-2e7d839720869abdff49e2da7fa6f46718e2c3b0/arm/proofs/instruction.ml
Exception:
Failure
 "typechecking error (initial type assignment): i cannot have type (32)word and ((8)word)list simultaneously".
Error in included file /nix/store/fjm9sg8dd3m84j9czn2yrfp6x20ws0lf-s2n_bignum-2e7d839720869abdff49e2da7fa6f46718e2c3b0/arm/proofs/arm.ml

But it happily continue to execute, so you may have not seen those exceptions.

I'd say that limitation is not introduced by this PR and you'll probably have to fix it upstream if you really want to support it.

hanno-becker · 2026-01-22T07:33:34Z

@mkannwischer Agreed

mkannwischer marked this pull request as ready for review January 20, 2026 08:31

mkannwischer requested a review from a team as a code owner January 20, 2026 08:31

mkannwischer changed the title ~~Add hol-server for programmatic HOL Light communication~~ HOL-Light: Add hol-server for interactive proof development Jan 20, 2026

hanno-becker force-pushed the hol-server branch from 0265f8c to a1f2360 Compare January 22, 2026 05:46

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

HOL-Light: Add hol-server for interactive proof development #1500

HOL-Light: Add hol-server for interactive proof development #1500

mkannwischer commented Jan 20, 2026

Uh oh!

oqs-bot commented Jan 20, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jan 20, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jan 20, 2026 •

edited

Loading

Uh oh!

hanno-becker commented Jan 22, 2026 •

edited

Loading

Uh oh!

mkannwischer commented Jan 22, 2026 •

edited

Loading

Uh oh!

hanno-becker commented Jan 22, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

HOL-Light: Add hol-server for interactive proof development #1500

Are you sure you want to change the base?

HOL-Light: Add hol-server for interactive proof development #1500

Conversation

mkannwischer commented Jan 20, 2026

Uh oh!

oqs-bot commented Jan 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-512)

Uh oh!

oqs-bot commented Jan 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-1024)

Uh oh!

oqs-bot commented Jan 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-768)

Uh oh!

hanno-becker commented Jan 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mkannwischer commented Jan 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hanno-becker commented Jan 22, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

oqs-bot commented Jan 20, 2026 •

edited

Loading

oqs-bot commented Jan 20, 2026 •

edited

Loading

oqs-bot commented Jan 20, 2026 •

edited

Loading

hanno-becker commented Jan 22, 2026 •

edited

Loading

mkannwischer commented Jan 22, 2026 •

edited

Loading