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

Implement hyper-transition analysis #299

Closed
wants to merge 3 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 4 additions & 5 deletions src/compiler/abepi.rs
Original file line number Diff line number Diff line change
Expand Up @@ -65,8 +65,8 @@ 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, call, state) => {
self.compiler_statement_hyper_transition(dsym, ids, call, state)
Statement::HyperTransition(dsym, assign_call, state_transition) => {
self.compiler_statement_hyper_transition(dsym, *assign_call, *state_transition)
}
_ => vec![],
}
Expand Down Expand Up @@ -427,9 +427,8 @@ impl<F: From<u64> + TryInto<u32> + Clone + Debug, V: Clone + Debug> CompilationU
fn compiler_statement_hyper_transition(
&self,
_dsym: DebugSymRef,
_ids: Vec<V>,
_call: Expression<F, V>,
_state: V,
_assign_call: Statement<F, V>,
_state_transition: Statement<F, V>,
) -> Vec<CompilationResult<F, V>> {
todo!("Compile expressions? Needs specs")
}
Expand Down
17 changes: 10 additions & 7 deletions src/compiler/compiler.rs
Original file line number Diff line number Diff line change
Expand Up @@ -570,10 +570,12 @@ mod test {
// Source code containing two machines
let circuit = "
machine caller (signal n) (signal b: field) {
signal b_1: field;
b_1' <== fibo(n) -> final;
}
machine fibo (signal n) (signal b: field) {
state initial {
signal b_1: field;
b_1' <== fibo(n) -> final;
}
}
machine fibo (signal n) (signal b: field) {
// n and be are created automatically as shared
// signals
signal a: field, i;
Expand Down Expand Up @@ -809,7 +811,8 @@ mod test {
fn test_parse_hyper_transition() {
let circuit = "
machine caller (signal n) (signal b: field) {
a', b, c' <== fibo(d, e, f + g) -> final;
var some_var;
a', b', some_var' <== fibo(d, e, f + g) -> final;
}
";

Expand All @@ -821,7 +824,7 @@ mod test {
let circuit = "
machine caller (signal n) (signal b: field) {
-> final {
a', b, c' <== fibo(d, e, f + g);
a', b', c' <== fibo(d, e, f + g);
}
}
";
Expand All @@ -834,7 +837,7 @@ mod test {
// TODO should no-arg calls be allowed? Needs more specs for function/machine calls
let circuit = "
machine caller (signal n) (signal b: field) {
smth <== a() -> final;
smth' <== a() -> final;
}
";

Expand Down
85 changes: 62 additions & 23 deletions src/compiler/semantic/analyser.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
use itertools::Itertools;
use num_bigint::BigInt;

use crate::{
Expand Down Expand Up @@ -48,46 +49,86 @@ impl Default for Analyser {
impl Analyser {
/// Analyse chiquito AST.
fn analyse(&mut self, program: &[TLDecl<BigInt, Identifier>]) {
program
.iter()
.for_each(|decl: &TLDecl<BigInt, Identifier>| self.collect_tl_decl(decl));
program.iter().for_each(|decl| self.analyse_tldcl(decl));
}

/// Analyse top level declaration.
fn analyse_tldcl(&mut self, decl: &TLDecl<BigInt, Identifier>) {
/// Collect a top level declaration to later perform necessary checks (e.g., validate the
/// calls of machines from other machines).
fn collect_tl_decl(&mut self, decl: &TLDecl<BigInt, Identifier>) {
match decl.clone() {
TLDecl::MachineDecl {
dsym: _,
id,
input_params,
output_params,
block,
block: _,
} => {
let sym = SymTableEntry::new(
let sym = SymTableEntry::new_machine(
id.name(),
id.debug_sym_ref(),
SymbolCategory::Machine,
None,
input_params
.iter()
.map(|param| match param {
Statement::SignalDecl(_, decls) | Statement::WGVarDecl(_, decls) => {
if decls.len() != 1 {
unreachable!("Each input should be a single identifier");
}
decls[0].id.name()
}
_ => unreachable!("Inputs should be signals or vars"),
})
.collect_vec(),
output_params
.iter()
.map(|param| match param {
Statement::SignalDecl(_, decls) | Statement::WGVarDecl(_, decls) => {
if decls.len() != 1 {
unreachable!("Each output should be a single identifier");
}
decls[0].id.name()
}
_ => unreachable!("Outputs should be signals or vars"),
})
.collect_vec(),
);

RULES.apply_new_symbol_tldecl(self, decl, &id, &sym);

self.symbols.add_symbol(&self.cur_scope, id.name(), sym);

self.analyse_machine(id, input_params, output_params, block);
self.enter_new_scope(id.name());

self.analyse_machine_input_params(input_params);

self.analyse_machine_output_params(output_params);

self.exit_scope();
}
}
}

fn analyse_machine(
&mut self,
id: Identifier,
input_params: Vec<Statement<BigInt, Identifier>>,
output_params: Vec<Statement<BigInt, Identifier>>,
block: Statement<BigInt, Identifier>,
) {
self.enter_new_scope(id.name());
/// Analyse top level declaration.
fn analyse_tldcl(&mut self, decl: &TLDecl<BigInt, Identifier>) {
match decl.clone() {
TLDecl::MachineDecl {
dsym: _,
id,
input_params: _,
output_params: _,
block,
} => {
self.analyse_machine(id, block);
}
}
}

self.analyse_machine_input_params(input_params);
self.analyse_machine_output_params(output_params);
fn analyse_machine(&mut self, id: Identifier, block: Statement<BigInt, Identifier>) {
self.enter_new_scope(id.name());

self.add_state_decls(&block);

Expand Down Expand Up @@ -193,9 +234,6 @@ impl Analyser {

fn analyse_statement(&mut self, stmt: Statement<BigInt, Identifier>) {
self.statement_add_symbols(&stmt);

RULES.apply_statement(self, &stmt);

self.analyse_statement_recursive(stmt);
}

Expand Down Expand Up @@ -233,6 +271,8 @@ impl Analyser {
}

fn analyse_statement_recursive(&mut self, stmt: Statement<BigInt, Identifier>) {
RULES.apply_statement(self, &stmt);

match stmt {
Statement::Assert(_, expr) => self.analyse_expression(expr),
Statement::SignalAssignment(_, ids, exprs) => {
Expand Down Expand Up @@ -272,10 +312,9 @@ impl Analyser {

Statement::SignalDecl(_, _) => {}
Statement::WGVarDecl(_, _) => {}
Statement::HyperTransition(_, ids, call, state) => {
self.analyse_expression(call);
self.collect_id_usages(&[state]);
self.collect_id_usages(&ids);
Statement::HyperTransition(_, ref assign_call, ref state_transition) => {
self.analyse_statement_recursive(*assign_call.clone());
self.analyse_statement_recursive(*state_transition.clone());
}
}
}
Expand Down Expand Up @@ -398,7 +437,7 @@ mod test {

assert_eq!(
format!("{:?}", result),
r#"AnalysisResult { symbols: /: ScopeTable { symbols: "fibo: SymTableEntry { id: \"fibo\", definition_ref: nofile:2:17, usages: [], category: Machine, ty: None }", scope: Global },//fibo: ScopeTable { symbols: "a: SymTableEntry { id: \"a\", definition_ref: nofile:5:20, usages: [nofile:13:17, nofile:16:15, nofile:23:20, nofile:31:20], category: Signal, ty: Some(\"field\") },b: SymTableEntry { id: \"b\", definition_ref: nofile:2:40, usages: [nofile:13:20, nofile:16:30, nofile:16:19, nofile:23:24, nofile:27:20, nofile:31:42, nofile:31:24], category: OutputSignal, ty: Some(\"field\") },i: SymTableEntry { id: \"i\", definition_ref: nofile:5:30, usages: [nofile:13:14, nofile:25:17, nofile:27:31, nofile:27:16, nofile:31:35, nofile:31:16], category: Signal, ty: None },initial: SymTableEntry { id: \"initial\", definition_ref: nofile:10:19, usages: [], category: State, ty: None },middle: SymTableEntry { id: \"middle\", definition_ref: nofile:20:19, usages: [nofile:15:17, nofile:30:18], category: State, ty: None },n: SymTableEntry { id: \"n\", definition_ref: nofile:2:29, usages: [nofile:16:36, nofile:16:23, nofile:25:26, nofile:27:41, nofile:27:24, nofile:31:48, nofile:31:28], category: InputSignal, ty: None }", scope: Machine },//fibo/initial: ScopeTable { symbols: "c: SymTableEntry { id: \"c\", definition_ref: nofile:11:21, usages: [nofile:13:23, nofile:16:33], category: Signal, ty: None }", scope: State },//fibo/middle: ScopeTable { symbols: "c: SymTableEntry { id: \"c\", definition_ref: nofile:21:21, usages: [nofile:23:14, nofile:27:38, nofile:31:45], category: Signal, ty: None }", scope: State }, messages: [] }"#
r#"AnalysisResult { symbols: /: ScopeTable { symbols: "fibo: SymTableEntry { id: \"fibo\", definition_ref: nofile:2:17, usages: [], category: Machine, ty: None, ins: Some([\"n\"]), outs: Some([\"b\"]) }", scope: Global },//fibo: ScopeTable { symbols: "a: SymTableEntry { id: \"a\", definition_ref: nofile:5:20, usages: [nofile:13:17, nofile:16:15, nofile:23:20, nofile:31:20], category: Signal, ty: Some(\"field\"), ins: None, outs: None },b: SymTableEntry { id: \"b\", definition_ref: nofile:2:40, usages: [nofile:13:20, nofile:16:30, nofile:16:19, nofile:23:24, nofile:27:20, nofile:31:42, nofile:31:24], category: OutputSignal, ty: Some(\"field\"), ins: None, outs: None },i: SymTableEntry { id: \"i\", definition_ref: nofile:5:30, usages: [nofile:13:14, nofile:25:17, nofile:27:31, nofile:27:16, nofile:31:35, nofile:31:16], category: Signal, ty: None, ins: None, outs: None },initial: SymTableEntry { id: \"initial\", definition_ref: nofile:10:19, usages: [], category: State, ty: None, ins: None, outs: None },middle: SymTableEntry { id: \"middle\", definition_ref: nofile:20:19, usages: [nofile:15:17, nofile:30:18], category: State, ty: None, ins: None, outs: None },n: SymTableEntry { id: \"n\", definition_ref: nofile:2:29, usages: [nofile:16:36, nofile:16:23, nofile:25:26, nofile:27:41, nofile:27:24, nofile:31:48, nofile:31:28], category: InputSignal, ty: None, ins: None, outs: None }", scope: Machine },//fibo/initial: ScopeTable { symbols: "c: SymTableEntry { id: \"c\", definition_ref: nofile:11:21, usages: [nofile:13:23, nofile:16:33], category: Signal, ty: None, ins: None, outs: None }", scope: State },//fibo/middle: ScopeTable { symbols: "c: SymTableEntry { id: \"c\", definition_ref: nofile:21:21, usages: [nofile:23:14, nofile:27:38, nofile:31:45], category: Signal, ty: None, ins: None, outs: None }", scope: State }, messages: [] }"#
);
}
}
23 changes: 23 additions & 0 deletions src/compiler/semantic/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ pub struct SymTableEntry {
pub category: SymbolCategory,
/// Type
pub ty: Option<String>,
pub ins: Option<Vec<String>>,
pub outs: Option<Vec<String>>,
}

impl SymTableEntry {
Expand All @@ -70,6 +72,27 @@ impl SymTableEntry {
usages: Vec::new(),
category,
ty,
ins: None,
outs: None,
}
}

pub fn new_machine(
id: String,
definition_ref: DebugSymRef,
category: SymbolCategory,
ty: Option<String>,
input_params: Vec<String>,
output_params: Vec<String>,
) -> Self {
SymTableEntry {
id,
definition_ref,
usages: Vec::new(),
category,
ty,
ins: Some(input_params),
outs: Some(output_params),
}
}

Expand Down
Loading
Loading