fiat-crypto specs follow papers rather than RFCs. However, there are some correspondences:
https://github.com/mit-plv/fiat-crypto/blob/master/src/Curves/Montgomery/XZProofs.v#L308 proves that the algorithm specified in rfc7748 (curve25519) implements arithmetic on a Montgomery curve.
fiat-crypto eddsa spec follows the paper "EdDSA for more curves", but it is quite close to rfc8032. The curve structure has its own spec in fiat-crypto (CompleteEdwardsCurve.v), the algorithms prescribed in the RFC are proven to implement that specification in https://github.com/mit-plv/fiat-crypto/blob/master/src/Curves/Edwards/XYZT/Basic.v#L89
fiat-crypto specs follow papers rather than RFCs. However, there are some correspondences:
https://github.com/mit-plv/fiat-crypto/blob/master/src/Curves/Montgomery/XZProofs.v#L308 proves that the algorithm specified in
rfc7748(curve25519) implements arithmetic on a Montgomery curve.fiat-crypto eddsa spec follows the paper "EdDSA for more curves", but it is quite close to
rfc8032. The curve structure has its own spec in fiat-crypto (CompleteEdwardsCurve.v), the algorithms prescribed in the RFC are proven to implement that specification in https://github.com/mit-plv/fiat-crypto/blob/master/src/Curves/Edwards/XYZT/Basic.v#L89