sonobe_fs/nova/instances/
circuits.rs

1//! In-circuit variables for Nova instances.
2
3use ark_r1cs_std::{
4    GR1CSVar,
5    alloc::{AllocVar, AllocationMode},
6    fields::fp::FpVar,
7    prelude::Boolean,
8    select::CondSelectGadget,
9};
10use ark_relations::gr1cs::{ConstraintSystemRef, Namespace, SynthesisError};
11use ark_std::borrow::Borrow;
12use sonobe_primitives::{commitments::CommitmentDefGadget, transcripts::AbsorbableVar};
13
14use super::{IncomingInstance, RunningInstance};
15use crate::FoldingInstanceVar;
16
17/// [`RunningInstanceVar`] defines Nova's running instance variable.
18#[derive(Clone, Debug, PartialEq)]
19pub struct RunningInstanceVar<CM: CommitmentDefGadget> {
20    /// [`RunningInstanceVar::cm_e`] is the error term commitment.
21    pub cm_e: CM::CommitmentVar,
22    /// [`RunningInstanceVar::u`] is the constant term.
23    pub u: CM::ScalarVar,
24    /// [`RunningInstanceVar::cm_w`] is the witness commitment.
25    pub cm_w: CM::CommitmentVar,
26    /// [`RunningInstanceVar::x`] is the vector of public inputs (to the
27    /// circuit).
28    pub x: Vec<CM::ScalarVar>,
29}
30
31impl<CM: CommitmentDefGadget> AllocVar<RunningInstance<CM::Widget>, CM::ConstraintField>
32    for RunningInstanceVar<CM>
33{
34    fn new_variable<T: Borrow<RunningInstance<CM::Widget>>>(
35        cs: impl Into<Namespace<CM::ConstraintField>>,
36        f: impl FnOnce() -> Result<T, SynthesisError>,
37        mode: AllocationMode,
38    ) -> Result<Self, SynthesisError> {
39        let cs = cs.into().cs();
40        let v = f()?;
41        let RunningInstance { cm_e, u, cm_w, x } = v.borrow();
42        Ok(Self {
43            cm_e: AllocVar::new_variable(cs.clone(), || Ok(cm_e), mode)?,
44            u: AllocVar::new_variable(cs.clone(), || Ok(u), mode)?,
45            cm_w: AllocVar::new_variable(cs.clone(), || Ok(cm_w), mode)?,
46            x: AllocVar::new_variable(cs.clone(), || Ok(&x[..]), mode)?,
47        })
48    }
49}
50
51impl<CM: CommitmentDefGadget> GR1CSVar<CM::ConstraintField> for RunningInstanceVar<CM> {
52    type Value = RunningInstance<CM::Widget>;
53
54    fn cs(&self) -> ConstraintSystemRef<CM::ConstraintField> {
55        self.cm_e
56            .cs()
57            .or(self.u.cs())
58            .or(self.cm_w.cs())
59            .or(self.x.cs())
60    }
61
62    fn value(&self) -> Result<Self::Value, SynthesisError> {
63        Ok(RunningInstance {
64            cm_e: self.cm_e.value()?,
65            u: self.u.value()?,
66            cm_w: self.cm_w.value()?,
67            x: self.x.value()?,
68        })
69    }
70}
71
72impl<CM: CommitmentDefGadget> AbsorbableVar<CM::ConstraintField> for RunningInstanceVar<CM> {
73    fn absorb_into(
74        &self,
75        dest: &mut Vec<FpVar<CM::ConstraintField>>,
76    ) -> Result<(), SynthesisError> {
77        self.u.absorb_into(dest)?;
78        self.x.absorb_into(dest)?;
79        self.cm_e.absorb_into(dest)?;
80        self.cm_w.absorb_into(dest)
81    }
82}
83
84impl<CM: CommitmentDefGadget> CondSelectGadget<CM::ConstraintField> for RunningInstanceVar<CM> {
85    fn conditionally_select(
86        cond: &Boolean<CM::ConstraintField>,
87        true_value: &Self,
88        false_value: &Self,
89    ) -> Result<Self, SynthesisError> {
90        if true_value.x.len() != false_value.x.len() {
91            return Err(SynthesisError::Unsatisfiable);
92        }
93        Ok(Self {
94            cm_e: cond.select(&true_value.cm_e, &false_value.cm_e)?,
95            u: cond.select(&true_value.u, &false_value.u)?,
96            cm_w: cond.select(&true_value.cm_w, &false_value.cm_w)?,
97            x: true_value
98                .x
99                .iter()
100                .zip(&false_value.x)
101                .map(|(t, f)| cond.select(t, f))
102                .collect::<Result<_, _>>()?,
103        })
104    }
105}
106
107impl<CM: CommitmentDefGadget> FoldingInstanceVar<CM> for RunningInstanceVar<CM> {
108    fn commitments(&self) -> Vec<&CM::CommitmentVar> {
109        vec![&self.cm_w, &self.cm_e]
110    }
111
112    fn public_inputs(&self) -> &Vec<CM::ScalarVar> {
113        &self.x
114    }
115
116    fn new_witness_with_public_inputs(
117        cs: impl Into<Namespace<CM::ConstraintField>>,
118        u: &Self::Value,
119        x: Vec<CM::ScalarVar>,
120    ) -> Result<Self, SynthesisError> {
121        let cs = cs.into().cs();
122        Ok(Self {
123            cm_e: AllocVar::new_witness(cs.clone(), || Ok(&u.cm_e))?,
124            u: AllocVar::new_witness(cs.clone(), || Ok(&u.u))?,
125            cm_w: AllocVar::new_witness(cs.clone(), || Ok(&u.cm_w))?,
126            x,
127        })
128    }
129}
130
131/// [`IncomingInstanceVar`] defines Nova's incoming instance variable.
132#[derive(Clone, Debug, PartialEq)]
133pub struct IncomingInstanceVar<CM: CommitmentDefGadget> {
134    /// [`IncomingInstanceVar::cm_w`] is the witness commitment.
135    pub cm_w: CM::CommitmentVar,
136    /// [`IncomingInstanceVar::x`] is the vector of public inputs (to the
137    /// circuit).
138    pub x: Vec<CM::ScalarVar>,
139}
140
141impl<CM: CommitmentDefGadget> AllocVar<IncomingInstance<CM::Widget>, CM::ConstraintField>
142    for IncomingInstanceVar<CM>
143{
144    fn new_variable<T: Borrow<IncomingInstance<CM::Widget>>>(
145        cs: impl Into<Namespace<CM::ConstraintField>>,
146        f: impl FnOnce() -> Result<T, SynthesisError>,
147        mode: AllocationMode,
148    ) -> Result<Self, SynthesisError> {
149        let cs = cs.into().cs();
150        let v = f()?;
151        let IncomingInstance { cm_w, x } = v.borrow();
152        Ok(Self {
153            cm_w: AllocVar::new_variable(cs.clone(), || Ok(cm_w), mode)?,
154            x: AllocVar::new_variable(cs.clone(), || Ok(&x[..]), mode)?,
155        })
156    }
157}
158
159impl<CM: CommitmentDefGadget> GR1CSVar<CM::ConstraintField> for IncomingInstanceVar<CM> {
160    type Value = IncomingInstance<CM::Widget>;
161
162    fn cs(&self) -> ConstraintSystemRef<CM::ConstraintField> {
163        self.cm_w.cs().or(self.x.cs())
164    }
165
166    fn value(&self) -> Result<Self::Value, SynthesisError> {
167        Ok(IncomingInstance {
168            cm_w: self.cm_w.value()?,
169            x: self.x.value()?,
170        })
171    }
172}
173
174impl<CM: CommitmentDefGadget> AbsorbableVar<CM::ConstraintField> for IncomingInstanceVar<CM> {
175    fn absorb_into(
176        &self,
177        dest: &mut Vec<FpVar<CM::ConstraintField>>,
178    ) -> Result<(), SynthesisError> {
179        self.x.absorb_into(dest)?;
180        self.cm_w.absorb_into(dest)
181    }
182}
183
184impl<CM: CommitmentDefGadget> CondSelectGadget<CM::ConstraintField> for IncomingInstanceVar<CM> {
185    fn conditionally_select(
186        cond: &Boolean<CM::ConstraintField>,
187        true_value: &Self,
188        false_value: &Self,
189    ) -> Result<Self, SynthesisError> {
190        if true_value.x.len() != false_value.x.len() {
191            return Err(SynthesisError::Unsatisfiable);
192        }
193        Ok(Self {
194            cm_w: cond.select(&true_value.cm_w, &false_value.cm_w)?,
195            x: true_value
196                .x
197                .iter()
198                .zip(&false_value.x)
199                .map(|(t, f)| cond.select(t, f))
200                .collect::<Result<_, _>>()?,
201        })
202    }
203}
204
205impl<CM: CommitmentDefGadget> FoldingInstanceVar<CM> for IncomingInstanceVar<CM> {
206    fn commitments(&self) -> Vec<&CM::CommitmentVar> {
207        vec![&self.cm_w]
208    }
209
210    fn public_inputs(&self) -> &Vec<CM::ScalarVar> {
211        &self.x
212    }
213
214    fn new_witness_with_public_inputs(
215        cs: impl Into<Namespace<CM::ConstraintField>>,
216        u: &Self::Value,
217        x: Vec<CM::ScalarVar>,
218    ) -> Result<Self, SynthesisError> {
219        let cs = cs.into().cs();
220        Ok(Self {
221            cm_w: AllocVar::new_witness(cs.clone(), || Ok(&u.cm_w))?,
222            x,
223        })
224    }
225}
sonobe_fs/nova/instances/circuits.rs

sonobe_fs/nova/instances/
circuits.rs
