From 0dc3ae762f40bd34d4dbbfdf419ff63b19fca749 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gast=C3=B3n=20Zanitti?= Date: Fri, 23 Aug 2024 04:39:50 -0300 Subject: [PATCH] Depreciation of `.` by `::` in paths (#1694) --- analysis/README.md | 6 +- ast/src/analyzed/display.rs | 14 +- ast/src/parsed/asm.rs | 22 +-- ast/src/parsed/display.rs | 10 +- backend/src/composite/split.rs | 2 +- backend/src/estark/json_exporter/mod.rs | 6 +- backend/src/estark/mod.rs | 6 +- executor/src/constant_evaluator/mod.rs | 72 ++++----- executor/src/witgen/block_processor.rs | 2 +- .../machines/double_sorted_witness_machine.rs | 8 +- .../src/witgen/machines/machine_extractor.rs | 2 +- linker/src/lib.rs | 38 ++--- parser/src/lib.rs | 8 +- pil-analyzer/src/condenser.rs | 7 +- pil-analyzer/src/evaluator.rs | 20 +-- pil-analyzer/src/lib.rs | 4 +- pil-analyzer/src/pil_analyzer.rs | 8 +- pil-analyzer/src/statement_processor.rs | 6 +- pil-analyzer/src/type_inference.rs | 2 +- pil-analyzer/tests/condenser.rs | 86 +++++------ pil-analyzer/tests/parse_display.rs | 138 +++++++++--------- pil-analyzer/tests/side_effects.rs | 2 +- pilopt/src/lib.rs | 51 +++---- pipeline/tests/asm.rs | 8 +- pipeline/tests/pil.rs | 30 ++-- pipeline/tests/powdr_std.rs | 2 +- riscv/benches/executor_benchmark.rs | 2 +- riscv/src/continuations.rs | 30 ++-- riscv/src/continuations/bootloader.rs | 36 ++--- test_data/pil/block_lookup_or.pil | 2 +- test_data/pil/block_lookup_or_permutation.pil | 4 +- test_data/pil/different_degrees.pil | 2 +- test_data/pil/pair_lookup.pil | 4 +- test_data/pil/single_line_blocks.pil | 2 +- test_data/pil/two_block_machine_functions.pil | 10 +- test_data/pil/vm_to_block_dynamic_length.pil | 26 ++-- 36 files changed, 332 insertions(+), 346 deletions(-) diff --git a/analysis/README.md b/analysis/README.md index df386cabc3..81823ed519 100644 --- a/analysis/README.md +++ b/analysis/README.md @@ -616,9 +616,9 @@ 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); diff --git a/ast/src/analyzed/display.rs b/ast/src/analyzed/display.rs index 09193af917..50321604ba 100644 --- a/ast/src/analyzed/display.rs +++ b/ast/src/analyzed/display.rs @@ -452,22 +452,12 @@ impl Display for AlgebraicReference { impl Display for PolynomialReference { fn fmt(&self, f: &mut Formatter<'_>) -> Result { + write!(f, "{}", self.name)?; if let Some(type_args) = &self.type_args { if !type_args.is_empty() { - // We need to add a `::`-component, so the name should not contain a `.`. - // NOTE: This special handling can be removed once we remove - // the `to_dotted_string` function. - let name = if self.name.contains('.') { - // Re-format the name with ``::`-separators. - SymbolPath::from_str(&self.name).unwrap().to_string() - } else { - self.name.clone() - }; - write!(f, "{name}::{}", format_type_args(type_args))?; - return Ok(()); + write!(f, "::{}", format_type_args(type_args))?; } } - write!(f, "{}", self.name)?; Ok(()) } diff --git a/ast/src/parsed/asm.rs b/ast/src/parsed/asm.rs index 4be84ab28a..3f066c4a80 100644 --- a/ast/src/parsed/asm.rs +++ b/ast/src/parsed/asm.rs @@ -162,13 +162,6 @@ impl SymbolPath { self } - /// Formats the path and uses `.` as separator if - /// there are at most two components. - pub fn to_dotted_string(&self) -> String { - let separator = if self.parts.len() <= 2 { "." } else { "::" }; - self.parts.iter().format(separator).to_string() - } - pub fn try_to_identifier(&self) -> Option<&String> { match &self.parts[..] { [Part::Named(name)] => Some(name), @@ -207,14 +200,10 @@ impl SymbolPath { impl FromStr for SymbolPath { type Err = String; - /// Parses a symbol path both in the "a.b" and the "a::b" notation. + /// Parses a symbol path using the "::" notation. fn from_str(s: &str) -> Result { - let (dots, double_colons) = (s.matches('.').count(), s.matches("::").count()); - if dots != 0 && double_colons != 0 { - Err(format!("Path mixes \"::\" and \".\" separators: {s}"))? - } let parts = s - .split(if double_colons > 0 { "::" } else { "." }) + .split("::") .map(|s| { if s == "super" { Part::Super @@ -361,13 +350,6 @@ impl AbsoluteSymbolPath { parts.push(part.to_string()); Self { parts } } - - /// Formats the path without leading `::` and uses `.` as separator if - /// there are at most two components. - pub fn to_dotted_string(&self) -> String { - let separator = if self.parts.len() <= 2 { "." } else { "::" }; - self.parts.join(separator) - } } impl Display for AbsoluteSymbolPath { diff --git a/ast/src/parsed/display.rs b/ast/src/parsed/display.rs index e76bf890e6..5aff3bae1a 100644 --- a/ast/src/parsed/display.rs +++ b/ast/src/parsed/display.rs @@ -743,7 +743,7 @@ impl Display for NamespacedPolynomialReference { if let Some(type_args) = &self.type_args { write!(f, "{}::{}", self.path, format_type_args(type_args)) } else { - write!(f, "{}", self.path.to_dotted_string()) + write!(f, "{}", self.path) } } } @@ -1216,12 +1216,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/backend/src/composite/split.rs b/backend/src/composite/split.rs index 0bd83d0c76..631e0057c3 100644 --- a/backend/src/composite/split.rs +++ b/backend/src/composite/split.rs @@ -63,7 +63,7 @@ pub(crate) fn machine_witness_columns( panic!("Machine {machine_name} has witness columns of different sizes") } }); - let dummy_column_name = format!("{machine_name}.{DUMMY_COLUMN_NAME}"); + let dummy_column_name = format!("{machine_name}::{DUMMY_COLUMN_NAME}"); let dummy_column = vec![F::zero(); size]; iter::once((dummy_column_name, dummy_column)) .chain(machine_columns.into_iter().cloned()) diff --git a/backend/src/estark/json_exporter/mod.rs b/backend/src/estark/json_exporter/mod.rs index 9b5b56e7b5..b94e403070 100644 --- a/backend/src/estark/json_exporter/mod.rs +++ b/backend/src/estark/json_exporter/mod.rs @@ -194,10 +194,8 @@ fn polynomial_reference_type_to_type(t: &str) -> &'static str { /// Makes names compatible with estark, which sometimes require that /// there is exactly one `.` in the name. fn fixup_name(name: &str) -> String { - if name.contains('.') { - name.to_string() - } else if let Some(last) = name.rfind("::") { - format!("{}.{}", &name[..last], &name[last + 1..]) + if let Some(last) = name.rfind("::") { + format!("{}.{}", &name[..last], &name[last + 2..]) } else { panic!("Witness or intermediate column is not inside a namespace: {name}"); } diff --git a/backend/src/estark/mod.rs b/backend/src/estark/mod.rs index 6677b52074..57db1add25 100644 --- a/backend/src/estark/mod.rs +++ b/backend/src/estark/mod.rs @@ -74,7 +74,7 @@ type Fixed = Vec<(String, Vec)>; /// eStark provers require a fixed column with the equivalent semantics to /// Polygon zkEVM's `L1` column. Powdr generated PIL will always have -/// `main.first_step`, but directly given PIL may not have it. This is a fixup +/// `main::first_step`, but directly given PIL may not have it. This is a fixup /// to inject such column if it doesn't exist. /// /// TODO Improve how this is done. @@ -86,7 +86,7 @@ fn first_step_fixup( let mut pil: PIL = json_exporter::export(pil); - let patched_constants = if !fixed.iter().any(|(k, _)| k == "main.first_step") { + let patched_constants = if !fixed.iter().any(|(k, _)| k == "main::first_step") { use starky::types::Reference; pil.nConstants += 1; pil.references.insert( @@ -125,7 +125,7 @@ struct EStarkFilesCommon { degree: DegreeType, pil: PIL, /// If this field is present, it means the constants were patched with - /// "main.first_step" column and must be written again to a file. + /// "main::first_step" column and must be written again to a file. constants: Arc>, output_dir: Option, proof_type: ProofType, diff --git a/executor/src/constant_evaluator/mod.rs b/executor/src/constant_evaluator/mod.rs index 30f0a5b2f4..2b109e4c9c 100644 --- a/executor/src/constant_evaluator/mod.rs +++ b/executor/src/constant_evaluator/mod.rs @@ -242,7 +242,7 @@ mod test { let constants = generate(&analyzed); assert_eq!( constants, - vec![("F.LAST".to_string(), convert(vec![0, 0, 0, 0, 0, 0, 0, 1]))] + vec![("F::LAST".to_string(), convert(vec![0, 0, 0, 0, 0, 0, 0, 1]))] ); } @@ -259,7 +259,7 @@ mod test { assert_eq!( constants, vec![( - "F.EVEN".to_string(), + "F::EVEN".to_string(), convert(vec![2, 4, 6, 8, 10, 12, 14, 16]) )] ); @@ -278,7 +278,7 @@ mod test { assert_eq!( constants, vec![( - "F.X".to_string(), + "F::X".to_string(), convert((0..8).map(|i| i ^ (i + 17) | 3).collect()) )] ); @@ -301,7 +301,7 @@ mod test { let constants = generate(&analyzed); assert_eq!( constants, - vec![("F.X".to_string(), convert(vec![8, 5, 5, 10, 5, 3, 5, 5]))] + vec![("F::X".to_string(), convert(vec![8, 5, 5, 10, 5, 3, 5, 5]))] ); } @@ -317,7 +317,7 @@ mod test { let constants = generate(&analyzed); assert_eq!( constants, - vec![("F.X".to_string(), convert(vec![7, 7, 7, 9, 9, 9, 9, 9]))] + vec![("F::X".to_string(), convert(vec![7, 7, 7, 9, 9, 9, 9, 9]))] ); } @@ -335,7 +335,7 @@ mod test { assert_eq!( constants, vec![( - "F.EVEN".to_string(), + "F::EVEN".to_string(), convert(vec![0, 2, 4, 6, 8, 10, 12, 14]) )] ); @@ -361,26 +361,29 @@ mod test { assert_eq!(constants.len(), 4); assert_eq!( constants[0], - ("F.seq".to_string(), convert((0..=9i32).collect::>())) + ( + "F::seq".to_string(), + convert((0..=9i32).collect::>()) + ) ); assert_eq!( constants[1], ( - "F.double_plus_one".to_string(), + "F::double_plus_one".to_string(), convert([1i32, 3, 5, 7, 9, 1, 3, 5, 7, 9].to_vec()) ) ); assert_eq!( constants[2], ( - "F.half_nibble".to_string(), + "F::half_nibble".to_string(), convert([0i32, 1, 2, 3, 4, 5, 6, 7, 0, 1].to_vec()) ) ); assert_eq!( constants[3], ( - "F.doubled_half_nibble".to_string(), + "F::doubled_half_nibble".to_string(), convert([0i32, 0, 1, 1, 2, 2, 3, 3, 4, 4].to_vec()) ) ); @@ -404,18 +407,18 @@ mod test { assert_eq!( constants[0], ( - "F.alt".to_string(), + "F::alt".to_string(), convert([0i32, 1, 0, 1, 0, 1, 0, 0, 0, 0].to_vec()) ) ); assert_eq!( constants[1], - ("F.empty".to_string(), convert([0i32; 10].to_vec())) + ("F::empty".to_string(), convert([0i32; 10].to_vec())) ); assert_eq!( constants[2], ( - "F.ref_other".to_string(), + "F::ref_other".to_string(), convert([9i32, 21, 8, 0, 0, 0, 0, 0, 0, 0].to_vec()) ) ); @@ -435,7 +438,7 @@ mod test { assert_eq!( constants[0], ( - "F.arr".to_string(), + "F::arr".to_string(), convert([0i32, 1, 2, 0, 1, 2, 0, 1, 2, 7].to_vec()) ) ); @@ -468,53 +471,56 @@ mod test { let constants = generate(&analyzed); assert_eq!( constants[0], - ("F.or".to_string(), convert([0, 1, 1, 1, 1, 1].to_vec())) + ("F::or".to_string(), convert([0, 1, 1, 1, 1, 1].to_vec())) ); assert_eq!( constants[1], - ("F.and".to_string(), convert([0, 0, 0, 1, 0, 1].to_vec())) + ("F::and".to_string(), convert([0, 0, 0, 1, 0, 1].to_vec())) ); assert_eq!( constants[2], - ("F.not".to_string(), convert([1, 0, 1, 0, 0, 0].to_vec())) + ("F::not".to_string(), convert([1, 0, 1, 0, 0, 0].to_vec())) ); assert_eq!( constants[3], - ("F.less".to_string(), convert([1, 1, 1, 0, 0, 0].to_vec())) + ("F::less".to_string(), convert([1, 1, 1, 0, 0, 0].to_vec())) ); assert_eq!( constants[4], ( - "F.less_eq".to_string(), + "F::less_eq".to_string(), convert([1, 1, 1, 1, 0, 0].to_vec()) ) ); assert_eq!( constants[5], - ("F.eq".to_string(), convert([0, 0, 0, 1, 0, 0].to_vec())) + ("F::eq".to_string(), convert([0, 0, 0, 1, 0, 0].to_vec())) ); assert_eq!( constants[6], - ("F.not_eq".to_string(), convert([1, 1, 1, 0, 1, 1].to_vec())) + ( + "F::not_eq".to_string(), + convert([1, 1, 1, 0, 1, 1].to_vec()) + ) ); assert_eq!( constants[7], ( - "F.greater".to_string(), + "F::greater".to_string(), convert([0, 0, 0, 0, 1, 1].to_vec()) ) ); assert_eq!( constants[8], ( - "F.greater_eq".to_string(), + "F::greater_eq".to_string(), convert([0, 0, 0, 1, 1, 1].to_vec()) ) ); } #[test] - #[should_panic = "got `expr` when calling function F.w"] + #[should_panic = "got `expr` when calling function F::w"] fn calling_witness() { let src = r#" let N: int = 10; @@ -541,7 +547,7 @@ mod test { } #[test] - #[should_panic = "got `expr` when calling function F.y"] + #[should_panic = "got `expr` when calling function F::y"] fn forward_reference_to_array() { let src = r#" let N: int = 10; @@ -569,11 +575,11 @@ mod test { let constants = generate(&analyzed); assert_eq!( constants[0], - ("F.X".to_string(), convert([21, 22, 23, 24].to_vec())) + ("F::X".to_string(), convert([21, 22, 23, 24].to_vec())) ); assert_eq!( constants[1], - ("F.Y".to_string(), convert([20, 21, 22, 23].to_vec())) + ("F::Y".to_string(), convert([20, 21, 22, 23].to_vec())) ); } @@ -592,7 +598,7 @@ mod test { let constants = generate(&analyzed); assert_eq!( constants[0], - ("F.x".to_string(), convert([1, 2, 4, 8].to_vec())) + ("F::x".to_string(), convert([1, 2, 4, 8].to_vec())) ); } @@ -614,7 +620,7 @@ mod test { // sgn(p) * |p| % |q| assert_eq!( constants[0], - ("F.x".to_string(), convert([103, 97, 103, 97].to_vec())) + ("F::x".to_string(), convert([103, 97, 103, 97].to_vec())) ); } @@ -632,11 +638,11 @@ mod test { let constants = generate(&analyzed); assert_eq!( constants[0], - ("F.y[0]".to_string(), convert([0, 1, 2, 3].to_vec())) + ("F::y[0]".to_string(), convert([0, 1, 2, 3].to_vec())) ); assert_eq!( constants[1], - ("F.y[1]".to_string(), convert([1, 2, 3, 4].to_vec())) + ("F::y[1]".to_string(), convert([1, 2, 3, 4].to_vec())) ); } @@ -656,7 +662,7 @@ mod test { let constants = generate(&analyzed); assert_eq!( constants[0], - ("F.a".to_string(), convert([14, 15, 16, 17].to_vec())) + ("F::a".to_string(), convert([14, 15, 16, 17].to_vec())) ); } @@ -676,7 +682,7 @@ mod test { let constants = generate(&analyzed); assert_eq!( constants[0], - ("N.g".to_string(), convert([0, 1, 2, 3].to_vec())) + ("N::g".to_string(), convert([0, 1, 2, 3].to_vec())) ); } } diff --git a/executor/src/witgen/block_processor.rs b/executor/src/witgen/block_processor.rs index 03d889f602..293755a4c6 100644 --- a/executor/src/witgen/block_processor.rs +++ b/executor/src/witgen/block_processor.rs @@ -245,6 +245,6 @@ mod tests { (1-ISLAST) * (y' - (x + y)) = 0; "#; - solve_and_assert::(src, &[(7, "Fibonacci.y", 34)]); + solve_and_assert::(src, &[(7, "Fibonacci::y", 34)]); } } diff --git a/executor/src/witgen/machines/double_sorted_witness_machine.rs b/executor/src/witgen/machines/double_sorted_witness_machine.rs index 1f98e896d3..dbe34ad9a1 100644 --- a/executor/src/witgen/machines/double_sorted_witness_machine.rs +++ b/executor/src/witgen/machines/double_sorted_witness_machine.rs @@ -36,7 +36,7 @@ const OPERATION_ID_WRITE: u64 = 1; const OPERATION_ID_BOOTLOADER_WRITE: u64 = 2; fn split_column_name(name: &str) -> (&str, &str) { - let mut limbs = name.split('.'); + let mut limbs = name.split("::"); let namespace = limbs.next().unwrap(); let col = limbs.next().unwrap(); (namespace, col) @@ -79,7 +79,7 @@ struct Operation { impl<'a, T: FieldElement> DoubleSortedWitnesses<'a, T> { fn namespaced(&self, name: &str) -> String { - format!("{}.{}", self.namespace, name) + format!("{}::{}", self.namespace, name) } pub fn try_new( @@ -141,12 +141,12 @@ impl<'a, T: FieldElement> DoubleSortedWitnesses<'a, T> { // Now, we check that they both have the same range constraint and use it to determine // the base of the two digits. let upper_poly_id = - fixed_data.try_column_by_name(&format!("{namespace}.{}", DIFF_COLUMNS[0]))?; + fixed_data.try_column_by_name(&format!("{namespace}::{}", DIFF_COLUMNS[0]))?; let upper_range_constraint = fixed_data.global_range_constraints().witness_constraints [&upper_poly_id] .as_ref()?; let lower_poly_id = - fixed_data.try_column_by_name(&format!("{namespace}.{}", DIFF_COLUMNS[1]))?; + fixed_data.try_column_by_name(&format!("{namespace}::{}", DIFF_COLUMNS[1]))?; let lower_range_constraint = fixed_data.global_range_constraints().witness_constraints [&lower_poly_id] .as_ref()?; diff --git a/executor/src/witgen/machines/machine_extractor.rs b/executor/src/witgen/machines/machine_extractor.rs index 84b71aa086..7da6d8876f 100644 --- a/executor/src/witgen/machines/machine_extractor.rs +++ b/executor/src/witgen/machines/machine_extractor.rs @@ -100,7 +100,7 @@ pub fn split_out_machines<'a, T: FieldElement>( let first_witness = machine_witnesses.iter().next().unwrap(); let first_witness_name = fixed.column_name(first_witness); let namespace = first_witness_name - .rfind('.') + .rfind("::") .map(|idx| &first_witness_name[..idx]); // For machines compiled using Powdr ASM we'll always have a namespace, but as a last diff --git a/linker/src/lib.rs b/linker/src/lib.rs index b544b158c5..95e0c040ab 100644 --- a/linker/src/lib.rs +++ b/linker/src/lib.rs @@ -281,7 +281,7 @@ mod test { pol commit pc_update; pc_update = instr__jump_to_operation * _operation_id + instr__loop * pc + instr_return * 0 + (1 - (instr__jump_to_operation + instr__loop + instr_return)) * (pc + 1); pc' = (1 - first_step') * pc_update; - 1 $ [0, pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return] in main__rom.latch $ [main__rom.operation_id, main__rom.p_line, main__rom.p_instr__jump_to_operation, main__rom.p_instr__reset, main__rom.p_instr__loop, main__rom.p_instr_return]; + 1 $ [0, pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return] in main__rom::latch $ [main__rom::operation_id, main__rom::p_line, main__rom::p_instr__jump_to_operation, main__rom::p_instr__reset, main__rom::p_instr__loop, main__rom::p_instr_return]; namespace main__rom(4 + 4); pol constant p_line = [0, 1, 2] + [2]*; pol constant p_instr__jump_to_operation = [0, 1, 0] + [0]*; @@ -356,10 +356,10 @@ namespace main__rom(4 + 4); pc' = (1 - first_step') * pc_update; pol commit X_free_value; pol commit Y_free_value; - 1 $ [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 main__rom.latch $ [main__rom.operation_id, main__rom.p_line, main__rom.p_reg_write_X_A, main__rom.p_reg_write_Y_A, main__rom.p_instr_identity, main__rom.p_instr_one, main__rom.p_instr_nothing, main__rom.p_instr__jump_to_operation, main__rom.p_instr__reset, main__rom.p_instr__loop, main__rom.p_instr_return, main__rom.p_X_const, main__rom.p_X_read_free, main__rom.p_read_X_A, main__rom.p_read_X_pc, main__rom.p_Y_const, main__rom.p_Y_read_free, main__rom.p_read_Y_A, main__rom.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_nothing $ [3] in main_sub.instr_return $ [main_sub._operation_id]; - instr_one $ [4, Y] in main_sub.instr_return $ [main_sub._operation_id, main_sub._output_0]; + 1 $ [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 main__rom::latch $ [main__rom::operation_id, main__rom::p_line, main__rom::p_reg_write_X_A, main__rom::p_reg_write_Y_A, main__rom::p_instr_identity, main__rom::p_instr_one, main__rom::p_instr_nothing, main__rom::p_instr__jump_to_operation, main__rom::p_instr__reset, main__rom::p_instr__loop, main__rom::p_instr_return, main__rom::p_X_const, main__rom::p_X_read_free, main__rom::p_read_X_A, main__rom::p_read_X_pc, main__rom::p_Y_const, main__rom::p_Y_read_free, main__rom::p_read_Y_A, main__rom::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_nothing $ [3] in main_sub::instr_return $ [main_sub::_operation_id]; + instr_one $ [4, Y] in main_sub::instr_return $ [main_sub::_operation_id, main_sub::_output_0]; pol constant _linker_first_step(i) { if i == 0 { 1 } else { 0 } }; _linker_first_step * (_operation_id - 2) = 0; namespace main__rom(16); @@ -406,7 +406,7 @@ namespace main_sub(16); pc_update = instr__jump_to_operation * _operation_id + instr__loop * pc + instr_return * 0 + (1 - (instr__jump_to_operation + instr__loop + instr_return)) * (pc + 1); pc' = (1 - first_step') * pc_update; pol commit _output_0_free_value; - 1 $ [0, pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return, _output_0_const, _output_0_read_free, read__output_0_pc, read__output_0__input_0] in main_sub__rom.latch $ [main_sub__rom.operation_id, main_sub__rom.p_line, main_sub__rom.p_instr__jump_to_operation, main_sub__rom.p_instr__reset, main_sub__rom.p_instr__loop, main_sub__rom.p_instr_return, main_sub__rom.p__output_0_const, main_sub__rom.p__output_0_read_free, main_sub__rom.p_read__output_0_pc, main_sub__rom.p_read__output_0__input_0]; + 1 $ [0, pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return, _output_0_const, _output_0_read_free, read__output_0_pc, read__output_0__input_0] in main_sub__rom::latch $ [main_sub__rom::operation_id, main_sub__rom::p_line, main_sub__rom::p_instr__jump_to_operation, main_sub__rom::p_instr__reset, main_sub__rom::p_instr__loop, main_sub__rom::p_instr_return, main_sub__rom::p__output_0_const, main_sub__rom::p__output_0_read_free, main_sub__rom::p_read__output_0_pc, main_sub__rom::p_read__output_0__input_0]; namespace main_sub__rom(8); pol constant p_line = [0, 1, 2, 3, 4, 5] + [5]*; pol constant p__output_0_const = [0, 0, 0, 0, 1, 0] + [0]*; @@ -478,7 +478,7 @@ namespace main_sub__rom(8); 7 => std::prelude::Query::Input(0), _ => std::prelude::Query::None, }; - 1 $ [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 main__rom.latch $ [main__rom.operation_id, main__rom.p_line, main__rom.p_reg_write_X_A, main__rom.p_reg_write_X_CNT, main__rom.p_instr_jmpz, main__rom.p_instr_jmpz_param_l, main__rom.p_instr_jmp, main__rom.p_instr_jmp_param_l, main__rom.p_instr_dec_CNT, main__rom.p_instr_assert_zero, main__rom.p_instr__jump_to_operation, main__rom.p_instr__reset, main__rom.p_instr__loop, main__rom.p_instr_return, main__rom.p_X_const, main__rom.p_X_read_free, main__rom.p_read_X_A, main__rom.p_read_X_CNT, main__rom.p_read_X_pc]; + 1 $ [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 main__rom::latch $ [main__rom::operation_id, main__rom::p_line, main__rom::p_reg_write_X_A, main__rom::p_reg_write_X_CNT, main__rom::p_instr_jmpz, main__rom::p_instr_jmpz_param_l, main__rom::p_instr_jmp, main__rom::p_instr_jmp_param_l, main__rom::p_instr_dec_CNT, main__rom::p_instr_assert_zero, main__rom::p_instr__jump_to_operation, main__rom::p_instr__reset, main__rom::p_instr__loop, main__rom::p_instr_return, main__rom::p_X_const, main__rom::p_X_read_free, main__rom::p_read_X_A, main__rom::p_read_X_CNT, main__rom::p_read_X_pc]; pol constant _linker_first_step(i) { if i == 0 { 1 } else { 0 } }; _linker_first_step * (_operation_id - 2) = 0; namespace main__rom(16); @@ -550,7 +550,7 @@ machine Machine { pol commit pc_update; pc_update = instr_adjust_fp * instr_adjust_fp_param_t + instr__jump_to_operation * _operation_id + instr__loop * pc + instr_return * 0 + (1 - (instr_adjust_fp + instr__jump_to_operation + instr__loop + instr_return)) * (pc + 1); pc' = (1 - first_step') * pc_update; - 1 $ [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 main__rom.latch $ [main__rom.operation_id, main__rom.p_line, main__rom.p_instr_inc_fp, main__rom.p_instr_inc_fp_param_amount, main__rom.p_instr_adjust_fp, main__rom.p_instr_adjust_fp_param_amount, main__rom.p_instr_adjust_fp_param_t, main__rom.p_instr__jump_to_operation, main__rom.p_instr__reset, main__rom.p_instr__loop, main__rom.p_instr_return]; + 1 $ [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 main__rom::latch $ [main__rom::operation_id, main__rom::p_line, main__rom::p_instr_inc_fp, main__rom::p_instr_inc_fp_param_amount, main__rom::p_instr_adjust_fp, main__rom::p_instr_adjust_fp_param_amount, main__rom::p_instr_adjust_fp_param_t, main__rom::p_instr__jump_to_operation, main__rom::p_instr__reset, main__rom::p_instr__loop, main__rom::p_instr_return]; pol constant _linker_first_step(i) { if i == 0 { 1 } else { 0 } }; _linker_first_step * (_operation_id - 2) = 0; namespace main__rom(8); @@ -645,8 +645,8 @@ machine Main { pc_update = instr__jump_to_operation * _operation_id + instr__loop * pc + instr_return * 0 + (1 - (instr__jump_to_operation + instr__loop + instr_return)) * (pc + 1); pc' = (1 - first_step') * pc_update; pol commit X_free_value; - instr_add5_into_A $ [0, X, A'] in main_vm.latch $ [main_vm.operation_id, main_vm.x, main_vm.y]; - 1 $ [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 main__rom.latch $ [main__rom.operation_id, main__rom.p_line, main__rom.p_reg_write_X_A, main__rom.p_instr_add5_into_A, main__rom.p_instr__jump_to_operation, main__rom.p_instr__reset, main__rom.p_instr__loop, main__rom.p_instr_return, main__rom.p_X_const, main__rom.p_X_read_free, main__rom.p_read_X_A, main__rom.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]; + 1 $ [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 main__rom::latch $ [main__rom::operation_id, main__rom::p_line, main__rom::p_reg_write_X_A, main__rom::p_instr_add5_into_A, main__rom::p_instr__jump_to_operation, main__rom::p_instr__reset, main__rom::p_instr__loop, main__rom::p_instr_return, main__rom::p_X_const, main__rom::p_X_read_free, main__rom::p_read_X_A, main__rom::p_read_X_pc]; pol constant _linker_first_step(i) { if i == 0 { 1 } else { 0 } }; _linker_first_step * (_operation_id - 2) = 0; namespace main__rom(4); @@ -729,9 +729,9 @@ namespace main_vm; pol commit X_free_value; pol commit Y_free_value; pol commit Z_free_value; - instr_or_into_B $ [0, X, Y, B'] is main_bin.latch * main_bin.sel[0] $ [main_bin.operation_id, main_bin.A, main_bin.B, main_bin.C]; - 1 $ [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 main__rom.latch $ [main__rom.operation_id, main__rom.p_line, main__rom.p_reg_write_X_A, main__rom.p_reg_write_Y_A, main__rom.p_reg_write_Z_A, main__rom.p_reg_write_X_B, main__rom.p_reg_write_Y_B, main__rom.p_reg_write_Z_B, main__rom.p_instr_or, main__rom.p_instr_or_into_B, main__rom.p_instr_assert_eq, main__rom.p_instr__jump_to_operation, main__rom.p_instr__reset, main__rom.p_instr__loop, main__rom.p_instr_return, main__rom.p_X_const, main__rom.p_X_read_free, main__rom.p_read_X_A, main__rom.p_read_X_B, main__rom.p_read_X_pc, main__rom.p_Y_const, main__rom.p_Y_read_free, main__rom.p_read_Y_A, main__rom.p_read_Y_B, main__rom.p_read_Y_pc, main__rom.p_Z_const, main__rom.p_Z_read_free, main__rom.p_read_Z_A, main__rom.p_read_Z_B, main__rom.p_read_Z_pc]; - instr_or $ [0, X, Y, Z] is main_bin.latch * main_bin.sel[1] $ [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[0] $ [main_bin::operation_id, main_bin::A, main_bin::B, main_bin::C]; + 1 $ [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 main__rom::latch $ [main__rom::operation_id, main__rom::p_line, main__rom::p_reg_write_X_A, main__rom::p_reg_write_Y_A, main__rom::p_reg_write_Z_A, main__rom::p_reg_write_X_B, main__rom::p_reg_write_Y_B, main__rom::p_reg_write_Z_B, main__rom::p_instr_or, main__rom::p_instr_or_into_B, main__rom::p_instr_assert_eq, main__rom::p_instr__jump_to_operation, main__rom::p_instr__reset, main__rom::p_instr__loop, main__rom::p_instr_return, main__rom::p_X_const, main__rom::p_X_read_free, main__rom::p_read_X_A, main__rom::p_read_X_B, main__rom::p_read_X_pc, main__rom::p_Y_const, main__rom::p_Y_read_free, main__rom::p_read_Y_A, main__rom::p_read_Y_B, main__rom::p_read_Y_pc, main__rom::p_Z_const, main__rom::p_Z_read_free, main__rom::p_read_Z_A, main__rom::p_read_Z_B, main__rom::p_read_Z_pc]; + instr_or $ [0, X, Y, Z] 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(i) { if i == 0 { 1 } else { 0 } }; _linker_first_step * (_operation_id - 2) = 0; namespace main__rom(128); @@ -879,12 +879,12 @@ namespace main_bin(128); pol commit Y_free_value; pol commit Z_free_value; pol commit W_free_value; - instr_add_to_A $ [0, X, Y, A'] in main_submachine.latch $ [main_submachine.operation_id, main_submachine.x, main_submachine.y, main_submachine.z]; - instr_add_BC_to_A $ [0, B, C, A'] in main_submachine.latch $ [main_submachine.operation_id, main_submachine.x, main_submachine.y, main_submachine.z]; - 1 $ [0, pc, reg_write_X_A, reg_write_Y_A, reg_write_Z_A, reg_write_W_A, reg_write_X_B, reg_write_Y_B, reg_write_Z_B, reg_write_W_B, reg_write_X_C, reg_write_Y_C, reg_write_Z_C, reg_write_W_C, instr_add, instr_sub_with_add, instr_addAB, instr_add3, instr_add_to_A, instr_add_BC_to_A, instr_sub, instr_add_with_sub, 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_C, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_B, read_Y_C, read_Y_pc, Z_const, Z_read_free, read_Z_A, read_Z_B, read_Z_C, read_Z_pc, W_const, W_read_free, read_W_A, read_W_B, read_W_C, read_W_pc] in main__rom.latch $ [main__rom.operation_id, main__rom.p_line, main__rom.p_reg_write_X_A, main__rom.p_reg_write_Y_A, main__rom.p_reg_write_Z_A, main__rom.p_reg_write_W_A, main__rom.p_reg_write_X_B, main__rom.p_reg_write_Y_B, main__rom.p_reg_write_Z_B, main__rom.p_reg_write_W_B, main__rom.p_reg_write_X_C, main__rom.p_reg_write_Y_C, main__rom.p_reg_write_Z_C, main__rom.p_reg_write_W_C, main__rom.p_instr_add, main__rom.p_instr_sub_with_add, main__rom.p_instr_addAB, main__rom.p_instr_add3, main__rom.p_instr_add_to_A, main__rom.p_instr_add_BC_to_A, main__rom.p_instr_sub, main__rom.p_instr_add_with_sub, main__rom.p_instr_assert_eq, main__rom.p_instr__jump_to_operation, main__rom.p_instr__reset, main__rom.p_instr__loop, main__rom.p_instr_return, main__rom.p_X_const, main__rom.p_X_read_free, main__rom.p_read_X_A, main__rom.p_read_X_B, main__rom.p_read_X_C, main__rom.p_read_X_pc, main__rom.p_Y_const, main__rom.p_Y_read_free, main__rom.p_read_Y_A, main__rom.p_read_Y_B, main__rom.p_read_Y_C, main__rom.p_read_Y_pc, main__rom.p_Z_const, main__rom.p_Z_read_free, main__rom.p_read_Z_A, main__rom.p_read_Z_B, main__rom.p_read_Z_C, main__rom.p_read_Z_pc, main__rom.p_W_const, main__rom.p_W_read_free, main__rom.p_read_W_A, main__rom.p_read_W_B, main__rom.p_read_W_C, main__rom.p_read_W_pc]; - instr_add + instr_add3 + instr_addAB + instr_sub_with_add $ [0, X * instr_add + X * instr_add3 + A * instr_addAB + Y * instr_sub_with_add, Y * instr_add + Y * instr_add3 + B * instr_addAB + Z * instr_sub_with_add, Z * instr_add + tmp * instr_add3 + X * instr_addAB + X * instr_sub_with_add] in main_submachine.latch $ [main_submachine.operation_id, main_submachine.x, main_submachine.y, main_submachine.z]; - instr_add3 $ [0, tmp, Z, W] in main_submachine.latch $ [main_submachine.operation_id, main_submachine.x, main_submachine.y, main_submachine.z]; - instr_add_with_sub + instr_sub $ [1, Z * instr_add_with_sub + X * instr_sub, X * instr_add_with_sub + Y * instr_sub, Y * instr_add_with_sub + Z * instr_sub] in main_submachine.latch $ [main_submachine.operation_id, main_submachine.z, main_submachine.x, main_submachine.y]; + instr_add_to_A $ [0, X, Y, A'] in main_submachine::latch $ [main_submachine::operation_id, main_submachine::x, main_submachine::y, main_submachine::z]; + instr_add_BC_to_A $ [0, B, C, A'] in main_submachine::latch $ [main_submachine::operation_id, main_submachine::x, main_submachine::y, main_submachine::z]; + 1 $ [0, pc, reg_write_X_A, reg_write_Y_A, reg_write_Z_A, reg_write_W_A, reg_write_X_B, reg_write_Y_B, reg_write_Z_B, reg_write_W_B, reg_write_X_C, reg_write_Y_C, reg_write_Z_C, reg_write_W_C, instr_add, instr_sub_with_add, instr_addAB, instr_add3, instr_add_to_A, instr_add_BC_to_A, instr_sub, instr_add_with_sub, 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_C, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_B, read_Y_C, read_Y_pc, Z_const, Z_read_free, read_Z_A, read_Z_B, read_Z_C, read_Z_pc, W_const, W_read_free, read_W_A, read_W_B, read_W_C, read_W_pc] in main__rom::latch $ [main__rom::operation_id, main__rom::p_line, main__rom::p_reg_write_X_A, main__rom::p_reg_write_Y_A, main__rom::p_reg_write_Z_A, main__rom::p_reg_write_W_A, main__rom::p_reg_write_X_B, main__rom::p_reg_write_Y_B, main__rom::p_reg_write_Z_B, main__rom::p_reg_write_W_B, main__rom::p_reg_write_X_C, main__rom::p_reg_write_Y_C, main__rom::p_reg_write_Z_C, main__rom::p_reg_write_W_C, main__rom::p_instr_add, main__rom::p_instr_sub_with_add, main__rom::p_instr_addAB, main__rom::p_instr_add3, main__rom::p_instr_add_to_A, main__rom::p_instr_add_BC_to_A, main__rom::p_instr_sub, main__rom::p_instr_add_with_sub, main__rom::p_instr_assert_eq, main__rom::p_instr__jump_to_operation, main__rom::p_instr__reset, main__rom::p_instr__loop, main__rom::p_instr_return, main__rom::p_X_const, main__rom::p_X_read_free, main__rom::p_read_X_A, main__rom::p_read_X_B, main__rom::p_read_X_C, main__rom::p_read_X_pc, main__rom::p_Y_const, main__rom::p_Y_read_free, main__rom::p_read_Y_A, main__rom::p_read_Y_B, main__rom::p_read_Y_C, main__rom::p_read_Y_pc, main__rom::p_Z_const, main__rom::p_Z_read_free, main__rom::p_read_Z_A, main__rom::p_read_Z_B, main__rom::p_read_Z_C, main__rom::p_read_Z_pc, main__rom::p_W_const, main__rom::p_W_read_free, main__rom::p_read_W_A, main__rom::p_read_W_B, main__rom::p_read_W_C, main__rom::p_read_W_pc]; + instr_add + instr_add3 + instr_addAB + instr_sub_with_add $ [0, X * instr_add + X * instr_add3 + A * instr_addAB + Y * instr_sub_with_add, Y * instr_add + Y * instr_add3 + B * instr_addAB + Z * instr_sub_with_add, Z * instr_add + tmp * instr_add3 + X * instr_addAB + X * instr_sub_with_add] in main_submachine::latch $ [main_submachine::operation_id, main_submachine::x, main_submachine::y, main_submachine::z]; + instr_add3 $ [0, tmp, Z, W] in main_submachine::latch $ [main_submachine::operation_id, main_submachine::x, main_submachine::y, main_submachine::z]; + instr_add_with_sub + instr_sub $ [1, Z * instr_add_with_sub + X * instr_sub, X * instr_add_with_sub + Y * instr_sub, Y * instr_add_with_sub + Z * instr_sub] in main_submachine::latch $ [main_submachine::operation_id, main_submachine::z, main_submachine::x, main_submachine::y]; pol constant _linker_first_step(i) { if i == 0 { 1 } else { 0 } }; _linker_first_step * (_operation_id - 2) = 0; namespace main__rom(32); diff --git a/parser/src/lib.rs b/parser/src/lib.rs index f165c6a8f9..41be1ca7ab 100644 --- a/parser/src/lib.rs +++ b/parser/src/lib.rs @@ -485,12 +485,12 @@ namespace N(2); fn parse_impl() { let input = r#" impl Iterator, T> { - next: |it| if it.pos >= 7 { (it, none) } else { some((increment(it), it.arr[it.pos])) }, + next_max: |it, max| if pos(it) >= max { None } else { Some(increment(it)) }, }"#; let expected = r#" impl Iterator, T> { - next: (|it| if it.pos >= 7 { (it, none) } else { some((increment(it), it.arr[it.pos])) }), + next_max: (|it, max| if pos(it) >= max { None } else { Some(increment(it)) }), }"#; let printed = format!("{}", parse(Some("input"), input).unwrap_err_to_stderr()); @@ -501,12 +501,12 @@ namespace N(2); fn parse_impl2() { let input = r#" impl Iterator, B> { - next: |it| if it.pos >= 7 { (it, it.pos) } else { (it, 0) }, + next: |it, pm| if pos(it) >= val(pm) { (it, pos(it)) } else { (it, 0) }, }"#; let expected = r#" impl Iterator, B> { - next: (|it| if it.pos >= 7 { (it, it.pos) } else { (it, 0) }), + next: (|it, pm| if pos(it) >= val(pm) { (it, pos(it)) } else { (it, 0) }), }"#; let printed = format!("{}", parse(Some("input"), input).unwrap_err_to_stderr()); diff --git a/pil-analyzer/src/condenser.rs b/pil-analyzer/src/condenser.rs index e07f6bcd15..a4f1e218ee 100644 --- a/pil-analyzer/src/condenser.rs +++ b/pil-analyzer/src/condenser.rs @@ -554,7 +554,12 @@ impl<'a, T: FieldElement> Condenser<'a, T> { once(None) .chain((1..).map(Some)) .map(|cnt| format!("{name}{}", cnt.map(|c| format!("_{c}")).unwrap_or_default())) - .map(|name| self.namespace.with_part(&name).to_dotted_string()) + .map(|name| { + self.namespace + .with_part(&name) + .relative_to(&Default::default()) + .to_string() + }) .find(|name| !self.symbols.contains_key(name) && !self.new_symbols.contains(name)) .unwrap() } diff --git a/pil-analyzer/src/evaluator.rs b/pil-analyzer/src/evaluator.rs index 1bd7022f99..054dc58729 100644 --- a/pil-analyzer/src/evaluator.rs +++ b/pil-analyzer/src/evaluator.rs @@ -1306,7 +1306,7 @@ mod test { let src = r#"namespace Main(16); let x: int = 1 + 20; "#; - let result = parse_and_evaluate_symbol(src, "Main.x"); + let result = parse_and_evaluate_symbol(src, "Main::x"); assert_eq!(result, r#"21"#); } @@ -1316,7 +1316,7 @@ mod test { let x: int -> int = |i| match i { 0 => 0, _ => x(i - 1) + 1 }; let y = x(4); "#; - let result = parse_and_evaluate_symbol(src, "Main.y"); + let result = parse_and_evaluate_symbol(src, "Main::y"); assert_eq!(result, r#"4"#); } @@ -1334,7 +1334,7 @@ mod test { let map_array = |arr, f| [f(arr[0]), f(arr[1]), f(arr[2]), f(arr[3])]; let translated = map_array(words, translate); "#; - let result = parse_and_evaluate_symbol(src, "Main.translated"); + let result = parse_and_evaluate_symbol(src, "Main::translated"); assert_eq!(result, r#"["franz", "jagt", "mit", "dem"]"#); } @@ -1349,7 +1349,7 @@ mod test { let result = fib(20); "#; assert_eq!( - parse_and_evaluate_symbol(src, "Main.result"), + parse_and_evaluate_symbol(src, "Main::result"), "6765".to_string() ); } @@ -1363,7 +1363,7 @@ mod test { // If the lambda function returned by the expression f(99, ...) does not // properly capture the value of n in a closure, then f(1, ...) would return 1. assert_eq!( - parse_and_evaluate_symbol(src, "Main.result"), + parse_and_evaluate_symbol(src, "Main::result"), "99".to_string() ); } @@ -1379,8 +1379,8 @@ mod test { let empty: int[] = []; let y = std::array::len(empty); "#; - assert_eq!(parse_and_evaluate_symbol(src, "F.x"), "3".to_string()); - assert_eq!(parse_and_evaluate_symbol(src, "F.y"), "0".to_string()); + assert_eq!(parse_and_evaluate_symbol(src, "F::x"), "3".to_string()); + assert_eq!(parse_and_evaluate_symbol(src, "F::y"), "0".to_string()); } #[test] @@ -1395,7 +1395,7 @@ mod test { let arg: int = 1; let x: int[] = (|i| if i == 1 { std::check::panic(concat("this ", "text")) } else { [9] })(arg); "#; - parse_and_evaluate_symbol(src, "F.x"); + parse_and_evaluate_symbol(src, "F::x"); } #[test] @@ -1408,7 +1408,7 @@ mod test { namespace F(N); let x: int = std::check::panic("text"); "#; - parse_and_evaluate_symbol(src, "F.x"); + parse_and_evaluate_symbol(src, "F::x"); } #[test] @@ -1683,7 +1683,7 @@ mod test { let test = query || std::prover::eval(2 * (1 + 1 + 1) + 1); "#; assert_eq!( - evaluate_function::(src, "main.test"), + evaluate_function::(src, "main::test"), 7u64.into() ); } diff --git a/pil-analyzer/src/lib.rs b/pil-analyzer/src/lib.rs index 325a27721f..7743ad4634 100644 --- a/pil-analyzer/src/lib.rs +++ b/pil-analyzer/src/lib.rs @@ -28,7 +28,9 @@ pub use pil_analyzer::{analyze_ast, analyze_file, analyze_string}; pub trait AnalysisDriver: Clone + Copy { /// Turns a declaration into an absolute name. fn resolve_decl(&self, name: &String) -> String { - self.resolve_namespaced_decl(&[name]).to_dotted_string() + self.resolve_namespaced_decl(&[name]) + .relative_to(&Default::default()) + .to_string() } /// Turns a nested declaration into an absolute name. fn resolve_namespaced_decl(&self, path: &[&String]) -> AbsoluteSymbolPath; diff --git a/pil-analyzer/src/pil_analyzer.rs b/pil-analyzer/src/pil_analyzer.rs index fa02f0631b..8d08ba0dd7 100644 --- a/pil-analyzer/src/pil_analyzer.rs +++ b/pil-analyzer/src/pil_analyzer.rs @@ -345,7 +345,8 @@ impl PILAnalyzer { Some(sub_name) => self .driver() .resolve_namespaced_decl(&[name, sub_name]) - .to_dotted_string(), + .relative_to(&Default::default()) + .to_string(), }, symbol_category, ) @@ -451,7 +452,10 @@ impl<'a> AnalysisDriver for Driver<'a> { .iter_to_root() .chain(once(parse_absolute_path("::std::prelude"))) .find_map(|prefix| { - let path = prefix.join(path.clone()).to_dotted_string(); + let path = prefix + .join(path.clone()) + .relative_to(&Default::default()) + .to_string(); self.0.known_symbols.get(&path).map(|cat| (path, *cat)) }) } diff --git a/pil-analyzer/src/statement_processor.rs b/pil-analyzer/src/statement_processor.rs index b5ddbd655d..359cc1aeef 100644 --- a/pil-analyzer/src/statement_processor.rs +++ b/pil-analyzer/src/statement_processor.rs @@ -456,7 +456,8 @@ where absolute_name: self .driver .resolve_namespaced_decl(&[&name, &variant.name]) - .to_dotted_string(), + .relative_to(&Default::default()) + .to_string(), stage: None, kind: SymbolKind::Other(), length: None, @@ -484,7 +485,8 @@ where absolute_name: self .driver .resolve_namespaced_decl(&[&name, &function.name]) - .to_dotted_string(), + .relative_to(&Default::default()) + .to_string(), stage: None, kind: SymbolKind::Other(), length: None, diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index 473183f6d0..94098d77ae 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -845,7 +845,7 @@ impl TypeChecker { // is not helpful because the type is obvious from the value. let (ty, _generic_args) = self .unifier - .instantiate_scheme(self.declared_types[&name.to_dotted_string()].1.clone()); + .instantiate_scheme(self.declared_types[&name.to_string()].1.clone()); let ty = type_for_reference(&ty); match data { diff --git a/pil-analyzer/tests/condenser.rs b/pil-analyzer/tests/condenser.rs index 82ef6ec624..cc99236b7a 100644 --- a/pil-analyzer/tests/condenser.rs +++ b/pil-analyzer/tests/condenser.rs @@ -30,13 +30,13 @@ fn new_witness_column() { }); col witness x; col witness y; - let z: expr = N.new_wit(); + let z: expr = N::new_wit(); col witness x_1; - N.x_1 = N.y; - N.x_1 $ [N.x_1] in [N.even]; - let t: expr[] = N.new_wit_arr(); + N::x_1 = N::y; + 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; + N::x_2 = N::x_2; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -56,7 +56,7 @@ fn new_witness_column_name_clash() { col witness x; col witness x_1; col witness x_2; - N.x = N.x_1 + N.x_2; + N::x = N::x_1 + N::x_2; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -84,26 +84,26 @@ fn create_constraints() { let force_bool: expr -> std::prelude::Constr = (|c| c * (1 - c) = 0); let new_bool: -> expr = (constr || { let x: col; - N.force_bool(x); + N::force_bool(x); x }); let is_zero: expr -> expr = (constr |x| { let x_is_zero: col; - N.force_bool(x_is_zero); + N::force_bool(x_is_zero); let x_inv: col; x_is_zero = 1 - x * x_inv; x_is_zero * x = 0; x_is_zero }); col witness x; - let x_is_zero: expr = N.is_zero(N.x); + let x_is_zero: expr = N::is_zero(N::x); col witness y; col witness x_is_zero_1; col witness x_inv; - N.x_is_zero_1 * (1 - N.x_is_zero_1) = 0; - N.x_is_zero_1 = 1 - N.x * N.x_inv; - N.x_is_zero_1 * N.x = 0; - N.y = N.x_is_zero_1 + 2; + N::x_is_zero_1 * (1 - N::x_is_zero_1) = 0; + N::x_is_zero_1 = 1 - N::x * N::x_inv; + N::x_is_zero_1 * N::x = 0; + N::y = N::x_is_zero_1 + 2; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -129,7 +129,7 @@ namespace std::prover; namespace Main(8); let d: int = std::prover::degree(); col witness w; - Main.w = 8; + Main::w = 8; "#; assert_eq!(formatted, expected); } @@ -167,10 +167,10 @@ pub fn constructed_constraints() { col witness x; 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]; + 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]; "#; assert_eq!(formatted, expected); } @@ -187,14 +187,14 @@ fn next() { let expected = r#"namespace N(16); col witness x; col witness y; - N.x * N.y = 1; - N.x * N.y = 1 + N.x'; + N::x * N::y = 1; + N::x * N::y = 1 + N::x'; "#; assert_eq!(formatted, expected); } #[test] -#[should_panic = "Double application of \\\"'\\\" on: N.x"] +#[should_panic = "Double application of \\\"'\\\" on: N::x"] fn double_next() { let input = r#"namespace N(16); col witness x; @@ -221,16 +221,16 @@ fn new_fixed_column() { let even: col = (|i| i * 2); even }); - let ev: expr = N.f(); + let ev: expr = N::f(); col witness x; col fixed even(i) { i * 2 }; - N.x = N.even; + N::x = N::even; "#; assert_eq!(formatted, expected); } #[test] -#[should_panic = "Error creating fixed column N.fi: Lambda expression must not reference outer variables: (|i| (i + j) * 2)"] +#[should_panic = "Error creating fixed column N::fi: Lambda expression must not reference outer variables: (|i| (i + j) * 2)"] fn new_fixed_column_as_closure() { let input = r#"namespace N(16); let f = constr |j| { @@ -268,9 +268,9 @@ fn set_hint() { namespace N(16); col witness x; col witness y; - std::prelude::set_hint(N.y, (query |i| std::prelude::Query::Hint(std::prover::eval(N.x)))); + std::prelude::set_hint(N::y, (query |i| std::prelude::Query::Hint(std::prover::eval(N::x)))); col witness z; - std::prelude::set_hint(N.z, (query |_| std::prelude::Query::Hint(1))); + std::prelude::set_hint(N::z, (query |_| std::prelude::Query::Hint(1))); "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -291,7 +291,7 @@ fn set_hint_invalid_function() { } #[test] -#[should_panic = "Array elements are not supported for std::prelude::set_hint (called on N.x[0])."] +#[should_panic = "Array elements are not supported for std::prelude::set_hint (called on N::x[0])."] fn set_hint_array_element() { let input = r#" namespace std::prover; @@ -309,14 +309,14 @@ fn set_hint_array_element() { } namespace N(16); col witness x(_) query std::prelude::Query::Hint(1); - col witness y(i) query std::prelude::Query::Hint(std::prover::eval(N.x)); + col witness y(i) query std::prelude::Query::Hint(std::prover::eval(N::x)); "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); } #[test] -#[should_panic = "Expected reference to witness column as first argument for std::prelude::set_hint, but got intermediate column N.y."] +#[should_panic = "Expected reference to witness column as first argument for std::prelude::set_hint, but got intermediate column N::y."] fn set_hint_no_col() { let input = r#" namespace std::prover; @@ -330,7 +330,7 @@ fn set_hint_no_col() { } #[test] -#[should_panic = "Column N.x already has a hint set, but tried to add another one."] +#[should_panic = "Column N::x already has a hint set, but tried to add another one."] fn set_hint_twice() { let input = r#" namespace std::prover; @@ -344,7 +344,7 @@ fn set_hint_twice() { } #[test] -#[should_panic = "Column N.x already has a hint set, but tried to add another one."] +#[should_panic = "Column N::x already has a hint set, but tried to add another one."] fn set_hint_twice_in_constr() { let input = r#" namespace std::prover; @@ -384,20 +384,20 @@ fn set_hint_outside() { } namespace N(16); col witness x; - std::prelude::set_hint(N.x, (query |_| std::prelude::Query::Hint(8))); + std::prelude::set_hint(N::x, (query |_| std::prelude::Query::Hint(8))); col witness y; - std::prelude::set_hint(N.y, (query |_| std::prelude::Query::Hint(8))); + std::prelude::set_hint(N::y, (query |_| std::prelude::Query::Hint(8))); let create_wit: -> expr = (constr || { let w: col; w }); - let z: expr = N.create_wit(); + let z: expr = N::create_wit(); let set_hint: expr -> () = (constr |c| { std::prelude::set_hint(c, (query |_| std::prelude::Query::Hint(8))); }); col witness w; - std::prelude::set_hint(N.w, (query |_| std::prelude::Query::Hint(8))); + std::prelude::set_hint(N::w, (query |_| std::prelude::Query::Hint(8))); "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -414,8 +414,8 @@ fn intermediate_syntax() { assert_eq!(analyzed.intermediate_count(), 6); let expected = r#"namespace N(65536); col witness x[5]; - col inter = N.x[2]; - col inter_arr[5] = [N.x[0], N.x[1], N.x[2], N.x[3], N.x[4]]; + col inter = N::x[2]; + col inter_arr[5] = [N::x[0], N::x[1], N::x[2], N::x[3], N::x[4]]; "#; assert_eq!(analyzed.to_string(), expected); } @@ -435,10 +435,10 @@ fn intermediate_dynamic() { assert_eq!(analyzed.intermediate_count(), 6); let expected = r#"namespace N(65536); col witness x[5]; - col inte = N.x[2]; - col inter_arr[5] = [N.x[0], N.x[1], N.x[2], N.x[3], N.x[4]]; - N.inte = 8; - N.inter_arr[3] = 9; + col inte = N::x[2]; + col inter_arr[5] = [N::x[0], N::x[1], N::x[2], N::x[3], N::x[4]]; + N::inte = 8; + N::inter_arr[3] = 9; "#; assert_eq!(analyzed.to_string(), expected); } @@ -455,13 +455,13 @@ fn intermediate_arr_no_length() { assert_eq!(analyzed.intermediate_count(), 5); let expected = r#"namespace N(65536); col witness x[5]; - col inte[5] = [N.x[0], N.x[1], N.x[2], N.x[3], N.x[4]]; + col inte[5] = [N::x[0], N::x[1], N::x[2], N::x[3], N::x[4]]; "#; assert_eq!(analyzed.to_string(), expected); } #[test] -#[should_panic = "Error creating intermediate column array N.inte: Expected array of length 6 as value but it has 2 elements."] +#[should_panic = "Error creating intermediate column array N::inte: Expected array of length 6 as value but it has 2 elements."] fn intermediate_arr_wrong_length() { let input = r#"namespace N(65536); col witness x[2]; diff --git a/pil-analyzer/tests/parse_display.rs b/pil-analyzer/tests/parse_display.rs index a1ce4c6b52..77acd2571e 100644 --- a/pil-analyzer/tests/parse_display.rs +++ b/pil-analyzer/tests/parse_display.rs @@ -8,7 +8,7 @@ use pretty_assertions::assert_eq; fn parse_print_analyzed() { // This is rather a test for the Display trait than for the analyzer. let input = r#" let N: int = 65536; -public P = T.pc(2); +public P = T::pc(2); namespace Bin(65536); col witness bla; namespace std::prover(65536); @@ -22,16 +22,16 @@ namespace T(65536); col witness pc; col witness XInv; col witness XIsZero; - T.XIsZero = 1 - T.X * T.XInv; - T.XIsZero * T.X = 0; - T.XIsZero * (1 - T.XIsZero) = 0; + T::XIsZero = 1 - T::X * T::XInv; + T::XIsZero * T::X = 0; + T::XIsZero * (1 - T::XIsZero) = 0; col witness instr_jmpz; col witness instr_jmpz_param_l; col witness instr_jmp; col witness instr_jmp_param_l; col witness instr_dec_CNT; col witness instr_assert_zero; - T.instr_assert_zero * (T.XIsZero - 1) = 0; + T::instr_assert_zero * (T::XIsZero - 1) = 0; col witness X; col witness X_const; col witness X_read_free; @@ -42,12 +42,12 @@ namespace T(65536); col witness reg_write_X_CNT; col witness read_X_pc; col witness reg_write_X_A; - T.X = T.read_X_A * T.A + T.read_X_CNT * T.CNT + T.X_const + T.X_read_free * T.X_free_value; - T.A' = T.first_step' * 0 + T.reg_write_X_A * T.X + (1 - (T.first_step' + T.reg_write_X_A)) * T.A; + T::X = T::read_X_A * T::A + T::read_X_CNT * T::CNT + T::X_const + T::X_read_free * T::X_free_value; + T::A' = T::first_step' * 0 + T::reg_write_X_A * T::X + (1 - (T::first_step' + T::reg_write_X_A)) * T::A; col witness X_free_value; - std::prelude::set_hint(T.X_free_value, (query |_| match std::prover::eval(T.pc) { + std::prelude::set_hint(T::X_free_value, (query |_| match std::prover::eval(T::pc) { 0 => std::prelude::Query::Input(1), - 3 => std::prelude::Query::Input(std::convert::int::(std::prover::eval(T.CNT) + 1)), + 3 => std::prelude::Query::Input(std::convert::int::(std::prover::eval(T::CNT) + 1)), 7 => std::prelude::Query::Input(0), _ => std::prelude::Query::None, })); @@ -58,7 +58,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); @@ -73,8 +73,8 @@ fn intermediate() { "#; let expected = r#"namespace N(65536); col witness x; - col intermediate = N.x; - N.intermediate = N.intermediate; + col intermediate = N::x; + N::intermediate = N::intermediate; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -91,10 +91,10 @@ fn intermediate_array() { "#; let expected = r#"namespace N(65536); col witness x; - col intermediate[3] = [N.x, N.x + 2, N.x * N.x]; - N.intermediate[0] = N.intermediate[0]; - N.intermediate[1] = N.intermediate[1]; - N.intermediate[2] = N.intermediate[2]; + col intermediate[3] = [N::x, N::x + 2, N::x * N::x]; + N::intermediate[0] = N::intermediate[0]; + N::intermediate[1] = N::intermediate[1]; + N::intermediate[2] = N::intermediate[2]; "#; let analyzed = analyze_string::(input); assert_eq!(analyzed.intermediate_count(), 3); @@ -113,10 +113,10 @@ fn intermediate_nested() { "#; let expected = r#"namespace N(65536); col witness x; - col intermediate = N.x; - col int2 = N.intermediate; - col int3 = N.int2 + N.intermediate; - N.int3 = 2 * N.x; + col intermediate = N::x; + col int2 = N::intermediate; + col int3 = N::int2 + N::intermediate; + N::int3 = 2 * N::x; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -136,8 +136,8 @@ namespace N(r); namespace N(65536); col witness x; let z: int = 2; - col fixed t(i) { i + N.z }; - let other: int[] = [1, N.z]; + col fixed t(i) { i + N::z }; + let other: int[] = [1, N::z]; let other_fun: int, fe -> (int, (int -> int)) = (|i, j| (i + 7, (|k| k - i))); "#; let formatted = analyze_string::(input).to_string(); @@ -146,11 +146,11 @@ namespace N(65536); #[test] fn reparse_arrays() { - let input = r#"public out = N.y[1](2); + let input = r#"public out = N::y[1](2); namespace N(16); col witness y[3]; - N.y[1] - 2 = 0; - N.y[2]' - 2 = 0; + N::y[1] - 2 = 0; + N::y[2]' - 2 = 0; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, input); @@ -161,7 +161,7 @@ namespace N(16); fn no_direct_array_references() { let input = r#"namespace N(16); col witness y[3]; - (N.y - 2) = 0; + (N::y - 2) = 0; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, input); @@ -172,7 +172,7 @@ fn no_direct_array_references() { fn no_out_of_bounds() { let input = r#"namespace N(16); col witness y[3]; - (N.y[3] - 2) = 0; + (N::y[3] - 2) = 0; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, input); @@ -182,13 +182,13 @@ fn no_out_of_bounds() { fn namespaced_call() { let input = r#"namespace Assembly(2); let A: int -> int = (|i| 0); - let C = (|i| (Assembly.A((i + 2)) + 3)); - let D = (|i| Assembly.C((i + 3))); + let C = (|i| (Assembly::A((i + 2)) + 3)); + let D = (|i| Assembly::C((i + 3))); "#; let expected = r#"namespace Assembly(2); let A: int -> int = (|i| 0); - let C: int -> int = (|i| Assembly.A(i + 2) + 3); - let D: int -> int = (|i| Assembly.C(i + 3)); + let C: int -> int = (|i| Assembly::A(i + 2) + 3); + let D: int -> int = (|i| Assembly::C(i + 3)); "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -199,12 +199,12 @@ fn if_expr() { let input = r#"namespace Assembly(2); col fixed A = [0]*; let c = (|i| if (i < 3) { i } else { (i + 9) }); - col fixed D(i) { if (Assembly.c(i) != 0) { 3 } else { 2 } }; + col fixed D(i) { if (Assembly::c(i) != 0) { 3 } else { 2 } }; "#; let expected = r#"namespace Assembly(2); col fixed A = [0]*; let c: int -> int = (|i| if i < 3 { i } else { i + 9 }); - col fixed D(i) { if Assembly.c(i) != 0 { 3 } else { 2 } }; + col fixed D(i) { if Assembly::c(i) != 0 { 3 } else { 2 } }; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -224,13 +224,13 @@ fn symbolic_functions() { "#; let expected = r#"namespace N(16); let last_row: int = 15; - col fixed ISLAST(i) { if i == N.last_row { 1 } else { 0 } }; + col fixed ISLAST(i) { if i == N::last_row { 1 } else { 0 } }; col witness x; col witness y; let constrain_equal_expr: expr, expr -> expr = (|A, B| A - B); - let on_regular_row: expr -> expr = (|cond| (1 - N.ISLAST) * cond); - (1 - N.ISLAST) * (N.x' - N.y) = 0; - (1 - N.ISLAST) * (N.y' - (N.x + N.y)) = 0; + let on_regular_row: expr -> expr = (|cond| (1 - N::ISLAST) * cond); + (1 - N::ISLAST) * (N::x' - N::y) = 0; + (1 - N::ISLAST) * (N::y' - (N::x + N::y)) = 0; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -248,7 +248,7 @@ fn next_op_on_param() { col witness x; col witness y; let next_is_seven: expr -> expr = (|t| t' - 7); - N.y' - 7 = 0; + N::y' - 7 = 0; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -258,7 +258,7 @@ fn next_op_on_param() { fn fixed_symbolic() { let input = r#"namespace N(16); let last_row = 15; - let islast = |i| if i == N.last_row { 1 } else { 0 }; + let islast = |i| if i == N::last_row { 1 } else { 0 }; let ISLAST: col = |i| islast(i); let x; let y; @@ -266,11 +266,11 @@ fn fixed_symbolic() { "#; let expected = r#"namespace N(16); let last_row: int = 15; - let islast: int -> fe = (|i| if i == N.last_row { 1 } else { 0 }); - col fixed ISLAST(i) { N.islast(i) }; + let islast: int -> fe = (|i| if i == N::last_row { 1 } else { 0 }); + col fixed ISLAST(i) { N::islast(i) }; col witness x; col witness y; - N.x - N.ISLAST = 0; + N::x - N::ISLAST = 0; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -284,7 +284,7 @@ fn parentheses_lambda() { "#; let expected = r#"namespace N(16); let w: -> fe = (|| 2); - let x: fe = (|i| (|| N.w()))(N.w())(); + let x: fe = (|i| (|| N::w()))(N::w())(); "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -314,7 +314,7 @@ fn complex_type_resolution() { let f: int -> int = (|i| i + 10); let x: (int -> int), int -> int = (|k, i| k(2 ** i)); col witness y[14]; - let z: (((int -> int), int -> int)[], expr) = ([N.x, N.x, N.x, N.x, N.x, N.x, N.x, N.x], N.y[0]); + let z: (((int -> int), int -> int)[], expr) = ([N::x, N::x, N::x, N::x, N::x, N::x, N::x, N::x], N::y[0]); "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -346,8 +346,8 @@ fn expr_and_identity() { let g: expr -> std::prelude::Constr[] = (|x| [x = 0]); col witness x; col witness y; - N.x = N.y; - N.x = 0; + N::x = N::y; + N::x = 0; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, expected); @@ -358,7 +358,7 @@ fn expr_and_identity() { fn expression_but_expected_constraint() { let input = r#"namespace N(16); col witness y; - (N.y - 2); + (N::y - 2); "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, input); @@ -369,7 +369,7 @@ fn expression_but_expected_constraint() { 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); @@ -415,7 +415,7 @@ fn to_expr() { namespace N(16); let mul_two: int -> int = (|i| i * 2); col witness y; - N.y = N.y * 14; + N::y = N::y * 14; "#; assert_eq!(formatted, expected); } @@ -442,9 +442,9 @@ namespace std::array(16); namespace main(16); col witness x1[16]; col witness x2[16]; - let t: int = std::array::len::(main.x1); - let r: int = std::array::len::(main.x2); - main.x1[0] * 16 = main.x2[0] * 16; + let t: int = std::array::len::(main::x1); + let r: int = std::array::len::(main::x2); + main::x1[0] * 16 = main::x2[0] * 16; "#; assert_eq!(formatted, expected); } @@ -456,8 +456,8 @@ namespace Main(8); col witness x; col witness stage(2) y; col witness stage(1) z[4]; - Main.x = Main.y; - Main.z[0] = Main.x; + Main::x = Main::y; + Main::z[0] = Main::x; "; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, input); @@ -483,8 +483,8 @@ fn challenges() { col witness x; col witness stage(2) y; let a: expr = std::prelude::challenge(2, 1); - Main.x' = (Main.x + 1) * (1 - Main.first); - Main.y' = (Main.x + std::prelude::challenge(2, 1)) * (1 - Main.first); + Main::x' = (Main::x + 1) * (1 - Main::first); + Main::y' = (Main::x + std::prelude::challenge(2, 1)) * (1 - Main::first); "#; assert_eq!(formatted, expected); } @@ -512,14 +512,14 @@ fn let_inside_block() { let x: col; x }, - 1 => Main.w, + 1 => Main::w, _ => if i < 3 { let y: col; y - } else { Main.w }, + } else { Main::w }, }); col witness z; - Main.z = 9; + Main::z = 9; "; assert_eq!(formatted, expected); } @@ -745,7 +745,7 @@ namespace T(8); let expected = "namespace X; let y: int = 7; namespace T(8); - let k: int = X.y; + let k: int = X::y; "; let analyzed = analyze_string::(input); assert_eq!(expected, analyzed.to_string()); @@ -818,7 +818,7 @@ fn reparse_generic_function_call() { let inc: T -> T = (|x| x + 1); namespace N(16); let x: int = 7; - let y: int = X::inc::(N.x); + let y: int = X::inc::(N::x); "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, input); @@ -828,7 +828,7 @@ namespace N(16); fn reparse_non_function_fixed_cols() { let input = r#"namespace X(16); let A: int -> int = (|i| i); - let B: col = X.A; + let B: col = X::A; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, input); @@ -840,8 +840,8 @@ fn reparse_array_typed_fixed_col() { let len: T[] -> int = 19; namespace Main(16); let make_array: int, (int -> T) -> T[] = (|n, f| if n == 0 { [] } else { Main::make_array::(n - 1, f) + [f(n - 1)] }); - let nth_clock: int -> (int -> int) = (|k| (|i| if i % std::array::len::(Main.clocks) == k { 1 } else { 0 })); - let clocks: col[4] = Main::make_array::<(int -> int)>(4, Main.nth_clock); + let nth_clock: int -> (int -> int) = (|k| (|i| if i % std::array::len::(Main::clocks) == k { 1 } else { 0 })); + let clocks: col[4] = Main::make_array::<(int -> int)>(4, Main::nth_clock); "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, input); @@ -851,7 +851,7 @@ namespace Main(16); fn reparse_array_typed_intermediate_col() { let input = r#"namespace Main(16); col witness w; - col clocks[4] = [Main.w, Main.w, Main.w, Main.w]; + col clocks[4] = [Main::w, Main::w, Main::w, Main::w]; "#; let formatted = analyze_string::(input).to_string(); assert_eq!(formatted, input); @@ -882,10 +882,10 @@ fn intermediate_syntax() { "#; let expected = r#"namespace X(16); col witness w; - col a = X.w; - col b[1] = [X.w]; - col c = X.w; - col d[1] = [X.w]; + col a = X::w; + col b[1] = [X::w]; + col c = X::w; + col d[1] = [X::w]; "#; let analyzed = analyze_string::(input); assert_eq!(analyzed.intermediate_count(), 4); diff --git a/pil-analyzer/tests/side_effects.rs b/pil-analyzer/tests/side_effects.rs index a9431a6767..6ebc6ef79e 100644 --- a/pil-analyzer/tests/side_effects.rs +++ b/pil-analyzer/tests/side_effects.rs @@ -61,7 +61,7 @@ fn call_eval_in_query() { } #[test] -#[should_panic = "Referenced a constr function inside a query context: N.new_wit"] +#[should_panic = "Referenced a constr function inside a query context: N::new_wit"] fn call_constr_in_query() { let input = r#" namespace std::prover(16); diff --git a/pilopt/src/lib.rs b/pilopt/src/lib.rs index aa8f6a7dbd..cccb7e8c2d 100644 --- a/pilopt/src/lib.rs +++ b/pilopt/src/lib.rs @@ -150,10 +150,7 @@ impl ReferencedSymbols for Expression { impl ReferencedSymbols for Type { fn symbols(&self) -> Box> + '_> { - Box::new( - self.contained_named_types() - .map(|n| n.to_dotted_string().into()), - ) + Box::new(self.contained_named_types().map(|n| n.to_string().into())) } } @@ -587,8 +584,8 @@ mod test { let expectation = r#"namespace N(65536); col witness X; col witness Y; - N.X = N.Y; - N.Y = 7 * N.X; + N::X = N::Y; + N::Y = 7 * N::X; "#; let optimized = optimize(analyze_string::(input)).to_string(); assert_eq!(optimized, expectation); @@ -616,13 +613,13 @@ 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.X = 0; - (1 - N.A) * N.Y = 1; - N.Z = (1 + N.A) * 2; - N.A = 1 + N.A; - N.Z = 1 + N.A; + 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; + N::A = 1 + N::A; + N::Z = 1 + N::A; "#; let optimized = optimize(analyze_string::(input)).to_string(); assert_eq!(optimized, expectation); @@ -637,8 +634,8 @@ mod test { "#; let expectation = r#"namespace N(65536); col witness x; - col intermediate = N.x; - N.intermediate = N.intermediate; + col intermediate = N::x; + N::intermediate = N::intermediate; "#; let optimized = optimize(analyze_string::(input)).to_string(); assert_eq!(optimized, expectation); @@ -660,8 +657,8 @@ mod test { namespace N(65536); col witness x[1]; col witness y[0]; - col fixed t(i) { std::array::len::(N.y) }; - N.x[0] = N.t; + col fixed t(i) { std::array::len::(N::y) }; + N::x[0] = N::t; "#; let optimized = optimize(analyze_string::(input)).to_string(); assert_eq!(optimized, expectation); @@ -687,10 +684,10 @@ namespace N(65536); 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 * (N::x - 1) = 0; + [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); @@ -714,9 +711,9 @@ namespace N(65536); "#; let expectation = r#"namespace N(65536); col witness x; - col fixed cnt(i) { N.inc(i) }; + 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); @@ -731,8 +728,8 @@ namespace N(65536); "#; let expectation = r#"namespace N(65536); col witness x[5]; - col inte[5] = [N.x[0], N.x[1], N.x[2], N.x[3], N.x[4]]; - N.x[2] = N.inte[4]; + col inte[5] = [N::x[0], N::x[1], N::x[2], N::x[3], N::x[4]]; + N::x[2] = N::inte[4]; "#; let optimized = optimize(analyze_string::(input)); assert_eq!(optimized.intermediate_count(), 5); @@ -767,9 +764,9 @@ namespace N(65536); T, } let t: N::X[] -> int = (|r| 1); - col fixed f(i) { if i == 0 { N.t([]) } else { (|x| 1)(N::Y::F([])) } }; + col fixed f(i) { if i == 0 { N::t([]) } else { (|x| 1)(N::Y::F([])) } }; col witness x; - N.x = N.f; + N::x = N::f; "#; let optimized = optimize(analyze_string::(input)).to_string(); assert_eq!(optimized, expectation); diff --git a/pipeline/tests/asm.rs b/pipeline/tests/asm.rs index 906290d283..6c354c862c 100644 --- a/pipeline/tests/asm.rs +++ b/pipeline/tests/asm.rs @@ -78,7 +78,7 @@ fn mem_write_once_external_write() { let pipeline = make_prepared_pipeline( f, Default::default(), - vec![("main_memory.value".to_string(), mem)], + vec![("main_memory::value".to_string(), mem)], ); test_pilcom(pipeline); } @@ -214,9 +214,9 @@ fn dynamic_vadcop() { .collect::>(); // Spot-check some witness columns to have the expected length. - assert_eq!(witness_by_name["main.X"].len(), 128); - assert_eq!(witness_by_name["main_arith.y"].len(), 32); - assert_eq!(witness_by_name["main_memory.m_addr"].len(), 32); + assert_eq!(witness_by_name["main::X"].len(), 128); + assert_eq!(witness_by_name["main_arith::y"].len(), 32); + assert_eq!(witness_by_name["main_memory::m_addr"].len(), 32); // Because machines have different lengths, this can only be proven // with a composite proof. diff --git a/pipeline/tests/pil.rs b/pipeline/tests/pil.rs index 43ceef2f32..c21c93df51 100644 --- a/pipeline/tests/pil.rs +++ b/pipeline/tests/pil.rs @@ -15,7 +15,7 @@ use test_log::test; #[test] fn invalid_witness() { let f = "pil/trivial.pil"; - let witness = vec![("main.w".to_string(), vec![0; 4])]; + let witness = vec![("main::w".to_string(), vec![0; 4])]; assert_proofs_fail_for_invalid_witnesses(f, &witness); } @@ -34,7 +34,7 @@ fn lookup_with_selector() { Pipeline::default() .from_file(resolve_test_file(f)) .set_witness(vec![( - "main.w".to_string(), + "main::w".to_string(), witness.iter().cloned().map(Bn254Field::from).collect(), )]) .with_backend(powdr_backend::BackendType::Halo2Mock, None) @@ -43,7 +43,7 @@ fn lookup_with_selector() { } // Invalid witness: 0 is not in the set {2, 4} - let witness = vec![("main.w".to_string(), vec![0, 42, 4, 17])]; + let witness = vec![("main::w".to_string(), vec![0, 42, 4, 17])]; assert_proofs_fail_for_invalid_witnesses_halo2(f, &witness); assert_proofs_fail_for_invalid_witnesses_pilcom(f, &witness); // Unfortunately, eStark panics in this case. That's why the test is marked @@ -66,7 +66,7 @@ fn permutation_with_selector() { Pipeline::default() .from_file(resolve_test_file(f)) .set_witness(vec![( - "main.w".to_string(), + "main::w".to_string(), witness.iter().cloned().map(Bn254Field::from).collect(), )]) .with_backend(powdr_backend::BackendType::Halo2Mock, None) @@ -75,7 +75,7 @@ fn permutation_with_selector() { } // Invalid witness: 0 is not in the set {2, 4} - let witness = vec![("main.w".to_string(), vec![0, 42, 4, 17])]; + let witness = vec![("main::w".to_string(), vec![0, 42, 4, 17])]; assert_proofs_fail_for_invalid_witnesses_halo2(f, &witness); assert_proofs_fail_for_invalid_witnesses_pilcom(f, &witness); // Unfortunately, eStark panics in this case. That's why the test is marked @@ -98,8 +98,8 @@ fn fibonacci_invalid_witness() { // The following constraint should fail in row 1: // (1-ISLAST) * (x' - y) = 0; let witness = vec![ - ("Fibonacci.x".to_string(), vec![1, 1, 10, 3]), - ("Fibonacci.y".to_string(), vec![1, 2, 3, 13]), + ("Fibonacci::x".to_string(), vec![1, 1, 10, 3]), + ("Fibonacci::y".to_string(), vec![1, 2, 3, 13]), ]; assert_proofs_fail_for_invalid_witnesses(f, &witness); @@ -107,8 +107,8 @@ fn fibonacci_invalid_witness() { // The following constraint should fail in row 3: // ISLAST * (y' - 1) = 0; let witness = vec![ - ("Fibonacci.x".to_string(), vec![1, 2, 3, 5]), - ("Fibonacci.y".to_string(), vec![2, 3, 5, 8]), + ("Fibonacci::x".to_string(), vec![1, 2, 3, 5]), + ("Fibonacci::y".to_string(), vec![2, 3, 5, 8]), ]; assert_proofs_fail_for_invalid_witnesses(f, &witness); } @@ -136,7 +136,7 @@ fn external_witgen_fails_if_none_provided() { #[test] fn external_witgen_a_provided() { let f = "pil/external_witgen.pil"; - let external_witness = vec![("main.a".to_string(), vec![GoldilocksField::from(3); 16])]; + let external_witness = vec![("main::a".to_string(), vec![GoldilocksField::from(3); 16])]; let pipeline = make_prepared_pipeline(f, Default::default(), external_witness); test_pilcom(pipeline); } @@ -144,7 +144,7 @@ fn external_witgen_a_provided() { #[test] fn external_witgen_b_provided() { let f = "pil/external_witgen.pil"; - let external_witness = vec![("main.b".to_string(), vec![GoldilocksField::from(4); 16])]; + let external_witness = vec![("main::b".to_string(), vec![GoldilocksField::from(4); 16])]; let pipeline = make_prepared_pipeline(f, Default::default(), external_witness); test_pilcom(pipeline); } @@ -153,8 +153,8 @@ fn external_witgen_b_provided() { fn external_witgen_both_provided() { let f = "pil/external_witgen.pil"; let external_witness = vec![ - ("main.a".to_string(), vec![GoldilocksField::from(3); 16]), - ("main.b".to_string(), vec![GoldilocksField::from(4); 16]), + ("main::a".to_string(), vec![GoldilocksField::from(3); 16]), + ("main::b".to_string(), vec![GoldilocksField::from(4); 16]), ]; let pipeline = make_prepared_pipeline(f, Default::default(), external_witness); test_pilcom(pipeline); @@ -165,9 +165,9 @@ fn external_witgen_both_provided() { fn external_witgen_fails_on_conflicting_external_witness() { let f = "pil/external_witgen.pil"; let external_witness = vec![ - ("main.a".to_string(), vec![GoldilocksField::from(3); 16]), + ("main::a".to_string(), vec![GoldilocksField::from(3); 16]), // Does not satisfy b = a + 1 - ("main.b".to_string(), vec![GoldilocksField::from(3); 16]), + ("main::b".to_string(), vec![GoldilocksField::from(3); 16]), ]; let pipeline = make_prepared_pipeline(f, Default::default(), external_witness); test_pilcom(pipeline); diff --git a/pipeline/tests/powdr_std.rs b/pipeline/tests/powdr_std.rs index 71a6175826..4dd674bcd4 100644 --- a/pipeline/tests/powdr_std.rs +++ b/pipeline/tests/powdr_std.rs @@ -104,7 +104,7 @@ fn permutation_via_challenges_bn() { } #[test] -#[should_panic = "Error reducing expression to constraint:\nExpression: std::protocols::permutation::permutation(main.is_first, [main.z], main.alpha, main.beta, main.permutation_constraint)\nError: FailedAssertion(\"The field is too small and needs to move to the extension field. Pass two elements instead!\")"] +#[should_panic = "Error reducing expression to constraint:\nExpression: std::protocols::permutation::permutation(main::is_first, [main::z], main::alpha, main::beta, main::permutation_constraint)\nError: FailedAssertion(\"The field is too small and needs to move to the extension field. Pass two elements instead!\")"] fn permutation_via_challenges_gl() { let f = "std/permutation_via_challenges.asm"; make_simple_prepared_pipeline::(f); diff --git a/riscv/benches/executor_benchmark.rs b/riscv/benches/executor_benchmark.rs index 99741769f9..829f0f8054 100644 --- a/riscv/benches/executor_benchmark.rs +++ b/riscv/benches/executor_benchmark.rs @@ -43,7 +43,7 @@ fn executor_benchmark(c: &mut Criterion) { pipeline.compute_fixed_cols().unwrap(); let pipeline = pipeline.add_external_witness_values(vec![( - "main_bootloader_inputs.value".to_string(), + "main_bootloader_inputs::value".to_string(), default_input(&[63, 64, 65]) .into_iter() .map(|e| e.into_fe()) diff --git a/riscv/src/continuations.rs b/riscv/src/continuations.rs index 1e0790c1df..cb7e11b2e6 100644 --- a/riscv/src/continuations.rs +++ b/riscv/src/continuations.rs @@ -42,7 +42,7 @@ fn transposed_trace(trace: &ExecutionTrace) -> HashMap( (transposed_trace::(&trace), trace.mem_ops) }; - let full_trace_length = full_trace["main.pc"].len(); + let full_trace_length = full_trace["main::pc"].len(); log::info!("Total trace length: {}", full_trace_length); - let (first_real_execution_row, _) = full_trace["main.pc"] + let (first_real_execution_row, _) = full_trace["main::pc"] .iter() .enumerate() .find(|(_, &pc)| pc.bin() as u64 == DEFAULT_PC) @@ -402,7 +402,7 @@ pub fn rust_continuations_dry_run( }) .collect::>(); - register_values.push(*chunk_trace["main.pc"].last().unwrap()); + register_values.push(*chunk_trace["main::pc"].last().unwrap()); // Replace final register values of the current chunk bootloader_inputs[REGISTER_NAMES.len()..2 * REGISTER_NAMES.len()] @@ -429,16 +429,16 @@ pub fn rust_continuations_dry_run( ) ); - let actual_num_rows = chunk_trace["main.pc"].len(); + let actual_num_rows = chunk_trace["main::pc"].len(); bootloader_inputs_and_num_rows.push(( bootloader_inputs.iter().map(|e| e.into_fe()).collect(), actual_num_rows as u64, )); - log::info!("Chunk trace length: {}", chunk_trace["main.pc"].len()); + log::info!("Chunk trace length: {}", chunk_trace["main::pc"].len()); log::info!("Validating chunk..."); log::info!("Looking for pc = {}...", bootloader_inputs[PC_INDEX]); - let (start, _) = chunk_trace["main.pc"] + let (start, _) = chunk_trace["main::pc"] .iter() .enumerate() .find(|(_, &pc)| pc == bootloader_inputs[PC_INDEX]) @@ -450,8 +450,8 @@ pub fn rust_continuations_dry_run( length, (length - start - shutdown_routine_rows) * 100 / length ); - for i in 0..(chunk_trace["main.pc"].len() - start) { - for ® in ["main.pc", "main.query_arg_1", "main.query_arg_2"].iter() { + for i in 0..(chunk_trace["main::pc"].len() - start) { + for ® in ["main::pc", "main::query_arg_1", "main::query_arg_2"].iter() { let chunk_i = i + start; let full_i = i + proven_trace; if chunk_trace[reg][chunk_i] != full_trace[reg][full_i] { @@ -461,8 +461,8 @@ pub fn rust_continuations_dry_run( ); log::error!( "The PCs are {} and {}.", - chunk_trace["main.pc"][chunk_i], - full_trace["main.pc"][full_i] + chunk_trace["main::pc"][chunk_i], + full_trace["main::pc"][full_i] ); log::error!( "The first difference is in register {}: {} != {} ", @@ -475,11 +475,11 @@ pub fn rust_continuations_dry_run( } } - if chunk_trace["main.pc"].len() < num_rows { + if chunk_trace["main::pc"].len() < num_rows { log::info!("Done!"); break; } - assert_eq!(chunk_trace["main.pc"].len(), num_rows); + assert_eq!(chunk_trace["main::pc"].len(), num_rows); // Minus one, because the last row will have to be repeated in the next chunk. let new_rows = num_rows - start - 1; diff --git a/riscv/src/continuations/bootloader.rs b/riscv/src/continuations/bootloader.rs index f3f038f0de..2c7f98bd65 100644 --- a/riscv/src/continuations/bootloader.rs +++ b/riscv/src/continuations/bootloader.rs @@ -89,26 +89,26 @@ pub fn bootloader_preamble() -> String { for (i, reg) in REGISTER_NAMES.iter().enumerate() { let reg = reg.strip_prefix("main.").unwrap(); preamble.push_str(&format!( - " //public initial_{reg} = main_bootloader_inputs.value({i});\n" + " //public initial_{reg} = main_bootloader_inputs::value({i});\n" )); } for (i, reg) in REGISTER_NAMES.iter().enumerate() { let reg = reg.strip_prefix("main.").unwrap(); preamble.push_str(&format!( - " //public final_{reg} = main_bootloader_inputs.value({});\n", + " //public final_{reg} = main_bootloader_inputs::value({});\n", i + REGISTER_NAMES.len() )); } preamble.push_str(&format!( r#" - //public initial_memory_hash_1 = main_bootloader_inputs.value({}); - //public initial_memory_hash_2 = main_bootloader_inputs.value({}); - //public initial_memory_hash_3 = main_bootloader_inputs.value({}); - //public initial_memory_hash_4 = main_bootloader_inputs.value({}); - //public initial_memory_hash_5 = main_bootloader_inputs.value({}); - //public initial_memory_hash_6 = main_bootloader_inputs.value({}); - //public initial_memory_hash_7 = main_bootloader_inputs.value({}); - //public initial_memory_hash_8 = main_bootloader_inputs.value({}); + //public initial_memory_hash_1 = main_bootloader_inputs::value({}); + //public initial_memory_hash_2 = main_bootloader_inputs::value({}); + //public initial_memory_hash_3 = main_bootloader_inputs::value({}); + //public initial_memory_hash_4 = main_bootloader_inputs::value({}); + //public initial_memory_hash_5 = main_bootloader_inputs::value({}); + //public initial_memory_hash_6 = main_bootloader_inputs::value({}); + //public initial_memory_hash_7 = main_bootloader_inputs::value({}); + //public initial_memory_hash_8 = main_bootloader_inputs::value({}); "#, MEMORY_HASH_START_INDEX, MEMORY_HASH_START_INDEX + 1, @@ -121,14 +121,14 @@ pub fn bootloader_preamble() -> String { )); preamble.push_str(&format!( r#" - //public final_memory_hash_1 = main_bootloader_inputs.value({}); - //public final_memory_hash_2 = main_bootloader_inputs.value({}); - //public final_memory_hash_3 = main_bootloader_inputs.value({}); - //public final_memory_hash_4 = main_bootloader_inputs.value({}); - //public final_memory_hash_5 = main_bootloader_inputs.value({}); - //public final_memory_hash_6 = main_bootloader_inputs.value({}); - //public final_memory_hash_7 = main_bootloader_inputs.value({}); - //public final_memory_hash_8 = main_bootloader_inputs.value({}); + //public final_memory_hash_1 = main_bootloader_inputs::value({}); + //public final_memory_hash_2 = main_bootloader_inputs::value({}); + //public final_memory_hash_3 = main_bootloader_inputs::value({}); + //public final_memory_hash_4 = main_bootloader_inputs::value({}); + //public final_memory_hash_5 = main_bootloader_inputs::value({}); + //public final_memory_hash_6 = main_bootloader_inputs::value({}); + //public final_memory_hash_7 = main_bootloader_inputs::value({}); + //public final_memory_hash_8 = main_bootloader_inputs::value({}); "#, MEMORY_HASH_START_INDEX + 8, MEMORY_HASH_START_INDEX + 9, diff --git a/test_data/pil/block_lookup_or.pil b/test_data/pil/block_lookup_or.pil index 6a08791272..60776dcfcb 100644 --- a/test_data/pil/block_lookup_or.pil +++ b/test_data/pil/block_lookup_or.pil @@ -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 eb2dd70ad1..b8a4ac53c1 100644 --- a/test_data/pil/block_lookup_or_permutation.pil +++ b/test_data/pil/block_lookup_or_permutation.pil @@ -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/different_degrees.pil b/test_data/pil/different_degrees.pil index 44a39e4c03..c4dc72fb51 100644 --- a/test_data/pil/different_degrees.pil +++ b/test_data/pil/different_degrees.pil @@ -19,6 +19,6 @@ namespace Main(2 * 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/pair_lookup.pil b/test_data/pil/pair_lookup.pil index 4bbd224860..42f6be4405 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/single_line_blocks.pil b/test_data/pil/single_line_blocks.pil index 17258c8937..a2566f0813 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 364911e360..c19350bfd2 100644 --- a/test_data/pil/two_block_machine_functions.pil +++ b/test_data/pil/two_block_machine_functions.pil @@ -5,16 +5,16 @@ 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)))); + 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]*; col fixed p_instr_baz = [0, 0, 1, 0] + [0]*; 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/vm_to_block_dynamic_length.pil b/test_data/pil/vm_to_block_dynamic_length.pil index ad84725253..16508c7b67 100644 --- a/test_data/pil/vm_to_block_dynamic_length.pil +++ b/test_data/pil/vm_to_block_dynamic_length.pil @@ -12,7 +12,7 @@ namespace std::prover; namespace main(256); col witness _operation_id(i) query std::prelude::Query::Hint(6); col fixed _block_enforcer_last_step = [0]* + [1]; - (1 - main._block_enforcer_last_step) * (1 - main.instr_return) * (main._operation_id' - main._operation_id) = 0; + (1 - main::_block_enforcer_last_step) * (1 - main::instr_return) * (main::_operation_id' - main::_operation_id) = 0; col witness pc; col witness X; col witness Y; @@ -22,28 +22,28 @@ namespace main(256); col witness instr_add; col witness instr_mul; col witness instr_assert_eq; - main.instr_assert_eq * (main.X - main.Y) = 0; + main::instr_assert_eq * (main::X - main::Y) = 0; col witness instr__jump_to_operation; col witness instr__reset; col witness instr__loop; col witness instr_return; col witness X_const; col witness read_X_A; - main.X = main.read_X_A * main.A + main.X_const; + main::X = main::read_X_A * main::A + main::X_const; col witness Y_const; - main.Y = main.Y_const; + main::Y = main::Y_const; col witness Z_read_free; - main.Z = main.Z_read_free * main.Z_free_value; + main::Z = main::Z_read_free * main::Z_free_value; col fixed first_step = [1] + [0]*; - main.A' = main.reg_write_Z_A * main.Z + (1 - (main.reg_write_Z_A + main.instr__reset)) * main.A; - col pc_update = main.instr__jump_to_operation * main._operation_id + main.instr__loop * main.pc + (1 - (main.instr__jump_to_operation + main.instr__loop + main.instr_return)) * (main.pc + 1); - main.pc' = (1 - main.first_step') * main.pc_update; + main::A' = main::reg_write_Z_A * main::Z + (1 - (main::reg_write_Z_A + main::instr__reset)) * main::A; + col pc_update = main::instr__jump_to_operation * main::_operation_id + main::instr__loop * main::pc + (1 - (main::instr__jump_to_operation + main::instr__loop + main::instr_return)) * (main::pc + 1); + main::pc' = (1 - main::first_step') * main::pc_update; col witness Z_free_value; - [main.pc, main.reg_write_Z_A, main.instr_add, main.instr_mul, main.instr_assert_eq, main.instr__jump_to_operation, main.instr__reset, main.instr__loop, main.instr_return, main.X_const, main.read_X_A, main.Y_const, main.Z_read_free] in [main__rom.p_line, main__rom.p_reg_write_Z_A, main__rom.p_instr_add, main__rom.p_instr_mul, main__rom.p_instr_assert_eq, main__rom.p_instr__jump_to_operation, main__rom.p_instr__reset, main__rom.p_instr__loop, main__rom.p_instr_return, main__rom.p_X_const, main__rom.p_read_X_A, main__rom.p_Y_const, main__rom.p_Z_read_free]; - main.instr_add $ [0, main.X, main.Y, main.Z] in [main_arith.operation_id, main_arith.x[0], main_arith.x[1], main_arith.y]; - main.instr_mul $ [1, main.X, main.Y, main.Z] in [main_arith.operation_id, main_arith.x[0], main_arith.x[1], main_arith.y]; + [main::pc, main::reg_write_Z_A, main::instr_add, main::instr_mul, main::instr_assert_eq, main::instr__jump_to_operation, main::instr__reset, main::instr__loop, main::instr_return, main::X_const, main::read_X_A, main::Y_const, main::Z_read_free] in [main__rom::p_line, main__rom::p_reg_write_Z_A, main__rom::p_instr_add, main__rom::p_instr_mul, main__rom::p_instr_assert_eq, main__rom::p_instr__jump_to_operation, main__rom::p_instr__reset, main__rom::p_instr__loop, main__rom::p_instr_return, main__rom::p_X_const, main__rom::p_read_X_A, main__rom::p_Y_const, main__rom::p_Z_read_free]; + main::instr_add $ [0, main::X, main::Y, main::Z] in [main_arith::operation_id, main_arith::x[0], main_arith::x[1], main_arith::y]; + main::instr_mul $ [1, main::X, main::Y, main::Z] in [main_arith::operation_id, main_arith::x[0], main_arith::x[1], main_arith::y]; col fixed _linker_first_step = [1] + [0]*; - main._linker_first_step * (main._operation_id - 2) = 0; + main::_linker_first_step * (main::_operation_id - 2) = 0; namespace main__rom(256); col fixed p_line = [0, 1, 2, 3, 4, 5, 6] + [6]*; col fixed p_X_const = [0, 0, 2, 0, 0, 0, 0] + [0]*; @@ -64,4 +64,4 @@ namespace main_arith; col witness operation_id; col witness x[2]; col witness y; - main_arith.y = main_arith.operation_id * (main_arith.x[0] * main_arith.x[1]) + (1 - main_arith.operation_id) * (main_arith.x[0] + main_arith.x[1]); + main_arith::y = main_arith::operation_id * (main_arith::x[0] * main_arith::x[1]) + (1 - main_arith::operation_id) * (main_arith::x[0] + main_arith::x[1]);