From 91d41df9a06d52be9dc9c7d35756c3606abc67f1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gast=C3=B3n=20Zanitti?= Date: Mon, 1 Jul 2024 12:05:32 -0300 Subject: [PATCH] Allow blocks to be empty (#1435) This PR builds on top of #1393. It mainly modifies the grammar by changing the way SelectedExpressions are declared, to allow blocks to be empty. --------- Co-authored-by: chriseth --- analysis/README.md | 22 +-- asm-to-pil/src/vm_to_constrained.rs | 32 ++-- ast/src/analyzed/display.rs | 32 ++-- ast/src/analyzed/mod.rs | 116 +++++++++--- ast/src/parsed/display.rs | 34 +++- ast/src/parsed/mod.rs | 30 +-- .../json_exporter/expression_counter.rs | 11 +- backend/src/estark/json_exporter/mod.rs | 174 ------------------ backend/src/halo2/circuit_builder.rs | 5 +- book/src/pil/types.md | 6 +- executor/src/lib.rs | 4 + executor/src/witgen/block_processor.rs | 12 +- executor/src/witgen/generator.rs | 13 +- executor/src/witgen/global_constraints.rs | 17 +- executor/src/witgen/identity_processor.rs | 20 +- executor/src/witgen/machines/block_machine.rs | 14 +- .../machines/double_sorted_witness_machine.rs | 7 +- .../witgen/machines/fixed_lookup_machine.rs | 6 +- .../src/witgen/machines/machine_extractor.rs | 13 +- .../witgen/machines/sorted_witness_machine.rs | 18 +- .../src/witgen/machines/write_once_memory.rs | 23 +-- executor/src/witgen/mod.rs | 2 +- executor/src/witgen/processor.rs | 16 +- executor/src/witgen/vm_processor.rs | 19 +- importer/src/path_canonicalizer.rs | 5 +- linker/src/lib.rs | 103 ++++++----- parser/src/lib.rs | 30 ++- parser/src/powdr.lalrpop | 19 +- pil-analyzer/src/condenser.rs | 31 ++-- pil-analyzer/src/evaluator.rs | 29 ++- pil-analyzer/src/expression_processor.rs | 37 +++- pil-analyzer/src/pil_analyzer.rs | 19 +- pil-analyzer/src/statement_processor.rs | 22 +-- pil-analyzer/src/type_inference.rs | 6 +- pil-analyzer/tests/condenser.rs | 10 +- pil-analyzer/tests/parse_display.rs | 6 +- pil-analyzer/tests/types.rs | 46 ++++- pilopt/src/lib.rs | 30 +-- plonky3/src/prover/mod.rs | 2 +- riscv/src/code_gen.rs | 30 +-- std/machines/arith.asm | 24 +-- std/machines/binary.asm | 2 +- std/machines/memory.asm | 4 +- std/machines/memory_with_bootloader_write.asm | 4 +- std/machines/shift.asm | 2 +- std/machines/split/split_bn254.asm | 2 +- std/machines/split/split_gl.asm | 2 +- test_data/asm/bit_access.asm | 8 +- test_data/asm/block_machine_cache_miss.asm | 4 +- test_data/asm/connect_no_witgen.asm | 2 +- test_data/asm/functional_instructions.asm | 8 +- test_data/asm/mem_read_write.asm | 6 +- test_data/asm/mem_read_write_large_diffs.asm | 8 +- .../asm/mem_read_write_no_memory_accesses.asm | 6 +- .../asm/mem_read_write_with_bootloader.asm | 8 +- test_data/asm/palindrome.asm | 6 +- test_data/asm/pass_range_constraints.asm | 8 +- test_data/asm/permutations/block_to_block.asm | 2 +- .../call_selectors_with_no_permutation.asm | 2 +- test_data/asm/permutations/simple.asm | 2 +- test_data/asm/permutations/vm_to_block.asm | 2 +- .../asm/secondary_block_machine_add2.asm | 2 +- test_data/asm/sqrt.asm | 2 +- .../asm/vm_to_block_unique_interface.asm | 2 +- test_data/pil/block_lookup_or.pil | 4 +- test_data/pil/block_lookup_or_permutation.pil | 6 +- .../pil/conditional_fixed_constraints.pil | 12 +- test_data/pil/lookup_with_selector.pil | 2 +- test_data/pil/naive_byte_decomposition.pil | 16 +- test_data/pil/pair_lookup.pil | 4 +- test_data/pil/permutation_with_selector.pil | 2 +- test_data/pil/simple_div.pil | 12 +- test_data/pil/single_line_blocks.pil | 2 +- test_data/pil/two_block_machine_functions.pil | 8 +- test_data/pil/witness_lookup.pil | 4 +- test_data/polygon-hermez/arith.pil | 4 +- test_data/polygon-hermez/binary.pil | 4 +- test_data/polygon-hermez/keccakf.pil | 10 +- test_data/polygon-hermez/main.pil | 158 ++++++++-------- test_data/polygon-hermez/mem.pil | 2 +- test_data/polygon-hermez/mem_align.pil | 8 +- test_data/polygon-hermez/padding_kk.pil | 16 +- test_data/polygon-hermez/padding_kkbit.pil | 2 +- test_data/polygon-hermez/padding_pg.pil | 14 +- test_data/polygon-hermez/storage.pil | 14 +- 85 files changed, 771 insertions(+), 722 deletions(-) diff --git a/analysis/README.md b/analysis/README.md index 10f774a63..df386cabc 100644 --- a/analysis/README.md +++ b/analysis/README.md @@ -211,7 +211,7 @@ The diff for our example program is as follows: + pol constant p_instr_return = [0, 0, 1, 1, 1, 0] + [0]*; + pol constant p_read__output_0__input_0 = [0, 0, 1, 0, 0, 0] + [0]*; + pol constant p_read__output_0_pc = [0, 0, 0, 0, 0, 0] + [0]*; -+ { pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return, _output_0_const, _output_0_read_free, read__output_0_pc, read__output_0__input_0 } in { p_line, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p__output_0_const, p__output_0_read_free, p_read__output_0_pc, p_read__output_0__input_0 }; ++ [ pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return, _output_0_const, _output_0_read_free, read__output_0_pc, read__output_0__input_0 ] in [ p_line, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p__output_0_const, p__output_0_read_free, p_read__output_0_pc, p_read__output_0__input_0 ]; - function one -> field { - return 1; - // END BATCH @@ -290,7 +290,7 @@ The diff for our example program is as follows: + pol constant p_read_Y_pc = [0, 0, 0, 0, 0] + [0]*; + pol constant p_reg_write_X_A = [0, 0, 0, 0, 0] + [0]*; + pol constant p_reg_write_Y_A = [0, 0, 1, 0, 0] + [0]*; -+ { pc, reg_write_X_A, reg_write_Y_A, instr_identity, instr_one, instr_nothing, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_pc } in { p_line, p_reg_write_X_A, p_reg_write_Y_A, p_instr_identity, p_instr_one, p_instr_nothing, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_A, p_read_Y_pc }; ++ [ pc, reg_write_X_A, reg_write_Y_A, instr_identity, instr_one, instr_nothing, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_pc ] in [ p_line, p_reg_write_X_A, p_reg_write_Y_A, p_instr_identity, p_instr_one, p_instr_nothing, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_A, p_read_Y_pc ]; + } + + @@ -359,7 +359,7 @@ machine DifferentSignatures with latch: instr_return, operation_id: _operation_i pol constant p_instr_return = [0, 0, 1, 1, 1, 0] + [0]*; pol constant p_read__output_0__input_0 = [0, 0, 1, 0, 0, 0] + [0]*; pol constant p_read__output_0_pc = [0, 0, 0, 0, 0, 0] + [0]*; - { pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return, _output_0_const, _output_0_read_free, read__output_0_pc, read__output_0__input_0 } in { p_line, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p__output_0_const, p__output_0_read_free, p_read__output_0_pc, p_read__output_0__input_0 }; + [ pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return, _output_0_const, _output_0_read_free, read__output_0_pc, read__output_0__input_0 ] in [ p_line, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p__output_0_const, p__output_0_read_free, p_read__output_0_pc, p_read__output_0__input_0 ]; } constraints { @@ -429,7 +429,7 @@ machine Main with degree: 16, latch: instr_return, operation_id: _operation_id { pol constant p_read_Y_pc = [0, 0, 0, 0, 0] + [0]*; pol constant p_reg_write_X_A = [0, 0, 0, 0, 0] + [0]*; pol constant p_reg_write_Y_A = [0, 0, 1, 0, 0] + [0]*; - { pc, reg_write_X_A, reg_write_Y_A, instr_identity, instr_one, instr_nothing, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_pc } in { p_line, p_reg_write_X_A, p_reg_write_Y_A, p_instr_identity, p_instr_one, p_instr_nothing, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_A, p_read_Y_pc }; + [ pc, reg_write_X_A, reg_write_Y_A, instr_identity, instr_one, instr_nothing, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_pc ] in [ p_line, p_reg_write_X_A, p_reg_write_Y_A, p_instr_identity, p_instr_one, p_instr_nothing, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_A, p_read_Y_pc ]; } constraints { @@ -503,7 +503,7 @@ pol constant p_read_Y_A = [0, 0, 0, 0, 0] + [0]*; pol constant p_read_Y_pc = [0, 0, 0, 0, 0] + [0]*; pol constant p_reg_write_X_A = [0, 0, 0, 0, 0] + [0]*; pol constant p_reg_write_Y_A = [0, 0, 1, 0, 0] + [0]*; -{ pc, reg_write_X_A, reg_write_Y_A, instr_identity, instr_one, instr_nothing, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_pc } in { p_line, p_reg_write_X_A, p_reg_write_Y_A, p_instr_identity, p_instr_one, p_instr_nothing, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_A, p_read_Y_pc }; +[ pc, reg_write_X_A, reg_write_Y_A, instr_identity, instr_one, instr_nothing, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_pc ] in [ p_line, p_reg_write_X_A, p_reg_write_Y_A, p_instr_identity, p_instr_one, p_instr_nothing, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_A, p_read_Y_pc ]; pol constant _block_enforcer_last_step = [0]* + [1]; pol commit _operation_id_no_change; _operation_id_no_change = ((1 - _block_enforcer_last_step) * (1 - instr_return)); @@ -545,7 +545,7 @@ pol constant p_instr__reset = [1, 0, 0, 0, 0, 0] + [0]*; pol constant p_instr_return = [0, 0, 1, 1, 1, 0] + [0]*; pol constant p_read__output_0__input_0 = [0, 0, 1, 0, 0, 0] + [0]*; pol constant p_read__output_0_pc = [0, 0, 0, 0, 0, 0] + [0]*; -{ pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return, _output_0_const, _output_0_read_free, read__output_0_pc, read__output_0__input_0 } in { p_line, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p__output_0_const, p__output_0_read_free, p_read__output_0_pc, p_read__output_0__input_0 }; +[ pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return, _output_0_const, _output_0_read_free, read__output_0_pc, read__output_0__input_0 ] in [ p_line, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p__output_0_const, p__output_0_read_free, p_read__output_0_pc, p_read__output_0__input_0 ]; pol constant _block_enforcer_last_step = [0]* + [1]; pol commit _operation_id_no_change; _operation_id_no_change = ((1 - _block_enforcer_last_step) * (1 - instr_return)); @@ -611,14 +611,14 @@ pol constant p_read_Y_A = [0, 0, 0, 0, 0] + [0]*; pol constant p_read_Y_pc = [0, 0, 0, 0, 0] + [0]*; pol constant p_reg_write_X_A = [0, 0, 0, 0, 0] + [0]*; pol constant p_reg_write_Y_A = [0, 0, 1, 0, 0] + [0]*; -{ pc, reg_write_X_A, reg_write_Y_A, instr_identity, instr_one, instr_nothing, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_pc } in { p_line, p_reg_write_X_A, p_reg_write_Y_A, p_instr_identity, p_instr_one, p_instr_nothing, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_A, p_read_Y_pc }; +[ pc, reg_write_X_A, reg_write_Y_A, instr_identity, instr_one, instr_nothing, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_pc ] in [ p_line, p_reg_write_X_A, p_reg_write_Y_A, p_instr_identity, p_instr_one, p_instr_nothing, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_A, p_read_Y_pc ]; pol constant _block_enforcer_last_step = [0]* + [1]; pol commit _operation_id_no_change; _operation_id_no_change = ((1 - _block_enforcer_last_step) * (1 - instr_return)); (_operation_id_no_change * (_operation_id' - _operation_id)) = 0; -instr_identity { 2, X, Y } in main_sub.instr_return { main_sub._operation_id, main_sub._input_0, main_sub._output_0 }; -instr_one { 4, Y } in main_sub.instr_return { main_sub._operation_id, main_sub._output_0 }; -instr_nothing { 3 } in main_sub.instr_return { main_sub._operation_id }; +instr_identity $ [ 2, X, Y ] in main_sub.instr_return $ [ main_sub._operation_id, main_sub._input_0, main_sub._output_0 ]; +instr_one $ [ 4, Y ] in main_sub.instr_return $ [ main_sub._operation_id, main_sub._output_0 ]; +instr_nothing $ [ 3 ] in main_sub.instr_return $ [ main_sub._operation_id ]; pol constant _linker_first_step = [1] + [0]*; (_linker_first_step * (_operation_id - 2)) = 0; namespace main_sub(16); @@ -652,7 +652,7 @@ pol constant p_instr__reset = [1, 0, 0, 0, 0, 0] + [0]*; pol constant p_instr_return = [0, 0, 1, 1, 1, 0] + [0]*; pol constant p_read__output_0__input_0 = [0, 0, 1, 0, 0, 0] + [0]*; pol constant p_read__output_0_pc = [0, 0, 0, 0, 0, 0] + [0]*; -{ pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return, _output_0_const, _output_0_read_free, read__output_0_pc, read__output_0__input_0 } in { p_line, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p__output_0_const, p__output_0_read_free, p_read__output_0_pc, p_read__output_0__input_0 }; +[ pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return, _output_0_const, _output_0_read_free, read__output_0_pc, read__output_0__input_0 ] in [ p_line, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p__output_0_const, p__output_0_read_free, p_read__output_0_pc, p_read__output_0__input_0 ]; pol constant _block_enforcer_last_step = [0]* + [1]; pol commit _operation_id_no_change; _operation_id_no_change = ((1 - _block_enforcer_last_step) * (1 - instr_return)); diff --git a/asm-to-pil/src/vm_to_constrained.rs b/asm-to-pil/src/vm_to_constrained.rs index df563edf5..ece96b0fb 100644 --- a/asm-to-pil/src/vm_to_constrained.rs +++ b/asm-to-pil/src/vm_to_constrained.rs @@ -13,7 +13,7 @@ use powdr_ast::{ asm::{CallableRef, InstructionBody, InstructionParams, LinkDeclaration}, build::{self, absolute_reference, direct_reference, next_reference}, visitor::ExpressionVisitable, - ArrayExpression, BinaryOperation, BinaryOperator, Expression, FunctionCall, + ArrayExpression, ArrayLiteral, BinaryOperation, BinaryOperator, Expression, FunctionCall, FunctionDefinition, FunctionKind, LambdaExpression, MatchArm, MatchExpression, Number, Pattern, PilStatement, PolynomialName, SelectedExpressions, UnaryOperation, UnaryOperator, }, @@ -181,19 +181,29 @@ impl VMConverter { SourceRef::unknown(), SelectedExpressions { selector: None, - expressions: self - .line_lookup - .iter() - .map(|x| direct_reference(&x.0)) - .collect(), + expressions: Box::new( + ArrayLiteral { + items: self + .line_lookup + .iter() + .map(|x| direct_reference(&x.0)) + .collect(), + } + .into(), + ), }, SelectedExpressions { selector: None, - expressions: self - .line_lookup - .iter() - .map(|x| direct_reference(&x.1)) - .collect(), + expressions: Box::new( + ArrayLiteral { + items: self + .line_lookup + .iter() + .map(|x| direct_reference(&x.1)) + .collect(), + } + .into(), + ), }, )); diff --git a/ast/src/analyzed/display.rs b/ast/src/analyzed/display.rs index 906e8c500..fd4065438 100644 --- a/ast/src/analyzed/display.rs +++ b/ast/src/analyzed/display.rs @@ -267,7 +267,21 @@ impl Display for RepeatedArray { } } -impl Display for Identity { +impl Display for SelectedExpressions { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + write!( + f, + "{}[{}]", + self.selector + .as_ref() + .map(|s| format!("{s} $ ")) + .unwrap_or_default(), + self.expressions.iter().format(", ") + ) + } +} + +impl Display for Identity> { fn fmt(&self, f: &mut Formatter<'_>) -> Result { match self.kind { IdentityKind::Polynomial => { @@ -285,7 +299,7 @@ impl Display for Identity { } } -impl Display for Identity> { +impl Display for Identity>> { fn fmt(&self, f: &mut Formatter<'_>) -> Result { match self.kind { IdentityKind::Polynomial => { @@ -303,20 +317,6 @@ impl Display for Identity> { } } -impl Display for SelectedExpressions { - fn fmt(&self, f: &mut Formatter<'_>) -> Result { - write!( - f, - "{}{{ {} }}", - self.selector - .as_ref() - .map(|s| format!("{s} ")) - .unwrap_or_default(), - self.expressions.iter().format(", ") - ) - } -} - impl Display for Reference { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { diff --git a/ast/src/analyzed/mod.rs b/ast/src/analyzed/mod.rs index c08f5b414..451a77146 100644 --- a/ast/src/analyzed/mod.rs +++ b/ast/src/analyzed/mod.rs @@ -18,7 +18,7 @@ use crate::parsed::types::{ArrayType, Type, TypeScheme}; use crate::parsed::visitor::{Children, ExpressionVisitable}; pub use crate::parsed::BinaryOperator; pub use crate::parsed::UnaryOperator; -use crate::parsed::{self, EnumDeclaration, EnumVariant, SelectedExpressions}; +use crate::parsed::{self, ArrayLiteral, EnumDeclaration, EnumVariant}; #[derive(Debug, Clone, Serialize, Deserialize, JsonSchema, PartialEq, Eq)] pub enum StatementIdentifier { @@ -36,7 +36,7 @@ pub struct Analyzed { pub definitions: HashMap)>, pub public_declarations: HashMap, pub intermediate_columns: HashMap>)>, - pub identities: Vec>>, + pub identities: Vec>>>, /// The order in which definitions and identities /// appear in the source. pub source_order: Vec, @@ -168,8 +168,11 @@ impl Analyzed { .max() .unwrap_or_default() + 1; - self.identities - .push(Identity::from_polynomial_identity(id, source, identity)); + self.identities.push( + Identity::>>::from_polynomial_identity( + id, source, identity, + ), + ); self.source_order .push(StatementIdentifier::Identity(self.identities.len() - 1)); id @@ -306,7 +309,7 @@ impl Analyzed { /// @returns all identities with intermediate polynomials inlined. pub fn identities_with_inlined_intermediate_polynomials( &self, - ) -> Vec>> { + ) -> Vec>>> { let intermediates = &self .intermediate_polys_in_source_order() .iter() @@ -337,9 +340,9 @@ impl Analyzed { /// Takes identities as values and inlines intermediate polynomials everywhere, returning a vector of the updated identities /// TODO: this could return an iterator fn substitute_intermediate( - identities: impl IntoIterator>>, + identities: impl IntoIterator>>>, intermediate_polynomials: &HashMap>, -) -> Vec>> { +) -> Vec>>> { identities .into_iter() .scan(HashMap::default(), |cache, mut identity| { @@ -629,21 +632,51 @@ impl PublicDeclaration { } } +#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Serialize, Deserialize, JsonSchema)] +pub struct SelectedExpressions { + pub selector: Option, + pub expressions: Vec, +} + +impl Default for SelectedExpressions { + fn default() -> Self { + Self { + selector: Default::default(), + expressions: vec![], + } + } +} + +impl Children for SelectedExpressions { + /// Returns an iterator over all (top-level) expressions in this SelectedExpressions. + fn children(&self) -> Box + '_> { + Box::new(self.selector.iter().chain(self.expressions.iter())) + } + /// Returns an iterator over all (top-level) expressions in this SelectedExpressions. + fn children_mut(&mut self) -> Box + '_> { + Box::new(self.selector.iter_mut().chain(self.expressions.iter_mut())) + } +} + #[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, JsonSchema)] -pub struct Identity { +pub struct Identity { /// The ID is globally unique among identities. pub id: u64, pub kind: IdentityKind, pub source: SourceRef, /// For a simple polynomial identity, the selector contains /// the actual expression (see expression_for_poly_id). - pub left: SelectedExpressions, - pub right: SelectedExpressions, + pub left: SelectedExpressions, + pub right: SelectedExpressions, } -impl Identity { +impl Identity>> { /// Constructs an Identity from a polynomial identity (expression assumed to be identical zero). - pub fn from_polynomial_identity(id: u64, source: SourceRef, identity: Expr) -> Self { + pub fn from_polynomial_identity( + id: u64, + source: SourceRef, + identity: AlgebraicExpression, + ) -> Self { Identity { id, kind: IdentityKind::Polynomial, @@ -652,23 +685,24 @@ impl Identity { selector: Some(identity), expressions: vec![], }, - right: Default::default(), + right: SelectedExpressions { + selector: Default::default(), + expressions: vec![], + }, } } /// Returns the expression in case this is a polynomial identity. - pub fn expression_for_poly_id(&self) -> &Expr { + pub fn expression_for_poly_id(&self) -> &AlgebraicExpression { assert_eq!(self.kind, IdentityKind::Polynomial); self.left.selector.as_ref().unwrap() } /// Returns the expression in case this is a polynomial identity. - pub fn expression_for_poly_id_mut(&mut self) -> &mut Expr { + pub fn expression_for_poly_id_mut(&mut self) -> &mut AlgebraicExpression { assert_eq!(self.kind, IdentityKind::Polynomial); self.left.selector.as_mut().unwrap() } -} -impl Identity> { pub fn contains_next_ref(&self) -> bool { self.left.contains_next_ref() || self.right.contains_next_ref() } @@ -691,7 +725,35 @@ impl Identity> { } } -impl Identity> { +impl Identity>> { + /// Constructs an Identity from a polynomial identity (expression assumed to be identical zero). + pub fn from_polynomial_identity( + id: u64, + source: SourceRef, + identity: parsed::Expression, + ) -> Self { + Identity { + id, + kind: IdentityKind::Polynomial, + source, + left: parsed::SelectedExpressions { + selector: Some(identity), + expressions: Box::new(ArrayLiteral { items: vec![] }.into()), + }, + right: Default::default(), + } + } + /// Returns the expression in case this is a polynomial identity. + pub fn expression_for_poly_id(&self) -> &parsed::Expression { + assert_eq!(self.kind, IdentityKind::Polynomial); + self.left.selector.as_ref().unwrap() + } + + /// Returns the expression in case this is a polynomial identity. + pub fn expression_for_poly_id_mut(&mut self) -> &mut parsed::Expression { + assert_eq!(self.kind, IdentityKind::Polynomial); + self.left.selector.as_mut().unwrap() + } /// Either returns (a, Some(b)) if this is a - b or (a, None) /// if it is a polynomial identity of a different structure. /// Panics if it is a different kind of constraint. @@ -713,12 +775,24 @@ impl Identity> { } } -impl Children for Identity { - fn children_mut(&mut self) -> Box + '_> { +impl Children> for Identity>> { + fn children_mut(&mut self) -> Box> + '_> { Box::new(self.left.children_mut().chain(self.right.children_mut())) } - fn children(&self) -> Box + '_> { + fn children(&self) -> Box> + '_> { + Box::new(self.left.children().chain(self.right.children())) + } +} + +impl Children> + for Identity>> +{ + fn children_mut(&mut self) -> Box> + '_> { + Box::new(self.left.children_mut().chain(self.right.children_mut())) + } + + fn children(&self) -> Box> + '_> { Box::new(self.left.children().chain(self.right.children())) } } diff --git a/ast/src/parsed/display.rs b/ast/src/parsed/display.rs index 5501bf1d0..3693b9763 100644 --- a/ast/src/parsed/display.rs +++ b/ast/src/parsed/display.rs @@ -515,7 +515,7 @@ impl Display for PilStatement { PilStatement::ConnectIdentity(_, left, right) => write_indented_by( f, format!( - "{{ {} }} connect {{ {} }};", + "[ {} ] connect [ {} ];", format_list(left), format_list(right) ), @@ -596,6 +596,20 @@ impl EnumDeclaration { } } +impl Display for SelectedExpressions { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + write!( + f, + "{}{}", + self.selector + .as_ref() + .map(|s| format!("{s} $ ")) + .unwrap_or_default(), + self.expressions + ) + } +} + impl Display for EnumVariant { fn fmt(&self, f: &mut Formatter<'_>) -> Result { write!(f, "{}", self.name)?; @@ -820,11 +834,17 @@ impl Display for UnaryOperator { impl Display for BlockExpression { fn fmt(&self, f: &mut Formatter<'_>) -> Result { if self.statements.is_empty() { - write!(f, "{{ {} }}", self.expr) + if let Some(expr) = &self.expr { + write!(f, "{{ {expr} }}") + } else { + write!(f, "{{ }}") + } } else { writeln!(f, "{{")?; write_items_indented(f, &self.statements)?; - write_indented_by(f, &self.expr, 1)?; + if let Some(expr) = &self.expr { + write_indented_by(f, expr, 1)?; + } write!(f, "\n}}") } } @@ -1113,12 +1133,12 @@ mod tests { "a | b * (c << d + e) & (f ^ g) = h * (i + g);", ), ( - "instr_or { 0, X, Y, Z } is (main_bin.latch * main_bin.sel[0]) { main_bin.operation_id, main_bin.A, main_bin.B, main_bin.C };", - "instr_or { 0, X, Y, Z } is main_bin.latch * main_bin.sel[0] { main_bin.operation_id, main_bin.A, main_bin.B, main_bin.C };", + "instr_or $ [0, X, Y, Z] is (main_bin.latch * main_bin.sel[0]) $ [main_bin.operation_id, main_bin.A, main_bin.B, main_bin.C];", + "instr_or $ [0, X, Y, Z] is main_bin.latch * main_bin.sel[0] $ [main_bin.operation_id, main_bin.A, main_bin.B, main_bin.C];", ), ( - "instr_or { 0, X, Y, Z } is main_bin.latch * main_bin.sel[0] { main_bin.operation_id, main_bin.A, main_bin.B, main_bin.C };", - "instr_or { 0, X, Y, Z } is main_bin.latch * main_bin.sel[0] { main_bin.operation_id, main_bin.A, main_bin.B, main_bin.C };", + "instr_or $ [0, X, Y, Z] is main_bin.latch * main_bin.sel[0] $ [main_bin.operation_id, main_bin.A, main_bin.B, main_bin.C];", + "instr_or $ [0, X, Y, Z] is main_bin.latch * main_bin.sel[0] $ [main_bin.operation_id, main_bin.A, main_bin.B, main_bin.C];", ), ( "pc' = (1 - first_step') * ((((instr__jump_to_operation * _operation_id) + (instr__loop * pc)) + (instr_return * 0)) + ((1 - ((instr__jump_to_operation + instr__loop) + instr_return)) * (pc + 1)));", diff --git a/ast/src/parsed/mod.rs b/ast/src/parsed/mod.rs index ad3391ba8..007f13bfa 100644 --- a/ast/src/parsed/mod.rs +++ b/ast/src/parsed/mod.rs @@ -307,29 +307,33 @@ impl Children> for EnumVariant> { } #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Serialize, Deserialize, JsonSchema)] -pub struct SelectedExpressions { - pub selector: Option, - pub expressions: Vec, +pub struct SelectedExpressions> { + pub selector: Option, + pub expressions: Box, } -impl Default for SelectedExpressions { +impl Default for SelectedExpressions> { fn default() -> Self { Self { selector: Default::default(), - expressions: Default::default(), + expressions: Box::new(ArrayLiteral { items: vec![] }.into()), } } } -impl Children for SelectedExpressions { +impl Children> for SelectedExpressions> { /// Returns an iterator over all (top-level) expressions in this SelectedExpressions. - fn children(&self) -> Box + '_> { - Box::new(self.selector.iter().chain(self.expressions.iter())) + fn children(&self) -> Box> + '_> { + Box::new(self.selector.iter().chain(self.expressions.children())) } /// Returns an iterator over all (top-level) expressions in this SelectedExpressions. - fn children_mut(&mut self) -> Box + '_> { - Box::new(self.selector.iter_mut().chain(self.expressions.iter_mut())) + fn children_mut(&mut self) -> Box> + '_> { + Box::new( + self.selector + .iter_mut() + .chain(self.expressions.children_mut()), + ) } } @@ -561,7 +565,7 @@ impl Children for MatchExpression { #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Serialize, Deserialize, JsonSchema)] pub struct BlockExpression { pub statements: Vec>, - pub expr: Box, + pub expr: Option>, } impl From>> for Expression { @@ -576,7 +580,7 @@ impl Children for BlockExpression { self.statements .iter() .flat_map(|s| s.children()) - .chain(once(self.expr.as_ref())), + .chain(self.expr.iter().map(|boxed| &**boxed)), ) } @@ -585,7 +589,7 @@ impl Children for BlockExpression { self.statements .iter_mut() .flat_map(|s| s.children_mut()) - .chain(once(self.expr.as_mut())), + .chain(self.expr.iter_mut().map(|boxed| &mut **boxed)), ) } } diff --git a/backend/src/estark/json_exporter/expression_counter.rs b/backend/src/estark/json_exporter/expression_counter.rs index d3cf84628..35313bd67 100644 --- a/backend/src/estark/json_exporter/expression_counter.rs +++ b/backend/src/estark/json_exporter/expression_counter.rs @@ -1,11 +1,8 @@ use std::collections::HashMap; -use powdr_ast::{ - analyzed::{ - Analyzed, Identity, PolynomialType, PublicDeclaration, StatementIdentifier, Symbol, - SymbolKind, - }, - parsed::SelectedExpressions, +use powdr_ast::analyzed::{ + Analyzed, Identity, PolynomialType, PublicDeclaration, SelectedExpressions, + StatementIdentifier, Symbol, SymbolKind, }; /// Computes expression IDs for each intermediate polynomial. @@ -42,7 +39,7 @@ trait ExpressionCounter { fn expression_count(&self) -> usize; } -impl ExpressionCounter for Identity { +impl ExpressionCounter for Identity> { fn expression_count(&self) -> usize { self.left.expression_count() + self.right.expression_count() } diff --git a/backend/src/estark/json_exporter/mod.rs b/backend/src/estark/json_exporter/mod.rs index e70324f3f..8734d1320 100644 --- a/backend/src/estark/json_exporter/mod.rs +++ b/backend/src/estark/json_exporter/mod.rs @@ -417,185 +417,11 @@ fn offset_to_line_col(offset: usize, line_starts: &[usize]) -> (usize, usize) { #[cfg(test)] mod test { - use powdr_pil_analyzer::analyze_file; use pretty_assertions::assert_eq; - use serde_json::Value as JsonValue; - use std::{fs, process::Command}; use test_log::test; - use powdr_number::GoldilocksField; - use super::*; - fn generate_json_pair(file: &str) -> (JsonValue, JsonValue) { - let temp_dir = mktemp::Temp::new_dir().unwrap(); - let output_file = temp_dir.join("out.json"); - - let file = std::path::PathBuf::from(format!( - "{}/../test_data/polygon-hermez/", - env!("CARGO_MANIFEST_DIR") - )) - .join(file); - - let analyzed = analyze_file::(&file); - let pil_out = export(&analyzed); - - let pilcom = std::env::var("PILCOM").expect( - "Please set the PILCOM environment variable to the path to the pilcom repository.", - ); - let pilcom_output = Command::new("node") - .args([ - format!("{pilcom}/src/pil.js"), - file.display().to_string(), - "-o".to_string(), - format!("{}", output_file.to_string_lossy()), - ]) - .output() - .expect("failed to run pilcom"); - if !pilcom_output.status.success() { - panic!( - "Pilcom run was unsuccessful.\nStdout: {}\nStderr: {}\n", - String::from_utf8_lossy(&pilcom_output.stdout), - String::from_utf8_lossy(&pilcom_output.stderr) - ); - } - - let pilcom_out = fs::read_to_string(&output_file).unwrap_or_else(|_| { - panic!("Pilcom did not generate {output_file:?} at the expected location.") - }); - drop(temp_dir); - - let json_out = serde_json::to_value(pil_out).unwrap(); - - let mut pilcom_parsed = - serde_json::from_str(&pilcom_out).expect("Invalid json from pilcom."); - - // Filter out expression's "deps" before comparison, since we don't - // export them. - filter_out_deps(&mut pilcom_parsed); - - (json_out, pilcom_parsed) - } - - fn filter_out_deps(value: &mut serde_json::Value) { - match value { - JsonValue::Array(arr) => { - for e in arr { - filter_out_deps(e); - } - } - JsonValue::Object(obj) => { - if let serde_json::map::Entry::Occupied(deps) = obj.entry("deps") { - deps.remove(); - } - - for (_, e) in obj.iter_mut() { - filter_out_deps(e); - } - } - _ => (), - } - } - - fn compare_export_file(file: &str) { - let (json_out, pilcom_parsed) = generate_json_pair(file); - if json_out != pilcom_parsed { - // Computing the pretty diff can take minutes, so we are printing an error already here. - eprintln!("Exported json and file re-exported by pilcom differ:"); - assert_eq!(json_out, pilcom_parsed); - } - } - - /// Normalizes the json in that it replaces all idQ values by "99" - /// and converts hex numbers to decimal. - fn normalize_idq_and_hex(v: &mut JsonValue) { - match v { - JsonValue::Object(obj) => obj.iter_mut().for_each(|(key, value)| { - if key == "idQ" { - *value = 99.into(); - } else if key == "value" { - match value.as_str() { - Some(v) if v.starts_with("0x") => { - *value = - format!("{}", i64::from_str_radix(&v[2..], 16).unwrap()).into(); - } - _ => {} - } - } else { - normalize_idq_and_hex(value) - } - }), - JsonValue::Array(arr) => arr.iter_mut().for_each(normalize_idq_and_hex), - _ => {} - } - } - - fn compare_export_file_ignore_idq_hex(file: &str) { - let (mut json_out, mut pilcom_parsed) = generate_json_pair(file); - normalize_idq_and_hex(&mut json_out); - normalize_idq_and_hex(&mut pilcom_parsed); - assert_eq!(json_out, pilcom_parsed); - } - - #[test] - fn export_config() { - compare_export_file("config.pil"); - } - - #[test] - fn export_binary() { - compare_export_file("binary.pil"); - } - - #[test] - fn export_byte4() { - compare_export_file("byte4.pil"); - } - - #[test] - fn export_global() { - compare_export_file("global.pil"); - } - - #[test] - fn export_arith() { - // We ignore the specific value assigned to idQ. - // It is just a counter and pilcom assigns it in a weird order. - compare_export_file_ignore_idq_hex("arith.pil"); - } - - #[test] - fn export_mem() { - compare_export_file_ignore_idq_hex("mem.pil"); - compare_export_file_ignore_idq_hex("mem_align.pil"); - } - - #[test] - fn export_keccakf() { - compare_export_file_ignore_idq_hex("keccakf.pil"); - } - - #[test] - fn export_padding() { - compare_export_file("nine2one.pil"); - compare_export_file_ignore_idq_hex("padding_kkbit.pil"); - compare_export_file_ignore_idq_hex("padding_kk.pil"); - compare_export_file_ignore_idq_hex("padding_kk.pil"); - } - - #[test] - fn export_poseidong() { - compare_export_file_ignore_idq_hex("padding_pg.pil"); - compare_export_file_ignore_idq_hex("poseidong.pil"); - compare_export_file_ignore_idq_hex("storage.pil"); - } - - #[test] - fn export_main() { - compare_export_file_ignore_idq_hex("rom.pil"); - compare_export_file_ignore_idq_hex("main.pil"); - } - #[test] fn line_calc() { let input = "abc\nde"; diff --git a/backend/src/halo2/circuit_builder.rs b/backend/src/halo2/circuit_builder.rs index bad2785ef..0412b77ab 100644 --- a/backend/src/halo2/circuit_builder.rs +++ b/backend/src/halo2/circuit_builder.rs @@ -11,9 +11,8 @@ use halo2_proofs::{ }; use powdr_executor::witgen::WitgenCallback; -use powdr_ast::{ - analyzed::{AlgebraicBinaryOperation, AlgebraicBinaryOperator, AlgebraicExpression}, - parsed::SelectedExpressions, +use powdr_ast::analyzed::{ + AlgebraicBinaryOperation, AlgebraicBinaryOperator, AlgebraicExpression, SelectedExpressions, }; use powdr_ast::{ analyzed::{Analyzed, IdentityKind}, diff --git a/book/src/pil/types.md b/book/src/pil/types.md index b36130b4c..412b7edf9 100644 --- a/book/src/pil/types.md +++ b/book/src/pil/types.md @@ -49,7 +49,7 @@ The integer value is converted to a field element during evaluation, but it has the field modulus. If you reference such a symbol, the type of the reference is `expr`. -A byte constraint is as easy as `{ X } in { byte }`, since the expected types in plookup columns is `expr`. +A byte constraint is as easy as `[ X ] in [ byte ]`, since the expected types in plookup columns is `expr`. The downside is that you cannot evaluate columns as functions. If you want to do that, you either have to assign a copy to an `int -> int` symbol: `let byte_f: int -> int = |i| i & 0xff; let byte: col = byte_f;`. Or you can use the built-in function `std::prover::eval` if you want to do that inside a prover query or hint. @@ -61,7 +61,7 @@ All other symbols use their declared type both for their value and for reference `FromLiteral`: Implemented by `int`, `fe`, `expr`. The type of a number literal needs to implement `FromLiteral`. -``Add``: Implemented by `int`, `fe`, `expr`, `T[]`, `string`. Used by ` +: T, T -> T` (binary plus). +`Add`: Implemented by `int`, `fe`, `expr`, `T[]`, `string`. Used by ` +: T, T -> T` (binary plus). `Sub`: Implemented by `int`, `fe`, `expr`. Used by ` -: T, T -> T` (binary minus). @@ -302,4 +302,4 @@ let d = EnumName::Variant4(1, [2, 3], EnumName::Variant1); Recursive enums are allowed. -Enums do not allow any operators. \ No newline at end of file +Enums do not allow any operators. diff --git a/executor/src/lib.rs b/executor/src/lib.rs index 68b5e2973..51180e59f 100644 --- a/executor/src/lib.rs +++ b/executor/src/lib.rs @@ -2,5 +2,9 @@ #![deny(clippy::print_stdout)] +use powdr_ast::analyzed::{AlgebraicExpression, Identity as IdentityStruct, SelectedExpressions}; + pub mod constant_evaluator; pub mod witgen; + +type Identity = IdentityStruct>>; diff --git a/executor/src/witgen/block_processor.rs b/executor/src/witgen/block_processor.rs index fb8e13076..2573c7f24 100644 --- a/executor/src/witgen/block_processor.rs +++ b/executor/src/witgen/block_processor.rs @@ -1,10 +1,10 @@ use std::collections::HashSet; -use powdr_ast::analyzed::{ - AlgebraicExpression as Expression, AlgebraicReference, Identity, PolyID, -}; +use powdr_ast::analyzed::{AlgebraicReference, PolyID}; use powdr_number::FieldElement; +use crate::Identity; + use super::{ data_structures::finalizable_data::FinalizableData, processor::{OuterQuery, Processor}, @@ -22,7 +22,7 @@ use super::{ pub struct BlockProcessor<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> { processor: Processor<'a, 'b, 'c, T, Q>, /// The list of identities - identities: &'c [&'a Identity>], + identities: &'c [&'a Identity], } impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> BlockProcessor<'a, 'b, 'c, T, Q> { @@ -30,7 +30,7 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> BlockProcessor<'a, 'b, 'c row_offset: RowIndex, data: FinalizableData<'a, T>, mutable_state: &'c mut MutableState<'a, 'b, T, Q>, - identities: &'c [&'a Identity>], + identities: &'c [&'a Identity], fixed_data: &'a FixedData<'a, T>, witness_cols: &'c HashSet, ) -> Self { @@ -43,7 +43,7 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> BlockProcessor<'a, 'b, 'c pub fn from_processor( processor: Processor<'a, 'b, 'c, T, Q>, - identities: &'c [&'a Identity>], + identities: &'c [&'a Identity], ) -> Self { Self { processor, diff --git a/executor/src/witgen/generator.rs b/executor/src/witgen/generator.rs index b6a3d2b92..56d845244 100644 --- a/executor/src/witgen/generator.rs +++ b/executor/src/witgen/generator.rs @@ -1,6 +1,4 @@ -use powdr_ast::analyzed::{ - AlgebraicExpression as Expression, AlgebraicReference, Identity, PolyID, -}; +use powdr_ast::analyzed::{AlgebraicExpression as Expression, AlgebraicReference, PolyID}; use powdr_number::{DegreeType, FieldElement}; use std::collections::{BTreeMap, HashMap, HashSet}; @@ -9,6 +7,7 @@ use crate::witgen::machines::profiling::{record_end, record_start}; use crate::witgen::processor::OuterQuery; use crate::witgen::rows::CellValue; use crate::witgen::EvalValue; +use crate::Identity; use super::block_processor::BlockProcessor; use super::data_structures::column_map::WitnessColumnMap; @@ -24,9 +23,9 @@ struct ProcessResult<'a, T: FieldElement> { } pub struct Generator<'a, T: FieldElement> { - connecting_identities: BTreeMap>>, + connecting_identities: BTreeMap>, fixed_data: &'a FixedData<'a, T>, - identities: Vec<&'a Identity>>, + identities: Vec<&'a Identity>, witnesses: HashSet, data: FinalizableData<'a, T>, latch: Option>, @@ -109,8 +108,8 @@ impl<'a, T: FieldElement> Generator<'a, T> { pub fn new( name: String, fixed_data: &'a FixedData<'a, T>, - connecting_identities: &BTreeMap>>, - identities: Vec<&'a Identity>>, + connecting_identities: &BTreeMap>, + identities: Vec<&'a Identity>, witnesses: HashSet, latch: Option>, ) -> Self { diff --git a/executor/src/witgen/global_constraints.rs b/executor/src/witgen/global_constraints.rs index 1b540fcf6..37a48d393 100644 --- a/executor/src/witgen/global_constraints.rs +++ b/executor/src/witgen/global_constraints.rs @@ -5,12 +5,13 @@ use num_traits::Zero; use powdr_ast::analyzed::{ AlgebraicBinaryOperation, AlgebraicBinaryOperator, AlgebraicExpression as Expression, - AlgebraicReference, Identity, IdentityKind, PolyID, PolynomialType, + AlgebraicReference, IdentityKind, PolyID, PolynomialType, }; use powdr_number::FieldElement; use crate::witgen::data_structures::column_map::{FixedColumnMap, WitnessColumnMap}; +use crate::Identity; use super::expression_evaluator::ExpressionEvaluator; use super::range_constraints::RangeConstraint; @@ -109,8 +110,8 @@ impl RangeConstraintSet<&AlgebraicReference, T> for GlobalConst /// TODO at some point, we should check that they still hold. pub fn set_global_constraints<'a, T: FieldElement>( fixed_data: FixedData, - identities: impl IntoIterator>>, -) -> (FixedData, Vec<&'a Identity>>) { + identities: impl IntoIterator>, +) -> (FixedData, Vec<&'a Identity>) { let mut known_constraints = BTreeMap::new(); // For these columns, we know that they are not only constrained to those bits // but also have one row for each possible value. @@ -208,7 +209,7 @@ fn process_fixed_column(fixed: &[T]) -> Option<(RangeConstraint /// no further information than the range constraint. fn propagate_constraints( mut known_constraints: BTreeMap>, - identity: &Identity>, + identity: &Identity, full_span: &BTreeSet, ) -> (BTreeMap>, bool) { let mut remove = false; @@ -427,12 +428,12 @@ namespace Global(2**20); // A bit more complicated to see that the 'pattern matcher' works properly. (1 - A + 0) * (A + 1 - 1) = 0; col witness B; - { B } in { BYTE }; + [ B ] in [ BYTE ]; col witness C; C = A * 512 + B; col witness D; - { D } in { BYTE }; - { D } in { SHIFTED }; + [ D ] in [ BYTE ]; + [ D ] in [ SHIFTED ]; "; let analyzed = powdr_pil_analyzer::analyze_string::(pil_source); let constants = crate::constant_evaluator::generate(&analyzed); @@ -495,7 +496,7 @@ namespace Global(2**20); namespace Global(1024); let bytes: col = |i| i % 256; let X; - { X * 4 } in { bytes }; + [ X * 4 ] in [ bytes ]; "; let analyzed = powdr_pil_analyzer::analyze_string::(pil_source); let known_constraints = vec![(constant_poly_id(0), RangeConstraint::from_max_bit(7))] diff --git a/executor/src/witgen/identity_processor.rs b/executor/src/witgen/identity_processor.rs index 96f559751..856078c48 100644 --- a/executor/src/witgen/identity_processor.rs +++ b/executor/src/witgen/identity_processor.rs @@ -5,12 +5,13 @@ use std::{ use itertools::{Either, Itertools}; use lazy_static::lazy_static; -use powdr_ast::analyzed::{ - AlgebraicExpression as Expression, AlgebraicReference, Identity, IdentityKind, -}; +use powdr_ast::analyzed::{AlgebraicExpression as Expression, AlgebraicReference, IdentityKind}; use powdr_number::FieldElement; -use crate::witgen::{global_constraints::CombinedRangeConstraintSet, machines::Machine, EvalError}; +use crate::{ + witgen::{global_constraints::CombinedRangeConstraintSet, machines::Machine, EvalError}, + Identity, +}; use super::{ machines::{FixedLookup, KnownMachine}, @@ -126,7 +127,7 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> IdentityProcessor<'a, 'b, /// Returns the updates. pub fn process_identity( &mut self, - identity: &'a Identity>, + identity: &'a Identity, rows: &RowPair<'_, 'a, T>, ) -> EvalResult<'a, T> { let result = match identity.kind { @@ -148,7 +149,7 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> IdentityProcessor<'a, 'b, fn process_polynomial_identity( &self, - identity: &'a Identity>, + identity: &'a Identity, rows: &RowPair, ) -> EvalResult<'a, T> { match rows.evaluate(identity.expression_for_poly_id()) { @@ -159,7 +160,7 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> IdentityProcessor<'a, 'b, fn process_plookup( &mut self, - identity: &'a Identity>, + identity: &'a Identity, rows: &RowPair<'_, 'a, T>, ) -> EvalResult<'a, T> { if let Some(left_selector) = &identity.left.selector { @@ -284,10 +285,7 @@ lazy_static! { Mutex::new(Default::default()); } -fn report_identity_solving( - identity: &Identity>, - result: &EvalResult, -) { +fn report_identity_solving(identity: &Identity, result: &EvalResult) { let success = result.as_ref().map(|r| r.is_complete()).unwrap_or_default() as u64; let mut stat = STATISTICS.lock().unwrap(); stat.entry(identity.id) diff --git a/executor/src/witgen/machines/block_machine.rs b/executor/src/witgen/machines/block_machine.rs index 24d71970b..369911572 100644 --- a/executor/src/witgen/machines/block_machine.rs +++ b/executor/src/witgen/machines/block_machine.rs @@ -15,10 +15,10 @@ use crate::witgen::sequence_iterator::{ use crate::witgen::util::try_to_simple_poly; use crate::witgen::{machines::Machine, EvalError, EvalValue, IncompleteCause}; use crate::witgen::{MutableState, QueryCallback}; +use crate::Identity; use itertools::Itertools; use powdr_ast::analyzed::{ - AlgebraicExpression as Expression, AlgebraicReference, Identity, IdentityKind, PolyID, - PolynomialType, + AlgebraicExpression as Expression, AlgebraicReference, IdentityKind, PolyID, PolynomialType, }; use powdr_ast::parsed::visitor::ExpressionVisitable; use powdr_number::{DegreeType, FieldElement}; @@ -103,11 +103,11 @@ pub struct BlockMachine<'a, T: FieldElement> { /// The row index (within the block) of the latch row latch_row: usize, /// Connecting identities, indexed by their ID. - connecting_identities: BTreeMap>>, + connecting_identities: BTreeMap>, /// The type of constraint used to connect this machine to its caller. connection_type: ConnectionType, /// The internal identities - identities: Vec<&'a Identity>>, + identities: Vec<&'a Identity>, /// The data of the machine. data: FinalizableData<'a, T>, /// The set of witness columns that are actually part of this machine. @@ -123,8 +123,8 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> { pub fn try_new( name: String, fixed_data: &'a FixedData<'a, T>, - connecting_identities: &BTreeMap>>, - identities: &[&'a Identity>], + connecting_identities: &BTreeMap>, + identities: &[&'a Identity], witness_cols: &HashSet, ) -> Option { let (is_permutation, block_size, latch_row) = @@ -175,7 +175,7 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> { fn detect_connection_type_and_block_size<'a, T: FieldElement>( fixed_data: &'a FixedData<'a, T>, - connecting_identities: &BTreeMap>>, + connecting_identities: &BTreeMap>, ) -> Option<(ConnectionType, usize, usize)> { // TODO we should check that the other constraints/fixed columns are also periodic. diff --git a/executor/src/witgen/machines/double_sorted_witness_machine.rs b/executor/src/witgen/machines/double_sorted_witness_machine.rs index 9da0c7c10..1627879b2 100644 --- a/executor/src/witgen/machines/double_sorted_witness_machine.rs +++ b/executor/src/witgen/machines/double_sorted_witness_machine.rs @@ -8,9 +8,10 @@ use crate::witgen::rows::RowPair; use crate::witgen::util::try_to_simple_poly; use crate::witgen::{EvalResult, FixedData, MutableState, QueryCallback}; use crate::witgen::{EvalValue, IncompleteCause}; +use crate::Identity; use powdr_number::{DegreeType, FieldElement}; -use powdr_ast::analyzed::{AlgebraicExpression as Expression, Identity, IdentityKind, PolyID}; +use powdr_ast::analyzed::{IdentityKind, PolyID}; /// If all witnesses of a machine have a name in this list (disregarding the namespace), /// we'll consider it to be a double-sorted machine. @@ -61,7 +62,7 @@ pub struct DoubleSortedWitnesses<'a, T: FieldElement> { has_bootloader_write_column: bool, /// All selector IDs that are used on the right-hand side connecting identities. selector_ids: BTreeMap, - connecting_identities: BTreeMap>>, + connecting_identities: BTreeMap>, } struct Operation { @@ -79,7 +80,7 @@ impl<'a, T: FieldElement> DoubleSortedWitnesses<'a, T> { pub fn try_new( name: String, fixed_data: &'a FixedData, - connecting_identities: &BTreeMap>>, + connecting_identities: &BTreeMap>, witness_cols: &HashSet, ) -> Option { // get the namespaces and column names diff --git a/executor/src/witgen/machines/fixed_lookup_machine.rs b/executor/src/witgen/machines/fixed_lookup_machine.rs index 1fe744575..a9e805269 100644 --- a/executor/src/witgen/machines/fixed_lookup_machine.rs +++ b/executor/src/witgen/machines/fixed_lookup_machine.rs @@ -6,8 +6,8 @@ use std::num::NonZeroUsize; use itertools::Itertools; use powdr_ast::analyzed::{ AlgebraicExpression as Expression, AlgebraicReference, IdentityKind, PolyID, PolynomialType, + SelectedExpressions, }; -use powdr_ast::parsed::SelectedExpressions; use powdr_number::FieldElement; use crate::witgen::affine_expression::AffineExpression; @@ -230,12 +230,12 @@ impl FixedLookup { && !left.first().unwrap().is_constant() && right.peek().unwrap().poly_id.ptype == PolynomialType::Constant { - // Lookup of the form "c { X } in { B }". Might be a conditional range check. + // Lookup of the form "c $ [ X ] in [ B ]". Might be a conditional range check. return self.process_range_check(rows, left.first().unwrap(), right.peek().unwrap()); } // split the fixed columns depending on whether their associated lookup variable is constant or not. Preserve the value of the constant arguments. - // {1, 2, x} in {A, B, C} -> [[(A, 1), (B, 2)], [C, x]] + // [1, 2, x] in [A, B, C] -> [[(A, 1), (B, 2)], [C, x]] let mut input_assignment = vec![]; let mut output_columns = vec![]; diff --git a/executor/src/witgen/machines/machine_extractor.rs b/executor/src/witgen/machines/machine_extractor.rs index ef3b5f581..5a32a7dee 100644 --- a/executor/src/witgen/machines/machine_extractor.rs +++ b/executor/src/witgen/machines/machine_extractor.rs @@ -9,16 +9,17 @@ use super::FixedData; use super::KnownMachine; use crate::witgen::generator::Generator; use crate::witgen::machines::write_once_memory::WriteOnceMemory; +use crate::Identity; use itertools::Itertools; -use powdr_ast::analyzed::{AlgebraicExpression as Expression, Identity, IdentityKind, PolyID}; +use powdr_ast::analyzed::SelectedExpressions; +use powdr_ast::analyzed::{AlgebraicExpression as Expression, IdentityKind, PolyID}; use powdr_ast::parsed::visitor::ExpressionVisitable; -use powdr_ast::parsed::SelectedExpressions; use powdr_number::FieldElement; pub struct ExtractionOutput<'a, T: FieldElement> { pub fixed_lookup: FixedLookup, pub machines: Vec>, - pub base_identities: Vec<&'a Identity>>, + pub base_identities: Vec<&'a Identity>, pub base_witnesses: HashSet, } @@ -27,7 +28,7 @@ pub struct ExtractionOutput<'a, T: FieldElement> { /// that are not "internal" to the machines. pub fn split_out_machines<'a, T: FieldElement>( fixed: &'a FixedData<'a, T>, - identities: Vec<&'a Identity>>, + identities: Vec<&'a Identity>, ) -> ExtractionOutput<'a, T> { let fixed_lookup = FixedLookup::new(fixed.global_range_constraints().clone()); @@ -191,7 +192,7 @@ pub fn split_out_machines<'a, T: FieldElement>( fn all_row_connected_witnesses( mut witnesses: HashSet, all_witnesses: &HashSet, - identities: &[&Identity>], + identities: &[&Identity], ) -> HashSet { loop { let count = witnesses.len(); @@ -224,7 +225,7 @@ fn all_row_connected_witnesses( } /// Extracts all references to names from an identity. -pub fn refs_in_identity(identity: &Identity>) -> HashSet { +pub fn refs_in_identity(identity: &Identity) -> HashSet { let mut refs: HashSet = Default::default(); identity.pre_visit_expressions(&mut |expr| { ref_of_expression(expr).map(|id| refs.insert(id)); diff --git a/executor/src/witgen/machines/sorted_witness_machine.rs b/executor/src/witgen/machines/sorted_witness_machine.rs index f17798e4a..2f93bdd4b 100644 --- a/executor/src/witgen/machines/sorted_witness_machine.rs +++ b/executor/src/witgen/machines/sorted_witness_machine.rs @@ -11,21 +11,22 @@ use crate::witgen::{ symbolic_evaluator::SymbolicEvaluator, }; use crate::witgen::{EvalValue, IncompleteCause, MutableState, QueryCallback}; +use crate::Identity; use powdr_ast::analyzed::{ - AlgebraicExpression as Expression, AlgebraicReference, Identity, IdentityKind, PolyID, + AlgebraicExpression as Expression, AlgebraicReference, IdentityKind, PolyID, }; use powdr_number::FieldElement; /// A machine that can support a lookup in a set of columns that are sorted /// by one specific column and values in that column have to be unique. /// This means there is a column A and a constraint of the form -/// NOTLAST { A' - A } in { POSITIVE } +/// NOTLAST $ [ A' - A ] in [ POSITIVE ] /// Where /// - NOTLAST is zero only on the last row /// - POSITIVE has all values from 1 to half of the field size. pub struct SortedWitnesses<'a, T: FieldElement> { rhs_references: BTreeMap>, - connecting_identities: BTreeMap>>, + connecting_identities: BTreeMap>, key_col: PolyID, /// Position of the witness columns in the data. witness_positions: HashMap, @@ -38,8 +39,8 @@ impl<'a, T: FieldElement> SortedWitnesses<'a, T> { pub fn try_new( name: String, fixed_data: &'a FixedData, - connecting_identities: &BTreeMap>>, - identities: &[&Identity>], + connecting_identities: &BTreeMap>, + identities: &[&Identity], witnesses: &HashSet, ) -> Option { if identities.len() != 1 { @@ -90,11 +91,8 @@ impl<'a, T: FieldElement> SortedWitnesses<'a, T> { } } -fn check_identity( - fixed_data: &FixedData, - id: &Identity>, -) -> Option { - // Looking for NOTLAST { A' - A } in { POSITIVE } +fn check_identity(fixed_data: &FixedData, id: &Identity) -> Option { + // Looking for NOTLAST $ [ A' - A ] in [ POSITIVE ] if id.kind != IdentityKind::Plookup || id.right.selector.is_some() || id.left.expressions.len() != 1 diff --git a/executor/src/witgen/machines/write_once_memory.rs b/executor/src/witgen/machines/write_once_memory.rs index 24f0a6ba9..f803f6892 100644 --- a/executor/src/witgen/machines/write_once_memory.rs +++ b/executor/src/witgen/machines/write_once_memory.rs @@ -2,14 +2,15 @@ use std::collections::{BTreeMap, HashMap}; use itertools::{Either, Itertools}; -use powdr_ast::analyzed::{ - AlgebraicExpression as Expression, Identity, IdentityKind, PolyID, PolynomialType, -}; +use powdr_ast::analyzed::{IdentityKind, PolyID, PolynomialType}; use powdr_number::{DegreeType, FieldElement}; -use crate::witgen::{ - rows::RowPair, util::try_to_simple_poly, EvalError, EvalResult, EvalValue, FixedData, - IncompleteCause, MutableState, QueryCallback, +use crate::{ + witgen::{ + rows::RowPair, util::try_to_simple_poly, EvalError, EvalResult, EvalValue, FixedData, + IncompleteCause, MutableState, QueryCallback, + }, + Identity, }; use super::{FixedLookup, Machine}; @@ -21,14 +22,14 @@ use super::{FixedLookup, Machine}; /// let ADDR = |i| i; /// let v; /// // Stores a value, fails if the cell already has a value that's different -/// instr mstore X, Y -> { {X, Y} in {ADDR, v} } +/// instr mstore X, Y -> { [X, Y] in [ADDR, v] } /// // Loads a value. If the cell is empty, the prover can choose a value. /// // Note that this is the same lookup, only Y is considered an output instead /// // of an input. -/// instr mload X -> Y { {X, Y} in {ADDR, v} } +/// instr mload X -> Y { [X, Y] in [ADDR, v] } /// ``` pub struct WriteOnceMemory<'a, T: FieldElement> { - connecting_identities: BTreeMap>>, + connecting_identities: BTreeMap>, /// The fixed data fixed_data: &'a FixedData<'a, T>, /// The polynomials that are used as values (witness polynomials on the RHS) @@ -44,8 +45,8 @@ impl<'a, T: FieldElement> WriteOnceMemory<'a, T> { pub fn try_new( name: String, fixed_data: &'a FixedData<'a, T>, - connecting_identities: &BTreeMap>>, - identities: &[&Identity>], + connecting_identities: &BTreeMap>, + identities: &[&Identity], ) -> Option { if !identities.is_empty() { return None; diff --git a/executor/src/witgen/mod.rs b/executor/src/witgen/mod.rs index ce3c726c2..36dd0f381 100644 --- a/executor/src/witgen/mod.rs +++ b/executor/src/witgen/mod.rs @@ -180,7 +180,7 @@ impl<'a, 'b, T: FieldElement> WitnessGenerator<'a, 'b, T> { }) .collect::>(); - // Removes identities like X * (X - 1) = 0 or { A } in { BYTES } + // Removes identities like X * (X - 1) = 0 or [ A ] in [ BYTES ] // These are already captured in the range constraints. let (fixed, retained_identities) = global_constraints::set_global_constraints(fixed, &identities); diff --git a/executor/src/witgen/processor.rs b/executor/src/witgen/processor.rs index 3bd34a3a9..25b454cad 100644 --- a/executor/src/witgen/processor.rs +++ b/executor/src/witgen/processor.rs @@ -1,12 +1,11 @@ use std::collections::{BTreeMap, HashSet}; use powdr_ast::analyzed::PolynomialType; -use powdr_ast::analyzed::{ - AlgebraicExpression as Expression, AlgebraicReference, Identity, PolyID, -}; +use powdr_ast::analyzed::{AlgebraicExpression as Expression, AlgebraicReference, PolyID}; use powdr_number::{DegreeType, FieldElement}; use crate::witgen::{query_processor::QueryProcessor, util::try_to_simple_poly, Constraint}; +use crate::Identity; use super::{ affine_expression::AffineExpression, @@ -27,16 +26,13 @@ pub struct OuterQuery<'a, 'b, T: FieldElement> { /// Rows of the calling machine. pub caller_rows: &'b RowPair<'b, 'a, T>, /// Connecting identity. - pub connecting_identity: &'a Identity>, + pub connecting_identity: &'a Identity, /// The left side of the connecting identity, evaluated. pub left: Left<'a, T>, } impl<'a, 'b, T: FieldElement> OuterQuery<'a, 'b, T> { - pub fn new( - caller_rows: &'b RowPair<'b, 'a, T>, - connecting_identity: &'a Identity>, - ) -> Self { + pub fn new(caller_rows: &'b RowPair<'b, 'a, T>, connecting_identity: &'a Identity) -> Self { // Evaluate once, for performance reasons. let left = connecting_identity .left @@ -204,7 +200,7 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> Processor<'a, 'b, 'c, T, pub fn process_identity( &mut self, row_index: usize, - identity: &'a Identity>, + identity: &'a Identity, unknown_strategy: UnknownStrategy, ) -> Result> { // Create row pair @@ -486,7 +482,7 @@ Known values in current row (local: {row_index}, global {global_row_index}): &mut self, row_index: usize, proposed_row: &Row<'a, T>, - identity: &'a Identity>, + identity: &'a Identity, // This could be computed from the identity, but should be pre-computed for performance reasons. has_next_reference: bool, ) -> bool { diff --git a/executor/src/witgen/vm_processor.rs b/executor/src/witgen/vm_processor.rs index 7f2abeb9b..ba0dc6556 100644 --- a/executor/src/witgen/vm_processor.rs +++ b/executor/src/witgen/vm_processor.rs @@ -1,8 +1,6 @@ use indicatif::{ProgressBar, ProgressStyle}; use itertools::Itertools; -use powdr_ast::analyzed::{ - AlgebraicExpression as Expression, AlgebraicReference, Identity, IdentityKind, PolyID, -}; +use powdr_ast::analyzed::{AlgebraicReference, IdentityKind, PolyID}; use powdr_ast::indent; use powdr_number::{DegreeType, FieldElement}; use std::cmp::max; @@ -11,6 +9,7 @@ use std::time::Instant; use crate::witgen::identity_processor::{self}; use crate::witgen::IncompleteCause; +use crate::Identity; use super::data_structures::finalizable_data::FinalizableData; use super::processor::{OuterQuery, Processor}; @@ -25,18 +24,18 @@ const REPORT_FREQUENCY: u64 = 1_000; /// A list of identities with a flag whether it is complete. struct CompletableIdentities<'a, T: FieldElement> { - identities_with_complete: Vec<(&'a Identity>, bool)>, + identities_with_complete: Vec<(&'a Identity, bool)>, } impl<'a, T: FieldElement> CompletableIdentities<'a, T> { - fn new(identities: impl Iterator>>) -> Self { + fn new(identities: impl Iterator>) -> Self { Self { identities_with_complete: identities.map(|identity| (identity, false)).collect(), } } /// Yields immutable references to the identity and mutable references to the complete flag. - fn iter_mut(&mut self) -> impl Iterator>, &mut bool)> { + fn iter_mut(&mut self) -> impl Iterator, &mut bool)> { self.identities_with_complete .iter_mut() .map(|(identity, complete)| (*identity, complete)) @@ -51,10 +50,10 @@ pub struct VmProcessor<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> { fixed_data: &'a FixedData<'a, T>, /// The subset of identities that contains a reference to the next row /// (precomputed once for performance reasons) - identities_with_next_ref: Vec<&'a Identity>>, + identities_with_next_ref: Vec<&'a Identity>, /// The subset of identities that does not contain a reference to the next row /// (precomputed once for performance reasons) - identities_without_next_ref: Vec<&'a Identity>>, + identities_without_next_ref: Vec<&'a Identity>, last_report: DegreeType, last_report_time: Instant, processor: Processor<'a, 'b, 'c, T, Q>, @@ -65,7 +64,7 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> VmProcessor<'a, 'b, 'c, T pub fn new( row_offset: RowIndex, fixed_data: &'a FixedData<'a, T>, - identities: &[&'a Identity>], + identities: &[&'a Identity], witnesses: &'c HashSet, data: FinalizableData<'a, T>, mutable_state: &'c mut MutableState<'a, 'b, T, Q>, @@ -401,7 +400,7 @@ impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback> VmProcessor<'a, 'b, 'c, T fn process_identity( &mut self, row_index: DegreeType, - identity: &'a Identity>, + identity: &'a Identity, is_complete: &mut bool, unknown_strategy: UnknownStrategy, ) -> Result, EvalError> { diff --git a/importer/src/path_canonicalizer.rs b/importer/src/path_canonicalizer.rs index 3d29ba38c..d529ef3b1 100644 --- a/importer/src/path_canonicalizer.rs +++ b/importer/src/path_canonicalizer.rs @@ -767,7 +767,10 @@ fn check_expression( } } } - check_expression(location, expr, state, &local_variables) + match expr { + Some(expr) => check_expression(location, expr, state, &local_variables), + None => Ok(()), + } } } } diff --git a/linker/src/lib.rs b/linker/src/lib.rs index 407bc6e1d..7c39a4ab1 100644 --- a/linker/src/lib.rs +++ b/linker/src/lib.rs @@ -8,7 +8,7 @@ use powdr_ast::{ parsed::{ asm::{AbsoluteSymbolPath, SymbolPath}, build::{index_access, namespaced_reference}, - PILFile, PilStatement, SelectedExpressions, TypedExpression, + ArrayLiteral, PILFile, PilStatement, SelectedExpressions, TypedExpression, }, }; use powdr_parser_util::SourceRef; @@ -146,10 +146,15 @@ fn process_link(link: Link) -> PilStatement { // permutation lhs is `flag { operation_id, inputs, outputs }` let lhs = SelectedExpressions { selector: Some(from.flag), - expressions: op_id - .chain(from.params.inputs) - .chain(from.params.outputs) - .collect(), + expressions: Box::new( + ArrayLiteral { + items: op_id + .chain(from.params.inputs) + .chain(from.params.outputs) + .collect(), + } + .into(), + ), }; // permutation rhs is `(latch * selector[idx]) { operation_id, inputs, outputs }` @@ -172,24 +177,35 @@ fn process_link(link: Link) -> PilStatement { let rhs = SelectedExpressions { selector: rhs_selector, - expressions: op_id - .chain(to.operation.params.inputs_and_outputs().map(|i| { - index_access( - namespaced_reference(to_namespace.clone(), &i.name), - i.index.clone(), - ) - })) - .collect(), + expressions: Box::new( + ArrayLiteral { + items: op_id + .chain(to.operation.params.inputs_and_outputs().map(|i| { + index_access( + namespaced_reference(to_namespace.clone(), &i.name), + i.index.clone(), + ) + })) + .collect(), + } + .into(), + ), }; + PilStatement::PermutationIdentity(SourceRef::unknown(), lhs, rhs) } else { - // plookup lhs is `flag { operation_id, inputs, outputs }` + // plookup lhs is `flag $ [ operation_id, inputs, outputs ]` let lhs = SelectedExpressions { selector: Some(from.flag), - expressions: op_id - .chain(from.params.inputs) - .chain(from.params.outputs) - .collect(), + expressions: Box::new( + ArrayLiteral { + items: op_id + .chain(from.params.inputs) + .chain(from.params.outputs) + .collect(), + } + .into(), + ), }; let to_namespace = to.machine.location.clone().to_string(); @@ -199,7 +215,7 @@ fn process_link(link: Link) -> PilStatement { .map(|oid| namespaced_reference(to_namespace.clone(), oid)) .into_iter(); - // plookup rhs is `latch { operation_id, inputs, outputs }` + // plookup rhs is `latch $ [ operation_id, inputs, outputs ]` let latch = Some(namespaced_reference( to_namespace.clone(), to.machine.latch.unwrap(), @@ -207,14 +223,19 @@ fn process_link(link: Link) -> PilStatement { let rhs = SelectedExpressions { selector: latch, - expressions: op_id - .chain(to.operation.params.inputs_and_outputs().map(|i| { - index_access( - namespaced_reference(to_namespace.clone(), &i.name), - i.index.clone(), - ) - })) - .collect(), + expressions: Box::new( + ArrayLiteral { + items: op_id + .chain(to.operation.params.inputs_and_outputs().map(|i| { + index_access( + namespaced_reference(to_namespace.clone(), &i.name), + i.index.clone(), + ) + })) + .collect(), + } + .into(), + ), }; PilStatement::PlookupIdentity(SourceRef::unknown(), lhs, rhs) } @@ -318,7 +339,7 @@ mod test { pol constant p_instr__loop = [0, 0, 1] + [1]*; pol constant p_instr__reset = [1, 0, 0] + [0]*; pol constant p_instr_return = [0]*; - { pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return } in { p_line, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return }; + [pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return] in [p_line, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return]; "#; let file_name = format!( @@ -403,10 +424,10 @@ mod test { pol constant p_read_Y_pc = [0]*; pol constant p_reg_write_X_A = [0]*; pol constant p_reg_write_Y_A = [0, 0, 1, 0, 0] + [0]*; - { pc, reg_write_X_A, reg_write_Y_A, instr_identity, instr_one, instr_nothing, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_pc } in { p_line, p_reg_write_X_A, p_reg_write_Y_A, p_instr_identity, p_instr_one, p_instr_nothing, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_A, p_read_Y_pc }; - instr_identity { 2, X, Y } in main_sub.instr_return { main_sub._operation_id, main_sub._input_0, main_sub._output_0 }; - instr_one { 4, Y } in main_sub.instr_return { main_sub._operation_id, main_sub._output_0 }; - instr_nothing { 3 } in main_sub.instr_return { main_sub._operation_id }; + [pc, reg_write_X_A, reg_write_Y_A, instr_identity, instr_one, instr_nothing, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_pc] in [p_line, p_reg_write_X_A, p_reg_write_Y_A, p_instr_identity, p_instr_one, p_instr_nothing, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_A, p_read_Y_pc]; + instr_identity $ [2, X, Y] in main_sub.instr_return $ [main_sub._operation_id, main_sub._input_0, main_sub._output_0]; + instr_one $ [4, Y] in main_sub.instr_return $ [main_sub._operation_id, main_sub._output_0]; + instr_nothing $ [3] in main_sub.instr_return $ [main_sub._operation_id]; pol constant _linker_first_step = [1] + [0]*; _linker_first_step * (_operation_id - 2) = 0; namespace main_sub(16); @@ -440,7 +461,7 @@ namespace main_sub(16); pol constant p_instr_return = [0, 0, 1, 1, 1, 0] + [0]*; pol constant p_read__output_0__input_0 = [0, 0, 1, 0, 0, 0] + [0]*; pol constant p_read__output_0_pc = [0]*; - { pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return, _output_0_const, _output_0_read_free, read__output_0_pc, read__output_0__input_0 } in { p_line, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p__output_0_const, p__output_0_read_free, p_read__output_0_pc, p_read__output_0__input_0 }; + [pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return, _output_0_const, _output_0_read_free, read__output_0_pc, read__output_0__input_0] in [p_line, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p__output_0_const, p__output_0_read_free, p_read__output_0_pc, p_read__output_0__input_0]; "#; let file_name = format!( "{}/../test_data/asm/different_signatures.asm", @@ -518,7 +539,7 @@ namespace main_sub(16); pol constant p_read_X_pc = [0]*; pol constant p_reg_write_X_A = [0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0] + [0]*; pol constant p_reg_write_X_CNT = [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; - { pc, reg_write_X_A, reg_write_X_CNT, instr_jmpz, instr_jmpz_param_l, instr_jmp, instr_jmp_param_l, instr_dec_CNT, instr_assert_zero, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_CNT, read_X_pc } in { p_line, p_reg_write_X_A, p_reg_write_X_CNT, p_instr_jmpz, p_instr_jmpz_param_l, p_instr_jmp, p_instr_jmp_param_l, p_instr_dec_CNT, p_instr_assert_zero, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_CNT, p_read_X_pc }; + [pc, reg_write_X_A, reg_write_X_CNT, instr_jmpz, instr_jmpz_param_l, instr_jmp, instr_jmp_param_l, instr_dec_CNT, instr_assert_zero, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_CNT, read_X_pc] in [p_line, p_reg_write_X_A, p_reg_write_X_CNT, p_instr_jmpz, p_instr_jmpz_param_l, p_instr_jmp, p_instr_jmp_param_l, p_instr_dec_CNT, p_instr_assert_zero, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_CNT, p_read_X_pc]; pol constant _linker_first_step = [1] + [0]*; _linker_first_step * (_operation_id - 2) = 0; "#; @@ -579,7 +600,7 @@ machine Machine { pol constant p_instr_inc_fp = [0, 0, 1, 0, 0] + [0]*; pol constant p_instr_inc_fp_param_amount = [0, 0, 7, 0, 0] + [0]*; pol constant p_instr_return = [0]*; - { pc, instr_inc_fp, instr_inc_fp_param_amount, instr_adjust_fp, instr_adjust_fp_param_amount, instr_adjust_fp_param_t, instr__jump_to_operation, instr__reset, instr__loop, instr_return } in { p_line, p_instr_inc_fp, p_instr_inc_fp_param_amount, p_instr_adjust_fp, p_instr_adjust_fp_param_amount, p_instr_adjust_fp_param_t, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return }; + [pc, instr_inc_fp, instr_inc_fp_param_amount, instr_adjust_fp, instr_adjust_fp_param_amount, instr_adjust_fp_param_t, instr__jump_to_operation, instr__reset, instr__loop, instr_return] in [p_line, p_instr_inc_fp, p_instr_inc_fp_param_amount, p_instr_adjust_fp, p_instr_adjust_fp_param_amount, p_instr_adjust_fp_param_t, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return]; pol constant _linker_first_step = [1] + [0]*; _linker_first_step * (_operation_id - 2) = 0; "#; @@ -671,8 +692,8 @@ machine Main { pol constant p_read_X_A = [0]*; pol constant p_read_X_pc = [0]*; pol constant p_reg_write_X_A = [0]*; - { pc, reg_write_X_A, instr_add5_into_A, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_pc } in { p_line, p_reg_write_X_A, p_instr_add5_into_A, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_pc }; - instr_add5_into_A { 0, X, A' } in main_vm.latch { main_vm.operation_id, main_vm.x, main_vm.y }; + [pc, reg_write_X_A, instr_add5_into_A, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_pc] in [p_line, p_reg_write_X_A, p_instr_add5_into_A, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_pc]; + instr_add5_into_A $ [0, X, A'] in main_vm.latch $ [main_vm.operation_id, main_vm.x, main_vm.y]; pol constant _linker_first_step = [1] + [0]*; _linker_first_step * (_operation_id - 2) = 0; namespace main_vm(1024); @@ -769,9 +790,9 @@ namespace main_vm(1024); pol constant p_reg_write_Y_B = [0]*; pol constant p_reg_write_Z_A = [0, 0, 1, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0] + [0]*; pol constant p_reg_write_Z_B = [0]*; - { pc, reg_write_X_A, reg_write_Y_A, reg_write_Z_A, reg_write_X_B, reg_write_Y_B, reg_write_Z_B, instr_or, instr_or_into_B, instr_assert_eq, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_B, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_B, read_Y_pc, Z_const, Z_read_free, read_Z_A, read_Z_B, read_Z_pc } in { p_line, p_reg_write_X_A, p_reg_write_Y_A, p_reg_write_Z_A, p_reg_write_X_B, p_reg_write_Y_B, p_reg_write_Z_B, p_instr_or, p_instr_or_into_B, p_instr_assert_eq, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_B, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_A, p_read_Y_B, p_read_Y_pc, p_Z_const, p_Z_read_free, p_read_Z_A, p_read_Z_B, p_read_Z_pc }; - instr_or { 0, X, Y, Z } is main_bin.latch * main_bin.sel[0] { main_bin.operation_id, main_bin.A, main_bin.B, main_bin.C }; - instr_or_into_B { 0, X, Y, B' } is main_bin.latch * main_bin.sel[1] { main_bin.operation_id, main_bin.A, main_bin.B, main_bin.C }; + [pc, reg_write_X_A, reg_write_Y_A, reg_write_Z_A, reg_write_X_B, reg_write_Y_B, reg_write_Z_B, instr_or, instr_or_into_B, instr_assert_eq, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_B, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_B, read_Y_pc, Z_const, Z_read_free, read_Z_A, read_Z_B, read_Z_pc] in [p_line, p_reg_write_X_A, p_reg_write_Y_A, p_reg_write_Z_A, p_reg_write_X_B, p_reg_write_Y_B, p_reg_write_Z_B, p_instr_or, p_instr_or_into_B, p_instr_assert_eq, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_B, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_A, p_read_Y_B, p_read_Y_pc, p_Z_const, p_Z_read_free, p_read_Z_A, p_read_Z_B, p_read_Z_pc]; + instr_or $ [0, X, Y, Z] is main_bin.latch * main_bin.sel[0] $ [main_bin.operation_id, main_bin.A, main_bin.B, main_bin.C]; + instr_or_into_B $ [0, X, Y, B'] is main_bin.latch * main_bin.sel[1] $ [main_bin.operation_id, main_bin.A, main_bin.B, main_bin.C]; pol constant _linker_first_step = [1] + [0]*; _linker_first_step * (_operation_id - 2) = 0; namespace main_bin(65536); @@ -792,7 +813,7 @@ namespace main_bin(65536); A' = A * (1 - latch) + A_byte * FACTOR; B' = B * (1 - latch) + B_byte * FACTOR; C' = C * (1 - latch) + C_byte * FACTOR; - { A_byte, B_byte, C_byte } in { P_A, P_B, P_C }; + [A_byte, B_byte, C_byte] in [P_A, P_B, P_C]; pol commit sel[2]; std::array::map(sel, std::utils::force_bool); "#; diff --git a/parser/src/lib.rs b/parser/src/lib.rs index d06a00ecc..b3f92aded 100644 --- a/parser/src/lib.rs +++ b/parser/src/lib.rs @@ -139,8 +139,8 @@ pub fn unescape_string(s: &str) -> String { mod test { use super::*; use powdr_ast::parsed::{ - asm::ASMProgram, build::direct_reference, PILFile, PilStatement, PolynomialName, - SelectedExpressions, + asm::ASMProgram, build::direct_reference, ArrayLiteral, PILFile, PilStatement, + PolynomialName, SelectedExpressions, }; use powdr_parser_util::UnwrapErrToStderr; use pretty_assertions::assert_eq; @@ -211,9 +211,11 @@ mod test { #[test] fn simple_plookup() { - let input = "f in g;"; + let input = "[f] in [g];"; let ctx = ParserContext::new(None, input); - let parsed = powdr::PILFileParser::new().parse(&ctx, "f in g;").unwrap(); + let parsed = powdr::PILFileParser::new() + .parse(&ctx, "[f] in [g];") + .unwrap(); assert_eq!( parsed, PILFile(vec![PilStatement::PlookupIdentity( @@ -221,15 +223,25 @@ mod test { file_name: None, file_contents: Some(input.into()), start: 0, - end: 6, + end: 10, }, SelectedExpressions { selector: None, - expressions: vec![direct_reference("f")] + expressions: Box::new( + ArrayLiteral { + items: vec![direct_reference("f")] + } + .into() + ) }, SelectedExpressions { selector: None, - expressions: vec![direct_reference("g")] + expressions: Box::new( + ArrayLiteral { + items: vec![direct_reference("g")] + } + .into() + ) } )]) ); @@ -407,8 +419,8 @@ namespace Fibonacci(%N); pol constant ISLAST(i) { one_hot(i, %last_row) }; pol commit arr[8]; pol commit x, y; - { x + 2, y' } in { ISLAST, 7 }; - y { x + 2, y' } is ISLAST { ISLAST, 7 }; + [x + 2, y'] in [ISLAST, 7]; + y $ [x + 2, y'] is ISLAST $ [ISLAST, 7]; (x - 2) * y = 8; public out = y(%last_row);"#; let printed = format!("{}", parse(Some("input"), input).unwrap()); diff --git a/parser/src/powdr.lalrpop b/parser/src/powdr.lalrpop index 29b19aaeb..f6dfbfa70 100644 --- a/parser/src/powdr.lalrpop +++ b/parser/src/powdr.lalrpop @@ -159,7 +159,7 @@ PolynomialConstantDefinition: PilStatement = { } FunctionDefinition: FunctionDefinition = { - "(" ")" => FunctionDefinition::Expression(Expression::LambdaExpression(ctx.source_ref(start, end), LambdaExpression{kind: FunctionKind::Pure, params, body})), + "(" ")" => FunctionDefinition::Expression(Expression::LambdaExpression(ctx.source_ref(start, end), LambdaExpression{kind: FunctionKind::Pure, params, body})), "=" => FunctionDefinition::Array(array), } @@ -209,8 +209,7 @@ PlookupIdentity: PilStatement = { } SelectedExpressions: SelectedExpressions = { - "{" "}" => SelectedExpressions{<>}, - Expression => SelectedExpressions{selector: None, expressions: vec![<>]}, + "$")?> => SelectedExpressions{selector, expressions: Box::new(expr)}, } PermutationIdentityStatement: PilStatement = { @@ -226,7 +225,7 @@ ConnectIdentityStatement: PilStatement = { } ConnectIdentity: PilStatement = { - "{" "}" "connect" "{" "}" => PilStatement::ConnectIdentity(ctx.source_ref(start, end), list1, list2) + "[" "]" "connect" "[" "]" => PilStatement::ConnectIdentity(ctx.source_ref(start, end), list1, list2) } ExpressionStatement: PilStatement = { @@ -621,19 +620,15 @@ MatchArm: MatchArm = { IfExpression: Box = { "if" - + "else" - + => ctx.to_expr_with_source_ref(IfExpression{condition, body, else_body}, start, end), } -BlockExpression: Box = { - "{" "}" => ctx.to_expr_with_source_ref(BlockExpression{statements, expr}, start, end), -} -BracedExpression: Box = { - "{" "}" => ctx.to_expr_with_source_ref(BlockExpression{statements, expr}, start, end), - "{" "}" => ctx.to_expr_with_source_ref(BlockExpression{statements: vec![], expr}, start, end), +BlockExpression: Box = { + "{" "}" => ctx.to_expr_with_source_ref(BlockExpression{statements, expr}, start, end), } StatementInsideBlock: StatementInsideBlock = { diff --git a/pil-analyzer/src/condenser.rs b/pil-analyzer/src/condenser.rs index c2b7404f8..fecb7f50d 100644 --- a/pil-analyzer/src/condenser.rs +++ b/pil-analyzer/src/condenser.rs @@ -10,15 +10,15 @@ use std::{ use powdr_ast::{ analyzed::{ - AlgebraicExpression, AlgebraicReference, Analyzed, Expression, FunctionValueDefinition, - Identity, IdentityKind, PolynomialType, PublicDeclaration, StatementIdentifier, Symbol, - SymbolKind, + self, AlgebraicExpression, AlgebraicReference, Analyzed, Expression, + FunctionValueDefinition, Identity, IdentityKind, PolynomialType, PublicDeclaration, + SelectedExpressions, StatementIdentifier, Symbol, SymbolKind, }, parsed::{ + self, asm::{AbsoluteSymbolPath, SymbolPath}, display::format_type_scheme_around_name, types::{ArrayType, Type}, - SelectedExpressions, }, }; use powdr_number::{DegreeType, FieldElement}; @@ -33,7 +33,7 @@ pub fn condense( degree: Option, mut definitions: HashMap)>, mut public_declarations: HashMap, - identities: &[Identity], + identities: &[Identity>], source_order: Vec, auto_added_symbols: HashSet, ) -> Analyzed { @@ -196,7 +196,7 @@ impl IdentityWithoutID { } } - pub fn into_identity(self, id: u64) -> Identity { + pub fn into_identity(self, id: u64) -> Identity> { Identity { id, kind: self.kind, @@ -234,7 +234,10 @@ impl<'a, T: FieldElement> Condenser<'a, T> { } } - pub fn condense_identity(&mut self, identity: &'a Identity) { + pub fn condense_identity( + &mut self, + identity: &'a Identity>, + ) { if identity.kind == IdentityKind::Polynomial { let expr = identity.expression_for_poly_id(); evaluator::evaluate(expr, self) @@ -280,18 +283,14 @@ impl<'a, T: FieldElement> Condenser<'a, T> { fn condense_selected_expressions( &mut self, - sel_expr: &'a SelectedExpressions, + sel_expr: &'a parsed::SelectedExpressions, ) -> SelectedExpressions> { SelectedExpressions { selector: sel_expr .selector .as_ref() .map(|expr| self.condense_to_algebraic_expression(expr)), - expressions: sel_expr - .expressions - .iter() - .map(|expr| self.condense_to_algebraic_expression(expr)) - .collect(), + expressions: self.condense_to_array_of_algebraic_expressions(&sel_expr.expressions), } } @@ -322,7 +321,7 @@ impl<'a, T: FieldElement> Condenser<'a, T> { _ => panic!("Expected expression but got {item}"), }) .collect(), - _ => panic!("Expected array of algebraic expressions, but got {result}"), + _ => panic!("Expected array of algebraic expressions but got {result}"), } } } @@ -486,11 +485,11 @@ fn to_constraint( IdentityWithoutID { kind: IdentityKind::Connect, source, - left: SelectedExpressions { + left: analyzed::SelectedExpressions { selector: None, expressions: from.into_iter().map(to_expr).collect(), }, - right: SelectedExpressions { + right: analyzed::SelectedExpressions { selector: None, expressions: to.into_iter().map(to_expr).collect(), }, diff --git a/pil-analyzer/src/evaluator.rs b/pil-analyzer/src/evaluator.rs index a2bb489d9..b2f1bb0b7 100644 --- a/pil-analyzer/src/evaluator.rs +++ b/pil-analyzer/src/evaluator.rs @@ -749,7 +749,10 @@ impl<'a, 'b, T: FieldElement, S: SymbolLookup<'a, T>> Evaluator<'a, 'b, T, S> { Expression::BlockExpression(_, BlockExpression { statements, expr }) => { self.op_stack .push(Operation::TruncateLocals(self.local_vars.len())); - self.op_stack.push(Operation::Expand(expr)); + match expr { + Some(expr) => self.op_stack.push(Operation::Expand(expr)), + None => self.value_stack.push(Value::Tuple(vec![]).into()), + } for s in statements.iter().rev() { match s { StatementInsideBlock::LetStatement(s) => { @@ -1647,4 +1650,28 @@ mod test { 7u64.into() ); } + + #[test] + fn no_stmts_in_block() { + let input = " + let f: int -> () = |i| (); + let g: int -> () = |i| { + f(1) + }; + + let h: () = g(1); + "; + + assert_eq!(parse_and_evaluate_symbol(input, "h"), "()".to_string()); + } + + #[test] + fn called_with_empty_block() { + let input = " + let f: T1 -> T2 = |_| 7; + let g: int = f({ }); + "; + + assert_eq!(parse_and_evaluate_symbol(input, "g"), "7".to_string()); + } } diff --git a/pil-analyzer/src/expression_processor.rs b/pil-analyzer/src/expression_processor.rs index 6b0774e6a..20c39f035 100644 --- a/pil-analyzer/src/expression_processor.rs +++ b/pil-analyzer/src/expression_processor.rs @@ -1,9 +1,4 @@ use core::panic; -use std::{ - collections::{HashMap, HashSet}, - str::FromStr, -}; - use powdr_ast::{ analyzed::{Expression, PolynomialReference, Reference, RepeatedArray}, parsed::{ @@ -15,6 +10,10 @@ use powdr_ast::{ }; use powdr_number::DegreeType; use powdr_parser_util::SourceRef; +use std::{ + collections::{HashMap, HashSet}, + str::FromStr, +}; use crate::{type_processor::TypeProcessor, AnalysisDriver}; @@ -44,7 +43,7 @@ impl<'a, D: AnalysisDriver> ExpressionProcessor<'a, D> { ) -> SelectedExpressions { SelectedExpressions { selector: expr.selector.map(|e| self.process_expression(e)), - expressions: self.process_expressions(expr.expressions), + expressions: Box::new(self.process_expression(*expr.expressions)), } } @@ -84,6 +83,23 @@ impl<'a, D: AnalysisDriver> ExpressionProcessor<'a, D> { .collect() } + pub fn process_vec_into_selected_expression( + &mut self, + exprs: Vec, + ) -> SelectedExpressions { + let exprs = Expression::ArrayLiteral( + SourceRef::unknown(), + ArrayLiteral { + items: self.process_expressions(exprs), + }, + ); + + SelectedExpressions { + selector: None, + expressions: Box::new(exprs), + } + } + pub fn process_expression(&mut self, expr: parsed::Expression) -> Expression { use parsed::Expression as PExpression; match expr { @@ -179,7 +195,7 @@ impl<'a, D: AnalysisDriver> ExpressionProcessor<'a, D> { }, ), PExpression::BlockExpression(src, BlockExpression { statements, expr }) => { - self.process_block_expression(statements, *expr, src) + self.process_block_expression(statements, expr, src) } PExpression::FreeInput(_, _) => panic!(), } @@ -292,7 +308,7 @@ impl<'a, D: AnalysisDriver> ExpressionProcessor<'a, D> { fn process_block_expression( &mut self, statements: Vec, - expr: ::powdr_ast::parsed::Expression, + expr: Option>, src: SourceRef, ) -> Expression { let vars = self.save_local_variables(); @@ -317,13 +333,14 @@ impl<'a, D: AnalysisDriver> ExpressionProcessor<'a, D> { }) .collect::>(); - let processed_expr = self.process_expression(expr); + let processed_expr = expr.map(|expr| Box::new(self.process_expression(*expr))); + self.reset_local_variables(vars); Expression::BlockExpression( src, BlockExpression { statements: processed_statements, - expr: Box::new(processed_expr), + expr: processed_expr, }, ) } diff --git a/pil-analyzer/src/pil_analyzer.rs b/pil-analyzer/src/pil_analyzer.rs index 2d06223dc..03fdda574 100644 --- a/pil-analyzer/src/pil_analyzer.rs +++ b/pil-analyzer/src/pil_analyzer.rs @@ -9,10 +9,11 @@ use itertools::Itertools; use powdr_ast::parsed::asm::{ parse_absolute_path, AbsoluteSymbolPath, ModuleStatement, SymbolPath, }; -use powdr_ast::parsed::types::Type; +use powdr_ast::parsed::types::{ArrayType, Type}; use powdr_ast::parsed::visitor::Children; use powdr_ast::parsed::{ - self, FunctionKind, LambdaExpression, PILFile, PilStatement, SymbolCategory, + self, FunctionKind, LambdaExpression, PILFile, PilStatement, SelectedExpressions, + SymbolCategory, }; use powdr_number::{DegreeType, FieldElement, GoldilocksField}; @@ -63,7 +64,7 @@ struct PILAnalyzer { /// Map of definitions, gradually being built up here. definitions: HashMap)>, public_declarations: HashMap, - identities: Vec>, + identities: Vec>>, /// The order in which definitions and identities /// appear in the source. source_order: Vec, @@ -287,9 +288,15 @@ impl PILAnalyzer { if let Some(selector) = &mut part.selector { expressions.push((selector, Type::Expr.into())) } - for e in &mut part.expressions { - expressions.push((e, Type::Expr.into())) - } + + expressions.push(( + part.expressions.as_mut(), + Type::Array(ArrayType { + base: Box::new(Type::Expr), + length: None, + }) + .into(), + )) } } } diff --git a/pil-analyzer/src/statement_processor.rs b/pil-analyzer/src/statement_processor.rs index 7e3dcd3c4..24d61ff90 100644 --- a/pil-analyzer/src/statement_processor.rs +++ b/pil-analyzer/src/statement_processor.rs @@ -8,7 +8,7 @@ use powdr_ast::analyzed::TypedExpression; use powdr_ast::parsed::{ self, types::{ArrayType, Type, TypeScheme}, - EnumDeclaration, EnumVariant, FunctionDefinition, PilStatement, PolynomialName, + ArrayLiteral, EnumDeclaration, EnumVariant, FunctionDefinition, PilStatement, PolynomialName, SelectedExpressions, }; use powdr_ast::parsed::{FunctionKind, LambdaExpression}; @@ -28,7 +28,7 @@ use crate::expression_processor::ExpressionProcessor; pub enum PILItem { Definition(Symbol, Option), PublicDeclaration(PublicDeclaration), - Identity(Identity), + Identity(Identity>), } pub struct Counters { @@ -317,7 +317,7 @@ where self.expression_processor(&Default::default()) .process_expression(expression), ), - expressions: vec![], + expressions: Box::new(ArrayLiteral { items: vec![] }.into()), }, SelectedExpressions::default(), ), @@ -340,18 +340,10 @@ where PilStatement::ConnectIdentity(source, left, right) => ( source, IdentityKind::Connect, - SelectedExpressions { - selector: None, - expressions: self - .expression_processor(&Default::default()) - .process_expressions(left), - }, - SelectedExpressions { - selector: None, - expressions: self - .expression_processor(&Default::default()) - .process_expressions(right), - }, + self.expression_processor(&Default::default()) + .process_vec_into_selected_expression(left), + self.expression_processor(&Default::default()) + .process_vec_into_selected_expression(right), ), // TODO at some point, these should all be caught by the type checker. _ => { diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index d0d90691e..25ce536ff 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -663,7 +663,11 @@ impl<'a> TypeChecker<'a> { } } } - let result = self.infer_type_of_expression(expr); + let result = match expr { + Some(expr) => self.infer_type_of_expression(expr), + None => Ok(Type::empty_tuple()), + }; + self.local_var_types.truncate(original_var_count); result? } diff --git a/pil-analyzer/tests/condenser.rs b/pil-analyzer/tests/condenser.rs index 24a9c2960..ba087198e 100644 --- a/pil-analyzer/tests/condenser.rs +++ b/pil-analyzer/tests/condenser.rs @@ -14,7 +14,7 @@ fn new_witness_column() { let y; let z = new_wit(); z = y; - z { z } in { even }; + z $ [z] in [even]; let t = new_wit_arr(); t[0] = t[1]; "#; @@ -33,7 +33,7 @@ fn new_witness_column() { let z: expr = N.new_wit(); col witness x_1; N.x_1 = N.y; - N.x_1 { N.x_1 } in { N.even }; + N.x_1 $ [N.x_1] in [N.even]; let t: expr[] = N.new_wit_arr(); col witness x_2; N.x_2 = N.x_2; @@ -168,9 +168,9 @@ pub fn constructed_constraints() { col witness y; col witness z; Main.x = Main.y; - 1 { Main.x, 3 } in { Main.y, Main.z }; - { Main.x, 3 } is Main.x { Main.y, Main.z }; - { Main.x, Main.y } connect { Main.z, 3 }; + 1 $ [Main.x, 3] in [Main.y, Main.z]; + [Main.x, 3] is Main.x $ [Main.y, Main.z]; + [Main.x, Main.y] connect [Main.z, 3]; "#; assert_eq!(formatted, expected); } diff --git a/pil-analyzer/tests/parse_display.rs b/pil-analyzer/tests/parse_display.rs index fe96d7d3b..e16176e21 100644 --- a/pil-analyzer/tests/parse_display.rs +++ b/pil-analyzer/tests/parse_display.rs @@ -61,7 +61,7 @@ namespace T(65536); col fixed p_read_X_pc = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; col fixed p_reg_write_X_A = [0, 0, 0, 1, 0, 0, 0, 1, 0] + [0]*; col fixed p_reg_write_X_CNT = [1, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; - { T.pc, T.reg_write_X_A, T.reg_write_X_CNT } in 1 - T.first_step { T.line, T.p_reg_write_X_A, T.p_reg_write_X_CNT }; + [T.pc, T.reg_write_X_A, T.reg_write_X_CNT] in 1 - T.first_step $ [T.line, T.p_reg_write_X_A, T.p_reg_write_X_CNT]; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(input, formatted); @@ -346,11 +346,11 @@ fn expression_but_expected_constraint() { } #[test] -#[should_panic = "Expected type expr but got type std::prelude::Constr."] +#[should_panic = "Expected type expr[] but got type std::prelude::Constr[]."] fn constraint_but_expected_expression() { let input = r#"namespace N(16); col witness y; - { (N.y - 2) = 0 } in { N.y }; + [ (N.y - 2) = 0 ] in [ N.y ]; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, input); diff --git a/pil-analyzer/tests/types.rs b/pil-analyzer/tests/types.rs index b9608469f..772af76d9 100644 --- a/pil-analyzer/tests/types.rs +++ b/pil-analyzer/tests/types.rs @@ -197,7 +197,7 @@ fn constraints() { let input = " let a; let BYTE: col = |i| std::convert::fe(i & 0xff); - { a + 1 } in {BYTE}; + [ a + 1 ] in [BYTE]; namespace std::convert(8); let fe = 18; "; @@ -516,3 +516,47 @@ fn enum_too_many_fields() { "; type_check(input, &[]); } + +#[test] +fn empty_function() { + let input = " + let f: int -> () = |i| { }; + let g: int -> () = |i| { + f(i); + }; + + let h: () = g(4); + "; + type_check(input, &[]); +} + +#[test] +fn empty_match() { + let input = " + let h: int -> int = |i| i; + let f: int -> () = |i| match i { + 5 => { + let _ = h(4); + }, + _ => { } + }; + + let g: () = f(4); + let k: () = f(5); + "; + type_check(input, &[]); +} + +#[test] +fn empty_conditional() { + let input = " + let h: int -> int = |i| i; + let f: int -> () = |i| if i == 5 { + let _ = h(4); + } else { }; + + let g: () = f(4); + let k: () = f(5); + "; + type_check(input, &[]); +} diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index 393f78874..c8acc5feb 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -578,9 +578,9 @@ mod test { col witness W; col witness Z; col witness A; - (1 - A) { X, Y, A } in { zero, one, cnt }; - { Y, W, Z, A } in (1 + A) { cnt, zero, two, one }; - { W, Z } in (1 + A) { zero, one }; + (1 - A) $ [ X, Y, A ] in [ zero, one, cnt ]; + [ Y, W, Z, A ] in (1 + A) $ [ cnt, zero, two, one ]; + [ W, Z ] in (1 + A) $ [ zero, one ]; "#; let expectation = r#"namespace N(65536); col fixed cnt(i) { i }; @@ -588,8 +588,8 @@ mod test { col witness Y; col witness Z; col witness A; - 1 - N.A { N.A } in { N.cnt }; - { N.Y } in 1 + N.A { N.cnt }; + 1 - N.A $ [N.A] in [N.cnt]; + [N.Y] in 1 + N.A $ [N.cnt]; (1 - N.A) * N.X = 0; (1 - N.A) * N.Y = 1; N.Z = (1 + N.A) * 2; @@ -649,20 +649,20 @@ namespace N(65536); x * (x - 1) = 0; x * (x - 1) = 0; - { x } in { cnt }; - { x } in { cnt }; - { x } in { cnt }; + [ x ] in [ cnt ]; + [ x ] in [ cnt ]; + [ x ] in [ cnt ]; - { x + 1 } in { cnt }; - { x } in { cnt + 1 }; + [ x + 1 ] in [ cnt ]; + [ x ] in [ cnt + 1 ]; "#; let expectation = r#"namespace N(65536); col witness x; col fixed cnt(i) { i }; N.x * (N.x - 1) = 0; - { N.x } in { N.cnt }; - { N.x + 1 } in { N.cnt }; - { N.x } in { N.cnt + 1 }; + [N.x] in [N.cnt]; + [N.x + 1] in [N.cnt]; + [N.x] in [N.cnt + 1]; "#; let optimized = optimize(analyze_string::(input)).to_string(); assert_eq!(optimized, expectation); @@ -681,14 +681,14 @@ namespace N(65536); let a: int -> int = |i| b(i + 1); let b: int -> int = |j| 8; // identity - { x } in { cnt }; + [ x ] in [ cnt ]; "#; let expectation = r#"namespace N(65536); col witness x; col fixed cnt(i) { N.inc(i) }; let inc: int -> int = (|x| x + 1); - { N.x } in { N.cnt }; + [N.x] in [N.cnt]; "#; let optimized = optimize(analyze_string::(input)).to_string(); assert_eq!(optimized, expectation); diff --git a/plonky3/src/prover/mod.rs b/plonky3/src/prover/mod.rs index 1e29c72c9..19f053b26 100644 --- a/plonky3/src/prover/mod.rs +++ b/plonky3/src/prover/mod.rs @@ -176,7 +176,7 @@ mod tests { #[test] #[should_panic = "not implemented"] fn lookup() { - let content = "namespace Global(8); pol fixed z = [0, 1]*; pol witness a; a in z;"; + let content = "namespace Global(8); pol fixed z = [0, 1]*; pol witness a; [a] in [z];"; run_test_goldilocks(content); } } diff --git a/riscv/src/code_gen.rs b/riscv/src/code_gen.rs index 622fb85b7..02cd72c49 100644 --- a/riscv/src/code_gen.rs +++ b/riscv/src/code_gen.rs @@ -376,10 +376,10 @@ fn preamble(runtime: &Runtime, with_bootloader: bool) -> String 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 }; + [ 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; @@ -391,7 +391,7 @@ fn preamble(runtime: &Runtime, with_bootloader: bool) -> String } col fixed seven_bit(i) { i & 0x7f }; col witness Y_7bit; - { Y_7bit } in { seven_bit }; + [ 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 { @@ -422,19 +422,19 @@ fn preamble(runtime: &Runtime, with_bootloader: bool) -> String 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 }; + [ 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 }; + [ 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 { @@ -523,9 +523,9 @@ fn memory(with_bootloader: bool) -> String { /// wraps the address to 32 bits and rounds it down to the next multiple of 4. /// Returns the loaded word and the remainder of the division by 4. instr mload Y -> X, Z link ~> X = memory.mload(X_b4 * 0x1000000 + X_b3 * 0x10000 + X_b2 * 0x100 + X_b1 * 4, STEP) { - { Z } in { up_to_three }, + [ Z ] in [ up_to_three ], Y = wrap_bit * 2**32 + X_b4 * 0x1000000 + X_b3 * 0x10000 + X_b2 * 0x100 + X_b1 * 4 + Z, - { X_b1 } in { six_bits } + [ X_b1 ] in [ six_bits ] } /// Stores Z at address Y % 2**32. Y can be between 0 and 2**33. diff --git a/std/machines/arith.asm b/std/machines/arith.asm index 6c47545e9..a5c64c976 100644 --- a/std/machines/arith.asm +++ b/std/machines/arith.asm @@ -309,12 +309,12 @@ machine Arith with * *****/ - sum(16, |i| x1[i] * CLK32[i]) + sum(16, |i| y1[i] * CLK32[16 + i]) in BYTE2; - sum(16, |i| x2[i] * CLK32[i]) + sum(16, |i| y2[i] * CLK32[16 + i]) in BYTE2; - sum(16, |i| x3[i] * CLK32[i]) + sum(16, |i| y3[i] * CLK32[16 + i]) in BYTE2; + [sum(16, |i| x1[i] * CLK32[i]) + sum(16, |i| y1[i] * CLK32[16 + i])] in [BYTE2]; + [sum(16, |i| x2[i] * CLK32[i]) + sum(16, |i| y2[i] * CLK32[16 + i])] in [BYTE2]; + [sum(16, |i| x3[i] * CLK32[i]) + sum(16, |i| y3[i] * CLK32[16 + i])] in [BYTE2]; // Note that for q0-q2, we only range-constrain the first 15 limbs here - sum(16, |i| s[i] * CLK32[i]) + sum(15, |i| q0[i] * CLK32[16 + i]) in BYTE2; - sum(15, |i| q1[i] * CLK32[i]) + sum(15, |i| q2[i] * CLK32[16 + i]) in BYTE2; + [sum(16, |i| s[i] * CLK32[i]) + sum(15, |i| q0[i] * CLK32[16 + i])] in [BYTE2]; + [sum(15, |i| q1[i] * CLK32[i]) + sum(15, |i| q2[i] * CLK32[16 + i])] in [BYTE2]; // The most significant limbs of q0-q2 are constrained to be 32 bits // In Polygon's version they are 19 bits, but that requires increasing the minimum degree @@ -324,7 +324,7 @@ machine Arith with // limbs of the prime, so the result is within 48 bits, still far from overflowing the // Goldilocks field. pol witness q0_15_high, q0_15_low, q1_15_high, q1_15_low, q2_15_high, q2_15_low; - q0_15_high * CLK32[0] + q0_15_low * CLK32[1] + q1_15_high * CLK32[2] + q1_15_low * CLK32[3] + q2_15_high * CLK32[4] + q2_15_low * CLK32[5] in BYTE2; + [q0_15_high * CLK32[0] + q0_15_low * CLK32[1] + q1_15_high * CLK32[2] + q1_15_low * CLK32[3] + q2_15_high * CLK32[4] + q2_15_low * CLK32[5]] in [BYTE2]; fixed_inside_32_block(q0_15_high); fixed_inside_32_block(q0_15_low); @@ -442,12 +442,12 @@ machine Arith with // while still preventing overflows: The 32-bit carry gets added to 32 48-Bit values, which can't overflow // the Goldilocks field. pol witness carry_low[3], carry_high[3]; - { carry_low[0] } in { BYTE2 }; - { carry_low[1] } in { BYTE2 }; - { carry_low[2] } in { BYTE2 }; - { carry_high[0] } in { BYTE2 }; - { carry_high[1] } in { BYTE2 }; - { carry_high[2] } in { BYTE2 }; + [ carry_low[0] ] in [ BYTE2 ]; + [ carry_low[1] ] in [ BYTE2 ]; + [ carry_low[2] ] in [ BYTE2 ]; + [ carry_high[0] ] in [ BYTE2 ]; + [ carry_high[1] ] in [ BYTE2 ]; + [ carry_high[2] ] in [ BYTE2 ]; // Carries can be any integer in the range [-2**31, 2**31 - 1) let carry: expr[3] = array::new(3, |i| carry_high[i] * 2**16 + carry_low[i] - 2 ** 31); diff --git a/std/machines/binary.asm b/std/machines/binary.asm index bbbbb3dea..be1fe61d2 100644 --- a/std/machines/binary.asm +++ b/std/machines/binary.asm @@ -51,5 +51,5 @@ machine Binary with 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}; + [operation_id', A_byte, B_byte, C_byte] in [P_operation, P_A, P_B, P_C]; } diff --git a/std/machines/memory.asm b/std/machines/memory.asm index 385105326..6e0599939 100644 --- a/std/machines/memory.asm +++ b/std/machines/memory.asm @@ -53,8 +53,8 @@ machine Memory with col fixed STEP(i) { i }; col fixed BIT16(i) { i & 0xffff }; - {m_diff_lower} in {BIT16}; - {m_diff_upper} in {BIT16}; + [m_diff_lower] in [BIT16]; + [m_diff_upper] in [BIT16]; std::utils::force_bool(m_change); diff --git a/std/machines/memory_with_bootloader_write.asm b/std/machines/memory_with_bootloader_write.asm index 01f8e1ada..40289aa0d 100644 --- a/std/machines/memory_with_bootloader_write.asm +++ b/std/machines/memory_with_bootloader_write.asm @@ -63,8 +63,8 @@ machine MemoryWithBootloaderWrite with col fixed STEP(i) { i }; col fixed BIT16(i) { i & 0xffff }; - {m_diff_lower} in {BIT16}; - {m_diff_upper} in {BIT16}; + [m_diff_lower] in [BIT16]; + [m_diff_upper] in [BIT16]; std::utils::force_bool(m_change); diff --git a/std/machines/shift.asm b/std/machines/shift.asm index dfa03ae0f..4c347bdfb 100644 --- a/std/machines/shift.asm +++ b/std/machines/shift.asm @@ -50,5 +50,5 @@ machine Shift with 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}; + [operation_id', A_byte, B', FACTOR_ROW, C_part] in [P_operation, P_A, P_B, P_ROW, P_C]; } diff --git a/std/machines/split/split_bn254.asm b/std/machines/split/split_bn254.asm index 589771e95..e439ca76e 100644 --- a/std/machines/split/split_bn254.asm +++ b/std/machines/split/split_bn254.asm @@ -78,7 +78,7 @@ machine SplitBN254 with // 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 }; + [ 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. diff --git a/std/machines/split/split_gl.asm b/std/machines/split/split_gl.asm index 6b60d5b19..dce42c09a 100644 --- a/std/machines/split/split_gl.asm +++ b/std/machines/split/split_gl.asm @@ -74,7 +74,7 @@ machine SplitGL with // 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 }; + [ 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. diff --git a/test_data/asm/bit_access.asm b/test_data/asm/bit_access.asm index 18a216569..763811bd4 100644 --- a/test_data/asm/bit_access.asm +++ b/test_data/asm/bit_access.asm @@ -20,10 +20,10 @@ machine BitAccess { col witness XB2; col witness XB3; col witness XB4; - { XB1 } in { BYTE }; - { XB2 } in { BYTE }; - { XB3 } in { BYTE }; - { XB4 } in { BYTE }; + [ XB1 ] in [ BYTE ]; + [ XB2 ] in [ BYTE ]; + [ XB3 ] in [ BYTE ]; + [ XB4 ] in [ BYTE ]; col commit wrap_bit; wrap_bit * (1 - wrap_bit) = 0; diff --git a/test_data/asm/block_machine_cache_miss.asm b/test_data/asm/block_machine_cache_miss.asm index ae166538b..cf25bcc1d 100644 --- a/test_data/asm/block_machine_cache_miss.asm +++ b/test_data/asm/block_machine_cache_miss.asm @@ -23,8 +23,8 @@ machine Arith with // - 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}; + (1 - operation_id) $ [x, y] in [X, DOUBLE]; + operation_id $ [x, y] in [X, SQUARE]; } machine Main with degree: 8 { diff --git a/test_data/asm/connect_no_witgen.asm b/test_data/asm/connect_no_witgen.asm index 0cd96f447..fde85489a 100644 --- a/test_data/asm/connect_no_witgen.asm +++ b/test_data/asm/connect_no_witgen.asm @@ -21,5 +21,5 @@ machine Empty { std::check::assert(omega ** 512 != 1, || ""); std::check::assert(omega ** 1024 == 1, || ""); - { w } connect { r }; + [ w ] connect [ r ]; } \ No newline at end of file diff --git a/test_data/asm/functional_instructions.asm b/test_data/asm/functional_instructions.asm index 137ebdccb..3678b6b75 100644 --- a/test_data/asm/functional_instructions.asm +++ b/test_data/asm/functional_instructions.asm @@ -21,10 +21,10 @@ machine FunctionalInstructions { col commit XB2; col commit XB3; col commit XB4; - { XB1 } in { BYTES }; - { XB2 } in { BYTES }; - { XB3 } in { BYTES }; - { XB4 } in { BYTES }; + [ XB1 ] in [ BYTES ]; + [ XB2 ] in [ BYTES ]; + [ XB3 ] in [ BYTES ]; + [ XB4 ] in [ BYTES ]; col commit wrap_bit; wrap_bit * (1 - wrap_bit) = 0; diff --git a/test_data/asm/mem_read_write.asm b/test_data/asm/mem_read_write.asm index 4207a709d..b86bce817 100644 --- a/test_data/asm/mem_read_write.asm +++ b/test_data/asm/mem_read_write.asm @@ -44,7 +44,7 @@ machine MemReadWrite { // 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; + (1 - LAST) $ [m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step)] in [POSITIVE]; // m_change has to be 1 in the last row, so that a first read on row zero is constrained to return 0 (1 - m_change) * LAST = 0; @@ -60,8 +60,8 @@ machine MemReadWrite { (1 - m_is_write') * m_change * m_value' = 0; instr assert_zero X { XIsZero = 1 } - instr mload -> X { { 0, ADDR, STEP, X } is m_selector1 { m_is_write, m_addr, m_step, m_value } } - instr mstore X { { 1, ADDR, STEP, X } is m_selector2 { m_is_write, m_addr, m_step, m_value } } + instr mload -> X { [0, ADDR, STEP, X] is m_selector1 $ [m_is_write, m_addr, m_step, m_value] } + instr mstore X { [1, ADDR, STEP, X] is m_selector2 $ [m_is_write, m_addr, m_step, m_value] } function main { ADDR <=X= 4; diff --git a/test_data/asm/mem_read_write_large_diffs.asm b/test_data/asm/mem_read_write_large_diffs.asm index 6c04751da..2809f99c5 100644 --- a/test_data/asm/mem_read_write_large_diffs.asm +++ b/test_data/asm/mem_read_write_large_diffs.asm @@ -42,8 +42,8 @@ machine MemReadWrite { col fixed STEP(i) { i }; col fixed BYTE(i) { i & 0xff }; - {m_diff_lower} in {BYTE}; - {m_diff_upper} in {BYTE}; + [m_diff_lower] in [BYTE]; + [m_diff_upper] in [BYTE]; m_change * (1 - m_change) = 0; @@ -71,8 +71,8 @@ machine MemReadWrite { (1 - m_is_write') * m_change * m_value' = 0; instr assert_zero X { XIsZero = 1 } - instr mload -> X { { 0, ADDR, STEP, X } is m_selector1 { m_is_write, m_addr, m_step, m_value } } - instr mstore X { { 1, ADDR, STEP, X } is m_selector2 { m_is_write, m_addr, m_step, m_value } } + instr mload -> X { [ 0, ADDR, STEP, X ] is m_selector1 $ [ m_is_write, m_addr, m_step, m_value ] } + instr mstore X { [ 1, ADDR, STEP, X ] is m_selector2 $ [ m_is_write, m_addr, m_step, m_value ] } function main { ADDR <=X= 4; diff --git a/test_data/asm/mem_read_write_no_memory_accesses.asm b/test_data/asm/mem_read_write_no_memory_accesses.asm index 41a14d4f5..3e5c524d8 100644 --- a/test_data/asm/mem_read_write_no_memory_accesses.asm +++ b/test_data/asm/mem_read_write_no_memory_accesses.asm @@ -44,7 +44,7 @@ machine MemReadWrite { // 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; + (1 - LAST) $ [ m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step) ] in [POSITIVE]; // m_change has to be 1 in the last row, so that a first read on row zero is constrained to return 0 (1 - m_change) * LAST = 0; @@ -61,8 +61,8 @@ machine MemReadWrite { (1 - m_is_write') * m_change * m_value' = 0; instr assert_zero X { XIsZero = 1 } - instr mload -> X { { 0, ADDR, STEP, X } is m_selector1 { m_is_write, m_addr, m_step, m_value } } - instr mstore X { { 1, ADDR, STEP, X } is m_selector2 { m_is_write, m_addr, m_step, m_value } } + instr mload -> X { [ 0, ADDR, STEP, X ] is m_selector1 $ [ m_is_write, m_addr, m_step, m_value ] } + instr mstore X { [ 1, ADDR, STEP, X ] is m_selector2 $ [ m_is_write, m_addr, m_step, m_value ] } function main { return; diff --git a/test_data/asm/mem_read_write_with_bootloader.asm b/test_data/asm/mem_read_write_with_bootloader.asm index a3e5b7a80..613e365d0 100644 --- a/test_data/asm/mem_read_write_with_bootloader.asm +++ b/test_data/asm/mem_read_write_with_bootloader.asm @@ -49,7 +49,7 @@ machine MemReadWrite { // 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; + (1 - LAST) $ [ m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step) ] in [POSITIVE]; // m_change has to be 1 in the last row, so that the above constraint is triggered. // An exception to this when the last address is -1, which is only possible if there is @@ -71,9 +71,9 @@ machine MemReadWrite { instr assert_zero X { XIsZero = 1 } let operation_id = m_is_write + 2 * m_is_bootloader_write; - instr mload -> X { { 0, ADDR, STEP, X } is m_selector1 { operation_id, m_addr, m_step, m_value } } - instr mstore X { { 1, ADDR, STEP, X } is m_selector2 { operation_id, m_addr, m_step, m_value } } - instr mstore_bootloader X { { 2, ADDR, STEP, X } is m_selector3 { operation_id, m_addr, m_step, m_value } } + instr mload -> X { [ 0, ADDR, STEP, X ] is m_selector1 $ [ operation_id, m_addr, m_step, m_value ] } + instr mstore X { [ 1, ADDR, STEP, X ] is m_selector2 $ [ operation_id, m_addr, m_step, m_value ] } + instr mstore_bootloader X { [ 2, ADDR, STEP, X ] is m_selector3 $ [ operation_id, m_addr, m_step, m_value ] } function main { ADDR <=X= 4; diff --git a/test_data/asm/palindrome.asm b/test_data/asm/palindrome.asm index 9d00e8bb8..e4a796bba 100644 --- a/test_data/asm/palindrome.asm +++ b/test_data/asm/palindrome.asm @@ -30,13 +30,13 @@ machine Palindrome with degree: 1024 { // This enforces that addresses are stored in an ascending order // (and in particular, are unique). - NOTLAST { m_addr' - m_addr } in POSITIVE; + 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 } instr assert_zero X { XIsZero = 1 } - instr mstore X { { ADDR, X } in { m_addr, m_value } } - instr mload -> X { { ADDR, X } in { m_addr, m_value } } + instr mstore X { [ ADDR, X ] in [ m_addr, m_value ] } + instr mload -> X { [ ADDR, X ] in [ m_addr, m_value ] } function main { // TOOD somehow this is not properly resolved here without "std::prover::" diff --git a/test_data/asm/pass_range_constraints.asm b/test_data/asm/pass_range_constraints.asm index d5ba761ed..65bc0ee74 100644 --- a/test_data/asm/pass_range_constraints.asm +++ b/test_data/asm/pass_range_constraints.asm @@ -26,8 +26,8 @@ machine Mul with // Make range constraints conditional on "used", just so // that witgen is forced to infer the range constraints // while solving, rather than inferring global range constraints. - used { x } in { FOUR_BIT }; - used { y } in { FOUR_BIT }; + used $ [ x ] in [ FOUR_BIT ]; + used $ [ y ] in [ FOUR_BIT ]; z = x * y; } @@ -53,6 +53,6 @@ machine Main with // Again, make range constraints conditional col fixed FOUR_BIT(i) { i & 0xf }; - latch { res_lower } in { FOUR_BIT }; - latch { res_upper } in { FOUR_BIT }; + latch $ [ res_lower ] in [ FOUR_BIT ]; + latch $ [ res_upper ] in [ FOUR_BIT ]; } diff --git a/test_data/asm/permutations/block_to_block.asm b/test_data/asm/permutations/block_to_block.asm index 1328e9d9d..3a6cd8068 100644 --- a/test_data/asm/permutations/block_to_block.asm +++ b/test_data/asm/permutations/block_to_block.asm @@ -28,7 +28,7 @@ machine Binary with B' = B * (1 - latch) + B_byte * FACTOR; C' = C * (1 - latch) + C_byte * FACTOR; - {A_byte, B_byte, C_byte} in {P_A, P_B, P_C}; + [A_byte, B_byte, C_byte] in [P_A, P_B, P_C]; } machine Binary4 with diff --git a/test_data/asm/permutations/call_selectors_with_no_permutation.asm b/test_data/asm/permutations/call_selectors_with_no_permutation.asm index b3e3c359a..77f520bda 100644 --- a/test_data/asm/permutations/call_selectors_with_no_permutation.asm +++ b/test_data/asm/permutations/call_selectors_with_no_permutation.asm @@ -31,7 +31,7 @@ machine Binary with B' = B * (1 - latch) + B_byte * FACTOR; C' = C * (1 - latch) + C_byte * FACTOR; - {A_byte, B_byte, C_byte} in {P_A, P_B, P_C}; + [A_byte, B_byte, C_byte] in [P_A, P_B, P_C]; } machine Main with degree: 65536 { diff --git a/test_data/asm/permutations/simple.asm b/test_data/asm/permutations/simple.asm index 7ddcd0f76..ec7ef681b 100644 --- a/test_data/asm/permutations/simple.asm +++ b/test_data/asm/permutations/simple.asm @@ -30,7 +30,7 @@ machine Binary with B' = B * (1 - latch) + B_byte * FACTOR; C' = C * (1 - latch) + C_byte * FACTOR; - {A_byte, B_byte, C_byte} in {P_A, P_B, P_C}; + [A_byte, B_byte, C_byte] in [P_A, P_B, P_C]; } machine Main with degree: 65536 { diff --git a/test_data/asm/permutations/vm_to_block.asm b/test_data/asm/permutations/vm_to_block.asm index 5ae79f0e6..a4ba5cbae 100644 --- a/test_data/asm/permutations/vm_to_block.asm +++ b/test_data/asm/permutations/vm_to_block.asm @@ -28,7 +28,7 @@ machine Binary with B' = B * (1 - latch) + B_byte * FACTOR; C' = C * (1 - latch) + C_byte * FACTOR; - {A_byte, B_byte, C_byte} in {P_A, P_B, P_C}; + [A_byte, B_byte, C_byte] in [P_A, P_B, P_C]; } machine Main with degree: 65536 { diff --git a/test_data/asm/secondary_block_machine_add2.asm b/test_data/asm/secondary_block_machine_add2.asm index f17f48a7c..635283d83 100644 --- a/test_data/asm/secondary_block_machine_add2.asm +++ b/test_data/asm/secondary_block_machine_add2.asm @@ -31,7 +31,7 @@ machine Main with degree: 16 { 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 } + [Y, X] in add_two_RESET $ [ add_two_input, add_two_state ] } function main { diff --git a/test_data/asm/sqrt.asm b/test_data/asm/sqrt.asm index 155b81c2d..4a897fd83 100644 --- a/test_data/asm/sqrt.asm +++ b/test_data/asm/sqrt.asm @@ -34,7 +34,7 @@ machine Sqrt with // Note that this is required to make the witness unique // (y := -y would also satisfy y * y = x, but we want the positive solution). - { y } in { range }; + [ y ] in [ range ]; } diff --git a/test_data/asm/vm_to_block_unique_interface.asm b/test_data/asm/vm_to_block_unique_interface.asm index 8acdd44b9..039f59d6d 100644 --- a/test_data/asm/vm_to_block_unique_interface.asm +++ b/test_data/asm/vm_to_block_unique_interface.asm @@ -16,7 +16,7 @@ machine Binary with 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 }; + [ operation_id, x, y, z ] in [ P_FUNCTION, P_X, P_Y, P_Z ]; } machine Arith with diff --git a/test_data/pil/block_lookup_or.pil b/test_data/pil/block_lookup_or.pil index 73cd01e87..4427d27bf 100644 --- a/test_data/pil/block_lookup_or.pil +++ b/test_data/pil/block_lookup_or.pil @@ -34,7 +34,7 @@ namespace Or(%N); B' = B * (1 - RESET) + B_byte * FACTOR; C' = C * (1 - RESET) + C_byte * FACTOR; - {A_byte, B_byte, C_byte} in {P_A, P_B, P_C}; + [A_byte, B_byte, C_byte] in [P_A, P_B, P_C]; namespace Main(%N); col fixed a(i) { (i + 13) & 0xffffffff }; @@ -42,5 +42,5 @@ namespace Main(%N); col witness c; col fixed NTH(i) { if i % 32 == 0 { 1 } else { 0 } }; - NTH {a, b, c} in Or.RESET {Or.A, Or.B, Or.C}; + NTH $ [a, b, c] in Or.RESET $ [Or.A, Or.B, Or.C]; diff --git a/test_data/pil/block_lookup_or_permutation.pil b/test_data/pil/block_lookup_or_permutation.pil index 08028e1bb..f0f9254e7 100644 --- a/test_data/pil/block_lookup_or_permutation.pil +++ b/test_data/pil/block_lookup_or_permutation.pil @@ -46,7 +46,7 @@ namespace Or(%N); B' = B * (1 - RESET) + B_byte * FACTOR; C' = C * (1 - RESET) + C_byte * FACTOR; - {A_byte, B_byte, C_byte} in {P_A, P_B, P_C}; + [A_byte, B_byte, C_byte] in [P_A, P_B, P_C]; namespace Main(%N); col fixed a(i) { (i + 13) & 0xffffffff }; @@ -54,6 +54,6 @@ namespace Main(%N); col witness c; col fixed NTH(i) { if i % 32 == 16 { 1 } else { 0 } }; - NTH {a, b, c} is (Or.selector1 * Or.RESET) {Or.A, Or.B, Or.C}; - NTH' {a, b, c} is (Or.selector2 * Or.RESET) {Or.A, Or.B, Or.C}; + NTH $ [a, b, c] is (Or.selector1 * Or.RESET) $ [Or.A, Or.B, Or.C]; + NTH' $ [a, b, c] is (Or.selector2 * Or.RESET) $ [Or.A, Or.B, Or.C]; diff --git a/test_data/pil/conditional_fixed_constraints.pil b/test_data/pil/conditional_fixed_constraints.pil index ee1923d9e..e6e96e687 100644 --- a/test_data/pil/conditional_fixed_constraints.pil +++ b/test_data/pil/conditional_fixed_constraints.pil @@ -11,19 +11,19 @@ namespace Main(N); let X_b3; let X_b2; let X_b1; - { X_b4 } in { bytes }; - { X_b3 } in { bytes }; - { X_b2 } in { bytes }; - { X_b1 } in { bytes }; + [ X_b4 ] in [ bytes ]; + [ X_b3 ] in [ bytes ]; + [ X_b2 ] in [ bytes ]; + [ X_b1 ] in [ bytes ]; let cond; - cond { Z } in { two_bits }; + cond $ [ Z ] in [ two_bits ]; let two_bits: col = |i| i % 4; 0 = cond * (Y - (wrap_bit * 2**32 + X_b4 * 0x1000000 + X_b3 * 0x10000 + X_b2 * 0x100 + X_b1 * 4 + Z)); let six_bits: col = |i| i % 2**6; - cond { X_b1 } in { six_bits }; + cond $ [ X_b1 ] in [ six_bits ]; let odd: col = |i| i % 2; cond = odd; diff --git a/test_data/pil/lookup_with_selector.pil b/test_data/pil/lookup_with_selector.pil index aef00d688..325610223 100644 --- a/test_data/pil/lookup_with_selector.pil +++ b/test_data/pil/lookup_with_selector.pil @@ -8,4 +8,4 @@ namespace main(%N); col fixed t = [1, 2, 3, 4]*; col fixed s_t = [0, 1]*; - s_w {w} in s_t {t}; + s_w $ [w] in s_t $ [t]; diff --git a/test_data/pil/naive_byte_decomposition.pil b/test_data/pil/naive_byte_decomposition.pil index 23b67ce2e..fff4fe80e 100644 --- a/test_data/pil/naive_byte_decomposition.pil +++ b/test_data/pil/naive_byte_decomposition.pil @@ -9,13 +9,13 @@ namespace Main(256); let BYTES: col = |i| i % 256; let bytes: col[8]; - { bytes[0] } in { BYTES }; - { bytes[1] } in { BYTES }; - { bytes[2] } in { BYTES }; - { bytes[3] } in { BYTES }; - { bytes[4] } in { BYTES }; - { bytes[5] } in { BYTES }; - { bytes[6] } in { BYTES }; - { bytes[7] } in { BYTES }; + [ bytes[0] ] in [ BYTES ]; + [ bytes[1] ] in [ BYTES ]; + [ bytes[2] ] in [ BYTES ]; + [ bytes[3] ] in [ BYTES ]; + [ bytes[4] ] in [ BYTES ]; + [ bytes[5] ] in [ BYTES ]; + [ bytes[6] ] in [ BYTES ]; + [ bytes[7] ] in [ BYTES ]; INPUT = bytes[0] + bytes[1] * 256 + bytes[2] * 256**2 + bytes[3] * 256**3 + bytes[4] * 256**4 + bytes[5] * 256**5 + bytes[6] * 256**6 + bytes[7] * 256**7; diff --git a/test_data/pil/pair_lookup.pil b/test_data/pil/pair_lookup.pil index 6e071a946..4bbd22486 100644 --- a/test_data/pil/pair_lookup.pil +++ b/test_data/pil/pair_lookup.pil @@ -14,5 +14,5 @@ namespace Main(N); col fixed b(i) { (i * 17 + 3) & 0xff }; col witness c; - {a, b, c} in {Main.A, Main.B, Main.C}; - {b, a, c} in {Main.A, Main.B, Main.C}; \ No newline at end of file + [a, b, c] in [Main.A, Main.B, Main.C]; + [b, a, c] in [Main.A, Main.B, Main.C]; \ No newline at end of file diff --git a/test_data/pil/permutation_with_selector.pil b/test_data/pil/permutation_with_selector.pil index cc8a513c3..3921cdfe8 100644 --- a/test_data/pil/permutation_with_selector.pil +++ b/test_data/pil/permutation_with_selector.pil @@ -8,4 +8,4 @@ namespace main(%N); col fixed t = [1, 2, 3, 4]*; col fixed s_t = [0, 1]*; - s_w {w} is s_t {t}; + s_w $ [w] is s_t $ [t]; diff --git a/test_data/pil/simple_div.pil b/test_data/pil/simple_div.pil index 90de6efcd..cce360f1d 100644 --- a/test_data/pil/simple_div.pil +++ b/test_data/pil/simple_div.pil @@ -25,12 +25,12 @@ namespace SimpleDiv(%N); col witness X_b2; col witness R_b1; col witness R_b2; - { Y_b1 } in { BYTE }; - { Y_b2 } in { BYTE }; - { X_b1 } in { BYTE }; - { X_b2 } in { BYTE }; - { R_b1 } in { BYTE }; - { R_b2 } in { BYTE }; + [ Y_b1 ] in [ BYTE ]; + [ Y_b2 ] in [ BYTE ]; + [ X_b1 ] in [ BYTE ]; + [ X_b2 ] in [ BYTE ]; + [ R_b1 ] in [ BYTE ]; + [ R_b2 ] in [ BYTE ]; // now the check: col fixed CHECK = [0, 0, 0, 0, 0] + [1] + [0]*; diff --git a/test_data/pil/single_line_blocks.pil b/test_data/pil/single_line_blocks.pil index 279b0b4b8..d0d1b5dbe 100644 --- a/test_data/pil/single_line_blocks.pil +++ b/test_data/pil/single_line_blocks.pil @@ -18,5 +18,5 @@ namespace Main(%N); col fixed CALL = [1, 0]*; (1 - CALL) * c = 0; - CALL {a, b, c} in {Add.A, Add.B, Add.C}; + CALL $ [a, b, c] in [Add.A, Add.B, Add.C]; diff --git a/test_data/pil/two_block_machine_functions.pil b/test_data/pil/two_block_machine_functions.pil index 3ad72beda..364911e36 100644 --- a/test_data/pil/two_block_machine_functions.pil +++ b/test_data/pil/two_block_machine_functions.pil @@ -5,11 +5,11 @@ namespace main(8); col witness x; col witness y; col witness instr_foo; - main.instr_foo { 1 } in main.latch { main.x }; + main.instr_foo $ [ 1 ] in main.latch $ [ main.x ]; col witness instr_bar; - main.instr_bar { 2 } in main.latch { main.y }; + main.instr_bar $ [ 2 ] in main.latch $ [ main.y ]; col witness instr_baz; - main.instr_baz { 3 } in main.latch { main.y }; + main.instr_baz $ [ 3 ] in main.latch $ [ main.y ]; col witness instr_loop; main.pc' = ((1 - main.first_step') * ((main.instr_loop * main.pc) + ((1 - main.instr_loop) * (main.pc + 1)))); col fixed p_line = [0, 1, 2, 3] + [3]*; @@ -17,4 +17,4 @@ namespace main(8); col fixed p_instr_bar = [0, 1, 0, 0] + [0]*; col fixed p_instr_foo = [1, 0, 0, 0] + [0]*; col fixed p_instr_loop = [0, 0, 0, 1] + [1]*; - { main.pc, main.instr_foo, main.instr_bar, main.instr_baz, main.instr_loop } in { main.p_line, main.p_instr_foo, main.p_instr_bar, main.p_instr_baz, main.p_instr_loop }; + [ main.pc, main.instr_foo, main.instr_bar, main.instr_baz, main.instr_loop ] in [ main.p_line, main.p_instr_foo, main.p_instr_bar, main.p_instr_baz, main.p_instr_loop ]; diff --git a/test_data/pil/witness_lookup.pil b/test_data/pil/witness_lookup.pil index 3ede97933..b43cb0d51 100644 --- a/test_data/pil/witness_lookup.pil +++ b/test_data/pil/witness_lookup.pil @@ -16,7 +16,7 @@ namespace Quad(%N); col witness wdouble; col witness quadruple; - {input, wdouble} in {id, double}; - {wdouble, quadruple} in {id, double}; + [input, wdouble] in [id, double]; + [wdouble, quadruple] in [id, double]; public out = quadruple(%N-1); diff --git a/test_data/polygon-hermez/arith.pil b/test_data/polygon-hermez/arith.pil index e3da19487..694451185 100644 --- a/test_data/polygon-hermez/arith.pil +++ b/test_data/polygon-hermez/arith.pil @@ -256,10 +256,10 @@ namespace Arith(%N); + q0[0]*Global.CLK32[16] + q0[1]*Global.CLK32[17] + q0[2]*Global.CLK32[18] + q0[3]*Global.CLK32[19] + q0[4]*Global.CLK32[20] + q0[5]*Global.CLK32[21] + q0[6]*Global.CLK32[22] + q0[7]*Global.CLK32[23] + q0[8]*Global.CLK32[24] + q0[9]*Global.CLK32[25] + q0[10]*Global.CLK32[26] + q0[11]*Global.CLK32[27] + q0[12]*Global.CLK32[28] + q0[13]*Global.CLK32[29] + q0[14]*Global.CLK32[30] + q1[0]*Global.CLK32[31] in Global.BYTE2; - {Global.CLK32[29] + Global.CLK32[30] + Global.CLK32[31], q1[1]*Global.CLK32[0] + q1[2]*Global.CLK32[1] + q1[3]*Global.CLK32[2] + q1[4]*Global.CLK32[3] + q1[5]*Global.CLK32[4] + q1[6]*Global.CLK32[5] + q1[7]*Global.CLK32[6] + q1[8]*Global.CLK32[7] + [Global.CLK32[29] + Global.CLK32[30] + Global.CLK32[31], q1[1]*Global.CLK32[0] + q1[2]*Global.CLK32[1] + q1[3]*Global.CLK32[2] + q1[4]*Global.CLK32[3] + q1[5]*Global.CLK32[4] + q1[6]*Global.CLK32[5] + q1[7]*Global.CLK32[6] + q1[8]*Global.CLK32[7] + q1[9]*Global.CLK32[8] + q1[10]*Global.CLK32[9] + q1[11]*Global.CLK32[10] + q1[12]*Global.CLK32[11] + q1[13]*Global.CLK32[12] + q1[14]*Global.CLK32[13] + q2[0]*Global.CLK32[14] + q2[1]*Global.CLK32[15] + q2[2]*Global.CLK32[16] + q2[3]*Global.CLK32[17] + q2[4]*Global.CLK32[18] + q2[5]*Global.CLK32[19] + q2[6]*Global.CLK32[20] + q2[7]*Global.CLK32[21] + q2[8]*Global.CLK32[22] + q2[9]*Global.CLK32[23] - + q2[10]*Global.CLK32[24] + q2[11]*Global.CLK32[25] + q2[12]*Global.CLK32[26] + q2[13]*Global.CLK32[27] + q2[14]*Global.CLK32[28] + q0[15]*Global.CLK32[29] + q1[15]*Global.CLK32[30] + q2[15]*Global.CLK32[31]} in {SEL_BYTE2_BIT19, BYTE2_BIT19}; + + q2[10]*Global.CLK32[24] + q2[11]*Global.CLK32[25] + q2[12]*Global.CLK32[26] + q2[13]*Global.CLK32[27] + q2[14]*Global.CLK32[28] + q0[15]*Global.CLK32[29] + q1[15]*Global.CLK32[30] + q2[15]*Global.CLK32[31]] in [SEL_BYTE2_BIT19, BYTE2_BIT19]; /******* * diff --git a/test_data/polygon-hermez/binary.pil b/test_data/polygon-hermez/binary.pil index 50793fef2..c24ad2363 100644 --- a/test_data/polygon-hermez/binary.pil +++ b/test_data/polygon-hermez/binary.pil @@ -91,8 +91,8 @@ namespace Binary(%N); lCout' = cOut; lOpcode' = opcode; - {0, opcode, freeInA[0], freeInB[0], cIn, 0, freeInC[0], cMiddle} in {P_LAST, P_OPCODE, Global.BYTE_2A, Global.BYTE, P_CIN, P_USE_CARRY, P_C, P_COUT}; - {resultValidRange' + resultBinOp', opcode, freeInA[1], freeInB[1], cMiddle, useCarry ,freeInC[1], cOut} in {P_LAST, P_OPCODE, Global.BYTE_2A, Global.BYTE, P_CIN, P_USE_CARRY, P_C, P_COUT}; + [0, opcode, freeInA[0], freeInB[0], cIn, 0, freeInC[0], cMiddle] in [P_LAST, P_OPCODE, Global.BYTE_2A, Global.BYTE, P_CIN, P_USE_CARRY, P_C, P_COUT]; + [resultValidRange' + resultBinOp', opcode, freeInA[1], freeInB[1], cMiddle, useCarry ,freeInC[1], cOut] in [P_LAST, P_OPCODE, Global.BYTE_2A, Global.BYTE, P_CIN, P_USE_CARRY, P_C, P_COUT]; a[0]' = a[0] * (1 - RESET) + freeInA[0] * FACTOR[0] + 256 * freeInA[1] * FACTOR[0]; a[1]' = a[1] * (1 - RESET) + freeInA[0] * FACTOR[1] + 256 * freeInA[1] * FACTOR[1]; diff --git a/test_data/polygon-hermez/keccakf.pil b/test_data/polygon-hermez/keccakf.pil index 6897d91d2..6fcd91e98 100644 --- a/test_data/polygon-hermez/keccakf.pil +++ b/test_data/polygon-hermez/keccakf.pil @@ -18,12 +18,12 @@ namespace KeccakF(%N); pol b44 = b[3] * 2**33 + b[2] * 2**22 + b[1] * 2**11 + b[0]; pol c44 = c[3] * 2**33 + c[2] * 2**22 + c[1] * 2**11 + c[0]; - {a44, b44, c44} connect {ConnA, ConnB, ConnC}; + [a44, b44, c44] connect [ConnA, ConnB, ConnC]; - { GateType, a[0], b[0], c[0] } in { kGateType, kA, kB, kC } ; - { GateType, a[1], b[1], c[1] } in { kGateType, kA, kB, kC } ; - { GateType, a[2], b[2], c[2] } in { kGateType, kA, kB, kC } ; - { GateType, a[3], b[3], c[3] } in { kGateType, kA, kB, kC } ; + [ GateType, a[0], b[0], c[0] ] in [ kGateType, kA, kB, kC ] ; + [ GateType, a[1], b[1], c[1] ] in [ kGateType, kA, kB, kC ] ; + [ GateType, a[2], b[2], c[2] ] in [ kGateType, kA, kB, kC ] ; + [ GateType, a[3], b[3], c[3] ] in [ kGateType, kA, kB, kC ] ; Global.L1 * a44 = 0; Global.L1 * (2**44-1-b44) = 0; \ No newline at end of file diff --git a/test_data/polygon-hermez/main.pil b/test_data/polygon-hermez/main.pil index 16e06d71c..1da2fbc22 100644 --- a/test_data/polygon-hermez/main.pil +++ b/test_data/polygon-hermez/main.pil @@ -449,12 +449,12 @@ namespace Main(%N); // Check that the calculated hash is well formed - sWR + hashPDigest { + sWR + hashPDigest $ [ op0, op1, op2, op3, op4, op5, op6, op7 - } is - Binary.resultValidRange { + ] is + Binary.resultValidRange $ [ Binary.a[0], Binary.a[1], Binary.a[2], Binary.a[3], Binary.a[4], Binary.a[5], Binary.a[6], Binary.a[7] - }; + ]; ///////// // ROM Plookpups @@ -528,19 +528,19 @@ namespace Main(%N); (1 - hashP1) * hashP1 = 0; (1 - useElseAddr) * useElseAddr = 0; - { + [ CONST0, CONST1, CONST2, CONST3, CONST4, CONST5, CONST6, CONST7, inA, inB, inC, inROTL_C, inD, inE, inSR, inFREE, inCTX, inSP, inPC, inGAS, inMAXMEM, inHASHPOS, inSTEP, inRR, inHASHPOS, inRCX, inCntArith, inCntBinary, inCntKeccakF, inCntMemAlign, inCntPaddingPG, inCntPoseidonG, operations, offset, incStack, binOpcode, jmpAddr, elseAddr, zkPC - } in { + ] in [ Rom.CONST0, Rom.CONST1, Rom.CONST2, Rom.CONST3, Rom.CONST4, Rom.CONST5, Rom.CONST6, Rom.CONST7, Rom.inA, Rom.inB, Rom.inC, Rom.inROTL_C, Rom.inD, Rom.inE, Rom.inSR, Rom.inFREE, Rom.inCTX, Rom.inSP, Rom.inPC, Rom.inGAS, Rom.inMAXMEM, Rom.inHASHPOS, Rom.inSTEP, Rom.inRR, Rom.inHASHPOS, Rom.inRCX, Rom.inCntArith, Rom.inCntBinary, Rom.inCntKeccakF, Rom.inCntMemAlign, Rom.inCntPaddingPG, Rom.inCntPoseidonG, Rom.operations, Rom.offset, Rom.incStack, Rom.binOpcode, Rom.jmpAddr, Rom.elseAddr, Rom.line - }; + ]; pol commit sKeyI[4]; pol commit sKey[4]; @@ -603,29 +603,29 @@ namespace Main(%N); pol ay3_6 = Arith.y3[12] + Arith.y3[13]*2**16; pol ay3_7 = Arith.y3[14] + Arith.y3[15]*2**16; - arithEq0 { 1, 0, 0, 0, + arithEq0 $ [ 1, 0, 0, 0, A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7, C0, C1, C2, C3, C4, C5, C6, C7, D0, D1, D2, D3, D4, D5, D6, D7, - op0, op1, op2, op3, op4, op5, op6, op7 } is - Arith.resultEq0 { + op0, op1, op2, op3, op4, op5, op6, op7 ] is + Arith.resultEq0 $ [ Arith.selEq[0], Arith.selEq[1], Arith.selEq[2], Arith.selEq[3], ax1_0, ax1_1, ax1_2, ax1_3, ax1_4, ax1_5, ax1_6, ax1_7, ay1_0, ay1_1, ay1_2, ay1_3, ay1_4, ay1_5, ay1_6, ay1_7, ax2_0, ax2_1, ax2_2, ax2_3, ax2_4, ax2_5, ax2_6, ax2_7, ay2_0, ay2_1, ay2_2, ay2_3, ay2_4, ay2_5, ay2_6, ay2_7, ay3_0, ay3_1, ay3_2, ay3_3, ay3_4, ay3_5, ay3_6, ay3_7 - }; + ]; - arithEq1 { 0, 1, 0, 1, + arithEq1 $ [ 0, 1, 0, 1, A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7, C0, C1, C2, C3, C4, C5, C6, C7, D0, D1, D2, D3, D4, D5, D6, D7, E0, E1, E2, E3, E4, E5, E6, E7, - op0, op1, op2, op3, op4, op5, op6, op7 } is - Arith.resultEq1 { + op0, op1, op2, op3, op4, op5, op6, op7 ] is + Arith.resultEq1 $ [ Arith.selEq[0], Arith.selEq[1], Arith.selEq[2], Arith.selEq[3], ax1_0, ax1_1, ax1_2, ax1_3, ax1_4, ax1_5, ax1_6, ax1_7, ay1_0, ay1_1, ay1_2, ay1_3, ay1_4, ay1_5, ay1_6, ay1_7, @@ -633,16 +633,16 @@ namespace Main(%N); ay2_0, ay2_1, ay2_2, ay2_3, ay2_4, ay2_5, ay2_6, ay2_7, ax3_0, ax3_1, ax3_2, ax3_3, ax3_4, ax3_5, ax3_6, ax3_7, ay3_0, ay3_1, ay3_2, ay3_3, ay3_4, ay3_5, ay3_6, ay3_7 - }; + ]; - arithEq2 { 0, 0, 1, 1, + arithEq2 $ [ 0, 0, 1, 1, A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7, A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7, E0, E1, E2, E3, E4, E5, E6, E7, - op0, op1, op2, op3, op4, op5, op6, op7 } is - Arith.resultEq2 { + op0, op1, op2, op3, op4, op5, op6, op7 ] is + Arith.resultEq2 $ [ Arith.selEq[0], Arith.selEq[1], Arith.selEq[2], Arith.selEq[3], ax1_0, ax1_1, ax1_2, ax1_3, ax1_4, ax1_5, ax1_6, ax1_7, ay1_0, ay1_1, ay1_2, ay1_3, ay1_4, ay1_5, ay1_6, ay1_7, @@ -650,7 +650,7 @@ namespace Main(%N); ay2_0, ay2_1, ay2_2, ay2_3, ay2_4, ay2_5, ay2_6, ay2_7, ax3_0, ax3_1, ax3_2, ax3_3, ax3_4, ax3_5, ax3_6, ax3_7, ay3_0, ay3_1, ay3_2, ay3_3, ay3_4, ay3_5, ay3_6, ay3_7 - }; + ]; cntArith' = cntArith*(1-Global.L1) + arithEq0 + arithEq1 + arithEq2; @@ -658,108 +658,108 @@ namespace Main(%N); // Binary Plookpups ///////// - bin { + bin $ [ binOpcode, A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7, op0, op1, op2, op3, op4, op5, op6, op7, carry - } is - Binary.resultBinOp { + ] is + Binary.resultBinOp $ [ Binary.lOpcode, Binary.a[0], Binary.a[1], Binary.a[2], Binary.a[3], Binary.a[4], Binary.a[5], Binary.a[6], Binary.a[7], Binary.b[0], Binary.b[1], Binary.b[2], Binary.b[3], Binary.b[4], Binary.b[5], Binary.b[6], Binary.b[7], Binary.c[0], Binary.c[1], Binary.c[2], Binary.c[3], Binary.c[4], Binary.c[5], Binary.c[6], Binary.c[7], Binary.lCout - }; + ]; cntBinary' = cntBinary*(1-Global.L1) + bin + sWR + hashPDigest; ///////// // HASHK Plookpups ///////// - hashK + hashK1 { + hashK + hashK1 $ [ addr, HASHPOS, D0 * hashK + hashK1, op0, op1, op2, op3, op4, op5, op6, op7 - } in - PaddingKK.crLatch * PaddingKK.r8valid { + ] in + PaddingKK.crLatch * PaddingKK.r8valid $ [ PaddingKK.addr, PaddingKK.len - PaddingKK.rem - PaddingKK.crLen + 1, PaddingKK.crLen, PaddingKK.crV0C, PaddingKK.crV1C, PaddingKK.crV2C, PaddingKK.crV3C, PaddingKK.crV4C, PaddingKK.crV5C, PaddingKK.crV6C, PaddingKK.crV7C - }; + ]; - hashKLen { + hashKLen $ [ addr, op0 - } is - PaddingKK.lastHashLen { + ] is + PaddingKK.lastHashLen $ [ PaddingKK.addr, PaddingKK.len - }; + ]; - hashKDigest { + hashKDigest $ [ addr, op0, op1, op2, op3, op4, op5, op6, op7, incCounter - } is - PaddingKK.lastHashDigest { + ] is + PaddingKK.lastHashDigest $ [ PaddingKK.addr, PaddingKK.hash0, PaddingKK.hash1, PaddingKK.hash2, PaddingKK.hash3, PaddingKK.hash4, PaddingKK.hash5, PaddingKK.hash6, PaddingKK.hash7, PaddingKK.incCounter - }; + ]; cntKeccakF' = cntKeccakF*(1-Global.L1) + incCounter*hashKDigest; ///////// // HASHP Plookpups ///////// - hashP + hashP1 { + hashP + hashP1 $ [ addr, HASHPOS, D0 * hashP + hashP1, op0, op1, op2, op3, op4, op5, op6, op7 - } in - PaddingPG.crLatch { + ] in + PaddingPG.crLatch $ [ PaddingPG.addr, PaddingPG.len - PaddingPG.rem - PaddingPG.crLen + 1, PaddingPG.crLen, PaddingPG.crV0C, PaddingPG.crV1C, PaddingPG.crV2C, PaddingPG.crV3C, PaddingPG.crV4C, PaddingPG.crV5C, PaddingPG.crV6C, PaddingPG.crV7C - }; + ]; - hashPLen { + hashPLen $ [ addr, op0 - } is - PaddingPG.lastHashLen { + ] is + PaddingPG.lastHashLen $ [ PaddingPG.addr, PaddingPG.len - }; + ]; - hashPDigest { + hashPDigest $ [ addr, op0 + 2**32 * op1, op2 + 2**32 * op3, op4 + 2**32 * op5, op6 + 2**32 * op7, incCounter - } is - PaddingPG.lastHashDigest { + ] is + PaddingPG.lastHashDigest $ [ PaddingPG.addr, PaddingPG.curHash0, PaddingPG.curHash1, PaddingPG.curHash2, PaddingPG.curHash3, PaddingPG.incCounter - }; + ]; cntPaddingPG' = cntPaddingPG*(1-Global.L1) + hashPDigest*incCounter; cntPoseidonG' = cntPoseidonG*(1-Global.L1) + (hashPDigest + sRD + sWR) * incCounter; @@ -767,33 +767,33 @@ namespace Main(%N); ///////// // Mem Plookpups ///////// - mOp { + mOp $ [ addr, Global.STEP, mWR, op0, op1, op2, op3, op4, op5, op6, op7 - } is - Mem.mOp { + ] is + Mem.mOp $ [ Mem.addr, Mem.step, Mem.mWr, Mem.val[0], Mem.val[1], Mem.val[2], Mem.val[3], Mem.val[4], Mem.val[5], Mem.val[6], Mem.val[7] - }; + ]; ///////// // Storage Plookpups ///////// - (sRD + sWR) { + (sRD + sWR) $ [ 1, 0, 0, // Poseidon Result ID C0, C1, C2, C3, C4, C5, C6, C7, 0, 0, 0, 0, sKeyI[0], sKeyI[1], sKeyI[2], sKeyI[3] - } is - PoseidonG.result1 { + ] is + PoseidonG.result1 $ [ PoseidonG.result1, PoseidonG.result2, PoseidonG.result3, PoseidonG.in0, PoseidonG.in1, @@ -811,15 +811,15 @@ namespace Main(%N); PoseidonG.hash1, PoseidonG.hash2, PoseidonG.hash3 - }; + ]; - (sRD + sWR) { + (sRD + sWR) $ [ 0, 1, 0, A0, A1, A2, A3, A4, A5, B0, B1, sKeyI[0], sKeyI[1], sKeyI[2], sKeyI[3], sKey[0], sKey[1], sKey[2], sKey[3] - } is - PoseidonG.result2 { + ] is + PoseidonG.result2 $ [ PoseidonG.result1, PoseidonG.result2, PoseidonG.result3, PoseidonG.in0, PoseidonG.in1, @@ -837,40 +837,40 @@ namespace Main(%N); PoseidonG.hash1, PoseidonG.hash2, PoseidonG.hash3 - }; + ]; - sRD { + sRD $ [ SR0 + 2**32*SR1, SR2 + 2**32*SR3, SR4 + 2**32*SR5, SR6 + 2**32*SR7, sKey[0], sKey[1], sKey[2], sKey[3], op0, op1, op2, op3, op4, op5, op6, op7, incCounter - } is - Storage.iLatchGet { + ] is + Storage.iLatchGet $ [ Storage.oldRoot0, Storage.oldRoot1, Storage.oldRoot2, Storage.oldRoot3, Storage.rkey0, Storage.rkey1, Storage.rkey2, Storage.rkey3, Storage.valueLow0, Storage.valueLow1, Storage.valueLow2, Storage.valueLow3, Storage.valueHigh0, Storage.valueHigh1, Storage.valueHigh2, Storage.valueHigh3, Storage.incCounter + 2 - }; + ]; - sWR { + sWR $ [ SR0 + 2**32*SR1, SR2 + 2**32*SR3, SR4 + 2**32*SR5, SR6 + 2**32*SR7, sKey[0], sKey[1], sKey[2], sKey[3], D0, D1, D2, D3, D4, D5, D6, D7, op0 + 2**32*op1, op2 + 2**32*op3, op4 + 2**32*op5, op6 + 2**32*op7, incCounter - } is - Storage.iLatchSet { + ] is + Storage.iLatchSet $ [ Storage.oldRoot0, Storage.oldRoot1, Storage.oldRoot2, Storage.oldRoot3, Storage.rkey0, Storage.rkey1, Storage.rkey2, Storage.rkey3, Storage.valueLow0, Storage.valueLow1, Storage.valueLow2, Storage.valueLow3, Storage.valueHigh0, Storage.valueHigh1, Storage.valueHigh2, Storage.valueHigh3, Storage.newRoot0, Storage.newRoot1, Storage.newRoot2, Storage.newRoot3, Storage.incCounter + 2 - }; + ]; ///////// @@ -878,7 +878,7 @@ namespace Main(%N); ///////// // memAlign RD - memAlignRD { + memAlignRD $ [ 0, 0, A0, A1, A2, A3, A4, A5, A6, A7, @@ -887,8 +887,8 @@ namespace Main(%N); op0, op1, op2, op3, op4, op5, op6, op7, C0 - } is - MemAlign.resultRd { + ] is + MemAlign.resultRd $ [ MemAlign.wr256, MemAlign.wr8, MemAlign.m0[0], MemAlign.m0[1], MemAlign.m0[2], MemAlign.m0[3], @@ -898,9 +898,9 @@ namespace Main(%N); MemAlign.v[0], MemAlign.v[1], MemAlign.v[2], MemAlign.v[3], MemAlign.v[4], MemAlign.v[5], MemAlign.v[6], MemAlign.v[7], MemAlign.offset - }; + ]; - memAlignWR { + memAlignWR $ [ 1, 0, A0, A1, A2, A3, A4, A5, A6, A7, @@ -913,8 +913,8 @@ namespace Main(%N); D4, D5, D6, D7, E0, E1, E2, E3, E4, E5, E6, E7 - } is - MemAlign.resultWr256 { + ] is + MemAlign.resultWr256 $ [ MemAlign.wr256, MemAlign.wr8, MemAlign.m0[0], MemAlign.m0[1], MemAlign.m0[2], MemAlign.m0[3], @@ -928,9 +928,9 @@ namespace Main(%N); MemAlign.w0[4], MemAlign.w0[5], MemAlign.w0[6], MemAlign.w0[7], MemAlign.w1[0], MemAlign.w1[1], MemAlign.w1[2], MemAlign.w1[3], MemAlign.w1[4], MemAlign.w1[5], MemAlign.w1[6], MemAlign.w1[7] - }; + ]; - memAlignWR8 { + memAlignWR8 $ [ 0, 1, A0, A1, A2, A3, A4, A5, A6, A7, @@ -939,8 +939,8 @@ namespace Main(%N); C0, D0, D1, D2, D3, D4, D5, D6, D7 - } is - MemAlign.resultWr8 { + ] is + MemAlign.resultWr8 $ [ MemAlign.wr256, MemAlign.wr8, MemAlign.m0[0], MemAlign.m0[1], MemAlign.m0[2], MemAlign.m0[3], @@ -950,7 +950,7 @@ namespace Main(%N); MemAlign.offset, MemAlign.w0[0], MemAlign.w0[1], MemAlign.w0[2], MemAlign.w0[3], MemAlign.w0[4], MemAlign.w0[5], MemAlign.w0[6], MemAlign.w0[7] - }; + ]; cntMemAlign' = cntMemAlign*(1-Global.L1) + memAlignRD + memAlignWR + memAlignWR8; diff --git a/test_data/polygon-hermez/mem.pil b/test_data/polygon-hermez/mem.pil index d5cf40902..785470175 100644 --- a/test_data/polygon-hermez/mem.pil +++ b/test_data/polygon-hermez/mem.pil @@ -21,7 +21,7 @@ namespace Mem(%N); // The list is sorted by [addr, step] lastAccess * (lastAccess - 1) = 0; - ISNOTLAST { lastAccess*( addr' - addr - (step'-step) ) + (step'-step) } in INCS; + ISNOTLAST $ [ lastAccess*( addr' - addr - (step'-step) ) + (step'-step) ] in INCS; (1 - lastAccess) * (addr' - addr) = 0; mOp * (mOp -1) = 0; diff --git a/test_data/polygon-hermez/mem_align.pil b/test_data/polygon-hermez/mem_align.pil index 598e2ec8d..195f5eeba 100644 --- a/test_data/polygon-hermez/mem_align.pil +++ b/test_data/polygon-hermez/mem_align.pil @@ -112,16 +112,16 @@ namespace MemAlign(%N); wr8 * wr256 = 0; // RangeCheck - {inM[1], inM[0]} in {Global.BYTE_2A, Global.BYTE}; + [inM[1], inM[0]] in [Global.BYTE_2A, Global.BYTE]; // Plookup - { + [ Global.STEP32, offset', wr256', wr8', selM1, inV, factorV[0], factorV[1], factorV[2], factorV[3], factorV[4], factorV[5], factorV[6], factorV[7] - } in { + ] in [ Global.STEP32, OFFSET, WR256, WR8, SELM1, BYTE_C4096, FACTORV[0], FACTORV[1], FACTORV[2], FACTORV[3], FACTORV[4], FACTORV[5], FACTORV[6], FACTORV[7] - }; + ]; m0[0]' = (1-RESET) * m0[0] + FACTOR[0] * inM[0]; m0[1]' = (1-RESET) * m0[1] + FACTOR[1] * inM[0]; diff --git a/test_data/polygon-hermez/padding_kk.pil b/test_data/polygon-hermez/padding_kk.pil index 1bcfb52f9..0f23db94d 100644 --- a/test_data/polygon-hermez/padding_kk.pil +++ b/test_data/polygon-hermez/padding_kk.pil @@ -47,14 +47,14 @@ namespace PaddingKK(%N); firstHash' = lastHash; pol aFreeIn = (1 - (remIsZero + spare))*freeIn + remIsZero + lastHash*0x80; - r8valid {aFreeIn, r8Id, connected} in { PaddingKKBit.r8, PaddingKKBit.r8Id, PaddingKKBit.connected }; + r8valid $ [aFreeIn, r8Id, connected] in [ PaddingKKBit.r8, PaddingKKBit.r8Id, PaddingKKBit.connected ]; connected' * ( 1-lastBlock) = connected * (1-lastBlock); connected'*lastBlock = (1 - lastHash)*lastBlock; pol constant sOutId; - lastHashLatch { + lastHashLatch $ [ hash0, hash1, hash2, @@ -64,7 +64,7 @@ namespace PaddingKK(%N); hash6, hash7, sOutId - } in { + ] in [ PaddingKKBit.sOut0, PaddingKKBit.sOut1, PaddingKKBit.sOut2, @@ -74,7 +74,7 @@ namespace PaddingKK(%N); PaddingKKBit.sOut6, PaddingKKBit.sOut7, PaddingKKBit.sOutId - }; + ]; pol constant forceLastHash; (1-lastHash)*forceLastHash = 0; // Force first block to be the beggining @@ -118,10 +118,10 @@ namespace PaddingKK(%N); pol commit crF0, crF1, crF2, crF3, crF4, crF5, crF6, crF7; - { crOffset, crF0, crF1, crF2, crF3, - crF4, crF5, crF6, crF7} in - { Global.STEP32, Global.BYTE_FACTOR[0], Global.BYTE_FACTOR[1], Global.BYTE_FACTOR[2], Global.BYTE_FACTOR[3], - Global.BYTE_FACTOR[4], Global.BYTE_FACTOR[5], Global.BYTE_FACTOR[6], Global.BYTE_FACTOR[7] }; + [ crOffset, crF0, crF1, crF2, crF3, + crF4, crF5, crF6, crF7] in + [ Global.STEP32, Global.BYTE_FACTOR[0], Global.BYTE_FACTOR[1], Global.BYTE_FACTOR[2], Global.BYTE_FACTOR[3], + Global.BYTE_FACTOR[4], Global.BYTE_FACTOR[5], Global.BYTE_FACTOR[6], Global.BYTE_FACTOR[7] ]; pol commit crV0, crV1, crV2, crV3, crV4, crV5, crV6, crV7; diff --git a/test_data/polygon-hermez/padding_kkbit.pil b/test_data/polygon-hermez/padding_kkbit.pil index 8b57a8b25..b205007e3 100644 --- a/test_data/polygon-hermez/padding_kkbit.pil +++ b/test_data/polygon-hermez/padding_kkbit.pil @@ -135,4 +135,4 @@ namespace PaddingKKBit(%N); pol constant ConnSOutBit, ConnSInBit, ConnNine2OneBit; - {sOutBit, sInBit, Nine2One.bit} connect {ConnSOutBit, ConnSInBit, ConnNine2OneBit}; + [sOutBit, sInBit, Nine2One.bit] connect [ConnSOutBit, ConnSInBit, ConnNine2OneBit]; diff --git a/test_data/polygon-hermez/padding_pg.pil b/test_data/polygon-hermez/padding_pg.pil index 0c2c9dc85..8a2d437fe 100644 --- a/test_data/polygon-hermez/padding_pg.pil +++ b/test_data/polygon-hermez/padding_pg.pil @@ -67,7 +67,7 @@ namespace PaddingPG(%N); acc[6]' = acc6C*(1-lastBlock); acc[7]' = acc7C*(1-lastBlock); - lastBlock { + lastBlock $ [ acc0C, acc1C, acc2C, @@ -84,7 +84,7 @@ namespace PaddingPG(%N); curHash1, curHash2, curHash3 - } in PoseidonG.LATCH { + ] in PoseidonG.LATCH $ [ PoseidonG.in0, PoseidonG.in1, PoseidonG.in2, @@ -101,7 +101,7 @@ namespace PaddingPG(%N); PoseidonG.hash1, PoseidonG.hash2, PoseidonG.hash3 - }; + ]; pol commit curHash0, curHash1, curHash2, curHash3; curHash0' * (1-lastBlock) = curHash0*(1-lastBlock); @@ -147,10 +147,10 @@ namespace PaddingPG(%N); pol commit crF0, crF1, crF2, crF3, crF4, crF5, crF6, crF7; - { crOffset, crF0, crF1, crF2, crF3, - crF4, crF5, crF6, crF7} in - { Global.STEP32, Global.BYTE_FACTOR[0], Global.BYTE_FACTOR[1], Global.BYTE_FACTOR[2], Global.BYTE_FACTOR[3], - Global.BYTE_FACTOR[4], Global.BYTE_FACTOR[5], Global.BYTE_FACTOR[6], Global.BYTE_FACTOR[7] }; + [ crOffset, crF0, crF1, crF2, crF3, + crF4, crF5, crF6, crF7] in + [ Global.STEP32, Global.BYTE_FACTOR[0], Global.BYTE_FACTOR[1], Global.BYTE_FACTOR[2], Global.BYTE_FACTOR[3], + Global.BYTE_FACTOR[4], Global.BYTE_FACTOR[5], Global.BYTE_FACTOR[6], Global.BYTE_FACTOR[7] ]; pol commit crV0, crV1, crV2, crV3, crV4, crV5, crV6, crV7; diff --git a/test_data/polygon-hermez/storage.pil b/test_data/polygon-hermez/storage.pil index 2ce9f0eb8..1dcb8ce31 100644 --- a/test_data/polygon-hermez/storage.pil +++ b/test_data/polygon-hermez/storage.pil @@ -175,13 +175,13 @@ namespace Storage(%N); level3' = setLevel*(op3-level3) + iRotateLevel*(rotatedLevel3-level3) + level3; // Instruction that guarantees that op = hash(hl, hr); the poseidon SM will do the work; the result will be feeded by free - iHash { + iHash $ [ 0, 0, 1, hashLeft0, hashLeft1, hashLeft2, hashLeft3, hashRight0, hashRight1, hashRight2, hashRight3, iHashType, 0, 0, 0, op0, op1, op2, op3 - } is PoseidonG.result3 { + ] is PoseidonG.result3 $ [ PoseidonG.result1, PoseidonG.result2, PoseidonG.result3, PoseidonG.in0, PoseidonG.in1, @@ -198,7 +198,7 @@ namespace Storage(%N); PoseidonG.hash0, PoseidonG.hash1, PoseidonG.hash2, - PoseidonG.hash3}; + PoseidonG.hash3]; pol climbedKey0 = (level0*(rkey0*2 + rkeyBit - rkey0) + rkey0); pol climbedKey1 = (level1*(rkey1*2 + rkeyBit - rkey1) + rkey1); @@ -266,19 +266,19 @@ namespace Storage(%N); pol constant rSetValueHigh; pol constant rSetValueLow; - { + [ iHash, iHashType, iLatchGet, iLatchSet, iClimbRkey, iClimbSiblingRkey, iClimbSiblingRkeyN, iRotateLevel, iJmpz, iJmp, iConst0, iConst1, iConst2, iConst3, iAddress, pc, inFree, inNewRoot, inOldRoot, inRkey, inRkeyBit, inSiblingRkey, inSiblingValueHash, setHashLeft, setHashRight, setLevel, setNewRoot, setOldRoot, setRkey, setRkeyBit, setSiblingRkey, setSiblingValueHash, setValueHigh, setValueLow - } + ] in - { + [ rHash, rHashType, rLatchGet, rLatchSet, rClimbRkey, rClimbSiblingRkey, rClimbSiblingRkeyN, rRotateLevel, rJmpz, rJmp, rConst0, rConst1, rConst2, rConst3, rAddress, rLine, rInFree, rInNewRoot, rInOldRoot, rInRkey, rInRkeyBit, rInSiblingRkey, rInSiblingValueHash, rSetHashLeft, rSetHashRight, rSetLevel, rSetNewRoot, rSetOldRoot, rSetRkey, rSetRkeyBit, rSetSiblingRkey, rSetSiblingValueHash, rSetValueHigh, rSetValueLow - }; + ];