zkStruDul: Programming zkSNARKs with Structural Duality

TL;DR

zkStruDul presents a compute-and-prove calculus that unifies input construction and predicate definition for zkSNARK systems, addressing the duplication and mismatch risks in conventional toolchains. By introducing a type-directed, label-based framework and a projection-based compiler, the approach extracts separate compute and prove procedures while enabling recursive proofs and layering on existing backends such as Circom or gnark. The authors formalize both an in-order source semantics and a projection semantics, prove their adequacy via a concurrent target semantics, and establish Robust Relational Hyperproperty Preservation for the compilation. Collectively, this yields a cleaner, more maintainable approach to building NIZK-based applications (e.g., Merkle proofs and zkVMs) with strong semantic guarantees and interoperability with existing cryptographic tooling.

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.

Figures (11)

• Figure 1: A Merkle tree with that path to data $d$ in yellow and the siblings highlighted in blue.
• Figure 2: Combined code to compute a Merkle sibling path and verify that two root hashes correspond to the same tree except for a change at the leaf at .
• Figure 3: Verifying correct interpretation by recursively verifying previous steps and then one more.
• Figure 4: $\textrm{FJ}_\textsc{nizk}$ Syntax, where $\ell \in \{\texttt{\color{cpcolor}C}\xspace, \texttt{\color{cpcolor}P}\xspace, \texttt{\color{cpcolor}CP}\xspace\}$ is a procedure label.
• Figure 5: Semantic Rules for NIZK Proof Terms

Theorems & Definitions (80)

• theorem 1: Type Soundness of
• theorem 2: Type Soundness Inside Combined Blocks
• definition 1: Adequacy
• theorem 3: Completeness of Concurrent Semantics
• theorem 4: Soundness of Concurrent Semantics
• theorem 5: Adequacy of $\fullComp{\cdot}$
• definition 2: Typed RrHP
• theorem 6: Robust Relational Hyperproperty Preservation
• lemma 1: Cnp Always in Head
• lemma 2: Simultaneous Substitution Preserves $\textrm{FJ}_\textsc{nizk}$ Typing