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. 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

Fiat Cryptography v0.1.2

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

What's Changed

• Adapt to coq/coq#18590 by @proux01 in #1821
• adapt to coq/coq#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 coq/coq#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 coq/coq#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 coq/coq#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 coq/coq#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

Fiat Cryptography v0.0.24

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

Fix publish.yml CI action, no other changes since v0.0.23

Full Changelog: v0.0.23...v0.0.24

Fiat Cryptography v0.0.23

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

What's Changed

• Edwards point doubling for X25519 by @bMacSwigg in #1642
• Rust: Add no_std CI by @pinkforest in #1648
• rust: use doc comments by @armfazh in #1668
• rust: Replaces return an empty tuple by nothing (void). by @armfazh in #1670
• Drop use of Pervasives by @JasonGross in #1676
• Stop relying on replace by automatic assumption-based solving by @SkySkimmer in #1657

New Contributors

• @pinkforest made their first contribution in #1648
• @armfazh made their first contribution in #1668

Full Changelog: v0.0.22...v0.0.23