v0.1.6: Ed25519: Cleanup Basic.v

Rename, shorten, and revise some proofs and definitions in Basic.v, also
add a Module to make it more clear that we're working with extended
coordinates. Some of this may be personal preference.

Fiat Cryptography v0.1.5

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

What's Changed

Dependency Updates

• Actions and Tools

  • Bump actions/cache from 3 to 4 by @dependabot in #1910
  • Bump JamesIves/github-pages-deploy-action from 4.6.0 to 4.6.1 by @dependabot in #1914
  • Bump JamesIves/github-pages-deploy-action from 4.6.1 to 4.6.3 by @dependabot in #1927
  • Bump JamesIves/github-pages-deploy-action from 4.6.3 to 4.6.4 by @dependabot in #1952
  • Bump JamesIves/github-pages-deploy-action from 4.6.8 to 4.6.9 by @dependabot in #1987
  • Bump JamesIves/github-pages-deploy-action from 4.6.9 to 4.7.1 by @dependabot in #1990
  • Bump JamesIves/github-pages-deploy-action from 4.7.1 to 4.7.2 by @dependabot in #1991
  • Bump actions/setup-java from 4.2.1 to 4.2.2 by @dependabot in #1942
  • Bump actions/setup-java from 4.2.2 to 4.3.0 by @dependabot in #1956
  • Bump actions/setup-java from 4.3.0 to 4.4.0 by @dependabot in #1967
  • Bump actions/setup-java from 4.4.0 to 4.5.0 by @dependabot in #1978
  • Bump actions/setup-java from 4.5.0 to 4.6.0 by @dependabot in #1996
  • Bump ocaml/setup-ocaml from 2 to 3 by @dependabot in #1925
  • Bump ocaml/setup-ocaml from 2 to 3 by @dependabot in #1939
  • Downgrade setup-ocaml to v3.2.16 by @JasonGross in #2078

• Project Dependencies

  • Bump rupicola from a85c012 to dc1e8f3 by @dependabot in #1911
  • Bump rupicola from dc1e8f3 to e4eb40b by @dependabot in #1920
  • Bump rupicola from e4eb40b to 71a5a07 by @dependabot in #1921
  • Bump rupicola from 71a5a07 to 0a93e26 by @dependabot in #1926
  • Bump rupicola from 0a93e26 to faef55d by @dependabot in #1931
  • Bump rupicola from faef55d to 941374a by @dependabot in #1932
  • Bump rupicola from 941374a to d55f2d7 by @dependabot in #1948
  • Bump rupicola from d55f2d7 to e7771d9 by @dependabot in #1968
  • Bump rupicola from e7771d9 to 7c4588d by @dependabot in #1995
  • Bump rupicola from 7c4588d to 24f4a75 by @dependabot in #1998
  • Bump rupicola from 7858221 to 00778a5 by @dependabot in #2064
  • Bump rupicola from 1f7e333 to 41662e4 by @dependabot in #2067
  • Bump rupicola from 41662e4 to 59751db by @dependabot in #2082
  • Bump rewriter from 9dd74a9 to edcec73 by @dependabot in #1918
  • Bump rewriter from edcec73 to 2315c27 by @dependabot in #1935
  • Bump rewriter from 2315c27 to 19f344b by @dependabot in #1937
  • Bump rewriter from 19f344b to 1ce9f1a by @dependabot in #1963
  • Bump rewriter from 1ce9f1a to 76973c4 by @dependabot in #1975
  • Bump rewriter from 76973c4 to e4d987c by @dependabot in #1977
  • Bump rewriter from e4d987c to edd0611 by @dependabot in #1981
  • Bump rewriter from edd0611 to 8ab716a by @dependabot in #1988
  • Bump rewriter from 8ab716a to 1e36197 by @dependabot in #1994
  • Bump rewriter from 1e36197 to 30c8507 by @dependabot in #1999
  • Bump rewriter from 30c8507 to 69cccb7 by @dependabot in #2002
  • Bump rewriter from 69cccb7 to 1e17dcd by @dependabot in #2008
  • Bump rewriter from 1e17dcd to 869b054 by @dependabot in #2033
  • Bump rewriter from 869b054 to e8da092 by @dependabot in #2063
  • Bump rewriter from e8da092 to 4b028fc by @dependabot in #2072
  • Bump rewriter from 4b028fc to 9496def by @dependabot in #2073
  • Bump coqprime from d5935ca to 6c225a2 by @dependabot in #1917
  • Bump coqprime from 6c225a2 to 845c00c by @dependabot in #1984
  • Bump coqprime from 845c00c to 09db3f8 by @dependabot in #2006
  • Bump coqprime from 09db3f8 to f23d095 by @dependabot in #2086
  • Bump etc/coq-scripts from e4d9e81 to 4327aa1 by @dependabot in #1974
  • Bump etc/coq-scripts from 4327aa1 to bf7754a by @dependabot in #2003
  • Bump etc/coq-scripts from bf7754a to fdfd924 by @dependabot in #2026

