odin-lang.Odin/core/crypto/_fiat

fiat

This package contains low level arithmetic required to implement certain cryptographic primitives, ported from the fiat-crypto project along with some higher-level helpers.

Notes

fiat-crypto gives the choice of 3 licenses for derived works. The 1-Clause BSD license is chosen as it is compatible with Odin's existing licensing.

The routines are intended to be timing-safe, as long as the underlying integer arithmetic is constant time. This is true on most systems commonly used today, with the notable exception of WASM.

While fiat-crypto provides both output targeting both 32-bit and 64-bit architectures, only the 64-bit versions were used, as 32-bit architectures are becoming increasingly uncommon and irrelevant.

With the current Odin syntax, the Go output is trivially ported in most cases and was used as the basis of the port.

In the future, it would be better to auto-generate Odin either directly by adding an appropriate code-gen backend written in Coq, or perhaps by parsing the JSON output.

As this is a port rather than autogenerated output, none of fiat-crypto's formal verification guarantees apply, unless it is possible to prove binary equivalence.

For the most part, alterations to the base fiat-crypto generated code was kept to a minimum, to aid auditability. This results in a somewhat ideosyncratic style, and in some cases minor performance penalties.