optimizations.md

Category	Name	Status	Lemma(s)	Description
Field Arithmetic	Unsaturated limbs/delayed carrying	Implemented	ModularBaseSystemProofs.v#L347	Represent field elements using more machine words than strictly necessary in order to delay carrying (for example, represent a 255-bit number using 51 bits per 64-bit word)
Field Arithmetic	Division-free Modular Reduction	Implemented	PseudoMersenneBaseParamProofs.v#L41	Reduce $x$ modulo $2^k-c$ by splitting $x$ into $a$ and $b$ such that $a + 2^k * b = x$, then returning $a + c * b$
Field Arithmetic	Inverse square root	Not Implemented	n/a	Compute $\frac{1}{\sqrt{x}}$ rather than $\sqrt{x}$. Then, for example, in order to compute $\sqrt{\frac{x}{y}}$, compute $x * \frac{1}{\sqrt{xy}}$ rather than doing two expensive square root computations
Field Arithmetic	Addition Chain Exponentiation	Implemented	AdditionChainExponentiation.v#L53	https://en.wikipedia.org/wiki/Addition-chain_exponentiation
Field Arithmetic	Specialized Squaring	Not Implemented	n/a	Write a specialized function for squaring field elts rather than just using mul
Field Arithmetic	Karatsuba	Not Implemented	n/a	Use Karatsuba's trick for multiplication (mostly relevant for primes $> 400$ bits in size)
Elliptic Curve Points	Extended Coordinates	Implemented	ExtendedCoordinates.v#L258	http://hyperelliptic.org/EFD/g1p/auto-edwards.html
Elliptic Curve Points	Precomputed Tables	Not Implemented	n/a	Precompute powers of base point
Elliptic Curve Points	Hex Exponentiation	Not Implemented	n/a	Use hexadecimal exponentiation for elliptic curve scalar multiplication
Elliptic Curve Points	Point Compression	Implemented	PointEncodingPre.v#L313 and PointEncodingPre.v#L412	Instead of transmitting $(x,y)$ to transmit a point, transmit $y$ and a bit representing the sign of $x$. Decode $x$ by solving the curve equation for $x^2$, taking the square root, and picking the square root with the appropriate sign bit
Low-Level	Use Varied-size Registers	Half-Implemented	MapCastWithCastOp.v#L116	Rather than using the largest available integer size (e.g., uint32_t on x86_32, uint64_t on x86_64) for all operations, pick the smallest integer size which is guaranteed to fit the result for each arithmetic operation separately