Formal Verification of Zero-Knowledge Circuits

• URL: http://arxiv.org/abs/2311.08858v1
• Date: Wed, 15 Nov 2023 10:47:28 GMT
• Title: Formal Verification of Zero-Knowledge Circuits
• Authors: Alessandro Coglio, Eric McCarthy, Eric W. Smith,
• Abstract summary: Zero-knowledge circuits are sets of equality constraints over arithmetic expressions interpreted in a prime field. We make contributions to the problem of ensuring that a circuit correctly encodes a computation.
• Score: 44.99833362998488
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Zero-knowledge circuits are sets of equality constraints over arithmetic expressions interpreted in a prime field; they are used to encode computations in cryptographic zero-knowledge proofs. We make the following contributions to the problem of ensuring that a circuit correctly encodes a computation: a formal framework for circuit correctness; an ACL2 library for prime fields; an ACL2 model of the existing R1CS (Rank-1 Constraint Systems) formalism to represent circuits, along with ACL2 and Axe tools to verify circuits of this form; a novel PFCS (Prime Field Constraint Systems) formalism to represent hierarchically structured circuits, along with an ACL2 model of it and ACL2 tools to verify circuits of this form in a compositional and scalable way; verification of circuits, ranging from simple to complex; and discovery of bugs and optimizations in existing zero-knowledge systems.

Related papers

• Architect of the Bits World: Masked Autoregressive Modeling for Circuit Generation Guided by Truth Table [5.300504429005315]
  We propose a novel approach integrating conditional generative models with differentiable architecture search (DAS) for circuit generation. Our approach first introduces CircuitVQ, a circuit tokenizer trained based on our Circuit AutoEncoder. We then develop CircuitAR, a masked autoregressive model leveraging CircuitVQ as the tokenizer.
  arXiv  Detail & Related papers  (2025-02-18T11:13:03Z)
• Functional Faithfulness in the Wild: Circuit Discovery with Differentiable Computation Graph Pruning [14.639036250438517]
  We introduce a comprehensive reformulation of the task known as Circuit Discovery, along with DiscoGP. DiscoGP is a novel and effective algorithm based on differentiable masking for discovering circuits.
  arXiv  Detail & Related papers  (2024-07-04T09:42:25Z)
• CIRCUITSYNTH: Leveraging Large Language Models for Circuit Topology Synthesis [7.131266114437393]
  We introduce CIRCUITSYNTH, a novel approach that harnesses LLMs to facilitate the automated synthesis of valid circuit topologies. Our approach lays the foundation for future research aimed at enhancing circuit efficiency and specifying output voltage.
  arXiv  Detail & Related papers  (2024-06-06T01:59:59Z)
• AC4: Algebraic Computation Checker for Circuit Constraints in ZKPs [4.810904298160317]
  Underconstrained or overconstrained circuits may lead to bugs. A tool, AC4, is proposed to represent the implementation of the method. Within a solvable range, the checking time has also exhibited noticeable improvement.
  arXiv  Detail & Related papers  (2024-03-23T01:44:57Z)
• Low-overhead non-Clifford fault-tolerant circuits for all non-chiral abelian topological phases [0.7873629568804646]
  We propose a family of explicit geometrically local circuits on a 2-dimensional planar grid of qudits. These circuits are constructed from measuring 1-form symmetries in discrete fixed-point path integrals. We prove fault tolerance under arbitrary local (including non-Pauli) noise for a very general class of topological circuits.
  arXiv  Detail & Related papers  (2024-03-18T18:00:00Z)
• CktGNN: Circuit Graph Neural Network for Electronic Design Automation [67.29634073660239]
  This paper presents a Circuit Graph Neural Network (CktGNN) that simultaneously automates the circuit topology generation and device sizing. We introduce Open Circuit Benchmark (OCB), an open-sourced dataset that contains $10$K distinct operational amplifiers. Our work paves the way toward a learning-based open-sourced design automation for analog circuits.
  arXiv  Detail & Related papers  (2023-08-31T02:20:25Z)
• Adaptive Planning Search Algorithm for Analog Circuit Verification [53.97809573610992]
  We propose a machine learning (ML) approach, which uses less simulations. We show that the proposed approach is able to provide OCCs closer to the specifications for all circuits.
  arXiv  Detail & Related papers  (2023-06-23T12:57:46Z)
• A Complete Equational Theory for Quantum Circuits [58.720142291102135]
  We introduce the first complete equational theory for quantum circuits. Two circuits represent the same unitary map if and only if they can be transformed one into the other using the equations.
  arXiv  Detail & Related papers  (2022-06-21T17:56:31Z)
• Machine Learning Optimization of Quantum Circuit Layouts [63.55764634492974]
  We introduce a quantum circuit mapping, QXX, and its machine learning version, QXX-MLP. The latter infers automatically the optimal QXX parameter values such that the layed out circuit has a reduced depth. We present empiric evidence for the feasibility of learning the layout method using approximation.
  arXiv  Detail & Related papers  (2020-07-29T05:26:19Z)
• Hardware-Encoding Grid States in a Non-Reciprocal Superconducting Circuit [62.997667081978825]
  We present a circuit design composed of a non-reciprocal device and Josephson junctions whose ground space is doubly degenerate and the ground states are approximate codewords of the Gottesman-Kitaev-Preskill (GKP) code. We find that the circuit is naturally protected against the common noise channels in superconducting circuits, such as charge and flux noise, implying that it can be used for passive quantum error correction.
  arXiv  Detail & Related papers  (2020-02-18T16:45:09Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.