Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge

John Kolesar, Shan Ali, Timos Antonopoulos, Ruzica Piskac

TL;DR

This work introduces Crepe, the first zero-knowledge protocol for proving equivalence between regular expressions, a PSPACE-complete problem. It builds a dedicated calculus based on derivatives and coinduction, with a sound and complete proof-generation algorithm that yields verifiable proofs without revealing the underlying expressions. The protocol employs a commit-and-prove ZK backend, three read-only AST tables, and a multiplexed set of checking instructions to balance security and efficiency. Empirical evaluation on hundreds of proofs shows Crepe validates most proofs within seconds, outperforming some baselines while highlighting the trade-offs between information leakage and performance. The results demonstrate a practical pathway for privacy-preserving reasoning about regular expressions with broad implications for compiler validation, DoS-resistance, and private code verification.

Abstract

Zero-knowledge (ZK) protocols enable software developers to provide proofs of their programs' correctness to other parties without revealing the programs themselves. Regular expressions are pervasive in real-world software, and zero-knowledge protocols have been developed in the past for the problem of checking whether an individual string appears in the language of a regular expression, but no existing protocol addresses the more complex PSPACE-complete problem of proving that two regular expressions are equivalent. We introduce Crepe, the first ZK protocol for encoding regular expression equivalence proofs and also the first ZK protocol to target a PSPACE-complete problem. Crepe uses a custom calculus of proof rules based on regular expression derivatives and coinduction, and we introduce a sound and complete algorithm for generating proofs in our format. We test Crepe on a suite of hundreds of regular expression equivalence proofs. Crepe can validate large proofs in only a few seconds each.

Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge

TL;DR

This work introduces Crepe, the first zero-knowledge protocol for proving equivalence between regular expressions, a PSPACE-complete problem. It builds a dedicated calculus based on derivatives and coinduction, with a sound and complete proof-generation algorithm that yields verifiable proofs without revealing the underlying expressions. The protocol employs a commit-and-prove ZK backend, three read-only AST tables, and a multiplexed set of checking instructions to balance security and efficiency. Empirical evaluation on hundreds of proofs shows Crepe validates most proofs within seconds, outperforming some baselines while highlighting the trade-offs between information leakage and performance. The results demonstrate a practical pathway for privacy-preserving reasoning about regular expressions with broad implications for compiler validation, DoS-resistance, and private code verification.

Abstract

Zero-knowledge (ZK) protocols enable software developers to provide proofs of their programs' correctness to other parties without revealing the programs themselves. Regular expressions are pervasive in real-world software, and zero-knowledge protocols have been developed in the past for the problem of checking whether an individual string appears in the language of a regular expression, but no existing protocol addresses the more complex PSPACE-complete problem of proving that two regular expressions are equivalent. We introduce Crepe, the first ZK protocol for encoding regular expression equivalence proofs and also the first ZK protocol to target a PSPACE-complete problem. Crepe uses a custom calculus of proof rules based on regular expression derivatives and coinduction, and we introduce a sound and complete algorithm for generating proofs in our format. We test Crepe on a suite of hundreds of regular expression equivalence proofs. Crepe can validate large proofs in only a few seconds each.

Paper Structure

This paper contains 63 sections, 3 theorems, 1 equation, 5 figures, 10 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Motivating Example
  3. Preliminaries
  4. Grammar
  5. Epsilon
  6. Derivatives
  7. Regular Expression Equivalence
  8. Custom Proof Format
  9. Coinduction
  10. Zero-Knowledge Proofs
  11. Protocol Design
  12. Proof Structure
  13. Checking Instructions
  14. Size Parameters
  15. Execution
  16. ...and 48 more sections

Key Result

Theorem 1

Any term $r$ can be converted into an equivalent regular expression using our normalization, equality, epsilon, and derivative rules. In particular, if $r$ is $E(r')$, then $r$ can be converted into either $\emptyset$ or $\epsilon$, but not both.

Figures (5)

  • Figure 1: State machines for motivating example
  • Figure 1: A proof of the equivalence of $(a^*a)^*$ and $a^*$ in $\texttt{Cr\^epe}$'s format. Some steps are omitted or simplified. We use $\#$ to denote the addresses of proof steps.
  • Figure 2: Equivalence checking time relative to the combined size of the regular expressions being compared, plotted on a logarithmic scale.
  • Figure 3: Proof generation time relative to the combined size of the regular expressions being compared, plotted on a logarithmic scale.
  • Figure 4: Proof validation times for all configurations of $\texttt{Cr\^epe}$ relative to proof step count.

Theorems & Definitions (3)

  • Theorem 1: Term Conversion
  • Theorem 2: Normal Form Conversion
  • Theorem 3: Uniqueness of Normal Form