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

Allow different degrees in witgen #1460

Merged
merged 51 commits into from
Jul 4, 2024
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
51 commits
Select commit Hold shift + click to select a range
db92a63
wip
Schaeff Jun 19, 2024
3285424
make tests pass
Schaeff Jun 20, 2024
9507915
lint, fmt
Schaeff Jun 20, 2024
e9a7199
fix empty degree tests
Schaeff Jun 20, 2024
3231e2b
Merge branch 'main' of github.com:powdr-labs/powdr into allow-differe…
Schaeff Jun 24, 2024
591a0d8
use RawPolyID
Schaeff Jun 25, 2024
c9e0ebd
clean
Schaeff Jun 25, 2024
925611c
fix tests
Schaeff Jun 25, 2024
17da5ce
fix estark artifacts
Schaeff Jun 26, 2024
adadec7
use cbor
Schaeff Jun 26, 2024
ac851ab
Merge branch 'main' of github.com:powdr-labs/powdr into allow-differe…
Schaeff Jun 26, 2024
896a1dd
clippy
Schaeff Jun 26, 2024
9a23e31
commit file.. fmt lint
Schaeff Jun 26, 2024
9420d05
clean
Schaeff Jun 26, 2024
0f6ca05
fix polygon
Schaeff Jun 26, 2024
c3c1700
expect proving to fail
Schaeff Jun 26, 2024
22fe520
fix test
Schaeff Jun 26, 2024
625bf41
fmt
Schaeff Jun 26, 2024
e7091f8
commit two_proof.pil
Schaeff Jun 26, 2024
d3b8414
fix vec_median test
Schaeff Jun 26, 2024
0ececa4
pull main
Schaeff Jun 26, 2024
7ba9587
revert pil file
Schaeff Jun 26, 2024
62a0af7
fix btree test, pass correct degree to main machine generator
Schaeff Jun 27, 2024
5bc0ec0
simplify, thanks chris
Schaeff Jun 27, 2024
33cbb24
clean
Schaeff Jun 27, 2024
db94bf3
pull main
Schaeff Jun 27, 2024
0bab7ac
fix estark
Schaeff Jun 27, 2024
c71299b
lint
Schaeff Jun 27, 2024
9f22b82
fix common_degree
Schaeff Jun 27, 2024
5ad32e9
fix permutation test, remove empty p3 test
Schaeff Jun 27, 2024
09675a1
pull main
Schaeff Jun 27, 2024
311fb58
pull main
Schaeff Jun 28, 2024
ef455ac
lint
Schaeff Jun 28, 2024
d24017a
remove speed bump
Schaeff Jun 28, 2024
80a05ff
remove degree method
Schaeff Jun 28, 2024
b2dc1b2
pull main
Schaeff Jul 1, 2024
17158a5
clean
Schaeff Jul 1, 2024
890d239
clean
Schaeff Jul 1, 2024
f2f6d91
commit backend
Schaeff Jul 1, 2024
462eeb4
fix test
Schaeff Jul 1, 2024
3ada82b
Merge branch 'main' of github.com:powdr-labs/powdr into allow-differe…
Schaeff Jul 1, 2024
fa7157b
pull main
Schaeff Jul 1, 2024
a3dd473
fix lookup
Schaeff Jul 1, 2024
109408b
fix test
Schaeff Jul 1, 2024
9977a13
address review comments
Schaeff Jul 2, 2024
a0ff0ee
Merge branch 'main' of github.com:powdr-labs/powdr into allow-differe…
Schaeff Jul 2, 2024
ebb1561
fix condenser
Schaeff Jul 2, 2024
1803f93
Merge branch 'main' of github.com:powdr-labs/powdr into allow-differe…
Schaeff Jul 3, 2024
1048471
pull main
Schaeff Jul 3, 2024
4dbbe21
pull main
Schaeff Jul 3, 2024
3a0ccbe
fix empty pil test in p3
Schaeff Jul 4, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
make tests pass
  • Loading branch information
Schaeff committed Jun 20, 2024
commit 3285424f3e6ec0433fc8e939b8f64990603861bf
17 changes: 10 additions & 7 deletions ast/src/analyzed/display.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,18 +21,18 @@ use super::*;

