github/circ
1
1
Fork 0
mirror of https://github.com/circify/circ.git synced 2026-01-08 21:28:04 -05:00
Code Issues Packages Projects Releases Wiki Activity

Add support for ZoKrates with curly brackets (wip) (#211)

Browse Source
This commit is contained in:
Stefanos Chaliasos
2025-02-12 19:07:15 +02:00
committed by GitHub
parent 38f585ecdf
commit 56c07d44e7
569 changed files with 25259 additions and 55 deletions
Download Patch File Download Diff File Expand all files Collapse all files

223
Cargo.lock generated
View File

@@ -337,7 +337,7 @@ dependencies = [
"group",
"ieee754",
"im",
"itertools",
"itertools 0.10.5",
"lang-c",
"lazy_static",
"log",
@@ -365,8 +365,10 @@ dependencies = [
"spartan",
"thiserror",
"typed-arena",
"zokrates_parser",
"zokrates_pest_ast",
"zokrates_parser 0.2.4",
"zokrates_parser 0.3.5",
"zokrates_pest_ast 0.2.3",
"zokrates_pest_ast 0.3.3",
]
[[package]]
@@ -437,8 +439,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0862016ff20d69b84ef8247369fabf5c008a7417002411897d40ee1f4532b873"
dependencies = [
"heck",
"proc-macro2",
"quote",
"proc-macro2 1.0.67",
"quote 1.0.33",
"syn 2.0.37",
]
@@ -590,8 +592,8 @@ version = "0.2.15"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "613e4ee15899913285b7612004bbd490abd605be7b11d35afada5902fb6b91d5"
dependencies = [
"proc-macro2",
"quote",
"proc-macro2 1.0.67",
"quote 1.0.33",
"syn 1.0.109",
]
@@ -679,6 +681,28 @@ dependencies = [
"version_check",
]
[[package]]
name = "failure"
version = "0.1.8"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d32e9bd16cc02eae7db7ef620b392808b89f6a5e16bb3497d159c6b92a0f4f86"
dependencies = [
"backtrace",
"failure_derive",
]
[[package]]
name = "failure_derive"
version = "0.1.8"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "aa4da3c766cd7a0db8242e326e9e4e081edd567072893ed320008189715366a4"
dependencies = [
"proc-macro2 1.0.67",
"quote 1.0.33",
"syn 1.0.109",
"synstructure",
]
[[package]]
name = "fastrand"
version = "2.0.0"
@@ -705,8 +729,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e715451ab983be06481e927a275ec12372103ad426c7cb82cebfe14698ed4cf4"
dependencies = [
"num-traits",
"proc-macro2",
"quote",
"proc-macro2 1.0.67",
"quote 1.0.33",
"syn 1.0.109",
]
@@ -721,8 +745,8 @@ dependencies = [
"num-bigint",
"num-integer",
"num-traits",
"proc-macro2",
"quote",
"proc-macro2 1.0.67",
"quote 1.0.33",
"syn 1.0.109",
]
@@ -761,11 +785,10 @@ checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1"
[[package]]
name = "from-pest"
version = "0.3.2"
version = "0.3.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d3380d8b4f459e3bb35904036044393332e71d5316be9061d9b545c44b6064db"
checksum = "aba9389cedcba1fb3a2aa2ed00f584f2606bce8e0106614a17327a24513bc60f"
dependencies = [
"log",
"pest",
"void",
]
@@ -942,6 +965,15 @@ dependencies = [
"windows-sys",
]
[[package]]
name = "itertools"
version = "0.7.11"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0d47946d458e94a1b7bcabbf6521ea7c037062c81f534615abcad76e84d4970d"
dependencies = [
"either",
]
[[package]]
name = "itertools"
version = "0.10.5"
@@ -1013,8 +1045,8 @@ checksum = "a1d849148dbaf9661a6151d1ca82b13bb4c4c128146a88d05253b38d4e2f496c"
dependencies = [
"beef",
"fnv",
"proc-macro2",
"quote",
"proc-macro2 1.0.67",
"quote 1.0.33",
"regex-syntax 0.6.29",
"syn 1.0.109",
]
@@ -1161,32 +1193,32 @@ checksum = "de3145af08024dea9fa9914f381a17b8fc6034dfb00f3a84013f7ff43f29ed4c"
[[package]]
name = "pest"
version = "2.7.3"
version = "2.4.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d7a4d085fd991ac8d5b05a147b437791b4260b76326baf0fc60cf7c9c27ecd33"
checksum = "a528564cc62c19a7acac4d81e01f39e53e25e17b934878f4c6d25cc2836e62f8"
dependencies = [
"memchr",
"thiserror",
"ucd-trie",
]
[[package]]
name = "pest-ast"
version = "0.3.4"
version = "0.3.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "40b5ac58ac48a503d1efdcf0ff044b442c07ac4645d179c62d4af79db89f9cda"
checksum = "3fbf404899169771dd6a32c84248b83cd67a26cc7cc957aac87661490e1227e4"
dependencies = [
"itertools",
"proc-macro2",
"quote",
"syn 2.0.37",
"itertools 0.7.11",
"proc-macro2 0.4.30",
"quote 0.6.13",
"single",
"syn 0.15.44",
]
[[package]]
name = "pest_derive"
version = "2.7.3"
version = "2.4.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a2bee7be22ce7918f641a33f08e3f43388c7656772244e2bbb2477f44cc9021a"
checksum = "d5fd9bc6500181952d34bd0b2b0163a54d794227b498be0b7afa7698d0a7b18f"
dependencies = [
"pest",
"pest_generator",
@@ -1194,26 +1226,26 @@ dependencies = [
[[package]]
name = "pest_generator"
version = "2.7.3"
version = "2.4.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d1511785c5e98d79a05e8a6bc34b4ac2168a0e3e92161862030ad84daa223141"
checksum = "d2610d5ac5156217b4ff8e46ddcef7cdf44b273da2ac5bca2ecbfa86a330e7c4"
dependencies = [
"pest",
"pest_meta",
"proc-macro2",
"quote",
"syn 2.0.37",
"proc-macro2 1.0.67",
"quote 1.0.33",
"syn 1.0.109",
]
[[package]]
name = "pest_meta"
version = "2.7.3"
version = "2.4.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b42f0394d3123e33353ca5e1e89092e533d2cc490389f2bd6131c43c634ebc5f"
checksum = "824749bf7e21dd66b36fbe26b3f45c713879cccd4a009a917ab8e045ca8246fe"
dependencies = [
"once_cell",
"pest",
"sha2",
"sha1",
]
[[package]]
@@ -1238,6 +1270,15 @@ version = "0.2.17"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5b40af805b3121feab8a3c29f04d8ad262fa8e0561883e7653e024ae4479e6de"
[[package]]
name = "proc-macro2"
version = "0.4.30"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "cf3d2011ab5c909338f7887f4fc896d35932e29146c12c8d01da6b22a80ba759"
dependencies = [
"unicode-xid 0.1.0",
]
[[package]]
name = "proc-macro2"
version = "1.0.67"
@@ -1264,18 +1305,27 @@ version = "1.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b22a693222d716a9587786f37ac3f6b4faedb5b80c23914e7303ff5a1d8016e9"
dependencies = [
"proc-macro2",
"quote",
"proc-macro2 1.0.67",
"quote 1.0.33",
"syn 1.0.109",
]
[[package]]
name = "quote"
version = "0.6.13"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6ce23b6b870e8f94f81fb0a363d65d86675884b34a09043c81e5562f11c1f8e1"
dependencies = [
"proc-macro2 0.4.30",
]
[[package]]
name = "quote"
version = "1.0.33"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5267fca4496028628a95160fc423a33e8b2e6af8a5302579e322e4b520293cae"
dependencies = [
"proc-macro2",
"proc-macro2 1.0.67",
]
[[package]]
@@ -1528,8 +1578,8 @@ version = "1.0.188"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4eca7ac642d82aa35b60049a6eccb4be6be75e599bd2e9adb5f875a737654af2"
dependencies = [
"proc-macro2",
"quote",
"proc-macro2 1.0.67",
"quote 1.0.33",
"syn 2.0.37",
]
@@ -1545,10 +1595,10 @@ dependencies = [
]
[[package]]
name = "sha2"
version = "0.10.7"
name = "sha1"
version = "0.10.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "479fb9d862239e610720565ca91403019f2f00410f1864c5aa7479b950a76ed8"
checksum = "e3bf829a2d51ab4a5ddf1352d8470c140cadc8301b2ae1789db023f01cedd6ba"
dependencies = [
"cfg-if",
"cpufeatures",
@@ -1568,6 +1618,15 @@ dependencies = [
"opaque-debug",
]
[[package]]
name = "single"
version = "1.0.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9db45bb685b486eec37e0271dcc0dac76eae5e893125f8a4f0511d0a1d29543b"
dependencies = [
"failure",
]
[[package]]
name = "sized-chunks"
version = "0.6.5"
@@ -1590,7 +1649,7 @@ dependencies = [
"curve25519-dalek",
"digest 0.8.1",
"flate2",
"itertools",
"itertools 0.10.5",
"merlin",
"rand 0.7.3",
"rand_core 0.5.1",
@@ -1613,14 +1672,25 @@ version = "2.5.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "81cdd64d312baedb58e21336b31bc043b77e01cc99033ce76ef539f78e965ebc"
[[package]]
name = "syn"
version = "0.15.44"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9ca4b3b69a77cbe1ffc9e198781b7acb0c7365a883670e8f1c1bc66fba79a5c5"
dependencies = [
"proc-macro2 0.4.30",
"quote 0.6.13",
"unicode-xid 0.1.0",
]
[[package]]
name = "syn"
version = "1.0.109"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
dependencies = [
"proc-macro2",
"quote",
"proc-macro2 1.0.67",
"quote 1.0.33",
"unicode-ident",
]
@@ -1630,11 +1700,23 @@ version = "2.0.37"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7303ef2c05cd654186cb250d29049a24840ca25d2747c25c0381c8d9e2f582e8"
dependencies = [
"proc-macro2",
"quote",
"proc-macro2 1.0.67",
"quote 1.0.33",
"unicode-ident",
]
[[package]]
name = "synstructure"
version = "0.12.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "f36bdaa60a83aca3921b5259d5400cbf5e90fc51931376a9bd4a0eb79aa7210f"
dependencies = [
"proc-macro2 1.0.67",
"quote 1.0.33",
"syn 1.0.109",
"unicode-xid 0.2.6",
]
[[package]]
name = "tap"
version = "1.0.1"
@@ -1678,8 +1760,8 @@ version = "1.0.48"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "49922ecae66cc8a249b77e68d1d0623c1b2c514f0060c27cdc68bd62a1219d35"
dependencies = [
"proc-macro2",
"quote",
"proc-macro2 1.0.67",
"quote 1.0.33",
"syn 2.0.37",
]
@@ -1707,6 +1789,18 @@ version = "1.0.12"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b"
[[package]]
name = "unicode-xid"
version = "0.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "fc72304796d0818e357ead4e000d19c9c174ab23dc11093ac919054d20a6a7fc"
[[package]]
name = "unicode-xid"
version = "0.2.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853"
[[package]]
name = "utf8parse"
version = "0.2.1"
@@ -1864,8 +1958,8 @@ version = "0.7.34"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "15e934569e47891f7d9411f1a451d947a60e000ab3bd24fbb970f000387d1b3b"
dependencies = [
"proc-macro2",
"quote",
"proc-macro2 1.0.67",
"quote 1.0.33",
"syn 2.0.37",
]
@@ -1884,8 +1978,8 @@ version = "1.4.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ce36e65b0d2999d2aafac989fb249189a141aee1f53c612c1f37d72631959f69"
dependencies = [
"proc-macro2",
"quote",
"proc-macro2 1.0.67",
"quote 1.0.33",
"syn 2.0.37",
]
@@ -1897,6 +1991,14 @@ dependencies = [
"pest_derive",
]
[[package]]
name = "zokrates_parser"
version = "0.3.5"
dependencies = [
"pest",
"pest_derive",
]
[[package]]
name = "zokrates_pest_ast"
version = "0.2.3"
@@ -1905,5 +2007,16 @@ dependencies = [
"lazy_static",
"pest",
"pest-ast",
"zokrates_parser",
"zokrates_parser 0.2.4",
]
[[package]]
name = "zokrates_pest_ast"
version = "0.3.3"
dependencies = [
"from-pest",
"lazy_static",
"pest",
"pest-ast",
"zokrates_parser 0.3.5",
]

7
Cargo.toml
View File

@@ -20,6 +20,8 @@ rsmt2 = { version = "0.14", optional = true }
ieee754 = { version = "0.2", optional = true}
zokrates_parser = { path = "third_party/ZoKrates/zokrates_parser", optional = true }
zokrates_pest_ast = { path = "third_party/ZoKrates/zokrates_pest_ast", optional = true }
zokrates_curly_parser = { package = "zokrates_parser", path = "third_party/ZoKratesCurly/zokrates_parser", optional = true }
zokrates_curly_pest_ast = { package = "zokrates_pest_ast", path = "third_party/ZoKratesCurly/zokrates_pest_ast", optional = true }
typed-arena = { version = "2.0", optional = true }
log = "0.4"
thiserror = "1.0"
@@ -65,6 +67,7 @@ default = []
# frontends
c = ["lang-c"]
zok = ["smt", "zokrates_parser", "zokrates_pest_ast", "typed-arena", "petgraph"]
zokc = ["smt", "zokrates_curly_parser", "zokrates_curly_pest_ast", "typed-arena", "petgraph"]
datalog = ["pest", "pest-ast", "pest_derive", "from-pest", "lazy_static"]
# backends
smt = ["rsmt2", "ieee754"]
@@ -90,6 +93,10 @@ required-features = ["bellman", "poly"]
name = "zxi"
required-features = ["smt", "zok"]
[[example]]
name = "zcxi"
required-features = ["smt", "zokc"]
[[example]]
name = "zxc"
required-features = ["smt", "zok"]

1
driver.py
View File

@@ -16,6 +16,7 @@ cargo_features = {
"r1cs",
"smt",
"zok",
"zokc",
"datalog",
"bellman",
"spartan",

3
examples/ZoKratesCurly/mpc/unit_tests/2pc_millionaires.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> bool {
return a < b;
}

11
examples/ZoKratesCurly/mpc/unit_tests/2pc_structs.zok Normal file
View File

@@ -0,0 +1,11 @@
struct Pt {
u32 x;
u32 y;
}
def main(private u32 a, private u32 b) -> u32 {
Pt c = Pt {x: 0, y: 1};
c.x = a;
c.y = b;
return c.y + c.x;
}

3
examples/ZoKratesCurly/mpc/unit_tests/arithmetic_tests/2pc_add.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> u32 {
return a + b;
}

3
examples/ZoKratesCurly/mpc/unit_tests/arithmetic_tests/2pc_int_equals.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> bool {
return a == b;
}

3
examples/ZoKratesCurly/mpc/unit_tests/arithmetic_tests/2pc_int_greater_equals.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> bool {
return a >= b;
}

3
examples/ZoKratesCurly/mpc/unit_tests/arithmetic_tests/2pc_int_greater_than.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> bool {
return a > b;
}

3
examples/ZoKratesCurly/mpc/unit_tests/arithmetic_tests/2pc_int_less_equals.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> bool {
return a <= b;
}

3
examples/ZoKratesCurly/mpc/unit_tests/arithmetic_tests/2pc_int_less_than.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> bool {
return a < b;
}

3
examples/ZoKratesCurly/mpc/unit_tests/arithmetic_tests/2pc_mult.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> u32 {
return a * b;
}

3
examples/ZoKratesCurly/mpc/unit_tests/arithmetic_tests/2pc_mult_add_pub.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b, u32 v) -> u32 {
return a * b + v;
}

3
examples/ZoKratesCurly/mpc/unit_tests/arithmetic_tests/2pc_sub.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> u32 {
return a - b;
}

3
examples/ZoKratesCurly/mpc/unit_tests/array_tests/2pc_array_ret.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> u32[2] {
return [a, b];
}

4
examples/ZoKratesCurly/mpc/unit_tests/array_tests/2pc_array_sum.zok Normal file
View File

@@ -0,0 +1,4 @@
def main(private u32 a, private u32 b) -> u32 {
u32[2] c = [a, b];
return c[0] + c[1];
}

3
examples/ZoKratesCurly/mpc/unit_tests/bitwise_tests/2pc_bitwise_and.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> u32 {
return a & b;
}

3
examples/ZoKratesCurly/mpc/unit_tests/bitwise_tests/2pc_bitwise_or.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> u32 {
return a | b;
}

3
examples/ZoKratesCurly/mpc/unit_tests/bitwise_tests/2pc_bitwise_xor.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> u32 {
return a ^ b;
}

3
examples/ZoKratesCurly/mpc/unit_tests/boolean_tests/2pc_boolean_and.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private bool a, private bool b) -> bool {
return a && b;
}

3
examples/ZoKratesCurly/mpc/unit_tests/boolean_tests/2pc_boolean_equals.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private bool a, private bool b) -> bool {
return a == b;
}

3
examples/ZoKratesCurly/mpc/unit_tests/boolean_tests/2pc_boolean_or.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private bool a, private bool b) -> bool {
return a || b;
}

4
examples/ZoKratesCurly/mpc/unit_tests/const_tests/2pc_const_arith.zok Normal file
View File

@@ -0,0 +1,4 @@
def main(private u32 a, private u32 b) -> u32 {
u32 c = 1;
return a + b + c;
}

4
examples/ZoKratesCurly/mpc/unit_tests/const_tests/2pc_const_bool.zok Normal file
View File

@@ -0,0 +1,4 @@
def main(private bool a, private bool b) -> bool {
bool c = true;
return a == c;
}

7
examples/ZoKratesCurly/mpc/unit_tests/function_tests/2pc_function_add.zok Normal file
View File

@@ -0,0 +1,7 @@
def add(u32 a, u32 b) -> u32 {
return a + b;
}
def main(private u32 a, private u32 b) -> u32 {
return add(a, b) + add(a, b);
}

7
examples/ZoKratesCurly/mpc/unit_tests/function_tests/function_arg_order.zok Normal file
View File

@@ -0,0 +1,7 @@
def sub(u32 b, u32 a) -> u32 {
return a - b;
}
def main(private u32 a, private u32 b) -> u32 {
return sub(b, a);
}

3
examples/ZoKratesCurly/mpc/unit_tests/ite_tests/2pc_ite_only_if.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b, public bool sel) -> u32 {
return if sel { a } else { b };
}

3
examples/ZoKratesCurly/mpc/unit_tests/ite_tests/2pc_ite_ret_bool.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private bool a, private bool b, public bool sel) -> bool {
return if sel { a } else { b };
}

3
examples/ZoKratesCurly/mpc/unit_tests/ite_tests/2pc_ite_ret_int.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b, public bool sel) -> u32 {
return if sel { a } else { b };
}

