Zcash-gadgets
A collection of Zcash gadgets, with formal specifications and proofs.
The .txt files in this directory contain
ACL2 representations of R1CS and tree gadgets,
generated via the bellman and librustzcash Rust libraries.
The R1CS and tree gadgets are functionally equivalent,
but the tree gadgets have more structure than the R1CS gadgets;
the additional structure has been derived
by modifying the Rust code that generates the gadgets
to output some additional information.
The .lisp files in this directory contain
ACL2 specifications and proofs of the gadgets.
The specifications are generally thin wrappers of
existing specifications in the Zcash formalization one directory up,
or in the elliptic curve library.
