snarkvm_circuit_environment/helpers/
converter.rs

1// Copyright (c) 2019-2025 Provable Inc.
2// This file is part of the snarkVM library.
3
4// Licensed under the Apache License, Version 2.0 (the "License");
5// you may not use this file except in compliance with the License.
6// You may obtain a copy of the License at:
7
8// http://www.apache.org/licenses/LICENSE-2.0
9
10// Unless required by applicable law or agreed to in writing, software
11// distributed under the License is distributed on an "AS IS" BASIS,
12// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13// See the License for the specific language governing permissions and
14// limitations under the License.
15
16use crate::{CanaryCircuit, Circuit, LinearCombination, R1CS, TestnetCircuit, Variable};
17use snarkvm_curves::edwards_bls12::Fq;
18use snarkvm_fields::PrimeField;
19
20use indexmap::IndexMap;
21
22/// A struct for tracking the mapping of variables from the virtual machine (first) to the gadget constraint system (second).
23struct Converter {
24    public: IndexMap<u64, snarkvm_algorithms::r1cs::Variable>,
25    private: IndexMap<u64, snarkvm_algorithms::r1cs::Variable>,
26}
27
28impl snarkvm_algorithms::r1cs::ConstraintSynthesizer<Fq> for Circuit {
29    /// Synthesizes the constraints from the environment into a `snarkvm_algorithms::r1cs`-compliant constraint system.
30    fn generate_constraints<CS: snarkvm_algorithms::r1cs::ConstraintSystem<Fq>>(
31        &self,
32        cs: &mut CS,
33    ) -> Result<(), snarkvm_algorithms::r1cs::SynthesisError> {
34        crate::circuit::CIRCUIT.with(|circuit| circuit.borrow().generate_constraints(cs))
35    }
36}
37
38impl snarkvm_algorithms::r1cs::ConstraintSynthesizer<Fq> for TestnetCircuit {
39    /// Synthesizes the constraints from the environment into a `snarkvm_algorithms::r1cs`-compliant constraint system.
40    fn generate_constraints<CS: snarkvm_algorithms::r1cs::ConstraintSystem<Fq>>(
41        &self,
42        cs: &mut CS,
43    ) -> Result<(), snarkvm_algorithms::r1cs::SynthesisError> {
44        crate::testnet_circuit::TESTNET_CIRCUIT.with(|circuit| circuit.borrow().generate_constraints(cs))
45    }
46}
47
48impl snarkvm_algorithms::r1cs::ConstraintSynthesizer<Fq> for CanaryCircuit {
49    /// Synthesizes the constraints from the environment into a `snarkvm_algorithms::r1cs`-compliant constraint system.
50    fn generate_constraints<CS: snarkvm_algorithms::r1cs::ConstraintSystem<Fq>>(
51        &self,
52        cs: &mut CS,
53    ) -> Result<(), snarkvm_algorithms::r1cs::SynthesisError> {
54        crate::canary_circuit::CANARY_CIRCUIT.with(|circuit| circuit.borrow().generate_constraints(cs))
55    }
56}
57
58impl<F: PrimeField> R1CS<F> {
59    /// Synthesizes the constraints from the environment into a `snarkvm_algorithms::r1cs`-compliant constraint system.
60    fn generate_constraints<CS: snarkvm_algorithms::r1cs::ConstraintSystem<F>>(
61        &self,
62        cs: &mut CS,
63    ) -> Result<(), snarkvm_algorithms::r1cs::SynthesisError> {
64        let mut converter = Converter { public: Default::default(), private: Default::default() };
65
66        // Ensure the given `cs` is starting off clean.
67        assert_eq!(1, cs.num_public_variables());
68        assert_eq!(0, cs.num_private_variables());
69        assert_eq!(0, cs.num_constraints());
70
71        let result = converter.public.insert(0, CS::one());
72        assert!(result.is_none(), "Overwrote an existing public variable in the converter");
73
74        // Allocate the public variables.
75        // NOTE: we skip the first public `One` variable because we already allocated it in the `ConstraintSystem` constructor.
76        for (i, public) in self.to_public_variables().iter().skip(1).enumerate() {
77            match public {
78                Variable::Public(index_value) => {
79                    let (index, value) = index_value.as_ref();
80
81                    assert_eq!(
82                        (i + 1) as u64,
83                        *index,
84                        "Public vars in first system must be processed in lexicographic order"
85                    );
86
87                    let gadget = cs.alloc_input(|| format!("Public {i}"), || Ok(*value))?;
88
89                    assert_eq!(
90                        snarkvm_algorithms::r1cs::Index::Public(*index as usize),
91                        gadget.get_unchecked(),
92                        "Public variables in the second system must match the first system (with an off-by-1 for the public case)"
93                    );
94
95                    let result = converter.public.insert(*index, gadget);
96
97                    assert!(result.is_none(), "Overwrote an existing public variable in the converter");
98                }
99                _ => unreachable!("Public variables in the first system are not well-formed"),
100            }
101        }
102
103        // Allocate the private variables.
104        for (i, private) in self.to_private_variables().iter().enumerate() {
105            match private {
106                Variable::Private(index_value) => {
107                    let (index, value) = index_value.as_ref();
108
109                    assert_eq!(
110                        i as u64, *index,
111                        "Private variables in first system must be processed in lexicographic order"
112                    );
113
114                    let gadget = cs.alloc(|| format!("Private {i}"), || Ok(*value))?;
115
116                    assert_eq!(
117                        snarkvm_algorithms::r1cs::Index::Private(i),
118                        gadget.get_unchecked(),
119                        "Private variables in the second system must match the first system"
120                    );
121
122                    let result = converter.private.insert(*index, gadget);
123
124                    assert!(result.is_none(), "Overwrote an existing private variable in the converter");
125                }
126                _ => unreachable!("Private variables in the first system are not well-formed"),
127            }
128        }
129
130        // Enforce all of the constraints.
131        for (i, constraint) in self.to_constraints().iter().enumerate() {
132            // Converts terms from one linear combination in the first system to the second system.
133            let convert_linear_combination =
134                |lc: &LinearCombination<F>| -> snarkvm_algorithms::r1cs::LinearCombination<F> {
135                    // Initialize a linear combination for the second system.
136                    let mut linear_combination = snarkvm_algorithms::r1cs::LinearCombination::<F>::zero();
137
138                    // Process every term in the linear combination.
139                    for (variable, coefficient) in lc.to_terms() {
140                        match variable {
141                            Variable::Constant(_) => {
142                                unreachable!(
143                                    "Failed during constraint translation. The first system by definition cannot have constant variables in the terms"
144                                )
145                            }
146                            Variable::Public(index_value) => {
147                                let (index, _value) = index_value.as_ref();
148                                let gadget = converter.public.get(index).unwrap();
149                                assert_eq!(
150                                    snarkvm_algorithms::r1cs::Index::Public((index + 1) as usize),
151                                    gadget.get_unchecked(),
152                                    "Failed during constraint translation. The public variable in the second system must match the first system (with an off-by-1 for the public case)"
153                                );
154                                linear_combination += (*coefficient, *gadget);
155                            }
156                            Variable::Private(index_value) => {
157                                let (index, _value) = index_value.as_ref();
158                                let gadget = converter.private.get(index).unwrap();
159                                assert_eq!(
160                                    snarkvm_algorithms::r1cs::Index::Private(*index as usize),
161                                    gadget.get_unchecked(),
162                                    "Failed during constraint translation. The private variable in the second system must match the first system"
163                                );
164                                linear_combination += (*coefficient, *gadget);
165                            }
166                        }
167                    }
168
169                    // Finally, add the accumulated constant value to the linear combination.
170                    if !lc.to_constant().is_zero() {
171                        linear_combination += (
172                            lc.to_constant(),
173                            snarkvm_algorithms::r1cs::Variable::new_unchecked(snarkvm_algorithms::r1cs::Index::Public(
174                                0,
175                            )),
176                        );
177                    }
178
179                    // Return the linear combination of the second system.
180                    linear_combination
181                };
182
183            let (a, b, c) = constraint.to_terms();
184
185            cs.enforce(
186                || format!("Constraint {i}"),
187                |lc| lc + convert_linear_combination(a),
188                |lc| lc + convert_linear_combination(b),
189                |lc| lc + convert_linear_combination(c),
190            );
191        }
192
193        // Ensure the given `cs` matches in size with the first system.
194        assert_eq!(self.num_public(), cs.num_public_variables() as u64);
195        assert_eq!(self.num_private(), cs.num_private_variables() as u64);
196        assert_eq!(self.num_constraints(), cs.num_constraints() as u64);
197
198        Ok(())
199    }
200}
201
202#[cfg(test)]
203mod tests {
204    use snarkvm_algorithms::{AlgebraicSponge, SNARK, r1cs::ConstraintSynthesizer, snark::varuna::VarunaVersion};
205    use snarkvm_circuit::prelude::*;
206    use snarkvm_curves::bls12_377::Fr;
207
208    /// Compute 2^EXPONENT - 1, in a purposefully constraint-inefficient manner for testing.
209    fn create_example_circuit<E: Environment>() -> Field<E> {
210        let one = snarkvm_console_types::Field::<E::Network>::one();
211        let two = one + one;
212
213        const EXPONENT: u64 = 64;
214
215        // Compute 2^EXPONENT - 1, in a purposefully constraint-inefficient manner for testing.
216        let mut candidate = Field::<E>::new(Mode::Public, one);
217        let mut accumulator = Field::new(Mode::Private, two);
218        for _ in 0..EXPONENT {
219            candidate += &accumulator;
220            accumulator *= Field::new(Mode::Private, two);
221        }
222
223        assert_eq!((accumulator - Field::one()).eject_value(), candidate.eject_value());
224        assert_eq!(2, E::num_public());
225        assert_eq!(2 * EXPONENT + 1, E::num_private());
226        assert_eq!(EXPONENT, E::num_constraints());
227        assert!(E::is_satisfied());
228
229        candidate
230    }
231
232    #[test]
233    fn test_constraint_converter() {
234        let _candidate_output = create_example_circuit::<Circuit>();
235
236        let mut cs = snarkvm_algorithms::r1cs::TestConstraintSystem::new();
237        Circuit.generate_constraints(&mut cs).unwrap();
238        {
239            use snarkvm_algorithms::r1cs::ConstraintSystem;
240            assert_eq!(Circuit::num_public(), cs.num_public_variables() as u64);
241            assert_eq!(Circuit::num_private(), cs.num_private_variables() as u64);
242            assert_eq!(Circuit::num_constraints(), cs.num_constraints() as u64);
243            assert!(cs.is_satisfied());
244        }
245    }
246
247    #[test]
248    fn test_varuna() {
249        let _candidate_output = create_example_circuit::<Circuit>();
250        let one = snarkvm_console_types::Field::<<Circuit as Environment>::Network>::one();
251
252        // Varuna setup, prove, and verify.
253
254        use snarkvm_algorithms::{
255            crypto_hash::PoseidonSponge,
256            snark::varuna::{VarunaHidingMode, VarunaSNARK, ahp::AHPForR1CS},
257        };
258        use snarkvm_curves::bls12_377::{Bls12_377, Fq};
259        use snarkvm_utilities::rand::TestRng;
260
261        type FS = PoseidonSponge<Fq, 2, 1>;
262        type VarunaInst = VarunaSNARK<Bls12_377, FS, VarunaHidingMode>;
263
264        let rng = &mut TestRng::default();
265
266        let max_degree = AHPForR1CS::<Fr, VarunaHidingMode>::max_degree(200, 200, 300).unwrap();
267        let universal_srs = VarunaInst::universal_setup(max_degree).unwrap();
268        let universal_prover = &universal_srs.to_universal_prover().unwrap();
269        let universal_verifier = &universal_srs.to_universal_verifier().unwrap();
270        let fs_pp = FS::sample_parameters();
271
272        let (index_pk, index_vk) = VarunaInst::circuit_setup(&universal_srs, &Circuit).unwrap();
273        let varuna_version = VarunaVersion::V2;
274        println!("Called circuit setup");
275
276        let proof = VarunaInst::prove(universal_prover, &fs_pp, &index_pk, varuna_version, &Circuit, rng).unwrap();
277        println!("Called prover");
278
279        assert!(
280            VarunaInst::verify(universal_verifier, &fs_pp, &index_vk, varuna_version, [*one, *one], &proof).unwrap()
281        );
282        println!("Called verifier");
283        println!("\nShould not verify (i.e. verifier messages should print below):");
284        assert!(
285            !VarunaInst::verify(universal_verifier, &fs_pp, &index_vk, varuna_version, [*one, *one + *one], &proof)
286                .unwrap()
287        );
288    }
289}