Identified during the 2026 soundness review (#1582, SOUNDNESS.md).
Constant-time properties of the C code are currently tested empirically using valgrind across many compilers and optimization levels, and the C code uses value barriers to prevent harmful compiler optimizations. However, there is no formal verification of constant-time-ness for the C code.
Consider introducing additional verification tooling that allows us to express and verify constant-time properties for the C code.
Identified during the 2026 soundness review (#1582, SOUNDNESS.md).
Constant-time properties of the C code are currently tested empirically using valgrind across many compilers and optimization levels, and the C code uses value barriers to prevent harmful compiler optimizations. However, there is no formal verification of constant-time-ness for the C code.
Consider introducing additional verification tooling that allows us to express and verify constant-time properties for the C code.