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

Remove constraints blocks #652

Merged
merged 1 commit into from
Oct 4, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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?
Expand Down
12 changes: 5 additions & 7 deletions airgen/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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},
Expand Down Expand Up @@ -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(
Expand All @@ -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
Expand Down
7 changes: 2 additions & 5 deletions analysis/src/block_enforcer.rs
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -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
}
44 changes: 30 additions & 14 deletions analysis/src/macro_expansion.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was changed to a functional approach, as a statement can yield many, and iter_mut does not allow that. Hence the usage of flat_map here.

.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])
Copy link
Collaborator Author

@Schaeff Schaeff Oct 2, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would make more sense to me for expand_macros to take a single statement rather than a list, but I tried to keep this diff small.

.into_iter()
.map(|s| MachineStatement::Pil(start, s))
.collect(),
s => {
vec![s]
}
})
.collect();

Ok(machine)
}
Expand Down
29 changes: 13 additions & 16 deletions asm_to_pil/src/romgen.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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::{
Expand Down Expand Up @@ -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());
Expand Down
7 changes: 2 additions & 5 deletions asm_to_pil/src/vm_to_constrained.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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
Expand Down
14 changes: 2 additions & 12 deletions ast/src/asm_analysis/display.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
};

Expand Down Expand Up @@ -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)?;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it a problem that these might be ordered differently? I mean can we always re-parse stuff that is printed here?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you elaborate here? Within constraints, the order is preserved throughout the compiler, but eventually this should not be a requirement, right? There are no tests which parse outputs of this display afaik, this could make sense to add but it seems unrelated to this change.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm just wondering if it might make sense to move the pil a bit further up or what happens if you mix constraints and instruction declarations and such, but yes, unrelated to this PR.

write_items_indented(f, &self.links)?;

writeln!(f, "}}")
Expand Down Expand Up @@ -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,)
Expand Down
10 changes: 2 additions & 8 deletions ast/src/asm_analysis/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
2 changes: 0 additions & 2 deletions ast/src/asm_analysis/utils.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1 @@



2 changes: 1 addition & 1 deletion ast/src/parsed/asm.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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),
}
Expand Down
4 changes: 1 addition & 3 deletions ast/src/parsed/display.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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,
Expand Down
2 changes: 1 addition & 1 deletion book/src/SUMMARY.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion book/src/asm/instructions.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
4 changes: 2 additions & 2 deletions book/src/asm/machines.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion book/src/pil/README.md
Original file line number Diff line number Diff line change
@@ -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.
4 changes: 2 additions & 2 deletions book/src/pil/fixed_columns.md
Original file line number Diff line number Diff line change
@@ -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:

Expand All @@ -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]`
Expand Down
6 changes: 3 additions & 3 deletions book/src/pil/macros.md
Original file line number Diff line number Diff line change
@@ -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}}
Expand All @@ -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}}
Expand Down
2 changes: 1 addition & 1 deletion executor/src/witgen/processor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
);
}

Expand Down
10 changes: 5 additions & 5 deletions parser/src/powdr.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -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(<>)
}
Expand Down Expand Up @@ -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(<>)
}
Expand Down
Loading