-
Notifications
You must be signed in to change notification settings - Fork 116
Apc stacking #2917
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
base: main
Are you sure you want to change the base?
Apc stacking #2917
Conversation
- another unknown instruction - handle interactions to the same bus id with different number of args
vm_config: VmConfig<T, B>, | ||
degree_bound: DegreeBound, | ||
opcode: u32, | ||
strict_is_valid_guards: bool, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you add some documentation on this parameter?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What about this?
/// "Guarding" constraints means that the prover can choose to disable them, which is useful for
/// filling up rows until the next power of two. A new boolean variable (`is_valid`) introduced
/// that allows the prover to disable constraints.
enum GuardingMode {
/// Makes sure that setting all variables to zero satisfies the constraints.
AllowZeroWitness,
/// Makes sure that all constraints are satisfied as long as `is_valid` is set to 0.
/// This mode always increases the constraint degree by one.
Strict,
}
autoprecompiles/src/lib.rs
Outdated
fn add_guards<T: FieldElement>( | ||
mut machine: SymbolicMachine<T>, | ||
bus_map: BusMap, | ||
strict: bool, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
strict: bool, | |
is_strict: bool, |
machine | ||
.constraints | ||
.into_iter() | ||
.map(|mut c| { | ||
c.expr = is_valid.clone() * c.expr.clone(); | ||
c | ||
}) | ||
.collect() | ||
} else { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Does this disable some cheaper stuff that add_guards_constraint
does in the non strict case? It seems like is_strict
could be pulled into add_guards_constraint
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
add_guards_constraint
is a recursive fn that ensures the degree doesn't increase... which is not the case here, so opted to be explicit here
impl<T: Clone + Ord, R: Clone + Ord> AlgebraicExpression<T, R> { | ||
/// Get a canonical form by expanding the expression and reordering operands. | ||
pub fn normalize(self) -> Self { | ||
normalize(expand(self)) | ||
} | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could this be done by going through quadratic expression? cc @georgwiese
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not quite. GroupedExpression
(formerly QuadraticSymbolicExpression
) has a canonical representation for expressions up to degree 1...
We could do this by introducing a CanonicalExpression
type which is essentially a BTreeMap<BTreeSet<R>, T>
. As long as it implements Add + Sub + Mul + Neg
, AlgebraicExpression::to_expression
can convert to it (via the ExpressionConvertible
trait).
If AlgebraicExpression
also implements From<CanonicalExpression>
, we could implement the normalization as something like
self.to_expression(
&|number| CanonicalExpression { coefficients:
[(BTreeSet::new(), *number)].into_iter().collect()
}, |reference| CanonicalExpression { coefficients:
([*reference].into_iter().collect(), T::one())].into_iter().collect()
}).into()
Not sure if it's worth it, but seems a bit cleaner.
); | ||
let height = next_power_of_two_or_zero(num_records); | ||
|
||
let trace = if self.executors.len() == 1 { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Stupid question: why do we need an if else, aka why isn't the else block also valid for a single opcode?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
it is valid, but its wasteful: when stacking we need to create the table and then copy the witness from each executor... this could be improved (TODO)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice!
I wasn't able to review the code of the AIR stacking itself yet, but I did run it and skimmed the results, looks really cool!
Maybe it's also fine, because we're not sure how much we'll use this feature and we should flag it as experimental anyway at this point. I think it's more important that the feature doesn't leak too much into the rest of the code base. I have a few smaller comments that might help with that.
let mut remapped = pcp.machine.clone(); | ||
remapped.pre_visit_expressions_mut(&mut |expr| { | ||
if let AlgebraicExpression::Reference(r) = expr { | ||
assert!(r.id <= is_valid_start); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
assert!(r.id <= is_valid_start); | |
assert!(r.id < is_valid_start); |
No?
// we assume each pcp to have a specific column named "is_valid" | ||
assert!(*r.name == "is_valid"); | ||
r.id = is_valid_new_id; | ||
r.name = format!("is_valid_{}", pcp.opcode.global_opcode().as_usize()).into(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This isn't going necessarily going to be unique, is it? Maybe idx
would be better?
input: Option<u32>, | ||
|
||
#[arg(long)] | ||
chip_stacking: Option<f32>, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you add a description here, with a note that the feature is experimental?
vm_config: VmConfig<T, B>, | ||
degree_bound: DegreeBound, | ||
opcode: u32, | ||
strict_is_valid_guards: bool, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What about this?
/// "Guarding" constraints means that the prover can choose to disable them, which is useful for
/// filling up rows until the next power of two. A new boolean variable (`is_valid`) introduced
/// that allows the prover to disable constraints.
enum GuardingMode {
/// Makes sure that setting all variables to zero satisfies the constraints.
AllowZeroWitness,
/// Makes sure that all constraints are satisfied as long as `is_valid` is set to 0.
/// This mode always increases the constraint degree by one.
Strict,
}
left, | ||
op: AlgebraicBinaryOperator::Sub, | ||
right, | ||
}) => normalize(*left) - normalize(*right), |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This seems sus, why would it be simpler than addition?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
its simpler because there's no need to handle commutativity (no need to flatten and reorder)
impl<T: Clone + Ord, R: Clone + Ord> AlgebraicExpression<T, R> { | ||
/// Get a canonical form by expanding the expression and reordering operands. | ||
pub fn normalize(self) -> Self { | ||
normalize(expand(self)) | ||
} | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not quite. GroupedExpression
(formerly QuadraticSymbolicExpression
) has a canonical representation for expressions up to degree 1...
We could do this by introducing a CanonicalExpression
type which is essentially a BTreeMap<BTreeSet<R>, T>
. As long as it implements Add + Sub + Mul + Neg
, AlgebraicExpression::to_expression
can convert to it (via the ExpressionConvertible
trait).
If AlgebraicExpression
also implements From<CanonicalExpression>
, we could implement the normalization as something like
self.to_expression(
&|number| CanonicalExpression { coefficients:
[(BTreeSet::new(), *number)].into_iter().collect()
}, |reference| CanonicalExpression { coefficients:
([*reference].into_iter().collect(), T::one())].into_iter().collect()
}).into()
Not sure if it's worth it, but seems a bit cleaner.
impl<P: IntoOpenVm> From<PowdrPrecompile<P>> for PowdrStackedPrecompile<P> { | ||
fn from(pcp: PowdrPrecompile<P>) -> Self { | ||
Self { | ||
machine: pcp.machine.clone(), |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmm, so by default, we store the machine twice. Maybe using an enum would be better?
} | ||
} | ||
|
||
impl<T: Clone + Ord, R: Clone + Ord> AlgebraicExpression<T, R> { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the changes to this file could be nice individual PR :)
original_config: &OriginalVmConfig, | ||
pgo_config: PgoConfig, | ||
) -> Vec<BlockWithApc<P>> { | ||
let strict_is_valid_guards = config.chip_stacking_log.is_some(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is passed down a few functions that could just compute it themselves from the config.
I think I'd pass the config all the way to generate_autoprecompile
(currently gets separate args for degree_bound
and strict_is_valid_guards
) and compute it there, before passing to powdr_autoprecompiles::build
.
); | ||
let air = PowdrAir::new(precompile.machine); | ||
|
||
let name = if precompile.precompiles.len() == 1 { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could be a method of PowdrStackedPrecompile
(which I think should be an enum, see comment above).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Also, maybe we should store the precompile directly? Looks like e.g. the name is re-computed later again.
This PR adds APC stacking to the powdr openvm pipeline.
On the openvm integration side, the main idea is adding a
PowdrStackedPrecompile
which may contain one or more of the existingPowdrPrecompile
, referenced by opcode.Similarly, the
PowdrChip
now contains a map of executors, one per precompile, by opcode.This way, the adaptations were relatively straightforward (e.g., witgen).
To enable stacking, there's a
chip_stacking_log
parameter which, if set, enables chip stacking with bucketing based on the given log of the number of witness columns.