Fiat Crypto Legacy for Coq 8.15

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

What's Changed

• [sp2019latest] Drop Coq < 8.14 in preparation for bbv bump by @JasonGross in #1540
• Bump bbv from 18c77da to 6144e21 by @dependabot in #1539
• Bump coqprime from 762c7f5 to 203ce86 by @dependabot in #1544
• Bump coqprime from 203ce86 to 0f9f20f by @dependabot in #1547
• Adapt w.r.t. coq/coq#16910. by @ppedrot in #1554
• Bump coqprime from 0f9f20f to 431d7a6 by @dependabot in #1567
• Adapt to coq/coq#16960 (less evar sensitive unification behaviour) by @SkySkimmer in #1574
• Adapt fiat-crypto-legacy to coq/coq#16920 by @olaure01 in #1589
• Adapt w.r.t. coq/coq#17564. by @ppedrot in #1602
• Bump etc/coq-scripts from efae533 to 8ce1d5d by @dependabot in #1614
• Qualifying expr.expr and cie coming from Uncurried and EdDSA.sign from Spec by @herbelin in #1628
• Bump actions/checkout from 3 to 4 by @dependabot in #1650
• Bump coqprime from 431d7a6 to ae85b57 by @dependabot in #1658
• Bump etc/coq-scripts from 8ce1d5d to 8b66ebe by @dependabot in #1660
• Bump coqprime from ae85b57 to f611fa4 by @dependabot in #1664
• Bump etc/coq-scripts from 8b66ebe to 2df5dbe by @dependabot in #1685
• Bump coqprime from f611fa4 to d5935ca by @dependabot in #1688

Full Changelog: SP2019+V8.13...sp2019latest+2023.10

Fiat Cryptography v0.0.22

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

What's Changed

• Rust: Reference newtype operators from core instead of std by @brycx in #1646

Full Changelog: v0.0.21...v0.0.22

Fiat Cryptography v0.0.21

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

Rust crate is now v0.2.*, using newtype structs for typedefs

What's Changed

• Generate p521_32 by @JasonGross in #1594
• Add a constant-time binary extended GCD algorithm. by @jadephilipoom in #1597
• Garagedoor Prettification by @samuelgruetter in #1598
• remove some dead code from garagedoor funcs, tidy by @andres-erbsen in #1619
• Optimize dettman algorithm by @OwenConoly in #1601
• Generalize dettman algorithm by @OwenConoly in #1608
• Prove dedicated doubling for Edwards curves by @andres-erbsen in #1607
• Spec & proof for add_precomputed by @bMacSwigg in #1622
• Use carry_add in AddPrecomputed by @bMacSwigg in #1638
• Pipe through carry_add function by @bMacSwigg in #1635
• Pipe through carry_sub function by @bMacSwigg in #1641
• Debugging
  • Print more casts when stringification fails by @JasonGross in #1634
• C
  • Exclude curve25519_64_msvc.c by @JasonGross in #1593
• Rust
  • Rust: Create newtype structs for typedefs by @divergentdave in #1623
• Zig
  • Minor changes to the build.zig files to prepare for Zig 0.11 by @jedisct1 in #1588
  • Update for Zig 0.11.0 by @jedisct1 in #1611
• MacOS
  • Use 66520 for stack size limit for MacOS compat by @JasonGross in #1586
• Coq Compat

• Adapt w.r.t. coq/coq#17564. by @ppedrot in #1603
• Qualifying M.eq coming from MontgomeryCurve by @herbelin in #1627

New Contributors

• @bMacSwigg made their first contribution in #1622
• @divergentdave made their first contribution in #1623

Full Changelog: v0.0.20...v0.0.21

Fiat Cryptography v0.0.20

For Coq Platform 8.17 beta.

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

What's Changed

• Add the dettman square operation by @OwenConoly in #1576
• bump rupicola with v8.15 support by @andres-erbsen in #1573
• Remove montladder output tests by @andres-erbsen in #1579

Full Changelog: v0.0.19...v0.0.20

Fiat Cryptography v0.0.19

Compatible with Coq 8.15 and 8.16 and probably 8.17, requires OCaml >= 4.08

Breaking changes

• secp256k1_{,scalar_}{32,64} has been renamed to secp256k1_montgomery_{,scalar_}{32,64} and secp256k1_dettman_* has been added

What's Changed

• CLI stuff for dettman multiplication function by @OwenConoly in #1550

Full Changelog: v0.0.18...v0.0.19

Fiat Cryptography v0.0.18

Compatible with Coq 8.15 and 8.16 and probably 8.17, requires OCaml >= 4.08

What's Changed

