diff --git a/examples/ZoKrates/pf/mm4_cond.zok b/examples/ZoKrates/pf/mm4_cond.zok new file mode 100644 index 00000000..992e0276 --- /dev/null +++ b/examples/ZoKrates/pf/mm4_cond.zok @@ -0,0 +1,18 @@ +def matmult(field[16] a, field[16] b) -> field[16]: + field[16] c = [0,0,0,0, 0,0,0,0, 0,0,0,0, 0,0,0,0] + + for field i in 0..4 do + for field j in 0..4 do + field s = 0 + for field k in 0..4 do + s = s + a[i*4 + k] * b[k*4 + j] + endfor + c[i*4 +j] = s + endfor + endfor + return c + +def main(public field[16] a, public field[16] b, public field[2] ab, public field init, public field final, private field doc) -> bool: + field[16] s = [1,0,0,0, 0,1,0,0, 0,0,1,0, 0,0,0,1] + s = if (doc == 0) then matmult(s, a) else matmult(s, b) fi + return if s[init*4 + final] == 1 then true else false fi diff --git a/scripts/zokrates_test.zsh b/scripts/zokrates_test.zsh index af34d990..0ae8c8ec 100755 --- a/scripts/zokrates_test.zsh +++ b/scripts/zokrates_test.zsh @@ -25,6 +25,14 @@ function r1cs_test { measure_time $BIN $zpath r1cs --action count } +function r1cs_test_count { + zpath=$1 + threshold=$2 + o=$($BIN $zpath r1cs --action count) + n_constraints=$(echo $o | grep 'Final R1cs size:' | grep -Eo '\b[0-9]+\b') + [[ $n_constraints -lt $threshold ]] || (echo "Got $n_constraints, expected < $threshold" && exit 1) +} + # Test prove workflow, given an example name function pf_test { ex_name=$1 @@ -43,6 +51,7 @@ function pf_test_isolate { rm -rf P V pi } +r1cs_test_count ./examples/ZoKrates/pf/mm4_cond.zok 120 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 diff --git a/src/front/zsharp/mod.rs b/src/front/zsharp/mod.rs index 6ab5a37c..afc98137 100644 --- a/src/front/zsharp/mod.rs +++ b/src/front/zsharp/mod.rs @@ -1825,11 +1825,15 @@ impl<'ast> ZGen<'ast> { /*** circify wrapper functions (hides RefCell) ***/ fn circ_enter_condition(&self, cond: Term) { - self.circ.borrow_mut().enter_condition(cond).unwrap(); + if self.isolate_asserts { + self.circ.borrow_mut().enter_condition(cond).unwrap(); + } } fn circ_exit_condition(&self) { - self.circ.borrow_mut().exit_condition() + if self.isolate_asserts { + self.circ.borrow_mut().exit_condition() + } } fn circ_condition(&self) -> Term { diff --git a/src/ir/opt/cfold.rs b/src/ir/opt/cfold.rs index bf291012..63163c93 100644 --- a/src/ir/opt/cfold.rs +++ b/src/ir/opt/cfold.rs @@ -195,20 +195,26 @@ pub fn fold_cache(node: &Term, cache: &mut TermCache, ignore: &[Op]) -> T let c = get(0); let t = get(1); let f = get(2); - match c.as_bool_opt() { - Some(true) => Some(t), - Some(false) => Some(f), - None => match t.as_bool_opt() { - Some(true) => Some(fold_cache(&term![OR; c, f], cache, ignore)), - Some(false) => Some(fold_cache(&term![AND; neg_bool(c), f], cache, ignore)), - _ => match f.as_bool_opt() { - Some(true) => { - Some(fold_cache(&term![OR; neg_bool(c), t], cache, ignore)) + if t == f { + Some(t) + } else { + match c.as_bool_opt() { + Some(true) => Some(t), + Some(false) => Some(f), + None => match t.as_bool_opt() { + Some(true) => Some(fold_cache(&term![OR; c, f], cache, ignore)), + Some(false) => { + Some(fold_cache(&term![AND; neg_bool(c), f], cache, ignore)) } - Some(false) => Some(fold_cache(&term![AND; c, t], cache, ignore)), - _ => None, + _ => match f.as_bool_opt() { + Some(true) => { + Some(fold_cache(&term![OR; neg_bool(c), t], cache, ignore)) + } + Some(false) => Some(fold_cache(&term![AND; c, t], cache, ignore)), + _ => None, + }, }, - }, + } } } Op::PfNaryOp(o) => Some(o.clone().flatten(t.cs.iter().map(|c| c_get(c)))), diff --git a/src/ir/opt/mem/lin.rs b/src/ir/opt/mem/lin.rs index b997dd82..7ec2144d 100644 --- a/src/ir/opt/mem/lin.rs +++ b/src/ir/opt/mem/lin.rs @@ -43,11 +43,16 @@ impl RewritePass for Linearizer { let tup = &cs[0]; if let Sort::Array(key_sort, _, size) = check(&orig.cs[0]) { assert!(size > 0); - let mut fields = (0..size).map(|idx| term![Op::Field(idx); tup.clone()]); - let first = fields.next().unwrap(); - Some(key_sort.elems_iter().take(size).skip(1).zip(fields).fold(first, |acc, (idx_c, field)| { - term![Op::Ite; term![Op::Eq; idx.clone(), idx_c], field, acc] - })) + if idx.is_const() { + let idx_usize = extras::as_uint_constant(idx).unwrap().to_usize().unwrap(); + Some(term![Op::Field(idx_usize); tup.clone()]) + } else { + let mut fields = (0..size).map(|idx| term![Op::Field(idx); tup.clone()]); + let first = fields.next().unwrap(); + Some(key_sort.elems_iter().take(size).skip(1).zip(fields).fold(first, |acc, (idx_c, field)| { + term![Op::Ite; term![Op::Eq; idx.clone(), idx_c], field, acc] + })) + } } else { unreachable!() } @@ -59,12 +64,17 @@ impl RewritePass for Linearizer { let val = &cs[2]; if let Sort::Array(key_sort, _, size) = check(&orig.cs[0]) { assert!(size > 0); - let mut updates = - (0..size).map(|idx| term![Op::Update(idx); tup.clone(), val.clone()]); - let first = updates.next().unwrap(); - Some(key_sort.elems_iter().take(size).skip(1).zip(updates).fold(first, |acc, (idx_c, update)| { + if idx.is_const() { + let idx_usize = extras::as_uint_constant(idx).unwrap().to_usize().unwrap(); + Some(term![Op::Update(idx_usize); tup.clone(), val.clone()]) + } else { + let mut updates = + (0..size).map(|idx| term![Op::Update(idx); tup.clone(), val.clone()]); + let first = updates.next().unwrap(); + Some(key_sort.elems_iter().take(size).skip(1).zip(updates).fold(first, |acc, (idx_c, update)| { term![Op::Ite; term![Op::Eq; idx.clone(), idx_c], update, acc] })) + } } else { unreachable!() } @@ -84,7 +94,6 @@ pub fn linearize(c: &mut Computation) { #[cfg(test)] mod test { use super::*; - use crate::util::field::DFL_T; fn array_free(t: &Term) -> bool { for c in PostOrderIter::new(t.clone()) { @@ -101,53 +110,91 @@ mod test { .count() } - fn field_lit(u: usize) -> Term { - leaf_term(Op::Const(Value::Field(DFL_T.new_v(u)))) - } - #[test] fn select_ite_stores() { - let z = term![Op::Const(Value::Array(Array::new( - Sort::BitVector(4), - Box::new(Sort::BitVector(4).default_value()), - Default::default(), - 6 - )))]; - let t = term![Op::Select; - term![Op::Ite; - leaf_term(Op::Const(Value::Bool(true))), - term![Op::Store; z.clone(), bv_lit(3, 4), bv_lit(1, 4)], - term![Op::Store; z, bv_lit(2, 4), bv_lit(1, 4)] - ], - bv_lit(3, 4) - ]; - let mut c = Computation::default(); - c.outputs.push(t); + let mut c = text::parse_computation( + b" + (computation + (metadata () ((a (bv 4)) (b (bv 4)) (c (bv 4))) ()) + (let + ( + (c_array (#a (bv 4) #x0 4 ())) + (store_1 (store c_array a #x1)) + (store_2 (store c_array b #x2)) + ) + (select (ite true store_1 store_2) c) + ) + ) + ", + ); linearize(&mut c); assert!(array_free(&c.outputs[0])); - assert_eq!(5 + 5 + 1 + 5, count_ites(&c.outputs[0])); + assert_eq!(3 + 3 + 1 + 3, count_ites(&c.outputs[0])); } #[test] fn select_ite_stores_field() { - let z = term![Op::Const(Value::Array(Array::new( - Sort::Field(DFL_T.clone()), - Box::new(Sort::BitVector(4).default_value()), - Default::default(), - 6 - )))]; - let t = term![Op::Select; - term![Op::Ite; - leaf_term(Op::Const(Value::Bool(true))), - term![Op::Store; z.clone(), field_lit(3), bv_lit(1, 4)], - term![Op::Store; z, field_lit(2), bv_lit(1, 4)] - ], - field_lit(3) - ]; - let mut c = Computation::default(); - c.outputs.push(t); + let mut c = text::parse_computation( + b" + (computation + (metadata () ((a (mod 5)) (b (mod 5)) (c (mod 5))) ()) + (let + ( + (c_array (#a (mod 5) #f1m5 4 ())) + (store_1 (store c_array a #f1m5)) + (store_2 (store c_array b #f2m5)) + ) + (select (ite true store_1 store_2) c) + ) + ) + ", + ); linearize(&mut c); assert!(array_free(&c.outputs[0])); - assert_eq!(5 + 5 + 1 + 5, count_ites(&c.outputs[0])); + assert_eq!(3 + 3 + 1 + 3, count_ites(&c.outputs[0])); + } + + #[test] + fn select_ite_stores_const() { + let mut c = text::parse_computation( + b" + (computation + (metadata () ((a (bv 4)) (b (bv 4)) (c (bv 4))) ()) + (let + ( + (c_array (#a (bv 4) #x0 4 ())) + (store_1 (store c_array #x0 #x1)) + (store_2 (store c_array b #x2)) + ) + (select (ite true store_1 store_2) c) + ) + ) + ", + ); + linearize(&mut c); + assert!(array_free(&c.outputs[0])); + assert_eq!(3 + 1 + 3, count_ites(&c.outputs[0])); + } + + #[test] + fn select_ite_stores_field_const() { + let mut c = text::parse_computation( + b" + (computation + (metadata () ((a (mod 5)) (b (mod 5)) (c (mod 5))) ()) + (let + ( + (c_array (#a (mod 5) #f1m5 4 ())) + (store_1 (store c_array #f1m5 #f1m5)) + (store_2 (store c_array b #f2m5)) + ) + (select (ite true store_1 store_2) c) + ) + ) + ", + ); + linearize(&mut c); + assert!(array_free(&c.outputs[0])); + assert_eq!(3 + 1 + 3, count_ites(&c.outputs[0])); } }