1
0
Fork 0
mirror of synced 2025-09-23 12:18:44 +00:00
This commit is contained in:
schaeff 2020-07-13 09:20:27 +02:00
parent bc5923b359
commit 5c1a361619
14 changed files with 85 additions and 45 deletions

View file

@ -1,3 +1,2 @@
def main(private field a, field b) -> (field): def main(private field a, field b) -> (bool):
field result = if a * a == b then 1 else 0 fi return a * a == b
return result

View file

@ -1,4 +1,4 @@
def main() -> (field): def main() -> ():
field pMinusOne = 21888242871839275222246405745257275088548364400416034343698204186575808495616 field pMinusOne = 21888242871839275222246405745257275088548364400416034343698204186575808495616
0 - 1 == pMinusOne 0 - 1 == pMinusOne
return 1 return

View file

@ -1,7 +1,7 @@
import "hashes/sha256/512bitPacked" as sha256packed import "hashes/sha256/512bitPacked" as sha256packed
def main(private field a, private field b, private field c, private field d) -> (field): def main(private field a, private field b, private field c, private field d) -> ():
field[2] h = sha256packed([a, b, c, d]) field[2] h = sha256packed([a, b, c, d])
h[0] == 263561599766550617289250058199814760685 h[0] == 263561599766550617289250058199814760685
h[1] == 65303172752238645975888084098459749904 h[1] == 65303172752238645975888084098459749904
return 1 return

View file

@ -2,8 +2,8 @@ def incr(field a) -> (field):
a = a + 1 a = a + 1
return a return a
def main() -> (field): def main() -> ():
field x = 1 field x = 1
field res = incr(x) field res = incr(x)
x == 1 // x has not changed x == 1 // x has not changed
return 1 return

View file

@ -4,6 +4,6 @@ def foo() -> (field, field[3]):
def foo() -> (field, field): def foo() -> (field, field):
return 1, 2 return 1, 2
def main() -> (field): def main() -> ():
field a, field[3] b = foo() field a, field[3] b = foo()
return 1 return

View file

@ -1,5 +1,5 @@
// a and b are factorization of c // a and b are factorization of c
def main(field c, private field a, private field b) -> (field): def main(field c, private field a, private field b) -> ():
field d = a * b field d = a * b
c == d c == d
return 1 return

View file

@ -1,6 +1,6 @@
def foo() -> (field): def foo() -> (field):
return 1 return 1
def main() -> (field): def main() -> ():
foo() + (1 + 44*3) == 1 foo() + (1 + 44*3) == 1
return 1 return

View file

