From d3135a69f653034f07b7657486f926a7a20ef3ee Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 1 Jun 2017 23:59:55 -0400 Subject: Strip trailing whitespace With ```bash bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh ``` --- optimizations.md | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'optimizations.md') diff --git a/optimizations.md b/optimizations.md index 90c0bc4e7..ca26adc5e 100644 --- a/optimizations.md +++ b/optimizations.md @@ -1,13 +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 | 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 | 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](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 | 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](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 | 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 | 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](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 | 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](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 | -- cgit v1.2.3