zkStruDul: Programming zkSNARKs with Structural Duality

TL;DR

zkStruDul introduces a unified language for zkSNARKs that combines input transformations and predicate definitions, reducing errors and simplifying development of zero-knowledge proofs with features like recursion.

Contribution

It presents a novel language that unifies predicate and input transformation definitions for zkSNARKs, ensuring correctness and reducing duplicated logic.

Findings

Eliminates mismatches between predicate and input transformations.

Supports recursive proofs in a high-level abstraction.

Proves semantic equivalence between source and projected semantics.

Abstract

Non-Interactive Zero Knowledge (NIZK) proofs, such as zkSNARKS, let one prove knowledge of private data without revealing it or interacting with a verifier. While existing tooling focuses on specifying the predicate to be proven, real-world applications optimize predicate definitions to minimize proof generation overhead, but must correspondingly transform predicate inputs. Implementing these two steps separately duplicates logic that must precisely match to avoid catastrophic security flaws. We address this shortcoming with zkStruDul, a language that unifies input transformations and predicate definitions into a single combined abstraction from which a compiler can project both procedures, eliminating duplicate code and problematic mismatches. zkStruDul provides a high-level abstraction to layer on top of existing NIZK technology and supports important features like recursive proofs. We provide a source-level semantics and prove its behavior is identical to the projected semantics, allowing straightforward standard reasoning.