exo_proofs/
circuit.rs

1// Copyright 2026 Exochain Foundation
2//
3// Licensed under the Apache License, Version 2.0 (the "License");
4// you may not use this file except in compliance with the License.
5// You may obtain a copy of the License at:
6//
7//     https://www.apache.org/licenses/LICENSE-2.0
8//
9// Unless required by applicable law or agreed to in writing, software
10// distributed under the License is distributed on an "AS IS" BASIS,
11// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12// See the License for the specific language governing permissions and
13// limitations under the License.
14//
15// SPDX-License-Identifier: Apache-2.0
16
17//! Circuit abstraction -- R1CS constraint system.
18//!
19//! Provides the `Circuit` trait and a `ConstraintSystem` for expressing
20//! arithmetic circuits as rank-1 constraint systems (A * B = C).
21
22use serde::{Deserialize, Serialize};
23
24use crate::error::{ProofError, Result};
25
26// ---------------------------------------------------------------------------
27// Variable
28// ---------------------------------------------------------------------------
29
30/// A variable in the constraint system.
31#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
32pub struct Variable {
33    /// Index into the constraint system's variable list.
34    pub index: usize,
35    /// The witness value (populated during proving, None during setup).
36    pub value: Option<u64>,
37}
38
39// ---------------------------------------------------------------------------
40// LinearCombination
41// ---------------------------------------------------------------------------
42
43/// A linear combination of variables: sum of (coefficient, variable_index) pairs.
44/// The constant term uses index `usize::MAX` as a sentinel for the "one" variable.
45#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
46pub struct LinearCombination {
47    pub terms: Vec<(u64, usize)>,
48}
49
50impl LinearCombination {
51    /// Create an empty linear combination.
52    #[must_use]
53    pub fn zero() -> Self {
54        Self { terms: Vec::new() }
55    }
56
57    /// Create a linear combination with a single variable.
58    #[must_use]
59    pub fn from_variable(var: Variable) -> Self {
60        Self {
61            terms: vec![(1, var.index)],
62        }
63    }
64
65    /// Create a constant linear combination.
66    #[must_use]
67    pub fn constant(value: u64) -> Self {
68        Self {
69            terms: vec![(value, usize::MAX)],
70        }
71    }
72
73    /// Add a term.
74    pub fn add_term(&mut self, coeff: u64, var_index: usize) {
75        self.terms.push((coeff, var_index));
76    }
77
78    /// Evaluate the linear combination given variable assignments.
79    /// `vars[i]` = value of variable i. The "one" variable (index MAX) = 1.
80    pub fn evaluate(&self, vars: &[u64]) -> Result<u64> {
81        let mut sum: u64 = 0;
82        for &(coeff, idx) in &self.terms {
83            let val = if idx == usize::MAX {
84                1u64
85            } else if idx < vars.len() {
86                vars[idx]
87            } else {
88                return Err(ProofError::ConstraintError(format!(
89                    "linear combination references unallocated variable index {idx}; allocated variables: {}",
90                    vars.len()
91                )));
92            };
93            let term = coeff.checked_mul(val).ok_or_else(|| {
94                ProofError::ConstraintError(format!(
95                    "linear combination term overflows u64: coefficient {coeff} multiplied by value {val}"
96                ))
97            })?;
98            sum = sum.checked_add(term).ok_or_else(|| {
99                ProofError::ConstraintError(format!(
100                    "linear combination sum overflows u64 when adding term {term}"
101                ))
102            })?;
103        }
104        Ok(sum)
105    }
106
107    fn references_only_allocated_variables(&self, variable_count: usize) -> bool {
108        self.terms
109            .iter()
110            .all(|&(_, idx)| idx == usize::MAX || idx < variable_count)
111    }
112}
113
114// ---------------------------------------------------------------------------
115// Constraint
116// ---------------------------------------------------------------------------
117
118/// An R1CS constraint: A * B = C, where A, B, C are linear combinations.
119#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
120pub struct Constraint {
121    pub a_terms: LinearCombination,
122    pub b_terms: LinearCombination,
123    pub c_terms: LinearCombination,
124}
125
126// ---------------------------------------------------------------------------
127// ConstraintSystem
128// ---------------------------------------------------------------------------
129
130/// A constraint system accumulating R1CS constraints.
131#[derive(Debug, Clone)]
132pub struct ConstraintSystem {
133    /// All allocated variables.
134    pub variables: Vec<Variable>,
135    /// All constraints.
136    pub constraints: Vec<Constraint>,
137    /// Number of public input variables.
138    pub num_public_inputs: usize,
139    /// Indices of public input variables.
140    pub public_input_indices: Vec<usize>,
141}
142
143impl ConstraintSystem {
144    /// Create a new empty constraint system.
145    #[must_use]
146    pub fn new() -> Self {
147        Self {
148            variables: Vec::new(),
149            constraints: Vec::new(),
150            num_public_inputs: 0,
151            public_input_indices: Vec::new(),
152        }
153    }
154
155    /// Number of variables.
156    #[must_use]
157    pub fn num_variables(&self) -> usize {
158        self.variables.len()
159    }
160
161    /// Number of constraints.
162    #[must_use]
163    pub fn num_constraints(&self) -> usize {
164        self.constraints.len()
165    }
166
167    /// Check if all constraints are satisfied by the current variable assignments.
168    pub fn is_satisfied(&self) -> bool {
169        let mut vals = Vec::with_capacity(self.variables.len());
170        for variable in &self.variables {
171            let Some(value) = variable.value else {
172                return false;
173            };
174            vals.push(value);
175        }
176
177        for c in &self.constraints {
178            if !c.a_terms.references_only_allocated_variables(vals.len())
179                || !c.b_terms.references_only_allocated_variables(vals.len())
180                || !c.c_terms.references_only_allocated_variables(vals.len())
181            {
182                return false;
183            }
184            let (Ok(a), Ok(b), Ok(c_val)) = (
185                c.a_terms.evaluate(&vals),
186                c.b_terms.evaluate(&vals),
187                c.c_terms.evaluate(&vals),
188            ) else {
189                return false;
190            };
191            let Some(product) = a.checked_mul(b) else {
192                return false;
193            };
194            if product != c_val {
195                return false;
196            }
197        }
198        true
199    }
200}
201
202impl Default for ConstraintSystem {
203    fn default() -> Self {
204        Self::new()
205    }
206}
207
208/// Allocate a variable in the constraint system.
209pub fn allocate(cs: &mut ConstraintSystem, value: Option<u64>) -> Variable {
210    let index = cs.variables.len();
211    let var = Variable { index, value };
212    cs.variables.push(var);
213    var
214}
215
216/// Allocate a public input variable.
217pub fn allocate_public(cs: &mut ConstraintSystem, value: Option<u64>) -> Variable {
218    let var = allocate(cs, value);
219    cs.public_input_indices.push(var.index);
220    cs.num_public_inputs += 1;
221    var
222}
223
224/// Enforce an R1CS constraint: A * B = C.
225pub fn enforce(
226    cs: &mut ConstraintSystem,
227    a: &LinearCombination,
228    b: &LinearCombination,
229    c: &LinearCombination,
230) {
231    cs.constraints.push(Constraint {
232        a_terms: a.clone(),
233        b_terms: b.clone(),
234        c_terms: c.clone(),
235    });
236}
237
238// ---------------------------------------------------------------------------
239// Circuit trait
240// ---------------------------------------------------------------------------
241
242/// A circuit that can synthesize constraints.
243pub trait Circuit {
244    /// Synthesize the circuit's constraints into the given constraint system.
245    fn synthesize(&self, cs: &mut ConstraintSystem) -> Result<()>;
246}
247
248// ---------------------------------------------------------------------------
249// Tests
250// ---------------------------------------------------------------------------
251
252#[cfg(test)]
253mod tests {
254    use super::*;
255
256    /// A simple circuit: x * y = z
257    #[derive(Debug)]
258    struct MultiplyCircuit {
259        x: Option<u64>,
260        y: Option<u64>,
261        z: Option<u64>,
262    }
263
264    impl Circuit for MultiplyCircuit {
265        fn synthesize(&self, cs: &mut ConstraintSystem) -> Result<()> {
266            let x = allocate_public(cs, self.x);
267            let y = allocate(cs, self.y);
268            let z = allocate_public(cs, self.z);
269
270            // x * y = z
271            let a = LinearCombination::from_variable(x);
272            let b = LinearCombination::from_variable(y);
273            let c = LinearCombination::from_variable(z);
274            enforce(cs, &a, &b, &c);
275
276            Ok(())
277        }
278    }
279
280    /// A circuit that checks a + b = c using a * 1 = (c - a) pattern: (a + b) * 1 = c
281    #[derive(Debug)]
282    struct AddCircuit {
283        a: Option<u64>,
284        b: Option<u64>,
285        c: Option<u64>,
286    }
287
288    impl Circuit for AddCircuit {
289        fn synthesize(&self, cs: &mut ConstraintSystem) -> Result<()> {
290            let a_var = allocate_public(cs, self.a);
291            let b_var = allocate(cs, self.b);
292            let c_var = allocate_public(cs, self.c);
293
294            // (a + b) * 1 = c
295            let mut a_lc = LinearCombination::zero();
296            a_lc.add_term(1, a_var.index);
297            a_lc.add_term(1, b_var.index);
298            let b_lc = LinearCombination::constant(1);
299            let c_lc = LinearCombination::from_variable(c_var);
300            enforce(cs, &a_lc, &b_lc, &c_lc);
301
302            Ok(())
303        }
304    }
305
306    #[test]
307    fn empty_constraint_system() {
308        let cs = ConstraintSystem::new();
309        assert_eq!(cs.num_variables(), 0);
310        assert_eq!(cs.num_constraints(), 0);
311        assert!(cs.is_satisfied());
312    }
313
314    #[test]
315    fn default_constraint_system() {
316        let cs = ConstraintSystem::default();
317        assert!(cs.is_satisfied());
318    }
319
320    #[test]
321    fn allocate_variable() {
322        let mut cs = ConstraintSystem::new();
323        let v = allocate(&mut cs, Some(42));
324        assert_eq!(v.index, 0);
325        assert_eq!(v.value, Some(42));
326        assert_eq!(cs.num_variables(), 1);
327    }
328
329    #[test]
330    fn allocate_public_input() {
331        let mut cs = ConstraintSystem::new();
332        let v = allocate_public(&mut cs, Some(10));
333        assert_eq!(v.index, 0);
334        assert_eq!(cs.num_public_inputs, 1);
335    }
336
337    #[test]
338    fn multiply_circuit_satisfied() {
339        let circuit = MultiplyCircuit {
340            x: Some(3),
341            y: Some(4),
342            z: Some(12),
343        };
344        let mut cs = ConstraintSystem::new();
345        circuit.synthesize(&mut cs).unwrap();
346        assert_eq!(cs.num_variables(), 3);
347        assert_eq!(cs.num_constraints(), 1);
348        assert_eq!(cs.num_public_inputs, 2);
349        assert!(cs.is_satisfied());
350    }
351
352    #[test]
353    fn multiply_circuit_not_satisfied() {
354        let circuit = MultiplyCircuit {
355            x: Some(3),
356            y: Some(4),
357            z: Some(13), // wrong
358        };
359        let mut cs = ConstraintSystem::new();
360        circuit.synthesize(&mut cs).unwrap();
361        assert!(!cs.is_satisfied());
362    }
363
364    #[test]
365    fn add_circuit_satisfied() {
366        let circuit = AddCircuit {
367            a: Some(5),
368            b: Some(7),
369            c: Some(12),
370        };
371        let mut cs = ConstraintSystem::new();
372        circuit.synthesize(&mut cs).unwrap();
373        assert!(cs.is_satisfied());
374    }
375
376    #[test]
377    fn add_circuit_not_satisfied() {
378        let circuit = AddCircuit {
379            a: Some(5),
380            b: Some(7),
381            c: Some(11), // wrong
382        };
383        let mut cs = ConstraintSystem::new();
384        circuit.synthesize(&mut cs).unwrap();
385        assert!(!cs.is_satisfied());
386    }
387
388    #[test]
389    fn linear_combination_evaluate() {
390        let mut lc = LinearCombination::zero();
391        lc.add_term(2, 0); // 2 * x0
392        lc.add_term(3, 1); // 3 * x1
393        lc.add_term(5, usize::MAX); // 5 * 1
394
395        let vars = vec![10, 20]; // x0=10, x1=20
396        assert_eq!(lc.evaluate(&vars).unwrap(), 2 * 10 + 3 * 20 + 5);
397    }
398
399    #[test]
400    fn linear_combination_zero() {
401        let lc = LinearCombination::zero();
402        assert_eq!(lc.evaluate(&[1, 2, 3]).unwrap(), 0);
403    }
404
405    #[test]
406    fn linear_combination_constant() {
407        let lc = LinearCombination::constant(42);
408        assert_eq!(lc.evaluate(&[]).unwrap(), 42);
409    }
410
411    #[test]
412    fn linear_combination_from_variable() {
413        let v = Variable {
414            index: 2,
415            value: Some(7),
416        };
417        let lc = LinearCombination::from_variable(v);
418        assert_eq!(lc.evaluate(&[0, 0, 7]).unwrap(), 7);
419    }
420
421    #[test]
422    fn enforce_constraint() {
423        let mut cs = ConstraintSystem::new();
424        let x = allocate(&mut cs, Some(5));
425        let y = allocate(&mut cs, Some(5));
426        let z = allocate(&mut cs, Some(25));
427
428        let a = LinearCombination::from_variable(x);
429        let b = LinearCombination::from_variable(y);
430        let c = LinearCombination::from_variable(z);
431        enforce(&mut cs, &a, &b, &c);
432
433        assert!(cs.is_satisfied());
434    }
435
436    #[test]
437    fn multiple_constraints() {
438        let mut cs = ConstraintSystem::new();
439        let x = allocate(&mut cs, Some(2));
440        let y = allocate(&mut cs, Some(3));
441        let z = allocate(&mut cs, Some(6)); // x*y
442        let w = allocate(&mut cs, Some(36)); // z*z
443
444        // x * y = z
445        enforce(
446            &mut cs,
447            &LinearCombination::from_variable(x),
448            &LinearCombination::from_variable(y),
449            &LinearCombination::from_variable(z),
450        );
451
452        // z * z = w
453        enforce(
454            &mut cs,
455            &LinearCombination::from_variable(z),
456            &LinearCombination::from_variable(z),
457            &LinearCombination::from_variable(w),
458        );
459
460        assert_eq!(cs.num_constraints(), 2);
461        assert!(cs.is_satisfied());
462    }
463
464    #[test]
465    fn constraint_system_with_missing_witness_is_not_satisfied() {
466        let mut cs = ConstraintSystem::new();
467        let x = allocate(&mut cs, None);
468
469        enforce(
470            &mut cs,
471            &LinearCombination::from_variable(x),
472            &LinearCombination::constant(1),
473            &LinearCombination::constant(0),
474        );
475
476        assert!(
477            !cs.is_satisfied(),
478            "missing witness variables must not be substituted with zero"
479        );
480    }
481
482    #[test]
483    fn constraint_system_with_unallocated_variable_reference_is_not_satisfied() {
484        let mut cs = ConstraintSystem::new();
485        let x = allocate(&mut cs, Some(0));
486        let mut unallocated = LinearCombination::zero();
487        unallocated.add_term(1, x.index + 1);
488
489        enforce(
490            &mut cs,
491            &unallocated,
492            &LinearCombination::constant(1),
493            &LinearCombination::constant(0),
494        );
495
496        assert!(
497            !cs.is_satisfied(),
498            "constraints must not satisfy by treating unallocated variables as zero"
499        );
500    }
501
502    #[test]
503    fn constraint_system_with_overflowing_linear_combination_is_not_satisfied() {
504        let mut cs = ConstraintSystem::new();
505        let x = allocate(&mut cs, Some(u64::MAX));
506        let y = allocate(&mut cs, Some(1));
507
508        let mut overflowing_sum = LinearCombination::zero();
509        overflowing_sum.add_term(1, x.index);
510        overflowing_sum.add_term(1, y.index);
511
512        enforce(
513            &mut cs,
514            &overflowing_sum,
515            &LinearCombination::constant(1),
516            &LinearCombination::constant(0),
517        );
518
519        assert!(
520            !cs.is_satisfied(),
521            "linear combination overflow must fail closed instead of wrapping to zero"
522        );
523    }
524
525    #[test]
526    fn constraint_system_with_overflowing_constraint_product_is_not_satisfied() {
527        let mut cs = ConstraintSystem::new();
528        let x = allocate(&mut cs, Some(u64::MAX));
529        let y = allocate(&mut cs, Some(2));
530        let z = allocate(&mut cs, Some(u64::MAX - 1));
531
532        enforce(
533            &mut cs,
534            &LinearCombination::from_variable(x),
535            &LinearCombination::from_variable(y),
536            &LinearCombination::from_variable(z),
537        );
538
539        assert!(
540            !cs.is_satisfied(),
541            "constraint multiplication overflow must fail closed instead of wrapping"
542        );
543    }
544
545    #[test]
546    fn variable_without_value() {
547        let mut cs = ConstraintSystem::new();
548        let _v = allocate(&mut cs, None);
549        assert_eq!(cs.variables[0].value, None);
550    }
551
552    #[test]
553    fn constraint_clone_eq() {
554        let c = Constraint {
555            a_terms: LinearCombination::constant(1),
556            b_terms: LinearCombination::constant(2),
557            c_terms: LinearCombination::constant(2),
558        };
559        let c2 = c.clone();
560        assert_eq!(c, c2);
561    }
562}
exo_proofs/circuit.rs

exo_proofs/
circuit.rs
