From ff8fda1563c807bd51fd7e4460d8a2d52891dee3 Mon Sep 17 00:00:00 2001 From: Leandro Pacheco Date: Wed, 13 Mar 2024 14:42:57 -0300 Subject: [PATCH] Expressions in instr/link params allow for `link` and RHS of `instr` params to use full on expressions --- analysis/src/machine_check.rs | 37 +---- asm-to-pil/Cargo.toml | 1 + asm-to-pil/src/vm_to_constrained.rs | 172 +++++++------------- ast/src/asm_analysis/mod.rs | 9 +- ast/src/object/mod.rs | 6 +- ast/src/parsed/asm.rs | 47 +++--- ast/src/parsed/display.rs | 4 +- book/src/asm/instructions.md | 6 +- book/src/asm/links.md | 2 +- importer/src/path_canonicalizer.rs | 24 ++- linker/src/lib.rs | 24 +-- parser/src/powdr.lalrpop | 10 +- riscv/src/coprocessors.rs | 2 +- test_data/asm/book/instructions.asm | 24 ++- test_data/asm/book/operations_and_links.asm | 4 +- test_data/asm/vm_instr_param_mapping.asm | 28 +++- 16 files changed, 185 insertions(+), 215 deletions(-) diff --git a/analysis/src/machine_check.rs b/analysis/src/machine_check.rs index 33c93bbf2..c1446bbe8 100644 --- a/analysis/src/machine_check.rs +++ b/analysis/src/machine_check.rs @@ -13,13 +13,11 @@ use powdr_ast::{ parsed::{ self, asm::{ - self, ASMModule, ASMProgram, AbsoluteSymbolPath, AssignmentRegister, CallableRef, - FunctionStatement, InstructionBody, LinkDeclaration, MachineStatement, ModuleStatement, - RegisterFlag, SymbolDefinition, + self, ASMModule, ASMProgram, AbsoluteSymbolPath, AssignmentRegister, FunctionStatement, + InstructionBody, LinkDeclaration, MachineStatement, ModuleStatement, RegisterFlag, + SymbolDefinition, }, - Expression, }, - SourceRef, }; /// Verifies certain properties of each machine and constructs the Machine objects. @@ -78,10 +76,7 @@ impl TypeChecker { } } MachineStatement::LinkDeclaration(source, LinkDeclaration { flag, to }) => { - match self.check_link_declaration(source, flag, to) { - Ok(link_definition) => links.push(link_definition), - Err(e) => errors.extend(e), - } + links.push(LinkDefinitionStatement { source, flag, to }); } MachineStatement::Pil(_source, statement) => { pil.push(statement); @@ -369,30 +364,6 @@ impl TypeChecker { body: instruction.body, }) } - - fn check_link_declaration( - &self, - source: SourceRef, - flag: Expression, - to: CallableRef, - ) -> Result> { - let mut err = vec![]; - - to.params.inputs_and_outputs().for_each(|p| { - if let Some(ty) = &p.ty { - err.push(format!( - "Invalid type '{}: {}' in link declaration", - p.name, ty - )); - } - }); - - if err.is_empty() { - Ok(LinkDefinitionStatement { source, flag, to }) - } else { - Err(err) - } - } } #[cfg(test)] diff --git a/asm-to-pil/Cargo.toml b/asm-to-pil/Cargo.toml index 56548dc70..bb65352f5 100644 --- a/asm-to-pil/Cargo.toml +++ b/asm-to-pil/Cargo.toml @@ -18,3 +18,4 @@ pretty_assertions = "1.4.0" [dev-dependencies] powdr-analysis = { path = "../analysis" } +powdr-importer = { path = "../importer" } diff --git a/asm-to-pil/src/vm_to_constrained.rs b/asm-to-pil/src/vm_to_constrained.rs index 9b3418fb5..ac260870e 100644 --- a/asm-to-pil/src/vm_to_constrained.rs +++ b/asm-to-pil/src/vm_to_constrained.rs @@ -9,7 +9,7 @@ use powdr_ast::{ LinkDefinitionStatement, Machine, RegisterDeclarationStatement, RegisterTy, Rom, }, parsed::{ - asm::{CallableRef, InstructionBody, Params}, + asm::{CallableRef, InstructionBody, InstructionParams}, build::{self, absolute_reference, direct_reference, next_reference}, visitor::ExpressionVisitable, ArrayExpression, BinaryOperator, Expression, FunctionCall, FunctionDefinition, @@ -353,7 +353,6 @@ impl ASMPILConverter { Some(ty) if ty == "unsigned" => { Input::Literal(param.name, LiteralKind::UnsignedConstant) } - Some(ty) if ty == "write" => Input::Register(param.name), None => Input::Register(param.name), Some(ty) => panic!("Invalid param type {}", ty), }) @@ -371,7 +370,7 @@ impl ASMPILConverter { source: SourceRef, name: &String, flag: String, - params: &Params, + params: &InstructionParams, mut body: Vec, ) { // check inputs are literals or assignment registers @@ -480,7 +479,7 @@ impl ASMPILConverter { &mut self, source: SourceRef, flag: String, - params: &Params, + params: &InstructionParams, mut callable: CallableRef, ) -> LinkDefinitionStatement { let lhs = params; @@ -490,7 +489,7 @@ impl ASMPILConverter { lhs.inputs_and_outputs().for_each(|p| { assert!( p.index.is_none(), - "Cannot use array elements for instruction outputs." + "Cannot use array elements for lhs params" ); let is_assignment_register = self @@ -506,64 +505,70 @@ impl ASMPILConverter { if rhs.is_empty() { // we allow declarations with an empty RHS as syntactic sugar for when RHS = LHS. - *rhs = lhs.clone(); - } else { - // if rhs is not empty, check it's valid - // rhs params must either be assignment registers declared in the lhs or write registers - rhs + rhs.inputs = lhs .inputs - .iter_mut() - .chain(rhs.outputs.iter_mut()) - .for_each(|p| { - let reg = self.registers.get(&p.name).expect("All rhs params must be registers"); - assert!(p.ty.is_none()); - match reg.ty { - RegisterTy::Assignment => { - assert!(lhs.inputs_and_outputs().any(|p_lhs| p_lhs.name == p.name), - "Assignment register '{}' on rhs must be also present on lhs params", p.name); - } - RegisterTy::Write => { - // the linker needs this information to build the - // plookup when a write register is used as output. - // TODO: less hackish way of passing this info? proper type for param.ty? - p.ty = Some("write".to_string()); - }, - _ => panic!("The rhs of an external instruction declaration must only use write or assignment registers"), - } - }); + .iter() + .map(|p| direct_reference(p.name.clone())) + .collect(); + rhs.outputs = lhs + .outputs + .iter() + .map(|p| direct_reference(p.name.clone())) + .collect(); + } else { + let mut rhs_assignment_registers = BTreeSet::new(); + let mut rhs_next_write_registers = BTreeSet::new(); - // all lhs params must be used on rhs + // collect assignment registers and next references to write registers used on rhs + for expr in rhs.inputs_and_outputs() { + expr.pre_visit_expressions(&mut |e| match e { + Expression::Reference(poly) => { + poly.try_to_identifier() + .and_then(|name| self.registers.get(name).map(|reg| (name, reg))) + .filter(|(_, reg)| reg.ty == RegisterTy::Assignment) + .map(|(name, _)| rhs_assignment_registers.insert(name.clone())); + } + Expression::UnaryOperation(UnaryOperator::Next, e) => { + if let Expression::Reference(poly) = e.as_ref() { + poly.try_to_identifier() + .and_then(|name| self.registers.get(name).map(|reg| (name, reg))) + .filter(|(_, reg)| reg.ty == RegisterTy::Write) + .map(|(name, _)| rhs_next_write_registers.insert(name.clone())); + } + } + _ => {} + }) + } + + // any assignment register present on the rhs (input or output) must be present on the lhs + for name in &rhs_assignment_registers { + assert!( + lhs.inputs_and_outputs().any(|p_lhs| p_lhs.name == *name), + "Assignment register '{}' used on rhs must be present on lhs params", + name + ); + } + + // all lhs assignment registers must be used on rhs lhs.inputs_and_outputs().for_each(|p| { assert!( - rhs.inputs_and_outputs().any(|rhs_p| rhs_p.name == p.name), + rhs_assignment_registers.contains(&p.name), "'{}' is declared on lhs but not used on the rhs", p.name ) }); - // can't repeat registers on output of rhs - let uniq: BTreeSet<_> = rhs.outputs.iter().map(|p| &p.name).collect(); - assert_eq!( - rhs.outputs.len(), - uniq.len(), - "rhs of external instruction can't have repeated output registers" - ); - } - - // if a write register is used as output in an external instruction mapping, we - // must induce a tautology in the update clause (Reg' = Reg') when the - // instruction is active, to allow the operation plookup to match. - for p in rhs.outputs.iter() { - let reg = self - .registers - .get_mut(&p.name) - .expect("All rhs params must be registers"); - if reg.ty.is_write() { - let value = next_reference(&p.name); + // if a write register next reference (R') is used in the instruction mapping, + // we must induce a tautology in the update clause (R' = R') when the + // instruction is active, to allow the operation plookup to match. + for name in rhs_next_write_registers { + let reg = self.registers.get_mut(&name).unwrap(); + let value = next_reference(name); reg.conditioned_updates .push((direct_reference(&flag), value)); } } + LinkDefinitionStatement { source, flag: direct_reference(flag), @@ -1210,13 +1215,13 @@ fn extract_update(expr: Expression) -> (Option, Expression) { #[cfg(test)] mod test { use powdr_ast::asm_analysis::AnalysisASMFile; + use powdr_importer::load_dependencies_and_resolve_str; use powdr_number::{FieldElement, GoldilocksField}; use crate::compile; fn parse_analyse_and_compile(input: &str) -> AnalysisASMFile { - let parsed = powdr_parser::parse_asm(None, input).unwrap(); - // let resolved = powdr_importer::load_dependencies_and_resolve(None, parsed).unwrap(); + let parsed = load_dependencies_and_resolve_str(input); let analyzed = powdr_analysis::analyze(parsed).unwrap(); compile::(analyzed) } @@ -1240,46 +1245,6 @@ machine Main { parse_analyse_and_compile::(asm); } - #[test] - #[should_panic(expected = "All rhs params must be registers")] - fn instr_external_rhs_not_register1() { - let asm = r" -machine Main { - degree 8; - reg pc[@pc]; - reg X[<=]; - reg A; - - instr foo X = vm.foo B; - - function main { - foo; - } -} -"; - parse_analyse_and_compile::(asm); - } - - #[test] - #[should_panic(expected = "All rhs params must be registers")] - fn instr_external_rhs_not_register2() { - let asm = r" -machine Main { - degree 8; - reg pc[@pc]; - reg X[<=]; - reg A; - - instr foo = vm.foo l: label; - - function main { - foo; - } -} -"; - parse_analyse_and_compile::(asm); - } - #[test] #[should_panic(expected = "'X' is declared on lhs but not used on the rhs")] fn instr_external_lhs_register_not_used() { @@ -1302,7 +1267,7 @@ machine Main { } #[test] - #[should_panic(expected = "Assignment register 'Y' on rhs must be also present on lhs params")] + #[should_panic(expected = "Assignment register 'Y' used on rhs must be present on lhs params")] fn instr_external_rhs_register_not_on_lhs() { let asm = r" machine Main { @@ -1318,27 +1283,6 @@ machine Main { foo; } } -"; - parse_analyse_and_compile::(asm); - } - - #[test] - #[should_panic(expected = "rhs of external instruction can't have repeated output registers")] - fn instr_external_rhs_repeated_output_register() { - let asm = r" -machine Main { - degree 8; - reg pc[@pc]; - reg X[<=]; - reg Y[<=]; - reg A; - - instr foo X = vm.foo X -> A, A; - - function main { - foo; - } -} "; parse_analyse_and_compile::(asm); } diff --git a/ast/src/asm_analysis/mod.rs b/ast/src/asm_analysis/mod.rs index 626bc4937..982fa211a 100644 --- a/ast/src/asm_analysis/mod.rs +++ b/ast/src/asm_analysis/mod.rs @@ -14,7 +14,8 @@ use powdr_number::BigUint; use crate::parsed::{ asm::{ - AbsoluteSymbolPath, AssignmentRegister, CallableRef, InstructionBody, OperationId, Params, + AbsoluteSymbolPath, AssignmentRegister, CallableRef, FunctionParams, InstructionBody, + InstructionParams, OperationId, OperationParams, }, visitor::{ExpressionVisitable, VisitOrder}, NamespacedPolynomialReference, PilStatement, TypedExpression, @@ -65,7 +66,7 @@ pub struct InstructionDefinitionStatement { #[derive(Clone, Debug)] pub struct Instruction { - pub params: Params, + pub params: InstructionParams, pub body: InstructionBody, } @@ -510,7 +511,7 @@ impl<'a> TryFrom<&'a mut CallableSymbol> for &'a mut OperationSymbol { pub struct FunctionSymbol { pub source: SourceRef, /// the parameters of this function, in the form of values - pub params: Params, + pub params: FunctionParams, /// the body of the function pub body: FunctionBody, } @@ -521,7 +522,7 @@ pub struct OperationSymbol { /// the id of this operation. This machine's operation id must be set to this value in order for this operation to be active. pub id: OperationId, /// the parameters of this operation, in the form of columns defined in some constraints block of this machine - pub params: Params, + pub params: OperationParams, } #[derive(Clone, Debug)] diff --git a/ast/src/object/mod.rs b/ast/src/object/mod.rs index 0c9c2d7a8..52505aefd 100644 --- a/ast/src/object/mod.rs +++ b/ast/src/object/mod.rs @@ -3,7 +3,7 @@ use std::collections::BTreeMap; use powdr_number::BigUint; use crate::parsed::{ - asm::{AbsoluteSymbolPath, Params}, + asm::{AbsoluteSymbolPath, CallableParams, OperationParams}, Expression, PilStatement, TypedExpression, }; @@ -63,7 +63,7 @@ pub struct Link { #[derive(Clone)] pub struct LinkFrom { pub flag: Expression, - pub params: Params, + pub params: CallableParams, } #[derive(Clone)] @@ -91,5 +91,5 @@ pub struct Operation { /// the value of the operation id of this machine which activates this operation pub id: Option, /// the parameters - pub params: Params, + pub params: OperationParams, } diff --git a/ast/src/parsed/asm.rs b/ast/src/parsed/asm.rs index 2edbcbd31..b535aba06 100644 --- a/ast/src/parsed/asm.rs +++ b/ast/src/parsed/asm.rs @@ -397,23 +397,22 @@ pub struct MachineArguments { } #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Default)] -pub struct Params { - pub inputs: Vec, - pub outputs: Vec, +pub struct Params { + pub inputs: Vec, + pub outputs: Vec, } -impl Params { - pub fn inputs_and_outputs(&self) -> impl Iterator { - self.inputs.iter().chain(self.outputs.iter()) - } +pub type CallableParams = Params; +// TODO: should we have separate Param types here? +// - Function: doesn't use `index` or `type` +// - Instruction: doesn't use `index` +// - Operation: doesn't use `type` +pub type FunctionParams = Params; +pub type InstructionParams = Params; +pub type OperationParams = Params; - pub fn inputs_and_outputs_mut(&mut self) -> impl Iterator { - self.inputs.iter_mut().chain(self.outputs.iter_mut()) - } -} - -impl Params { - pub fn new(inputs: Vec, outputs: Vec) -> Self { +impl Params { + pub fn new(inputs: Vec, outputs: Vec) -> Self { Self { inputs, outputs } } @@ -421,6 +420,16 @@ impl Params { self.inputs.is_empty() && self.outputs.is_empty() } + pub fn inputs_and_outputs(&self) -> impl Iterator { + self.inputs.iter().chain(self.outputs.iter()) + } + + pub fn inputs_and_outputs_mut(&mut self) -> impl Iterator { + self.inputs.iter_mut().chain(self.outputs.iter_mut()) + } +} + +impl Params { pub fn prepend_space_if_non_empty(&self) -> String { let mut params_str = self.to_string(); if !self.is_empty() { @@ -438,7 +447,7 @@ pub struct OperationId { #[derive(Debug, PartialEq, Eq, Clone, PartialOrd, Ord)] pub struct Instruction { - pub params: Params, + pub params: Params, pub body: InstructionBody, } @@ -450,8 +459,8 @@ pub enum MachineStatement { RegisterDeclaration(SourceRef, String, Option), InstructionDeclaration(SourceRef, String, Instruction), LinkDeclaration(SourceRef, LinkDeclaration), - FunctionDeclaration(SourceRef, String, Params, Vec), - OperationDeclaration(SourceRef, String, OperationId, Params), + FunctionDeclaration(SourceRef, String, FunctionParams, Vec), + OperationDeclaration(SourceRef, String, OperationId, OperationParams), } #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)] @@ -464,7 +473,7 @@ pub struct LinkDeclaration { pub struct CallableRef { pub instance: String, pub callable: String, - pub params: Params, + pub params: CallableParams, } #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)] @@ -516,7 +525,7 @@ pub enum RegisterFlag { IsReadOnly, } -#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)] +#[derive(Debug, Default, PartialEq, Eq, PartialOrd, Ord, Clone)] pub struct Param { pub name: String, pub index: Option, diff --git a/ast/src/parsed/display.rs b/ast/src/parsed/display.rs index ac774d8b1..dc168ceca 100644 --- a/ast/src/parsed/display.rs +++ b/ast/src/parsed/display.rs @@ -274,7 +274,7 @@ impl Display for RegisterFlag { } } -impl Display for Params { +impl Display for Params { fn fmt(&self, f: &mut Formatter<'_>) -> Result { write!( f, @@ -683,7 +683,7 @@ mod tests { ty: Some("ty".into()), }; assert_eq!(p.to_string(), "abc: ty"); - let empty = Params::default(); + let empty = Params::::default(); assert_eq!(empty.to_string(), ""); assert_eq!(empty.prepend_space_if_non_empty(), ""); let in_out = Params { diff --git a/book/src/asm/instructions.md b/book/src/asm/instructions.md index 90107574e..33215252c 100644 --- a/book/src/asm/instructions.md +++ b/book/src/asm/instructions.md @@ -30,10 +30,10 @@ An external instruction calling into this operation can be declared as follows: ``` {{#include ../../../test_data/asm/book/instructions.asm:trivial}} ``` -The left-hand side of the definition declares the local instruction and which assignment registers are used for its inputs and outputs. -The right-hand side of the definition specifies the external operation being called and how it should be called. +The left-hand side of the definition declares the local instruction and which assignment registers are used in its inputs and outputs. +It describes how the instruction is used. +The right-hand side of the definition specifies the call to the external operation, with its inputs and outputs. All assignment registers on the left-hand side must be used in the call to the external operation. -Additionally, regular registers can also be used in the call (can be seen as implicit inputs/outputs of the instruction). In the previous example, parameters of the instruction match exactly with how the target operation should be called, and the right-hand parameters can thus be omitted. The following example shows more complex usages of external instructions: diff --git a/book/src/asm/links.md b/book/src/asm/links.md index 089b5bcaa..bced31091 100644 --- a/book/src/asm/links.md +++ b/book/src/asm/links.md @@ -1,7 +1,7 @@ # Links Links enable a constrained machine to call into another machine. -They are defined by a boolean flag and a mapping from local machine columns to the operation and its parameters (inputs and outputs): +They are defined by a boolean flag and a call to the operation, where inputs and outputs are expressions. ``` {{#include ../../../test_data/asm/book/operations_and_links.asm:links}} ``` diff --git a/importer/src/path_canonicalizer.rs b/importer/src/path_canonicalizer.rs index 55372a2ff..c8e6d7bf5 100644 --- a/importer/src/path_canonicalizer.rs +++ b/importer/src/path_canonicalizer.rs @@ -8,8 +8,9 @@ use powdr_ast::{ parsed::Expression, parsed::{ asm::{ - ASMModule, ASMProgram, AbsoluteSymbolPath, Import, Machine, MachineStatement, Module, - ModuleRef, ModuleStatement, SymbolDefinition, SymbolValue, SymbolValueRef, + ASMModule, ASMProgram, AbsoluteSymbolPath, Import, Instruction, InstructionBody, + LinkDeclaration, Machine, MachineStatement, Module, ModuleRef, ModuleStatement, + SymbolDefinition, SymbolValue, SymbolValueRef, }, folder::Folder, visitor::ExpressionVisitable, @@ -356,6 +357,25 @@ fn check_machine( MachineStatement::Pil(_, statement) => statement .expressions() .try_for_each(|e| check_expression(&module_location, e, state, &local_variables))?, + // check rhs input exrpressions for `instr` and `link` declarations + MachineStatement::LinkDeclaration( + _, + LinkDeclaration { + to: callable_ref, .. + }, + ) + | MachineStatement::InstructionDeclaration( + _, + _, + Instruction { + body: InstructionBody::CallableRef(callable_ref), + .. + }, + ) => { + callable_ref.params.inputs.iter().try_for_each(|e| { + check_expression(&module_location, e, state, &local_variables) + })?; + } _ => {} } } diff --git a/linker/src/lib.rs b/linker/src/lib.rs index 1e054f5a1..bbb0d6634 100644 --- a/linker/src/lib.rs +++ b/linker/src/lib.rs @@ -6,7 +6,7 @@ use powdr_ast::{ parsed::{ asm::AbsoluteSymbolPath, asm::SymbolPath, - build::{direct_reference, index_access, namespaced_reference, next_reference}, + build::{index_access, namespaced_reference}, Expression, PILFile, PilStatement, SelectedExpressions, TypedExpression, }, SourceRef, @@ -98,24 +98,12 @@ pub fn link(graph: PILGraph) -> Result> { .iter() .cloned() .map(|n| Expression::Number(n, None)); - let inputs = from - .params - .inputs - .into_iter() - .map(|i| { - assert!(i.ty.is_none() || i.ty == Some("write".to_string())); - (i.name, i.index) - }) - .map(|(name, index)| index_access(direct_reference(name), index)); - let outputs = from.params.outputs.into_iter().map(|p| match p.ty { - None => index_access(direct_reference(p.name), p.index), - // write register as output is mapped as a next ref in the plookup - Some(s) if s == "write" => index_access(next_reference(p.name), p.index), - _ => panic!(), - }); let lhs = SelectedExpressions { selector: Some(from.flag), - expressions: op_id.chain(inputs).chain(outputs).collect(), + expressions: op_id + .chain(from.params.inputs) + .chain(from.params.outputs) + .collect(), }; // the rhs is `latch { operation_id, inputs, outputs }` @@ -567,7 +555,7 @@ machine Main { SubVM vm; - instr add5_into_A X = vm.add5 X -> A; + instr add5_into_A X = vm.add5 X -> A'; function main { add5_into_A 10; // A <== 15 diff --git a/parser/src/powdr.lalrpop b/parser/src/powdr.lalrpop index caf45c441..a8aeb1b94 100644 --- a/parser/src/powdr.lalrpop +++ b/parser/src/powdr.lalrpop @@ -281,7 +281,13 @@ pub InstructionBody: InstructionBody = { } pub CallableRef: CallableRef = { - "." => CallableRef { instance, callable, params }, + "." => CallableRef { instance, callable, params }, +} + +CallableParams: CallableParams = { + "->" => CallableParams::new(inputs, output), + // we can ommit the arrow if there are no outputs + => CallableParams::new(inputs, vec![]) } InstructionBodyElements: Vec = { @@ -295,7 +301,7 @@ InstructionBodyElement: PilStatement = { ExpressionStatementWithoutSemicolon, } -Params: Params = { +Params: Params = { <_input: ParamList> "->" => Params::new(_input, output), // we can ommit the arrow if there are no outputs <_input: ParamList> => Params::new(_input, vec![]) diff --git a/riscv/src/coprocessors.rs b/riscv/src/coprocessors.rs index e1e3223cc..088f75d1e 100644 --- a/riscv/src/coprocessors.rs +++ b/riscv/src/coprocessors.rs @@ -59,7 +59,7 @@ static POSEIDON_GL_COPROCESSOR: CoProcessor = CoProcessor { import: "use std::hash::poseidon_gl::PoseidonGL;", instructions: r#" // ================== hashing instructions ============== -instr poseidon_gl = poseidon_gl.poseidon_permutation P0, P1, P2, P3, P4, P5, P6, P7, P8, P9, P10, P11 -> P0, P1, P2, P3; +instr poseidon_gl = poseidon_gl.poseidon_permutation P0, P1, P2, P3, P4, P5, P6, P7, P8, P9, P10, P11 -> P0', P1', P2', P3'; "#, runtime_function_impl: Some(("poseidon_gl_coprocessor", poseidon_gl_call)), diff --git a/test_data/asm/book/instructions.asm b/test_data/asm/book/instructions.asm index db33a87f4..66b5c326c 100644 --- a/test_data/asm/book/instructions.asm +++ b/test_data/asm/book/instructions.asm @@ -40,11 +40,17 @@ machine Main { instr add X, Y -> Z = submachine.add; // - trivial usage, equivalent to: // instr add X, Y -> Z = submachine.add X, Y -> Z; // ANCHOR_END: trivial - instr add_to_A X, Y = submachine.add X, Y -> A; // - output to a regular register + instr add_to_A X, Y = submachine.add X, Y -> A';// - output to a regular register instr addAB -> X = submachine.add A, B -> X; // - inputs from regular registers - instr addAB_to_C = submachine.add A, B -> C; // - all inputs and output are regular registers - instr addAB_to_A = submachine.add A, B -> A; // - reusing an input register as output - instr sub X, Y -> Z = submachine.add Y, Z -> X; // - find input for a given output (doesn't always work!) + instr addAB_to_C = submachine.add A, B -> C'; // - inputs and output from regular registers + instr addAB_to_A = submachine.add A, B -> A'; // - reusing an input register as output + instr sub X, Y -> Z = submachine.add Y, Z -> X; // - swapping input/output + // any expression can be used in the external call + instr add5 X -> Z = submachine.add X, 3+2 -> Z; // - literal expression as argument + col fixed STEP(i) { i }; + instr add_current_time_step X -> Z = submachine.add X, STEP -> Z;// - columns can be referenced + let arr = [1,2,3,4,5]; // - functions can be used + instr add_arr_sum X -> Z = submachine.add X, std::array::sum(arr) -> Z; instr assert_eq X, Y { X = Y } @@ -70,6 +76,16 @@ machine Main { addAB_to_A; assert_eq A, 77; + A <== add5(2); + assert_eq A, 7; + A <== add_arr_sum(3); + assert_eq A, 18; + + // Note that the result of this operation depends on when it executed + A <== add_current_time_step(42); + B <== add_current_time_step(42); + assert_eq B - A, 1; + return; } } diff --git a/test_data/asm/book/operations_and_links.asm b/test_data/asm/book/operations_and_links.asm index 4aed0d5d5..55291c286 100644 --- a/test_data/asm/book/operations_and_links.asm +++ b/test_data/asm/book/operations_and_links.asm @@ -33,6 +33,8 @@ machine Add4(latch, operation_id) { link 1 => adder.add x, y -> n; // - constrain the values of `z`, `w`, and `m` so that `m = adder.add(z, w)` link 1 => adder.add z, w -> m; + // - constrain the values of `m`, `n` and `r` so that `r = adder.add(m,n)` + link 1 => adder.add m, n -> r; col fixed operation_id = [0]*; col fixed latch = [1]*; @@ -44,8 +46,6 @@ machine Add4(latch, operation_id) { col witness r; col witness m; col witness n; - - r = m + n; } // ANCHOR: one_operation diff --git a/test_data/asm/vm_instr_param_mapping.asm b/test_data/asm/vm_instr_param_mapping.asm index 4ccc0844c..9316b3e89 100644 --- a/test_data/asm/vm_instr_param_mapping.asm +++ b/test_data/asm/vm_instr_param_mapping.asm @@ -43,20 +43,33 @@ machine Main { reg C; instr add X, Y -> Z = addvm.add; - instr add_to_A X, Y = addvm.add X, Y -> A; - instr sub_from_add X, Y -> Z = addvm.add Y, Z -> X; + instr add_to_A X, Y = addvm.add X, Y -> A'; instr addAB -> X = addvm.add A, B -> X; - instr addAB_to_C = addvm.add A, B -> C; - instr addAB_to_A = addvm.add A, B -> A; + instr addAB_to_C = addvm.add A, B -> C'; + instr addAB_to_A = addvm.add A, B -> A'; + instr sub_from_add X, Y -> Z = addvm.add Y, Z -> X; + instr sub_from_add_into_A X, Y = addvm.add Y, A' -> X; + instr add5 X -> Z = addvm.add X, 5 -> Z; + col fixed NUM(i) { 42 }; + instr add42 X -> Z = addvm.add X, NUM -> Z; + let arr = [1,2,3,4,5]; + instr add_arr_sum X -> Z = addvm.add X, std::array::sum(arr) -> Z; instr sub X, Y -> Z = subvm.sub; - instr sub_to_C X, Y = subvm.sub X, Y -> C; + instr sub_to_C X, Y = subvm.sub X, Y -> C'; instr assert_eq X, Y { X = Y } function main { A <== add(2, 3); assert_eq A, 5; + + A <== add5(2); + assert_eq A, 7; + + A <== add42(3); + assert_eq A, 45; + add_to_A 6, 7; assert_eq A, 13; @@ -71,12 +84,13 @@ machine Main { addAB_to_C; assert_eq C, 5; + A <== add_arr_sum(3); + assert_eq A, 18; + A <=X= 33; B <=X= 44; - C <== sub(B, A); assert_eq C, 11; - addAB_to_A; assert_eq A, 77;