Halo2 constraints and verifier graphs #1448

New issue

Open

opened 2026-10-16 21:05:31 +00:00 by bsakaguchi · 0 comments

bsakaguchi commented

2026-10-16 21:05:31 +00:00

Owner

Originally created by @matbrgz on GitHub (Oct 14, 2026).
Original GitHub issue: https://github.com/morluto/rea/issues/3740

Problem Statement & Context

Zero-Knowledge Proofs (ZKPs) are the mathematical backbone of privacy protocols, validity rollups (zk-Rollups), and verifiable computation. ZK programs are authored in domain-specific languages (Circom, Noir, Leo) and compiled into mathematical constraint systems:

Rank-1 Constraint Systems (R1CS): Binary representation of arithmetic circuits composed of constraints of the form \langle A, s \rangle \cdot \langle B, s \rangle - \langle C, s \rangle = 0, where s is the witness vector. Stored in binary .r1cs containers (magic r1cs, version, field size, variable counts, linear combination matrices).
PLONKish & Custom Gates (Halo2 / UltraPLONK): Constraint tables structured as columns (Advice, Fixed, Instance), selector polynomials, permutation arguments (copy constraints), and custom non-linear lookup gates (Plookup).
Witness & Proving Artifacts (.wtns, .zkey): Binary witness vectors assigning concrete values to circuit variables, and proving keys packing evaluation domain polynomials, G1/G2 elliptic curve points (BN254 / BLS12-381), and lagrange bases.
On-Chain Verifier Contracts: Solidity smart contracts verifying Groth16 or PLONK proofs using EVM pairing precompiles (ecPairing at 0x08, ecAdd at 0x06, ecMul at 0x07).

Currently, reverse engineering a ZK artifact is nearly impossible without specialized cryptographic tools. REA needs a dedicated ZK circuit engine capable of parsing .r1cs files, analyzing constraint graphs, extracting public/private input relationships, and correlating circuit artifacts with on-chain EVM verifier contracts.

Proposed Architecture

flowchart TD
    A["ZK Circuit File (.r1cs, .zkey, .wtns) / Verifier Contract (Solidity)"] --> B["Zero-Knowledge Semantic Engine"]
    B --> C["R1CS & PLONKish Constraint Deserializer"]
    B --> D["Circuit Signal & Witness Graph Reconstructor"]
    B --> E["On-Chain Verifier Correlator (EVM Precompiles)"]
    
    C --> C1[".r1cs Binary Header (Field Prime, Variables, Constraints)"]
    C --> C2["Matrix Slicing (A, B, C Linear Combinations)"]
    
    D --> D1["Signal Classification (Public Inputs, Private Inputs, Outputs)"]
    D --> D2["Under-Constrained Signal & Witness Bug Detection"]
    
    E --> E1["EVM Verifier Verification Key (VK Alpha, Beta, Gamma, Delta)"]
    E --> E2["ecPairing Precompile Call Mapping"]
    
    C & D & E --> F["Synthesized Circuit Constraint Graph & Verifier Specification"]

Technical Capabilities & Modules

Binary R1CS Constraint Parsing (.r1cs):
- Parse R1CS binary container: magic header (0x73633172), version, section offsets.
- Decode prime field modulus (e.g. BN254 scalar field r = 21888242871839275222246405745257275088548364400416034343698204186575808495617).
- Extract variable counts: total variables, public inputs, public outputs, private inputs, number of constraints.
- Decompress and parse sparse matrices A, B, C.
Signal Hierarchy & Constraint Graph Reconstruction:
- Map symbolic variable names using symbol files (.sym).
- Categorize signals: public inputs, private inputs (secrets), intermediate witness variables, and outputs.
- Construct a directed constraint graph: trace data dependencies from inputs through intermediate constraints to final public assertions.
Circuit Audit & Under-Constrained Signal Analysis:
- Detect under-constrained signals: identify private or intermediate variables that appear in linear combinations but lack quadratic locking constraints (a common source of critical ZK vulnerabilities).
- Detect unused or dead signals that do not influence public outputs.
Proving Key (.zkey) & Witness (.wtns) Deserialization:
- Parse .zkey files: extract verification key parameters, toxic waste powers of tau commitments, and Groth16 evaluation points.
- Parse binary .wtns witness files and verify satisfiability against candidate R1CS constraints.
On-Chain Verifier Contract Correlation:
- Disassemble EVM verifier contracts (e.g. Tornado Cash, Semaphore, zkSync verifiers).
- Extract verification key constants hardcoded in bytecode: IC vectors, ^Glpha_1, eta_2, \gamma_2, \delta_2.
- Match on-chain verifying keys with static .zkey circuit artifacts to prove provenance.

Acceptance Criteria

Automated parsing of binary .r1cs constraint files across standard prime fields.
Structural mapping of public, private, and intermediate signals.
Detection of under-constrained and unconstrained signals.
Extraction of verification key parameters from on-chain Solidity verifier bytecodes.
Generation of an interactive circuit dependency graph detailing constraint flows.

Complements #972 (Solidity/EVM reverse engineering)
Complements #3621 (Unknown binary file-format inference)

