Release Fiat Cryptography v0.1.1 · mit-plv/fiat-crypto

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

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