fiat-crypto 0.2.9 is the machine-generated, formally-verified Rust extraction of the Fiat Cryptography project: field-arithmetic primitives for P-224, P-256, P-384, P-521, Curve25519, secp256k1, p434, and Poly1305. VCS byte-equivalence holds. No unsafe code, no I/O, no build-time execution, no dependencies, and no binary artefacts. No findings. Correctness and constant-time claims are left unasserted; the upstream Coq proofs are the documented correctness evidence.
fiat-crypto 0.2.9 is the extracted Rust output of the Fiat Cryptography project from MIT. It contains machine-generated, formally-verified field-arithmetic implementations for P-224, P-256, P-384, P-521, Curve25519, secp256k1, p434 (SIKE), Poly1305, and related scalar fields. Each implementation covers the primitive field operations: multiply, square, add, subtract, negate, Montgomery encode/decode, serialise, and deserialise. The crate exposes 28 public modules totalling approximately 83K lines of safe Rust (edition 2018, no_std compatible). The generation pipeline extracts Rust code from Coq proofs that establish correctness and constant-time behavior for each output; the Rust files carry autogeneration headers identifying the exact extraction command that produced them.
The published crate contents were compared against the upstream Git repository at the commit recorded in .cargo_vcs_info.json using diff -rq. All source files were surveyed for unsafe code, network calls, filesystem operations, process execution, environment access, and concurrency via grep; each returned zero matches crate-wide. src/lib.rs (31 lines) was read in full. src/p256_64.rs was read end-to-end as a representative generated module to verify the header provenance comments, type definitions, and function structure. No binary artefacts, no build.rs, and no proc-macro declarations were found.
Scope. crypto-impl-safe, crypto-impl-correct, crypto-impl-tested, algorithm-impl-safe, algorithm-impl-correct, algorithm-impl-tested, and algorithm-impl-bounds were not evaluated and are left unasserted. Correctness and constant-time safety of the generated arithmetic are established upstream by the Fiat Cryptography Coq extraction pipeline; independently re-verifying 83K lines of generated limb arithmetic against the formal proofs is out of scope for this audit. This audit verifies supply-chain integrity (VCS byte-equivalence), the capability surface (uses-crypto, uses-interpreter, uses-jit among others), build/install-time execution, is-benign, and dependency enumeration.
The comparison of contents/src/ against vcs/src/ shows byte-for-byte identity across all 28 generated modules and lib.rs. The only difference between contents/Cargo.toml and vcs/Cargo.toml is cargo's standard normalisation (field reordering, autogenerated header comment, minor whitespace); the Cargo.toml.orig matches the VCS copy exactly.
The crate ships no pre-compiled binary artefacts (has-binaries) and no build.rs (has-build-exec). No #[proc_macro] declarations appear, and the crate is not declared as a proc macro. There is no install hook (has-install-exec).
Source surveys returned zero matches for unsafe, extern "C", network APIs, filesystem APIs, std::process, std::env, and concurrency primitives. The crate is pure safe Rust with no I/O or external calls (uses-unsafe, uses-network, uses-filesystem, uses-exec, uses-environment, uses-concurrency, uses-crypto, uses-interpreter, uses-jit). No dependencies are declared (has-unit-tests, has-integration-tests, has-fuzz-tests, has-property-tests: the published crate contains no test suite; tests exist in the upstream repository but are not included in the published crate).
The generated modules implement finite-field arithmetic for cryptographic groups (impl-crypto, impl-algorithm). Each module's header identifies the Coq extraction command, the curve, the machine word size, and the modulus polynomial; every public function's pre- and post-conditions are documented in formal notation. The crate does not implement parsers, interpreters, JIT, protocols, data structures, or concurrency primitives (impl-parser, impl-interpreter, impl-jit, impl-protocol, impl-datastructure, impl-concurrency).
No malicious patterns were found on a crate-wide survey: no obfuscated strings, no base64 blobs, no hardcoded network addresses, no telemetry (is-benign).
The published crate has no test suite; tests reside in the upstream Fiat Cryptography repository and are excluded from the published crate. The conditional claims crypto-impl-safe, crypto-impl-correct, and crypto-impl-tested were not evaluated; correctness evidence comes from the Fiat Coq extraction pipeline, not from independent manual review.
This audit found no findings. The supply chain is intact: VCS byte-equivalence holds, no binary artefacts are present, and there is no build-time or install-time code execution. The crate's entire surface is 83K lines of generated, safe, no_std Rust arithmetic with zero runtime capabilities beyond pure computation. The conditional claims crypto-impl-safe, crypto-impl-correct, crypto-impl-tested, algorithm-impl-safe, algorithm-impl-correct, algorithm-impl-tested, and algorithm-impl-bounds are left unasserted; the upstream Coq proofs are the documented correctness evidence for this generated code.
No findings.
src/lib.rsEntry point for the crate. Marked #![cfg_attr(not(feature = "std"), no_std)] and annotated "AUTOGENERATED FILE: DO NOT EDIT". Contains only pub mod declarations for the 28 generated field-arithmetic modules. Justifies has-build-exec (no build.rs), uses-unsafe (no unsafe blocks), uses-network, uses-filesystem, uses-exec, uses-environment, uses-concurrency. All of these were confirmed crate-wide via grep (zero matches each).
src/p256_64.rsRepresentative generated module for P-256 (64-bit). The file header identifies the Fiat Cryptography extraction command that produced it: src/ExtractionOCaml/word_by_word_montgomery ... p256 64 '2^256 - 2^224 + 2^192 + 2^96 - 1'. Every public function carries an //! comment specifying its mathematical postconditions and input/output bounds. The implementation consists entirely of ordinary Rust arithmetic on arrays of u64/u32 limbs; no unsafe, no I/O, no external calls. Justifies impl-crypto and impl-algorithm (field arithmetic for elliptic-curve groups). The same structure is uniform across all 28 modules; this module was read as the representative sample.