impl<T: Display> Display for Analyzed<T> {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
let degree = self.degree.unwrap_or_default();
let mut current_namespace = AbsoluteSymbolPath::default();
let mut update_namespace = |name: &str, f: &mut Formatter<'_>| {
let mut update_namespace = |name: &str, degree: Option<DegreeType>, f: &mut Formatter<'_>| {
let mut namespace =
AbsoluteSymbolPath::default().join(SymbolPath::from_str(name).unwrap());
let name = namespace.pop().unwrap();
if namespace != current_namespace {
current_namespace = namespace;
writeln!(
f,
"namespace {}({degree});",
current_namespace.relative_to(&Default::default())
"namespace {}({});",
current_namespace.relative_to(&Default::default()),
degree.map(|d| d.to_string()).unwrap_or_default()
)?;
};
Ok((name, !current_namespace.is_empty()))
Expand All @@ -53,7 +53,7 @@ impl<T: Display> Display for Analyzed<T> {
// These are printed as part of the enum.
continue;
}
let (name, is_local) = update_namespace(name, f)?;
let (name, is_local) = update_namespace(name, symbol.degree, f)?;
match symbol.kind {
SymbolKind::Poly(_) => {
writeln_indented(f, format_poly(&name, symbol, definition))?;
Expand Down Expand Up @@ -110,7 +110,7 @@ impl<T: Display> Display for Analyzed<T> {
}
} else if let Some((symbol, definition)) = self.intermediate_columns.get(name) {
assert!(symbol.stage.is_none());
let (name, _) = update_namespace(name, f)?;
let (name, _) = update_namespace(name, symbol.degree, f)?;
assert_eq!(symbol.kind, SymbolKind::Poly(PolynomialType::Intermediate));
if let Some(length) = symbol.length {
writeln_indented(
Expand All @@ -130,7 +130,7 @@ impl<T: Display> Display for Analyzed<T> {
}
StatementIdentifier::PublicDeclaration(name) => {
let decl = &self.public_declarations[name];
let (name, is_local) = update_namespace(&decl.name, f)?;
let (name, is_local) = update_namespace(&decl.name, None, f)?;
writeln_indented_by(
f,
format_public_declaration(&name, decl),
Expand Down Expand Up @@ -485,6 +485,7 @@ mod test {
poly_id: super::PolyID {
id: 0,
ptype: super::PolynomialType::Committed,
degree: None,
},
next: false,
});
Expand All @@ -493,6 +494,7 @@ mod test {
poly_id: super::PolyID {
id: 1,
ptype: super::PolynomialType::Committed,
degree: None,
},
next: false,
});
Expand All @@ -501,6 +503,7 @@ mod test {
poly_id: super::PolyID {
id: 2,
ptype: super::PolynomialType::Committed,
degree: None,
},
next: false,
});
Expand Down
15 changes: 10 additions & 5 deletions ast/src/analyzed/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,8 +31,6 @@ pub enum StatementIdentifier {

#[derive(Debug, Clone, Default, Serialize, Deserialize, JsonSchema)]
pub struct Analyzed<T> {
/// The degree of all namespaces, which must match if provided. If no degrees are given, then `None`.
pub degree: Option<DegreeType>,
pub definitions: HashMap<String, (Symbol, Option<FunctionValueDefinition>)>,
pub public_declarations: HashMap<String, PublicDeclaration>,
pub intermediate_columns: HashMap<String, (Symbol, Vec<AlgebraicExpression<T>>)>,
Expand All @@ -45,10 +43,14 @@ pub struct Analyzed<T> {
}

impl<T> Analyzed<T> {
/// @returns the degree if any. Panics if there is none.
pub fn degree(&self) -> DegreeType {
self.degree.unwrap()
pub fn max_degree(&self) -> DegreeType {
self.definitions
.values()
.filter_map(|(symbol, _)| symbol.degree)
.max()
.unwrap()
}

/// @returns the number of committed polynomials (with multiplicities for arrays)
pub fn commitment_count(&self) -> usize {
self.declaration_type_count(PolynomialType::Committed)
Expand Down Expand Up @@ -466,6 +468,7 @@ impl Symbol {
PolyID {
id: self.id + i,
ptype,
degree: self.degree,
},
)
})
Expand Down Expand Up @@ -1152,6 +1155,7 @@ pub struct PolynomialReference {
pub struct PolyID {
pub id: u64,
pub ptype: PolynomialType,
pub degree: Option<DegreeType>,
Schaeff marked this conversation as resolved.
Show resolved Hide resolved
}

impl From<&Symbol> for PolyID {
Expand All @@ -1162,6 +1166,7 @@ impl From<&Symbol> for PolyID {
PolyID {
id: symbol.id,
ptype,
degree: symbol.degree,
}
}
}
Expand Down
6 changes: 3 additions & 3 deletions backend/src/estark/json_exporter/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -232,7 +232,7 @@ impl<'a, T: FieldElement> Exporter<'a, T> {
polType: None,
type_: symbol_kind_to_json_string(symbol.kind).to_string(),
id: id as usize,
polDeg: self.analyzed.degree() as usize,
polDeg: self.analyzed.max_degree() as usize,
isArray: symbol.is_array(),
elementType: None,
len: symbol.length.map(|l| l as usize),
Expand All @@ -251,7 +251,7 @@ impl<'a, T: FieldElement> Exporter<'a, T> {
polType: None,
type_: symbol_kind_to_json_string(symbol.kind).to_string(),
id: id as usize,
polDeg: self.analyzed.degree() as usize,
polDeg: self.analyzed.max_degree() as usize,
isArray: symbol.is_array(),
elementType: None,
len: symbol.length.map(|l| l as usize),
Expand Down Expand Up @@ -369,7 +369,7 @@ impl<'a, T: FieldElement> Exporter<'a, T> {

fn polynomial_reference_to_json(
&self,
PolyID { id, ptype }: PolyID,
PolyID { id, ptype, .. }: PolyID,
next: bool,
) -> (u32, StarkyExpr) {
let id = if ptype == PolynomialType::Intermediate {
Expand Down
4 changes: 2 additions & 2 deletions backend/src/estark/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ fn first_step_fixup<'a, F: FieldElement>(
pil: &'a Analyzed<F>,
fixed: &'a [(String, Vec<F>)],
) -> (PIL, Option<PatchedConstants<F>>) {
let degree = pil.degree();
let degree = pil.max_degree();

let mut pil: PIL = json_exporter::export(pil);

Expand Down Expand Up @@ -161,7 +161,7 @@ impl<'a, F: FieldElement> EStarkFilesCommon<'a, F> {
let proof_type: ProofType = ProofType::from(options);

Ok(EStarkFilesCommon {
degree: analyzed.degree(),
degree: analyzed.max_degree(),
pil,
patched_constants,
output_dir,
Expand Down
2 changes: 1 addition & 1 deletion backend/src/estark/starky_wrapper.rs
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ impl<F: FieldElement> BackendFactory<F> for Factory {

let proof_type: ProofType = ProofType::from(options);

let params = create_stark_struct(pil.degree(), proof_type.hash_type());
let params = create_stark_struct(pil.max_degree(), proof_type.hash_type());

let (pil_json, patched_fixed) = first_step_fixup(pil, fixed);

Expand Down
4 changes: 2 additions & 2 deletions backend/src/halo2/circuit_builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -272,7 +272,7 @@ impl<'a, T: FieldElement, F: PrimeField<Repr = [u8; 32]>> Circuit<F> for PowdrCi
let first_row = meta.query_advice(config.advice[name], Rotation::cur());
let last_row = meta.query_advice(
config.advice[name],
Rotation(analyzed.degree().try_into().unwrap()),
Rotation(analyzed.max_degree().try_into().unwrap()),
);
let expr = first_step.clone() * (first_row - last_row);
(format!("enforce wrapping ({name})"), expr)
Expand Down Expand Up @@ -411,7 +411,7 @@ impl<'a, T: FieldElement, F: PrimeField<Repr = [u8; 32]>> Circuit<F> for PowdrCi
)?;
}
}
let degree = self.analyzed.degree() as usize;
let degree = self.analyzed.max_degree() as usize;
for i in 0..(2 * degree) {
let value = F::from((i < degree) as u64);
region.assign_fixed(
Expand Down
2 changes: 1 addition & 1 deletion backend/src/halo2/mock_prover.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ pub fn mock_prove<T: FieldElement>(
// double the row count in order to make space for the cells introduced by the backend
// TODO: use a precise count of the extra rows needed to avoid using so many rows

let circuit_row_count_log = usize::BITS - pil.degree().leading_zeros();
let circuit_row_count_log = usize::BITS - pil.max_degree().leading_zeros();
let expanded_row_count_log = circuit_row_count_log + 1;

let circuit = PowdrCircuit::new(pil, constants)
Expand Down
8 changes: 4 additions & 4 deletions backend/src/halo2/prover.rs
Original file line number Diff line number Diff line change
Expand Up @@ -94,10 +94,10 @@ impl<'a, F: FieldElement> Halo2Prover<'a, F> {
let mut params = setup
.map(|mut setup| ParamsKZG::<Bn256>::read(&mut setup))
.transpose()?
.unwrap_or_else(|| generate_setup(analyzed.degree()));
.unwrap_or_else(|| generate_setup(analyzed.max_degree()));

if matches!(proof_type, ProofType::Poseidon | ProofType::SnarkSingle) {
params.downsize(degree_bits(analyzed.degree()));
params.downsize(degree_bits(analyzed.max_degree()));
}

Ok(Self {
Expand Down Expand Up @@ -250,7 +250,7 @@ impl<'a, F: FieldElement> Halo2Prover<'a, F> {
log::info!("Generating VK for app snark...");

let mut params_app = self.params.clone();
params_app.downsize(degree_bits(self.analyzed.degree()));
params_app.downsize(degree_bits(self.analyzed.max_degree()));

log::info!("Generating circuit for compression snark...");
let protocol_app = compile(
Expand Down Expand Up @@ -375,7 +375,7 @@ impl<'a, F: FieldElement> Halo2Prover<'a, F> {
};

let mut params_app = self.params.clone();
params_app.downsize(degree_bits(self.analyzed.degree()));
params_app.downsize(degree_bits(self.analyzed.max_degree()));

let protocol_app = compile(
&params_app,
Expand Down
36 changes: 18 additions & 18 deletions executor/src/constant_evaluator/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -186,7 +186,7 @@ mod test {
col fixed LAST(i) { if i == N - 1 { 1 } else { 0 } };
"#;
let analyzed = analyze_string(src);
assert_eq!(analyzed.degree(), 8);
assert_eq!(analyzed.max_degree(), 8);
let constants = generate(&analyzed);
assert_eq!(
constants,
Expand All @@ -202,7 +202,7 @@ mod test {
pol constant EVEN(i) { 2 * (i - 1) + 4 };
"#;
let analyzed = analyze_string(src);
assert_eq!(analyzed.degree(), 8);
assert_eq!(analyzed.max_degree(), 8);
let constants = generate(&analyzed);
assert_eq!(
constants,
Expand All @@ -221,7 +221,7 @@ mod test {
pol constant X(i) { i ^ (i + 17) | 3 };
"#;
let analyzed = analyze_string(src);
assert_eq!(analyzed.degree(), 8);
assert_eq!(analyzed.max_degree(), 8);
let constants = generate(&analyzed);
assert_eq!(
constants,
Expand All @@ -245,7 +245,7 @@ mod test {
} + 1 };
"#;
let analyzed = analyze_string(src);
assert_eq!(analyzed.degree(), 8);
assert_eq!(analyzed.max_degree(), 8);
let constants = generate(&analyzed);
assert_eq!(
constants,
Expand All @@ -261,7 +261,7 @@ mod test {
let X: col = |i| if i < 3 { 7 } else { 9 };
"#;
let analyzed = analyze_string(src);
assert_eq!(analyzed.degree(), 8);
assert_eq!(analyzed.max_degree(), 8);
let constants = generate(&analyzed);
assert_eq!(
constants,
Expand All @@ -278,7 +278,7 @@ mod test {
pol constant EVEN(i) { 2 * minus_one(i) + 2 };
"#;
let analyzed = analyze_string(src);
assert_eq!(analyzed.degree(), 8);
assert_eq!(analyzed.max_degree(), 8);
let constants = generate(&analyzed);
assert_eq!(
constants,
Expand All @@ -304,7 +304,7 @@ mod test {
col fixed doubled_half_nibble(i) { half_nibble_f(i / 2) };
"#;
let analyzed = analyze_string(src);
assert_eq!(analyzed.degree(), 10);
assert_eq!(analyzed.max_degree(), 10);
let constants = generate(&analyzed);
assert_eq!(constants.len(), 4);
assert_eq!(
Expand Down Expand Up @@ -346,7 +346,7 @@ mod test {
col fixed ref_other = [n-1, f(1), 8] + [0]*;
"#;
let analyzed = analyze_string(src);
assert_eq!(analyzed.degree(), 10);
assert_eq!(analyzed.max_degree(), 10);
let constants = generate(&analyzed);
assert_eq!(constants.len(), 3);
assert_eq!(
Expand Down Expand Up @@ -377,7 +377,7 @@ mod test {
col fixed arr = [0, 1, 2]* + [7];
"#;
let analyzed = analyze_string(src);
assert_eq!(analyzed.degree(), 10);
assert_eq!(analyzed.max_degree(), 10);
let constants = generate(&analyzed);
assert_eq!(constants.len(), 1);
assert_eq!(
Expand Down Expand Up @@ -412,7 +412,7 @@ mod test {
col fixed greater_eq(i) { if id(i) >= inv(i) { 1 } else { 0 } };
"#;
let analyzed = analyze_string(src);
assert_eq!(analyzed.degree(), 6);
assert_eq!(analyzed.max_degree(), 6);
let constants = generate(&analyzed);
assert_eq!(
constants[0],
Expand Down Expand Up @@ -471,7 +471,7 @@ mod test {
let x: col = |i| w(i) + 1;
"#;
let analyzed = analyze_string::<GoldilocksField>(src);
assert_eq!(analyzed.degree(), 10);
assert_eq!(analyzed.max_degree(), 10);
generate(&analyzed);
}

Expand All @@ -484,7 +484,7 @@ mod test {
let x = |i| w(i) + 1;
"#;
let analyzed = analyze_string::<GoldilocksField>(src);
assert_eq!(analyzed.degree(), 10);
assert_eq!(analyzed.max_degree(), 10);
generate(&analyzed);
}

Expand All @@ -498,7 +498,7 @@ mod test {
col fixed y = [1, 2, 3]*;
"#;
let analyzed = analyze_string::<GoldilocksField>(src);
assert_eq!(analyzed.degree(), 10);
assert_eq!(analyzed.max_degree(), 10);
generate(&analyzed);
}

Expand All @@ -513,7 +513,7 @@ mod test {
let Y: col = y;
"#;
let analyzed = analyze_string::<GoldilocksField>(src);
assert_eq!(analyzed.degree(), 4);
assert_eq!(analyzed.max_degree(), 4);
let constants = generate(&analyzed);
assert_eq!(
constants[0],
Expand All @@ -536,7 +536,7 @@ mod test {
let x: col = |i| (1 << (2000 + i)) >> 2000;
"#;
let analyzed = analyze_string::<GoldilocksField>(src);
assert_eq!(analyzed.degree(), 4);
assert_eq!(analyzed.max_degree(), 4);
let constants = generate(&analyzed);
assert_eq!(
constants[0],
Expand All @@ -556,7 +556,7 @@ mod test {
let x: col = |i| 100 + x_arr[i];
"#;
let analyzed = analyze_string::<GoldilocksField>(src);
assert_eq!(analyzed.degree(), 4);
assert_eq!(analyzed.max_degree(), 4);
let constants = generate(&analyzed);
// Semantics of p % q involving negative numbers:
// sgn(p) * |p| % |q|
Expand All @@ -576,7 +576,7 @@ mod test {
let fe = || fe();
"#;
let analyzed = analyze_string::<GoldilocksField>(src);
assert_eq!(analyzed.degree(), 4);
assert_eq!(analyzed.max_degree(), 4);
let constants = generate(&analyzed);
assert_eq!(
constants[0],
Expand All @@ -600,7 +600,7 @@ mod test {
let a: col = |i| std::convert::fe(i + seven) + seven;
"#;
let analyzed = analyze_string::<GoldilocksField>(src);
assert_eq!(analyzed.degree(), 4);
assert_eq!(analyzed.max_degree(), 4);
let constants = generate(&analyzed);
assert_eq!(
constants[0],
Expand Down
Loading
Loading