From 63be983d745a8551b28642367dcd71319291223f Mon Sep 17 00:00:00 2001 From: schaeff Date: Thu, 5 Aug 2021 15:22:46 +0200 Subject: [PATCH] add tests, tweak out of range interpreter --- Cargo.lock | 1 + zokrates_core/Cargo.toml | 1 + zokrates_core/src/ir/interpreter.rs | 51 +++++----- zokrates_core/src/static_analysis/mod.rs | 6 +- zokrates_core/tests/out_of_range.rs | 117 ++++++++++++++++++++++- zokrates_fs_resolver/src/lib.rs | 13 ++- 6 files changed, 151 insertions(+), 38 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index c87c1802..cf5b77b4 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2394,6 +2394,7 @@ dependencies = [ "zokrates_common", "zokrates_embed", "zokrates_field", + "zokrates_fs_resolver", "zokrates_pest_ast", ] diff --git a/zokrates_core/Cargo.toml b/zokrates_core/Cargo.toml index e81f04fb..91b31714 100644 --- a/zokrates_core/Cargo.toml +++ b/zokrates_core/Cargo.toml @@ -59,6 +59,7 @@ sha2 = { version = "0.9.3", optional = true } [dev-dependencies] wasm-bindgen-test = "^0.3.0" pretty_assertions = "0.6.1" +zokrates_fs_resolver = { version = "0.5", path = "../zokrates_fs_resolver"} [build-dependencies] cc = { version = "1.0", features = ["parallel"], optional = true } diff --git a/zokrates_core/src/ir/interpreter.rs b/zokrates_core/src/ir/interpreter.rs index b68574f3..ef344e91 100644 --- a/zokrates_core/src/ir/interpreter.rs +++ b/zokrates_core/src/ir/interpreter.rs @@ -65,33 +65,27 @@ impl Interpreter { } } }, - Statement::Directive(ref d) => { - match (&d.solver, &d.inputs, self.should_try_out_of_range) { - (Solver::Bits(bitwidth), inputs, true) - if inputs[0].left.0.len() > 1 - || inputs[0].right.0.len() > 1 - && *bitwidth == T::get_required_bits() => - { - Self::try_solve_out_of_range(&d, &mut witness) - } - _ => { - let inputs: Vec<_> = d - .inputs - .iter() - .map(|i| i.evaluate(&witness).unwrap()) - .collect(); - match self.execute_solver(&d.solver, &inputs) { - Ok(res) => { - for (i, o) in d.outputs.iter().enumerate() { - witness.insert(*o, res[i].clone()); - } - continue; - } - Err(_) => return Err(Error::Solver), - }; - } + Statement::Directive(ref d) => match (&d.solver, self.should_try_out_of_range) { + (Solver::Bits(bitwidth), true) if *bitwidth >= T::get_required_bits() => { + Self::try_solve_out_of_range(&d, &mut witness) } - } + _ => { + let inputs: Vec<_> = d + .inputs + .iter() + .map(|i| i.evaluate(&witness).unwrap()) + .collect(); + match self.execute_solver(&d.solver, &inputs) { + Ok(res) => { + for (i, o) in d.outputs.iter().enumerate() { + witness.insert(*o, res[i].clone()); + } + continue; + } + Err(_) => return Err(Error::Solver), + }; + } + }, } } @@ -104,7 +98,9 @@ impl Interpreter { // we target the `2a - 2b` part of the `<` check by only returning out-of-range results // when the input is not a single summand let value = d.inputs[0].evaluate(&witness).unwrap(); + let candidate = value.to_biguint() + T::max_value().to_biguint() + T::from(1).to_biguint(); + let input = if candidate < T::from(2).to_biguint().pow(T::get_required_bits()) { candidate } else { @@ -123,6 +119,9 @@ impl Interpreter { } } assert_eq!(num, T::zero().to_biguint()); + + println!("RES {:?}", res); + for (i, o) in d.outputs.iter().enumerate() { witness.insert(*o, res[i].clone()); } diff --git a/zokrates_core/src/static_analysis/mod.rs b/zokrates_core/src/static_analysis/mod.rs index bf658118..b2dab63e 100644 --- a/zokrates_core/src/static_analysis/mod.rs +++ b/zokrates_core/src/static_analysis/mod.rs @@ -39,7 +39,7 @@ pub trait Analyse { pub enum Error { Reducer(self::reducer::Error), Propagation(self::propagation::Error), - NonConstantShift(self::constant_argument_checker::Error), + NonConstantArgument(self::constant_argument_checker::Error), } impl From for Error { @@ -56,7 +56,7 @@ impl From for Error { impl From for Error { fn from(e: constant_argument_checker::Error) -> Self { - Error::NonConstantShift(e) + Error::NonConstantArgument(e) } } @@ -65,7 +65,7 @@ impl fmt::Display for Error { match self { Error::Reducer(e) => write!(f, "{}", e), Error::Propagation(e) => write!(f, "{}", e), - Error::NonConstantShift(e) => write!(f, "{}", e), + Error::NonConstantArgument(e) => write!(f, "{}", e), } } } diff --git a/zokrates_core/tests/out_of_range.rs b/zokrates_core/tests/out_of_range.rs index 6d2f19ab..95fd5497 100644 --- a/zokrates_core/tests/out_of_range.rs +++ b/zokrates_core/tests/out_of_range.rs @@ -10,9 +10,10 @@ use zokrates_core::{ ir::Interpreter, }; use zokrates_field::Bn128Field; +use zokrates_fs_resolver::FileSystemResolver; #[test] -fn out_of_range() { +fn lt_field() { let source = r#" def main(private field a, private field b) -> field: field x = if a < b then 3333 else 4444 fi @@ -21,7 +22,7 @@ fn out_of_range() { "# .to_string(); - // let's try to prove that "10000 < 5555" is true by exploiting + // let's try to prove that "10000f < 5555f" is true by exploiting // the fact that `2*10000 - 2*5555` has two distinct bit decompositions // we chose the one which is out of range, ie the sum check features an overflow @@ -42,3 +43,115 @@ fn out_of_range() { ) .is_err()); } + +#[test] +fn lt_uint() { + let source = r#" + def main(private u32 a, private u32 b): + field x = if a < b then 3333 else 4444 fi + assert(x == 3333) + return + "# + .to_string(); + + // let's try to prove that "10000u32 < 5555u32" is true by exploiting + // the fact that `2*10000 - 2*5555` has two distinct bit decompositions + // we chose the one which is out of range, ie the sum check features an overflow + + let res: CompilationArtifacts = compile( + source, + "./path/to/file".into(), + None::<&dyn Resolver>, + &CompileConfig::default(), + ) + .unwrap(); + + let interpreter = Interpreter::try_out_of_range(); + + assert!(interpreter + .execute( + &res.prog(), + &[Bn128Field::from(10000), Bn128Field::from(5555)] + ) + .is_err()); +} + +#[test] +fn unpack256() { + let source = r#" + import "utils/pack/bool/unpack256" + + def main(private field a): + bool[256] bits = unpack256(a) + assert(bits[255]) + return + "# + .to_string(); + + // let's try to prove that the least significant bit of 0 is 1 + // we exploit the fact that the bits of 0 are the bits of p, and p is even + // we want this to still fail + + let stdlib_path = std::fs::canonicalize( + std::env::current_dir() + .unwrap() + .join("../zokrates_stdlib/stdlib"), + ) + .unwrap(); + + let res: CompilationArtifacts = compile( + source, + "./path/to/file".into(), + Some(&FileSystemResolver::with_stdlib_root( + stdlib_path.to_str().unwrap(), + )), + &CompileConfig::default(), + ) + .unwrap(); + + let interpreter = Interpreter::try_out_of_range(); + + assert!(interpreter + .execute(&res.prog(), &[Bn128Field::from(0)]) + .is_err()); +} + +#[test] +fn unpack256_unchecked() { + let source = r#" + import "utils/pack/bool/nonStrictUnpack256" + + def main(private field a): + bool[256] bits = nonStrictUnpack256(a) + assert(bits[255]) + return + "# + .to_string(); + + // let's try to prove that the least significant bit of 0 is 1 + // we exploit the fact that the bits of 0 are the bits of p, and p is even + // we want this to succeed as the non strict version does not enforce the bits to be in range + + let stdlib_path = std::fs::canonicalize( + std::env::current_dir() + .unwrap() + .join("../zokrates_stdlib/stdlib"), + ) + .unwrap(); + + let res: CompilationArtifacts = compile( + source, + "./path/to/file".into(), + Some(&FileSystemResolver::with_stdlib_root( + stdlib_path.to_str().unwrap(), + )), + &CompileConfig::default(), + ) + .unwrap(); + + let interpreter = Interpreter::try_out_of_range(); + + assert!(interpreter + .execute(&res.prog(), &[Bn128Field::from(0)]) + .is_ok()); +} diff --git a/zokrates_fs_resolver/src/lib.rs b/zokrates_fs_resolver/src/lib.rs index b38a0b17..1289bbe3 100644 --- a/zokrates_fs_resolver/src/lib.rs +++ b/zokrates_fs_resolver/src/lib.rs @@ -26,17 +26,16 @@ impl<'a> Resolver for FileSystemResolver<'a> { ) -> Result<(String, PathBuf), io::Error> { let source = Path::new(&import_location); - if !current_location.is_file() { - return Err(io::Error::new( - io::ErrorKind::Other, - format!("{} was expected to be a file", current_location.display()), - )); - } - // paths starting with `./` or `../` are interpreted relative to the current file // other paths `abc/def` are interpreted relative to the standard library root path let base = match source.components().next() { Some(Component::CurDir) | Some(Component::ParentDir) => { + if !current_location.is_file() { + return Err(io::Error::new( + io::ErrorKind::Other, + format!("{} was expected to be a file", current_location.display()), + )); + } current_location.parent().unwrap().into() } _ => PathBuf::from(self.stdlib_root_path.unwrap_or("")),