From 29f423bdc44fcad91c85fb4e7766c85f39c165f0 Mon Sep 17 00:00:00 2001 From: porcuquine Date: Wed, 26 Jul 2023 18:51:06 -0700 Subject: [PATCH] Initial FOIL implemenation. --- .gitignore | 1 + Cargo.lock | 397 +++++++------- Cargo.toml | 3 +- foil/Cargo.toml | 26 + foil/src/circuit.rs | 128 +++++ foil/src/coil.rs | 780 +++++++++++++++++++++++++++ foil/src/congruence.rs | 536 ++++++++++++++++++ foil/src/constructors.rs | 697 ++++++++++++++++++++++++ foil/src/lib.rs | 725 +++++++++++++++++++++++++ lurk-macros/src/lib.rs | 6 + lurk-macros/tests/lurk_macro_test.rs | 12 +- src/circuit/gadgets/constraints.rs | 2 +- src/foil/coil.rs | 780 +++++++++++++++++++++++++++ src/store.rs | 19 + src/symbol.rs | 2 +- 15 files changed, 3911 insertions(+), 203 deletions(-) create mode 100644 foil/Cargo.toml create mode 100644 foil/src/circuit.rs create mode 100644 foil/src/coil.rs create mode 100644 foil/src/congruence.rs create mode 100644 foil/src/constructors.rs create mode 100644 foil/src/lib.rs create mode 100644 src/foil/coil.rs diff --git a/.gitignore b/.gitignore index 4d590a1f9b..4a5c6bec37 100644 --- a/.gitignore +++ b/.gitignore @@ -3,6 +3,7 @@ result* /scratch /.direnv *.commit +.direnv/ # Configurations for VSCode .vscode/ diff --git a/Cargo.lock b/Cargo.lock index 93b03a1467..06de25731e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -53,9 +53,9 @@ dependencies = [ [[package]] name = "aho-corasick" -version = "1.0.2" +version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "43f6cb1bf222025340178f382c426f13757b2960e89779dfcb319c32542a5a41" +checksum = "6748e8def348ed4d14996fa801f4122cd763fff530258cdc03f64b25f89d3a5a" dependencies = [ "memchr", ] @@ -107,9 +107,9 @@ dependencies = [ [[package]] name = "anstyle-wincon" -version = "1.0.1" +version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "180abfa45703aebe0093f79badacc01b8fd4ea2e35118747e5811127f926e188" +checksum = "c677ab05e09154296dd37acecd46420c17b9713e8366facafa8fc0885167cf4c" dependencies = [ "anstyle", "windows-sys 0.48.0", @@ -117,9 +117,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.72" +version = "1.0.74" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3b13c32d80ecc7ab747b80c3784bce54ee8a7a0cc4fbda9bf4cda2cf6fe90854" +checksum = "8c6f84b74db2535ebae81eede2f39b947dcbf01d093ae5f791e5dd414a1bf289" [[package]] name = "anymap" @@ -162,13 +162,13 @@ dependencies = [ [[package]] name = "async-trait" -version = "0.1.71" +version = "0.1.73" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a564d521dd56509c4c47480d00b80ee55f7e385ae48db5744c67ad50c92d2ebf" +checksum = "bc00ceb34980c03614e35a3a4e218276a0a824e911d07651cd0d858a51e8c0f0" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.28", ] [[package]] @@ -282,9 +282,9 @@ checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" [[package]] name = "bitflags" -version = "2.3.3" +version = "2.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "630be753d4e58660abd17930c71b647fe46c27ea6b63cc59e1e3851406972e42" +checksum = "b4682ae6287fcf752ecaabbfcc7b6f9b72aa33933dc23a554d853aea8eea8635" [[package]] name = "bitvec" @@ -342,22 +342,21 @@ dependencies = [ [[package]] name = "blst" -version = "0.3.10" +version = "0.3.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6a30d0edd9dd1c60ddb42b80341c7852f6f985279a5c1a83659dcb65899dec99" +checksum = "c94087b935a822949d3291a9989ad2b2051ea141eda0fd4e478a75f6aa3e604b" dependencies = [ "cc", "glob", "threadpool", - "which", "zeroize", ] [[package]] name = "blstrs" -version = "0.7.0" +version = "0.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "33149fccb7f93271f0192614b884430cf274e880506bbd171cbc8918dcc95b14" +checksum = "7a8a8ed6fefbeef4a8c7b460e4110e12c5e22a5b7cf32621aae6ad650c4dcf29" dependencies = [ "blst", "byte-slice-cast", @@ -425,9 +424,12 @@ checksum = "37b2a672a2cb129a2e41c10b1224bb368f9f37a2b16b612598138befd7b37eb5" [[package]] name = "cc" -version = "1.0.79" +version = "1.0.82" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "50d30906286121d95be3d479533b458f87493b30a4b5f79a607db8f5d11aa91f" +checksum = "305fe645edc1442a0fa8b6726ba61d422798d37a52e12eaecf4b022ebbb88f01" +dependencies = [ + "libc", +] [[package]] name = "cfg-if" @@ -464,12 +466,13 @@ dependencies = [ [[package]] name = "cl3" -version = "0.9.1" +version = "0.9.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0e014961508a981c7ef28a65d0c965af7061593b4db50cff83952c62931b39ec" +checksum = "215a3aa32ab5d7928c539c4289d1cf144257c3cb05e05a4b7e61d5a6bb6583a5" dependencies = [ "libc", "opencl-sys", + "thiserror", ] [[package]] @@ -497,9 +500,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.3.17" +version = "4.3.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5b0827b011f6f8ab38590295339817b0d26f344aa4932c3ced71b45b0c54b4a9" +checksum = "c27cdf28c0f604ba3f512b0c9a409f8de8513e4816705deb0498b627e7c3a3fd" dependencies = [ "clap_builder", "clap_derive", @@ -512,15 +515,15 @@ version = "2.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1eef05769009513df2eb1c3b4613e7fad873a14c600ff025b08f250f59fee7de" dependencies = [ - "clap 4.3.17", + "clap 4.3.21", "log", ] [[package]] name = "clap_builder" -version = "4.3.17" +version = "4.3.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9441b403be87be858db6a23edb493e7f694761acdc3343d5a0fcaafd304cbc9e" +checksum = "08a9f1ab5e9f01a9b81f202e8562eb9a10de70abf9eaeac1be465c28b75aa4aa" dependencies = [ "anstream", "anstyle", @@ -536,8 +539,8 @@ checksum = "54a9bb5758fc5dfe728d1019941681eccaf0cf8a4189b692a0ee2f2ecf90a050" dependencies = [ "heck 0.4.1", "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.28", ] [[package]] @@ -574,7 +577,7 @@ dependencies = [ "assert_cmd", "blstrs", "camino", - "clap 4.3.17", + "clap 4.3.21", "fcomm", "ff", "lurk", @@ -853,9 +856,9 @@ dependencies = [ [[package]] name = "either" -version = "1.8.1" +version = "1.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7fcaabb2fef8c910e7f4c7ce9f67a1283a1715879a7c230ca9d6d1ae31f16d91" +checksum = "a26ae43d7bcc3b814de94796a5e736d4029efb0ee900c12e2d54c993ad1a1e07" [[package]] name = "encode_unicode" @@ -870,7 +873,20 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "44533bbbb3bb3c1fa17d9f2e4e38bbbaf8396ba82193c4cb1b6445d711445d36" dependencies = [ "atty", - "humantime", + "humantime 1.3.0", + "log", + "regex", + "termcolor", +] + +[[package]] +name = "env_logger" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "85cdab6a89accf66733ad5a1693a4dcced6aeff64602b634530dd73c1f3ee9f0" +dependencies = [ + "humantime 2.1.0", + "is-terminal", "log", "regex", "termcolor", @@ -878,9 +894,9 @@ dependencies = [ [[package]] name = "errno" -version = "0.3.1" +version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4bcfec3a70f97c962c307b2d2c56e358cf1d00b558d74262b5f929ee8cc7e73a" +checksum = "6b30f669a7961ef1631673d2766cc92f52d64f7ef354d4fe0ddfd30ed52f0f4f" dependencies = [ "errno-dragonfly", "libc", @@ -934,8 +950,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "55a9a55d1dab3b07854648d48e366f684aefe2ac78ae28cec3bf65e3cd53d9a3" dependencies = [ "execute-command-tokens", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.28", ] [[package]] @@ -956,12 +972,9 @@ dependencies = [ [[package]] name = "fastrand" -version = "1.9.0" +version = "2.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e51093e27b0797c359783294ca4f0a911c270184cb10f85783b118614a1501be" -dependencies = [ - "instant", -] +checksum = "6999dc1837253364c2ebb0704ba97994bd874e8f195d665c50b7548f6ea92764" [[package]] name = "fcomm" @@ -974,7 +987,7 @@ dependencies = [ "bincode", "blstrs", "camino", - "clap 4.3.17", + "clap 4.3.21", "clap-verbosity-flag", "ff", "hex", @@ -1004,7 +1017,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ef033ed5e9bad94e55838ca0ca906db0e043f517adda0c8b79c7a8c66c93c1b5" dependencies = [ "cfg-if", - "rustix 0.38.4", + "rustix", "windows-sys 0.48.0", ] @@ -1033,7 +1046,7 @@ dependencies = [ "num-integer", "num-traits", "proc-macro2 1.0.66", - "quote 1.0.31", + "quote 1.0.32", "syn 1.0.109", ] @@ -1063,9 +1076,9 @@ dependencies = [ [[package]] name = "flate2" -version = "1.0.26" +version = "1.0.27" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3b9429470923de8e8cbd4d2dc513535400b4b3fef0319fb5c4e1f520a7bef743" +checksum = "c6c98ee8095e9d1dcbf2fcc6d95acccb90d1c81db1e44725c6a984b1dbdfb010" dependencies = [ "crc32fast", "miniz_oxide", @@ -1095,6 +1108,26 @@ version = "1.0.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1" +[[package]] +name = "foil" +version = "0.1.0" +dependencies = [ + "anyhow", + "bellperson", + "env_logger 0.10.0", + "ff", + "generic-array", + "indexmap", + "log", + "lurk", + "lurk-macros", + "neptune", + "once_cell", + "pasta_curves", + "pretty_env_logger", + "test-log", +] + [[package]] name = "fs2" version = "0.4.3" @@ -1269,6 +1302,12 @@ dependencies = [ "quick-error", ] +[[package]] +name = "humantime" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" + [[package]] name = "indexmap" version = "1.9.3" @@ -1312,26 +1351,6 @@ dependencies = [ "yaml-rust", ] -[[package]] -name = "instant" -version = "0.1.12" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7a5bbe824c507c5da5956355e86a746d82e0e1464f65d862cc5e71da70e94b2c" -dependencies = [ - "cfg-if", -] - -[[package]] -name = "io-lifetimes" -version = "1.0.11" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eae7b9aee968036d54dce06cebaefd919e4472e753296daccd6d344e3e2df0c2" -dependencies = [ - "hermit-abi 0.3.2", - "libc", - "windows-sys 0.48.0", -] - [[package]] name = "is-terminal" version = "0.4.9" @@ -1339,7 +1358,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cb0889898416213fab133e1d33a0e5858a48177452750691bde3666d0fdbaf8b" dependencies = [ "hermit-abi 0.3.2", - "rustix 0.38.4", + "rustix", "windows-sys 0.48.0", ] @@ -1381,9 +1400,9 @@ dependencies = [ [[package]] name = "itoa" -version = "1.0.8" +version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "62b02a5381cc465bd3041d84623d0fa3b66738b52b8e2fc3bab8ad63ab032f4a" +checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38" [[package]] name = "js-sys" @@ -1443,15 +1462,9 @@ checksum = "0717cef1bc8b636c6e1c1bbdefc09e6322da8a9321966e8928ef80d20f7f770f" [[package]] name = "linux-raw-sys" -version = "0.3.8" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ef53942eb7bf7ff43a617b3e2c1c4a5ecf5944a7c1bc12d7ee39bbb15e5c1519" - -[[package]] -name = "linux-raw-sys" -version = "0.4.3" +version = "0.4.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09fc20d2ca12cb9f044c93e3bd6d32d523e6e2ec3db4f7b2939cd99026ecd3f0" +checksum = "57bcfdad1b858c2db7c38303a6d2ad4dfaf5eb53dfeb0910128b2c26d6158503" [[package]] name = "lock_api" @@ -1465,9 +1478,9 @@ dependencies = [ [[package]] name = "log" -version = "0.4.19" +version = "0.4.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b06a4cde4c0f271a446782e3eff8de789548ce57dbc8eca9292c27f4a42004b4" +checksum = "b5e6163cb8c49088c2c36f57875e58ccd8c87c7427f7fbd50ea6710b2f3f2e8f" [[package]] name = "lurk" @@ -1485,7 +1498,7 @@ dependencies = [ "blstrs", "camino", "cfg-if", - "clap 4.3.17", + "clap 4.3.21", "config", "criterion", "dashmap", @@ -1546,7 +1559,7 @@ dependencies = [ "proc-macro2 1.0.66", "proptest", "proptest-derive", - "quote 1.0.31", + "quote 1.0.32", "serde", "syn 1.0.109", ] @@ -1605,8 +1618,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ddece26afd34c31585c74a4db0630c376df271c285d682d1e55012197830b6df" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.28", ] [[package]] @@ -1762,9 +1775,9 @@ dependencies = [ [[package]] name = "num-traits" -version = "0.2.15" +version = "0.2.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "578ede34cf02f8924ab9447f50c28075b4d3e5b269972345e7e0372b38c6cdcd" +checksum = "f30b0abd723be7e2ffca1272140fac1a2f084c77ec3e123c192b66af1ee9e6c2" dependencies = [ "autocfg", "libm", @@ -1865,7 +1878,7 @@ dependencies = [ "libc", "redox_syscall", "smallvec", - "windows-targets 0.48.1", + "windows-targets 0.48.2", ] [[package]] @@ -1901,9 +1914,9 @@ dependencies = [ [[package]] name = "paste" -version = "1.0.13" +version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4b27ab7be369122c218afc2079489cdcb4b517c0a3fc386ff11e1fedfcc2b35" +checksum = "de3145af08024dea9fa9914f381a17b8fc6034dfb00f3a84013f7ff43f29ed4c" [[package]] name = "pathdiff" @@ -1919,9 +1932,9 @@ checksum = "9163e1259760e83d528d1b3171e5100c1767f10c52e1c4d6afad26e63d47d758" [[package]] name = "pest" -version = "2.7.0" +version = "2.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f73935e4d55e2abf7f130186537b19e7a4abc886a0252380b59248af473a3fc9" +checksum = "1acb4a4365a13f749a93f1a094a7805e5cfa0955373a9de860d962eaa3a5fe5a" dependencies = [ "thiserror", "ucd-trie", @@ -1929,9 +1942,9 @@ dependencies = [ [[package]] name = "pest_derive" -version = "2.7.0" +version = "2.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aef623c9bbfa0eedf5a0efba11a5ee83209c326653ca31ff019bec3a95bfff2b" +checksum = "666d00490d4ac815001da55838c500eafb0320019bbaa44444137c48b443a853" dependencies = [ "pest", "pest_generator", @@ -1939,22 +1952,22 @@ dependencies = [ [[package]] name = "pest_generator" -version = "2.7.0" +version = "2.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b3e8cba4ec22bada7fc55ffe51e2deb6a0e0db2d0b7ab0b103acc80d2510c190" +checksum = "68ca01446f50dbda87c1786af8770d535423fa8a53aec03b8f4e3d7eb10e0929" dependencies = [ "pest", "pest_meta", "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.28", ] [[package]] name = "pest_meta" -version = "2.7.0" +version = "2.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a01f71cb40bd8bb94232df14b946909e14660e33fc05db3e50ae2a82d7ea0ca0" +checksum = "56af0a30af74d0445c0bf6d9d051c979b516a1a5af790d251daee76005420a48" dependencies = [ "once_cell", "pest", @@ -1991,9 +2004,9 @@ dependencies = [ [[package]] name = "portable-atomic" -version = "1.4.1" +version = "1.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "edc55135a600d700580e406b4de0d59cb9ad25e344a3a091a97ded2622ec4ec6" +checksum = "f32154ba0af3a075eefa1eda8bb414ee928f62303a54ea85b8d6638ff1a6ee9e" [[package]] name = "pprof" @@ -2071,7 +2084,7 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "926d36b9553851b8b0005f1275891b392ee4d2d833852c417ed025477350fb9d" dependencies = [ - "env_logger", + "env_logger 0.7.1", "log", ] @@ -2083,7 +2096,7 @@ checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" dependencies = [ "proc-macro-error-attr", "proc-macro2 1.0.66", - "quote 1.0.31", + "quote 1.0.32", "syn 1.0.109", "version_check", ] @@ -2095,7 +2108,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", + "quote 1.0.32", "version_check", ] @@ -2174,9 +2187,9 @@ dependencies = [ [[package]] name = "quote" -version = "1.0.31" +version = "1.0.32" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5fe8a65d69dd0808184ebb5f836ab526bb259db23c657efa38711b1072ee47f0" +checksum = "50f3b39ccfb720540debaa0164757101c08ecb8d326b15358ce76a62c7e85965" dependencies = [ "proc-macro2 1.0.66", ] @@ -2259,9 +2272,9 @@ dependencies = [ [[package]] name = "regex" -version = "1.9.1" +version = "1.9.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b2eae68fc220f7cf2532e4494aded17545fce192d59cd996e0fe7887f4ceb575" +checksum = "81bc1d4caf89fac26a70747fe603c130093b53c773888797a6329091246d651a" dependencies = [ "aho-corasick", "memchr", @@ -2271,9 +2284,9 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.3.3" +version = "0.3.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "39354c10dd07468c2e73926b23bb9c2caca74c5501e38a35da70406f1d923310" +checksum = "fed1ceff11a1dddaee50c9dc8e4938bd106e9d89ae372f192311e7da498e3b69" dependencies = [ "aho-corasick", "memchr", @@ -2352,7 +2365,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "43ce8670a1a1d0fc2514a3b846dacdb65646f9bd494b6674cfacbb4ce430bd7e" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", + "quote 1.0.32", "syn 1.0.109", ] @@ -2364,36 +2377,22 @@ checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76" [[package]] name = "rustix" -version = "0.37.23" +version = "0.38.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4d69718bf81c6127a49dc64e44a742e8bb9213c0ff8869a22c308f84c1d4ab06" +checksum = "19ed4fa021d81c8392ce04db050a3da9a60299050b7ae1cf482d862b54a7218f" dependencies = [ - "bitflags 1.3.2", + "bitflags 2.4.0", "errno", - "io-lifetimes", "libc", - "linux-raw-sys 0.3.8", - "windows-sys 0.48.0", -] - -[[package]] -name = "rustix" -version = "0.38.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0a962918ea88d644592894bc6dc55acc6c0956488adcebbfb6e273506b7fd6e5" -dependencies = [ - "bitflags 2.3.3", - "errno", - "libc", - "linux-raw-sys 0.4.3", + "linux-raw-sys", "windows-sys 0.48.0", ] [[package]] name = "rustversion" -version = "1.0.13" +version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dc31bd9b61a32c31f9650d18add92aa83a49ba979c143eefd27fe7177b05bd5f" +checksum = "7ffc183a10b4478d04cbbbfc96d0873219d962dd5accaff2ffbd4ceb7df837f4" [[package]] name = "rusty-fork" @@ -2436,15 +2435,15 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8218eaf5d960e3c478a1b0f129fa888dd3d8d22eb3de097e9af14c1ab4438024" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", + "quote 1.0.32", "syn 1.0.109", ] [[package]] name = "ryu" -version = "1.0.14" +version = "1.0.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fe232bdf6be8c8de797b22184ee71118d63780ea42ac85b61d1baa6d3b782ae9" +checksum = "1ad4cc8da4ef723ed60bced201181d83791ad433213d8c24efffda1eec85d741" [[package]] name = "same-file" @@ -2473,9 +2472,9 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.171" +version = "1.0.183" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "30e27d1e4fd7659406c492fd6cfaf2066ba8773de45ca75e855590f856dc34a9" +checksum = "32ac8da02677876d532745a130fc9d8e6edfa81a269b107c5b00829b91d8eb3c" dependencies = [ "serde_derive", ] @@ -2500,20 +2499,20 @@ dependencies = [ [[package]] name = "serde_derive" -version = "1.0.171" +version = "1.0.183" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "389894603bd18c46fa56231694f8d827779c0951a667087194cf9de94ed24682" +checksum = "aafe972d60b0b9bee71a91b92fee2d4fb3c9d7e8f6b179aa99f27203d99a4816" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.28", ] [[package]] name = "serde_json" -version = "1.0.100" +version = "1.0.104" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0f1e14e89be7aa4c4b78bdbdc9eb5bf8517829a600ae8eaa39a6e1d960b5185c" +checksum = "076066c5f1078eac5b722a31827a8832fe108bed65dfa75e233c89f8206e976c" dependencies = [ "itoa", "ryu", @@ -2522,13 +2521,13 @@ dependencies = [ [[package]] name = "serde_repr" -version = "0.1.14" +version = "0.1.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1d89a8107374290037607734c0b73a85db7ed80cae314b3c5791f192a496e731" +checksum = "8725e1dfadb3a50f7e5ce0b1a540466f6ed3fe7a0fca2ac2b8b831d31316bd00" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.28", ] [[package]] @@ -2638,7 +2637,7 @@ dependencies = [ "heck 0.3.3", "proc-macro-error", "proc-macro2 1.0.66", - "quote 1.0.31", + "quote 1.0.32", "syn 1.0.109", ] @@ -2689,18 +2688,18 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", + "quote 1.0.32", "unicode-ident", ] [[package]] name = "syn" -version = "2.0.26" +version = "2.0.28" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "45c3457aacde3c65315de5031ec191ce46604304d2446e803d71ade03308d970" +checksum = "04361975b3f5e348b2189d8dc55bc942f278b2d482a6a0365de5bdd62d351567" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", + "quote 1.0.32", "unicode-ident", ] @@ -2721,15 +2720,14 @@ dependencies = [ [[package]] name = "tempfile" -version = "3.6.0" +version = "3.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "31c0432476357e58790aaa47a8efb0c5138f137343f3b5f23bd36a27e3b0a6d6" +checksum = "dc02fddf48964c42031a0b3fe0428320ecf3a73c401040fc0096f97794310651" dependencies = [ - "autocfg", "cfg-if", "fastrand", "redox_syscall", - "rustix 0.37.23", + "rustix", "windows-sys 0.48.0", ] @@ -2748,6 +2746,17 @@ version = "0.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3369f5ac52d5eb6ab48c6b4ffdc8efbcad6b89c765749064ba298f2c68a16a76" +[[package]] +name = "test-log" +version = "0.2.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d9601d162c1d77e62c1ea0bc8116cd1caf143ce3af947536c3c9052a1677fe0c" +dependencies = [ + "proc-macro2 1.0.66", + "quote 1.0.32", + "syn 1.0.109", +] + [[package]] name = "testing_logger" version = "0.1.1" @@ -2774,22 +2783,22 @@ checksum = "222a222a5bfe1bba4a77b45ec488a741b3cb8872e5e499451fd7d0129c9c7c3d" [[package]] name = "thiserror" -version = "1.0.43" +version = "1.0.46" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a35fc5b8971143ca348fa6df4f024d4d55264f3468c71ad1c2f365b0a4d58c42" +checksum = "d9207952ae1a003f42d3d5e892dac3c6ba42aa6ac0c79a6a91a2b5cb4253e75c" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.43" +version = "1.0.46" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "463fe12d7993d3b327787537ce8dd4dfa058de32fc2b195ef3cde03dc4771e8f" +checksum = "f1728216d3244de4f14f14f8c15c79be1a7c67867d28d69b719690e2a19fb445" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.28", ] [[package]] @@ -2827,7 +2836,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b79e2e9c9ab44c6d7c20d5976961b47e8f49ac199154daa514b77cd1ab536625" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", + "quote 1.0.32", "syn 1.0.109", ] @@ -2881,9 +2890,9 @@ checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a" [[package]] name = "uuid" -version = "1.4.0" +version = "1.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d023da39d1fde5a8a3fe1f3e01ca9632ada0a63e9797de55a879d6e2236277be" +checksum = "79daa5ed5740825c40b389c5e50312b9c86df53fccd33f281df655642b43869d" [[package]] name = "version_check" @@ -2936,8 +2945,8 @@ dependencies = [ "log", "once_cell", "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.28", "wasm-bindgen-shared", ] @@ -2947,7 +2956,7 @@ version = "0.2.87" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "dee495e55982a3bd48105a7b947fd2a9b4a8ae3010041b9e0faab3f9cd028f1d" dependencies = [ - "quote 1.0.31", + "quote 1.0.32", "wasm-bindgen-macro-support", ] @@ -2958,8 +2967,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "54681b18a46765f095758388f2d0cf16eb8d4169b639ab575a8f5693af210c7b" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.28", "wasm-bindgen-backend", "wasm-bindgen-shared", ] @@ -3037,7 +3046,7 @@ version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" dependencies = [ - "windows-targets 0.48.1", + "windows-targets 0.48.2", ] [[package]] @@ -3057,17 +3066,17 @@ dependencies = [ [[package]] name = "windows-targets" -version = "0.48.1" +version = "0.48.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "05d4b17490f70499f20b9e791dcf6a299785ce8af4d709018206dc5b4953e95f" +checksum = "d1eeca1c172a285ee6c2c84c341ccea837e7c01b12fbb2d0fe3c9e550ce49ec8" dependencies = [ - "windows_aarch64_gnullvm 0.48.0", - "windows_aarch64_msvc 0.48.0", - "windows_i686_gnu 0.48.0", - "windows_i686_msvc 0.48.0", - "windows_x86_64_gnu 0.48.0", - "windows_x86_64_gnullvm 0.48.0", - "windows_x86_64_msvc 0.48.0", + "windows_aarch64_gnullvm 0.48.2", + "windows_aarch64_msvc 0.48.2", + "windows_i686_gnu 0.48.2", + "windows_i686_msvc 0.48.2", + "windows_x86_64_gnu 0.48.2", + "windows_x86_64_gnullvm 0.48.2", + "windows_x86_64_msvc 0.48.2", ] [[package]] @@ -3078,9 +3087,9 @@ checksum = "597a5118570b68bc08d8d59125332c54f1ba9d9adeedeef5b99b02ba2b0698f8" [[package]] name = "windows_aarch64_gnullvm" -version = "0.48.0" +version = "0.48.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "91ae572e1b79dba883e0d315474df7305d12f569b400fcf90581b06062f7e1bc" +checksum = "b10d0c968ba7f6166195e13d593af609ec2e3d24f916f081690695cf5eaffb2f" [[package]] name = "windows_aarch64_msvc" @@ -3090,9 +3099,9 @@ checksum = "e08e8864a60f06ef0d0ff4ba04124db8b0fb3be5776a5cd47641e942e58c4d43" [[package]] name = "windows_aarch64_msvc" -version = "0.48.0" +version = "0.48.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b2ef27e0d7bdfcfc7b868b317c1d32c641a6fe4629c171b8928c7b08d98d7cf3" +checksum = "571d8d4e62f26d4932099a9efe89660e8bd5087775a2ab5cdd8b747b811f1058" [[package]] name = "windows_i686_gnu" @@ -3102,9 +3111,9 @@ checksum = "c61d927d8da41da96a81f029489353e68739737d3beca43145c8afec9a31a84f" [[package]] name = "windows_i686_gnu" -version = "0.48.0" +version = "0.48.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "622a1962a7db830d6fd0a69683c80a18fda201879f0f447f065a3b7467daa241" +checksum = "2229ad223e178db5fbbc8bd8d3835e51e566b8474bfca58d2e6150c48bb723cd" [[package]] name = "windows_i686_msvc" @@ -3114,9 +3123,9 @@ checksum = "44d840b6ec649f480a41c8d80f9c65108b92d89345dd94027bfe06ac444d1060" [[package]] name = "windows_i686_msvc" -version = "0.48.0" +version = "0.48.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4542c6e364ce21bf45d69fdd2a8e455fa38d316158cfd43b3ac1c5b1b19f8e00" +checksum = "600956e2d840c194eedfc5d18f8242bc2e17c7775b6684488af3a9fff6fe3287" [[package]] name = "windows_x86_64_gnu" @@ -3126,9 +3135,9 @@ checksum = "8de912b8b8feb55c064867cf047dda097f92d51efad5b491dfb98f6bbb70cb36" [[package]] name = "windows_x86_64_gnu" -version = "0.48.0" +version = "0.48.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ca2b8a661f7628cbd23440e50b05d705db3686f894fc9580820623656af974b1" +checksum = "ea99ff3f8b49fb7a8e0d305e5aec485bd068c2ba691b6e277d29eaeac945868a" [[package]] name = "windows_x86_64_gnullvm" @@ -3138,9 +3147,9 @@ checksum = "26d41b46a36d453748aedef1486d5c7a85db22e56aff34643984ea85514e94a3" [[package]] name = "windows_x86_64_gnullvm" -version = "0.48.0" +version = "0.48.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7896dbc1f41e08872e9d5e8f8baa8fdd2677f29468c4e156210174edc7f7b953" +checksum = "8f1a05a1ece9a7a0d5a7ccf30ba2c33e3a61a30e042ffd247567d1de1d94120d" [[package]] name = "windows_x86_64_msvc" @@ -3150,9 +3159,9 @@ checksum = "9aec5da331524158c6d1a4ac0ab1541149c0b9505fde06423b02f5ef0106b9f0" [[package]] name = "windows_x86_64_msvc" -version = "0.48.0" +version = "0.48.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a" +checksum = "d419259aba16b663966e29e6d7c6ecfa0bb8425818bb96f6f1f3c3eb71a6e7b9" [[package]] name = "wyz" @@ -3198,6 +3207,6 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ce36e65b0d2999d2aafac989fb249189a141aee1f53c612c1f37d72631959f69" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.28", ] diff --git a/Cargo.toml b/Cargo.toml index b7b7165ada..07e2775faa 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -105,7 +105,8 @@ tempfile = { workspace = true } resolver = "2" members = [ "clutch", - "fcomm", + "fcomm", + "foil", "lurk-macros", "lurk-metrics" ] diff --git a/foil/Cargo.toml b/foil/Cargo.toml new file mode 100644 index 0000000000..a942254824 --- /dev/null +++ b/foil/Cargo.toml @@ -0,0 +1,26 @@ +[package] +name = "foil" +version = "0.1.0" +edition = "2021" +authors = ["porcuquine "] +description = "Flat Optimization Intermediate Language" +repository = "https://github.com/lurk-lab/lurk-rs" +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +anyhow = { workspace = true } +bellperson = { workspace = true } +ff = { workspace = true } +indexmap = { version = "1.9.3", features = ["rayon"] } +generic-array = "0.14.7" +lurk = { path = "../" } +lurk-macros = { path = "../lurk-macros" } +log = { workspace = true } +neptune = { workspace = true, features = ["arity2","arity4","arity8","arity16","pasta","bls"] } +once_cell = { workspace = true } +pasta_curves = { workspace = true, features = ["repr-c", "serde"] } +pretty_env_logger = "0.4" + +[dev-dependencies] +env_logger = "*" +test-log = "0.2.12" diff --git a/foil/src/circuit.rs b/foil/src/circuit.rs new file mode 100644 index 0000000000..abc535ad4d --- /dev/null +++ b/foil/src/circuit.rs @@ -0,0 +1,128 @@ +//! This module provides a general mechanism for synthesizing a circuit for a minimized Foil instance. + +use std::collections::HashSet; +use std::fmt::Debug; + +use bellperson::{gadgets::num::AllocatedNum, Circuit, ConstraintSystem, SynthesisError}; + +use crate::{Id, MappedFoil, MetaData, MetaMapper}; +use lurk::field::LurkField; + +pub trait Relation: Debug { + fn synthesize>( + &self, + _cs: &mut CS, + _allocated_head: AllocatedNum, + _successors: Vec>, + ) -> Result<(), SynthesisError> { + unimplemented!() + } +} + +// This is an incomplete schematic sketch of what synthesis should entail. NOTE: the simplicity and uniformity of this +// last-mile conversion to a circuit. Most circuit-specific heavy lifting will be concentrated in the individual +// `Relation` implementations. +impl, MR: MetaMapper> + Circuit for MappedFoil +{ + fn synthesize>(self, cs: &mut CS) -> Result<(), SynthesisError> { + let foil = self.foil; + assert!( + foil.is_minimized(), + "only minimized Foils can be synthesized" + ); + + let partition = foil.graph.partition(); + let _classes = partition.classes().clone(); + + let allocated = foil + .graph + .vertices() + .iter() + .enumerate() + .map(|(i, vertex)| { + AllocatedNum::alloc( + &mut cs.namespace(|| format!("allocated-{i}-{vertex}")), + //|| todo!("get from witness, calculate, or get as constant..."), + || Ok(F::ZERO), // Just for initial testing. + ) + }) + .collect::, SynthesisError>>()?; + + let mut constrained: HashSet = Default::default(); + // for constructor in foil.schema.constructors.iter() { + // let _projectors = constructor.projectors(); + // todo!(); + // } + + for (i, (representative_id, _)) in partition.classes.iter().enumerate() { + let vertex = foil.graph.vertex(*representative_id); + let allocated_head = allocated[i].clone(); + + //if todo!("determine whether this vertex requires allocation") { + if true { + // For example, projectors do not require allocation given that they will be constrained by their + // corresponding constructor. This *could* be handled at the `Relation` level, however, in general this + // decision may require more global context -- so for now, consider that it should be made in the + // top-level `synthesize` method. + + // Currently, so-called `Bindings` (equivalences specified through the graph) become trivial after + // finalization. There is no reason to allocate variables for them or add any related constraints. The + // right answer is probably that minimization should remove them -- along with any other superfluous + // nodes of the graph. + // + // The point is that some parts of the decision (whether a given vertex needs constraints of its own) + // should probably be handled upstream. What is important is that we clearly understand the separation + // of concerns -- so decisions at each stage do not rely on invalid assumptions about the + // responsibilities of others. Some redundancy may therefore be appropriate. + // + // For example, in the case of bindings, all of the following could be implemented: + // + // - A full 'minimization' can remove them (with a check to ensure they were indeed enforced -- which + // means their successors have been made equivalent). This implies that the bindings themselves will not + // be seen here. + + // - If they do appear here, we can detect that and not allocate or constrain them. However, note that + // maybe this is the wrong approach -- since it will require increasing knowledge of semantics here. Not + // special-casing would be simplest. One answer is to ensure that `Func`s can be defined in such a way + // as to provide hints here. Designation of `Bindings` (in the constructors example) as `equivalences` + // is effectively such an annotation, but it may be useful to provide a more general (probably + // trait-based) mechanism. + // + // - If we do reach the point of constraining such nodes, their defined `Relation::synthesize` method + // can be a no-op. + + constrained.insert(*representative_id); + + let allocated_successors = vertex + .successors() + .borrow() + .iter() + .map(|successor_id| { + constrained.insert(*successor_id); + allocated[*successor_id].clone() + }) + .collect::>(); + + let relation = { + self.mapper + .find(vertex.metadata()) + .unwrap_or_else(|| panic!("relation missing for {:?}", vertex.metadata())) + }; + + dbg!(relation); + + relation.synthesize( + &mut cs.namespace(|| format!("relation-{}", i)), + allocated_head, + allocated_successors, + )?; + } + } + + // Every allocation has been constrained. + assert_eq!(constrained.len(), partition.size()); + + Ok(()) + } +} diff --git a/foil/src/coil.rs b/foil/src/coil.rs new file mode 100644 index 0000000000..a32ac4d506 --- /dev/null +++ b/foil/src/coil.rs @@ -0,0 +1,780 @@ +use log::info; +use std::collections::{HashMap, HashSet}; +use std::marker::PhantomData; + +use bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError}; + +use anyhow::{anyhow, bail, Result}; + +use crate::{Foil, Func, Id, Label, MetaData, MetaMapper, Relation, Schema, Var, Vert}; +use lurk::field::LurkField; +use lurk::ptr::Ptr; +use lurk::store::Store; +use lurk::sym; +use lurk::symbol::Symbol; +use lurk::tag::ExprTag; +use lurk::writer::Write; + +impl From for Func { + fn from(sym: Symbol) -> Self { + Self::from(&sym) + } +} + +impl From<&Symbol> for Func { + fn from(sym: &Symbol) -> Self { + Self::new_with_metadata(sym.to_string(), CoilMeta::from(sym.clone())) + } +} + +impl From for Var { + fn from(sym: Symbol) -> Self { + Self::from(&sym) + } +} + +impl From<&Symbol> for Var { + fn from(sym: &Symbol) -> Self { + Self::new(sym.to_string()) + } +} + +impl From for Label { + fn from(sym: Symbol) -> Self { + Self::from(&sym) + } +} + +impl From<&Symbol> for Label { + fn from(sym: &Symbol) -> Self { + Self::from(Var::from(sym)) + } +} + +#[derive(Debug, Clone, Hash, PartialEq, Eq, PartialOrd, Ord)] +pub struct CoilMeta { + name: Symbol, +} + +impl From for CoilMeta { + fn from(name: Symbol) -> Self { + Self { name } + } +} + +impl Default for CoilMeta { + fn default() -> Self { + let name = sym!("coil", "var"); + + Self { name } + } +} + +impl MetaData for CoilMeta {} + +#[derive(Clone, Debug, PartialEq)] +pub struct Context { + env: Ptr, +} + +/// Look up `var` in `env`, where `env` is a list of bindings from `Symbol` to `U64` representing bindings of variables to vertices +/// by id. +fn lookup_vertex_id( + store: &Store, + env: &Ptr, + var: &Ptr, +) -> Result> { + if let Some((binding, rest_env)) = store + .maybe_car_cdr(env) + .map_err(|_| anyhow!("env not a list"))? + { + if let Some((bound_var, id)) = store + .maybe_car_cdr(&binding) + .map_err(|_| anyhow!("binding not a pair"))? + { + if *var == bound_var { + match store.fetch_num(&id) { + Some(lurk::Num::U64(n)) => { + info!("found {n}"); + Ok(((*n) as Id).into()) + } + _ => { + bail!("binding Id could not be fetched"); + } + } + } else { + lookup_vertex_id(store, &rest_env, var) + } + } else { + info!("unbound"); + Ok(None) + } + } else { + info!("unbound"); + Ok(None) + } +} + +impl Context { + fn new(store: &mut Store) -> Self { + Self { + env: lurk::eval::empty_sym_env(store), + } + } + + fn lookup(&self, store: &Store, var: &Ptr) -> Result> { + info!( + "looking up {} in env: {}", + var.fmt_to_string(store), + self.env.fmt_to_string(store) + ); + lookup_vertex_id(store, &self.env, var) + } + + fn push_binding(&mut self, store: &mut Store, var: Ptr, id: Id) { + let num = store.intern_num(id as u64); + let binding = store.cons(var, num); + self.env = store.cons(binding, self.env); + } + + fn pop_binding(&mut self, store: &Store) -> Result { + let (car, cdr) = store + .car_cdr(&self.env) + .map_err(|_| anyhow!("failed to destructure env"))?; + self.env = cdr; + let (_var, id) = store + .car_cdr(&car) + .map_err(|_| anyhow!("failed to destrcture binding"))?; + + Ok(match store.fetch_num(&id) { + Some(lurk::Num::U64(n)) => (*n) as Id, + _ => { + bail!("binding Id could not be fetched"); + } + }) + } +} + +pub trait Syntax { + fn expand( + &self, + foil: &mut Foil, + store: &mut Store, + head: &Ptr, + rest: &[Ptr], + ) -> Result>> + where + Self: Sized; +} + +#[derive(Clone, Debug)] +pub struct CoilDef, S: Syntax> { + relations: HashMap, + syntax: HashMap, + constructors: HashMap>, + equivalences: HashSet, + _p: PhantomData, +} + +pub struct AsSyntax<'a, T>(&'a T); + +pub struct Let {} + +impl Syntax for Let { + fn expand( + &self, + _foil: &mut Foil, + store: &mut Store, + _head: &Ptr, + rest: &[Ptr], + ) -> Result>> { + let bind = store.intern_symbol(sym!("coil", "bind")); + let pop_binding = store.intern_symbol(sym!("coil", "pop-binding")); + + if rest.is_empty() { + bail!("Let bindings missing"); + } + + let bindings = store.fetch_list(&rest[0]).unwrap(); + + let mut result = Vec::with_capacity((2 * bindings.len()) + rest.len() - 1); + + result.extend(bindings.iter().map(|binding| { + let b = store.fetch_list(binding).unwrap(); + assert_eq!(2, b.len()); + // let var = b[0]; + // let val_form = b[1]; + + // This is also store.cons(bind, binding). + store.cons(bind, *binding) + //store.list(&[bind, var, val_form]) + })); + + result.extend(&rest[1..]); + + let pop_binding_form = store.list(&[pop_binding]); + result.extend(bindings.iter().map(|_| pop_binding_form)); + + Ok(result) + } +} + +#[derive(Default, Debug)] +struct BindRel {} + +#[derive(Default, Debug)] +struct VarRel {} + +impl Relation for BindRel { + fn synthesize>( + &self, + _cs: &mut CS, + _allocated_head: AllocatedNum, + _successors: Vec>, + ) -> Result<(), SynthesisError> { + // TODO: Actually implement constraints enforcing equality of the successors. Ideally, there would also exist a + // mechanism such that this could be implemented without allocating the head -- since the head is not required + // for this. Similarly, we should eventually allow for 'head' values to sometimes be unallocated + // linear-combinations. That is an optimization that can come later, when we focus on improving the generated + // R1CS based on the computation finally assembled. + Ok(()) + } +} +impl Relation for VarRel { + fn synthesize>( + &self, + _cs: &mut CS, + _allocated_head: AllocatedNum, + successors: Vec>, + ) -> Result<(), SynthesisError> { + assert!(successors.is_empty()); + Ok(()) + } +} + +pub enum CoilSyntax { + Let(Let), +} + +impl Syntax for CoilSyntax { + fn expand( + &self, + foil: &mut Foil, + store: &mut Store, + head: &Ptr, + rest: &[Ptr], + ) -> Result>> { + match self { + Self::Let(x) => x.expand(foil, store, head, rest), + } + } +} + +impl, S: Syntax> Default for CoilDef { + fn default() -> Self { + Self { + relations: Default::default(), + syntax: Default::default(), + constructors: Default::default(), + equivalences: Default::default(), + _p: Default::default(), + } + } +} + +impl> CoilDef { + fn new_std() -> Self { + let mut def = Self::default(); + + let let_sym = sym!("lurk", "let"); + let bind = sym!("coil", "bind"); + let _var = sym!("coil", "var"); + + def.register_equivalence(bind); + def.register_syntax(let_sym, CoilSyntax::Let(Let {})); + + def + } +} + +impl, S: Syntax> CoilDef { + fn register_relation(&mut self, sym: Symbol, rel: R) { + self.relations.insert(sym, rel); + } + fn register_syntax(&mut self, sym: Symbol, syn: S) { + self.syntax.insert(sym, syn); + } + fn register_constructor(&mut self, constructor: Symbol, projectors: Vec) { + self.constructors.insert(constructor, projectors); + } + fn register_equivalence(&mut self, equivalence: Symbol) { + self.equivalences.insert(equivalence); + } + fn symbol_func(&self, sym: Symbol) -> Func { + if let Some(projectors) = self.constructors.get(&sym) { + Func::constructor( + sym.to_string(), + projectors.iter().map(Func::from).collect(), + CoilMeta::from(sym), + ) + } else { + Func::from(sym) + } + } + + fn schema(&self) -> Schema { + let mut equivalences: Vec> = self + .equivalences + .iter() + .map(|sym| self.symbol_func(sym.clone())) + .collect(); + + equivalences.sort(); + + let mut constructors: Vec> = self + .constructors + .keys() + .map(|sym| self.symbol_func(sym.clone())) + .collect(); + constructors.sort(); + + Schema { + constructors, + equivalences, + } + } +} + +impl, S: Syntax> MetaMapper for CoilDef { + fn find(&self, meta: &CoilMeta) -> Option<&R> { + self.relations.get(&meta.name) + } +} + +impl<'a, F: LurkField, R: Relation, S: Syntax> MetaMapper + for AsSyntax<'a, CoilDef> +{ + fn find(&self, meta: &CoilMeta) -> Option<&S> { + self.0.syntax.get(&meta.name) + } +} + +impl, S: Syntax> CoilDef { + fn add_to_foil( + &self, + foil: &mut Foil, + store: &mut Store, + context: &mut Context, + expr: &Ptr, + ) -> Result> { + match expr.tag { + ExprTag::Cons => { + info!("adding sexp: {}", expr.fmt_to_string(store)); + + let list = store.fetch_list(expr).expect("sexps must be proper lists"); + let head = list.get(0).ok_or(anyhow!("missing head"))?; + let sym = store.fetch_sym(head).ok_or(anyhow!("sym not in store"))?; + let rest = &list[1..]; + let meta = CoilMeta::from(sym.clone()); + + if let Some(syntax) = AsSyntax::>(self).find(&meta) { + let expanded = syntax.expand(foil, store, head, rest)?; + + let mut last = None; + for (i, x) in expanded.iter().enumerate() { + info!( + "expanded ({} of {}): {}", + i + 1, + expanded.len(), + x.fmt_to_string(store) + ); + + if let Some(vert) = self.add_to_foil(foil, store, context, x)? { + last = Some(vert); + } + } + info!("completed expansion"); + Ok(last) + } else { + if sym == sym!("coil", "pop-binding") { + return self.handle_pop_binding(store, context, rest); + } + + // TODO: don't actually create these literal symbols here. + let successor_verts = if sym == sym!("coil", "bind") { + let var = store + .fetch_sym(&rest[0]) + .ok_or(anyhow!("bind var not in store"))?; + let var_vert = foil.alloc_unique_var(var.to_string()); + + let val_vert = self + .add_to_foil(foil, store, context, &rest[1])? + .ok_or(anyhow!("bind val missing"))?; + + self.handle_bind(store, context, rest, &[var_vert])?; + // return Ok(Some(self.handle_bind(store, context, rest, &[val_vert])?)); + + vec![Some(var_vert), Some(val_vert)] + } else { + rest.iter() + .map(|succ| self.add_to_foil(foil, store, context, succ)) + .collect::>>()? + }; + + info!("adding to foil: {sym:}, {meta:?}"); + let func = self.symbol_func(sym); + + Ok(Some(foil.add_with_meta( + func, + successor_verts.into_iter().flatten().collect(), + meta, + ))) + } + } + ExprTag::Sym => { + info!("adding symbol"); + + if let Some(bound_id) = context + .lookup(store, expr) + .map_err(|_| anyhow!("lookup error"))? + { + Ok(Some(Vert::new(bound_id))) + } else { + let sym = store.fetch_sym(expr).expect("missing sym"); + + Ok(Some(foil.alloc(sym))) + } + } + x => { + dbg!(x); + todo!("intern constant") + } + } + } + + fn handle_bind( + &self, + store: &mut Store, + context: &mut Context, + args: &[Ptr], + successors: &[Vert], + ) -> Result { + if args.len() != 2 { + bail!("bind needs exactly two args") + }; + if successors.len() != 1 { + bail!("bind needs exactly two successors") + }; + + let var = args[0]; + let vert = successors[0]; + info!("binding {} to {}", var.fmt_to_string(store), vert.id()); + + context.push_binding(store, var, vert.id()); + + Ok(vert) + } + fn handle_pop_binding( + &self, + store: &mut Store, + context: &mut Context, + args: &[Ptr], + ) -> Result> { + if !args.is_empty() { + bail!("pop-binding needs exactly zero args") + }; + + context + .pop_binding(store) + .map_err(|_| anyhow!("failed to pop binding"))?; + + Ok(None) + } +} + +impl, S: Syntax> From> for Schema { + fn from(coil_def: CoilDef) -> Self { + coil_def.schema() + } +} +impl, S: Syntax> From<&CoilDef> for Schema { + fn from(coil_def: &CoilDef) -> Self { + coil_def.schema() + } +} + +#[cfg(test)] +mod test { + use super::*; + use crate::congruence::test::assert_expected_classes; + use crate::{FoilConfig, MappedFoil}; + use bellperson::{ + gadgets::num::AllocatedNum, util_cs::test_cs::TestConstraintSystem, Circuit, + ConstraintSystem, SynthesisError, + }; + use generic_array::typenum::U2; + use lurk::circuit::gadgets::constraints::enforce_equal; + use lurk_macros::{let_store, lurk, store}; + use neptune::circuit2::poseidon_hash_allocated as poseidon_hash; + use neptune::poseidon::PoseidonConstants; + use once_cell::sync::Lazy; + use pasta_curves::pallas::Scalar as Fr; + + #[derive(Default, Debug)] + struct ConsRel {} + + #[derive(Default, Debug)] + struct CarRel {} + + #[derive(Default, Debug)] + struct CdrRel {} + + #[derive(Default, Debug)] + struct XxxRel {} + + #[derive(Debug)] + enum TestRel { + Bind(BindRel), + Var(VarRel), + Cons(ConsRel), + Car(CarRel), + Cdr(CdrRel), + Xxx(XxxRel), + } + + static P: Lazy> = Lazy::new(PoseidonConstants::new); + + impl Relation for TestRel { + fn synthesize>( + &self, + cs: &mut CS, + allocated_head: AllocatedNum, + successors: Vec>, + ) -> Result<(), SynthesisError> { + match self { + Self::Bind(x) => x.synthesize(cs, allocated_head, successors), + Self::Var(x) => x.synthesize(cs, allocated_head, successors), + Self::Cons(x) => x.synthesize(cs, allocated_head, successors), + Self::Car(x) => x.synthesize(cs, allocated_head, successors), + Self::Cdr(x) => x.synthesize(cs, allocated_head, successors), + Self::Xxx(x) => x.synthesize(cs, allocated_head, successors), + } + } + } + impl Relation for ConsRel { + fn synthesize>( + &self, + cs: &mut CS, + allocated_head: AllocatedNum, + successors: Vec>, + ) -> Result<(), SynthesisError> { + let allocated_digest = + poseidon_hash(&mut cs.namespace(|| "poseidon hash"), successors, &*P)?; + enforce_equal(cs, || "digest equal", &allocated_head, &allocated_digest); + Ok(()) + } + } + impl Relation for CarRel { + fn synthesize>( + &self, + _cs: &mut CS, + _allocated_head: AllocatedNum, + _successors: Vec>, + ) -> Result<(), SynthesisError> { + // Nothing to do. The constraints are created by the corresponding ConsRel. + Ok(()) + } + } + impl Relation for CdrRel { + fn synthesize>( + &self, + _cs: &mut CS, + _allocated_head: AllocatedNum, + _successors: Vec>, + ) -> Result<(), SynthesisError> { + // Nothing to do. The constraints are created by the corresponding ConsRel. + Ok(()) + } + } + impl Relation for XxxRel { + fn synthesize>( + &self, + _cs: &mut CS, + _allocated_head: AllocatedNum, + _successors: Vec>, + ) -> Result<(), SynthesisError> { + // Nothing to do. The constraints are created by the corresponding ConsRel. + Ok(()) + } + } + + #[test_log::test] + fn test_coil_foil() { + let mut def = CoilDef::<_, _, CoilSyntax>::new_std(); + + //////////////////////////////////////////////////////////////////////////////// + // Set up the CoilDef and Schema + // + // TODO: derive all this from something simpler and declarative. + + // These shouldn't really be .lurk symbols, but until we have better package support, we need to use those. + let cons = sym!("lurk", "cons"); + let car = sym!("lurk", "car"); + let cdr = sym!("lurk", "cdr"); + + let bind = sym!("coil", "bind"); + let var = sym!("coil", "var"); + let xxx = sym!("xxx"); + + def.register_relation(var, TestRel::Var(VarRel {})); + def.register_relation(bind, TestRel::Bind(BindRel {})); + def.register_relation(cons.clone(), TestRel::Cons(ConsRel {})); + def.register_relation(car.clone(), TestRel::Car(CarRel {})); + def.register_relation(cdr.clone(), TestRel::Cdr(CdrRel {})); + def.register_relation(xxx, TestRel::Xxx(XxxRel {})); + + def.register_constructor(cons, vec![car, cdr]); + + let_store!(); // TODO: take field type parameter. This macro currently hard-codes Fr. + + let prog = lurk!((let ((x (cons q r))) + (let ((s (let ((x (cons a b))) + (car x) + (xxx qqq)))) + (car x)))) + .unwrap(); + + let mut foil = Foil::::new( + &def, + FoilConfig { + // This is necessary and should either be made the only option, or be required for Coil. + dedup_var_names: true, + }, + ); + + { + let f = &mut foil; + + let mut context = Context::new(store!()); + def.add_to_foil(f, store!(), &mut context, &prog).unwrap(); + + let classes = dbg!(f.graph.class_info(None)); + + let expected_classes = &[ + (0, vec!["Var(x)[0]: 0"], None), + (1, vec!["Var(q): 1"], None), + (2, vec!["Var(r): 2"], None), + (3, vec!["lurk.cons: 3"], Some(vec![1, 2])), + (4, vec!["coil.bind: 4"], Some(vec![0, 3])), + (5, vec!["Var(s)[1]: 5"], None), + (6, vec!["Var(x)[2]: 6"], None), + (7, vec!["Var(a): 7"], None), + (8, vec!["Var(b): 8"], None), + (9, vec!["lurk.cons: 9"], Some(vec![7, 8])), + (10, vec!["coil.bind: 10"], Some(vec![6, 9])), + (11, vec!["lurk.car: 11"], Some(vec![6])), + (12, vec!["Var(qqq): 12"], None), + (13, vec!["xxx: 13"], Some(vec![12])), + (14, vec!["coil.bind: 14"], Some(vec![5, 13])), + (15, vec!["lurk.car: 15"], Some(vec![0])), + ]; + assert_expected_classes(expected_classes, classes); + } + + { + foil.finalize(); + let classes = dbg!(foil.graph.class_info(None)); + let expected_classes = &[ + ( + 0, + vec!["Var(x)[0]: 0", "lurk.cons: 3", "lurk.cons: 19"], + Some(vec![20, 21]), + ), + (4, vec!["coil.bind: 4"], Some(vec![0, 0])), + (5, vec!["Var(s)[1]: 5", "xxx: 13"], Some(vec![12])), + ( + 6, + vec!["Var(x)[2]: 6", "lurk.cons: 9", "lurk.cons: 16"], + Some(vec![17, 18]), + ), + (10, vec!["coil.bind: 10"], Some(vec![6, 6])), + (12, vec!["Var(qqq): 12"], None), + (14, vec!["coil.bind: 14"], Some(vec![5, 5])), + ( + 17, + vec![ + "Var(a): 7", + "lurk.car: 11", + "Var(lurk.car)[3]: 17", + "lurk.car: 24", + "lurk.car: 26", + ], + Some(vec![6]), + ), + ( + 18, + vec![ + "Var(b): 8", + "Var(lurk.cdr)[4]: 18", + "lurk.cdr: 25", + "lurk.cdr: 27", + ], + Some(vec![6]), + ), + ( + 20, + vec![ + "Var(q): 1", + "lurk.car: 15", + "Var(lurk.car)[5]: 20", + "lurk.car: 22", + "lurk.car: 28", + ], + Some(vec![0]), + ), + ( + 21, + vec![ + "Var(r): 2", + "Var(lurk.cdr)[6]: 21", + "lurk.cdr: 23", + "lurk.cdr: 29", + ], + Some(vec![0]), + ), + ]; + assert_expected_classes(expected_classes, classes); + } + + info!("minimizing"); + + let minimized = foil.minimize(); + let classes = dbg!(minimized.graph.class_info(None)); + + let expected_classes = &[ + (0, vec!["lurk.cons: 0"], Some(vec![6, 7])), + (1, vec!["xxx: 1"], Some(vec![3])), + (2, vec!["lurk.cons: 2"], Some(vec![4, 5])), + (3, vec!["Var(qqq): 3"], None), + (4, vec!["lurk.car: 4"], Some(vec![2])), + (5, vec!["lurk.cdr: 5"], Some(vec![2])), + (6, vec!["lurk.car: 6"], Some(vec![0])), + (7, vec!["lurk.cdr: 7"], Some(vec![0])), + ]; + assert_expected_classes(expected_classes, classes); + + let fx = MappedFoil::new(minimized, def); + let cs = &mut TestConstraintSystem::::new(); + + fx.synthesize(cs).unwrap(); + + // Binary poseidon hash with standard strength is 237 constraints. + // This includes a constraint (and allocation) for the returned digest, + // and another to enforce equality with the `allocated_head` of the relation. + // One constraint and allocation could be optimized away by calling the unallocated + // poseidon-circuit function. However, that may add complexity to witness generation. + // + // 239 * 2 = 478, since there are two conses. + assert_eq!(478, cs.num_constraints()); + } +} diff --git a/foil/src/congruence.rs b/foil/src/congruence.rs new file mode 100644 index 0000000000..3bddf70860 --- /dev/null +++ b/foil/src/congruence.rs @@ -0,0 +1,536 @@ +//! Congruence Closure +//! +//! As described in [Fast Decision Procedures Based on Congruence Closure](https://dl.acm.org/doi/10.1145/322186.322198) + +use log::info; +use std::cell::RefCell; +use std::collections::HashMap; +use std::fmt::{Debug, Display, Formatter}; +use std::hash::Hash; + +use indexmap::IndexSet; + +pub trait LabelTrait: PartialEq + Clone + Display + Debug + Eq {} +pub trait MetaData: PartialEq + Clone + Debug + Default {} + +impl MetaData for () {} + +pub type Id = usize; +pub type SimpleLabel = &'static str; +impl LabelTrait for SimpleLabel {} + +#[derive(Debug, Default, Eq, Clone, PartialEq)] +pub struct Vertex { + id: Id, + label: L, + metadata: T, + predecessors: RefCell>, + successors: RefCell>, + equiv: RefCell, +} + +impl Display for Vertex { + fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), std::fmt::Error> { + write!(fmt, "{}: {}", self.label, self.id) + } +} + +#[derive(Debug, Clone, Copy, Hash, Eq, PartialEq)] +pub struct Vert { + id: Id, +} + +impl From for Vert { + fn from(id: Id) -> Self { + Self::new(id) + } +} + +impl Vert { + pub fn new(id: Id) -> Self { + Self { id } + } + pub fn vertex<'a, T: MetaData, L: LabelTrait>(&'a self, g: &'a Graph) -> &Vertex { + g.vertex(self.id) + } + pub fn id(&self) -> Id { + self.id + } + pub fn congruent(&self, g: &Graph, other: &Self) -> bool { + g.congruent(self.id(), other.id()) + } + pub fn merge(&self, g: &mut Graph, other: &Self) { + g.merge(self.id(), other.id()) + } + pub fn connect<'a, V: IntoIterator, T: MetaData, L: LabelTrait>( + &self, + g: &mut Graph, + targets: V, + ) { + g.connect(self, targets) + } + pub fn find(&self, g: &Graph) -> Id { + g.find(self.id()) + } + pub fn find_vertex<'a, T: MetaData, L: LabelTrait>( + &'a self, + g: &'a Graph, + ) -> &Vertex { + let id = self.find(g); + g.vertex(id) + } +} + +impl From<&Vert> for Id { + fn from(v: &Vert) -> Id { + v.id + } +} +impl From<&Vertex> for Id { + fn from(v: &Vertex) -> Id { + v.id + } +} + +impl Vertex { + pub fn new(id: Id, label: L, metadata: T) -> Self { + Self { + id, + label, + metadata, + successors: Default::default(), + predecessors: Default::default(), + equiv: RefCell::new(id), + } + } + + pub fn id(&self) -> usize { + self.id + } + + pub fn vert(&self) -> Vert { + Vert::new(self.id) + } + + pub fn label(&self) -> &L { + &self.label + } + + pub fn arity(&self) -> usize { + self.successors.borrow().len() + } + + pub fn metadata(&self) -> &T { + &self.metadata + } + + pub fn predecessors(&self) -> RefCell> { + self.predecessors.clone() + } + + pub fn predecessors_owned(&self) -> IndexSet { + self.predecessors.borrow().clone() + } + + pub fn find_predecessor<'a, P: FnMut(&Vertex) -> bool>( + &'a self, + g: &'a Graph, + mut predicate: P, + ) -> Option<&Vertex> { + for id in self.predecessors.borrow().iter() { + let vertex = g.vertex(*id); + if predicate(vertex) { + return Some(vertex); + } + } + None + } + + pub fn successors(&self) -> RefCell> { + self.successors.clone() + } + + pub fn successor(&self, n: usize) -> Option { + self.successors.borrow().get(n).copied() + } + + pub fn equiv(&self) -> Id { + *self.equiv.borrow() + } + + pub fn set_equiv(&self, id: Id) { + *(self.equiv.borrow_mut()) = id; + } +} + +#[derive(Debug, Clone, PartialEq)] +pub struct Graph { + vertices: Vec>, + union_called: bool, +} + +impl Default for Graph { + fn default() -> Self { + Self { + vertices: Default::default(), + union_called: false, + } + } +} + +impl<'a, T: MetaData, L: LabelTrait> Graph { + pub fn alloc>(&'a mut self, label: LL, metadata: T) -> Vert { + // Vertices can never be removed, + let new_id = self.vertices.len(); + self.vertices + .push(Vertex::new(new_id, label.into(), metadata)); + + Vert::new(new_id) + } + + pub fn connect>(&self, source: &Vert, targets: V) { + // union coalesces predecessors into the class representative, + // so the graph must not be modified once it has been called. + assert!(!self.union_called, "connect must not be called after union"); + + let source_id = source.id(); + let target_ids: Vec = targets + .into_iter() + .map(|target_vert| { + // NOTE: We use the target's class representative via find. + let target_find = target_vert.find_vertex(self); + + //target_ids.push(target_find.id()); + target_find.predecessors.borrow_mut().insert(source_id); + + target_find.id() + }) + .collect(); + + // Replace any existing successors. `connect` is not cumulative. + *(source.vertex(self).successors.borrow_mut()) = target_ids; + } + + pub fn vertices(&self) -> &Vec> { + &self.vertices + } + + pub fn vertex(&self, id: Id) -> &Vertex { + &self.vertices[id] + } + + pub fn partition(&self) -> Partition { + self.into() + } + + /// Returns a vector of triples, each represnting the following per equivalence class: + /// - The `Id` of its representative member. + /// - A vector of its members' Vertex's descriptive strings. + /// - An optional vector of its ordered successors, if any. + /// Successor vectors include the `Id` of the class representative at each position, rather than that originally + /// specified. + pub fn class_info( + &self, + p: Option>, + ) -> Vec<(Id, Vec, Option>)> { + let p = p.unwrap_or_else(|| self.partition()); + + let mut classes = p.classes().iter().collect::>(); + classes.sort_by_key(|(id, _)| *id); + + classes + .iter() + .map(|(id, set)| { + let mut class = set + .iter() + .map(|id| (id, format!("{}", self.vertex(*id)), None::>>)) + .collect::>(); + + class.sort_by_key(|x| *x.0); + ( + **id, + class.into_iter().map(|x| x.1).collect(), + p.successors(**id), + ) + }) + .collect() + } + + pub fn find(&self, mut id: Id) -> Id { + // let input_id = id; + loop { + let old_id = id; + let v = self.vertex(id); + id = v.equiv(); + + if id == old_id { + break; + } + } + // info!("find(id{input_id}) => {id}"); + id + } + + pub fn union(&mut self, u: Id, v: Id) { + self.union_called = true; + + let find_u = self.find(u); + let uu = self.vertex(find_u); + + let find_v = self.find(v); + let vv = self.vertex(find_v); + + let l = vv.predecessors.borrow().len(); + for pred in vv.predecessors.borrow_mut().drain(0..l) { + uu.predecessors.borrow_mut().insert(pred); + } + + vv.set_equiv(find_u); + } + + pub fn merge(&mut self, u: Id, v: Id) { + info!("merging {} and {}", self.vertex(u), self.vertex(v)); + let find_u = self.find(u); + let find_v = self.find(v); + + if find_u == find_v { + return; + } + + let p_u = self.vertex(find_u).predecessors().borrow().clone(); + let p_v = self.vertex(find_v).predecessors().borrow().clone(); + info!( + "num predecessors: {}={} and {}={}", + self.vertex(find_u), + p_u.len(), + self.vertex(find_v), + p_v.len() + ); + self.union(u, v); + + for x in p_u.iter() { + for y in p_v.iter() { + info!( + "checking predecesor congruence: {} and {}", + self.vertex(*x), + self.vertex(*y) + ); + let find_x = self.find(*x); + let find_y = self.find(*y); + + if find_x != find_y && self.congruent(*x, *y) { + info!("recursive merge"); + // TODO: We might need or want an explicit stack rather than recursive call. + self.merge(*x, *y) + } + } + } + } + + pub fn congruent(&self, u: Id, v: Id) -> bool { + info!( + "checking congruence of {} and {}", + self.vertex(u), + self.vertex(v) + ); + let u_succ = self.vertex(u).successors(); + let v_succ = self.vertex(v).successors(); + + let labels_equal = self.vertex(u).label == self.vertex(v).label; + + let result = labels_equal + && u_succ.borrow().len() == v_succ.borrow().len() + && u_succ + .borrow() + .iter() + .zip(v_succ.borrow().iter()) + .all(|(x, y)| self.find(*x) == self.find(*y)); + if result { + info!("congruent") + } else { + info!("not congruent") + } + result + } + + /// Partition `self` (a `Graph`), filtering vertices to those for which `predicate` is true. + pub fn to_partition) -> bool>(&self, predicate: F) -> Partition { + let mut classes: HashMap> = Default::default(); + let mut index: HashMap = Default::default(); + let mut successors: HashMap> = Default::default(); + let mut labels: HashMap = Default::default(); + let mut metadata: HashMap = Default::default(); + + for (id, _v) in self + .vertices + .iter() + .enumerate() + .filter(|(_, v)| predicate(*v)) + { + let find_v = self.find(id); + let vertex = self.vertex(id); + let successor_ids = vertex + .successors() + .borrow() + .iter() + .map(|id| self.find(*id)) + .collect::>(); + + if !successor_ids.is_empty() { + dbg!(&successor_ids); + successors.insert(find_v, successor_ids); + + // The label we want is that of the original vertex that has successors. By definition, this must be the + // same for all such vertices in an equivalence class. + labels.insert(find_v, vertex.label().clone()); + + // Same goes for the metadata. + metadata.insert(find_v, vertex.metadata().clone()); + info!( + "partition, assigning {id} to class {find_v} with label {:?} and metadata {:?}", + vertex.label(), + vertex.metadata() + ); + } else { + info!("partition, assigning {id} to class {find_v}",); + } + classes + .entry(find_v) + .and_modify(|set| { + (*set).insert(id); + }) + .or_insert_with(|| IndexSet::from([find_v, id])); + index.insert(id, find_v); + } + Partition { + classes, + index, + successors, + labels, + metadata, + } + } +} + +#[derive(Debug, Default, Clone, PartialEq)] +pub struct Partition { + // mapping from unique representative to all members of equivalence classes + pub classes: HashMap>, + // mapping from members to the unique representative indexing the class + pub index: HashMap, + // successors of the class, indexed by representative + // all successors are themselves class representatives (via find). + pub successors: HashMap>, + pub labels: HashMap, + pub metadata: HashMap, +} + +impl Partition { + pub fn class(&self, id: Id) -> Option<&IndexSet> { + self.index + .get(&id) + .and_then(|index| self.classes.get(index)) + } + + pub fn classes(&self) -> &HashMap> { + &self.classes + } + + pub fn index(&self) -> &HashMap { + &self.index + } + pub fn successors(&self, id: Id) -> Option> { + self.successors.get(&id).cloned() + } + pub fn label(&self, id: Id) -> Option<&L> { + self.labels.get(&id) + } + + pub fn metadata(&self, id: Id) -> Option<&T> { + self.metadata.get(&id) + } + + pub fn size(&self) -> usize { + self.index.len() + } + + pub fn find(&self, id: Id) -> Id { + *self.index.get(&id).expect("invalid id") + } +} + +impl From<&Graph> for Partition { + fn from(g: &Graph) -> Self { + g.to_partition(|_| true) + } +} + +#[cfg(test)] +pub(crate) mod test { + use super::*; + + pub type IdVec = Vec; + pub(crate) fn assert_expected_classes( + expected: &[(Id, Vec<&str>, Option)], + actual: Vec<(Id, Vec, Option)>, + ) { + assert_eq!(expected.len(), actual.len()); + for ((expected_id, expected_class, expected_successors), (id, class, successors)) in + expected.iter().zip(actual.iter()) + { + assert_eq!(expected_id, id); + for (expected_member, member) in expected_class.iter().zip(class.iter()) { + assert_eq!(expected_member, &member); + } + assert_eq!(expected_successors, successors); + } + } + + #[test] + fn test_congruence() { + let g = &mut Graph::<(), SimpleLabel>::default(); + + // See Figure 1 of the paper. + // + // f<--f + // / \ / + // a b + let v1 = g.alloc("f", ()); + let v2 = g.alloc("f", ()); + let v3 = g.alloc("a", ()); + let v4 = g.alloc("b", ()); + + v1.connect(g, &[v2, v4]); + v2.connect(g, &[v3, v4]); + + { + let partition = g.partition(); + + assert_eq!(partition.class(0), Some(&IndexSet::from([0]))); + assert_eq!(partition.class(1), Some(&IndexSet::from([1]))); + assert_eq!(partition.class(2), Some(&IndexSet::from([2]))); + assert_eq!(partition.class(3), Some(&IndexSet::from([3]))); + } + assert!(!v1.congruent(g, &v2)); + assert!(!v1.congruent(g, &v3)); + assert!(!v1.congruent(g, &v4)); + assert!(!v2.congruent(g, &v3)); + assert!(!v2.congruent(g, &v4)); + assert!(!v3.congruent(g, &v4)); + + v2.merge(g, &v3); + + { + let partition = dbg!(g.partition()); + + assert_eq!(partition.class(0), Some(&IndexSet::from([0, 1, 2]))); + assert_eq!(partition.class(1), Some(&IndexSet::from([0, 1, 2]))); + assert_eq!(partition.class(2), Some(&IndexSet::from([0, 1, 2]))); + assert_eq!(partition.class(3), Some(&IndexSet::from([3]))); + } + + assert!(v1.congruent(g, &v2)); + assert_eq!(g.find(v2.id()), g.find(v3.id())); + assert!(!v3.congruent(g, &v4)); + } +} diff --git a/foil/src/constructors.rs b/foil/src/constructors.rs new file mode 100644 index 0000000000..f54cc78d21 --- /dev/null +++ b/foil/src/constructors.rs @@ -0,0 +1,697 @@ +//! Congruence Closure extended with constructors and projectors. +//! The `constructors` module is just an example of how `Foil` can be used. +//! The enum-based implementation of `Fun` is not necessary, just a somewhat simple way to +//! make a small, self-contained example. + +use crate::{Func, Label, Meta, Schema}; + +#[derive(Clone, Copy, Eq, PartialEq, Hash)] +enum Fun { + Car, + Cdr, + Cons, + Binding, + Add, +} + +impl Fun { + fn equivalences() -> Vec> { + vec![Self::Binding.into()] + } + fn constructors() -> Vec> { + vec![Self::Cons.into()] + } + fn schema() -> Schema { + Schema { + equivalences: Self::equivalences(), + constructors: Self::constructors(), + } + } +} + +impl From for Func { + fn from(fun: Fun) -> Self { + match fun { + Fun::Car => Self::new("Car"), + Fun::Cdr => Self::new("Cdr"), + Fun::Cons => Self::constructor( + "Cons", + vec![Fun::Car.into(), Fun::Cdr.into()], + Meta::default(), + ), + Fun::Binding => Self::new("Binding"), + Fun::Add => Self::new("Add"), + } + } +} + +impl From for Label { + fn from(fun: Fun) -> Self { + Self::from(Func::::from(fun)) + } +} + +#[cfg(test)] +mod test { + use super::*; + use crate::congruence::{test::assert_expected_classes, Graph}; + use crate::{Foil, FoilConfig, Label, Meta, Var}; + + /* + * In Lurk context, we can generalize the treatment of 'Quantifier-Free Theory of Equality' with 'Extensions to Theory of List Structure'. + *** Procedure to extend CC to deal with CAR, CDR, and CONS. + - Start with graph of uninterpreted functions, with equivalence relation + - For every CONS, add a unary CAR and unary CDR vertex whose target is the CONS. + - MERGE the CAR with CONS[1] (1-indexed), and merge the CDR with CONS[2]. + *** We can generalize this for Lurk, to deal with N-ary constructors and their respective projection operators. + **** For example, in a notional world where CONS is a binary hash (unlike Lurk's concrete use of hashes): + - CONS = HASH2 + - CAR = HASH2-PROJECT1 + - CDR = HASH2-PROJECT2 + **** Then a 3-ary hash (i.e. a triple constructor) would yield: + - TRIPLE = HASH3 + - HASH3-PROJECT1 + - HASH3-PROJECT2 + - HASH3-PROJECT3 + **** In each case, the same procedure is followed: + - extend the graph to add missing projection operators + - MERGE with the concrete projections + *** We can also perform the complementary extension, to find congruence between the CONS(tructors) implied by projectors. + Conder this example: + + (lambda (a) + (let ((x (car a)) + (y (cdr a))) + (+ x y))) + + The proof of this expression should only require proof of a single CONS. + + This: + A<-CAR<=X + \ + + + / + A<-CDR<=Y + + Becomes: + B + \ + CONS(1)<=A + / \ + C CAR<=X + \ + + + / + D CDR<=Y + \ / + CONS(2)<=A + / + E + + Then: + - MERGE B and CAR + - MERGE E and CDR + + But because we now have new CONSes, we need to add missing projectors. (Should this happen before or after the previous MERGEs?) + + NOTE: Actually, we don't need to add CAR(2) and CDR(2) because they are redundant. The right procedure is to check for + the existence of CAR(1) and CDR(1). Since they exist, we should perform the next MERGE using those instead. + + B CDR(2) + \ / + CONS(1)<=A + / \ + C CAR(1)<=X + \ + + + / + D CDR(1)<=Y + \ / + CONS(2)<=A + / \ + E CAR(2) + + Then: + - MERGE CDR and C + - MERGE CAR and D + + NOTE: In this example, since we added CAR(2) and CDR(2), if we merged those just above, then we should also merge them + with their pre-existing counterparts. + - MERGE CAR(1) and CAR(2) + - MERGE CDR(1) and CDR(2) + + Now we have the following partition: + - 1: {B, CAR(1), CAR(2), D, X} + - 2: {E, CDR(1), CDR(2), C, Y} + - 3: {A, CONS(1), CONS(2)} + - 4: {+} + + With this graph: + + 1 + / \ + 3 4 + \ / + 2 + + Or equivalently: + + X:CAR + / \ + A:CONS + + \ / + Y:CDR + #+end_src + + */ + + #[test_log::test] + fn test_deduce_constructor() { + // This was the original test described above. + + // (let ((x (car a)) + // (y (cdr a))) + // (+ x y))) + + type G = Graph<(), Label>; + let g = &mut G::default(); + + let a = g.alloc(Var::new("a"), ()); + let x = g.alloc(Var::new("x"), ()); + let y = g.alloc(Var::new("y"), ()); + let car = g.alloc(Fun::Car, ()); + let cdr = g.alloc(Fun::Cdr, ()); + let bind_x = g.alloc(Fun::Binding, ()); + let bind_y = g.alloc(Fun::Binding, ()); + let plus = g.alloc(Fun::Add, ()); + + car.connect(g, &[a]); + cdr.connect(g, &[a]); + + // These binding nodes are not really necessary, but they may be useful for bookkeeping. Actually, for our + // purposes, it probably makes sense to use these as the sole indicators of explicit equality. + // These can mark the vertices to be merged, and those merges can be performed programmatically. + // New vertices that need to be added first can add pending merges by creating these connections. + // Binding is probably the wrong term in that context, though. TODO: Better name. + bind_x.connect(g, &[x, car]); + bind_y.connect(g, &[y, cdr]); + + plus.connect(g, &[x, y]); + + let cons = g.alloc(Fun::Cons, ()); + let car1 = g.alloc(Fun::Car, ()); + let cdr1 = g.alloc(Fun::Cdr, ()); + let b = g.alloc(Var::new("b"), ()); + let c = g.alloc(Var::new("c"), ()); + + cons.connect(g, &[b, c]); + + car1.connect(g, &[cons]); + cdr1.connect(g, &[cons]); + + // All merges must follow all connections. + + // This effects the equivalences the bindings signal. + x.merge(g, &car); + y.merge(g, &cdr); + + // This adds the Cons. We know this is needed because `a` has a predecessor that is labeled `Car` and one that is + // labeled `Cdr`. Either would suffice to require this new vertex labeled `Cons` to be added. Such an added cons + // must be merged with the vertex that forced its creation. + a.merge(g, &cons); + + // When a new `Cons` is created, corresponding projection (`Car` and `Cdr`) vertices are created, and their axiomatic + // equivalence to the `Cons`'s successors must be asserted by merging them. + b.merge(g, &car1); + c.merge(g, &cdr1); + + // The bindings each inhabit singleton equivalence classes and can be removed. + let actual_classes = dbg!(g.class_info(None)); + let expected_classes = &[ + // Notice that variable a has been labeld as a cons. + (0, vec!["Var(a): 0", "Cons: 8"], Some(vec![11, 12])), + // Notice that now the bindings point to identical vertices. That is because their potentially distinct + // successors have been merged, by virtue of `Binding` having been specified as an 'equivalence' in the schema. + (5, vec!["Binding: 5"], Some(vec![11, 11])), + (6, vec!["Binding: 6"], Some(vec![12, 12])), + (7, vec!["Add: 7"], Some(vec![11, 12])), + ( + 11, + vec!["Var(x): 1", "Car: 3", "Car: 9", "Var(b): 11"], + Some(vec![0]), + ), + ( + 12, + vec!["Var(y): 2", "Cdr: 4", "Cdr: 10", "Var(c): 12"], + Some(vec![0]), + ), + ]; + assert_expected_classes(expected_classes, actual_classes); + } + + #[test_log::test] + fn test_auto_deduce_constructor() { + // This is the original test with all the 'annotation' (i.e. the added vertices and equivalences) automated. + + // (let ((x (car a)) + // (y (cdr a))) + // (+ x y))) + + let f = &mut Foil::<(), Meta>::new(Fun::schema(), FoilConfig::default()); + + let a = f.alloc(Var::new("a")); + let x = f.alloc(Var::new("x")); + let y = f.alloc(Var::new("y")); + let car = f.alloc(Fun::Car); + let cdr = f.alloc(Fun::Cdr); + let bind_x = f.alloc(Fun::Binding); + let bind_y = f.alloc(Fun::Binding); + let plus = f.alloc(Fun::Add); + + f.connect(&car, &[a]); + f.connect(&cdr, &[a]); + + // These binding nodes are not really necessary, but they may be useful for bookkeeping. Actually, for our + // purposes, it probably makes sense to use these as the sole indicators of explicit equality. + // These can mark the vertices to be merged, and those merges can be performed programmatically. + // New vertices that need to be added first can add pending merges by creating these connections. + // Binding is probably the wrong term in that context, though. TODO: Better name. + f.connect(&bind_x, &[x, car]); + f.connect(&bind_y, &[y, cdr]); + + f.connect(&plus, &[x, y]); + + f.finalize(); + + let actual_classes = dbg!(f.graph.class_info(None)); + + // Notice that the final equivalence classes correspond to those predicted in the analysis (which preceded the implementation): + /* + Now we have the following partition: + - 1: {B, CAR(1), CAR(2), D, X} + - 2: {E, CDR(1), CDR(2), C, Y} + - 3: {A, CONS(1), CONS(2)} + - 4: {+} + */ + + let expected_classes = &[ + ( + 0, + // {A, CONS(1), CONS(2)} + vec!["Var(a): 0", "Cons: 8", "Cons: 11"], + Some(vec![1, 2]), + ), + ( + 1, + // {B, CAR(1), CAR(2), D, X} + vec![ + "Var(x): 1", + "Car: 3", + "Var(Car)[0]: 9", + "Var(Car)[2]: 12", + "Car: 14", + "Car: 16", + ], + Some(vec![0]), + ), + ( + 2, + // {E, CDR(1), CDR(2), C, Y} + vec![ + "Var(y): 2", + "Cdr: 4", + "Var(Cdr)[1]: 10", + "Var(Cdr)[3]: 13", + "Cdr: 15", + "Cdr: 17", + ], + Some(vec![0]), + ), + // These 'Binding's are syntactic and can be removed from the graph. They may have been explicit in the + // source from which the graph was generated, but their children (the bound vars/values) are now equivalent + // in the graph. + (5, vec!["Binding: 5"], Some(vec![1, 1])), + (6, vec!["Binding: 6"], Some(vec![2, 2])), + (7, vec!["Add: 7"], Some(vec![1, 2])), + ]; + + assert_expected_classes(expected_classes, actual_classes); + } + + #[test_log::test] + fn test_simplify_minimal() { + // This is a test showing that the car of a 'cons' is understood to be the first input to the cons expression + // that produced it. + + // (let* ((a (cons b c)) + // (d (car a))) + // ...) + let f = &mut Foil::<(), Meta>::new(Fun::schema(), FoilConfig::default()); + + let a = f.alloc(Var::new("a")); + let b = f.alloc(Var::new("b")); + let c = f.alloc(Var::new("c")); + let d = f.alloc(Var::new("d")); + let cons1 = f.alloc(Fun::Cons); + let car = f.alloc(Fun::Car); + let bind_a = f.alloc(Fun::Binding); + let bind_d = f.alloc(Fun::Binding); + + f.connect(&bind_a, &[a, cons1]); + f.connect(&cons1, &[b, c]); + + f.connect(&bind_d, &[d, car]); + f.connect(&car, &[a]); + + f.finalize(); + + // We want to see that b and d are in the same equivalence class. + + let actual_classes = dbg!(f.graph.class_info(None)); + + let expected_classes = &[ + ( + 0, + vec!["Var(a): 0", "Cons: 4", "Cons: 8"], + Some(vec![3, 10]), + ), + ( + 3, + // Notice that variables b and d are in the same equivalence class. + vec![ + "Var(b): 1", + "Var(d): 3", + "Car: 5", + "Var(Car)[0]: 9", + "Car: 11", + "Car: 13", + ], + Some(vec![0]), + ), + (6, vec!["Binding: 6"], Some(vec![0, 0])), + (7, vec!["Binding: 7"], Some(vec![3, 3])), + ( + 10, + vec!["Var(c): 2", "Var(Cdr)[1]: 10", "Cdr: 12", "Cdr: 14"], + Some(vec![0]), + ), + ]; + + assert_expected_classes(expected_classes, actual_classes); + + let minimized = f.minimize(); + assert!(minimized.is_minimized()); + let minimized_classes = dbg!(minimized.graph.class_info(None)); + + let expected_minimized = &[ + // Notice that all equivalence classes have exactly one member, + // and that its member corresponds to the Func it represents (if any). + (0, vec!["Cons: 0"], Some(vec![1, 2])), + (1, vec!["Car: 1"], Some(vec![0])), + (2, vec!["Cdr: 2"], Some(vec![0])), + ]; + + assert_expected_classes(expected_minimized, minimized_classes); + } + + #[test_log::test] + fn test_auto_simplify_harder() { + // This is a more elaborate version of the minimal test. + + // (let* ((a (cons b c)) + // (d (car a)) + // (e (cdr a)) + // (f (cons d e))) + // (+ a f)) + let f = &mut Foil::<(), Meta>::new(Fun::schema(), FoilConfig::default()); + + let a = f.alloc(Var::new("a")); + let b = f.alloc(Var::new("b")); + let c = f.alloc(Var::new("c")); + let cons1 = f.alloc(Fun::Cons); + f.connect(&cons1, &[b, c]); + let bind_a = f.alloc(Fun::Binding); + f.connect(&bind_a, &[a, cons1]); + + let car = f.alloc(Fun::Car); + f.connect(&car, &[a]); + let d = f.alloc(Var::new("d")); + let bind_d = f.alloc(Fun::Binding); + f.connect(&bind_d, &[d, car]); + + let cdr = f.alloc(Fun::Cdr); + f.connect(&cdr, &[a]); + let e = f.alloc(Var::new("e")); + let bind_e = f.alloc(Fun::Binding); + f.connect(&bind_e, &[e, cdr]); + + let cons2 = f.alloc(Fun::Cons); + f.connect(&cons2, &[d, e]); + let bind_ff = f.alloc(Fun::Binding); + let ff = f.alloc(Var::new("ff")); + f.connect(&bind_ff, &[ff, cons2]); + + let plus = f.alloc(Fun::Add); + f.connect(&plus, &[a, ff]); + + f.finalize(); + + let actual_classes = dbg!(f.graph.class_info(None)); + + let expected_classes = &[ + ( + 6, + vec![ + "Var(b): 1", + "Car: 5", + "Var(d): 6", + "Var(Car)[0]: 16", + "Var(Car)[2]: 19", + "Car: 21", + "Car: 23", + "Car: 25", + "Car: 27", + ], + Some(vec![13]), + ), + (7, vec!["Binding: 7"], Some(vec![6, 6])), + ( + 9, + vec![ + "Var(c): 2", + "Cdr: 8", + "Var(e): 9", + "Var(Cdr)[1]: 17", + "Var(Cdr)[3]: 20", + "Cdr: 22", + "Cdr: 24", + "Cdr: 26", + "Cdr: 28", + ], + Some(vec![13]), + ), + (10, vec!["Binding: 10"], Some(vec![9, 9])), + (12, vec!["Binding: 4", "Binding: 12"], Some(vec![13, 13])), + ( + 13, + vec![ + "Var(a): 0", + "Cons: 3", + "Cons: 11", + "Var(ff): 13", + "Cons: 15", + "Cons: 18", + ], + Some(vec![6, 9]), + ), + (14, vec!["Add: 14"], Some(vec![13, 13])), + ]; + + assert_expected_classes(expected_classes, actual_classes); + + let minimized = f.minimize(); + assert!(minimized.is_minimized()); + let minimized_classes = dbg!(minimized.graph.class_info(None)); + + let expected_minimized = &[ + (0, vec!["Car: 0"], Some(vec![2])), + (1, vec!["Cdr: 1"], Some(vec![2])), + (2, vec!["Cons: 2"], Some(vec![0, 1])), + (3, vec!["Add: 3"], Some(vec![2, 2])), + ]; + + assert_expected_classes(expected_minimized, minimized_classes); + } + + #[test_log::test] + fn test_var_equivalence() { + // Allocate distinct vertices for each instance of `a`: + // + // TODO: But do we really *want* this behavior, or should it be possible for multiple vertices to be labeled by + // the same var? Currently, we resolve this ambiguity by requiring 'unique' vars to be allocated when that + // behavior is desired (for example, projectors). + // + // The alternate behavior might actually be more natural when variables may be shadowed and therefore share + // names while representing unique values. + // + // (let ((a (cons x y)) + // (b (car a)) + // (c (cdr a))) + // (cons b c))) + let f = &mut Foil::<(), Meta>::new( + Fun::schema(), + FoilConfig { + dedup_var_names: true, + }, + ); + let f2 = &mut Foil::<(), Meta>::new( + Fun::schema(), + FoilConfig { + dedup_var_names: false, + }, + ); + + let setup = |f: &mut Foil<(), Meta>| { + let a1 = f.alloc(Var::new("a")); + let a2 = f.alloc(Var::new("a")); + let a3 = f.alloc(Var::new("a")); + let x = f.alloc(Var::new("x")); + let y = f.alloc(Var::new("y")); + let b = f.alloc(Var::new("b")); + let c = f.alloc(Var::new("c")); + let cons1 = f.alloc(Fun::Cons); + let cons2 = f.alloc(Fun::Cons); + let car = f.alloc(Fun::Car); + let cdr = f.alloc(Fun::Cdr); + let bind_a = f.alloc(Fun::Binding); + let bind_b = f.alloc(Fun::Binding); + let bind_c = f.alloc(Fun::Binding); + + f.connect(&cons1, &[x, y]); + f.connect(&cons2, &[b, c]); + f.connect(&car, &[a2]); + f.connect(&cdr, &[a3]); + f.connect(&bind_a, &[a1, cons1]); + f.connect(&bind_b, &[b, car]); + f.connect(&bind_c, &[c, cdr]); + }; + + setup(f); + setup(f2); + + f.finalize(); + f2.finalize(); + + let actual_classes = dbg!(f.graph.class_info(None)); + let f2_actual_classes = dbg!(f2.graph.class_info(None)); + let expected_classes = &[ + ( + 5, + vec![ + "Var(x): 3", + "Var(b): 5", + "Car: 9", + "Var(Car)[0]: 15", + "Var(Car)[2]: 18", + "Car: 20", + "Car: 22", + "Car: 24", + "Car: 26", + ], + Some(vec![8]), + ), + ( + 6, + vec![ + "Var(y): 4", + "Var(c): 6", + "Cdr: 10", + "Var(Cdr)[1]: 16", + "Var(Cdr)[3]: 19", + "Cdr: 21", + "Cdr: 23", + "Cdr: 25", + "Cdr: 27", + ], + Some(vec![8]), + ), + ( + 8, + vec![ + "Var(a): 0", + "Var(a): 1", + "Var(a): 2", + "Cons: 7", + "Cons: 8", + "Cons: 14", + "Cons: 17", + ], + Some(vec![5, 6]), + ), + (11, vec!["Binding: 11"], Some(vec![8, 8])), + (12, vec!["Binding: 12"], Some(vec![5, 5])), + (13, vec!["Binding: 13"], Some(vec![6, 6])), + ]; + assert_expected_classes(expected_classes, actual_classes); + + let f2_expected_classes = &[ + // Notice that there are three distinct `a` variables, each of which has been deduced to be a cons. + // Because we did not 'dedup' these (per the config), they manifest as three distinct conses. + (0, vec!["Var(a): 0", "Cons: 7"], Some(vec![3, 4])), + (1, vec!["Var(a): 1", "Cons: 14"], Some(vec![5, 16])), + (2, vec!["Var(a): 2", "Cons: 17"], Some(vec![18, 6])), + (3, vec!["Var(x): 3", "Car: 20"], Some(vec![0])), + (4, vec!["Var(y): 4", "Cdr: 21"], Some(vec![0])), + ( + 5, + vec!["Var(b): 5", "Car: 9", "Var(Car): 15", "Car: 22", "Car: 24"], + Some(vec![1]), + ), + ( + 6, + vec!["Var(c): 6", "Cdr: 10", "Var(Cdr): 19", "Cdr: 23", "Cdr: 27"], + Some(vec![2]), + ), + // Because the previous `(car a)` and `(cdr a)` were not discovered to refer to projections of the same + // cons, The cons joining them is not identified with some existing cons and instead appears as yet another + // unique cons in the graph. + (8, vec!["Cons: 8"], Some(vec![5, 6])), + (11, vec!["Binding: 11"], Some(vec![0, 0])), + (12, vec!["Binding: 12"], Some(vec![5, 5])), + (13, vec!["Binding: 13"], Some(vec![6, 6])), + (16, vec!["Var(Cdr): 16", "Cdr: 25"], Some(vec![1])), + (18, vec!["Var(Car): 18", "Car: 26"], Some(vec![2])), + ]; + + assert_expected_classes(f2_expected_classes, f2_actual_classes); + + let minimized = f.minimize(); + let f2_minimized = f2.minimize(); + assert!(minimized.is_minimized()); + assert!(f2_minimized.is_minimized()); + let minimized_classes = dbg!(minimized.graph.class_info(None)); + let f2_minimized_classes = dbg!(f2_minimized.graph.class_info(None)); + + let expected_minimized = &[ + (0, vec!["Car: 0"], Some(vec![2])), + (1, vec!["Cdr: 1"], Some(vec![2])), + (2, vec!["Cons: 2"], Some(vec![0, 1])), + ]; + + assert_expected_classes(expected_minimized, minimized_classes); + + let f2_expected_minimized = &[ + (0, vec!["Cons: 0"], Some(vec![3, 4])), + (1, vec!["Cons: 1"], Some(vec![5, 8])), + (2, vec!["Cons: 2"], Some(vec![9, 6])), + (3, vec!["Car: 3"], Some(vec![0])), + (4, vec!["Cdr: 4"], Some(vec![0])), + (5, vec!["Car: 5"], Some(vec![1])), + (6, vec!["Cdr: 6"], Some(vec![2])), + (7, vec!["Cons: 7"], Some(vec![5, 6])), + (8, vec!["Cdr: 8"], Some(vec![1])), + (9, vec!["Car: 9"], Some(vec![2])), + ]; + assert_expected_classes(f2_expected_minimized, f2_minimized_classes); + } +} diff --git a/foil/src/lib.rs b/foil/src/lib.rs new file mode 100644 index 0000000000..cee8a0ee2d --- /dev/null +++ b/foil/src/lib.rs @@ -0,0 +1,725 @@ +#![allow(dead_code)] + +//! FOIL +//! Flat Optimization Intermediate Language +use log::{info, warn}; +use std::collections::{HashMap, HashSet, VecDeque}; +use std::fmt::{Debug, Display, Formatter}; +use std::hash::Hash; +use std::marker::PhantomData; + +use anyhow::{bail, Error}; +use indexmap::IndexSet; + +pub mod circuit; +pub mod coil; +pub mod congruence; +pub mod constructors; + +pub use circuit::Relation; +pub use congruence::{Graph, Id, LabelTrait, MetaData, Vert}; + +#[derive(Debug, Clone, Hash, PartialEq, Eq, PartialOrd, Ord)] +pub struct Func { + name: String, + projectors: Option>, + // For now, we need to keep metadata with Funcs so it can be reproduced when automatically allocating new + // constructors and projectors. This is basically due to Funcs in the Schema acting as prototypes. + metadata: M, +} + +impl Display for Func { + fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), std::fmt::Error> { + write!(fmt, "{}", self.name) + } +} + +#[derive(Debug, Default, Clone, Hash, PartialEq, Eq)] +pub struct Schema { + equivalences: Vec>, + constructors: Vec>, +} + +impl Schema { + pub fn equivalences(&self) -> Vec> { + self.equivalences.clone() + } + pub fn constructors(&self) -> Vec> { + self.constructors.clone() + } + pub fn add_constructor(&mut self, constructor: Func, _metadata: T) { + self.constructors.push(constructor) + } +} + +impl Func { + pub fn new>(name: S) -> Self { + Self { + name: name.into(), + projectors: None, + metadata: T::default(), + } + } + pub fn new_with_metadata>(name: S, metadata: T) -> Self { + Self { + name: name.into(), + projectors: None, + metadata, + } + } + pub fn constructor>(name: S, projectors: Vec, metadata: T) -> Self { + Self { + name: name.into(), + projectors: Some(projectors), + metadata, + } + } + pub fn name(&self) -> &String { + &self.name + } + pub fn metadata(&self) -> &T { + &self.metadata + } + pub fn projectors(&self) -> Option<&Vec> { + self.projectors.as_ref() + } +} + +#[derive(Debug, Eq, Clone, Hash, PartialEq)] +pub struct FoilConfig { + /// If `dedup_var_names` is `true`, `Var`s with identical names will be merged when finalizing. + /// This option may be removed if it becomes clear that one setting is preferred. + dedup_var_names: bool, +} + +impl Default for FoilConfig { + fn default() -> Self { + Self { + dedup_var_names: true, + } + } +} + +#[derive(Debug, Clone)] +pub struct Foil { + graph: G, + merge_queue: VecDeque<(Id, Id)>, + fun_map: HashMap>, + var_map: HashMap>, + var_counter: usize, + constants: HashMap, + schema: Schema, + state: State, + config: FoilConfig, +} + +#[derive(Debug, Default, Eq, Clone, Hash, PartialEq)] +pub struct Var(pub String, pub Option); + +impl Var { + pub fn new>(name: S) -> Self { + Self(name.into(), None) + } +} + +impl Display for Var { + fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), std::fmt::Error> { + let res = write!(fmt, "Var({})", self.0); + if let Some(id) = self.1 { + write!(fmt, "[{}]", id) + } else { + res + } + } +} + +#[derive(Debug, Clone, Hash, PartialEq)] +pub enum Label { + F(String), + V(String, Option), +} + +impl Eq for Label {} + +impl Label { + pub fn var>(name: S) -> Self { + Var(name.into(), None).into() + } +} + +impl Display for Label { + fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), std::fmt::Error> { + match self { + Self::F(f) => std::fmt::Display::fmt(&f, fmt), + Self::V(_, _) => std::fmt::Display::fmt(&Var::from(self), fmt), + } + } +} + +impl LabelTrait for Label {} + +impl From for Label { + fn from(v: Var) -> Self { + Self::V(v.0, v.1) + } +} +impl From<&Var> for Label { + fn from(v: &Var) -> Self { + Self::V(v.0.clone(), v.1) + } +} + +impl From