Skip to content

Commit

Permalink
VM-to-VM Witness Generation
Browse files Browse the repository at this point in the history
  • Loading branch information
georgwiese committed Nov 2, 2023
1 parent e70b9b7 commit ec8c994
Show file tree
Hide file tree
Showing 17 changed files with 660 additions and 168 deletions.
28 changes: 27 additions & 1 deletion compiler/tests/asm.rs
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,6 @@ fn vm_to_block_multiple_interfaces() {
}

#[test]
#[should_panic = "not implemented"]
fn vm_to_vm() {
let f = "vm_to_vm.asm";
let i = [];
Expand All @@ -174,6 +173,33 @@ fn vm_to_vm() {
gen_estark_proof(f, slice_to_vec(&i));
}

#[test]
fn vm_to_vm_dynamic_trace_length() {
let f = "vm_to_vm_dynamic_trace_length.asm";
let i = [];
verify_asm::<GoldilocksField>(f, slice_to_vec(&i));
gen_halo2_proof(f, slice_to_vec(&i));
gen_estark_proof(f, slice_to_vec(&i));
}

#[test]
fn vm_to_vm_to_block() {
let f = "vm_to_vm_to_block.asm";
let i = [];
verify_asm::<GoldilocksField>(f, slice_to_vec(&i));
gen_halo2_proof(f, slice_to_vec(&i));
gen_estark_proof(f, slice_to_vec(&i));
}

#[test]
fn vm_to_vm_to_vm() {
let f = "vm_to_vm_to_vm.asm";
let i = [];
verify_asm::<GoldilocksField>(f, slice_to_vec(&i));
gen_halo2_proof(f, slice_to_vec(&i));
gen_estark_proof(f, slice_to_vec(&i));
}

#[test]
fn test_mem_read_write() {
let f = "mem_read_write.asm";
Expand Down
13 changes: 7 additions & 6 deletions compiler/tests/pil.rs
Original file line number Diff line number Diff line change
Expand Up @@ -221,12 +221,13 @@ fn test_single_line_blocks() {
gen_estark_proof(f, Default::default());
}

#[test]
fn test_two_block_machine_functions() {
let f = "two_block_machine_functions.pil";
verify_pil(f, None);
gen_estark_proof(f, Default::default());
}
// TODO: Add back once #693 is merged
// #[test]
// fn test_two_block_machine_functions() {
// let f = "two_block_machine_functions.pil";
// verify_pil(f, None);
// gen_estark_proof(f, Default::default());
// }

#[test]
fn test_fixed_columns() {
Expand Down
10 changes: 7 additions & 3 deletions executor/src/witgen/block_processor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -27,15 +27,19 @@ pub struct WithoutCalldata;
pub struct OuterQuery<'a, T: FieldElement> {
/// A local copy of the left-hand side of the outer query.
/// This will be mutated while processing the block.
left: Left<'a, T>,
pub left: Left<'a, T>,
/// The right-hand side of the outer query.
right: &'a SelectedExpressions<Expression<T>>,
pub right: &'a SelectedExpressions<Expression<T>>,
}

impl<'a, T: FieldElement> OuterQuery<'a, T> {
pub fn new(left: Left<'a, T>, right: &'a SelectedExpressions<Expression<T>>) -> Self {
Self { left, right }
}

pub fn is_complete(&self) -> bool {
self.left.iter().all(|l| l.is_constant())
}
}

/// A basic processor that knows how to determine a unique satisfying witness
Expand Down Expand Up @@ -343,7 +347,7 @@ mod tests {
fn name_to_poly_id<T: FieldElement>(fixed_data: &FixedData<T>) -> BTreeMap<String, PolyID> {
let mut name_to_poly_id = BTreeMap::new();
for (poly_id, col) in fixed_data.witness_cols.iter() {
name_to_poly_id.insert(col.name.clone(), poly_id);
name_to_poly_id.insert(col.poly.name.clone(), poly_id);
}
for (poly_id, col) in fixed_data.fixed_cols.iter() {
name_to_poly_id.insert(col.name.clone(), poly_id);
Expand Down
12 changes: 12 additions & 0 deletions executor/src/witgen/data_structures/finalizable_data.rs
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,10 @@ impl<'a, T: FieldElement> FinalizableData<'a, T> {
self.data.len()
}

pub fn is_empty(&self) -> bool {
self.data.is_empty()
}

pub fn push(&mut self, row: Row<'a, T>) {
self.data.push(Entry::InProgress(row));
}
Expand Down Expand Up @@ -86,6 +90,14 @@ impl<'a, T: FieldElement> FinalizableData<'a, T> {
}
}

pub fn last(&self) -> Option<&Row<'a, T>> {
match self.data.last() {
Some(Entry::InProgress(row)) => Some(row),
Some(Entry::Finalized(_, _)) => panic!("Last row already finalized."),
None => None,
}
}

pub fn mutable_row_pair(&mut self, i: usize) -> (&mut Row<'a, T>, &mut Row<'a, T>) {
let (before, after) = self.data.split_at_mut(i + 1);
let current = before.last_mut().unwrap();
Expand Down
114 changes: 94 additions & 20 deletions executor/src/witgen/generator.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,18 +7,23 @@ use std::collections::{HashMap, HashSet};

use crate::witgen::data_structures::finalizable_data::FinalizableData;
use crate::witgen::rows::CellValue;
use crate::witgen::EvalValue;

use super::affine_expression::AffineExpression;
use super::block_processor::BlockProcessor;
use super::block_processor::{BlockProcessor, OuterQuery};
use super::data_structures::column_map::WitnessColumnMap;
use super::global_constraints::GlobalConstraints;
use super::machines::Machine;

use super::machines::{FixedLookup, Machine};
use super::rows::{Row, RowFactory};
use super::sequence_iterator::{DefaultSequenceIterator, ProcessingSequenceIterator};
use super::vm_processor::VmProcessor;
use super::{EvalResult, FixedData, MutableState, QueryCallback};

struct ProcessResult<'a, T: FieldElement> {
eval_value: EvalValue<&'a AlgebraicReference, T>,
block: FinalizableData<'a, T>,
}

pub struct Generator<'a, T: FieldElement> {
fixed_data: &'a FixedData<'a, T>,
identities: Vec<&'a Identity<Expression<T>>>,
Expand All @@ -31,15 +36,63 @@ pub struct Generator<'a, T: FieldElement> {
impl<'a, T: FieldElement> Machine<'a, T> for Generator<'a, T> {
fn process_plookup<Q: QueryCallback<T>>(
&mut self,
_mutable_state: &mut MutableState<'a, '_, T, Q>,
mutable_state: &mut MutableState<'a, '_, T, Q>,
_kind: IdentityKind,
_left: &[AffineExpression<&'a AlgebraicReference, T>],
_right: &'a SelectedExpressions<Expression<T>>,
left: &[AffineExpression<&'a AlgebraicReference, T>],
right: &'a SelectedExpressions<Expression<T>>,
) -> Option<EvalResult<'a, T>> {
unimplemented!()
if right.selector != self.latch {
None
} else {
log::trace!("Start processing secondary VM '{}'", self.name());
log::trace!("Arguments:");
for (r, l) in right.expressions.iter().zip(left) {
log::trace!(" {r} = {l}");
}

let first_row = self
.data
.last()
.cloned()
.unwrap_or_else(|| self.compute_partial_first_row(mutable_state));

let outer_query = OuterQuery {
left: left.to_vec(),
right,
};
let ProcessResult { eval_value, block } =
self.process(first_row, 0, mutable_state, Some(outer_query));

if eval_value.is_complete() {
log::trace!("End processing VM '{}' (successfully)", self.name());
// Remove the last row of the previous block, as it is the first row of the current
// block.
self.data.pop();
self.data.extend(block);
} else {
log::trace!("End processing VM '{}' (incomplete)", self.name());
}
Some(Ok(eval_value))
}
}

fn take_witness_col_values(&mut self) -> HashMap<String, Vec<T>> {
fn take_witness_col_values<'b, Q: QueryCallback<T>>(
&mut self,
fixed_lookup: &'b mut FixedLookup<T>,
query_callback: &'b mut Q,
) -> HashMap<String, Vec<T>> {
log::debug!("Finalizing VM: {}", self.name());

// In this stage, we don't have access to other machines, as they might already be finalized.
let mut mutable_state_no_machines = MutableState {
fixed_lookup,
machines: [].into_iter().into(),
query_callback,
};

self.fill_remaining_rows(&mut mutable_state_no_machines);
self.fix_first_row();

self.data
.take_transposed()
.map(|(id, (values, _))| (self.fixed_data.column_name(&id).to_string(), values))
Expand All @@ -66,11 +119,23 @@ impl<'a, T: FieldElement> Generator<'a, T> {
}
}

pub fn run<Q: QueryCallback<T>>(&mut self, mutable_state: &mut MutableState<'a, '_, T, Q>) {
pub fn name(&self) -> &str {
let first_witness = self.witnesses.iter().next().unwrap();
let first_witness_name = self.fixed_data.column_name(first_witness);
let namespace = first_witness_name
.rfind('.')
.map(|idx| &first_witness_name[..idx]);

// For machines compiled using Powdr ASM we'll always have a namespace, but as a last
// resort we'll use the first witness name.
namespace.unwrap_or(first_witness_name)
}

/// Runs the machine without any arguments from the first row.
pub fn run<'b, Q: QueryCallback<T>>(&mut self, mutable_state: &mut MutableState<'a, 'b, T, Q>) {
assert!(self.data.is_empty());
let first_row = self.compute_partial_first_row(mutable_state);
self.data = self.process(first_row, 0, mutable_state);
self.fill_remaining_rows(mutable_state);
self.fix_first_row();
self.data = self.process(first_row, 0, mutable_state, None).block;
}

fn fill_remaining_rows<Q>(&mut self, mutable_state: &mut MutableState<'a, '_, T, Q>)
Expand All @@ -81,9 +146,15 @@ impl<'a, T: FieldElement> Generator<'a, T> {
assert!(self.latch.is_some());

let first_row = self.data.pop().unwrap();

self.data
.extend(self.process(first_row, self.data.len() as DegreeType, mutable_state));
let ProcessResult { block, eval_value } = self.process(
first_row,
self.data.len() as DegreeType,
mutable_state,
None,
);
assert!(eval_value.is_complete());

self.data.extend(block);
}
}

Expand Down Expand Up @@ -131,7 +202,8 @@ impl<'a, T: FieldElement> Generator<'a, T> {
first_row: Row<'a, T>,
row_offset: DegreeType,
mutable_state: &mut MutableState<'a, '_, T, Q>,
) -> FinalizableData<'a, T> {
outer_query: Option<OuterQuery<'a, T>>,
) -> ProcessResult<'a, T> {
log::trace!(
"Running main machine from row {row_offset} with the following initial values in the first row:\n{}", first_row.render_values(false, None)
);
Expand All @@ -147,11 +219,13 @@ impl<'a, T: FieldElement> Generator<'a, T> {
self.witnesses.clone(),
data,
row_factory,
self.latch.clone(),
);
let result = processor.run(mutable_state);
assert!(result.is_complete(), "Main machine did not complete");
processor.finish()
if let Some(outer_query) = outer_query {
processor = processor.with_outer_query(outer_query);
}
let eval_value = processor.run(mutable_state);
let block = processor.finish();
ProcessResult { eval_value, block }
}

/// At the end of the solving algorithm, we'll have computed the first row twice
Expand Down
19 changes: 10 additions & 9 deletions executor/src/witgen/machines/block_machine.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
use std::collections::{HashMap, HashSet};

use super::{EvalResult, FixedData};
use super::{EvalResult, FixedData, FixedLookup};
use crate::witgen::affine_expression::AffineExpression;

use crate::witgen::block_processor::{BlockProcessor, OuterQuery};
Expand Down Expand Up @@ -164,7 +164,11 @@ impl<'a, T: FieldElement> Machine<'a, T> for BlockMachine<'a, T> {
})
}

