add sample_challenge builtin (#179)

This commit is contained in:
Alex Ozdemir
2023-11-15 09:59:29 -08:00
committed by GitHub
parent 7a805323d0
commit fca98ddc5a
10 changed files with 119 additions and 3 deletions

View File

@@ -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]

View File

@@ -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
))

View File

@@ -0,0 +1,5 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(return #f1)
) false ; ignored
))

View File

@@ -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

View File

@@ -0,0 +1,6 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(x #f7)
(y #f7)
) false ; ignored
))

View File

@@ -0,0 +1,6 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(return #f7)
) false ; ignored
))

View File

@@ -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 ""

View File

@@ -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,
}
@@ -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<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" => {
@@ -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::<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);

View File

@@ -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 {

View File

@@ -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