github-mig/ZoKrates
github-mig/ZoKrates
1
0
Fork 0
mirror of synced 2025-09-24 04:40:05 +00:00
Code Issues Projects Releases Wiki Activity

introduce strict lt check, test with modified interpreter

Browse source
This commit is contained in:
schaeff 2020-06-03 13:47:46 +02:00
parent c3228f81e1
commit f37c28230c
11 changed files with 306 additions and 156 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
zokrates_cli/src/bin.rs
View file

@ -458,8 +458,10 @@ fn cli() -> Result<(), String> {
}
.map_err(|e| format!("Could not parse argument: {}", e))?;
let witness = ir_prog
.execute(&arguments.encode())
let interpreter = ir::Interpreter::default();
let witness = interpreter
.execute(&ir_prog, &arguments.encode())
.map_err(|e| format!("Execution failed: {}", e))?;
use zokrates_abi::Decode;
@ -705,9 +707,10 @@ mod tests {
let artifacts: CompilationArtifacts<FieldPrime> =
compile(source, path, Some(&fs_resolve)).unwrap();
let _ = artifacts
.prog()
.execute(&vec![FieldPrime::from(0)])
let interpreter = ir::Interpreter::default();
let _ = interpreter
.execute(&artifacts.prog(), &vec![FieldPrime::from(0)])
.unwrap();
}
}
@ -732,9 +735,10 @@ mod tests {
let artifacts: CompilationArtifacts<FieldPrime> =
compile(source, path, Some(&fs_resolve)).unwrap();
let _ = artifacts
.prog()
.execute(&vec![FieldPrime::from(0)])
let interpreter = ir::Interpreter::default();
let _ = interpreter
.execute(&artifacts.prog(), &vec![FieldPrime::from(0)])
.unwrap();
}
}

5
zokrates_core/src/embed.rs
View file

