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.

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 by @ppedrot in #1919
• Refined/Signed Barrett Reduction by @atrieu in #2013

Code Generation and Cryptography

• Rust Crate Version Bump by @github-actions in #1907
• Generate code for SM2 by @emmansun in #1940
• Update Curves/Weierstrass by @andres-erbsen in #1953
• Bedrock2 End2End field and co-Z operations for secp256k1 by @andres-erbsen in #1954
• feat: make rust const by @Daniel-Aaron-Bloom in #2080

Assembly and Parsing

• Add some example asm files by @JasonGross in #2021
• Add some assembly example tests by @JasonGross in #2024
• Add support for parsing more assembly by @JasonGross in #2027
• Parse various directives starting with . in intel syntax by @JasonGross in #2030
• Parse label-based addressing by @JasonGross in #2028
• Handle rip-relative addressing by @JasonGross in #2029
• Allow fuzzy matching of assembly labels by @JasonGross in #2032
• Add support for nop by @JasonGross in #2034
• Add support for shld by @JasonGross in #2037
• Add support for movabs,movdqa,movdqu,movq,movd,movups by @JasonGross in #2035
• Add more directives by @JasonGross in #2047
• Add .ascii, .asciz by @JasonGross in #2049
• Strip trailing newlines from asm by @JasonGross in #2051
• Actually test more asm functions by @JasonGross in #2044
• Add from_bytes asm tests by @JasonGross in #2043
• Revert "Add from_bytes asm tests" by @JasonGross in #2045
• Add --debug-asm-symex-first by @JasonGross in #2036
• Fix the help of --asm-rewriting-pipeline by @JasonGross in #2053
• Add --asm-node-reveal-depth by @JasonGross in #2055
• Print the node values of registers by @JasonGross in #2056
• Add opcode_size for nop so we don't get errors by @JasonGross in #2060

Coq and Formal Verification

• Adapt w.r.t. rocq-prover/rocq#19228 by @ppedrot in #1934
• Adapt to rocq-prover/rocq#19530 by @proux01 in #1957
• Adapt to rocq-prover/rocq#19530 by @proux01 in #1992
• Require Import BinNat before using it in ParseArithmetic.v (for rocq-prover/rocq#19801) by @andres-erbsen in #1980
• Adapt to rocq-prover/rocq#19690 (Hint Extern follows proof mode) by @SkySkimmer in #2058
• Use Listable to prove equality of registers and opcodes by @JasonGross in #2020
• Add proof that map is injective by @JasonGross in #2061
• remove PermutationCompat by @andres-erbsen in #2091

HTML and Documentation

• [HTML] Add support for input and output files by @JasonGross in #2014
• Update HTML to support more files by @JasonGross in #2015
• Fix filling of files from url by @JasonGross in #2054
• Add CI shield for opam package to README by @JasonGross in #1972

Miscellaneous

• switch GarageDoor to LeakageSemantics by @OwenConoly in #2009
• Add is_substring by @JasonGross in #2018
• Add some reduction notations by @JasonGross in #2017
• Don't parse 'ah' as a hex number by @JasonGross in #2019
• Move signed to Z.signed in ZUtil.Definitions by @JasonGross in #2039
• Add ZRange.bitwidth, ZRange.of_bitwidth by @JasonGross in #2041
• Add more string notations for some constants by @JasonGross in #2048
• Move a lemma to util by @JasonGross in #2052
• Better ordering on print-report by @JasonGross in #2062
• Enable +fragile-hint-constr by @JasonGross in #2069
• Enable +fragile-hint-constr (take 2) by @JasonGross in #2075
• Readdition in bedrock2 by @miriampolzer in #2068

New Contributors

• @emmansun made their first contribution in #1940
• @miriampolzer made their first contribution in #2068
• @Daniel-Aaron-Bloom made their first contribution in #2079

Full Changelog: v0.1.4...v0.1.5

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

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

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

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

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