Most files in this directory are generated using Fiat Cryptography from the associated library of arithmetic-implementation templates. These files are included under the Apache 2.0 license. (See LICENSE file.)
Some files are included directly from the fiat-c/src directory of the Fiat Cryptography repository. Their contents are #included into source files, so we rename them to .h. Implementations that use saturated arithmetic on 64-bit words are further manually edited to use platform-appropriate incantations for operations such as addition with carry; these changes are marked with “NOTE: edited after generation”.
Files in the asm directory are compiled from Fiat-Cryptography templates using CryptOpt. These generated assembly files have been edited to support call-stack unwinding. The modified files have been checked for functional correctness using the CryptOpt translation validator that is included in the Fiat-Cryptography repository. Correct unwinding and manual assembler-directive changes related to object-file conventions are validated using unit tests.
Routines for which assembly-level optimization is not necessary are written in Bedrock2 and tranlated to C. The file bedrock_unverified_platform.c.inc provides the platform functionality code thus translated expects.
The P256 coordinate subtraction function in 64-bit C code generated by Fiat Cryptography has been manually replaced with a version written in Bedrock. This is an early step towards using Bedrock more widely, both on its own and as an alternative pathway from Fiat Cryptography to C.