|
|
|---|
|
|
|
|---|
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.