Skip to content

Commit

Permalink
add sample_challenge builtin (#179)
Browse files Browse the repository at this point in the history
  • Loading branch information
alex-ozdemir authored Nov 15, 2023
1 parent 7a80532 commit fca98dd
Show file tree
Hide file tree
Showing 10 changed files with 119 additions and 3 deletions.
21 changes: 21 additions & 0 deletions examples/ZoKrates/pf/chall/poly_mult.zok
Original file line number Diff line number Diff line change
@@ -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]

20 changes: 20 additions & 0 deletions examples/ZoKrates/pf/chall/poly_mult.zok.pin
Original file line number Diff line number Diff line change
@@ -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
))

5 changes: 5 additions & 0 deletions examples/ZoKrates/pf/chall/poly_mult.zok.vin
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(return #f1)
) false ; ignored
))
7 changes: 7 additions & 0 deletions examples/ZoKrates/pf/chall/simple.zok
Original file line number Diff line number Diff line change
@@ -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

6 changes: 6 additions & 0 deletions examples/ZoKrates/pf/chall/simple.zok.pin
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(x #f7)
(y #f7)
) false ; ignored
))
6 changes: 6 additions & 0 deletions examples/ZoKrates/pf/chall/simple.zok.vin
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(return #f7)
) false ; ignored
))

5 changes: 4 additions & 1 deletion scripts/ram_test.zsh
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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 ""
29 changes: 27 additions & 2 deletions src/front/zsharp/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,7 @@ struct ZGen<'ast> {
ret_ty_stack: RefCell<Vec<Ty>>,
gc_depth_estimate: Cell<usize>,
assertions: RefCell<Vec<Term>>,
challenge_count: Cell<usize>,
isolate_asserts: bool,
}

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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<T>, mut generics: Vec<T>) -> Result<T, String> {
fn builtin_call(
&self,
f_name: &str,
mut args: Vec<T>,
mut generics: Vec<T>,
) -> Result<T, String> {
debug!("Builtin Call: {}", f_name);
match f_name {
"u8_to_bits" | "u16_to_bits" | "u32_to_bits" | "u64_to_bits" => {
Expand Down Expand Up @@ -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}'")),
}
}
Expand Down Expand Up @@ -544,7 +569,7 @@ impl<'ast> ZGen<'ast> {
})
})
.collect::<Result<Vec<_>, _>>()?;
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);
Expand Down
18 changes: 18 additions & 0 deletions src/front/zsharp/term.rs
Original file line number Diff line number Diff line change
Expand Up @@ -909,6 +909,24 @@ pub fn bit_array_le(a: T, b: T, n: usize) -> Result<T, String> {
))
}

pub fn sample_challenge(a: T, number: usize) -> Result<T, String> {
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 {
Expand Down
5 changes: 5 additions & 0 deletions third_party/ZoKrates/zokrates_stdlib/stdlib/EMBED.zok
Original file line number Diff line number Diff line change
Expand Up @@ -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<N>(field[N] x) -> field:
return 0

0 comments on commit fca98dd

Please sign in to comment.