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

Commit

Permalink
Merge branch 'chiquito-2024' into rutefig/274-using-m-type-to-keep-de…
Browse files Browse the repository at this point in the history
…bugsym-in-expr
  • Loading branch information
rutefig committed Aug 29, 2024
2 parents dd7a3eb + 1d3f060 commit 9d28861
Show file tree
Hide file tree
Showing 13 changed files with 194 additions and 88 deletions.
10 changes: 5 additions & 5 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -8,18 +8,18 @@ authors = ["Leo Lara <[email protected]>"]
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[patch.crates-io]
halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2.git", default-features = false, rev = "da4983e" }
halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2.git", default-features = false, rev = "bc857a7" }

[patch."https://github.com/scroll-tech/halo2.git"]
halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2.git", default-features = false, rev = "da4983e" }
halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2.git", default-features = false, rev = "bc857a7" }

[dependencies]
pyo3 = { version = "0.19.1", features = ["extension-module"] }

halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2.git", default-features = false, features = [ "circuit-params", "derive_serde"], rev = "da4983e"}
halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2.git", default-features = false, features = [ "circuit-params", "derive_serde"], rev = "bc857a7"}

halo2_middleware = { git = "https://github.com/privacy-scaling-explorations/halo2.git", rev = "da4983e" }
halo2_backend = { git = "https://github.com/privacy-scaling-explorations/halo2.git", features = ["derive_serde"], rev = "da4983e" }
halo2_middleware = { git = "https://github.com/privacy-scaling-explorations/halo2.git", rev = "bc857a7" }
halo2_backend = { git = "https://github.com/privacy-scaling-explorations/halo2.git", features = ["derive_serde"], rev = "bc857a7" }

num-bigint = { version = "0.4", features = ["rand"] }
uuid = { version = "1.4.0", features = ["v1", "rng"] }
Expand Down
13 changes: 13 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, call, state) => {
self.compiler_statement_hyper_transition(dsym, ids, call, state)
}
_ => vec![],
}
}
Expand Down Expand Up @@ -420,6 +423,16 @@ impl<F: From<u64> + TryInto<u32> + Clone + Debug, V: Clone + Debug> CompilationU

result
}

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

fn flatten_bin_op<F: Clone, V: Clone>(
Expand Down
86 changes: 45 additions & 41 deletions src/compiler/compiler.rs
Original file line number Diff line number Diff line change
Expand Up @@ -561,57 +561,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 @@ -842,4 +807,43 @@ 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());

let circuit = "
machine caller (signal n) (signal b: field) {
-> final {
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_ok());

// 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;
}
";

let debug_sym_ref_factory = DebugSymRefFactory::new("", circuit);
let result = TLDeclsParser::new().parse(&debug_sym_ref_factory, circuit);

assert!(result.is_ok());
}
}
11 changes: 11 additions & 0 deletions src/compiler/semantic/analyser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -272,6 +272,11 @@ 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);
}
}
}

Expand Down Expand Up @@ -308,6 +313,12 @@ impl Analyser {
} => {
self.extract_usages_expression(&sub);
}
Expression::Call(_, fun, exprs) => {
self.collect_id_usages(&[fun]);
exprs
.into_iter()
.for_each(|expr| self.extract_usages_expression(&expr));
}
_ => {}
}
}
Expand Down
3 changes: 3 additions & 0 deletions src/compiler/semantic/rules.rs
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,9 @@ fn undeclared_rule(analyser: &mut Analyser, expr: &Expression<BigInt, Identifier
undeclared_rule(analyser, when_false);
}
Expression::Const(_, _) | Expression::True(_) | Expression::False(_) => {}
Expression::Call(_, _, args) => {
args.iter().for_each(|arg| undeclared_rule(analyser, arg));
}
}
}

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 @@ -254,6 +254,7 @@ impl SetupInterpreter {

SignalAssignment(_, _, _) | WGAssignment(_, _, _) => vec![],
SignalDecl(_, _) | WGVarDecl(_, _) => vec![],
HyperTransition(_, _, _, _) => todo!("Implement compilation for hyper transitions"),
};

