Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove branch isolation #1353

Merged
merged 6 commits into from
Nov 9, 2023
Merged
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
1 change: 1 addition & 0 deletions changelogs/unreleased/1353-dark64
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Remove expensive and buggy branch isolation
43 changes: 0 additions & 43 deletions zokrates_analysis/src/branch_isolator.rs

This file was deleted.

13 changes: 0 additions & 13 deletions zokrates_analysis/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@

mod assembly_transformer;
mod boolean_array_comparator;
mod branch_isolator;
mod condition_redefiner;
mod constant_argument_checker;
mod constant_resolver;
Expand All @@ -25,7 +24,6 @@ mod variable_write_remover;
mod zir_propagation;

use self::boolean_array_comparator::BooleanArrayComparator;
use self::branch_isolator::Isolator;
use self::condition_redefiner::ConditionRedefiner;
use self::constant_argument_checker::ConstantArgumentChecker;
use self::flatten_complex_types::Flattener;
Expand Down Expand Up @@ -132,17 +130,6 @@ pub fn analyse<'ast, T: Field>(
let r = ConstantResolver::inline(p);
log::trace!("\n{}", r);

// isolate branches
let r = if config.isolate_branches {
log::debug!("Static analyser: Isolate branches");
let r = Isolator::isolate(r);
log::trace!("\n{}", r);
r
} else {
log::debug!("Static analyser: Branch isolation skipped");
r
};

// include logs
let r = if config.debug {
log::debug!("Static analyser: Include logs");
Expand Down
2 changes: 1 addition & 1 deletion zokrates_ast/src/ir/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ impl<T: Field> fmt::Display for ConstraintStatement<T> {
self.error
.as_ref()
.map(|e| format!(" // {}", e))
.unwrap_or_else(|| "".to_string())
.unwrap_or_default()
)
}
}
Expand Down
3 changes: 3 additions & 0 deletions zokrates_ast/src/lib.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
// see https://github.com/mcarton/rust-derivative/issues/115
#![allow(clippy::incorrect_partial_ord_impl_on_ord_type)]

pub mod common;
pub mod flat;
pub mod ir;
Expand Down
7 changes: 2 additions & 5 deletions zokrates_ast/src/untyped/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -543,11 +543,8 @@ impl<'ast> fmt::Display for Range<'ast> {
self.from
.as_ref()
.map(|e| e.to_string())
.unwrap_or_else(|| "".to_string()),
self.to
.as_ref()
.map(|e| e.to_string())
.unwrap_or_else(|| "".to_string())
.unwrap_or_default(),
self.to.as_ref().map(|e| e.to_string()).unwrap_or_default()
)
}
}
Expand Down
3 changes: 1 addition & 2 deletions zokrates_book/src/language/control_flow.md
Original file line number Diff line number Diff line change
Expand Up @@ -47,9 +47,8 @@ Now the two caveats:
```zokrates
{{#include ../../../zokrates_cli/examples/book/conditional_panic.zok}}
```
The experimental flag `--branch-isolation` can be activated in the CLI in order to restrict any unsatisfied constraint to make the execution fail only if it is in a logically executed branch. This way, the execution of the program above will always succeed.

>The reason for these caveats is that the program is compiled down to an arithmetic circuit. This construct does not support jumping to a branch depending on a condition as you could do on traditional architectures. Instead, all branches are inlined as if they were printed on a circuit board. The `branch-isolation` feature comes with overhead for each assertion in each branch, and this overhead compounds when deeply nesting conditionals.
>The reason for these caveats is that the program is compiled down to an arithmetic circuit. This construct does not support jumping to a branch depending on a condition as you could do on traditional architectures. Instead, all branches are inlined as if they were printed on a circuit board.
### For loops

Expand Down
15 changes: 3 additions & 12 deletions zokrates_cli/src/ops/check.rs
Original file line number Diff line number Diff line change
Expand Up @@ -44,11 +44,6 @@ pub fn subcommand() -> App<'static, 'static> {
.possible_values(cli_constants::CURVES)
.default_value(BN128),
)
.arg(Arg::with_name("isolate-branches")
.long("isolate-branches")
.help("Isolate the execution of branches: a panic in a branch only makes the program panic if this branch is being logically executed")
.required(false)
)
}

pub fn exec(sub_matches: &ArgMatches) -> Result<(), String> {
Expand Down Expand Up @@ -94,17 +89,13 @@ fn cli_check<T: Field>(sub_matches: &ArgMatches) -> Result<(), String> {
)),
}?;

let config =
CompileConfig::default().isolate_branches(sub_matches.is_present("isolate-branches"));

let config = CompileConfig::default();
let resolver = FileSystemResolver::with_stdlib_root(stdlib_path);

check::<T, _>(source, path, Some(&resolver), &config).map_err(|e| {
format!(
"Check failed:\n\n{}",
e.0.iter()
.map(|e| fmt_error(e))
.collect::<Vec<_>>()
.join("\n\n")
e.0.iter().map(fmt_error).collect::<Vec<_>>().join("\n\n")
)
})?;