fn take_witness_col_values(&mut self) -> HashMap<String, Vec<T>> {
fn take_witness_col_values<'b, Q: QueryCallback<T>>(
&mut self,
_fixed_lookup: &'b mut FixedLookup<T>,
_query_callback: &'b mut Q,
) -> HashMap<String, Vec<T>> {
if self.data.len() < 2 * self.block_size {
log::warn!(
"Filling empty blocks with zeros, because the block machine is never used. \
Expand Down Expand Up @@ -253,13 +257,10 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> {
let namespace = first_witness_name
.rfind('.')
.map(|idx| &first_witness_name[..idx]);
if let Some(namespace) = namespace {
namespace
} else {
// For machines compiled using Powdr ASM we'll always have a namespace, but as a last
// resort we'll use the first witness name.
first_witness_name
}

// For machines compiled using Powdr ASM we'll always have a namespace, but as a last
// resort we'll use the first witness name.
namespace.unwrap_or(first_witness_name)
}

fn process_plookup_internal<'b, Q: QueryCallback<T>>(
Expand Down
8 changes: 6 additions & 2 deletions executor/src/witgen/machines/double_sorted_witness_machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ use ast::parsed::SelectedExpressions;
use itertools::Itertools;
use num_traits::Zero;

use super::Machine;
use super::{FixedLookup, Machine};
use crate::witgen::affine_expression::AffineExpression;
use crate::witgen::util::is_simple_poly_of_name;
use crate::witgen::{EvalResult, FixedData, MutableState, QueryCallback};
Expand Down Expand Up @@ -111,7 +111,11 @@ impl<'a, T: FieldElement> Machine<'a, T> for DoubleSortedWitnesses<T> {
Some(self.process_plookup_internal(left, right))
}

fn take_witness_col_values(&mut self) -> HashMap<String, Vec<T>> {
fn take_witness_col_values<'b, Q: QueryCallback<T>>(
&mut self,
_fixed_lookup: &'b mut FixedLookup<T>,
_query_callback: &'b mut Q,
) -> HashMap<String, Vec<T>> {
let mut addr = vec![];
let mut step = vec![];
let mut value = vec![];
Expand Down
Loading

0 comments on commit ec8c994

Please sign in to comment.