From 4ca0808b780d5426e294b069f9dc3a3c45bf04eb Mon Sep 17 00:00:00 2001 From: porcuquine Date: Wed, 26 Jul 2023 18:51:06 -0700 Subject: [PATCH] Initial FOIL implemenation. --- Cargo.lock | 252 +++++++++-------- Cargo.toml | 2 + src/foil/circuit.rs | 81 ++++++ src/foil/congruence.rs | 493 ++++++++++++++++++++++++++++++++++ src/foil/constructors.rs | 526 ++++++++++++++++++++++++++++++++++++ src/foil/mod.rs | 564 +++++++++++++++++++++++++++++++++++++++ src/lib.rs | 1 + 7 files changed, 1787 insertions(+), 132 deletions(-) create mode 100644 src/foil/circuit.rs create mode 100644 src/foil/congruence.rs create mode 100644 src/foil/constructors.rs create mode 100644 src/foil/mod.rs diff --git a/Cargo.lock b/Cargo.lock index 27bf56d355..6166eb8186 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -162,13 +162,13 @@ dependencies = [ [[package]] name = "async-trait" -version = "0.1.71" +version = "0.1.72" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a564d521dd56509c4c47480d00b80ee55f7e385ae48db5744c67ad50c92d2ebf" +checksum = "cc6dde6e4ed435a4c1ee4e73592f5ba9da2151af10076cc04858746af9352d09" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.27", ] [[package]] @@ -528,9 +528,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.3.17" +version = "4.3.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5b0827b011f6f8ab38590295339817b0d26f344aa4932c3ced71b45b0c54b4a9" +checksum = "5fd304a20bff958a57f04c4e96a2e7594cc4490a0e809cbd48bb6437edaa452d" dependencies = [ "clap_builder", "clap_derive 4.3.12", @@ -549,9 +549,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.3.17" +version = "4.3.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9441b403be87be858db6a23edb493e7f694761acdc3343d5a0fcaafd304cbc9e" +checksum = "01c6a3f08f1fe5662a35cfe393aec09c4df95f60ee93b7556505260f75eee9e1" dependencies = [ "anstream", "anstyle", @@ -568,7 +568,7 @@ dependencies = [ "heck 0.4.1", "proc-macro-error", "proc-macro2 1.0.66", - "quote 1.0.31", + "quote 1.0.32", "syn 1.0.109", ] @@ -580,8 +580,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.27", ] [[package]] @@ -617,7 +617,7 @@ dependencies = [ "anyhow", "assert_cmd", "blstrs", - "clap 4.3.17", + "clap 4.3.19", "fcomm", "ff", "lurk", @@ -899,9 +899,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" @@ -916,7 +916,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", @@ -980,8 +993,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.27", ] [[package]] @@ -992,12 +1005,9 @@ checksum = "8ba569491c70ec8471e34aa7e9c0b9e82bb5d2464c0398442d17d3c4af814e5a" [[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" @@ -1040,7 +1050,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", ] @@ -1069,7 +1079,7 @@ dependencies = [ "num-integer", "num-traits", "proc-macro2 1.0.66", - "quote 1.0.31", + "quote 1.0.32", "syn 1.0.109", ] @@ -1294,6 +1304,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" @@ -1337,26 +1353,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" @@ -1364,7 +1360,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", ] @@ -1397,9 +1393,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" @@ -1457,12 +1453,6 @@ version = "0.5.6" source = "registry+https://github.com/rust-lang/crates.io-index" 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" @@ -1500,10 +1490,11 @@ dependencies = [ "bincode", "blstrs", "cfg-if", - "clap 4.3.17", + "clap 4.3.19", "config", "criterion", "dashmap", + "env_logger 0.10.0", "ff", "generic-array 0.14.7", "getrandom", @@ -1545,6 +1536,7 @@ dependencies = [ "structopt", "tap", "tempfile", + "test-log", "thiserror", ] @@ -1558,7 +1550,7 @@ dependencies = [ "proc-macro2 1.0.66", "proptest", "proptest-derive", - "quote 1.0.31", + "quote 1.0.32", "serde", "syn 1.0.109", ] @@ -1740,9 +1732,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", @@ -1885,9 +1877,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" @@ -1903,9 +1895,9 @@ checksum = "9163e1259760e83d528d1b3171e5100c1767f10c52e1c4d6afad26e63d47d758" [[package]] name = "pest" -version = "2.7.0" +version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f73935e4d55e2abf7f130186537b19e7a4abc886a0252380b59248af473a3fc9" +checksum = "0d2d1d55045829d65aad9d389139882ad623b33b904e7c9f1b10c5b8927298e5" dependencies = [ "thiserror", "ucd-trie", @@ -1913,9 +1905,9 @@ dependencies = [ [[package]] name = "pest_derive" -version = "2.7.0" +version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aef623c9bbfa0eedf5a0efba11a5ee83209c326653ca31ff019bec3a95bfff2b" +checksum = "5f94bca7e7a599d89dea5dfa309e217e7906c3c007fb9c3299c40b10d6a315d3" dependencies = [ "pest", "pest_generator", @@ -1923,22 +1915,22 @@ dependencies = [ [[package]] name = "pest_generator" -version = "2.7.0" +version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b3e8cba4ec22bada7fc55ffe51e2deb6a0e0db2d0b7ab0b103acc80d2510c190" +checksum = "99d490fe7e8556575ff6911e45567ab95e71617f43781e5c05490dc8d75c965c" dependencies = [ "pest", "pest_meta", "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.27", ] [[package]] name = "pest_meta" -version = "2.7.0" +version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a01f71cb40bd8bb94232df14b946909e14660e33fc05db3e50ae2a82d7ea0ca0" +checksum = "2674c66ebb4b4d9036012091b537aae5878970d6999f81a265034d85b136b341" dependencies = [ "once_cell", "pest", @@ -2049,7 +2041,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", ] @@ -2061,7 +2053,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", ] @@ -2073,7 +2065,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", ] @@ -2152,9 +2144,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", ] @@ -2330,7 +2322,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", ] @@ -2340,20 +2332,6 @@ version = "0.1.23" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76" -[[package]] -name = "rustix" -version = "0.37.23" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4d69718bf81c6127a49dc64e44a742e8bb9213c0ff8869a22c308f84c1d4ab06" -dependencies = [ - "bitflags 1.3.2", - "errno", - "io-lifetimes", - "libc", - "linux-raw-sys 0.3.8", - "windows-sys 0.48.0", -] - [[package]] name = "rustix" version = "0.38.4" @@ -2363,15 +2341,15 @@ 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" @@ -2414,15 +2392,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" @@ -2451,9 +2429,9 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.171" +version = "1.0.176" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "30e27d1e4fd7659406c492fd6cfaf2066ba8773de45ca75e855590f856dc34a9" +checksum = "76dc28c9523c5d70816e393136b86d48909cfb27cecaa902d338c19ed47164dc" dependencies = [ "serde_derive", ] @@ -2478,20 +2456,20 @@ dependencies = [ [[package]] name = "serde_derive" -version = "1.0.171" +version = "1.0.176" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "389894603bd18c46fa56231694f8d827779c0951a667087194cf9de94ed24682" +checksum = "a4e7b8c5dc823e3b90651ff1d3808419cd14e5ad76de04feaf37da114e7a306f" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.27", ] [[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", @@ -2500,13 +2478,13 @@ dependencies = [ [[package]] name = "serde_repr" -version = "0.1.14" +version = "0.1.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1d89a8107374290037607734c0b73a85db7ed80cae314b3c5791f192a496e731" +checksum = "e168eaaf71e8f9bd6037feb05190485708e019f4fd87d161b3c0a0d37daf85e5" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.27", ] [[package]] @@ -2619,7 +2597,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", ] @@ -2670,18 +2648,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.27" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "45c3457aacde3c65315de5031ec191ce46604304d2446e803d71ade03308d970" +checksum = "b60f673f44a8255b9c8c657daf66a596d435f2da81a555b06dc644d080ba45e0" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", + "quote 1.0.32", "unicode-ident", ] @@ -2702,15 +2680,14 @@ dependencies = [ [[package]] name = "tempfile" -version = "3.6.0" +version = "3.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "31c0432476357e58790aaa47a8efb0c5138f137343f3b5f23bd36a27e3b0a6d6" +checksum = "5486094ee78b2e5038a6382ed7645bc084dc2ec433426ca4c3cb61e2007b8998" dependencies = [ - "autocfg", "cfg-if", "fastrand", "redox_syscall", - "rustix 0.37.23", + "rustix", "windows-sys 0.48.0", ] @@ -2729,6 +2706,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 = "textwrap" version = "0.11.0" @@ -2746,22 +2734,22 @@ checksum = "222a222a5bfe1bba4a77b45ec488a741b3cb8872e5e499451fd7d0129c9c7c3d" [[package]] name = "thiserror" -version = "1.0.43" +version = "1.0.44" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a35fc5b8971143ca348fa6df4f024d4d55264f3468c71ad1c2f365b0a4d58c42" +checksum = "611040a08a0439f8248d1990b111c95baa9c704c805fa1f62104b39655fd7f90" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.43" +version = "1.0.44" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "463fe12d7993d3b327787537ce8dd4dfa058de32fc2b195ef3cde03dc4771e8f" +checksum = "090198534930841fab3a5d1bb637cde49e339654e606195f8d9c76eeb081dc96" dependencies = [ "proc-macro2 1.0.66", - "quote 1.0.31", - "syn 2.0.26", + "quote 1.0.32", + "syn 2.0.27", ] [[package]] @@ -2799,7 +2787,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", ] @@ -2853,9 +2841,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" @@ -2908,8 +2896,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.27", "wasm-bindgen-shared", ] @@ -2919,7 +2907,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", ] @@ -2930,8 +2918,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.27", "wasm-bindgen-backend", "wasm-bindgen-shared", ] @@ -3170,6 +3158,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.27", ] diff --git a/Cargo.toml b/Cargo.toml index e8896da295..aafe60de21 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -79,12 +79,14 @@ flamegraph = ["pprof/flamegraph", "pprof/criterion"] assert_cmd = "2.0.12" cfg-if = "1.0.0" criterion = "0.4" +env_logger = "*" hex = "0.4.3" pprof = { version = "0.11" } sha2 = { version = "0.10.7" } structopt = { version = "0.3", default-features = false } tap = "1.0.1" tempfile = "3.6.0" +test-log = "0.2.12" [workspace] resolver = "2" diff --git a/src/foil/circuit.rs b/src/foil/circuit.rs new file mode 100644 index 0000000000..7890842136 --- /dev/null +++ b/src/foil/circuit.rs @@ -0,0 +1,81 @@ +//! This module provides a general mechanism for converting a minimized Foil instance. + +use bellperson::{gadgets::num::AllocatedNum, Circuit, ConstraintSystem, SynthesisError}; + +use crate::field::LurkField; +use crate::foil::{Foil, Id, MetaData}; + +// 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 Circuit for Foil { + fn synthesize>(self, cs: &mut CS) -> Result<(), SynthesisError> { + assert!( + self.is_minimized(), + "only minimized Foils can be synthesized" + ); + + let partition = self.graph.partition(); + let _classes = partition.classes().clone(); + + let allocated = self + .graph + .vertices() + .iter() + .enumerate() + .map(|(i, vertex)| { + Ok(AllocatedNum::alloc( + &mut cs.namespace(|| format!("allocated-{}", i)), + || todo!("get from witness or calculate..."), + )?) + }) + .collect::, SynthesisError>>()?; + + // Allocate all the constructors and their projections, and constrain them. + for constructor in self.schema.constructors().iter() { + let _ids = self.fun_map.get(constructor.name()); + } + for (i, (representative_id, _member_ids)) in partition.classes.iter().enumerate() { + let vertex = self.graph.vertex(*representative_id); + let allocated_head = allocated[i].clone(); + let allocated_successors = vertex + .successors() + .borrow() + .iter() + .map(|successor_id| allocated[*successor_id].clone()) + .collect::>(); + let relation: Rel = { + let arity = allocated_successors.len(); + let label = vertex.label(); + let metadata = vertex.metadata(); + + todo!( + "recover source intent from the above -- possibly enhancing Foil to simplify" + ); + }; + + relation.synthesize( + &mut cs.namespace(|| format!("relation-{}", i)), + allocated_head, + allocated_successors, + )?; + } + + Ok(()) + } +} + +trait Relation { + fn synthesize, F: LurkField>( + &self, + cs: &mut CS, + allocated_head: AllocatedNum, + successors: Vec>, + ) -> Result<(), SynthesisError> { + unimplemented!() + } +} + +enum Rel {} + +impl Relation for Rel {} diff --git a/src/foil/congruence.rs b/src/foil/congruence.rs new file mode 100644 index 0000000000..cc6fbcf1c7 --- /dev/null +++ b/src/foil/congruence.rs @@ -0,0 +1,493 @@ +//! 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 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(&self, g: &mut Graph, targets: Vec) { + 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: Vec) { + // 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 mut target_ids = Vec::with_capacity(targets.len()); + + for target_vert in targets.iter() { + // 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); + } + + // 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 + } +} + +#[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, +} + +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 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 { + let mut classes: HashMap> = Default::default(); + let mut index: HashMap = Default::default(); + let mut successors: HashMap> = Default::default(); + let mut labels: HashMap = Default::default(); + + for (id, _v) in g.vertices.iter().enumerate() { + let find_v = g.find(id); + let vertex = g.vertex(id); + let successor_ids = vertex + .successors() + .borrow() + .iter() + .map(|id| g.find(*id)) + .collect::>(); + + if !successor_ids.is_empty() { + 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()); + } + + 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); + } + Self { + classes, + index, + successors, + labels, + } + } +} + +#[cfg(test)] +pub(crate) mod test { + use super::*; + + 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, vec![v2, v4]); + v2.connect(g, vec![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/src/foil/constructors.rs b/src/foil/constructors.rs new file mode 100644 index 0000000000..326daa292d --- /dev/null +++ b/src/foil/constructors.rs @@ -0,0 +1,526 @@ +//! 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::foil::{Func, Label, 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()]), + 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::foil::congruence::{test::assert_expected_classes, Graph}; + use crate::foil::{Foil, 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, vec![a]); + cdr.connect(g, vec![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, vec![x, car]); + bind_y.connect(g, vec![y, cdr]); + + plus.connect(g, vec![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, vec![b, c]); + + car1.connect(g, vec![cons]); + cdr1.connect(g, vec![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()); + + 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, vec![a]); + f.connect(&cdr, vec![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, vec![x, car]); + f.connect(&bind_y, vec![y, cdr]); + + f.connect(&plus, vec![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): 9", + "Var(Car): 12", + "Car: 14", + "Car: 16", + ], + Some(vec![0]), + ), + ( + 2, + // {E, CDR(1), CDR(2), C, Y} + vec![ + "Var(y): 2", + "Cdr: 4", + "Var(Cdr): 10", + "Var(Cdr): 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()); + + 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, vec![a, cons1]); + f.connect(&cons1, vec![b, c]); + + f.connect(&bind_d, vec![d, car]); + f.connect(&car, vec![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): 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): 10", "Cdr: 12", "Cdr: 14"], + Some(vec![0]), + ), + ]; + + assert_expected_classes(expected_classes, actual_classes); + + let minimized = f.minimize(); + assert!(minimize.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, 4])), + (1, vec!["Car: 1"], Some(vec![0])), + (2, vec!["Binding: 2"], Some(vec![0, 0])), + (3, vec!["Binding: 3"], Some(vec![1, 1])), + (4, vec!["Cdr: 4"], 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()); + + 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, vec![b, c]); + let bind_a = f.alloc(Fun::Binding); + f.connect(&bind_a, vec![a, cons1]); + + let car = f.alloc(Fun::Car); + f.connect(&car, vec![a]); + let d = f.alloc(Var::new("d")); + let bind_d = f.alloc(Fun::Binding); + f.connect(&bind_d, vec![d, car]); + + let cdr = f.alloc(Fun::Cdr); + f.connect(&cdr, vec![a]); + let e = f.alloc(Var::new("e")); + let bind_e = f.alloc(Fun::Binding); + f.connect(&bind_e, vec![e, cdr]); + + let cons2 = f.alloc(Fun::Cons); + f.connect(&cons2, vec![d, e]); + let bind_ff = f.alloc(Fun::Binding); + let ff = f.alloc(Var::new("ff")); + f.connect(&bind_ff, vec![ff, cons2]); + + let plus = f.alloc(Fun::Add); + f.connect(&plus, vec![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): 16", + "Var(Car): 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): 17", + "Var(Cdr): 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.minimized); + let minimized_classes = dbg!(minimized.graph.class_info(None)); + + let expected_minimized = &[ + (0, vec!["Car: 0"], Some(vec![5])), + (1, vec!["Binding: 1"], Some(vec![0, 0])), + (2, vec!["Cdr: 2"], Some(vec![5])), + (3, vec!["Binding: 3"], Some(vec![2, 2])), + (4, vec!["Binding: 4"], Some(vec![5, 5])), + (5, vec!["Cons: 5"], Some(vec![0, 2])), + (6, vec!["Add: 6"], Some(vec![5, 5])), + ]; + + assert_expected_classes(expected_minimized, minimized_classes); + } +} diff --git a/src/foil/mod.rs b/src/foil/mod.rs new file mode 100644 index 0000000000..c5623e6330 --- /dev/null +++ b/src/foil/mod.rs @@ -0,0 +1,564 @@ +//! FOIL +//! Flat Optimization Intermediate Language +use log::{info, warn}; +use std::collections::{HashMap, VecDeque}; +use std::fmt::{Debug, Display, Formatter}; +use std::hash::Hash; + +use anyhow::{bail, Error}; +use indexmap::IndexSet; + +pub mod circuit; +pub mod congruence; +pub mod constructors; + +pub use congruence::{Graph, Id, LabelTrait, MetaData, Vert}; + +#[derive(Debug, Clone, Hash, PartialEq, Eq)] +pub struct Func { + name: &'static str, + projectors: Option>, +} + +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 { + fn equivalences(&self) -> Vec { + self.equivalences.clone() + } + fn constructors(&self) -> Vec { + self.constructors.clone() + } + fn add_constructor(&mut self, constructor: Func) { + self.constructors.push(constructor) + } +} + +impl Func { + fn new(name: &'static str) -> Self { + Self { + name, + projectors: None, + } + } + fn constructor(name: &'static str, projectors: Vec) -> Self { + Self { + name, + projectors: Some(projectors), + } + } + fn name(&self) -> &'static str { + self.name + } + fn projectors(&self) -> Option<&[Self]> { + if let Some(p) = &self.projectors { + Some(p) + } else { + None + } + } +} + +#[derive(Debug, Clone)] +pub struct Foil { + graph: G, + merge_queue: VecDeque<(Id, Id)>, + fun_map: HashMap<&'static str, IndexSet>, + var_map: HashMap<(&'static str, Option), IndexSet>, + var_counter: usize, + vars: HashMap, + constants: HashMap, + schema: Schema, + finalized: bool, + minimized: bool, +} + +#[derive(Debug, Default, Eq, Clone, Copy, Hash, PartialEq)] +pub struct Var(pub &'static str, pub Option); + +impl Var { + pub fn new(name: &'static str) -> Self { + Self(name, 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, Copy, Hash, PartialEq)] +pub enum Label { + F(&'static str), + V(&'static str, Option), +} + +impl Eq for Label {} + +impl Label { + pub fn var(name: &'static str) -> Self { + Var(name, 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, v.1) + } +} + +impl From