Skip to content
This repository has been archived by the owner on Nov 4, 2024. It is now read-only.

Commit

Permalink
Parse HyperTransition syntax
Browse files Browse the repository at this point in the history
  • Loading branch information
alxkzmn committed Aug 26, 2024
1 parent 9c08b6d commit 1b76018
Show file tree
Hide file tree
Showing 8 changed files with 109 additions and 70 deletions.
14 changes: 14 additions & 0 deletions src/compiler/abepi.rs
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,9 @@ impl<F: From<u64> + TryInto<u32> + 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![],
}
}
Expand Down Expand Up @@ -420,6 +423,17 @@ impl<F: From<u64> + TryInto<u32> + Clone + Debug, V: Clone + Debug> CompilationU

result
}

fn compiler_statement_hyper_transition(
&self,
_dsym: DebugSymRef,
_ids: Vec<V>,
_machine: V,
_exprs: Vec<Expression<F, V>>,
_state: V,
) -> Vec<CompilationResult<F, V>> {
todo!("Compile expressions?")
}
}

fn flatten_bin_op<F: Clone, V: Clone>(
Expand Down
95 changes: 54 additions & 41 deletions src/compiler/compiler.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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 \"->\""
);
}
}
7 changes: 7 additions & 0 deletions src/compiler/semantic/analyser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}
}

Expand Down
1 change: 1 addition & 0 deletions src/compiler/setup_inter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand Down
1 change: 1 addition & 0 deletions src/interpreter/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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?
}
}

Expand Down
25 changes: 24 additions & 1 deletion src/parser/ast/statement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,10 +31,22 @@ pub enum Statement<F, V> {
WGVarDecl(DebugSymRef, Vec<TypedIdDecl<V>>), // var x;

StateDecl(DebugSymRef, V, Box<Statement<F, V>>), // state x { y }

/// Transition to another state.
Transition(DebugSymRef, V, Box<Statement<F, V>>), // -> x { y }

Block(DebugSymRef, Vec<Statement<F, V>>), // { 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>, V, Vec<Expression<F, V>>, V),
}

impl<F: Debug> Debug for Statement<F, Identifier> {
Expand Down Expand Up @@ -84,6 +96,16 @@ impl<F: Debug> Debug for Statement<F, Identifier> {
.join(" ")
)
}
Statement::HyperTransition(_, ids, machine, exprs, state) => {
write!(
f,
"{:?} <== {} ({:?}) --> {:?};",
ids,
machine.name(),
exprs,
state
)
}
}
}
}
Expand All @@ -102,6 +124,7 @@ impl<F, V> Statement<F, V> {
Statement::StateDecl(dsym, _, _) => dsym.clone(),
Statement::Transition(dsym, _, _) => dsym.clone(),
Statement::Block(dsym, _) => dsym.clone(),
Statement::HyperTransition(dsym, _, _, _, _) => dsym.clone(),
}
}
}
25 changes: 0 additions & 25 deletions src/parser/build.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
use num_bigint::BigInt;

use super::ast::{expression::Expression, statement::Statement, DebugSymRef, Identifier};

pub fn build_bin_op<S: Into<String>, F, V>(
Expand Down Expand Up @@ -63,26 +61,3 @@ pub fn build_transition<F>(
) -> Statement<F, Identifier> {
Statement::Transition(dsym, id, Box::new(block))
}

pub fn add_dsym(
dsym: DebugSymRef,
stmt: Statement<BigInt, Identifier>,
) -> Statement<BigInt, Identifier> {
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),
}
}
11 changes: 8 additions & 3 deletions src/parser/chiquito.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -37,9 +37,9 @@ pub Statements: Vec<Statement<BigInt, Identifier>> = {
}

ParseStatement: Statement<BigInt, Identifier> = {
<l: @L> <s: StatementType> ";" <r: @R> => add_dsym(dsym_factory.create(l,r), s),
<l: @L> <s: ConditionalStatement> <r: @R> => add_dsym(dsym_factory.create(l,r), s),
<l: @L> <s: StateTransition> <r: @R> => add_dsym(dsym_factory.create(l,r), s),
<s: StatementType> ";" => s,
<s: ConditionalStatement> => s,
<s: StateTransition> => s,
}

StatementType: Statement<BigInt, Identifier> = {
Expand All @@ -53,6 +53,7 @@ StatementType: Statement<BigInt, Identifier> = {
ParseWGVarDecl,
ParseTransitionSimple,
ParseTransition,
HyperTransition
}

AssertEq: Statement<BigInt, Identifier> = {
Expand Down Expand Up @@ -111,6 +112,10 @@ ParseTransition: Statement<BigInt, Identifier> = {
<l: @L> "->" <id: Identifier> <block: StatementsBlock> <r: @R> => build_transition(dsym_factory.create(l,r), id, block),
}

HyperTransition: Statement<BigInt, Identifier> = {
<l: @L> <ids: ParseIdsList> "<==" <machine: Identifier> "(" <es:ParseExpressionList> ")" "->" <st: Identifier> <r: @R> => Statement::HyperTransition(dsym_factory.create(l,r), ids, machine, es, st),
}

ParseSignalDecl: Statement<BigInt, Identifier> = {
<l: @L> "signal" <ids: ParseTypedIdList> <r: @R> => Statement::SignalDecl(dsym_factory.create(l,r), ids),
}
Expand Down

0 comments on commit 1b76018

Please sign in to comment.