6
examples/ZoKratesCurly/mpc/unit_tests/loop_tests/2pc_loop_addition.zok Normal file
View File

@@ -0,0 +1,6 @@
def main(private u32 a, private u32 b) -> u32 {
for u32 i in 0..4 {
a = a + b;
}
return a;
}

7
examples/ZoKratesCurly/mpc/unit_tests/loop_tests/2pc_loop_sum.zok Normal file
View File

@@ -0,0 +1,7 @@
def main(private u32 a, private u32 b) -> u32 {
u32 mut res = 0x00000000;
for u32 i in 0..5 {
res = res + i;
}
return res;
}

3
examples/ZoKratesCurly/mpc/unit_tests/nary_arithmetic_tests/2pc_nary_arithmetic_add.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b, private u32 c) -> u32 {
return a + b + c;
}

3
examples/ZoKratesCurly/mpc/unit_tests/nary_boolean_tests/2pc_nary_boolean_and.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private bool a, private bool b, private bool c) -> bool {
return a && b && c;
}

4
examples/ZoKratesCurly/mpc/unit_tests/shift_tests/2pc_lhs.zok Normal file
View File

@@ -0,0 +1,4 @@
def main(private u32 a, private u32 b) -> u32 {
u32 c = 0x00000001;
return a << c;
}

