github/powdr
1
1
Fork 0
mirror of https://github.com/powdr-labs/powdr.git synced 2026-04-20 03:03:25 -04:00
Code Issues Packages Projects Releases Wiki Activity

Rust phantom constr (#1945)

Browse Source 
Following #1934, adds these new variants to the rust side. A follow up
PR by @georgwiese will actually compute multiplicities in witgen.

---------

Co-authored-by: Georg Wiese <georgwiese@gmail.com>
This commit is contained in:
Thibaut Schaeffer
2024-11-04 17:08:50 +01:00
committed by GitHub
parent 2ec0d157ed
commit 073572aafa
23 changed files with 386 additions and 234 deletions
Download Patch File Download Diff File Expand all files Collapse all files

42
ast/src/analyzed/display.rs
View File

@@ -350,12 +350,54 @@ impl<T: Display> Display for LookupIdentity<T> {
}
}
fn format_selector<T: Display>(selector: &AlgebraicExpression<T>) -> String {
match selector.to_string().as_str() {
"1" => "Option::None".to_string(),
s => format!("Option::Some({s})"),
}
}
impl<T: Display> Display for PhantomLookupIdentity<T> {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
write!(
f,
"Constr::PhantomLookup(({}, {}), [{}], {});",
format_selector(&self.left.selector),
format_selector(&self.right.selector),
self.left
.expressions
.iter()
.zip_eq(&self.right.expressions)
.map(|(left, right)| format!("({left}, {right})"))
.format(", "),
self.multiplicity
)
}
}
impl<T: Display> Display for PermutationIdentity<T> {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
write!(f, "{} is {};", self.left, self.right)
}
}
impl<T: Display> Display for PhantomPermutationIdentity<T> {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
write!(
f,
"Constr::PhantomPermutation(({}, {}), [{}]);",
format_selector(&self.left.selector),
format_selector(&self.right.selector),
self.left
.expressions
.iter()
.zip_eq(&self.right.expressions)
.map(|(left, right)| format!("({left}, {right})"))
.format(", ")
)
}
}
impl<T: Display> Display for ConnectIdentity<T> {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
write!(

91
ast/src/analyzed/mod.rs
View File

@@ -927,6 +927,39 @@ impl<T> Children<AlgebraicExpression<T>> for LookupIdentity<T> {
}
}
/// A witness generation helper for a lookup identity.
///
/// This identity is used as a replactement for a lookup identity which has been turned into challenge-based polynomial identities.
/// This is ignored by the backend.
#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)]
pub struct PhantomLookupIdentity<T> {
// The ID is globally unique among identities.
pub id: u64,
pub source: SourceRef,
pub left: SelectedExpressions<T>,
pub right: SelectedExpressions<T>,
pub multiplicity: AlgebraicExpression<T>,
}
impl<T> Children<AlgebraicExpression<T>> for PhantomLookupIdentity<T> {
fn children_mut(&mut self) -> Box<dyn Iterator<Item = &mut AlgebraicExpression<T>> + '_> {
Box::new(
self.left
.children_mut()
.chain(self.right.children_mut())
.chain(self.multiplicity.children_mut()),
)
}
fn children(&self) -> Box<dyn Iterator<Item = &AlgebraicExpression<T>> + '_> {
Box::new(
self.left
.children()
.chain(self.right.children())
.chain(self.multiplicity.children()),
)
}
}
#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)]
pub struct PermutationIdentity<T> {
// The ID is globally unique among identitites.
@@ -945,6 +978,28 @@ impl<T> Children<AlgebraicExpression<T>> for PermutationIdentity<T> {
}
}
/// A witness generation helper for a permutation identity.
///
/// This identity is used as a replactement for a permutation identity which has been turned into challenge-based polynomial identities.
/// This is ignored by the backend.
#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)]
pub struct PhantomPermutationIdentity<T> {
// The ID is globally unique among identitites.
pub id: u64,
pub source: SourceRef,
pub left: SelectedExpressions<T>,
pub right: SelectedExpressions<T>,
}
impl<T> Children<AlgebraicExpression<T>> for PhantomPermutationIdentity<T> {
fn children_mut(&mut self) -> Box<dyn Iterator<Item = &mut AlgebraicExpression<T>> + '_> {
Box::new(self.left.children_mut().chain(self.right.children_mut()))
}
fn children(&self) -> Box<dyn Iterator<Item = &AlgebraicExpression<T>> + '_> {
Box::new(self.left.children().chain(self.right.children()))
}
}
#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)]
pub struct ConnectIdentity<T> {
// The ID is globally unique among identitites.
@@ -963,22 +1018,6 @@ impl<T> Children<AlgebraicExpression<T>> for ConnectIdentity<T> {
}
}
impl<T> ConnectIdentity<T> {
pub fn new(
id: u64,
source: SourceRef,
left: Vec<AlgebraicExpression<T>>,
right: Vec<AlgebraicExpression<T>>,
) -> Self {
Self {
id,
source,
left,
right,
}
}
}
#[derive(
Debug,
PartialEq,
@@ -994,7 +1033,9 @@ impl<T> ConnectIdentity<T> {
pub enum Identity<T> {
Polynomial(PolynomialIdentity<T>),
Lookup(LookupIdentity<T>),
PhantomLookup(PhantomLookupIdentity<T>),
Permutation(PermutationIdentity<T>),
PhantomPermutation(PhantomPermutationIdentity<T>),
Connect(ConnectIdentity<T>),
}
@@ -1011,7 +1052,9 @@ impl<T> Identity<T> {
match self {
Identity::Polynomial(i) => i.id,
Identity::Lookup(i) => i.id,
Identity::PhantomLookup(i) => i.id,
Identity::Permutation(i) => i.id,
Identity::PhantomPermutation(i) => i.id,
Identity::Connect(i) => i.id,
}
}
@@ -1019,8 +1062,10 @@ impl<T> Identity<T> {
pub fn kind(&self) -> IdentityKind {
match self {
Identity::Polynomial(_) => IdentityKind::Polynomial,
Identity::Lookup(_) => IdentityKind::Plookup,
Identity::Lookup(_) => IdentityKind::Lookup,
Identity::PhantomLookup(_) => IdentityKind::PhantomLookup,
Identity::Permutation(_) => IdentityKind::Permutation,
Identity::PhantomPermutation(_) => IdentityKind::PhantomPermutation,
Identity::Connect(_) => IdentityKind::Connect,
}
}
@@ -1031,7 +1076,9 @@ impl<T> SourceReference for Identity<T> {
match self {
Identity::Polynomial(i) => &i.source,
Identity::Lookup(i) => &i.source,
Identity::PhantomLookup(i) => &i.source,
Identity::Permutation(i) => &i.source,
Identity::PhantomPermutation(i) => &i.source,
Identity::Connect(i) => &i.source,
}
}
@@ -1040,7 +1087,9 @@ impl<T> SourceReference for Identity<T> {
match self {
Identity::Polynomial(i) => &mut i.source,
Identity::Lookup(i) => &mut i.source,
Identity::PhantomLookup(i) => &mut i.source,
Identity::Permutation(i) => &mut i.source,
Identity::PhantomPermutation(i) => &mut i.source,
Identity::Connect(i) => &mut i.source,
}
}
@@ -1051,7 +1100,9 @@ impl<T> Children<AlgebraicExpression<T>> for Identity<T> {
match self {
Identity::Polynomial(i) => i.children_mut(),
Identity::Lookup(i) => i.children_mut(),
Identity::PhantomLookup(i) => i.children_mut(),
Identity::Permutation(i) => i.children_mut(),
Identity::PhantomPermutation(i) => i.children_mut(),
Identity::Connect(i) => i.children_mut(),
}
}
@@ -1060,7 +1111,9 @@ impl<T> Children<AlgebraicExpression<T>> for Identity<T> {
match self {
Identity::Polynomial(i) => i.children(),
Identity::Lookup(i) => i.children(),
Identity::PhantomLookup(i) => i.children(),
Identity::Permutation(i) => i.children(),
Identity::PhantomPermutation(i) => i.children(),
Identity::Connect(i) => i.children(),
}
}
@@ -1071,8 +1124,10 @@ impl<T> Children<AlgebraicExpression<T>> for Identity<T> {
)]
pub enum IdentityKind {
Polynomial,
Plookup,
Lookup,
PhantomLookup,
Permutation,
PhantomPermutation,
Connect,
}

10
backend-utils/src/lib.rs
View File

@@ -9,7 +9,7 @@ use itertools::Itertools;
use powdr_ast::{
analyzed::{
AlgebraicExpression, Analyzed, Identity, LookupIdentity, PermutationIdentity,
StatementIdentifier, Symbol, SymbolKind,
PhantomLookupIdentity, PhantomPermutationIdentity, StatementIdentifier, Symbol, SymbolKind,
},
parsed::{
asm::{AbsoluteSymbolPath, SymbolPath},
@@ -193,7 +193,13 @@ fn split_by_namespace<F: FieldElement>(
.then(|| (current_namespace.clone(), statement)),
_ => match identity {
Identity::Lookup(LookupIdentity { left, right, .. })
| Identity::Permutation(PermutationIdentity { left, right, .. }) => {
| Identity::PhantomLookup(PhantomLookupIdentity { left, right, .. })
| Identity::Permutation(PermutationIdentity { left, right, .. })
| Identity::PhantomPermutation(PhantomPermutationIdentity {
left,
right,
..
}) => {
assert_eq!(
referenced_namespaces(left).len(),
1,

2
backend/src/estark/json_exporter/expression_counter.rs
View File

@@ -59,6 +59,8 @@ impl<T: FieldElement> ExpressionCounter for Identity<T> {
Identity::Connect(connect_identity) => {
connect_identity.left.len() + connect_identity.right.len()
}
// phantom identities are not relevant in this context
Identity::PhantomLookup(..) | Identity::PhantomPermutation(..) => 0,
}
}
}

3
backend/src/estark/json_exporter/mod.rs
View File

@@ -135,6 +135,9 @@ pub fn export<T: FieldElement>(analyzed: &Analyzed<T>) -> PIL {
line,
});
}
Identity::PhantomLookup(..) | Identity::PhantomPermutation(..) => {
// These are not relevant for the PIL
}
}
}
StatementIdentifier::ProverFunction(_)

3
backend/src/halo2/circuit_builder.rs
View File

@@ -320,6 +320,9 @@ impl<'a, T: FieldElement, F: PrimeField<Repr = [u8; 32]>> Circuit<F> for PowdrCi
.collect()
});
}
Identity::PhantomLookup(..) | Identity::PhantomPermutation(..) => {
// Phantom identities are only used in witness generation
}
}
}