Expand Down
131 changes: 67 additions & 64 deletions zokrates_cli/src/ops/compile.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,62 +18,71 @@ use zokrates_fs_resolver::FileSystemResolver;
pub fn subcommand() -> App<'static, 'static> {
SubCommand::with_name("compile")
.about("Compiles into a runnable constraint system")
.arg(Arg::with_name("input")
.short("i")
.long("input")
.help("Path of the source code")
.value_name("FILE")
.takes_value(true)
.required(true)
).arg(Arg::with_name("stdlib-path")
.long("stdlib-path")
.help("Path to the standard library")
.value_name("PATH")
.takes_value(true)
.required(false)
.env("ZOKRATES_STDLIB")
.default_value(cli_constants::DEFAULT_STDLIB_PATH.as_str())
).arg(Arg::with_name("abi-spec")
.short("s")
.long("abi-spec")
.help("Path of the ABI specification")
.value_name("FILE")
.takes_value(true)
.required(false)
.default_value(cli_constants::ABI_SPEC_DEFAULT_PATH)
).arg(Arg::with_name("output")
.short("o")
.long("output")
.help("Path of the output binary")
.value_name("FILE")
.takes_value(true)
.required(false)
.default_value(cli_constants::FLATTENED_CODE_DEFAULT_PATH)
).arg(Arg::with_name("r1cs")
.short("r1cs")
.long("r1cs")
.help("Path of the output r1cs file")
.value_name("FILE")
.takes_value(true)
.required(false)
.default_value(cli_constants::CIRCOM_R1CS_DEFAULT_PATH)
).arg(Arg::with_name("curve")
.short("c")
.long("curve")
.help("Curve to be used in the compilation")
.takes_value(true)
.required(false)
.possible_values(cli_constants::CURVES)
.default_value(BN128)
).arg(Arg::with_name("isolate-branches")
.long("isolate-branches")
.help("Isolate the execution of branches: a panic in a branch only makes the program panic if this branch is being logically executed")
.required(false)
).arg(Arg::with_name("debug")
.long("debug")
.help("Include logs")
.required(false)
)
.arg(
Arg::with_name("input")
.short("i")
.long("input")
.help("Path of the source code")
.value_name("FILE")
.takes_value(true)
.required(true),
)
.arg(
Arg::with_name("stdlib-path")
.long("stdlib-path")
.help("Path to the standard library")
.value_name("PATH")
.takes_value(true)
.required(false)
.env("ZOKRATES_STDLIB")
.default_value(cli_constants::DEFAULT_STDLIB_PATH.as_str()),
)
.arg(
Arg::with_name("abi-spec")
.short("s")
.long("abi-spec")
.help("Path of the ABI specification")
.value_name("FILE")
.takes_value(true)
.required(false)
.default_value(cli_constants::ABI_SPEC_DEFAULT_PATH),
)
.arg(
Arg::with_name("output")
.short("o")
.long("output")
.help("Path of the output binary")
.value_name("FILE")
.takes_value(true)
.required(false)
.default_value(cli_constants::FLATTENED_CODE_DEFAULT_PATH),
)
.arg(
Arg::with_name("r1cs")
.short("r1cs")
.long("r1cs")
.help("Path of the output r1cs file")
.value_name("FILE")
.takes_value(true)
.required(false)
.default_value(cli_constants::CIRCOM_R1CS_DEFAULT_PATH),
)
.arg(
Arg::with_name("curve")
.short("c")
.long("curve")
.help("Curve to be used in the compilation")
.takes_value(true)
.required(false)
.possible_values(cli_constants::CURVES)
.default_value(BN128),
)
.arg(
Arg::with_name("debug")
.long("debug")
.help("Include logs")
.required(false),
)
}

pub fn exec(sub_matches: &ArgMatches) -> Result<(), String> {
Expand Down Expand Up @@ -124,10 +133,7 @@ fn cli_compile<T: Field>(sub_matches: &ArgMatches) -> Result<(), String> {
)),
}?;

let config = CompileConfig::default()
.isolate_branches(sub_matches.is_present("isolate-branches"))
.debug(sub_matches.is_present("debug"));

let config = CompileConfig::default().debug(sub_matches.is_present("debug"));
let resolver = FileSystemResolver::with_stdlib_root(stdlib_path);

log::debug!("Compile");
Expand All @@ -138,10 +144,7 @@ fn cli_compile<T: Field>(sub_matches: &ArgMatches) -> Result<(), String> {
.map_err(|e| {
format!(
"Compilation failed:\n\n{}",
e.0.iter()
.map(|e| fmt_error(e))
.collect::<Vec<_>>()
.join("\n\n")
e.0.iter().map(fmt_error).collect::<Vec<_>>().join("\n\n")
)
})?;

Expand Down
Loading
Loading