4
examples/ZoKratesCurly/mpc/unit_tests/shift_tests/2pc_rhs.zok Normal file
View File

@@ -0,0 +1,4 @@
def main(private u32 a, private u32 b) -> u32 {
u32 c = 0x00000001;
return a >> c;
}

3
examples/ZoKratesCurly/opt/3_plus_opt.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u8 x) -> u8 {
return x + x + x;
}

3
examples/ZoKratesCurly/opt/id_opt.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u8 x) -> u8 {
return x;
}

12
examples/ZoKratesCurly/opt/log.zok Normal file
View File

@@ -0,0 +1,12 @@
def u8log2(u8 x) -> u8 {
u8 mut acc = 0x00;
for field i in 0..8 {
acc = acc + if x != 0x00 { 0x01 } else { 0x00 };
x = x >> 1;
}
return acc;
}
def main(private u8 x) -> u8 {
return x + u8log2(x);
}

12
examples/ZoKratesCurly/opt/log16.zok Normal file
View File

@@ -0,0 +1,12 @@
def u16log2(x: u16) -> u16 {
u16 mut acc = 0x0000;
for field i in 0..16 {
acc = acc + if x != 0x0000 { 0x0001 } else { 0x0000 };
x = x >> 1;
}
return acc;
}
def main(private x: u16) -> u16 {
return x + u16log2(x);
}

3
examples/ZoKratesCurly/opt/mult_opt.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u8 x, private u8 y) -> u8 {
return x * y;
}

3
examples/ZoKratesCurly/opt/plus_3_opt.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u8 x) -> u8 {
return 0x03 + x;
}

3
examples/ZoKratesCurly/opt/times_2_opt.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u8 x) -> u8 {
return 0x02 * x;
}

3
examples/ZoKratesCurly/opt/times_2_u32_opt.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u32 x) -> u32 {
return 0x00000002 * x;
}

3
examples/ZoKratesCurly/opt/times_3_opt.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u8 x) -> u8 {
return 0x03 * x;
}

7
examples/ZoKratesCurly/pf/2024_05_24_benny_bug.zok.pin Normal file
View File

@@ -0,0 +1,7 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(x #f6)
) false ; ignored
))

7
examples/ZoKratesCurly/pf/2024_05_24_benny_bug.zok.vin Normal file
View File

@@ -0,0 +1,7 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(x #f6)
(return #f0)
) false ; ignored
))

6
examples/ZoKratesCurly/pf/2024_05_31_benny_bug.zok.pin Normal file
View File

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

7
examples/ZoKratesCurly/pf/2024_05_31_benny_bug.zok.vin Normal file
View File

@@ -0,0 +1,7 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(x #f6)
(return #f6)
) false ; ignored
))

23
examples/ZoKratesCurly/pf/2024_06_02_chad_bug.zok Normal file
View File

@@ -0,0 +1,23 @@
struct BigNat_init_quotient<Qm1, Lp1> {
field[Qm1][Lp1] limbs;
field last_limb;
}
struct BigNat_init<N, Lp1> {
field[N][Lp1] limbs;
}
struct BigNatModMult_init<Qm1, Lp1, ZG, CL> {
BigNat_init_quotient<Qm1, Lp1> quotient_init;
BigNat_init<ZG, CL> carry_init;
}
const u32 Qm1 = 7;
const u32 Lp1 = 4;
const u32 ZG = 2;
const u32 CL = 5;
def main(private BigNatModMult_init<Qm1,Lp1,ZG,CL>[1] intermediate_mod) -> bool {
BigNat_init<ZG, CL> carry = intermediate_mod[0].carry_init;
assert(carry.limbs[0][0] == 1);
return true;
}

19
examples/ZoKratesCurly/pf/2024_07_01_chad_bug_wit.zok Normal file
View File

@@ -0,0 +1,19 @@
def unsafe_baz<M>(field input) -> field[M] {
return [input; M];
}
def foo<M>(field input) -> field[M] {
unsafe witness field[M] inputs = unsafe_baz::<M>(input);
assert(inputs[0] == input);
return inputs;
}
def bar<N, M>(field[N][M] input) -> field[M] {
return foo::<M>(input[0][0]);
}
def main(field[8] a) -> bool {
field[8] x = bar::<2, 8>([a, a]);
field[8] y = bar::<2, 8>([x, a]);
return true;
}

3
examples/ZoKratesCurly/pf/3_plus.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private u8 x) -> u8 {
return x + x + x;
}

5
examples/ZoKratesCurly/pf/3_plus.zok.pin Normal file
View File

@@ -0,0 +1,5 @@
(let (
(x #x04)
)
false
)

6
examples/ZoKratesCurly/pf/3_plus.zok.vin Normal file
View File

@@ -0,0 +1,6 @@
(let (
(return #x0c)
)
false
)

15
examples/ZoKratesCurly/pf/arr_str_arr_str.zok Normal file
View File

@@ -0,0 +1,15 @@
struct Pt {
field x;
field y;
}
struct Pts {
Pt[2] pts;
}
def main(private field y) -> field {
Pt p1 = Pt {x: 2, y: y};
Pt p2 = Pt {x: y, y: 2};
Pts[1] pts = [Pts { pts: [p1, p2] }];
return pts[0].pts[0].y * pts[0].pts[1].x;
}

9
examples/ZoKratesCurly/pf/arr_str_arr_str.zok.pin Normal file
View File

@@ -0,0 +1,9 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(y #f4)
) true ;ignored
)
)

7
examples/ZoKratesCurly/pf/arr_str_arr_str.zok.vin Normal file
View File

@@ -0,0 +1,7 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(return #f16)
) true ;ignored
)
)

10
examples/ZoKratesCurly/pf/assembly_constraint.zok Normal file
View File

@@ -0,0 +1,10 @@
def main(private field a, private field b, private field c) -> field{
field d = a * b;
field e = 7;
asm {
e <-- a * c;
20 === a * c;
}
assert(d == e);
return 1;
}

8
examples/ZoKratesCurly/pf/assembly_constraint.zok.pin Normal file
View File

@@ -0,0 +1,8 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(a #f4)
(b #f5)
(c #f5)
) true ;ignored
)
)

9
examples/ZoKratesCurly/pf/assembly_constraint.zok.vin Normal file
View File

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

9
examples/ZoKratesCurly/pf/assembly_field_to_bool_unsafe.zok Normal file
View File

@@ -0,0 +1,9 @@
from "EMBED" import field_to_bool_unsafe;
def main(private field x) -> bool {
asm {
x * (x - 1) === 0;
}
bool out = field_to_bool_unsafe(x);
return out;
}

6
examples/ZoKratesCurly/pf/assembly_field_to_bool_unsafe.zok.pin Normal file
View File

@@ -0,0 +1,6 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(x #f1)
) true ;ignored
)
)

9
examples/ZoKratesCurly/pf/assembly_field_to_bool_unsafe.zok.vin Normal file
View File

@@ -0,0 +1,9 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(return true)
) true; ignored
))

10
examples/ZoKratesCurly/pf/assembly_unconstraint.zok Normal file
View File

@@ -0,0 +1,10 @@
// Here we miss the constraint so we can give different values than 5 to b and c
def main(private field a, private field b, private field c) -> field{
field d = a * b;
field e = 7;
asm {
e <-- a * c;
}
assert(d == e);
return 1;
}

8
examples/ZoKratesCurly/pf/assembly_unconstraint.zok.pin Normal file
View File

@@ -0,0 +1,8 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(a #f4)
(b #f4)
(c #f4)
) true ;ignored
)
)

9
examples/ZoKratesCurly/pf/assembly_unconstraint.zok.vin Normal file
View File

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

4
examples/ZoKratesCurly/pf/assert.zok Normal file
View File

@@ -0,0 +1,4 @@
def main(private field A, private field B) -> field {
assert(A != B);
return A * B;
}

10
examples/ZoKratesCurly/pf/assert.zok.pin Normal file
View File

@@ -0,0 +1,10 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(A #f4)
(B #f5)
) true ;ignored
)
)

9
examples/ZoKratesCurly/pf/assert.zok.vin Normal file
View File

@@ -0,0 +1,9 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(return #f20)
) true ;ignored
)
)

4
examples/ZoKratesCurly/pf/assert2.zok Normal file
View File

@@ -0,0 +1,4 @@
def main(private field A, private field B) -> bool {
assert(A + B == 123);
return true;
}

10
examples/ZoKratesCurly/pf/assert2.zok.pin Normal file
View File

@@ -0,0 +1,10 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(A #f4)
(B #f-4)
) true ;ignored
))

9
examples/ZoKratesCurly/pf/assert2.zok.vin Normal file
View File

@@ -0,0 +1,9 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(return true)
) true; ignored
))

19
examples/ZoKratesCurly/pf/chall/poly_mult.zok Normal file
View File

@@ -0,0 +1,19 @@
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 {
xpows[i+1] = xpows[i] * x;
}
field fx = 0;
field gx = 0;
field hx = 0;
for field i in 0..3 {
fx = fx + xpows[i] * f[i];
gx = gx + xpows[i] * g[i];
}
for field i in 0..6 {
hx = hx + xpows[i] * h[i];
}
assert(fx * gx == hx);
return f[0];
}

20
examples/ZoKratesCurly/pf/chall/poly_mult.zok.pin Normal file
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
))

