v0.3.1

What's Changed

• Lift requirement that choice_types have to be inhabited by @MarkusKL in #98
• add chTuple to choice_type and otf_injective by @ErVinuelas in #103
• Add dune setup by @4ever2 in #107
• Corrected error in DL assumption by @ErVinuelas in #104
• Adapt to math-comp/math-comp#1545 by @proux01 in #108
• Hybrid Arguments by @MarkusKL in #101
• Update mathcomp-word to 3.3 by @vbgl in #109

New Contributors

• @proux01 made their first contribution in #108
• @vbgl made their first contribution in #109

Full Changelog: v0.3.0...v0.3.1

v0.3.0

What's Changed

• Adapt to MC#1354 by @4ever2 in #68
• Port SigmaProtocol changes from jasmin branch by @4ever2 in #73
• Add documentation, clarification and optimization of the joy of state separating proofs by @ErVinuelas in #57
• Towards nominals by @4ever2 in #70
• Added some examples missed in the README by @ErVinuelas in #78
• Adapt to MC#1439 by @Tragicus in #86
• Add new assumptions and move the DDH by @ErVinuelas in #81
• Add nominal features by @MarkusKL in #82
• Reversible coercion from choice_type by @MarkusKL in #77
• Adapt to MC#1439 by @Tragicus in #88
• Drop support for Coq 8.18 by @4ever2 in #84
• More invariants by @MarkusKL in #90
• Drop support for Coq 8.19 by @4ever2 in #85
• Update to use the new chList by @ErVinuelas in #93
• Adapt to math-comp/math-comp#1433 by @pi8027 in #96
• Support Rocq 9.1 by @4ever2 in #91
• Simpler nominal semantics proof by @MarkusKL in #97

New Contributors

• @ErVinuelas made their first contribution in #57
• @pi8027 made their first contribution in #96

Full Changelog: v0.2.4...v0.3.0

v0.2.4

What's Changed

• Adapt to MC#1300 by @4ever2 in #56
• Adapt to MC#1256 by @Tragicus in #58
• Adapt to MC#1256 by @Tragicus in #62
• Build with Coq 9.0 in CI by @4ever2 in #59
• Add chInt, chWord, chList, and chSum choice_types by @4ever2 in #60
• Compatible with math-comp 2.4.0

New Contributors

• @Tragicus made their first contribution in #58

Full Changelog: v0.2.3...v0.2.4

v0.2.3

What's Changed

• Compatibility with mathcomp 2.3.0 by @4ever2 in #49

Full Changelog: v0.2.2...v0.2.3

v0.2.2

What's Changed

• Compatibility with mathcom-analysis 1.7.0 by @4ever2 in #47
• Nix flake suppport and CI by @sertel in #43
• Coq 8.20 compatibility by @4ever2 in #48

Full Changelog: v0.2.1...v0.2.2

v0.2.1

What's Changed

• Add SSProve prefix to logpaths by @4ever2 in #41
• Simplify logpaths by @4ever2 in #42

Full Changelog: v0.2.0...v0.2.1

v0.2.0

What's Changed

• Mathcomp 2.1.0 support by @sertel in #40

New Contributors

• @sertel made their first contribution in #40

Full Changelog: v0.1.0...v0.2.0

v0.1.0

What's Changed

• OVN fixes by @4ever2 in #34

Full Changelog: journal-version...v0.1.0

Companion to journal version "SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq"

Merge pull request #37 from 4ever2/update-deps

Support Coq 8.16 and 8.17

Companion to journal submission "SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq"

journal-submission

Fix KEM-DEM definition of CCA