|
|
|---|
|
|
|
|---|
Ethereum's Semaphore.
Semaphore is a zero-knowledge gadget for Ethereum, but it may have wider applicability. See the Ethereum Semaphore repository for more information.
This library provides an ACL2 formalization of the Semaphore functionality, and formal proofs that the R1CS used to implement Semaphore are equivalent to the formalization. The formalization is primarily based on the specification in the paper Community Proposal: Semaphore: Zero-Knowledge Signaling on Ethereum, referenced here as `[Sema-Spec]' for brevity. Sections are referenced by appending their designations separated by a colon, e.g., `[Sema-Spec:5.3.2]' references Section 5.3.2.