5
examples/ZoKratesCurly/pf/chall/poly_mult.zok.vin Normal file
View File

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

5
examples/ZoKratesCurly/pf/chall/simple.zok Normal file
View File

@@ -0,0 +1,5 @@
def main(private field x, private field y) -> field {
field a = sample_challenge([x, y]);
assert(a * x == a * y);
return x;
}

6
examples/ZoKratesCurly/pf/chall/simple.zok.pin Normal file
View File

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

6
examples/ZoKratesCurly/pf/chall/simple.zok.vin Normal file
View File

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

24
examples/ZoKratesCurly/pf/const_linear_lookup.zok Normal file
View File

@@ -0,0 +1,24 @@
struct T {
field v;
field w;
field x;
field y;
field z;
}
const T[9] TABLE = [
T { v: 1, w: 12, x: 13, y: 14, z: 15 },
T { v: 2, w: 22, x: 23, y: 24, z: 25 },
T { v: 3, w: 32, x: 33, y: 34, z: 35 },
T { v: 4, w: 42, x: 43, y: 44, z: 45 },
T { v: 5, w: 52, x: 53, y: 54, z: 55 },
T { v: 6, w: 62, x: 63, y: 64, z: 65 },
T { v: 7, w: 72, x: 73, y: 74, z: 75 },
T { v: 8, w: 82, x: 83, y: 84, z: 85 },
T { v: 9, w: 92, x: 93, y: 94, z: 95 }
];
def main(field i) -> field {
T t = TABLE[i];
return t.v + t.w + t.x + t.y + t.z;
}

3
examples/ZoKratesCurly/pf/field_max.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(private field x, private field y) -> field {
return if x > y { x } else { y };
}

6
examples/ZoKratesCurly/pf/field_max.zok.pin Normal file
View File

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

5
examples/ZoKratesCurly/pf/field_max.zok.vin Normal file
View File

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

1
examples/ZoKratesCurly/pf/hash/sha256lookup/Readme.md Normal file
View File

@@ -0,0 +1 @@
This directory contains a SHA256 implementation by Anna Woo.

3
examples/ZoKratesCurly/pf/hash/sha256lookup/assert_well_formed.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(BigNatb<10, 256> a, BigNat<10> b) -> bool {
return true;
}

133
examples/ZoKratesCurly/pf/hash/sha256lookup/basic_op.zok Normal file
View File

@@ -0,0 +1,133 @@
def split_for_shift<N, R>(field[N] input, u32[N] LIMBWIDTH) -> field[2] {
u32 CUR_WIDTH = 0;
u32 SPLIT_IDX = 0;
u32 RED_R = R;
for u32 i in 0..N {
SPLIT_IDX = if CUR_WIDTH < R then i else SPLIT_IDX;
RED_R = if CUR_WIDTH < R then R-CUR_WIDTH else RED_R;
CUR_WIDTH = CUR_WIDTH + LIMBWIDTH[i];
}
u32 TOTAL_WIDTH = CUR_WIDTH;
u32 LOW_BITS = RED_R * 2;
u32 HIGH_BITS = 2*LIMBWIDTH[SPLIT_IDX] - 1 - LOW_BITS;
unsafe witness field[2] split = unsafe_split::<LOW_BITS, HIGH_BITS>(input[SPLIT_IDX]);
field[2] safe_split = [0, split[1]];
safe_split[0] = input[SPLIT_IDX] - split[1] * (2 ** LOW_BITS);
u32 RED_L = LIMBWIDTH[SPLIT_IDX] - RED_R;
assert(fits_in_bits_sparse::<RED_L>(safe_split[1]));
assert(fits_in_bits_sparse::<RED_R>(safe_split[0]));
CUR_WIDTH = 0;
field right = 0;
for u32 i in 0..SPLIT_IDX {
right = right + input[i] * (2 ** (2 * CUR_WIDTH));
CUR_WIDTH = CUR_WIDTH + LIMBWIDTH[i];
}
right = right + safe_split[0] * (2 ** (2 * CUR_WIDTH));
CUR_WIDTH = RED_L;
field left = safe_split[1];
for u32 i in (SPLIT_IDX+1)..N {
left = left + input[i] * (2 ** (2 * CUR_WIDTH));
CUR_WIDTH = CUR_WIDTH + LIMBWIDTH[i];
}
return [right, left];
}
def rotr<N, R>(field[N] input, u32[N] LIMBWIDTH_ORI, u32[N] LIMBWIDTH_NEW) -> field {
field[2] overall_split = split_for_shift::<N, R>(input, LIMBWIDTH_ORI);
u32 TOTAL_WIDTH = 0;
for u32 i in 0..N {
TOTAL_WIDTH = TOTAL_WIDTH + LIMBWIDTH_ORI[i];
}
assert(TOTAL_WIDTH == 32);
field output_val = overall_split[0] * (2 ** (2 * (TOTAL_WIDTH - R))) + overall_split[1];
return output_val;
}
def shr<N, R>(field[N] input, u32[N] LIMBWIDTH_ORI, u32[N] LIMBWIDTH_NEW) -> field {
field[2] overall_split = split_for_shift::<N, R>(input, LIMBWIDTH_ORI);
field output_val = overall_split[1];
return output_val;
}
def xor_10<N>(field[N] input) -> field {
assert(N == 2 || N == 3);
field sum = 0;
for u32 i in 0..N {
sum = sum + input[i];
}
Dual dual = split_even_dual_10(sum);
return dual.d;
}
def xor_11<N>(field[N] input) -> field {
assert(N == 2 || N == 3);
field sum = 0;
for u32 i in 0..N {
sum = sum + input[i];
}
Dual dual = split_even_dual_11(sum);
return dual.d;
}
def xor_for_all_limbs<N>(field[3] input, u32[3] LIMBWIDTH) -> field[3] {
field int = 0;
for u32 i in 0..3 {
int = int + input[i];
}
return split_even_dual_for_all_limbs(int, LIMBWIDTH);
}
def and_10(field[2] input) -> Dual {
return split_odd_dual_10(input[0] + input[1]);
}
def and_11(field[2] input) -> Dual {
return split_odd_dual_11(input[0] + input[1]);
}
def and(field[3] x, field[3] y) -> Dual[3] {
Dual[3] output = [Dual {d: 0, s: 0} ; 3];
output[0] = and_11([x[0], y[0]]);
output[1] = and_11([x[1], y[1]]);
output[2] = and_10([x[2], y[2]]);
return output;
}
def and_s2d(field[3] x, field[3] y) -> field[3] {
Dual[3] output = and(x, y);
return dual_limbs_to_dense_limbs(output);
}
def not_10(field input) -> field {
return S_ONES_10 - input;
}
def not_11(field input) -> field {
return S_ONES_11 - input;
}
def not(field[3] input) -> field[3] {
field[3] output = [0; 3];
output[0] = not_11(input[0]);
output[1] = not_11(input[1]);
output[2] = not_10(input[2]);
return output;
}
def sum<N, M, C, CM>(field[N] input, u32[M] LIMBWIDTH) -> Dual[M] {
assert((1 << C) >= N);
field sum = 0;
for u32 i in 0..N {
sum = sum + input[i];
}
u32 MP1 = M + 1;
u32[MP1] SPLITWIDTH = [...LIMBWIDTH, C];
unsafe witness field[MP1] split = unsafe_split_dyn::<MP1>(sum, SPLITWIDTH);
field[MP1] safe_split = [0, ...split[1..MP1]];
safe_split[0] = sum - combine_limbs::<M>(safe_split[1..MP1], SPLITWIDTH[1..MP1]) * (2 ** (LIMBWIDTH[0]));
assert(fits_in_bits::<CM>(safe_split[M]));
field res_sum = combine_limbs::<M>(safe_split[0..MP1], LIMBWIDTH);
return dense_limb_to_dual_limb::<M>(safe_split[0..M], LIMBWIDTH);
}

105
examples/ZoKratesCurly/pf/hash/sha256lookup/big_nat.zok Normal file
View File

@@ -0,0 +1,105 @@
struct BigNatParams {
field max_words;
}
struct BigNatb<N, W> {
bool[N][W] limbs;
}
struct BigNatb_v2<Nm1, W, W2> {
bool[Nm1][W] limbs;
bool[W2] limb;
}
struct BigNat<N> {
field[N] limbs;
}
struct GpBigNats<NG> {
BigNat<NG> left;
BigNat<NG> right;
}
struct BigNatModMult<W, A, Z, ZG, CW, Q, V> {
BigNat<Z> z;
BigNat<V> v;
BigNatb<Q, W> quotientb;
bool[ZG][CW] carry;
BigNatb<A, W> res;
}
struct BigNatModMult_v4<W, A, Z, CW, Q, V> {
BigNat<Z> z;
BigNat<V> v;
BigNatb<Q, W> quotientb;
bool[CW] carry;
BigNatb<A, W> res;
}
struct BigNatModMult_v5<W, W2, A, Z, CW, Qm1, V> {
BigNat<Z> z;
BigNat<V> v;
BigNatb_v2<Qm1, W, W2> quotientb;
bool[CW] carry;
BigNatb<A, W> res;
}
struct BigNatModMult_v6<W, W2, A, Z, ZG, Qm1, V> {
BigNat<Z> z;
BigNat<V> v;
BigNatb_v2<Qm1, W, W2> quotientb;
field[ZG] carry;
BigNatb<A, W> res;
}
struct BigNatModMultwores_v5<W, W2, Z, V, Qm1, CW> {
BigNat<Z> z;
BigNat<V> v;
BigNatb_v2<Qm1, W, W2> quotientb;
bool[CW] carry;
}
struct BigNatModMult_v2<W, W2, Am1, Z, ZG, CW, Qm1, V> {
BigNat<Z> z;
BigNat<V> v;
BigNatb_v2<Qm1, W, W2> quotientb;
bool[ZG][CW] carry;
BigNatb_v2<Am1, W, W2> res;
}
struct BigNatMod<W, A, ZG, CW, Q, V> {
BigNat<V> v;
BigNatb<Q, W> quotientb;
bool[ZG][CW] carry;
BigNatb<A, W> res;
}
struct BigNatMont<W, Z, ZG, CW, P, Q, V> {
BigNatb<P, W>[3] res;
BigNatModMult<W, Z, ZG, CW, Q, V>[3] mm;
bool greaterthanp;
bool[ZG][CW] carry;
}
struct BigNatAdd<Z, ZG, ZGW, Q, QW, V> {
BigNat<V> v;
BigNatb<Q, QW> quotientb;
bool[ZG][ZGW] carry;
}
struct ModuloConst<ZG, NG, AC>{
u8[ZG] CW_list;
field[NG] gp_maxword;
field[AC] aux_const;
}
struct ModuloHelperConst<ZG, NG, AC>{
ModuloConst<ZG, NG, AC> moduloconst;
field shift;
}
const BigNat<34> r = {limbs: [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,10141204801825835211973625643008]};
def main(BigNatb<10, 256> a, BigNat<10> b) -> bool {
return true;
}

