sonobe/folding-schemes/src/folding/protogalaxy/circuits.rs
folding-schemes/src/folding/protogalaxy/circuits.rsRaw
1use ark_crypto_primitives::sponge::{
2 constraints::CryptographicSpongeVar,
3 poseidon::{constraints::PoseidonSpongeVar, PoseidonConfig, PoseidonSponge},
4 Absorb, CryptographicSponge,
5};
6use ark_ec::CurveGroup;
7use ark_ff::PrimeField;
8use ark_poly::{univariate::DensePolynomial, EvaluationDomain, GeneralEvaluationDomain};
9use ark_r1cs_std::{
10 alloc::AllocVar,
11 boolean::Boolean,
12 eq::EqGadget,
13 fields::{fp::FpVar, FieldVar},
14 groups::CurveVar,
15 poly::polynomial::univariate::dense::DensePolynomialVar,
16 R1CSVar, ToBitsGadget, ToConstraintFieldGadget,
17};
18use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, SynthesisError};
19use ark_std::{fmt::Debug, marker::PhantomData, One, Zero};
20
21use super::{
22 folding::lagrange_polys,
23 utils::{all_powers_var, betas_star_var, exponential_powers_var},
24 CommittedInstance, CommittedInstanceVar, ProtoGalaxyCycleFoldConfig,
25};
26use crate::{
27 folding::{
28 circuits::{
29 cyclefold::{
30 CycleFoldChallengeGadget, CycleFoldCommittedInstance,
31 CycleFoldCommittedInstanceVar, CycleFoldConfig, NIFSFullGadget,
32 },
33 nonnative::{affine::NonNativeAffineVar, uint::NonNativeUintVar},
34 CF1, CF2,
35 },
36 traits::{CommittedInstanceVarOps, Dummy},
37 },
38 frontend::FCircuit,
39 transcript::{AbsorbNonNativeGadget, TranscriptVar},
40 utils::gadgets::VectorGadget,
41};
42
43pub struct FoldingGadget {}
44
45impl FoldingGadget {
46 #[allow(clippy::type_complexity)]
47 pub fn fold_committed_instance<C: CurveGroup, S: CryptographicSponge>(
48 transcript: &mut impl TranscriptVar<C::ScalarField, S>,
49 // running instance
50 instance: &CommittedInstanceVar<C, true>,
51 // incoming instances
52 vec_instances: &[CommittedInstanceVar<C, false>],
53 // polys from P
54 F_coeffs: Vec<FpVar<C::ScalarField>>,
55 K_coeffs: Vec<FpVar<C::ScalarField>>,
56 ) -> Result<(CommittedInstanceVar<C, true>, Vec<FpVar<C::ScalarField>>), SynthesisError> {
57 let t = instance.betas.len();
58
59 // absorb the committed instances
60 transcript.absorb(instance)?;
61 transcript.absorb(&vec_instances)?;
62
63 let delta = transcript.get_challenge()?;
64 let deltas = exponential_powers_var(delta, t);
65
66 transcript.absorb(&F_coeffs)?;
67
68 let alpha = transcript.get_challenge()?;
69 let alphas = all_powers_var(alpha.clone(), t);
70
71 // F(alpha) = e + \sum_t F_i * alpha^i
72 let mut F_alpha = instance.e.clone();
73 for (i, F_i) in F_coeffs.iter().skip(1).enumerate() {
74 F_alpha += F_i * &alphas[i + 1];
75 }
76
77 let betas_star = betas_star_var(&instance.betas, &deltas, &alpha);
78
79 let k = vec_instances.len();
80 let H =
81 GeneralEvaluationDomain::new(k + 1).ok_or(SynthesisError::PolynomialDegreeTooLarge)?;
82 let L_X = lagrange_polys(H)
83 .into_iter()
84 .map(|poly| {
85 DensePolynomialVar::from_coefficients_vec(
86 poly.coeffs
87 .into_iter()
88 .map(FpVar::constant)
89 .collect::<Vec<_>>(),
90 )
91 })
92 .collect::<Vec<_>>();
93 let Z_X = DensePolynomialVar::from_coefficients_vec(
94 DensePolynomial::from(H.vanishing_polynomial())
95 .coeffs
96 .into_iter()
97 .map(FpVar::constant)
98 .collect::<Vec<_>>(),
99 );
100 let K_X = DensePolynomialVar { coeffs: K_coeffs };
101
102 transcript.absorb(&K_X.coeffs)?;
103
104 let gamma = transcript.get_challenge()?;
105
106 let L_X_evals = L_X
107 .iter()
108 .take(k + 1)
109 .map(|L| L.evaluate(&gamma))
110 .collect::<Result<Vec<_>, _>>()?;
111
112 let e_star = F_alpha * &L_X_evals[0] + Z_X.evaluate(&gamma)? * K_X.evaluate(&gamma)?;
113
114 let mut x_star = instance.x.mul_scalar(&L_X_evals[0])?;
115 for i in 0..k {
116 x_star = x_star.add(&vec_instances[i].x.mul_scalar(&L_X_evals[i + 1])?)?;
117 }
118
119 // return the folded instance
120 Ok((
121 CommittedInstanceVar {
122 betas: betas_star,
123 // phi will be computed in CycleFold
124 phi: NonNativeAffineVar::new_constant(ConstraintSystemRef::None, C::zero())?,
125 e: e_star,
126 x: x_star,
127 },
128 L_X_evals,
129 ))
130 }
131}
132
133pub struct AugmentationGadget;
134
135impl AugmentationGadget {
136 #[allow(clippy::type_complexity)]
137 pub fn prepare_and_fold_primary<C: CurveGroup, S: CryptographicSponge>(
138 transcript: &mut impl TranscriptVar<CF1<C>, S>,
139 U: CommittedInstanceVar<C, true>,
140 u_phis: Vec<NonNativeAffineVar<C>>,
141 u_xs: Vec<Vec<FpVar<CF1<C>>>>,
142 new_U_phi: NonNativeAffineVar<C>,
143 F_coeffs: Vec<FpVar<CF1<C>>>,
144 K_coeffs: Vec<FpVar<CF1<C>>>,
145 ) -> Result<(CommittedInstanceVar<C, true>, Vec<FpVar<CF1<C>>>), SynthesisError> {
146 assert_eq!(u_phis.len(), u_xs.len());
147
148 // Prepare the incoming instances.
149 // For each instance `u`, we have `u.betas = []`, `u.e = 0`.
150 let us = u_phis
151 .into_iter()
152 .zip(u_xs)
153 .map(|(phi, x)| CommittedInstanceVar {
154 phi,
155 betas: vec![],
156 e: FpVar::zero(),
157 x,
158 })
159 .collect::<Vec<_>>();
160
161 // Fold the incoming instances `us` into the running instance `U`.
162 let (mut U, L_X_evals) =
163 FoldingGadget::fold_committed_instance(transcript, &U, &us, F_coeffs, K_coeffs)?;
164 // Notice that FoldingGadget::fold_committed_instance does not fold phi.
165 // We set `U.phi` to unconstrained witnesses `U_phi` here, whose
166 // correctness will be checked on the other curve.
167 U.phi = new_U_phi;
168
169 Ok((U, L_X_evals))
170 }
171
172 pub fn prepare_and_fold_cyclefold<
173 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
174 C2: CurveGroup,
175 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
176 S: CryptographicSponge,
177 >(
178 transcript: &mut PoseidonSpongeVar<CF1<C1>>,
179 pp_hash: FpVar<CF1<C1>>,
180 mut cf_U: CycleFoldCommittedInstanceVar<C2, GC2>,
181 cf_u_cmWs: Vec<GC2>,
182 cf_u_xs: Vec<Vec<NonNativeUintVar<CF1<C1>>>>,
183 cf_cmTs: Vec<GC2>,
184 ) -> Result<CycleFoldCommittedInstanceVar<C2, GC2>, SynthesisError>
185 where
186 C2::BaseField: PrimeField + Absorb,
187 {
188 assert_eq!(cf_u_cmWs.len(), cf_u_xs.len());
189 assert_eq!(cf_u_xs.len(), cf_cmTs.len());
190
191 // Fold the incoming CycleFold instances into the running CycleFold
192 // instance in a iterative way, since `NIFSFullGadget` only supports
193 // folding one incoming instance at a time.
194 for ((cmW, x), cmT) in cf_u_cmWs.into_iter().zip(cf_u_xs).zip(cf_cmTs) {
195 // Prepare the incoming CycleFold instance `cf_u` for the current
196 // iteration.
197 // For each CycleFold instance `cf_u`, we have `cf_u.cmE = 0`, and
198 // `cf_u.u = 1`.
199 let cf_u = CycleFoldCommittedInstanceVar {
200 cmE: GC2::zero(),
201 u: NonNativeUintVar::new_constant(ConstraintSystemRef::None, C1::BaseField::one())?,
202 cmW,
203 x,
204 };
205
206 let cf_r_bits = CycleFoldChallengeGadget::get_challenge_gadget(
207 transcript,
208 pp_hash.clone(),
209 cf_U.to_native_sponge_field_elements()?,
210 cf_u.clone(),
211 cmT.clone(),
212 )?;
213 // Fold the current incoming CycleFold instance `cf_u` into the
214 // running CycleFold instance `cf_U`.
215 cf_U = NIFSFullGadget::fold_committed_instance(cf_r_bits, cmT, cf_U, cf_u)?;
216 }
217
218 Ok(cf_U)
219 }
220}
221
222/// `AugmentedFCircuit` enhances the original step function `F`, so that it can
223/// be used in recursive arguments such as IVC.
224///
225/// The method for converting `F` to `AugmentedFCircuit` (`F'`) is defined in
226/// [Nova](https://eprint.iacr.org/2021/370.pdf), where `AugmentedFCircuit` not
227/// only invokes `F`, but also adds additional constraints for verifying the
228/// correct folding of primary instances (i.e., the instances over `C1`).
229/// In the paper, the primary instances are Nova's `CommittedInstance`, but we
230/// extend this method to support using ProtoGalaxy's `CommittedInstance` as
231/// primary instances.
232///
233/// Furthermore, to reduce circuit size over `C2`, we implement the constraints
234/// defined in [CycleFold](https://eprint.iacr.org/2023/1192.pdf). These extra
235/// constraints verify the correct folding of CycleFold instances.
236#[derive(Debug, Clone)]
237pub struct AugmentedFCircuit<
238 C1: CurveGroup,
239 C2: CurveGroup,
240 GC2: CurveVar<C2, CF2<C2>>,
241 FC: FCircuit<CF1<C1>>,
242> {
243 pub(super) _gc2: PhantomData<GC2>,
244 pub(super) poseidon_config: PoseidonConfig<CF1<C1>>,
245 pub(super) pp_hash: CF1<C1>,
246 pub(super) i: CF1<C1>,
247 pub(super) i_usize: usize,
248 pub(super) z_0: Vec<CF1<C1>>,
249 pub(super) z_i: Vec<CF1<C1>>,
250 pub(super) external_inputs: Vec<CF1<C1>>,
251 pub(super) F: FC, // F circuit
252 pub(super) u_i_phi: C1,
253 pub(super) U_i: CommittedInstance<C1, true>,
254 pub(super) U_i1_phi: C1,
255 pub(super) F_coeffs: Vec<CF1<C1>>,
256 pub(super) K_coeffs: Vec<CF1<C1>>,
257 pub(super) x: Option<CF1<C1>>, // public input (u_{i+1}.x[0])
258
259 pub(super) phi_stars: Vec<C1>,
260
261 pub(super) cf1_u_i_cmW: C2, // input
262 pub(super) cf2_u_i_cmW: C2, // input
263 pub(super) cf_U_i: CycleFoldCommittedInstance<C2>, // input
264 pub(super) cf1_cmT: C2,
265 pub(super) cf2_cmT: C2,
266 pub(super) cf_x: Option<CF1<C1>>, // public input (u_{i+1}.x[1])
267}
268
269impl<C1: CurveGroup, C2: CurveGroup, GC2: CurveVar<C2, CF2<C2>>, FC: FCircuit<CF1<C1>>>
270 AugmentedFCircuit<C1, C2, GC2, FC>
271{
272 pub fn empty(
273 poseidon_config: &PoseidonConfig<CF1<C1>>,
274 F_circuit: FC,
275 t: usize,
276 d: usize,
277 k: usize,
278 ) -> Self {
279 let u_dummy = CommittedInstance::dummy((2, t));
280 let cf_u_dummy =
281 CycleFoldCommittedInstance::dummy(ProtoGalaxyCycleFoldConfig::<C1>::IO_LEN);
282
283 Self {
284 _gc2: PhantomData,
285 poseidon_config: poseidon_config.clone(),
286 pp_hash: CF1::<C1>::zero(),
287 i: CF1::<C1>::zero(),
288 i_usize: 0,
289 z_0: vec![CF1::<C1>::zero(); F_circuit.state_len()],
290 z_i: vec![CF1::<C1>::zero(); F_circuit.state_len()],
291 external_inputs: vec![CF1::<C1>::zero(); F_circuit.external_inputs_len()],
292 u_i_phi: C1::zero(),
293 U_i: u_dummy,
294 U_i1_phi: C1::zero(),
295 F_coeffs: vec![CF1::<C1>::zero(); t],
296 K_coeffs: vec![CF1::<C1>::zero(); d * k + 1],
297 phi_stars: vec![C1::zero(); k],
298 F: F_circuit,
299 x: None,
300 // cyclefold values
301 cf1_u_i_cmW: C2::zero(),
302 cf2_u_i_cmW: C2::zero(),
303 cf_U_i: cf_u_dummy,
304 cf1_cmT: C2::zero(),
305 cf2_cmT: C2::zero(),
306 cf_x: None,
307 }
308 }
309}
310
311impl<C1, C2, GC2, FC> ConstraintSynthesizer<CF1<C1>> for AugmentedFCircuit<C1, C2, GC2, FC>
312where
313 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
314 C2: CurveGroup,
315 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
316 FC: FCircuit<CF1<C1>>,
317 C2::BaseField: PrimeField + Absorb,
318{
319 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
320 let pp_hash = FpVar::<CF1<C1>>::new_witness(cs.clone(), || Ok(self.pp_hash))?;
321 let i = FpVar::<CF1<C1>>::new_witness(cs.clone(), || Ok(self.i))?;
322 let z_0 = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || Ok(self.z_0))?;
323 let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || Ok(self.z_i))?;
324 let external_inputs =
325 Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || Ok(self.external_inputs))?;
326
327 let u_dummy = CommittedInstance::<C1, true>::dummy((2, self.U_i.betas.len()));
328 let U_i = CommittedInstanceVar::<C1, true>::new_witness(cs.clone(), || Ok(self.U_i))?;
329 let u_i_phi = NonNativeAffineVar::new_witness(cs.clone(), || Ok(self.u_i_phi))?;
330 let U_i1_phi = NonNativeAffineVar::new_witness(cs.clone(), || Ok(self.U_i1_phi))?;
331 let phi_stars =
332 Vec::<NonNativeAffineVar<C1>>::new_witness(cs.clone(), || Ok(self.phi_stars))?;
333
334 let cf_u_dummy =
335 CycleFoldCommittedInstance::dummy(ProtoGalaxyCycleFoldConfig::<C1>::IO_LEN);
336 let cf_U_i =
337 CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || Ok(self.cf_U_i))?;
338 let cf1_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf1_cmT))?;
339 let cf2_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf2_cmT))?;
340
341 let F_coeffs = Vec::new_witness(cs.clone(), || Ok(self.F_coeffs))?;
342 let K_coeffs = Vec::new_witness(cs.clone(), || Ok(self.K_coeffs))?;
343
344 // `sponge` is for digest computation.
345 let sponge = PoseidonSpongeVar::<C1::ScalarField>::new(cs.clone(), &self.poseidon_config);
346 // `transcript` is for challenge generation.
347 let mut transcript = sponge.clone();
348
349 let is_basecase = i.is_zero()?;
350
351 // Primary Part
352 // P.1. Compute u_i.x
353 // u_i.x[0] = H(i, z_0, z_i, U_i)
354 let (u_i_x, _) = U_i.clone().hash(&sponge, &pp_hash, &i, &z_0, &z_i)?;
355 // u_i.x[1] = H(cf_U_i)
356 let (cf_u_i_x, _) = cf_U_i.clone().hash(&sponge, pp_hash.clone())?;
357
358 // P.2. Prepare incoming primary instances
359 // P.3. Fold incoming primary instances into the running instance
360 let (U_i1, r) = AugmentationGadget::prepare_and_fold_primary(
361 &mut transcript,
362 U_i.clone(),
363 vec![u_i_phi.clone()],
364 vec![vec![u_i_x, cf_u_i_x]],
365 U_i1_phi,
366 F_coeffs,
367 K_coeffs,
368 )?;
369
370 // P.4.a compute and check the first output of F'
371
372 // get z_{i+1} from the F circuit
373 let z_i1 =
374 self.F
375 .generate_step_constraints(cs.clone(), self.i_usize, z_i, external_inputs)?;
376
377 // Base case: u_{i+1}.x[0] == H((i+1, z_0, z_{i+1}, U_{\bot})
378 // Non-base case: u_{i+1}.x[0] == H((i+1, z_0, z_{i+1}, U_{i+1})
379 let (u_i1_x, _) = U_i1.clone().hash(
380 &sponge,
381 &pp_hash,
382 &(i + FpVar::<CF1<C1>>::one()),
383 &z_0,
384 &z_i1,
385 )?;
386 let (u_i1_x_base, _) = CommittedInstanceVar::new_constant(cs.clone(), u_dummy)?.hash(
387 &sponge,
388 &pp_hash,
389 &FpVar::<CF1<C1>>::one(),
390 &z_0,
391 &z_i1,
392 )?;
393 let x = FpVar::new_input(cs.clone(), || Ok(self.x.unwrap_or(u_i1_x_base.value()?)))?;
394 x.enforce_equal(&is_basecase.select(&u_i1_x_base, &u_i1_x)?)?;
395
396 // CycleFold part
397 // C.1. Compute cf1_u_i.x and cf2_u_i.x
398 let mut r0_bits = r[0].to_bits_le()?;
399 let mut r1_bits = r[1].to_bits_le()?;
400 r0_bits.resize(C1::ScalarField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
401 r1_bits.resize(C1::ScalarField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
402 let cf1_x = [
403 r0_bits
404 .chunks(C1::BaseField::MODULUS_BIT_SIZE as usize - 1)
405 .map(|bits| {
406 let mut bits = bits.to_vec();
407 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
408 NonNativeUintVar::from(&bits)
409 })
410 .collect::<Vec<_>>(),
411 vec![
412 NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::zero())?,
413 NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::zero())?,
414 U_i.phi.x.clone(),
415 U_i.phi.y.clone(),
416 phi_stars[0].x.clone(),
417 phi_stars[0].y.clone(),
418 ],
419 ]
420 .concat();
421 let cf2_x = [
422 r1_bits
423 .chunks(C1::BaseField::MODULUS_BIT_SIZE as usize - 1)
424 .map(|bits| {
425 let mut bits = bits.to_vec();
426 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
427 NonNativeUintVar::from(&bits)
428 })
429 .collect::<Vec<_>>(),
430 vec![
431 phi_stars[0].x.clone(),
432 phi_stars[0].y.clone(),
433 u_i_phi.x.clone(),
434 u_i_phi.y.clone(),
435 U_i1.phi.x.clone(),
436 U_i1.phi.y.clone(),
437 ],
438 ]
439 .concat();
440
441 // C.2. Prepare incoming CycleFold instances
442 // C.3. Fold incoming CycleFold instances into the running instance
443 let cf_U_i1 =
444 AugmentationGadget::prepare_and_fold_cyclefold::<C1, C2, GC2, PoseidonSponge<CF1<C1>>>(
445 &mut transcript,
446 pp_hash.clone(),
447 cf_U_i,
448 vec![
449 GC2::new_witness(cs.clone(), || Ok(self.cf1_u_i_cmW))?,
450 GC2::new_witness(cs.clone(), || Ok(self.cf2_u_i_cmW))?,
451 ],
452 vec![cf1_x, cf2_x],
453 vec![cf1_cmT, cf2_cmT],
454 )?;
455
456 // Back to Primary Part
457 // P.4.b compute and check the second output of F'
458 // Base case: u_{i+1}.x[1] == H(cf_U_{\bot})
459 // Non-base case: u_{i+1}.x[1] == H(cf_U_{i+1})
460 let (cf_u_i1_x, _) = cf_U_i1.clone().hash(&sponge, pp_hash.clone())?;
461 let (cf_u_i1_x_base, _) =
462 CycleFoldCommittedInstanceVar::<C2, GC2>::new_constant(cs.clone(), cf_u_dummy)?
463 .hash(&sponge, pp_hash.clone())?;
464 let cf_x = FpVar::new_input(cs.clone(), || {
465 Ok(self.cf_x.unwrap_or(cf_u_i1_x_base.value()?))
466 })?;
467 cf_x.enforce_equal(&is_basecase.select(&cf_u_i1_x_base, &cf_u_i1_x)?)?;
468
469 Ok(())
470 }
471}
472
473#[cfg(test)]
474mod tests {
475 use std::error::Error;
476
477 use super::*;
478 use crate::{
479 arith::r1cs::tests::get_test_r1cs,
480 folding::protogalaxy::folding::{tests::prepare_inputs, Folding},
481 transcript::poseidon::poseidon_canonical_config,
482 };
483
484 use ark_bn254::{Fr, G1Projective as Projective};
485 use ark_relations::r1cs::ConstraintSystem;
486
487 #[test]
488 fn test_folding_gadget() -> Result<(), Box<dyn Error>> {
489 let k = 7;
490 let (witness, instance, witnesses, instances) = prepare_inputs(k);
491 let r1cs = get_test_r1cs::<Fr>();
492
493 // init Prover & Verifier's transcript
494 let poseidon_config = poseidon_canonical_config::<Fr>();
495 let mut transcript_p = PoseidonSponge::new(&poseidon_config);
496 let mut transcript_v = PoseidonSponge::new(&poseidon_config);
497
498 let (_, _, proof, _) = Folding::<Projective>::prove(
499 &mut transcript_p,
500 &r1cs,
501 &instance,
502 &witness,
503 &instances,
504 &witnesses,
505 )?;
506
507 let folded_instance =
508 Folding::<Projective>::verify(&mut transcript_v, &instance, &instances, proof.clone())?;
509
510 let cs = ConstraintSystem::new_ref();
511 let mut transcript_var = PoseidonSpongeVar::new(cs.clone(), &poseidon_config);
512 let instance_var = CommittedInstanceVar::new_witness(cs.clone(), || Ok(instance))?;
513 let instances_var = Vec::new_witness(cs.clone(), || Ok(instances))?;
514 let F_coeffs_var = Vec::new_witness(cs.clone(), || Ok(proof.F_coeffs))?;
515 let K_coeffs_var = Vec::new_witness(cs.clone(), || Ok(proof.K_coeffs))?;
516
517 let (folded_instance_var, _) = FoldingGadget::fold_committed_instance(
518 &mut transcript_var,
519 &instance_var,
520 &instances_var,
521 F_coeffs_var,
522 K_coeffs_var,
523 )?;
524 assert_eq!(folded_instance.betas, folded_instance_var.betas.value()?);
525 assert_eq!(folded_instance.e, folded_instance_var.e.value()?);
526 assert_eq!(folded_instance.x, folded_instance_var.x.value()?);
527 assert!(cs.is_satisfied()?);
528
529 Ok(())
530 }
531}