Merge pull request #652 from powdr-labs/remove-constraints-blocks

Remove constraints blocks

README.md

@@ -22,10 +22,10 @@ Both frontend and backend are highly flexible.
 As an example, *powdr* contains a frontend that enables you to write code in (no-std) Rust,
 which is compiled to RISCV, then to powdr-asm and finally to PIL.
 
-*powdr*-PIL can be used to generate proofs using multiple backends, such as:
+*powdr*-pil can be used to generate proofs using multiple backends, such as:
 
 - Halo2
-- eSTARKs: *powdr*-PIL is fully compatible with the eSTARKS backend from Polygon Hermez,
+- eSTARKs: *powdr*-pil is fully compatible with the eSTARKS backend from Polygon Hermez,
   although not yet fully integrated in an automatic way.
 - Nova: ongoing work.
 - other STARKs: maybe?

airgen/src/lib.rs

@@ -3,9 +3,7 @@
 use std::collections::BTreeMap;
 
 use ast::{
-    asm_analysis::{
-        AnalysisASMFile, LinkDefinitionStatement, Machine, PilBlock, SubmachineDeclaration,
-    },
+    asm_analysis::{AnalysisASMFile, LinkDefinitionStatement, Machine, SubmachineDeclaration},
     object::{Link, LinkFrom, LinkTo, Location, Object, Operation, PILGraph},
     parsed::{
         asm::{parse_absolute_path, AbsoluteSymbolPath, CallableRef},
@@ -108,8 +106,8 @@ impl<'a, T: FieldElement> ASMPILConverter<'a, T> {
         }
     }
 
-    fn handle_inline_pil(&mut self, PilBlock { statements, .. }: PilBlock<T>) {
-        self.pil.extend(statements)
+    fn handle_pil_statement(&mut self, statement: PilStatement<T>) {
+        self.pil.push(statement);
     }
 
     fn convert_machine(
@@ -134,8 +132,8 @@ impl<'a, T: FieldElement> ASMPILConverter<'a, T> {
         assert!(input.registers.is_empty());
         assert!(input.callable.is_only_operations());
 
-        for block in input.constraints {
-            self.handle_inline_pil(block);
+        for block in input.pil {
+            self.handle_pil_statement(block);
         }
 
         let links = input

analysis/src/block_enforcer.rs

@@ -1,6 +1,6 @@
 //! For all machines, enforce that the `operation_id` can only change when the `latch` is on
 
-use ast::asm_analysis::{AnalysisASMFile, PilBlock};
+use ast::asm_analysis::AnalysisASMFile;
 use number::FieldElement;
 
 use crate::utils::parse_pil_statement;
@@ -27,10 +27,7 @@ pub fn enforce<T: FieldElement>(mut file: AnalysisASMFile<T>) -> AnalysisASMFile
             )),
         ];
 
-        machine.constraints.push(PilBlock {
-            start: 0,
-            statements: embedded_constraints.into_iter().collect(),
-        });
+        machine.pil.extend(embedded_constraints);
     }
     file
 }

analysis/src/macro_expansion.rs