@ -330,6 +330,7 @@ mod tests {
#[cfg(test)]
mod sha256 {
use super::*;
use ir::Interpreter;
#[test]
fn generate_sha256_constraints() {
@ -401,7 +402,9 @@ mod tests {
.chain((0..256).map(|_| FieldPrime::from(1)))
.collect();
prog.execute(&input).unwrap();
let interpreter = Interpreter::default();
interpreter.execute(&prog, &input).unwrap();
}
}
}

229
zokrates_core/src/ir/interpreter.rs
View file

@ -1,16 +1,42 @@
use crate::flat_absy::flat_variable::FlatVariable;
use crate::ir::{LinComb, Prog, QuadComb, Statement, Witness};
use crate::solvers::Executable;
use ir::Directive;
use solvers::Solver;
use std::collections::BTreeMap;
use std::fmt;
use zokrates_embed::generate_sha256_round_witness;
use zokrates_field::field::Field;
pub type ExecutionResult<T> = Result<Witness<T>, Error>;
impl<T: Field> Prog<T> {
pub fn execute(&self, inputs: &Vec<T>) -> ExecutionResult<T> {
let main = &self.main;
self.check_inputs(&inputs)?;
impl<T: Field> Prog<T> {}
pub struct Interpreter {
/// Whether we should try to give out-of-range bit decompositions when the input is not a single summand.
/// Used to do targetted testing of `<` flattening, making sure the bit decomposition we base the result on is unique.
should_try_out_of_range: bool,
}
impl Default for Interpreter {
fn default() -> Interpreter {
Interpreter {
should_try_out_of_range: false,
}
}
}
impl Interpreter {
pub fn try_out_of_range() -> Interpreter {
Interpreter {
should_try_out_of_range: true,
}
}
}
impl Interpreter {
pub fn execute<T: Field>(&self, program: &Prog<T>, inputs: &Vec<T>) -> ExecutionResult<T> {
let main = &program.main;
self.check_inputs(&program, &inputs)?;
let mut witness = BTreeMap::new();
witness.insert(FlatVariable::one(), T::one());
for (arg, value) in main.arguments.iter().zip(inputs.iter()) {
@ -36,20 +62,27 @@ impl<T: Field> Prog<T> {
}
},
Statement::Directive(ref d) => {
let input_values: Vec<T> = d
.inputs
.iter()
.map(|i| i.evaluate(&witness).unwrap())
.collect();
match d.solver.execute(&input_values) {
Ok(res) => {
for (i, o) in d.outputs.iter().enumerate() {
witness.insert(o.clone(), res[i].clone());
}
continue;
match (&d.solver, &d.inputs, self.should_try_out_of_range) {
(Solver::Bits, inputs, true) if inputs[0].0.len() > 1 => {
Self::try_solve_out_of_range(&d, &mut witness)
}
Err(_) => return Err(Error::Solver),
};
_ => {
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.clone(), res[i].clone());
}
continue;
}
Err(_) => return Err(Error::Solver),
};
}
}
}
}
}
@ -57,16 +90,100 @@ impl<T: Field> Prog<T> {
Ok(Witness(witness))
}
fn check_inputs<U>(&self, inputs: &Vec<U>) -> Result<(), Error> {
if self.main.arguments.len() == inputs.len() {
fn try_solve_out_of_range<T: Field>(d: &Directive<T>, witness: &mut BTreeMap<FlatVariable, T>) {
use num::traits::Pow;
// 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 {
value.to_biguint()
};
let mut num = input.clone();
let mut res = vec![];
let bits = 254;
for i in (0..bits).rev() {
if T::from(2).to_biguint().pow(i as usize) <= num {
num = num - T::from(2).to_biguint().pow(i as usize);
res.push(T::one());
} else {
res.push(T::zero());
}
}
assert_eq!(num, T::zero().to_biguint());
for (i, o) in d.outputs.iter().enumerate() {
witness.insert(o.clone(), res[i].clone());
}
}
fn check_inputs<T: Field, U>(&self, program: &Prog<T>, inputs: &Vec<U>) -> Result<(), Error> {
if program.main.arguments.len() == inputs.len() {
Ok(())
} else {
Err(Error::WrongInputCount {
expected: self.main.arguments.len(),
expected: program.main.arguments.len(),
received: inputs.len(),
})
}
}
fn execute_solver<T: Field>(&self, s: &Solver, inputs: &Vec<T>) -> Result<Vec<T>, String> {
use solvers::Signed;
let (expected_input_count, expected_output_count) = s.get_signature();
assert!(inputs.len() == expected_input_count);
let res = match s {
Solver::ConditionEq => match inputs[0].is_zero() {
true => vec![T::zero(), T::one()],
false => vec![T::one(), T::one() / inputs[0].clone()],
},
Solver::Bits => {
use num::traits::Pow;
let input = if self.should_try_out_of_range
&& inputs[0].to_biguint() + (T::max_value() + T::from(1)).to_biguint()
< T::from(2).to_biguint().pow(T::get_required_bits())
{
inputs[0].to_biguint() + (T::max_value() + T::from(1)).to_biguint()
} else {
inputs[0].to_biguint()
};
let mut num = input.clone();
let mut res = vec![];
let bits = 254;
for i in (0..bits).rev() {
if T::from(2).to_biguint().pow(i as usize) <= num {
num = num - T::from(2).to_biguint().pow(i as usize);
res.push(T::one());
} else {
res.push(T::zero());
}
}
assert_eq!(num, T::zero().to_biguint());
res
}
Solver::Div => vec![inputs[0].clone() / inputs[1].clone()],
Solver::Sha256Round => {
let i = &inputs[0..512];
let h = &inputs[512..];
let i: Vec<_> = i.iter().map(|x| x.clone().into_bellman()).collect();
let h: Vec<_> = h.iter().map(|x| x.clone().into_bellman()).collect();
assert!(h.len() == 256);
generate_sha256_round_witness::<T::BellmanEngine>(&i, &h)
.into_iter()
.map(|x| T::from_bellman(x))
.collect()
}
};
assert_eq!(res.len(), expected_output_count);
Ok(res)
}
}
impl<T: Field> LinComb<T> {
@ -125,3 +242,73 @@ impl fmt::Debug for Error {
write!(f, "{}", self)
}
}
#[cfg(test)]
mod tests {
use super::*;
use zokrates_field::field::FieldPrime;
mod eq_condition {
// Wanted: (Y = (X != 0) ? 1 : 0)
// # Y = if X == 0 then 0 else 1 fi
// # M = if X == 0 then 1 else 1/X fi
use super::*;
#[test]
fn execute() {
let cond_eq = Solver::ConditionEq;
let inputs = vec![0];
let interpreter = Interpreter::default();
let r = interpreter
.execute_solver(
&cond_eq,
&inputs.iter().map(|&i| FieldPrime::from(i)).collect(),
)
.unwrap();
let res: Vec<FieldPrime> = vec![0, 1].iter().map(|&i| FieldPrime::from(i)).collect();
assert_eq!(r, &res[..]);
}
#[test]
fn execute_non_eq() {
let cond_eq = Solver::ConditionEq;
let inputs = vec![1];
let interpreter = Interpreter::default();
let r = interpreter
.execute_solver(
&cond_eq,
&inputs.iter().map(|&i| FieldPrime::from(i)).collect(),
)
.unwrap();
let res: Vec<FieldPrime> = vec![1, 1].iter().map(|&i| FieldPrime::from(i)).collect();
assert_eq!(r, &res[..]);
}
}
#[test]
fn bits_of_one() {
let inputs = vec![FieldPrime::from(1)];
let interpreter = Interpreter::default();
let res = interpreter.execute_solver(&Solver::Bits, &inputs).unwrap();
assert_eq!(res[253], FieldPrime::from(1));
for i in 0..253 {
assert_eq!(res[i], FieldPrime::from(0));
}
}
#[test]
fn bits_of_42() {
let inputs = vec![FieldPrime::from(42)];
let interpreter = Interpreter::default();
let res = interpreter.execute_solver(&Solver::Bits, &inputs).unwrap();
assert_eq!(res[253], FieldPrime::from(0));
assert_eq!(res[252], FieldPrime::from(1));
assert_eq!(res[251], FieldPrime::from(0));
assert_eq!(res[250], FieldPrime::from(1));
assert_eq!(res[249], FieldPrime::from(0));
assert_eq!(res[248], FieldPrime::from(1));
assert_eq!(res[247], FieldPrime::from(0));
}
}

