Tidy up third_party/fiat.
Originally, when we imported fiat-crypto field operations, the pipeline
was in early stages and the generated code had to be manually integrated
with the rest of the curve implementation, so we moved all our
supporting code to third_party/fiat for simplicity. Over time more
supporting code, like the table generators, landed there to be next to
its callers.
fiat-crypto now generates standalone files which we #include into the
supporting code. This moves the supporting code back to the usual
location. It also updates the README.md file to reflect the new
pipeline. (Most of it was a documentation of the old pipeline, which was
much more manual.)
Change-Id: I64db7235feb6566f0d3cd4db3a7146050edaf25a
Reviewed-on: https://boringssl-review.googlesource.com/c/boringssl/+/40904
Commit-Queue: David Benjamin <davidben@google.com>
Reviewed-by: Adam Langley <agl@google.com>
diff --git a/crypto/CMakeLists.txt b/crypto/CMakeLists.txt
index 1d35b97..20af6e4 100644
--- a/crypto/CMakeLists.txt
+++ b/crypto/CMakeLists.txt
@@ -263,6 +263,7 @@
cpu-intel.c
cpu-ppc64le.c
crypto.c
+ curve25519/curve25519.c
curve25519/spake25519.c
dh/dh.c
dh/params.c
@@ -420,7 +421,6 @@
x509v3/v3_skey.c
x509v3/v3_sxnet.c
x509v3/v3_utl.c
- ../third_party/fiat/curve25519.c
$<TARGET_OBJECTS:fipsmodule>
diff --git a/third_party/fiat/curve25519.c b/crypto/curve25519/curve25519.c
similarity index 97%
rename from third_party/fiat/curve25519.c
rename to crypto/curve25519/curve25519.c
index 564becb..232f6e0 100644
--- a/third_party/fiat/curve25519.c
+++ b/crypto/curve25519/curve25519.c
@@ -1,29 +1,21 @@
-// The MIT License (MIT)
-//
-// Copyright (c) 2015-2016 the fiat-crypto authors (see the AUTHORS file).
-//
-// Permission is hereby granted, free of charge, to any person obtaining a copy
-// of this software and associated documentation files (the "Software"), to deal
-// in the Software without restriction, including without limitation the rights
-// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-// copies of the Software, and to permit persons to whom the Software is
-// furnished to do so, subject to the following conditions:
-//
-// The above copyright notice and this permission notice shall be included in all
-// copies or substantial portions of the Software.
-//
-// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-// SOFTWARE.
+/* Copyright (c) 2020, Google Inc.
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
+ * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION
+ * OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN
+ * CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. */
// Some of this code is taken from the ref10 version of Ed25519 in SUPERCOP
// 20141124 (http://bench.cr.yp.to/supercop.html). That code is released as
-// public domain but parts have been replaced with code generated by Fiat
-// (https://github.com/mit-plv/fiat-crypto), which is MIT licensed.
+// public domain. Other parts have been replaced to call into code generated by
+// Fiat (https://github.com/mit-plv/fiat-crypto) in //third_party/fiat.
//
// The field functions are shared by Ed25519 and X25519 where possible.
@@ -39,16 +31,16 @@
#include <openssl/type_check.h>
#include "internal.h"
-#include "../../crypto/internal.h"
+#include "../internal.h"
// Various pre-computed constants.
#include "./curve25519_tables.h"
#if defined(BORINGSSL_CURVE25519_64BIT)
-#include "./curve25519_64.h"
+#include "../../third_party/fiat/curve25519_64.h"
#else
-#include "./curve25519_32.h"
+#include "../../third_party/fiat/curve25519_32.h"
#endif // BORINGSSL_CURVE25519_64BIT
diff --git a/third_party/fiat/curve25519_tables.h b/crypto/curve25519/curve25519_tables.h
similarity index 99%
rename from third_party/fiat/curve25519_tables.h
rename to crypto/curve25519/curve25519_tables.h
index c293e95..310581c 100644
--- a/third_party/fiat/curve25519_tables.h
+++ b/crypto/curve25519/curve25519_tables.h
@@ -1,24 +1,16 @@
-// The MIT License (MIT)
-//
-// Copyright (c) 2015-2016 the fiat-crypto authors (see the AUTHORS file).
-//
-// Permission is hereby granted, free of charge, to any person obtaining a copy
-// of this software and associated documentation files (the "Software"), to deal
-// in the Software without restriction, including without limitation the rights
-// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-// copies of the Software, and to permit persons to whom the Software is
-// furnished to do so, subject to the following conditions:
-//
-// The above copyright notice and this permission notice shall be included in
-// all copies or substantial portions of the Software.
-//
-// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-// SOFTWARE.
+/* Copyright (c) 2020, Google Inc.
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
+ * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION
+ * OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN
+ * CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. */
// This file is generated from
// ./make_curve25519_tables.py > curve25519_tables.h
diff --git a/third_party/fiat/internal.h b/crypto/curve25519/internal.h
similarity index 74%
rename from third_party/fiat/internal.h
rename to crypto/curve25519/internal.h
index be3e265..01be307 100644
--- a/third_party/fiat/internal.h
+++ b/crypto/curve25519/internal.h
@@ -1,24 +1,16 @@
-// The MIT License (MIT)
-//
-// Copyright (c) 2015-2016 the fiat-crypto authors (see the AUTHORS file).
-//
-// Permission is hereby granted, free of charge, to any person obtaining a copy
-// of this software and associated documentation files (the "Software"), to deal
-// in the Software without restriction, including without limitation the rights
-// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-// copies of the Software, and to permit persons to whom the Software is
-// furnished to do so, subject to the following conditions:
-//
-// The above copyright notice and this permission notice shall be included in all
-// copies or substantial portions of the Software.
-//
-// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-// SOFTWARE.
+/* Copyright (c) 2020, Google Inc.
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
+ * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION
+ * OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN
+ * CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. */
#ifndef OPENSSL_HEADER_CURVE25519_INTERNAL_H
#define OPENSSL_HEADER_CURVE25519_INTERNAL_H
@@ -29,7 +21,7 @@
#include <openssl/base.h>
-#include "../../crypto/internal.h"
+#include "../internal.h"
#if defined(OPENSSL_ARM) && !defined(OPENSSL_NO_ASM) && !defined(OPENSSL_APPLE)
diff --git a/third_party/fiat/make_curve25519_tables.py b/crypto/curve25519/make_curve25519_tables.py
similarity index 66%
rename from third_party/fiat/make_curve25519_tables.py
rename to crypto/curve25519/make_curve25519_tables.py
index 22936d9..50dee2a 100755
--- a/third_party/fiat/make_curve25519_tables.py
+++ b/crypto/curve25519/make_curve25519_tables.py
@@ -1,26 +1,18 @@
#!/usr/bin/env python
# coding=utf-8
-# The MIT License (MIT)
+# Copyright (c) 2020, Google Inc.
#
-# Copyright (c) 2015-2016 the fiat-crypto authors (see the AUTHORS file).
+# Permission to use, copy, modify, and/or distribute this software for any
+# purpose with or without fee is hereby granted, provided that the above
+# copyright notice and this permission notice appear in all copies.
#
-# Permission is hereby granted, free of charge, to any person obtaining a copy
-# of this software and associated documentation files (the "Software"), to deal
-# in the Software without restriction, including without limitation the rights
-# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-# copies of the Software, and to permit persons to whom the Software is
-# furnished to do so, subject to the following conditions:
-#
-# The above copyright notice and this permission notice shall be included in all
-# copies or substantial portions of the Software.
-#
-# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-# SOFTWARE.
+# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
+# SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION
+# OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN
+# CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
import StringIO
import subprocess
@@ -149,27 +141,19 @@
buf = StringIO.StringIO()
- buf.write("""// The MIT License (MIT)
-//
-// Copyright (c) 2015-2016 the fiat-crypto authors (see the AUTHORS file).
-//
-// Permission is hereby granted, free of charge, to any person obtaining a copy
-// of this software and associated documentation files (the "Software"), to deal
-// in the Software without restriction, including without limitation the rights
-// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-// copies of the Software, and to permit persons to whom the Software is
-// furnished to do so, subject to the following conditions:
-//
-// The above copyright notice and this permission notice shall be included in
-// all copies or substantial portions of the Software.
-//
-// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-// SOFTWARE.
+ buf.write("""/* Copyright (c) 2020, Google Inc.
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
+ * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION
+ * OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN
+ * CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. */
// This file is generated from
// ./make_curve25519_tables.py > curve25519_tables.h
diff --git a/crypto/curve25519/spake25519.c b/crypto/curve25519/spake25519.c
index 650178c..f750911 100644
--- a/crypto/curve25519/spake25519.c
+++ b/crypto/curve25519/spake25519.c
@@ -23,7 +23,7 @@
#include <openssl/sha.h>
#include "../internal.h"
-#include "../../third_party/fiat/internal.h"
+#include "./internal.h"
// The following precomputation tables are for the following
diff --git a/crypto/curve25519/spake25519_test.cc b/crypto/curve25519/spake25519_test.cc
index 71c9771..df20ec8 100644
--- a/crypto/curve25519/spake25519_test.cc
+++ b/crypto/curve25519/spake25519_test.cc
@@ -23,7 +23,7 @@
#include <gtest/gtest.h>
#include "../internal.h"
-#include "../../third_party/fiat/internal.h"
+#include "./internal.h"
// TODO(agl): add tests with fixed vectors once SPAKE2 is nailed down.
diff --git a/crypto/fipsmodule/bcm.c b/crypto/fipsmodule/bcm.c
index 567a0cd..4a53c32 100644
--- a/crypto/fipsmodule/bcm.c
+++ b/crypto/fipsmodule/bcm.c
@@ -70,7 +70,7 @@
#include "ec/felem.c"
#include "ec/oct.c"
#include "ec/p224-64.c"
-#include "../../third_party/fiat/p256.c"
+#include "ec/p256.c"
#include "ec/p256-x86_64.c"
#include "ec/scalar.c"
#include "ec/simple.c"
diff --git a/third_party/fiat/p256.c b/crypto/fipsmodule/ec/p256.c
similarity index 95%
rename from third_party/fiat/p256.c
rename to crypto/fipsmodule/ec/p256.c
index f3f03e5..9abac0b 100644
--- a/third_party/fiat/p256.c
+++ b/crypto/fipsmodule/ec/p256.c
@@ -1,31 +1,20 @@
-// The MIT License (MIT)
-//
-// Copyright (c) 2015-2016 the fiat-crypto authors (see the AUTHORS file).
-//
-// Permission is hereby granted, free of charge, to any person obtaining a copy
-// of this software and associated documentation files (the "Software"), to deal
-// in the Software without restriction, including without limitation the rights
-// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-// copies of the Software, and to permit persons to whom the Software is
-// furnished to do so, subject to the following conditions:
-//
-// The above copyright notice and this permission notice shall be included in all
-// copies or substantial portions of the Software.
-//
-// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-// SOFTWARE.
+/* Copyright (c) 2020, Google Inc.
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
+ * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION
+ * OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN
+ * CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. */
-// The field arithmetic code is generated by Fiat
-// (https://github.com/mit-plv/fiat-crypto), which is MIT licensed.
-//
// An implementation of the NIST P-256 elliptic curve point multiplication.
-// 256-bit Montgomery form, generated using fiat-crypto, for 64 and 32-bit.
-// Field operations with inputs in [0,p) return outputs in [0,p).
+// 256-bit Montgomery form for 64 and 32-bit. Field operations are generated by
+// Fiat, which lives in //third_party/fiat.
#include <openssl/base.h>
@@ -38,17 +27,17 @@
#include <assert.h>
#include <string.h>
-#include "../../crypto/fipsmodule/delocate.h"
-#include "../../crypto/fipsmodule/ec/internal.h"
-#include "../../crypto/internal.h"
+#include "../../internal.h"
+#include "../delocate.h"
+#include "./internal.h"
// MSVC does not implement uint128_t, and crashes with intrinsics
#if defined(BORINGSSL_HAS_UINT128)
#define BORINGSSL_NISTP256_64BIT 1
-#include "p256_64.h"
+#include "../../../third_party/fiat/p256_64.h"
#else
-#include "p256_32.h"
+#include "../../../third_party/fiat/p256_32.h"
#endif
diff --git a/third_party/fiat/README.md b/third_party/fiat/README.md
index cf66900..56accd4 100644
--- a/third_party/fiat/README.md
+++ b/third_party/fiat/README.md
@@ -1,47 +1,8 @@
# Fiat
-Some of the code in this directory is generated by
+This directory contains code 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>.
+The files are imported from the `fiat-c/src` directory of the Fiat repository.
+Their contents are `#include`d into source files, so we rename them to `.h`.
diff --git a/util/generate_build_files.py b/util/generate_build_files.py
index 22e19e3..23d7ea5 100644
--- a/util/generate_build_files.py
+++ b/util/generate_build_files.py
@@ -846,12 +846,6 @@
tool_c_files = FindCFiles(os.path.join('src', 'tool'), NoTests)
tool_h_files = FindHeaderFiles(os.path.join('src', 'tool'), AllFiles)
- # third_party/fiat/p256.c lives in third_party/fiat, but it is a FIPS
- # fragment, not a normal source file.
- p256 = os.path.join('src', 'third_party', 'fiat', 'p256.c')
- fips_fragments.append(p256)
- crypto_c_files.remove(p256)
-
# BCM shared library C files
bcm_crypto_c_files = [
os.path.join('src', 'crypto', 'fipsmodule', 'bcm.c')
