From 7f259b43c76ef281731a77da91b0abbbda909be6 Mon Sep 17 00:00:00 2001 From: Thibaut Schaeffer Date: Tue, 3 Sep 2024 14:37:44 +0200 Subject: [PATCH] Support degree ranges (#1667) We currently hardcode the range of degrees that variable degree machines are preprocessed for. Expose that in machines instead. This changes pil namespaces to accept a min and max degree: ``` namespace main(123..456); namespace main(5); // allowed for backward compatibility, translates to `5..5` ``` It adds two new builtins: ``` std::prover::min_degree std::prover::max_degree ``` And sets the behavior of the `std::prover::degree` builtin to only succeed if `min_degree` and `max_degree` are equal. --- analysis/src/machine_check.rs | 28 ++++- asm-to-pil/src/vm_to_constrained.rs | 17 +-- ast/src/analyzed/display.rs | 11 +- ast/src/analyzed/mod.rs | 77 ++++++++++++- ast/src/asm_analysis/display.rs | 29 ++++- ast/src/asm_analysis/mod.rs | 28 ++++- ast/src/object/display.rs | 4 +- ast/src/object/mod.rs | 18 ++- ast/src/parsed/asm.rs | 12 ++ ast/src/parsed/display.rs | 10 ++ ast/src/parsed/mod.rs | 29 +++-- backend/src/composite/mod.rs | 46 ++++---- backend/src/composite/split.rs | 18 +-- book/src/architecture/linker.md | 7 +- book/src/asm/degree_range.md | 6 + book/src/asm/machines.md | 4 +- book/src/pil/builtins.md | 6 +- executor/src/constant_evaluator/mod.rs | 106 ++++++++---------- executor/src/witgen/generator.rs | 4 +- executor/src/witgen/machines/block_machine.rs | 38 ++++--- .../machines/double_sorted_witness_machine.rs | 37 +++--- .../src/witgen/machines/machine_extractor.rs | 1 - .../witgen/machines/sorted_witness_machine.rs | 2 +- .../src/witgen/machines/write_once_memory.rs | 4 +- executor/src/witgen/mod.rs | 29 +---- executor/src/witgen/vm_processor.rs | 37 +++--- linker/Cargo.toml | 2 + linker/src/lib.rs | 71 +++++++++--- parser/src/powdr.lalrpop | 7 +- pil-analyzer/src/condenser.rs | 24 +++- pil-analyzer/src/evaluator.rs | 26 ++++- pil-analyzer/src/pil_analyzer.rs | 43 +++---- pil-analyzer/src/side_effect_checker.rs | 2 + pil-analyzer/src/statement_processor.rs | 7 +- pil-analyzer/src/type_builtins.rs | 2 + pil-analyzer/tests/condenser.rs | 16 ++- riscv/Cargo.toml | 1 + riscv/src/code_gen.rs | 7 +- riscv/src/continuations.rs | 45 +++++--- std/machines/binary.asm | 2 +- std/machines/shift.asm | 2 +- std/prover.asm | 6 +- test_data/pil/vm_to_block_dynamic_length.pil | 6 +- 43 files changed, 573 insertions(+), 304 deletions(-) create mode 100644 book/src/asm/degree_range.md diff --git a/analysis/src/machine_check.rs b/analysis/src/machine_check.rs index d23cb8e528..6ec580bd2b 100644 --- a/analysis/src/machine_check.rs +++ b/analysis/src/machine_check.rs @@ -6,8 +6,8 @@ use powdr_ast::{ asm_analysis::{ AnalysisASMFile, AssignmentStatement, CallableSymbolDefinitions, DebugDirective, FunctionBody, FunctionStatements, FunctionSymbol, InstructionDefinitionStatement, - InstructionStatement, Item, LabelStatement, LinkDefinition, Machine, OperationSymbol, - RegisterDeclarationStatement, RegisterTy, Return, SubmachineDeclaration, + InstructionStatement, Item, LabelStatement, LinkDefinition, Machine, MachineDegree, + OperationSymbol, RegisterDeclarationStatement, RegisterTy, Return, SubmachineDeclaration, }, parsed::{ self, @@ -172,11 +172,35 @@ impl TypeChecker { let MachineProperties { degree, + min_degree, + max_degree, latch, operation_id, call_selectors, } = machine.properties; + let degree = match (degree, min_degree, max_degree) { + (Some(d), None, None) => MachineDegree { + min: Some(d.clone()), + max: Some(d), + }, + (Some(d), Some(_), _) => { + errors.push("Machine {ctx} should not have a min_degree if it has a degree".into()); + MachineDegree { + min: Some(d.clone()), + max: Some(d), + } + } + (Some(d), _, Some(_)) => { + errors.push("Machine {ctx} should not have a max_degree if it has a degree".into()); + MachineDegree { + min: Some(d.clone()), + max: Some(d), + } + } + (None, min, max) => MachineDegree { min, max }, + }; + if !registers.iter().any(|r| r.ty.is_pc()) { let operation_count = callable.operation_definitions().count(); if operation_count > 0 && latch.is_none() { diff --git a/asm-to-pil/src/vm_to_constrained.rs b/asm-to-pil/src/vm_to_constrained.rs index efd7d82434..86cc957fc9 100644 --- a/asm-to-pil/src/vm_to_constrained.rs +++ b/asm-to-pil/src/vm_to_constrained.rs @@ -9,8 +9,8 @@ use powdr_ast::{ asm_analysis::{ combine_flags, AssignmentStatement, Batch, CallableSymbol, CallableSymbolDefinitions, DebugDirective, FunctionStatement, InstructionDefinitionStatement, InstructionStatement, - LabelStatement, LinkDefinition, Machine, OperationSymbol, RegisterDeclarationStatement, - RegisterTy, Rom, + LabelStatement, LinkDefinition, Machine, MachineDegree, OperationSymbol, + RegisterDeclarationStatement, RegisterTy, Rom, }, parsed::{ self, @@ -62,12 +62,12 @@ pub const ROM_SUBMACHINE_NAME: &str = "_rom"; const ROM_ENTRY_POINT: &str = "get_line"; fn rom_machine<'a>( - degree: Expression, + degree: MachineDegree, mut pil: Vec, mut line_lookup: impl Iterator, ) -> Machine { Machine { - degree: Some(degree), + degree, operation_id: Some(ROM_OPERATION_ID.into()), latch: Some(ROM_LATCH.into()), pil: { @@ -283,10 +283,11 @@ impl VMConverter { // This is hacky: in the absence of proof objects, we want to support both monolithic proofs and composite proofs. // In the monolithic case, all degrees must be the same, so we align the degree of the rom to that of the vm. // In the composite case, we set the minimum degree for the rom, which is the number of lines in the code. - let rom_degree = input - .degree - .clone() - .unwrap_or_else(|| Expression::from(self.code_lines.len().next_power_of_two() as u32)); + // this can lead to false negatives as we apply expression equality here, so `4` and `2 + 2` would be considered different. + let rom_degree = match input.degree.is_static() { + true => input.degree.clone(), + false => Expression::from(self.code_lines.len().next_power_of_two() as u32).into(), + }; ( input, diff --git a/ast/src/analyzed/display.rs b/ast/src/analyzed/display.rs index 50321604ba..1438352094 100644 --- a/ast/src/analyzed/display.rs +++ b/ast/src/analyzed/display.rs @@ -20,11 +20,20 @@ use self::parsed::{ use super::*; +impl Display for DegreeRange { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + match (self.min, self.max) { + (min, max) if min == max => write!(f, "{min}"), + (min, max) => write!(f, "{min}..{max}"), + } + } +} + impl Display for Analyzed { fn fmt(&self, f: &mut Formatter<'_>) -> Result { let (mut current_namespace, mut current_degree) = (AbsoluteSymbolPath::default(), None); let mut update_namespace = - |name: &str, degree: Option, f: &mut Formatter<'_>| { + |name: &str, degree: Option, f: &mut Formatter<'_>| { let mut namespace = AbsoluteSymbolPath::default().join(SymbolPath::from_str(name).unwrap()); let name = namespace.pop().unwrap(); diff --git a/ast/src/analyzed/mod.rs b/ast/src/analyzed/mod.rs index b4a126c3a7..98fa194d70 100644 --- a/ast/src/analyzed/mod.rs +++ b/ast/src/analyzed/mod.rs @@ -59,6 +59,15 @@ impl Analyzed { .unique() .exactly_one() .unwrap() + .try_into_unique() + .unwrap() + } + + pub fn degree_ranges(&self) -> HashSet { + self.definitions + .values() + .filter_map(|(symbol, _)| symbol.degree) + .collect::>() } /// Returns the set of all explicit degrees in this [`Analyzed`]. @@ -66,6 +75,7 @@ impl Analyzed { self.definitions .values() .filter_map(|(symbol, _)| symbol.degree) + .map(|d| d.try_into_unique().unwrap()) .collect::>() } @@ -495,6 +505,44 @@ pub fn type_from_definition( } } +#[derive(PartialEq, Eq, Hash, Debug, Clone, Serialize, Deserialize, JsonSchema, Copy)] +pub struct DegreeRange { + pub min: DegreeType, + pub max: DegreeType, +} + +impl From for DegreeRange { + fn from(value: DegreeType) -> Self { + Self { + min: value, + max: value, + } + } +} + +impl DegreeRange { + pub fn try_into_unique(self) -> Option { + (self.min == self.max).then_some(self.min) + } + + /// Iterate through powers of two in this range + pub fn iter(&self) -> impl Iterator { + let min_ceil = self.min.next_power_of_two(); + let max_ceil = self.max.next_power_of_two(); + let min_log = usize::BITS - min_ceil.leading_zeros() - 1; + let max_log = usize::BITS - max_ceil.leading_zeros() - 1; + (min_log..=max_log).map(|exponent| 1 << exponent) + } + + /// Fit a degree to this range: + /// - returns the smallest value in the range which is larger or equal to `new_degree` + /// - panics if no such value exists + pub fn fit(&self, new_degree: u64) -> u64 { + assert!(new_degree <= self.max); + self.min.max(new_degree) + } +} + #[derive(Debug, Clone, Serialize, Deserialize, JsonSchema)] pub struct Symbol { pub id: u64, @@ -502,8 +550,8 @@ pub struct Symbol { pub absolute_name: String, pub stage: Option, pub kind: SymbolKind, - pub length: Option, - pub degree: Option, + pub length: Option, + pub degree: Option, } impl Symbol { @@ -1306,9 +1354,10 @@ impl Display for PolynomialType { #[cfg(test)] mod tests { + use powdr_number::DegreeType; use powdr_parser_util::SourceRef; - use crate::analyzed::{AlgebraicReference, PolyID, PolynomialType}; + use crate::analyzed::{AlgebraicReference, DegreeRange, PolyID, PolynomialType}; use super::{AlgebraicExpression, Analyzed}; @@ -1380,4 +1429,26 @@ mod tests { let expr = column.clone() * column.clone() * column.clone(); assert_eq!(expr.degree(), 3); } + + #[test] + fn degree_range() { + assert_eq!( + DegreeRange { min: 4, max: 4 }.iter().collect::>(), + vec![4] + ); + assert_eq!( + DegreeRange { min: 4, max: 16 }.iter().collect::>(), + vec![4, 8, 16] + ); + assert_eq!( + DegreeRange { min: 3, max: 15 }.iter().collect::>(), + vec![4, 8, 16] + ); + assert_eq!( + DegreeRange { min: 15, max: 3 } + .iter() + .collect::>(), + Vec::::new() + ); + } } diff --git a/ast/src/asm_analysis/display.rs b/ast/src/asm_analysis/display.rs index d64ff1123a..d36cd49c17 100644 --- a/ast/src/asm_analysis/display.rs +++ b/ast/src/asm_analysis/display.rs @@ -20,7 +20,7 @@ use super::{ AnalysisASMFile, AssignmentStatement, CallableSymbol, CallableSymbolDefinitionRef, DebugDirective, FunctionBody, FunctionStatement, FunctionStatements, Incompatible, IncompatibleSet, InstructionDefinitionStatement, InstructionStatement, Item, LabelStatement, - LinkDefinition, Machine, RegisterDeclarationStatement, RegisterTy, Return, Rom, + LinkDefinition, Machine, MachineDegree, RegisterDeclarationStatement, RegisterTy, Return, Rom, SubmachineDeclaration, }; @@ -76,13 +76,30 @@ impl Display for AnalysisASMFile { } } +impl Display for MachineDegree { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + match (&self.min, &self.max) { + (Some(min), Some(max)) if min == max => write!(f, "degree: {min}"), + (min, max) => write!( + f, + "{}", + min.iter() + .map(|min_degree| format!("min_degree: {min_degree}")) + .chain( + max.iter() + .map(|max_degree| format!("max_degree: {max_degree}")), + ) + .collect::>() + .join(", ") + ), + } + } +} + impl Display for Machine { fn fmt(&self, f: &mut Formatter<'_>) -> Result { - let props = self - .degree - .as_ref() - .map(|s| format!("degree: {s}")) - .into_iter() + let props = std::iter::once(&self.degree) + .map(|d| format!("{d}")) .chain(self.latch.as_ref().map(|s| format!("latch: {s}"))) .chain( self.operation_id diff --git a/ast/src/asm_analysis/mod.rs b/ast/src/asm_analysis/mod.rs index 8cbefd8803..d485931a6e 100644 --- a/ast/src/asm_analysis/mod.rs +++ b/ast/src/asm_analysis/mod.rs @@ -697,10 +697,32 @@ impl Item { } } -#[derive(Clone, Default, Debug)] +#[derive(Default, Debug, PartialEq, Eq, PartialOrd, Ord, Clone)] +pub struct MachineDegree { + pub min: Option, + pub max: Option, +} + +impl MachineDegree { + pub fn is_static(&self) -> bool { + // we use expression equality here, so `2 + 2 != 4` + matches!((&self.min, &self.max), (Some(min), Some(max)) if min == max) + } +} + +impl From for MachineDegree { + fn from(value: Expression) -> Self { + Self { + min: Some(value.clone()), + max: Some(value), + } + } +} + +#[derive(Clone, Debug, Default)] pub struct Machine { - /// The degree if any, i.e. the number of rows in instances of this machine type - pub degree: Option, + /// The degree i.e. the number of rows in instances of this machine type + pub degree: MachineDegree, /// The latch, i.e. the boolean column whose values must be 1 in order for this machine to be accessed. Must be defined in one of the constraint blocks of this machine. pub latch: Option, /// The operation id, i.e. the column whose values determine which operation is being invoked in the current block. Must be defined in one of the constraint blocks of this machine. diff --git a/ast/src/object/display.rs b/ast/src/object/display.rs index b31bb1a61d..f728b1b305 100644 --- a/ast/src/object/display.rs +++ b/ast/src/object/display.rs @@ -43,9 +43,7 @@ impl Display for PILGraph { impl Display for Object { fn fmt(&self, f: &mut Formatter<'_>) -> Result { - if let Some(degree) = self.degree.as_ref() { - writeln!(f, "// Degree {degree}")?; - } + writeln!(f, "// Degree {}", self.degree)?; for s in &self.pil { writeln!(f, "{s}")?; } diff --git a/ast/src/object/mod.rs b/ast/src/object/mod.rs index 757e5e7fe6..f8f78f52c9 100644 --- a/ast/src/object/mod.rs +++ b/ast/src/object/mod.rs @@ -2,9 +2,12 @@ use std::collections::BTreeMap; use powdr_number::BigUint; -use crate::parsed::{ - asm::{AbsoluteSymbolPath, CallableParams, OperationParams}, - EnumDeclaration, Expression, PilStatement, TypedExpression, +use crate::{ + asm_analysis::MachineDegree, + parsed::{ + asm::{AbsoluteSymbolPath, CallableParams, OperationParams}, + EnumDeclaration, Expression, PilStatement, TypedExpression, + }, }; mod display; @@ -52,7 +55,7 @@ pub enum TypeOrExpression { #[derive(Default, Clone)] pub struct Object { - pub degree: Option, + pub degree: MachineDegree, /// the pil identities for this machine pub pil: Vec, /// the links from this machine to its children @@ -65,13 +68,6 @@ pub struct Object { pub has_pc: bool, } -impl Object { - pub fn with_degree>(mut self, degree: Option) -> Self { - self.degree = degree.map(Into::into); - self - } -} - #[derive(Clone, Debug)] /// A link between two machines pub struct Link { diff --git a/ast/src/parsed/asm.rs b/ast/src/parsed/asm.rs index cfa9e12533..7d7e4d51b3 100644 --- a/ast/src/parsed/asm.rs +++ b/ast/src/parsed/asm.rs @@ -440,6 +440,8 @@ impl MachineParams { #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Default, Clone)] pub struct MachineProperties { pub degree: Option, + pub min_degree: Option, + pub max_degree: Option, pub latch: Option, pub operation_id: Option, pub call_selectors: Option, @@ -463,6 +465,16 @@ impl MachineProperties { already_defined = true; } } + "min_degree" => { + if props.min_degree.replace(value).is_some() { + already_defined = true; + } + } + "max_degree" => { + if props.max_degree.replace(value).is_some() { + already_defined = true; + } + } "latch" => { let id = value.try_to_identifier().ok_or_else(|| { source_ref.with_error(format!( diff --git a/ast/src/parsed/display.rs b/ast/src/parsed/display.rs index e66430f413..2390f702d2 100644 --- a/ast/src/parsed/display.rs +++ b/ast/src/parsed/display.rs @@ -453,6 +453,16 @@ pub fn quote(input: &str) -> String { format!("\"{}\"", input.escape_default()) } +impl Display for NamespaceDegree { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + if self.min == self.max { + write!(f, "{}", self.min) + } else { + write!(f, "{}..{}", self.min, self.max) + } + } +} + impl Display for PilStatement { fn fmt(&self, f: &mut Formatter<'_>) -> Result { match self { diff --git a/ast/src/parsed/mod.rs b/ast/src/parsed/mod.rs index 1e60cea281..535caad481 100644 --- a/ast/src/parsed/mod.rs +++ b/ast/src/parsed/mod.rs @@ -58,12 +58,28 @@ impl SymbolCategory { #[derive(Debug, PartialEq, Eq, Clone)] pub struct PILFile(pub Vec); +#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)] +pub struct NamespaceDegree { + pub min: Expression, + pub max: Expression, +} + +impl Children for NamespaceDegree { + fn children(&self) -> Box + '_> { + Box::new(once(&self.min).chain(once(&self.max))) + } + + fn children_mut(&mut self) -> Box + '_> { + Box::new(once(&mut self.min).chain(once(&mut self.max))) + } +} + #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)] pub enum PilStatement { /// File name Include(SourceRef, String), /// Name of namespace and optional polynomial degree (constant) - Namespace(SourceRef, SymbolPath, Option), + Namespace(SourceRef, SymbolPath, Option), LetStatement( SourceRef, String, @@ -184,9 +200,8 @@ impl Children for PilStatement { PilStatement::ConnectIdentity(_start, left, right) => { Box::new(left.iter().chain(right.iter())) } - PilStatement::Expression(_, e) | PilStatement::Namespace(_, _, Some(e)) => { - Box::new(once(e)) - } + PilStatement::Expression(_, e) => Box::new(once(e)), + PilStatement::Namespace(_, _, Some(d)) => d.children(), PilStatement::PolynomialDefinition(_, PolynomialName { array_size, .. }, e) => { Box::new(array_size.iter().chain(once(e))) } @@ -223,10 +238,8 @@ impl Children for PilStatement { PilStatement::ConnectIdentity(_start, left, right) => { Box::new(left.iter_mut().chain(right.iter_mut())) } - PilStatement::Expression(_, e) | PilStatement::Namespace(_, _, Some(e)) => { - Box::new(once(e)) - } - + PilStatement::Expression(_, e) => Box::new(once(e)), + PilStatement::Namespace(_, _, Some(d)) => d.children_mut(), PilStatement::PolynomialDefinition(_, PolynomialName { array_size, .. }, e) => { Box::new(array_size.iter_mut().chain(once(e))) } diff --git a/backend/src/composite/mod.rs b/backend/src/composite/mod.rs index b9ed8de25f..92032a52bc 100644 --- a/backend/src/composite/mod.rs +++ b/backend/src/composite/mod.rs @@ -215,35 +215,26 @@ pub(crate) struct CompositeBackend { /// Panics if the machine PIL contains definitions with different degrees, or if the machine /// already has a degree set that is different from the provided degree. fn set_size(pil: Arc>, degree: DegreeType) -> Arc> { - let current_degrees = pil.degrees(); + let current_ranges = pil.degree_ranges(); assert!( - current_degrees.len() <= 1, + current_ranges.len() <= 1, "Expected at most one degree within a machine" ); - - match current_degrees.iter().next() { - None => { - // Clone the PIL and set the degree for all definitions - let pil = (*pil).clone(); - let definitions = pil - .definitions - .into_iter() - .map(|(name, (mut symbol, def))| { - symbol.degree = Some(degree); - (name, (symbol, def)) - }) - .collect(); - Arc::new(Analyzed { definitions, ..pil }) - } - Some(existing_degree) => { - // Keep the the PIL as is - assert_eq!( - existing_degree, °ree, - "Expected all definitions within a machine to have the same degree" - ); - pil - } - } + // Clone the PIL and set the degree for all polynomial definitions + let pil = (*pil).clone(); + let definitions = pil + .definitions + .into_iter() + .map(|(name, (mut symbol, def))| { + if let Some(range) = symbol.degree.as_mut() { + assert!(degree <= range.max); + assert!(degree >= range.min); + *range = degree.into(); + }; + (name, (symbol, def)) + }) + .collect(); + Arc::new(Analyzed { definitions, ..pil }) } mod sub_prover; @@ -272,7 +263,8 @@ fn process_witness_for_machine( .map(|(_, witness)| witness.len()) .unique() .exactly_one() - .expect("All witness columns of a machine must have the same size"); + .expect("All witness columns of a machine must have the same size") + as DegreeType; (witness, size as DegreeType) } diff --git a/backend/src/composite/split.rs b/backend/src/composite/split.rs index 631e0057c3..b19de6debb 100644 --- a/backend/src/composite/split.rs +++ b/backend/src/composite/split.rs @@ -15,7 +15,7 @@ use powdr_ast::{ visitor::{ExpressionVisitable, VisitOrder}, }, }; -use powdr_executor::constant_evaluator::{VariablySizedColumn, MAX_DEGREE_LOG, MIN_DEGREE_LOG}; +use powdr_executor::constant_evaluator::VariablySizedColumn; use powdr_number::{DegreeType, FieldElement}; const DUMMY_COLUMN_NAME: &str = "__dummy"; @@ -90,19 +90,13 @@ pub(crate) fn machine_fixed_columns( ); let sizes = sizes.into_iter().next().unwrap_or_else(|| { - // There is no fixed column with a set size. So either the PIL has a degree, or we - // assume all possible degrees. - let machine_degrees = machine_pil.degrees(); + let machine_degree_ranges = machine_pil.degree_ranges(); assert!( - machine_degrees.len() <= 1, - "All fixed columns of a machine must have the same sizes" + machine_degree_ranges.len() <= 1, + "All fixed columns of a machine must have the same size range" ); - match machine_degrees.iter().next() { - Some(°ree) => iter::once(degree).collect(), - None => (MIN_DEGREE_LOG..=*MAX_DEGREE_LOG) - .map(|log_size| (1 << log_size) as DegreeType) - .collect(), - } + let range = machine_degree_ranges.iter().next().unwrap(); + range.iter().collect() }); sizes diff --git a/book/src/architecture/linker.md b/book/src/architecture/linker.md index 57fb2cd1a7..d756656228 100644 --- a/book/src/architecture/linker.md +++ b/book/src/architecture/linker.md @@ -4,13 +4,14 @@ A linker is used to turn an [AIR tree](./compiler.md#air-generation) into a sing The linking process operates in the following way: 1. Create an empty PIL file -2. Start from the main AIR. Let `optional_main_degree` be its optional degree. +2. Start from the main AIR. Let `main_degree_range` be its degree after replacing any unspecified bounds with a default value. If `main_degree_range` is a single value, we are in the monolithic case. Otherwise, we're in the composite case. 3. For each AIR 1. Create a new namespace in the PIL file - 2. If a degree is defined, set it as the namespace degree. If no degree is defined, set the namespace degree to `optional_main_degree` + 2a. In the monolithic case, set the namespace degree to `main_degree_range` + 2b. In the composite case, set the namespace degree to that of the AIR, replacing any unspecified bounds with a default value 3. Add the constraints to the namespace 4. Turn the links into lookups and add them to the namespace The result is a monolithic AIR where: - each machine instance is a namespace -- each namespace defines its own optional degree \ No newline at end of file +- each namespace defines its own degree range \ No newline at end of file diff --git a/book/src/asm/degree_range.md b/book/src/asm/degree_range.md new file mode 100644 index 0000000000..a23d2f1c2a --- /dev/null +++ b/book/src/asm/degree_range.md @@ -0,0 +1,6 @@ +# Degree range + +Machines can specify the number of steps they run for. Three parameters come into play: +- `min_degree` expresses that the machine will run for a minimum of `min_degree` steps, included +- `max_degree` expresses that the machine will run for a maximum of `max_degree` steps, included +- `degree` is a shortcut to set `min_degree` and `max_degree` to the same value \ No newline at end of file diff --git a/book/src/asm/machines.md b/book/src/asm/machines.md index 682851fa6f..533dd3c2fc 100644 --- a/book/src/asm/machines.md +++ b/book/src/asm/machines.md @@ -5,7 +5,7 @@ Machines are the first main concept in powdr-asm. They can currently be of two t ## Virtual machines Dynamic machines are defined by: -- a degree, indicating the number of execution steps +- a [degree range](./degree_range.md), indicating the number of execution steps - a set of [registers](./registers.md), including a program counter - an [instruction set](./instructions.md) - a set of [powdr-pil](../pil/) statements @@ -23,7 +23,7 @@ An example of a simple dynamic machine is the following: Constrained machines are a lower-level type of machine. They do not have registers, and instead rely on simple committed and fixed columns. They are used to implement hand-optimized computation. They are defined by: -- a degree, indicating the number of execution steps +- a [degree range](./degree_range.md), indicating the number of execution steps - a set of [operations](./operations.md) - an `operation_identifier` column, used to make constraints conditional over which function is called. It can be omitted with `_` if the machine has at most one operation. - a `latch` column, used to identify rows at which the machine can be accessed from the outside (where the inputs and outputs are passed). It can be omitted if the machine has no operations. diff --git a/book/src/pil/builtins.md b/book/src/pil/builtins.md index b8fe3c3f83..6aa3faaad8 100644 --- a/book/src/pil/builtins.md +++ b/book/src/pil/builtins.md @@ -155,11 +155,13 @@ If you want two challenges to be different, you have to choose different IDs. ### Degree ```rust +let std::prover::min_degree: -> int +let std::prover::max_degree: -> int let std::prover::degree: -> int ``` -Returns the current number of rows / the length of the witness columns, also -known as the degree. +Returns the number of rows / the length of the witness columns, also +known as the degree. Outside of fixed column definitions, `degree` fails if `min_degree` and `max_degree` are different. ### Hints diff --git a/executor/src/constant_evaluator/mod.rs b/executor/src/constant_evaluator/mod.rs index 2b109e4c9c..71f8b82d3a 100644 --- a/executor/src/constant_evaluator/mod.rs +++ b/executor/src/constant_evaluator/mod.rs @@ -1,12 +1,10 @@ use std::{ collections::{BTreeMap, HashMap}, - env, sync::{Arc, RwLock}, }; pub use data_structures::{get_uniquely_sized, get_uniquely_sized_cloned, VariablySizedColumn}; use itertools::Itertools; -use lazy_static::lazy_static; use powdr_ast::{ analyzed::{Analyzed, FunctionValueDefinition, Symbol, TypedExpression}, parsed::{ @@ -20,24 +18,6 @@ use rayon::prelude::{IntoParallelIterator, ParallelIterator}; mod data_structures; -pub const MIN_DEGREE_LOG: usize = 5; -lazy_static! { - // The maximum degree can add a significant cost during setup, because - // the fixed columns need to be committed to in all sizes up to the max degree. - // This gives the user the possibility to overwrite the default value. - pub static ref MAX_DEGREE_LOG: usize = { - let default_max_degree_log = 22; - - let max_degree_log = match env::var("MAX_DEGREE_LOG") { - Ok(val) => val.parse::().unwrap(), - Err(_) => default_max_degree_log, - }; - log::info!("For variably-sized machine, the maximum degree is 2^{max_degree_log}. \ - You can set the environment variable MAX_DEGREE_LOG to change this value."); - max_degree_log - }; -} - /// Generates the fixed column values for all fixed columns that are defined /// (and not just declared). /// @returns the names (in source order) and the values for the columns. @@ -51,17 +31,12 @@ pub fn generate(analyzed: &Analyzed) -> Vec<(String, Variabl // for non-arrays, set index to None. for (index, (name, id)) in poly.array_elements().enumerate() { let index = poly.is_array().then_some(index as u64); - let values = if let Some(degree) = poly.degree { - generate_values(analyzed, degree, &name, value, index).into() - } else { - (MIN_DEGREE_LOG..=*MAX_DEGREE_LOG) - .map(|degree_log| { - let degree = 1 << degree_log; - generate_values(analyzed, degree, &name, value, index) - }) - .collect::>() - .into() - }; + let range = poly.degree.unwrap(); + let values = range + .iter() + .map(|degree| generate_values(analyzed, degree, &name, value, index)) + .collect::>() + .into(); assert!(fixed_cols.insert(name, (id, values)).is_none()); } } @@ -344,7 +319,7 @@ mod test { #[test] fn poly_call() { let src = r#" - let N = 10; + let N = 16; namespace std::convert(N); let int = []; namespace F(N); @@ -356,35 +331,35 @@ 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.degree(), 16); let constants = generate(&analyzed); assert_eq!(constants.len(), 4); assert_eq!( constants[0], ( "F::seq".to_string(), - convert((0..=9i32).collect::>()) + convert((0..=15i32).collect::>()) ) ); assert_eq!( constants[1], ( "F::double_plus_one".to_string(), - convert([1i32, 3, 5, 7, 9, 1, 3, 5, 7, 9].to_vec()) + convert([1i32, 3, 5, 7, 9, 11, 13, 15, 1, 3, 5, 7, 9, 11, 13, 15].to_vec()) ) ); assert_eq!( constants[2], ( "F::half_nibble".to_string(), - convert([0i32, 1, 2, 3, 4, 5, 6, 7, 0, 1].to_vec()) + convert([0i32, 1, 2, 3, 4, 5, 6, 7, 0, 1, 2, 3, 4, 5, 6, 7].to_vec()) ) ); assert_eq!( constants[3], ( "F::doubled_half_nibble".to_string(), - convert([0i32, 0, 1, 1, 2, 2, 3, 3, 4, 4].to_vec()) + convert([0i32, 0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6, 7, 7].to_vec()) ) ); } @@ -392,7 +367,7 @@ mod test { #[test] fn arrays() { let src = r#" - let N: int = 10; + let N: int = 8; let n: fe = 10; namespace F(N); let f = |i| i + 20; @@ -401,25 +376,25 @@ 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.degree(), 8); let constants = generate(&analyzed); assert_eq!(constants.len(), 3); assert_eq!( constants[0], ( "F::alt".to_string(), - convert([0i32, 1, 0, 1, 0, 1, 0, 0, 0, 0].to_vec()) + convert([0i32, 1, 0, 1, 0, 1, 0, 0].to_vec()) ) ); assert_eq!( constants[1], - ("F::empty".to_string(), convert([0i32; 10].to_vec())) + ("F::empty".to_string(), convert([0i32; 8].to_vec())) ); assert_eq!( constants[2], ( "F::ref_other".to_string(), - convert([9i32, 21, 8, 0, 0, 0, 0, 0, 0, 0].to_vec()) + convert([9i32, 21, 8, 0, 0, 0, 0, 0].to_vec()) ) ); } @@ -427,19 +402,19 @@ mod test { #[test] fn repetition_front() { let src = r#" - let N: int = 10; + let N: int = 8; namespace F(N); col fixed arr = [0, 1, 2]* + [7]; "#; let analyzed = analyze_string(src); - assert_eq!(analyzed.degree(), 10); + assert_eq!(analyzed.degree(), 8); let constants = generate(&analyzed); assert_eq!(constants.len(), 1); assert_eq!( constants[0], ( "F::arr".to_string(), - convert([0i32, 1, 2, 0, 1, 2, 0, 1, 2, 7].to_vec()) + convert([0i32, 1, 2, 0, 1, 2, 0, 7].to_vec()) ) ); } @@ -447,15 +422,15 @@ mod test { #[test] fn comparisons() { let src = r#" - let N: int = 6; + let N: int = 8; namespace std::convert(N); let int = 9; let fe = 8; namespace F(N); let id = |i| i; let inv = |i| N - i; - let a: int -> int = |i| [0, 1, 0, 1, 2, 1][i]; - let b: int -> int = |i| [0, 0, 1, 1, 0, 5][i]; + let a: int -> int = |i| [0, 1, 0, 1, 2, 1, 1, 1][i]; + let b: int -> int = |i| [0, 0, 1, 1, 0, 5, 5, 5][i]; col fixed or(i) { if (a(i) != 0) || (b(i) != 0) { 1 } else { 0 } }; col fixed and(i) { if (a(i) != 0) && (b(i) != 0) { 1 } else { 0 } }; col fixed not(i) { if !(a(i) != 0) { 1 } else { 0 } }; @@ -467,54 +442,69 @@ 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.degree(), 8); let constants = generate(&analyzed); assert_eq!( constants[0], - ("F::or".to_string(), convert([0, 1, 1, 1, 1, 1].to_vec())) + ( + "F::or".to_string(), + convert([0, 1, 1, 1, 1, 1, 1, 1].to_vec()) + ) ); assert_eq!( constants[1], - ("F::and".to_string(), convert([0, 0, 0, 1, 0, 1].to_vec())) + ( + "F::and".to_string(), + convert([0, 0, 0, 1, 0, 1, 1, 1].to_vec()) + ) ); assert_eq!( constants[2], - ("F::not".to_string(), convert([1, 0, 1, 0, 0, 0].to_vec())) + ( + "F::not".to_string(), + convert([1, 0, 1, 0, 0, 0, 0, 0].to_vec()) + ) ); assert_eq!( constants[3], - ("F::less".to_string(), convert([1, 1, 1, 0, 0, 0].to_vec())) + ( + "F::less".to_string(), + convert([1, 1, 1, 1, 0, 0, 0, 0].to_vec()) + ) ); assert_eq!( constants[4], ( "F::less_eq".to_string(), - convert([1, 1, 1, 1, 0, 0].to_vec()) + convert([1, 1, 1, 1, 1, 0, 0, 0].to_vec()) ) ); assert_eq!( constants[5], - ("F::eq".to_string(), convert([0, 0, 0, 1, 0, 0].to_vec())) + ( + "F::eq".to_string(), + convert([0, 0, 0, 0, 1, 0, 0, 0].to_vec()) + ) ); assert_eq!( constants[6], ( "F::not_eq".to_string(), - convert([1, 1, 1, 0, 1, 1].to_vec()) + convert([1, 1, 1, 1, 0, 1, 1, 1].to_vec()) ) ); assert_eq!( constants[7], ( "F::greater".to_string(), - convert([0, 0, 0, 0, 1, 1].to_vec()) + convert([0, 0, 0, 0, 0, 1, 1, 1].to_vec()) ) ); assert_eq!( constants[8], ( "F::greater_eq".to_string(), - convert([0, 0, 0, 1, 1, 1].to_vec()) + convert([0, 0, 0, 0, 1, 1, 1, 1].to_vec()) ) ); } diff --git a/executor/src/witgen/generator.rs b/executor/src/witgen/generator.rs index 9006427e52..f4c5ad5f87 100644 --- a/executor/src/witgen/generator.rs +++ b/executor/src/witgen/generator.rs @@ -98,7 +98,6 @@ impl<'a, T: FieldElement> Machine<'a, T> for Generator<'a, T> { impl<'a, T: FieldElement> Generator<'a, T> { pub fn new( name: String, - degree: DegreeType, fixed_data: &'a FixedData<'a, T>, connecting_identities: &BTreeMap>, identities: Vec<&'a Identity>, @@ -108,7 +107,7 @@ impl<'a, T: FieldElement> Generator<'a, T> { let data = FinalizableData::new(&witnesses); Self { - degree, + degree: fixed_data.common_degree_range(&witnesses).max, connecting_identities: connecting_identities.clone(), name, fixed_data, @@ -215,7 +214,6 @@ impl<'a, T: FieldElement> Generator<'a, T> { let mut processor = VmProcessor::new( self.name().to_string(), - self.degree, RowIndex::from_degree(row_offset, self.degree), self.fixed_data, &self.identities, diff --git a/executor/src/witgen/machines/block_machine.rs b/executor/src/witgen/machines/block_machine.rs index d1aaa4d9bd..5aae4e61fa 100644 --- a/executor/src/witgen/machines/block_machine.rs +++ b/executor/src/witgen/machines/block_machine.rs @@ -4,7 +4,6 @@ use std::iter::{self, once}; use super::{EvalResult, FixedData}; -use crate::constant_evaluator::MIN_DEGREE_LOG; use crate::witgen::block_processor::BlockProcessor; use crate::witgen::data_structures::finalizable_data::FinalizableData; use crate::witgen::processor::{OuterQuery, Processor}; @@ -18,7 +17,8 @@ use crate::witgen::{MutableState, QueryCallback}; use crate::Identity; use itertools::Itertools; use powdr_ast::analyzed::{ - AlgebraicExpression as Expression, AlgebraicReference, IdentityKind, PolyID, PolynomialType, + AlgebraicExpression as Expression, AlgebraicReference, DegreeRange, IdentityKind, PolyID, + PolynomialType, }; use powdr_ast::parsed::visitor::ExpressionVisitable; use powdr_number::{DegreeType, FieldElement}; @@ -91,7 +91,9 @@ impl<'a, T: FieldElement> Display for BlockMachine<'a, T> { /// TODO we do not actually "detect" the machine yet, we just check if /// the lookup has a binary selector that is 1 every k rows for some k pub struct BlockMachine<'a, T: FieldElement> { - /// The unique degree of all columns in this machine + /// The degree range of all columns in this machine + degree_range: DegreeRange, + /// The current degree of all columns in this machine degree: DegreeType, /// Block size, the period of the selector. block_size: usize, @@ -125,7 +127,10 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> { identities: &[&'a Identity], witness_cols: &HashSet, ) -> Option { - let degree = fixed_data.common_degree(witness_cols); + let degree_range = fixed_data.common_degree_range(witness_cols); + + // start from the max degree + let degree = degree_range.max; let (is_permutation, block_size, latch_row) = detect_connection_type_and_block_size(fixed_data, connecting_identities)?; @@ -156,6 +161,7 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> { ); Some(BlockMachine { name, + degree_range, degree, block_size, latch_row, @@ -248,7 +254,7 @@ fn try_to_period( return None; } - let degree = fixed_data.common_degree(once(&poly.poly_id)); + let degree = fixed_data.common_degree_range(once(&poly.poly_id)).max; let values = fixed_data.fixed_cols[&poly.poly_id].values(degree); @@ -313,18 +319,16 @@ impl<'a, T: FieldElement> Machine<'a, T> for BlockMachine<'a, T> { ); } - if self.fixed_data.is_variable_size(&self.witness_cols) { - let new_degree = self.data.len().next_power_of_two() as DegreeType; - let new_degree = new_degree.max(1 << MIN_DEGREE_LOG); - log::info!( - "Resizing variable length machine '{}': {} -> {} (rounded up from {})", - self.name, - self.degree, - new_degree, - self.data.len() - ); - self.degree = new_degree; - } + let new_degree = self.data.len().next_power_of_two() as DegreeType; + let new_degree = self.degree_range.fit(new_degree); + log::info!( + "Resizing variable length machine '{}': {} -> {} (rounded up from {})", + self.name, + self.degree, + new_degree, + self.data.len() + ); + self.degree = new_degree; if matches!(self.connection_type, ConnectionType::Permutation) { // We have to make sure that *all* selectors are 0 in the dummy block, diff --git a/executor/src/witgen/machines/double_sorted_witness_machine.rs b/executor/src/witgen/machines/double_sorted_witness_machine.rs index 4096064636..e4b443a58d 100644 --- a/executor/src/witgen/machines/double_sorted_witness_machine.rs +++ b/executor/src/witgen/machines/double_sorted_witness_machine.rs @@ -4,7 +4,6 @@ use std::iter::once; use itertools::Itertools; use super::Machine; -use crate::constant_evaluator::{MAX_DEGREE_LOG, MIN_DEGREE_LOG}; use crate::witgen::rows::RowPair; use crate::witgen::util::try_to_simple_poly; use crate::witgen::{EvalError, EvalResult, FixedData, MutableState, QueryCallback}; @@ -12,7 +11,7 @@ use crate::witgen::{EvalValue, IncompleteCause}; use crate::Identity; use powdr_number::{DegreeType, FieldElement}; -use powdr_ast::analyzed::{IdentityKind, PolyID}; +use powdr_ast::analyzed::{DegreeRange, IdentityKind, PolyID}; /// If all witnesses of a machine have a name in this list (disregarding the namespace), /// we'll consider it to be a double-sorted machine. @@ -46,6 +45,7 @@ fn split_column_name(name: &str) -> (&str, &str) { pub struct DoubleSortedWitnesses<'a, T: FieldElement> { fixed: &'a FixedData<'a, T>, + degree_range: DegreeRange, degree: DegreeType, //key_col: String, /// Position of the witness columns in the data. @@ -58,8 +58,6 @@ pub struct DoubleSortedWitnesses<'a, T: FieldElement> { is_initialized: BTreeMap, namespace: String, name: String, - /// The set of witness columns that are actually part of this machine. - witness_cols: HashSet, /// If the machine has the `m_diff_upper` and `m_diff_lower` columns, this is the base of the /// two digits. diff_columns_base: Option, @@ -88,7 +86,9 @@ impl<'a, T: FieldElement> DoubleSortedWitnesses<'a, T> { connecting_identities: &BTreeMap>, witness_cols: &HashSet, ) -> Option { - let degree = fixed_data.common_degree(witness_cols); + let degree_range = fixed_data.common_degree_range(witness_cols); + + let degree = degree_range.max; // get the namespaces and column names let (mut namespaces, columns): (HashSet<_>, HashSet<_>) = witness_cols @@ -163,7 +163,7 @@ impl<'a, T: FieldElement> DoubleSortedWitnesses<'a, T> { }; Some(Self { name, - witness_cols: witness_cols.clone(), + degree_range, namespace, fixed: fixed_data, degree, @@ -257,20 +257,17 @@ impl<'a, T: FieldElement> Machine<'a, T> for DoubleSortedWitnesses<'a, T> { set_selector(None); } - if self.fixed.is_variable_size(&self.witness_cols) { - let current_size = addr.len(); - assert!(current_size <= 1 << *MAX_DEGREE_LOG); - let new_size = current_size.next_power_of_two() as DegreeType; - let new_size = new_size.max(1 << MIN_DEGREE_LOG); - log::info!( - "Resizing variable length machine '{}': {} -> {} (rounded up from {})", - self.name, - self.degree, - new_size, - current_size - ); - self.degree = new_size; - } + let current_size = addr.len(); + let new_size = current_size.next_power_of_two() as DegreeType; + let new_size = self.degree_range.fit(new_size); + log::info!( + "Resizing variable length machine '{}': {} -> {} (rounded up from {})", + self.name, + self.degree, + new_size, + current_size + ); + self.degree = new_size; while addr.len() < self.degree as usize { addr.push(*addr.last().unwrap()); diff --git a/executor/src/witgen/machines/machine_extractor.rs b/executor/src/witgen/machines/machine_extractor.rs index b20b77be7b..8baa633141 100644 --- a/executor/src/witgen/machines/machine_extractor.rs +++ b/executor/src/witgen/machines/machine_extractor.rs @@ -201,7 +201,6 @@ fn build_machine<'a, T: FieldElement>( .unwrap(); KnownMachine::Vm(Generator::new( name_with_type("Vm"), - fixed.common_degree(&machine_witnesses), fixed, &connecting_identities, machine_identities, diff --git a/executor/src/witgen/machines/sorted_witness_machine.rs b/executor/src/witgen/machines/sorted_witness_machine.rs index f4f7c71679..35e1424f78 100644 --- a/executor/src/witgen/machines/sorted_witness_machine.rs +++ b/executor/src/witgen/machines/sorted_witness_machine.rs @@ -44,7 +44,7 @@ impl<'a, T: FieldElement> SortedWitnesses<'a, T> { identities: &[&Identity], witnesses: &HashSet, ) -> Option { - let degree = fixed_data.common_degree(witnesses); + let degree = fixed_data.common_degree_range(witnesses).max; if identities.len() != 1 { return None; diff --git a/executor/src/witgen/machines/write_once_memory.rs b/executor/src/witgen/machines/write_once_memory.rs index b58cc13fce..e7957406f1 100644 --- a/executor/src/witgen/machines/write_once_memory.rs +++ b/executor/src/witgen/machines/write_once_memory.rs @@ -100,7 +100,9 @@ impl<'a, T: FieldElement> WriteOnceMemory<'a, T> { } }); - let degree = fixed_data.common_degree(key_polys.iter().chain(value_polys.iter())); + let degree = fixed_data + .common_degree_range(key_polys.iter().chain(value_polys.iter())) + .max; let mut key_to_index = BTreeMap::new(); for row in 0..degree { diff --git a/executor/src/witgen/mod.rs b/executor/src/witgen/mod.rs index 0583a180ab..7cf184e63e 100644 --- a/executor/src/witgen/mod.rs +++ b/executor/src/witgen/mod.rs @@ -3,14 +3,14 @@ use std::sync::Arc; use itertools::Itertools; use powdr_ast::analyzed::{ - AlgebraicExpression, AlgebraicReference, Analyzed, Expression, FunctionValueDefinition, - IdentityKind, PolyID, PolynomialType, SymbolKind, TypedExpression, + AlgebraicExpression, AlgebraicReference, Analyzed, DegreeRange, Expression, + FunctionValueDefinition, IdentityKind, PolyID, PolynomialType, SymbolKind, TypedExpression, }; use powdr_ast::parsed::visitor::ExpressionVisitable; use powdr_ast::parsed::{FunctionKind, LambdaExpression}; use powdr_number::{DegreeType, FieldElement}; -use crate::constant_evaluator::{VariablySizedColumn, MAX_DEGREE_LOG}; +use crate::constant_evaluator::VariablySizedColumn; use self::data_structures::column_map::{FixedColumnMap, WitnessColumnMap}; pub use self::eval_result::{ @@ -238,17 +238,8 @@ impl<'a, 'b, T: FieldElement> WitnessGenerator<'a, 'b, T> { }; let generator = (!base_witnesses.is_empty()).then(|| { - let main_size = fixed - .common_set_degree(&base_witnesses) - // In the dynamic VADCOP setting, we assume that some machines - // (e.g. register memory) may take up to 4x the number of rows - // of the main machine. By running the main machine only 1/4 of - // of the steps, we ensure that no secondary machine will run out - // of rows. - .unwrap_or(1 << (*MAX_DEGREE_LOG - 2)); let mut generator = Generator::new( "Main Machine".to_string(), - main_size, &fixed, &BTreeMap::new(), // No connecting identities base_identities, @@ -334,10 +325,7 @@ impl<'a, T: FieldElement> FixedData<'a, T> { /// - the degree is not unique /// - the set of polynomials is empty /// - a declared polynomial does not have an explicit degree - fn common_set_degree<'b>( - &self, - ids: impl IntoIterator, - ) -> Option { + fn common_degree_range<'b>(&self, ids: impl IntoIterator) -> DegreeRange { let ids: HashSet<_> = ids.into_iter().collect(); self.analyzed @@ -356,14 +344,7 @@ impl<'a, T: FieldElement> FixedData<'a, T> { .unique() .exactly_one() .unwrap_or_else(|_| panic!("expected all polynomials to have the same degree")) - } - - fn common_degree<'b>(&self, ids: impl IntoIterator) -> DegreeType { - self.common_set_degree(ids).unwrap_or(1 << *MAX_DEGREE_LOG) - } - - fn is_variable_size<'b>(&self, ids: impl IntoIterator) -> bool { - self.common_set_degree(ids).is_none() + .unwrap() } pub fn new( diff --git a/executor/src/witgen/vm_processor.rs b/executor/src/witgen/vm_processor.rs index 71ae6cfb1a..f99da7ed25 100644 --- a/executor/src/witgen/vm_processor.rs +++ b/executor/src/witgen/vm_processor.rs @@ -1,13 +1,12 @@ use indicatif::{ProgressBar, ProgressStyle}; use itertools::Itertools; -use powdr_ast::analyzed::{AlgebraicReference, IdentityKind, PolyID}; +use powdr_ast::analyzed::{AlgebraicReference, DegreeRange, IdentityKind, PolyID}; use powdr_ast::indent; use powdr_number::{DegreeType, FieldElement}; use std::cmp::max; use std::collections::HashSet; use std::time::Instant; -use crate::constant_evaluator::MIN_DEGREE_LOG; use crate::witgen::identity_processor::{self}; use crate::witgen::IncompleteCause; use crate::Identity; @@ -46,7 +45,9 @@ impl<'a, T: FieldElement> CompletableIdentities<'a, T> { pub struct VmProcessor<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> { /// The name of the machine being run machine_name: String, - /// The common degree of all referenced columns + /// The common degree range of all referenced columns + degree_range: DegreeRange, + /// The current degree of all referenced columns degree: DegreeType, /// The global index of the first row of [VmProcessor::data]. row_offset: DegreeType, @@ -69,7 +70,6 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> VmProcessor<'a, 'b, 'c, T #[allow(clippy::too_many_arguments)] pub fn new( machine_name: String, - degree: DegreeType, row_offset: RowIndex, fixed_data: &'a FixedData<'a, T>, identities: &[&'a Identity], @@ -77,6 +77,10 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> VmProcessor<'a, 'b, 'c, T data: FinalizableData, mutable_state: &'c mut MutableState<'a, 'b, T, Q>, ) -> Self { + let degree_range = fixed_data.common_degree_range(witnesses); + + let degree = degree_range.max; + let (identities_with_next, identities_without_next): (Vec<_>, Vec<_>) = identities .iter() .partition(|identity| identity.contains_next_ref()); @@ -99,6 +103,7 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> VmProcessor<'a, 'b, 'c, T VmProcessor { machine_name, + degree_range, degree, row_offset: row_offset.into(), witnesses: witnesses.clone(), @@ -179,19 +184,17 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> VmProcessor<'a, 'b, 'c, T "Found loop with period {p} starting at row {row_index}" ); - if self.fixed_data.is_variable_size(&self.witnesses) { - let new_degree = self.processor.len().next_power_of_two() as DegreeType; - let new_degree = new_degree.max(1 << MIN_DEGREE_LOG); - log::info!( - "Resizing variable length machine '{}': {} -> {} (rounded up from {})", - self.machine_name, - self.degree, - new_degree, - self.processor.len() - ); - self.degree = new_degree; - self.processor.set_size(new_degree); - } + let new_degree = self.processor.len().next_power_of_two() as DegreeType; + let new_degree = self.degree_range.fit(new_degree); + log::info!( + "Resizing variable length machine '{}': {} -> {} (rounded up from {})", + self.machine_name, + self.degree, + new_degree, + self.processor.len() + ); + self.degree = new_degree; + self.processor.set_size(new_degree); } } if let Some(period) = looping_period { diff --git a/linker/Cargo.toml b/linker/Cargo.toml index ac91538999..5d05b58d3c 100644 --- a/linker/Cargo.toml +++ b/linker/Cargo.toml @@ -15,6 +15,8 @@ powdr-parser-util.workspace = true pretty_assertions = "1.4.0" itertools = "0.13" +lazy_static = "1.4.0" +log = "0.4.22" [dev-dependencies] powdr-airgen.workspace = true diff --git a/linker/src/lib.rs b/linker/src/lib.rs index 418602da3a..a1173a2d3b 100644 --- a/linker/src/lib.rs +++ b/linker/src/lib.rs @@ -1,22 +1,54 @@ #![deny(clippy::print_stdout)] -use std::collections::BTreeMap; - +use lazy_static::lazy_static; use powdr_analysis::utils::parse_pil_statement; use powdr_ast::{ - asm_analysis::combine_flags, + asm_analysis::{combine_flags, MachineDegree}, object::{Link, Location, PILGraph, TypeOrExpression}, parsed::{ asm::{AbsoluteSymbolPath, SymbolPath}, build::{index_access, namespaced_reference}, - ArrayLiteral, PILFile, PilStatement, SelectedExpressions, TypedExpression, + ArrayLiteral, Expression, NamespaceDegree, PILFile, PilStatement, SelectedExpressions, + TypedExpression, }, }; use powdr_parser_util::SourceRef; +use std::collections::BTreeMap; use itertools::Itertools; const MAIN_OPERATION_NAME: &str = "main"; +/// The log of the default minimum degree +pub const MIN_DEGREE_LOG: usize = 5; +lazy_static! { + // The maximum degree can add a significant cost during setup, because + // the fixed columns need to be committed to in all sizes up to the max degree. + // This gives the user the possibility to overwrite the default value. + /// The log of the default maximum degree + pub static ref MAX_DEGREE_LOG: usize = { + let default_max_degree_log = 22; + + let max_degree_log = match std::env::var("MAX_DEGREE_LOG") { + Ok(val) => val.parse::().unwrap(), + Err(_) => default_max_degree_log, + }; + log::info!("For variably-sized machine, the maximum degree is 2^{max_degree_log}. \ + You can set the environment variable MAX_DEGREE_LOG to change this value."); + max_degree_log + }; +} + +/// Convert a [MachineDegree] into a [NamespaceDegree], setting any unset bounds to the relevant default values +fn to_namespace_degree(d: MachineDegree) -> NamespaceDegree { + NamespaceDegree { + min: d + .min + .unwrap_or_else(|| Expression::from(1 << MIN_DEGREE_LOG)), + max: d + .max + .unwrap_or_else(|| Expression::from(1 << *MAX_DEGREE_LOG)), + } +} /// The optional degree of the namespace is set to that of the object if it's set, to that of the main object otherwise. pub fn link(graph: PILGraph) -> Result> { @@ -32,10 +64,15 @@ pub fn link(graph: PILGraph) -> Result> { for (location, object) in graph.objects.into_iter() { // create a namespace for this object + let degree = match main_degree.is_static() { + true => main_degree.clone(), + false => object.degree, + }; + pil.push(PilStatement::Namespace( SourceRef::unknown(), SymbolPath::from_identifier(location.to_string()), - object.degree.or(main_degree.clone()), + Some(to_namespace_degree(degree)), )); pil.extend(object.pil); @@ -237,7 +274,7 @@ mod test { use pretty_assertions::assert_eq; - use crate::link; + use crate::{link, MAX_DEGREE_LOG, MIN_DEGREE_LOG}; fn parse_analyze_and_compile_file(file: &str) -> PILGraph { let contents = fs::read_to_string(file).unwrap(); @@ -303,8 +340,12 @@ namespace main__rom(4 + 4); #[test] fn compile_really_empty_vm() { - let expectation = r#"namespace main; -"#; + let expectation = format!( + r#"namespace main({}..{}); +"#, + 1 << MIN_DEGREE_LOG, + 1 << *MAX_DEGREE_LOG + ); let graph = parse_analyze_and_compile::(""); let pil = link(graph).unwrap(); @@ -407,7 +448,7 @@ namespace main_sub(16); pc' = (1 - first_step') * pc_update; pol commit _output_0_free_value; 1 $ [0, pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return, _output_0_const, _output_0_read_free, read__output_0_pc, read__output_0__input_0] in main_sub__rom::latch $ [main_sub__rom::operation_id, main_sub__rom::p_line, main_sub__rom::p_instr__jump_to_operation, main_sub__rom::p_instr__reset, main_sub__rom::p_instr__loop, main_sub__rom::p_instr_return, main_sub__rom::p__output_0_const, main_sub__rom::p__output_0_read_free, main_sub__rom::p_read__output_0_pc, main_sub__rom::p_read__output_0__input_0]; -namespace main_sub__rom(8); +namespace main_sub__rom(16); pol constant p_line = [0, 1, 2, 3, 4, 5] + [5]*; pol constant p__output_0_const = [0, 0, 0, 0, 1, 0] + [0]*; pol constant p__output_0_read_free = [0]*; @@ -515,7 +556,7 @@ namespace main__rom(16); #[test] fn compile_literal_number_args() { let source = r#" -machine Machine { +machine Machine with min_degree: 32, max_degree: 64 { reg pc[@pc]; reg fp; @@ -529,7 +570,7 @@ machine Machine { } } "#; - let expectation = r#"namespace main; + let expectation = r#"namespace main(32..64); pol commit _operation_id(i) query std::prelude::Query::Hint(4); pol constant _block_enforcer_last_step = [0]* + [1]; let _operation_id_no_change = (1 - _block_enforcer_last_step) * (1 - instr_return); @@ -594,7 +635,7 @@ machine NegativeForUnsigned { #[test] fn instr_links_generated_pil() { let asm = r" -machine SubVM with latch: latch, operation_id: operation_id { +machine SubVM with latch: latch, operation_id: operation_id, min_degree: 64, max_degree: 128 { operation add5<0> x -> y; col witness operation_id; @@ -606,7 +647,7 @@ machine SubVM with latch: latch, operation_id: operation_id { y = x + 5; } -machine Main { +machine Main with min_degree: 32, max_degree: 64 { reg pc[@pc]; reg X[<=]; reg A; @@ -620,7 +661,7 @@ machine Main { } } "; - let expected = r#"namespace main; + let expected = r#"namespace main(32..64); pol commit _operation_id(i) query std::prelude::Query::Hint(3); pol constant _block_enforcer_last_step = [0]* + [1]; let _operation_id_no_change = (1 - _block_enforcer_last_step) * (1 - instr_return); @@ -663,7 +704,7 @@ namespace main__rom(4); pol constant p_reg_write_X_A = [0]*; pol constant operation_id = [0]*; pol constant latch = [1]*; -namespace main_vm; +namespace main_vm(64..128); pol commit operation_id; pol constant latch = [1]*; pol commit x; diff --git a/parser/src/powdr.lalrpop b/parser/src/powdr.lalrpop index f44155079c..9afa613ee3 100644 --- a/parser/src/powdr.lalrpop +++ b/parser/src/powdr.lalrpop @@ -131,8 +131,13 @@ Include: PilStatement = { "include" ";" => PilStatement::Include(ctx.source_ref(start, end), file) }; +NamespaceDegree: NamespaceDegree = { + ".." => NamespaceDegree {min, max}, + => NamespaceDegree { min: degree.clone(), max: degree } +} + Namespace: PilStatement = { - "namespace" ")")?> ";" + "namespace" ")")?> ";" => PilStatement::Namespace(ctx.source_ref(start, end), name.unwrap_or_default(), pol_degree) } diff --git a/pil-analyzer/src/condenser.rs b/pil-analyzer/src/condenser.rs index f9c11dd11b..203e5b9d58 100644 --- a/pil-analyzer/src/condenser.rs +++ b/pil-analyzer/src/condenser.rs @@ -11,7 +11,7 @@ use std::{ use powdr_ast::{ analyzed::{ - self, AlgebraicExpression, AlgebraicReference, Analyzed, Expression, + self, AlgebraicExpression, AlgebraicReference, Analyzed, DegreeRange, Expression, FunctionValueDefinition, Identity, IdentityKind, PolyID, PolynomialType, PublicDeclaration, SelectedExpressions, StatementIdentifier, Symbol, SymbolKind, }, @@ -23,7 +23,7 @@ use powdr_ast::{ FunctionKind, TypedExpression, }, }; -use powdr_number::{DegreeType, FieldElement}; +use powdr_number::FieldElement; use powdr_parser_util::SourceRef; use crate::{ @@ -175,7 +175,7 @@ pub fn condense( type SymbolCache<'a, T> = HashMap>, Arc>>>; pub struct Condenser<'a, T> { - degree: Option, + degree: Option, /// All the definitions from the PIL file. symbols: &'a HashMap)>, /// Evaluation cache. @@ -246,7 +246,7 @@ impl<'a, T: FieldElement> Condenser<'a, T> { pub fn set_namespace_and_degree( &mut self, namespace: AbsoluteSymbolPath, - degree: Option, + degree: Option, ) { self.namespace = namespace; self.degree = degree; @@ -349,9 +349,23 @@ impl<'a, T: FieldElement> SymbolLookup<'a, T> for Condenser<'a, T> { Definitions(self.symbols).lookup_public_reference(name) } + fn min_degree(&self) -> Result>, EvalError> { + let degree = self.degree.ok_or(EvalError::DataNotAvailable)?; + Ok(Value::Integer(degree.min.into()).into()) + } + + fn max_degree(&self) -> Result>, EvalError> { + let degree = self.degree.ok_or(EvalError::DataNotAvailable)?; + Ok(Value::Integer(degree.max.into()).into()) + } + fn degree(&self) -> Result>, EvalError> { let degree = self.degree.ok_or(EvalError::DataNotAvailable)?; - Ok(Value::Integer(degree.into()).into()) + if degree.min == degree.max { + Ok(Value::Integer(degree.min.into()).into()) + } else { + Err(EvalError::DataNotAvailable) + } } fn new_column( diff --git a/pil-analyzer/src/evaluator.rs b/pil-analyzer/src/evaluator.rs index 054dc58729..54ecf09327 100644 --- a/pil-analyzer/src/evaluator.rs +++ b/pil-analyzer/src/evaluator.rs @@ -308,7 +308,7 @@ impl<'a, T: FieldElement> Value<'a, T> { } } -const BUILTINS: [(&str, BuiltinFunction); 11] = [ +const BUILTINS: [(&str, BuiltinFunction); 13] = [ ("std::array::len", BuiltinFunction::ArrayLen), ("std::check::panic", BuiltinFunction::Panic), ("std::convert::expr", BuiltinFunction::ToExpr), @@ -318,6 +318,8 @@ const BUILTINS: [(&str, BuiltinFunction); 11] = [ ("std::field::modulus", BuiltinFunction::Modulus), ("std::prelude::challenge", BuiltinFunction::Challenge), ("std::prelude::set_hint", BuiltinFunction::SetHint), + ("std::prover::min_degree", BuiltinFunction::MinDegree), + ("std::prover::max_degree", BuiltinFunction::MaxDegree), ("std::prover::degree", BuiltinFunction::Degree), ("std::prover::eval", BuiltinFunction::Eval), ]; @@ -344,7 +346,11 @@ pub enum BuiltinFunction { Challenge, /// std::prelude::set_hint: expr, (int -> std::prelude::Query) -> (), adds a hint to a witness column. SetHint, - /// std::prover::degree: -> int, returns the current column length / degree. + /// std::prover::min_degree: -> int, returns the minimum column length / degree. + MinDegree, + /// std::prover::max_degree: -> int, returns the maximum column length / degree. + MaxDegree, + /// std::prover::degree: -> int, returns the column length / degree, if the minimum and maximum are equal. Degree, /// std::prover::eval: expr -> fe, evaluates an expression on the current row Eval, @@ -537,6 +543,18 @@ pub trait SymbolLookup<'a, T: FieldElement> { Err(EvalError::DataNotAvailable) } + fn min_degree(&self) -> Result>, EvalError> { + Err(EvalError::Unsupported( + "Cannot evaluate min degree.".to_string(), + )) + } + + fn max_degree(&self) -> Result>, EvalError> { + Err(EvalError::Unsupported( + "Cannot evaluate max degree.".to_string(), + )) + } + fn degree(&self) -> Result>, EvalError> { Err(EvalError::Unsupported( "Cannot evaluate degree.".to_string(), @@ -1127,6 +1145,8 @@ fn evaluate_builtin_function<'a, T: FieldElement>( BuiltinFunction::ToInt => 1, BuiltinFunction::Challenge => 2, BuiltinFunction::SetHint => 2, + BuiltinFunction::MinDegree => 0, + BuiltinFunction::MaxDegree => 0, BuiltinFunction::Degree => 0, BuiltinFunction::Eval => 1, }; @@ -1201,6 +1221,8 @@ fn evaluate_builtin_function<'a, T: FieldElement>( symbols.set_hint(col, expr)?; Value::Tuple(vec![]).into() } + BuiltinFunction::MaxDegree => symbols.max_degree()?, + BuiltinFunction::MinDegree => symbols.min_degree()?, BuiltinFunction::Degree => symbols.degree()?, BuiltinFunction::Eval => { let arg = arguments.pop().unwrap(); diff --git a/pil-analyzer/src/pil_analyzer.rs b/pil-analyzer/src/pil_analyzer.rs index 8d08ba0dd7..03eaa721de 100644 --- a/pil-analyzer/src/pil_analyzer.rs +++ b/pil-analyzer/src/pil_analyzer.rs @@ -14,11 +14,12 @@ use powdr_ast::parsed::{ self, FunctionKind, LambdaExpression, PILFile, PilStatement, SelectedExpressions, SymbolCategory, }; -use powdr_number::{DegreeType, FieldElement, GoldilocksField}; +use powdr_number::{FieldElement, GoldilocksField}; use powdr_ast::analyzed::{ - type_from_definition, Analyzed, Expression, FunctionValueDefinition, Identity, IdentityKind, - PolynomialType, PublicDeclaration, StatementIdentifier, Symbol, SymbolKind, TypedExpression, + type_from_definition, Analyzed, DegreeRange, Expression, FunctionValueDefinition, Identity, + IdentityKind, PolynomialType, PublicDeclaration, StatementIdentifier, Symbol, SymbolKind, + TypedExpression, }; use powdr_parser::{parse, parse_module, parse_type}; @@ -60,7 +61,7 @@ struct PILAnalyzer { /// Known symbols by name and category, determined in the first step. known_symbols: HashMap, current_namespace: AbsoluteSymbolPath, - polynomial_degree: Option, + polynomial_degree: Option, /// Map of definitions, gradually being built up here. definitions: HashMap)>, public_declarations: HashMap, @@ -406,23 +407,23 @@ impl PILAnalyzer { } } - fn handle_namespace(&mut self, name: SymbolPath, degree: Option) { - self.polynomial_degree = degree - .map(|degree| { - ExpressionProcessor::new(self.driver(), &Default::default()) - .process_expression(degree) - }) - // TODO we should maybe implement a separate evaluator that is able to run before type checking - // and is field-independent (only uses integers)? - .map(|degree| { - u64::try_from( - evaluator::evaluate_expression::(°ree, &self.definitions) - .unwrap() - .try_to_integer() - .unwrap(), - ) - .unwrap() - }); + fn handle_namespace(&mut self, name: SymbolPath, degree: Option) { + let evaluate_degree_bound = |e| { + let e = + ExpressionProcessor::new(self.driver(), &Default::default()).process_expression(e); + u64::try_from( + evaluator::evaluate_expression::(&e, &self.definitions) + .unwrap() + .try_to_integer() + .unwrap(), + ) + .unwrap() + }; + + self.polynomial_degree = degree.map(|degree| DegreeRange { + min: evaluate_degree_bound(degree.min), + max: evaluate_degree_bound(degree.max), + }); self.current_namespace = AbsoluteSymbolPath::default().join(name); } diff --git a/pil-analyzer/src/side_effect_checker.rs b/pil-analyzer/src/side_effect_checker.rs index 3b1d16b1cc..d84597c6c1 100644 --- a/pil-analyzer/src/side_effect_checker.rs +++ b/pil-analyzer/src/side_effect_checker.rs @@ -145,6 +145,8 @@ lazy_static! { ("std::debug::print", FunctionKind::Pure), ("std::field::modulus", FunctionKind::Pure), ("std::prelude::challenge", FunctionKind::Constr), // strictly, only new_challenge would need "constr" + ("std::prover::min_degree", FunctionKind::Pure), + ("std::prover::max_degree", FunctionKind::Pure), ("std::prover::degree", FunctionKind::Pure), ("std::prelude::set_hint", FunctionKind::Constr), ("std::prover::eval", FunctionKind::Query), diff --git a/pil-analyzer/src/statement_processor.rs b/pil-analyzer/src/statement_processor.rs index 359cc1aeef..a44e056399 100644 --- a/pil-analyzer/src/statement_processor.rs +++ b/pil-analyzer/src/statement_processor.rs @@ -4,7 +4,7 @@ use std::sync::Arc; use itertools::Itertools; -use powdr_ast::analyzed::TypedExpression; +use powdr_ast::analyzed::{DegreeRange, TypedExpression}; use powdr_ast::parsed::{ self, types::{ArrayType, Type, TypeScheme}, @@ -12,7 +12,6 @@ use powdr_ast::parsed::{ PilStatement, PolynomialName, SelectedExpressions, TraitDeclaration, TraitFunction, }; -use powdr_number::DegreeType; use powdr_parser_util::SourceRef; use powdr_ast::analyzed::{ @@ -101,14 +100,14 @@ impl Counters { pub struct StatementProcessor<'a, D> { driver: D, counters: &'a mut Counters, - degree: Option, + degree: Option, } impl<'a, D> StatementProcessor<'a, D> where D: AnalysisDriver, { - pub fn new(driver: D, counters: &'a mut Counters, degree: Option) -> Self { + pub fn new(driver: D, counters: &'a mut Counters, degree: Option) -> Self { StatementProcessor { driver, counters, diff --git a/pil-analyzer/src/type_builtins.rs b/pil-analyzer/src/type_builtins.rs index bec8c05c93..c6192709f8 100644 --- a/pil-analyzer/src/type_builtins.rs +++ b/pil-analyzer/src/type_builtins.rs @@ -42,6 +42,8 @@ lazy_static! { ("std::debug::print", ("T: ToString", "T -> ()")), ("std::field::modulus", ("", "-> int")), ("std::prelude::challenge", ("", "int, int -> expr")), + ("std::prover::min_degree", ("", "-> int")), + ("std::prover::max_degree", ("", "-> int")), ("std::prover::degree", ("", "-> int")), ( "std::prelude::set_hint", diff --git a/pil-analyzer/tests/condenser.rs b/pil-analyzer/tests/condenser.rs index 8cd8ab95a4..9eb01d750a 100644 --- a/pil-analyzer/tests/condenser.rs +++ b/pil-analyzer/tests/condenser.rs @@ -116,20 +116,34 @@ pub fn degree() { let expr = []; namespace std::prover; let degree = []; + let min_degree = []; + let max_degree = []; namespace Main(8); let d = std::prover::degree(); let w; w = std::convert::expr(d); + namespace Other(32..64); + let min = std::prover::min_degree(); + let max = std::prover::max_degree(); + col witness w; + w = 8; "#; let formatted = analyze_string::(input).to_string(); let expected = r#"namespace std::convert; let expr = []; namespace std::prover; let degree = []; + let min_degree = []; + let max_degree = []; namespace Main(8); let d: int = std::prover::degree(); col witness w; Main::w = 8; +namespace Other(32..64); + let min: int = std::prover::min_degree(); + let max: int = std::prover::max_degree(); + col witness w; + Other::w = 8; "#; assert_eq!(formatted, expected); } @@ -142,7 +156,7 @@ pub fn degree_unset() { let expr = []; namespace std::prover; let degree = []; - namespace Main; + namespace Main(32..63); let d = std::prover::degree(); let w; w = std::convert::expr(d); diff --git a/riscv/Cargo.toml b/riscv/Cargo.toml index 1637a7551c..82402c9cdc 100644 --- a/riscv/Cargo.toml +++ b/riscv/Cargo.toml @@ -17,6 +17,7 @@ estark-polygon = ["powdr-pipeline/estark-polygon"] powdr-ast.workspace = true powdr-asm-utils.workspace = true powdr-executor.workspace = true +powdr-linker.workspace = true powdr-number.workspace = true powdr-parser.workspace = true powdr-parser-util.workspace = true diff --git a/riscv/src/code_gen.rs b/riscv/src/code_gen.rs index c5929a69dd..ca1ca43e31 100644 --- a/riscv/src/code_gen.rs +++ b/riscv/src/code_gen.rs @@ -300,7 +300,7 @@ fn riscv_machine( format!( r#" {} -machine Main {{ +machine Main with min_degree: {}, max_degree: {} {{ {} {} @@ -315,6 +315,11 @@ let initial_memory: (fe, fe)[] = [ }} "#, runtime.submachines_import(), + 1 << powdr_linker::MIN_DEGREE_LOG, + // We expect some machines (e.g. register memory) to use up to 4x the number + // of rows as main. By setting the max degree of main to be smaller by a factor + // of 4, we ensure that we don't run out of rows in those machines. + 1 << (*powdr_linker::MAX_DEGREE_LOG - 2), runtime.submachines_declare(), preamble, initial_memory diff --git a/riscv/src/continuations.rs b/riscv/src/continuations.rs index 3e26c00edf..826d442e30 100644 --- a/riscv/src/continuations.rs +++ b/riscv/src/continuations.rs @@ -4,10 +4,9 @@ use std::{ }; use powdr_ast::{ - asm_analysis::AnalysisASMFile, + asm_analysis::{AnalysisASMFile, Machine}, parsed::{asm::parse_absolute_path, Expression, Number, PilStatement}, }; -use powdr_executor::constant_evaluator::MAX_DEGREE_LOG; use powdr_number::FieldElement; use powdr_pipeline::Pipeline; use powdr_riscv_executor::{get_main_machine, Elem, ExecutionTrace, MemoryState, ProfilerOptions}; @@ -75,13 +74,6 @@ where let bootloader_inputs = dry_run_result.bootloader_inputs; let num_chunks = bootloader_inputs.len(); - // The size of the main machine is dynamic, so we need to chose a size. - // We chose a size 4x smaller than the maximum size, so that we can guarantee - // that the register memory does not run out of rows. - // TODO: After #1667 ("Support degree ranges") is merged, this can be set in ASM - // and we can just use the maximum size here. - let length = 1 << (*MAX_DEGREE_LOG - 2); - log::info!("Computing fixed columns..."); pipeline.compute_fixed_cols().unwrap(); @@ -114,6 +106,20 @@ where } else { pipeline }; + + // get the length of the main machine + // quite hacky, is there a better way? + let length = pipeline + .optimized_pil() + .unwrap() + .definitions + .iter() + .find_map(|(name, (s, _))| match (name.starts_with("main::"), s) { + (true, s) => s.degree.map(|d| d.max), + _ => None, + }) + .unwrap(); + // The `jump_to_shutdown_routine` column indicates when the execution should jump to the shutdown routine. // In that row, the normal PC update is ignored and the PC is set to the address of the shutdown routine. // In other words, it should be a one-hot encoding of `start_of_shutdown_routine`. @@ -138,10 +144,7 @@ where Ok(()) } -fn sanity_check(program: &AnalysisASMFile) { - let main_machine = program.items[&parse_absolute_path("::Main")] - .try_to_machine() - .unwrap(); +fn sanity_check(main_machine: &Machine) { for expected_instruction in BOOTLOADER_SPECIFIC_INSTRUCTION_NAMES { if !main_machine .instructions @@ -218,7 +221,10 @@ pub fn rust_continuations_dry_run( let mut register_values = default_register_values(); let program = pipeline.compute_analyzed_asm().unwrap().clone(); - sanity_check(&program); + let main_machine = program.items[&parse_absolute_path("::Main")] + .try_to_machine() + .unwrap(); + sanity_check(main_machine); log::info!("Initializing memory merkle tree..."); @@ -268,7 +274,16 @@ pub fn rust_continuations_dry_run( let mut proven_trace = first_real_execution_row; let mut chunk_index = 0; - let length = 1 << (*MAX_DEGREE_LOG - 2); + let max_degree_expr = main_machine.degree.max.as_ref(); + + let length: usize = match max_degree_expr { + Some(Expression::Number(_, n)) => n.value.clone().try_into().unwrap(), + // if the max degree is not defined, it defaults to `1 << MAX_DEGREE_LOG` which is too large + None => unimplemented!("Continuations rely on `Main` defining a max degree"), + Some(e) => { + unimplemented!("Continuations rely on `Main` not using a complex expression as its max degree, found {e}") + } + }; loop { log::info!("\nRunning chunk {} for {} steps...", chunk_index, length); diff --git a/std/machines/binary.asm b/std/machines/binary.asm index c53fb9235b..370e393e4d 100644 --- a/std/machines/binary.asm +++ b/std/machines/binary.asm @@ -15,7 +15,7 @@ machine ByteBinary with let bit_counts = [256, 256, 3]; let min_degree = std::array::product(bit_counts); - std::check::assert(std::prover::degree() >= std::array::product(bit_counts), || "The binary machine needs at least 196608 rows to work."); + std::check::assert(std::prover::min_degree() >= std::array::product(bit_counts), || "The binary machine needs at least 196608 rows to work."); // TODO would be nice with destructuring assignment for arrays. let inputs: (int -> int)[] = cross_product(bit_counts); let a = inputs[0]; diff --git a/std/machines/shift.asm b/std/machines/shift.asm index 5f35507d38..e498763b2b 100644 --- a/std/machines/shift.asm +++ b/std/machines/shift.asm @@ -16,7 +16,7 @@ machine ByteShift with let bit_counts = [256, 32, 4, 2]; let min_degree = std::array::product(bit_counts); - std::check::assert(std::prover::degree() >= std::array::product(bit_counts), || "The shift machine needs at least 65536 rows to work."); + std::check::assert(std::prover::min_degree() >= std::array::product(bit_counts), || "The shift machine needs at least 65536 rows to work."); let inputs = cross_product(bit_counts); let a: int -> int = inputs[0]; let b: int -> int = inputs[1]; diff --git a/std/prover.asm b/std/prover.asm index c937a7d980..9a9f646d01 100644 --- a/std/prover.asm +++ b/std/prover.asm @@ -7,7 +7,11 @@ let eval: expr -> fe = []; /// The arguments are the proof stage and the id of the challenge, in this order. let challenge: int, int -> expr = constr |st, id| std::prelude::challenge(st, id); -/// Returns the current number of rows, sometimes known as the "degree". +/// Returns the minimum number of rows in this namespace, sometimes known as the minimum "degree". +let min_degree: -> int = []; +/// Returns the maximum number of rows in this namespace, sometimes known as the maximum "degree". +let max_degree: -> int = []; +/// Returns the number of rows in this namespace, sometimes known as the "degree". Fails if the minimum and maximum degree are not equal. let degree: -> int = []; /// Asserts that the current degree or row count is at least m. diff --git a/test_data/pil/vm_to_block_dynamic_length.pil b/test_data/pil/vm_to_block_dynamic_length.pil index 16508c7b67..4054beb1c5 100644 --- a/test_data/pil/vm_to_block_dynamic_length.pil +++ b/test_data/pil/vm_to_block_dynamic_length.pil @@ -44,7 +44,7 @@ namespace main(256); main::instr_mul $ [1, main::X, main::Y, main::Z] in [main_arith::operation_id, main_arith::x[0], main_arith::x[1], main_arith::y]; col fixed _linker_first_step = [1] + [0]*; main::_linker_first_step * (main::_operation_id - 2) = 0; -namespace main__rom(256); +namespace main__rom(8); col fixed p_line = [0, 1, 2, 3, 4, 5, 6] + [6]*; col fixed p_X_const = [0, 0, 2, 0, 0, 0, 0] + [0]*; col fixed p_Y_const = [0, 0, 1, 9, 27, 0, 0] + [0]*; @@ -59,8 +59,8 @@ namespace main__rom(256); col fixed p_read_X_A = [0, 0, 0, 1, 1, 0, 0] + [0]*; col fixed p_reg_write_Z_A = [0, 0, 1, 1, 0, 0, 0] + [0]*; -// CHANGED HERE: The degree of this namespace is None, meaning that this machine has a variable size. -namespace main_arith; +// CHANGED HERE: The degree of this namespace is a range, meaning that this machine has a variable size. +namespace main_arith(8..64); col witness operation_id; col witness x[2]; col witness y;