2
zokrates_core/src/ir/mod.rs
View file

@ -13,7 +13,7 @@ mod witness;
pub use self::expression::QuadComb;
pub use self::expression::{CanonicalLinComb, LinComb};
pub use self::interpreter::{Error, ExecutionResult};
pub use self::interpreter::{Error, ExecutionResult, Interpreter};
pub use self::witness::Witness;
#[derive(Debug, Serialize, Deserialize, Clone, PartialEq, Hash, Eq)]

7
zokrates_core/src/proof_system/bn128/g16.rs
View file

@ -368,9 +368,10 @@ mod tests {
private: vec![false],
};
let witness = program
.clone()
.execute(&vec![FieldPrime::from(42)])
let interpreter = Interpreter::default();
let witness = interpreter
.execute(&program, &vec![FieldPrime::from(42)])
.unwrap();
let computation = Computation::with_witness(program, witness);

41
zokrates_core/src/proof_system/bn128/utils/bellman.rs
View file

@ -294,6 +294,7 @@ mod parse {
mod tests {
use super::*;
use crate::ir::{Function, LinComb};
use ir::Interpreter;
use zokrates_field::field::FieldPrime;
mod prove {
@ -311,7 +312,9 @@ mod tests {
private: vec![],
};
let witness = program.clone().execute(&vec![]).unwrap();
let interpreter = Interpreter::default();
let witness = interpreter.execute(&program, &vec![]).unwrap();
let computation = Computation::with_witness(program, witness);
let params = computation.clone().setup();
@ -333,7 +336,11 @@ mod tests {
private: vec![true],
};
let witness = program.clone().execute(&vec![FieldPrime::from(0)]).unwrap();
let interpreter = Interpreter::default();
let witness = interpreter
.execute(&program, &vec![FieldPrime::from(0)])
.unwrap();
let computation = Computation::with_witness(program, witness);
let params = computation.clone().setup();
@ -355,7 +362,11 @@ mod tests {
private: vec![false],
};
let witness = program.clone().execute(&vec![FieldPrime::from(0)]).unwrap();
let interpreter = Interpreter::default();
let witness = interpreter
.execute(&program, &vec![FieldPrime::from(0)])
.unwrap();
let computation = Computation::with_witness(program, witness);
let params = computation.clone().setup();
@ -377,7 +388,9 @@ mod tests {
private: vec![],
};
let witness = program.clone().execute(&vec![]).unwrap();
let interpreter = Interpreter::default();
let witness = interpreter.execute(&program, &vec![]).unwrap();
let computation = Computation::with_witness(program, witness);
let params = computation.clone().setup();
@ -411,9 +424,10 @@ mod tests {
private: vec![true, false],
};
let witness = program
.clone()
.execute(&vec![FieldPrime::from(3), FieldPrime::from(4)])
let interpreter = Interpreter::default();
let witness = interpreter
.execute(&program, &vec![FieldPrime::from(3), FieldPrime::from(4)])
.unwrap();
let computation = Computation::with_witness(program, witness);
@ -436,7 +450,11 @@ mod tests {
private: vec![false],
};
let witness = program.clone().execute(&vec![FieldPrime::from(3)]).unwrap();
let interpreter = Interpreter::default();
let witness = interpreter
.execute(&program, &vec![FieldPrime::from(3)])
.unwrap();
let computation = Computation::with_witness(program, witness);
let params = computation.clone().setup();
@ -460,9 +478,10 @@ mod tests {
private: vec![true, false],
};
let witness = program
.clone()
.execute(&vec![FieldPrime::from(3), FieldPrime::from(4)])
let interpreter = Interpreter::default();
let witness = interpreter
.execute(&program, &vec![FieldPrime::from(3), FieldPrime::from(4)])
.unwrap();
let computation = Computation::with_witness(program, witness);

106
zokrates_core/src/solvers/mod.rs
View file

@ -1,5 +1,4 @@
use std::fmt;
use zokrates_embed::generate_sha256_round_witness;
use zokrates_field::field::Field;
#[derive(Clone, PartialEq, Debug, Serialize, Deserialize, Hash, Eq)]
@ -27,51 +26,6 @@ impl Signed for Solver {
}
}
impl<T: Field> Executable<T> for Solver {
fn execute(&self, inputs: &Vec<T>) -> Result<Vec<T>, String> {
let (expected_input_count, expected_output_count) = self.get_signature();
assert!(inputs.len() == expected_input_count);
let res = match self {
Solver::ConditionEq => match inputs[0].is_zero() {
true => vec![T::zero(), T::one()],
false => vec![T::one(), T::one() / inputs[0].clone()],
},
Solver::Bits => {
let mut num = inputs[0].clone();
let mut res = vec![];
let bits = 254;
for i in (0..bits).rev() {
if T::from(2).pow(i) <= num {
num = num - T::from(2).pow(i);
res.push(T::one());
} else {
res.push(T::zero());
}
}
assert_eq!(num, T::zero());
res
}
Solver::Div => vec![inputs[0].clone() / inputs[1].clone()],
Solver::Sha256Round => {
let i = &inputs[0..512];
let h = &inputs[512..];
let i: Vec<_> = i.iter().map(|x| x.clone().into_bellman()).collect();
let h: Vec<_> = h.iter().map(|x| x.clone().into_bellman()).collect();
assert!(h.len() == 256);
generate_sha256_round_witness::<T::BellmanEngine>(&i, &h)
.into_iter()
.map(|x| T::from_bellman(x))
.collect()
}
};
assert_eq!(res.len(), expected_output_count);
Ok(res)
}
}
impl Solver {
pub fn bits() -> Self {
Solver::Bits
@ -85,63 +39,3 @@ pub trait Executable<T: Field>: Signed {
pub trait Signed {
fn get_signature(&self) -> (usize, usize);
}
#[cfg(test)]
mod tests {
use super::*;
use zokrates_field::field::FieldPrime;
mod eq_condition {
// Wanted: (Y = (X != 0) ? 1 : 0)
// # Y = if X == 0 then 0 else 1 fi
// # M = if X == 0 then 1 else 1/X fi
use super::*;
#[test]
fn execute() {
let cond_eq = Solver::ConditionEq;
let inputs = vec![0];
let r = cond_eq
.execute(&inputs.iter().map(|&i| FieldPrime::from(i)).collect())
.unwrap();
let res: Vec<FieldPrime> = vec![0, 1].iter().map(|&i| FieldPrime::from(i)).collect();
assert_eq!(r, &res[..]);
}
#[test]
fn execute_non_eq() {
let cond_eq = Solver::ConditionEq;
let inputs = vec![1];
let r = cond_eq
.execute(&inputs.iter().map(|&i| FieldPrime::from(i)).collect())
.unwrap();
let res: Vec<FieldPrime> = vec![1, 1].iter().map(|&i| FieldPrime::from(i)).collect();
assert_eq!(r, &res[..]);
}
}
#[test]
fn bits_of_one() {
let inputs = vec![FieldPrime::from(1)];
let res = Solver::Bits.execute(&inputs).unwrap();
assert_eq!(res[253], FieldPrime::from(1));
for i in 0..252 {
assert_eq!(res[i], FieldPrime::from(0));
}
}
#[test]
fn bits_of_42() {
let inputs = vec![FieldPrime::from(42)];
let res = Solver::Bits.execute(&inputs).unwrap();
assert_eq!(res[253], FieldPrime::from(0));
assert_eq!(res[252], FieldPrime::from(1));
assert_eq!(res[251], FieldPrime::from(0));
assert_eq!(res[250], FieldPrime::from(1));
assert_eq!(res[249], FieldPrime::from(0));
assert_eq!(res[248], FieldPrime::from(1));
assert_eq!(res[247], FieldPrime::from(0));
}
}

32
zokrates_core/tests/out_of_range.rs Normal file
View file

@ -0,0 +1,32 @@
extern crate zokrates_core;
extern crate zokrates_field;
use std::io;
use zokrates_core::{
compile::{compile, CompilationArtifacts, CompileErrors, Resolve},
ir::Interpreter,
};
use zokrates_field::field::{Field, FieldPrime};
#[test]
fn out_of_range() {
let source = r#"
def main(field a) -> ():
true == a < 1
return
"#
.to_string();
// let's try to prove that "2 < 1" is true by exploiting
// the fact that `2*2 - 2*1` has two distinct bit decompositions
// we chose the one which is out of range, ie the sum check features an overflow
let res: CompilationArtifacts<FieldPrime> =
compile(source, "./path/to/file".into(), None::<Resolve<io::Error>>).unwrap();
let interpreter = Interpreter::try_out_of_range();
assert!(interpreter
.execute(&res.prog(), &vec![FieldPrime::from(2)])
.is_err());
}

9
zokrates_core/tests/wasm.rs
View file

@ -5,7 +5,7 @@ extern crate zokrates_core;
extern crate zokrates_field;
use wasm_bindgen_test::*;
use zokrates_core::flat_absy::FlatVariable;
use zokrates_core::ir::{Function, Prog, Statement};
use zokrates_core::ir::{Function, Interpreter, Prog, Statement};
use zokrates_core::proof_system::ProofSystem;
use zokrates_field::field::FieldPrime;
@ -26,9 +26,10 @@ fn generate_proof() {
private: vec![false],
};
let witness = program
.clone()
.execute(&vec![FieldPrime::from(42)])
let interpreter = Interpreter::default();
let witness = interpreter
.execute(&program, &vec![FieldPrime::from(42)])
.unwrap();
let keys = G16::new().setup(program.clone());

6
zokrates_field/src/field.rs
View file

@ -106,6 +106,8 @@ pub trait Field:
let field_bits_be = &field_bits_be[field_bits_be.len() - Self::get_required_bits()..];
field_bits_be.to_vec()
}
/// Returns the value as a BigUint
fn to_biguint(&self) -> BigUint;
}
#[derive(PartialEq, PartialOrd, Clone, Eq, Ord, Hash, Serialize, Deserialize)]
@ -116,6 +118,10 @@ pub struct FieldPrime {
impl Field for FieldPrime {
type BellmanEngine = Bn256;
fn to_biguint(&self) -> BigUint {
self.value.to_biguint().unwrap()
}
fn into_byte_vector(&self) -> Vec<u8> {
match self.value.to_biguint() {
Option::Some(val) => val.to_bytes_le(),

5
zokrates_test/src/lib.rs
View file

@ -81,9 +81,12 @@ pub fn test_inner(test_path: &str) {
let bin = artifacts.prog();
let interpreter = zokrates_core::ir::Interpreter::default();
for test in t.tests.into_iter() {
let input = &test.input.values;
let output = bin.execute(
let output = interpreter.execute(
bin,
&input
.iter()
.map(|v| FieldPrime::try_from_dec_str(&v.clone()).unwrap())