Originally created by @matbrgz on GitHub (Oct 14, 2026). Original GitHub issue: https://github.com/morluto/rea/issues/3740 [![Type: Feature](https://img.shields.io/badge/type-feature-blue.svg?style=flat-square)](https://github.com/morluto/rea) [![Domain: Blockchain RE](https://img.shields.io/badge/domain-blockchain_RE-orange.svg?style=flat-square)](https://github.com/morluto/rea) [![Status: Proposed](https://img.shields.io/badge/status-proposed-blue.svg?style=flat-square)](https://github.com/morluto/rea) [![Ecosystem: REA](https://img.shields.io/badge/ecosystem-morluto%2Frea-8A2BE2.svg?style=flat-square)](https://github.com/morluto/rea) ### Problem Statement & Context Zero-Knowledge Proofs (ZKPs) are the mathematical backbone of privacy protocols, validity rollups (zk-Rollups), and verifiable computation. ZK programs are authored in domain-specific languages (Circom, Noir, Leo) and compiled into mathematical constraint systems: 1. **Rank-1 Constraint Systems (R1CS)**: Binary representation of arithmetic circuits composed of constraints of the form $\langle A, s \rangle \cdot \langle B, s \rangle - \langle C, s \rangle = 0$, where $s$ is the witness vector. Stored in binary `.r1cs` containers (magic `r1cs`, version, field size, variable counts, linear combination matrices). 2. **PLONKish & Custom Gates (Halo2 / UltraPLONK)**: Constraint tables structured as columns (Advice, Fixed, Instance), selector polynomials, permutation arguments (copy constraints), and custom non-linear lookup gates (Plookup). 3. **Witness & Proving Artifacts (`.wtns`, `.zkey`)**: Binary witness vectors assigning concrete values to circuit variables, and proving keys packing evaluation domain polynomials, G1/G2 elliptic curve points (BN254 / BLS12-381), and lagrange bases. 4. **On-Chain Verifier Contracts**: Solidity smart contracts verifying Groth16 or PLONK proofs using EVM pairing precompiles (`ecPairing` at `0x08`, `ecAdd` at `0x06`, `ecMul` at `0x07`). Currently, reverse engineering a ZK artifact is nearly impossible without specialized cryptographic tools. REA needs a dedicated ZK circuit engine capable of parsing `.r1cs` files, analyzing constraint graphs, extracting public/private input relationships, and correlating circuit artifacts with on-chain EVM verifier contracts. ### Proposed Architecture ```mermaid flowchart TD A["ZK Circuit File (.r1cs, .zkey, .wtns) / Verifier Contract (Solidity)"] --> B["Zero-Knowledge Semantic Engine"] B --> C["R1CS & PLONKish Constraint Deserializer"] B --> D["Circuit Signal & Witness Graph Reconstructor"] B --> E["On-Chain Verifier Correlator (EVM Precompiles)"] C --> C1[".r1cs Binary Header (Field Prime, Variables, Constraints)"] C --> C2["Matrix Slicing (A, B, C Linear Combinations)"] D --> D1["Signal Classification (Public Inputs, Private Inputs, Outputs)"] D --> D2["Under-Constrained Signal & Witness Bug Detection"] E --> E1["EVM Verifier Verification Key (VK Alpha, Beta, Gamma, Delta)"] E --> E2["ecPairing Precompile Call Mapping"] C & D & E --> F["Synthesized Circuit Constraint Graph & Verifier Specification"] ``` ### Technical Capabilities & Modules 1. **Binary R1CS Constraint Parsing (`.r1cs`):** - Parse R1CS binary container: magic header (`0x73633172`), version, section offsets. - Decode prime field modulus (e.g. BN254 scalar field $r = 21888242871839275222246405745257275088548364400416034343698204186575808495617$). - Extract variable counts: total variables, public inputs, public outputs, private inputs, number of constraints. - Decompress and parse sparse matrices $A$, $B$, $C$. 2. **Signal Hierarchy & Constraint Graph Reconstruction:** - Map symbolic variable names using symbol files (`.sym`). - Categorize signals: public inputs, private inputs (secrets), intermediate witness variables, and outputs. - Construct a directed constraint graph: trace data dependencies from inputs through intermediate constraints to final public assertions. 3. **Circuit Audit & Under-Constrained Signal Analysis:** - Detect under-constrained signals: identify private or intermediate variables that appear in linear combinations but lack quadratic locking constraints (a common source of critical ZK vulnerabilities). - Detect unused or dead signals that do not influence public outputs. 4. **Proving Key (`.zkey`) & Witness (`.wtns`) Deserialization:** - Parse `.zkey` files: extract verification key parameters, toxic waste powers of tau commitments, and Groth16 evaluation points. - Parse binary `.wtns` witness files and verify satisfiability against candidate R1CS constraints. 5. **On-Chain Verifier Contract Correlation:** - Disassemble EVM verifier contracts (e.g. Tornado Cash, Semaphore, zkSync verifiers). - Extract verification key constants hardcoded in bytecode: $IC$ vectors, $^Glpha_1$, $eta_2$, $\gamma_2$, $\delta_2$. - Match on-chain verifying keys with static `.zkey` circuit artifacts to prove provenance. ### Acceptance Criteria - [ ] Automated parsing of binary `.r1cs` constraint files across standard prime fields. - [ ] Structural mapping of public, private, and intermediate signals. - [ ] Detection of under-constrained and unconstrained signals. - [ ] Extraction of verification key parameters from on-chain Solidity verifier bytecodes. - [ ] Generation of an interactive circuit dependency graph detailing constraint flows. ### Related Issues & Dependencies - Complements #972 (Solidity/EVM reverse engineering) - Complements #3621 (Unknown binary file-format inference)

bsakaguchi referenced this issue

2026-10-17 21:01:32 +00:00

[GH-ISSUE #2383] [Tracker] Audit analysis and debugging coverage for the TIOBE top 100 languages (October 2026) #794

bsakaguchi referenced this issue

2026-10-17 21:11:30 +00:00

[PR #1448] [MERGED] test(javascript): reuse comparison node fixtures #2894