mit-plv/fiat-crypto v0.0.18

Fiat Cryptography v0.0.18

on GitHub

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