CI and Build Improvements

• Make build.zig files compatible with newly released zig 0.12 by @jedisct1 in #1913
• Pin Zig to the current stable version instead of master by @jedisct1 in #1951
• Update to Zig 0.14 by @jedisct1 in #2031
• [CI] [Haskell] Increase heap size to avoid heap overflow by @JasonGross in #1915
• [CI] [debian] Containerize testing of standalone by @JasonGross in #1924
• [CI] macOS 11 is no longer available on GHA by @JasonGross in #1928
• [CI] [Windows] Bump to OCaml 4.13.1 by @JasonGross in #1936
• use python-is-python3 by @JasonGross in #1938
• fix Debian CI by @JasonGross in #1946
• [CI] [Debian] use -j1 on js-of-ocaml by @JasonGross in #1947
• [CI] [Debian] sudo work around broken git config by @JasonGross in #1949
• [CI] [Windows] Attempt to fix Windows CI by @JasonGross in #1962
• [CI] Pin action steps that use setup-ocaml to ubuntu 22.04 by @JasonGross in #1971
• Revert "[CI] Pin action steps that use setup-ocaml to ubuntu 22.04" by @JasonGross in #1976
• Work around issue with brew and opam by @JasonGross in #1989
• Remove --output-sync from build log when make fails by @JasonGross in #2010
• Upload *.timing files on failure by @JasonGross in #2012
• Add a workflow_dispatch for running timing diffs on CI by @JasonGross in #2022
• [CI] [alpine-edge] coq => rocq by @JasonGross in #2066
• [CI] update wasm_of_ocaml by @JasonGross in #2074
• fix: ulimit typo by @Daniel-Aaron-Bloom in #2079

WebAssembly and JavaScript

• Also install .wasm.map files by @JasonGross in #1908
• [js] Set up workers earlier by @JasonGross in #1941
• Attempt to fix wasm_of_ocaml by @JasonGross in #1958
• Don't sed wasm files, instead use subfolders to ensure the binary names are correct from the start by @JasonGross in #1961
• Add support for wasm files in assets subdirectory by @JasonGross in #1966
• Fix wasm_of_ocaml version, hopefully by @JasonGross in #1986

Performance and Optimization

• Greatly reduce the compilation time of src/Arithmetic/BarrettReduction.v ...

Fiat Cryptography v0.1.4

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

What's Changed

• Releases now distribute universal (x86_64+arm64) binaries for MacOS
  • Build universal (x86_64+arm64) binaries for MacOS by @JasonGross in #1891
• Misc
  • Bump rewriter from b1e8367 to 9dd74a9 by @dependabot in #1904
  • Disable implicit suffix rules in submakefiles by @JasonGross in #1902

Full Changelog: v0.1.3...v0.1.4

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. rocq-prover/rocq#18895. by @ppedrot in #1866
• Adapt w.r.t. rocq-prover/rocq#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

Fiat Cryptography v0.1.2

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

What's Changed

• Adapt to rocq-prover/rocq#18590 by @proux01 in #1821
• adapt to rocq-prover/rocq#18730 by @andres-erbsen in #1826
• bump rupicola (requires Coq >= 8.18) by @samuelgruetter in #1818
• Bump rupicola from e047275 to 7259f52 by @dependabot in #1835
• Bump rewriter from 3342e29 to 21b82e9 by @dependabot in #1819

Full Changelog: v0.1.1...v0.1.2

Fiat Cryptography v0.1.1

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

Last release compatible with Coq 8.17

What's Changed

• fiat-crypto code generator now runs on the web!
  • Add js_of_ocaml build and deployment by @JasonGross in #1737
  • Use WebWorkers and a cache for js-of-ocaml by @JasonGross in #1739
  • Add wasm_of_ocaml build by @JasonGross in #1747
  • Deploy WASM integration to https://mit-plv.github.io/fiat-crypto by @JasonGross in #1749