17
executor/src/witgen/global_constraints.rs
View File

@@ -3,9 +3,10 @@ use std::marker::PhantomData;
use num_traits::Zero;
use num_traits::One;
use powdr_ast::analyzed::{
AlgebraicBinaryOperation, AlgebraicBinaryOperator, AlgebraicExpression as Expression,
AlgebraicReference, LookupIdentity, PermutationIdentity, PolyID, PolynomialType,
AlgebraicReference, LookupIdentity, PhantomLookupIdentity, PolyID, PolynomialType,
};
use powdr_number::FieldElement;
@@ -237,10 +238,11 @@ fn propagate_constraints<T: FieldElement>(
}
}
Identity::Lookup(LookupIdentity { left, right, .. })
| Identity::Permutation(PermutationIdentity { left, right, .. }) => {
if left.selector != T::one().into() || right.selector != T::one().into() {
| Identity::PhantomLookup(PhantomLookupIdentity { left, right, .. }) => {
if !left.selector.is_one() || !right.selector.is_one() {
return (known_constraints, false);
}
// We learn range constraints from both lookups and permutations
for (left, right) in left.expressions.iter().zip(right.expressions.iter()) {
if let (Some(left), Some(right)) =
(try_to_simple_poly(left), try_to_simple_poly(right))
@@ -253,7 +255,11 @@ fn propagate_constraints<T: FieldElement>(
}
}
}
if right.expressions.len() == 1 {
// We only remove lookups, since permutations hold more information than just range constraints.
if right.expressions.len() == 1
&& matches!(identity, Identity::Lookup(..) | Identity::PhantomLookup(..))
{
// We can only remove the lookup if the RHS is a fixed polynomial that
// provides all values in the span.
if let Some(name) = try_to_simple_poly(&right.expressions[0]) {
@@ -268,6 +274,9 @@ fn propagate_constraints<T: FieldElement>(
Identity::Connect(..) => {
// we do not handle connect identities yet, so we do nothing
}
Identity::Permutation(..) | Identity::PhantomPermutation(..) => {
// permutation identities are stronger than just range constraints, so we do nothing
}
}
(known_constraints, remove)

7
executor/src/witgen/identity_processor.rs
View File

@@ -5,7 +5,8 @@ use std::{
use lazy_static::lazy_static;
use powdr_ast::analyzed::{
AlgebraicExpression as Expression, LookupIdentity, PermutationIdentity, PolynomialIdentity,
AlgebraicExpression as Expression, LookupIdentity, PermutationIdentity, PhantomLookupIdentity,
PhantomPermutationIdentity, PolynomialIdentity,
};
use powdr_number::FieldElement;
@@ -152,7 +153,9 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback<T>> IdentityProcessor<'a, 'b,
let result = match identity {
Identity::Polynomial(identity) => self.process_polynomial_identity(identity, rows),
Identity::Lookup(LookupIdentity { left, id, .. })
| Identity::Permutation(PermutationIdentity { left, id, .. }) => {
| Identity::Permutation(PermutationIdentity { left, id, .. })
| Identity::PhantomLookup(PhantomLookupIdentity { left, id, .. })
| Identity::PhantomPermutation(PhantomPermutationIdentity { left, id, .. }) => {
self.process_lookup_or_permutation(*id, left, rows)
}
Identity::Connect(..) => {

21
executor/src/witgen/machines/fixed_lookup_machine.rs
View File

@@ -6,7 +6,9 @@ use std::num::NonZeroUsize;
use std::str::FromStr;
use itertools::Itertools;
use powdr_ast::analyzed::{AlgebraicReference, PolyID, PolynomialType};
use powdr_ast::analyzed::{
AlgebraicReference, LookupIdentity, PhantomLookupIdentity, PolyID, PolynomialType,
};
use powdr_ast::parsed::asm::SymbolPath;
use powdr_number::{DegreeType, FieldElement};
@@ -199,18 +201,23 @@ impl<'a, T: FieldElement> FixedLookup<'a, T> {
let connections = all_identities
.into_iter()
.filter_map(|i| match i {
Identity::Lookup(i) => (i.right.selector.is_one()
&& i.right.expressions.iter().all(|e| {
Identity::Lookup(LookupIdentity {
id, left, right, ..
})
| Identity::PhantomLookup(PhantomLookupIdentity {
id, left, right, ..
}) => (right.selector.is_one()
&& right.expressions.iter().all(|e| {
try_to_simple_poly_ref(e)
.map(|poly| poly.poly_id.ptype == PolynomialType::Constant)
.unwrap_or(false)
})
&& !i.right.expressions.is_empty())
&& !right.expressions.is_empty())
.then_some((
i.id,
*id,
Connection {
left: &i.left,
right: &i.right,
left,
right,
kind: ConnectionKind::Lookup,
},
)),

16
executor/src/witgen/machines/machine_extractor.rs
View File

@@ -3,6 +3,8 @@ use std::collections::{BTreeMap, BTreeSet, HashSet};
use itertools::Itertools;
use powdr_ast::analyzed::LookupIdentity;
use powdr_ast::analyzed::PermutationIdentity;
use powdr_ast::analyzed::PhantomLookupIdentity;
use powdr_ast::analyzed::PhantomPermutationIdentity;
use super::block_machine::BlockMachine;
use super::double_sorted_witness_machine_16::DoubleSortedWitnesses16;
@@ -66,7 +68,9 @@ pub fn split_out_machines<'a, T: FieldElement>(
// Extract all witness columns in the RHS of the lookup.
let lookup_witnesses = match id {
Identity::Lookup(LookupIdentity { right, .. })
| Identity::Permutation(PermutationIdentity { right, .. }) => {
| Identity::PhantomLookup(PhantomLookupIdentity { right, .. })
| Identity::Permutation(PermutationIdentity { right, .. })
| Identity::PhantomPermutation(PhantomPermutationIdentity { right, .. }) => {
&refs_in_selected_expressions(right) & (&remaining_witnesses)
}
_ => Default::default(),
@@ -344,7 +348,11 @@ fn all_row_connected_witnesses<T>(
}
}
Identity::Lookup(LookupIdentity { left, right, .. })
| Identity::Permutation(PermutationIdentity { left, right, .. }) => {
| Identity::Permutation(PermutationIdentity { left, right, .. })
| Identity::PhantomLookup(PhantomLookupIdentity { left, right, .. })
| Identity::PhantomPermutation(PhantomPermutationIdentity {
left, right, ..
}) => {
// If we already have witnesses on the LHS, include the LHS,
// and vice-versa, but not across the "sides".
let in_lhs = &refs_in_selected_expressions(left) & all_witnesses;
@@ -378,7 +386,9 @@ fn refs_in_selected_expressions<T>(sel_expr: &SelectedExpressions<T>) -> HashSet
fn refs_in_identity_left<T>(identity: &Identity<T>) -> HashSet<PolyID> {
match identity {
Identity::Lookup(LookupIdentity { left, .. })
| Identity::Permutation(PermutationIdentity { left, .. }) => {
| Identity::PhantomLookup(PhantomLookupIdentity { left, .. })
| Identity::Permutation(PermutationIdentity { left, .. })
| Identity::PhantomPermutation(PhantomPermutationIdentity { left, .. }) => {
refs_in_selected_expressions(left)
}
Identity::Polynomial(i) => refs_in_expression(&i.expression).collect(),

10
executor/src/witgen/machines/mod.rs
View File

@@ -186,11 +186,21 @@ impl<'a, T> TryFrom<&'a Identity<T>> for Connection<'a, T> {
right: &i.right,
kind: ConnectionKind::Lookup,
}),
Identity::PhantomLookup(i) => Ok(Connection {
left: &i.left,
right: &i.right,
kind: ConnectionKind::Lookup,
}),
Identity::Permutation(i) => Ok(Connection {
left: &i.left,
right: &i.right,
kind: ConnectionKind::Permutation,
}),
Identity::PhantomPermutation(i) => Ok(Connection {
left: &i.left,
right: &i.right,
kind: ConnectionKind::Permutation,
}),
_ => Err(identity),
}
}

21
executor/src/witgen/machines/sorted_witness_machine.rs
View File

@@ -13,7 +13,10 @@ use crate::witgen::{EvalValue, IncompleteCause, MutableState, QueryCallback};
use crate::Identity;
use itertools::Itertools;
use num_traits::One;
use powdr_ast::analyzed::{AlgebraicExpression as Expression, AlgebraicReference, PolyID};
use powdr_ast::analyzed::{
AlgebraicExpression as Expression, AlgebraicReference, LookupIdentity, PhantomLookupIdentity,
PolyID,
};
use powdr_number::{DegreeType, FieldElement};
/// A machine that can support a lookup in a set of columns that are sorted
@@ -109,22 +112,22 @@ fn check_identity<T: FieldElement>(
degree: DegreeType,
) -> Option<PolyID> {
// Looking for a lookup
let id = if let Identity::Lookup(id) = id {
id
} else {
return None;
let (left, right) = match id {
Identity::Lookup(LookupIdentity { left, right, .. })
| Identity::PhantomLookup(PhantomLookupIdentity { left, right, .. }) => (left, right),
_ => return None,
};
// Looking for NOTLAST $ [ A' - A ] in [ POSITIVE ]
if !id.right.selector.is_one() || id.left.expressions.len() != 1 {
if !right.selector.is_one() || left.expressions.len() != 1 {
return None;
}
// Check for A' - A in the LHS
let key_column = check_constraint(id.left.expressions.first().unwrap())?;
let key_column = check_constraint(left.expressions.first().unwrap())?;
let not_last = &id.left.selector;
let positive = id.right.expressions.first().unwrap();
let not_last = &left.selector;
let positive = right.expressions.first().unwrap();
// TODO this could be rather slow. We should check the code for identity instead
// of evaluating it.

17
executor/src/witgen/vm_processor.rs
View File

@@ -1,6 +1,6 @@
use indicatif::{ProgressBar, ProgressStyle};
use itertools::Itertools;
use powdr_ast::analyzed::DegreeRange;
use powdr_ast::analyzed::{DegreeRange, LookupIdentity, PhantomLookupIdentity};
use powdr_ast::indent;
use powdr_number::{DegreeType, FieldElement};
use std::cmp::max;
@@ -355,10 +355,13 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback<T>> VmProcessor<'a, 'b, 'c, T
.iter_mut()
.enumerate()
.filter_map(|(index, (ident, _))| match ident {
Identity::Lookup(i) => Some((index, i)),
Identity::Lookup(LookupIdentity { left, .. })
| Identity::PhantomLookup(PhantomLookupIdentity { left, .. }) => {
Some((index, left))
}
_ => None,
})
.max_by_key(|(_, ident)| ident.left.expressions.len())
.max_by_key(|(_, left)| left.expressions.len())
.map(|(i, _)| i);
loop {
let mut progress = false;
@@ -447,7 +450,13 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback<T>> VmProcessor<'a, 'b, 'c, T
return Ok(None);
}
let is_machine_call = matches!(identity, Identity::Lookup(..) | Identity::Permutation(..));
let is_machine_call = matches!(
identity,
Identity::Lookup(..)
| Identity::Permutation(..)
| Identity::PhantomLookup(..)
| Identity::PhantomPermutation(..)
);
if is_machine_call && unknown_strategy == UnknownStrategy::Zero {
// The fact that we got to the point where we assume 0 for unknown cells, but this identity
// is still not complete, means that either the inputs or the machine is under-constrained.

61
pil-analyzer/src/condenser.rs
View File

@@ -15,9 +15,10 @@ use powdr_ast::{
analyzed::{
self, AlgebraicBinaryOperation, AlgebraicExpression, AlgebraicReference,
AlgebraicUnaryOperation, Analyzed, Challenge, ConnectIdentity, DegreeRange, Expression,
FunctionValueDefinition, Identity, LookupIdentity, PermutationIdentity, PolyID,
PolynomialIdentity, PolynomialReference, PolynomialType, PublicDeclaration, Reference,
SelectedExpressions, SolvedTraitImpls, StatementIdentifier, Symbol, SymbolKind,
FunctionValueDefinition, Identity, LookupIdentity, PermutationIdentity,
PhantomLookupIdentity, PhantomPermutationIdentity, PolyID, PolynomialIdentity,
PolynomialReference, PolynomialType, PublicDeclaration, Reference, SelectedExpressions,
SolvedTraitImpls, StatementIdentifier, Symbol, SymbolKind,
},
parsed::{
self,
@@ -678,8 +679,12 @@ fn to_constraint<T: FieldElement>(
}
.into()
}
"Lookup" | "Permutation" => {
assert_eq!(fields.len(), 2);
"Lookup" | "Permutation" | "PhantomLookup" | "PhantomPermutation" => {
if variant == &"PhantomLookup" {
assert_eq!(fields.len(), 3);
} else {
assert_eq!(fields.len(), 2);
}
let (sel_from, sel_to) = if let Value::Tuple(t) = fields[0].as_ref() {
assert_eq!(t.len(), 2);
@@ -703,22 +708,44 @@ fn to_constraint<T: FieldElement>(
unreachable!()
};
if variant == &"Lookup" {
LookupIdentity {
id: counters.dispense_identity_id(),
let id = counters.dispense_identity_id();
let left = to_selected_exprs(sel_from, from);
let right = to_selected_exprs(sel_to, to);
match *variant {
"Lookup" => LookupIdentity {
id,
source,
left: to_selected_exprs(sel_from, from),
right: to_selected_exprs(sel_to, to),
left,
right,
}
.into()
} else {
PermutationIdentity {
id: counters.dispense_identity_id(),
.into(),
"Permutation" => PermutationIdentity {
id,
source,
left: to_selected_exprs(sel_from, from),
right: to_selected_exprs(sel_to, to),
left,
right,
}
.into()
.into(),
"PhantomPermutation" => PhantomPermutationIdentity {
id,
source,
left,
right,
}
.into(),
"PhantomLookup" => {
let multiplicity = to_expr(&fields[2]);
PhantomLookupIdentity {
id,
source,
left,
right,
multiplicity,
}
.into()
}
_ => unreachable!(),
}
}
"Connection" => {

129
pilopt/src/lib.rs
View File

@@ -7,8 +7,9 @@ use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet};
use powdr_ast::analyzed::{
AlgebraicBinaryOperation, AlgebraicBinaryOperator, AlgebraicExpression, AlgebraicReference,
AlgebraicUnaryOperation, AlgebraicUnaryOperator, Analyzed, ConnectIdentity, Expression,
FunctionValueDefinition, Identity, LookupIdentity, PermutationIdentity, PolyID,
PolynomialIdentity, PolynomialReference, PolynomialType, Reference, SymbolKind,
FunctionValueDefinition, Identity, LookupIdentity, PermutationIdentity, PhantomLookupIdentity,
PhantomPermutationIdentity, PolyID, PolynomialIdentity, PolynomialReference, PolynomialType,
Reference, SymbolKind,
};
use powdr_ast::parsed::types::Type;
use powdr_ast::parsed::visitor::{AllChildren, Children, ExpressionVisitable};
@@ -326,47 +327,55 @@ fn simplify_expression_single<T: FieldElement>(e: &mut AlgebraicExpression<T>) {
fn extract_constant_lookups<T: FieldElement>(pil_file: &mut Analyzed<T>) {
let mut new_identities = vec![];
for identity in &mut pil_file.identities.iter_mut() {
if let Identity::Lookup(LookupIdentity {
source,
left,
right,
..
}) = identity
{
let mut extracted = HashSet::new();
for (i, (l, r)) in left
.expressions
.iter()
.zip(&right.expressions)
.enumerate()
.filter_map(|(i, (l, r))| {
if let AlgebraicExpression::Number(n) = r {
Some((i, (l, n)))
} else {
None
}
})
{
// TODO remove clones
let l_sel = left.selector.clone();
let r_sel = right.selector.clone();
let pol_id = (l_sel * l.clone()) - (r_sel * AlgebraicExpression::from(*r));
new_identities.push((simplify_expression(pol_id), source.clone()));
match identity {
Identity::Lookup(LookupIdentity {
source,
left,
right,
..
})
| Identity::PhantomLookup(PhantomLookupIdentity {
source,
left,
right,
..
}) => {
let mut extracted = HashSet::new();
for (i, (l, r)) in left
.expressions
.iter()
.zip(&right.expressions)
.enumerate()
.filter_map(|(i, (l, r))| {
if let AlgebraicExpression::Number(n) = r {
Some((i, (l, n)))
} else {
None
}
})
{
// TODO remove clones
let l_sel = left.selector.clone();
let r_sel = right.selector.clone();
let pol_id = (l_sel * l.clone()) - (r_sel * AlgebraicExpression::from(*r));
new_identities.push((simplify_expression(pol_id), source.clone()));
extracted.insert(i);
extracted.insert(i);
}
// TODO rust-ize this.
let mut c = 0usize;
left.expressions.retain(|_i| {
c += 1;
!extracted.contains(&(c - 1))
});
let mut c = 0usize;
right.expressions.retain(|_i| {
c += 1;
!extracted.contains(&(c - 1))
});
}
// TODO rust-ize this.
let mut c = 0usize;
left.expressions.retain(|_i| {
c += 1;
!extracted.contains(&(c - 1))
});
let mut c = 0usize;
right.expressions.retain(|_i| {
c += 1;
!extracted.contains(&(c - 1))
});
_ => {}
}
}
for (identity, source) in new_identities {
@@ -484,11 +493,13 @@ fn remove_trivial_identities<T: FieldElement>(pil_file: &mut Analyzed<T>) {
}
None
}
Identity::Lookup(LookupIdentity { left, right, .. }) => {
Identity::Lookup(LookupIdentity { left, right, .. })
| Identity::Permutation(PermutationIdentity { left, right, .. })
| Identity::PhantomLookup(PhantomLookupIdentity { left, right, .. })
| Identity::PhantomPermutation(PhantomPermutationIdentity { left, right, .. }) => {
assert_eq!(left.expressions.len(), right.expressions.len());
left.expressions.is_empty().then_some(index)
}
Identity::Permutation(..) => None,
Identity::Connect(..) => None,
})
.collect();
@@ -506,8 +517,10 @@ fn remove_duplicate_identities<T: FieldElement>(pil_file: &mut Analyzed<T>) {
let discriminant = |i: &CanonicalIdentity<T>| match i.0 {
Identity::Polynomial(..) => 0,
Identity::Lookup(..) => 1,
Identity::Permutation(..) => 2,
Identity::Connect(..) => 3,
Identity::PhantomLookup(..) => 2,
Identity::Permutation(..) => 3,
Identity::PhantomPermutation(..) => 4,
Identity::Connect(..) => 5,
};
discriminant(self)
@@ -525,6 +538,20 @@ fn remove_duplicate_identities<T: FieldElement>(pil_file: &mut Analyzed<T>) {
left: c, right: d, ..
}),
) => a.cmp(c).then_with(|| b.cmp(d)),
(
Identity::PhantomLookup(PhantomLookupIdentity {
left: a,
right: b,
multiplicity: c,
..
}),
Identity::PhantomLookup(PhantomLookupIdentity {
left: d,
right: e,
multiplicity: f,
..
}),
) => a.cmp(d).then_with(|| b.cmp(e)).then_with(|| c.cmp(f)),
(
Identity::Permutation(PermutationIdentity {
left: a, right: b, ..
@@ -533,6 +560,18 @@ fn remove_duplicate_identities<T: FieldElement>(pil_file: &mut Analyzed<T>) {
left: c, right: d, ..
}),
) => a.cmp(c).then_with(|| b.cmp(d)),
(
Identity::PhantomPermutation(PhantomPermutationIdentity {
left: a,
right: b,
..
}),
Identity::PhantomPermutation(PhantomPermutationIdentity {
left: c,
right: d,
..
}),
) => a.cmp(c).then_with(|| b.cmp(d)),
(
Identity::Connect(ConnectIdentity {
left: a, right: b, ..

36
pipeline/tests/powdr_std.rs
View File

@@ -171,15 +171,11 @@ fn lookup_via_challenges() {
}
#[test]
fn lookup_via_challenges_ext() {
let f = "std/lookup_via_challenges_ext.asm";
test_halo2(make_simple_prepared_pipeline(f));
test_plonky3::<GoldilocksField>(f, vec![]);
}
#[test]
fn lookup_via_challenges_ext_simple() {
let f = "std/lookup_via_challenges_ext_simple.asm";
#[should_panic = "Failed to merge the first and last row of the VM 'Main Machine'"]
fn lookup_via_challenges_range_constraint() {
// This test currently fails, because witness generation for the multiplicity column
// does not yet work for range constraints, so the lookup constraints are not satisfied.
let f = "std/lookup_via_challenges_range_constraint.asm";
test_halo2(make_simple_prepared_pipeline(f));
test_plonky3::<GoldilocksField>(f, vec![]);
}
@@ -191,35 +187,17 @@ fn bus_permutation_via_challenges() {
}
#[test]
fn bus_permutation_via_challenges_ext() {
fn bus_permutation_via_challenges_ext_bn() {
let f = "std/bus_permutation_via_challenges_ext.asm";
test_halo2(make_simple_prepared_pipeline(f));
test_plonky3::<GoldilocksField>(f, vec![]);
}
#[test]
fn test_multiplicities() {
let f = "std/multiplicities.asm";
test_halo2(make_simple_prepared_pipeline(f));
// This test currently has a native lookup to aid witness generation,
// which is not supported by the Plonky3 backend.
// test_plonky3::<GoldilocksField>(f, vec![]);
}
#[test]
fn bus_lookup_via_challenges() {
fn bus_lookup_via_challenges_bn() {
let f = "std/bus_lookup_via_challenges.asm";
test_halo2(make_simple_prepared_pipeline(f));
}
#[test]
fn bus_lookup_via_challenges_ext() {
let f = "std/bus_lookup_via_challenges_ext.asm";
test_halo2(make_simple_prepared_pipeline(f));
test_plonky3::<GoldilocksField>(f, vec![]);
}
#[test]
fn write_once_memory_test() {
let f = "std/write_once_memory_test.asm";

3
plonky3/src/circuit_builder.rs
View File

@@ -466,6 +466,9 @@ where
unimplemented!("Plonky3 does not support permutations")
}
Identity::Connect(..) => unimplemented!("Plonky3 does not support connections"),
Identity::PhantomPermutation(..) | Identity::PhantomLookup(..) => {
// phantom identities are only used in witgen
}
}
}
}

8
std/protocols/lookup.asm
View File

@@ -113,11 +113,9 @@ let lookup: Constr, expr -> () = constr |lookup_constraint, multiplicities| {
is_first * acc_2 = 0;
constrain_eq_ext(update_expr, from_base(0));
// Build an annotation for witness generation
let witgen_annotation = to_phantom_lookup(lookup_constraint, multiplicities);
// TODO: Adding it to the constraint set currently fails
// witgen_annotation;
// Add an annotation for witness generation
to_phantom_lookup(lookup_constraint, multiplicities);
// In the extension field, we need a prover function for the accumulator.
if needs_extension() {
// TODO: Helper columns, because we can't access the previous row in hints

31
test_data/std/lookup_via_challenges.asm
View File

@@ -1,25 +1,24 @@
use std::prelude::Query;
use std::convert::fe;
use std::protocols::lookup::lookup;
use std::math::fp2::from_base;
use std::prover::challenge;
machine Main with degree: 8 {
col fixed random_six = [1, 1, 1, 0, 1, 1, 1, 0];
col fixed first_seven = [1, 1, 1, 1, 1, 1, 1, 0];
col fixed a1 = [1, 2, 4, 3, 1, 1, 4, 1];
col fixed a2 = [1, 2, 4, 1, 1, 1, 4, 1];
col fixed a3 = [1, 2, 4, 1, 1, 1, 4, 3];
col witness b1, b2, b3;
query |i| {
std::prover::provide_value(b1, i, fe(i + 1));
std::prover::provide_value(b2, i, fe(i + 1));
std::prover::provide_value(b3, i, fe(i + 1));
};
col fixed m = [3, 1, 0, 2, 0, 0, 0, 0];
col fixed x = [1, 5, 2, 6, 4, 2, 6, 3];
col witness y;
let lookup_constraint = random_six $ [a1, a2, a3] in first_seven $ [b1, b2, b3];
// Pre-compute f(x) = x + 1 for all x in [1, 8]
col fixed INC_X = [1, 2, 3, 4, 5, 6, 7, 8];
col fixed INC_Y = [2, 3, 4, 5, 6, 7, 8, 9];
lookup(lookup_constraint, m);
}
// Machine extractor currently accepts the multiplicity column with exact the name of "m_logup_multiplicity"
col witness m_logup_multiplicity;
// This would be the correct multiplicity values that would satisfy the constraints:
//col fixed m_logup_multiplicity = [1, 2, 1, 1, 1, 2, 0, 0];
let lookup_constraint = [x, y] in [INC_X, INC_Y];
lookup(lookup_constraint, m_logup_multiplicity);
}

26
test_data/std/lookup_via_challenges_ext.asm
View File

@@ -1,26 +0,0 @@
use std::prelude::Query;
use std::convert::fe;
use std::protocols::lookup::lookup;
use std::protocols::lookup::compute_next_z;
use std::math::fp2::Fp2;
use std::prover::challenge;
machine Main with degree: 8 {
col fixed a_sel = [0, 1, 1, 1, 0, 1, 0, 0];
col fixed b_sel = [1, 1, 0, 1, 1, 1, 1, 0];
col fixed a1 = [16, 20, 22, 17, 16, 20, 4, 1];
col fixed a2 = [12, 5, 7, 2, 5, 5, 4, 1];
col fixed a3 = [20, 36, 38, 33, 36, 36, 4, 3];
col witness b1, b2, b3;
query |i| {
std::prover::provide_value(b1, i, fe(i + 16));
std::prover::provide_value(b2, i, fe(i + 1));
std::prover::provide_value(b3, i, fe(i + 32));
};
col fixed m = [0, 1, 0, 0, 2, 0, 1, 0];
let lookup_constraint = a_sel $ [a1, a2, a3] in b_sel $ [b1, b2, b3];
lookup(lookup_constraint, m);
}

19
test_data/std/lookup_via_challenges_ext_simple.asm
View File

@@ -1,19 +0,0 @@
use std::prelude::Query;
use std::convert::fe;
use std::protocols::lookup::lookup;
use std::protocols::lookup::compute_next_z;
use std::math::fp2::Fp2;
use std::prover::challenge;
machine Main with degree: 8 {
col fixed a = [1, 1, 4, 1, 1, 2, 1, 1];
let b;
query |i| {
std::prover::provide_value(b, i, fe(i + 1));
};
col fixed m = [6, 1, 0, 1, 0, 0, 0, 0];
let lookup_constraint = [a] in [b];
lookup(lookup_constraint, m);
}

19
test_data/std/lookup_via_challenges_range_constraint.asm Normal file
View File

@@ -0,0 +1,19 @@
use std::convert::fe;
use std::protocols::lookup::lookup;
use std::math::fp2::from_base;
use std::prover::challenge;
machine Main with degree: 8 {
// Prove a correct decomposition of x into 3-bit limbs
col fixed x = [1, 6, 23, 55, 63, 4, 1, 0];
col witness x_low, x_high;
col fixed BIT3 = [0, 1, 2, 3, 4, 5, 6, 7];
col witness m_low, m_high;
lookup([x_low] in [BIT3], m_low);
lookup([x_high] in [BIT3], m_high);
x = x_low + 8 * x_high;
}

28
test_data/std/multiplicities.asm
View File

@@ -1,28 +0,0 @@
use std::convert::fe;
use std::protocols::lookup::lookup;
use std::math::fp2::from_base;
use std::prover::challenge;
machine Main with degree: 8 {
col fixed x = [1, 5, 2, 6, 4, 2, 6, 3];
col witness y;
// Pre-compute f(x) = x + 1 for all x in [1, 8]
col fixed INC_X = [1, 2, 3, 4, 5, 6, 7, 8];
col fixed INC_Y = [2, 3, 4, 5, 6, 7, 8, 9];
// Native lookup to implement y = f(x). From this, witgen should
// figure out the values in column y via FixedLookup.
[x, y] in [INC_X, INC_Y];
// Machine extractor currently accepts the multiplicity column with exact the name of "m_logup_multiplicity"
col witness m_logup_multiplicity;
// This would be the correct multiplicity values that would satisfy the constraints:
//col fixed m_logup_multiplicity = [1, 2, 1, 1, 1, 2, 0, 0];
let lookup_constraint = [x, y] in [INC_X, INC_Y];
lookup(lookup_constraint, m_logup_multiplicity);
}