openvm_static_verifier/
chip_traits.rs

1//! Backend abstraction traits for circuit construction.
2//!
3//! Each trait mirrors one concrete chip used by the static verifier:
4//! [`GateInst`] ↔ `GateChip` (plus raw `Context` cell operations), [`BabyBearInst`] ↔
5//! `BabyBearChip`, [`BabyBearExt4Inst`] ↔ `BabyBearExt4Chip`, [`TranscriptInst`] ↔
6//! `TranscriptChip`, and [`Poseidon2Inst`] ↔ the Poseidon2 digest hashing helpers.
7//! [`PopulateInputs`] is the exception: it groups the witness-loading methods used by
8//! `load_proof_wire` and inherits only from [`ChipBase`].
9//!
10//! Circuit-construction code is generic over a single backend object `B` bounded by the
11//! traits it needs, e.g. `B: TranscriptInst + GateInst`. All chip traits inherit their
12//! associated types from [`ChipBase`], so `B::F` (the wire/value representation
13//! abstracting `AssignedValue<Fr>`) is unambiguous and never needs to be repeated
14//! per-trait in bounds. Backends own their circuit-building context (e.g. a
15//! `&mut halo2_base::Context<Fr>` for the halo2 backend, or an IR builder).
16//!
17//! Trait methods never inspect `B::F` values on the host; all nondeterminism (witness
18//! loading, inversions, decompositions) lives inside backend implementations.
19
20use core::fmt::Debug;
21
22use halo2_base::halo2_proofs::halo2curves::bn256::Fr;
23use openvm_stark_sdk::p3_baby_bear::BabyBear;
24
25use crate::{
26    field::baby_bear::{
27        BabyBearExt4, BabyBearExt4Wire, BabyBearWire, ReducedBabyBearExt4Wire, ReducedBabyBearWire,
28    },
29    transcript::DigestWire,
30};
31
32/// Associated types shared by all chip traits.
33pub trait ChipBase {
34    /// Wire/value representation abstracting `AssignedValue<Fr>`.
35    type F: Copy + Debug;
36}
37
38/// Witness-loading operations needed to populate proof input wires
39/// (see `stages::full_pipeline::load_proof_wire`).
40pub trait PopulateInputs: ChipBase {
41    fn load_witness(&mut self, value: Fr) -> Self::F;
42    fn bb_load_reduced_witness(&mut self, value: BabyBear) -> ReducedBabyBearWire<Self::F>;
43    fn ext_load_reduced_witness(&mut self, value: BabyBearExt4)
44        -> ReducedBabyBearExt4Wire<Self::F>;
45}
46
47/// Raw `Fr`-cell operations mirroring `GateChip` and direct `Context` usage.
48pub trait GateInst: ChipBase {
49    fn load_constant(&mut self, value: Fr) -> Self::F;
50    fn constrain_equal(&mut self, a: Self::F, b: Self::F);
51    /// `if cond { when_true } else { when_false }`; `cond` must already be boolean-constrained.
52    fn select(&mut self, when_true: Self::F, when_false: Self::F, cond: Self::F) -> Self::F;
53    /// [`Self::select`] with constant branch values.
54    fn select_const(&mut self, when_true: Fr, when_false: Fr, cond: Self::F) -> Self::F;
55    /// Little-endian bit decomposition, constrained to `range_bits` bits.
56    fn num_to_bits(&mut self, a: Self::F, range_bits: usize) -> Vec<Self::F>;
57    /// Inner product of `values` with constant coefficients.
58    fn inner_product_const(&mut self, values: &[Self::F], coeffs: &[Fr]) -> Self::F;
59    /// Number of cells assigned so far (for cell profiling).
60    fn cell_count(&self) -> usize;
61}
62
63/// BabyBear base-field operations mirroring `BabyBearChip`.
64pub trait BabyBearInst: GateInst {
65    fn bb_load_constant(&mut self, value: BabyBear) -> BabyBearWire<Self::F>;
66    fn bb_load_reduced_constant(&mut self, value: BabyBear) -> ReducedBabyBearWire<Self::F>;
67    fn bb_reduce(&mut self, a: BabyBearWire<Self::F>) -> BabyBearWire<Self::F>;
68    fn bb_reduce_max_bits(&mut self, a: BabyBearWire<Self::F>) -> BabyBearWire<Self::F>;
69    fn bb_add(
70        &mut self,
71        a: BabyBearWire<Self::F>,
72        b: BabyBearWire<Self::F>,
73    ) -> BabyBearWire<Self::F>;
74    fn bb_neg(&mut self, a: BabyBearWire<Self::F>) -> BabyBearWire<Self::F>;
75    fn bb_sub(
76        &mut self,
77        a: BabyBearWire<Self::F>,
78        b: BabyBearWire<Self::F>,
79    ) -> BabyBearWire<Self::F>;
80    fn bb_mul(
81        &mut self,
82        a: BabyBearWire<Self::F>,
83        b: BabyBearWire<Self::F>,
84    ) -> BabyBearWire<Self::F>;
85    /// `a * b + c`
86    fn bb_mul_add(
87        &mut self,
88        a: BabyBearWire<Self::F>,
89        b: BabyBearWire<Self::F>,
90        c: BabyBearWire<Self::F>,
91    ) -> BabyBearWire<Self::F>;
92    fn bb_div(
93        &mut self,
94        a: BabyBearWire<Self::F>,
95        b: BabyBearWire<Self::F>,
96    ) -> BabyBearWire<Self::F>;
97    fn bb_assert_zero(&mut self, a: BabyBearWire<Self::F>);
98    fn bb_assert_equal(&mut self, a: BabyBearWire<Self::F>, b: BabyBearWire<Self::F>);
99    fn bb_zero(&mut self) -> BabyBearWire<Self::F>;
100    fn bb_one(&mut self) -> BabyBearWire<Self::F>;
101    fn bb_mul_const(&mut self, a: BabyBearWire<Self::F>, c: BabyBear) -> BabyBearWire<Self::F>;
102    fn bb_square(&mut self, a: BabyBearWire<Self::F>) -> BabyBearWire<Self::F>;
103    /// `a^(2^n)`
104    fn bb_pow_power_of_two(&mut self, a: BabyBearWire<Self::F>, n: usize) -> BabyBearWire<Self::F>;
105}
106
107/// BabyBear quartic-extension operations mirroring `BabyBearExt4Chip`.
108pub trait BabyBearExt4Inst: BabyBearInst {
109    fn ext_load_constant(&mut self, value: BabyBearExt4) -> BabyBearExt4Wire<Self::F>;
110    fn ext_load_reduced_constant(
111        &mut self,
112        value: BabyBearExt4,
113    ) -> ReducedBabyBearExt4Wire<Self::F>;
114    fn ext_add(
115        &mut self,
116        a: BabyBearExt4Wire<Self::F>,
117        b: BabyBearExt4Wire<Self::F>,
118    ) -> BabyBearExt4Wire<Self::F>;
119    fn ext_neg(&mut self, a: BabyBearExt4Wire<Self::F>) -> BabyBearExt4Wire<Self::F>;
120    fn ext_sub(
121        &mut self,
122        a: BabyBearExt4Wire<Self::F>,
123        b: BabyBearExt4Wire<Self::F>,
124    ) -> BabyBearExt4Wire<Self::F>;
125    fn ext_scalar_mul(
126        &mut self,
127        a: BabyBearExt4Wire<Self::F>,
128        b: BabyBearWire<Self::F>,
129    ) -> BabyBearExt4Wire<Self::F>;
130    /// `a * b + c` where `b` is a base-field scalar.
131    fn ext_scalar_mul_add(
132        &mut self,
133        a: BabyBearExt4Wire<Self::F>,
134        b: BabyBearWire<Self::F>,
135        c: BabyBearExt4Wire<Self::F>,
136    ) -> BabyBearExt4Wire<Self::F>;
137    fn ext_assert_zero(&mut self, a: BabyBearExt4Wire<Self::F>);
138    fn ext_assert_equal(&mut self, a: BabyBearExt4Wire<Self::F>, b: BabyBearExt4Wire<Self::F>);
139    fn ext_mul(
140        &mut self,
141        a: BabyBearExt4Wire<Self::F>,
142        b: BabyBearExt4Wire<Self::F>,
143    ) -> BabyBearExt4Wire<Self::F>;
144    fn ext_div(
145        &mut self,
146        a: BabyBearExt4Wire<Self::F>,
147        b: BabyBearExt4Wire<Self::F>,
148    ) -> BabyBearExt4Wire<Self::F>;
149    fn ext_reduce_max_bits(&mut self, a: BabyBearExt4Wire<Self::F>) -> BabyBearExt4Wire<Self::F>;
150    fn ext_zero(&mut self) -> BabyBearExt4Wire<Self::F>;
151    fn ext_from_base_const(&mut self, value: BabyBear) -> BabyBearExt4Wire<Self::F>;
152    fn ext_from_base_var(&mut self, value: BabyBearWire<Self::F>) -> BabyBearExt4Wire<Self::F>;
153    fn ext_mul_base_const(
154        &mut self,
155        a: BabyBearExt4Wire<Self::F>,
156        c: BabyBear,
157    ) -> BabyBearExt4Wire<Self::F>;
158    fn ext_square(&mut self, a: BabyBearExt4Wire<Self::F>) -> BabyBearExt4Wire<Self::F>;
159    /// `a^(2^n)`
160    fn ext_pow_power_of_two(
161        &mut self,
162        a: BabyBearExt4Wire<Self::F>,
163        n: usize,
164    ) -> BabyBearExt4Wire<Self::F>;
165}
166
167/// Poseidon2 digest hashing/compression mirroring the helpers in `hash::poseidon2`.
168pub trait Poseidon2Inst: ChipBase {
169    /// Hash a slice of reduced BabyBear wires into a single Bn254 digest cell.
170    fn hash_babybear_slice_to_digest(&mut self, values: &[ReducedBabyBearWire<Self::F>])
171        -> Self::F;
172    /// Two-to-one Poseidon2 digest compression (Merkle node).
173    fn compress_digests(&mut self, left: Self::F, right: Self::F) -> Self::F;
174}
175
176/// Stateful Fiat–Shamir transcript mirroring `TranscriptChip`.
177pub trait TranscriptInst: BabyBearExt4Inst {
178    /// (Re)initialize the transcript sponge to the all-zero state.
179    fn init_transcript(&mut self);
180    fn observe(&mut self, value: &ReducedBabyBearWire<Self::F>);
181    fn observe_ext(&mut self, value: &ReducedBabyBearExt4Wire<Self::F>);
182    fn observe_commit(&mut self, digest: &DigestWire<Self::F>);
183    fn sample(&mut self) -> BabyBearWire<Self::F>;
184    fn sample_ext(&mut self) -> BabyBearExt4Wire<Self::F>;
185    /// Sample and truncate to `bits` bits; returns a raw cell in `[0, 2^bits)`.
186    fn sample_bits(&mut self, bits: usize) -> Self::F;
187    /// Asserts that the proof-of-work `witness` passes with `bits` leading zero bits.
188    fn check_witness(&mut self, bits: usize, witness: &ReducedBabyBearWire<Self::F>);
189
190    /// Load a reduced constant through `TranscriptChip`'s baby-bear constant
191    /// cache, which is distinct from `BabyBearChip::const_cache`. This split
192    /// is preserved to keep the verifying key unchanged.
193    fn transcript_load_reduced_constant(&mut self, value: BabyBear)
194        -> ReducedBabyBearWire<Self::F>;
195}
openvm_static_verifier/chip_traits.rs

openvm_static_verifier/
chip_traits.rs