• Fix DCE/Subst01 to work under lambdas by @JasonGross in #1809
• Make install targets depend on vo files by @JasonGross in #1741
• zig: use "const" for variables that are never mutated by @jedisct1 in #1742
• Adapt to expr.Wf4 by @JasonGross in #1752
• adapt to rocq-prover/rocq#18164 by @Villetaneuse in #1760
• Future-proof CompilersTestCases by @JasonGross in #1762
• Factor ZRange Proper proof by @JasonGross in #1764
• Add some more ZRangeProofs by @JasonGross in #1766
• Update ZRangeProofs by @JasonGross in #1767
• Add support for applying bool functions to zrange by @JasonGross in #1770
• Add Util.Option.bind2 by @JasonGross in #1768
• More fine-grained bounds analysis by @JasonGross in #1769
• Add more identifiers for saturated solinas by @JasonGross in #1773
• Add remaining identifiers for saturated solinas by @JasonGross in #1774
• Add subst! and typeof! to Notations.v by @JasonGross in #1775
• Allow leaving over shelved goals when debugging cache_term by @JasonGross in #1779
• Add prod_rect rewrite rule for saturated arithmetic by @JasonGross in #1780
• Augment rewrite rule proving tactics for saturated arithmetic by @JasonGross in #1783
• Cache intermediate values for Edwards addition by @bMacSwigg in #1808

New Contributors

• @dra27 made their first contribution in #1755

Full Changelog: v0.1.0...v0.1.1

Fiat Cryptography v0.1.0

Compatible with Coq 8.17, 8.18; requires OCaml >= 4.08

We now generate single unified fiat_crypto binaries which can synthesize according to all the various implementation strategies.

What's Changed

• Rust Crate Version Bump by @github-actions in #1731
• Single Binaries by @JasonGross in #1730

Full Changelog: v0.0.26...v0.1.0

Fiat Cryptography v0.0.26

Compatible with Coq 8.17, 8.18; requires OCaml >= 4.08

If the automation was set up right, this release should have attached precompiled binaries.

What's Changed

• Rust Crate Version Bump by @github-actions in #1707
• Drop CI testing of 8.16 by @JasonGross in #1708
• Bump rupicola from 0e001bb to 3691f9a by @dependabot in #1709
• add Alpine CI by @andres-erbsen in #1625
• Adapt to rocq-prover/rocq#18280 (case relevance outside case info) by @SkySkimmer in #1713
• Bump actions/checkout from 3 to 4 by @dependabot in #1714
• POSIX-compliant github-actions-display-per-line-timing.sh by @JasonGross in #1716
• Make etc/ci/describe-system-config.sh POSIX-compliant by @JasonGross in #1715
• Model coq-alpine after coq-debian by @JasonGross in #1712
• Add packaging for standalone files by @JasonGross in #1710
• Allow passing CAMLEXTRAFLAGS for standalone build by @JasonGross in #1717
• remove RupicolaCrypto.Low by @andres-erbsen in #1719
• Only test full amd64 files in Docker CI by @JasonGross in #1722
• Upload standalone binaries to release pages by @JasonGross in #1711
• Statically link alpine binaries: -ccopt -static by @JasonGross in #1718
• Bump rewriter from 5d274d2 to 3e84ec2 by @dependabot in #1728
• [CI] Add names to build jobs by @JasonGross in #1729
• Adapt to rocq-prover/rocq#18273 (Ltac2 supports head reduction) by @SkySkimmer in #1725
• rust: Include documentation comments for type alias. by @armfazh in #1669
• Only upload one copy of linux binaries to releases by @JasonGross in #1721

Full Changelog: v0.0.25...v0.0.26

Fiat Cryptography v0.0.25

Compatible with Coq 8.16, 8.17, 8.18 requires OCaml >= 4.08

Last release compatible with Coq 8.16.

What's Changed

• Optimize & fix Edwards XYZT operations by @bMacSwigg in #1693
• Adapt to rocq-prover/rocq#17576 by @proux01 in #1698
• Bump rupicola from e6daa5e to 0e001bb by @dependabot in #1705
• Bump etc/coq-scripts from 2df5dbe to d3dc888 by @dependabot in #1701
• Bump rewriter from 2f9a755 to 5b13cd7 by @dependabot in #1697
• Bump rewriter from 5b13cd7 to 5e74224 by @dependabot in #1702
• Bump rewriter from 5e74224 to 5d274d2 by @dependabot in #1704

Full Changelog: v0.0.24...v0.0.25

Fiat Crypto Legacy for Coq 8.16, 8.17, 8.18

This is the last version of Fiat Crypto Legacy (the S&P 2019 paper version) compatible with Coq 8.16, 8.17, 8.18. This version supports Coq versions 8.16 -- 8.18.

What's Changed

• [sp2019latest] [CI] Drop Coq < 8.16 by @JasonGross in #1691
• Bump bbv from 6144e21 to f4caa05 by @dependabot in #1690
• [sp2019latest] User docker for master test by @JasonGross in #1696

Full Changelog: SP2019+V8.15...SP2019+V8.16