From 57d1746f125a1a3308da532866a9c5ed466f8c0e Mon Sep 17 00:00:00 2001 From: jadep Date: Mon, 9 Jan 2017 10:45:50 -0500 Subject: Add list of optimizations currently implemented --- optimizations.md | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 optimizations.md (limited to 'optimizations.md') 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 | | -- cgit v1.2.3