5
examples/ZoKratesCurly/pf/hash/sha256lookup/const.zok Normal file
View File

@@ -0,0 +1,5 @@
def main() {
const field[64] K_DD = [1116352408, 1899447441, 3049323471, 3921009573, 961987163, 1508970993, 2453635748, 2870763221, 3624381080, 310598401, 607225278, 1426881987, 1925078388, 2162078206, 2614888103, 3248222580, 3835390401, 4022224774, 264347078, 604807628, 770255983, 1249150122, 1555081692, 1996064986, 2554220882, 2821834349, 2952996808, 3210313671, 3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298];
const Dual[8][3] IV_S = [[Dual {d: 1639, s: 1315861}, Dual {d: 316, s: 66896}, Dual {d: 424, s: 83008}], [Dual {d: 1669, s: 1327121}, Dual {d: 1269, s: 1070353}, Dual {d: 749, s: 283729}], [Dual {d: 882, s: 333060}, Dual {d: 1502, s: 1134932}, Dual {d: 241, s: 21761}], [Dual {d: 1338, s: 1115460}, Dual {d: 510, s: 87380}, Dual {d: 661, s: 278801}], [Dual {d: 639, s: 267605}, Dual {d: 458, s: 86084}, Dual {d: 324, s: 69648}], [Dual {d: 140, s: 16464}, Dual {d: 173, s: 17489}, Dual {d: 620, s: 267344}], [Dual {d: 427, s: 83013}, Dual {d: 123, s: 5445}, Dual {d: 126, s: 5460}], [Dual {d: 1305, s: 1114433}, Dual {d: 1049, s: 1048897}, Dual {d: 367, s: 70741}]];
return;
}

10
examples/ZoKratesCurly/pf/hash/sha256lookup/const_range_check.zok Normal file
View File

@@ -0,0 +1,10 @@
const transcript field[2] D_1 = [0, 1];
const transcript field[4] D_2 = [0, 1, 2, 3];
const transcript field[8] D_3 = [0, 1, 2, 3, 4, 5, 6, 7];
const transcript field[16] D_4 = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15];
const transcript field[32] D_5 = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31];
const transcript field[64] D_6 = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63];
const transcript field[128] D_7 = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127];
const transcript field[256] D_8 = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255];
const transcript field[512] D_9 = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255, 256, 257, 258, 259, 260, 261, 262, 263, 264, 265, 266, 267, 268, 269, 270, 271, 272, 273, 274, 275, 276, 277, 278, 279, 280, 281, 282, 283, 284, 285, 286, 287, 288, 289, 290, 291, 292, 293, 294, 295, 296, 297, 298, 299, 300, 301, 302, 303, 304, 305, 306, 307, 308, 309, 310, 311, 312, 313, 314, 315, 316, 317, 318, 319, 320, 321, 322, 323, 324, 325, 326, 327, 328, 329, 330, 331, 332, 333, 334, 335, 336, 337, 338, 339, 340, 341, 342, 343, 344, 345, 346, 347, 348, 349, 350, 351, 352, 353, 354, 355, 356, 357, 358, 359, 360, 361, 362, 363, 364, 365, 366, 367, 368, 369, 370, 371, 372, 373, 374, 375, 376, 377, 378, 379, 380, 381, 382, 383, 384, 385, 386, 387, 388, 389, 390, 391, 392, 393, 394, 395, 396, 397, 398, 399, 400, 401, 402, 403, 404, 405, 406, 407, 408, 409, 410, 411, 412, 413, 414, 415, 416, 417, 418, 419, 420, 421, 422, 423, 424, 425, 426, 427, 428, 429, 430, 431, 432, 433, 434, 435, 436, 437, 438, 439, 440, 441, 442, 443, 444, 445, 446, 447, 448, 449, 450, 451, 452, 453, 454, 455, 456, 457, 458, 459, 460, 461, 462, 463, 464, 465, 466, 467, 468, 469, 470, 471, 472, 473, 474, 475, 476, 477, 478, 479, 480, 481, 482, 483, 484, 485, 486, 487, 488, 489, 490, 491, 492, 493, 494, 495, 496, 497, 498, 499, 500, 501, 502, 503, 504, 505, 506, 507, 508, 509, 510, 511];
const transcript field[1024] D_10 = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255, 256, 257, 258, 259, 260, 261, 262, 263, 264, 265, 266, 267, 268, 269, 270, 271, 272, 273, 274, 275, 276, 277, 278, 279, 280, 281, 282, 283, 284, 285, 286, 287, 288, 289, 290, 291, 292, 293, 294, 295, 296, 297, 298, 299, 300, 301, 302, 303, 304, 305, 306, 307, 308, 309

69
examples/ZoKratesCurly/pf/hash/sha256lookup/logic_func.zok Normal file
View File

@@ -0,0 +1,69 @@
// Importing external functions
from "basic_op" import xor_11, xor_10, xor_for_all_limbs, rotr, shr, and_s2s, and_s2d, not;
from "utils" import combine_limbs, combine_sparse_limbs, split_odd_dual_11, split_odd_dual_10, Dual, dual_limbs_to_dense_limbs;
def ssig0<N>(field[N] input, u32[N] LIMBWIDTH) -> field {
field[3] int = [0; 3];
int[0] = rotr::<N, 7>(input, LIMBWIDTH, LIMBWIDTH);
int[1] = rotr::<N, 18>(input, LIMBWIDTH, LIMBWIDTH);
int[2] = shr::<N, 3>(input, LIMBWIDTH, LIMBWIDTH);
field[N] output_limbs = xor_for_all_limbs::<3>(int, LIMBWIDTH);
return combine_limbs::<N>(output_limbs, LIMBWIDTH);
}
def ssig1<N>(field[N] input, u32[N] LIMBWIDTH) -> field {
field[3] int = [0; 3];
int[0] = rotr::<N, 17>(input, LIMBWIDTH, LIMBWIDTH);
int[1] = rotr::<N, 19>(input, LIMBWIDTH, LIMBWIDTH);
int[2] = shr::<N, 10>(input, LIMBWIDTH, LIMBWIDTH);
field[N] output_limbs = xor_for_all_limbs::<3>(int, LIMBWIDTH);
return combine_limbs::<N>(output_limbs, LIMBWIDTH);
}
def bsig0<N>(field[N] input) -> field {
u32[N] LIMBWIDTH_ORI = [11, 11, 10];
u32[N] LIMBWIDTH_NEW = [10, 11, 11];
field[3] int = [0; 3];
int[0] = rotr::<N, 2>(input, LIMBWIDTH_ORI, LIMBWIDTH_NEW);
int[1] = rotr::<N, 13>(input, LIMBWIDTH_ORI, LIMBWIDTH_NEW);
int[2] = combine_sparse_limbs::<N>([input[2], input[0], input[1]], LIMBWIDTH_NEW);
field[N] output_limbs = xor_for_all_limbs::<3>(int, LIMBWIDTH_ORI);
return combine_limbs::<N>(output_limbs, LIMBWIDTH_ORI);
}
def bsig1<N>(field[N] input) -> field {
u32[N] LIMBWIDTH_ORI = [11, 11, 10];
u32[N] LIMBWIDTH_NEW = [11, 10, 11];
field[3] int = [0; 3];
int[0] = rotr::<N, 6>(input, LIMBWIDTH_ORI, LIMBWIDTH_NEW);
int[1] = combine_sparse_limbs::<N>([input[1], input[2], input[0]], LIMBWIDTH_NEW);
int[2] = rotr::<N, 25>(input, LIMBWIDTH_ORI, LIMBWIDTH_NEW);
field[N] output_limbs = xor_for_all_limbs::<3>(int, LIMBWIDTH_ORI);
return combine_limbs::<N>(output_limbs, LIMBWIDTH_ORI);
}
def maj<N>(field[3][N] input) -> field {
field[N] intermediate = [0; N];
for u32 i in 0..N {
intermediate[i] = input[0][i] + input[1][i] + input[2][i];
}
Dual[N] output_dual = [Dual{d: 0, s: 0}; N];
output_dual[0] = split_odd_dual_11(intermediate[0]);
output_dual[1] = split_odd_dual_11(intermediate[1]);
output_dual[2] = split_odd_dual_10(intermediate[2]);
u32[N] LIMBWIDTH = [11, 11, 10];
field[N] output_limbs = dual_limbs_to_dense_limbs::<N>(output_dual);
return combine_limbs::<N>(output_limbs, LIMBWIDTH);
}
def ch<N>(field[3][N] input) -> field {
field[2][N] int = [[0; N]; 2];
int[0] = and_s2d(input[0], input[1]);
int[1] = and_s2d(not(input[0]), input[2]);
field[N] output_limbs = [0; N];
for u32 i in 0..N {
output_limbs[i] = int[0][i] + int[1][i];
}
u32[N] LIMBWIDTH = [11, 11, 10];
return combine_limbs::<N>(output_limbs, LIMBWIDTH);
}

