v1.5.0

What's Changed

• upgrade Lean version by @kustosz in #25
• Support gnark 12 by @kustosz in #26

Full Changelog: v1.4.0...v1.5.0

v1.4.0

What's Changed

• chore: mathlib update to v4.2.0 in #20
• feat: updated gates in #24

v1.3.0

Reworked merkle tree and bit decompositions.

v1.2.1

What's Changed

• chore: refactoring Hash.lean

v1.2.0

What's Changed

• chore: Updated mathlib4 to commit 26d0eab43f05db777d1cf31abd31d3a57954b2a9

Binary.lean

• feat: Added dropLast lemmas for Vector Bit n
• feat: Added lemmas for conversion between Vector ZMod n and Vector Bit n

Basic.lean

• feat: Added lemmas for dropLast

Merkle.lean

• feat: Added dropLast lemmas for Vector Dir n
• feat: Added lemmas for conversion between Vector ZMod n and Vector Dir n
• feat: Added lemmas for conversion between Vector Bit n and Vector Dir n
• feat: Added item_at and proof functions for MerkleTree using Fin d in place of Vector Dir d
• feat: Added new MerkleTree theorems

v1.1.0

What's Changed

• chore: Importing single mathlib modules instead of full library in #17
• feat: new theorems in #18
  • Refactored Binary.lean and removed unused theorems
  • Added convertion from Nat to Vector Dir using Dir.nat_to_dir_vec
  • Expanded MerkleTree functions to take Nat in place of Vector Dir
  • Expanded MerkleTree theorems
  • Expanded Vector theorems
  • Added semantic equivalence for Gates.select and Gates.or

v1.0.0

What's Changed

• feat: add utils for loops in #4
• feat: more utils for hashes & aux types in #5
• feat: remove the getElem override in #7
• feat: add more helpers for vectors and binary reps in #8
• feat: added readme in #9
• chore: refactoring theorems in #12