self.add_poly_constraints(
Expand Down
3 changes: 3 additions & 0 deletions src/interpreter/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,9 @@ pub(crate) fn eval_expr<F: Field + Hash, V: Identifiable>(
Const(_, v) => Ok(Value::Field(F::from_big_int(v))),
True(_) => Ok(Value::Bool(true)),
False(_) => Ok(Value::Bool(false)),
Call(_, _, _) => {
todo!("Needs specs. Evaluate the argument expressions, evaluate the function output?")
}
}
.map_err(|msg| Message::RuntimeErr {
msg,
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(_, _, _, _) => todo!("Needs specs"),
}
}

Expand Down
15 changes: 15 additions & 0 deletions src/parser/ast/expression.rs
Original file line number Diff line number Diff line change
Expand Up @@ -193,6 +193,12 @@ pub enum Expression<F, V> {
Const(DebugSymRef, F),
True(DebugSymRef),
False(DebugSymRef),
/// Function or machine call.
/// Tuple values:
/// - debug symbol reference;
/// - function/machine ID;
/// - call argument expressions vector.
Call(DebugSymRef, V, Vec<Expression<F, V>>),
}

// Shorthand for BigInt expression
Expand All @@ -217,6 +223,9 @@ impl<F, V> Expression<F, V> {
Const(_, _) => true,
True(_) => false,
False(_) => false,
Call(_, _, _) => {
todo!("Needs specs. For a function call, depends on the function return type?")
}
}
}

Expand All @@ -234,6 +243,9 @@ impl<F, V> Expression<F, V> {

when_true.is_logic()
}
Expression::Call { .. } => {
todo!("Needs specs. For a function call, depends on the function return type?")
}
_ => false,
}
}
Expand All @@ -247,6 +259,7 @@ impl<F, V> Expression<F, V> {
Expression::Const(dsym, _) => dsym,
Expression::True(dsym) => dsym,
Expression::False(dsym) => dsym,
Expression::Call(dsym, _, _) => dsym,
}
}

Expand All @@ -260,6 +273,7 @@ impl<F, V> Expression<F, V> {
Expression::Query(_, _) => false,
Expression::True(_) => false,
Expression::False(_) => false,
Expression::Call(_, _, _) => false,
}
}
}
Expand Down Expand Up @@ -315,6 +329,7 @@ impl<F: Debug, V: Debug> Debug for Expression<F, V> {

Expression::True(_) => write!(f, "true"),
Expression::False(_) => write!(f, "false"),
Expression::Call(_, fun, exprs) => write!(f, "{:?}({:?})", fun, exprs),
}
}
}
33 changes: 32 additions & 1 deletion src/parser/ast/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -141,6 +141,24 @@ impl PartialEq for DebugSymRef {
}
}

/// Interface of the debug symbol reference to use with the Chiquito language server
pub trait Spanned {
/// Get span start
fn get_start(&self) -> usize;
/// Get span end
fn get_end(&self) -> usize;
}

impl Spanned for DebugSymRef {
fn get_start(&self) -> usize {
self.start
}

fn get_end(&self) -> usize {
self.end
}
}

#[derive(Clone, PartialEq, Eq)]
pub struct Identifier(
/// Name
Expand Down Expand Up @@ -227,7 +245,20 @@ mod test {

use codespan_reporting::files::SimpleFile;

use crate::parser::ast::{DebugSymRef, Identifier};
use crate::parser::ast::{DebugSymRef, Identifier, Spanned};

#[test]
fn test_language_server_interface() {
let debug_sym_ref = DebugSymRef {
start: 0,
end: 1,
file: Arc::new(SimpleFile::new("file_path".to_string(), "".to_string())),
virt: false,
};

assert_eq!(debug_sym_ref.get_start(), 0);
assert_eq!(debug_sym_ref.get_end(), 1);
}

#[test]
fn test_from_string() {
Expand Down
Loading

0 comments on commit 9d28861

Please sign in to comment.