@ -6,7 +6,7 @@ import "hashes/utils/256bitsDirectionHelper" as multiplex
// Merke-Tree inclusion proof for tree depth 3 using SNARK efficient pedersen hashes // Merke-Tree inclusion proof for tree depth 3 using SNARK efficient pedersen hashes
// directionSelector=> 1/true if current digest is on the rhs of the hash // directionSelector=> 1/true if current digest is on the rhs of the hash
def main(bool[256] rootDigest, private bool[256] leafDigest, private bool[3] directionSelector, bool[256] PathDigest0, private bool[256] PathDigest1, private bool[256] PathDigest2) -> (field): def main(bool[256] rootDigest, private bool[256] leafDigest, private bool[3] directionSelector, bool[256] PathDigest0, private bool[256] PathDigest1, private bool[256] PathDigest2) -> (bool):
BabyJubJubParams context = context() BabyJubJubParams context = context()
//Setup //Setup
@ -22,7 +22,5 @@ def main(bool[256] rootDigest, private bool[256] leafDigest, private bool[3] dir
preimage = multiplex(directionSelector[2], currentDigest, PathDigest2) preimage = multiplex(directionSelector[2], currentDigest, PathDigest2)
currentDigest = hash(preimage) currentDigest = hash(preimage)
rootDigest == currentDigest return rootDigest == currentDigest
return 1 //return true in success

View file

@ -23,8 +23,4 @@ def main(field treeDepth, bool[256] rootDigest, private bool[256] leafDigest, pr
currentDigest = sha256(lhs, rhs) currentDigest = sha256(lhs, rhs)
counter = counter + 1 counter = counter + 1
//Asserts return counter == treeDepth && rootDigest == currentDigest
counter == treeDepth
rootDigest == currentDigest
return 1 //return true in success

View file

@ -2,6 +2,6 @@ def foo(field a) -> (field, field, field, field):
field b = 12*a field b = 12*a
return a, 2*a, 5*b, a*b return a, 2*a, 5*b, a*b
def main(field i) -> (field): def main(field i) -> ():
field x, field y, field z, field t = foo(i) field x, field y, field z, field t = foo(i)
return 1 return

View file

@ -1,4 +1,4 @@
def main() -> (field): def main() -> ():
field x = 2**4 field x = 2**4
x == 16 x == 16
x = x**2 x = x**2
@ -13,4 +13,4 @@ def main() -> (field):
a == 625 a == 625
a = 5**5 a = 5**5
a == 3125 a == 3125
return 1 return

View file

@ -0,0 +1,58 @@
// Sudoku of format
// | a11 | a12 || b11 | b12 |
// --------------------------
// | a21 | a22 || b21 | b22 |
// ==========================
// | c11 | c12 || d11 | d12 |
// --------------------------
// | c21 | c22 || d21 | d22 |
// We encode values in the following way:
// 1 -> 2
// 2 -> 3
// 3 -> 5
// 4 -> 7
// returns true if there are no duplicates
// assumption: `a, b, c, d` are all in `{ 2, 3, 5, 7 }`
def checkNoDuplicates(field a, field b, field c, field d) -> (bool):
// as `{ 2, 3, 5, 7 }` are primes, the set `{ a, b, c, d }` is equal to the set `{ 2, 3, 5, 7}` if and only if the products match
return a * b * c * d == 2 * 3 * 5 * 7
// returns `0` if and only if `x` in `{ 2, 3, 5, 7 }`
def validateInput(field x) -> (bool):
return (x-2) * (x-3) * (x-5) * (x-7) == 0
// variables naming: box'row''column'
def main(field a21, field b11, field b22, field c11, field c22, field d21, private field a11, private field a12, private field a22, private field b12, private field b21, private field c12, private field c21, private field d11, private field d12, private field d22) -> (bool):
field[4][4] a = [[a11, a12, b11, b12], [a21, a22, b21, b22], [c11, c12, d11, d12], [c21, c22, d21, d22]]
bool res = true
// go through the whole grid and check that all elements are valid
for field i in 0..4 do
for field j in 0..4 do
res = res && validateInput(a[i][j])
endfor
endfor
// go through the 4 2x2 boxes and check that they do not contain duplicates
for field i in 0..1 do
for field j in 0..1 do
res = res && checkNoDuplicates(a[2*i][2*i], a[2*i][2*i + 1], a[2*i + 1][2*i], a[2*i + 1][2*i + 1])
endfor
endfor
// go through the 4 rows and check that they do not contain duplicates
for field i in 0..4 do
res = res && checkNoDuplicates(a[i][0], a[i][1], a[i][2], a[i][3])
endfor
// go through the 4 columns and check that they do not contain duplicates
for field j in 0..4 do
res = res && checkNoDuplicates(a[0][j], a[1][j], a[2][j], a[3][j])
endfor
return res

View file

@ -2,24 +2,13 @@
// In this example, the crowd is a series of numbers, ideally* all prime but one, and Waldo is a non-prime number // In this example, the crowd is a series of numbers, ideally* all prime but one, and Waldo is a non-prime number
// * we don't enforce only one number being non-prime, so there could be multiple Waldos // * we don't enforce only one number being non-prime, so there could be multiple Waldos
def isWaldo(field a, field p, field q) -> (field): def isWaldo(field a, field p, field q) -> (bool):
// make sure that p and q are both non zero // make sure that neither `p` nor `q` is `1`
// we can't check inequalities, so let's create binary (!(p == 1) && !(q == 1)) == true
// variables
field p1 = if p == 1 then 0 else 1 fi // "p != 1"
field q1 = if q == 1 then 0 else 1 fi // "q != 1"
q1 * p1 == 1 // "p1 and q1"
// we know how to factor a // we know how to factor a
a == p * q return a == p * q
return 1 def main(field[3] a, private field index, private field p, private field q) -> (bool):
// define all
def main(field a0, field a1, field a2, field a3, private field index, private field p, private field q) -> (field):
// prover provides the index of Waldo // prover provides the index of Waldo
field waldo = if index == 0 then a0 else 0 fi return isWaldo(a[index], p, q)
waldo = waldo + if index == 1 then a1 else 0 fi
waldo = waldo + if index == 2 then a2 else 0 fi
waldo = waldo + if index == 3 then a3 else 0 fi
return isWaldo(waldo, p, q)