13
examples/ZoKratesCurly/pf/hash/sha256lookup/sha256.zok Normal file
View File

@@ -0,0 +1,13 @@
def main<N, NL>(field[N][16][NL] message) -> field[8] {
u32[NL] LIMBWIDTH = [11, 11, 10];
Dual[8][NL] current = IV_S;
for u32 i in 0..N {
Dual[16][NL] cur_msg = dense_limbs_to_dual_limbs::<16, NL>(message[i], LIMBWIDTH);
current = shaRound::<NL>(cur_msg, current, LIMBWIDTH);
}
field[8] output = [0; 8];
for u32 i in 0..8 {
output[i] = combine_limbs(dual_limbs_to_dense_limbs(current[i]), LIMBWIDTH);
}
return output;
}

71
examples/ZoKratesCurly/pf/hash/sha256lookup/shaRound.zok Normal file
View File

@@ -0,0 +1,71 @@
from "logic_func" import ssig0, ssig1, bsig0, bsig1, ch, maj
from "utils" import Dual, combine_limbs, dual_limbs_to_sparse_limbs, dual_limbs_to_dense_limbs
from "basic_op" import sum
from "const" import K_DD // K_S
def one_extend<N, CM>(w_input: Dual[4][N], LIMBWIDTH: u32[N]) -> Dual[N] {
let addend: field[4] = [0; 4];
addend[0] = ssig1::<N>(dual_limbs_to_sparse_limbs(w_input[0]), LIMBWIDTH);
addend[1] = combine_limbs::<N>(dual_limbs_to_dense_limbs(w_input[1]), LIMBWIDTH);
addend[2] = ssig0::<N>(dual_limbs_to_sparse_limbs(w_input[2]), LIMBWIDTH);
addend[3] = combine_limbs::<N>(dual_limbs_to_dense_limbs(w_input[3]), LIMBWIDTH);
return sum::<4, N, 2, CM>(addend, LIMBWIDTH);
}
def whole_extend<N, CM>(message: Dual[16][N], LIMBWIDTH: u32[N]) -> Dual[64][N] {
let mut w: Dual[64][N] = [...message, ...[[Dual{s: 0, d: 0}; N]; 48]];
for i: u32 in 16..64 {
w[i] = one_extend::<N, CM>([w[i-2], w[i-7], w[i-15], w[i-16]], LIMBWIDTH);
}
return w;
}
def one_main<N, CM>(input: Dual[8][N], k: field, w: Dual[N], LIMBWIDTH: u32[N]) -> Dual[8][N] {
let t1: field[5] = [0; 5];
t1[0] = combine_limbs::<N>(dual_limbs_to_dense_limbs(input[7]), LIMBWIDTH);
t1[1] = bsig1::<N>(dual_limbs_to_sparse_limbs(input[4]));
let input_to_ch: field[3][N] = [dual_limbs_to_sparse_limbs(input[4]), dual_limbs_to_sparse_limbs(input[5]), dual_limbs_to_sparse_limbs(input[6])];
t1[2] = ch::<N>(input_to_ch);
t1[3] = k;
t1[4] = combine_limbs::<N>(dual_limbs_to_dense_limbs(w), LIMBWIDTH);
let t2: field[2] = [0; 2];
t2[0] = bsig0::<N>(dual_limbs_to_sparse_limbs(input[0]));
let input_to_maj: field[3][N] = [dual_limbs_to_sparse_limbs(input[0]), dual_limbs_to_sparse_limbs(input[1]), dual_limbs_to_sparse_limbs(input[2])];
t2[1] = maj::<N>(input_to_maj);
let mut output: Dual[8][N] = [[Dual{s: 0, d: 0}; N]; 8];
for i: u32 in 0..8 {
let j: u32 = (i + 7) % 8;
output[i] = input[j];
}
output[0] = sum::<7, N, 3, CM>([...t1, ...t2], LIMBWIDTH);
let d_val: field = combine_limbs::<N>(dual_limbs_to_dense_limbs(input[3]), LIMBWIDTH);
output[4] = sum::<6, N, 3, CM>([d_val, ...t1], LIMBWIDTH);
return output;
}
def whole_main<N, CM>(current: Dual[8][N], w: Dual[64][N], LIMBWIDTH: u32[N]) -> Dual[8][N] {
let mut interm: Dual[8][N] = current;
for i: u32 in 0..64 {
interm = one_main::<N, CM>(interm, K_DD[i], w[i], LIMBWIDTH);
}
return interm;
}
def compute_final_output<N, CM>(interm: Dual[8][N], current: Dual[8][N], LIMBWIDTH: u32[N]) -> Dual[8][N] {
let mut output: Dual[8][N] = [[Dual{s: 0, d: 0}; N]; 8];
for i: u32 in 0..8 {
let cur_val: field = combine_limbs::<N>(dual_limbs_to_dense_limbs(current[i]), LIMBWIDTH);
let interm_val: field = combine_limbs::<N>(dual_limbs_to_dense_limbs(interm[i]), LIMBWIDTH);
output[i] = sum::<2, N, 1, CM>([cur_val, interm_val], LIMBWIDTH);
}
return output;
}
def main<N>(input: Dual[16][N], current: Dual[8][N], LIMBWIDTH: u32[3]) -> Dual[8][N] {
let CM: u32 = 3;
let w: Dual[64][N] = whole_extend::<N, CM>(input, LIMBWIDTH);
let interm: Dual[8][N] = whole_main::<N, CM>(current, w, LIMBWIDTH);
return compute_final_output::<N, CM>(interm, current, LIMBWIDTH);
}

5
examples/ZoKratesCurly/pf/hash/sha256lookup/test_sha256_adv.zok Normal file
View File

@@ -0,0 +1,5 @@
def test_sha256<N, NL>(field[8] expected_hash, field[N][16][NL] padded_message) -> bool {
field[8] actual_hash = sha256::<N, NL>(padded_message);
assert(expected_hash == actual_hash);
return true;
}

3
examples/ZoKratesCurly/pf/hash/sha256lookup/test_sha256_adv1.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(field[8] expected_hash, private field[N][16][NL] padded_message) -> bool {
return test_sha256::<N, NL>(expected_hash, padded_message);
}

3
examples/ZoKratesCurly/pf/hash/sha256lookup/test_sha256_adv8.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(field[8] expected_hash, private field[8][16][3] padded_message) -> bool {
return test_sha256::<8, 3>(expected_hash, padded_message);
}

396
examples/ZoKratesCurly/pf/hash/sha256lookup/test_sha256_adv8.zok.pin Normal file
View File

