Paper 2026/2307
Functional Verification of Additive FFT Assembly Implementations in Code-Based PQC
Abstract
We present the first formal verification results for the highly optimized additive Fast Fourier Transforms (FFTs) in two different code-based post-quantum cryptosystems: Classic McEliece and Hamming Quasi-Cyclic. Since Classic McEliece is already a standard and HQC is being standardized, they may both see wide adoption in the future. The Gao-Mateer and Frobenius additive FFTs during decoding are clearly the most intricate, error-prone components in the two cryptosystems respectively. They are not only complicated and mathematically intricate, but also aggressively optimized in practical implementations. A main problem of this verification is the $>2^{14}$ independent bit-variables in each multiplicand. Aside from adding a vector syntax and improving various syntactic transformations to the open-source tool CryptoLine, we also formulate additive FFTs as Chinese Remainder Theorem decompositions which factors the verification problem into local checks feasible for computer algebra systems like Singular. The workload was also tractable: the calendar time for the formal verification in this paper was less than three months for our very limited workforce.
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Preprint.
- Keywords
- Calssic McElieceHQCPQCFormal Verification
- Contact author(s)
-
liujx @ ios ac cn
shixm @ ios ac cn
mhtsai @ cs ntust edu tw
bywang @ iis sinica edu tw
byyang @ iis sinica edu tw - History
- 2026-10-04: approved
- 2026-10-02: received
- See all versions
- Short URL
- https://ia.cr/2026/2307
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2026/2307,
author = {Jiaxiang Liu and Kuang-Lin Pan and Xiaomu Shi and Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang},
title = {Functional Verification of Additive {FFT} Assembly Implementations in Code-Based {PQC}},
howpublished = {Cryptology {ePrint} Archive, Paper 2026/2307},
year = {2026},
url = {https://eprint.iacr.org/2026/2307}
}