@@ -32,22 +32,38 @@ impl<T: FieldElement> Folder<T> for MacroExpander<T> {
     type Error = Infallible;
 
     fn fold_machine(&mut self, mut machine: Machine<T>) -> Result<Machine<T>, Self::Error> {
-        machine.statements.iter_mut().for_each(|s| match s {
-            MachineStatement::InstructionDeclaration(_, _, Instruction { body, .. }) => {
-                match body {
-                    InstructionBody::Local(body) => {
-                        *body = self.expand_macros(std::mem::take(body))
-                    }
-                    InstructionBody::CallableRef(..) => {
+        machine.statements = machine
+            .statements
+            .into_iter()
+            .flat_map(|s| match s {
+                MachineStatement::InstructionDeclaration(
+                    start,
+                    name,
+                    Instruction { body, params },
+                ) => {
+                    let body = match body {
+                        InstructionBody::Local(body) => {
+                            InstructionBody::Local(self.expand_macros(body))
+                        }
                         // there is nothing to expand in a callable ref
-                    }
+                        InstructionBody::CallableRef(r) => InstructionBody::CallableRef(r),
+                    };
+                    vec![MachineStatement::InstructionDeclaration(
+                        start,
+                        name,
+                        Instruction { body, params },
+                    )]
                 }
-            }
-            MachineStatement::InlinePil(_, statements) => {
-                *statements = self.expand_macros(std::mem::take(statements));
-            }
-            _ => {}
-        });
+                MachineStatement::Pil(start, statement) => self
+                    .expand_macros(vec![statement])
+                    .into_iter()
+                    .map(|s| MachineStatement::Pil(start, s))
+                    .collect(),
+                s => {
+                    vec![s]
+                }
+            })
+            .collect();
 
         Ok(machine)
     }

asm_to_pil/src/romgen.rs

@@ -4,7 +4,7 @@ use std::{collections::HashMap, iter::repeat};
 
 use ast::asm_analysis::{
     Batch, CallableSymbol, FunctionStatement, FunctionSymbol, Incompatible, IncompatibleSet,
-    Machine, OperationSymbol, PilBlock, Rom,
+    Machine, OperationSymbol, Rom,
 };
 use ast::parsed::visitor::ExpressionVisitable;
 use ast::parsed::{
@@ -224,21 +224,18 @@ pub fn generate_machine_rom<T: FieldElement>(
         let sigma = "_sigma";
         let first_step = "_romgen_first_step";
 
-        machine.constraints.push(PilBlock {
-            start: 0,
-            statements: vec![
-                // inject the operation_id
-                parse_pil_statement(&format!("col witness {operation_id}")),
-                // declare `_sigma` as the sum of the latch, will be 0 and then 1 after the end of the first call
-                parse_pil_statement(&format!("col witness {sigma}")),
-                parse_pil_statement(&format!("col fixed {first_step} = [1] + [0]*")),
-                parse_pil_statement(&format!(
-                    "{sigma}' = (1 - {first_step}') * ({sigma} + {latch})"
-                )),
-                // once `_sigma` is 1, constrain `_operation_id` to the label of the sink
-                parse_pil_statement(&format!("{sigma} * ({operation_id} - {sink_id}) = 0")),
-            ],
-        });
+        machine.pil.extend([
+            // inject the operation_id
+            parse_pil_statement(&format!("col witness {operation_id}")),
+            // declare `_sigma` as the sum of the latch, will be 0 and then 1 after the end of the first call
+            parse_pil_statement(&format!("col witness {sigma}")),
+            parse_pil_statement(&format!("col fixed {first_step} = [1] + [0]*")),
+            parse_pil_statement(&format!(
+                "{sigma}' = (1 - {first_step}') * ({sigma} + {latch})"
+            )),
+            // once `_sigma` is 1, constrain `_operation_id` to the label of the sink
+            parse_pil_statement(&format!("{sigma} * ({operation_id} - {sink_id}) = 0")),
+        ]);
         ///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
 
         machine.operation_id = Some(operation_id.into());

asm_to_pil/src/vm_to_constrained.rs

@@ -6,7 +6,7 @@ use ast::{
     asm_analysis::{
         AssignmentStatement, Batch, DebugDirective, FunctionStatement,
         InstructionDefinitionStatement, InstructionStatement, LabelStatement,
-        LinkDefinitionStatement, Machine, PilBlock, RegisterDeclarationStatement, RegisterTy, Rom,
+        LinkDefinitionStatement, Machine, RegisterDeclarationStatement, RegisterTy, Rom,
     },
     parsed::{
         asm::InstructionBody,
@@ -202,10 +202,7 @@ impl<T: FieldElement> ASMPILConverter<T> {
         ));
 
         if !self.pil.is_empty() {
-            input.constraints.push(PilBlock {
-                start: 0,
-                statements: self.pil,
-            });
+            input.pil.extend(self.pil);
         }
 
         input

ast/src/asm_analysis/display.rs

@@ -11,7 +11,7 @@ use super::{
     AnalysisASMFile, AssignmentStatement, CallableSymbol, CallableSymbolDefinitionRef,
     DebugDirective, DegreeStatement, FunctionBody, FunctionStatement, FunctionStatements,
     Incompatible, IncompatibleSet, Instruction, InstructionDefinitionStatement,
-    InstructionStatement, LabelStatement, LinkDefinitionStatement, Machine, PilBlock,
+    InstructionStatement, LabelStatement, LinkDefinitionStatement, Machine,
     RegisterDeclarationStatement, RegisterTy, Return, Rom, SubmachineDeclaration,
 };
 
@@ -40,7 +40,7 @@ impl<T: Display> Display for Machine<T> {
         write_items_indented(f, &self.registers)?;
         write_items_indented(f, &self.instructions)?;
         write_items_indented(f, &self.callable)?;
-        write_items_indented(f, &self.constraints)?;
+        write_items_indented(f, &self.pil)?;
         write_items_indented(f, &self.links)?;
 
         writeln!(f, "}}")
@@ -144,16 +144,6 @@ impl Display for LabelStatement {
     }
 }
 
-impl<T: Display> Display for PilBlock<T> {
-    fn fmt(&self, f: &mut Formatter<'_>) -> Result {
-        writeln!(f, "constraints {{")?;
-        for statement in &self.statements {
-            writeln!(f, "{}", indent(statement, 1))?;
-        }
-        writeln!(f, "}}")
-    }
-}
-
 impl Display for RegisterDeclarationStatement {
     fn fmt(&self, f: &mut Formatter<'_>) -> Result {
         write!(f, "reg {}{};", self.name, self.ty,)

ast/src/asm_analysis/mod.rs

@@ -659,12 +659,6 @@ pub struct Return<T> {
     pub values: Vec<Expression<T>>,
 }
 
-#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
-pub struct PilBlock<T> {
-    pub start: usize,
-    pub statements: Vec<PilStatement<T>>,
-}
-
 #[derive(Clone, Default, Debug, PartialEq, Eq, PartialOrd, Ord)]
 pub struct SubmachineDeclaration {
     /// the name of this instance
@@ -685,8 +679,8 @@ pub struct Machine<T> {
     pub registers: Vec<RegisterDeclarationStatement>,
     /// The index of the program counter in the registers, if any
     pub pc: Option<usize>,
-    /// The set of contraint blocks
-    pub constraints: Vec<PilBlock<T>>,
+    /// The set of pil statements
+    pub pil: Vec<PilStatement<T>>,
     /// The set of instructions which can be invoked in functions
     pub instructions: Vec<InstructionDefinitionStatement<T>>,
     /// The set of low level links to other machines

ast/src/asm_analysis/utils.rs

@@ -1,3 +1 @@
 
-
-

ast/src/parsed/asm.rs

@@ -263,11 +263,11 @@ pub struct Instruction<T> {
 #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)]
 pub enum MachineStatement<T> {
     Degree(usize, AbstractNumberType),
+    Pil(usize, PilStatement<T>),
     Submachine(usize, SymbolPath, String),
     RegisterDeclaration(usize, String, Option<RegisterFlag>),
     InstructionDeclaration(usize, String, Instruction<T>),
     LinkDeclaration(LinkDeclaration<T>),
-    InlinePil(usize, Vec<PilStatement<T>>),
     FunctionDeclaration(usize, String, Params, Vec<FunctionStatement<T>>),
     OperationDeclaration(usize, String, OperationId<T>, Params),
 }

ast/src/parsed/display.rs

@@ -137,6 +137,7 @@ impl<T: Display> Display for MachineStatement<T> {
     fn fmt(&self, f: &mut Formatter<'_>) -> Result {
         match self {
             MachineStatement::Degree(_, degree) => write!(f, "degree {};", degree),
+            MachineStatement::Pil(_, statement) => write!(f, "{statement};"),
             MachineStatement::Submachine(_, ty, name) => write!(f, "{ty} {name};"),
             MachineStatement::RegisterDeclaration(_, name, flag) => write!(
                 f,
@@ -152,9 +153,6 @@ impl<T: Display> Display for MachineStatement<T> {
             MachineStatement::LinkDeclaration(link) => {
                 write!(f, "{link}")
             }
-            MachineStatement::InlinePil(_, statements) => {
-                write!(f, "pil{{\n{}\n}}", statements.iter().format("\n"))
-            }
             MachineStatement::FunctionDeclaration(_, name, params, statements) => {
                 write!(
                     f,

book/src/SUMMARY.md

@@ -18,7 +18,7 @@
     - [Instructions](./asm/instructions.md)
     - [Operations](./asm/operations.md)
     - [Links](./asm/links.md)
-- [PIL](./pil/README.md)
+- [pil](./pil/README.md)
     - [Fixed Columns](./pil/fixed_columns.md)
     - [Macros](./pil/macros.md)
 - [Frontends](./frontends/README.md)

book/src/asm/instructions.md

@@ -16,7 +16,7 @@ Instructions feature:
 - a name
 - some inputs
 - some outputs
-- a set of PIL constraints to activate when the instruction is called
+- a set of [powdr-pil](../pil/) constraints to activate when the instruction is called
 
 # External instructions
 

book/src/asm/machines.md

@@ -8,7 +8,7 @@ Dynamic machines are defined by:
 - a degree, indicating the number of execution steps
 - a set of [registers](./registers.md), including a program counter
 - an [instruction set](./instructions.md)
-- constraints
+- a set of [powdr-pil](../pil/) statements
 - a set of [functions](./functions.md)
 - a set of submachines
 
@@ -36,7 +36,7 @@ An example of a simple constrained machine is the following:
 {{#include ../../../test_data/asm/book/simple_static.asm}}
 ```
 
-For more details on the constraints, check out the [pil](../pil) section of this book. Note that the parameters of the operation are columns declared within the constraints block.
+For more details on the powdr-pil statements, check out the [pil](../pil) section of this book. Note that the parameters of the operation are columns defined in powdr-pil statements.
 
 ## Submachines
 

book/src/pil/README.md

@@ -1,3 +1,3 @@
 # PIL
 
-powdr PIL is the lower level of abstraction in powdr. It is strongly inspired by and compatible with [Polygon zkEVM PIL](https://github.com/0xPolygonHermez/pilcom/). We refer to the [Polygon zkEVM PIL documentation](https://wiki.polygon.technology/docs/category/polynomial-identity-language/) and document deviations from the original design here.
+powdr-pil is the lower level of abstraction in powdr. It is strongly inspired by [Polygon zkEVM PIL](https://github.com/0xPolygonHermez/pilcom/). We refer to the [Polygon zkEVM PIL documentation](https://wiki.polygon.technology/docs/category/polynomial-identity-language/) and document deviations from the original design here.

book/src/pil/fixed_columns.md

@@ -1,6 +1,6 @@
 # Fixed columns
 
-powdr PIL requires the definition of fixed columns at the time of declaration.
+powdr-pil requires the definition of fixed columns at the time of declaration.
 
 For example:
 
@@ -12,7 +12,7 @@ A number of mechanisms are supported to declare fixed columns. Let `N` be the to
 
 ## Values with repetitions
 
-powdr PIL supports a basic language to define the value of constant columns using:
+powdr-pil supports a basic language to define the value of constant columns using:
 - arrays, for example `[1, 2, 3]`
 - repetition, for example `[1, 2]*`
 - concatenation, for example `[1, 2] + [3, 4]`

book/src/pil/macros.md

@@ -1,10 +1,10 @@
 # Macros
 
-powdr PIL exposes a macro system which can generate arbitrary powdr PIL code.
+powdr-pil exposes a macro system which can generate arbitrary powdr-pil code.
 
 ## Definition
 
-Let's define some macros which generate powdr PIL expressions:
+Let's define some macros which generate powdr-pil expressions:
 
 ```
 {{#include ../../../test_data/pil/fib_macro.pil:expression_macro_definitions}}
@@ -20,7 +20,7 @@ In particular, we can generate constraints inside macros:
 
 > Macros currently have global scope
 
-Usage of the defined macros happens as expected in powdr PIL code:
+Usage of the defined macros happens as expected in powdr-pil code:
 
 ```
 {{#include ../../../test_data/pil/fib_macro.pil:expression_macro_usage}}

executor/src/witgen/processor.rs

@@ -366,7 +366,7 @@ mod tests {
             for (i, row) in data.iter().enumerate() {
                 println!(
                     "{}",
-                    row.render(&format!("Row {i}"), true, &processor.witness_cols)
+                    row.render(&format!("Row {i}"), true, processor.witness_cols)
                 );
             }
 

parser/src/powdr.lalrpop

@@ -194,11 +194,15 @@ MachineStatement: MachineStatement<T> = {
     RegisterDeclaration,
     InstructionDeclaration,
     LinkDeclaration,
-    InlinePil,
+    PilStatementWithSemiColon,
     FunctionDeclaration,
     OperationDeclaration,
 }
 
+PilStatementWithSemiColon: MachineStatement<T> = {
+    <@L> <PilStatement> ";" => MachineStatement::Pil(<>)
+}
+
 Degree: MachineStatement<T> = {
     <@L> "degree" <Integer> ";" => MachineStatement::Degree(<>)
 }
@@ -271,10 +275,6 @@ Param: Param = {
         Param{name, ty}
 }
 
-InlinePil: MachineStatement<T> = {
-    <@L> "constraints" "{" <(<PilStatement> ";")*> "}" => MachineStatement::InlinePil(<>)
-}
-
 FunctionDeclaration: MachineStatement<T> = {
     <@L> "function" <Identifier> <Params> "{" <(<FunctionStatement>)*> "}" => MachineStatement::FunctionDeclaration(<>)
 }