• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
        • Jubjub
        • Verify-zcash-r1cs
        • Lift-zcash-r1cs
        • Pedersen-hash
        • Zcash-gadgets
        • Bit/byte/integer-conversions
        • Constants
        • Blake2-hash
          • Blake2s-256
        • Randomness-beacon
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Zcash

Blake2-hash

The BLAKE2 hash functions used by Zcash.

The definition of BLAKE2 is more general than Zcash. BLAKE2 is defined elsewhere, and used by Zcash. In the ACL2 community books, this is defined under kestrel/crypto/blake/.

Subtopics

Blake2s-256

The function \mathsf{BLAKE2s}\textsf{-}\mathsf{256} [ZPS:5.4.1.2].