diff --git a/src/compiler/abepi.rs b/src/compiler/abepi.rs index ceac8789..caa11804 100644 --- a/src/compiler/abepi.rs +++ b/src/compiler/abepi.rs @@ -65,6 +65,9 @@ impl + TryInto + Clone + Debug, V: Clone + Debug> CompilationU Statement::Transition(dsym, id, stmt) => { self.compiler_statement_transition(dsym, id, *stmt) } + Statement::HyperTransition(dsym, ids, machine, exprs, state) => { + self.compiler_statement_hyper_transition(dsym, ids, machine, exprs, state) + } _ => vec![], } } @@ -420,6 +423,17 @@ impl + TryInto + Clone + Debug, V: Clone + Debug> CompilationU result } + + fn compiler_statement_hyper_transition( + &self, + _dsym: DebugSymRef, + _ids: Vec, + _machine: V, + _exprs: Vec>, + _state: V, + ) -> Vec> { + todo!("Compile expressions?") + } } fn flatten_bin_op( diff --git a/src/compiler/compiler.rs b/src/compiler/compiler.rs index 9a3c5584..27ee0b39 100644 --- a/src/compiler/compiler.rs +++ b/src/compiler/compiler.rs @@ -558,57 +558,22 @@ mod test { use crate::{ compiler::{compile, compile_file, compile_legacy}, - parser::ast::debug_sym_factory::DebugSymRefFactory, + parser::{ast::debug_sym_factory::DebugSymRefFactory, lang::TLDeclsParser}, wit_gen::TraceGenerator, }; use super::Config; - // TODO rewrite the test after machines are able to call other machines + // TODO improve the test for HyperTransition #[test] fn test_compiler_fibo_multiple_machines() { // Source code containing two machines let circuit = " - machine fibo1 (signal n) (signal b: field) { - // n and be are created automatically as shared - // signals - signal a: field, i; - - // there is always a state called initial - // input signals get bound to the signal - // in the initial state (first instance) - state initial { - signal c; - - i, a, b, c <== 1, 1, 1, 2; - - -> middle { - i', a', b', n' <== i + 1, b, c, n; - } - } - - state middle { - signal c; - - c <== a + b; - - if i + 1 == n { - -> final { - i', b', n' <== i + 1, c, n; - } - } else { - -> middle { - i', a', b', n' <== i + 1, b, c, n; - } - } - } - - // There is always a state called final. - // Output signals get automatically bound to the signals - // with the same name in the final step (last instance). - // This state can be implicit if there are no constraints in it. + machine caller (signal n) (signal b: field) { + signal b_1: field; + b_1' <== fibo(n) -> final; } - machine fibo2 (signal n) (signal b: field) { + machine fibo (signal n) (signal b: field) { // n and be are created automatically as shared // signals signal a: field, i; @@ -839,4 +804,52 @@ mod test { r#"[SemErr { msg: "use of undeclared variable c", dsym: test/circuit_error.chiquito:24:39 }, SemErr { msg: "use of undeclared variable c", dsym: test/circuit_error.chiquito:28:46 }]"# ) } + + #[test] + fn test_parse_hyper_transition() { + let circuit = " + machine caller (signal n) (signal b: field) { + a', b, c' <== fibo(d, e, f + g) -> final; + } + "; + + let debug_sym_ref_factory = DebugSymRefFactory::new("", circuit); + let result = TLDeclsParser::new().parse(&debug_sym_ref_factory, circuit); + + assert!(result.is_ok()); + + // Wrong transition operator + let circuit = " + machine caller (signal n) (signal b: field) { + a', b, c' <== fibo(d, e, f + g) --> final; + } + "; + + let debug_sym_ref_factory = DebugSymRefFactory::new("", circuit); + let result = TLDeclsParser::new().parse(&debug_sym_ref_factory, circuit); + + assert!(result.is_err()); + let err = result.err().unwrap(); + assert_eq!( + err.to_string(), + "Unrecognized token `-` found at 99:100\nExpected one of \"->\"" + ); + + // No transition + let circuit = " + machine caller (signal n) (signal b: field) { + a', b, c' <== fibo(d, e, f + g); + } + "; + + let debug_sym_ref_factory = DebugSymRefFactory::new("", circuit); + let result = TLDeclsParser::new().parse(&debug_sym_ref_factory, circuit); + + assert!(result.is_err()); + let err = result.err().unwrap(); + assert_eq!( + err.to_string(), + "Unrecognized token `;` found at 98:99\nExpected one of \"->\"" + ); + } } diff --git a/src/compiler/semantic/analyser.rs b/src/compiler/semantic/analyser.rs index 3664608d..1314b89e 100644 --- a/src/compiler/semantic/analyser.rs +++ b/src/compiler/semantic/analyser.rs @@ -272,6 +272,13 @@ impl Analyser { Statement::SignalDecl(_, _) => {} Statement::WGVarDecl(_, _) => {} + Statement::HyperTransition(_, ids, _machine, exprs, _state) => { + // TODO analyze machine? analyze state? + exprs + .into_iter() + .for_each(|expr| self.analyse_expression(expr)); + self.collect_id_usages(&ids); + } } } diff --git a/src/compiler/setup_inter.rs b/src/compiler/setup_inter.rs index 9b2b3e24..8434bae9 100644 --- a/src/compiler/setup_inter.rs +++ b/src/compiler/setup_inter.rs @@ -250,6 +250,7 @@ impl SetupInterpreter { SignalAssignment(_, _, _) | WGAssignment(_, _, _) => vec![], SignalDecl(_, _) | WGVarDecl(_, _) => vec![], + HyperTransition(_, _, _, _, _) => todo!(), }; self.add_poly_constraints(result.into_iter().map(|cr| cr.anti_booly).collect()); diff --git a/src/interpreter/mod.rs b/src/interpreter/mod.rs index 7cd05010..6c98822e 100644 --- a/src/interpreter/mod.rs +++ b/src/interpreter/mod.rs @@ -206,6 +206,7 @@ impl<'a, F: Field + Hash> Interpreter<'a, F> { Block(_, stmts) => self.exec_step_block(stmts), Assert(_, _) => Ok(None), StateDecl(_, _, _) => Ok(None), + HyperTransition(_, _, _, _, _) => Ok(None), // TODO execute transition? } } diff --git a/src/parser/ast/statement.rs b/src/parser/ast/statement.rs index 1d7e9b7f..2534d598 100644 --- a/src/parser/ast/statement.rs +++ b/src/parser/ast/statement.rs @@ -31,10 +31,22 @@ pub enum Statement { WGVarDecl(DebugSymRef, Vec>), // var x; StateDecl(DebugSymRef, V, Box>), // state x { y } - + /// Transition to another state. Transition(DebugSymRef, V, Box>), // -> x { y } Block(DebugSymRef, Vec>), // { x } + /// Call into another machine with assertion and subsequent transition to another + /// state: + /// ```no_run + /// id_1', id_2' <== machine_id(expr1, expr2 + expr3) -> state_id; + /// ``` + /// Tuple values: + /// - debug symbol reference; + /// - assigned/asserted ids vector; + /// - machine ID; + /// - call argument expressions vector; + /// - next state ID. + HyperTransition(DebugSymRef, Vec, V, Vec>, V), } impl Debug for Statement { @@ -84,6 +96,16 @@ impl Debug for Statement { .join(" ") ) } + Statement::HyperTransition(_, ids, machine, exprs, state) => { + write!( + f, + "{:?} <== {} ({:?}) --> {:?};", + ids, + machine.name(), + exprs, + state + ) + } } } } @@ -102,6 +124,7 @@ impl Statement { Statement::StateDecl(dsym, _, _) => dsym.clone(), Statement::Transition(dsym, _, _) => dsym.clone(), Statement::Block(dsym, _) => dsym.clone(), + Statement::HyperTransition(dsym, _, _, _, _) => dsym.clone(), } } } diff --git a/src/parser/build.rs b/src/parser/build.rs index d832991d..03348fd8 100644 --- a/src/parser/build.rs +++ b/src/parser/build.rs @@ -1,5 +1,3 @@ -use num_bigint::BigInt; - use super::ast::{expression::Expression, statement::Statement, DebugSymRef, Identifier}; pub fn build_bin_op, F, V>( @@ -63,26 +61,3 @@ pub fn build_transition( ) -> Statement { Statement::Transition(dsym, id, Box::new(block)) } - -pub fn add_dsym( - dsym: DebugSymRef, - stmt: Statement, -) -> Statement { - match stmt { - Statement::Assert(_, expr) => Statement::Assert(dsym, expr), - Statement::SignalAssignment(_, ids, exprs) => Statement::SignalAssignment(dsym, ids, exprs), - Statement::SignalAssignmentAssert(_, ids, exprs) => { - Statement::SignalAssignmentAssert(dsym, ids, exprs) - } - Statement::WGAssignment(_, ids, exprs) => Statement::WGAssignment(dsym, ids, exprs), - Statement::StateDecl(_, id, block) => Statement::StateDecl(dsym, id, block), - Statement::IfThen(_, cond, then_block) => Statement::IfThen(dsym, cond, then_block), - Statement::IfThenElse(_, cond, then_block, else_block) => { - Statement::IfThenElse(dsym, cond, then_block, else_block) - } - Statement::Block(_, stmts) => Statement::Block(dsym, stmts), - Statement::SignalDecl(_, ids) => Statement::SignalDecl(dsym, ids), - Statement::WGVarDecl(_, ids) => Statement::WGVarDecl(dsym, ids), - Statement::Transition(_, id, stmt) => Statement::Transition(dsym, id, stmt), - } -} diff --git a/src/parser/chiquito.lalrpop b/src/parser/chiquito.lalrpop index b8fb582c..35c2d04a 100644 --- a/src/parser/chiquito.lalrpop +++ b/src/parser/chiquito.lalrpop @@ -37,9 +37,9 @@ pub Statements: Vec> = { } ParseStatement: Statement = { - ";" => add_dsym(dsym_factory.create(l,r), s), - => add_dsym(dsym_factory.create(l,r), s), - => add_dsym(dsym_factory.create(l,r), s), + ";" => s, + => s, + => s, } StatementType: Statement = { @@ -53,6 +53,7 @@ StatementType: Statement = { ParseWGVarDecl, ParseTransitionSimple, ParseTransition, + HyperTransition } AssertEq: Statement = { @@ -111,6 +112,10 @@ ParseTransition: Statement = { "->" => build_transition(dsym_factory.create(l,r), id, block), } +HyperTransition: Statement = { + "<==" "(" ")" "->" => Statement::HyperTransition(dsym_factory.create(l,r), ids, machine, es, st), +} + ParseSignalDecl: Statement = { "signal" => Statement::SignalDecl(dsym_factory.create(l,r), ids), }