Abstract CairoZero is a programming language for running decentralized applications (dApps) at scale. Programs written in the CairoZero language are compiled to machine code for the Cairo CPU architecture and cryptographic protocols are used to verify the results of execution efficiently on blockchain. We explain how we have extended the CairoZero compiler with tooling that enables users to prove, in the Lean 3 proof assistant, that compiled code satisfies high-level functional specifications. We demonstrate the success of our approach by verifying primitives for computation with the secp256k1 and secp256r1 curves over a large finite field as well as the validation of cryptographic signatures using the former. We also verify a mechanism for simulating a read-write dictionary data structure in a read-only setting. Finally, we reflect on our methodology and discuss some of the benefits of our approach.

Given disjoint sets S , S' ⊆ 𝔽 q of size n and a function f : S → 𝔽 q , where 𝔽 q is a finite field, the low-degree extension (LDE) of f to S' is the function f ' : S ' → 𝔽 q obtained by restricting the interpolating polynomial of f to S' . LDE computation is a fundamental primitive of modern algebraic coding theory and cryptography. The best asymptotic running time for LDE with parameter n is O(n log n ) arithmetic operations over 𝔽 q - when q and the sets S, S' are special. This running time is achieved via the Fast Fourier Transform (FFT), and requires 𝔽 q to contain a multiplicative subgroup of smooth order ≥ n (smoothness means being the product of small primes). Another variant uses an additive subgroup of smooth order ≥ n . Most finite fields do not contain such a subgroup, which raises the question of computing the LDE in time O(n · log n ) over general finite fields, for some disjoint pair of sets S , S ' of size n . The main result of this paper is a positive answer to this question, presenting O(n log n )-time LDE for special S , S ' shown to exist over all fields, as long as q = Ω( n 2 ). This result is achieved by introducing a new FFT-like transform, the Elliptic Curve Fast Fourier Transform (ECFFT), which gives an approach to fast algorithms (using preprocessing) for polynomial operations over all large finite fields. The key idea is to replace the group of roots of unity with a set of points L ⊂ 𝔽 q suitably related to a well-chosen elliptic curve group over 𝔽 q (the set L itself is not a group). The key advantage of this approach is that elliptic curve groups can be of any size in the Hasse-Weil interval and thus can have subgroups of large, smooth order, which an FFT-like divide and conquer algorithm can exploit. Compare this with multiplicative subgroups over 𝔽 q whose order must divide q − 1. By analogy, our method extends the standard, multiplicative FFT in a similar way to how Lenstra's elliptic curve method [Len87] extended Pollard's p − 1 algorithm [Pol74] for factoring integers. Representing polynomials by their evaluation over (well-chosen) subsets of L , we use the ECFFT to compute the LDE in time O(n log n ). We also give small arithmetic circuits for polynomial multiplication, division, degree-computation, interpolation, evaluation and Reed-Solomon encoding (also known as low-degree extension) with fixed evaluation points , matching the circuit size of classical FFT-based algorithms when the field size q is special. For the classical problems (in the standard representation) of low degree extension with chosen evaluation points, and evaluating elementary symmetric polynomials, this yields the asymptotically smallest known arithmetic circuits. The efficiency of the classical FFT follows from using the 2-to-1 squaring map to reduce the evaluation set of roots of unity of order 2 k to similar groups of size 2 k-i , i > 0. Our algorithms operate similarly, using isogenies of elliptic curves with kernel size 2 as 2-to-1 maps to reduce L of size 2 k to sets of size 2 k-i that are, like L , suitably related to elliptic curves, albeit different ones.

Cryptographic interactive proof systems provide an efficient and scalable means of verifying the results of computation on blockchain. A prover constructs a proof, off-chain, that the execution of a program on a given input terminates with a certain result. The prover then publishes a certificate that can be verified efficiently and reliably modulo commonly accepted cryptographic assumptions. The method relies on an algebraic encoding of execution traces of programs. Here we report on a verification of the correctness of such an encoding of the Cairo model of computation with respect to the STARK interactive proof system, using the Lean 3 proof assistant.