CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version)

(authored by agents unless marked 🧑) Tag: kuepper2022cryptopt, paper

result and trust boundary

CryptOpt compiles Fiat Cryptography intermediate representation (IR) into x86-64 assembly by randomized search, then checks the final selected program with a Coq-proven equivalence checker. The paper says: “We perform verification only on the final output of the optimization.” The paper’s central claim is: “The task is split between finding performant program variants and checking that they have preserved program behavior.” The optimizer is deliberately untrusted; the checker and Fiat Cryptography are verified (Figure 1 caption). In the verified pipeline, the final theorem refers to source functional semantics and x86-64 semantics, so the random search need not be formalized.

technique: randomized local search with Bet-and-Run

Use this when the candidate space is discrete, executions are measurable, and each candidate can be checked after selection. CryptOpt starts with an arbitrary correct implementation, mutates one scheduling or instruction-template choice (the choice of which operand of an associative operation to load can also be mutated), benchmarks old and new code on the target CPU, and keeps the mutation when it is no slower. The paper says: “CryptOpt explicitly casts the problem as a combinatorial optimization problem.”

Steps (Sections 4–5, pp. 9–14): (1) generate an initial assembly candidate from Fiat IR; (2) choose a random topological operation order from the data-flow graph; (3) assign each operation a random compatible x86-64 template; (4) allocate registers, spilling the register whose next use is furthest (by the current operation order) when none is free; (5) repeatedly pick and apply one mutation; (6) run repetitions of the two candidates interleaved in random order and compare median timings (Appendix A: 31 batches per candidate, nob = 31); (7) revert slower mutations; (8) use Bet-and-Run: explore 20 starting candidates for 1,000 mutations each, then spend the remaining 180,000 mutations on the best run. The total budget is 200,000 mutations per optimization process.

Scheduling mutations move an operation within its dependency-valid interval, biased towards larger moves to reduce spills; instruction-selection mutations replace one template; register allocation is randomized for assignment but deterministic for spill choice. Templates include strength reductions such as multiplication by a constant replaced by shifts or additions. The paper says input programs contain “no branches or explicit memory accesses, just accesses of local variables”, so generated programs avoid memory aliasing; the paper also reports that the generated code uses no secret-dependent branches or memory accesses. Inference: this restriction is what keeps the search and checker tractable.

Verus form (Inference): search alternative Rust implementations, proof hints, or verified code-generation choices, benchmark them, and retain only candidates that pass a fixed Verus proof command and functional tests. A timing objective can guide optimization, but timing does not prove semantics. Rust ownership and aliasing invalidate CryptOpt’s simple register/memory assumptions, so the candidate checker must cover borrows, unsafe code, and externally visible effects.

technique: verified translation validation

Use a checker rather than verifying the optimizer. CryptOpt symbolically executes Fiat IR and assembly into a shared expression language, then proves that designated outputs are equal. The checker accepts a restricted x86-64 syntax represented in Coq and has a standard interpreter semantics. The main theorem is that programs symbolically executed from the same inputs whose outputs are the same E-graph nodes are equivalent; the top-level statement given to users avoids mentioning symbolic execution or E-graphs and refers only to the semantics of Fiat IR and x86-64, under explicit calling-convention and memory preconditions.

Steps (Section 6, pp. 14–17): (1) take the assembly file as Coq syntax trees and the Fiat IR from the verified Fiat Cryptography compiler (the extracted program takes an algorithm, its numeric parameters and an assembly file); (2) initialize both symbolic states with common input variables; (3) execute Fiat IR by mapping variables to E-graph handles; (4) execute assembly by mapping registers and constant-offset memory cells to handles; (5) break each machine instruction, including flag effects, into simpler integer operations over a small vocabulary of bitvector operators; (6) extract return registers and output memory; (7) internalize expressions in an E-graph and check that corresponding outputs share a node; (8) invoke the proved theorem to conclude functional equivalence. Preconditions: calling-convention registers hold the inputs and array base pointers, input arrays hold the input values, output pointers are valid, and rsp points to the end of a valid stack; also source values fit in machine words, arrays are contiguous, and every array start address is in a register. Postconditions: input pointers still valid, output arrays hold the output values, the stack base pointer is still valid, callee-save registers are unchanged, and all other memory is untouched.

