diff --git a/examples/ZoKrates/pf/chall/poly_mult.zok b/examples/ZoKrates/pf/chall/poly_mult.zok new file mode 100644 index 00000000..db9b5aab --- /dev/null +++ b/examples/ZoKrates/pf/chall/poly_mult.zok @@ -0,0 +1,21 @@ +from "EMBED" import sample_challenge + +def main(private field[4] f, private field[4] g, private field[7] h) -> field: + field x = sample_challenge([...f, ...g, ...h]) + field[7] xpows = [1; 7] + for field i in 0..6 do + xpows[i+1] = xpows[i] * x + endfor + field fx = 0 + field gx = 0 + field hx = 0 + for field i in 0..4 do + fx = fx + xpows[i] * f[i] + gx = gx + xpows[i] * g[i] + endfor + for field i in 0..7 do + hx = hx + xpows[i] * h[i] + endfor + assert(fx * gx == hx) + return f[0] + diff --git a/examples/ZoKrates/pf/chall/poly_mult.zok.pin b/examples/ZoKrates/pf/chall/poly_mult.zok.pin new file mode 100644 index 00000000..bd07e8e2 --- /dev/null +++ b/examples/ZoKrates/pf/chall/poly_mult.zok.pin @@ -0,0 +1,20 @@ +(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513 +(let ( + (f.0 #f1) + (f.1 #f1) + (f.2 #f1) + (f.3 #f1) + (g.0 #f1) + (g.1 #f1) + (g.2 #f1) + (g.3 #f1) + (h.0 #f1) + (h.1 #f2) + (h.2 #f3) + (h.3 #f4) + (h.4 #f3) + (h.5 #f2) + (h.6 #f1) +) false ; ignored +)) + diff --git a/examples/ZoKrates/pf/chall/poly_mult.zok.vin b/examples/ZoKrates/pf/chall/poly_mult.zok.vin new file mode 100644 index 00000000..b7322ee6 --- /dev/null +++ b/examples/ZoKrates/pf/chall/poly_mult.zok.vin @@ -0,0 +1,5 @@ +(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513 +(let ( + (return #f1) +) false ; ignored +)) diff --git a/examples/ZoKrates/pf/chall/simple.zok b/examples/ZoKrates/pf/chall/simple.zok new file mode 100644 index 00000000..9e683bd1 --- /dev/null +++ b/examples/ZoKrates/pf/chall/simple.zok @@ -0,0 +1,7 @@ +from "EMBED" import sample_challenge + +def main(private field x, private field y) -> field: + field a = sample_challenge([x, y]) + assert(a * x == a * y) + return x + diff --git a/examples/ZoKrates/pf/chall/simple.zok.pin b/examples/ZoKrates/pf/chall/simple.zok.pin new file mode 100644 index 00000000..10483ef6 --- /dev/null +++ b/examples/ZoKrates/pf/chall/simple.zok.pin @@ -0,0 +1,6 @@ +(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513 +(let ( + (x #f7) + (y #f7) +) false ; ignored +)) diff --git a/examples/ZoKrates/pf/chall/simple.zok.vin b/examples/ZoKrates/pf/chall/simple.zok.vin new file mode 100644 index 00000000..9998618a --- /dev/null +++ b/examples/ZoKrates/pf/chall/simple.zok.vin @@ -0,0 +1,6 @@ +(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513 +(let ( + (return #f7) +) false ; ignored +)) + diff --git a/scripts/ram_test.zsh b/scripts/ram_test.zsh index 306f0f4e..1b4a8ce9 100755 --- a/scripts/ram_test.zsh +++ b/scripts/ram_test.zsh @@ -8,7 +8,7 @@ disable -r time # cargo build --features "zok smt bellman" --example circ --example zk MODE=release -# MODE=debug +MODE=debug BIN=./target/$MODE/examples/circ ZK_BIN=./target/$MODE/examples/zk @@ -71,3 +71,6 @@ ram_test ./examples/ZoKrates/pf/mem/volatile_struct.zok mirage "" ram_test ./examples/ZoKrates/pf/mem/arr_of_str.zok mirage "" ram_test ./examples/ZoKrates/pf/mem/arr_of_str_of_arr.zok mirage "" +# challenges +ram_test ./examples/ZoKrates/pf/chall/simple.zok mirage "" +ram_test ./examples/ZoKrates/pf/chall/poly_mult.zok mirage "" diff --git a/src/front/zsharp/mod.rs b/src/front/zsharp/mod.rs index 98513a2b..6800ec28 100644 --- a/src/front/zsharp/mod.rs +++ b/src/front/zsharp/mod.rs @@ -97,6 +97,7 @@ struct ZGen<'ast> { ret_ty_stack: RefCell>, gc_depth_estimate: Cell, assertions: RefCell>, + challenge_count: Cell, isolate_asserts: bool, } @@ -172,6 +173,7 @@ impl<'ast> ZGen<'ast> { ret_ty_stack: Default::default(), gc_depth_estimate: Cell::new(2 * GC_INC), assertions: Default::default(), + challenge_count: Cell::new(0), isolate_asserts, }; this.circ @@ -200,7 +202,12 @@ impl<'ast> ZGen<'ast> { r.unwrap_or_else(|e| self.err(e, s)) } - fn builtin_call(f_name: &str, mut args: Vec, mut generics: Vec) -> Result { + fn builtin_call( + &self, + f_name: &str, + mut args: Vec, + mut generics: Vec, + ) -> Result { debug!("Builtin Call: {}", f_name); match f_name { "u8_to_bits" | "u16_to_bits" | "u32_to_bits" | "u64_to_bits" => { @@ -339,6 +346,24 @@ impl<'ast> ZGen<'ast> { Ok(uint_lit(cfg().field().modulus().significant_bits(), 32)) } } + "sample_challenge" => { + if args.len() != 1 { + Err(format!( + "Got {} args to EMBED/sample_challenge, expected 1", + args.len() + )) + } else if generics.len() != 1 { + Err(format!( + "Got {} generic args to EMBED/sample_challenge, expected 1", + generics.len() + )) + } else { + let n = self.challenge_count.get(); + let t = sample_challenge(args.pop().unwrap(), n)?; + self.challenge_count.set(n + 1); + Ok(t) + } + } _ => Err(format!("Unknown or unimplemented builtin '{f_name}'")), } } @@ -544,7 +569,7 @@ impl<'ast> ZGen<'ast> { }) }) .collect::, _>>()?; - Self::builtin_call(&f_name, args, generics) + self.builtin_call(&f_name, args, generics) } else { // XXX(unimpl) multi-return unimplemented assert!(f.returns.len() <= 1); diff --git a/src/front/zsharp/term.rs b/src/front/zsharp/term.rs index 0f37f593..59572ab4 100644 --- a/src/front/zsharp/term.rs +++ b/src/front/zsharp/term.rs @@ -909,6 +909,24 @@ pub fn bit_array_le(a: T, b: T, n: usize) -> Result { )) } +pub fn sample_challenge(a: T, number: usize) -> Result { + if let Ty::Array(_, ta) = &a.ty { + if let Ty::Field = &**ta { + Ok(T::new( + Ty::Field, + term( + Op::PfChallenge(format!("zx_chall_{number}"), default_field()), + a.unwrap_array_ir()?, + ), + )) + } else { + Err(format!("sample_challenge called on non-field array {a}")) + } + } else { + Err(format!("sample_challenge called on non-array {a}")) + } +} + pub struct ZSharp {} fn field_name(struct_name: &str, field_name: &str) -> String { diff --git a/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok b/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok index 84c5dc07..e6d6b130 100644 --- a/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok +++ b/third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok @@ -75,3 +75,8 @@ def u16_to_u32(u16 i) -> u32: def u8_to_u16(u8 i) -> u16: return 0u16 + +// the output is sampled uniformly and independently of the inputs +def sample_challenge(field[N] x) -> field: + return 0 +