Formal Verification of Emulated Floating-Point Arithmetic in Falcon

ePrint Report: Formal Verification of Emulated Floating-Point Arithmetic in Falcon

Vincent Hwang

We show that there is a discrepancy between the emulated floating-point multiplications in the submission package of Falcon and the claimed behavior. In particular, we show that floating-point products with absolute values the smallest normal positive floating-point number are incorrectly zeroized. However, we show that the discrepancy doesn’t effect the complex fast Fourier transform by modeling the floating-point addition, subtraction, and multiplication in CryptoLine. We later implement our …

absolute eprint report falcon normal package point products report submission verification