# Fiat Cryptography

Most files in this directory are generated using [Fiat
Cryptography](https://github.com/mit-plv/fiat-crypto) 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 `#include`d 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`".

# CryptOpt

Files in the `asm` directory are compiled from Fiat-Cryptography templates
using [CryptOpt](https://github.com/0xADE1A1DE/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.

# Bedrock

Routines for which assembly-level optimization is not necessary are written in
[Bedrock2](https://github.com/mit-plv/bedrock2) and tranlated to C. The file
`bedrock_unverified_platform.c.inc` provides the platform functionality code
thus translated expects.

The P256 point doubling and addition are implemented in this manner in
p256_coord.br.c.inc. This code originates from Fiat Cryptogaphy commit
6e22d333861d51c7f6baa0826648a2215d0c333f file src/Bedrock/P256.v
Field arithmetic operations are dispatched in p256_field.c.inc to
platform-specific code including assembly, fiat-crypto-generated C, and
Bedrock-generated C.