Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Try zero #2357

Draft
wants to merge 11 commits into
base: main
Choose a base branch
from
55 changes: 50 additions & 5 deletions executor/src/witgen/jit/block_machine_processor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -254,11 +254,17 @@ params[2] = Add::c[0];"
col witness sel, a, b, c;
a + b = 0;
";
let err_str = generate_for_block_machine(input, "Unconstrained", 2, 1)
.err()
.unwrap();
assert!(err_str
.contains("The following variables or values are still missing: Unconstrained::c"));
let code = generate_for_block_machine(input, "Unconstrained", 2, 1)
.unwrap()
.code;
assert_eq!(
format_code(&code),
"Unconstrained::sel[0] = 1;
Unconstrained::a[0] = params[0];
Unconstrained::b[0] = params[1];
params[2] = 0;
Unconstrained::c[0] = 0;"
);
}

#[test]
Expand Down Expand Up @@ -350,4 +356,43 @@ params[3] = main_binary::C[3];"
let input = read_to_string("../test_data/pil/poseidon_gl.pil").unwrap();
generate_for_block_machine(&input, "main_poseidon", 12, 4).unwrap();
}

#[test]
fn bitfield_opid() {
// The issue with this machine is that if we pass 0 as the operation_id, the machine
// is fully unconstrained.
let input = "
namespace Main(256);
col witness x, a, b, c;
[x, a, b, c] is [
Arith::is_add + 2 * Arith::is_mul, Arith::X, Arith::Y, Arith::Z];
namespace Arith(256);
col witness is_add, is_mul, X, Y, Z;
is_add * (1 - is_add) = 0;
is_mul * (1 - is_mul) = 0;
is_add * (X + Y - Z) = 0;
is_mul * (X * Y - Z) = 0;
";
let code = generate_for_block_machine(input, "Arith", 3, 1);
assert_eq!(
format_code(&code.unwrap().code),
"Arith::is_add[0] = (params[0] & 0x1);
Arith::is_mul[0] = ((params[0] & 0x2) // 2);
assert (params[0] & 0xfffffffffffffffc) == 0;
Arith::X[0] = params[1];
Arith::Y[0] = params[2];
if (Arith::is_add[0] == 1) {
Arith::Z[0] = (Arith::X[0] + Arith::Y[0]);
params[3] = Arith::Z[0];
} else {
if (Arith::is_mul[0] == 1) {
Arith::Z[0] = (Arith::X[0] * Arith::Y[0]);
params[3] = Arith::Z[0];
} else {
params[3] = 0;
Arith::Z[0] = 0;
}
}"
);
}
}
70 changes: 57 additions & 13 deletions executor/src/witgen/jit/processor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ use itertools::Itertools;
use powdr_ast::{
analyzed::{
AlgebraicExpression as Expression, AlgebraicReference, AlgebraicReferenceThin, Identity,
PolyID, PolynomialType,
PolyID, PolynomialIdentity, PolynomialType,
},
parsed::visitor::{AllChildren, Children},
};
Expand Down Expand Up @@ -136,18 +136,15 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> Processor<'a, T, FixedEv
self.check_block_shape(&witgen);
}

// Check that we could derive all requested variables.
let missing_variables = self
.requested_known_vars
.iter()
.filter(|var| !witgen.is_known(var))
// Sort to get deterministic code.
.sorted()
.cloned()
.collect_vec();

let incomplete_machine_calls = self.incomplete_machine_calls(&witgen);
if missing_variables.is_empty() && incomplete_machine_calls.is_empty() {
if self.is_finished(&witgen) {
// Set the requested known variables, so that potential output params are
// actually assigned. We can do that because `is_finished` guarantees that
// the remaining unknown variables are all unconstrained.
for v in &self.requested_known_vars {
if !witgen.is_known(v) {
witgen.set_variable(v.clone(), 0.into()).unwrap();
}
}
let range_constraints = self
.requested_range_constraints
.iter()
Expand Down Expand Up @@ -181,6 +178,14 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> Processor<'a, T, FixedEv
} else {
ErrorReason::MaxBranchDepthReached(self.max_branch_depth)
};
let missing_variables = self
.requested_known_vars
.iter()
.filter(|var| !witgen.is_known(var))
// Sort to get deterministic code.
.sorted()
.cloned()
.collect_vec();
let incomplete_identities = self
.identities
.iter()
Expand Down Expand Up @@ -283,6 +288,45 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> Processor<'a, T, FixedEv
Ok(())
}