• Add support for printing to stderr by @JasonGross in #1441
• Add default_assembly_conventions by @JasonGross in #1443
• Be more robust to ulimit failures by @JasonGross in #1445
• Make fancy arguments an implicit typeclass by @JasonGross in #1447
• Factor out some logic from UnsaturatedSolinas.to_bytes_correct by @JasonGross in #1449
• Show more casts in PHOAS printing, sometimes by @JasonGross in #1450
• Reorganize pipeline options to allow for easier additions to them by @JasonGross in #1448
• Try a different order on prove_pipeline_wf by @JasonGross in #1456
• allow input aliasing in compile_binop by @andres-erbsen in #1461
• Add Tuple.{cons,rsnoc} by @JasonGross in #1462
• sprinkle Optimize Proof and Optimize Heap by @andres-erbsen in #1466
• Use return rather than exit in ensure_stack_limit.sh by @JasonGross in #1467
• Add --debug flag and debug info for rewriting by @JasonGross in #1464
• Add Z.divideb and Bool.reflect for Z.divide by @JasonGross in #1473
• Handle r[0~>0] casts on Z.mul_split by @JasonGross in #1474
• Finish broadcast and make progress on chacha20 by @DIJamner in #1482
• add cmovo by @andres-erbsen in #1483
• Add some ZUtil/Land/Fold.v lemmas by @JasonGross in #1487
• Ensure TIMER is defined in config by @JasonGross in #1488
• test-amd64: dependency on binary should not be order-only by @JasonGross in #1489
• Factor out ListUtil commits from Dettman multiplication by @JasonGross in #1490
• Modified assembly equivalence checker to allow parsing asm files containing "or" instructions. by @JasonGross in #1492
• Reuse PHOAS bounds analysis for asm bounds by @JasonGross in #1485
• Saturated Solinas Reduction, rebased and fixed by @andres-erbsen in #1493
• Asm equiv checker: addZ is associative and commutative by @JasonGross in #1494
• Equiv checker: fuse inner add{,Z} into addcarry{,Z} by @JasonGross in #1486
• Use Ltac2 to prove Show instances for enums by @JasonGross in #1497
• Rename Debug options to Flag options by @JasonGross in #1496
• Factor out assembly options a bit more by @JasonGross in #1495
• ASM Equiv: Move bounds definitions up by @JasonGross in #1499
• Enable CLI control of equiv checker rewrite passes with --asm-rewriting-pipeline, --asm-rewriting-passes by @JasonGross in #1498
• Add primed versions of {destruct,inversion}_one_head that don't run simpl by @JasonGross in #1504
• Make the dag available in ASM equiv rewrite passes by @JasonGross in #1505
• ASM Equiv Checker: Include bounds info in dag by @JasonGross in #1503
• Reorganize dag modules to enforce better abstraction by @JasonGross in #1508
• Prove some properties of the bounds in the dag by @JasonGross in #1509
• Adjust a lemma for use in dag bounds by @JasonGross in #1510
• ASM Equivalence Checker: Use bounds from the dag by @JasonGross in #1511
• add classification of Curve25519 points by @andres-erbsen in #1514
• Go back to building src/{,Bedrock/}Everything.vo by @JasonGross in #1515
• Add a performance test for Search for Coq's bench by @JasonGross in #1518
• Use default gcc version by @JasonGross in #1523
• (Almost) finish the chacha20 derivation by @DIJamner in #1533
• Dettman Multiplication Arithmetic by @OwenConoly in #1500
• Chacha20 by @DIJamner in #1548
• Zig inversion code: replace std.meta.bitCount() with @bitSizeOf() by @jedisct1 in #1552
• Montgomery loop by @andres-erbsen in #1562

New Contributors

• @olaure01 made their first contribution in #1529

Full Changelog: v0.0.17...v0.0.18

Fiat Crypto Legacy for Coq 8.13

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

Fiat Cryptography v0.0.17

Compatible with Coq 8.15 and 8.16, requires OCaml >= 4.08

What's Changed

• Update ensure_stack_limit.sh to be POSIX-compliant and not always unconditionally invoke ulimit by @JasonGross in #1438
• Add some rewrite rules about Z bool comparisons by @JasonGross in #1436
• Use Hint Cut rather than Hint Immediate by @JasonGross in #1439

New Contributors

• @github-actions made their first contribution in #1435

Full Changelog: v0.0.16...v0.0.17

Fiat Cryptography v0.0.16

Compatible with Coq 8.15 and 8.16, requires OCaml >= 4.08

What's Changed

• Bump rewriter for more reification performance, including caching reified lemmas via LetIn
  • Bump rewriter to regain Ltac2 reification performance on par with Ltac1 by @JasonGross in #1389
  • More Ltac2 Reification performance experiments by @JasonGross in #1403
  • Bump rewriter: Don't duplicate reification typechecking time in Qed by @JasonGross in #1409
  • More selective correctness proof tactics for PushButtonSynthesis by @JasonGross in #1416
  • Bump rewriter for Cache reified lemmas with LetIn by @JasonGross in #1413
• Automatically increase stack size to avoid stack overflows in OCaml compilation of extracted binaries by @JasonGross in #1430
  • Add stacksize warnings to avoid confusion by @JasonGross in #1407
• Split out makefiles to allow binary testing without Coq files by @JasonGross in #1423
• Performance improvements in GarageDoor
  • use vm_compute instead of Ltac to check instruction bounds by @samuelgruetter in #1429
  • More Blind Optmimizations for GarageDoor by @andres-erbsen in #1431

Full Changelog: v0.0.15...v0.0.16

Fiat Cryptography v0.0.15

The biggest change of this release is Ltac2 reification and (hopefully) compatibility with Coq 8.15 and 8.16 on Windows. Minimum required versions: Coq 8.15, OCaml 4.08

What's Changed

• Port reification to Ltac2 by @JasonGross in #1361
• Garagedoor opens by @andres-erbsen in #1369
• Zig backend: bump the comptime branch quota up for cast() calls by @jedisct1 in #1360
• Use $$ rather than $ for var so as to not conflict with Ltac2 antiquotations by @JasonGross in #1359
• Makefile fixups by @andres-erbsen in #1393

Full Changelog: v0.0.14...v0.0.15