Skip to content

Commit

Permalink
Prepare block machine processor (#2231)
Browse files Browse the repository at this point in the history
A few preparations for #2226:
- Extracted a `test_utils` module
- Introduced a new `Variable` type, which can refer to either a cell or
a "parameter" (either input or output of a machine call). I think in the
future, we could have more variants (e.g. scalar publics). `Variable` is
now used instead of `Cell` in `WitgenInference`.
- `WitgenInference::process_identity` now also returns whether any
progress has been made.
- Renamed `lookup` -> `machine_call` when rendering `Effect`s
  • Loading branch information
georgwiese authored Dec 16, 2024
1 parent 19a9457 commit d007b8f
Show file tree
Hide file tree
Showing 4 changed files with 186 additions and 112 deletions.
5 changes: 4 additions & 1 deletion executor/src/witgen/jit/mod.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
pub(crate) mod affine_symbolic_expression;
mod cell;
pub(crate) mod jit_processor;
mod symbolic_expression;
mod variable;
pub(crate) mod witgen_inference;

#[cfg(test)]
pub(crate) mod test_util;
42 changes: 42 additions & 0 deletions executor/src/witgen/jit/test_util.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
use itertools::Itertools;
use powdr_number::GoldilocksField;

use crate::witgen::jit::affine_symbolic_expression::MachineCallArgument;

use super::{
affine_symbolic_expression::{Assertion, Effect},
variable::Variable,
};

pub fn format_code(effects: &[Effect<GoldilocksField, Variable>]) -> String {
effects
.iter()
.map(|effect| match effect {
Effect::Assignment(v, expr) => format!("{v} = {expr};"),
Effect::Assertion(Assertion {
lhs,
rhs,
expected_equal,
}) => {
format!(
"assert {lhs} {} {rhs};",
if *expected_equal { "==" } else { "!=" }
)
}
Effect::MachineCall(id, args) => {
format!(
"machine_call({id}, [{}]);",
args.iter()
.map(|arg| match arg {
MachineCallArgument::Known(k) => format!("Known({k})"),
MachineCallArgument::Unknown(u) => format!("Unknown({u})"),
})
.join(", ")
)
}
Effect::RangeConstraint(..) => {
panic!("Range constraints should not be part of the code.")
}
})
.join("\n")
}
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,49 @@ use std::{
hash::{Hash, Hasher},
};

use powdr_ast::analyzed::AlgebraicReference;
use powdr_ast::analyzed::{AlgebraicReference, PolyID, PolynomialType};

#[derive(PartialEq, Eq, PartialOrd, Ord, Hash, Clone, Debug)]
/// A variable that can be used in the inference engine.
pub enum Variable {
/// A witness cell in the current block machine.
Cell(Cell),
/// A parameter (input or output) of the machine.
#[allow(dead_code)]
Param(usize),
}

impl Display for Variable {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match self {
Variable::Cell(cell) => write!(f, "{cell}"),
Variable::Param(i) => write!(f, "params[{i}]"),
}
}
}

impl Variable {
/// Create a variable from an algebraic reference.
pub fn from_reference(r: &AlgebraicReference, row_offset: i32) -> Self {
assert!(r.is_witness());
Self::Cell(Cell {
column_name: r.name.clone(),
id: r.poly_id.id,
row_offset: r.next as i32 + row_offset,
})
}

/// If this variable corresponds to a witness cell, return the corresponding polynomial ID.
pub fn try_to_witness_poly_id(&self) -> Option<powdr_ast::analyzed::PolyID> {
match self {
Variable::Cell(cell) => Some(PolyID {
id: cell.id,
ptype: PolynomialType::Committed,
}),
Variable::Param(_) => None,
}
}
}

/// The identifier of a witness cell in the trace table.
/// The `row_offset` is relative to a certain "zero row" defined
Expand Down Expand Up @@ -41,17 +83,6 @@ impl PartialOrd for Cell {
}
}

impl Cell {
pub fn from_reference(r: &AlgebraicReference, row_offset: i32) -> Self {
assert!(r.is_witness());
Self {
column_name: r.name.clone(),
id: r.poly_id.id,
row_offset: r.next as i32 + row_offset,
}
}
}

impl Display for Cell {
fn fmt(&self, f: &mut Formatter) -> fmt::Result {
write!(f, "{}[{}]", self.column_name, self.row_offset)
Expand Down
Loading

0 comments on commit d007b8f

Please sign in to comment.