Skip to main content

sonobe_fs/nova/circuits/
verifier.rs

1//! Partial and full in-circuit verifier implementations for Nova.
2
3use ark_r1cs_std::{GR1CSVar, alloc::AllocVar, groups::CurveVar};
4use ark_relations::gr1cs::SynthesisError;
5use sonobe_primitives::{
6    algebra::ops::bits::FromBitsGadget,
7    commitments::{CommitmentDef, CommitmentDefGadget, GroupBasedCommitment},
8    transcripts::TranscriptGadget,
9};
10
11use crate::{
12    FoldingSchemeFullVerifierGadget, FoldingSchemePartialVerifierGadget, nova::AbstractNovaGadget,
13};
14
15impl<CM, const B: usize> FoldingSchemePartialVerifierGadget<1, 1> for AbstractNovaGadget<CM, B>
16where
17    CM: CommitmentDefGadget<Widget: GroupBasedCommitment>,
18{
19    #[allow(non_snake_case)]
20    fn verify_hinted(
21        _vk: &Self::VerifierKey,
22        transcript: &mut impl TranscriptGadget<CM::ConstraintField>,
23        [U]: [&Self::RU; 1],
24        [u]: [&Self::IU; 1],
25        proof: &Self::Proof<1, 1>,
26    ) -> Result<Self::RU, SynthesisError> {
27        let rho_bits = transcript.add(&U)?.add(&u)?.add(proof)?.challenge_bits(B)?;
28        let rho = CM::ScalarVar::from_bits_le(&rho_bits)?;
29
30        if U.x.len() != u.x.len() {
31            return Err(SynthesisError::Unsatisfiable);
32        }
33
34        Ok(Self::RU {
35            u: (U.u.clone() + &rho)
36                .try_into()
37                .map_err(|_| SynthesisError::Unsatisfiable)?,
38            cm_e: CM::CommitmentVar::new_witness(U.cm_e.cs().or(proof.cs()).or(rho.cs()), || {
39                Ok(U.cm_e.value().unwrap_or_default()
40                    + proof.value().unwrap_or_default() * rho.value().unwrap_or_default())
41            })?,
42            cm_w: CM::CommitmentVar::new_witness(U.cm_w.cs().or(u.cm_w.cs()).or(rho.cs()), || {
43                Ok(U.cm_w.value().unwrap_or_default()
44                    + u.cm_w.value().unwrap_or_default() * rho.value().unwrap_or_default())
45            })?,
46            x: U.x
47                .iter()
48                .zip(&u.x)
49                .map(|(a, b)| (b.clone() * &rho + a).try_into())
50                .collect::<Result<_, _>>()
51                .map_err(|_| SynthesisError::Unsatisfiable)?,
52        })
53    }
54}
55
56impl<CM, const B: usize> FoldingSchemePartialVerifierGadget<2, 0> for AbstractNovaGadget<CM, B>
57where
58    CM: CommitmentDefGadget<Widget: GroupBasedCommitment>,
59{
60    #[allow(non_snake_case)]
61    fn verify_hinted(
62        _vk: &Self::VerifierKey,
63        transcript: &mut impl TranscriptGadget<CM::ConstraintField>,
64        [U1, U2]: [&Self::RU; 2],
65        _: [&Self::IU; 0],
66        proof: &Self::Proof<2, 0>,
67    ) -> Result<Self::RU, SynthesisError> {
68        let rho_bits = transcript.add(&(U1, U2))?.add(proof)?.challenge_bits(B)?;
69        let rho = CM::ScalarVar::from_bits_le(&rho_bits)?;
70
71        if U1.x.len() != U2.x.len() {
72            return Err(SynthesisError::Unsatisfiable);
73        }
74
75        Ok(Self::RU {
76            u: (U2.u.clone() * &rho + &U1.u)
77                .try_into()
78                .map_err(|_| SynthesisError::Unsatisfiable)?,
79            cm_e: CM::CommitmentVar::new_witness(
80                U1.cm_e.cs().or(U2.cm_e.cs()).or(proof.cs()).or(rho.cs()),
81                || {
82                    let rho = rho.value().unwrap_or_default();
83                    Ok(U1.cm_e.value().unwrap_or_default()
84                        + proof.value().unwrap_or_default() * rho
85                        + U2.cm_e.value().unwrap_or_default() * rho * rho)
86                },
87            )?,
88            cm_w: CM::CommitmentVar::new_witness(
89                U1.cm_w.cs().or(U2.cm_w.cs()).or(rho.cs()),
90                || {
91                    Ok(U1.cm_w.value().unwrap_or_default()
92                        + U2.cm_w.value().unwrap_or_default() * rho.value().unwrap_or_default())
93                },
94            )?,
95            x: U1
96                .x
97                .iter()
98                .zip(&U2.x)
99                .map(|(a, b)| (b.clone() * &rho + a).try_into())
100                .collect::<Result<_, _>>()
101                .map_err(|_| SynthesisError::Unsatisfiable)?,
102        })
103    }
104}
105
106impl<CM, const B: usize> FoldingSchemeFullVerifierGadget<1, 1> for AbstractNovaGadget<CM, B>
107where
108    CM: CommitmentDefGadget<Widget: GroupBasedCommitment>,
109    CM::CommitmentVar: CurveVar<<CM::Widget as CommitmentDef>::Commitment, CM::ConstraintField>,
110{
111    #[allow(non_snake_case)]
112    fn verify(
113        _vk: &Self::VerifierKey,
114        transcript: &mut impl TranscriptGadget<CM::ConstraintField>,
115        [U]: [&Self::RU; 1],
116        [u]: [&Self::IU; 1],
117        proof: &Self::Proof<1, 1>,
118    ) -> Result<Self::RU, SynthesisError> {
119        let rho_bits = transcript.add(&U)?.add(&u)?.add(proof)?.challenge_bits(B)?;
120        let rho = CM::ScalarVar::from_bits_le(&rho_bits)?;
121
122        if U.x.len() != u.x.len() {
123            return Err(SynthesisError::Unsatisfiable);
124        }
125
126        Ok(Self::RU {
127            u: (U.u.clone() + &rho)
128                .try_into()
129                .map_err(|_| SynthesisError::Unsatisfiable)?,
130            cm_e: proof.scalar_mul_le(rho_bits.iter())? + &U.cm_e,
131            cm_w: u.cm_w.scalar_mul_le(rho_bits.iter())? + &U.cm_w,
132            x: U.x
133                .iter()
134                .zip(&u.x)
135                .map(|(a, b)| (b.clone() * &rho + a).try_into())
136                .collect::<Result<_, _>>()
137                .map_err(|_| SynthesisError::Unsatisfiable)?,
138        })
139    }
140}