fn is_finished(&self, witgen: &WitgenInference<'a, T, FixedEval>) -> bool {
if !self.incomplete_machine_calls(witgen).is_empty() {
return false;
}
// We completed all required submachine calls.
let missing_variables = self
.requested_known_vars
.iter()
.filter(|var| !witgen.is_known(var))
.collect_vec();
if missing_variables.is_empty() {
return true;
}

// Some variables are missing. Check if they are unconstrained.
let incomplete_poly_identities = self
.identities
.iter()
.filter(|(id, row)| !witgen.is_complete(id, *row))
.filter_map(|(id, row)| match id {
// We already know that all machine calls are completed,
// so only consider polynomial identities.
Identity::Polynomial(PolynomialIdentity { expression, .. }) => {
Some((expression, row))
}
_ => None,
});
// If all incomplete identities only evaluate to known variables, we are done.
for (e, row) in incomplete_poly_identities {
let Some(e) = witgen.evaluate(e, *row) else {
return false;
};
if e.try_to_known().is_none() {
return false;
}
}
true
}

/// If any machine call could not be completed, that's bad because machine calls typically have side effects.
/// So, the underlying lookup / permutation / bus argument likely does not hold.
/// This function checks that all machine calls are complete, at least for a window of <block_size> rows.
Expand Down
29 changes: 24 additions & 5 deletions executor/src/witgen/jit/single_step_processor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -202,16 +202,23 @@ namespace M(256);

#[test]
fn no_progress() {
let input = "namespace M(256); let X; let Y; X' = X;";
let input = "namespace M(256); let X; let Y; X' = X * X';";
let err = generate_single_step(input, "M").err().unwrap();
assert_eq!(
err.to_string(),
"Unable to derive algorithm to compute required values: \
No variable available to branch on.\nThe following variables or values are still missing: M::Y[1]\n\
No variable available to branch on.\nThe following variables or values are still missing: M::X[1], M::Y[1]\n\
The following identities have not been fully processed:\n\
--------------[ identity 0 on row 0: ]--------------
M::X' = ( M::X * M::X')
??? = <known> ???
=
M::X' = ( M::X * M::X')
??? = <known> ???
= \n\
The following branch decisions were taken:\n\
\n\
Generated code so far:\n\
M::X[1] = M::X[0];"
No code generated so far."
);
}

Expand Down Expand Up @@ -321,8 +328,20 @@ VM::instr_mul[1] = 1;"
col witness X, Y, Z;
Z = X + Y;
";

// TODO: This currently succeeds with the following code:
chriseth marked this conversation as resolved.
Show resolved Hide resolved
// Main::a[1] = 2;
// Main::b[1] = 0;
// Main::c[1] = 0;
// Main::is_arith[1] = 0;

// But it does not do the call, which should be required!
// It should not set `is_arith` to zero - or should it?

match generate_single_step(input, "Main") {
Ok(_) => panic!("Expected error"),
Ok(r) => {
panic!("Expected error, got code:\n{}", format_code(&r));
}
Err(e) => {
let expected = "\
Main::is_arith $ [ Main::a, Main::b, Main::c ]
Expand Down
11 changes: 11 additions & 0 deletions executor/src/witgen/jit/witgen_inference.rs
Original file line number Diff line number Diff line change
Expand Up @@ -230,6 +230,17 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
self.process_assignments().unwrap();
}

/// Set the provided variable to a constant value.
pub fn set_variable(&mut self, variable: Variable, value: T) -> Result<Vec<Variable>, Error> {
self.ingest_effects(
ProcessResult {
effects: vec![Effect::Assignment(variable.clone(), value.into())],
complete: true,
},
None,
)
}

/// Processes an equality constraint.
/// If this returns an error, it means we have conflicting constraints.
fn process_equality_on_row(
Expand Down
Loading