Fiat Cryptography v0.1.3

Compatible with Coq 8.18, 8.19; requires OCaml >= 4.08.

What's Changed

• merge MontgomeryEquivalence into MontgomeryLadder by @andres-erbsen in #1841
• merge Group.Scalarmult into MontgomeryLadder, use in x25519_base by @andres-erbsen in #1843
• Edwards twist isomorphism by @andres-erbsen in #1844
• implement and prove Curve25519 scalar clamping by @andres-erbsen in #1845
• Joye double-add ladder for short Weierstrass curves in co-Z arithmetic by @atrieu in #1823
• instantiate Edwards-Montgomery isomorphism for Curve25519 by @andres-erbsen in #1847
• Decide point equality by @andres-erbsen in #1848
• paperify spec by @andres-erbsen in #1849
• move only_mmio_satisfying to bedrock2 by @andres-erbsen in #1852
• Fix typos by @atrieu in #1860
• Remove Bvector by @andres-erbsen in #1864
• Adapt w.r.t. coq/coq#18895. by @ppedrot in #1866
• Adapt w.r.t. coq/coq#18909. by @ppedrot in #1881
• bump bedrock2, use "always" in GarageDoor spec by @andres-erbsen in #1846
• Bump rupicola from 2aa6b13 to e849928 by @dependabot in #1850
• Bump rupicola from e849928 to d9d95af by @dependabot in #1851
• Bump rupicola from 73addd2 to d4a6c84 by @dependabot in #1858
• Bump rupicola from d4a6c84 to 0f4e201 by @dependabot in #1862
• Bump rupicola from 0f4e201 to 6c63c08 by @dependabot in #1863
• Bump rupicola from 6c63c08 to 4036171 by @dependabot in #1867
• Bump rupicola from 4036171 to 7533776 by @dependabot in #1880
• Bump rupicola from 7533776 to a85c012 by @dependabot in #1886
• Bump rewriter from 21b82e9 to 1cd64f2 by @dependabot in #1840
• Bump rewriter from 1cd64f2 to 56ae1fe by @dependabot in #1883
• Bump rewriter from 56ae1fe to b1e8367 by @dependabot in #1885

New Contributors

• @atrieu made their first contribution in #1823

Full Changelog: v0.1.2...v0.1.3