optimizations.md: formatting fix

1 files changed, 13 insertions, 11 deletions

diff --git a/optimizations.md b/optimizations.md
index 20ac9aaf7..cf9c9fe89 100644
--- a/optimizations.md
+++ b/optimizations.md
@@ -1,11 +1,13 @@
- Category              |  Name                                        |  Status                                                                                                                 |  Lemma(s)                                                                                                                                                                                                                                  |  Description                                                                                                                                                                                                                                     | 
-|-----------------------|----------------------------------------------|-------------------------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| 
-| Field Arithmetic      |  Unsaturated limbs/delayed carrying          |  Implemented                                                                                                            |  [ModularBaseSystemProofs.v#L347](https://github.com/mit-plv/fiat-crypto/blob/master/src/ModularArithmetic/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](https://github.com/mit-plv/fiat-crypto/blob/master/src/ModularArithmetic/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      |  Hex Exponentiation                          |  Not Implemented                                                                                                        |  n/a, TODO                                                                                                                                                                                                                                 |                                                                                                                                                                                                                                                  | 
-| Field Arithmetic      |  Addition Chain Exponentiation               |  Implemented                                                                                                            |  [AdditionChainExponentiation.v#L53](https://github.com/mit-plv/fiat-crypto/blob/master/src/Util/AdditionChainExponentiation.v#L53)                                                                                                        |  https://en.wikipedia.org/wiki/Addition-chain_exponentiation                                                                                                                                                                                     | 
-| Field Arithmetic      |  Precomputed Tables                          |  Not Implemented                                                                                                        |  n/a, TODO                                                                                                                                                                                                                                 |                                                                                                                                                                                                                                                  | 
-| Elliptic Curve Points |  Extended Coordinates                        |  Implemented                                                                                                            |  [ExtendedCoordinates.v#L258](https://github.com/mit-plv/fiat-crypto/blob/master/src/CompleteEdwardsCurve/ExtendedCoordinates.v#L258)                                                                                                      |  http://hyperelliptic.org/EFD/g1p/auto-edwards.html                                                                                                                                                                                              | 
-| Elliptic Curve Points |  Point Compression                           |  Implemented                                                                                                            |  [PointEncodingPre.v#L313](https://github.com/mit-plv/fiat-crypto/blob/master/src/Encoding/PointEncodingPre.v#L313) and [PointEncodingPre.v#L412](https://github.com/mit-plv/fiat-crypto/blob/master/src/Encoding/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](https://github.com/mit-plv/fiat-crypto/blob/master/src/Reflection/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 |                                                                                                                                                                                                                                                  | 
+| Category              |  Name                               |  Status           |  Lemma(s)                                                                                                                                                                                                                                  |  Description                                                                                                                                                                                                                                     | 
+|-----------------------|-------------------------------------|-------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| 
+| Field Arithmetic      |  Unsaturated limbs/delayed carrying |  Implemented      |  [ModularBaseSystemProofs.v#L347](https://github.com/mit-plv/fiat-crypto/blob/master/src/ModularArithmetic/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](https://github.com/mit-plv/fiat-crypto/blob/master/src/ModularArithmetic/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      |  Hex Exponentiation                 |  Not Implemented  |  n/a                                                                                                                                                                                                                                       |  TODO                                                                                                                                                                                                                                            | 
+| Field Arithmetic      |  Addition Chain Exponentiation      |  Implemented      |  [AdditionChainExponentiation.v#L53](https://github.com/mit-plv/fiat-crypto/blob/master/src/Util/AdditionChainExponentiation.v#L53)                                                                                                        |  https://en.wikipedia.org/wiki/Addition-chain_exponentiation                                                                                                                                                                                     | 
+| Field Arithmetic      |  Precomputed Tables                 |  Not Implemented  |  n/a                                                                                                                                                                                                                                       |  TODO                                                                                                                                                                                                                                            | 
+| Elliptic Curve Points |  Extended Coordinates               |  Implemented      |  [ExtendedCoordinates.v#L258](https://github.com/mit-plv/fiat-crypto/blob/master/src/CompleteEdwardsCurve/ExtendedCoordinates.v#L258)                                                                                                      |  http://hyperelliptic.org/EFD/g1p/auto-edwards.html                                                                                                                                                                                              | 
+| Elliptic Curve Points |  Point Compression                  |  Implemented      |  [PointEncodingPre.v#L313](https://github.com/mit-plv/fiat-crypto/blob/master/src/Encoding/PointEncodingPre.v#L313) and [PointEncodingPre.v#L412](https://github.com/mit-plv/fiat-crypto/blob/master/src/Encoding/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](https://github.com/mit-plv/fiat-crypto/blob/master/src/Reflection/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       | 
+
+