libntruprime is intended to become a central target for verification of full functional correctness of implementations of sntrup. Full functional correctness of an sntrup implementation means that the implementation computes the same output as the NTRU Prime Sage package for all possible inputs. This document tracks what has been verified so far and what has not.

Changes in C compilers and in assemblers often change the behavior of software and might introduce bugs where no bugs existed before. Some tools address this by verifying correctness at the machine-language level. It is important to re-run these tools whenever new binaries are produced.

Changes in CPUs can also introduce bugs where no bugs existed before. Verification is always relative to a model of CPU behavior, and physical CPUs often deviate from these models, sometimes in problematic ways.

There is also a risk that current or future versions of Sage do not correctly compute the documented Sage functions used by the Sage package. This can interfere with falsifiability: even if the CPU matches the model, a bug in an sntrup implementation could be hidden by a bug in Sage.

The supercop/crypto_kem/sntrup* checksums match the checksums produced by libntruprime and checksums produced by the Sage package. These checksums are hashes of outputs for various pseudorandomly generated inputs (with randomness treated as another input). However, there could be bugs for other inputs.

Various runs under valgrind and asan have not detected any abnormal use of RAM. However, valgrind will not notice overflows from a C variable into an adjacent C variable; asan will not notice overflows in assembly language; and neither tool addresses the risk of bugs for rare inputs.

The NTT software used inside libntruprime comes from nttcompiler and has been computer-verified to work correctly on all inputs. The sorting software used inside libntruprime comes from djbsort and has also been computer-verified to work correctly on all inputs. However, there could be bugs in the verification tools, and there are other computations happening inside libntruprime.