|
| 1 | +# GKR Protocol |
| 2 | + |
| 3 | +An implementation of the Goldwasser-Kalai-Rothblum (GKR) Non-Interactive Protocol for proving correct evaluation of arithmetic circuits. |
| 4 | + |
| 5 | +To help with the understanding of this implementation, we recommend reading our [blog post](https://blog.lambdaclass.com/gkr-protocol-a-step-by-step-example/). |
| 6 | + |
| 7 | +**Warning:** This GKR implementation is for educational purposes and should not be used in production. It uses the Fiat-Shamir transform, which is vulnerable to practical attacks in this context (see ["How to Prove False Statements"](https://eprint.iacr.org/2025/118.pdf)). |
| 8 | + |
| 9 | +## Overview |
| 10 | + |
| 11 | +The GKR Protocol allows a Prover to convince a Verifier that he correctly evaluated an arithmetic circuit on a given input without the Verifier having to perform the entire computation. |
| 12 | + |
| 13 | +It is a fundamental building block for many interactive proof systems and argument systems, providing a way to verify computations in time roughly proportional to the circuit's depth rather than its size. |
| 14 | + |
| 15 | +The protocol works by reducing claims about each layer of the circuit to claims about the next layer, using the Sumcheck Protocol as a subroutine. This process continues until reaching the input layer, where the verifier can directly check the final claim. The key insight is that the wiring of the circuit can be expressed as multilinear polynomials, allowing the use of sumcheck for efficient verification. |
| 16 | + |
| 17 | +### Key Features |
| 18 | + |
| 19 | +- **Layered Circuit Support**: Works with circuits organized in layers where each gate takes inputs from the previous layer. |
| 20 | +- **Power-of-Two Constraint**: Each layer must have a power-of-two number of gates for protocol compatibility. |
| 21 | +- **Addition and Multiplication Gates**: Supports both addition and multiplication operations. |
| 22 | +- **Complete Verification**: Includes input verification to ensure end-to-end correctness. |
| 23 | + |
| 24 | +## Circuit Structure |
| 25 | + |
| 26 | +Circuits are organized in layers, with each layer containing gates that operate on outputs from the previous layer: |
| 27 | + |
| 28 | +``` |
| 29 | +Output: o o <- circuit.layers[0] |
| 30 | + / \ / \ |
| 31 | + o o o o <- circuit.layers[1] |
| 32 | + ... |
| 33 | + o o o o <- circuit.layers[layer.len() - 1] |
| 34 | + / \ / \ / \ / \ |
| 35 | +Input: o o o o o o o o |
| 36 | +``` |
| 37 | + |
| 38 | +Each layer must have a power-of-two number of gates. |
| 39 | + |
| 40 | +## API |
| 41 | + |
| 42 | +### Main Functions |
| 43 | + |
| 44 | +- `gkr_prove(circuit, input)` - Generate a GKR proof for a circuit evaluation. |
| 45 | +- `gkr_verify(proof, circuit, input)` - Verify a GKR proof. |
| 46 | + |
| 47 | +### Circuit Construction |
| 48 | + |
| 49 | +- `Circuit::new(layers, num_inputs)` - Create a new circuit with specified layers, gates, and number of inputs. |
| 50 | +- `CircuitLayer::new(gates)` - Create a layer with the given gates. |
| 51 | +- `Gate::new(gate_type, inputs_idx)` - Create a gate with type (Add/Mul) and certain input indices. |
| 52 | + |
| 53 | +## Example |
| 54 | + |
| 55 | +Here's a simple example of how to use the GKR Protocol: |
| 56 | + |
| 57 | +```rust |
| 58 | +use lambdaworks_math::field::fields::u64_prime_field::U64PrimeField; |
| 59 | +use lambdaworks_math::field::element::FieldElement; |
| 60 | +use lambdaworks_gkr::{gkr_prove, gkr_verify, circuit_from_lambda}; |
| 61 | + |
| 62 | +// Define the field (We use modulus 23 as in the example of our blog post). |
| 63 | +const MODULUS23: u64 = 23; |
| 64 | +type F23 = U64PrimeField<MODULUS23>; |
| 65 | +type F23E = FieldElement<F23>; |
| 66 | + |
| 67 | +// Create the circuit of our blog post. |
| 68 | +// This creates a 2-layer circuit plus the input layer. |
| 69 | +let circuit = lambda_post_circuit.unwrap(); |
| 70 | + |
| 71 | +// Define input values (from the post example). |
| 72 | +let input = [F23E::from(3), F23E::from(1)]; |
| 73 | + |
| 74 | +// Generate proof. |
| 75 | +let proof_result = gkr_prove(&circuit, &input); |
| 76 | +assert!(proof_result.is_ok()); |
| 77 | +let proof = proof_result.unwrap(); |
| 78 | + |
| 79 | +// Verify proof. |
| 80 | +let verification_result = gkr_verify(&proof, &circuit, &input); |
| 81 | +assert!(verification_result.is_ok() && verification_result.unwrap()); |
| 82 | +println!("GKR verification successful!"); |
| 83 | + |
| 84 | +// You can also check the actual output. |
| 85 | +let evaluation = circuit.evaluate(&input); |
| 86 | +println!("Circuit output: {:?}", evaluation.layers[0]); |
| 87 | +``` |
| 88 | + |
| 89 | +### Creating Custom Circuits |
| 90 | + |
| 91 | +You can create custom circuits by defining your own layers, gates, and number of inputs.: |
| 92 | + |
| 93 | +```rust |
| 94 | +use lambdaworks_gkr::circuit::{Circuit, CircuitLayer, Gate, GateType}; |
| 95 | + |
| 96 | +// Create a simple 2-layer circuit |
| 97 | +let custom_circuit = Circuit::new( |
| 98 | + vec![ |
| 99 | + // Output layer: 1 gate |
| 100 | + CircuitLayer::new(vec![ |
| 101 | + Gate::new(GateType::Add, [0, 1]), // Add the two results from layer 1 |
| 102 | + ]), |
| 103 | + // Layer 1: 2 gates |
| 104 | + CircuitLayer::new(vec![ |
| 105 | + Gate::new(GateType::Mul, [0, 1]), // Multiply first two inputs |
| 106 | + Gate::new(GateType::Mul, [2, 3]), // Multiply last two inputs |
| 107 | + ]), |
| 108 | + ], |
| 109 | + 4, // 4 inputs (power of 2) |
| 110 | +).unwrap(); |
| 111 | + |
| 112 | +// Test with inputs [2, 3, 4, 5] |
| 113 | +let input = [F23E::from(2), F23E::from(3), F23E::from(4), F23E::from(5)]; |
| 114 | + |
| 115 | +let proof = gkr_prove(&custom_circuit, &input).unwrap(); |
| 116 | +let is_valid = gkr_verify(&proof, &custom_circuit, &input).unwrap(); |
| 117 | + |
| 118 | +assert!(is_valid); |
| 119 | +``` |
| 120 | + |
| 121 | +## Protocol Details |
| 122 | + |
| 123 | +The GKR protocol works through the following steps: |
| 124 | + |
| 125 | +1. **Circuit Evaluation**: The prover evaluates the circuit on the given input to obtain the values at each layer. |
| 126 | +2. **Layer-by-Layer Reduction**: For each layer $i$, the prover uses the Sumcheck Protocol to reduce a claim about the current layer to a claim about the next layer $i+1$. |
| 127 | + |
| 128 | + - **Wiring Polynomial Construction**: The circuit's wiring is encoded as multilinear polynomials $\widetilde{\text{add}_i}$ and $\widetilde{\text{mul}_i}$ that describe which gates are addition/multiplication gates. |
| 129 | + |
| 130 | + - **Sumcheck Application**: The sumcheck is applied to the polynomial: |
| 131 | + $$\tilde f_{r_i}(b,c) = \widetilde{\text{add}_i(}r_i, b, c) \cdot (\tilde W_{i+1}(b) + \tilde W_{i+1}(c)) + \widetilde{\text{mul}_i}(r_i, b, c) \cdot (\tilde W_{i+1}(b) \cdot \tilde W_{i+1}(c))$$ |
| 132 | + |
| 133 | + where $\tilde W_{i+1}$ is the multilinear extension of layer $i+1$ values. |
| 134 | + |
| 135 | + - **Line Function**: A line function transforms the two claims of $\tilde W_{i+1}(b)$ and $\tilde W_{i+1}(c)$ into a single claim. |
| 136 | +3. **Input Verification**: The verifier checks the final claim, evaluating the input multilinear polynomial extension at the final evaluation point. |
| 137 | + |
| 138 | +Each *layer proof* consists of: |
| 139 | +- The claimed sum (that the sumcheck proves). |
| 140 | +- All the univariate polynomials used in the sumcheck. They are built by fixing the first variable and summing over the remaining variables. |
| 141 | +- The polynomial $q = \tilde W_{i+1} \circ \ell$ where $\ell$ is the line function. |
| 142 | + |
| 143 | +The protocol achieves $O(d \log S)$ verifier time and $O(S)$ prover time, where $d$ is the circuit depth and $S$ is the circuit size (i.e., the number of gates). |
| 144 | + |
| 145 | + |
| 146 | +## Fiat-Shamir transform |
| 147 | + |
| 148 | +This implementation uses the **Fiat-Shamir** to transform the interactive GKR protocol into a non-interactive proof system. Instead of requiring back-and-forth communication between prover and verifier, the prover generates all challenges deterministically by applying a hash function to the transcript. |
| 149 | + |
| 150 | +### How Fiat-Shamir is Applied |
| 151 | + |
| 152 | +The transformation works by replacing the verifier's random challenges with outputs from a cryptographic hash function applied on the transcript: |
| 153 | + |
| 154 | +1. **Transcript Initialization**: A transcript is created and seeded with: |
| 155 | + - Circuit structure (via `circuit_to_bytes(circuit)`) |
| 156 | + - Input values |
| 157 | + - Output values |
| 158 | + |
| 159 | +2. **Challenge Generation**: At each step where the interactive protocol would require a random challenge, the implementation: |
| 160 | + - Adds the current proof data to the transcript. |
| 161 | + - Samples a "random" field element from the transcript using `transcript.sample_field_element()`. |
| 162 | + |
| 163 | +3. **Key Challenge Points**: |
| 164 | + - **Initial random values** `r_0` for the output layer. |
| 165 | + - **Sumcheck challenges** ($s_j$) for each round of each layer's sumcheck protocol. |
| 166 | + - **Line function parameter** `r_last` for connecting layers. |
| 167 | + |
| 168 | + |
| 169 | +## References |
| 170 | + |
| 171 | +- [Goldwasser, Kalai, and Rothblum. "Delegating computation: interactive proofs for muggles"](https://dl.acm.org/doi/10.1145/1374376.1374396) |
| 172 | +- [Proofs, Arguments, and Zero-Knowledge. Chapter 4](https://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.pdf) |
| 173 | +- [Lambdaclass Blog Post: GKR protocol: a step-by-step example](https://blog.lambdaclass.com/gkr-protocol-a-step-by-step-example/) |
0 commit comments