Skip to content

Commit 03690de

Browse files
author
Aurélien Nicolas
committed
bus-auto: add query_advice and query_fixed function in witness generation
1 parent e7fde0b commit 03690de

File tree

9 files changed

+174
-1
lines changed

9 files changed

+174
-1
lines changed

‎halo2_proofs/src/circuit.rs

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -221,6 +221,16 @@ impl<'r, F: Field> Region<'r, F> {
221221
.name_column(&|| annotation().into(), column.into());
222222
}
223223

224+
/// Get the last assigned value of an advice cell.
225+
pub fn query_advice(&self, column: Column<Advice>, offset: usize) -> Result<F, Error> {
226+
self.region.query_advice(column, offset)
227+
}
228+
229+
/// Get the last assigned value of a fixed cell.
230+
pub fn query_fixed(&self, column: Column<Fixed>, offset: usize) -> Result<F, Error> {
231+
self.region.query_fixed(column, offset)
232+
}
233+
224234
/// Assign an advice column value (witness).
225235
///
226236
/// Even though `to` has `FnMut` bounds, it is guaranteed to be called at most once.
@@ -368,6 +378,7 @@ impl<'r, F: Field> Region<'r, F> {
368378
self.region.constrain_equal(left, right)
369379
}
370380

381+
/// Return the offset of a row within the overall circuit.
371382
pub fn global_offset(&self, row_offset: usize) -> usize {
372383
self.region.global_offset(row_offset)
373384
}

‎halo2_proofs/src/circuit/floor_planner/single_pass.rs

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -489,6 +489,20 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F>
489489
self.layouter.cs.annotate_column(annotation, column);
490490
}
491491

492+
fn query_advice(&self, column: Column<Advice>, offset: usize) -> Result<F, Error> {
493+
self.layouter.cs.query_advice(
494+
column,
495+
*self.layouter.regions[*self.region_index] + offset,
496+
)
497+
}
498+
499+
fn query_fixed(&self, column: Column<Fixed>, offset: usize) -> Result<F, Error> {
500+
self.layouter.cs.query_fixed(
501+
column,
502+
*self.layouter.regions[*self.region_index] + offset,
503+
)
504+
}
505+
492506
fn assign_advice<'v>(
493507
&'v mut self,
494508
annotation: &'v (dyn Fn() -> String + 'v),

‎halo2_proofs/src/circuit/floor_planner/v1.rs

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -427,6 +427,18 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F> for V1Region<'r
427427
)
428428
}
429429

430+
fn query_advice(&self, column: Column<Advice>, offset: usize) -> Result<F, Error> {
431+
self.plan
432+
.cs
433+
.query_advice(column, *self.plan.regions[*self.region_index] + offset)
434+
}
435+
436+
fn query_fixed(&self, column: Column<Fixed>, offset: usize) -> Result<F, Error> {
437+
self.plan
438+
.cs
439+
.query_fixed(column, *self.plan.regions[*self.region_index] + offset)
440+
}
441+
430442
fn assign_advice<'v>(
431443
&'v mut self,
432444
annotation: &'v (dyn Fn() -> String + 'v),

‎halo2_proofs/src/circuit/layouter.rs

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,12 @@ pub trait RegionLayouter<F: Field>: fmt::Debug {
5858
column: Column<Any>,
5959
);
6060

61+
/// Get the last assigned value of an advice cell.
62+
fn query_advice(&self, column: Column<Advice>, offset: usize) -> Result<F, Error>;
63+
64+
/// Get the last assigned value of a fixed cell.
65+
fn query_fixed(&self, column: Column<Fixed>, offset: usize) -> Result<F, Error>;
66+
6167
/// Assign an advice column value (witness)
6268
fn assign_advice<'v>(
6369
&'v mut self,
@@ -222,6 +228,14 @@ impl<F: Field> RegionLayouter<F> for RegionShape {
222228
Ok(())
223229
}
224230

231+
fn query_advice(&self, column: Column<Advice>, offset: usize) -> Result<F, Error> {
232+
Ok(F::zero())
233+
}
234+
235+
fn query_fixed(&self, column: Column<Fixed>, offset: usize) -> Result<F, Error> {
236+
Ok(F::zero())
237+
}
238+
225239
fn assign_advice<'v>(
226240
&'v mut self,
227241
_: &'v (dyn Fn() -> String + 'v),

