Skip to content

Commit

Permalink
Fix second stage witgen (#2173)
Browse files Browse the repository at this point in the history
Builds on #2169

With this PR, second-stage witness generation works for the bus used in
the RISC-V machine 🎉

This is an end-to-end test:
```bash
cargo run -r --bin powdr-rs compile riscv/tests/riscv_data/sum-o output --max-degree-log 15 --field gl
cargo run -r pil output/sum.asm -o output -f --field gl --prove-with mock --linker-mode bus -i 1,1,1
```

What's needed is two small changes to `VmProcessor`:
- The degree is now passed by the caller (`DynamicMachine` or
`SecondStageMachine`). That way, `SecondStageMachine` can set it to the
actual final size, instead of the maximum allowed degree.
- I disabled loop detection for second-stage witness generation for now.
  • Loading branch information
georgwiese authored Nov 29, 2024
1 parent 8c3f478 commit 2832ff1
Show file tree
Hide file tree
Showing 4 changed files with 34 additions and 5 deletions.
2 changes: 2 additions & 0 deletions executor/src/witgen/machines/dynamic_machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -230,6 +230,8 @@ impl<'a, T: FieldElement> DynamicMachine<'a, T> {
&self.parts,
SolverState::new(data, self.publics.clone()),
mutable_state,
self.degree,
true,
);
if let Some(outer_query) = outer_query {
processor = processor.with_outer_query(outer_query);
Expand Down
14 changes: 13 additions & 1 deletion executor/src/witgen/machines/second_stage_machine.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
use itertools::Itertools;
use powdr_ast::analyzed::Identity;
use powdr_number::{DegreeType, FieldElement};
use std::collections::{BTreeMap, HashMap};
Expand Down Expand Up @@ -82,8 +83,17 @@ impl<'a, T: FieldElement> SecondStageMachine<'a, T> {
parts.prover_functions,
);

let witness_sizes = fixed_data
.witness_cols
.values()
.filter_map(|w| w.external_values.as_ref())
.map(|values| values.len())
.unique()
.collect::<Vec<_>>();
let degree = witness_sizes.into_iter().exactly_one().unwrap() as DegreeType;

Self {
degree: parts.common_degree_range().max,
degree,
name,
fixed_data,
parts,
Expand Down Expand Up @@ -159,6 +169,8 @@ impl<'a, T: FieldElement> SecondStageMachine<'a, T> {
&self.parts,
SolverState::new(data, self.publics.clone()),
mutable_state,
self.degree,
false,
);
processor.run(true);
let (updated_data, degree) = processor.finish();
Expand Down
9 changes: 8 additions & 1 deletion executor/src/witgen/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -570,7 +570,14 @@ impl<'a, T> FixedColumn<'a, T> {
}

pub fn values(&self, size: DegreeType) -> &[T] {
self.values.get_by_size(size).unwrap()
self.values.get_by_size(size).unwrap_or_else(|| {
panic!(
"Fixed column {} does not have a value for size {}. Available sizes: {:?}",
self.name,
size,
self.values.available_sizes()
)
})
}

pub fn values_max_size(&self) -> &[T] {
Expand Down
14 changes: 11 additions & 3 deletions executor/src/witgen/vm_processor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,9 @@ pub struct VmProcessor<'a, 'c, T: FieldElement, Q: QueryCallback<T>> {
last_report_time: Instant,
processor: Processor<'a, 'c, T, Q>,
progress_bar: ProgressBar,
/// If true, we'll periodically check if we are in a loop. If yes, we'll add new rows by
/// copying the old ones and check the constraints.
loop_detection: bool,
}

impl<'a, 'c, T: FieldElement, Q: QueryCallback<T>> VmProcessor<'a, 'c, T, Q> {
Expand All @@ -79,11 +82,11 @@ impl<'a, 'c, T: FieldElement, Q: QueryCallback<T>> VmProcessor<'a, 'c, T, Q> {
parts: &'c MachineParts<'a, T>,
mutable_data: SolverState<'a, T>,
mutable_state: &'c MutableState<'a, T, Q>,
degree: DegreeType,
loop_detection: bool,
) -> Self {
let degree_range = parts.common_degree_range();

let degree = degree_range.max;

let (identities_with_next, identities_without_next): (Vec<_>, Vec<_>) = parts
.identities
.iter()
Expand Down Expand Up @@ -118,6 +121,7 @@ impl<'a, 'c, T: FieldElement, Q: QueryCallback<T>> VmProcessor<'a, 'c, T, Q> {
last_report_time: Instant::now(),
processor,
progress_bar,
loop_detection,
}
}

Expand Down Expand Up @@ -181,7 +185,11 @@ impl<'a, 'c, T: FieldElement, Q: QueryCallback<T>> VmProcessor<'a, 'c, T, Q> {
}

// Check if we are in a loop.
if looping_period.is_none() && row_index % 100 == 0 && row_index > 0 {
if looping_period.is_none()
&& row_index % 100 == 0
&& row_index > 0
&& self.loop_detection
{
looping_period = self.rows_are_repeating(row_index);
if let Some(p) = looping_period {
log::log!(
Expand Down

0 comments on commit 2832ff1

Please sign in to comment.