mit-plv/fiat-crypto v0.1.5

Fiat Cryptography v0.1.5

on GitHub

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