‎halo2_proofs/src/dev.rs

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -651,6 +651,56 @@ impl<'a, F: Field + Group> Assignment<F> for MockProver<'a, F> {
651651
Ok(())
652652
}
653653

654+
fn query_advice(&self, column: Column<Advice>, row: usize) -> Result<F, Error> {
655+
if !self.usable_rows.contains(&row) {
656+
return Err(Error::not_enough_rows_available(self.k));
657+
}
658+
if !self.rw_rows.contains(&row) {
659+
return Err(Error::InvalidRange(
660+
row,
661+
self.current_region
662+
.as_ref()
663+
.map(|region| region.name.clone())
664+
.unwrap(),
665+
));
666+
}
667+
self.advice
668+
.get(column.index())
669+
.and_then(|v| v.get(row - self.rw_rows.start))
670+
.map(|v| match v {
671+
CellValue::Assigned(f) => *f,
672+
#[cfg(feature = "mock-batch-inv")]
673+
CellValue::Rational(n, d) => n * d.invert().unwrap_or_default(),
674+
_ => F::zero(),
675+
})
676+
.ok_or(Error::BoundsFailure)
677+
}
678+
679+
fn query_fixed(&self, column: Column<Fixed>, row: usize) -> Result<F, Error> {
680+
if !self.usable_rows.contains(&row) {
681+
return Err(Error::not_enough_rows_available(self.k));
682+
}
683+
if !self.rw_rows.contains(&row) {
684+
return Err(Error::InvalidRange(
685+
row,
686+
self.current_region
687+
.as_ref()
688+
.map(|region| region.name.clone())
689+
.unwrap(),
690+
));
691+
}
692+
self.fixed
693+
.get(column.index())
694+
.and_then(|v| v.get(row - self.rw_rows.start))
695+
.map(|v| match v {
696+
CellValue::Assigned(f) => *f,
697+
#[cfg(feature = "mock-batch-inv")]
698+
CellValue::Rational(n, d) => n * d.invert().unwrap_or_default(),
699+
_ => F::zero(),
700+
})
701+
.ok_or(Error::BoundsFailure)
702+
}
703+
654704
fn query_instance(
655705
&self,
656706
column: Column<Instance>,

‎halo2_proofs/src/dev/cost.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,14 @@ impl<F: Field> Assignment<F> for Assembly {
7878
todo!()
7979
}
8080

81+
fn query_advice(&self, column: Column<Advice>, row: usize) -> Result<F, Error> {
82+
Ok(F::zero())
83+
}
84+
85+
fn query_fixed(&self, column: Column<Fixed>, row: usize) -> Result<F, Error> {
86+
Ok(F::zero())
87+
}
88+
8189
fn query_instance(&self, _: Column<Instance>, _: usize) -> Result<Value<F>, Error> {
8290
Ok(Value::unknown())
8391
}

‎halo2_proofs/src/plonk/circuit.rs

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,6 @@ pub struct Column<C: ColumnType> {
3232
}
3333

3434
impl<C: ColumnType> Column<C> {
35-
#[cfg(test)]
3635
pub(crate) fn new(index: usize, column_type: C) -> Self {
3736
Column { index, column_type }
3837
}
@@ -409,6 +408,10 @@ impl FixedQuery {
409408
pub fn column_index(&self) -> usize {
410409
self.column_index
411410
}
411+
/// Column
412+
pub fn column(&self) -> Column<Fixed> {
413+
Column::new(self.column_index, Fixed)
414+
}
412415

413416
/// Rotation of this query
414417
pub fn rotation(&self) -> Rotation {
@@ -438,6 +441,10 @@ impl AdviceQuery {
438441
pub fn column_index(&self) -> usize {
439442
self.column_index
440443
}
444+
/// Column
445+
pub fn column(&self) -> Column<Advice> {
446+
Column::new(self.column_index, Advice { phase: self.phase })
447+
}
441448

442449
/// Rotation of this query
443450
pub fn rotation(&self) -> Rotation {
@@ -577,6 +584,12 @@ pub trait Assignment<F: Field>: Sized + Send {
577584
unimplemented!("merge is not implemented by default")
578585
}
579586

587+
/// Get the last assigned value of an advice cell.
588+
fn query_advice(&self, column: Column<Advice>, row: usize) -> Result<F, Error>;
589+
590+
/// Get the last assigned value of a fixed cell.
591+
fn query_fixed(&self, column: Column<Fixed>, row: usize) -> Result<F, Error>;
592+
580593
/// Queries the cell of an instance column at a particular absolute row.
581594
///
582595
/// Returns the cell's value, if known.

‎halo2_proofs/src/plonk/keygen.rs

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -186,6 +186,26 @@ impl<'a, F: Field> Assignment<F> for Assembly<'a, F> {
186186
Ok(())
187187
}
188188

189+
fn query_advice(&self, _column: Column<Advice>, _row: usize) -> Result<F, Error> {
190+
// We only care about fixed columns here
191+
Ok(F::zero())
192+
}
193+
194+
fn query_fixed(&self, column: Column<Fixed>, row: usize) -> Result<F, Error> {
195+
if !self.usable_rows.contains(&row) {
196+
return Err(Error::not_enough_rows_available(self.k));
197+
}
198+
if !self.rw_rows.contains(&row) {
199+
log::error!("query_fixed: {:?}, row: {}", column, row);
200+
return Err(Error::Synthesis);
201+
}
202+
self.fixed
203+
.get(column.index())
204+
.and_then(|v| v.get(row - self.rw_rows.start))
205+
.map(|v| v.evaluate())
206+
.ok_or(Error::BoundsFailure)
207+
}
208+
189209
fn query_instance(&self, _: Column<Instance>, row: usize) -> Result<Value<F>, Error> {
190210
if !self.usable_rows.contains(&row) {
191211
return Err(Error::not_enough_rows_available(self.k));

‎halo2_proofs/src/plonk/prover.rs

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -146,6 +146,7 @@ pub fn create_proof<
146146
advice: Vec<&'a mut [Assigned<F>]>,
147147
challenges: &'a HashMap<usize, F>,
148148
instances: &'a [&'a [F]],
149+
fixed_values: &'a [Polynomial<F, LagrangeCoeff>],
149150
rw_rows: Range<usize>,
150151
usable_rows: RangeTo<usize>,
151152
_marker: std::marker::PhantomData<F>,
@@ -229,6 +230,7 @@ pub fn create_proof<
229230
advice,
230231
challenges: self.challenges,
231232
instances: self.instances,
233+
fixed_values: self.fixed_values.clone(),
232234
rw_rows: sub_range.clone(),
233235
usable_rows: self.usable_rows,
234236
_marker: Default::default(),
@@ -250,6 +252,34 @@ pub fn create_proof<
250252
// Do nothing
251253
}
252254

255+
/// Get the last assigned value of a cell.
256+
fn query_advice(&self, column: Column<Advice>, row: usize) -> Result<F, Error> {
257+
if !self.usable_rows.contains(&row) {
258+
return Err(Error::not_enough_rows_available(self.k));
259+
}
260+
if !self.rw_rows.contains(&row) {
261+
log::error!("query_advice: {:?}, row: {}", column, row);
262+
return Err(Error::Synthesis);
263+
}
264+
self.advice
265+
.get(column.index())
266+
.and_then(|v| v.get(row - self.rw_rows.start))
267+
.map(|v| v.evaluate())
268+
.ok_or(Error::BoundsFailure)
269+
}
270+
271+
fn query_fixed(
272+
&self,
273+
column: Column<Fixed>,
274+
row: usize,
275+
) -> Result<F, Error> {
276+
self.fixed_values
277+
.get(column.index())
278+
.and_then(|v| v.get(row))
279+
.map(|v| *v)
280+
.ok_or(Error::BoundsFailure)
281+
}
282+
253283
fn query_instance(&self, column: Column<Instance>, row: usize) -> Result<Value<F>, Error> {
254284
if !self.usable_rows.contains(&row) {
255285
return Err(Error::not_enough_rows_available(self.k));
@@ -403,6 +433,7 @@ pub fn create_proof<
403433
advice_vec,
404434
advice: advice_slice,
405435
instances,
436+
fixed_values: &pk.fixed_values,
406437
challenges: &challenges,
407438
// The prover will not be allowed to assign values to advice
408439
// cells that exist within inactive rows, which include some

0 commit comments

Comments
 (0)