diff --git a/README.md b/README.md index e60acb9661..430b0032a9 100644 --- a/README.md +++ b/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? diff --git a/airgen/src/lib.rs b/airgen/src/lib.rs index cd4a8ff22e..202ff7665c 100644 --- a/airgen/src/lib.rs +++ b/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) { - self.pil.extend(statements) + fn handle_pil_statement(&mut self, statement: PilStatement) { + 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 diff --git a/analysis/src/block_enforcer.rs b/analysis/src/block_enforcer.rs index 31eb86ab1b..b86fc20cb5 100644 --- a/analysis/src/block_enforcer.rs +++ b/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(mut file: AnalysisASMFile) -> AnalysisASMFile )), ]; - machine.constraints.push(PilBlock { - start: 0, - statements: embedded_constraints.into_iter().collect(), - }); + machine.pil.extend(embedded_constraints); } file } diff --git a/analysis/src/macro_expansion.rs b/analysis/src/macro_expansion.rs index 93ddc64c68..6106947c81 100644 --- a/analysis/src/macro_expansion.rs +++ b/analysis/src/macro_expansion.rs @@ -32,22 +32,38 @@ impl Folder for MacroExpander { type Error = Infallible; fn fold_machine(&mut self, mut machine: Machine) -> Result, 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) } diff --git a/asm_to_pil/src/romgen.rs b/asm_to_pil/src/romgen.rs index 2ad1f2af54..d015a4de98 100644 --- a/asm_to_pil/src/romgen.rs +++ b/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( 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()); diff --git a/asm_to_pil/src/vm_to_constrained.rs b/asm_to_pil/src/vm_to_constrained.rs index 01f4c21cf5..19ed3916e4 100644 --- a/asm_to_pil/src/vm_to_constrained.rs +++ b/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 ASMPILConverter { )); if !self.pil.is_empty() { - input.constraints.push(PilBlock { - start: 0, - statements: self.pil, - }); + input.pil.extend(self.pil); } input diff --git a/ast/src/asm_analysis/display.rs b/ast/src/asm_analysis/display.rs index 2a5b8b525e..a02650ceb0 100644 --- a/ast/src/asm_analysis/display.rs +++ b/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 Display for Machine { 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 Display for PilBlock { - 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,) diff --git a/ast/src/asm_analysis/mod.rs b/ast/src/asm_analysis/mod.rs index 0a79b2e69e..8cb330bac2 100644 --- a/ast/src/asm_analysis/mod.rs +++ b/ast/src/asm_analysis/mod.rs @@ -659,12 +659,6 @@ pub struct Return { pub values: Vec>, } -#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)] -pub struct PilBlock { - pub start: usize, - pub statements: Vec>, -} - #[derive(Clone, Default, Debug, PartialEq, Eq, PartialOrd, Ord)] pub struct SubmachineDeclaration { /// the name of this instance @@ -685,8 +679,8 @@ pub struct Machine { pub registers: Vec, /// The index of the program counter in the registers, if any pub pc: Option, - /// The set of contraint blocks - pub constraints: Vec>, + /// The set of pil statements + pub pil: Vec>, /// The set of instructions which can be invoked in functions pub instructions: Vec>, /// The set of low level links to other machines diff --git a/ast/src/asm_analysis/utils.rs b/ast/src/asm_analysis/utils.rs index b28b04f643..8b13789179 100644 --- a/ast/src/asm_analysis/utils.rs +++ b/ast/src/asm_analysis/utils.rs @@ -1,3 +1 @@ - - diff --git a/ast/src/parsed/asm.rs b/ast/src/parsed/asm.rs index 104d6a094b..7420d7a536 100644 --- a/ast/src/parsed/asm.rs +++ b/ast/src/parsed/asm.rs @@ -263,11 +263,11 @@ pub struct Instruction { #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)] pub enum MachineStatement { Degree(usize, AbstractNumberType), + Pil(usize, PilStatement), Submachine(usize, SymbolPath, String), RegisterDeclaration(usize, String, Option), InstructionDeclaration(usize, String, Instruction), LinkDeclaration(LinkDeclaration), - InlinePil(usize, Vec>), FunctionDeclaration(usize, String, Params, Vec>), OperationDeclaration(usize, String, OperationId, Params), } diff --git a/ast/src/parsed/display.rs b/ast/src/parsed/display.rs index 8e1f34e261..ca229465c1 100644 --- a/ast/src/parsed/display.rs +++ b/ast/src/parsed/display.rs @@ -137,6 +137,7 @@ impl Display for MachineStatement { 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 Display for MachineStatement { 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, diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index 65df9d1d18..4844a5c942 100644 --- a/book/src/SUMMARY.md +++ b/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) diff --git a/book/src/asm/instructions.md b/book/src/asm/instructions.md index 09a753f29c..a19d2223e9 100644 --- a/book/src/asm/instructions.md +++ b/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 diff --git a/book/src/asm/machines.md b/book/src/asm/machines.md index aca380c23a..a97dc66f55 100644 --- a/book/src/asm/machines.md +++ b/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 diff --git a/book/src/pil/README.md b/book/src/pil/README.md index 1cb389c035..f3ec5595e3 100644 --- a/book/src/pil/README.md +++ b/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. diff --git a/book/src/pil/fixed_columns.md b/book/src/pil/fixed_columns.md index 1ae6b37944..13b842648f 100644 --- a/book/src/pil/fixed_columns.md +++ b/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]` diff --git a/book/src/pil/macros.md b/book/src/pil/macros.md index 2ea986395d..56c06b02e8 100644 --- a/book/src/pil/macros.md +++ b/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}} diff --git a/executor/src/witgen/processor.rs b/executor/src/witgen/processor.rs index c65bf5e2c3..5d8a88fdaf 100644 --- a/executor/src/witgen/processor.rs +++ b/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) ); } diff --git a/parser/src/powdr.lalrpop b/parser/src/powdr.lalrpop index ea44064872..632b13ec79 100644 --- a/parser/src/powdr.lalrpop +++ b/parser/src/powdr.lalrpop @@ -194,11 +194,15 @@ MachineStatement: MachineStatement = { RegisterDeclaration, InstructionDeclaration, LinkDeclaration, - InlinePil, + PilStatementWithSemiColon, FunctionDeclaration, OperationDeclaration, } +PilStatementWithSemiColon: MachineStatement = { + <@L> ";" => MachineStatement::Pil(<>) +} + Degree: MachineStatement = { <@L> "degree" ";" => MachineStatement::Degree(<>) } @@ -271,10 +275,6 @@ Param: Param = { Param{name, ty} } -InlinePil: MachineStatement = { - <@L> "constraints" "{" <( ";")*> "}" => MachineStatement::InlinePil(<>) -} - FunctionDeclaration: MachineStatement = { <@L> "function" "{" <()*> "}" => MachineStatement::FunctionDeclaration(<>) } diff --git a/riscv/src/compiler.rs b/riscv/src/compiler.rs index b39810994e..bda24ac7f7 100644 --- a/riscv/src/compiler.rs +++ b/riscv/src/compiler.rs @@ -454,64 +454,60 @@ fn preamble() -> String { + r#" reg addr; - constraints { - x0 = 0; - } + x0 = 0; - constraints{ // ============== iszero check for X ======================= - col witness XInv; - col witness XIsZero; - XIsZero = 1 - X * XInv; - XIsZero * X = 0; - XIsZero * (1 - XIsZero) = 0; + col witness XInv; + col witness XIsZero; + XIsZero = 1 - X * XInv; + XIsZero * X = 0; + XIsZero * (1 - XIsZero) = 0; // =============== read-write memory ======================= - // Read-write memory. Columns are sorted by m_addr and - // then by m_step. m_change is 1 if and only if m_addr changes - // in the next row. - col witness m_addr; - col witness m_step; - col witness m_change; - col witness m_value; - // If we have an operation at all (needed because this needs to be a permutation) - col witness m_op; - // If the operation is a write operation. - col witness m_is_write; - col witness m_is_read; - - // positive numbers (assumed to be much smaller than the field order) - col fixed POSITIVE(i) { i + 1 }; - col fixed FIRST = [1] + [0]*; - col fixed LAST(i) { FIRST(i + 1) }; - col fixed STEP(i) { i }; - - m_change * (1 - m_change) = 0; - - // if m_change is zero, m_addr has to stay the same. - (m_addr' - m_addr) * (1 - m_change) = 0; - - // Except for the last row, if m_change is 1, then m_addr has to increase, - // if it is zero, m_step has to increase. - (1 - LAST) { m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step) } in POSITIVE; - - m_op * (1 - m_op) = 0; - m_is_write * (1 - m_is_write) = 0; - m_is_read * (1 - m_is_read) = 0; - // m_is_write can only be 1 if m_op is 1. - m_is_write * (1 - m_op) = 0; - m_is_read * (1 - m_op) = 0; - m_is_read * m_is_write = 0; - - - // If the next line is a read and we stay at the same address, then the - // value cannot change. - (1 - m_is_write') * (1 - m_change) * (m_value' - m_value) = 0; - - // If the next line is a read and we have an address change, - // then the value is zero. - (1 - m_is_write') * m_change * m_value' = 0; - } + // Read-write memory. Columns are sorted by m_addr and + // then by m_step. m_change is 1 if and only if m_addr changes + // in the next row. + col witness m_addr; + col witness m_step; + col witness m_change; + col witness m_value; + // If we have an operation at all (needed because this needs to be a permutation) + col witness m_op; + // If the operation is a write operation. + col witness m_is_write; + col witness m_is_read; + + // positive numbers (assumed to be much smaller than the field order) + col fixed POSITIVE(i) { i + 1 }; + col fixed FIRST = [1] + [0]*; + col fixed LAST(i) { FIRST(i + 1) }; + col fixed STEP(i) { i }; + + m_change * (1 - m_change) = 0; + + // if m_change is zero, m_addr has to stay the same. + (m_addr' - m_addr) * (1 - m_change) = 0; + + // Except for the last row, if m_change is 1, then m_addr has to increase, + // if it is zero, m_step has to increase. + (1 - LAST) { m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step) } in POSITIVE; + + m_op * (1 - m_op) = 0; + m_is_write * (1 - m_is_write) = 0; + m_is_read * (1 - m_is_read) = 0; + // m_is_write can only be 1 if m_op is 1. + m_is_write * (1 - m_op) = 0; + m_is_read * (1 - m_op) = 0; + m_is_read * m_is_write = 0; + + + // If the next line is a read and we stay at the same address, then the + // value cannot change. + (1 - m_is_write') * (1 - m_change) * (m_value' - m_value) = 0; + + // If the next line is a read and we have an address change, + // then the value is zero. + (1 - m_is_write') * m_change * m_value' = 0; // ============== memory instructions ============== @@ -578,19 +574,17 @@ fn preamble() -> String { instr wrap Y -> X { Y = X + wrap_bit * 2**32, X = X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000 } // Requires -2**32 <= Y < 2**32 instr wrap_signed Y -> X { Y + 2**32 = X + wrap_bit * 2**32, X = X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000 } - constraints{ - col fixed bytes(i) { i & 0xff }; - col witness X_b1; - col witness X_b2; - col witness X_b3; - col witness X_b4; - { X_b1 } in { bytes }; - { X_b2 } in { bytes }; - { X_b3 } in { bytes }; - { X_b4 } in { bytes }; - col witness wrap_bit; - wrap_bit * (1 - wrap_bit) = 0; - } + col fixed bytes(i) { i & 0xff }; + col witness X_b1; + col witness X_b2; + col witness X_b3; + col witness X_b4; + { X_b1 } in { bytes }; + { X_b2 } in { bytes }; + { X_b3 } in { bytes }; + { X_b4 } in { bytes }; + col witness wrap_bit; + wrap_bit * (1 - wrap_bit) = 0; // Input is a 32 bit unsigned number. We check bit 7 and set all higher bits to that value. instr sign_extend_byte Y -> X { @@ -598,11 +592,9 @@ fn preamble() -> String { Y = Y_7bit + wrap_bit * 0x80 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000, X = Y_7bit + wrap_bit * 0xffffff80 } - constraints{ - col fixed seven_bit(i) { i & 0x7f }; - col witness Y_7bit; - { Y_7bit } in { seven_bit }; - } + col fixed seven_bit(i) { i & 0x7f }; + col witness Y_7bit; + { Y_7bit } in { seven_bit }; // Input is a 32 bit unsigned number. We check bit 15 and set all higher bits to that value. instr sign_extend_16_bits Y -> X { @@ -612,9 +604,7 @@ fn preamble() -> String { Y = Y_15bit + wrap_bit * 0x8000 + X_b3 * 0x10000 + X_b4 * 0x1000000, X = Y_15bit + wrap_bit * 0xffff8000 } - constraints{ - col witness Y_15bit; - } + col witness Y_15bit; // Input is a 32 but unsigned number (0 <= Y < 2**32) interpreted as a two's complement numbers. // Returns a signed number (-2**31 <= X < 2**31). @@ -631,25 +621,23 @@ fn preamble() -> String { // Removes up to 16 bits beyond 32 // TODO is this really safe? instr wrap16 Y -> X { Y = Y_b5 * 2**32 + Y_b6 * 2**40 + X, X = X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000 } - constraints { - col witness Y_b5; - col witness Y_b6; - col witness Y_b7; - col witness Y_b8; - { Y_b5 } in { bytes }; - { Y_b6 } in { bytes }; - { Y_b7 } in { bytes }; - { Y_b8 } in { bytes }; - - col witness REM_b1; - col witness REM_b2; - col witness REM_b3; - col witness REM_b4; - { REM_b1 } in { bytes }; - { REM_b2 } in { bytes }; - { REM_b3 } in { bytes }; - { REM_b4 } in { bytes }; - } + col witness Y_b5; + col witness Y_b6; + col witness Y_b7; + col witness Y_b8; + { Y_b5 } in { bytes }; + { Y_b6 } in { bytes }; + { Y_b7 } in { bytes }; + { Y_b8 } in { bytes }; + + col witness REM_b1; + col witness REM_b2; + col witness REM_b3; + col witness REM_b4; + { REM_b1 } in { bytes }; + { REM_b2 } in { bytes }; + { REM_b3 } in { bytes }; + { REM_b4 } in { bytes }; // implements Z = Y / X and W = Y % X. instr divremu Y, X -> Z, W { diff --git a/std/binary.asm b/std/binary.asm index 63473e0ef3..8c3237a9a3 100644 --- a/std/binary.asm +++ b/std/binary.asm @@ -8,38 +8,36 @@ machine Binary(latch, operation_id) { operation xor<2> A, B -> C; - constraints{ - col witness operation_id; - - macro is_nonzero(X) { match X { 0 => 0, _ => 1, } }; - macro is_zero(X) { 1 - is_nonzero(X) }; - - col fixed latch(i) { is_zero((i % 4) - 3) }; - col fixed FACTOR(i) { 1 << (((i + 1) % 4) * 8) }; - - col fixed P_A(i) { i % 256 }; - col fixed P_B(i) { (i >> 8) % 256 }; - col fixed P_operation(i) { (i / (256 * 256)) % 3 }; - col fixed P_C(i) { - match P_operation(i) { - 0 => P_A(i) & P_B(i), - 1 => P_A(i) | P_B(i), - 2 => P_A(i) ^ P_B(i), - } & 0xff - }; - - col witness A_byte; - col witness B_byte; - col witness C_byte; - - col witness A; - col witness B; - col witness C; - - A' = A * (1 - latch) + A_byte * FACTOR; - B' = B * (1 - latch) + B_byte * FACTOR; - C' = C * (1 - latch) + C_byte * FACTOR; - - {operation_id', A_byte, B_byte, C_byte} in {P_operation, P_A, P_B, P_C}; - } + col witness operation_id; + + macro is_nonzero(X) { match X { 0 => 0, _ => 1, } }; + macro is_zero(X) { 1 - is_nonzero(X) }; + + col fixed latch(i) { is_zero((i % 4) - 3) }; + col fixed FACTOR(i) { 1 << (((i + 1) % 4) * 8) }; + + col fixed P_A(i) { i % 256 }; + col fixed P_B(i) { (i >> 8) % 256 }; + col fixed P_operation(i) { (i / (256 * 256)) % 3 }; + col fixed P_C(i) { + match P_operation(i) { + 0 => P_A(i) & P_B(i), + 1 => P_A(i) | P_B(i), + 2 => P_A(i) ^ P_B(i), + } & 0xff + }; + + col witness A_byte; + col witness B_byte; + col witness C_byte; + + col witness A; + col witness B; + col witness C; + + A' = A * (1 - latch) + A_byte * FACTOR; + B' = B * (1 - latch) + B_byte * FACTOR; + C' = C * (1 - latch) + C_byte * FACTOR; + + {operation_id', A_byte, B_byte, C_byte} in {P_operation, P_A, P_B, P_C}; } \ No newline at end of file diff --git a/std/hash/poseidon_bn254.asm b/std/hash/poseidon_bn254.asm index fdfad6697e..bfdceec30e 100644 --- a/std/hash/poseidon_bn254.asm +++ b/std/hash/poseidon_bn254.asm @@ -11,105 +11,103 @@ machine PoseidonBN254(LASTBLOCK, operation_id) { // hash functions. operation poseidon_permutation<0> input_in0, input_in1, input_cap -> in0; - constraints { - col witness operation_id; - - // Using parameters from https://eprint.iacr.org/2019/458.pdf - // See https://extgit.iaik.tugraz.at/krypto/hadeshash/-/blob/master/code/poseidonperm_x5_254_3.sage - - // The PIL is heavily inspired by Polygon's Poseidon PIL: - // https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/pil/poseidong.pil - - // Number of full rounds - constant %nRoundsF = 8; - // Number of partial rounds (half of them before and half of them after the full rounds) - constant %nRoundsP = 57; - constant %rowsPerHash = %nRoundsF + %nRoundsP + 1; - - pol constant L0 = [1] + [0]*; - pol constant FIRSTBLOCK(i) { match i % %rowsPerHash { - 0 => 1, - _ => 0 - }}; - pol constant LASTBLOCK(i) { match i % %rowsPerHash { - %rowsPerHash - 1 => 1, - _ => 0 - }}; - // Like LASTBLOCK, but also 1 in the last row of the table - // Specified this way because we can't access the degree in the match statement - pol constant LAST = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]* + [1]; - - // Whether the current round is a partial round - pol constant PARTIAL = [0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0]*; - - // The round constants - pol constant C_0 = [0x0ee9a592ba9a9518d05986d656f40c2114c4993c11bb29938d21d47304cd8e6e, 0x2f27be690fdaee46c3ce28f7532b13c856c35342c84bda6e20966310fadc01d0, 0x28813dcaebaeaa828a376df87af4a63bc8b7bf27ad49c6298ef7b387bf28526d, 0x15b52534031ae18f7f862cb2cf7cf760ab10a8150a337b1ccd99ff6e8797d428, 0x10520b0ab721cadfe9eff81b016fc34dc76da36c2578937817cb978d069de559, 0x04df5a56ff95bcafb051f7b1cd43a99ba731ff67e47032058fe3d4185697cc7d, 0x052cba2255dfd00c7c483143ba8d469448e43586a9b4cd9183fd0e843a6b9fa6, 0x03150b7cd6d5d17b2529d36be0f67b832c4acfc884ef4ee5ce15be0bfb4a8d09, 0x233237e3289baa34bb147e972ebcb9516469c399fcc069fb88f9da2cc28276b5, 0x2a73b71f9b210cf5b14296572c9d32dbf156e2b086ff47dc5df542365a404ec0, 0x0b7475b102a165ad7f5b18db4e1e704f52900aa3253baac68246682e56e9a28e, 0x29a795e7d98028946e947b75d54e9f044076e87a7b2883b47b675ef5f38bd66e, 0x143fd115ce08fb27ca38eb7cce822b4517822cd2109048d2e6d0ddcca17d71c8, 0x2e4ef510ff0b6fda5fa940ab4c4380f26a6bcb64d89427b824d6755b5db9e30c, 0x30509991f88da3504bbf374ed5aae2f03448a22c76234c8c990f01f33a735206, 0x2a1982979c3ff7f43ddd543d891c2abddd80f804c077d775039aa3502e43adef, 0x21576b438e500449a151e4eeaf17b154285c68f42d42c1808a11abf3764c0750, 0x162f5243967064c390e095577984f291afba2266c38f5abcd89be0f5b2747eab, 0x1d6f347725e4816af2ff453f0cd56b199e1b61e9f601e9ade5e88db870949da9, 0x174ad61a1448c899a25416474f4930301e5c49475279e0639a616ddc45bc7b54, 0x2a4c4fc6ec0b0cf52195782871c6dd3b381cc65f72e02ad527037a62aa1bd804, 0x00ef653322b13d6c889bc81715c37d77a6cd267d595c4a8909a5546c7c97cff1, 0x2a56ef9f2c53febadfda33575dbdbd885a124e2780bbea170e456baace0fa5be, 0x04c6187e41ed881dc1b239c88f7f9d43a9f52fc8c8b6cdd1e76e47615b51f100, 0x2ab3561834ca73835ad05f5d7acb950b4a9a2c666b9726da832239065b7c3b02, 0x154ac98e01708c611c4fa715991f004898f57939d126e392042971dd90e81fc6, 0x06746a6156eba54426b9e22206f15abca9a6f41e6f535c6f3525401ea0654626, 0x2b56973364c4c4f5c1a3ec4da3cdce038811eb116fb3e45bc1768d26fc0b3758, 0x0fdc1f58548b85701a6c5505ea332a29647e6f34ad4243c2ea54ad897cebe54d, 0x16243916d69d2ca3dfb4722224d4c462b57366492f45e90d8a81934f1bc3b147, 0x05a8c4f9968b8aa3b7b478a30f9a5b63650f19a75e7ce11ca9fe16c0b76c00bc, 0x27e88d8c15f37dcee44f1e5425a51decbd136ce5091a6767e49ec9544ccd101a, 0x15742e99b9bfa323157ff8c586f5660eac6783476144cdcadf2874be45466b1a, 0x15a5821565cc2ec2ce78457db197edf353b7ebba2c5523370ddccc3d9f146a67, 0x2ff7bc8f4380cde997da00b616b0fcd1af8f0e91e2fe1ed7398834609e0315d2, 0x00248156142fd0373a479f91ff239e960f599ff7e94be69b7f2a290305e1198d, 0x29aba33f799fe66c2ef3134aea04336ecc37e38c1cd211ba482eca17e2dbfae1, 0x22cdbc8b70117ad1401181d02e15459e7ccd426fe869c7c95d1dd2cb0f24af38, 0x1166d9e554616dba9e753eea427c17b7fecd58c076dfe42708b08f5b783aa9af, 0x2af41fbb61ba8a80fdcf6fff9e3f6f422993fe8f0a4639f962344c8225145086, 0x28201a34c594dfa34d794996c6433a20d152bac2a7905c926c40e285ab32eeb6, 0x0ec868e6d15e51d9644f66e1d6471a94589511ca00d29e1014390e6ee4254f5b, 0x0b2d722d0919a1aad8db58f10062a92ea0c56ac4270e822cca228620188a1d40, 0x0c2d0e3b5fd57549329bf6885da66b9b790b40defd2c8650762305381b168873, 0x1e6ff3216b688c3d996d74367d5cd4c1bc489d46754eb712c243f70d1b53cfbb, 0x2522b60f4ea3307640a0c2dce041fba921ac10a3d5f096ef4745ca838285f019, 0x0f9406b8296564a37304507b8dba3ed162371273a07b1fc98011fcd6ad72205f, 0x193a56766998ee9e0a8652dd2f3b1da0362f4f54f72379544f957ccdeefb420f, 0x04e1181763050e58013444dbcb99f1902b11bc25d90bbdca408d3819f4fed32b, 0x1382edce9971e186497eadb1aeb1f52b23b4b83bef023ab0d15228b4cceca59a, 0x0a59a158e3eec2117e6e94e7f0e9decf18c3ffd5e1531a9219636158bbaf62f2, 0x13d69fa127d834165ad5c7cba7ad59ed52e0b0f0e42d7fea95e1906b520921b1, 0x256e175a1dc079390ecd7ca703fb2e3b19ec61805d4f03ced5f45ee6dd0f69ec, 0x193edd8e9fcf3d7625fa7d24b598a1d89f3362eaf4d582efecad76f879e36860, 0x10646d2f2603de39a1f4ae5e7771a64a702db6e86fb76ab600bf573f9010c711, 0x0a6abd1d833938f33c74154e0404b4b40a555bbbec21ddfafd672dd62047f01a, 0x161b42232e61b84cbf1810af93a38fc0cece3d5628c9282003ebacb5c312c72b, 0x2c8120f268ef054f817064c369dda7ea908377feaba5c4dffbda10ef58e8c556, 0x23ff4f9d46813457cf60d92f57618399a5e022ac321ca550854ae23918a22eea, 0x3050e37996596b7f81f68311431d8734dba7d926d3633595e0c0d8ddf4f0f47f, 0x2796ea90d269af29f5f8acf33921124e4e4fad3dbe658945e546ee411ddaa9cb, 0x054efa1f65b0fce283808965275d877b438da23ce5b13e1963798cb1447d25a4, 0x1cfb5662e8cf5ac9226a80ee17b36abecb73ab5f87e161927b4349e10e4bdf08, 0x0fa3ec5b9488259c2eb4cf24501bfad9be2ec9e42c5cc8ccd419d2a692cad870, 0x0fe0af7858e49859e2a54d6f1ad945b1316aa24bfbdd23ae40a6d0cb70c3eab1, 0]*; - pol constant C_1 = [0x00f1445235f2148c5986587169fc1bcd887b08d4d00868df5696fff40956e864, 0x2b2ae1acf68b7b8d2416bebf3d4f6234b763fe04b8043ee48b8327bebca16cf2, 0x2727673b2ccbc903f181bf38e1c1d40d2033865200c352bc150928adddf9cb78, 0x0dc8fad6d9e4b35f5ed9a3d186b79ce38e0e8a8d1b58b132d701d4eecf68d1f6, 0x1f6d48149b8e7f7d9b257d8ed5fbbaf42932498075fed0ace88a9eb81f5627f6, 0x0672d995f8fff640151b3d290cedaf148690a10a8c8424a7f6ec282b6e4be828, 0x0b8badee690adb8eb0bd74712b7999af82de55707251ad7716077cb93c464ddc, 0x2cc6182c5e14546e3cf1951f173912355374efb83d80898abe69cb317c9ea565, 0x05c8f4f4ebd4a6e3c980d31674bfbe6323037f21b34ae5a4e80c2d4c24d60280, 0x1ac9b0417abcc9a1935107e9ffc91dc3ec18f2c4dbe7f22976a760bb5c50c460, 0x037c2849e191ca3edb1c5e49f6e8b8917c843e379366f2ea32ab3aa88d7f8448, 0x20439a0c84b322eb45a3857afc18f5826e8c7382c8a1585c507be199981fd22f, 0x0c64cbecb1c734b857968dbbdcf813cdf8611659323dbcbfc84323623be9caf1, 0x0081c95bc43384e663d79270c956ce3b8925b4f6d033b078b96384f50579400e, 0x1c3f20fd55409a53221b7c4d49a356b9f0a1119fb2067b41a7529094424ec6ad, 0x1c74ee64f15e1db6feddbead56d6d55dba431ebc396c9af95cad0f1315bd5c91, 0x2f17c0559b8fe79608ad5ca193d62f10bce8384c815f0906743d6930836d4a9e, 0x2b4cb233ede9ba48264ecd2c8ae50d1ad7a8596a87f29f8a7777a70092393311, 0x204b0c397f4ebe71ebc2d8b3df5b913df9e6ac02b68d31324cd49af5c4565529, 0x1a96177bcf4d8d89f759df4ec2f3cde2eaaa28c177cc0fa13a9816d49a38d2ef, 0x13ab2d136ccf37d447e9f2e14a7cedc95e727f8446f6d9d7e55afc01219fd649, 0x0e25483e45a665208b261d8ba74051e6400c776d652595d9845aca35d8a397d3, 0x1c8361c78eb5cf5decfb7a2d17b5c409f2ae2999a46762e8ee416240a8cb9af1, 0x13b37bd80f4d27fb10d84331f6fb6d534b81c61ed15776449e801b7ddc9c2967, 0x1d4d8ec291e720db200fe6d686c0d613acaf6af4e95d3bf69f7ed516a597b646, 0x0b339d8acca7d4f83eedd84093aef51050b3684c88f8b0b04524563bc6ea4da4, 0x0f18f5a0ecd1423c496f3820c549c27838e5790e2bd0a196ac917c7ff32077fb, 0x123769dd49d5b054dcd76b89804b1bcb8e1392b385716a5d83feb65d437f29ef, 0x12373a8251fea004df68abcf0f7786d4bceff28c5dbbe0c3944f685cc0a0b1f2, 0x1efbe46dd7a578b4f66f9adbc88b4378abc21566e1a0453ca13a4159cac04ac2, 0x20f057712cc21654fbfe59bd345e8dac3f7818c701b9c7882d9d57b72a32e83f, 0x2feed17b84285ed9b8a5c8c5e95a41f66e096619a7703223176c41ee433de4d1, 0x1aac285387f65e82c895fc6887ddf40577107454c6ec0317284f033f27d0c785, 0x2411d57a4813b9980efa7e31a1db5966dcf64f36044277502f15485f28c71727, 0x00b9831b948525595ee02724471bcd182e9521f6b7bb68f1e93be4febb0d3cbe, 0x171d5620b87bfb1328cf8c02ab3f0c9a397196aa6a542c2350eb512a2b2bcda9, 0x1e9bc179a4fdd758fdd1bb1945088d47e70d114a03f6a0e8b5ba650369e64973, 0x0ef042e454771c533a9f57a55c503fcefd3150f52ed94a7cd5ba93b9c7dacefd, 0x2de52989431a859593413026354413db177fbf4cd2ac0b56f855a888357ee466, 0x119e684de476155fe5a6b41a8ebc85db8718ab27889e85e781b214bace4827c3, 0x083efd7a27d1751094e80fefaf78b000864c82eb571187724a761f88c22cc4e7, 0x2af33e3f866771271ac0c9b3ed2e1142ecd3e74b939cd40d00d937ab84c98591, 0x1f790d4d7f8cf094d980ceb37c2453e957b54a9991ca38bbe0061d1ed6e562d4, 0x1162fb28689c27154e5a8228b4e72b377cbcafa589e283c35d3803054407a18d, 0x01ca8be73832b8d0681487d27d157802d741a6f36cdc2a0576881f9326478875, 0x23f0bee001b1029d5255075ddc957f833418cad4f52b6c3f8ce16c235572575b, 0x2360a8eb0cc7defa67b72998de90714e17e75b174a52ee4acb126c8cd995f0a8, 0x2a394a43934f86982f9be56ff4fab1703b2e63c8ad334834e4309805e777ae0f, 0x0fdb253dee83869d40c335ea64de8c5bb10eb82db08b5e8b1f5e5552bfd05f23, 0x03464990f045c6ee0819ca51fd11b0be7f61b8eb99f14b77e1e6634601d9e8b5, 0x06ec54c80381c052b58bf23b312ffd3ce2c4eba065420af8f4c23ed0075fd07b, 0x169a177f63ea681270b1c6877a73d21bde143942fb71dc55fd8a49f19f10c77b, 0x30102d28636abd5fe5f2af412ff6004f75cc360d3205dd2da002813d3e2ceeb2, 0x18168afd34f2d915d0368ce80b7b3347d1c7a561ce611425f2664d7aa51f0b5d, 0x0beb5e07d1b27145f575f1395a55bf132f90c25b40da7b3864d0242dcb1117fb, 0x1a679f5d36eb7b5c8ea12a4c2dedc8feb12dffeec450317270a6f19b34cf1860, 0x0ada10a90c7f0520950f7d47a60d5e6a493f09787f1564e5d09203db47de1a0b, 0x1c7c8824f758753fa57c00789c684217b930e95313bcb73e6e7b8649a4968f70, 0x09945a5d147a4f66ceece6405dddd9d0af5a2c5103529407dff1ea58f180426d, 0x15af1169396830a91600ca8102c35c426ceae5461e3f95d89d829518d30afd78, 0x202d7dd1da0f6b4b0325c8b3307742f01e15612ec8e9304a7cb0319e01d32d60, 0x1b162f83d917e93edb3308c29802deb9d8aa690113b2e14864ccf6e18e4165f1, 0x0f21177e302a771bbae6d8d1ecb373b62c99af346220ac0129c53f666eb24100, 0x193c0e04e0bd298357cb266c1506080ed36edce85c648cc085e8c57b1ab54bba, 0x216f6717bbc7dedb08536a2220843f4e2da5f1daa9ebdefde8a5ea7344798d22, 0]*; - pol constant C_2 = [0x08dff3487e8ac99e1f29a058d0fa80b930c728730b7ab36ce879f3890ecf73f5, 0x0319d062072bef7ecca5eac06f97d4d55952c175ab6b03eae64b44c7dbf11cfa, 0x234ec45ca27727c2e74abd2b2a1494cd6efbd43e340587d6b8fb9e31e65cc632, 0x1bcd95ffc211fbca600f705fad3fb567ea4eb378f62e1fec97805518a47e4d9c, 0x1d9655f652309014d29e00ef35a2089bfff8dc1c816f0dc9ca34bdb5460c8705, 0x099952b414884454b21200d7ffafdd5f0c9a9dcc06f2708e9fc1d8209b5c75b9, 0x119b1590f13307af5a1ee651020c07c749c15d60683a8050b963d0a8e4b2bdd1, 0x005032551e6378c450cfe129a404b3764218cadedac14e2b92d2cd73111bf0f9, 0x0a7b1db13042d396ba05d818a319f25252bcf35ef3aeed91ee1f09b2590fc65b, 0x12c0339ae08374823fabb076707ef479269f3e4d6cb104349015ee046dc93fc0, 0x05a6811f8556f014e92674661e217e9bd5206c5c93a07dc145fdb176a716346f, 0x2e0ba8d94d9ecf4a94ec2050c7371ff1bb50f27799a84b6d4a2a6f2a0982c887, 0x028a305847c683f646fca925c163ff5ae74f348d62c2b670f1426cef9403da53, 0x2ed5f0c91cbd9749187e2fade687e05ee2491b349c039a0bba8a9f4023a0bb38, 0x10b4e7f3ab5df003049514459b6e18eec46bb2213e8e131e170887b47ddcb96c, 0x07533ec850ba7f98eab9303cace01b4b9e4f2e8b82708cfa9c2fe45a0ae146a0, 0x2d477e3862d07708a79e8aae946170bc9775a4201318474ae665b0b1b7e2730e, 0x2c8fbcb2dd8573dc1dbaf8f4622854776db2eece6d85c4cf4254e7c35e03b07a, 0x0c4cb9dc3c4fd8174f1149b3c63c3c2f9ecb827cd7dc25534ff8fb75bc79c502, 0x066d04b24331d71cd0ef8054bc60c4ff05202c126a233c1a8242ace360b8a30a, 0x1121552fca26061619d24d843dc82769c1b04fcec26f55194c2e3e869acc6a9a, 0x29f536dcb9dd7682245264659e15d88e395ac3d4dde92d8c46448db979eeba89, 0x151aff5f38b20a0fc0473089aaf0206b83e8e68a764507bfd3d0ab4be74319c5, 0x01a5c536273c2d9df578bfbd32c17b7a2ce3664c2a52032c9321ceb1c4e8a8e4, 0x041294d2cc484d228f5784fe7919fd2bb925351240a04b711514c9c80b65af1d, 0x0955e49e6610c94254a4f84cfbab344598f0e71eaff4a7dd81ed95b50839c82e, 0x04f6eeca1751f7308ac59eff5beb261e4bb563583ede7bc92a738223d6f76e13, 0x2147b424fc48c80a88ee52b91169aacea989f6446471150994257b2fb01c63e9, 0x21e4f4ea5f35f85bad7ea52ff742c9e8a642756b6af44203dd8a1f35c1a90035, 0x07ea5e8537cf5dd08886020e23a7f387d468d5525be66f853b672cc96a88969a, 0x04a12ededa9dfd689672f8c67fee31636dcd8e88d01d49019bd90b33eb33db69, 0x1ed7cc76edf45c7c404241420f729cf394e5942911312a0d6972b8bd53aff2b8, 0x25851c3c845d4790f9ddadbdb6057357832e2e7a49775f71ec75a96554d67c77, 0x002e6f8d6520cd4713e335b8c0b6d2e647e9a98e12f4cd2558828b5ef6cb4c9b, 0x0a2f53768b8ebf6a86913b0e57c04e011ca408648a4743a87d77adbf0c9c3512, 0x170a4f55536f7dc970087c7c10d6fad760c952172dd54dd99d1045e4ec34a808, 0x1dd269799b660fad58f7f4892dfb0b5afeaad869a9c4b44f9c9e1c43bdaf8f09, 0x11609e06ad6c8fe2f287f3036037e8851318e8b08a0359a03b304ffca62e8284, 0x3006eb4ffc7a85819a6da492f3a8ac1df51aee5b17b8e89d74bf01cf5f71e9ad, 0x1835b786e2e8925e188bea59ae363537b51248c23828f047cff784b97b3fd800, 0x0b6f88a3577199526158e61ceea27be811c16df7774dd8519e079564f61fd13b, 0x0b520211f904b5e7d09b5d961c6ace7734568c547dd6858b364ce5e47951f178, 0x0171eb95dfbf7d1eaea97cd385f780150885c16235a2a6a8da92ceb01e504233, 0x2f1459b65dee441b64ad386a91e8310f282c5a92a89e19921623ef8249711bc0, 0x1f7735706ffe9fc586f976d5bdf223dc680286080b10cea00b9b5de315f9650e, 0x2bc1ae8b8ddbb81fcaac2d44555ed5685d142633e9df905f66d9401093082d59, 0x15871a5cddead976804c803cbaef255eb4815a5e96df8b006dcbbc2767f88948, 0x1859954cfeb8695f3e8b635dcb345192892cd11223443ba7b4166e8876c0d142, 0x058cbe8a9a5027bdaa4efb623adead6275f08686f1c08984a9d7c5bae9b4f1c0, 0x23f7bfc8720dc296fff33b41f98ff83c6fcab4605db2eb5aaa5bc137aeb70a58, 0x118872dc832e0eb5476b56648e867ec8b09340f7a7bcb1b4962f0ff9ed1f9d01, 0x04ef51591c6ead97ef42f287adce40d93abeb032b922f66ffb7e9a5a7450544d, 0x10998e42dfcd3bbf1c0714bc73eb1bf40443a3fa99bef4a31fd31be182fcc792, 0x29383c01ebd3b6ab0c017656ebe658b6a328ec77bc33626e29e2e95b33ea6111, 0x16d685252078c133dc0d3ecad62b5c8830f95bb2e54b59abdffbf018d96fa336, 0x0980fb233bd456c23974d50e0ebfde4726a423eada4e8f6ffbc7592e3f1b93d6, 0x1a730d372310ba82320345a29ac4238ed3f07a8a2b4e121bb50ddb9af407f451, 0x2cd9ed31f5f8691c8e39e4077a74faa0f400ad8b491eb3f7b47b27fa3fd1cf77, 0x188d9c528025d4c2b67660c6b771b90f7c7da6eaa29d3f268a6dd223ec6fc630, 0x1da6d09885432ea9a06d9f37f873d985dae933e351466b2904284da3320d8acc, 0x096d6790d05bb759156a952ba263d672a2d7f9c788f4c831a29dace4c0f8be5f, 0x21e5241e12564dd6fd9f1cdd2a0de39eedfefc1466cc568ec5ceb745a0506edc, 0x1671522374606992affb0dd7f71b12bec4236aede6290546bcef7e1f515c2320, 0x102adf8ef74735a27e9128306dcbc3c99f6f7291cd406578ce14ea2adaba68f8, 0x1da55cc900f0d21f4a3e694391918a1b3c23b2ac773c6b3ef88e2e4228325161, 0]*; - - // State of the Poseidon permutation - pol commit in0, in1, cap; - - // The initial state of the Poseidon permutation - // (constrained to be equal to (in0, in1, cap) in the first row and then repeated until - // the end of the block) - pol commit input_in0, input_in1, input_cap; - - // Add round constants - pol commit a0, a1, a2; - a0 = in0 + C_0; - a1 = in1 + C_1; - a2 = cap + C_2; - - // Compute S-Boxes (x^5) - pol commit x2_0, x4_0, x5_0; - x2_0 = a0 * a0; - x4_0 = x2_0 * x2_0; - x5_0 = x4_0 * a0; - - pol commit x2_1, x4_1, x5_1; - x2_1 = a1 * a1; - x4_1 = x2_1 * x2_1; - x5_1 = x4_1 * a1; - - pol commit x2_2, x4_2, x5_2; - x2_2 = a2 * a2; - x4_2 = x2_2 * x2_2; - x5_2 = x4_2 * a2; - - // Apply S-Boxes on the first element and otherwise if it is a full round. - pol commit b0, b1, b2; - b0 = x5_0; - b1 = PARTIAL * (a1 - x5_1) + x5_1; - b2 = PARTIAL * (a2 - x5_2) + x5_2; - - // The MDS matrix - constant %m_0_0 = 0x109b7f411ba0e4c9b2b70caf5c36a7b194be7c11ad24378bfedb68592ba8118b; - constant %m_0_1 = 0x16ed41e13bb9c0c66ae119424fddbcbc9314dc9fdbdeea55d6c64543dc4903e0; - constant %m_0_2 = 0x2b90bba00fca0589f617e7dcbfe82e0df706ab640ceb247b791a93b74e36736d; - constant %m_1_0 = 0x2969f27eed31a480b9c36c764379dbca2cc8fdd1415c3dded62940bcde0bd771; - constant %m_1_1 = 0x2e2419f9ec02ec394c9871c832963dc1b89d743c8c7b964029b2311687b1fe23; - constant %m_1_2 = 0x101071f0032379b697315876690f053d148d4e109f5fb065c8aacc55a0f89bfa; - constant %m_2_0 = 0x143021ec686a3f330d5f9e654638065ce6cd79e28c5b3753326244ee65a1b1a7; - constant %m_2_1 = 0x176cc029695ad02582a70eff08a6fd99d057e12e58e7d7b6b16cdfabc8ee2911; - constant %m_2_2 = 0x19a3fc0a56702bf417ba7fee3802593fa644470307043f7773279cd71d25d5e0; - - // Multiply with MDS Matrix - pol commit c0, c1, c2; - c0 = %m_0_0 * b0 + %m_0_1 * b1 + %m_0_2 * b2; - c1 = %m_1_0 * b0 + %m_1_1 * b1 + %m_1_2 * b2; - c2 = %m_2_0 * b0 + %m_2_1 * b1 + %m_2_2 * b2; - - (in0' - c0) * (1-LAST) = 0; - (in1' - c1) * (1-LAST) = 0; - (cap' - c2) * (1-LAST) = 0; - - FIRSTBLOCK * (input_in0 - in0) = 0; - FIRSTBLOCK * (input_in1 - in1) = 0; - FIRSTBLOCK * (input_cap - cap) = 0; - - (1 - LAST) * (input_in0 - input_in0') = 0; - (1 - LAST) * (input_in1 - input_in1') = 0; - (1 - LAST) * (input_cap - input_cap') = 0; - } + col witness operation_id; + + // Using parameters from https://eprint.iacr.org/2019/458.pdf + // See https://extgit.iaik.tugraz.at/krypto/hadeshash/-/blob/master/code/poseidonperm_x5_254_3.sage + + // The PIL is heavily inspired by Polygon's Poseidon PIL: + // https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/pil/poseidong.pil + + // Number of full rounds + constant %nRoundsF = 8; + // Number of partial rounds (half of them before and half of them after the full rounds) + constant %nRoundsP = 57; + constant %rowsPerHash = %nRoundsF + %nRoundsP + 1; + + pol constant L0 = [1] + [0]*; + pol constant FIRSTBLOCK(i) { match i % %rowsPerHash { + 0 => 1, + _ => 0 + }}; + pol constant LASTBLOCK(i) { match i % %rowsPerHash { + %rowsPerHash - 1 => 1, + _ => 0 + }}; + // Like LASTBLOCK, but also 1 in the last row of the table + // Specified this way because we can't access the degree in the match statement + pol constant LAST = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]* + [1]; + + // Whether the current round is a partial round + pol constant PARTIAL = [0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0]*; + + // The round constants + pol constant C_0 = [0x0ee9a592ba9a9518d05986d656f40c2114c4993c11bb29938d21d47304cd8e6e, 0x2f27be690fdaee46c3ce28f7532b13c856c35342c84bda6e20966310fadc01d0, 0x28813dcaebaeaa828a376df87af4a63bc8b7bf27ad49c6298ef7b387bf28526d, 0x15b52534031ae18f7f862cb2cf7cf760ab10a8150a337b1ccd99ff6e8797d428, 0x10520b0ab721cadfe9eff81b016fc34dc76da36c2578937817cb978d069de559, 0x04df5a56ff95bcafb051f7b1cd43a99ba731ff67e47032058fe3d4185697cc7d, 0x052cba2255dfd00c7c483143ba8d469448e43586a9b4cd9183fd0e843a6b9fa6, 0x03150b7cd6d5d17b2529d36be0f67b832c4acfc884ef4ee5ce15be0bfb4a8d09, 0x233237e3289baa34bb147e972ebcb9516469c399fcc069fb88f9da2cc28276b5, 0x2a73b71f9b210cf5b14296572c9d32dbf156e2b086ff47dc5df542365a404ec0, 0x0b7475b102a165ad7f5b18db4e1e704f52900aa3253baac68246682e56e9a28e, 0x29a795e7d98028946e947b75d54e9f044076e87a7b2883b47b675ef5f38bd66e, 0x143fd115ce08fb27ca38eb7cce822b4517822cd2109048d2e6d0ddcca17d71c8, 0x2e4ef510ff0b6fda5fa940ab4c4380f26a6bcb64d89427b824d6755b5db9e30c, 0x30509991f88da3504bbf374ed5aae2f03448a22c76234c8c990f01f33a735206, 0x2a1982979c3ff7f43ddd543d891c2abddd80f804c077d775039aa3502e43adef, 0x21576b438e500449a151e4eeaf17b154285c68f42d42c1808a11abf3764c0750, 0x162f5243967064c390e095577984f291afba2266c38f5abcd89be0f5b2747eab, 0x1d6f347725e4816af2ff453f0cd56b199e1b61e9f601e9ade5e88db870949da9, 0x174ad61a1448c899a25416474f4930301e5c49475279e0639a616ddc45bc7b54, 0x2a4c4fc6ec0b0cf52195782871c6dd3b381cc65f72e02ad527037a62aa1bd804, 0x00ef653322b13d6c889bc81715c37d77a6cd267d595c4a8909a5546c7c97cff1, 0x2a56ef9f2c53febadfda33575dbdbd885a124e2780bbea170e456baace0fa5be, 0x04c6187e41ed881dc1b239c88f7f9d43a9f52fc8c8b6cdd1e76e47615b51f100, 0x2ab3561834ca73835ad05f5d7acb950b4a9a2c666b9726da832239065b7c3b02, 0x154ac98e01708c611c4fa715991f004898f57939d126e392042971dd90e81fc6, 0x06746a6156eba54426b9e22206f15abca9a6f41e6f535c6f3525401ea0654626, 0x2b56973364c4c4f5c1a3ec4da3cdce038811eb116fb3e45bc1768d26fc0b3758, 0x0fdc1f58548b85701a6c5505ea332a29647e6f34ad4243c2ea54ad897cebe54d, 0x16243916d69d2ca3dfb4722224d4c462b57366492f45e90d8a81934f1bc3b147, 0x05a8c4f9968b8aa3b7b478a30f9a5b63650f19a75e7ce11ca9fe16c0b76c00bc, 0x27e88d8c15f37dcee44f1e5425a51decbd136ce5091a6767e49ec9544ccd101a, 0x15742e99b9bfa323157ff8c586f5660eac6783476144cdcadf2874be45466b1a, 0x15a5821565cc2ec2ce78457db197edf353b7ebba2c5523370ddccc3d9f146a67, 0x2ff7bc8f4380cde997da00b616b0fcd1af8f0e91e2fe1ed7398834609e0315d2, 0x00248156142fd0373a479f91ff239e960f599ff7e94be69b7f2a290305e1198d, 0x29aba33f799fe66c2ef3134aea04336ecc37e38c1cd211ba482eca17e2dbfae1, 0x22cdbc8b70117ad1401181d02e15459e7ccd426fe869c7c95d1dd2cb0f24af38, 0x1166d9e554616dba9e753eea427c17b7fecd58c076dfe42708b08f5b783aa9af, 0x2af41fbb61ba8a80fdcf6fff9e3f6f422993fe8f0a4639f962344c8225145086, 0x28201a34c594dfa34d794996c6433a20d152bac2a7905c926c40e285ab32eeb6, 0x0ec868e6d15e51d9644f66e1d6471a94589511ca00d29e1014390e6ee4254f5b, 0x0b2d722d0919a1aad8db58f10062a92ea0c56ac4270e822cca228620188a1d40, 0x0c2d0e3b5fd57549329bf6885da66b9b790b40defd2c8650762305381b168873, 0x1e6ff3216b688c3d996d74367d5cd4c1bc489d46754eb712c243f70d1b53cfbb, 0x2522b60f4ea3307640a0c2dce041fba921ac10a3d5f096ef4745ca838285f019, 0x0f9406b8296564a37304507b8dba3ed162371273a07b1fc98011fcd6ad72205f, 0x193a56766998ee9e0a8652dd2f3b1da0362f4f54f72379544f957ccdeefb420f, 0x04e1181763050e58013444dbcb99f1902b11bc25d90bbdca408d3819f4fed32b, 0x1382edce9971e186497eadb1aeb1f52b23b4b83bef023ab0d15228b4cceca59a, 0x0a59a158e3eec2117e6e94e7f0e9decf18c3ffd5e1531a9219636158bbaf62f2, 0x13d69fa127d834165ad5c7cba7ad59ed52e0b0f0e42d7fea95e1906b520921b1, 0x256e175a1dc079390ecd7ca703fb2e3b19ec61805d4f03ced5f45ee6dd0f69ec, 0x193edd8e9fcf3d7625fa7d24b598a1d89f3362eaf4d582efecad76f879e36860, 0x10646d2f2603de39a1f4ae5e7771a64a702db6e86fb76ab600bf573f9010c711, 0x0a6abd1d833938f33c74154e0404b4b40a555bbbec21ddfafd672dd62047f01a, 0x161b42232e61b84cbf1810af93a38fc0cece3d5628c9282003ebacb5c312c72b, 0x2c8120f268ef054f817064c369dda7ea908377feaba5c4dffbda10ef58e8c556, 0x23ff4f9d46813457cf60d92f57618399a5e022ac321ca550854ae23918a22eea, 0x3050e37996596b7f81f68311431d8734dba7d926d3633595e0c0d8ddf4f0f47f, 0x2796ea90d269af29f5f8acf33921124e4e4fad3dbe658945e546ee411ddaa9cb, 0x054efa1f65b0fce283808965275d877b438da23ce5b13e1963798cb1447d25a4, 0x1cfb5662e8cf5ac9226a80ee17b36abecb73ab5f87e161927b4349e10e4bdf08, 0x0fa3ec5b9488259c2eb4cf24501bfad9be2ec9e42c5cc8ccd419d2a692cad870, 0x0fe0af7858e49859e2a54d6f1ad945b1316aa24bfbdd23ae40a6d0cb70c3eab1, 0]*; + pol constant C_1 = [0x00f1445235f2148c5986587169fc1bcd887b08d4d00868df5696fff40956e864, 0x2b2ae1acf68b7b8d2416bebf3d4f6234b763fe04b8043ee48b8327bebca16cf2, 0x2727673b2ccbc903f181bf38e1c1d40d2033865200c352bc150928adddf9cb78, 0x0dc8fad6d9e4b35f5ed9a3d186b79ce38e0e8a8d1b58b132d701d4eecf68d1f6, 0x1f6d48149b8e7f7d9b257d8ed5fbbaf42932498075fed0ace88a9eb81f5627f6, 0x0672d995f8fff640151b3d290cedaf148690a10a8c8424a7f6ec282b6e4be828, 0x0b8badee690adb8eb0bd74712b7999af82de55707251ad7716077cb93c464ddc, 0x2cc6182c5e14546e3cf1951f173912355374efb83d80898abe69cb317c9ea565, 0x05c8f4f4ebd4a6e3c980d31674bfbe6323037f21b34ae5a4e80c2d4c24d60280, 0x1ac9b0417abcc9a1935107e9ffc91dc3ec18f2c4dbe7f22976a760bb5c50c460, 0x037c2849e191ca3edb1c5e49f6e8b8917c843e379366f2ea32ab3aa88d7f8448, 0x20439a0c84b322eb45a3857afc18f5826e8c7382c8a1585c507be199981fd22f, 0x0c64cbecb1c734b857968dbbdcf813cdf8611659323dbcbfc84323623be9caf1, 0x0081c95bc43384e663d79270c956ce3b8925b4f6d033b078b96384f50579400e, 0x1c3f20fd55409a53221b7c4d49a356b9f0a1119fb2067b41a7529094424ec6ad, 0x1c74ee64f15e1db6feddbead56d6d55dba431ebc396c9af95cad0f1315bd5c91, 0x2f17c0559b8fe79608ad5ca193d62f10bce8384c815f0906743d6930836d4a9e, 0x2b4cb233ede9ba48264ecd2c8ae50d1ad7a8596a87f29f8a7777a70092393311, 0x204b0c397f4ebe71ebc2d8b3df5b913df9e6ac02b68d31324cd49af5c4565529, 0x1a96177bcf4d8d89f759df4ec2f3cde2eaaa28c177cc0fa13a9816d49a38d2ef, 0x13ab2d136ccf37d447e9f2e14a7cedc95e727f8446f6d9d7e55afc01219fd649, 0x0e25483e45a665208b261d8ba74051e6400c776d652595d9845aca35d8a397d3, 0x1c8361c78eb5cf5decfb7a2d17b5c409f2ae2999a46762e8ee416240a8cb9af1, 0x13b37bd80f4d27fb10d84331f6fb6d534b81c61ed15776449e801b7ddc9c2967, 0x1d4d8ec291e720db200fe6d686c0d613acaf6af4e95d3bf69f7ed516a597b646, 0x0b339d8acca7d4f83eedd84093aef51050b3684c88f8b0b04524563bc6ea4da4, 0x0f18f5a0ecd1423c496f3820c549c27838e5790e2bd0a196ac917c7ff32077fb, 0x123769dd49d5b054dcd76b89804b1bcb8e1392b385716a5d83feb65d437f29ef, 0x12373a8251fea004df68abcf0f7786d4bceff28c5dbbe0c3944f685cc0a0b1f2, 0x1efbe46dd7a578b4f66f9adbc88b4378abc21566e1a0453ca13a4159cac04ac2, 0x20f057712cc21654fbfe59bd345e8dac3f7818c701b9c7882d9d57b72a32e83f, 0x2feed17b84285ed9b8a5c8c5e95a41f66e096619a7703223176c41ee433de4d1, 0x1aac285387f65e82c895fc6887ddf40577107454c6ec0317284f033f27d0c785, 0x2411d57a4813b9980efa7e31a1db5966dcf64f36044277502f15485f28c71727, 0x00b9831b948525595ee02724471bcd182e9521f6b7bb68f1e93be4febb0d3cbe, 0x171d5620b87bfb1328cf8c02ab3f0c9a397196aa6a542c2350eb512a2b2bcda9, 0x1e9bc179a4fdd758fdd1bb1945088d47e70d114a03f6a0e8b5ba650369e64973, 0x0ef042e454771c533a9f57a55c503fcefd3150f52ed94a7cd5ba93b9c7dacefd, 0x2de52989431a859593413026354413db177fbf4cd2ac0b56f855a888357ee466, 0x119e684de476155fe5a6b41a8ebc85db8718ab27889e85e781b214bace4827c3, 0x083efd7a27d1751094e80fefaf78b000864c82eb571187724a761f88c22cc4e7, 0x2af33e3f866771271ac0c9b3ed2e1142ecd3e74b939cd40d00d937ab84c98591, 0x1f790d4d7f8cf094d980ceb37c2453e957b54a9991ca38bbe0061d1ed6e562d4, 0x1162fb28689c27154e5a8228b4e72b377cbcafa589e283c35d3803054407a18d, 0x01ca8be73832b8d0681487d27d157802d741a6f36cdc2a0576881f9326478875, 0x23f0bee001b1029d5255075ddc957f833418cad4f52b6c3f8ce16c235572575b, 0x2360a8eb0cc7defa67b72998de90714e17e75b174a52ee4acb126c8cd995f0a8, 0x2a394a43934f86982f9be56ff4fab1703b2e63c8ad334834e4309805e777ae0f, 0x0fdb253dee83869d40c335ea64de8c5bb10eb82db08b5e8b1f5e5552bfd05f23, 0x03464990f045c6ee0819ca51fd11b0be7f61b8eb99f14b77e1e6634601d9e8b5, 0x06ec54c80381c052b58bf23b312ffd3ce2c4eba065420af8f4c23ed0075fd07b, 0x169a177f63ea681270b1c6877a73d21bde143942fb71dc55fd8a49f19f10c77b, 0x30102d28636abd5fe5f2af412ff6004f75cc360d3205dd2da002813d3e2ceeb2, 0x18168afd34f2d915d0368ce80b7b3347d1c7a561ce611425f2664d7aa51f0b5d, 0x0beb5e07d1b27145f575f1395a55bf132f90c25b40da7b3864d0242dcb1117fb, 0x1a679f5d36eb7b5c8ea12a4c2dedc8feb12dffeec450317270a6f19b34cf1860, 0x0ada10a90c7f0520950f7d47a60d5e6a493f09787f1564e5d09203db47de1a0b, 0x1c7c8824f758753fa57c00789c684217b930e95313bcb73e6e7b8649a4968f70, 0x09945a5d147a4f66ceece6405dddd9d0af5a2c5103529407dff1ea58f180426d, 0x15af1169396830a91600ca8102c35c426ceae5461e3f95d89d829518d30afd78, 0x202d7dd1da0f6b4b0325c8b3307742f01e15612ec8e9304a7cb0319e01d32d60, 0x1b162f83d917e93edb3308c29802deb9d8aa690113b2e14864ccf6e18e4165f1, 0x0f21177e302a771bbae6d8d1ecb373b62c99af346220ac0129c53f666eb24100, 0x193c0e04e0bd298357cb266c1506080ed36edce85c648cc085e8c57b1ab54bba, 0x216f6717bbc7dedb08536a2220843f4e2da5f1daa9ebdefde8a5ea7344798d22, 0]*; + pol constant C_2 = [0x08dff3487e8ac99e1f29a058d0fa80b930c728730b7ab36ce879f3890ecf73f5, 0x0319d062072bef7ecca5eac06f97d4d55952c175ab6b03eae64b44c7dbf11cfa, 0x234ec45ca27727c2e74abd2b2a1494cd6efbd43e340587d6b8fb9e31e65cc632, 0x1bcd95ffc211fbca600f705fad3fb567ea4eb378f62e1fec97805518a47e4d9c, 0x1d9655f652309014d29e00ef35a2089bfff8dc1c816f0dc9ca34bdb5460c8705, 0x099952b414884454b21200d7ffafdd5f0c9a9dcc06f2708e9fc1d8209b5c75b9, 0x119b1590f13307af5a1ee651020c07c749c15d60683a8050b963d0a8e4b2bdd1, 0x005032551e6378c450cfe129a404b3764218cadedac14e2b92d2cd73111bf0f9, 0x0a7b1db13042d396ba05d818a319f25252bcf35ef3aeed91ee1f09b2590fc65b, 0x12c0339ae08374823fabb076707ef479269f3e4d6cb104349015ee046dc93fc0, 0x05a6811f8556f014e92674661e217e9bd5206c5c93a07dc145fdb176a716346f, 0x2e0ba8d94d9ecf4a94ec2050c7371ff1bb50f27799a84b6d4a2a6f2a0982c887, 0x028a305847c683f646fca925c163ff5ae74f348d62c2b670f1426cef9403da53, 0x2ed5f0c91cbd9749187e2fade687e05ee2491b349c039a0bba8a9f4023a0bb38, 0x10b4e7f3ab5df003049514459b6e18eec46bb2213e8e131e170887b47ddcb96c, 0x07533ec850ba7f98eab9303cace01b4b9e4f2e8b82708cfa9c2fe45a0ae146a0, 0x2d477e3862d07708a79e8aae946170bc9775a4201318474ae665b0b1b7e2730e, 0x2c8fbcb2dd8573dc1dbaf8f4622854776db2eece6d85c4cf4254e7c35e03b07a, 0x0c4cb9dc3c4fd8174f1149b3c63c3c2f9ecb827cd7dc25534ff8fb75bc79c502, 0x066d04b24331d71cd0ef8054bc60c4ff05202c126a233c1a8242ace360b8a30a, 0x1121552fca26061619d24d843dc82769c1b04fcec26f55194c2e3e869acc6a9a, 0x29f536dcb9dd7682245264659e15d88e395ac3d4dde92d8c46448db979eeba89, 0x151aff5f38b20a0fc0473089aaf0206b83e8e68a764507bfd3d0ab4be74319c5, 0x01a5c536273c2d9df578bfbd32c17b7a2ce3664c2a52032c9321ceb1c4e8a8e4, 0x041294d2cc484d228f5784fe7919fd2bb925351240a04b711514c9c80b65af1d, 0x0955e49e6610c94254a4f84cfbab344598f0e71eaff4a7dd81ed95b50839c82e, 0x04f6eeca1751f7308ac59eff5beb261e4bb563583ede7bc92a738223d6f76e13, 0x2147b424fc48c80a88ee52b91169aacea989f6446471150994257b2fb01c63e9, 0x21e4f4ea5f35f85bad7ea52ff742c9e8a642756b6af44203dd8a1f35c1a90035, 0x07ea5e8537cf5dd08886020e23a7f387d468d5525be66f853b672cc96a88969a, 0x04a12ededa9dfd689672f8c67fee31636dcd8e88d01d49019bd90b33eb33db69, 0x1ed7cc76edf45c7c404241420f729cf394e5942911312a0d6972b8bd53aff2b8, 0x25851c3c845d4790f9ddadbdb6057357832e2e7a49775f71ec75a96554d67c77, 0x002e6f8d6520cd4713e335b8c0b6d2e647e9a98e12f4cd2558828b5ef6cb4c9b, 0x0a2f53768b8ebf6a86913b0e57c04e011ca408648a4743a87d77adbf0c9c3512, 0x170a4f55536f7dc970087c7c10d6fad760c952172dd54dd99d1045e4ec34a808, 0x1dd269799b660fad58f7f4892dfb0b5afeaad869a9c4b44f9c9e1c43bdaf8f09, 0x11609e06ad6c8fe2f287f3036037e8851318e8b08a0359a03b304ffca62e8284, 0x3006eb4ffc7a85819a6da492f3a8ac1df51aee5b17b8e89d74bf01cf5f71e9ad, 0x1835b786e2e8925e188bea59ae363537b51248c23828f047cff784b97b3fd800, 0x0b6f88a3577199526158e61ceea27be811c16df7774dd8519e079564f61fd13b, 0x0b520211f904b5e7d09b5d961c6ace7734568c547dd6858b364ce5e47951f178, 0x0171eb95dfbf7d1eaea97cd385f780150885c16235a2a6a8da92ceb01e504233, 0x2f1459b65dee441b64ad386a91e8310f282c5a92a89e19921623ef8249711bc0, 0x1f7735706ffe9fc586f976d5bdf223dc680286080b10cea00b9b5de315f9650e, 0x2bc1ae8b8ddbb81fcaac2d44555ed5685d142633e9df905f66d9401093082d59, 0x15871a5cddead976804c803cbaef255eb4815a5e96df8b006dcbbc2767f88948, 0x1859954cfeb8695f3e8b635dcb345192892cd11223443ba7b4166e8876c0d142, 0x058cbe8a9a5027bdaa4efb623adead6275f08686f1c08984a9d7c5bae9b4f1c0, 0x23f7bfc8720dc296fff33b41f98ff83c6fcab4605db2eb5aaa5bc137aeb70a58, 0x118872dc832e0eb5476b56648e867ec8b09340f7a7bcb1b4962f0ff9ed1f9d01, 0x04ef51591c6ead97ef42f287adce40d93abeb032b922f66ffb7e9a5a7450544d, 0x10998e42dfcd3bbf1c0714bc73eb1bf40443a3fa99bef4a31fd31be182fcc792, 0x29383c01ebd3b6ab0c017656ebe658b6a328ec77bc33626e29e2e95b33ea6111, 0x16d685252078c133dc0d3ecad62b5c8830f95bb2e54b59abdffbf018d96fa336, 0x0980fb233bd456c23974d50e0ebfde4726a423eada4e8f6ffbc7592e3f1b93d6, 0x1a730d372310ba82320345a29ac4238ed3f07a8a2b4e121bb50ddb9af407f451, 0x2cd9ed31f5f8691c8e39e4077a74faa0f400ad8b491eb3f7b47b27fa3fd1cf77, 0x188d9c528025d4c2b67660c6b771b90f7c7da6eaa29d3f268a6dd223ec6fc630, 0x1da6d09885432ea9a06d9f37f873d985dae933e351466b2904284da3320d8acc, 0x096d6790d05bb759156a952ba263d672a2d7f9c788f4c831a29dace4c0f8be5f, 0x21e5241e12564dd6fd9f1cdd2a0de39eedfefc1466cc568ec5ceb745a0506edc, 0x1671522374606992affb0dd7f71b12bec4236aede6290546bcef7e1f515c2320, 0x102adf8ef74735a27e9128306dcbc3c99f6f7291cd406578ce14ea2adaba68f8, 0x1da55cc900f0d21f4a3e694391918a1b3c23b2ac773c6b3ef88e2e4228325161, 0]*; + + // State of the Poseidon permutation + pol commit in0, in1, cap; + + // The initial state of the Poseidon permutation + // (constrained to be equal to (in0, in1, cap) in the first row and then repeated until + // the end of the block) + pol commit input_in0, input_in1, input_cap; + + // Add round constants + pol commit a0, a1, a2; + a0 = in0 + C_0; + a1 = in1 + C_1; + a2 = cap + C_2; + + // Compute S-Boxes (x^5) + pol commit x2_0, x4_0, x5_0; + x2_0 = a0 * a0; + x4_0 = x2_0 * x2_0; + x5_0 = x4_0 * a0; + + pol commit x2_1, x4_1, x5_1; + x2_1 = a1 * a1; + x4_1 = x2_1 * x2_1; + x5_1 = x4_1 * a1; + + pol commit x2_2, x4_2, x5_2; + x2_2 = a2 * a2; + x4_2 = x2_2 * x2_2; + x5_2 = x4_2 * a2; + + // Apply S-Boxes on the first element and otherwise if it is a full round. + pol commit b0, b1, b2; + b0 = x5_0; + b1 = PARTIAL * (a1 - x5_1) + x5_1; + b2 = PARTIAL * (a2 - x5_2) + x5_2; + + // The MDS matrix + constant %m_0_0 = 0x109b7f411ba0e4c9b2b70caf5c36a7b194be7c11ad24378bfedb68592ba8118b; + constant %m_0_1 = 0x16ed41e13bb9c0c66ae119424fddbcbc9314dc9fdbdeea55d6c64543dc4903e0; + constant %m_0_2 = 0x2b90bba00fca0589f617e7dcbfe82e0df706ab640ceb247b791a93b74e36736d; + constant %m_1_0 = 0x2969f27eed31a480b9c36c764379dbca2cc8fdd1415c3dded62940bcde0bd771; + constant %m_1_1 = 0x2e2419f9ec02ec394c9871c832963dc1b89d743c8c7b964029b2311687b1fe23; + constant %m_1_2 = 0x101071f0032379b697315876690f053d148d4e109f5fb065c8aacc55a0f89bfa; + constant %m_2_0 = 0x143021ec686a3f330d5f9e654638065ce6cd79e28c5b3753326244ee65a1b1a7; + constant %m_2_1 = 0x176cc029695ad02582a70eff08a6fd99d057e12e58e7d7b6b16cdfabc8ee2911; + constant %m_2_2 = 0x19a3fc0a56702bf417ba7fee3802593fa644470307043f7773279cd71d25d5e0; + + // Multiply with MDS Matrix + pol commit c0, c1, c2; + c0 = %m_0_0 * b0 + %m_0_1 * b1 + %m_0_2 * b2; + c1 = %m_1_0 * b0 + %m_1_1 * b1 + %m_1_2 * b2; + c2 = %m_2_0 * b0 + %m_2_1 * b1 + %m_2_2 * b2; + + (in0' - c0) * (1-LAST) = 0; + (in1' - c1) * (1-LAST) = 0; + (cap' - c2) * (1-LAST) = 0; + + FIRSTBLOCK * (input_in0 - in0) = 0; + FIRSTBLOCK * (input_in1 - in1) = 0; + FIRSTBLOCK * (input_cap - cap) = 0; + + (1 - LAST) * (input_in0 - input_in0') = 0; + (1 - LAST) * (input_in1 - input_in1') = 0; + (1 - LAST) * (input_cap - input_cap') = 0; } \ No newline at end of file diff --git a/std/hash/poseidon_gl.asm b/std/hash/poseidon_gl.asm index 5ad31f35ea..209d8bc4de 100644 --- a/std/hash/poseidon_gl.asm +++ b/std/hash/poseidon_gl.asm @@ -8,204 +8,201 @@ machine PoseidonGL(LASTBLOCK, operation_id) { // hash functions. operation poseidon_permutation<0> input_in0, input_in1, input_in2, input_in3, input_in4, input_in5, input_in6, input_in7, input_cap0, input_cap1, input_cap2, input_cap3 -> in0, in1, in2, in3; - - constraints { - col witness operation_id; - - // Ported from: - // - https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/pil/poseidong.pil - // - https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/src/sm/sm_poseidong.js - - // Difference between our and Polygon's implementation: - // - Polygon puts the latch on the first row, rather than the last. - // Instead of reserving extra columns to repeat the inputs throughout the entire block, - // they reserve extra columns to repeat the output. This saves some columns, because the - // function has more inputs than outputs. Should be fixed once #627 is fixed. - - // Number of full rounds - constant %nRoundsF = 8; - // Number of partial rounds (half of them before and half of them after the full rounds) - constant %nRoundsP = 22; - constant %rowsPerHash = %nRoundsF + %nRoundsP + 1; - - pol constant L0 = [1] + [0]*; - pol constant FIRSTBLOCK(i) { match i % %rowsPerHash { - 0 => 1, - _ => 0 - }}; - pol constant LASTBLOCK(i) { match i % %rowsPerHash { - %rowsPerHash - 1 => 1, - _ => 0 - }}; - // Like LASTBLOCK, but also 1 in the last row of the table - // Specified this way because we can't access the degree in the match statement - pol constant LAST = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]* + [1]; - - // Whether the current round is a partial round - pol constant PARTIAL = [0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0]*; - - // The round constants - pol constant C_0 = [0xb585f766f2144405, 0x86287821f722c881, 0xe9fa634a21de0082, 0x92a756e67e2b9413, 0x3cc3f892184df408, 0x7131aa45268d7d8c, 0x99ad1aab0814283b, 0xeb84f608da56ef48, 0x7159cd30c3ac118e, 0xdcef0797c2b69ec7, 0xd0762cbc8ca6570c, 0x30a4680593258387, 0x15a16a8a8322d458, 0x5a3f1bb1c53a9645, 0x775005982d74d7f7, 0xf9cc95c22b4c1fcc, 0xc49366bb25e8513, 0xdd611f1000c17442, 0x2ff876fa5ef97c4, 0x3d06c8bd1514e2d9, 0xe89cd854d5d01d33, 0xece5a71e0cfedc75, 0x90004c1371b893c5, 0xde122bebe9a39368, 0x4d61e56a525d225a, 0x1478d361dbbf9fac, 0x475cd3205a3bdcde, 0xe70201e960cb78b8, 0x7be5b9ffda905e1c, 0xf3c12fe54d5c653b, 0x0]*; - pol constant C_1 = [0x7746a55f43921ad7, 0x59cd1a8a41c18e55, 0xf56f6d48959a600d, 0x70e741ebfee96586, 0x2e479dc157bf31bb, 0x9351036095630f9f, 0x438a7c91d416ca4d, 0xda608834c40e603d, 0x839b4e8fafead540, 0x3d639263da827b13, 0x34c6efb812b04bf5, 0x337dc00c61bd9ce1, 0x388a128b7fd9a609, 0xdb7f023869fb8d38, 0x86ab99b4dde6c8b0, 0x8d37f755f4ae9f6, 0x784d3d2f1698309, 0xd8185f9adfea4fd0, 0xc5cb72a2a51159b0, 0x9c9c98207cb10767, 0x5cd377dc8bb882a2, 0x5ff98fd5d51fe610, 0xb932b7cf752e5545, 0x4d001fd58f002526, 0x262e963c8da05d3d, 0x6f02dc07d141875c, 0x18a42105c31b7e88, 0x6f90ff3b6a65f108, 0xa3c95eaec244aa30, 0x40b9e922ed9771e2, 0x0]*; - pol constant C_2 = [0xb2fb0d31cee799b4, 0xc3b919ad495dc574, 0xf7d713e806391165, 0x19d5ee2af82ec1c, 0x6f49de07a6234346, 0xad535b24afc26bfb, 0xb60de3bcc5ea751c, 0x8f97fe408061f183, 0xd3f3e5e82920adc, 0xe273fd971bc8d0e7, 0x40bf0ab5fa14c112, 0xd5eca244c7a4ff1d, 0x2300e5d6baedf0fb, 0xb462065911d4e1fc, 0xb1204f603f51c080, 0xeec49b613478675b, 0x530fb67ea1809a81, 0xef87139ca9a3ab1e, 0x8470f39d2d5c900e, 0x65700b51aedfb5ef, 0xa7b0fb7883eee860, 0x83e8941918964615, 0xa0b1df81b6fe59fc, 0xca6637000eb4a9f8, 0x59e89b094d220ec2, 0x296a202ed8e556a2, 0x23e7414af663068, 0x42747a7245e7fa84, 0x230bca8f4df0544, 0x551f5b0fbe7b1840, 0x0]*; - pol constant C_3 = [0xf6760a4803427d7, 0xa484c4c5ef6a0781, 0x8297132b32825daf, 0x6f6f2ed772466352, 0x213ce7bede378d7b, 0x4627f5c6993e44be, 0xc99cab6aef6f58bc, 0xa93f485c96f37b89, 0x8f7d83bddee7bba8, 0x418f02702d227ed5, 0xb6b570fc7c5740d3, 0x7762638264d279bd, 0x2f63aa8647e15104, 0x49c24ae4437d8030, 0xef61ac8470250ecf, 0xf143933aed25e0b0, 0x410492299bb01f49, 0x3ba71336c34ee133, 0x25abb3f1d39fcb76, 0x911f451539869408, 0x7684403ec392950d, 0x5922040b47f150c1, 0x8ef1dd26770af2c2, 0x2f2339d624f91f78, 0x55d5b52b78b9c5e, 0x2afd67999bf32ee5, 0x15147108121967d7, 0xd1f507e43ab749b2, 0x4135c2bebfe148c6, 0x25032aa7c4cb1811, 0x0]*; - pol constant C_4 = [0xe10d666650f4e012, 0x308bbd23dc5416cc, 0xad6805e0e30b2c8a, 0x7cf416cfe7e14ca1, 0x5b0431345d4dea83, 0x645cf794b8f1cc58, 0x69a5ed92a72ee4ff, 0x6704e8ee8f18d563, 0x780f2243ea071d06, 0x8c25fda3b503038c, 0x5a27b9002de33454, 0xc1e434bedeefd767, 0xf1c36ce86ecec269, 0xd793862c112b0566, 0x1bbcd90f132c603f, 0xe4c5dd8255dfc622, 0x139542347424b9ac, 0x7d3a455d56b70238, 0x23eb8cc9b372442f, 0x7ae6849fbc3a0ec6, 0x5fa3f06f4fed3b52, 0xf97d750e3dd94521, 0x541a4f9cfbeed35, 0x6d1a7918c80df518, 0x82b27eb33514ef99, 0x7acfd96efa95491d, 0xe4a3dff1d7d6fef9, 0x1c86d265f15750cd, 0x166fc0cc438a3c72, 0xaaed34074b164346, 0x0]*; - pol constant C_5 = [0x8cae14cb07d09bf1, 0x6e4a40c18f30c09c, 0xac51d9f5fcf8535e, 0x61df517b86a46439, 0xa2de45780344d6a1, 0x241c70ed0af61617, 0x5e7b329c1ed4ad71, 0xcee3e9ac1e072119, 0xeb915845f3de1634, 0x2cbaed4daec8c07c, 0xb1a5b165b6d2b2d2, 0x299351a53b8ec22, 0x27181125183970c9, 0xaadd1106730d8feb, 0xcd1dabd964db557, 0xe7ad7756f193198e, 0x9cb0bd5ea1a1115e, 0x660d32e130182684, 0xd687ba55c64f6364, 0x3bb340eba06afe7e, 0x8df57ac11bc04831, 0x5080d4c2b86f56d7, 0x9e61106178bfc530, 0xdf9a4939342308e9, 0xd30094ca96b7ce7b, 0x6798ba0c0abb2c6d, 0x1a8d1a588085737, 0x3996ce73dd832c1c, 0x3762b59a8ae83efa, 0x8ffd96bbf9c9c81d, 0x0]*; - pol constant C_6 = [0xd438539c95f63e9f, 0x9a2eedb70d8f8cfa, 0x502ad7dc18c2ad87, 0x85dc499b11d77b75, 0x7103aaf94a7bf308, 0xacb8e076647905f1, 0x5fc0ac0800144885, 0x510d0e65e2b470c1, 0xd19e120d26b6f386, 0x5f58e6afcdd6ddc2, 0x8722e0ace9d1be22, 0xb2d456e4ad251b80, 0xe584029370dca96d, 0xc43b6e0e97b0d568, 0x11a3ae5beb9d1ec9, 0x92c2318b87fff9cb, 0x2e3f615c38f49a1, 0x297a863f48cd1f43, 0xda8d9e90fd8ff158, 0xb46e9d8b682ea65e, 0x2db01efa1e1e1897, 0xa7de115b56c78d70, 0xb3767e80935d8af2, 0xebc2151ee6c8398c, 0xcf5cb381cd0a1535, 0x34c6f57b26c92122, 0x11b4c74eda62beef, 0x8e7fba02983224bd, 0xe8928a4c89114750, 0x70fc91eb5937085c, 0x0]*; - pol constant C_7 = [0xef781c7ce35b4c3d, 0xe360c6e0ae486f38, 0x57a1550c110b3041, 0x4b959b48b9c10733, 0x5326fc0d97279301, 0x3737e9db4c4f474d, 0x32db829239774eca, 0xf6323f486b9038f0, 0x16ee53a7e5fecc6, 0x284650ac5e1b0eba, 0x788ee3b37e5680fb, 0x3e9ed1fda49cea0b, 0x4d9bbc3e02f1cfb2, 0xe29024c18ee6fca2, 0xf755bfeea585d11d, 0x739c25f8fd73596d, 0x985d4f4a9c5291ef, 0x90e0a736a751ebb7, 0xe3cbdc7d2fe45ea7, 0x8dcf22f9a3b34356, 0x54846de4aadb9ca2, 0x6a9242ac87538194, 0x98d5782065af06, 0x3cc2ba8a1116515, 0xfeed4db6919e5a7c, 0x5736e1bad206b5de, 0xe587cc0d69a73346, 0xba0dec7103255dd4, 0x2a440b51a4945ee5, 0x7f795e2a5f915440, 0x0]*; - pol constant C_8 = [0xcdc4a239b0c44426, 0xd5c7718fbfc647fb, 0x66bbd30e6ce0e583, 0xe8be3e5da8043e57, 0xa9ceb74fec024747, 0xe7ea5e33e75fffb6, 0xade699c5830f310, 0xb508cdeffa5ceef, 0xcb5fd54e7933e477, 0x635b337ee819dab5, 0x14a726661551e284, 0x2972a92ba450bed8, 0xea35bc29692af6f8, 0x5e50c27535b88c66, 0xa3b83250268ea4d7, 0x5636cac9f16dfed0, 0x775b9feafdcd26e7, 0x549f80ce550c4fd3, 0xb9a8c9b3aee52297, 0x77bdaeda586257a7, 0xba6745385893c784, 0xf7856ef7f9173e44, 0x31d191cd5c1466c7, 0xd341d037e840cf83, 0x41703f53753be59f, 0x20057d2a0056521b, 0x1ff7327017aa2a6e, 0x9e9cbd781628fc5b, 0x80cefd2b7d99ff83, 0x4543d9df5476d3cb, 0x0]*; - pol constant C_9 = [0x277fa208bf337bff, 0xc35eae071903ff0b, 0xda2abef589d644e, 0xf5c0bc1de6da8699, 0x27f8ec88bb21b1a3, 0x90dee49fc9bfc23a, 0x7cc5583b10415f21, 0xf2417089e4fb3cbd, 0xacb8417879fd449f, 0x9f9a036ed4f2d49f, 0x98b7672f9ef3b419, 0x20216dd77be493de, 0x18e21b4beabb4137, 0x10383f20a4ff9a87, 0x516306f4927c93af, 0xdd8f909a938e0172, 0x304265a6384f0f2d, 0xf73b2922f38bd64, 0xc0d28a5c10960bd3, 0xf19e400a5104d20d, 0x541d496344d2c75b, 0x2265fc92feb0dc09, 0x410fefafa319ac9d, 0x387cb5d25af4afcc, 0x5eeea940fcde8b6f, 0x3dea5bd5d0578bd7, 0x594e29c42473d06b, 0xdae8645996edd6a5, 0xbb9879c6e61fd62a, 0xf172d73e004fc90d, 0x0]*; - pol constant C_10 = [0xe17653a29da578a1, 0x849c2656969c4be7, 0xf061274fdb150d61, 0x40b12cbf09ef74bf, 0xfceb4fda1ded0893, 0xd1b1edf76bc09c92, 0x85df9ed2e166d64f, 0x60e75c2890d15730, 0x9c22190be7f74732, 0xb93e260cae5c170e, 0xbb93ae776bb30e3a, 0xadffe8cf28449ec6, 0x1e3b9fc625b554f4, 0x38e8ee9d71a45af8, 0xddb4ac49c9efa1da, 0xc6401fe115063f5b, 0x593664c39773012c, 0x16bf1f73fb7a9c3f, 0x45d7ac9b68f71a34, 0xc368a348e46d950f, 0xe909678474e687fe, 0x17dfc8e4f7ba8a57, 0xbdf8f242e316c4ab, 0xbba2515f22909e87, 0x4cd1f1b175100206, 0x16e50d897d4634ac, 0xf6f31db1899b12d5, 0xdebe0853b1a1d378, 0x6e7c8f1a84265034, 0xdfd1c4febcc81238, 0x0]*; - pol constant C_11 = [0xc54302f225db2c76, 0xc0572c8c08cbbbad, 0x28b8ec3ae9c29633, 0xa637093ecb2ad631, 0xfac6ff1346a41675, 0xb65481ba645c602, 0x6604df4fee32bcb1, 0xa6217d8bf660f29c, 0x5d693c1ba3ba3621, 0xb0a7eae879ddb76d, 0x28fd3b046380f850, 0x1c4dbb1c4c27d243, 0x25d64362697828fd, 0xdd5118375bf1a9b9, 0x64bb6dec369d4418, 0x8ad97b33f1ac1455, 0x4f0a2e5fb028f2ce, 0x6d1f5a59005bec17, 0xeeb76e397069e804, 0x9ef1cd60e679f284, 0xdfe89923f6c9c2ff, 0x9001a64209f21db8, 0x9e8cd55b57637ed0, 0x7248fe7705f38e47, 0x4a20358574454ec0, 0x29bff3ecb9b7a6e3, 0xc02ac5e47312d3ca, 0xa49229d24d014343, 0x164bb2de1bbeddc8, 0xbc8dfb627fe558fc, 0x0]*; - - // State of the Poseidon permutation - pol commit in0, in1, in2, in3, in4, in5, in6, in7, cap0, cap1, cap2, cap3; - - // The initial state of the Poseidon permutation - // (constrained to be equal to (in0, in1, in2, in3, in4, in5, in6, in7, cap0, cap1, cap2, cap3) - // in the first row and then repeated until the end of the block) - pol commit input_in0, input_in1, input_in2, input_in3, input_in4, input_in5, input_in6, input_in7, input_cap0, input_cap1, input_cap2, input_cap3; - - // Add round constants - pol a0 = in0 + C_0; - pol a1 = in1 + C_1; - pol a2 = in2 + C_2; - pol a3 = in3 + C_3; - pol a4 = in4 + C_4; - pol a5 = in5 + C_5; - pol a6 = in6 + C_6; - pol a7 = in7 + C_7; - pol a8 = cap0 + C_8; - pol a9 = cap1 + C_9; - pol a10 = cap2 + C_10; - pol a11 = cap3 + C_11; - - // Compute S-Boxes (x^7) - pol x2_0 = a0 * a0; - pol x4_0 = x2_0 * x2_0; - pol x6_0 = x2_0 * x4_0; - pol x7_0 = x6_0 * a0; - - pol x2_1 = a1 * a1; - pol x4_1 = x2_1 * x2_1; - pol x6_1 = x2_1 * x4_1; - pol x7_1 = x6_1 * a1; - - pol x2_2 = a2 * a2; - pol x4_2 = x2_2 * x2_2; - pol x6_2 = x2_2 * x4_2; - pol x7_2 = x6_2 * a2; - - pol x2_3 = a3 * a3; - pol x4_3 = x2_3 * x2_3; - pol x6_3 = x2_3 * x4_3; - pol x7_3 = x6_3 * a3; - - pol x2_4 = a4 * a4; - pol x4_4 = x2_4 * x2_4; - pol x6_4 = x2_4 * x4_4; - pol x7_4 = x6_4 * a4; - - pol x2_5 = a5 * a5; - pol x4_5 = x2_5 * x2_5; - pol x6_5 = x2_5 * x4_5; - pol x7_5 = x6_5 * a5; - - pol x2_6 = a6 * a6; - pol x4_6 = x2_6 * x2_6; - pol x6_6 = x2_6 * x4_6; - pol x7_6 = x6_6 * a6; - - pol x2_7 = a7 * a7; - pol x4_7 = x2_7 * x2_7; - pol x6_7 = x2_7 * x4_7; - pol x7_7 = x6_7 * a7; - - pol x2_8 = a8 * a8; - pol x4_8 = x2_8 * x2_8; - pol x6_8 = x2_8 * x4_8; - pol x7_8 = x6_8 * a8; - - pol x2_9 = a9 * a9; - pol x4_9 = x2_9 * x2_9; - pol x6_9 = x2_9 * x4_9; - pol x7_9 = x6_9 * a9; - - pol x2_10 = a10 * a10; - pol x4_10 = x2_10 * x2_10; - pol x6_10 = x2_10 * x4_10; - pol x7_10 = x6_10 * a10; - - pol x2_11 = a11 * a11; - pol x4_11 = x2_11 * x2_11; - pol x6_11 = x2_11 * x4_11; - pol x7_11 = x6_11 * a11; - - // Apply S-Boxes on the first element and otherwise if it is a full round. - pol b0 = x7_0; - pol b1 = PARTIAL * (a1 - x7_1) + x7_1; - pol b2 = PARTIAL * (a2 - x7_2) + x7_2; - pol b3 = PARTIAL * (a3 - x7_3) + x7_3; - pol b4 = PARTIAL * (a4 - x7_4) + x7_4; - pol b5 = PARTIAL * (a5 - x7_5) + x7_5; - pol b6 = PARTIAL * (a6 - x7_6) + x7_6; - pol b7 = PARTIAL * (a7 - x7_7) + x7_7; - pol b8 = PARTIAL * (a8 - x7_8) + x7_8; - pol b9 = PARTIAL * (a9 - x7_9) + x7_9; - pol b10 = PARTIAL * (a10 - x7_10) + x7_10; - pol b11 = PARTIAL * (a11 - x7_11) + x7_11; - - // Multiply with MDS Matrix - pol c0 = 25*b0 + 15*b1 + 41*b2 + 16*b3 + 2*b4 + 28*b5 + 13*b6 + 13*b7 + 39*b8 + 18*b9 + 34*b10 + 20*b11; - pol c1 = 20*b0 + 17*b1 + 15*b2 + 41*b3 + 16*b4 + 2*b5 + 28*b6 + 13*b7 + 13*b8 + 39*b9 + 18*b10 + 34*b11 ; - pol c2 = 34*b0 + 20*b1 + 17*b2 + 15*b3 + 41*b4 + 16*b5 + 2*b6 + 28*b7 + 13*b8 + 13*b9 + 39*b10 + 18*b11; - pol c3 = 18*b0 + 34*b1 + 20*b2 + 17*b3 + 15*b4 + 41*b5 + 16*b6 + 2*b7 + 28*b8 + 13*b9 + 13*b10 + 39*b11; - pol c4 = 39*b0 + 18*b1 + 34*b2 + 20*b3 + 17*b4 + 15*b5 + 41*b6 + 16*b7 + 2*b8 + 28*b9 + 13*b10 + 13*b11; - pol c5 = 13*b0 + 39*b1 + 18*b2 + 34*b3 + 20*b4 + 17*b5 + 15*b6 + 41*b7 + 16*b8 + 2*b9 + 28*b10 + 13*b11; - pol c6 = 13*b0 + 13*b1 + 39*b2 + 18*b3 + 34*b4 + 20*b5 + 17*b6 + 15*b7 + 41*b8 + 16*b9 + 2*b10 + 28*b11; - pol c7 = 28*b0 + 13*b1 + 13*b2 + 39*b3 + 18*b4 + 34*b5 + 20*b6 + 17*b7 + 15*b8 + 41*b9 + 16*b10 + 2*b11; - pol c8 = 2*b0 + 28*b1 + 13*b2 + 13*b3 + 39*b4 + 18*b5 + 34*b6 + 20*b7 + 17*b8 + 15*b9 + 41*b10 + 16*b11; - pol c9 = 16*b0 + 2*b1 + 28*b2 + 13*b3 + 13*b4 + 39*b5 + 18*b6 + 34*b7 + 20*b8 + 17*b9 + 15*b10 + 41*b11; - pol c10 = 41*b0 + 16*b1 + 2*b2 + 28*b3 + 13*b4 + 13*b5 + 39*b6 + 18*b7 + 34*b8 + 20*b9 + 17*b10 + 15*b11; - pol c11 = 15*b0 + 41*b1 + 16*b2 + 2*b3 + 28*b4 + 13*b5 + 13*b6 + 39*b7 + 18*b8 + 34*b9 + 20*b10 + 17*b11; - - (in0' - c0) * (1-LAST) = 0; - (in1' - c1) * (1-LAST) = 0; - (in2' - c2) * (1-LAST) = 0; - (in3' - c3) * (1-LAST) = 0; - (in4' - c4) * (1-LAST) = 0; - (in5' - c5) * (1-LAST) = 0; - (in6' - c6) * (1-LAST) = 0; - (in7' - c7) * (1-LAST) = 0; - (cap0' - c8) * (1-LAST) = 0; - (cap1' - c9) * (1-LAST) = 0; - (cap2' - c10) * (1-LAST) = 0; - (cap3' - c11) * (1-LAST) = 0; - - FIRSTBLOCK * (input_in0 - in0) = 0; - FIRSTBLOCK * (input_in1 - in1) = 0; - FIRSTBLOCK * (input_in2 - in2) = 0; - FIRSTBLOCK * (input_in3 - in3) = 0; - FIRSTBLOCK * (input_in4 - in4) = 0; - FIRSTBLOCK * (input_in5 - in5) = 0; - FIRSTBLOCK * (input_in6 - in6) = 0; - FIRSTBLOCK * (input_in7 - in7) = 0; - FIRSTBLOCK * (input_cap0 - cap0) = 0; - FIRSTBLOCK * (input_cap1 - cap1) = 0; - FIRSTBLOCK * (input_cap2 - cap2) = 0; - FIRSTBLOCK * (input_cap3 - cap3) = 0; - - (1 - LAST) * (input_in0 - input_in0') = 0; - (1 - LAST) * (input_in1 - input_in1') = 0; - (1 - LAST) * (input_in2 - input_in2') = 0; - (1 - LAST) * (input_in3 - input_in3') = 0; - (1 - LAST) * (input_in4 - input_in4') = 0; - (1 - LAST) * (input_in5 - input_in5') = 0; - (1 - LAST) * (input_in6 - input_in6') = 0; - (1 - LAST) * (input_in7 - input_in7') = 0; - (1 - LAST) * (input_cap0 - input_cap0') = 0; - (1 - LAST) * (input_cap1 - input_cap1') = 0; - (1 - LAST) * (input_cap2 - input_cap2') = 0; - (1 - LAST) * (input_cap3 - input_cap3') = 0; - } + col witness operation_id; + + // Ported from: + // - https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/pil/poseidong.pil + // - https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/src/sm/sm_poseidong.js + + // Difference between our and Polygon's implementation: + // - Polygon puts the latch on the first row, rather than the last. + // Instead of reserving extra columns to repeat the inputs throughout the entire block, + // they reserve extra columns to repeat the output. This saves some columns, because the + // function has more inputs than outputs. Should be fixed once #627 is fixed. + + // Number of full rounds + constant %nRoundsF = 8; + // Number of partial rounds (half of them before and half of them after the full rounds) + constant %nRoundsP = 22; + constant %rowsPerHash = %nRoundsF + %nRoundsP + 1; + + pol constant L0 = [1] + [0]*; + pol constant FIRSTBLOCK(i) { match i % %rowsPerHash { + 0 => 1, + _ => 0 + }}; + pol constant LASTBLOCK(i) { match i % %rowsPerHash { + %rowsPerHash - 1 => 1, + _ => 0 + }}; + // Like LASTBLOCK, but also 1 in the last row of the table + // Specified this way because we can't access the degree in the match statement + pol constant LAST = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]* + [1]; + + // Whether the current round is a partial round + pol constant PARTIAL = [0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0]*; + + // The round constants + pol constant C_0 = [0xb585f766f2144405, 0x86287821f722c881, 0xe9fa634a21de0082, 0x92a756e67e2b9413, 0x3cc3f892184df408, 0x7131aa45268d7d8c, 0x99ad1aab0814283b, 0xeb84f608da56ef48, 0x7159cd30c3ac118e, 0xdcef0797c2b69ec7, 0xd0762cbc8ca6570c, 0x30a4680593258387, 0x15a16a8a8322d458, 0x5a3f1bb1c53a9645, 0x775005982d74d7f7, 0xf9cc95c22b4c1fcc, 0xc49366bb25e8513, 0xdd611f1000c17442, 0x2ff876fa5ef97c4, 0x3d06c8bd1514e2d9, 0xe89cd854d5d01d33, 0xece5a71e0cfedc75, 0x90004c1371b893c5, 0xde122bebe9a39368, 0x4d61e56a525d225a, 0x1478d361dbbf9fac, 0x475cd3205a3bdcde, 0xe70201e960cb78b8, 0x7be5b9ffda905e1c, 0xf3c12fe54d5c653b, 0x0]*; + pol constant C_1 = [0x7746a55f43921ad7, 0x59cd1a8a41c18e55, 0xf56f6d48959a600d, 0x70e741ebfee96586, 0x2e479dc157bf31bb, 0x9351036095630f9f, 0x438a7c91d416ca4d, 0xda608834c40e603d, 0x839b4e8fafead540, 0x3d639263da827b13, 0x34c6efb812b04bf5, 0x337dc00c61bd9ce1, 0x388a128b7fd9a609, 0xdb7f023869fb8d38, 0x86ab99b4dde6c8b0, 0x8d37f755f4ae9f6, 0x784d3d2f1698309, 0xd8185f9adfea4fd0, 0xc5cb72a2a51159b0, 0x9c9c98207cb10767, 0x5cd377dc8bb882a2, 0x5ff98fd5d51fe610, 0xb932b7cf752e5545, 0x4d001fd58f002526, 0x262e963c8da05d3d, 0x6f02dc07d141875c, 0x18a42105c31b7e88, 0x6f90ff3b6a65f108, 0xa3c95eaec244aa30, 0x40b9e922ed9771e2, 0x0]*; + pol constant C_2 = [0xb2fb0d31cee799b4, 0xc3b919ad495dc574, 0xf7d713e806391165, 0x19d5ee2af82ec1c, 0x6f49de07a6234346, 0xad535b24afc26bfb, 0xb60de3bcc5ea751c, 0x8f97fe408061f183, 0xd3f3e5e82920adc, 0xe273fd971bc8d0e7, 0x40bf0ab5fa14c112, 0xd5eca244c7a4ff1d, 0x2300e5d6baedf0fb, 0xb462065911d4e1fc, 0xb1204f603f51c080, 0xeec49b613478675b, 0x530fb67ea1809a81, 0xef87139ca9a3ab1e, 0x8470f39d2d5c900e, 0x65700b51aedfb5ef, 0xa7b0fb7883eee860, 0x83e8941918964615, 0xa0b1df81b6fe59fc, 0xca6637000eb4a9f8, 0x59e89b094d220ec2, 0x296a202ed8e556a2, 0x23e7414af663068, 0x42747a7245e7fa84, 0x230bca8f4df0544, 0x551f5b0fbe7b1840, 0x0]*; + pol constant C_3 = [0xf6760a4803427d7, 0xa484c4c5ef6a0781, 0x8297132b32825daf, 0x6f6f2ed772466352, 0x213ce7bede378d7b, 0x4627f5c6993e44be, 0xc99cab6aef6f58bc, 0xa93f485c96f37b89, 0x8f7d83bddee7bba8, 0x418f02702d227ed5, 0xb6b570fc7c5740d3, 0x7762638264d279bd, 0x2f63aa8647e15104, 0x49c24ae4437d8030, 0xef61ac8470250ecf, 0xf143933aed25e0b0, 0x410492299bb01f49, 0x3ba71336c34ee133, 0x25abb3f1d39fcb76, 0x911f451539869408, 0x7684403ec392950d, 0x5922040b47f150c1, 0x8ef1dd26770af2c2, 0x2f2339d624f91f78, 0x55d5b52b78b9c5e, 0x2afd67999bf32ee5, 0x15147108121967d7, 0xd1f507e43ab749b2, 0x4135c2bebfe148c6, 0x25032aa7c4cb1811, 0x0]*; + pol constant C_4 = [0xe10d666650f4e012, 0x308bbd23dc5416cc, 0xad6805e0e30b2c8a, 0x7cf416cfe7e14ca1, 0x5b0431345d4dea83, 0x645cf794b8f1cc58, 0x69a5ed92a72ee4ff, 0x6704e8ee8f18d563, 0x780f2243ea071d06, 0x8c25fda3b503038c, 0x5a27b9002de33454, 0xc1e434bedeefd767, 0xf1c36ce86ecec269, 0xd793862c112b0566, 0x1bbcd90f132c603f, 0xe4c5dd8255dfc622, 0x139542347424b9ac, 0x7d3a455d56b70238, 0x23eb8cc9b372442f, 0x7ae6849fbc3a0ec6, 0x5fa3f06f4fed3b52, 0xf97d750e3dd94521, 0x541a4f9cfbeed35, 0x6d1a7918c80df518, 0x82b27eb33514ef99, 0x7acfd96efa95491d, 0xe4a3dff1d7d6fef9, 0x1c86d265f15750cd, 0x166fc0cc438a3c72, 0xaaed34074b164346, 0x0]*; + pol constant C_5 = [0x8cae14cb07d09bf1, 0x6e4a40c18f30c09c, 0xac51d9f5fcf8535e, 0x61df517b86a46439, 0xa2de45780344d6a1, 0x241c70ed0af61617, 0x5e7b329c1ed4ad71, 0xcee3e9ac1e072119, 0xeb915845f3de1634, 0x2cbaed4daec8c07c, 0xb1a5b165b6d2b2d2, 0x299351a53b8ec22, 0x27181125183970c9, 0xaadd1106730d8feb, 0xcd1dabd964db557, 0xe7ad7756f193198e, 0x9cb0bd5ea1a1115e, 0x660d32e130182684, 0xd687ba55c64f6364, 0x3bb340eba06afe7e, 0x8df57ac11bc04831, 0x5080d4c2b86f56d7, 0x9e61106178bfc530, 0xdf9a4939342308e9, 0xd30094ca96b7ce7b, 0x6798ba0c0abb2c6d, 0x1a8d1a588085737, 0x3996ce73dd832c1c, 0x3762b59a8ae83efa, 0x8ffd96bbf9c9c81d, 0x0]*; + pol constant C_6 = [0xd438539c95f63e9f, 0x9a2eedb70d8f8cfa, 0x502ad7dc18c2ad87, 0x85dc499b11d77b75, 0x7103aaf94a7bf308, 0xacb8e076647905f1, 0x5fc0ac0800144885, 0x510d0e65e2b470c1, 0xd19e120d26b6f386, 0x5f58e6afcdd6ddc2, 0x8722e0ace9d1be22, 0xb2d456e4ad251b80, 0xe584029370dca96d, 0xc43b6e0e97b0d568, 0x11a3ae5beb9d1ec9, 0x92c2318b87fff9cb, 0x2e3f615c38f49a1, 0x297a863f48cd1f43, 0xda8d9e90fd8ff158, 0xb46e9d8b682ea65e, 0x2db01efa1e1e1897, 0xa7de115b56c78d70, 0xb3767e80935d8af2, 0xebc2151ee6c8398c, 0xcf5cb381cd0a1535, 0x34c6f57b26c92122, 0x11b4c74eda62beef, 0x8e7fba02983224bd, 0xe8928a4c89114750, 0x70fc91eb5937085c, 0x0]*; + pol constant C_7 = [0xef781c7ce35b4c3d, 0xe360c6e0ae486f38, 0x57a1550c110b3041, 0x4b959b48b9c10733, 0x5326fc0d97279301, 0x3737e9db4c4f474d, 0x32db829239774eca, 0xf6323f486b9038f0, 0x16ee53a7e5fecc6, 0x284650ac5e1b0eba, 0x788ee3b37e5680fb, 0x3e9ed1fda49cea0b, 0x4d9bbc3e02f1cfb2, 0xe29024c18ee6fca2, 0xf755bfeea585d11d, 0x739c25f8fd73596d, 0x985d4f4a9c5291ef, 0x90e0a736a751ebb7, 0xe3cbdc7d2fe45ea7, 0x8dcf22f9a3b34356, 0x54846de4aadb9ca2, 0x6a9242ac87538194, 0x98d5782065af06, 0x3cc2ba8a1116515, 0xfeed4db6919e5a7c, 0x5736e1bad206b5de, 0xe587cc0d69a73346, 0xba0dec7103255dd4, 0x2a440b51a4945ee5, 0x7f795e2a5f915440, 0x0]*; + pol constant C_8 = [0xcdc4a239b0c44426, 0xd5c7718fbfc647fb, 0x66bbd30e6ce0e583, 0xe8be3e5da8043e57, 0xa9ceb74fec024747, 0xe7ea5e33e75fffb6, 0xade699c5830f310, 0xb508cdeffa5ceef, 0xcb5fd54e7933e477, 0x635b337ee819dab5, 0x14a726661551e284, 0x2972a92ba450bed8, 0xea35bc29692af6f8, 0x5e50c27535b88c66, 0xa3b83250268ea4d7, 0x5636cac9f16dfed0, 0x775b9feafdcd26e7, 0x549f80ce550c4fd3, 0xb9a8c9b3aee52297, 0x77bdaeda586257a7, 0xba6745385893c784, 0xf7856ef7f9173e44, 0x31d191cd5c1466c7, 0xd341d037e840cf83, 0x41703f53753be59f, 0x20057d2a0056521b, 0x1ff7327017aa2a6e, 0x9e9cbd781628fc5b, 0x80cefd2b7d99ff83, 0x4543d9df5476d3cb, 0x0]*; + pol constant C_9 = [0x277fa208bf337bff, 0xc35eae071903ff0b, 0xda2abef589d644e, 0xf5c0bc1de6da8699, 0x27f8ec88bb21b1a3, 0x90dee49fc9bfc23a, 0x7cc5583b10415f21, 0xf2417089e4fb3cbd, 0xacb8417879fd449f, 0x9f9a036ed4f2d49f, 0x98b7672f9ef3b419, 0x20216dd77be493de, 0x18e21b4beabb4137, 0x10383f20a4ff9a87, 0x516306f4927c93af, 0xdd8f909a938e0172, 0x304265a6384f0f2d, 0xf73b2922f38bd64, 0xc0d28a5c10960bd3, 0xf19e400a5104d20d, 0x541d496344d2c75b, 0x2265fc92feb0dc09, 0x410fefafa319ac9d, 0x387cb5d25af4afcc, 0x5eeea940fcde8b6f, 0x3dea5bd5d0578bd7, 0x594e29c42473d06b, 0xdae8645996edd6a5, 0xbb9879c6e61fd62a, 0xf172d73e004fc90d, 0x0]*; + pol constant C_10 = [0xe17653a29da578a1, 0x849c2656969c4be7, 0xf061274fdb150d61, 0x40b12cbf09ef74bf, 0xfceb4fda1ded0893, 0xd1b1edf76bc09c92, 0x85df9ed2e166d64f, 0x60e75c2890d15730, 0x9c22190be7f74732, 0xb93e260cae5c170e, 0xbb93ae776bb30e3a, 0xadffe8cf28449ec6, 0x1e3b9fc625b554f4, 0x38e8ee9d71a45af8, 0xddb4ac49c9efa1da, 0xc6401fe115063f5b, 0x593664c39773012c, 0x16bf1f73fb7a9c3f, 0x45d7ac9b68f71a34, 0xc368a348e46d950f, 0xe909678474e687fe, 0x17dfc8e4f7ba8a57, 0xbdf8f242e316c4ab, 0xbba2515f22909e87, 0x4cd1f1b175100206, 0x16e50d897d4634ac, 0xf6f31db1899b12d5, 0xdebe0853b1a1d378, 0x6e7c8f1a84265034, 0xdfd1c4febcc81238, 0x0]*; + pol constant C_11 = [0xc54302f225db2c76, 0xc0572c8c08cbbbad, 0x28b8ec3ae9c29633, 0xa637093ecb2ad631, 0xfac6ff1346a41675, 0xb65481ba645c602, 0x6604df4fee32bcb1, 0xa6217d8bf660f29c, 0x5d693c1ba3ba3621, 0xb0a7eae879ddb76d, 0x28fd3b046380f850, 0x1c4dbb1c4c27d243, 0x25d64362697828fd, 0xdd5118375bf1a9b9, 0x64bb6dec369d4418, 0x8ad97b33f1ac1455, 0x4f0a2e5fb028f2ce, 0x6d1f5a59005bec17, 0xeeb76e397069e804, 0x9ef1cd60e679f284, 0xdfe89923f6c9c2ff, 0x9001a64209f21db8, 0x9e8cd55b57637ed0, 0x7248fe7705f38e47, 0x4a20358574454ec0, 0x29bff3ecb9b7a6e3, 0xc02ac5e47312d3ca, 0xa49229d24d014343, 0x164bb2de1bbeddc8, 0xbc8dfb627fe558fc, 0x0]*; + + // State of the Poseidon permutation + pol commit in0, in1, in2, in3, in4, in5, in6, in7, cap0, cap1, cap2, cap3; + + // The initial state of the Poseidon permutation + // (constrained to be equal to (in0, in1, in2, in3, in4, in5, in6, in7, cap0, cap1, cap2, cap3) + // in the first row and then repeated until the end of the block) + pol commit input_in0, input_in1, input_in2, input_in3, input_in4, input_in5, input_in6, input_in7, input_cap0, input_cap1, input_cap2, input_cap3; + + // Add round constants + pol a0 = in0 + C_0; + pol a1 = in1 + C_1; + pol a2 = in2 + C_2; + pol a3 = in3 + C_3; + pol a4 = in4 + C_4; + pol a5 = in5 + C_5; + pol a6 = in6 + C_6; + pol a7 = in7 + C_7; + pol a8 = cap0 + C_8; + pol a9 = cap1 + C_9; + pol a10 = cap2 + C_10; + pol a11 = cap3 + C_11; + + // Compute S-Boxes (x^7) + pol x2_0 = a0 * a0; + pol x4_0 = x2_0 * x2_0; + pol x6_0 = x2_0 * x4_0; + pol x7_0 = x6_0 * a0; + + pol x2_1 = a1 * a1; + pol x4_1 = x2_1 * x2_1; + pol x6_1 = x2_1 * x4_1; + pol x7_1 = x6_1 * a1; + + pol x2_2 = a2 * a2; + pol x4_2 = x2_2 * x2_2; + pol x6_2 = x2_2 * x4_2; + pol x7_2 = x6_2 * a2; + + pol x2_3 = a3 * a3; + pol x4_3 = x2_3 * x2_3; + pol x6_3 = x2_3 * x4_3; + pol x7_3 = x6_3 * a3; + + pol x2_4 = a4 * a4; + pol x4_4 = x2_4 * x2_4; + pol x6_4 = x2_4 * x4_4; + pol x7_4 = x6_4 * a4; + + pol x2_5 = a5 * a5; + pol x4_5 = x2_5 * x2_5; + pol x6_5 = x2_5 * x4_5; + pol x7_5 = x6_5 * a5; + + pol x2_6 = a6 * a6; + pol x4_6 = x2_6 * x2_6; + pol x6_6 = x2_6 * x4_6; + pol x7_6 = x6_6 * a6; + + pol x2_7 = a7 * a7; + pol x4_7 = x2_7 * x2_7; + pol x6_7 = x2_7 * x4_7; + pol x7_7 = x6_7 * a7; + + pol x2_8 = a8 * a8; + pol x4_8 = x2_8 * x2_8; + pol x6_8 = x2_8 * x4_8; + pol x7_8 = x6_8 * a8; + + pol x2_9 = a9 * a9; + pol x4_9 = x2_9 * x2_9; + pol x6_9 = x2_9 * x4_9; + pol x7_9 = x6_9 * a9; + + pol x2_10 = a10 * a10; + pol x4_10 = x2_10 * x2_10; + pol x6_10 = x2_10 * x4_10; + pol x7_10 = x6_10 * a10; + + pol x2_11 = a11 * a11; + pol x4_11 = x2_11 * x2_11; + pol x6_11 = x2_11 * x4_11; + pol x7_11 = x6_11 * a11; + + // Apply S-Boxes on the first element and otherwise if it is a full round. + pol b0 = x7_0; + pol b1 = PARTIAL * (a1 - x7_1) + x7_1; + pol b2 = PARTIAL * (a2 - x7_2) + x7_2; + pol b3 = PARTIAL * (a3 - x7_3) + x7_3; + pol b4 = PARTIAL * (a4 - x7_4) + x7_4; + pol b5 = PARTIAL * (a5 - x7_5) + x7_5; + pol b6 = PARTIAL * (a6 - x7_6) + x7_6; + pol b7 = PARTIAL * (a7 - x7_7) + x7_7; + pol b8 = PARTIAL * (a8 - x7_8) + x7_8; + pol b9 = PARTIAL * (a9 - x7_9) + x7_9; + pol b10 = PARTIAL * (a10 - x7_10) + x7_10; + pol b11 = PARTIAL * (a11 - x7_11) + x7_11; + + // Multiply with MDS Matrix + pol c0 = 25*b0 + 15*b1 + 41*b2 + 16*b3 + 2*b4 + 28*b5 + 13*b6 + 13*b7 + 39*b8 + 18*b9 + 34*b10 + 20*b11; + pol c1 = 20*b0 + 17*b1 + 15*b2 + 41*b3 + 16*b4 + 2*b5 + 28*b6 + 13*b7 + 13*b8 + 39*b9 + 18*b10 + 34*b11 ; + pol c2 = 34*b0 + 20*b1 + 17*b2 + 15*b3 + 41*b4 + 16*b5 + 2*b6 + 28*b7 + 13*b8 + 13*b9 + 39*b10 + 18*b11; + pol c3 = 18*b0 + 34*b1 + 20*b2 + 17*b3 + 15*b4 + 41*b5 + 16*b6 + 2*b7 + 28*b8 + 13*b9 + 13*b10 + 39*b11; + pol c4 = 39*b0 + 18*b1 + 34*b2 + 20*b3 + 17*b4 + 15*b5 + 41*b6 + 16*b7 + 2*b8 + 28*b9 + 13*b10 + 13*b11; + pol c5 = 13*b0 + 39*b1 + 18*b2 + 34*b3 + 20*b4 + 17*b5 + 15*b6 + 41*b7 + 16*b8 + 2*b9 + 28*b10 + 13*b11; + pol c6 = 13*b0 + 13*b1 + 39*b2 + 18*b3 + 34*b4 + 20*b5 + 17*b6 + 15*b7 + 41*b8 + 16*b9 + 2*b10 + 28*b11; + pol c7 = 28*b0 + 13*b1 + 13*b2 + 39*b3 + 18*b4 + 34*b5 + 20*b6 + 17*b7 + 15*b8 + 41*b9 + 16*b10 + 2*b11; + pol c8 = 2*b0 + 28*b1 + 13*b2 + 13*b3 + 39*b4 + 18*b5 + 34*b6 + 20*b7 + 17*b8 + 15*b9 + 41*b10 + 16*b11; + pol c9 = 16*b0 + 2*b1 + 28*b2 + 13*b3 + 13*b4 + 39*b5 + 18*b6 + 34*b7 + 20*b8 + 17*b9 + 15*b10 + 41*b11; + pol c10 = 41*b0 + 16*b1 + 2*b2 + 28*b3 + 13*b4 + 13*b5 + 39*b6 + 18*b7 + 34*b8 + 20*b9 + 17*b10 + 15*b11; + pol c11 = 15*b0 + 41*b1 + 16*b2 + 2*b3 + 28*b4 + 13*b5 + 13*b6 + 39*b7 + 18*b8 + 34*b9 + 20*b10 + 17*b11; + + (in0' - c0) * (1-LAST) = 0; + (in1' - c1) * (1-LAST) = 0; + (in2' - c2) * (1-LAST) = 0; + (in3' - c3) * (1-LAST) = 0; + (in4' - c4) * (1-LAST) = 0; + (in5' - c5) * (1-LAST) = 0; + (in6' - c6) * (1-LAST) = 0; + (in7' - c7) * (1-LAST) = 0; + (cap0' - c8) * (1-LAST) = 0; + (cap1' - c9) * (1-LAST) = 0; + (cap2' - c10) * (1-LAST) = 0; + (cap3' - c11) * (1-LAST) = 0; + + FIRSTBLOCK * (input_in0 - in0) = 0; + FIRSTBLOCK * (input_in1 - in1) = 0; + FIRSTBLOCK * (input_in2 - in2) = 0; + FIRSTBLOCK * (input_in3 - in3) = 0; + FIRSTBLOCK * (input_in4 - in4) = 0; + FIRSTBLOCK * (input_in5 - in5) = 0; + FIRSTBLOCK * (input_in6 - in6) = 0; + FIRSTBLOCK * (input_in7 - in7) = 0; + FIRSTBLOCK * (input_cap0 - cap0) = 0; + FIRSTBLOCK * (input_cap1 - cap1) = 0; + FIRSTBLOCK * (input_cap2 - cap2) = 0; + FIRSTBLOCK * (input_cap3 - cap3) = 0; + + (1 - LAST) * (input_in0 - input_in0') = 0; + (1 - LAST) * (input_in1 - input_in1') = 0; + (1 - LAST) * (input_in2 - input_in2') = 0; + (1 - LAST) * (input_in3 - input_in3') = 0; + (1 - LAST) * (input_in4 - input_in4') = 0; + (1 - LAST) * (input_in5 - input_in5') = 0; + (1 - LAST) * (input_in6 - input_in6') = 0; + (1 - LAST) * (input_in7 - input_in7') = 0; + (1 - LAST) * (input_cap0 - input_cap0') = 0; + (1 - LAST) * (input_cap1 - input_cap1') = 0; + (1 - LAST) * (input_cap2 - input_cap2') = 0; + (1 - LAST) * (input_cap3 - input_cap3') = 0; } \ No newline at end of file diff --git a/std/shift.asm b/std/shift.asm index d4069e468f..a1e740c7de 100644 --- a/std/shift.asm +++ b/std/shift.asm @@ -5,36 +5,34 @@ machine Shift(latch, operation_id) { operation shr<1> A, B -> C; - constraints{ - col witness operation_id; - - col fixed latch(i) { is_zero((i % 4) - 3) }; - col fixed FACTOR_ROW(i) { (i + 1) % 4 }; - col fixed FACTOR(i) { 1 << (((i + 1) % 4) * 8) }; - - col fixed P_A(i) { i % 256 }; - col fixed P_B(i) { (i / 256) % 32 }; - col fixed P_ROW(i) { (i / (256 * 32)) % 4 }; - col fixed P_operation(i) { (i / (256 * 32 * 4)) % 2 }; - col fixed P_C(i) { - match P_operation(i) { - 0 => (P_A(i) << (P_B(i) + (P_ROW(i) * 8))), - 1 => (P_A(i) << (P_ROW(i) * 8)) >> P_B(i), - } & 0xffffffff - }; - - col witness A_byte; - col witness C_part; - - col witness A; - col witness B; - col witness C; - - A' = A * (1 - latch) + A_byte * FACTOR; - (B' - B) * (1 - latch) = 0; - C' = C * (1 - latch) + C_part; - - // TODO this way, we cannot prove anything that shifts by more than 31 bits. - {operation_id', A_byte, B', FACTOR_ROW, C_part} in {P_operation, P_A, P_B, P_ROW, P_C}; - } + col witness operation_id; + + col fixed latch(i) { is_zero((i % 4) - 3) }; + col fixed FACTOR_ROW(i) { (i + 1) % 4 }; + col fixed FACTOR(i) { 1 << (((i + 1) % 4) * 8) }; + + col fixed P_A(i) { i % 256 }; + col fixed P_B(i) { (i / 256) % 32 }; + col fixed P_ROW(i) { (i / (256 * 32)) % 4 }; + col fixed P_operation(i) { (i / (256 * 32 * 4)) % 2 }; + col fixed P_C(i) { + match P_operation(i) { + 0 => (P_A(i) << (P_B(i) + (P_ROW(i) * 8))), + 1 => (P_A(i) << (P_ROW(i) * 8)) >> P_B(i), + } & 0xffffffff + }; + + col witness A_byte; + col witness C_part; + + col witness A; + col witness B; + col witness C; + + A' = A * (1 - latch) + A_byte * FACTOR; + (B' - B) * (1 - latch) = 0; + C' = C * (1 - latch) + C_part; + + // TODO this way, we cannot prove anything that shifts by more than 31 bits. + {operation_id', A_byte, B', FACTOR_ROW, C_part} in {P_operation, P_A, P_B, P_ROW, P_C}; } \ No newline at end of file diff --git a/std/wrap/wrap_gl.asm b/std/wrap/wrap_gl.asm index b758f8bac8..d02342d5b6 100644 --- a/std/wrap/wrap_gl.asm +++ b/std/wrap/wrap_gl.asm @@ -3,78 +3,74 @@ machine WrapGL(RESET, operation_id) { operation wrap<0> in_acc -> output; - constraints { + // Latch and operation ID + col fixed RESET(i) { i % 8 == 7 }; + col witness operation_id; - // Latch and operation ID - col fixed RESET(i) { i % 8 == 7 }; - col witness operation_id; + // 1. Decompose the input into bytes - // 1. Decompose the input into bytes + // The byte decomposition of the input, in little-endian order + // and shifted forward by one (to use the last row of the + // previous block) + col witness bytes; + // Puts the bytes together to form the input + col witness in_acc; + // Factors to multiply the bytes by + col fixed FACTOR(i) { 1 << (((i + 1) % 8) * 8) }; - // The byte decomposition of the input, in little-endian order - // and shifted forward by one (to use the last row of the - // previous block) - col witness bytes; - // Puts the bytes together to form the input - col witness in_acc; - // Factors to multiply the bytes by - col fixed FACTOR(i) { 1 << (((i + 1) % 8) * 8) }; + in_acc' = (1 - RESET) * in_acc + bytes * FACTOR; - in_acc' = (1 - RESET) * in_acc + bytes * FACTOR; + // 2. Build the output, packing the least significant 4 byte into + // a field element + col witness output; + col fixed FACTOR_OUTPUT = [0x100, 0x10000, 0x1000000, 0, 0, 0, 0, 1]*; + output' = (1 - RESET) * output + bytes * FACTOR_OUTPUT; - // 2. Build the output, packing the least significant 4 byte into - // a field element - col witness output; - col fixed FACTOR_OUTPUT = [0x100, 0x10000, 0x1000000, 0, 0, 0, 0, 1]*; - output' = (1 - RESET) * output + bytes * FACTOR_OUTPUT; + // 3. Check that the byte decomposition does not overflow + // + // Skipping this step would work but it wouldn't be sound, because + // the 8-byte decomposition could overflow, since the Goldilocks + // prime 2**64 - 2**32 + 1 is smaller than 2^64. + // + // The approach is to compare the byte decomposition with that of + // the maximum possible value (0xffffffff00000000) byte by byte, + // from most significant to least significant (i.e., going backwards). + // A byte can only be larger than that of the max value if any previous + // byte has been smaller. - // 3. Check that the byte decomposition does not overflow - // - // Skipping this step would work but it wouldn't be sound, because - // the 8-byte decomposition could overflow, since the Goldilocks - // prime 2**64 - 2**32 + 1 is smaller than 2^64. - // - // The approach is to compare the byte decomposition with that of - // the maximum possible value (0xffffffff00000000) byte by byte, - // from most significant to least significant (i.e., going backwards). - // A byte can only be larger than that of the max value if any previous - // byte has been smaller. + // This is an example for input 0xfffffffeffffffff: + // Row RESET bytes BYTES_MAX lt was_lt gt + // -1 0x1 0xff 0x0 0x0 0x1 0x1 + // 0 0x0 0xff 0x0 0x0 0x1 0x1 + // 1 0x0 0xff 0x0 0x0 0x1 0x1 + // 2 0x0 0xff 0x0 0x0 0x1 0x1 + // 3 0x0 0xfe 0xff 0x1 0x1 0x0 # 0xfe < 0xff, so now greater bytes are allowed + // 4 0x0 0xff 0xff 0x0 0x0 0x0 + // 5 0x0 0xff 0xff 0x0 0x0 0x0 + // 6 0x0 0xff 0xff 0x0 0x0 0x0 + // 7 0x1 ---- ---- --- --- --- - // This is an example for input 0xfffffffeffffffff: - // Row RESET bytes BYTES_MAX lt was_lt gt - // -1 0x1 0xff 0x0 0x0 0x1 0x1 - // 0 0x0 0xff 0x0 0x0 0x1 0x1 - // 1 0x0 0xff 0x0 0x0 0x1 0x1 - // 2 0x0 0xff 0x0 0x0 0x1 0x1 - // 3 0x0 0xfe 0xff 0x1 0x1 0x0 # 0xfe < 0xff, so now greater bytes are allowed - // 4 0x0 0xff 0xff 0x0 0x0 0x0 - // 5 0x0 0xff 0xff 0x0 0x0 0x0 - // 6 0x0 0xff 0xff 0x0 0x0 0x0 - // 7 0x1 ---- ---- --- --- --- + // Bytes of the maximum value, in little endian order, rotated by one + col fixed BYTES_MAX = [0, 0, 0, 0xff, 0xff, 0xff, 0xff, 0]*; - // Bytes of the maximum value, in little endian order, rotated by one - col fixed BYTES_MAX = [0, 0, 0, 0xff, 0xff, 0xff, 0xff, 0]*; + // Byte comparison block machine + col fixed P_A(i) { i % 256 }; + col fixed P_B(i) { (i >> 8) % 256 }; + col fixed P_LT(i) { (P_A(i) < P_B(i)) }; + col fixed P_GT(i) { (P_A(i) > P_B(i)) }; - // Byte comparison block machine - col fixed P_A(i) { i % 256 }; - col fixed P_B(i) { (i >> 8) % 256 }; - col fixed P_LT(i) { (P_A(i) < P_B(i)) }; - col fixed P_GT(i) { (P_A(i) > P_B(i)) }; + // Compare the current byte with the corresponding byte of the maximum value. + col witness lt; + col witness gt; + { bytes, BYTES_MAX, lt, gt } in { P_A, P_B, P_LT, P_GT }; - // Compare the current byte with the corresponding byte of the maximum value. - col witness lt; - col witness gt; - { bytes, BYTES_MAX, lt, gt } in { P_A, P_B, P_LT, P_GT }; + // Compute whether the current or any previous byte has been less than + // the corresponding byte of the maximum value. + // This moves *backward* from the second to last row. + col witness was_lt; + was_lt = RESET' * lt + (1 - RESET') * (was_lt' + lt - was_lt' * lt); - // Compute whether the current or any previous byte has been less than - // the corresponding byte of the maximum value. - // This moves *backward* from the second to last row. - col witness was_lt; - was_lt = RESET' * lt + (1 - RESET') * (was_lt' + lt - was_lt' * lt); - - // If any byte is larger, but no previous byte was smaller, the byte - // decomposition has overflowed and should be rejected. - gt * (1 - was_lt) = 0; - - } + // If any byte is larger, but no previous byte was smaller, the byte + // decomposition has overflowed and should be rejected. + gt * (1 - was_lt) = 0; } diff --git a/test_data/asm/bit_access.asm b/test_data/asm/bit_access.asm index 4518c56ebe..1a04c3a289 100644 --- a/test_data/asm/bit_access.asm +++ b/test_data/asm/bit_access.asm @@ -5,30 +5,27 @@ machine BitAccess { reg A; reg B; - constraints { - col witness XInv; - col witness XIsZero; - XIsZero = 1 - X * XInv; - XIsZero * X = 0; - XIsZero * (1 - XIsZero) = 0; - } + col witness XInv; + col witness XIsZero; + XIsZero = 1 - X * XInv; + XIsZero * X = 0; + XIsZero * (1 - XIsZero) = 0; // Wraps a value in Y to 32 bits. // Requires 0 <= Y < 2**33 instr wrap Y -> X { Y = X + wrap_bit * 2**32, X = XB1 + 0x100 * XB2 + 0x10000 * XB3 + 0x1000000 * XB4 } - constraints { - col fixed BYTE(i) { i & 0xff }; - col witness XB1; - col witness XB2; - col witness XB3; - col witness XB4; - { XB1 } in { BYTE }; - { XB2 } in { BYTE }; - { XB3 } in { BYTE }; - { XB4 } in { BYTE }; - col commit wrap_bit; - wrap_bit * (1 - wrap_bit) = 0; - } + + col fixed BYTE(i) { i & 0xff }; + col witness XB1; + col witness XB2; + col witness XB3; + col witness XB4; + { XB1 } in { BYTE }; + { XB2 } in { BYTE }; + { XB3 } in { BYTE }; + { XB4 } in { BYTE }; + col commit wrap_bit; + wrap_bit * (1 - wrap_bit) = 0; instr assert_zero X { XIsZero = 1 } diff --git a/test_data/asm/block_machine_cache_miss.asm b/test_data/asm/block_machine_cache_miss.asm index 818d17103e..22e467e381 100644 --- a/test_data/asm/block_machine_cache_miss.asm +++ b/test_data/asm/block_machine_cache_miss.asm @@ -6,27 +6,25 @@ machine Arith(latch, operation_id) { operation double<0> x -> y; operation square<1> x -> y; - constraints { - col witness operation_id; - col fixed latch = [1]*; - col fixed X(i) {i}; - col fixed DOUBLE(i) {2*i}; - col fixed SQUARE(i) {i*i}; - col witness x; - col witness y; - - // Depending on the operation ID, one of these identities - // has to be processed, the other can be ignored. - // Because powdr doesn't include the operation ID into the cache key - // for the sequence cache, this will lead to a cache miss: - // - For the very first execution, the sequence for the operation ID - // will be computed and stored in the cache. - // - If the operation ID is different in the next execution, the - // cached sequence won't include the correct lookup. - // Powdr should be able to recover from this. - (1 - operation_id) {x, y} in {X, DOUBLE}; - operation_id {x, y} in {X, SQUARE}; - } + col witness operation_id; + col fixed latch = [1]*; + col fixed X(i) {i}; + col fixed DOUBLE(i) {2*i}; + col fixed SQUARE(i) {i*i}; + col witness x; + col witness y; + + // Depending on the operation ID, one of these identities + // has to be processed, the other can be ignored. + // Because powdr doesn't include the operation ID into the cache key + // for the sequence cache, this will lead to a cache miss: + // - For the very first execution, the sequence for the operation ID + // will be computed and stored in the cache. + // - If the operation ID is different in the next execution, the + // cached sequence won't include the correct lookup. + // Powdr should be able to recover from this. + (1 - operation_id) {x, y} in {X, DOUBLE}; + operation_id {x, y} in {X, SQUARE}; } machine Main { diff --git a/test_data/asm/block_to_block.asm b/test_data/asm/block_to_block.asm index 659a712ec6..1b617d9f04 100644 --- a/test_data/asm/block_to_block.asm +++ b/test_data/asm/block_to_block.asm @@ -5,14 +5,12 @@ machine Arith(latch, operation_id) { operation add<0> x, y -> z; - constraints { - col fixed operation_id = [0]*; - col fixed latch = [1]*; - col witness x; - col witness y; - col witness z; - z = x + y; - } + col fixed operation_id = [0]*; + col fixed latch = [1]*; + col witness x; + col witness y; + col witness z; + z = x + y; } machine Main(latch, operation_id) { @@ -26,22 +24,20 @@ machine Main(latch, operation_id) { link instr_add x, y -> z = arith.add; - constraints { - col fixed operation_id = [0]*; - col fixed x(i) { i / 4 }; - col fixed y(i) { i / 4 + 1 }; - col witness z; - col witness res; - col fixed latch = [0, 0, 0, 1]*; // return every 4th row - - // accumulate the intermediate results into `res` - // we waste a row here as we initialize res at 0 - // this is due to a limitation in witgen - res' = (1 - latch) * (res + z); - - // add locally when `instr_add` is off - (1 - instr_add) * (x + y - z) = 0; - // add using `arith` every other row - col fixed instr_add = [0, 1]*; - } + col fixed operation_id = [0]*; + col fixed x(i) { i / 4 }; + col fixed y(i) { i / 4 + 1 }; + col witness z; + col witness res; + col fixed latch = [0, 0, 0, 1]*; // return every 4th row + + // accumulate the intermediate results into `res` + // we waste a row here as we initialize res at 0 + // this is due to a limitation in witgen + res' = (1 - latch) * (res + z); + + // add locally when `instr_add` is off + (1 - instr_add) * (x + y - z) = 0; + // add using `arith` every other row + col fixed instr_add = [0, 1]*; } \ No newline at end of file diff --git a/test_data/asm/book/function.asm b/test_data/asm/book/function.asm index 66731b678c..7e6a1dee00 100644 --- a/test_data/asm/book/function.asm +++ b/test_data/asm/book/function.asm @@ -68,13 +68,11 @@ machine Machine { } // some superpowers on `X` to allow us to check if it's 0 - constraints { - col witness XInv; - col witness XIsZero; - XIsZero = 1 - X * XInv; - XIsZero * X = 0; - XIsZero * (1 - XIsZero) = 0; - } + col witness XInv; + col witness XIsZero; + XIsZero = 1 - X * XInv; + XIsZero * X = 0; + XIsZero * (1 - XIsZero) = 0; } /* ANCHOR_END: all */ \ No newline at end of file diff --git a/test_data/asm/book/hello_world.asm b/test_data/asm/book/hello_world.asm index b2f19227e5..7c0d8cddb3 100644 --- a/test_data/asm/book/hello_world.asm +++ b/test_data/asm/book/hello_world.asm @@ -21,10 +21,6 @@ machine HelloWorld { X = 0 } - constraints { - // in this machine, we do not add more constraints - } - // the main function assigns the first prover input to A, increments it, decrements it, and loops forever function main { A <=X= ${ ("input", 0) }; diff --git a/test_data/asm/book/modules.asm b/test_data/asm/book/modules.asm index a1d61a2c03..8bb234320e 100644 --- a/test_data/asm/book/modules.asm +++ b/test_data/asm/book/modules.asm @@ -40,9 +40,7 @@ mod my_module { machine Other(latch, operation_id) { operation nothing<0>; - constraints { - col fixed latch = [1]*; - col fixed operation_id = [0]*; - } + col fixed latch = [1]*; + col fixed operation_id = [0]*; } } \ No newline at end of file diff --git a/test_data/asm/book/operations_and_links.asm b/test_data/asm/book/operations_and_links.asm index 3daf3cea97..823a77b8db 100644 --- a/test_data/asm/book/operations_and_links.asm +++ b/test_data/asm/book/operations_and_links.asm @@ -9,14 +9,12 @@ machine Main(latch, operation_id) { // TODO: uncomment the link once witness generation supports it // link 1 x, y -> z = adder.add; - constraints { - col fixed operation_id = [0]*; - col fixed latch = [1]*; - - col witness x; - col witness y; - col witness z; - } + col fixed operation_id = [0]*; + col fixed latch = [1]*; + + col witness x; + col witness y; + col witness z; } // ANCHOR_END: links @@ -25,15 +23,13 @@ machine Arith(latch, operation_id) { operation add<0> a, b -> c; operation sub<1> a, b -> c; - constraints { - col witness operation_id; - col fixed latch = [1]*; + col witness operation_id; + col fixed latch = [1]*; - col witness a; - col witness b; - col witness c; + col witness a; + col witness b; + col witness c; - c = (1 - operation_id) * (a + b) + operation_id * (a - b); - } + c = (1 - operation_id) * (a + b) + operation_id * (a - b); } // ANCHOR_END: operations \ No newline at end of file diff --git a/test_data/asm/book/simple_static.asm b/test_data/asm/book/simple_static.asm index 4759204be4..67114af62c 100644 --- a/test_data/asm/book/simple_static.asm +++ b/test_data/asm/book/simple_static.asm @@ -4,19 +4,17 @@ machine SimpleStatic(latch, operation_id) { operation power_4<0> x -> y; - constraints { - col fixed operation_id = [0]*; - col fixed latch = [0, 0, 0, 1]*; - col witness x; - col witness y; + col fixed operation_id = [0]*; + col fixed latch = [0, 0, 0, 1]*; + col witness x; + col witness y; - // initialise y to x at the beginning of each block - latch * (y' - x') = 0; - // x is unconstrained at the beginning of the block + // initialise y to x at the beginning of each block + latch * (y' - x') = 0; + // x is unconstrained at the beginning of the block - // x is constant within a block - (1 - latch) * (x' - x) = 0; - // y is multiplied by x at each row - (1 - latch) * (y' - x * y) = 0; - } + // x is constant within a block + (1 - latch) * (x' - x) = 0; + // y is multiplied by x at each row + (1 - latch) * (y' - x * y) = 0; } \ No newline at end of file diff --git a/test_data/asm/book/submodule.asm b/test_data/asm/book/submodule.asm index d7db50e338..cca6bf9a7f 100644 --- a/test_data/asm/book/submodule.asm +++ b/test_data/asm/book/submodule.asm @@ -1,11 +1,9 @@ machine Other(latch, operation_id) { operation nothing<0>; - constraints { - col fixed latch = [1]*; - col fixed operation_id = [0]*; + col fixed latch = [1]*; + col fixed operation_id = [0]*; - col witness w; - w * w = w; - } + col witness w; + w * w = w; } \ No newline at end of file diff --git a/test_data/asm/book/submodule_in_folder/mod.asm b/test_data/asm/book/submodule_in_folder/mod.asm index d7db50e338..cca6bf9a7f 100644 --- a/test_data/asm/book/submodule_in_folder/mod.asm +++ b/test_data/asm/book/submodule_in_folder/mod.asm @@ -1,11 +1,9 @@ machine Other(latch, operation_id) { operation nothing<0>; - constraints { - col fixed latch = [1]*; - col fixed operation_id = [0]*; + col fixed latch = [1]*; + col fixed operation_id = [0]*; - col witness w; - w * w = w; - } + col witness w; + w * w = w; } \ No newline at end of file diff --git a/test_data/asm/full_pil_constant.asm b/test_data/asm/full_pil_constant.asm index 8aeaf47bba..d8b8031e90 100644 --- a/test_data/asm/full_pil_constant.asm +++ b/test_data/asm/full_pil_constant.asm @@ -1,11 +1,9 @@ machine FullConstant(latch, operation_id) { degree 2; - constraints { - pol constant operation_id = [0]*; - pol constant latch = [1]*; - pol constant C = [0, 1]*; - col commit w; - w = C; - } + pol constant operation_id = [0]*; + pol constant latch = [1]*; + pol constant C = [0, 1]*; + col commit w; + w = C; } \ No newline at end of file diff --git a/test_data/asm/functional_instructions.asm b/test_data/asm/functional_instructions.asm index 90a30412dc..dd224e8772 100644 --- a/test_data/asm/functional_instructions.asm +++ b/test_data/asm/functional_instructions.asm @@ -6,31 +6,27 @@ machine FunctionalInstructions { reg B; reg CNT; - constraints { - col witness XInv; - col witness XIsZero; - XIsZero = 1 - X * XInv; - XIsZero * X = 0; - XIsZero * (1 - XIsZero) = 0; - } + col witness XInv; + col witness XIsZero; + XIsZero = 1 - X * XInv; + XIsZero * X = 0; + XIsZero * (1 - XIsZero) = 0; // Wraps a value in Y to 32 bits. // Requires 0 <= Y < 2**33 instr wrap Y -> X { Y = X + wrap_bit * 2**32, X = XB1 + 0x100 * XB2 + 0x10000 * XB3 + 0x1000000 * XB4 } - constraints { - col fixed BYTES(i) { i & 0xff }; - col commit XB1; - col commit XB2; - col commit XB3; - col commit XB4; - { XB1 } in { BYTES }; - { XB2 } in { BYTES }; - { XB3 } in { BYTES }; - { XB4 } in { BYTES }; - col commit wrap_bit; - wrap_bit * (1 - wrap_bit) = 0; - } + col fixed BYTES(i) { i & 0xff }; + col commit XB1; + col commit XB2; + col commit XB3; + col commit XB4; + { XB1 } in { BYTES }; + { XB2 } in { BYTES }; + { XB3 } in { BYTES }; + { XB4 } in { BYTES }; + col commit wrap_bit; + wrap_bit * (1 - wrap_bit) = 0; instr assert_zero X { XIsZero = 1 } diff --git a/test_data/asm/intermediate.asm b/test_data/asm/intermediate.asm index 979e3f0f6c..012dbfb8f4 100644 --- a/test_data/asm/intermediate.asm +++ b/test_data/asm/intermediate.asm @@ -1,9 +1,7 @@ machine Intermediate(latch, operation_id) { - constraints { - col fixed latch = [1]*; - col fixed operation_id = [0]*; - col witness x; - col intermediate = x; - intermediate = intermediate; - } + col fixed latch = [1]*; + col fixed operation_id = [0]*; + col witness x; + col intermediate = x; + intermediate = intermediate; } \ No newline at end of file diff --git a/test_data/asm/intermediate_nested.asm b/test_data/asm/intermediate_nested.asm index dd2746cb96..a511a53c4c 100644 --- a/test_data/asm/intermediate_nested.asm +++ b/test_data/asm/intermediate_nested.asm @@ -1,11 +1,9 @@ machine Intermediate(latch, operation_id) { - constraints { - col fixed latch = [1]*; - col fixed operation_id = [0]*; - col witness x; - col intermediate = x; - col int2 = intermediate * x; - col int3 = int2 + intermediate; - int3 = (3 * x) + x; - } + col fixed latch = [1]*; + col fixed operation_id = [0]*; + col witness x; + col intermediate = x; + col int2 = intermediate * x; + col int3 = int2 + intermediate; + int3 = (3 * x) + x; } \ No newline at end of file diff --git a/test_data/asm/macros_in_instructions.asm b/test_data/asm/macros_in_instructions.asm index 819f8e4d44..d48b57030d 100644 --- a/test_data/asm/macros_in_instructions.asm +++ b/test_data/asm/macros_in_instructions.asm @@ -4,17 +4,15 @@ machine MacroAsm { reg Y[<=]; reg A; - constraints { - macro branch_if(condition, target) { - pc' = condition * target + (1 - condition) * (pc + 1); - }; + macro branch_if(condition, target) { + pc' = condition * target + (1 - condition) * (pc + 1); + }; - col witness XInv; - col witness XIsZero; - XIsZero = 1 - X * XInv; - XIsZero * X = 0; - XIsZero * (1 - XIsZero) = 0; - } + col witness XInv; + col witness XIsZero; + XIsZero = 1 - X * XInv; + XIsZero * X = 0; + XIsZero * (1 - XIsZero) = 0; instr bz X, target: label { branch_if(XIsZero, target) } instr fail { X = X + 1 } diff --git a/test_data/asm/mem_read_write.asm b/test_data/asm/mem_read_write.asm index 524de391b9..036bb2711a 100644 --- a/test_data/asm/mem_read_write.asm +++ b/test_data/asm/mem_read_write.asm @@ -7,58 +7,56 @@ machine MemReadWrite { reg CNT; reg ADDR; - constraints { - col witness XInv; - col witness XIsZero; - XIsZero = 1 - X * XInv; - XIsZero * X = 0; - XIsZero * (1 - XIsZero) = 0; + col witness XInv; + col witness XIsZero; + XIsZero = 1 - X * XInv; + XIsZero * X = 0; + XIsZero * (1 - XIsZero) = 0; - // Read-write memory. Columns are sorted by m_addr and - // then by m_step. m_change is 1 if and only if m_addr changes - // in the next row. - col witness m_addr; - col witness m_step; - col witness m_change; - col witness m_value; - // If we have an operation at all (needed because this needs to be a permutation) - col witness m_op; - // If the operation is a write operation. - col witness m_is_write; - col witness m_is_read; + // Read-write memory. Columns are sorted by m_addr and + // then by m_step. m_change is 1 if and only if m_addr changes + // in the next row. + col witness m_addr; + col witness m_step; + col witness m_change; + col witness m_value; + // If we have an operation at all (needed because this needs to be a permutation) + col witness m_op; + // If the operation is a write operation. + col witness m_is_write; + col witness m_is_read; - // positive numbers (assumed to be much smaller than the field order) - col fixed POSITIVE(i) { i + 1 }; - col fixed FIRST = [1] + [0]*; - col fixed LAST = [0]* + [1]; - col fixed STEP(i) { i }; + // positive numbers (assumed to be much smaller than the field order) + col fixed POSITIVE(i) { i + 1 }; + col fixed FIRST = [1] + [0]*; + col fixed LAST = [0]* + [1]; + col fixed STEP(i) { i }; - m_change * (1 - m_change) = 0; + m_change * (1 - m_change) = 0; - // if m_change is zero, m_addr has to stay the same. - (m_addr' - m_addr) * (1 - m_change) = 0; + // if m_change is zero, m_addr has to stay the same. + (m_addr' - m_addr) * (1 - m_change) = 0; - // Except for the last row, if m_change is 1, then m_addr has to increase, - // if it is zero, m_step has to increase. - (1 - LAST) { m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step) } in POSITIVE; + // Except for the last row, if m_change is 1, then m_addr has to increase, + // if it is zero, m_step has to increase. + (1 - LAST) { m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step) } in POSITIVE; - m_op * (1 - m_op) = 0; - m_is_write * (1 - m_is_write) = 0; - m_is_read * (1 - m_is_read) = 0; - // m_is_write can only be 1 if m_op is 1. - m_is_write * (1 - m_op) = 0; - m_is_read * (1 - m_op) = 0; - m_is_read * m_is_write = 0; + m_op * (1 - m_op) = 0; + m_is_write * (1 - m_is_write) = 0; + m_is_read * (1 - m_is_read) = 0; + // m_is_write can only be 1 if m_op is 1. + m_is_write * (1 - m_op) = 0; + m_is_read * (1 - m_op) = 0; + m_is_read * m_is_write = 0; - // If the next line is a read and we stay at the same address, then the - // value cannot change. - (1 - m_is_write') * (1 - m_change) * (m_value' - m_value) = 0; + // If the next line is a read and we stay at the same address, then the + // value cannot change. + (1 - m_is_write') * (1 - m_change) * (m_value' - m_value) = 0; - // If the next line is a read and we have an address change, - // then the value is zero. - (1 - m_is_write') * m_change * m_value' = 0; - } + // If the next line is a read and we have an address change, + // then the value is zero. + (1 - m_is_write') * m_change * m_value' = 0; instr assert_zero X { XIsZero = 1 } instr mstore X { { ADDR, STEP, X } is m_is_write { m_addr, m_step, m_value } } diff --git a/test_data/asm/multi_assign.asm b/test_data/asm/multi_assign.asm index c73a5e5acc..4165de5d90 100644 --- a/test_data/asm/multi_assign.asm +++ b/test_data/asm/multi_assign.asm @@ -4,13 +4,11 @@ machine MultiAssign { reg Y[<=]; reg A; - constraints { - col witness XInv; - col witness XIsZero; - XIsZero = 1 - X * XInv; - XIsZero * X = 0; - XIsZero * (1 - XIsZero) = 0; - } + col witness XInv; + col witness XIsZero; + XIsZero = 1 - X * XInv; + XIsZero * X = 0; + XIsZero * (1 - XIsZero) = 0; instr assert_zero X { XIsZero = 1 } diff --git a/test_data/asm/palindrome.asm b/test_data/asm/palindrome.asm index e2953a5e86..3fa1dea4d9 100644 --- a/test_data/asm/palindrome.asm +++ b/test_data/asm/palindrome.asm @@ -12,26 +12,24 @@ machine Palindrome { reg CNT; reg ADDR; - constraints { - col witness XInv; - col witness XIsZero; - XIsZero = 1 - X * XInv; - XIsZero * X = 0; - XIsZero * (1 - XIsZero) = 0; + col witness XInv; + col witness XIsZero; + XIsZero = 1 - X * XInv; + XIsZero * X = 0; + XIsZero * (1 - XIsZero) = 0; - /// Write-once memory (actually a key-value store) - col witness m_addr; - col witness m_value; + /// Write-once memory (actually a key-value store) + col witness m_addr; + col witness m_value; - // positive numbers (assumed to be less than half the field order) - col fixed POSITIVE(i) { i + 1 }; - col fixed FIRST = [1] + [0]*; - col fixed NOTLAST = [1]* + [0]; + // positive numbers (assumed to be less than half the field order) + col fixed POSITIVE(i) { i + 1 }; + col fixed FIRST = [1] + [0]*; + col fixed NOTLAST = [1]* + [0]; - // This enforces that addresses are stored in an ascending order - // (and in particular, are unique). - NOTLAST { m_addr' - m_addr } in POSITIVE; - } + // This enforces that addresses are stored in an ascending order + // (and in particular, are unique). + NOTLAST { m_addr' - m_addr } in POSITIVE; instr jmpz X, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) } instr jmp l: label { pc' = l } diff --git a/test_data/asm/secondary_block_machine_add2.asm b/test_data/asm/secondary_block_machine_add2.asm index 7f39badcd2..ecd0377764 100644 --- a/test_data/asm/secondary_block_machine_add2.asm +++ b/test_data/asm/secondary_block_machine_add2.asm @@ -8,32 +8,29 @@ machine Main { reg A; reg B; + // Add a block state machine that adds 2 to a number by adding 1 two times + col fixed add_two_RESET = [0, 0, 1]*; + col fixed LAST = [0]* + [1]; + col fixed RESET = [0, 0, 1]* + [1]; - constraints { - // Add a block state machine that adds 2 to a number by adding 1 two times - col fixed add_two_RESET = [0, 0, 1]*; - col fixed LAST = [0]* + [1]; - col fixed RESET = [0, 0, 1]* + [1]; + // State is initialized with the input and incremented by 1 in each step + col witness add_two_state; + // The input column needs to be constant for the entire block + col witness add_two_input; - // State is initialized with the input and incremented by 1 in each step - col witness add_two_state; - // The input column needs to be constant for the entire block - col witness add_two_input; + // Because constraints are not cyclic, we need to explicitly constrain the first state + first_step * (add_two_state - add_two_input) = 0; - // Because constraints are not cyclic, we need to explicitly constrain the first state - first_step * (add_two_state - add_two_input) = 0; + // Add %offset in a single step of computation + constant %offset = 1; - // Add %offset in a single step of computation - constant %offset = 1; + // If RESET is true, constrain the next state to be equal to the input + // if RESET is false, increment the current state + add_two_state' = (1 - RESET) * (add_two_state + %offset) + RESET * add_two_input'; - // If RESET is true, constrain the next state to be equal to the input - // if RESET is false, increment the current state - add_two_state' = (1 - RESET) * (add_two_state + %offset) + RESET * add_two_input'; - - // If RESET is true, the next input is unconstrained - // If RESET is false, the next input is equal to the current input - 0 = (1 - RESET) * (add_two_input - add_two_input'); - } + // If RESET is true, the next input is unconstrained + // If RESET is false, the next input is equal to the current input + 0 = (1 - RESET) * (add_two_input - add_two_input'); instr add2 Y -> X { {Y, X} in add_two_RESET { add_two_input, add_two_state } diff --git a/test_data/asm/simple_sum.asm b/test_data/asm/simple_sum.asm index e441fe6d85..369a97927a 100644 --- a/test_data/asm/simple_sum.asm +++ b/test_data/asm/simple_sum.asm @@ -13,18 +13,15 @@ machine Main { reg A; reg CNT; - // Code in `constraints {`..`}` is pil code that is inserted into the pil file. - constraints { - col witness XInv; - col witness XIsZero; - // assume X = 7 - // XisZero * 7 = 0 -> XIzZero = 0 - // 0 = 1 - 7 * XInv - // => XInv = 1/7 (finite field) - XIsZero = 1 - X * XInv; - XIsZero * X = 0; - XIsZero * (1 - XIsZero) = 0; - } + col witness XInv; + col witness XIsZero; + // assume X = 7 + // XisZero * 7 = 0 -> XIzZero = 0 + // 0 = 1 - 7 * XInv + // => XInv = 1/7 (finite field) + XIsZero = 1 - X * XInv; + XIsZero * X = 0; + XIsZero * (1 - XIsZero) = 0; instr jmpz X, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) } instr jmp l: label { pc' = l } diff --git a/test_data/asm/vm_to_block_multiple_interfaces.asm b/test_data/asm/vm_to_block_multiple_interfaces.asm index 9631f5a3db..c570e4b94a 100644 --- a/test_data/asm/vm_to_block_multiple_interfaces.asm +++ b/test_data/asm/vm_to_block_multiple_interfaces.asm @@ -8,14 +8,12 @@ machine Arith(latch, operation_id) { operation sub<1> z, x -> y; - constraints { - col witness operation_id; - col fixed latch = [1]*; - col witness x; - col witness y; - col witness z; - z = x + y; - } + col witness operation_id; + col fixed latch = [1]*; + col witness x; + col witness y; + col witness z; + z = x + y; } machine Main { diff --git a/test_data/asm/vm_to_block_to_block.asm b/test_data/asm/vm_to_block_to_block.asm index e6230659c4..58f1d829c3 100644 --- a/test_data/asm/vm_to_block_to_block.asm +++ b/test_data/asm/vm_to_block_to_block.asm @@ -4,13 +4,11 @@ machine Inc(latch, operation_id) { operation inc<0> x -> y; - constraints { - col witness operation_id; - col fixed latch = [1]*; - col witness x; - col witness y; - y = x + 1; - } + col witness operation_id; + col fixed latch = [1]*; + col witness x; + col witness y; + y = x + 1; } machine Assert1(latch, operation_id) { @@ -24,14 +22,12 @@ machine Assert1(latch, operation_id) { // Increment x by calling into inc machine link 1 x -> y = inc.inc; - constraints { - col witness operation_id; - col fixed latch = [1]*; - col witness x; - col witness y; + col witness operation_id; + col fixed latch = [1]*; + col witness x; + col witness y; - y = 2; - } + y = 2; } machine Main { diff --git a/test_data/asm/vm_to_block_unique_interface.asm b/test_data/asm/vm_to_block_unique_interface.asm index 459e7392bd..20c7a4e160 100644 --- a/test_data/asm/vm_to_block_unique_interface.asm +++ b/test_data/asm/vm_to_block_unique_interface.asm @@ -4,18 +4,16 @@ machine Binary(latch, operation_id) { operation or<1> x, y -> z; - constraints { - col witness operation_id; - col fixed latch = [1]*; - col witness x; - col witness y; - col witness z; - col fixed P_FUNCTION = [0, 0, 0, 0, 1, 1, 1, 1] + [1]*; - col fixed P_X = [0, 0, 1, 1, 0, 0, 1, 1] + [1]*; - col fixed P_Y = [0, 1, 0, 1, 0, 1, 0, 1] + [1]*; - col fixed P_Z = [0, 0, 0, 1, 0, 1, 1, 1] + [1]*; - { operation_id, x, y, z } in { P_FUNCTION, P_X, P_Y, P_Z }; - } + col witness operation_id; + col fixed latch = [1]*; + col witness x; + col witness y; + col witness z; + col fixed P_FUNCTION = [0, 0, 0, 0, 1, 1, 1, 1] + [1]*; + col fixed P_X = [0, 0, 1, 1, 0, 0, 1, 1] + [1]*; + col fixed P_Y = [0, 1, 0, 1, 0, 1, 0, 1] + [1]*; + col fixed P_Z = [0, 0, 0, 1, 0, 1, 1, 1] + [1]*; + { operation_id, x, y, z } in { P_FUNCTION, P_X, P_Y, P_Z }; } machine Arith(latch, operation_id) { @@ -24,14 +22,12 @@ machine Arith(latch, operation_id) { operation sub<1> x, y -> z; - constraints { - col witness operation_id; - col fixed latch = [1]*; - col witness x; - col witness y; - col witness z; - z = (1 - operation_id) * (x + y) + operation_id * (x - y); - } + col witness operation_id; + col fixed latch = [1]*; + col witness x; + col witness y; + col witness z; + z = (1 - operation_id) * (x + y) + operation_id * (x - y); } machine Main { diff --git a/type_check/src/lib.rs b/type_check/src/lib.rs index 71eb766f02..743d08079b 100644 --- a/type_check/src/lib.rs +++ b/type_check/src/lib.rs @@ -5,7 +5,7 @@ use ast::{ AnalysisASMFile, AssignmentStatement, CallableSymbolDefinitions, DebugDirective, DegreeStatement, FunctionBody, FunctionStatements, FunctionSymbol, Instruction, InstructionDefinitionStatement, InstructionStatement, LabelStatement, - LinkDefinitionStatement, Machine, OperationSymbol, PilBlock, RegisterDeclarationStatement, + LinkDefinitionStatement, Machine, OperationSymbol, RegisterDeclarationStatement, RegisterTy, Return, SubmachineDeclaration, }, parsed::{ @@ -42,7 +42,7 @@ impl TypeChecker { let mut degree = None; let mut registers = vec![]; - let mut constraints = vec![]; + let mut pil = vec![]; let mut instructions = vec![]; let mut links = vec![]; let mut callable = CallableSymbolDefinitions::default(); @@ -87,8 +87,8 @@ impl TypeChecker { to, }); } - MachineStatement::InlinePil(start, statements) => { - constraints.push(PilBlock { start, statements }); + MachineStatement::Pil(_start, statement) => { + pil.push(statement); } MachineStatement::Submachine(_, ty, name) => { submachines.push(SubmachineDeclaration { @@ -234,7 +234,7 @@ impl TypeChecker { registers, links, instructions, - constraints, + pil, callable, submachines, };