sonobe_fs/nova/circuits/
verifier.rs1use 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}