diff --git a/examples/ZoKrates/pf/assert2.zok b/examples/ZoKrates/pf/assert2.zok new file mode 100644 index 00000000..966c0916 --- /dev/null +++ b/examples/ZoKrates/pf/assert2.zok @@ -0,0 +1,3 @@ +def main(private field A, private field B) -> bool: + assert(A+B == 123) + return true diff --git a/examples/ZoKrates/pf/assert2.zok.pin b/examples/ZoKrates/pf/assert2.zok.pin new file mode 100644 index 00000000..cbb92e0a --- /dev/null +++ b/examples/ZoKrates/pf/assert2.zok.pin @@ -0,0 +1,10 @@ +(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513 + +(let ( + + (A #f4) + (B #f-4) + +) true ;ignored + +)) diff --git a/examples/ZoKrates/pf/assert2.zok.vin b/examples/ZoKrates/pf/assert2.zok.vin new file mode 100644 index 00000000..04e3a61d --- /dev/null +++ b/examples/ZoKrates/pf/assert2.zok.vin @@ -0,0 +1,9 @@ +(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513 + +(let ( + + (return true) + +) true; ignored + +)) diff --git a/scripts/zokrates_test.zsh b/scripts/zokrates_test.zsh index ebd3e1dc..b80a8517 100755 --- a/scripts/zokrates_test.zsh +++ b/scripts/zokrates_test.zsh @@ -90,6 +90,7 @@ pf_test_only_pf sha_temp2 #pf_test_only_pf test_sha256 pf_test assert +pf_test assert2 pf_test_isolate isolate_assert pf_test 3_plus pf_test xor diff --git a/src/target/r1cs/bellman.rs b/src/target/r1cs/bellman.rs index d8b8dbd6..e23e6c54 100644 --- a/src/target/r1cs/bellman.rs +++ b/src/target/r1cs/bellman.rs @@ -112,16 +112,17 @@ impl<'a, F: PrimeField> Circuit for SynthInput<'a> { "Bellman doesn't support rounds" ); let public = matches!(var.ty(), VarType::Inst); - let name_f = || format!("{var:?}"); + let name = self.0.r1cs.names.get(&var).unwrap(); + let name_f = || format!("{name:?}"); let val_f = || { Ok({ let i_val = &values.as_ref().expect("missing values")[i]; let ff_val = int_to_ff(i_val.as_pf().into()); - debug!("value : {var:?} -> {ff_val:?} ({i_val})"); + debug!("value : {name:?} -> {ff_val:?} ({i_val})"); ff_val }) }; - debug!("var: {:?}, public: {}", var, public); + debug!("var: {:?}, public: {}", name, public); let v = if public { cs.alloc_input(name_f, val_f)? } else { diff --git a/src/target/r1cs/opt.rs b/src/target/r1cs/opt.rs index f48daed6..f5e335d4 100644 --- a/src/target/r1cs/opt.rs +++ b/src/target/r1cs/opt.rs @@ -133,15 +133,39 @@ impl LinReducer { self.queue.push(use_id); } } - self.r1cs.idx_to_sig.remove_fwd(&var); - self.r1cs.terms.remove(&var); + self.remove_var(var); debug_assert_eq!(0, self.uses[&var].len()); } } } self.r1cs.constraints.retain(|c| !constantly_true(c)); + self.remove_dead_variables(); self.r1cs } + + fn remove_var(&mut self, var: Var) { + self.r1cs.idx_to_sig.remove_fwd(&var); + self.r1cs.terms.remove(&var); + } + + /// Remove any private dead variables. Run this at the end of optimization. + fn remove_dead_variables(&mut self) { + let used: HashSet = self + .r1cs + .constraints + .iter() + .flat_map(|c| { + c.0.monomials + .keys() + .chain(c.1.monomials.keys().chain(c.2.monomials.keys())) + }) + .copied() + .collect(); + let present: HashSet = self.r1cs.terms.keys().copied().collect(); + for to_remove in present.difference(&used) { + self.remove_var(*to_remove); + } + } } fn as_linear_sub((a, b, c): &(Lc, Lc, Lc), r1cs: &R1cs) -> Option<(Var, Lc)> {