blob: bb41dffdb488e9d64eddea8384767ae20bc674cf (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
| Category | Name | Status | Lemma(s) | |
|-----------------------|-------------------------------------|-------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|------------------|
| Field Arithmetic | Unsaturated limbs/delayed carrying | Implemented | [ModularBaseSystemProofs.v#L347](https://github.com/mit-plv/fiat-crypto/blob/master/src/ModularArithmetic/ModularBaseSystemProofs.v#L347) | |
| Field Arithmetic | Division-free Modular Reduction | Implemented | [PseudoMersenneBaseParamProofs.v#L41](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 | [AdditionChainExponentiation.v#L53](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 | [ExtendedCoordinates.v#L258](https://github.com/mit-plv/fiat-crypto/blob/master/src/CompleteEdwardsCurve/ExtendedCoordinates.v#L258) | |
| 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) | |
| 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) | |
|
