af halo2 Protokollen, H. G. S., & Spitters, B. 2023. High Assurance Specification of the halo2 Protocol.
Added by: Jack (29/07/2023, 03:01) Last edited by: Jack (29/07/2023, 03:03)
|
 |
|
Abstract
|
halo2 is a zk-SNARK building on the original halo. It is novel in that it has several interesting properties; in particular, it is the first system to have recursive proof composition without needing a trusted setup. It has been developed by the Zcash team and the Electric Coin Company for use in the Zcash blockchain, but it is general purpose and can be used in any zero-knowledge application. This paper presents an executable specification of halo2’s proving system, realized using hacspec. hacspec is a specification language for producing executable specifications of cryptographic primitives. As halo2 is one of the more extensive projects to be specified with hacspec , it has also been an exploration of hacspec’s abilities for projects of this size. The tool rustdoc is used to organically present the specification together with its description, as hacpsec is a subset of rust. The labor of this paper also led to contributions to the official halo2 protocol de- scription, a hacspec specification of the Pasta curves, and a hacspec specification of a polynomial ring over the Vesta curve’s base field.
|
[23/655]