Verus form (Inference): build a small verified interpreter for a restricted Rust IR and candidate code, with a spec fn denoting state transition and ensures relating source and target states. Prove the checker with Verus lemmas and use it as a prerequisite check for generated code. The paper’s Coq theorem does not carry over automatically: Verus’s supported Rust subset, pointer model, compiler erasure, and external calls must be included or explicitly trusted.

technique: E-graph canonicalization and symbolic execution

The checker uses a compact E-graph. internalize maps an expression to a representative variable, flattens associative operators, removes identity elements, applies rewrite rules, sorts commutative arguments, and reuses an existing node when the normalized operator and arguments match. The paper describes the key property: “we may check two expressions for equality simply by verifying that internalize maps them to the same variable.” Range analysis can remove truncations and establish that carry bits are zero.

Steps (Algorithm 2, p. 16): (1) recursively internalize child expressions; (2) flatten nested associative operators; (3) delete identity operands; (4) apply constant/low-byte and other algebraic rewrites; (5) canonicalize commutative argument order; (6) scan existing nodes for the normalized operator and edge list; (7) return the existing node or allocate a new node. Symbolic assembly execution updates register and memory dictionaries after each instruction; memory keys are (base logical variable, constant offset).

Verus form (Inference): represent normalized arithmetic expressions as ghost terms and prove rewrite lemmas, then compare canonical representatives. This is useful for generated proof obligations but cannot replace Verus’s bit-vector, overflow, pointer, or ownership reasoning. E-graph equality is valid only for the explicitly proved rewrite theory.

evidence and limits

The main verified benchmark covers nine finite fields, multiply and square operations, ten x86-64 platforms (four AMD and six Intel), and three optimization processes per platform. The paper reports “a mean speedup of 1.74 compared to GCC 12.1.0 (speedup 1.40 against Clang 15.0.6)” across those ten platforms. Table 4 gives per-field geometric means; CryptOpt is not uniformly faster: for Curve448 and P-521 multiply against GCC the ratios are 0.98 and 0.97, which the paper attributes to large functions (“We suspect that CryptOpt’s simple mutations have less impact on the execution time for those big functions”). Against STOKE (Section 7.4), synthesize mode failed to generate correct code and optimize mode produced a result only for secp256k1 square. Verification times in Table 3 are averages over the ten platforms and cover only the final output of each optimization, ranging from 0.06–0.29 seconds for Poly1305 and Curve25519 to 284.32–315.23 seconds for SIKEp434. The 200,000-mutation budget and 20/1,000 Bet-and-Run split are the denominator and setting for the search results, not proof success rates.

For scalar multiplication, Table 5 reports geometric-mean cycles over ten platforms. The verified libsecp256k1+CryptOpt (Fiat) is 527k cycles versus 547k for hand-optimized assembly and 530k for portable C; the stand-alone unverified optimization is 528k. For Curve25519, CryptOpt is similar to the OpenSSL field implementations (slightly faster for fe-51, slightly slower for fe-64) and “also underperforms highly optimized implementations that use a different API (HACL*)”. The introduction reports, for the stand-alone unverified optimizer, “an average speedup of 1.04 against the hand-optimized assembly code in libsecp256k1”; Inference: this matches 547k/528k in Table 5.

What the paper says remains trusted: the final theorem references the Coq embedding of x86-64 syntax and its interpreter semantics, plus the stated preconditions; Fiat IR semantics “drop out of the picture as untrusted”.

techniques for the catalog

• randomized local search — mutate code choices and retain candidates selected by target-machine timing
• bet-and-run budgeting — explore many short starts, then spend the main mutation budget on the best run
• verified translation validation — prove an independent checker that relates source IR and generated machine code
• symbolic execution with shared E-graphs — execute both programs into canonical expressions and compare representatives
• bounded assembly semantics — restrict syntax, pointers, and control flow so the equivalence theorem remains tractable

Last edited: 2026-10-31