@@ -0,0 +1,396 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(padded_message.3.0.2 #f12)
(padded_message.0.1.0 #f513)
(padded_message.1.0.0 #f531)
(padded_message.5.0.1 #f6)
(padded_message.4.15.1 #f2016)
(padded_message.0.0.1 #f65)
(padded_message.0.2.1 #f66)
(padded_message.1.3.1 #f1614)
(padded_message.1.12.2 #f197)
(padded_message.1.15.0 #f49)
(padded_message.3.10.0 #f1503)
(padded_message.3.13.2 #f751)
(padded_message.4.14.2 #f340)
(padded_message.5.15.2 #f83)
(padded_message.3.6.1 #f961)
(padded_message.6.3.1 #f32)
(padded_message.3.14.2 #f621)
(padded_message.2.0.2 #f216)
(padded_message.2.7.0 #f1036)
(padded_message.7.6.2 #f0)
(expected_hash.1 #f1327195860)
(padded_message.5.14.0 #f582)
(padded_message.3.0.0 #f1795)
(padded_message.5.9.2 #f13)
(padded_message.1.13.1 #f737)
(padded_message.3.10.2 #f163)
(padded_message.6.0.1 #f1254)
(padded_message.2.6.1 #f192)
(padded_message.4.7.2 #f8)
(padded_message.7.4.2 #f0)
(padded_message.0.9.2 #f988)
(padded_message.1.8.2 #f192)
(padded_message.7.11.1 #f0)
(padded_message.2.2.0 #f304)
(padded_message.2.4.0 #f560)
(padded_message.3.3.1 #f71)
(padded_message.7.15.1 #f1)
(padded_message.4.11.1 #f192)
(expected_hash.7 #f1529670075)
(padded_message.5.12.1 #f1520)
(padded_message.5.4.2 #f315)
(padded_message.3.13.1 #f228)
(padded_message.4.14.1 #f930)
(padded_message.5.15.1 #f1646)
(padded_message.7.13.1 #f0)
(padded_message.7.3.2 #f0)
(padded_message.2.5.1 #f1570)
(padded_message.4.2.2 #f520)
(padded_message.4.9.0 #f1036)
(padded_message.0.4.2 #f900)
(padded_message.0.6.2 #f502)
(padded_message.5.2.2 #f56)
(padded_message.0.11.1 #f1569)
(padded_message.5.9.0 #f1315)
(padded_message.6.7.2 #f192)
(padded_message.4.13.1 #f384)
(padded_message.6.9.2 #f232)
(padded_message.7.6.0 #f0)
(padded_message.7.8.0 #f0)
(padded_message.1.5.2 #f457)
(padded_message.1.8.0 #f1539)
(padded_message.7.9.1 #f0)
(padded_message.2.1.0 #f563)
(padded_message.4.8.1 #f192)
(padded_message.3.10.1 #f273)
(expected_hash.5 #f2797358084)
(padded_message.0.15.2 #f192)
(padded_message.5.1.2 #f24)
(padded_message.5.4.0 #f1892)
(padded_message.5.6.0 #f605)
(padded_message.3.14.1 #f560)
(padded_message.6.4.2 #f193)
(padded_message.7.3.0 #f0)
(padded_message.0.12.0 #f853)
(padded_message.4.2.0 #f1328)
(padded_message.7.5.0 #f0)
(padded_message.0.1.2 #f640)
(padded_message.0.3.2 #f623)
(padded_message.0.6.0 #f501)
(padded_message.1.0.2 #f340)
(padded_message.1.2.2 #f413)
(padded_message.1.9.0 #f787)
(padded_message.4.7.1 #f240)
(padded_message.4.11.2 #f172)
(padded_message.5.12.2 #f510)
(padded_message.3.7.2 #f728)
(padded_message.4.10.1 #f320)
(padded_message.5.7.1 #f512)
(padded_message.5.11.1 #f657)
(padded_message.4.15.0 #f1026)
(padded_message.5.14.1 #f540)
(padded_message.6.8.1 #f1678)
(padded_message.7.4.1 #f0)
(expected_hash.0 #f2856353870)
(padded_message.0.7.1 #f416)
(padded_message.0.9.1 #f416)
(padded_message.1.6.1 #f1636)
(padded_message.4.13.2 #f192)
(padded_message.7.0.0 #f1285)
(padded_message.1.14.2 #f204)
(padded_message.0.12.2 #f36)
(padded_message.2.9.2 #f445)
(padded_message.4.3.0 #f304)
(padded_message.5.1.0 #f1309)
(padded_message.4.12.1 #f224)
(padded_message.5.3.0 #f961)
(padded_message.5.13.1 #f697)
(padded_message.6.1.2 #f24)
(padded_message.6.4.0 #f39)
(padded_message.3.2.2 #f272)
(padded_message.3.9.0 #f2022)
(padded_message.0.3.0 #f865)
(padded_message.1.2.0 #f1312)
(padded_message.5.2.1 #f130)
(padded_message.5.4.1 #f225)
(padded_message.6.11.2 #f449)
(padded_message.4.0.1 #f23)
(padded_message.7.1.1 #f0)
(padded_message.0.4.1 #f920)
(padded_message.0.11.0 #f816)
(padded_message.1.5.1 #f1741)
(padded_message.1.7.1 #f102)
(padded_message.6.5.1 #f261)
(padded_message.6.7.1 #f48)
(padded_message.1.10.2 #f41)
(padded_message.3.8.1 #f766)
(padded_message.2.12.2 #f24)
(padded_message.6.13.2 #f189)
(padded_message.2.2.2 #f192)
(padded_message.1.14.0 #f1073)
(padded_message.2.9.0 #f1125)
(padded_message.6.15.1 #f193)
(padded_message.0.13.1 #f194)
(padded_message.1.1.0 #f1903)
(padded_message.7.8.2 #f0)
(padded_message.6.1.0 #f774)
(padded_message.2.13.1 #f455)
(padded_message.3.2.0 #f1342)
(padded_message.5.1.1 #f106)
(padded_message.6.2.1 #f160)
(padded_message.0.14.0 #f290)
(padded_message.4.9.2 #f116)
(padded_message.2.8.1 #f1484)
(padded_message.3.11.1 #f1138)
(padded_message.0.1.1 #f96)
(padded_message.1.0.1 #f129)
(padded_message.2.10.1 #f1133)
(padded_message.6.14.2 #f197)
(padded_message.2.1.2 #f92)
(padded_message.2.3.2 #f192)
(padded_message.2.6.0 #f853)
(padded_message.2.15.2 #f537)
(padded_message.3.5.1 #f1629)
(padded_message.3.15.1 #f280)
(padded_message.2.12.0 #f646)
(padded_message.2.14.1 #f193)
(padded_message.3.1.0 #f1109)
(padded_message.3.3.0 #f1951)
(padded_message.5.6.2 #f983)
(padded_message.5.8.2 #f668)
(padded_message.7.5.2 #f0)
(padded_message.2.7.1 #f97)
(padded_message.4.4.2 #f56)
(padded_message.7.7.2 #f0)
(padded_message.0.8.2 #f170)
(padded_message.4.12.0 #f769)
(padded_message.6.10.2 #f397)
(padded_message.2.11.2 #f193)
(padded_message.7.12.2 #f0)
(padded_message.3.0.1 #f32)
(padded_message.6.11.1 #f1389)
(padded_message.1.7.2 #f305)
(padded_message.1.9.2 #f340)
(expected_hash.2 #f3085693120)
(padded_message.2.3.0 #f310)
(padded_message.2.15.0 #f1597)
(padded_message.1.15.1 #f1543)
(padded_message.1.12.1 #f102)
(padded_message.5.3.2 #f80)
(padded_message.5.5.2 #f961)
(padded_message.5.8.0 #f1798)
(padded_message.3.12.0 #f81)
(padded_message.6.6.2 #f4)
(padded_message.6.10.0 #f46)
(padded_message.2.0.1 #f1638)
(padded_message.4.1.2 #f567)
(padded_message.4.3.2 #f520)
(padded_message.0.5.2 #f67)
(padded_message.0.8.0 #f134)
(padded_message.1.4.2 #f464)
(padded_message.2.14.2 #f4)
(padded_message.4.4.0 #f853)
(padded_message.4.6.0 #f1027)
(padded_message.4.9.1 #f1184)
(padded_message.6.13.1 #f1262)
(padded_message.7.0.2 #f24)
(padded_message.3.9.2 #f290)
(padded_message.5.9.1 #f675)
(padded_message.7.6.1 #f0)
(padded_message.7.7.0 #f0)
(padded_message.7.8.1 #f0)
(padded_message.7.10.1 #f0)
(padded_message.7.12.0 #f0)
(padded_message.7.14.1 #f0)
(padded_message.7.15.2 #f0)
(padded_message.1.8.1 #f544)
(padded_message.7.2.0 #f0)
(padded_message.2.1.1 #f422)
(padded_message.4.5.0 #f257)
(padded_message.3.15.0 #f504)
(padded_message.0.0.2 #f194)
(padded_message.0.7.0 #f1545)
(padded_message.0.15.0 #f1539)
(padded_message.5.5.0 #f466)
(padded_message.7.11.2 #f0)
(padded_message.6.3.2 #f4)
(padded_message.3.12.2 #f889)
(padded_message.6.6.0 #f1287)
(padded_message.3.4.2 #f640)
(padded_message.5.6.1 #f1734)
(padded_message.0.5.0 #f902)
(padded_message.1.1.2 #f101)
(padded_message.1.4.0 #f869)
(padded_message.7.15.0 #f1568)
(padded_message.4.11.0 #f261)
(padded_message.4.2.1 #f387)
(padded_message.4.4.1 #f192)
(padded_message.5.12.0 #f1485)
(padded_message.0.6.1 #f932)
(padded_message.1.9.1 #f128)
(padded_message.7.3.1 #f0)
(padded_message.7.5.1 #f0)
(padded_message.7.13.2 #f0)
(padded_message.0.14.2 #f341)
(padded_message.4.15.2 #f7)
(padded_message.6.9.1 #f1509)
(expected_hash.6 #f186422342)
(padded_message.3.11.0 #f359)
(padded_message.5.0.0 #f29)
(padded_message.2.10.0 #f1901)
(padded_message.6.5.0 #f774)
(padded_message.6.7.0 #f1563)
(padded_message.4.13.0 #f1539)
(padded_message.2.4.2 #f204)
(padded_message.7.11.0 #f0)
(padded_message.4.10.2 #f192)
(padded_message.0.0.0 #f1316)
(padded_message.1.3.0 #f1395)
(padded_message.5.11.2 #f512)
(padded_message.7.14.2 #f0)
(padded_message.7.0.1 #f32)
(padded_message.1.11.1 #f104)
(padded_message.6.3.0 #f1118)
(padded_message.6.12.1 #f1517)
(padded_message.5.10.1 #f774)
(padded_message.3.1.2 #f264)
(padded_message.3.4.0 #f822)
(padded_message.3.6.0 #f1501)
(padded_message.3.13.0 #f1021)
(padded_message.4.14.0 #f769)
(padded_message.5.3.1 #f2039)
(padded_message.5.15.0 #f309)
(padded_message.4.1.1 #f98)
(padded_message.6.4.1 #f902)
(padded_message.4.12.2 #f20)
(padded_message.0.3.1 #f221)
(padded_message.1.2.1 #f1420)
(padded_message.0.11.2 #f280)
(padded_message.5.13.2 #f954)
(padded_message.7.10.2 #f0)
(padded_message.2.5.2 #f92)
(padded_message.2.8.0 #f1903)
(padded_message.7.12.1 #f0)
(padded_message.1.10.0 #f1107)
(padded_message.3.7.1 #f906)
(padded_message.7.13.0 #f0)
(padded_message.7.14.0 #f0)
(expected_hash.4 #f537200913)
(padded_message.6.0.0 #f106)
(expected_hash.3 #f203566965)
(padded_message.3.5.0 #f1593)
(padded_message.4.10.0 #f1544)
(padded_message.5.11.0 #f628)
(padded_message.7.9.2 #f0)
(padded_message.0.10.0 #f48)
(padded_message.2.9.1 #f1261)
(padded_message.4.6.2 #f1020)
(padded_message.0.15.1 #f1024)
(padded_message.1.1.1 #f237)
(padded_message.4.8.2 #f76)
(padded_message.6.1.1 #f261)
(padded_message.0.12.1 #f192)
(padded_message.7.10.0 #f0)
(padded_message.3.2.1 #f1291)
(padded_message.3.4.1 #f628)
(padded_message.5.13.0 #f1341)
(padded_message.6.14.0 #f816)
(padded_message.2.5.0 #f1328)
(padded_message.5.10.2 #f16)
(padded_message.5.7.2 #f567)
(padded_message.6.8.2 #f417)
(padded_message.7.2.2 #f0)
(padded_message.2.2.1 #f1766)
(padded_message.0.10.2 #f44)
(padded_message.2.4.1 #f1579)
(padded_message.0.7.2 #f192)
(padded_message.1.6.2 #f405)
(padded_message.4.5.2 #f116)
(padded_message.1.11.0 #f288)
(padded_message.4.8.0 #f853)
(padded_message.2.0.0 #f602)
(padded_message.5.10.0 #f22)
(padded_message.6.12.0 #f1895)
(padded_message.2.11.0 #f19)
(padded_message.3.1.1 #f0)
(padded_message.6.15.2 #f196)
(padded_message.7.9.0 #f0)
(padded_message.5.14.2 #f627)
(padded_message.2.13.0 #f1282)
(padded_message.1.13.0 #f1330)
(padded_message.0.14.1 #f614)
(padded_message.4.7.0 #f48)
(padded_message.1.10.1 #f234)
(padded_message.2.3.1 #f1798)
(padded_message.0.2.2 #f8)
(padded_message.0.9.0 #f257)
(padded_message.4.0.2 #f534)
(padded_message.2.10.2 #f185)
(padded_message.5.0.2 #f192)
(padded_message.5.7.0 #f72)
(padded_message.6.5.2 #f24)
(padded_message.6.8.0 #f1136)
(padded_message.1.14.1 #f1542)
(padded_message.3.6.2 #f201)
(padded_message.3.8.2 #f759)
(padded_message.0.13.0 #f770)
(padded_message.1.3.2 #f337)
(padded_message.1.6.0 #f76)
(padded_message.2.12.1 #f229)
(padded_message.1.11.2 #f129)
(padded_message.4.6.1 #f128)
(padded_message.2.14.0 #f42)
(padded_message.5.8.1 #f1539)
(padded_message.0.8.1 #f201)
(padded_message.2.13.2 #f291)
(padded_message.6.12.2 #f413)
(padded_message.6.15.0 #f43)
(padded_message.7.1.2 #f512)
(padded_message.7.4.0 #f0)
(padded_message.7.7.1 #f0)
(padded_message.5.2.0 #f1540)
(padded_message.6.0.2 #f116)
(padded_message.6.2.2 #f4)
(padded_message.1.13.2 #f120)
(padded_message.2.6.2 #f76)
(padded_message.2.8.2 #f168)
(padded_message.4.0.0 #f887)
(padded_message.0.2.0 #f256)
(padded_message.0.4.0 #f776)
(padded_message.1.5.0 #f355)
(padded_message.1.7.0 #f275)
(padded_message.3.15.2 #f691)
(padded_message.4.5.1 #f480)
(padded_message.6.9.0 #f1903)
(padded_message.6.11.0 #f302)
(padded_message.7.1.0 #f0)
(padded_message.3.3.2 #f209)
(padded_message.3.5.2 #f859)
(padded_message.1.15.2 #f220)
(padded_message.0.13.2 #f16)
(padded_message.3.8.0 #f1905)
(padded_message.5.5.1 #f1696)
(padded_message.0.10.1 #f160)
(padded_message.4.3.1 #f387)
(padded_message.6.6.1 #f160)
(padded_message.1.12.0 #f816)
(padded_message.0.5.1 #f1977)
(padded_message.1.4.1 #f1034)
(padded_message.6.13.0 #f1139)
(padded_message.3.12.1 #f1173)
(padded_message.3.14.0 #f1764)
(padded_message.2.7.2 #f16)
(padded_message.2.11.1 #f806)
(padded_message.4.1.0 #f1443)
(padded_message.6.10.1 #f1646)
(padded_message.3.9.1 #f1443)
(padded_message.3.11.2 #f198)
(padded_message.7.2.1 #f0)
(padded_message.6.2.0 #f1287)
(padded_message.6.14.1 #f1126)
(padded_message.2.15.1 #f281)
(padded_message.3.7.0 #f1559)
) true;ignored
))

131
examples/ZoKratesCurly/pf/hash/sha256lookup/utils.zok Normal file
View File

@@ -0,0 +1,131 @@
```rust
use "assert_well_formed"::fits_in_bits_sparse;
use "EMBED"::{unpack, reverse_lookup};
use "const_range_check"::{D_TO_S_10, D_TO_S_11};
struct Dual {
s: field,
d: field,
}
fn ceildiv(x: u32, y: u32) -> u32 {
(x + y - 1) / y
}
fn reverse_limbs<const N: usize>(input: [field; N]) -> [field; N] {
let mut output = [0; N];
for i in 0..N {
output[i] = input[N - 1 - i];
}
output
}
fn combine_limbs<const N: usize>(input: [field; N], limbw: [u32; N]) -> field {
let mut output = 0;
let mut cur_width = 0;
for (limb, &width) in input.iter().zip(limbw.iter()) {
output += limb * (2 ** cur_width);
cur_width += width;
}
output
}
fn combine_sparse_limbs<const N: usize>(input: [field; N], limbw: [u32; N]) -> field {
let sparse_limbw: [u32; N] = array::from_fn(|i| 2 * limbw[i]);
combine_limbs(input, sparse_limbw)
}
fn unsafe_split<const LOW_BITS: u32, const HIGH_BITS: u32>(x: field) -> [field; 2] {
let total_bits = LOW_BITS + HIGH_BITS;
let bits = unpack(x);
let (mut low, mut high) = (0, 0);
for i in 0..LOW_BITS {
low += (2 ** i) * bits[total_bits - 1 - i] as field;
}
for i in LOW_BITS..total_bits {
high += (2 ** (i - LOW_BITS)) * bits[total_bits - 1 - i] as field;
}
[low, high]
}
fn unsafe_split_dyn<const N: usize>(x: field, limbw: [u32; N]) -> [field; N] {
let total_width = limbw.iter().sum::<u32>();
let bits = unpack(x);
let mut output = [0; N];
let mut idx = total_width - 1;
for (out_limb, &width) in output.iter_mut().zip(limbw.iter()) {
for j in 0..width {
*out_limb += 2 ** j * bits[idx] as field;
idx -= 1;
}
}
output
}
fn unsafe_split_dyn_sparse<const N: usize>(x: field, limbw: [u32; N]) -> [field; N] {
let sparse_limbw: [u32; N] = array::from_fn(|i| 2 * limbw[i]);
unsafe_split_dyn(x, sparse_limbw)
}
fn unsafe_separate_sparse<const N: u32>(x: field) -> [field; 2] {
let bits = unpack(x);
let (mut even, mut odd) = (0, 0);
for i in 0..N {
even += 4 ** i * bits[2 * N - 1 - 2 * i] as field;
odd += 4 ** i * bits[2 * N - 2 * i] as field;
}
[even, odd]
}
fn split_limbs_in_sparse<const N: usize>(input: field, limbw: [u32; N]) -> [field; N] {
let output_limbs = unsafe_split_dyn_sparse(input, limbw);
let mut safe_output_limbs = [0; N];
safe_output_limbs[0..].copy_from_slice(&output_limbs[1..]);
let nm1 = N - 1;
safe_output_limbs[0] = input - combine_sparse_limbs(safe_output_limbs[1..].try_into().unwrap(), limbw[1..].try_into().unwrap()) * (2 ** (2 * limbw[0]));
for (limb, &width) in output_limbs.iter().zip(limbw.iter()) {
assert!(fits_in_bits_sparse(*limb, width));
}
output_limbs
}
fn split_even_dual_10(x: field) -> Dual {
let split = split_both_sparse_inner::<10>(x);
let (even, even_d) = (split[0], reverse_lookup(D_TO_S_10, split[0]));
assert!(fits_in_bits_sparse(split[1], 10));
Dual { s: even, d: even_d }
}
fn split_odd_dual_10(x: field) -> Dual {
let split = split_both_sparse_inner::<10>(x);
let (odd, odd_d) = (split[1], reverse_lookup(D_TO_S_10, split[1]));
assert!(fits_in_bits_sparse(split[0], 10));
Dual { s: odd, d: odd_d }
}
fn split_even_dual_11(x: field) -> Dual {
let split = split_both_sparse_inner::<11>(x);
let (even, even_d) = (split[0], reverse_lookup(D_TO_S_11, split[0]));
assert!(fits_in_bits_sparse(split[1], 11));
Dual { s: even, d: even_d }
}
fn dense_to_dual<const W: u32>(x: field) -> Dual {
let s = match W {
10 => reverse_lookup(D_TO_S_10, x),
11 => reverse_lookup(D_TO_S_11, x),
_ => panic!(),
};
Dual { s, d: x }
}
fn dense_limbs_to_dual_limbs<const N: usize, const NL: usize>(input: [[field; NL]; N], limbw: [u32; NL]) -> [[Dual; NL]; N] {
let mut output = array::from_fn(|_| array::from_fn(|_| Dual { s: 0, d: 0 }));
for (i, each) in input.iter().enumerate() {
output[i] = dense_limb_to_dual_limb(each, limbw);
}
output
}
```

8
examples/ZoKratesCurly/pf/isolate_assert.zok Normal file
View File

@@ -0,0 +1,8 @@
def mult(field x, field y) -> field {
assert(x != y);
return x * y;
}
def main(private field x, private field y) -> field {
return if x == y { x * x } else { mult(x, y) };
}

10
examples/ZoKratesCurly/pf/isolate_assert.zok.pin Normal file
View File

@@ -0,0 +1,10 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(x #f4)
(y #f4)
) true ;ignored
)
)

9
examples/ZoKratesCurly/pf/isolate_assert.zok.vin Normal file
View File

@@ -0,0 +1,9 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(return #f16)
) true ;ignored
)
)

3
examples/ZoKratesCurly/pf/maj.zok Normal file
View File

@@ -0,0 +1,3 @@
def main(u8 a, u8 b, u8 c) -> u8 {
return (a & b) ^ (a & c) ^ (b & c);
}

7
examples/ZoKratesCurly/pf/maj.zok.pin Normal file
View File

@@ -0,0 +1,7 @@
(let (
(a #xFD)
(b #xC9)
(c #xD0)
)
false
)

Some files were not shown because too many files have changed in this diff Show More