ZoKrates assertion bugfix and option to isolate (#89)

examples/ZoKrates/pf/assert.zok

@@ -0,0 +1,3 @@
+def main(private field A, private field B) -> field:
+    assert(A != B)
+    return A * B

examples/ZoKrates/pf/assert.zok.pin

@@ -0,0 +1,10 @@
+(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
+(let (
+    (A #f4)
+    (B #f5)
+) true ;ignored
+)
+)
+
+
+

examples/ZoKrates/pf/assert.zok.vin

@@ -0,0 +1,9 @@
+(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
+(let (
+    (return #f20)
+) true ;ignored
+)
+)
+
+
+

examples/ZoKrates/pf/isolate_assert.zok

@@ -0,0 +1,7 @@
+def mult(field x, field y) -> field:
+    assert(x != y)
+    return x * y
+
+def main(private field x, private field y) -> field:
+    return if x == y then x * x else mult(x, y) fi
+

examples/ZoKrates/pf/isolate_assert.zok.pin

@@ -0,0 +1,10 @@
+(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
+(let (
+    (x #f4)
+    (y #f4)
+) true ;ignored
+)
+)
+
+
+

examples/ZoKrates/pf/isolate_assert.zok.vin

@@ -0,0 +1,9 @@
+(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
+(let (
+    (return #f16)
+) true ;ignored
+)
+)
+
+
+

examples/circ.rs

@@ -80,6 +80,14 @@ struct FrontendOptions {
     /// Lint recursions that are allegedly primitive recursive (datalog)
     #[structopt(long)]
     lint_prim_rec: bool,
+
+    /// In Z#, "isolate" assertions. That is, assertions in if/then/else expressions only take
+    /// effect if that branch is active.
+    ///
+    /// See `--branch-isolation` in
+    /// [ZoKrates](https://zokrates.github.io/language/control_flow.html).
+    #[structopt(long)]
+    z_isolate_asserts: bool,
 }
 
 #[derive(Debug, StructOpt)]
@@ -182,6 +190,7 @@ fn main() {
             let inputs = zsharp::Inputs {
                 file: options.path,
                 mode,
+                isolate_asserts: options.frontend.z_isolate_asserts,
             };
             ZSharpFE::gen(inputs)
         }

examples/zxc.rs

@@ -92,6 +92,7 @@ fn main() {
         let inputs = zsharp::Inputs {
             file: options.path,
             mode: Mode::Proof,
+            isolate_asserts: false,
         };
         ZSharpFE::gen(inputs)
     };

examples/zxi.rs

@@ -38,6 +38,7 @@ fn main() {
     let inputs = Inputs {
         file: options.zsharp_path,
         mode,
+        isolate_asserts: false,
     };
     let cs = ZSharpFE::interpret(inputs);
     cs.pretty(&mut std::io::stdout().lock())

scripts/zokrates_test.zsh

@@ -34,6 +34,15 @@ function pf_test {
     rm -rf P V pi
 }
 
+# Test prove workflow with --z-isolate-asserts, given an example name
+function pf_test_isolate {
+    ex_name=$1
+    $BIN --z-isolate-asserts examples/ZoKrates/pf/$ex_name.zok r1cs --action setup
+    $ZK_BIN --inputs examples/ZoKrates/pf/$ex_name.zok.pin --action prove
+    $ZK_BIN --inputs examples/ZoKrates/pf/$ex_name.zok.vin --action verify
+    rm -rf P V pi
+}
+
 r1cs_test ./third_party/ZoKrates/zokrates_stdlib/stdlib/ecc/edwardsAdd.zok
 r1cs_test ./third_party/ZoKrates/zokrates_stdlib/stdlib/ecc/edwardsOnCurve.zok
 r1cs_test ./third_party/ZoKrates/zokrates_stdlib/stdlib/ecc/edwardsOrderCheck.zok
@@ -48,6 +57,8 @@ r1cs_test ./third_party/ZoKrates/zokrates_stdlib/stdlib/ecc/edwardsScalarMult.zo
 r1cs_test ./third_party/ZoKrates/zokrates_stdlib/stdlib/hashes/mimc7/mimc7R20.zok
 r1cs_test ./third_party/ZoKrates/zokrates_stdlib/stdlib/hashes/pedersen/512bit.zok
 
+pf_test assert
+pf_test_isolate isolate_assert
 pf_test 3_plus
 pf_test xor
 pf_test mul

src/front/zsharp/mod.rs

@@ -32,6 +32,10 @@ pub struct Inputs {
     pub file: PathBuf,
     /// The mode to generate for (MPC or proof). Effects visibility.
     pub mode: Mode,
+    /// Whether to isolate assertions.
+    ///
+    /// That is, whether assertions in in-active if/then/else branches are disabled.
+    pub isolate_asserts: bool,
 }
 
 /// The Z# front-end. Implements [FrontEnd].
@@ -46,7 +50,7 @@ impl FrontEnd for ZSharpFE {
         );
         let loader = parser::ZLoad::new();
         let asts = loader.load(&i.file);
-        let mut g = ZGen::new(asts, i.mode, loader.stdlib());
+        let mut g = ZGen::new(asts, i.mode, loader.stdlib(), i.isolate_asserts);
         g.visit_files();
         g.file_stack_push(i.file);
         g.generics_stack_push(HashMap::new());
@@ -65,7 +69,7 @@ impl ZSharpFE {
     pub fn interpret(i: Inputs) -> T {
         let loader = parser::ZLoad::new();
         let asts = loader.load(&i.file);
-        let mut g = ZGen::new(asts, i.mode, loader.stdlib());
+        let mut g = ZGen::new(asts, i.mode, loader.stdlib(), i.isolate_asserts);
         g.visit_files();
         g.file_stack_push(i.file);
         g.generics_stack_push(HashMap::new());
@@ -93,6 +97,8 @@ struct ZGen<'ast> {
     lhs_ty: RefCell<Option<Ty>>,
     ret_ty_stack: RefCell<Vec<Ty>>,
     gc_depth_estimate: Cell<usize>,
+    assertions: RefCell<Vec<Term>>,
+    isolate_asserts: bool,
 }
 
 impl<'ast> Drop for ZGen<'ast> {
@@ -138,6 +144,7 @@ impl<'ast> ZGen<'ast> {
         asts: HashMap<PathBuf, ast::File<'ast>>,
         mode: Mode,
         stdlib: &'ast parser::ZStdLib,
+        isolate_asserts: bool,
     ) -> Self {
         let this = Self {
             circ: RefCell::new(Circify::new(ZSharp::new())),
@@ -155,6 +162,8 @@ impl<'ast> ZGen<'ast> {
             lhs_ty: Default::default(),
             ret_ty_stack: Default::default(),
             gc_depth_estimate: Cell::new(2 * GC_INC),
+            assertions: Default::default(),
+            isolate_asserts,
         };
         this.circ
             .borrow()
@@ -697,9 +706,15 @@ impl<'ast> ZGen<'ast> {
                     let ret_var_val = self
                         .circ_declare_input(name, ty, PUBLIC_VIS, Some(ret_val.clone()), false)
                         .expect("circ_declare return");
-                    self.circ
-                        .borrow_mut()
-                        .assert(eq(ret_val, ret_var_val).unwrap().term);
+                    let ret_eq = eq(ret_val, ret_var_val).unwrap().term;
+                    let mut assertions = std::mem::take(&mut *self.assertions.borrow_mut());
+                    let to_assert = if assertions.is_empty() {
+                        ret_eq
+                    } else {
+                        assertions.push(ret_eq);
+                        term(AND, assertions)
+                    };
+                    self.circ.borrow_mut().assert(to_assert);
                 }
                 Mode::Opt => {
                     let ret_term = r.unwrap_term();
@@ -924,8 +939,13 @@ impl<'ast> ZGen<'ast> {
                     None if IS_CNST => Err("ternary condition not const bool".to_string()),
                     _ => {
                         let c = self.expr_impl_::<false>(&u.first)?;
+                        let cbool = bool(c.clone())?;
+                        self.circ_enter_condition(cbool.clone());
                         let a = self.expr_impl_::<false>(&u.second)?;
+                        self.circ_exit_condition();
+                        self.circ_enter_condition(term![NOT; cbool]);
                         let b = self.expr_impl_::<false>(&u.third)?;
+                        self.circ_exit_condition();
                         cond(c, a, b)
                     }
                 }
@@ -1107,7 +1127,7 @@ impl<'ast> ZGen<'ast> {
                     )),
                     _ => {
                         let b = bool(self.expr_impl_::<false>(&e.expression)?)?;
-                        self.circ_assert(b);
+                        self.assert(b);
                         Ok(())
                     }
                 }
@@ -1787,10 +1807,30 @@ impl<'ast> ZGen<'ast> {
             .map(|m| (m.as_ref(), s_path))
     }
 
+    fn assert(&self, asrt: Term) {
+        debug_assert!(matches!(check(&asrt), Sort::Bool));
+        if self.isolate_asserts {
+            let path = self.circ_condition();
+            self.assertions
+                .borrow_mut()
+                .push(term![IMPLIES; path, asrt]);
+        } else {
+            self.assertions.borrow_mut().push(asrt);
+        }
+    }
+
     /*** circify wrapper functions (hides RefCell) ***/
 
-    fn circ_assert(&self, asrt: Term) {
-        self.circ.borrow_mut().assert(asrt)
+    fn circ_enter_condition(&self, cond: Term) {
+        self.circ.borrow_mut().enter_condition(cond).unwrap();
+    }
+
+    fn circ_exit_condition(&self) {
+        self.circ.borrow_mut().exit_condition()
+    }
+
+    fn circ_condition(&self) -> Term {
+        self.circ.borrow().condition()
     }
 
     fn circ_return_(&self, ret: Option<T>) -> Result<(), CircError> {