diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-01-09 10:45:50 -0500 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-01-09 10:46:26 -0500 |
| commit | 57d1746f125a1a3308da532866a9c5ed466f8c0e (patch) | |
| tree | 92145c85bc4e0263884a7e302aefe345140fcecd /optimizations.md | |
| parent | c4dbf0a6214dfdd4cdc060fd929a667e82a96c5b (diff) | |
Add list of optimizations currently implemented
Diffstat (limited to 'optimizations.md')
| -rw-r--r-- | optimizations.md | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/optimizations.md b/optimizations.md new file mode 100644 index 000000000..af72dcd68 --- /dev/null +++ b/optimizations.md @@ -0,0 +1,11 @@ +| Category | Name | Status | Lemma(s) | | +|-----------------------|-------------------------------------|-------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|------------------| +| Field Arithmetic | Unsaturated limbs/delayed carrying | Implemented | https://github.com/mit-plv/fiat-crypto/blob/master/src/ModularArithmetic/ModularBaseSystemProofs.v#L347 | | +| Field Arithmetic | Division-free Modular Reduction | Implemented | https://github.com/mit-plv/fiat-crypto/blob/master/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v#L41 | | +| Field Arithmetic | Inverse square root | Not Implemented | n/a | | +| Field Arithmetic | Hex Exponentiation | Not Implemented | n/a | | +| Field Arithmetic | Addition Chain Exponentiation | Implemented | https://github.com/mit-plv/fiat-crypto/blob/master/src/Util/AdditionChainExponentiation.v#L53 | | +| Field Arithmetic | Precomputed Tables | Not Implemented | n/a | | +| Elliptic Curve Points | Extended Coordinates | Implemented | https://github.com/mit-plv/fiat-crypto/blob/master/src/CompleteEdwardsCurve/ExtendedCoordinates.v#L258 | | +| Elliptic Curve Points | Point Compression | Implemented | https://github.com/mit-plv/fiat-crypto/blob/master/src/Encoding/PointEncodingPre.v#L313 and https://github.com/mit-plv/fiat-crypto/blob/master/src/Encoding/PointEncodingPre.v#L412 | | +| Low-Level | Use Varied-size Registers | Half-Implemented | https://github.com/mit-plv/fiat-crypto/blob/master/src/Reflection/MapCastWithCastOp.v#L116 | | |