Built motion from commit 6a09e18b.|2.6.11

[motion2.git] / legacy-libs / grpc-cloned / deps / grpc / third_party / boringssl / third_party / fiat / README.md

diff --git a/legacy-libs/grpc-cloned/deps/grpc/third_party/boringssl/third_party/fiat/README.md b/legacy-libs/grpc-cloned/deps/grpc/third_party/boringssl/third_party/fiat/README.md
new file mode 100644 (file)
index 0000000..cf66900
--- /dev/null
+++ b/legacy-libs/grpc-cloned/deps/grpc/third_party/boringssl/third_party/fiat/README.md
@@ -0,0 +1,47 @@
+# Fiat
+
+Some of the code in this directory is generated by
+[Fiat](https://github.com/mit-plv/fiat-crypto) and thus these files are
+licensed under the MIT license. (See LICENSE file.)
+
+## Curve25519
+
+To generate the field arithmetic procedures in `curve25519.c` from a fiat-crypto
+checkout (as of `7892c66d5e0e5770c79463ce551193ceef870641`), run
+`make src/Specific/solinas32_2e255m19_10limbs/femul.c` (replacing `femul` with
+the desired field operation). The "source" file specifying the finite field and
+referencing the desired implementation strategy is
+`src/Specific/solinas32_2e255m19_10limbs/CurveParameters.v`, specifying roughly
+"unsaturated arithmetic modulo 2^255-19 using 10 limbs of radix 2^25.5 in 32-bit
+unsigned integers with a single carry chain and two wraparound carries" where
+only the prime is considered normative and everything else is treated as
+"compiler hints".
+
+The 64-bit implementation uses 5 limbs of radix 2^51 with instruction scheduling
+taken from curve25519-donna-c64. It is found in
+`src/Specific/solinas64_2e255m19_5limbs_donna`.
+
+## P256
+
+To generate the field arithmetic procedures in `p256.c` from a fiat-crypto
+checkout, run
+`make src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs/femul.c`.
+The corresponding "source" file is
+`src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs/CurveParameters.v`,
+specifying roughly "64-bit saturated word-by-word Montgomery reduction modulo
+2^256 - 2^224 + 2^192 + 2^96 - 1". Again, everything except for the prime is
+untrusted. There is currently a known issue where `fesub.c` for p256 does not
+manage to complete the build (specialization) within a week on Coq 8.7.0.
+<https://github.com/JasonGross/fiat-crypto/tree/3e6851ddecaac70d0feb484a75360d57f6e41244/src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs>
+does manage to build that file, but the work on that branch was never finished
+(the correctness proofs of implementation templates still apply, but the
+now abandoned prototype specialization facilities there are unverified).
+
+## Working With Fiat Crypto Field Arithmetic
+
+The fiat-crypto readme <https://github.com/mit-plv/fiat-crypto#arithmetic-core>
+contains an overview of the implementation templates followed by a tour of the
+specialization machinery. It may be helpful to first read about the less messy
+parts of the system from chapter 3 of <http://adam.chlipala.net/theses/andreser.pdf>.
+There is work ongoing to replace the entire specialization mechanism with
+something much more principled <https://github.com/mit-plv/fiat-crypto/projects/4>.