mirror of
https://github.com/circify/circ.git
synced 2026-01-10 06:08:02 -05:00
field flexibility ; add limit for linearity reduction (#66)
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
This commit is contained in:
Riad S. Wahby
1
.gitignore
vendored
1
.gitignore
vendored
@@ -8,6 +8,7 @@ __pycache__
|
||||
/pi
|
||||
/x
|
||||
/perf.data*
|
||||
/heaptrack.*
|
||||
/.gdb_history
|
||||
.features.txt
|
||||
scripts/aby_tests/tests
|
||||
|
||||
112
Cargo.lock
generated
112
Cargo.lock
generated
@@ -2,6 +2,17 @@
|
||||
# It is not intended for manual editing.
|
||||
version = 3
|
||||
|
||||
[[package]]
|
||||
name = "addchain"
|
||||
version = "0.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3b2e69442aa5628ea6951fa33e24efe8313f4321a91bd729fc2f75bdfc858570"
|
||||
dependencies = [
|
||||
"num-bigint",
|
||||
"num-integer",
|
||||
"num-traits",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "addr2line"
|
||||
version = "0.16.0"
|
||||
@@ -226,6 +237,7 @@ dependencies = [
|
||||
"approx",
|
||||
"bellman",
|
||||
"bls12_381",
|
||||
"circ_fields",
|
||||
"env_logger",
|
||||
"ff",
|
||||
"from-pest",
|
||||
@@ -240,6 +252,7 @@ dependencies = [
|
||||
"log",
|
||||
"logos",
|
||||
"lp-solvers",
|
||||
"paste",
|
||||
"pest",
|
||||
"pest-ast",
|
||||
"pest_derive",
|
||||
@@ -257,6 +270,21 @@ dependencies = [
|
||||
"zokrates_pest_ast",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "circ_fields"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"ff",
|
||||
"ff-derive-num",
|
||||
"ff_derive 0.11.0 (git+https://github.com/kwantam/ff.git?rev=b3041c177b9ae28095c9ce8347600212252abc83)",
|
||||
"lazy_static",
|
||||
"num-traits",
|
||||
"paste",
|
||||
"rand",
|
||||
"rug",
|
||||
"serde",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "clap"
|
||||
version = "2.33.3"
|
||||
@@ -411,10 +439,53 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "b2958d04124b9f27f175eaeb9a9f383d026098aa837eadd8ba22c11f13a05b9e"
|
||||
dependencies = [
|
||||
"bitvec",
|
||||
"byteorder",
|
||||
"ff_derive 0.11.0 (registry+https://github.com/rust-lang/crates.io-index)",
|
||||
"rand_core",
|
||||
"subtle",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ff-derive-num"
|
||||
version = "0.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e715451ab983be06481e927a275ec12372103ad426c7cb82cebfe14698ed4cf4"
|
||||
dependencies = [
|
||||
"num-traits",
|
||||
"proc-macro2 1.0.30",
|
||||
"quote 1.0.10",
|
||||
"syn 1.0.80",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ff_derive"
|
||||
version = "0.11.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a923972863adcef93ac7092c9bf6543a26e922c1bd6c925518156411e05bf85c"
|
||||
dependencies = [
|
||||
"addchain",
|
||||
"num-bigint",
|
||||
"num-integer",
|
||||
"num-traits",
|
||||
"proc-macro2 1.0.30",
|
||||
"quote 1.0.10",
|
||||
"syn 1.0.80",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ff_derive"
|
||||
version = "0.11.0"
|
||||
source = "git+https://github.com/kwantam/ff.git?rev=b3041c177b9ae28095c9ce8347600212252abc83#b3041c177b9ae28095c9ce8347600212252abc83"
|
||||
dependencies = [
|
||||
"addchain",
|
||||
"num-bigint",
|
||||
"num-integer",
|
||||
"num-traits",
|
||||
"proc-macro2 1.0.30",
|
||||
"quote 1.0.10",
|
||||
"syn 1.0.80",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "fixedbitset"
|
||||
version = "0.4.0"
|
||||
@@ -694,6 +765,27 @@ dependencies = [
|
||||
"autocfg",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "num-bigint"
|
||||
version = "0.3.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5f6f7833f2cbf2360a6cfd58cd41a53aa7a90bd4c202f5b1c7dd2ed73c57b2c3"
|
||||
dependencies = [
|
||||
"autocfg",
|
||||
"num-integer",
|
||||
"num-traits",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "num-integer"
|
||||
version = "0.1.44"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d2cc698a63b549a70bc047073d2949cce27cd1c7b0a4a862d08a8031bc2801db"
|
||||
dependencies = [
|
||||
"autocfg",
|
||||
"num-traits",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "num-traits"
|
||||
version = "0.2.14"
|
||||
@@ -743,6 +835,12 @@ dependencies = [
|
||||
"group",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "paste"
|
||||
version = "1.0.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0744126afe1a6dd7f394cb50a716dbe086cb06e255e53d8d0185d82828358fb5"
|
||||
|
||||
[[package]]
|
||||
name = "pest"
|
||||
version = "2.1.3"
|
||||
@@ -1046,6 +1144,20 @@ name = "serde"
|
||||
version = "1.0.130"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "f12d06de37cf59146fbdecab66aa99f9fe4f78722e3607577a5375d66bd0c913"
|
||||
dependencies = [
|
||||
"serde_derive",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "serde_derive"
|
||||
version = "1.0.130"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d7bc1a1ab1961464eae040d96713baa5a724a8152c1222492465b54322ec508b"
|
||||
dependencies = [
|
||||
"proc-macro2 1.0.30",
|
||||
"quote 1.0.10",
|
||||
"syn 1.0.80",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "serde_json"
|
||||
|
||||
@@ -7,6 +7,7 @@ edition = "2018"
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
||||
circ_fields = { path = "circ_fields" }
|
||||
#hashconsing = "1.3"
|
||||
hashconsing = { git = "https://github.com/alex-ozdemir/hashconsing.git", branch = "phash"}
|
||||
rug = "1.11"
|
||||
@@ -35,6 +36,7 @@ pest-ast = "0.3"
|
||||
from-pest = "0.3"
|
||||
itertools = "0.10"
|
||||
petgraph = "0.6"
|
||||
paste = "1.0"
|
||||
|
||||
[dev-dependencies]
|
||||
quickcheck = "1"
|
||||
@@ -47,11 +49,12 @@ approx = "0.5.0"
|
||||
[features]
|
||||
default = ["bls12381"]
|
||||
bls12381 = []
|
||||
ff_dfl = []
|
||||
c = ["lang-c"]
|
||||
lp = ["good_lp", "lp-solvers"]
|
||||
r1cs = ["bellman"]
|
||||
smt = ["rsmt2"]
|
||||
zok = ["zokrates_parser", "zokrates_pest_ast", ]
|
||||
zok = ["zokrates_parser", "zokrates_pest_ast"]
|
||||
|
||||
[[example]]
|
||||
name = "circ"
|
||||
|
||||
13
circ_fields/.gitignore
vendored
Normal file
13
circ_fields/.gitignore
vendored
Normal file
@@ -0,0 +1,13 @@
|
||||
/target
|
||||
/pf
|
||||
/assignment.txt
|
||||
/params
|
||||
__pycache__
|
||||
/P
|
||||
/V
|
||||
/pi
|
||||
/x
|
||||
/perf.data*
|
||||
/.gdb_history
|
||||
.features.txt
|
||||
scripts/aby_tests/tests
|
||||
351
circ_fields/Cargo.lock
generated
Normal file
351
circ_fields/Cargo.lock
generated
Normal file
@@ -0,0 +1,351 @@
|
||||
# This file is automatically @generated by Cargo.
|
||||
# It is not intended for manual editing.
|
||||
version = 3
|
||||
|
||||
[[package]]
|
||||
name = "addchain"
|
||||
version = "0.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3b2e69442aa5628ea6951fa33e24efe8313f4321a91bd729fc2f75bdfc858570"
|
||||
dependencies = [
|
||||
"num-bigint",
|
||||
"num-integer",
|
||||
"num-traits",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "autocfg"
|
||||
version = "1.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"
|
||||
|
||||
[[package]]
|
||||
name = "az"
|
||||
version = "1.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "f771a5d1f5503f7f4279a30f3643d3421ba149848b89ecaaec0ea2acf04a5ac4"
|
||||
|
||||
[[package]]
|
||||
name = "bitvec"
|
||||
version = "0.22.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5237f00a8c86130a0cc317830e558b966dd7850d48a953d998c813f01a41b527"
|
||||
dependencies = [
|
||||
"funty",
|
||||
"radium",
|
||||
"tap",
|
||||
"wyz",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "byteorder"
|
||||
version = "1.4.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "14c189c53d098945499cdfa7ecc63567cf3886b3332b312a5b4585d8d3a6a610"
|
||||
|
||||
[[package]]
|
||||
name = "cfg-if"
|
||||
version = "1.0.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
|
||||
|
||||
[[package]]
|
||||
name = "circ_fields"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"ff",
|
||||
"ff-derive-num",
|
||||
"ff_derive 0.11.0 (git+https://github.com/kwantam/ff.git?rev=b3041c177b9ae28095c9ce8347600212252abc83)",
|
||||
"lazy_static",
|
||||
"num-traits",
|
||||
"paste",
|
||||
"rand",
|
||||
"rug",
|
||||
"serde",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ff"
|
||||
version = "0.11.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "b2958d04124b9f27f175eaeb9a9f383d026098aa837eadd8ba22c11f13a05b9e"
|
||||
dependencies = [
|
||||
"bitvec",
|
||||
"byteorder",
|
||||
"ff_derive 0.11.0 (registry+https://github.com/rust-lang/crates.io-index)",
|
||||
"rand_core",
|
||||
"subtle",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ff-derive-num"
|
||||
version = "0.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e715451ab983be06481e927a275ec12372103ad426c7cb82cebfe14698ed4cf4"
|
||||
dependencies = [
|
||||
"num-traits",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ff_derive"
|
||||
version = "0.11.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a923972863adcef93ac7092c9bf6543a26e922c1bd6c925518156411e05bf85c"
|
||||
dependencies = [
|
||||
"addchain",
|
||||
"num-bigint",
|
||||
"num-integer",
|
||||
"num-traits",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ff_derive"
|
||||
version = "0.11.0"
|
||||
source = "git+https://github.com/kwantam/ff.git?rev=b3041c177b9ae28095c9ce8347600212252abc83#b3041c177b9ae28095c9ce8347600212252abc83"
|
||||
dependencies = [
|
||||
"addchain",
|
||||
"num-bigint",
|
||||
"num-integer",
|
||||
"num-traits",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "funty"
|
||||
version = "1.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "1847abb9cb65d566acd5942e94aea9c8f547ad02c98e1649326fc0e8910b8b1e"
|
||||
|
||||
[[package]]
|
||||
name = "getrandom"
|
||||
version = "0.2.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d39cd93900197114fa1fcb7ae84ca742095eed9442088988ae74fa744e930e77"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"libc",
|
||||
"wasi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "gmp-mpfr-sys"
|
||||
version = "1.4.7"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a146a7357ce9573bdcc416fc4a99b960e166e72d8eaffa7c59966d51866b5bfb"
|
||||
dependencies = [
|
||||
"libc",
|
||||
"winapi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "lazy_static"
|
||||
version = "1.4.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
|
||||
|
||||
[[package]]
|
||||
name = "libc"
|
||||
version = "0.2.119"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "1bf2e165bb3457c8e098ea76f3e3bc9db55f87aa90d52d0e6be741470916aaa4"
|
||||
|
||||
[[package]]
|
||||
name = "num-bigint"
|
||||
version = "0.3.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5f6f7833f2cbf2360a6cfd58cd41a53aa7a90bd4c202f5b1c7dd2ed73c57b2c3"
|
||||
dependencies = [
|
||||
"autocfg",
|
||||
"num-integer",
|
||||
"num-traits",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "num-integer"
|
||||
version = "0.1.44"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d2cc698a63b549a70bc047073d2949cce27cd1c7b0a4a862d08a8031bc2801db"
|
||||
dependencies = [
|
||||
"autocfg",
|
||||
"num-traits",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "num-traits"
|
||||
version = "0.2.14"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9a64b1ec5cda2586e284722486d802acf1f7dbdc623e2bfc57e65ca1cd099290"
|
||||
dependencies = [
|
||||
"autocfg",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "paste"
|
||||
version = "1.0.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0744126afe1a6dd7f394cb50a716dbe086cb06e255e53d8d0185d82828358fb5"
|
||||
|
||||
[[package]]
|
||||
name = "ppv-lite86"
|
||||
version = "0.2.16"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "eb9f9e6e233e5c4a35559a617bf40a4ec447db2e84c20b55a6f83167b7e57872"
|
||||
|
||||
[[package]]
|
||||
name = "proc-macro2"
|
||||
version = "1.0.36"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "c7342d5883fbccae1cc37a2353b09c87c9b0f3afd73f5fb9bba687a1f733b029"
|
||||
dependencies = [
|
||||
"unicode-xid",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "quote"
|
||||
version = "1.0.15"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "864d3e96a899863136fc6e99f3d7cae289dafe43bf2c5ac19b70df7210c0a145"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "radium"
|
||||
version = "0.6.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "643f8f41a8ebc4c5dc4515c82bb8abd397b527fc20fd681b7c011c2aee5d44fb"
|
||||
|
||||
[[package]]
|
||||
name = "rand"
|
||||
version = "0.8.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404"
|
||||
dependencies = [
|
||||
"libc",
|
||||
"rand_chacha",
|
||||
"rand_core",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rand_chacha"
|
||||
version = "0.3.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88"
|
||||
dependencies = [
|
||||
"ppv-lite86",
|
||||
"rand_core",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rand_core"
|
||||
version = "0.6.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d34f1408f55294453790c48b2f1ebbb1c5b4b7563eb1f418bcfcfdbb06ebb4e7"
|
||||
dependencies = [
|
||||
"getrandom",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rug"
|
||||
version = "1.15.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6ac804305677221f4c82469fd7eb8bfe00dd01420aa191197cb87d738520feef"
|
||||
dependencies = [
|
||||
"az",
|
||||
"gmp-mpfr-sys",
|
||||
"libc",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "serde"
|
||||
version = "1.0.136"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ce31e24b01e1e524df96f1c2fdd054405f8d7376249a5110886fb4b658484789"
|
||||
dependencies = [
|
||||
"serde_derive",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "serde_derive"
|
||||
version = "1.0.136"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "08597e7152fcd306f41838ed3e37be9eaeed2b61c42e2117266a554fab4662f9"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "subtle"
|
||||
version = "2.4.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6bdef32e8150c2a081110b42772ffe7d7c9032b606bc226c8260fd97e0976601"
|
||||
|
||||
[[package]]
|
||||
name = "syn"
|
||||
version = "1.0.86"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "8a65b3f4ffa0092e9887669db0eae07941f023991ab58ea44da8fe8e2d511c6b"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"unicode-xid",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "tap"
|
||||
version = "1.0.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "55937e1799185b12863d447f42597ed69d9928686b8d88a1df17376a097d8369"
|
||||
|
||||
[[package]]
|
||||
name = "unicode-xid"
|
||||
version = "0.2.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "8ccb82d61f80a663efe1f787a51b16b5a51e3314d6ac365b08639f52387b33f3"
|
||||
|
||||
[[package]]
|
||||
name = "wasi"
|
||||
version = "0.10.2+wasi-snapshot-preview1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "fd6fbd9a79829dd1ad0cc20627bf1ed606756a7f77edff7b66b7064f9cb327c6"
|
||||
|
||||
[[package]]
|
||||
name = "winapi"
|
||||
version = "0.3.9"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419"
|
||||
dependencies = [
|
||||
"winapi-i686-pc-windows-gnu",
|
||||
"winapi-x86_64-pc-windows-gnu",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "winapi-i686-pc-windows-gnu"
|
||||
version = "0.4.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
|
||||
|
||||
[[package]]
|
||||
name = "winapi-x86_64-pc-windows-gnu"
|
||||
version = "0.4.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
|
||||
|
||||
[[package]]
|
||||
name = "wyz"
|
||||
version = "0.4.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "129e027ad65ce1453680623c3fb5163cbf7107bfe1aa32257e7d0e63f9ced188"
|
||||
dependencies = [
|
||||
"tap",
|
||||
]
|
||||
19
circ_fields/Cargo.toml
Normal file
19
circ_fields/Cargo.toml
Normal file
@@ -0,0 +1,19 @@
|
||||
[package]
|
||||
name = "circ_fields"
|
||||
version = "0.1.0"
|
||||
authors = ["kwantam <kwantam@gmail.com>"]
|
||||
edition = "2021"
|
||||
|
||||
[dependencies]
|
||||
ff = { version = "0.11", features = ["derive"] }
|
||||
ff_derive = { git = "https://github.com/kwantam/ff.git", rev = "b3041c177b9ae28095c9ce8347600212252abc83" }
|
||||
ff-derive-num = "0.2"
|
||||
lazy_static = "1.4"
|
||||
num-traits = "0.2"
|
||||
paste = "1.0"
|
||||
rand = "0.8"
|
||||
rug = "1.11"
|
||||
serde = { version = "1.0", features = ["derive"] }
|
||||
|
||||
[dev-dependencies]
|
||||
rand = "0.8"
|
||||
116
circ_fields/src/ff_field.rs
Normal file
116
circ_fields/src/ff_field.rs
Normal file
@@ -0,0 +1,116 @@
|
||||
//! ff-based fields for use in CirC
|
||||
|
||||
use paste::paste;
|
||||
|
||||
macro_rules! def_field {
|
||||
($name: ident, $mod: literal, $gen: literal, $limbs: literal) => {
|
||||
paste! { pub use $name::Ft as [<$name:camel>]; }
|
||||
paste! { pub use $name::FMOD as [<$name:upper _FMOD>]; }
|
||||
paste! { pub use $name::FMOD_ARC as [<$name:upper _FMOD_ARC>]; }
|
||||
pub mod $name {
|
||||
#![allow(warnings, clippy::derive_hash_xor_eq)]
|
||||
use ff_derive::PrimeField;
|
||||
use ff_derive_num::Num;
|
||||
use serde::{Deserialize, Serialize};
|
||||
#[derive(PrimeField, Num, Deserialize, Serialize, Hash)]
|
||||
#[PrimeFieldModulus = $mod]
|
||||
#[PrimeFieldGenerator = $gen]
|
||||
#[PrimeFieldReprEndianness = "little"]
|
||||
/// Field definition
|
||||
pub struct Ft([u64; $limbs]);
|
||||
|
||||
use lazy_static::lazy_static;
|
||||
use rug::Integer;
|
||||
use std::sync::Arc;
|
||||
lazy_static! {
|
||||
/// Field modulus
|
||||
pub static ref FMOD: Integer = Integer::from_str_radix($mod, 10).unwrap();
|
||||
pub static ref FMOD_ARC: Arc<Integer> = Arc::new(FMOD.clone());
|
||||
}
|
||||
|
||||
use rug::integer::Order;
|
||||
impl std::convert::From<&Ft> for Integer {
|
||||
fn from(f: &Ft) -> Self {
|
||||
use ff::PrimeField;
|
||||
Self::from_digits(f.to_repr().as_ref(), Order::Lsf)
|
||||
}
|
||||
}
|
||||
|
||||
impl std::convert::TryFrom<&Integer> for Ft {
|
||||
type Error = &'static str;
|
||||
|
||||
fn try_from(i: &Integer) -> Result<Self, Self::Error> {
|
||||
use ff::PrimeField;
|
||||
let len = 8 * $limbs;
|
||||
if i.significant_digits::<u8>() > len {
|
||||
return Err("Tried to convert un-reduced Integer to Ft");
|
||||
}
|
||||
let mut bytes = [0u8; 8 * $limbs];
|
||||
i.write_digits(&mut bytes, Order::Lsf);
|
||||
Self::from_repr_vartime(FtRepr(bytes))
|
||||
.ok_or("Tried to convert un-reduced Integer to Ft")
|
||||
}
|
||||
}
|
||||
|
||||
impl std::convert::From<Integer> for Ft {
|
||||
#[track_caller]
|
||||
fn from(mut i: Integer) -> Self {
|
||||
use ff::PrimeField;
|
||||
use rug::ops::RemRoundingAssign;
|
||||
use std::cmp::Ordering::Less;
|
||||
|
||||
let len = 8 * $limbs;
|
||||
let mut bytes = [0u8; 8 * $limbs];
|
||||
if i.significant_digits::<u8>() > len || i.cmp0() == Less {
|
||||
i.rem_floor_assign(&*FMOD);
|
||||
}
|
||||
i.write_digits(&mut bytes, Order::Lsf);
|
||||
Self::from_repr_vartime(FtRepr(bytes)).unwrap()
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod test {
|
||||
use super::{Ft, FMOD};
|
||||
use ff::Field;
|
||||
use rand::thread_rng;
|
||||
use rug::Integer;
|
||||
|
||||
#[test]
|
||||
fn test_ff_roundtrip() {
|
||||
let mut rng = thread_rng();
|
||||
for _ in 0..1024 {
|
||||
let a0 = Ft::random(&mut rng);
|
||||
let a1 = Integer::from(&a0);
|
||||
let a2 = Ft::try_from(&a1).unwrap();
|
||||
assert_eq!(a0, a2);
|
||||
|
||||
let ainv0 = a0.invert().unwrap();
|
||||
let ainv1 = Integer::from(a1.invert_ref(&*FMOD).unwrap());
|
||||
let ainv2 = Ft::try_from(&ainv1).unwrap();
|
||||
assert_eq!(ainv0, ainv2);
|
||||
|
||||
let a3 = Ft::from(a1);
|
||||
assert_eq!(a0, a3);
|
||||
let ainv3 = Ft::from(ainv1);
|
||||
assert_eq!(ainv0, ainv3);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
def_field!(
|
||||
f_bls12381,
|
||||
"52435875175126190479447740508185965837690552500527637822603658699938581184513",
|
||||
"7",
|
||||
4
|
||||
);
|
||||
|
||||
def_field!(
|
||||
f_bn254,
|
||||
"21888242871839275222246405745257275088548364400416034343698204186575808495617",
|
||||
"5",
|
||||
4
|
||||
);
|
||||
165
circ_fields/src/int_field.rs
Normal file
165
circ_fields/src/int_field.rs
Normal file
@@ -0,0 +1,165 @@
|
||||
//! Integer-based fields for use in CirC
|
||||
// based on Alex's original FieldElem impl
|
||||
|
||||
use paste::paste;
|
||||
use rug::{
|
||||
ops::{RemRounding, RemRoundingAssign},
|
||||
Integer,
|
||||
};
|
||||
use std::fmt::{self, Display, Formatter};
|
||||
use std::ops::Deref;
|
||||
use std::sync::Arc;
|
||||
|
||||
#[derive(PartialEq, Eq, Clone, Debug, PartialOrd, Ord, Hash)]
|
||||
pub struct IntField {
|
||||
pub(crate) i: Integer,
|
||||
m: Arc<Integer>,
|
||||
}
|
||||
|
||||
impl Display for IntField {
|
||||
fn fmt(&self, f: &mut Formatter) -> fmt::Result {
|
||||
if self.i.significant_bits() + 1 < self.m.significant_bits() {
|
||||
write!(f, "#f{}m{}", self.i, self.m)
|
||||
} else {
|
||||
write!(f, "#f-{}m{}", self.m.deref().clone() - &self.i, self.m)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[allow(clippy::from_over_into)]
|
||||
impl Into<Integer> for IntField {
|
||||
fn into(self) -> Integer {
|
||||
self.i
|
||||
}
|
||||
}
|
||||
|
||||
#[allow(clippy::from_over_into)]
|
||||
impl Into<Integer> for &IntField {
|
||||
fn into(self) -> Integer {
|
||||
self.i.clone()
|
||||
}
|
||||
}
|
||||
|
||||
impl IntField {
|
||||
#[track_caller]
|
||||
#[inline]
|
||||
/// Check value in-range (debug only)
|
||||
pub fn check(&self, location: &str) {
|
||||
debug_assert!(
|
||||
self.i >= 0,
|
||||
"Negative field elem: {}\nat {}",
|
||||
self,
|
||||
location
|
||||
);
|
||||
debug_assert!(
|
||||
self.i < *self.m,
|
||||
"Field elem too big: {}\nat {}",
|
||||
self,
|
||||
location
|
||||
);
|
||||
}
|
||||
|
||||
/// Get a ref to the modulus
|
||||
pub fn modulus(&self) -> &Integer {
|
||||
&*self.m
|
||||
}
|
||||
|
||||
/// Get an Arc of the modulus
|
||||
pub fn modulus_arc(&self) -> Arc<Integer> {
|
||||
self.m.clone()
|
||||
}
|
||||
|
||||
/// Invert mod p
|
||||
pub fn recip(self) -> Self {
|
||||
let r = Self {
|
||||
i: self.i.invert(&*self.m).expect("no inverse!"),
|
||||
m: self.m,
|
||||
};
|
||||
r.check("recip");
|
||||
r
|
||||
}
|
||||
|
||||
/// Construct a new IntField
|
||||
pub fn new(mut i: Integer, m: Arc<Integer>) -> Self {
|
||||
if i < 0 || i > *m {
|
||||
i.rem_floor_assign(&*m);
|
||||
}
|
||||
Self { i, m }
|
||||
}
|
||||
|
||||
/// Check if this value is equal to zero
|
||||
pub fn is_zero(&self) -> bool {
|
||||
self.check("is_zero");
|
||||
self.i == 0
|
||||
}
|
||||
}
|
||||
|
||||
macro_rules! arith_impl {
|
||||
($Trait: ident, $fn: ident) => {
|
||||
impl $Trait for IntField {
|
||||
type Output = Self;
|
||||
fn $fn(self, other: Self) -> Self {
|
||||
assert_eq!(self.m, other.m);
|
||||
let r = Self {
|
||||
i: (self.i.$fn(other.i)).rem_floor(&*self.m),
|
||||
m: self.m,
|
||||
};
|
||||
r.check(std::stringify!($fn));
|
||||
r
|
||||
}
|
||||
}
|
||||
|
||||
impl $Trait<&IntField> for IntField {
|
||||
type Output = Self;
|
||||
fn $fn(self, other: &Self) -> Self {
|
||||
assert_eq!(self.m, other.m);
|
||||
let r = Self {
|
||||
i: (self.i.$fn(&other.i)).rem_floor(&*self.m),
|
||||
m: self.m,
|
||||
};
|
||||
r.check(std::stringify!($fn));
|
||||
r
|
||||
}
|
||||
}
|
||||
|
||||
impl $Trait<IntField> for &IntField {
|
||||
type Output = IntField;
|
||||
fn $fn(self, other: IntField) -> IntField {
|
||||
assert_eq!(self.m, other.m);
|
||||
let r = IntField {
|
||||
i: ((&self.i).$fn(other.i)).rem_floor(&*self.m),
|
||||
m: other.m,
|
||||
};
|
||||
r.check(std::stringify!($fn));
|
||||
r
|
||||
}
|
||||
}
|
||||
|
||||
paste! {
|
||||
impl [<$Trait Assign>]<&IntField> for IntField {
|
||||
fn [<$fn _assign>](&mut self, other: &IntField) {
|
||||
assert_eq!(self.m, other.m);
|
||||
self.i.[<$fn _assign>](&other.i);
|
||||
self.i.rem_floor_assign(&*self.m);
|
||||
}
|
||||
}
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
use std::ops::{Add, AddAssign, Mul, MulAssign, Neg, Sub, SubAssign};
|
||||
arith_impl!(Add, add);
|
||||
arith_impl!(Sub, sub);
|
||||
arith_impl!(Mul, mul);
|
||||
|
||||
impl Neg for IntField {
|
||||
type Output = Self;
|
||||
fn neg(self) -> Self {
|
||||
let r = Self {
|
||||
i: (-self.i).rem_floor(&*self.m),
|
||||
m: self.m,
|
||||
};
|
||||
r.check("neg");
|
||||
r
|
||||
}
|
||||
}
|
||||
381
circ_fields/src/lib.rs
Normal file
381
circ_fields/src/lib.rs
Normal file
@@ -0,0 +1,381 @@
|
||||
//! Fields for use in CirC
|
||||
|
||||
#![warn(missing_docs)]
|
||||
#![deny(warnings)]
|
||||
|
||||
mod ff_field;
|
||||
mod int_field;
|
||||
|
||||
/// Exports for moduli defined in this crate, as ARCs
|
||||
pub mod moduli {
|
||||
pub use super::ff_field::{F_BLS12381_FMOD_ARC, F_BN254_FMOD_ARC};
|
||||
}
|
||||
|
||||
use ff_field::{FBls12381, FBn254};
|
||||
use ff_field::{F_BLS12381_FMOD, F_BN254_FMOD};
|
||||
use ff_field::{F_BLS12381_FMOD_ARC, F_BN254_FMOD_ARC};
|
||||
use int_field::IntField;
|
||||
|
||||
use ff::Field;
|
||||
use paste::paste;
|
||||
use rug::Integer;
|
||||
use std::fmt::{self, Display, Formatter};
|
||||
use std::ops::{Add, AddAssign, Mul, MulAssign, Neg, Sub, SubAssign};
|
||||
use std::sync::Arc;
|
||||
|
||||
// TODO: rework this using macros?
|
||||
|
||||
/// Field element type
|
||||
#[derive(PartialEq, Eq, Clone, Debug, PartialOrd, Ord, Hash)]
|
||||
pub enum FieldT {
|
||||
/// BLS12-381 scalar field as `ff`
|
||||
FBls12381,
|
||||
/// BN-254 scalar field as `ff`
|
||||
FBn254,
|
||||
/// Generic field element based on `rug::Integer`
|
||||
IntField(Arc<Integer>),
|
||||
}
|
||||
|
||||
impl Display for FieldT {
|
||||
fn fmt(&self, f: &mut Formatter) -> fmt::Result {
|
||||
match self {
|
||||
Self::FBls12381 => write!(f, "FieldT::FBls12381"),
|
||||
Self::FBn254 => write!(f, "FieldT::FBn254"),
|
||||
Self::IntField(m) => write!(f, "FieldT::(mod {})", &*m),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl From<Arc<Integer>> for FieldT {
|
||||
fn from(m: Arc<Integer>) -> Self {
|
||||
Self::as_ff_opt(m.as_ref()).unwrap_or(Self::IntField(m))
|
||||
}
|
||||
}
|
||||
|
||||
impl From<Integer> for FieldT {
|
||||
fn from(m: Integer) -> Self {
|
||||
Self::as_ff_opt(&m).unwrap_or_else(|| Self::IntField(Arc::new(m)))
|
||||
}
|
||||
}
|
||||
|
||||
impl From<&Integer> for FieldT {
|
||||
fn from(m: &Integer) -> Self {
|
||||
Self::as_ff_opt(m).unwrap_or_else(|| Self::IntField(Arc::new(m.clone())))
|
||||
}
|
||||
}
|
||||
|
||||
impl FieldT {
|
||||
// Returns a FieldT if this modulus can be represented as `ff`, `None` otherwise.
|
||||
fn as_ff_opt(m: &Integer) -> Option<Self> {
|
||||
match m {
|
||||
m if m == &*F_BLS12381_FMOD => Some(Self::FBls12381),
|
||||
m if m == &*F_BN254_FMOD => Some(Self::FBn254),
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
|
||||
/// Field modulus
|
||||
#[inline]
|
||||
pub fn modulus(&self) -> &Integer {
|
||||
match self {
|
||||
Self::FBls12381 => &*F_BLS12381_FMOD,
|
||||
Self::FBn254 => &*F_BN254_FMOD,
|
||||
Self::IntField(m) => m.as_ref(),
|
||||
}
|
||||
}
|
||||
|
||||
/// Field modulus as an ARC
|
||||
#[inline]
|
||||
pub fn modulus_arc(&self) -> Arc<Integer> {
|
||||
match self {
|
||||
Self::FBls12381 => F_BLS12381_FMOD_ARC.clone(),
|
||||
Self::FBn254 => F_BN254_FMOD_ARC.clone(),
|
||||
Self::IntField(m) => m.clone(),
|
||||
}
|
||||
}
|
||||
|
||||
/// Default value for this type
|
||||
#[inline]
|
||||
pub fn default_value(&self) -> FieldV {
|
||||
match self {
|
||||
Self::FBls12381 => FieldV::FBls12381(Default::default()),
|
||||
Self::FBn254 => FieldV::FBn254(Default::default()),
|
||||
Self::IntField(m) => FieldV::IntField(IntField::new(Integer::from(0), m.clone())),
|
||||
}
|
||||
}
|
||||
|
||||
/// Zero for this type
|
||||
#[inline]
|
||||
pub fn zero(&self) -> FieldV {
|
||||
self.default_value()
|
||||
}
|
||||
|
||||
/// Random value of this type
|
||||
#[inline]
|
||||
pub fn random_v(&self, rng: impl rand::RngCore) -> FieldV {
|
||||
FieldV::random(self.clone(), rng)
|
||||
}
|
||||
|
||||
/// New value of this type
|
||||
#[inline]
|
||||
pub fn new_v<I>(&self, i: I) -> FieldV
|
||||
where
|
||||
Integer: From<I>,
|
||||
{
|
||||
FieldV::new_ty(i, self.clone())
|
||||
}
|
||||
}
|
||||
|
||||
/// Field element value
|
||||
#[derive(PartialEq, Eq, Clone, Debug, PartialOrd, Ord, Hash)]
|
||||
pub enum FieldV {
|
||||
/// BLS12-381 scalar field element as `ff`
|
||||
FBls12381(FBls12381),
|
||||
/// BN-254 scalar field element as `ff`
|
||||
FBn254(FBn254),
|
||||
/// Generic field element based on `rug::Integer`
|
||||
IntField(IntField),
|
||||
}
|
||||
|
||||
impl FieldV {
|
||||
/// Type of this value
|
||||
#[inline]
|
||||
pub fn ty(&self) -> FieldT {
|
||||
match self {
|
||||
Self::FBls12381(_) => FieldT::FBls12381,
|
||||
Self::FBn254(_) => FieldT::FBn254,
|
||||
Self::IntField(i) => FieldT::IntField(i.modulus_arc()),
|
||||
}
|
||||
}
|
||||
|
||||
/// New field element from value and modulus.
|
||||
///
|
||||
/// This function uses `FieldT::from`, which means that if there is
|
||||
/// an `ff` implementation available it will return that, otherwise
|
||||
/// it will use a `rug::Integer` implementation.
|
||||
#[inline]
|
||||
pub fn new<I>(i: I, m: Arc<Integer>) -> Self
|
||||
where
|
||||
Integer: From<I>,
|
||||
{
|
||||
Self::new_ty(i, FieldT::from(m))
|
||||
}
|
||||
|
||||
/// Check that a value is well formed
|
||||
#[track_caller]
|
||||
#[inline]
|
||||
pub fn check(&self, loc: &str) {
|
||||
if let Self::IntField(m) = self {
|
||||
m.check(loc);
|
||||
}
|
||||
}
|
||||
|
||||
/// Field modulus as `&rug::Integer`
|
||||
#[inline]
|
||||
pub fn modulus(&self) -> &Integer {
|
||||
match self {
|
||||
Self::FBls12381(_) => &*F_BLS12381_FMOD,
|
||||
Self::FBn254(_) => &*F_BN254_FMOD,
|
||||
Self::IntField(i) => i.modulus(),
|
||||
}
|
||||
}
|
||||
|
||||
/// Compute the multiplicative inverse (panics on 0)
|
||||
#[track_caller]
|
||||
#[inline]
|
||||
pub fn recip_ref(&self) -> Self {
|
||||
match self {
|
||||
Self::FBls12381(pf) => Self::FBls12381(pf.invert().unwrap()),
|
||||
Self::FBn254(pf) => Self::FBn254(pf.invert().unwrap()),
|
||||
Self::IntField(i) => Self::IntField(i.clone().recip()),
|
||||
}
|
||||
}
|
||||
|
||||
/// Ccompute the multiplicative inverse (panics on 0)
|
||||
#[track_caller]
|
||||
#[inline]
|
||||
pub fn recip(self) -> Self {
|
||||
match self {
|
||||
Self::FBls12381(pf) => Self::FBls12381(pf.invert().unwrap()),
|
||||
Self::FBn254(pf) => Self::FBn254(pf.invert().unwrap()),
|
||||
Self::IntField(i) => Self::IntField(i.recip()),
|
||||
}
|
||||
}
|
||||
|
||||
/// Get value as an integer
|
||||
#[inline]
|
||||
pub fn i(&self) -> Integer {
|
||||
self.into()
|
||||
}
|
||||
|
||||
/// Test if value is zero
|
||||
#[inline]
|
||||
pub fn is_zero(&self) -> bool {
|
||||
match self {
|
||||
Self::FBls12381(pf) => bool::from(pf.is_zero()),
|
||||
Self::FBn254(pf) => bool::from(pf.is_zero()),
|
||||
Self::IntField(i) => i.is_zero(),
|
||||
}
|
||||
}
|
||||
|
||||
/// Test if value is 1
|
||||
#[inline]
|
||||
pub fn is_one(&self) -> bool {
|
||||
use num_traits::One;
|
||||
match self {
|
||||
Self::FBls12381(pf) => pf.is_one(),
|
||||
Self::FBn254(pf) => pf.is_one(),
|
||||
Self::IntField(i) => i.i == 1,
|
||||
}
|
||||
}
|
||||
|
||||
#[inline]
|
||||
fn new_ty<I>(i: I, ty: FieldT) -> Self
|
||||
where
|
||||
Integer: From<I>,
|
||||
{
|
||||
let i = Integer::from(i);
|
||||
match ty {
|
||||
FieldT::FBls12381 => Self::FBls12381(FBls12381::from(i)),
|
||||
FieldT::FBn254 => Self::FBn254(FBn254::from(i)),
|
||||
FieldT::IntField(m) => Self::IntField(IntField::new(i, m)),
|
||||
}
|
||||
}
|
||||
|
||||
fn random(ty: FieldT, mut rng: impl rand::RngCore) -> Self {
|
||||
match ty {
|
||||
FieldT::FBls12381 => Self::FBls12381(FBls12381::random(rng)),
|
||||
FieldT::FBn254 => Self::FBn254(FBn254::random(rng)),
|
||||
FieldT::IntField(m) => {
|
||||
let mut rug_rng = rug::rand::RandState::new_mersenne_twister();
|
||||
rug_rng.seed(&Integer::from(rng.next_u64()));
|
||||
let i = Integer::from(m.random_below_ref(&mut rug_rng));
|
||||
Self::IntField(IntField::new(i, m))
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Convert to a different FieldT --- will fail if moduli are not the same!
|
||||
#[track_caller]
|
||||
#[inline]
|
||||
pub fn as_ty_ref(&self, ty: &FieldT) -> Self {
|
||||
if &self.ty() == ty {
|
||||
self.clone()
|
||||
} else if self.modulus() != ty.modulus() {
|
||||
panic!(
|
||||
"Incompatible modulus specified: {:#?} vs {:#?}",
|
||||
self.ty(),
|
||||
ty,
|
||||
);
|
||||
} else {
|
||||
ty.new_v(self.i())
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for FieldV {
|
||||
fn fmt(&self, f: &mut Formatter) -> fmt::Result {
|
||||
match self {
|
||||
Self::FBls12381(pf) => write!(f, "#f{}m{}", Integer::from(pf), &*F_BLS12381_FMOD),
|
||||
Self::FBn254(pf) => write!(f, "#f{}m{}", Integer::from(pf), &*F_BN254_FMOD),
|
||||
Self::IntField(i) => i.fmt(f),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
macro_rules! arith_impl {
|
||||
($Trait: ident, $fn: ident) => {
|
||||
paste! {
|
||||
impl $Trait<FieldV> for FieldV {
|
||||
type Output = Self;
|
||||
fn $fn(mut self, other: Self) -> Self {
|
||||
self.[<$fn _assign>](&other);
|
||||
self
|
||||
}
|
||||
}
|
||||
|
||||
impl $Trait<&FieldV> for FieldV {
|
||||
type Output = Self;
|
||||
fn $fn(mut self, other: &Self) -> Self {
|
||||
self.[<$fn _assign>](other);
|
||||
self
|
||||
}
|
||||
}
|
||||
|
||||
impl [<$Trait Assign>]<&FieldV> for FieldV {
|
||||
fn [<$fn _assign>](&mut self, other: &FieldV) {
|
||||
match (self, other) {
|
||||
(Self::FBls12381(f1), Self::FBls12381(f2)) => f1.[<$fn _assign>](f2),
|
||||
(Self::FBn254(f1), Self::FBn254(f2)) => f1.[<$fn _assign>](f2),
|
||||
(Self::IntField(i1), Self::IntField(i2)) => i1.[<$fn _assign>](i2),
|
||||
(s, o) => panic!("Operation [<$Trait Assign>] on {} and {}", s.ty(), o.ty()),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl [<$Trait Assign>]<FieldV> for FieldV {
|
||||
fn [<$fn _assign>](&mut self, other: FieldV) {
|
||||
self.[<$fn _assign>](&other);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
arith_impl!(Add, add);
|
||||
arith_impl!(Mul, mul);
|
||||
arith_impl!(Sub, sub);
|
||||
|
||||
impl Neg for FieldV {
|
||||
type Output = Self;
|
||||
fn neg(self) -> Self {
|
||||
match self {
|
||||
Self::FBls12381(pf) => Self::FBls12381(pf.neg()),
|
||||
Self::FBn254(pf) => Self::FBn254(pf.neg()),
|
||||
Self::IntField(i) => Self::IntField(i.neg()),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[allow(clippy::from_over_into)]
|
||||
impl Into<FieldV> for FBls12381 {
|
||||
fn into(self) -> FieldV {
|
||||
FieldV::FBls12381(self)
|
||||
}
|
||||
}
|
||||
|
||||
#[allow(clippy::from_over_into)]
|
||||
impl Into<FieldV> for FBn254 {
|
||||
fn into(self) -> FieldV {
|
||||
FieldV::FBn254(self)
|
||||
}
|
||||
}
|
||||
|
||||
#[allow(clippy::from_over_into)]
|
||||
impl Into<FieldV> for IntField {
|
||||
fn into(self) -> FieldV {
|
||||
FieldV::IntField(self)
|
||||
}
|
||||
}
|
||||
|
||||
#[allow(clippy::from_over_into)]
|
||||
impl Into<Integer> for FieldV {
|
||||
fn into(self) -> Integer {
|
||||
match self {
|
||||
FieldV::FBls12381(f) => Integer::from(&f),
|
||||
FieldV::FBn254(f) => Integer::from(&f),
|
||||
FieldV::IntField(i) => i.i,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[allow(clippy::from_over_into)]
|
||||
impl Into<Integer> for &FieldV {
|
||||
fn into(self) -> Integer {
|
||||
match self {
|
||||
FieldV::FBls12381(f) => Integer::from(f),
|
||||
FieldV::FBn254(f) => Integer::from(f),
|
||||
FieldV::IntField(i) => i.i.clone(),
|
||||
}
|
||||
}
|
||||
}
|
||||
37
driver.py
37
driver.py
@@ -16,7 +16,7 @@ def install(features):
|
||||
"""
|
||||
|
||||
def verify_path_empty(path) -> bool:
|
||||
return not os.path.isdir(path) or (os.path.isdir(path) and not os.listdir(path))
|
||||
return not os.path.isdir(path) or (os.path.isdir(path) and not os.listdir(path))
|
||||
|
||||
for f in features:
|
||||
if f == "aby":
|
||||
@@ -37,9 +37,9 @@ def check(features):
|
||||
set of features required
|
||||
"""
|
||||
|
||||
cmd = ["cargo", "check"]
|
||||
cmd = ["cargo", "check", "--tests", "--examples", "--benches", "--bins"]
|
||||
cargo_features = filter_cargo_features(features)
|
||||
if cargo_features:
|
||||
if cargo_features:
|
||||
cmd = cmd + ["--features"] + cargo_features
|
||||
subprocess.run(cmd, check=True)
|
||||
|
||||
@@ -57,14 +57,14 @@ def build(features):
|
||||
check(features)
|
||||
install(features)
|
||||
|
||||
cmd = ["cargo", "build"]
|
||||
cmd = ["cargo", "build"]
|
||||
if mode:
|
||||
cmd += ["--"+mode]
|
||||
cmd += ["--"+mode]
|
||||
else:
|
||||
# default to release mode
|
||||
cmd += ["--release"]
|
||||
cmd += ["--release"]
|
||||
cmd += ["--examples"]
|
||||
|
||||
|
||||
cargo_features = filter_cargo_features(features)
|
||||
if cargo_features:
|
||||
cmd = cmd + ["--features"] + cargo_features
|
||||
@@ -117,8 +117,21 @@ def format():
|
||||
subprocess.run(["cargo", "fmt", "--all"], check=True)
|
||||
|
||||
def lint():
|
||||
"""
|
||||
Run cargo clippy
|
||||
|
||||
Parameters
|
||||
----------
|
||||
features : set of str
|
||||
set of features required
|
||||
"""
|
||||
print("linting!")
|
||||
subprocess.run(["cargo", "clippy"], check=True)
|
||||
|
||||
cmd = ["cargo", "clippy", "--tests", "--examples", "--benches", "--bins"]
|
||||
cargo_features = filter_cargo_features(features)
|
||||
if cargo_features:
|
||||
cmd = cmd + ["--features"] + cargo_features
|
||||
subprocess.run(cmd, check=True)
|
||||
|
||||
def flamegraph(features, extra):
|
||||
cmd = ["cargo", "flamegraph"]
|
||||
@@ -163,7 +176,7 @@ def set_features(features):
|
||||
features = set(sorted([f for f in features if verify_feature(f)]))
|
||||
save_features(features)
|
||||
print("Feature set:", sorted(list(features)))
|
||||
return features
|
||||
return features
|
||||
|
||||
if __name__ == "__main__":
|
||||
parser = argparse.ArgumentParser()
|
||||
@@ -221,15 +234,15 @@ if __name__ == "__main__":
|
||||
|
||||
if args.clean:
|
||||
clean(features)
|
||||
|
||||
|
||||
if args.mode:
|
||||
set_mode(args.mode)
|
||||
|
||||
if args.all_features:
|
||||
features = set_features(valid_features)
|
||||
|
||||
|
||||
if args.list_features:
|
||||
print("Feature set: ", sorted(list(features)))
|
||||
print("Feature set:", sorted(list(features)))
|
||||
|
||||
if args.features:
|
||||
features = set_features(args.features)
|
||||
|
||||
@@ -28,6 +28,8 @@ use circ::target::r1cs::opt::reduce_linearities;
|
||||
use circ::target::r1cs::trans::to_r1cs;
|
||||
#[cfg(feature = "smt")]
|
||||
use circ::target::smt::find_model;
|
||||
use circ::util::field::DFL_T;
|
||||
use circ_fields::FieldT;
|
||||
#[cfg(feature = "lp")]
|
||||
use good_lp::default_solver;
|
||||
use std::fs::File;
|
||||
@@ -91,6 +93,9 @@ enum Backend {
|
||||
proof: PathBuf,
|
||||
#[structopt(long, default_value = "x", parse(from_os_str))]
|
||||
instance: PathBuf,
|
||||
#[structopt(long, default_value = "50")]
|
||||
/// linear combination constraints up to this size will be eliminated
|
||||
lc_elimination_thresh: usize,
|
||||
#[structopt(long, default_value = "count")]
|
||||
action: ProofAction,
|
||||
},
|
||||
@@ -273,12 +278,13 @@ fn main() {
|
||||
prover_key,
|
||||
verifier_key,
|
||||
instance,
|
||||
lc_elimination_thresh,
|
||||
..
|
||||
} => {
|
||||
println!("Converting to r1cs");
|
||||
let r1cs = to_r1cs(cs, circ::front::ZSHARP_MODULUS.clone());
|
||||
let r1cs = to_r1cs(cs, FieldT::from(DFL_T.modulus()));
|
||||
println!("Pre-opt R1cs size: {}", r1cs.constraints().len());
|
||||
let r1cs = reduce_linearities(r1cs);
|
||||
let r1cs = reduce_linearities(r1cs, Some(lc_elimination_thresh));
|
||||
println!("Final R1cs size: {}", r1cs.constraints().len());
|
||||
match action {
|
||||
ProofAction::Count => (),
|
||||
|
||||
@@ -8,14 +8,15 @@ use bellman::Circuit;
|
||||
use bls12_381::{Bls12, Scalar};
|
||||
*/
|
||||
use circ::front::zsharp::{self, ZSharpFE};
|
||||
|
||||
use circ::front::{FrontEnd, Mode};
|
||||
use circ::ir::opt::{opt, Opt};
|
||||
use circ_fields::FieldT;
|
||||
/*
|
||||
use circ::target::r1cs::bellman::parse_instance;
|
||||
*/
|
||||
use circ::target::r1cs::opt::reduce_linearities;
|
||||
use circ::target::r1cs::trans::to_r1cs;
|
||||
use circ::util::field::DFL_T;
|
||||
/*
|
||||
use std::fs::File;
|
||||
use std::io::Read;
|
||||
@@ -49,8 +50,13 @@ struct Options {
|
||||
instance: PathBuf,
|
||||
*/
|
||||
#[structopt(short = "L")]
|
||||
/// skip linearity reduction entirely
|
||||
skip_linred: bool,
|
||||
|
||||
#[structopt(long, default_value = "50")]
|
||||
/// linear combination constraints up to this size will be eliminated (if the pass is enabled)
|
||||
lc_elimination_thresh: usize,
|
||||
|
||||
#[structopt(long, default_value = "count")]
|
||||
action: ProofAction,
|
||||
}
|
||||
@@ -132,7 +138,7 @@ fn main() {
|
||||
*/
|
||||
|
||||
println!("Converting to r1cs");
|
||||
let r1cs = to_r1cs(cs, circ::front::ZSHARP_MODULUS.clone());
|
||||
let r1cs = to_r1cs(cs, FieldT::from(DFL_T.modulus()));
|
||||
let r1cs = if options.skip_linred {
|
||||
println!("Skipping linearity reduction, as requested.");
|
||||
r1cs
|
||||
@@ -141,12 +147,12 @@ fn main() {
|
||||
"R1cs size before linearity reduction: {}",
|
||||
r1cs.constraints().len()
|
||||
);
|
||||
reduce_linearities(r1cs)
|
||||
reduce_linearities(r1cs, Some(options.lc_elimination_thresh))
|
||||
};
|
||||
println!("Final R1cs size: {}", r1cs.constraints().len());
|
||||
match action {
|
||||
ProofAction::Count => {
|
||||
println!("{:#?}", r1cs.constraints());
|
||||
eprintln!("{:#?}", r1cs.constraints());
|
||||
}
|
||||
ProofAction::Prove => {
|
||||
unimplemented!()
|
||||
|
||||
5
scripts/zx_tests/slice_assign.zx
Normal file
5
scripts/zx_tests/slice_assign.zx
Normal file
@@ -0,0 +1,5 @@
|
||||
def main() -> u32[4]:
|
||||
u32[7] foo = [1, 2, 3, 4, 5, 6, 7]
|
||||
u32[4] bar = [0; 4]
|
||||
bar = foo[2..6]
|
||||
return bar
|
||||
18
scripts/zx_tests/struct_generic.zx
Normal file
18
scripts/zx_tests/struct_generic.zx
Normal file
@@ -0,0 +1,18 @@
|
||||
struct Bar<N> {
|
||||
field[N] c
|
||||
bool d
|
||||
}
|
||||
|
||||
struct Foo<P> {
|
||||
Bar<P> a
|
||||
bool b
|
||||
}
|
||||
|
||||
// const Bar<2> VAR_B = Bar{ c: [0, 0], d: false }
|
||||
|
||||
def main() -> (Foo<2>):
|
||||
Bar<2> var_b = Bar{ c: [0, 0], d: false }
|
||||
// Bar<2> var_b = VAR_B
|
||||
Foo<2>[2] f = [Foo { a: var_b, b: true}, Foo { a: var_b, b: true}]
|
||||
f[0].a.c = [42, 43]
|
||||
return f[0]
|
||||
@@ -452,18 +452,17 @@ impl CGen {
|
||||
let base_ty: Ty = decl_info.ty;
|
||||
let derived = &d.declarator.node.derived;
|
||||
let derived_ty = self.derived_type_(base_ty, derived.to_vec());
|
||||
let expr: CTerm;
|
||||
if let Some(init) = d.initializer {
|
||||
expr = self.gen_init(derived_ty.clone(), init.node);
|
||||
let expr = if let Some(init) = d.initializer {
|
||||
self.gen_init(derived_ty.clone(), init.node)
|
||||
} else {
|
||||
expr = match derived_ty {
|
||||
match derived_ty {
|
||||
Ty::Array(size, ref ty) => {
|
||||
let id = self.circ.zero_allocate(size.unwrap(), 32, ty.num_bits());
|
||||
cterm(CTermData::CArray(*ty.clone(), Some(id)))
|
||||
}
|
||||
_ => derived_ty.default(),
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
let res = self.circ.declare_init(
|
||||
decl_info.name,
|
||||
|
||||
@@ -8,6 +8,7 @@ use rug::Integer;
|
||||
use std::collections::HashMap;
|
||||
use std::fmt::{self, Display, Formatter};
|
||||
|
||||
#[allow(clippy::enum_variant_names)]
|
||||
#[derive(Clone)]
|
||||
pub enum CTermData {
|
||||
CBool(Term),
|
||||
|
||||
@@ -1,7 +1,6 @@
|
||||
//! Terms in our datalog variant
|
||||
|
||||
use std::fmt::{self, Display, Formatter};
|
||||
use std::sync::Arc;
|
||||
|
||||
use rug::Integer;
|
||||
|
||||
@@ -9,8 +8,8 @@ use super::error::ErrorKind;
|
||||
use super::ty::Ty;
|
||||
|
||||
use crate::circify::{CirCtx, Embeddable};
|
||||
use crate::front::{ZSHARP_FIELD_SORT, ZSHARP_MODULUS_ARC};
|
||||
use crate::ir::term::*;
|
||||
use crate::util::field::DFL_T;
|
||||
|
||||
/// A term
|
||||
#[derive(Debug, Clone)]
|
||||
@@ -64,10 +63,7 @@ pub fn pf_ir_lit<I>(i: I) -> Term
|
||||
where
|
||||
Integer: From<I>,
|
||||
{
|
||||
leaf_term(Op::Const(Value::Field(FieldElem::new(
|
||||
Integer::from(i),
|
||||
ZSHARP_MODULUS_ARC.clone(),
|
||||
))))
|
||||
leaf_term(Op::Const(Value::Field(DFL_T.new_v(i))))
|
||||
}
|
||||
|
||||
/// Initialize a boolean literal
|
||||
@@ -85,9 +81,9 @@ impl Ty {
|
||||
match self {
|
||||
Self::Bool => Sort::Bool,
|
||||
Self::Uint(w) => Sort::BitVector(*w as usize),
|
||||
Self::Field => ZSHARP_FIELD_SORT.clone(),
|
||||
Self::Field => Sort::Field(DFL_T.clone()),
|
||||
Self::Array(n, b) => {
|
||||
Sort::Array(Box::new(ZSHARP_FIELD_SORT.clone()), Box::new(b.sort()), *n)
|
||||
Sort::Array(Box::new(Sort::Field(DFL_T.clone())), Box::new(b.sort()), *n)
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -320,7 +316,7 @@ pub fn or(s: &T, t: &T) -> Result<T> {
|
||||
pub fn uint_to_field(s: &T) -> Result<T> {
|
||||
match &s.ty {
|
||||
Ty::Uint(_) => Ok(T::new(
|
||||
term![Op::UbvToPf(ZSHARP_MODULUS_ARC.clone()); s.ir.clone()],
|
||||
term![Op::UbvToPf(DFL_T.clone()); s.ir.clone()],
|
||||
Ty::Field,
|
||||
)),
|
||||
_ => Err(ErrorKind::InvalidUnOp("to_field".into(), s.clone())),
|
||||
@@ -343,9 +339,7 @@ pub fn array_idx(a: &T, i: &T) -> Result<T> {
|
||||
}
|
||||
|
||||
/// Datalog lang def
|
||||
pub struct Datalog {
|
||||
modulus: Arc<Integer>,
|
||||
}
|
||||
pub struct Datalog;
|
||||
|
||||
impl Embeddable for Datalog {
|
||||
type T = T;
|
||||
@@ -372,8 +366,8 @@ impl Embeddable for Datalog {
|
||||
Ty::Field => T::new(
|
||||
ctx.cs.borrow_mut().new_var(
|
||||
&raw_name,
|
||||
Sort::Field(self.modulus.clone()),
|
||||
|| Value::Field(FieldElem::new(get_int_val(), self.modulus.clone())),
|
||||
Sort::Field(DFL_T.clone()),
|
||||
|| Value::Field(DFL_T.new_v(get_int_val())),
|
||||
visibility,
|
||||
),
|
||||
Ty::Field,
|
||||
@@ -450,9 +444,7 @@ impl Default for Datalog {
|
||||
impl Datalog {
|
||||
/// Initialize the Datalog lang def
|
||||
pub fn new() -> Self {
|
||||
Self {
|
||||
modulus: ZSHARP_MODULUS_ARC.clone(),
|
||||
}
|
||||
Self
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -6,53 +6,16 @@ pub mod datalog;
|
||||
#[cfg(all(feature = "smt", feature = "zok"))]
|
||||
pub mod zsharp;
|
||||
|
||||
use crate::ir::{
|
||||
proof,
|
||||
term::{PartyId, Sort},
|
||||
};
|
||||
use crate::ir::proof;
|
||||
use crate::ir::term::{Computation, PartyId};
|
||||
|
||||
use super::ir::term::Computation;
|
||||
use lazy_static::lazy_static;
|
||||
use rug::Integer;
|
||||
use std::{
|
||||
fmt::{self, Display, Formatter},
|
||||
sync::Arc,
|
||||
};
|
||||
use std::fmt::{self, Display, Formatter};
|
||||
|
||||
/// The prover visibility
|
||||
pub const PROVER_VIS: Option<PartyId> = Some(proof::PROVER_ID);
|
||||
/// Public visibility
|
||||
pub const PUBLIC_VIS: Option<PartyId> = None;
|
||||
|
||||
// The modulus for Z#.
|
||||
// TODO: handle this better!
|
||||
#[cfg(feature = "bls12381")]
|
||||
lazy_static! {
|
||||
/// The modulus for Z#
|
||||
pub static ref ZSHARP_MODULUS: Integer = Integer::from_str_radix(
|
||||
"52435875175126190479447740508185965837690552500527637822603658699938581184513", // BLS12-381 group order
|
||||
10
|
||||
)
|
||||
.unwrap();
|
||||
}
|
||||
|
||||
#[cfg(not(feature = "bls12381"))]
|
||||
lazy_static! {
|
||||
/// The modulus for Z#
|
||||
pub static ref ZSHARP_MODULUS: Integer = Integer::from_str_radix(
|
||||
"21888242871839275222246405745257275088548364400416034343698204186575808495617", // BN-254 group order
|
||||
10
|
||||
)
|
||||
.unwrap();
|
||||
}
|
||||
|
||||
lazy_static! {
|
||||
/// The modulus for Z#, as an ARC
|
||||
pub static ref ZSHARP_MODULUS_ARC: Arc<Integer> = Arc::new(ZSHARP_MODULUS.clone());
|
||||
/// The modulus for Z#, as an IR sort
|
||||
pub static ref ZSHARP_FIELD_SORT: Sort = Sort::Field(ZSHARP_MODULUS_ARC.clone());
|
||||
}
|
||||
|
||||
/// A front-end
|
||||
pub trait FrontEnd {
|
||||
/// Representation of an input program (possibly with argument assignments) for this language
|
||||
|
||||
@@ -29,6 +29,18 @@
|
||||
- optimization: for a < b, only expand a to b's bit width;
|
||||
a < b is (a_expansion == a) && (a_expansion < b_expansion)
|
||||
|
||||
--
|
||||
wants
|
||||
|
||||
- improve speed (atomics?)
|
||||
- shake is fast in zxi but slow in zxc (linearity reduction)
|
||||
|
||||
--> fix field up-front?
|
||||
|
||||
- cc-snarks/examples/sha3/keccakf-zxc.zok
|
||||
|
||||
--
|
||||
|
||||
== done ==
|
||||
|
||||
[x] generic inf: monomorphize at call time
|
||||
|
||||
@@ -6,10 +6,11 @@ pub mod zvisit;
|
||||
|
||||
use super::{FrontEnd, Mode};
|
||||
use crate::circify::{CircError, Circify, Loc, Val};
|
||||
use crate::front::ZSHARP_MODULUS;
|
||||
use crate::front::{PROVER_VIS, PUBLIC_VIS};
|
||||
use crate::ir::proof::ConstraintMetadata;
|
||||
use crate::ir::term::*;
|
||||
use crate::util::field::DFL_T;
|
||||
|
||||
use log::{debug, warn};
|
||||
use rug::Integer;
|
||||
use std::cell::{Cell, RefCell};
|
||||
@@ -202,6 +203,47 @@ impl<'ast> ZGen<'ast> {
|
||||
uint_from_bits(args.pop().unwrap())
|
||||
}
|
||||
}
|
||||
"u8_to_field" | "u16_to_field" | "u32_to_field" | "u64_to_field" => {
|
||||
if args.len() != 1 {
|
||||
Err(format!(
|
||||
"Got {} args to EMBED/{}, expected 1",
|
||||
args.len(),
|
||||
f_name
|
||||
))
|
||||
} else if !generics.is_empty() {
|
||||
Err(format!(
|
||||
"Got {} generic args to EMBED/{}, expected 0",
|
||||
generics.len(),
|
||||
f_name
|
||||
))
|
||||
} else {
|
||||
uint_to_field(args.pop().unwrap())
|
||||
}
|
||||
}
|
||||
"u8_to_u64" | "u16_to_u64" | "u32_to_u64" | "u8_to_u32" | "u16_to_u32"
|
||||
| "u8_to_u16" => {
|
||||
if args.len() != 1 {
|
||||
Err(format!(
|
||||
"Got {} args to EMBED/{}, expected 1",
|
||||
args.len(),
|
||||
f_name
|
||||
))
|
||||
} else if !generics.is_empty() {
|
||||
Err(format!(
|
||||
"Got {} generic args to EMBED/{}, expected 0",
|
||||
generics.len(),
|
||||
f_name
|
||||
))
|
||||
} else {
|
||||
let len = f_name.len();
|
||||
match &f_name[len - 2..] {
|
||||
"64" => uint_to_uint(args.pop().unwrap(), 64),
|
||||
"32" => uint_to_uint(args.pop().unwrap(), 32),
|
||||
"16" => uint_to_uint(args.pop().unwrap(), 16),
|
||||
_ => unreachable!(),
|
||||
}
|
||||
}
|
||||
}
|
||||
"unpack" => {
|
||||
if args.len() != 1 {
|
||||
Err(format!(
|
||||
@@ -260,7 +302,7 @@ impl<'ast> ZGen<'ast> {
|
||||
generics.len()
|
||||
))
|
||||
} else {
|
||||
Ok(uint_lit(ZSHARP_MODULUS.significant_bits(), 32))
|
||||
Ok(uint_lit(DFL_T.modulus().significant_bits(), 32))
|
||||
}
|
||||
}
|
||||
_ => Err(format!("Unknown or unimplemented builtin '{}'", f_name)),
|
||||
@@ -901,12 +943,6 @@ impl<'ast> ZGen<'ast> {
|
||||
assert!(!p.accesses.is_empty());
|
||||
let (val, accs) = if let Some(ast::Access::Call(c)) = p.accesses.first() {
|
||||
let (f_path, f_name) = self.deref_import(&p.id.value);
|
||||
let args = c
|
||||
.arguments
|
||||
.expressions
|
||||
.iter()
|
||||
.map(|e| self.expr_impl_::<IS_CNST>(e))
|
||||
.collect::<Result<Vec<_>, _>>()?;
|
||||
let exp_ty = self.lhs_ty_take().and_then(|ty| {
|
||||
if p.accesses.len() > 1 {
|
||||
None
|
||||
@@ -914,6 +950,12 @@ impl<'ast> ZGen<'ast> {
|
||||
Some(ty)
|
||||
}
|
||||
});
|
||||
let args = c
|
||||
.arguments
|
||||
.expressions
|
||||
.iter()
|
||||
.map(|e| self.expr_impl_::<IS_CNST>(e))
|
||||
.collect::<Result<Vec<_>, _>>()?;
|
||||
let egv = c
|
||||
.explicit_generics
|
||||
.as_ref()
|
||||
@@ -1001,15 +1043,15 @@ impl<'ast> ZGen<'ast> {
|
||||
.map_err(|e| format!("{}", e))
|
||||
}
|
||||
ast::Statement::Assertion(e) => {
|
||||
match self
|
||||
.expr_impl_::<true>(&e.expression)
|
||||
.ok()
|
||||
.and_then(const_bool)
|
||||
{
|
||||
Some(true) => Ok(()),
|
||||
Some(false) => Err("Const assert failed".to_string()),
|
||||
None if IS_CNST => Err(format!(
|
||||
"Const assert expression eval failed: {}",
|
||||
match self.expr_impl_::<true>(&e.expression).and_then(|v| {
|
||||
const_bool(v)
|
||||
.ok_or_else(|| "interpreting expr as const bool failed".to_string())
|
||||
}) {
|
||||
Ok(true) => Ok(()),
|
||||
Ok(false) => Err("Const assert failed".to_string()),
|
||||
Err(err) if IS_CNST => Err(format!(
|
||||
"Const assert expression eval failed at {}: {}",
|
||||
err,
|
||||
span_to_string(e.expression.span()),
|
||||
)),
|
||||
_ => {
|
||||
|
||||
@@ -97,7 +97,7 @@ impl ZStdLib {
|
||||
/// check if this path is the EMBED prototypes path
|
||||
pub fn is_embed<P: AsRef<Path>>(&self, p: P) -> bool {
|
||||
p.as_ref().starts_with(&self.path)
|
||||
&& p.as_ref().file_stem().map(|s| s.to_str()).flatten() == Some("EMBED")
|
||||
&& p.as_ref().file_stem().and_then(|s| s.to_str()) == Some("EMBED")
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -1,11 +1,6 @@
|
||||
//! Symbolic Z# terms
|
||||
use std::collections::{BTreeMap, HashMap};
|
||||
use std::fmt::{self, Display, Formatter};
|
||||
use std::sync::Arc;
|
||||
|
||||
use crate::front::ZSHARP_FIELD_SORT;
|
||||
use crate::front::ZSHARP_MODULUS;
|
||||
use crate::front::ZSHARP_MODULUS_ARC;
|
||||
|
||||
use log::warn;
|
||||
use rug::Integer;
|
||||
@@ -13,6 +8,7 @@ use rug::Integer;
|
||||
use crate::circify::{CirCtx, Embeddable};
|
||||
use crate::ir::opt::cfold::fold as constant_fold;
|
||||
use crate::ir::term::*;
|
||||
use crate::util::field::DFL_T;
|
||||
|
||||
#[derive(Clone, PartialEq, Eq)]
|
||||
pub enum Ty {
|
||||
@@ -99,9 +95,9 @@ impl Ty {
|
||||
match self {
|
||||
Self::Bool => Sort::Bool,
|
||||
Self::Uint(w) => Sort::BitVector(*w),
|
||||
Self::Field => ZSHARP_FIELD_SORT.clone(),
|
||||
Self::Field => Sort::Field(DFL_T.clone()),
|
||||
Self::Array(n, b) => {
|
||||
Sort::Array(Box::new(ZSHARP_FIELD_SORT.clone()), Box::new(b.sort()), *n)
|
||||
Sort::Array(Box::new(Sort::Field(DFL_T.clone())), Box::new(b.sort()), *n)
|
||||
}
|
||||
Self::Struct(_name, fs) => {
|
||||
Sort::Tuple(fs.fields().map(|(_f_name, f_ty)| f_ty.sort()).collect())
|
||||
@@ -395,10 +391,10 @@ pub fn div(a: T, b: T) -> Result<T, String> {
|
||||
}
|
||||
|
||||
fn rem_field(a: Term, b: Term) -> Term {
|
||||
let len = ZSHARP_MODULUS.significant_bits() as usize;
|
||||
let len = DFL_T.modulus().significant_bits() as usize;
|
||||
let a_bv = term![Op::PfToBv(len); a];
|
||||
let b_bv = term![Op::PfToBv(len); b];
|
||||
term![Op::UbvToPf(ZSHARP_MODULUS_ARC.clone()); term![Op::BvBinOp(BvBinOp::Urem); a_bv, b_bv]]
|
||||
term![Op::UbvToPf(DFL_T.clone()); term![Op::BvBinOp(BvBinOp::Urem); a_bv, b_bv]]
|
||||
}
|
||||
|
||||
fn rem_uint(a: Term, b: Term) -> Term {
|
||||
@@ -476,7 +472,7 @@ fn ult_uint(a: Term, b: Term) -> Term {
|
||||
// XXX(constr_opt) see TODO file - only need to expand to MIN of two bit-lengths if done right
|
||||
// XXX(constr_opt) do this using subtraction instead?
|
||||
fn field_comp(a: Term, b: Term, op: BvBinPred) -> Term {
|
||||
let len = ZSHARP_MODULUS.significant_bits() as usize;
|
||||
let len = DFL_T.modulus().significant_bits() as usize;
|
||||
let a_bv = term![Op::PfToBv(len); a];
|
||||
let b_bv = term![Op::PfToBv(len); b];
|
||||
term![Op::BvBinPred(op); a_bv, b_bv]
|
||||
@@ -595,7 +591,7 @@ pub fn not(a: T) -> Result<T, String> {
|
||||
|
||||
pub fn const_int(a: T) -> Result<Integer, String> {
|
||||
match const_value(&a.term) {
|
||||
Some(Value::Field(f)) => Ok(f.i().clone()),
|
||||
Some(Value::Field(f)) => Ok(f.i()),
|
||||
Some(Value::BitVector(f)) => Ok(f.uint().clone()),
|
||||
_ => Err(format!("{} is not a constant integer", a)),
|
||||
}
|
||||
@@ -669,7 +665,7 @@ fn pf_val<I>(i: I) -> Value
|
||||
where
|
||||
Integer: From<I>,
|
||||
{
|
||||
Value::Field(FieldElem::new(Integer::from(i), ZSHARP_MODULUS_ARC.clone()))
|
||||
Value::Field(DFL_T.new_v(i))
|
||||
}
|
||||
|
||||
pub fn field_lit<I>(i: I) -> T
|
||||
@@ -747,7 +743,7 @@ pub fn array_select(array: T, idx: T) -> Result<T, String> {
|
||||
Ty::Array(_, elem_ty) if matches!(idx.ty, Ty::Uint(_) | Ty::Field) => {
|
||||
let iterm = if matches!(idx.ty, Ty::Uint(_)) {
|
||||
warn!("warning: indexing array with Uint type");
|
||||
term![Op::UbvToPf(ZSHARP_MODULUS_ARC.clone()); idx.term]
|
||||
term![Op::UbvToPf(DFL_T.clone()); idx.term]
|
||||
} else {
|
||||
idx.term
|
||||
};
|
||||
@@ -762,7 +758,7 @@ pub fn array_store(array: T, idx: T, val: T) -> Result<T, String> {
|
||||
// XXX(q) typecheck here?
|
||||
let iterm = if matches!(idx.ty, Ty::Uint(_)) {
|
||||
warn!("warning: indexing array with Uint type");
|
||||
term![Op::UbvToPf(ZSHARP_MODULUS_ARC.clone()); idx.term]
|
||||
term![Op::UbvToPf(DFL_T.clone()); idx.term]
|
||||
} else {
|
||||
idx.term
|
||||
};
|
||||
@@ -793,7 +789,7 @@ fn ir_array<I: IntoIterator<Item = Term>>(sort: Sort, elems: I) -> Term {
|
||||
.collect::<Vec<(Term, Term)>>();
|
||||
let len = values.len() + to_insert.len();
|
||||
let arr = leaf_term(Op::Const(Value::Array(Array::new(
|
||||
ZSHARP_FIELD_SORT.clone(),
|
||||
Sort::Field(DFL_T.clone()),
|
||||
Box::new(sort.default_value()),
|
||||
values,
|
||||
len,
|
||||
@@ -821,6 +817,21 @@ pub fn array<I: IntoIterator<Item = T>>(elems: I) -> Result<T, String> {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn uint_to_field(u: T) -> Result<T, String> {
|
||||
match &u.ty {
|
||||
Ty::Uint(_) => Ok(T::new(Ty::Field, term![Op::UbvToPf(DFL_T.clone()); u.term])),
|
||||
u => Err(format!("Cannot do uint-to-field on {}", u)),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn uint_to_uint(u: T, w: usize) -> Result<T, String> {
|
||||
match &u.ty {
|
||||
Ty::Uint(n) if *n <= w => Ok(T::new(Ty::Uint(w), term![Op::BvUext(w - n); u.term])),
|
||||
Ty::Uint(n) => Err(format!("Tried narrowing uint{}-to-uint{} attempted", n, w)),
|
||||
u => Err(format!("Cannot do uint-to-uint on {}", u)),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn uint_to_bits(u: T) -> Result<T, String> {
|
||||
match &u.ty {
|
||||
Ty::Uint(n) => Ok(T::new(
|
||||
@@ -902,7 +913,6 @@ pub fn bit_array_le(a: T, b: T, n: usize) -> Result<T, String> {
|
||||
|
||||
pub struct ZSharp {
|
||||
values: Option<HashMap<String, Integer>>,
|
||||
modulus: Arc<Integer>,
|
||||
}
|
||||
|
||||
fn field_name(struct_name: &str, field_name: &str) -> String {
|
||||
@@ -915,10 +925,7 @@ fn idx_name(struct_name: &str, idx: usize) -> String {
|
||||
|
||||
impl ZSharp {
|
||||
pub fn new(values: Option<HashMap<String, Integer>>) -> Self {
|
||||
Self {
|
||||
values,
|
||||
modulus: ZSHARP_MODULUS_ARC.clone(),
|
||||
}
|
||||
Self { values }
|
||||
}
|
||||
}
|
||||
|
||||
@@ -959,8 +966,8 @@ impl Embeddable for ZSharp {
|
||||
Ty::Field,
|
||||
ctx.cs.borrow_mut().new_var(
|
||||
&raw_name,
|
||||
Sort::Field(self.modulus.clone()),
|
||||
|| Value::Field(FieldElem::new(get_int_val(), self.modulus.clone())),
|
||||
Sort::Field(DFL_T.clone()),
|
||||
|| Value::Field(DFL_T.new_v(get_int_val())),
|
||||
visibility,
|
||||
),
|
||||
),
|
||||
|
||||
@@ -267,23 +267,26 @@ impl<'ast> ZVisitorMut<'ast> for ZConstLiteralRewriter {
|
||||
}
|
||||
|
||||
fn visit_array_type(&mut self, aty: &mut ast::ArrayType<'ast>) -> ZVisitorResult {
|
||||
if self.to_ty.is_some() {
|
||||
if let Ty::Array(_, arr_ty) = self.to_ty.clone().unwrap() {
|
||||
// ArrayType::value should match arr_ty
|
||||
let to_ty = self.replace(Some(*arr_ty));
|
||||
self.visit_basic_or_struct_type(&mut aty.ty)?;
|
||||
self.to_ty = to_ty;
|
||||
} else {
|
||||
return Err(
|
||||
"ZConstLiteralRewriter: rewriting ArrayType to non-Array type"
|
||||
.to_string()
|
||||
.into(),
|
||||
);
|
||||
}
|
||||
}
|
||||
// ArrayType.ty should match arr_ty
|
||||
let to_ty = self.replace(
|
||||
self.to_ty
|
||||
.as_ref()
|
||||
.map(|to_ty| {
|
||||
if let Ty::Array(_, arr_ty) = to_ty {
|
||||
Ok(*arr_ty.clone())
|
||||
} else {
|
||||
Err(
|
||||
"ZConstLiteralRewriter: rewriting ArrayType to non-Array type"
|
||||
.to_string(),
|
||||
)
|
||||
}
|
||||
})
|
||||
.transpose()?,
|
||||
);
|
||||
self.visit_basic_or_struct_type(&mut aty.ty)?;
|
||||
|
||||
// always rewrite ArrayType::dimensions literals to type U32
|
||||
let to_ty = self.replace(Some(Ty::Uint(32)));
|
||||
self.replace(Some(Ty::Uint(32)));
|
||||
aty.dimensions
|
||||
.iter_mut()
|
||||
.try_for_each(|d| self.visit_expression(d))?;
|
||||
|
||||
@@ -161,7 +161,7 @@ impl<'ast, 'gen, const IS_CNST: bool> ZGenericInf<'ast, 'gen, IS_CNST> {
|
||||
.constr
|
||||
.as_ref()
|
||||
.and_then(|t| find_unique_model(t, g_names.clone()))
|
||||
.unwrap_or_else(HashMap::new);
|
||||
.unwrap_or_default();
|
||||
|
||||
// 5. extract the assignments from the solver result
|
||||
let mut res = HashMap::with_capacity(g_names.len());
|
||||
|
||||
@@ -1,6 +1,8 @@
|
||||
//! Constant folding
|
||||
|
||||
use crate::ir::term::*;
|
||||
|
||||
use circ_fields::FieldV;
|
||||
use lazy_static::lazy_static;
|
||||
use rug::Integer;
|
||||
use std::ops::DerefMut;
|
||||
@@ -193,12 +195,9 @@ pub fn fold_cache(node: &Term, cache: &mut TermCache<Term>) -> Term {
|
||||
PfUnOp::Neg => -pf.clone(),
|
||||
})))
|
||||
}),
|
||||
Op::UbvToPf(m) => get(0).as_bv_opt().map(|bv| {
|
||||
leaf_term(Op::Const(Value::Field(FieldElem::new(
|
||||
bv.uint().clone(),
|
||||
m.clone(),
|
||||
))))
|
||||
}),
|
||||
Op::UbvToPf(fty) => get(0)
|
||||
.as_bv_opt()
|
||||
.map(|bv| leaf_term(Op::Const(Value::Field(fty.new_v(bv.uint()))))),
|
||||
Op::Store => {
|
||||
match (
|
||||
get(0).as_array_opt(),
|
||||
@@ -459,19 +458,19 @@ impl NaryFlat<BitVector> for BvNaryOp {
|
||||
}
|
||||
}
|
||||
|
||||
impl NaryFlat<FieldElem> for PfNaryOp {
|
||||
fn as_const(t: Term) -> Result<FieldElem, Term> {
|
||||
impl NaryFlat<FieldV> for PfNaryOp {
|
||||
fn as_const(t: Term) -> Result<FieldV, Term> {
|
||||
match &t.op {
|
||||
Op::Const(Value::Field(b)) => Ok(b.clone()),
|
||||
_ => Err(t),
|
||||
}
|
||||
}
|
||||
fn combine(self, mut children: Vec<Term>, mut consts: Vec<FieldElem>) -> Term {
|
||||
fn combine(self, mut children: Vec<Term>, mut consts: Vec<FieldV>) -> Term {
|
||||
match self {
|
||||
PfNaryOp::Add => {
|
||||
if let Some(c) = consts.pop() {
|
||||
let c = consts.into_iter().fold(c, std::ops::Add::add);
|
||||
if c.i() != &Integer::from(0) || children.is_empty() {
|
||||
if !c.is_zero() || children.is_empty() {
|
||||
children.push(leaf_term(Op::Const(Value::Field(c))));
|
||||
}
|
||||
}
|
||||
@@ -480,10 +479,10 @@ impl NaryFlat<FieldElem> for PfNaryOp {
|
||||
PfNaryOp::Mul => {
|
||||
if let Some(c) = consts.pop() {
|
||||
let c = consts.into_iter().fold(c, std::ops::Mul::mul);
|
||||
if c.i() == &Integer::from(0) || children.is_empty() {
|
||||
if c.is_zero() || children.is_empty() {
|
||||
leaf_term(Op::Const(Value::Field(c)))
|
||||
} else {
|
||||
if c.i() != &Integer::from(1) {
|
||||
if !c.is_one() {
|
||||
children.push(leaf_term(Op::Const(Value::Field(c))));
|
||||
}
|
||||
safe_nary(PF_MUL, children)
|
||||
|
||||
@@ -97,9 +97,7 @@ pub fn linearize(c: &mut Computation) {
|
||||
#[cfg(test)]
|
||||
mod test {
|
||||
use super::*;
|
||||
use crate::ir::term::field::TEST_FIELD;
|
||||
use rug::Integer;
|
||||
use std::sync::Arc;
|
||||
use crate::util::field::DFL_T;
|
||||
|
||||
fn array_free(t: &Term) -> bool {
|
||||
for c in PostOrderIter::new(t.clone()) {
|
||||
@@ -117,10 +115,7 @@ mod test {
|
||||
}
|
||||
|
||||
fn field_lit(u: usize) -> Term {
|
||||
leaf_term(Op::Const(Value::Field(FieldElem::new(
|
||||
Integer::from(u),
|
||||
Arc::new(Integer::from(TEST_FIELD)),
|
||||
))))
|
||||
leaf_term(Op::Const(Value::Field(DFL_T.new_v(u))))
|
||||
}
|
||||
|
||||
#[test]
|
||||
@@ -149,7 +144,7 @@ mod test {
|
||||
#[test]
|
||||
fn select_ite_stores_field() {
|
||||
let z = term![Op::Const(Value::Array(Array::new(
|
||||
Sort::Field(Arc::new(Integer::from(TEST_FIELD))),
|
||||
Sort::Field(DFL_T.clone()),
|
||||
Box::new(Sort::BitVector(4).default_value()),
|
||||
Default::default(),
|
||||
6
|
||||
|
||||
@@ -387,11 +387,11 @@ mod test {
|
||||
5
|
||||
)))];
|
||||
let t0 = term![Op::Select;
|
||||
term![Op::Store; z0.clone(), v_bv("a", 4), bv_lit(1, 4)],
|
||||
term![Op::Store; z0, v_bv("a", 4), bv_lit(1, 4)],
|
||||
bv_lit(3, 4)
|
||||
];
|
||||
let t1 = term![Op::Select;
|
||||
term![Op::Store; z1.clone(), bv_lit(3, 4), bv_lit(1, 4)],
|
||||
term![Op::Store; z1, bv_lit(3, 4), bv_lit(1, 4)],
|
||||
bv_lit(3, 4)
|
||||
];
|
||||
let mut c = Computation::default();
|
||||
@@ -415,7 +415,7 @@ mod test {
|
||||
bv_lit(3, 4)
|
||||
];
|
||||
let t1 = term![Op::Select;
|
||||
term![Op::Store; z.clone(), bv_lit(3, 4), bv_lit(1, 4)],
|
||||
term![Op::Store; z, bv_lit(3, 4), bv_lit(1, 4)],
|
||||
bv_lit(3, 4)
|
||||
];
|
||||
let mut c = Computation::default();
|
||||
|
||||
@@ -1,9 +1,10 @@
|
||||
//! Distributions over terms (useful for fuzz testing)
|
||||
|
||||
use super::*;
|
||||
|
||||
use circ_fields::{FieldT, FieldV};
|
||||
use rand::{distributions::Distribution, prelude::SliceRandom, Rng};
|
||||
use std::iter::repeat;
|
||||
use std::sync::Arc;
|
||||
|
||||
// A distribution of boolean terms with some size.
|
||||
// All subterms are booleans.
|
||||
@@ -72,7 +73,7 @@ impl rand::distributions::Distribution<Term> for PureBoolDist {
|
||||
pub(crate) struct FixedSizeDist {
|
||||
pub size: usize,
|
||||
pub bv_width: Option<usize>,
|
||||
pub pf_mod: Option<Arc<Integer>>,
|
||||
pub pf_t: Option<FieldT>,
|
||||
pub tuples: bool,
|
||||
pub sort: Sort,
|
||||
}
|
||||
@@ -198,7 +199,7 @@ impl FixedSizeDist {
|
||||
if let Some(w) = &self.bv_width {
|
||||
sort_choices.push(Sort::BitVector(*w));
|
||||
}
|
||||
if let Some(m) = &self.pf_mod {
|
||||
if let Some(m) = &self.pf_t {
|
||||
sort_choices.push(Sort::Field(m.clone()));
|
||||
}
|
||||
let s = sort_choices.choose(rng).unwrap();
|
||||
@@ -243,7 +244,7 @@ impl FixedSizeDist {
|
||||
fn sample_sort<R: Rng + ?Sized>(&self, rng: &mut R, max_size: usize) -> Sort {
|
||||
match rng.gen_range(0..=3) {
|
||||
0 if self.bv_width.is_some() => Sort::BitVector(self.bv_width.unwrap()),
|
||||
1 if self.pf_mod.is_some() => Sort::Field(self.pf_mod.clone().unwrap()),
|
||||
1 if self.pf_t.is_some() => Sort::Field(self.pf_t.clone().unwrap()),
|
||||
2 if self.tuples && max_size > 1 => self.sample_tuple_sort(1, max_size - 1, rng),
|
||||
_ => Sort::Bool,
|
||||
}
|
||||
@@ -263,16 +264,11 @@ impl rand::distributions::Distribution<BitVector> for UniformBitVector {
|
||||
}
|
||||
}
|
||||
|
||||
pub(crate) struct UniformFieldElem(pub Arc<Integer>);
|
||||
pub(crate) struct UniformFieldV<'a>(&'a FieldT);
|
||||
|
||||
impl rand::distributions::Distribution<FieldElem> for UniformFieldElem {
|
||||
fn sample<R: rand::Rng + ?Sized>(&self, rng: &mut R) -> FieldElem {
|
||||
let mut rug_rng = rug::rand::RandState::new_mersenne_twister();
|
||||
rug_rng.seed(&Integer::from(rng.next_u32()));
|
||||
FieldElem::new(
|
||||
Integer::from(self.0.random_below_ref(&mut rug_rng)),
|
||||
self.0.clone(),
|
||||
)
|
||||
impl<'a> rand::distributions::Distribution<FieldV> for UniformFieldV<'a> {
|
||||
fn sample<R: rand::Rng + ?Sized>(&self, rng: &mut R) -> FieldV {
|
||||
self.0.random_v(rng)
|
||||
}
|
||||
}
|
||||
|
||||
@@ -284,7 +280,7 @@ impl<'a> rand::distributions::Distribution<Value> for UniformValue<'a> {
|
||||
Sort::Bool => Value::Bool(rng.gen()),
|
||||
Sort::F32 => Value::F32(rng.gen()),
|
||||
Sort::F64 => Value::F64(rng.gen()),
|
||||
Sort::Field(m) => Value::Field(UniformFieldElem(m.clone()).sample(rng)),
|
||||
Sort::Field(fty) => Value::Field(UniformFieldV(fty).sample(rng)),
|
||||
Sort::BitVector(w) => Value::BitVector(UniformBitVector(*w).sample(rng)),
|
||||
Sort::Tuple(sorts) => {
|
||||
Value::Tuple(sorts.iter().map(|s| UniformValue(s).sample(rng)).collect())
|
||||
@@ -320,6 +316,8 @@ impl rand::distributions::Distribution<Term> for FixedSizeDist {
|
||||
pub mod test {
|
||||
use super::*;
|
||||
|
||||
use crate::util::field::DFL_T;
|
||||
|
||||
use fxhash::FxHashMap as HashMap;
|
||||
use quickcheck::{Arbitrary, Gen};
|
||||
use rand::distributions::Distribution;
|
||||
@@ -339,7 +337,7 @@ pub mod test {
|
||||
let mut rng = rand::rngs::StdRng::seed_from_u64(u64::arbitrary(g));
|
||||
let d = FixedSizeDist {
|
||||
bv_width: Some(8),
|
||||
pf_mod: Some(Arc::new(Integer::from(super::field::TEST_FIELD))),
|
||||
pf_t: Some(DFL_T.clone()),
|
||||
tuples: true,
|
||||
size: g.size(),
|
||||
sort: Sort::Bool,
|
||||
@@ -402,9 +400,9 @@ pub mod test {
|
||||
let mut rng = rand::rngs::StdRng::seed_from_u64(u64::arbitrary(g));
|
||||
let d = FixedSizeDist {
|
||||
bv_width: Some(8),
|
||||
pf_t: Default::default(),
|
||||
tuples: true,
|
||||
size: g.size(),
|
||||
pf_mod: Some(Arc::new(Integer::from(super::field::TEST_FIELD))),
|
||||
sort: Sort::Bool,
|
||||
};
|
||||
let t = d.sample(&mut rng);
|
||||
|
||||
@@ -137,7 +137,7 @@ pub fn free_in(v: &str, t: Term) -> bool {
|
||||
pub fn as_uint_constant(t: &Term) -> Option<Integer> {
|
||||
match &t.op {
|
||||
Op::Const(Value::BitVector(bv)) => Some(bv.uint().clone()),
|
||||
Op::Const(Value::Field(f)) => Some(f.i().clone()),
|
||||
Op::Const(Value::Field(f)) => Some(f.i()),
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1,111 +0,0 @@
|
||||
//! Prime field literal definition
|
||||
|
||||
use rug::ops::RemRounding;
|
||||
use rug::Integer;
|
||||
|
||||
use std::fmt::{self, Display, Formatter};
|
||||
use std::sync::Arc;
|
||||
|
||||
/// Test modulus.
|
||||
pub const TEST_FIELD: usize = 1014088787;
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug, PartialOrd, Ord)]
|
||||
/// A prime field element
|
||||
pub struct FieldElem {
|
||||
i: Integer,
|
||||
modulus: Arc<Integer>,
|
||||
}
|
||||
|
||||
impl Display for FieldElem {
|
||||
fn fmt(&self, f: &mut Formatter) -> fmt::Result {
|
||||
if self.i.significant_bits() + 1 < self.modulus.significant_bits() {
|
||||
write!(f, "#f{}m{}", self.i, self.modulus)
|
||||
} else {
|
||||
write!(
|
||||
f,
|
||||
"#f-{}m{}",
|
||||
(*self.modulus).clone() - &self.i,
|
||||
self.modulus
|
||||
)
|
||||
}
|
||||
}
|
||||
}
|
||||
impl FieldElem {
|
||||
#[track_caller]
|
||||
#[inline]
|
||||
/// Check that the value is in-range.
|
||||
pub fn check(&self, location: &str) {
|
||||
debug_assert!(
|
||||
self.i >= 0,
|
||||
"Too small field elem: {}\n at {}",
|
||||
self,
|
||||
location
|
||||
);
|
||||
debug_assert!(
|
||||
self.i <= *self.modulus,
|
||||
"Too large field elem: {}\n at {}",
|
||||
self,
|
||||
location
|
||||
);
|
||||
}
|
||||
/// Get the integer value.
|
||||
pub fn i(&self) -> &Integer {
|
||||
&self.i
|
||||
}
|
||||
/// Get the modulus.
|
||||
pub fn modulus(&self) -> &Arc<Integer> {
|
||||
&self.modulus
|
||||
}
|
||||
/// Take the reciprocal.
|
||||
pub fn recip(self) -> Self {
|
||||
let r = FieldElem {
|
||||
i: self.i.invert(&*self.modulus).expect("no inverse!"),
|
||||
modulus: self.modulus,
|
||||
};
|
||||
r.check("recip");
|
||||
r
|
||||
}
|
||||
#[track_caller]
|
||||
/// Make a new prime-field element
|
||||
pub fn new(mut i: Integer, modulus: Arc<Integer>) -> FieldElem {
|
||||
if i < 0 {
|
||||
i += &*modulus;
|
||||
}
|
||||
let r = FieldElem { i, modulus };
|
||||
r.check("new");
|
||||
r
|
||||
}
|
||||
}
|
||||
|
||||
macro_rules! pf_arith_impl {
|
||||
($Trait:path, $fn:ident) => {
|
||||
impl $Trait for FieldElem {
|
||||
type Output = Self;
|
||||
fn $fn(self, other: Self) -> Self {
|
||||
assert_eq!(self.modulus, other.modulus);
|
||||
let r = FieldElem {
|
||||
i: (self.i.$fn(other.i)).rem_floor(&*self.modulus),
|
||||
modulus: self.modulus,
|
||||
};
|
||||
r.check(std::stringify!($fn));
|
||||
r
|
||||
}
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
pf_arith_impl!(std::ops::Add, add);
|
||||
pf_arith_impl!(std::ops::Sub, sub);
|
||||
pf_arith_impl!(std::ops::Mul, mul);
|
||||
|
||||
impl std::ops::Neg for FieldElem {
|
||||
type Output = Self;
|
||||
fn neg(self) -> Self {
|
||||
let r = FieldElem {
|
||||
i: (-self.i).rem_floor(&*self.modulus),
|
||||
modulus: self.modulus,
|
||||
};
|
||||
r.check("neg");
|
||||
r
|
||||
}
|
||||
}
|
||||
@@ -22,6 +22,8 @@
|
||||
//! * [Value]: a variable-free (and evaluated) term
|
||||
//!
|
||||
use crate::util::once::OnceQueue;
|
||||
|
||||
use circ_fields::{FieldT, FieldV};
|
||||
use fxhash::{FxHashMap, FxHashSet};
|
||||
use hashconsing::{HConsed, WHConsed};
|
||||
use lazy_static::lazy_static;
|
||||
@@ -34,12 +36,10 @@ use std::sync::{Arc, RwLock};
|
||||
pub mod bv;
|
||||
pub mod dist;
|
||||
pub mod extras;
|
||||
pub mod field;
|
||||
pub mod text;
|
||||
pub mod ty;
|
||||
|
||||
pub use bv::BitVector;
|
||||
pub use field::FieldElem;
|
||||
pub use ty::{check, check_rec, TypeError, TypeErrorReason};
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
|
||||
@@ -118,7 +118,7 @@ pub enum Op {
|
||||
/// Unsigned bit-vector to prime-field
|
||||
///
|
||||
/// Takes the modulus.
|
||||
UbvToPf(Arc<Integer>),
|
||||
UbvToPf(FieldT),
|
||||
|
||||
/// Binary operator, with arguments (array, index).
|
||||
///
|
||||
@@ -285,7 +285,7 @@ impl Display for Op {
|
||||
Op::FpToFp(a) => write!(f, "(fp2fp {})", a),
|
||||
Op::PfUnOp(a) => write!(f, "{}", a),
|
||||
Op::PfNaryOp(a) => write!(f, "{}", a),
|
||||
Op::UbvToPf(a) => write!(f, "(bv2pf {})", a),
|
||||
Op::UbvToPf(a) => write!(f, "(bv2pf {})", a.modulus()),
|
||||
Op::Select => write!(f, "select"),
|
||||
Op::Store => write!(f, "store"),
|
||||
Op::Tuple => write!(f, "tuple"),
|
||||
@@ -623,7 +623,7 @@ pub enum Value {
|
||||
/// Arbitrary-precision integer
|
||||
Int(Integer),
|
||||
/// Finite field element
|
||||
Field(FieldElem),
|
||||
Field(FieldV),
|
||||
/// Boolean
|
||||
Bool(bool),
|
||||
/// Array
|
||||
@@ -794,8 +794,8 @@ pub enum Sort {
|
||||
F64,
|
||||
/// arbitrary-precision integer
|
||||
Int,
|
||||
/// prime field, integers mod this modulus
|
||||
Field(Arc<Integer>),
|
||||
/// prime field, integers mod FieldT.modulus()
|
||||
Field(FieldT),
|
||||
/// boolean
|
||||
Bool,
|
||||
/// Array from one sort to another, of fixed size.
|
||||
@@ -820,8 +820,8 @@ impl Sort {
|
||||
#[track_caller]
|
||||
/// Unwrap the modulus of this prime field, panicking otherwise.
|
||||
pub fn as_pf(&self) -> Arc<Integer> {
|
||||
if let Sort::Field(w) = self {
|
||||
w.clone()
|
||||
if let Sort::Field(fty) = self {
|
||||
fty.modulus_arc()
|
||||
} else {
|
||||
panic!("{} is not a field", self)
|
||||
}
|
||||
@@ -841,46 +841,7 @@ impl Sort {
|
||||
/// Only defined for booleans, bit-vectors, and field elements.
|
||||
#[track_caller]
|
||||
pub fn elems_iter(&self) -> Box<dyn Iterator<Item = Term>> {
|
||||
match self {
|
||||
Sort::Bool => Box::new(
|
||||
vec![false, true]
|
||||
.into_iter()
|
||||
.map(|b| leaf_term(Op::Const(Value::Bool(b)))),
|
||||
),
|
||||
Sort::BitVector(w) => {
|
||||
let w = *w;
|
||||
let lim = Integer::from(1) << w as u32;
|
||||
Box::new(
|
||||
std::iter::successors(Some(Integer::from(0)), move |p| {
|
||||
let q = p.clone() + 1;
|
||||
if q < lim {
|
||||
Some(q)
|
||||
} else {
|
||||
None
|
||||
}
|
||||
})
|
||||
.map(move |i| bv_lit(i, w)),
|
||||
)
|
||||
}
|
||||
Sort::Field(m) => {
|
||||
let m = m.clone();
|
||||
let m2 = m.clone();
|
||||
Box::new(
|
||||
std::iter::successors(Some(Integer::from(0)), move |p| {
|
||||
let q = p.clone() + 1;
|
||||
if q < *m {
|
||||
Some(q)
|
||||
} else {
|
||||
None
|
||||
}
|
||||
})
|
||||
.map(move |i| {
|
||||
leaf_term(Op::Const(Value::Field(FieldElem::new(i, m2.clone()))))
|
||||
}),
|
||||
)
|
||||
}
|
||||
_ => panic!("Cannot iterate over {}", self),
|
||||
}
|
||||
Box::new(self.elems_iter_values().map(|v| leaf_term(Op::Const(v))))
|
||||
}
|
||||
|
||||
/// An iterator over the elements of this sort (as IR values).
|
||||
@@ -888,7 +849,7 @@ impl Sort {
|
||||
#[track_caller]
|
||||
pub fn elems_iter_values(&self) -> Box<dyn Iterator<Item = Value>> {
|
||||
match self {
|
||||
Sort::Bool => Box::new(vec![false, true].into_iter().map(Value::Bool)),
|
||||
Sort::Bool => Box::new([false, true].iter().map(|b| Value::Bool(*b))),
|
||||
Sort::BitVector(w) => {
|
||||
let w = *w;
|
||||
let lim = Integer::from(1) << w as u32;
|
||||
@@ -904,9 +865,9 @@ impl Sort {
|
||||
.map(move |i| Value::BitVector(BitVector::new(i, w))),
|
||||
)
|
||||
}
|
||||
Sort::Field(m) => {
|
||||
let m = m.clone();
|
||||
let m2 = m.clone();
|
||||
Sort::Field(fty) => {
|
||||
let m = fty.modulus_arc();
|
||||
let fty = fty.clone();
|
||||
Box::new(
|
||||
std::iter::successors(Some(Integer::from(0)), move |p| {
|
||||
let q = p.clone() + 1;
|
||||
@@ -916,7 +877,7 @@ impl Sort {
|
||||
None
|
||||
}
|
||||
})
|
||||
.map(move |i| Value::Field(FieldElem::new(i, m2.clone()))),
|
||||
.map(move |i| Value::Field(fty.new_v(i))),
|
||||
)
|
||||
}
|
||||
_ => panic!("Cannot iterate over {}", self),
|
||||
@@ -945,7 +906,7 @@ impl Sort {
|
||||
match self {
|
||||
Sort::Bool => Value::Bool(false),
|
||||
Sort::BitVector(w) => Value::BitVector(BitVector::new(0.into(), *w)),
|
||||
Sort::Field(m) => Value::Field(FieldElem::new(Integer::from(0), m.clone())),
|
||||
Sort::Field(fty) => Value::Field(fty.default_value()),
|
||||
Sort::Int => Value::Int(0.into()),
|
||||
Sort::F32 => Value::F32(0.0f32),
|
||||
Sort::F64 => Value::F64(0.0),
|
||||
@@ -963,7 +924,7 @@ impl Display for Sort {
|
||||
Sort::Int => write!(f, "int"),
|
||||
Sort::F32 => write!(f, "f32"),
|
||||
Sort::F64 => write!(f, "f64"),
|
||||
Sort::Field(i) => write!(f, "(mod {})", i),
|
||||
Sort::Field(fty) => write!(f, "(mod {})", fty.modulus()),
|
||||
Sort::Array(k, v, n) => write!(f, "(array {} {} {})", k, v, n),
|
||||
Sort::Tuple(fields) => {
|
||||
write!(f, "(tuple")?;
|
||||
@@ -1154,7 +1115,7 @@ impl TermData {
|
||||
}
|
||||
}
|
||||
/// Get the underlying prime field constant, if possible.
|
||||
pub fn as_pf_opt(&self) -> Option<&FieldElem> {
|
||||
pub fn as_pf_opt(&self) -> Option<&FieldV> {
|
||||
if let Op::Const(Value::Field(b)) = &self.op {
|
||||
Some(b)
|
||||
} else {
|
||||
@@ -1205,7 +1166,7 @@ impl Value {
|
||||
pub fn sort(&self) -> Sort {
|
||||
match &self {
|
||||
Value::Bool(_) => Sort::Bool,
|
||||
Value::Field(f) => Sort::Field(f.modulus().clone()),
|
||||
Value::Field(f) => Sort::Field(f.ty()),
|
||||
Value::Int(_) => Sort::Int,
|
||||
Value::F64(_) => Sort::F64,
|
||||
Value::F32(_) => Sort::F32,
|
||||
@@ -1239,7 +1200,7 @@ impl Value {
|
||||
}
|
||||
#[track_caller]
|
||||
/// Get the underlying prime field constant, if possible.
|
||||
pub fn as_pf(&self) -> &FieldElem {
|
||||
pub fn as_pf(&self) -> &FieldV {
|
||||
if let Value::Field(b) = self {
|
||||
b
|
||||
} else {
|
||||
@@ -1383,9 +1344,9 @@ fn eval_value(vs: &mut TermMap<Value>, h: &FxHashMap<String, Value>, c: Term) ->
|
||||
BitVector::new(a.uint() | (mask << a.width() as u32), a.width() + w)
|
||||
}),
|
||||
Op::PfToBv(w) => Value::BitVector({
|
||||
let a = vs.get(&c.cs[0]).unwrap().as_pf().clone();
|
||||
assert!(a.i() < &(Integer::from(1) << 1));
|
||||
BitVector::new(a.i().clone(), *w)
|
||||
let i = vs.get(&c.cs[0]).unwrap().as_pf().i();
|
||||
assert!(i < (Integer::from(1) << *w as u32));
|
||||
BitVector::new(i, *w)
|
||||
}),
|
||||
Op::BvUext(w) => Value::BitVector({
|
||||
let a = vs.get(&c.cs[0]).unwrap().as_bv().clone();
|
||||
@@ -1434,10 +1395,7 @@ fn eval_value(vs: &mut TermMap<Value>, h: &FxHashMap<String, Value>, c: Term) ->
|
||||
},
|
||||
)
|
||||
}),
|
||||
Op::UbvToPf(m) => Value::Field({
|
||||
let a = vs.get(&c.cs[0]).unwrap().as_bv().clone();
|
||||
field::FieldElem::new(a.uint().clone(), m.clone())
|
||||
}),
|
||||
Op::UbvToPf(fty) => Value::Field(fty.new_v(vs.get(&c.cs[0]).unwrap().as_bv().uint())),
|
||||
// tuple
|
||||
Op::Tuple => Value::Tuple(c.cs.iter().map(|c| vs.get(c).unwrap().clone()).collect()),
|
||||
Op::Field(i) => {
|
||||
|
||||
@@ -60,7 +60,7 @@ fn map_test_bv_key() {
|
||||
vec![bv(0b0001, 4), bv(0b0100, 4), bv(0b1001, 4), bv(0b0000, 4)],
|
||||
);
|
||||
let actual_eq = term![Op::Map(Box::new(Op::Eq)); a1.clone(), a2.clone()];
|
||||
let actual_add = term![Op::Map(Box::new(BV_ADD)); a1.clone(), a2.clone()];
|
||||
let actual_add = term![Op::Map(Box::new(BV_ADD)); a1, a2];
|
||||
let expected_eq = make_array(
|
||||
Sort::BitVector(32),
|
||||
Sort::Bool,
|
||||
|
||||
@@ -30,11 +30,15 @@
|
||||
//! * let: `(let ((X1 T1) ... (Xn Tn)) T)`
|
||||
//! * declare: `(declare ((X1 S1) ... (Xn Sn)) T)`
|
||||
//! * set_default_modulus: `(set_default_modulus I T)`
|
||||
//! * set_default_modulus: `(O T1 ... TN)`
|
||||
//! * within term T, I will be the default field modulus
|
||||
//! * NB: after the closing paren, I is *no longer* the default modulus
|
||||
//! * operator: `(O T1 ... TN)`
|
||||
//! * Operator `O`:
|
||||
//! * Plain operators: (`bvmul`, `and`, ...)
|
||||
//! * Composite operators: `(field N)`, `(update N)`, `(sext N)`, `(uext N)`, `(bit N)`, ...
|
||||
|
||||
use circ_fields::{FieldT, FieldV};
|
||||
|
||||
use logos::Logos;
|
||||
|
||||
use fxhash::FxHashMap as HashMap;
|
||||
@@ -126,8 +130,10 @@ struct IrInterp<'src> {
|
||||
/// A map from an identifier to a stack of bindings.
|
||||
/// The stack is there for scoping.
|
||||
bindings: HashMap<&'src [u8], Vec<Term>>,
|
||||
/// The stack of default field moduli
|
||||
moduli: Vec<Arc<Integer>>,
|
||||
/// The stack of field moduli used in this IR
|
||||
int_arcs: Vec<Arc<Integer>>,
|
||||
/// The current default field modulus, if any
|
||||
modulus_stack: Vec<Arc<Integer>>,
|
||||
}
|
||||
|
||||
enum CtrlOp {
|
||||
@@ -141,8 +147,9 @@ enum CtrlOp {
|
||||
impl<'src> IrInterp<'src> {
|
||||
fn new() -> Self {
|
||||
Self {
|
||||
moduli: Vec::new(),
|
||||
bindings: HashMap::default(),
|
||||
int_arcs: Vec::new(),
|
||||
modulus_stack: Vec::new(),
|
||||
}
|
||||
}
|
||||
|
||||
@@ -248,7 +255,7 @@ impl<'src> IrInterp<'src> {
|
||||
[Leaf(Ident, b"ubv2fp"), a] => Ok(Op::UbvToFp(self.usize(a))),
|
||||
[Leaf(Ident, b"sbv2fp"), a] => Ok(Op::SbvToFp(self.usize(a))),
|
||||
[Leaf(Ident, b"fp2fp"), a] => Ok(Op::FpToFp(self.usize(a))),
|
||||
[Leaf(Ident, b"bv2pf"), a] => Ok(Op::UbvToPf(Arc::new(self.int(a)))),
|
||||
[Leaf(Ident, b"bv2pf"), a] => Ok(Op::UbvToPf(FieldT::from(self.int(a)))),
|
||||
[Leaf(Ident, b"field"), a] => Ok(Op::Field(self.usize(a))),
|
||||
[Leaf(Ident, b"update"), a] => Ok(Op::Update(self.usize(a))),
|
||||
_ => todo!("Unparsed op: {}", tt),
|
||||
@@ -273,7 +280,7 @@ impl<'src> IrInterp<'src> {
|
||||
List(ls) => {
|
||||
assert!(!ls.is_empty());
|
||||
match &ls[..] {
|
||||
[Leaf(Ident, b"mod"), m] => Sort::Field(Arc::new(self.int(m))),
|
||||
[Leaf(Ident, b"mod"), m] => Sort::Field(FieldT::from(self.int(m))),
|
||||
[Leaf(Ident, b"bv"), w] => Sort::BitVector(self.usize(w)),
|
||||
[Leaf(Ident, b"array"), k, v, s] => Sort::Array(
|
||||
Box::new(self.sort(k)),
|
||||
@@ -289,9 +296,21 @@ impl<'src> IrInterp<'src> {
|
||||
_ => panic!("Expected sort, found {}", tt),
|
||||
}
|
||||
}
|
||||
fn int(&self, tt: &TokTree) -> Integer {
|
||||
/// Parse this text as an integer, but check the ARC cache before creating a new one.
|
||||
fn parse_int(&mut self, s: &[u8]) -> Arc<Integer> {
|
||||
let i: Integer = Integer::parse(s).unwrap().into();
|
||||
match self.int_arcs.binary_search_by(|v| v.as_ref().cmp(&i)) {
|
||||
Ok(idx) => self.int_arcs[idx].clone(),
|
||||
Err(idx) => {
|
||||
let i = Arc::new(i);
|
||||
self.int_arcs.insert(idx, i.clone());
|
||||
i
|
||||
}
|
||||
}
|
||||
}
|
||||
fn int(&mut self, tt: &TokTree) -> Arc<Integer> {
|
||||
match tt {
|
||||
Leaf(Token::Int, s) => Integer::parse(s).unwrap().into(),
|
||||
Leaf(Token::Int, s) => self.parse_int(s),
|
||||
_ => panic!("Expected integer, got {}", tt),
|
||||
}
|
||||
}
|
||||
@@ -372,11 +391,11 @@ impl<'src> IrInterp<'src> {
|
||||
let (v, m) = if let Some(i) = s.iter().position(|b| *b == b'm') {
|
||||
(
|
||||
Integer::parse(&s[2..i]).unwrap().into(),
|
||||
Arc::new(Integer::parse(&s[i + 1..]).unwrap().into()),
|
||||
self.parse_int(&s[i + 1..]),
|
||||
)
|
||||
} else {
|
||||
let m = self
|
||||
.moduli
|
||||
.modulus_stack
|
||||
.last()
|
||||
.unwrap_or_else(|| {
|
||||
panic!("Field value without a modulus, and no default modulus set")
|
||||
@@ -384,7 +403,7 @@ impl<'src> IrInterp<'src> {
|
||||
.clone();
|
||||
(Integer::parse(&s[2..]).unwrap().into(), m)
|
||||
};
|
||||
leaf_term(Op::Const(Value::Field(FieldElem::new(v, m))))
|
||||
leaf_term(Op::Const(Value::Field(FieldV::new::<Integer>(v, m))))
|
||||
}
|
||||
Leaf(Ident, b"false") => bool_lit(false),
|
||||
Leaf(Ident, b"true") => bool_lit(true),
|
||||
@@ -440,10 +459,10 @@ impl<'src> IrInterp<'src> {
|
||||
3,
|
||||
"A set_default_modulus should have 2 arguments: modulus and term"
|
||||
);
|
||||
let m = Arc::new(self.int(&tts[1]));
|
||||
self.moduli.push(m);
|
||||
let m = self.int(&tts[1]);
|
||||
self.modulus_stack.push(m);
|
||||
let t = self.term(&tts[2]);
|
||||
self.moduli.pop().unwrap();
|
||||
self.modulus_stack.pop();
|
||||
t
|
||||
}
|
||||
Ok(o) => term(o, tts[1..].iter().map(|tti| self.term(tti)).collect()),
|
||||
@@ -582,4 +601,26 @@ mod test {
|
||||
let t2 = parse_term(s.as_bytes());
|
||||
assert_eq!(t, t2);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn set_default_modulus() {
|
||||
let t = parse_term(
|
||||
b"
|
||||
(set_default_modulus 7
|
||||
(and
|
||||
(=
|
||||
(set_default_modulus 11
|
||||
(+ #f1m11 #f5) ; well-type b/c default modulus
|
||||
)
|
||||
#f2m11
|
||||
)
|
||||
(=
|
||||
#f2 ; default modulus is now 7, so still well-typed
|
||||
#f2m7
|
||||
)
|
||||
)
|
||||
)",
|
||||
);
|
||||
assert_eq!(check_rec(&t), Sort::Bool);
|
||||
}
|
||||
}
|
||||
|
||||
@@ -290,7 +290,7 @@ pub fn rec_check_raw_helper(oper: &Op, a: &[&Sort]) -> Result<Sort, TypeErrorRea
|
||||
.and_then(|t| pf_or(t, ctx))
|
||||
.map(|a| a.clone())
|
||||
}
|
||||
(Op::UbvToPf(m), &[a]) => bv_or(a, "sbv-to-fp").map(|_| Sort::Field(m.clone())),
|
||||
(Op::UbvToPf(m), &[a]) => bv_or(a, "ubv-to-pf").map(|_| Sort::Field(m.clone())),
|
||||
(Op::PfUnOp(_), &[a]) => pf_or(a, "pf unary op").map(|a| a.clone()),
|
||||
(Op::Select, &[Sort::Array(k, v, _), a]) => eq_or(k, a, "select").map(|_| (**v).clone()),
|
||||
(Op::Store, &[Sort::Array(k, v, n), a, b]) => eq_or(k, a, "store")
|
||||
@@ -392,7 +392,6 @@ pub fn rec_check_raw(t: &Term) -> Result<Sort, TypeError> {
|
||||
.iter()
|
||||
.map(|c| term_tys.get(&c.to_weak()).unwrap())
|
||||
.collect::<Vec<_>>();
|
||||
|
||||
let ty =
|
||||
rec_check_raw_helper(&back.0.op, &tys[..]).map_err(|reason| TypeError {
|
||||
op: back.0.op.clone(),
|
||||
|
||||
@@ -1,6 +1,6 @@
|
||||
//! Exporting our R1CS to bellman
|
||||
use ::bellman::{Circuit, ConstraintSystem, LinearCombination, SynthesisError, Variable};
|
||||
use ff::{PrimeField, PrimeFieldBits};
|
||||
use ff::{Field, PrimeField};
|
||||
use gmp_mpfr_sys::gmp::limb_t;
|
||||
use log::debug;
|
||||
use std::collections::HashMap;
|
||||
@@ -9,10 +9,13 @@ use std::io::{BufRead, BufReader};
|
||||
use std::path::Path;
|
||||
use std::str::FromStr;
|
||||
|
||||
use rug::integer::{IsPrime, Order};
|
||||
use rug::Integer;
|
||||
|
||||
use super::*;
|
||||
|
||||
/// Convert a (rug) integer to a prime field element.
|
||||
fn int_to_ff<F: PrimeField>(i: &Integer) -> F {
|
||||
fn int_to_ff<F: PrimeField>(i: Integer) -> F {
|
||||
let mut accumulator = F::from(0);
|
||||
let limb_bits = (std::mem::size_of::<limb_t>() as u64) << 3;
|
||||
let limb_base = F::from(2).pow_vartime(&[limb_bits]);
|
||||
@@ -33,56 +36,66 @@ fn lc_to_bellman<F: PrimeField, CS: ConstraintSystem<F>>(
|
||||
) -> LinearCombination<F> {
|
||||
let mut lc_bellman = zero_lc;
|
||||
// This zero test is needed until https://github.com/zkcrypto/bellman/pull/78 is resolved
|
||||
if lc.constant != 0 {
|
||||
lc_bellman = lc_bellman + (int_to_ff(&lc.constant), CS::one());
|
||||
if !lc.constant.is_zero() {
|
||||
lc_bellman = lc_bellman + (int_to_ff((&lc.constant).into()), CS::one());
|
||||
}
|
||||
for (v, c) in &lc.monomials {
|
||||
// ditto
|
||||
if c != &0 {
|
||||
lc_bellman = lc_bellman + (int_to_ff(c), *vars.get(v).unwrap());
|
||||
if !c.is_zero() {
|
||||
lc_bellman = lc_bellman + (int_to_ff(c.into()), *vars.get(v).unwrap());
|
||||
}
|
||||
}
|
||||
lc_bellman
|
||||
}
|
||||
|
||||
fn modulus_as_int<F: PrimeFieldBits>() -> Integer {
|
||||
let mut bits = F::char_le_bits().to_bitvec();
|
||||
let mut acc = Integer::from(0);
|
||||
while let Some(b) = bits.pop() {
|
||||
acc <<= 1;
|
||||
acc += b as u8;
|
||||
// hmmm... this should work essentially all the time, I think
|
||||
fn get_modulus<F: Field + PrimeField>() -> Integer {
|
||||
let neg_1_f = -F::one();
|
||||
let p_lsf: Integer = Integer::from_digits(neg_1_f.to_repr().as_ref(), Order::Lsf) + 1;
|
||||
let p_msf: Integer = Integer::from_digits(neg_1_f.to_repr().as_ref(), Order::Msf) + 1;
|
||||
if p_lsf.is_probably_prime(30) != IsPrime::No {
|
||||
p_lsf
|
||||
} else if p_msf.is_probably_prime(30) != IsPrime::No {
|
||||
p_msf
|
||||
} else {
|
||||
panic!("could not determine ff::Field byte order")
|
||||
}
|
||||
acc
|
||||
}
|
||||
|
||||
impl<'a, F: PrimeField + PrimeFieldBits, S: Display + Eq + Hash + Ord> Circuit<F> for &'a R1cs<S> {
|
||||
impl<'a, F: PrimeField, S: Display + Eq + Hash + Ord> Circuit<F> for &'a R1cs<S> {
|
||||
#[track_caller]
|
||||
fn synthesize<CS>(self, cs: &mut CS) -> std::result::Result<(), SynthesisError>
|
||||
where
|
||||
CS: ConstraintSystem<F>,
|
||||
{
|
||||
let f_mod = modulus_as_int::<F>();
|
||||
let f_mod = get_modulus::<F>();
|
||||
assert_eq!(
|
||||
*self.modulus, f_mod,
|
||||
"\nR1CS has modulus \n{},\n but Bellman CS expectes \n{}",
|
||||
self.modulus, f_mod
|
||||
self.modulus.modulus(),
|
||||
&f_mod,
|
||||
"\nR1CS has modulus \n{},\n but Bellman CS expects \n{}",
|
||||
self.modulus,
|
||||
f_mod
|
||||
);
|
||||
let mut uses = self
|
||||
.idxs_signals
|
||||
.iter()
|
||||
.map(|(i, _)| (*i, 0))
|
||||
.collect::<HashMap<usize, usize>>();
|
||||
let mut uses = HashMap::with_capacity(self.next_idx);
|
||||
for (a, b, c) in self.constraints.iter() {
|
||||
[a, b, c].iter().for_each(|x| {
|
||||
x.monomials
|
||||
.iter()
|
||||
.for_each(|(i, _)| *uses.get_mut(i).unwrap() += 1)
|
||||
[a, b, c].iter().for_each(|y| {
|
||||
y.monomials.keys().for_each(|k| {
|
||||
uses.get_mut(k)
|
||||
.map(|i| {
|
||||
*i += 1;
|
||||
})
|
||||
.or_else(|| {
|
||||
uses.insert(*k, 1);
|
||||
None
|
||||
});
|
||||
})
|
||||
});
|
||||
}
|
||||
let mut vars = HashMap::default();
|
||||
let mut vars = HashMap::with_capacity(self.next_idx);
|
||||
for i in 0..self.next_idx {
|
||||
if let Some(s) = self.idxs_signals.get(&i) {
|
||||
//for (_i, s) in self.idxs_signals.get() {
|
||||
if uses.get(&i).unwrap() > &0 {
|
||||
if uses.get(&i).is_some() {
|
||||
let name_f = || format!("{}", s);
|
||||
let val_f = || {
|
||||
Ok({
|
||||
@@ -92,7 +105,7 @@ impl<'a, F: PrimeField + PrimeFieldBits, S: Display + Eq + Hash + Ord> Circuit<F
|
||||
.expect("missing values")
|
||||
.get(&i)
|
||||
.unwrap();
|
||||
let ff_val = int_to_ff(i_val);
|
||||
let ff_val = int_to_ff(i_val.into());
|
||||
debug!("value : {} -> {:?} ({})", s, ff_val, i_val);
|
||||
ff_val
|
||||
})
|
||||
@@ -134,7 +147,7 @@ pub fn parse_instance<P: AsRef<Path>, F: PrimeField>(path: P) -> Vec<F> {
|
||||
.map(|line| {
|
||||
let s = line.unwrap();
|
||||
let i = Integer::from_str(s.trim()).unwrap();
|
||||
int_to_ff(&i)
|
||||
int_to_ff(i)
|
||||
})
|
||||
.collect()
|
||||
}
|
||||
@@ -168,13 +181,13 @@ mod test {
|
||||
|
||||
#[quickcheck]
|
||||
fn int_to_ff_random(BlsScalar(i): BlsScalar) -> bool {
|
||||
let by_fn = int_to_ff::<Scalar>(&i);
|
||||
let by_fn = int_to_ff::<Scalar>(i.clone());
|
||||
let by_str = Scalar::from_str_vartime(&format!("{}", i)).unwrap();
|
||||
by_fn == by_str
|
||||
}
|
||||
|
||||
fn convert(i: Integer) {
|
||||
let by_fn = int_to_ff::<Scalar>(&i);
|
||||
let by_fn = int_to_ff::<Scalar>(i.clone());
|
||||
let by_str = Scalar::from_str_vartime(&format!("{}", i)).unwrap();
|
||||
assert_eq!(by_fn, by_str);
|
||||
}
|
||||
|
||||
@@ -1,13 +1,13 @@
|
||||
//! Rank 1 Constraint Systems
|
||||
|
||||
use circ_fields::{FieldT, FieldV};
|
||||
use fxhash::{FxHashMap as HashMap, FxHashSet as HashSet};
|
||||
use log::debug;
|
||||
use rug::ops::{RemRounding, RemRoundingAssign};
|
||||
use paste::paste;
|
||||
use rug::Integer;
|
||||
use std::collections::hash_map::Entry;
|
||||
use std::fmt::Display;
|
||||
use std::hash::Hash;
|
||||
use std::rc::Rc;
|
||||
|
||||
#[cfg(feature = "r1cs")]
|
||||
pub mod bellman;
|
||||
@@ -17,209 +17,167 @@ pub mod trans;
|
||||
#[derive(Clone, Debug)]
|
||||
/// A Rank 1 Constraint System.
|
||||
pub struct R1cs<S: Hash + Eq> {
|
||||
modulus: Rc<Integer>,
|
||||
modulus: FieldT,
|
||||
signal_idxs: HashMap<S, usize>,
|
||||
idxs_signals: HashMap<usize, S>,
|
||||
next_idx: usize,
|
||||
public_idxs: HashSet<usize>,
|
||||
values: Option<HashMap<usize, Integer>>,
|
||||
values: Option<HashMap<usize, FieldV>>,
|
||||
constraints: Vec<(Lc, Lc, Lc)>,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
/// A linear combination
|
||||
pub struct Lc {
|
||||
modulus: Rc<Integer>,
|
||||
constant: Integer,
|
||||
monomials: HashMap<usize, Integer>,
|
||||
modulus: FieldT,
|
||||
constant: FieldV,
|
||||
monomials: HashMap<usize, FieldV>,
|
||||
}
|
||||
|
||||
impl Lc {
|
||||
/// Is this the zero combination?
|
||||
pub fn is_zero(&self) -> bool {
|
||||
self.monomials.is_empty() && self.constant == 0
|
||||
self.monomials.is_empty() && self.constant.is_zero()
|
||||
}
|
||||
/// Make this the zero combination.
|
||||
pub fn clear(&mut self) {
|
||||
self.monomials.clear();
|
||||
self.constant = Integer::from(0);
|
||||
self.constant = self.modulus.zero();
|
||||
}
|
||||
/// Take this linear combination, leaving zero in its place.
|
||||
pub fn take(&mut self) -> Self {
|
||||
let monomials = std::mem::take(&mut self.monomials);
|
||||
let constant = std::mem::take(&mut self.constant);
|
||||
let constant = std::mem::replace(&mut self.constant, self.modulus.zero());
|
||||
Self {
|
||||
monomials,
|
||||
constant,
|
||||
modulus: self.modulus.clone(),
|
||||
constant,
|
||||
monomials,
|
||||
}
|
||||
}
|
||||
/// Is this a constant? If so, return that constant.
|
||||
pub fn as_const(&self) -> Option<&Integer> {
|
||||
pub fn as_const(&self) -> Option<&FieldV> {
|
||||
self.monomials.is_empty().then(|| &self.constant)
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::Add<&Lc> for Lc {
|
||||
type Output = Lc;
|
||||
fn add(mut self, other: &Lc) -> Lc {
|
||||
self += other;
|
||||
self
|
||||
}
|
||||
}
|
||||
macro_rules! arith_impl {
|
||||
($Trait: ident, $fn: ident) => {
|
||||
paste! {
|
||||
impl $Trait<&Lc> for Lc {
|
||||
type Output = Self;
|
||||
fn $fn(mut self, other: &Self) -> Self {
|
||||
self.[<$fn _assign>](other);
|
||||
self
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::AddAssign<&Lc> for Lc {
|
||||
fn add_assign(&mut self, other: &Lc) {
|
||||
assert_eq!(&self.modulus, &other.modulus);
|
||||
self.constant += &other.constant;
|
||||
self.constant.rem_floor_assign(&*self.modulus);
|
||||
for (i, v) in &other.monomials {
|
||||
match self.monomials.entry(*i) {
|
||||
Entry::Occupied(mut e) => {
|
||||
let m = e.get_mut();
|
||||
*m += v;
|
||||
m.rem_floor_assign(&*other.modulus);
|
||||
if e.get() == &Integer::from(0) {
|
||||
e.remove_entry();
|
||||
impl [<$Trait Assign>]<&Lc> for Lc {
|
||||
fn [<$fn _assign>](&mut self, other: &Self) {
|
||||
assert_eq!(&self.modulus, &other.modulus);
|
||||
self.constant.[<$fn _assign>](&other.constant);
|
||||
let tot = self.monomials.len() + other.monomials.len();
|
||||
if tot > self.monomials.capacity() {
|
||||
self.monomials.reserve(tot - self.monomials.capacity());
|
||||
}
|
||||
for (i, v) in &other.monomials {
|
||||
match self.monomials.entry(*i) {
|
||||
Entry::Occupied(mut e) => {
|
||||
e.get_mut().[<$fn _assign>](v);
|
||||
if e.get().is_zero() {
|
||||
e.remove_entry();
|
||||
}
|
||||
}
|
||||
Entry::Vacant(e) => {
|
||||
let mut m = self.modulus.zero();
|
||||
m.[<$fn _assign>](v);
|
||||
e.insert(m);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
Entry::Vacant(e) => {
|
||||
e.insert(v.clone());
|
||||
}
|
||||
|
||||
impl $Trait<&FieldV> for Lc {
|
||||
type Output = Self;
|
||||
fn $fn(mut self, other: &FieldV) -> Self {
|
||||
self.[<$fn _assign>](other);
|
||||
self
|
||||
}
|
||||
}
|
||||
|
||||
impl [<$Trait Assign>]<&FieldV> for Lc {
|
||||
fn [<$fn _assign>](&mut self, other: &FieldV) {
|
||||
self.constant.[<$fn _assign>](other);
|
||||
}
|
||||
}
|
||||
|
||||
impl [<$Trait Assign>]<FieldV> for Lc {
|
||||
fn [<$fn _assign>](&mut self, other: FieldV) {
|
||||
self.[<$fn _assign>](&other);
|
||||
}
|
||||
}
|
||||
|
||||
impl $Trait<isize> for Lc {
|
||||
type Output = Self;
|
||||
fn $fn(mut self, other: isize) -> Self {
|
||||
self.[<$fn _assign>](other);
|
||||
self
|
||||
}
|
||||
}
|
||||
|
||||
impl [<$Trait Assign>]<isize> for Lc {
|
||||
fn [<$fn _assign>](&mut self, other: isize) {
|
||||
self.constant.[<$fn _assign>](self.modulus.new_v(other));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
impl std::ops::Add<&Integer> for Lc {
|
||||
type Output = Lc;
|
||||
fn add(mut self, other: &Integer) -> Lc {
|
||||
self += other;
|
||||
self
|
||||
}
|
||||
}
|
||||
use std::ops::{Add, AddAssign, Mul, MulAssign, Neg, Sub, SubAssign};
|
||||
|
||||
impl std::ops::AddAssign<&Integer> for Lc {
|
||||
fn add_assign(&mut self, other: &Integer) {
|
||||
self.constant += other;
|
||||
self.constant.rem_floor_assign(&*self.modulus);
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::Add<isize> for Lc {
|
||||
type Output = Lc;
|
||||
fn add(mut self, other: isize) -> Lc {
|
||||
self += other;
|
||||
self
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::AddAssign<isize> for Lc {
|
||||
fn add_assign(&mut self, other: isize) {
|
||||
self.constant += Integer::from(other);
|
||||
self.constant.rem_floor_assign(&*self.modulus);
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::Sub<&Lc> for Lc {
|
||||
type Output = Lc;
|
||||
fn sub(mut self, other: &Lc) -> Lc {
|
||||
self -= other;
|
||||
self
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::SubAssign<&Lc> for Lc {
|
||||
fn sub_assign(&mut self, other: &Lc) {
|
||||
assert_eq!(&self.modulus, &other.modulus);
|
||||
self.constant -= &other.constant;
|
||||
self.constant.rem_floor_assign(&*self.modulus);
|
||||
for (i, v) in &other.monomials {
|
||||
match self.monomials.entry(*i) {
|
||||
Entry::Occupied(mut e) => {
|
||||
let m = e.get_mut();
|
||||
*m -= v;
|
||||
m.rem_floor_assign(&*other.modulus);
|
||||
if e.get() == &Integer::from(0) {
|
||||
e.remove_entry();
|
||||
}
|
||||
}
|
||||
Entry::Vacant(e) => {
|
||||
let m = e.insert(-v.clone());
|
||||
m.rem_floor_assign(&*other.modulus);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::Sub<&Integer> for Lc {
|
||||
type Output = Lc;
|
||||
fn sub(mut self, other: &Integer) -> Lc {
|
||||
self -= other;
|
||||
self
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::SubAssign<&Integer> for Lc {
|
||||
fn sub_assign(&mut self, other: &Integer) {
|
||||
self.constant -= other;
|
||||
self.constant.rem_floor_assign(&*self.modulus);
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::Sub<isize> for Lc {
|
||||
type Output = Lc;
|
||||
fn sub(mut self, other: isize) -> Lc {
|
||||
self -= other;
|
||||
self
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::SubAssign<isize> for Lc {
|
||||
fn sub_assign(&mut self, other: isize) {
|
||||
self.constant -= Integer::from(other);
|
||||
self.constant.rem_floor_assign(&*self.modulus);
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::Neg for Lc {
|
||||
impl Neg for Lc {
|
||||
type Output = Lc;
|
||||
fn neg(mut self) -> Lc {
|
||||
self.constant = -self.constant;
|
||||
self.constant.rem_floor_assign(&*self.modulus);
|
||||
for v in &mut self.monomials.values_mut() {
|
||||
*v *= Integer::from(-1);
|
||||
v.rem_floor_assign(&*self.modulus);
|
||||
*v = -v.clone();
|
||||
}
|
||||
self
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::Mul<&Integer> for Lc {
|
||||
arith_impl! {Add, add}
|
||||
arith_impl! {Sub, sub}
|
||||
|
||||
impl Mul<&FieldV> for Lc {
|
||||
type Output = Lc;
|
||||
fn mul(mut self, other: &Integer) -> Lc {
|
||||
fn mul(mut self, other: &FieldV) -> Lc {
|
||||
self *= other;
|
||||
self
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::MulAssign<&Integer> for Lc {
|
||||
fn mul_assign(&mut self, other: &Integer) {
|
||||
impl MulAssign<FieldV> for Lc {
|
||||
fn mul_assign(&mut self, other: FieldV) {
|
||||
self.mul_assign(&other);
|
||||
}
|
||||
}
|
||||
|
||||
impl MulAssign<&FieldV> for Lc {
|
||||
fn mul_assign(&mut self, other: &FieldV) {
|
||||
self.constant *= other;
|
||||
self.constant.rem_floor_assign(&*self.modulus);
|
||||
if other == &Integer::from(0) {
|
||||
if other.is_zero() {
|
||||
self.monomials.clear();
|
||||
} else {
|
||||
for v in &mut self.monomials.values_mut() {
|
||||
*v *= other;
|
||||
v.rem_floor_assign(&*self.modulus);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::Mul<isize> for Lc {
|
||||
impl Mul<isize> for Lc {
|
||||
type Output = Lc;
|
||||
fn mul(mut self, other: isize) -> Lc {
|
||||
self *= other;
|
||||
@@ -227,27 +185,18 @@ impl std::ops::Mul<isize> for Lc {
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::MulAssign<isize> for Lc {
|
||||
impl MulAssign<isize> for Lc {
|
||||
fn mul_assign(&mut self, other: isize) {
|
||||
self.constant *= Integer::from(other);
|
||||
self.constant.rem_floor_assign(&*self.modulus);
|
||||
if other == 0 {
|
||||
self.monomials.clear();
|
||||
} else {
|
||||
for v in &mut self.monomials.values_mut() {
|
||||
*v *= Integer::from(other);
|
||||
v.rem_floor_assign(&*self.modulus);
|
||||
}
|
||||
}
|
||||
self.mul_assign(self.modulus.new_v(other));
|
||||
}
|
||||
}
|
||||
|
||||
impl<S: Clone + Hash + Eq + Display> R1cs<S> {
|
||||
/// Make an empty constraint system, mod `modulus`.
|
||||
/// If `values`, then this constraint system will track & expect concrete values.
|
||||
pub fn new(modulus: Integer, values: bool) -> Self {
|
||||
pub fn new(modulus: FieldT, values: bool) -> Self {
|
||||
R1cs {
|
||||
modulus: Rc::new(modulus),
|
||||
modulus,
|
||||
signal_idxs: HashMap::default(),
|
||||
idxs_signals: HashMap::default(),
|
||||
next_idx: 0,
|
||||
@@ -264,7 +213,17 @@ impl<S: Clone + Hash + Eq + Display> R1cs<S> {
|
||||
pub fn zero(&self) -> Lc {
|
||||
Lc {
|
||||
modulus: self.modulus.clone(),
|
||||
constant: Integer::from(0),
|
||||
constant: self.modulus.zero(),
|
||||
monomials: HashMap::default(),
|
||||
}
|
||||
}
|
||||
/// Get a constant constraint for this system.
|
||||
#[track_caller]
|
||||
pub fn constant(&self, c: FieldV) -> Lc {
|
||||
assert_eq!(c.ty(), self.modulus);
|
||||
Lc {
|
||||
modulus: self.modulus.clone(),
|
||||
constant: c,
|
||||
monomials: HashMap::default(),
|
||||
}
|
||||
}
|
||||
@@ -275,12 +234,12 @@ impl<S: Clone + Hash + Eq + Display> R1cs<S> {
|
||||
.get(s)
|
||||
.expect("Missing signal in signal_lc");
|
||||
let mut lc = self.zero();
|
||||
lc.monomials.insert(*idx, Integer::from(1));
|
||||
lc.monomials.insert(*idx, self.modulus.new_v(1));
|
||||
lc
|
||||
}
|
||||
/// Create a new wire, `s`. If this system is tracking concrete values, you must provide the
|
||||
/// value, `v`.
|
||||
pub fn add_signal(&mut self, s: S, v: Option<Integer>) {
|
||||
pub fn add_signal(&mut self, s: S, v: Option<FieldV>) {
|
||||
let n = self.next_idx;
|
||||
self.next_idx += 1;
|
||||
self.signal_idxs.insert(s.clone(), n);
|
||||
@@ -321,25 +280,28 @@ impl<S: Clone + Hash + Eq + Display> R1cs<S> {
|
||||
/// Get a nice string represenation of the combination `a`.
|
||||
pub fn format_lc(&self, a: &Lc) -> String {
|
||||
let mut s = String::new();
|
||||
|
||||
let half_m: Integer = self.modulus().clone() / 2;
|
||||
let abs = |i: &Integer| {
|
||||
if i < &half_m {
|
||||
i.clone()
|
||||
let abs = |i: Integer| {
|
||||
if i <= half_m {
|
||||
i
|
||||
} else {
|
||||
self.modulus() - i.clone()
|
||||
self.modulus() - i
|
||||
}
|
||||
};
|
||||
let sign = |i: &Integer| if i < &half_m { "+" } else { "-" };
|
||||
let format_i = |i: &Integer| format!("{}{}", sign(i), abs(i));
|
||||
let format_i = |i: &FieldV| {
|
||||
let ii: Integer = i.into();
|
||||
format!("{}{}", sign(&ii), abs(ii))
|
||||
};
|
||||
|
||||
s.push_str(&format_i(&Integer::from(&a.constant)));
|
||||
s.push_str(&format_i(&a.constant));
|
||||
for (idx, coeff) in &a.monomials {
|
||||
s.extend(
|
||||
format!(
|
||||
" {} {}{}",
|
||||
sign(coeff),
|
||||
abs(coeff),
|
||||
" {} {}",
|
||||
self.idxs_signals.get(idx).unwrap(),
|
||||
format_i(coeff),
|
||||
)
|
||||
.chars(),
|
||||
);
|
||||
@@ -362,7 +324,7 @@ impl<S: Clone + Hash + Eq + Display> R1cs<S> {
|
||||
let av = self.eval(a).unwrap();
|
||||
let bv = self.eval(b).unwrap();
|
||||
let cv = self.eval(c).unwrap();
|
||||
if (av.clone() * &bv).rem_floor(&*self.modulus) != cv {
|
||||
if (av.clone() * &bv) != cv {
|
||||
panic!(
|
||||
"Error! Bad constraint:\n {} (value {})\n * {} (value {})\n = {} (value {})",
|
||||
self.format_lc(a),
|
||||
@@ -375,8 +337,8 @@ impl<S: Clone + Hash + Eq + Display> R1cs<S> {
|
||||
}
|
||||
}
|
||||
|
||||
fn eval(&self, lc: &Lc) -> Option<Integer> {
|
||||
self.values.as_ref().map(|values| {
|
||||
fn eval(&self, lc: &Lc) -> Option<FieldV> {
|
||||
let ret = self.values.as_ref().map(|values| {
|
||||
let mut acc = lc.constant.clone();
|
||||
for (var, coeff) in &lc.monomials {
|
||||
let val = values
|
||||
@@ -384,13 +346,13 @@ impl<S: Clone + Hash + Eq + Display> R1cs<S> {
|
||||
.expect("Missing value in R1cs::eval")
|
||||
.clone();
|
||||
acc += val * coeff;
|
||||
acc.rem_floor_assign(&*self.modulus);
|
||||
}
|
||||
acc
|
||||
})
|
||||
});
|
||||
ret
|
||||
}
|
||||
fn modulus(&self) -> &Integer {
|
||||
&self.modulus
|
||||
self.modulus.modulus()
|
||||
}
|
||||
|
||||
/// Check all assertions, if values are being tracked.
|
||||
|
||||
@@ -8,37 +8,46 @@ struct LinReducer<S: Eq + Hash> {
|
||||
r1cs: R1cs<S>,
|
||||
uses: HashMap<usize, HashSet<usize>>,
|
||||
queue: OnceQueue<usize>,
|
||||
/// The maximum size LC (number of non-constant monomials)
|
||||
/// that will be used for propagation
|
||||
lc_size_thresh: usize,
|
||||
}
|
||||
|
||||
impl<S: Eq + Hash + Display + Clone> LinReducer<S> {
|
||||
fn new(mut r1cs: R1cs<S>) -> Self {
|
||||
let sigs: HashSet<usize> = r1cs
|
||||
.constraints
|
||||
.iter()
|
||||
.flat_map(|(a, b, c)| {
|
||||
a.monomials
|
||||
.keys()
|
||||
.chain(b.monomials.keys().chain(c.monomials.keys()))
|
||||
})
|
||||
.cloned()
|
||||
.collect();
|
||||
let mut uses: HashMap<usize, HashSet<usize>> =
|
||||
sigs.into_iter().map(|i| (i, HashSet::default())).collect();
|
||||
for (i, (a, b, c)) in r1cs.constraints.iter().enumerate() {
|
||||
let mut add = |y: &Lc| {
|
||||
for x in y.monomials.keys() {
|
||||
uses.get_mut(x).unwrap().insert(i);
|
||||
}
|
||||
};
|
||||
add(a);
|
||||
add(b);
|
||||
add(c);
|
||||
}
|
||||
fn new(mut r1cs: R1cs<S>, lc_size_thresh: usize) -> Self {
|
||||
let uses = LinReducer::gen_uses(&r1cs);
|
||||
let queue = (0..r1cs.constraints.len()).collect::<OnceQueue<usize>>();
|
||||
for c in &mut r1cs.constraints {
|
||||
normalize(c);
|
||||
}
|
||||
Self { r1cs, uses, queue }
|
||||
Self {
|
||||
r1cs,
|
||||
uses,
|
||||
queue,
|
||||
lc_size_thresh,
|
||||
}
|
||||
}
|
||||
|
||||
// generate a new uses hash
|
||||
fn gen_uses(r1cs: &R1cs<S>) -> HashMap<usize, HashSet<usize>> {
|
||||
let mut uses: HashMap<usize, HashSet<usize>> =
|
||||
HashMap::with_capacity_and_hasher(r1cs.next_idx, Default::default());
|
||||
let mut add = |i: usize, y: &Lc| {
|
||||
for x in y.monomials.keys() {
|
||||
uses.get_mut(x).map(|m| m.insert(i)).or_else(|| {
|
||||
let mut m: HashSet<usize> = Default::default();
|
||||
m.insert(i);
|
||||
uses.insert(*x, m);
|
||||
None
|
||||
});
|
||||
}
|
||||
};
|
||||
for (i, (a, b, c)) in r1cs.constraints.iter().enumerate() {
|
||||
add(i, a);
|
||||
add(i, b);
|
||||
add(i, c);
|
||||
}
|
||||
uses
|
||||
}
|
||||
|
||||
/// Substitute `val` for `var` in constraint with id `con_id`.
|
||||
@@ -49,22 +58,24 @@ impl<S: Eq + Hash + Display + Clone> LinReducer<S> {
|
||||
let uses = &mut self.uses;
|
||||
let mut do_in = |a: &mut Lc| {
|
||||
if let Some(sc) = a.monomials.remove(&var) {
|
||||
a.constant += val.constant.clone() * ≻
|
||||
a.constant.rem_floor_assign(&*val.modulus);
|
||||
assert_eq!(&a.modulus, &val.modulus);
|
||||
a.constant += sc.clone() * &val.constant;
|
||||
let tot = a.monomials.len() + val.monomials.len();
|
||||
if tot > a.monomials.capacity() {
|
||||
a.monomials.reserve(tot - a.monomials.capacity());
|
||||
}
|
||||
for (i, v) in &val.monomials {
|
||||
match a.monomials.entry(*i) {
|
||||
Entry::Occupied(mut e) => {
|
||||
let m = e.get_mut();
|
||||
*m += v.clone() * ≻
|
||||
m.rem_floor_assign(&*val.modulus);
|
||||
if e.get() == &Integer::from(0) {
|
||||
*m += sc.clone() * v;
|
||||
if e.get().is_zero() {
|
||||
uses.get_mut(i).unwrap().remove(&con_id);
|
||||
e.remove_entry();
|
||||
}
|
||||
}
|
||||
Entry::Vacant(e) => {
|
||||
let m = e.insert(v.clone() * &sc);
|
||||
m.rem_floor_assign(&*val.modulus);
|
||||
e.insert(sc.clone() * v);
|
||||
uses.get_mut(i).unwrap().insert(con_id);
|
||||
}
|
||||
}
|
||||
@@ -105,21 +116,23 @@ impl<S: Eq + Hash + Display + Clone> LinReducer<S> {
|
||||
if let Some((var, lc)) =
|
||||
as_linear_sub(&self.r1cs.constraints[con_id], &self.r1cs.public_idxs)
|
||||
{
|
||||
debug!(
|
||||
"Elim: {} -> {}",
|
||||
self.r1cs.idxs_signals.get(&var).unwrap(),
|
||||
self.r1cs.format_lc(&lc)
|
||||
);
|
||||
self.clear_constraint(con_id);
|
||||
for use_id in self.uses[&var].clone() {
|
||||
if self.sub_in(var, &lc, use_id)
|
||||
&& (self.r1cs.constraints[use_id].0.is_zero()
|
||||
|| self.r1cs.constraints[use_id].1.is_zero())
|
||||
{
|
||||
self.queue.push(use_id);
|
||||
if lc.monomials.len() < self.lc_size_thresh {
|
||||
debug!(
|
||||
"Elim: {} -> {}",
|
||||
self.r1cs.idxs_signals.get(&var).unwrap(),
|
||||
self.r1cs.format_lc(&lc)
|
||||
);
|
||||
self.clear_constraint(con_id);
|
||||
for use_id in self.uses[&var].clone() {
|
||||
if self.sub_in(var, &lc, use_id)
|
||||
&& (self.r1cs.constraints[use_id].0.is_zero()
|
||||
|| self.r1cs.constraints[use_id].1.is_zero())
|
||||
{
|
||||
self.queue.push(use_id);
|
||||
}
|
||||
}
|
||||
debug_assert_eq!(0, self.uses[&var].len());
|
||||
}
|
||||
debug_assert_eq!(0, self.uses[&var].len());
|
||||
}
|
||||
}
|
||||
self.r1cs.constraints.retain(|c| !constantly_true(c));
|
||||
@@ -133,8 +146,8 @@ fn as_linear_sub((a, b, c): &(Lc, Lc, Lc), public: &HashSet<usize>) -> Option<(u
|
||||
if !public.contains(i) {
|
||||
let mut lc = c.clone();
|
||||
let v = lc.monomials.remove(i).unwrap();
|
||||
lc *= &(-v.invert(&*lc.modulus).unwrap());
|
||||
return Some((*i, lc));
|
||||
lc *= v.recip();
|
||||
return Some((*i, -lc));
|
||||
}
|
||||
}
|
||||
None
|
||||
@@ -159,14 +172,22 @@ fn normalize((a, b, c): &mut (Lc, Lc, Lc)) {
|
||||
|
||||
fn constantly_true((a, b, c): &(Lc, Lc, Lc)) -> bool {
|
||||
match (a.as_const(), b.as_const(), c.as_const()) {
|
||||
(Some(x), Some(y), Some(z)) => (x.clone() * y - z).rem_floor(&*a.modulus) == 0,
|
||||
(Some(x), Some(y), Some(z)) => (x.clone() * y - z).is_zero(),
|
||||
_ => false,
|
||||
}
|
||||
}
|
||||
|
||||
/// Attempt to shrink this system by reducing linearities.
|
||||
pub fn reduce_linearities<S: Eq + Hash + Clone + Display>(r1cs: R1cs<S>) -> R1cs<S> {
|
||||
LinReducer::new(r1cs).run()
|
||||
///
|
||||
/// ## Parameters
|
||||
///
|
||||
/// * `lc_size_thresh`: the maximum size LC (number of non-constant monomials) that will be used
|
||||
/// for propagation. `None` means no size limit.
|
||||
pub fn reduce_linearities<S: Eq + Hash + Clone + Display>(
|
||||
r1cs: R1cs<S>,
|
||||
lc_size_thresh: Option<usize>,
|
||||
) -> R1cs<S> {
|
||||
LinReducer::new(r1cs, lc_size_thresh.unwrap_or(usize::MAX)).run()
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
@@ -176,6 +197,7 @@ mod test {
|
||||
|
||||
use quickcheck::{Arbitrary, Gen};
|
||||
use quickcheck_macros::quickcheck;
|
||||
use rand::SeedableRng;
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct SatR1cs(R1cs<String>);
|
||||
@@ -183,33 +205,28 @@ mod test {
|
||||
impl Arbitrary for SatR1cs {
|
||||
fn arbitrary(g: &mut Gen) -> Self {
|
||||
let m = 101;
|
||||
let modulus = Integer::from(m);
|
||||
let modulus = FieldT::from(Integer::from(m));
|
||||
let n_vars = g.size() + 1;
|
||||
let vars: Vec<_> = (0..n_vars).map(|i| format!("v{}", i)).collect();
|
||||
let mut r1cs = R1cs::new(modulus.clone(), true);
|
||||
let mut rug_rng = rug::rand::RandState::new_mersenne_twister();
|
||||
let s: u32 = Arbitrary::arbitrary(g);
|
||||
rug_rng.seed(&Integer::from(s));
|
||||
let mut rng = rand::rngs::StdRng::seed_from_u64(u64::arbitrary(g));
|
||||
for v in &vars {
|
||||
r1cs.add_signal(v.clone(), Some(modulus.clone().random_below(&mut rug_rng)));
|
||||
r1cs.add_signal(v.clone(), Some(modulus.random_v(&mut rng)));
|
||||
}
|
||||
for _ in 0..(2 * g.size()) {
|
||||
let mut ac: isize = Arbitrary::arbitrary(g);
|
||||
ac.rem_floor_assign(m);
|
||||
let ac: isize = <isize as Arbitrary>::arbitrary(g) % m;
|
||||
let a = if Arbitrary::arbitrary(g) {
|
||||
r1cs.signal_lc(g.choose(&vars[..]).unwrap())
|
||||
} else {
|
||||
r1cs.zero()
|
||||
} + ac;
|
||||
let mut bc: isize = Arbitrary::arbitrary(g);
|
||||
bc.rem_floor_assign(m);
|
||||
let bc: isize = <isize as Arbitrary>::arbitrary(g) % m;
|
||||
let b = if Arbitrary::arbitrary(g) {
|
||||
r1cs.signal_lc(g.choose(&vars[..]).unwrap())
|
||||
} else {
|
||||
r1cs.zero()
|
||||
} + bc;
|
||||
let mut cc: isize = Arbitrary::arbitrary(g);
|
||||
cc.rem_floor_assign(m);
|
||||
let cc: isize = <isize as Arbitrary>::arbitrary(g) % m;
|
||||
let mut c = if Arbitrary::arbitrary(g) {
|
||||
r1cs.signal_lc(g.choose(&vars[..]).unwrap())
|
||||
} else {
|
||||
@@ -233,7 +250,7 @@ mod test {
|
||||
|
||||
#[quickcheck]
|
||||
fn random(SatR1cs(r1cs): SatR1cs) {
|
||||
let r1cs2 = reduce_linearities(r1cs);
|
||||
let r1cs2 = reduce_linearities(r1cs, None);
|
||||
r1cs2.check_all();
|
||||
}
|
||||
}
|
||||
|
||||
@@ -8,6 +8,7 @@ use crate::ir::term::*;
|
||||
use crate::target::bitsize;
|
||||
use crate::target::r1cs::*;
|
||||
|
||||
use circ_fields::{FieldT, FieldV};
|
||||
use fxhash::{FxHashMap, FxHashSet};
|
||||
use log::debug;
|
||||
use rug::ops::Pow;
|
||||
@@ -43,7 +44,7 @@ struct ToR1cs {
|
||||
|
||||
impl ToR1cs {
|
||||
fn new(
|
||||
modulus: Integer,
|
||||
modulus: FieldT,
|
||||
values: Option<FxHashMap<String, Value>>,
|
||||
public_inputs: FxHashSet<String>,
|
||||
) -> Self {
|
||||
@@ -61,7 +62,7 @@ impl ToR1cs {
|
||||
fn fresh_var<D: Display + ?Sized>(
|
||||
&mut self,
|
||||
ctx: &D,
|
||||
value: Option<Integer>,
|
||||
value: Option<FieldV>,
|
||||
public: bool,
|
||||
) -> Lc {
|
||||
let n = format!("{}_n{}", ctx, self.next_idx);
|
||||
@@ -80,7 +81,7 @@ impl ToR1cs {
|
||||
|
||||
/// Get a new bit-valued variable, with name dependent on `d`.
|
||||
/// If values are being recorded, `value` must be provided.
|
||||
fn fresh_bit<D: Display + ?Sized>(&mut self, ctx: &D, value: Option<Integer>) -> Lc {
|
||||
fn fresh_bit<D: Display + ?Sized>(&mut self, ctx: &D, value: Option<FieldV>) -> Lc {
|
||||
let v = self.fresh_var(ctx, value, false);
|
||||
//debug!("Fresh bit: {}", self.r1cs.format_lc(&v));
|
||||
self.enforce_bit(v.clone());
|
||||
@@ -94,17 +95,19 @@ impl ToR1cs {
|
||||
let m = self.fresh_var(
|
||||
"is_zero_inv",
|
||||
self.r1cs.eval(&x).map(|x| {
|
||||
if x == 0 {
|
||||
Integer::from(0)
|
||||
if x.is_zero() {
|
||||
self.r1cs.modulus.zero()
|
||||
} else {
|
||||
x.invert(self.r1cs.modulus()).unwrap()
|
||||
x.recip()
|
||||
}
|
||||
}),
|
||||
false,
|
||||
);
|
||||
let is_zero = self.fresh_var(
|
||||
"is_zero",
|
||||
self.r1cs.eval(&x).map(|x| Integer::from(x == 0)),
|
||||
self.r1cs
|
||||
.eval(&x)
|
||||
.map(|x| self.r1cs.modulus.new_v(x.is_zero())),
|
||||
false,
|
||||
);
|
||||
self.r1cs.constraint(m, x.clone(), -is_zero.clone() + 1);
|
||||
@@ -124,36 +127,36 @@ impl ToR1cs {
|
||||
|
||||
/// Evaluate `var`'s value as an (integer-casted) boolean.
|
||||
/// Returns `None` if values are not stored.
|
||||
fn eval_bool(&self, var: &str) -> Option<Integer> {
|
||||
fn eval_bool(&self, var: &str) -> Option<FieldV> {
|
||||
self.values
|
||||
.as_ref()
|
||||
.map(|vs| match vs.get(var).expect("missing value") {
|
||||
Value::Bool(b) => Integer::from(*b),
|
||||
Value::Bool(b) => self.r1cs.modulus.new_v(*b),
|
||||
v => panic!("{} should be a bool, but is {:?}", var, v),
|
||||
})
|
||||
}
|
||||
|
||||
/// Evaluate `var`'s value as an (integer-casted) bit-vector.
|
||||
/// Returns `None` if values are not stored.
|
||||
fn eval_bv(&self, var: &str) -> Option<Integer> {
|
||||
fn eval_bv(&self, var: &str) -> Option<FieldV> {
|
||||
self.values.as_ref().map(|vs| {
|
||||
match vs
|
||||
.get(var)
|
||||
.unwrap_or_else(|| panic!("missing value for {}", var))
|
||||
{
|
||||
Value::BitVector(b) => b.uint().clone(),
|
||||
Value::BitVector(b) => self.r1cs.modulus.new_v(b.uint()),
|
||||
v => panic!("{} should be a bit-vector, but is {:?}", var, v),
|
||||
}
|
||||
})
|
||||
}
|
||||
|
||||
/// Evaluate `var`'s value as an (integer-casted) field element
|
||||
/// Evaluate `var`'s value as a field element
|
||||
/// Returns `None` if values are not stored.
|
||||
fn eval_pf(&self, var: &str) -> Option<Integer> {
|
||||
fn eval_pf(&self, var: &str) -> Option<FieldV> {
|
||||
self.values
|
||||
.as_ref()
|
||||
.map(|vs| match vs.get(var).expect("missing value") {
|
||||
Value::Field(b) => b.i().clone(),
|
||||
Value::Field(b) => b.as_ty_ref(&self.r1cs.modulus),
|
||||
v => panic!("{} should be a field element, but is {:?}", var, v),
|
||||
})
|
||||
}
|
||||
@@ -163,13 +166,15 @@ impl ToR1cs {
|
||||
/// They have values according the the (infinite) two's complement representation of `x`.
|
||||
/// The LSB is at index 0.
|
||||
fn decomp<D: Display + ?Sized>(&mut self, d: &D, x: &Lc, n: usize) -> Vec<Lc> {
|
||||
let x_val = self.r1cs.eval(x);
|
||||
(0..n)
|
||||
let x_val: Option<Integer> = self.r1cs.eval(x).map(|x| x.into());
|
||||
(0..n as u32)
|
||||
.map(|i| {
|
||||
self.fresh_bit(
|
||||
// We get the right repr here because of infinite two's complement.
|
||||
&format!("{}_b{}", d, i),
|
||||
x_val.as_ref().map(|x| Integer::from(x.get_bit(i as u32))),
|
||||
x_val
|
||||
.as_ref()
|
||||
.map(|x| self.r1cs.modulus.new_v(x.get_bit(i))),
|
||||
)
|
||||
})
|
||||
.collect::<Vec<_>>()
|
||||
@@ -199,8 +204,12 @@ impl ToR1cs {
|
||||
/// If `signed` is set, then the MSB is negated; i.e., the two's-complement sum is returned.
|
||||
fn debitify<I: ExactSizeIterator<Item = Lc>>(&self, bits: I, signed: bool) -> Lc {
|
||||
let n = bits.len();
|
||||
let two = self.r1cs.modulus.new_v(2);
|
||||
let mut acc = self.r1cs.modulus.new_v(1);
|
||||
bits.enumerate().fold(self.r1cs.zero(), |sum, (i, bit)| {
|
||||
let summand = bit * &Integer::from(2).pow(i as u32);
|
||||
let summand = bit * &acc;
|
||||
acc *= &two;
|
||||
|
||||
if signed && i + 1 == n {
|
||||
sum - &summand
|
||||
} else {
|
||||
@@ -558,7 +567,9 @@ impl ToR1cs {
|
||||
Op::BvUnOp(BvUnOp::Neg) => {
|
||||
let x = self.get_bv_uint(&bv.cs[0]);
|
||||
// Wrong for x == 0
|
||||
let almost_neg_x = self.r1cs.zero() + &Integer::from(2).pow(n as u32) - &x;
|
||||
let almost_neg_x = self.r1cs.zero()
|
||||
+ &self.r1cs.modulus.new_v(Integer::from(2).pow(n as u32))
|
||||
- &x;
|
||||
let is_zero = self.is_zero(x);
|
||||
let neg_x = self.ite(is_zero, self.r1cs.zero(), &almost_neg_x);
|
||||
self.set_bv_uint(bv, neg_x, n);
|
||||
@@ -656,7 +667,9 @@ impl ToR1cs {
|
||||
let b = self.get_bv_uint(&bv.cs[1]);
|
||||
match o {
|
||||
BvBinOp::Sub => {
|
||||
let sum = a + &(Integer::from(1) << n as u32) - &b;
|
||||
let sum =
|
||||
a + &self.r1cs.modulus.new_v(Integer::from(2).pow(n as u32))
|
||||
- &b;
|
||||
let mut bits = self.bitify("sub", &sum, n + 1, false);
|
||||
bits.truncate(n);
|
||||
self.set_bv_bits(bv, bits);
|
||||
@@ -668,10 +681,22 @@ impl ToR1cs {
|
||||
.eval(&a)
|
||||
.and_then(|a| {
|
||||
self.r1cs.eval(&b).map(|b| {
|
||||
if b == 0 {
|
||||
((Integer::from(1) << n as u32) - 1, a)
|
||||
if b.is_zero() {
|
||||
(
|
||||
self.r1cs
|
||||
.modulus
|
||||
.new_v(Integer::from(2).pow(n as u32) - 1),
|
||||
a,
|
||||
)
|
||||
} else {
|
||||
(a.clone() / &b, a % b)
|
||||
let aa: Integer = a.into();
|
||||
let bb: Integer = b.into();
|
||||
let q = aa.clone() / &bb;
|
||||
let r = aa % bb;
|
||||
(
|
||||
self.r1cs.modulus.new_v(q),
|
||||
self.r1cs.modulus.new_v(r),
|
||||
)
|
||||
}
|
||||
})
|
||||
})
|
||||
@@ -754,7 +779,13 @@ impl ToR1cs {
|
||||
#[allow(dead_code)]
|
||||
fn debug_lc<D: Display + ?Sized>(&self, tag: &D, lc: &Lc) {
|
||||
if let Some(v) = self.r1cs.eval(lc) {
|
||||
println!("{}: {} (value {},{:b})", tag, self.r1cs.format_lc(lc), v, v);
|
||||
println!(
|
||||
"{}: {} (value {},{:b})",
|
||||
tag,
|
||||
self.r1cs.format_lc(lc),
|
||||
v,
|
||||
<&FieldV as Into<Integer>>::into(&v)
|
||||
);
|
||||
} else {
|
||||
println!("{}: {} (novalue)", tag, self.r1cs.format_lc(lc));
|
||||
}
|
||||
@@ -849,7 +880,7 @@ impl ToR1cs {
|
||||
let public = self.public_inputs.contains(name);
|
||||
self.fresh_var(name, self.eval_pf(name), public)
|
||||
}
|
||||
Op::Const(Value::Field(r)) => self.r1cs.zero() + r.i(),
|
||||
Op::Const(Value::Field(r)) => self.r1cs.constant(r.as_ty_ref(&self.r1cs.modulus)),
|
||||
Op::Ite => {
|
||||
let cond = self.get_bool(&c.cs[0]).clone();
|
||||
let t = self.get_pf(&c.cs[1]).clone();
|
||||
@@ -896,7 +927,7 @@ impl ToR1cs {
|
||||
}
|
||||
|
||||
/// Convert this (IR) constraint system `cs` to R1CS, over a prime field defined by `modulus`.
|
||||
pub fn to_r1cs(cs: Computation, modulus: Integer) -> R1cs<String> {
|
||||
pub fn to_r1cs(cs: Computation, modulus: FieldT) -> R1cs<String> {
|
||||
let Computation {
|
||||
outputs: assertions,
|
||||
metadata,
|
||||
@@ -931,15 +962,18 @@ pub fn to_r1cs(cs: Computation, modulus: Integer) -> R1cs<String> {
|
||||
#[cfg(test)]
|
||||
pub mod test {
|
||||
use super::*;
|
||||
use crate::util::field::DFL_T;
|
||||
|
||||
use crate::ir::proof::Constraints;
|
||||
use crate::ir::term::dist::test::*;
|
||||
use crate::ir::term::dist::*;
|
||||
use crate::target::r1cs::opt::reduce_linearities;
|
||||
|
||||
use circ_fields::FieldT;
|
||||
use quickcheck::{Arbitrary, Gen};
|
||||
use quickcheck_macros::quickcheck;
|
||||
use rand::distributions::Distribution;
|
||||
use rand::SeedableRng;
|
||||
use std::sync::Arc;
|
||||
|
||||
fn init() {
|
||||
let _ = env_logger::builder().is_test(true).try_init();
|
||||
@@ -965,7 +999,7 @@ pub mod test {
|
||||
.collect(),
|
||||
),
|
||||
);
|
||||
let r1cs = to_r1cs(cs, Integer::from(17));
|
||||
let r1cs = to_r1cs(cs, FieldT::from(Integer::from(17)));
|
||||
r1cs.check_all();
|
||||
}
|
||||
|
||||
@@ -1007,7 +1041,7 @@ pub mod test {
|
||||
term![Op::Not; t]
|
||||
};
|
||||
let cs = Computation::from_constraint_system_parts(vec![t], Vec::new(), Some(values));
|
||||
let r1cs = to_r1cs(cs, Integer::from(crate::ir::term::field::TEST_FIELD));
|
||||
let r1cs = to_r1cs(cs, DFL_T.clone());
|
||||
r1cs.check_all();
|
||||
}
|
||||
|
||||
@@ -1018,7 +1052,7 @@ pub mod test {
|
||||
let mut cs = Computation::from_constraint_system_parts(vec![t], Vec::new(), Some(values));
|
||||
crate::ir::opt::scalarize_vars::scalarize_inputs(&mut cs);
|
||||
crate::ir::opt::tuple::eliminate_tuples(&mut cs);
|
||||
let r1cs = to_r1cs(cs, Integer::from(crate::ir::term::field::TEST_FIELD));
|
||||
let r1cs = to_r1cs(cs, DFL_T.clone());
|
||||
r1cs.check_all();
|
||||
}
|
||||
|
||||
@@ -1027,9 +1061,9 @@ pub mod test {
|
||||
let v = eval(&t, &values);
|
||||
let t = term![Op::Eq; t, leaf_term(Op::Const(v))];
|
||||
let cs = Computation::from_constraint_system_parts(vec![t], Vec::new(), Some(values));
|
||||
let r1cs = to_r1cs(cs, Integer::from(crate::ir::term::field::TEST_FIELD));
|
||||
let r1cs = to_r1cs(cs, DFL_T.clone());
|
||||
r1cs.check_all();
|
||||
let r1cs2 = reduce_linearities(r1cs);
|
||||
let r1cs2 = reduce_linearities(r1cs, None);
|
||||
r1cs2.check_all();
|
||||
}
|
||||
|
||||
@@ -1040,9 +1074,9 @@ pub mod test {
|
||||
let mut cs = Computation::from_constraint_system_parts(vec![t], Vec::new(), Some(values));
|
||||
crate::ir::opt::scalarize_vars::scalarize_inputs(&mut cs);
|
||||
crate::ir::opt::tuple::eliminate_tuples(&mut cs);
|
||||
let r1cs = to_r1cs(cs, Integer::from(crate::ir::term::field::TEST_FIELD));
|
||||
let r1cs = to_r1cs(cs, DFL_T.clone());
|
||||
r1cs.check_all();
|
||||
let r1cs2 = reduce_linearities(r1cs);
|
||||
let r1cs2 = reduce_linearities(r1cs, None);
|
||||
r1cs2.check_all();
|
||||
}
|
||||
|
||||
@@ -1061,7 +1095,7 @@ pub mod test {
|
||||
.collect(),
|
||||
),
|
||||
);
|
||||
let r1cs = to_r1cs(cs, Integer::from(crate::ir::term::field::TEST_FIELD));
|
||||
let r1cs = to_r1cs(cs, DFL_T.clone());
|
||||
r1cs.check_all();
|
||||
}
|
||||
|
||||
@@ -1075,9 +1109,9 @@ pub mod test {
|
||||
let v = eval(&t, &values);
|
||||
let t = term![Op::Eq; t, leaf_term(Op::Const(v))];
|
||||
let cs = Computation::from_constraint_system_parts(vec![t], vec![], Some(values));
|
||||
let r1cs = to_r1cs(cs, Integer::from(crate::ir::term::field::TEST_FIELD));
|
||||
let r1cs = to_r1cs(cs, DFL_T.clone());
|
||||
r1cs.check_all();
|
||||
let r1cs2 = reduce_linearities(r1cs);
|
||||
let r1cs2 = reduce_linearities(r1cs, None);
|
||||
r1cs2.check_all();
|
||||
}
|
||||
|
||||
@@ -1090,16 +1124,13 @@ pub mod test {
|
||||
}
|
||||
|
||||
fn pf(i: isize) -> Term {
|
||||
leaf_term(Op::Const(Value::Field(FieldElem::new(
|
||||
Integer::from(i),
|
||||
Arc::new(Integer::from(crate::ir::term::field::TEST_FIELD)),
|
||||
))))
|
||||
leaf_term(Op::Const(Value::Field(DFL_T.new_v(i))))
|
||||
}
|
||||
|
||||
fn const_test(term: Term) {
|
||||
let mut cs = Computation::new(true);
|
||||
cs.assert(term);
|
||||
let r1cs = to_r1cs(cs, Integer::from(crate::ir::term::field::TEST_FIELD));
|
||||
let r1cs = to_r1cs(cs, DFL_T.clone());
|
||||
r1cs.check_all();
|
||||
}
|
||||
|
||||
@@ -1221,7 +1252,7 @@ pub mod test {
|
||||
),
|
||||
);
|
||||
crate::ir::opt::tuple::eliminate_tuples(&mut cs);
|
||||
let r1cs = to_r1cs(cs, Integer::from(17));
|
||||
let r1cs = to_r1cs(cs, FieldT::from(Integer::from(17)));
|
||||
r1cs.check_all();
|
||||
}
|
||||
}
|
||||
|
||||
28
src/util/field.rs
Normal file
28
src/util/field.rs
Normal file
@@ -0,0 +1,28 @@
|
||||
//! Field type defaults
|
||||
//
|
||||
// NOTE: when we eventually break CirC into separate crates,
|
||||
// each crate may want its own field type default
|
||||
|
||||
#[cfg(not(feature = "ff_dfl"))]
|
||||
use circ_fields::moduli::*;
|
||||
use circ_fields::FieldT;
|
||||
#[cfg(not(feature = "ff_dfl"))]
|
||||
use lazy_static::lazy_static;
|
||||
|
||||
#[cfg(all(feature = "bls12381", feature = "ff_dfl"))]
|
||||
/// Default field
|
||||
pub const DFL_T: FieldT = FieldT::FBls12381;
|
||||
#[cfg(all(feature = "bls12381", not(feature = "ff_dfl")))]
|
||||
lazy_static! {
|
||||
/// Default field
|
||||
pub static ref DFL_T: FieldT = FieldT::IntField(F_BLS12381_FMOD_ARC.clone());
|
||||
}
|
||||
|
||||
#[cfg(all(not(feature = "bls12381"), feature = "ff_dfl"))]
|
||||
/// Default field
|
||||
pub const DFL_T: FieldT = FieldT::FBn254;
|
||||
#[cfg(all(not(feature = "bls12381"), not(feature = "ff_dfl")))]
|
||||
lazy_static! {
|
||||
/// Default field
|
||||
pub static ref DFL_T: FieldT = FieldT::IntField(F_BN254_FMOD_ARC.clone());
|
||||
}
|
||||
@@ -1,5 +1,6 @@
|
||||
//! Various data structures, etc.
|
||||
|
||||
pub mod field;
|
||||
pub mod hc;
|
||||
pub mod once;
|
||||
|
||||
|
||||
Reference in New Issue
Block a user