openvm_static_verifier/
backend.rs

1//! Halo2 (`halo2-base`) implementation of the [`chip_traits`](crate::chip_traits) backend.
2//!
3//! Pure delegation to the concrete chips so that the generic circuit-construction code
4//! assigns exactly the same advice cells as the original non-generic code.
5
6use std::sync::Arc;
7
8use halo2_base::{
9    gates::{GateInstructions, RangeChip},
10    halo2_proofs::halo2curves::bn256::Fr,
11    AssignedValue, Context, QuantumCell,
12};
13use openvm_stark_sdk::p3_baby_bear::BabyBear;
14
15use crate::{
16    chip_traits::{
17        BabyBearExt4Inst, BabyBearInst, ChipBase, GateInst, PopulateInputs, Poseidon2Inst,
18        TranscriptInst,
19    },
20    field::baby_bear::{
21        BabyBearChip, BabyBearExt4, BabyBearExt4Chip, BabyBearExt4Wire, BabyBearWire,
22        ReducedBabyBearExt4Wire, ReducedBabyBearWire,
23    },
24    hash::poseidon2::{compress_bn254_digests, hash_babybear_slice_to_digest},
25    transcript::{DigestWire, TranscriptChip},
26};
27
28/// Backend bundling the concrete halo2 chips and the circuit-building [`Context`]. The
29/// transcript is created lazily by [`TranscriptInst::init_transcript`], mirroring
30/// `TranscriptChip::new` at the start of `constrained_verify`.
31pub struct Halo2Backend<'ctx> {
32    ctx: &'ctx mut Context<Fr>,
33    ext: BabyBearExt4Chip,
34    transcript: Option<TranscriptChip>,
35}
36
37impl<'ctx> Halo2Backend<'ctx> {
38    pub fn new(range: Arc<RangeChip<Fr>>, ctx: &'ctx mut Context<Fr>) -> Self {
39        Self::from_ext_chip(BabyBearExt4Chip::new(BabyBearChip::new(range)), ctx)
40    }
41
42    pub fn from_ext_chip(ext: BabyBearExt4Chip, ctx: &'ctx mut Context<Fr>) -> Self {
43        Self {
44            ctx,
45            ext,
46            transcript: None,
47        }
48    }
49
50    pub fn ext_chip(&self) -> &BabyBearExt4Chip {
51        &self.ext
52    }
53
54    /// Escape hatch for code that needs the raw context (e.g. test pranks).
55    pub fn ctx_mut(&mut self) -> &mut Context<Fr> {
56        self.ctx
57    }
58
59    /// Disjoint borrows of the extension chip and the context.
60    fn ext_parts(&mut self) -> (&BabyBearExt4Chip, &mut Context<Fr>) {
61        (&self.ext, &mut *self.ctx)
62    }
63
64    /// Disjoint borrows of the base-field chip and the context.
65    fn bb_parts(&mut self) -> (&BabyBearChip, &mut Context<Fr>) {
66        (self.ext.base(), &mut *self.ctx)
67    }
68
69    /// Disjoint borrows of the transcript chip and the context.
70    fn transcript_parts(&mut self) -> (&mut TranscriptChip, &mut Context<Fr>) {
71        (
72            self.transcript
73                .as_mut()
74                .expect("transcript not initialized; call init_transcript first"),
75            &mut *self.ctx,
76        )
77    }
78}
79
80impl ChipBase for Halo2Backend<'_> {
81    type F = AssignedValue<Fr>;
82}
83
84impl PopulateInputs for Halo2Backend<'_> {
85    fn load_witness(&mut self, value: Fr) -> AssignedValue<Fr> {
86        self.ctx.load_witness(value)
87    }
88
89    fn bb_load_reduced_witness(&mut self, value: BabyBear) -> ReducedBabyBearWire {
90        let (bb, ctx) = self.bb_parts();
91        bb.load_reduced_witness(ctx, value)
92    }
93
94    fn ext_load_reduced_witness(&mut self, value: BabyBearExt4) -> ReducedBabyBearExt4Wire {
95        let (ext, ctx) = self.ext_parts();
96        ext.load_reduced_witness(ctx, value)
97    }
98}
99
100impl GateInst for Halo2Backend<'_> {
101    fn load_constant(&mut self, value: Fr) -> AssignedValue<Fr> {
102        self.ctx.load_constant(value)
103    }
104
105    fn constrain_equal(&mut self, a: AssignedValue<Fr>, b: AssignedValue<Fr>) {
106        self.ctx.constrain_equal(&a, &b);
107    }
108
109    fn select(
110        &mut self,
111        when_true: AssignedValue<Fr>,
112        when_false: AssignedValue<Fr>,
113        cond: AssignedValue<Fr>,
114    ) -> AssignedValue<Fr> {
115        let (bb, ctx) = self.bb_parts();
116        bb.gate().select(ctx, when_true, when_false, cond)
117    }
118
119    fn select_const(
120        &mut self,
121        when_true: Fr,
122        when_false: Fr,
123        cond: AssignedValue<Fr>,
124    ) -> AssignedValue<Fr> {
125        let (bb, ctx) = self.bb_parts();
126        bb.gate().select(
127            ctx,
128            QuantumCell::Constant(when_true),
129            QuantumCell::Constant(when_false),
130            cond,
131        )
132    }
133
134    fn num_to_bits(&mut self, a: AssignedValue<Fr>, range_bits: usize) -> Vec<AssignedValue<Fr>> {
135        let (bb, ctx) = self.bb_parts();
136        bb.gate().num_to_bits(ctx, a, range_bits)
137    }
138
139    fn inner_product_const(
140        &mut self,
141        values: &[AssignedValue<Fr>],
142        coeffs: &[Fr],
143    ) -> AssignedValue<Fr> {
144        let (bb, ctx) = self.bb_parts();
145        bb.gate().inner_product(
146            ctx,
147            values.iter().copied(),
148            coeffs.iter().copied().map(QuantumCell::Constant),
149        )
150    }
151
152    fn cell_count(&self) -> usize {
153        self.ctx.advice.len()
154    }
155}
156
157impl BabyBearInst for Halo2Backend<'_> {
158    fn bb_load_constant(&mut self, value: BabyBear) -> BabyBearWire {
159        let (bb, ctx) = self.bb_parts();
160        bb.load_constant(ctx, value)
161    }
162
163    fn bb_load_reduced_constant(&mut self, value: BabyBear) -> ReducedBabyBearWire {
164        let (bb, ctx) = self.bb_parts();
165        bb.load_reduced_constant(ctx, value)
166    }
167
168    fn bb_reduce(&mut self, a: BabyBearWire) -> BabyBearWire {
169        let (bb, ctx) = self.bb_parts();
170        bb.reduce(ctx, a)
171    }
172
173    fn bb_reduce_max_bits(&mut self, a: BabyBearWire) -> BabyBearWire {
174        let (bb, ctx) = self.bb_parts();
175        bb.reduce_max_bits(ctx, a)
176    }
177
178    fn bb_add(&mut self, a: BabyBearWire, b: BabyBearWire) -> BabyBearWire {
179        let (bb, ctx) = self.bb_parts();
180        bb.add(ctx, a, b)
181    }
182
183    fn bb_neg(&mut self, a: BabyBearWire) -> BabyBearWire {
184        let (bb, ctx) = self.bb_parts();
185        bb.neg(ctx, a)
186    }
187
188    fn bb_sub(&mut self, a: BabyBearWire, b: BabyBearWire) -> BabyBearWire {
189        let (bb, ctx) = self.bb_parts();
190        bb.sub(ctx, a, b)
191    }
192
193    fn bb_mul(&mut self, a: BabyBearWire, b: BabyBearWire) -> BabyBearWire {
194        let (bb, ctx) = self.bb_parts();
195        bb.mul(ctx, a, b)
196    }
197
198    fn bb_mul_add(&mut self, a: BabyBearWire, b: BabyBearWire, c: BabyBearWire) -> BabyBearWire {
199        let (bb, ctx) = self.bb_parts();
200        bb.mul_add(ctx, a, b, c)
201    }
202
203    fn bb_div(&mut self, a: BabyBearWire, b: BabyBearWire) -> BabyBearWire {
204        let (bb, ctx) = self.bb_parts();
205        bb.div(ctx, a, b)
206    }
207
208    fn bb_assert_zero(&mut self, a: BabyBearWire) {
209        let (bb, ctx) = self.bb_parts();
210        bb.assert_zero(ctx, a)
211    }
212
213    fn bb_assert_equal(&mut self, a: BabyBearWire, b: BabyBearWire) {
214        let (bb, ctx) = self.bb_parts();
215        bb.assert_equal(ctx, a, b)
216    }
217
218    fn bb_zero(&mut self) -> BabyBearWire {
219        let (bb, ctx) = self.bb_parts();
220        bb.zero(ctx)
221    }
222
223    fn bb_one(&mut self) -> BabyBearWire {
224        let (bb, ctx) = self.bb_parts();
225        bb.one(ctx)
226    }
227
228    fn bb_mul_const(&mut self, a: BabyBearWire, c: BabyBear) -> BabyBearWire {
229        let (bb, ctx) = self.bb_parts();
230        bb.mul_const(ctx, a, c)
231    }
232
233    fn bb_square(&mut self, a: BabyBearWire) -> BabyBearWire {
234        let (bb, ctx) = self.bb_parts();
235        bb.square(ctx, a)
236    }
237
238    fn bb_pow_power_of_two(&mut self, a: BabyBearWire, n: usize) -> BabyBearWire {
239        let (bb, ctx) = self.bb_parts();
240        bb.pow_power_of_two(ctx, a, n)
241    }
242}
243
244impl BabyBearExt4Inst for Halo2Backend<'_> {
245    fn ext_load_constant(&mut self, value: BabyBearExt4) -> BabyBearExt4Wire {
246        let (ext, ctx) = self.ext_parts();
247        ext.load_constant(ctx, value)
248    }
249
250    fn ext_load_reduced_constant(&mut self, value: BabyBearExt4) -> ReducedBabyBearExt4Wire {
251        let (ext, ctx) = self.ext_parts();
252        ext.load_reduced_constant(ctx, value)
253    }
254
255    fn ext_add(&mut self, a: BabyBearExt4Wire, b: BabyBearExt4Wire) -> BabyBearExt4Wire {
256        let (ext, ctx) = self.ext_parts();
257        ext.add(ctx, a, b)
258    }
259
260    fn ext_neg(&mut self, a: BabyBearExt4Wire) -> BabyBearExt4Wire {
261        let (ext, ctx) = self.ext_parts();
262        ext.neg(ctx, a)
263    }
264
265    fn ext_sub(&mut self, a: BabyBearExt4Wire, b: BabyBearExt4Wire) -> BabyBearExt4Wire {
266        let (ext, ctx) = self.ext_parts();
267        ext.sub(ctx, a, b)
268    }
269
270    fn ext_scalar_mul(&mut self, a: BabyBearExt4Wire, b: BabyBearWire) -> BabyBearExt4Wire {
271        let (ext, ctx) = self.ext_parts();
272        ext.scalar_mul(ctx, a, b)
273    }
274
275    fn ext_scalar_mul_add(
276        &mut self,
277        a: BabyBearExt4Wire,
278        b: BabyBearWire,
279        c: BabyBearExt4Wire,
280    ) -> BabyBearExt4Wire {
281        let (ext, ctx) = self.ext_parts();
282        ext.scalar_mul_add(ctx, a, b, c)
283    }
284
285    fn ext_assert_zero(&mut self, a: BabyBearExt4Wire) {
286        let (ext, ctx) = self.ext_parts();
287        ext.assert_zero(ctx, a)
288    }
289
290    fn ext_assert_equal(&mut self, a: BabyBearExt4Wire, b: BabyBearExt4Wire) {
291        let (ext, ctx) = self.ext_parts();
292        ext.assert_equal(ctx, a, b)
293    }
294
295    fn ext_mul(&mut self, a: BabyBearExt4Wire, b: BabyBearExt4Wire) -> BabyBearExt4Wire {
296        let (ext, ctx) = self.ext_parts();
297        ext.mul(ctx, a, b)
298    }
299
300    fn ext_div(&mut self, a: BabyBearExt4Wire, b: BabyBearExt4Wire) -> BabyBearExt4Wire {
301        let (ext, ctx) = self.ext_parts();
302        ext.div(ctx, a, b)
303    }
304
305    fn ext_reduce_max_bits(&mut self, a: BabyBearExt4Wire) -> BabyBearExt4Wire {
306        let (ext, ctx) = self.ext_parts();
307        ext.reduce_max_bits(ctx, a)
308    }
309
310    fn ext_zero(&mut self) -> BabyBearExt4Wire {
311        let (ext, ctx) = self.ext_parts();
312        ext.zero(ctx)
313    }
314
315    fn ext_from_base_const(&mut self, value: BabyBear) -> BabyBearExt4Wire {
316        let (ext, ctx) = self.ext_parts();
317        ext.from_base_const(ctx, value)
318    }
319
320    fn ext_from_base_var(&mut self, value: BabyBearWire) -> BabyBearExt4Wire {
321        let (ext, ctx) = self.ext_parts();
322        ext.from_base_var(ctx, value)
323    }
324
325    fn ext_mul_base_const(&mut self, a: BabyBearExt4Wire, c: BabyBear) -> BabyBearExt4Wire {
326        let (ext, ctx) = self.ext_parts();
327        ext.mul_base_const(ctx, a, c)
328    }
329
330    fn ext_square(&mut self, a: BabyBearExt4Wire) -> BabyBearExt4Wire {
331        let (ext, ctx) = self.ext_parts();
332        ext.square(ctx, a)
333    }
334
335    fn ext_pow_power_of_two(&mut self, a: BabyBearExt4Wire, n: usize) -> BabyBearExt4Wire {
336        let (ext, ctx) = self.ext_parts();
337        ext.pow_power_of_two(ctx, a, n)
338    }
339}
340
341impl Poseidon2Inst for Halo2Backend<'_> {
342    fn hash_babybear_slice_to_digest(
343        &mut self,
344        values: &[ReducedBabyBearWire],
345    ) -> AssignedValue<Fr> {
346        let (bb, ctx) = self.bb_parts();
347        hash_babybear_slice_to_digest(ctx, bb.range(), values)
348    }
349
350    fn compress_digests(
351        &mut self,
352        left: AssignedValue<Fr>,
353        right: AssignedValue<Fr>,
354    ) -> AssignedValue<Fr> {
355        let (bb, ctx) = self.bb_parts();
356        compress_bn254_digests(ctx, bb.range(), left, right)
357    }
358}
359
360impl TranscriptInst for Halo2Backend<'_> {
361    fn init_transcript(&mut self) {
362        self.transcript = Some(TranscriptChip::new(self.ctx, self.ext.base().clone()));
363    }
364
365    fn observe(&mut self, value: &ReducedBabyBearWire) {
366        let (transcript, ctx) = self.transcript_parts();
367        transcript.observe(ctx, value)
368    }
369
370    fn observe_ext(&mut self, value: &ReducedBabyBearExt4Wire) {
371        let (transcript, ctx) = self.transcript_parts();
372        transcript.observe_ext(ctx, value)
373    }
374
375    fn observe_commit(&mut self, digest: &DigestWire) {
376        let (transcript, ctx) = self.transcript_parts();
377        transcript.observe_commit(ctx, digest)
378    }
379
380    fn sample(&mut self) -> BabyBearWire {
381        let (transcript, ctx) = self.transcript_parts();
382        transcript.sample(ctx)
383    }
384
385    fn sample_ext(&mut self) -> BabyBearExt4Wire {
386        let (transcript, ctx) = self.transcript_parts();
387        transcript.sample_ext(ctx)
388    }
389
390    fn sample_bits(&mut self, bits: usize) -> AssignedValue<Fr> {
391        let (transcript, ctx) = self.transcript_parts();
392        transcript.sample_bits(ctx, bits)
393    }
394
395    fn check_witness(&mut self, bits: usize, witness: &ReducedBabyBearWire) {
396        let (transcript, ctx) = self.transcript_parts();
397        transcript.check_witness(ctx, bits, witness)
398    }
399
400    fn transcript_load_reduced_constant(
401        &mut self,
402        value: BabyBear,
403    ) -> ReducedBabyBearWire<Self::F> {
404        let (transcript, ctx) = self.transcript_parts();
405        transcript.baby_bear().load_reduced_constant(ctx, value)
406    }
407}
openvm_static_verifier/backend.rs

openvm_static_verifier/
backend.rs
