Merge pull request #609 from Zokrates/patch-unconstrained-lt

Patch unconstrained lt

zokrates_cli/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "zokrates_cli"
-version = "0.5.2"
+version = "0.5.3"
 authors = ["Jacob Eberhardt <jacob.eberhardt@tu-berlin.de>", "Dennis Kuhnert <mail@kyroy.com>", "Thibaut Schaeffer <thibaut@schaeff.fr>"]
 repository = "https://github.com/JacobEberhardt/ZoKrates.git"
 edition = "2018"

zokrates_cli/src/bin.rs

@@ -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();
         }
     }

zokrates_core/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "zokrates_core"
-version = "0.4.2"
+version = "0.4.3"
 authors = ["Jacob Eberhardt <jacob.eberhardt@tu-berlin.de>", "Dennis Kuhnert <mail@kyroy.com>"]
 repository = "https://github.com/JacobEberhardt/ZoKrates"
 readme = "README.md"
@@ -25,14 +25,14 @@ serde_json = "1.0"
 serde_bytes = "0.10"
 bincode = "0.8.0"
 regex = "0.2"
-pairing_ce = "0.18"
-ff_ce = "0.7"
+pairing_ce = "^0.21"
+ff_ce = "^0.9"
 zokrates_field = { version = "0.3.0", path = "../zokrates_field" }
 zokrates_pest_ast = { version = "0.1.0", path = "../zokrates_pest_ast" }
 zokrates_embed = { path = "../zokrates_embed" }
 rand = "0.4"
 csv = "1"
-bellman_ce = { git = "https://github.com/matter-labs/bellman", rev = "9e35737", default-features = false }
+bellman_ce = { version = "^0.3", default-features = false }
 
 [dev-dependencies]
 glob = "0.2.11"

zokrates_core/src/embed.rs

@@ -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();
         }
     }
 }

zokrates_core/src/flatten/mod.rs

@@ -118,6 +118,108 @@ impl<'ast, T: Field> Flattener<'ast, T> {
         }
     }
 
+    // Let's assume b = [1, 1, 1, 0]
+    //
+    // 1. Init `sizeUnknown = true`
+    //    As long as `sizeUnknown` is `true` we don't yet know if a is <= than b.
+    // 2. Loop over `b`:
+    //     * b[0] = 1
+    //       when `b` is 1 we check wether `a` is 0 in that particular run and update
+    //       `sizeUnknown` accordingly:
+    //       `sizeUnknown = sizeUnknown && a[0]`
+    //     * b[1] = 1
+    //       `sizrUnknown = sizeUnknown && a[1]`
+    //     * b[2] = 1
+    //       `sizeUnknown = sizeUnknown && a[2]`
+    //     * b[3] = 0
+    //       we need to enforce that `a` is 0 in case `sizeUnknown`is still `true`,
+    //       otherwise `a` can be {0,1}:
+    //      `true == (!sizeUnknown || !a[3])`
+    //      ```
+    //                     **true => a -> 0
+    //         sizeUnkown *
+    //                     **false => a -> {0,1}
+    //      ```
+    fn strict_le_check(
+        &mut self,
+        statements_flattened: &mut Vec<FlatStatement<T>>,
+        b: &[bool],
+        a: Vec<FlatVariable>,
+    ) {
+        let len = b.len();
+        assert_eq!(a.len(), T::get_required_bits());
+        assert_eq!(a.len(), b.len());
+
+        let mut is_not_smaller_run = vec![];
+        let mut size_unknown = vec![];
+
+        for _ in 0..len {
+            is_not_smaller_run.push(self.use_sym());
+            size_unknown.push(self.use_sym());
+        }
+
+        // init size_unknown = true
+        statements_flattened.push(FlatStatement::Definition(
+            size_unknown[0],
+            FlatExpression::Number(T::from(1)),
+        ));
+
+        for (i, b) in b.iter().enumerate() {
+            if *b {
+                statements_flattened.push(FlatStatement::Definition(
+                    is_not_smaller_run[i],
+                    a[i].clone().into(),
+                ));
+
+                // don't need to update size_unknown in the last round
+                if i < len - 1 {
+                    statements_flattened.push(FlatStatement::Definition(
+                        size_unknown[i + 1],
+                        FlatExpression::Mult(
+                            box size_unknown[i].into(),
+                            box is_not_smaller_run[i].into(),
+                        ),
+                    ));
+                }
+            } else {
+                // don't need to update size_unknown in the last round
+                if i < len - 1 {
+                    statements_flattened.push(
+                        // sizeUnknown is not changing in this case
+                        // We sill have to assign the old value to the variable of the current run
+                        // This trivial definition will later be removed by the optimiser
+                        FlatStatement::Definition(
+                            size_unknown[i + 1].into(),
+                            size_unknown[i].into(),
+                        ),
+                    );
+                }
+
+                let or_left = FlatExpression::Sub(
+                    box FlatExpression::Number(T::from(1)),
+                    box size_unknown[i].clone().into(),
+                );
+                let or_right: FlatExpression<_> = FlatExpression::Sub(
+                    box FlatExpression::Number(T::from(1)),
+                    box a[i].clone().into(),
+                );
+
+                let and_name = self.use_sym();
+                let and = FlatExpression::Mult(box or_left.clone(), box or_right.clone());
+                statements_flattened.push(FlatStatement::Definition(and_name, and));
+                let or = FlatExpression::Sub(
+                    box FlatExpression::Add(box or_left, box or_right),
+                    box and_name.into(),
+                );
+
+                statements_flattened.push(FlatStatement::Condition(
+                    FlatExpression::Number(T::from(1)),
+                    or,
+                ));
+            }
+        }
+    }
+
     /// Flatten an if/else expression
     ///
     /// # Arguments
@@ -707,6 +809,13 @@ impl<'ast, T: Field> Flattener<'ast, T> {
                     ));
                 }
 
+                // check that the decomposition is in the field with a strict `< p` checks
+                self.strict_le_check(
+                    statements_flattened,
+                    &T::max_value_bit_vector_be(),
+                    sub_bits_be.clone(),
+                );
+
                 // sum(sym_b{i} * 2**i)
                 let mut expr = FlatExpression::Number(T::from(0));