A library for Zcash.

Zcash is a blockchain currency that provides confidentiality via zero-knowledge proofs.

This library provides an ACL2 formalization of some aspects of Zcash. The formalization is based on the Zcash Protocol Specification (Version 2021.1.15 [NU5 proposal] of 2021-09-01, as of this writing), referenced as `[ZPS]' in the documentation of this library. Sections, appendices, theorems, etc. are referenced by appending their designations separated by colo, e.g. `[ZPS:4.1.1]' references Section 4.1.1, `[ZPS:A.2]' references Appendix A.2, and `[ZPS:T.A.2.1]' references Theorem A.2.1 (that is, we use `T' to refer to theorems, including lemmas). These square-bracketed references may be used as nouns or parenthentically.

- Jubjub
- The Jubjub complete twisted Edwards elliptic curve [ZPS:5.4.9.3].
- Verify-zcash-r1cs
- A tool to verify a zcash R1CS
- Lift-zcash-r1cs
- A tool to lift a zcash R1CS
- Pedersen-hash
- A formalization of Zcash's Pedersen hash.
- Zcash-gadgets
- A collection of Zcash gadgets, with formal specifications and proofs.
- Bit/byte/integer-conversions
- Conversions between bit sequences, byte sequenes, and integers.
- Constants
- Constants used in Zcash.
- Blake2-hash
- The BLAKE2 hash functions used by Zcash.
- Randomness-beacon
- Randomness beacon in Zcash.