diff --git a/Cargo.lock b/Cargo.lock index 300d924e..fd78818a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,6 +2,17 @@ # It is not intended for manual editing. version = 4 +[[package]] +name = "aes" +version = "0.9.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "35f0f96ce78e38c3dc6d8948aa8163d06385be74000f3c7a95bf1eef35d3ea32" +dependencies = [ + "cipher", + "cpubits", + "cpufeatures 0.3.1", +] + [[package]] name = "ahash" version = "0.8.12" @@ -29,12 +40,30 @@ version = "0.2.21" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "683d7910e743518b0e34f1186f92494becacb047c7b6bf616c96772180fef923" +[[package]] +name = "atomic-waker" +version = "1.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1505bd5d3d116872e7271a6d4e16d81d0c8570876c8de68093a09ac269d8aac0" + [[package]] name = "autocfg" version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8" +[[package]] +name = "base64" +version = "0.22.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b3254f16251a8381aa12e40e3c4d2f0199f8c6508fbecb9d91f575e0fbb8c6" + +[[package]] +name = "base64" +version = "0.23.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac07cdecf99051d9a5238b80f35af32cdeba5b336e55d957b318b50137e18da5" + [[package]] name = "bench" version = "0.1.0" @@ -44,9 +73,9 @@ dependencies = [ "regex", "serde", "serde_json", - "sha2", - "syn", - "windows-sys", + "sha2 0.10.9", + "syn 2.0.117", + "windows-sys 0.61.2", ] [[package]] @@ -83,24 +112,112 @@ dependencies = [ "generic-array", ] +[[package]] +name = "block-buffer" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d2f6c7dbe95a6ed67ad9f18e57daf93a2f034c524b99fd2b76d18fdfeb6660aa" +dependencies = [ + "hybrid-array", + "zeroize", +] + [[package]] name = "bumpalo" version = "3.20.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5d20789868f4b01b2f2caec9f5c4e0213b41e3e5702a50157d699ae31ced2fcb" +[[package]] +name = "bytes" +version = "1.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fc652a48c352aef3ea3aed32080501cf3ef6ed5da78602a020c991775b0aff04" + +[[package]] +name = "bzip2" +version = "0.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f3a53fac24f34a81bc9954b5d6cfce0c21e18ec6959f44f56e8e90e4bb7c346c" +dependencies = [ + "libbz2-rs-sys", +] + +[[package]] +name = "cc" +version = "1.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "877bf67ac8e52449eb2f9e98a344ea163beb70dd1f9eebe3cc5357dcfeaee4df" +dependencies = [ + "find-msvc-tools", + "jobserver", + "libc", + "shlex", +] + [[package]] name = "cfg-if" version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" +[[package]] +name = "cfg_aliases" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f079e83a288787bcd14a6aea84cee5c87a67c5a3e660c30f557a3d24761b3527" + +[[package]] +name = "chacha20" +version = "0.10.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "65c35e4b699c7e15ccbe7ee35c005e4fc0a278d22238a2857e6ce2dadeda1b06" +dependencies = [ + "cfg-if", + "cpufeatures 0.3.1", + "rand_core 0.10.1", +] + +[[package]] +name = "cipher" +version = "0.5.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e8cf2a2c93cd704877c0858356ed03480ff301ee950b43f1cbe4573b088bfa6c" +dependencies = [ + "crypto-common 0.2.2", + "inout", +] + +[[package]] +name = "cmov" +version = "0.5.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0c9ea0ac24bc397ab3c98583a3c9ba74fa56b09a4449bbe172b9b1ddb016027a" + +[[package]] +name = "const-oid" +version = "0.10.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a6ef517f0926dd24a1582492c791b6a4818a4d94e789a334894aa15b0d12f55c" + +[[package]] +name = "constant_time_eq" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3d52eff69cd5e647efe296129160853a42795992097e8af39800e1060caeea9b" + [[package]] name = "convert_case" version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6245d59a3e82a7fc217c5828a6692dbc6dfb63a0c8c90495621f7b9d79704a0e" +[[package]] +name = "cpubits" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "15b85f9c39137c3a891689859392b1bd49812121d0d61c9caf00d46ed5ce06ae" + [[package]] name = "cpufeatures" version = "0.2.17" @@ -110,6 +227,24 @@ dependencies = [ "libc", ] +[[package]] +name = "cpufeatures" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5ca28b0ae3115b884660db4118d803791fd6756b6e88f39c0f3f7859060d7566" +dependencies = [ + "libc", +] + +[[package]] +name = "crc32fast" +version = "1.5.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "01a7799fd6b852db0e61728dde9a204c423b44d689dbd432522543614b490e78" +dependencies = [ + "cfg-if", +] + [[package]] name = "crossbeam-utils" version = "0.8.21" @@ -126,6 +261,36 @@ dependencies = [ "typenum", ] +[[package]] +name = "crypto-common" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ce6e4c961d6cd6c9a86db418387425e8bdeaf05b3c8bc1411e6dca4c252f1453" +dependencies = [ + "hybrid-array", +] + +[[package]] +name = "ctutils" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "03bb0e1cc970d482d121d9a1744999169b69a07470b3d644a7894e53fcaf4574" +dependencies = [ + "cmov", +] + +[[package]] +name = "deflate64" +version = "0.1.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac6b926516df9c60bfa16e107b21086399f8285a44ca9711344b9e553c5146e2" + +[[package]] +name = "deranged" +version = "0.5.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9e9de72ce2ad1f90dc62fa25f0f430ef85eb4b0d8fa0be4f30373bc40a21d28e" + [[package]] name = "derive-where" version = "1.6.1" @@ -134,7 +299,7 @@ checksum = "d08b3a0bcc0d079199cd476b2cae8435016ec11d1c0986c6901c5ac223041534" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 2.0.117", ] [[package]] @@ -147,7 +312,7 @@ dependencies = [ "proc-macro2", "quote", "rustc_version", - "syn", + "syn 2.0.117", ] [[package]] @@ -156,8 +321,32 @@ version = "0.10.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9ed9a281f7bc9b7576e61468ba615a66a5c8cfdff42420a70aa82701a3b1e292" dependencies = [ - "block-buffer", - "crypto-common", + "block-buffer 0.10.4", + "crypto-common 0.1.7", +] + +[[package]] +name = "digest" +version = "0.11.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f1dd6dbb5841937940781866fa1281a1ff7bd3bf827091440879f9994983d5c2" +dependencies = [ + "block-buffer 0.12.1", + "const-oid", + "crypto-common 0.2.2", + "ctutils", + "zeroize", +] + +[[package]] +name = "displaydoc" +version = "0.2.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c6232dd377dcc64799954cbd3a9bb882e9cdc1308ccd87b1c098f1fb2eaf82a8" +dependencies = [ + "proc-macro2", + "quote", + "syn 3.0.9", ] [[package]] @@ -175,7 +364,7 @@ dependencies = [ "smallvec", "symbol_table", "symbolic_expressions", - "thiserror", + "thiserror 1.0.69", ] [[package]] @@ -199,18 +388,91 @@ version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f" +[[package]] +name = "find-msvc-tools" +version = "0.1.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1c66915cc5391097de7a2b0b972e8505aa33c0df401fd3a6811dbdb32881ba48" + [[package]] name = "fixedbitset" version = "0.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0ce7134b9999ecaf8bcd65542e436736ef32ddca1b3e06094cb6ec5755203b80" +[[package]] +name = "flate2" +version = "1.1.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6e634e2e0ebac1ee034020da1ca582e17ffe4e0f5e985823721e168928136dcb" +dependencies = [ + "zlib-rs", +] + [[package]] name = "foldhash" version = "0.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2" +[[package]] +name = "form_urlencoded" +version = "1.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cb4cb245038516f5f85277875cdaa4f7d2c9a0fa0468de06ed190163b1581fcf" +dependencies = [ + "percent-encoding", +] + +[[package]] +name = "futures-channel" +version = "0.3.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b1f9e3d69d39e4862ffed03ed071a76f9a13ba1d9109d355b0f0aa6b15e393c4" +dependencies = [ + "futures-core", + "futures-sink", +] + +[[package]] +name = "futures-core" +version = "0.3.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "92d699e522242e69e3003b94ecc1f960f3a5e015aa7c5d7486e65ad01dd94f5e" + +[[package]] +name = "futures-io" +version = "0.3.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "53c0fa8157de1303bfffdaa1cc2a673bfffb60102f76b0ef4441659124373fed" + +[[package]] +name = "futures-sink" +version = "0.3.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1944426bf7d03f1d14f708785e4b33efd750b36d48a157b836b3efc15ede8e1d" + +[[package]] +name = "futures-task" +version = "0.3.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cd417de3d1d015fc3bfd2b1ea46dfc7bab72ef86f1cc7cc9c78e728b34a6d1fd" + +[[package]] +name = "futures-util" +version = "0.3.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0d50a92467f8ba5dd6e3ee5d4bd04d73ab2e4e1c44474a0674821dfce14b79bc" +dependencies = [ + "futures-core", + "futures-io", + "futures-sink", + "futures-task", + "memchr", + "pin-project-lite", + "slab", +] + [[package]] name = "generic-array" version = "0.14.7" @@ -221,6 +483,33 @@ dependencies = [ "version_check", ] +[[package]] +name = "getrandom" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ff2abc00be7fca6ebc474524697ae276ad847ad0a6b3faa4bcb027e9a4614ad0" +dependencies = [ + "cfg-if", + "js-sys", + "libc", + "wasi", + "wasm-bindgen", +] + +[[package]] +name = "getrandom" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "300e883d756b2e4ec94e02791f39b04b522276138852cfc41d9fb7e904106099" +dependencies = [ + "cfg-if", + "js-sys", + "libc", + "r-efi", + "rand_core 0.10.1", + "wasm-bindgen", +] + [[package]] name = "hashbrown" version = "0.14.5" @@ -249,134 +538,423 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "841d1cc9bed7f9236f321df977030373f4a4163ae1a7dbfe1a51a2c1a51d9100" [[package]] -name = "im" -version = "15.1.0" +name = "hmac" +version = "0.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d0acd33ff0285af998aaf9b57342af478078f53492322fafc47450e09397e0e9" +checksum = "6303bc9732ae41b04cb554b844a762b4115a61bfaa81e3e83050991eeb56863f" dependencies = [ - "bitmaps", - "rand_core", - "rand_xoshiro", - "sized-chunks", - "typenum", - "version_check", + "digest 0.11.3", ] [[package]] -name = "indexmap" -version = "2.13.0" +name = "http" +version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7714e70437a7dc3ac8eb7e6f8df75fd8eb422675fc7678aff7364301092b1017" +checksum = "918d3568bebf352712bc2ef3d46a8bcf1a75b373be6539de198e9105cbbf9ce0" dependencies = [ - "equivalent", - "hashbrown 0.16.1", + "bytes", + "itoa", ] [[package]] -name = "itertools" -version = "0.13.0" +name = "http-body" +version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186" +checksum = "ca2a8f2913ee65f60facd6a5905613afaa448497a0230cc41ce022d93290bc2c" dependencies = [ - "either", + "bytes", + "http", ] [[package]] -name = "itoa" -version = "1.0.18" +name = "http-body-util" +version = "0.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" +checksum = "23169fe34a5fbcdd3f3862e78fb9b6fccd5f02a6dc6f732547005d45631ce71c" +dependencies = [ + "bytes", + "futures-core", + "http", + "http-body", + "pin-project-lite", +] [[package]] -name = "js-sys" -version = "0.3.91" +name = "httparse" +version = "1.10.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b49715b7073f385ba4bc528e5747d02e66cb39c6146efb66b781f131f0fb399c" -dependencies = [ - "once_cell", - "wasm-bindgen", -] +checksum = "6dbf3de79e51f3d586ab4cb9d5c3e2c14aa28ed23d180cf89b4df0454a69cc87" [[package]] -name = "lasso" -version = "0.7.3" +name = "hybrid-array" +version = "0.4.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6e14eda50a3494b3bf7b9ce51c52434a761e383d7238ce1dd5dcec2fbc13e9fb" +checksum = "3944cf8cf766b40e2a1a333ee5e9b563f854d5fa49d6a8ca2764e97c6eddb214" dependencies = [ - "hashbrown 0.14.5", + "typenum", ] [[package]] -name = "libc" -version = "0.2.183" +name = "hyper" +version = "1.12.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5b646652bf6661599e1da8901b3b9522896f01e736bad5f723fe7a3a27f899d" +checksum = "2c3e324da4c95177d6291d4c8730197c0d1822f8a9766814a4a44fa5ab797c9c" +dependencies = [ + "atomic-waker", + "bytes", + "futures-core", + "http", + "http-body", + "httparse", + "itoa", + "pin-project-lite", + "smallvec", + "tokio", + "want", +] [[package]] -name = "log" -version = "0.4.29" +name = "hyper-rustls" +version = "0.27.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897" +checksum = "dfa8e654703247911e29c23fbeaa261834bd9bb74efba2f9acddc37bfb127f53" +dependencies = [ + "http", + "hyper", + "hyper-util", + "rustls", + "tokio", + "tokio-rustls", + "tower-service", + "webpki-roots", +] [[package]] -name = "memchr" -version = "2.8.3" +name = "hyper-util" +version = "0.1.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cf8baf1c55e62ffcace7a9f06f4bd9cd3f0c4beb022d3b367256b91b87513d98" +checksum = "ddc03d96684f9226b8a787cdb71488417b53ab5ea8fdb1dac946cb9431cc8bff" +dependencies = [ + "base64 0.23.1", + "bytes", + "futures-channel", + "futures-util", + "http", + "http-body", + "httparse", + "hyper", + "ipnet", + "libc", + "percent-encoding", + "pin-project-lite", + "socket2", + "tokio", + "tower-service", + "tracing", +] [[package]] -name = "nonmax" -version = "0.5.5" +name = "icu_collections" +version = "2.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "610a5acd306ec67f907abe5567859a3c693fb9886eb1f012ab8f2a47bef3db51" +checksum = "fa68d21081c4a05d5a901a1c62add574c77048b6a1c67be3b50ce0b60d4ca513" +dependencies = [ + "displaydoc", + "potential_utf", + "utf8_iter", + "yoke", + "zerofrom", + "zerovec", +] [[package]] -name = "num" -version = "0.4.3" +name = "icu_locale_core" +version = "2.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "35bd024e8b2ff75562e5f34e7f4905839deb4b22955ef5e73d2fea1b9813cb23" +checksum = "d56e28588da92eee5c3201a6eff33fabdd49b62269c8938d4ff050ce4d900deb" dependencies = [ - "num-bigint", - "num-complex", - "num-integer", - "num-iter", - "num-rational", - "num-traits", + "displaydoc", + "litemap", + "tinystr", + "writeable", + "zerovec", ] [[package]] -name = "num-bigint" -version = "0.4.6" +name = "icu_normalizer" +version = "2.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9" +checksum = "12f9cf5f235641ed274641dd81c3f28d870e276763d0797aeeab72317b1c646f" dependencies = [ - "num-integer", - "num-traits", + "icu_collections", + "icu_normalizer_data", + "icu_properties", + "icu_provider", + "smallvec", + "zerovec", ] [[package]] -name = "num-complex" -version = "0.4.6" +name = "icu_normalizer_data" +version = "2.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "73f88a1307638156682bada9d7604135552957b7818057dcef22705b4d509495" +checksum = "1563da1ed3e0b3bf3d74c9b85917ac9c56464d2f57242270c09c9e752f8021a0" + +[[package]] +name = "icu_properties" +version = "2.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7e7ca276ad3145661a65914e6daf131ca5120cd3dcee8f8f3214b8875184a148" dependencies = [ - "num-traits", + "displaydoc", + "icu_collections", + "icu_locale_core", + "icu_properties_data", + "icu_provider", + "zerotrie", + "zerovec", ] [[package]] -name = "num-integer" -version = "0.1.46" +name = "icu_properties_data" +version = "2.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f" +checksum = "e590f038c1464a96894fd6d10127e90a8be4509f56ff7ecef851b15cee0b7caa" + +[[package]] +name = "icu_provider" +version = "2.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d27bbb9d3abbefac45d55f647c9de1d44aafcd1186eb91879afef17c396c3e73" dependencies = [ - "num-traits", + "displaydoc", + "icu_locale_core", + "writeable", + "yoke", + "zerofrom", + "zerotrie", + "zerovec", ] [[package]] -name = "num-iter" -version = "0.1.45" +name = "idna" +version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1429034a0490724d0075ebb2bc9e875d6503c3cf69e235a8941aa757d83ef5bf" +checksum = "3b0875f23caa03898994f6ddc501886a45c7d3d62d04d2d90788d47be1b1e4de" +dependencies = [ + "idna_adapter", + "smallvec", + "utf8_iter", +] + +[[package]] +name = "idna_adapter" +version = "1.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cb68373c0d6620ef8105e855e7745e18b0d00d3bdb07fb532e434244cdb9a714" +dependencies = [ + "icu_normalizer", + "icu_properties", +] + +[[package]] +name = "im" +version = "15.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d0acd33ff0285af998aaf9b57342af478078f53492322fafc47450e09397e0e9" +dependencies = [ + "bitmaps", + "rand_core 0.6.4", + "rand_xoshiro", + "sized-chunks", + "typenum", + "version_check", +] + +[[package]] +name = "indexmap" +version = "2.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7714e70437a7dc3ac8eb7e6f8df75fd8eb422675fc7678aff7364301092b1017" +dependencies = [ + "equivalent", + "hashbrown 0.16.1", +] + +[[package]] +name = "inout" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4250ce6452e92010fdf7268ccc5d14faa80bb12fc741938534c58f16804e03c7" +dependencies = [ + "hybrid-array", +] + +[[package]] +name = "ipnet" +version = "2.12.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "791930b43c0d5973160d90a8f3894509f2b273430f5c5c73b668636d0287c5c0" + +[[package]] +name = "itertools" +version = "0.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186" +dependencies = [ + "either", +] + +[[package]] +name = "itoa" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" + +[[package]] +name = "jobserver" +version = "0.1.35" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1c00acbd29eabad4a2392fa0e921c874934dbbf4194312ad20f04a0ed67a3cb3" +dependencies = [ + "getrandom 0.4.3", + "libc", +] + +[[package]] +name = "js-sys" +version = "0.3.91" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b49715b7073f385ba4bc528e5747d02e66cb39c6146efb66b781f131f0fb399c" +dependencies = [ + "once_cell", + "wasm-bindgen", +] + +[[package]] +name = "lasso" +version = "0.7.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6e14eda50a3494b3bf7b9ce51c52434a761e383d7238ce1dd5dcec2fbc13e9fb" +dependencies = [ + "hashbrown 0.14.5", +] + +[[package]] +name = "libbz2-rs-sys" +version = "0.2.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "34b357333733e8260735ba5894eb928c02ecc69c78715f01a8019e7fa7f2db4c" + +[[package]] +name = "libc" +version = "0.2.183" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b5b646652bf6661599e1da8901b3b9522896f01e736bad5f723fe7a3a27f899d" + +[[package]] +name = "litemap" +version = "0.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "47d9d19d1d6efa0109d2f65ff4c85cddd50bd572e5a00127ab10987290bcefae" + +[[package]] +name = "log" +version = "0.4.29" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897" + +[[package]] +name = "lru-slab" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4050469837a6ff301cd14c1f8f24f88549e6d548f24f64e2148eb0f72cebc51f" + +[[package]] +name = "lzma-rust2" +version = "0.16.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ca93e534d1142d1d0dcca6d25fe302508a5dfb40b302802904577725ea0b695b" +dependencies = [ + "sha2 0.11.1", +] + +[[package]] +name = "memchr" +version = "2.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf8baf1c55e62ffcace7a9f06f4bd9cd3f0c4beb022d3b367256b91b87513d98" + +[[package]] +name = "mio" +version = "1.2.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1788edb87fdc09c7e26304471e2f5be8cdefb1b6930d6e3985fc02ff53bf86ee" +dependencies = [ + "libc", + "wasi", + "windows-sys 0.61.2", +] + +[[package]] +name = "nonmax" +version = "0.5.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "610a5acd306ec67f907abe5567859a3c693fb9886eb1f012ab8f2a47bef3db51" + +[[package]] +name = "num" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "35bd024e8b2ff75562e5f34e7f4905839deb4b22955ef5e73d2fea1b9813cb23" +dependencies = [ + "num-bigint", + "num-complex", + "num-integer", + "num-iter", + "num-rational", + "num-traits", +] + +[[package]] +name = "num-bigint" +version = "0.4.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9" +dependencies = [ + "num-integer", + "num-traits", +] + +[[package]] +name = "num-complex" +version = "0.4.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "73f88a1307638156682bada9d7604135552957b7818057dcef22705b4d509495" +dependencies = [ + "num-traits", +] + +[[package]] +name = "num-conv" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "521739c6d2bac4aa25192232afe6841231376b2b26d4d9fae5ecf8ca5772e441" + +[[package]] +name = "num-integer" +version = "0.1.46" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f" +dependencies = [ + "num-traits", +] + +[[package]] +name = "num-iter" +version = "0.1.45" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1429034a0490724d0075ebb2bc9e875d6503c3cf69e235a8941aa757d83ef5bf" dependencies = [ "autocfg", "num-integer", @@ -409,6 +987,16 @@ version = "1.21.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9f7c3e4beb33f85d45ae3e3a1792185706c8e16d043238c593331cc7cd313b50" +[[package]] +name = "pbkdf2" +version = "0.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "112d82ceb8c5bf524d9af484d4e4970c9fd5a0cc15ba14ad93dccd28873b0629" +dependencies = [ + "digest 0.11.3", + "hmac", +] + [[package]] name = "peg" version = "0.8.5" @@ -436,6 +1024,12 @@ version = "0.8.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "132dca9b868d927b35b5dd728167b2dee150eb1ad686008fc71ccb298b776fca" +[[package]] +name = "percent-encoding" +version = "2.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9b4f627cb1b25917193a259e49bdad08f671f8d9708acfd5fe0a8c1455d87220" + [[package]] name = "petgraph" version = "0.6.5" @@ -446,6 +1040,39 @@ dependencies = [ "indexmap", ] +[[package]] +name = "pin-project-lite" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd" + +[[package]] +name = "pkg-config" +version = "0.3.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f6b464fbc74e149a392436b17d523f769e057cb6877f6a5c4618bc6f11800548" + +[[package]] +name = "potential_utf" +version = "0.1.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d83eb9bc6d8e5cf568e7a1101d60ee05e81ed50ea106026f3d18deeb046d7661" +dependencies = [ + "zerovec", +] + +[[package]] +name = "powerfmt" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4a6394b9e965e73d0a289ee54f589087e2c676aedf60885baf52c76b771e4958" + +[[package]] +name = "ppmd-rust" +version = "1.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "196a7c80b9a7652aba7cc070827516c2abe4ccdf53d128e1944003cf5726cff1" + [[package]] name = "proc-macro2" version = "1.0.106" @@ -470,6 +1097,62 @@ dependencies = [ "winapi", ] +[[package]] +name = "quinn" +version = "0.11.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4051e23e9185c255a7e33ef59cdbca87a22d359052eecd22fc6b901fb37d9d11" +dependencies = [ + "bytes", + "cfg_aliases", + "pin-project-lite", + "quinn-proto", + "quinn-udp", + "rustc-hash", + "rustls", + "socket2", + "thiserror 2.0.21", + "tokio", + "tracing", + "web-time", +] + +[[package]] +name = "quinn-proto" +version = "0.11.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0e750cca55fe4f0439a15d0bb529da9651e79993e8e72c61a899a36d462befbe" +dependencies = [ + "bytes", + "getrandom 0.4.3", + "lru-slab", + "rand", + "rand_pcg", + "ring", + "rustc-hash", + "rustls", + "rustls-pki-types", + "slab", + "thiserror 2.0.21", + "tinyvec", + "tracing", + "web-time", +] + +[[package]] +name = "quinn-udp" +version = "0.5.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "af66907df18639dcf4db56ca65490cabc4b27a97dbadd96f2926cca73298f016" +dependencies = [ + "cfg_aliases", + "libc", + "once_cell", + "socket2", + "tracing", + "windows-sys 0.61.2", +] + [[package]] name = "quote" version = "1.0.45" @@ -479,19 +1162,51 @@ dependencies = [ "proc-macro2", ] +[[package]] +name = "r-efi" +version = "6.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf" + +[[package]] +name = "rand" +version = "0.10.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "65c9fb96cbc91e3478eaae79a69fcd3f1ae4ad052e471fe6732fff548984b4af" +dependencies = [ + "chacha20", + "getrandom 0.4.3", + "rand_core 0.10.1", +] + [[package]] name = "rand_core" version = "0.6.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" +[[package]] +name = "rand_core" +version = "0.10.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "63b8176103e19a2643978565ca18b50549f6101881c443590420e4dc998a3c69" + +[[package]] +name = "rand_pcg" +version = "0.10.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "caa0f4137e1c0a72f4c651489402276c8e8e1cf081f3b0ba156d2cbeef09e86a" +dependencies = [ + "rand_core 0.10.1", +] + [[package]] name = "rand_xoshiro" version = "0.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6f97cdb2a36ed4183de61b2f824cc45c9f1037f28afe0a322e9fff4c108b5aaa" dependencies = [ - "rand_core", + "rand_core 0.6.4", ] [[package]] @@ -532,6 +1247,60 @@ version = "0.8.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d6f6ff9a378485b298a5286656da665ba74413d36db0979633275d2e708145d4" +[[package]] +name = "reqwest" +version = "0.12.28" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eddd3ca559203180a307f12d114c268abf583f59b03cb906fd0b3ff8646c1147" +dependencies = [ + "base64 0.22.1", + "bytes", + "futures-channel", + "futures-core", + "futures-util", + "http", + "http-body", + "http-body-util", + "hyper", + "hyper-rustls", + "hyper-util", + "js-sys", + "log", + "percent-encoding", + "pin-project-lite", + "quinn", + "rustls", + "rustls-pki-types", + "serde", + "serde_json", + "serde_urlencoded", + "sync_wrapper", + "tokio", + "tokio-rustls", + "tower", + "tower-http", + "tower-service", + "url", + "wasm-bindgen", + "wasm-bindgen-futures", + "web-sys", + "webpki-roots", +] + +[[package]] +name = "ring" +version = "0.17.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a4689e6c2294d81e88dc6261c768b63bc4fcdb852be6d1352498b114f61383b7" +dependencies = [ + "cc", + "cfg-if", + "getrandom 0.2.17", + "libc", + "untrusted", + "windows-sys 0.52.0", +] + [[package]] name = "rustc-hash" version = "2.1.1" @@ -547,6 +1316,41 @@ dependencies = [ "semver", ] +[[package]] +name = "rustls" +version = "0.23.46" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "48e13bd8c0e9365c43cfa5c9e8f9ad49d3c8444926c9aac819e0e4dc503c8fdf" +dependencies = [ + "once_cell", + "ring", + "rustls-pki-types", + "rustls-webpki", + "subtle", + "zeroize", +] + +[[package]] +name = "rustls-pki-types" +version = "1.15.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2f4925028c7eb5d1fcdaf196971378ed9d2c1c4efc7dc5d011256f76c99c0a96" +dependencies = [ + "web-time", + "zeroize", +] + +[[package]] +name = "rustls-webpki" +version = "0.103.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f3c3cf1d8b1e7d4927e2d154c3fcb02979afb9939629c62cd9048d4f07b60ac2" +dependencies = [ + "ring", + "rustls-pki-types", + "untrusted", +] + [[package]] name = "rusttyc" version = "0.5.0" @@ -559,6 +1363,12 @@ version = "1.0.22" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b39cdef0fa800fc44525c84ccb54a029961a8215f9619753635a9c0d2538d46d" +[[package]] +name = "ryu" +version = "1.0.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9774ba4a74de5f7b1c1451ed6cd5285a32eddb5cccb8cc655a4e50009e06477f" + [[package]] name = "semver" version = "1.0.27" @@ -581,129 +1391,385 @@ version = "1.0.228" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad" dependencies = [ - "serde_derive", + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.117", +] + +[[package]] +name = "serde_json" +version = "1.0.151" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c841b55ecdae098c80dcae9cf767f6f8a0c2cdb3416bbef72181df4d0fe73f14" +dependencies = [ + "indexmap", + "itoa", + "memchr", + "serde", + "serde_core", + "zmij", +] + +[[package]] +name = "serde_urlencoded" +version = "0.7.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d3491c14715ca2294c4d6a88f15e84739788c1d030eed8c110436aafdaa2f3fd" +dependencies = [ + "form_urlencoded", + "itoa", + "ryu", + "serde", +] + +[[package]] +name = "sha1" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "aacc4cc499359472b4abe1bf11d0b12e688af9a805fa5e3016f9a386dc2d0214" +dependencies = [ + "cfg-if", + "cpufeatures 0.3.1", + "digest 0.11.3", +] + +[[package]] +name = "sha2" +version = "0.10.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a7507d819769d01a365ab707794a4084392c824f54a7a6a7862f8c3d0892b283" +dependencies = [ + "cfg-if", + "cpufeatures 0.2.17", + "digest 0.10.7", +] + +[[package]] +name = "sha2" +version = "0.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "47d7069beb7d6ac7b9acd1039986e73443f24234f41074da099d6f994ac9ad19" +dependencies = [ + "cfg-if", + "cpufeatures 0.3.1", + "digest 0.11.3", +] + +[[package]] +name = "shlex" +version = "2.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8fadd59c855ef2080decdef8ff161eb6661b86933c9d82e5ba29dc602a55aba" + +[[package]] +name = "silver-oxide" +version = "0.1.0" +dependencies = [ + "derive-where", + "derive_more", + "egg", + "im", + "indexmap", + "itertools", + "lasso", + "nonmax", + "num", + "peg", + "petgraph", + "rustc-hash", + "rusttyc", + "typed-index-collections", + "z3", +] + +[[package]] +name = "simd-adler32" +version = "0.3.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3a219298ac11a56ea9a6d2120044824d6f01aeb034955e7af7bc16858527deea" + +[[package]] +name = "sized-chunks" +version = "0.6.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "16d69225bde7a69b235da73377861095455d298f2b970996eec25ddbb42b3d1e" +dependencies = [ + "bitmaps", + "typenum", +] + +[[package]] +name = "slab" +version = "0.4.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0c790de23124f9ab44544d7ac05d60440adc586479ce501c1d6d7da3cd8c9cf5" + +[[package]] +name = "smallvec" +version = "1.15.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03" + +[[package]] +name = "socket2" +version = "0.6.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c3d1e2c7f27f8d4cb10542a02c49005dbd6e93095799d6f3be745fae9f8fedd4" +dependencies = [ + "libc", + "windows-sys 0.61.2", +] + +[[package]] +name = "stable_deref_trait" +version = "1.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6ce2be8dc25455e1f91df71bfa12ad37d7af1092ae736f3a6cd0e37bc7810596" + +[[package]] +name = "subtle" +version = "2.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "13c2bddecc57b384dee18652358fb23172facb8a2c51ccc10d74c157bdea3292" + +[[package]] +name = "symbol_table" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f19bffd69fb182e684d14e3c71d04c0ef33d1641ac0b9e81c712c734e83703bc" +dependencies = [ + "crossbeam-utils", + "foldhash", + "hashbrown 0.15.5", +] + +[[package]] +name = "symbolic_expressions" +version = "5.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7c68d531d83ec6c531150584c42a4290911964d5f0d79132b193b67252a23b71" + +[[package]] +name = "syn" +version = "2.0.117" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "syn" +version = "3.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d78c8dee4c7bf0e14673097256fed6142ce9d3b85a408189d07482442145823b" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "sync_wrapper" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0bf256ce5efdfa370213c1dabab5935a12e49f2c58d15e9eac2870d3b4f27263" +dependencies = [ + "futures-core", +] + +[[package]] +name = "synstructure" +version = "0.14.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "901704edd0dfe137f1987838ee4f259e4e063c31371bdb423f7ae38ec6f77f02" +dependencies = [ + "proc-macro2", + "quote", + "syn 3.0.9", +] + +[[package]] +name = "thiserror" +version = "1.0.69" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52" +dependencies = [ + "thiserror-impl 1.0.69", +] + +[[package]] +name = "thiserror" +version = "2.0.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09e52cb86a36cede5cb101bf8908837b3e4c6e5e59fe7fd85c23fb56200d189e" +dependencies = [ + "thiserror-impl 2.0.21", +] + +[[package]] +name = "thiserror-impl" +version = "1.0.69" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.117", ] [[package]] -name = "serde_derive" -version = "1.0.228" +name = "thiserror-impl" +version = "2.0.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79" +checksum = "fe5197923287db20a58125f0bc85c062f7f2c892de97b18c356f9efb14b28524" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 3.0.9", ] [[package]] -name = "serde_json" -version = "1.0.151" +name = "time" +version = "0.3.55" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c841b55ecdae098c80dcae9cf767f6f8a0c2cdb3416bbef72181df4d0fe73f14" +checksum = "cdb87b95ec50ddfa440816d227a17b2ccbdda963a316a727fda0fc4334f7d134" dependencies = [ - "indexmap", - "itoa", - "memchr", - "serde", + "deranged", + "js-sys", + "num-conv", + "powerfmt", "serde_core", - "zmij", + "time-core", ] [[package]] -name = "sha2" -version = "0.10.9" +name = "time-core" +version = "0.1.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a7507d819769d01a365ab707794a4084392c824f54a7a6a7862f8c3d0892b283" +checksum = "9e1c906769ad99c88eaa54e728060edef082f8e358ff32030cb7c7d315e81109" + +[[package]] +name = "tinystr" +version = "0.8.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b1e27c91459209c2986af3dcf603a5a74a4368754ce37414f59acc971167f643" dependencies = [ - "cfg-if", - "cpufeatures", - "digest", + "displaydoc", + "zerovec", ] [[package]] -name = "silver-oxide" -version = "0.1.0" +name = "tinyvec" +version = "1.13.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fd3ca314f692efd6c868f8408f53fe444634a845f96c028b97d35f6a1f79f0ee" + +[[package]] +name = "tokio" +version = "1.53.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ce3335fa71841cda333a58d7615b03901380ecf09d59b3296d21f8bbac0dde4e" dependencies = [ - "derive-where", - "derive_more", - "egg", - "im", - "indexmap", - "itertools", - "lasso", - "nonmax", - "num", - "peg", - "petgraph", - "rustc-hash", - "rusttyc", - "typed-index-collections", + "bytes", + "libc", + "mio", + "pin-project-lite", + "socket2", + "windows-sys 0.61.2", ] [[package]] -name = "sized-chunks" -version = "0.6.5" +name = "tokio-rustls" +version = "0.26.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "16d69225bde7a69b235da73377861095455d298f2b970996eec25ddbb42b3d1e" +checksum = "c9cc2678c2cdd569ef8215e2afd7954ada2ae20b4fdd2c5fe6139a3b02d105db" dependencies = [ - "bitmaps", - "typenum", + "rustls", + "tokio", ] [[package]] -name = "smallvec" -version = "1.15.1" +name = "tower" +version = "0.5.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03" +checksum = "ebe5ef63511595f1344e2d5cfa636d973292adc0eec1f0ad45fae9f0851ab1d4" +dependencies = [ + "futures-core", + "futures-util", + "pin-project-lite", + "sync_wrapper", + "tokio", + "tower-layer", + "tower-service", +] [[package]] -name = "symbol_table" -version = "0.4.0" +name = "tower-http" +version = "0.6.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f19bffd69fb182e684d14e3c71d04c0ef33d1641ac0b9e81c712c734e83703bc" +checksum = "4cfcf7e2740e6fc6d4d688b4ef00650406bb94adf4731e43c096c3a19fe40840" dependencies = [ - "crossbeam-utils", - "foldhash", - "hashbrown 0.15.5", + "bitflags", + "bytes", + "futures-util", + "http", + "http-body", + "pin-project-lite", + "tower", + "tower-layer", + "tower-service", + "url", ] [[package]] -name = "symbolic_expressions" -version = "5.0.3" +name = "tower-layer" +version = "0.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7c68d531d83ec6c531150584c42a4290911964d5f0d79132b193b67252a23b71" +checksum = "121c2a6cda46980bb0fcd1647ffaf6cd3fc79a013de288782836f6df9c48780e" [[package]] -name = "syn" -version = "2.0.117" +name = "tower-service" +version = "0.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", -] +checksum = "8df9b6e13f2d32c91b9bd719c00d1958837bc7dec474d94952798cc8e69eeec3" [[package]] -name = "thiserror" -version = "1.0.69" +name = "tracing" +version = "0.1.44" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52" +checksum = "63e71662fa4b2a2c3a26f570f037eb95bb1f85397f3cd8076caed2f026a6d100" dependencies = [ - "thiserror-impl", + "pin-project-lite", + "tracing-core", ] [[package]] -name = "thiserror-impl" -version = "1.0.69" +name = "tracing-core" +version = "0.1.36" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" +checksum = "db97caf9d906fbde555dd62fa95ddba9eecfd14cb388e4f491a66d74cd5fb79a" dependencies = [ - "proc-macro2", - "quote", - "syn", + "once_cell", ] +[[package]] +name = "try-lock" +version = "0.2.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e421abadd41a4225275504ea4d6566923418b7f05506fbc9c0fe86ba7396114b" + [[package]] name = "typed-index-collections" version = "3.5.0" @@ -714,6 +1780,12 @@ dependencies = [ "serde", ] +[[package]] +name = "typed-path" +version = "0.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8e28f89b80c87b8fb0cf04ab448d5dd0dd0ade2f8891bae878de66a75a28600e" + [[package]] name = "typenum" version = "1.19.0" @@ -726,18 +1798,51 @@ version = "1.0.24" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" +[[package]] +name = "untrusted" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8ecb6da28b8a351d773b68d5825ac39017e680750f980f3a1a85cd8dd28a47c1" + [[package]] name = "unty" version = "0.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6d49784317cd0d1ee7ec5c716dd598ec5b4483ea832a2dced265471cc0f690ae" +[[package]] +name = "url" +version = "2.5.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ff67a8a4397373c3ef660812acab3268222035010ab8680ec4215f38ba3d0eed" +dependencies = [ + "form_urlencoded", + "idna", + "percent-encoding", + "serde", +] + +[[package]] +name = "utf8_iter" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b6c140620e7ffbb22c2dee59cafe6084a59b5ffc27a8859a5f0d494b5d52b6be" + [[package]] name = "version_check" version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" +[[package]] +name = "want" +version = "0.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ec4cdd0dd910afe868b7ef477227d8d538b46b3075031afee8a9f2acb0a2ed0b" +dependencies = [ + "try-lock", +] + [[package]] name = "wasi" version = "0.11.1+wasi-snapshot-preview1" @@ -757,6 +1862,20 @@ dependencies = [ "wasm-bindgen-shared", ] +[[package]] +name = "wasm-bindgen-futures" +version = "0.4.64" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e9c5522b3a28661442748e09d40924dfb9ca614b21c00d3fd135720e48b67db8" +dependencies = [ + "cfg-if", + "futures-util", + "js-sys", + "once_cell", + "wasm-bindgen", + "web-sys", +] + [[package]] name = "wasm-bindgen-macro" version = "0.2.114" @@ -776,7 +1895,7 @@ dependencies = [ "bumpalo", "proc-macro2", "quote", - "syn", + "syn 2.0.117", "wasm-bindgen-shared", ] @@ -799,6 +1918,25 @@ dependencies = [ "wasm-bindgen", ] +[[package]] +name = "web-time" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5a6580f308b1fad9207618087a65c04e7a10bc77e02c8e84e9b00dd4b12fa0bb" +dependencies = [ + "js-sys", + "wasm-bindgen", +] + +[[package]] +name = "webpki-roots" +version = "1.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7dcd9d09a39985f5344844e66b0c530a33843579125f23e21e9f0f220850f22a" +dependencies = [ + "rustls-pki-types", +] + [[package]] name = "winapi" version = "0.3.9" @@ -827,6 +1965,15 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" +[[package]] +name = "windows-sys" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" +dependencies = [ + "windows-targets", +] + [[package]] name = "windows-sys" version = "0.61.2" @@ -836,6 +1983,122 @@ dependencies = [ "windows-link", ] +[[package]] +name = "windows-targets" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" +dependencies = [ + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", + "windows_i686_gnullvm", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", +] + +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" + +[[package]] +name = "windows_aarch64_msvc" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" + +[[package]] +name = "windows_i686_gnu" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" + +[[package]] +name = "windows_i686_gnullvm" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" + +[[package]] +name = "windows_i686_msvc" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" + +[[package]] +name = "windows_x86_64_gnu" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" + +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" + +[[package]] +name = "windows_x86_64_msvc" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" + +[[package]] +name = "writeable" +version = "0.6.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3ad82d2a33cdc9674dc7465672f271e096168fcdbe0f799d9e6db8c5892679dc" + +[[package]] +name = "yoke" +version = "0.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "709fe23a0424b6a435d82152b1bd3fdfb0833487d5fa90d05d42762a9891fef5" +dependencies = [ + "stable_deref_trait", + "yoke-derive", + "zerofrom", +] + +[[package]] +name = "yoke-derive" +version = "0.8.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ec8ebde2db3681e8c9980cc27822030e68752690ddfa9473e739aeb4dbde6d71" +dependencies = [ + "proc-macro2", + "quote", + "syn 3.0.9", + "synstructure", +] + +[[package]] +name = "z3" +version = "0.21.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "83c8c28827f094697c982c88a730ef2511b5cb551f86f532a0bba2723178a37a" +dependencies = [ + "log", + "num", + "z3-sys", +] + +[[package]] +name = "z3-sys" +version = "0.13.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1343ed2cd33696498898195eb63613ef7891d9353bbc33ddc87d0292c6e3b1e6" +dependencies = [ + "pkg-config", + "reqwest", + "serde_json", + "zip", +] + [[package]] name = "zerocopy" version = "0.8.47" @@ -853,11 +2116,144 @@ checksum = "0e8bc7269b54418e7aeeef514aa68f8690b8c0489a06b0136e5f57c4c5ccab89" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 2.0.117", ] +[[package]] +name = "zerofrom" +version = "0.1.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0ec05a11813ea801ff6d75110ad09cd0824ddba17dfe17128ea0d5f68e6c5272" +dependencies = [ + "zerofrom-derive", +] + +[[package]] +name = "zerofrom-derive" +version = "0.1.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f75b4683f6c7f45248d4d64056a24298c6281e0993356d7d1b4a1a962ef10d4a" +dependencies = [ + "proc-macro2", + "quote", + "syn 3.0.9", + "synstructure", +] + +[[package]] +name = "zeroize" +version = "1.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e13084392c5e4bc371903e2935a5eaeed24905a7511356b883835e18a78f6879" + +[[package]] +name = "zerotrie" +version = "0.2.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4ea269c3bd32f0a32c321907a2ae912ba6f4649bb0fc764a15627e99a7095a3f" +dependencies = [ + "displaydoc", + "yoke", + "zerofrom", +] + +[[package]] +name = "zerovec" +version = "0.11.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bb0464e17806c1d976d5cba29399c7f08e516e279e2ba493f63123b5fca67dd8" +dependencies = [ + "yoke", + "zerofrom", + "zerovec-derive", +] + +[[package]] +name = "zerovec-derive" +version = "0.11.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "34df6fc39dbd26ddc9c10e6a2984476e13acce22e64e4487636ef494369225da" +dependencies = [ + "proc-macro2", + "quote", + "syn 3.0.9", +] + +[[package]] +name = "zip" +version = "8.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2d04a6b5381502aa6087c94c669499eb1602eb9c5e8198e534de571f7154809b" +dependencies = [ + "aes", + "bzip2", + "constant_time_eq", + "crc32fast", + "deflate64", + "flate2", + "getrandom 0.4.3", + "hmac", + "indexmap", + "lzma-rust2", + "memchr", + "pbkdf2", + "ppmd-rust", + "sha1", + "time", + "typed-path", + "zeroize", + "zopfli", + "zstd", +] + +[[package]] +name = "zlib-rs" +version = "0.6.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b268e58e7c693d7c271f93ffc4ba3b380412554231c85bf61ca7af91042a4112" + [[package]] name = "zmij" version = "1.0.23" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "29666d0abbfad1e3dc4dcf6144730dd3a3ab225bbbdac83319345b1b44ccfc1b" + +[[package]] +name = "zopfli" +version = "0.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f05cd8797d63865425ff89b5c4a48804f35ba0ce8d125800027ad6017d2b5249" +dependencies = [ + "bumpalo", + "crc32fast", + "log", + "simd-adler32", +] + +[[package]] +name = "zstd" +version = "0.13.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e91ee311a569c327171651566e07972200e76fcfe2242a4fa446149a3881c08a" +dependencies = [ + "zstd-safe", +] + +[[package]] +name = "zstd-safe" +version = "7.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "64d80649ab6db9d9f6f9c80a40becd948eda4714a0a5ac8c4d157a32231c7882" +dependencies = [ + "zstd-sys", +] + +[[package]] +name = "zstd-sys" +version = "2.1.0+zstd.1.5.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0ef0a8027ec3ee71300ab3bcbcd0393f434aa72b91ca6d635a39941deae8eea0" +dependencies = [ + "cc", + "pkg-config", +] diff --git a/Cargo.toml b/Cargo.toml index deb6ff62..eedb4a90 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -20,6 +20,7 @@ rusttyc = "0.5.0" im = "15.1.0" itertools = "0.13" rustc-hash = "2" +z3 = { version = "0.21.1", features = ["gh-release", "num"] } [lints.clippy] # Style lints the existing code trips; the CI clippy gate runs with `-D warnings`. diff --git a/README.md b/README.md index 01f8f7af..fe098c0c 100644 --- a/README.md +++ b/README.md @@ -88,7 +88,7 @@ Useful option: cargo run --bin verify -- --breakdown tests/cases/passing/field.vpr ``` -This prints the verification status of each member and, with `--breakdown`, the slowest verification steps and rule timings. +This prints the verification status of each member and, with `--breakdown`, the slowest verification steps, rule timings, and the time the Z3 rung spent building and solving its problems (`SILVER_OXIDE_Z3=1`). For tools, `--json` prints one JSON object instead (statuses, phase timings, per-member times, all verifier counters, peak memory, the build's git commit), and `--viper-metrics` prints shape metrics of the parsed program without verifying: diff --git a/src/bin/verify.rs b/src/bin/verify.rs index e2db49b2..4268c216 100644 --- a/src/bin/verify.rs +++ b/src/bin/verify.rs @@ -7,7 +7,8 @@ //! The same line is a plain string in the binary, so a binary that cannot be //! run can be checked with `strings verify | grep helium-build`. //! -//! `--breakdown` (`-b`) prints per-member verify times, slowest first. +//! `--breakdown` (`-b`) prints per-member verify times, slowest first, then +//! rule timings and the Z3 rung's build/solve time. //! //! `--json` prints one JSON object on stdout instead of the text rows: every //! member's status, the phase timings, per-member verify times, the full @@ -266,4 +267,10 @@ fn print_breakdown(member_times: &[(String, Duration)], stats: &VerifyStats) { t.apply * 1e3 ); } + let z3 = stats.z3_timing.0; + eprintln!( + "[Z3-TIMING] build {:>8.1}ms solve {:>8.1}ms", + z3.build * 1e3, + z3.solve * 1e3 + ); } diff --git a/src/verify/context/mod.rs b/src/verify/context/mod.rs index 9e4e8131..d500360b 100644 --- a/src/verify/context/mod.rs +++ b/src/verify/context/mod.rs @@ -4,6 +4,7 @@ use prove::BlockScratch; use crate::dhash::HashMap; +use crate::verify::z3::Z3Translation; use crate::{ verify::{ analysis::ConstFold, @@ -129,6 +130,9 @@ pub(crate) struct VerifyContext<'a> { /// Unlike [`Self::is_inconsistent`] this is a fact about the *scratch*, so it /// must never be consulted outside the block that established it. block_dead: bool, + + /// Sort and datatype caches of the Z3 translation (`verify::z3`). + pub(crate) z3translator: Z3Translation, } /// Whether any declaration uses a `wildcard` permission. Scanned once per unit at @@ -200,6 +204,7 @@ impl<'a> VerifyContext<'a> { in_block: false, scratch: None, block_dead: false, + z3translator: Z3Translation::default(), } } diff --git a/src/verify/context/prove.rs b/src/verify/context/prove.rs index e3990e14..a0b17c62 100644 --- a/src/verify/context/prove.rs +++ b/src/verify/context/prove.rs @@ -11,8 +11,6 @@ use crate::dhash::HashMap; -use egg::Language as _; - use crate::{ verify::{ analysis::ConstFold, @@ -23,6 +21,8 @@ use crate::{ }, vmir::{Literal, Polarity}, }; +use egg::Language as _; +use z3::SatResult; /// A parallel "scratch" e-graph for one method block: a clone of ground taken at /// build time with the block cube assumed, kept in sync with ground through the @@ -287,7 +287,9 @@ impl<'a> VerifyContext<'a> { // Functions/resources have no CFG — a whole-body scratch would just equal // ground — so they keep the per-obligation clone path below. if self.in_block { - let proven = self.prove_via_scratch(goal, pc_lits); + // Z3 is the last rung: it runs on ground plus the cube, never on the + // scratch (translation.typ, "Inputs"). + let proven = self.prove_via_scratch(goal, pc_lits) || self.prove_by_z3(goal, pc_lits); if proven { // Export under the **full** path condition. `pc_lits` is only the // instruction's delta; the block's cube is ambient — assumed by the @@ -322,7 +324,8 @@ impl<'a> VerifyContext<'a> { ) }) { let probe = self.egraph.clone(); - let proven = self.prove_by_ite_decomposition(&probe, goal, Rung::Saturated); + let proven = self.prove_by_ite_decomposition(&probe, goal, Rung::Saturated) + || self.prove_by_z3(goal, pc_lits); if proven { self.record_proven(imp, true_, pc_lits.is_empty()); } @@ -354,10 +357,11 @@ impl<'a> VerifyContext<'a> { true } else { let probe = self.run_probe_until(probe, goal); - // Last resort is the non-forking ite-goal decomposition; there is no - // case split beyond it. + // Then the non-forking ite-goal decomposition, and finally Z3, which + // adds arithmetic and real case splits. probe.find(goal) == probe.find(true_p) || self.prove_by_ite_decomposition(&probe, goal, Rung::Saturated) + || self.prove_by_z3(goal, pc_lits) }; // Persist the result so future identical obligations hit the `memo` tier. @@ -832,6 +836,49 @@ impl<'a> VerifyContext<'a> { } } + fn prove_by_z3(&mut self, goal: egg::Id, pc_lits: &[(egg::Id, Polarity)]) -> bool { + let t_build = std::time::Instant::now(); + + crate::verify::z3::sync_facts(self); + + let goal_z3 = crate::verify::z3::build_goal(self, goal); + + // The block's cube is ambient (assumed by the scratch, not in `pc_lits`), + // so it has to be added here for its guarded facts to apply. + let pc: Vec<_> = self.current_cube().iter().chain(pc_lits).copied().collect(); + let pc_cond = crate::verify::z3::build_pc(self, &pc); + + // Asserted in a scope rather than passed as assumptions; the `pop` + // drops them again before the next query. + let solver = &self.z3translator.solver; + solver.push(); + pc_cond + .iter() + .for_each(|lit| crate::verify::z3::assert_fact(solver, lit)); + crate::verify::z3::assert_fact(solver, &!goal_z3); + + stats::bump(|s| s.z3_timing.0.build += t_build.elapsed().as_secs_f64()); + + let t_solve = std::time::Instant::now(); + let res = solver.check(); + solver.pop(1); + stats::bump(|s| { + s.z3_timing.0.solve += t_solve.elapsed().as_secs_f64(); + s.z3_timing.0.calls += 1; + match res { + SatResult::Unsat => s.z3_timing.0.unsat += 1, + SatResult::Sat => s.z3_timing.0.sat += 1, + SatResult::Unknown => s.z3_timing.0.unknown += 1, + } + }); + + match res { + SatResult::Unsat => true, + SatResult::Unknown => false, + SatResult::Sat => false, + } + } + /// Whether e-class `id` folds to the boolean literal `b` in `probe`. fn known_bool_class(probe: &egg::EGraph, id: egg::Id, b: bool) -> bool { matches!(probe[probe.find(id)].data.known(), Some(Literal::Bool(v)) if *v == b) @@ -969,7 +1016,9 @@ impl<'a> VerifyContext<'a> { let clean = self.clean; let scratch = self.scratch.take(); let in_block = std::mem::replace(&mut self.in_block, false); + let solver_state = crate::verify::z3::enter_scratch(self); let out = f(self); + crate::verify::z3::leave_scratch(self, solver_state); self.in_block = in_block; self.scratch = scratch; self.egraph = live; diff --git a/src/verify/func_registry.rs b/src/verify/func_registry.rs index 982dff2f..bb40c25c 100644 --- a/src/verify/func_registry.rs +++ b/src/verify/func_registry.rs @@ -28,12 +28,36 @@ use crate::vmir::{Declaration, MemberId, Program, Type}; type Rule = egg::Rewrite; +#[derive(Debug, Clone, Copy)] +pub enum FuncKind { + Decl(MemberId), + Cons { + head: MemberId, + variant: usize, + }, + Proj { + head: MemberId, + variant: usize, + field: usize, + }, + IsVariant { + head: MemberId, + variant: usize, + }, + Limited(MemberId), + PreToken(MemberId), +} + /// Allocates and names the verifier ids for polymorphic ADT constructors / /// testers / projections, and accumulates their reduction rules. pub struct FuncRegistry { /// Next func id to mint (starts past every real declaration id, so a minted /// id never collides with a plain function reusing its declaration index). next: usize, + + /// Returns the kind of function. + kind: HashMap, + /// Keyed by **concept**, not by type instantiation: one id per `(head, /// variant)` / `(head, variant, field)`. The e-graph is polymorphic — /// the ground type args ride in the `FuncApp` discriminant, so a single id @@ -131,37 +155,24 @@ impl FuncRegistry { } } - let mut names = HashMap::default(); - names.insert(BUILTIN_OPTION_SOME, "Option::Some".to_string()); - names.insert(BUILTIN_OPTION_NONE, "Option::None".to_string()); - names.insert(BUILTIN_OPTION_VALUE, "Option::Some.0".to_string()); - names.insert(BUILTIN_OPTION_IS_SOME, "Option::Some?".to_string()); - names.insert(BUILTIN_OPTION_IS_NONE, "Option::None?".to_string()); - - let rules = vec![ - proj_rule(BUILTIN_OPTION_VALUE, BUILTIN_OPTION_SOME, 0), - inj_rule(BUILTIN_OPTION_SOME), - is_excl_rule(Arc::new([BUILTIN_OPTION_IS_SOME, BUILTIN_OPTION_IS_NONE])), - ]; - let mut ctor_head = HashMap::default(); - ctor_head.insert(BUILTIN_OPTION_SOME, BUILTIN_OPTION_HEAD); - ctor_head.insert(BUILTIN_OPTION_NONE, BUILTIN_OPTION_HEAD); - let mut registry = FuncRegistry { next: program.decls.len(), - cons: HashMap::default(), - proj: HashMap::default(), - adt_is: Default::default(), - limited: HashMap::default(), - fn_pre_token: HashMap::default(), - names, - rules, shapes, head_names, variant_names, - ctor_head, - quant_table: Default::default(), + ..Self::empty() }; + // Declaration-backed ids are never minted: `func_id_for_member` reuses the + // member index. Every `Function` (plain, domain, contract) and every + // `Resource` (its field/predicate location function) can be applied, so + // each gets its `Decl` kind here. + for (id, decl) in program.decls.iter_enumerated() { + if let Declaration::Function(_) | Declaration::Resource(_) = decl { + registry + .kind + .insert(func_id_for_member(id), FuncKind::Decl(id)); + } + } // Mint every head up front. Lazily minting on first use would leave // `ctor_head` incomplete for any `ConstFold` built before that use, and // the analysis is handed an immutable snapshot of the table. @@ -182,36 +193,82 @@ impl FuncRegistry { &self.quant_table } - /// An empty allocator (no ADT heads). For tests / programs without ADTs. - #[cfg(test)] + /// An allocator with no ADT heads: only the builtin `Option` ids, names and + /// rules. The base [`FuncRegistry::new`] builds on; also used directly by + /// tests / programs without ADTs. pub fn empty() -> Self { let mut names = HashMap::default(); names.insert(BUILTIN_OPTION_SOME, "Option::Some".to_string()); names.insert(BUILTIN_OPTION_NONE, "Option::None".to_string()); names.insert(BUILTIN_OPTION_VALUE, "Option::Some.0".to_string()); + names.insert(BUILTIN_OPTION_IS_SOME, "Option::Some?".to_string()); + names.insert(BUILTIN_OPTION_IS_NONE, "Option::None?".to_string()); let rules = vec![ proj_rule(BUILTIN_OPTION_VALUE, BUILTIN_OPTION_SOME, 0), - inj_rule(BUILTIN_OPTION_VALUE), + inj_rule(BUILTIN_OPTION_SOME), + is_excl_rule(Arc::new([BUILTIN_OPTION_IS_SOME, BUILTIN_OPTION_IS_NONE])), ]; let mut ctor_head = HashMap::default(); ctor_head.insert(BUILTIN_OPTION_SOME, BUILTIN_OPTION_HEAD); ctor_head.insert(BUILTIN_OPTION_NONE, BUILTIN_OPTION_HEAD); + let kind: HashMap<_, _> = [ + ( + BUILTIN_OPTION_SOME, + FuncKind::Cons { + head: BUILTIN_OPTION_HEAD, + variant: 0, + }, + ), + ( + BUILTIN_OPTION_NONE, + FuncKind::Cons { + head: BUILTIN_OPTION_HEAD, + variant: 1, + }, + ), + ( + BUILTIN_OPTION_VALUE, + FuncKind::Proj { + head: BUILTIN_OPTION_HEAD, + variant: 0, + field: 0, + }, + ), + ( + BUILTIN_OPTION_IS_SOME, + FuncKind::IsVariant { + head: BUILTIN_OPTION_HEAD, + variant: 0, + }, + ), + ( + BUILTIN_OPTION_IS_NONE, + FuncKind::IsVariant { + head: BUILTIN_OPTION_HEAD, + variant: 1, + }, + ), + ] + .into_iter() + .collect(); + FuncRegistry { next: 0, + kind, cons: HashMap::default(), proj: HashMap::default(), - adt_is: Default::default(), + adt_is: HashMap::default(), limited: HashMap::default(), fn_pre_token: HashMap::default(), names, rules, - quant_table: Default::default(), shapes: HashMap::default(), head_names: HashMap::default(), variant_names: HashMap::default(), ctor_head, + quant_table: Default::default(), } } @@ -247,7 +304,7 @@ impl FuncRegistry { if let Some(&id) = self.limited.get(&func) { return id; } - let id = self.mint(format!("{name}#lim")); + let id = self.mint(format!("{name}#lim"), FuncKind::Limited(func)); self.limited.insert(func, id); id } @@ -262,7 +319,7 @@ impl FuncRegistry { if let Some(&id) = self.fn_pre_token.get(&func) { return id; } - let id = self.mint(format!("{name}%pre")); + let id = self.mint(format!("{name}%pre"), FuncKind::PreToken(func)); self.fn_pre_token.insert(func, id); id } @@ -333,10 +390,13 @@ impl FuncRegistry { Some(name) => format!("{label}::{name}"), None => format!("{label}::#{variant}"), }; - let is_id = self.mint(format!("{cons_label}?")); + let is_id = self.mint( + format!("{cons_label}?"), + FuncKind::IsVariant { head: adt, variant }, + ); self.adt_is.insert((adt, variant), is_id); - let cons_id = self.mint(cons_label.clone()); + let cons_id = self.mint(cons_label.clone(), FuncKind::Cons { head: adt, variant }); self.rules.push(is_rule(is_id, cons_id)); self.cons.insert((adt, variant), cons_id); self.ctor_head.insert(cons_id, adt); @@ -345,7 +405,14 @@ impl FuncRegistry { self.rules.push(inj_rule(cons_id)); } for field in 0..fields { - let proj_id = self.mint(format!("{cons_label}.{field}")); + let proj_id = self.mint( + format!("{cons_label}.{field}"), + FuncKind::Proj { + head: adt, + variant, + field, + }, + ); self.proj.insert((adt, variant, field), proj_id); self.rules.push(proj_rule(proj_id, cons_id, field)); } @@ -366,10 +433,11 @@ impl FuncRegistry { .and_then(|n| n.as_deref()) } - fn mint(&mut self, name: String) -> FuncId { + fn mint(&mut self, name: String, kind: FuncKind) -> FuncId { let id = FuncId(self.next); self.next += 1; self.names.insert(id, name); + self.kind.insert(id, kind); id } @@ -381,6 +449,14 @@ impl FuncRegistry { .cloned() .unwrap_or_else(|| format!("d{}", adt.0)) } + + /// Looks up the function kind + pub fn kind(&self, f_id: &FuncId) -> FuncKind { + *self + .kind + .get(f_id) + .unwrap_or_else(|| panic!("unknown FuncId {f_id:?}")) + } } /// Derives the verifier `FuncId` for a plain, declaration-backed function. diff --git a/src/verify/mod.rs b/src/verify/mod.rs index cc8088b4..29bf6cf6 100644 --- a/src/verify/mod.rs +++ b/src/verify/mod.rs @@ -20,6 +20,7 @@ mod stats; pub(crate) mod test_support; mod types; mod viz; +mod z3; pub use error::VerifyError; pub use stats::VerifyStats; diff --git a/src/verify/stats.rs b/src/verify/stats.rs index 3b119f93..fe9a1745 100644 --- a/src/verify/stats.rs +++ b/src/verify/stats.rs @@ -128,6 +128,8 @@ pub struct VerifyStats { pub timing: TimingTrend, /// Per-e-graph wall clock (ground vs block scratch vs probes vs clones). pub graph_timing: GraphTimingTrend, + /// Z3 rung wall clock: problem building vs solving. + pub z3_timing: Z3TimingTrend, /// Per-rule search/apply wall clock (excluded from `Eq` / the snapshot). pub rule_timing: RuleTimingTrend, } @@ -170,6 +172,43 @@ impl PartialEq for GraphTimingTrend { } impl Eq for GraphTimingTrend {} +/// Wall-clock seconds spent in the Z3 rung (`prove_by_z3`), split into building +/// the problem and solving it, plus how often the rung ran and what Z3 answered. +/// Non-deterministic — a trend, never gated. +#[derive(Debug, Clone, Copy, Default)] +pub struct Z3Timing { + /// Creating the problem: translating the e-graph, goal and path condition + /// to Z3 terms and asserting them on a fresh solver. + pub build: f64, + /// `Solver::check`. + pub solve: f64, + /// Creating solvers (and the tactics they are built from). Outside `build`. + pub init: f64, + /// The `Solver::assert` calls alone. Part of `build`. + pub assert: f64, + /// Queries that reached Z3, and its answers to them. + pub calls: u64, + pub unsat: u64, + pub sat: u64, + pub unknown: u64, + /// Facts passed to `Solver::assert`, path condition and goal included. + pub facts: u64, + /// Throwaway-graph scopes (`with_scratch_graph`) in which Z3 learned + /// something that had to be discarded afterwards. + pub scratch_scopes: u64, +} + +/// [`Z3Timing`] wrapper, `Eq`-transparent like [`TimingTrend`]. +#[derive(Debug, Clone, Copy, Default)] +pub struct Z3TimingTrend(pub Z3Timing); + +impl PartialEq for Z3TimingTrend { + fn eq(&self, _: &Self) -> bool { + true + } +} +impl Eq for Z3TimingTrend {} + /// Wall-clock seconds one rule spent in its searcher/applier over the whole /// run. Non-deterministic — a trend, never gated. #[derive(Debug, Clone, Copy, Default)] @@ -271,6 +310,7 @@ impl VerifyStats { prove_ite_decompose, timing, graph_timing, + z3_timing, rule_timing, } = self; let n = |v: &u64| Json::from(*v); @@ -319,6 +359,21 @@ impl VerifyStats { ("scratch_clone", Json::from(graph_timing.0.scratch_clone)), ]), ), + ( + "z3_timing", + Json::obj([ + ("build", Json::from(z3_timing.0.build)), + ("solve", Json::from(z3_timing.0.solve)), + ("init", Json::from(z3_timing.0.init)), + ("assert", Json::from(z3_timing.0.assert)), + ("calls", n(&z3_timing.0.calls)), + ("unsat", n(&z3_timing.0.unsat)), + ("sat", n(&z3_timing.0.sat)), + ("unknown", n(&z3_timing.0.unknown)), + ("facts", n(&z3_timing.0.facts)), + ("scratch_scopes", n(&z3_timing.0.scratch_scopes)), + ]), + ), ( "rule_timing", Json::obj(rule_timing.0.iter().map(|(k, t)| { diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs new file mode 100644 index 00000000..79091fd0 --- /dev/null +++ b/src/verify/z3/mod.rs @@ -0,0 +1,744 @@ +use crate::verify::lang::{FuncId, Symbolic}; +use itertools::Itertools; + +use crate::verify::context::VerifyContext; +use crate::verify::func_registry::{BUILTIN_OPTION_HEAD, FuncKind}; +use crate::verify::stats; +use crate::vmir::{BinOp, Literal, MemberId, Polarity, Type}; +use crate::{HashMap, vmir}; +use egg::Id; +use std::borrow::Cow; +use z3::ast::{Ast, Bool, Dynamic}; +use z3::datatype_builder::create_datatypes; +use z3::{DatatypeAccessor, DatatypeBuilder, DatatypeSort, FuncDecl, Solver, Sort}; + +/// The translator's caches, kept in `VerifyContext::z3translator` so sorts and +/// datatypes are created once per context. The translation itself is the free +/// functions below, which reach these through the context. +pub(crate) struct Z3Translation { + sorts: HashMap, + adts: HashMap, + class_types: HashMap, + func_cache: HashMap, FuncDecl>>, + max_node_id: usize, + max_merges_is: usize, + pub(crate) solver: Solver, +} + +impl Default for Z3Translation { + fn default() -> Self { + Self { + sorts: HashMap::default(), + adts: HashMap::default(), + class_types: HashMap::default(), + func_cache: HashMap::default(), + max_node_id: 0, + max_merges_is: 0, + solver: new_solver(), + } + } +} + +/// The options Silicon sets in its preamble (`z3config.smt2`) that change how +/// Z3 solves. MBQI is off, so quantifiers are instantiated only through their +/// triggers, and arithmetic uses the old simplex solver (2) rather than Z3's +/// default (6). `auto_config false` keeps Z3 from choosing its own settings per +/// query over these. Silicon's other options only concern its SMT-LIB pipe +/// (`print-success`, `global-decls`, `type_check`) or how models and numbers +/// are printed (`model.*`, `pp.*`). +const SILICON_PARAMS: &[(&str, &str)] = &[ + ("auto_config", "false"), + ("smt.case_split", "3"), + ("smt.delay_units", "true"), + ("smt.mbqi", "false"), + ("smt.qi.eager_threshold", "100"), + ("smt.arith.solver", "2"), + ("smt.qi.max_multi_patterns", "1000"), +]; + +/// Set [`SILICON_PARAMS`] once per process. They are global parameters, and +/// `auto_config` is read when a context is made, so this has to run before the +/// first z3 call on any thread creates that thread's context. +fn set_silicon_params() { + static ONCE: std::sync::Once = std::sync::Once::new(); + ONCE.call_once(|| { + for (k, v) in SILICON_PARAMS { + z3::set_global_param(k, v); + } + }); +} + +/// The solver one context keeps for all its queries; its creation is counted as +/// `z3_timing.init`. +/// +/// Every check is limited to `SILVER_OXIDE_Z3_RLIMIT` resource units (default +/// 1,500,000, about 2 s on the benchmark suite). The persistent solver can get +/// stuck on one query for minutes; running out of units ends it as `unknown`, +/// which the rung treats as "not proven". Unlike a timeout, the limit gives the +/// same verdict on every machine. Z3 applies `rlimit` to each check, although +/// its `rlimit count` statistic keeps running over the solver's life. +pub(crate) fn new_solver() -> Solver { + let t = std::time::Instant::now(); + set_silicon_params(); + let solver = Solver::new(); + let rlimit = std::env::var("SILVER_OXIDE_Z3_RLIMIT") + .ok() + .and_then(|v| v.parse().ok()) + .unwrap_or(1_500_000); + let mut params = z3::Params::new(); + params.set_u32("rlimit", rlimit); + solver.set_params(¶ms); + crate::verify::stats::bump(|s| s.z3_timing.0.init += t.elapsed().as_secs_f64()); + solver +} + +/// The translator state that names e-graph ids, saved while a throwaway graph +/// stands in for the live one (`VerifyContext::with_scratch_graph`). +pub(crate) struct ScratchScope { + max_node_id: usize, + max_merges_is: usize, + class_types: HashMap, +} + +/// Open a solver scope before the live graph is swapped for a throwaway clone. +/// The clone hands out ids past the live graph's, and those ids are handed out +/// again once the live graph is back, for different terms. Everything Z3 learns +/// about them has to go with the clone. +pub(crate) fn enter_scratch(ctxt: &mut VerifyContext) -> ScratchScope { + ctxt.z3translator.solver.push(); + let tr = &ctxt.z3translator; + ScratchScope { + max_node_id: tr.max_node_id, + max_merges_is: tr.max_merges_is, + class_types: tr.class_types.clone(), + } +} + +/// Drop what Z3 learned on the throwaway graph: its facts (`pop`), the +/// watermarks past the live graph, and the sorts cached for its ids. +pub(crate) fn leave_scratch(ctxt: &mut VerifyContext, scope: ScratchScope) { + let tr = &mut ctxt.z3translator; + tr.solver.pop(1); + if tr.max_node_id != scope.max_node_id || tr.max_merges_is != scope.max_merges_is { + stats::bump(|s| s.z3_timing.0.scratch_scopes += 1); + } + tr.max_node_id = scope.max_node_id; + tr.max_merges_is = scope.max_merges_is; + tr.class_types = scope.class_types; +} + +/// `solver.assert(fact)`, timed as `z3_timing.assert` and counted as a fact. +pub(crate) fn assert_fact(solver: &Solver, fact: &Bool) { + let t = std::time::Instant::now(); + solver.assert(fact); + crate::verify::stats::bump(|s| { + s.z3_timing.0.assert += t.elapsed().as_secs_f64(); + s.z3_timing.0.facts += 1; + }); +} + +/// Parameter and return types of function declaration `func` at instantiation +/// `tys`. Every declared `FuncId` is a `vmir::Function`: ordinary, domain, and +/// field/predicate address functions alike. +fn function_signature(ctxt: &VerifyContext, func: MemberId, tys: &[Type]) -> (Vec, Type) { + match &ctxt.decls[func] { + vmir::Declaration::Domain(_) => { + unreachable!( + "the domain declaration only holds the name of the declaration. It can never be a function." + ) + } + vmir::Declaration::Axiom(_) => { + unreachable!("the axiom declaration only holds the axiom. It can never be a function.") + } + vmir::Declaration::Function(fun) => { + let params = fun.params.iter().map(|t| t.subst_generics(tys)).collect(); + (params, fun.ret.subst_generics(tys)) + } + vmir::Declaration::Method(_) => { + unreachable!("methods are lowered to exhale/inhale. A method is never called.") + } + vmir::Declaration::Resource(r) => { + let params = r.params.iter().map(|t| t.subst_generics(tys)).collect(); + let group = ctxt + .groups + .get(ctxt.interner.resolve(&r.name)) + .expect("predicate group tag"); + let ret = r.derive_location(func, group).ret; + (params, ret) + } + vmir::Declaration::Adt(_) => { + unreachable!("adt are lowered to specific pure instructions and not to a function call") + } + } +} + +/// The type of e-class `id` (translation.typ, "Class sorts"), or `None` when no +/// node of the class has a certain type. Unlike `types::infer_type` this never +/// guesses: without a sort the class cannot be declared to Z3, so its facts are +/// left out instead. +/// +/// Cached per canonical id. Only `Some` is cached: a type survives merges, +/// "unknown" may not. +fn class_type(ctxt: &mut VerifyContext, id: Id) -> Option { + // Take the cache out so `ctxt` can be borrowed immutably (and the class's + // nodes iterated in place) while the cache is filled. + let mut cache = std::mem::take(&mut ctxt.z3translator.class_types); + let ty = cached_class_type(ctxt, &mut cache, &mut Vec::new(), id); + ctxt.z3translator.class_types = cache; + ty +} + +/// `visiting` holds the classes whose `Ite` nodes are being followed, so an +/// `Ite` cycle back into one of them counts as uncertain instead of looping. +fn cached_class_type( + ctxt: &VerifyContext, + cache: &mut HashMap, + visiting: &mut Vec, + id: Id, +) -> Option { + let id = ctxt.egraph.find(id); + if let Some(ty) = cache.get(&id) { + return Some(ty.clone()); + } + if visiting.contains(&id) { + return None; + } + let nodes = &ctxt.egraph[id].nodes; + // Nodes with a type of their own first: no recursion, and nearly every + // class has one. + let ty = nodes + .iter() + .find_map(|n| local_node_type(ctxt, n)) + .or_else(|| { + visiting.push(id); + let ty = nodes.iter().find_map(|n| match n { + Symbolic::Ite([_, then, els]) => cached_class_type(ctxt, cache, visiting, *then) + .or_else(|| cached_class_type(ctxt, cache, visiting, *els)), + _ => None, + }); + visiting.pop(); + ty + }); + debug_assert!( + ty.as_ref().is_none_or(|ty| nodes + .iter() + .filter_map(|n| local_node_type(ctxt, n)) + .all(|other| other == *ty)), + "e-class {id} mixes types" + ); + if let Some(ty) = &ty { + cache.insert(id, ty.clone()); + } + ty +} + +/// The type of one e-node from the node alone, or `None` when it is not +/// certain. An `Ite` takes its branches' type, so it is `None` here and left to +/// [`cached_class_type`]. +fn local_node_type(ctxt: &VerifyContext, node: &Symbolic) -> Option { + match node { + Symbolic::Lit(lit) => Some(crate::verify::types::lit_type(lit)), + Symbolic::Fresh(u) => ctxt.fresh_types.get(u).cloned(), + Symbolic::Binary(op, _) => match op { + BinOp::Eq | BinOp::LtI | BinOp::LtR => Some(Type::Bool), + // Arithmetic yields its operand type. + _ => op.sort(), + }, + Symbolic::RealCast(_) => Some(Type::Real), + Symbolic::Forall(..) => Some(Type::Bool), + Symbolic::Ite(_) => None, + Symbolic::FuncApp(f, tys, _) => match ctxt.alloc.kind(f) { + FuncKind::Decl(m) | FuncKind::Limited(m) => Some(function_signature(ctxt, m, tys).1), + FuncKind::PreToken(_) => Some(Type::Bool), + FuncKind::Cons { head, .. } => Some(adt_type(ctxt, head, tys)), + FuncKind::Proj { + head, + variant, + field, + } => Some(field_types(ctxt, head, variant, tys).swap_remove(field)), + FuncKind::IsVariant { .. } => Some(Type::Bool), + }, + } +} + +/// One equation `c_{class} == ⟦node⟧` per e-node (translation.typ, "The e-graph"). +/// An equation that needs a sort we cannot determine is dropped with a warning: +/// leaving out an assumption only weakens what Z3 knows, so it stays sound. +pub(crate) fn sync_facts(ctxt: &mut VerifyContext) { + let start = ctxt.z3translator.max_node_id; + let end = ctxt.egraph.nodes().len(); + for i in start..end { + let id = Id::from(i); + // Clone just this node: translating needs `ctxt` mutably (the caches), + // so the node list cannot stay borrowed across the call. + let node = ctxt.egraph.id_to_node(id).clone(); + if matches!(node, Symbolic::Forall(..)) { + continue; + } + let Some(expr) = symbol_to_z3(ctxt, &node) else { + eprintln!( + "[z3] warning: an operand of `{node}` has no certain type; dropping its fact" + ); + continue; + }; + let class = ctxt.egraph.find(id); + let Some(c) = class_const(ctxt, class) else { + eprintln!("[z3] warning: could not create the class_const for {class}"); + continue; + }; + assert_fact(&ctxt.z3translator.solver, &c.eq(expr)); + } + ctxt.z3translator.max_node_id = end; + + let start = ctxt.z3translator.max_merges_is; + let end = ctxt.egraph.union_log().len(); + for i in start..end { + let (a, b) = ctxt.egraph.union_log()[i]; + match (logged_class_const(ctxt, a), logged_class_const(ctxt, b)) { + (Some(c_a), Some(c_b)) => assert_fact(&ctxt.z3translator.solver, &c_a.eq(c_b)), + (_, _) => eprintln!("[z3] warning: could not find class_const for {a} or {b}"), + } + } + ctxt.z3translator.max_merges_is = end; +} + +pub(crate) fn build_goal(ctxt: &mut VerifyContext, id: Id) -> Bool { + class_const_given_sort(ctxt, id, &Sort::bool()) + .as_bool() + .unwrap() +} + +pub(crate) fn build_pc(ctxt: &mut VerifyContext, pc: &[(egg::Id, Polarity)]) -> Vec { + pc.iter() + .map(|(id, p)| { + let c_const = class_const_given_sort(ctxt, *id, &Sort::bool()) + .as_bool() + .unwrap(); + match p { + Polarity::Positive => c_const, + Polarity::Negative => !c_const, + } + }) + .collect() +} + +/// The constant for `id` itself, *not* its current root. +fn raw_class_const(id: Id, sort: &Sort) -> Dynamic { + Dynamic::new_const(format!("c_{id}"), sort) +} + +fn class_const_given_sort(ctxt: &VerifyContext, id: Id, sort: &Sort) -> Dynamic { + raw_class_const(ctxt.egraph.find(id), sort) +} + +/// The constant of a root recorded in the union log, named by that id and not +/// by its current root: by now both sides of a merge share one root, so +/// `find` would turn every logged merge into `c_r == c_r`. Facts were asserted +/// under the root at sync time, and the log links every former root to its +/// absorber, so these equations connect them to the current root. +fn logged_class_const(ctxt: &mut VerifyContext, id: Id) -> Option { + let typ = class_type(ctxt, id)?; + let sort = sort(ctxt, &typ); + Some(raw_class_const(id, &sort)) +} + +/// `None` when the class's type is not certain (see [`class_type`]). +fn class_const(ctxt: &mut VerifyContext, id: Id) -> Option { + let typ = class_type(ctxt, id)?; + let sort = sort(ctxt, &typ); + Some(class_const_given_sort(ctxt, id, &sort)) +} + +pub(crate) fn sort(ctxt: &mut VerifyContext, ty: &Type) -> Sort { + if let Some(s) = ctxt.z3translator.sorts.get(ty) { + return s.clone(); + } + // Copy the `&'a` references out, so what they point to is not borrowed + // through `ctxt` while `ctxt` is passed on mutably. + let (decls, interner) = (ctxt.decls, ctxt.interner); + let sort = match ty { + Type::Int => Sort::int(), + Type::Bool => Sort::bool(), + Type::Real => Sort::real(), + Type::Ref => Sort::uninterpreted("Ref".into()), + Type::Domain(id, args) => match &decls[*id] { + vmir::Declaration::Domain(d) => { + debug_assert!(args.is_empty(), "domains are monomorphic"); + Sort::uninterpreted(format!("dom@{}", interner.resolve(&d.name)).into()) + } + vmir::Declaration::Adt(_) => datatype(ctxt, ty).sort.clone(), + _ => unreachable!("Type::Domain must name a domain or an ADT"), + }, + Type::Snap(_) | Type::Option(_) => datatype(ctxt, ty).sort.clone(), + // `addr@[g] T` (translation.typ). The bound is not part of the name: the + // group already fixes it (fields are 1/1, predicates unbounded). + Type::Addr { group, value, .. } => { + Sort::uninterpreted(format!("addr@[{}] {value}", ctxt.groups.resolve(group)).into()) + } + Type::Generic(_) => unreachable!("generics are currently not supported"), + }; + ctxt.z3translator.sorts.insert(ty.clone(), sort.clone()); + sort +} + +/// `⟦symbol⟧`, or `None` when an operand's sort is not certain. +fn symbol_to_z3(ctxt: &mut VerifyContext, symbol: &Symbolic) -> Option { + Some(match symbol { + Symbolic::Fresh(i) => { + let ty = ctxt.fresh_types.get(i)?.clone(); + Dynamic::new_const(format!("fresh{i}"), &sort(ctxt, &ty)) + } + Symbolic::Lit(literal) => match literal { + Literal::Null => Dynamic::new_const("null", &sort(ctxt, &Type::Ref)), + Literal::Bool(value) => z3::ast::Bool::from_bool(*value).into(), + Literal::Int(value) => z3::ast::Int::from_big_int(value).into(), + Literal::Real(value) => z3::ast::Real::from_big_rational(value).into(), + }, + Symbolic::Binary(op, [l, r]) => { + // `Eq` is the only operator without a fixed operand sort; either + // side fixes it. + let operand_ty = match op.sort() { + Some(ty) => ty, + None => class_type(ctxt, *l).or_else(|| class_type(ctxt, *r))?, + }; + let sort = sort(ctxt, &operand_ty); + let l = class_const_given_sort(ctxt, *l, &sort); + let r = class_const_given_sort(ctxt, *r, &sort); + match op { + BinOp::Eq => l.eq(&r).into(), + BinOp::AddI | BinOp::SubI | BinOp::MulI | BinOp::DivI | BinOp::Mod | BinOp::LtI => { + let (l, r) = (l.as_int().unwrap(), r.as_int().unwrap()); + match op { + BinOp::AddI => (l + r).into(), + BinOp::SubI => (l - r).into(), + BinOp::MulI => (l * r).into(), + BinOp::DivI => l.div(&r).into(), + BinOp::Mod => l.modulo(&r).into(), + BinOp::LtI => l.lt(&r).into(), + _ => unreachable!("excluded by outer matching"), + } + } + BinOp::AddR | BinOp::SubR | BinOp::MulR | BinOp::DivR | BinOp::LtR => { + let (l, r) = (l.as_real().unwrap(), r.as_real().unwrap()); + match op { + BinOp::AddR => (l + r).into(), + BinOp::SubR => (l - r).into(), + BinOp::MulR => (l * r).into(), + BinOp::DivR => l.div(&r).into(), + BinOp::LtR => l.lt(&r).into(), + _ => unreachable!("excluded by outer matching"), + } + } + } + } + Symbolic::Ite([cond, then, els]) => { + let then_ty = class_type(ctxt, *then).or_else(|| class_type(ctxt, *els))?; + let sort = sort(ctxt, &then_ty); + let cond = class_const_given_sort(ctxt, *cond, &Sort::bool()) + .as_bool() + .unwrap(); + let then = class_const_given_sort(ctxt, *then, &sort); + let els = class_const_given_sort(ctxt, *els, &sort); + cond.ite(&then, &els) + } + Symbolic::FuncApp(id, ty, args) => translate_function(ctxt, id, ty, args), + Symbolic::RealCast(id) => { + let class = class_const(ctxt, *id)?.as_int().unwrap(); + class.to_real().into() + } + Symbolic::Forall(_, _) => todo!("implement translation for forall nodes"), + }) +} + +// the type build by heads constructor at instantiation typs +fn adt_type(ctxt: &VerifyContext, head: MemberId, tys: &[Type]) -> Type { + if head == BUILTIN_OPTION_HEAD { + return Type::Option(Box::new(tys[0].clone())); + } + + match &ctxt.decls[head] { + vmir::Declaration::Adt(_) => Type::Domain(head, tys.into()), + vmir::Declaration::Resource(_) => Type::Snap(head), + _ => unreachable!("an ADT head is an ADT, a predicate (snapshot), or Option"), + } +} + +fn field_types(ctxt: &VerifyContext, head: MemberId, variant: usize, tys: &[Type]) -> Vec { + if head == BUILTIN_OPTION_HEAD { + return if variant == 0 { + vec![tys[0].clone()] + } else { + vec![] + }; // Some(T) / None + } + match &ctxt.decls[head] { + vmir::Declaration::Adt(adt) => adt.variants[variant] + .field_types + .iter() + .map(|t| t.subst_generics(tys)) + .collect(), + vmir::Declaration::Resource(r) => r + .derive_snapshot() + .expect("snapshot of a resource that is not self-framed") + .variants[variant] + .field_types + .clone(), + _ => unreachable!("an ADT head is an ADT, a predicate (snapshot), or Option"), + } +} +/// `f[tys](args)` as an application of the uninterpreted Z3 function +/// `fn{f}` with signature `params -> ret`. The name carries the type +/// arguments because one `FuncId` serves every instantiation +/// (translation.typ, "Function applications"). +fn uninterpreted_app( + ctxt: &mut VerifyContext, + f: FuncId, + tys: &[Type], + params: &[Type], + ret: &Type, + args: &[Id], +) -> Dynamic { + assert_eq!( + params.len(), + args.len(), + "arity mismatch applying fn{}", + f.0 + ); + + let domain: Vec = params.iter().map(|t| sort(ctxt, t)).collect(); + let arg_consts: Vec = args + .iter() + .zip(&domain) + .map(|(a, s)| class_const_given_sort(ctxt, *a, s)) + .collect(); + let arg_refs: Vec<&dyn Ast> = arg_consts.iter().map(|a| a as &dyn Ast).collect(); + if let Some(decl) = ctxt + .z3translator + .func_cache + .get(&f) + .and_then(|m| m.get(tys)) + { + decl.apply(&arg_refs) + } else { + let range = sort(ctxt, ret); + let name = if tys.is_empty() { + format!("fn{}", f.0) + } else { + format!("fn{}<{}>", f.0, tys.iter().join(",")) + }; + let domain_refs: Vec<&Sort> = domain.iter().collect(); + let func_decl = FuncDecl::new(name, &domain_refs, &range); + let res = func_decl.apply(&arg_refs); + ctxt.z3translator + .func_cache + .entry(f) + .or_default() + .insert(tys.into(), func_decl); + res + } +} + +fn translate_function( + ctxt: &mut VerifyContext, + f_id: &FuncId, + ty: &[Type], + args: &[Id], +) -> Dynamic { + let function_type = ctxt.alloc.kind(f_id); + + match function_type { + // A function, a domain function, or a field/predicate address + // or a resource function + // function: all are `vmir::Function`s. + FuncKind::Decl(id) => { + let (params, ret) = function_signature(ctxt, id, ty); + uninterpreted_app(ctxt, *f_id, ty, ¶ms, &ret, args) + } + // ADT construction + FuncKind::Cons { variant, head } => { + let adt_ty = adt_type(ctxt, head, ty); + let field_tys = field_types(ctxt, head, variant, ty); + let fields = args + .iter() + .zip(&field_tys) + .map(|(arg, ty)| { + let s = sort(ctxt, ty); + class_const_given_sort(ctxt, *arg, &s) + }) + .collect::>(); + + let field_refs = fields + .iter() + .map(|f| f as &dyn Ast) + .collect::>(); + + sort(ctxt, &adt_ty); // builds and caches the datatype + ctxt.z3translator.adts[&adt_ty].variants[variant] + .constructor + .apply(&field_refs) + } + // ADT projection + FuncKind::Proj { + head, + variant, + field, + } => { + let adt_ty = adt_type(ctxt, head, ty); + let adt_sort = sort(ctxt, &adt_ty); // builds and caches the datatype + let base = class_const_given_sort(ctxt, args[0], &adt_sort); + ctxt.z3translator.adts[&adt_ty].variants[variant].accessors[field].apply(&[&base]) + } + // ADT tester `Adt::Ctor?`: the datatype's own recognizer for `variant`. + FuncKind::IsVariant { head, variant } => { + let adt_ty = adt_type(ctxt, head, ty); + let adt_sort = sort(ctxt, &adt_ty); // builds and caches the datatype + let base = class_const_given_sort(ctxt, args[0], &adt_sort); + ctxt.z3translator.adts[&adt_ty].variants[variant] + .tester + .apply(&[&base]) + } + // `f#lim`: same signature as `f`, only the id (and so the name) differs. + // `f(x) == f#lim(x)` reaches Z3 only where the e-graph already has it. + FuncKind::Limited(func) => { + let (params, ret) = function_signature(ctxt, func, ty); + uninterpreted_app(ctxt, *f_id, ty, ¶ms, &ret, args) + } + // `f%pre`: over `f`'s own parameters, returning `Bool`. + FuncKind::PreToken(func) => { + let (params, _) = function_signature(ctxt, func, ty); + uninterpreted_app(ctxt, *f_id, ty, ¶ms, &Type::Bool, args) + } + } +} + +/// A datatype's declaration before Z3 sees it: the builder name and, per +/// constructor, its name and its `(accessor name, field type)`s. +struct DatatypeShape { + name: String, + variants: Vec<(String, Vec<(String, Type)>)>, +} + +/// The shape of `ty` if it is a datatype (an ADT, a snapshot, or `Option`); +/// `None` for every other sort. +fn datatype_shape(ctxt: &VerifyContext, ty: &Type) -> Option { + let interner = ctxt.interner; + let (adt, args): (Cow, &[Type]) = match ty { + Type::Option(inner) => { + let name = format!("adt@{ty}"); // `adt@Option` + return Some(DatatypeShape { + variants: vec![ + ( + format!("{name}.Some"), + vec![(format!("{name}.Some.0"), (**inner).clone())], + ), + (format!("{name}.None"), vec![]), + ], + name, + }); + } + Type::Domain(id, args) => match &ctxt.decls[*id] { + vmir::Declaration::Adt(a) => (Cow::Borrowed(a), &args[..]), + _ => return None, + }, + Type::Snap(id) => match &ctxt.decls[*id] { + vmir::Declaration::Resource(r) => ( + Cow::Owned(r.derive_snapshot().expect("adt of resource")), + &[], + ), + _ => unreachable!("snapshot can only be taken from resources."), + }, + _ => return None, + }; + let base = format!("adt@{}", interner.resolve(&adt.name)); + let name = if args.is_empty() { + base + } else { + format!("{base}<{}>", args.iter().join(",")) + }; + let mut variants = Vec::new(); + for (v, variant) in adt.variants.iter().enumerate() { + let ctor = match variant.name { + Some(n) => format!("{name}.{}", interner.resolve(&n)), + None => format!("{name}#{v}"), + }; + let fields = variant + .field_types + .iter() + .enumerate() + .map(|(i, field)| (format!("{ctor}.{i}"), field.subst_generics(args))) + .collect(); + variants.push((ctor, fields)); + } + Some(DatatypeShape { name, variants }) +} + +/// The Z3 datatype for `ty`, declared on first use. +pub(crate) fn datatype<'c>(ctxt: &'c mut VerifyContext, ty: &Type) -> &'c DatatypeSort { + if !ctxt.z3translator.adts.contains_key(ty) { + declare_datatypes(ctxt, ty); + } + &ctxt.z3translator.adts[ty] +} + +/// Declare `root` together with every not-yet-declared datatype reachable from +/// it through constructor fields, in one `create_datatypes` call. Inside the +/// group a field refers to another member by name, so recursion through another +/// datatype (a snapshot holding `Option` of itself, mutually recursive ADTs) +/// never needs a sort that does not exist yet. +fn declare_datatypes(ctxt: &mut VerifyContext, root: &Type) { + let mut group: HashMap = HashMap::default(); + let mut pending = vec![root.clone()]; + while let Some(ty) = pending.pop() { + if group.contains_key(&ty) || ctxt.z3translator.adts.contains_key(&ty) { + continue; + } + let Some(shape) = datatype_shape(ctxt, &ty) else { + continue; + }; + for (_, fields) in &shape.variants { + pending.extend(fields.iter().map(|(_, field)| field.clone())); + } + group.insert(ty, shape); + } + + // A field outside the group is not a datatype or is already declared, so + // `sort` on it never comes back here. + let mut builders = Vec::new(); + for shape in group.values() { + let mut builder = DatatypeBuilder::new(shape.name.as_str()); + for (ctor, fields) in &shape.variants { + let mut accs = Vec::new(); + for (acc, field) in fields { + accs.push(( + acc.as_str(), + match group.get(field) { + Some(member) => DatatypeAccessor::datatype(member.name.as_str()), + None => DatatypeAccessor::sort(sort(ctxt, field)), + }, + )); + } + builder = builder.variant(ctor, accs); + } + builders.push(builder); + } + + // `create_datatypes` returns the sorts in builder order. + for (ty, dt) in group.into_keys().zip(create_datatypes(builders)) { + ctxt.z3translator.adts.insert(ty, dt); + } +} + +#[cfg(test)] +mod tests { + use super::*; + + /// Z3 only warns on stderr about a parameter it does not know, so check + /// that every one of Silicon's options took. + #[test] + fn silicon_params_are_set() { + set_silicon_params(); + for (k, v) in SILICON_PARAMS { + assert_eq!(z3::get_global_param(k).as_deref(), Some(*v), "{k}"); + } + } +} diff --git a/tests/cases/failing/ctor_ite_same_ctor_arms_pin_nothing.vpr b/tests/cases/failing/ctor_ite_same_ctor_arms_pin_nothing.vpr deleted file mode 100644 index 60f8e0c9..00000000 --- a/tests/cases/failing/ctor_ite_same_ctor_arms_pin_nothing.vpr +++ /dev/null @@ -1,16 +0,0 @@ -// Soundness canary for the constructor half of `ite-reduce`'s arm-differs -// pinning (see passing/ctor_arm_pins_ite_condition.vpr). -// -// The fingerprint is the constructor's *identity*, not the whole term, so two -// applications of one constructor never separate — even here, where the -// payloads are known to differ. Losing that is incompleteness; pinning `b` -// would be unsound. Must stay rejected. - -adt SH { c0() c1(x: Int) } - -method same_ctor_different_payloads(b: Bool, x: Int, y: Int) - requires x != y -{ - assume (b ? c1(x) : c1(y)) == c1(x) - assert b -} diff --git a/tests/cases/known_limitations/loops/ORACLE.md b/tests/cases/known_limitations/loops/ORACLE.md deleted file mode 100644 index da83d380..00000000 --- a/tests/cases/known_limitations/loops/ORACLE.md +++ /dev/null @@ -1,88 +0,0 @@ -# Loop corpus — Silicon oracle - -Every case below was run through Silicon and its outcome recorded. Silicon is -the reference: any disagreement between us and this table is a bug in one of the -two, and the burden is on us. - -Reproduce: - -```sh -Z3_EXE=/usr/sbin/z3 java -Xss512m \ - -cp ~/Documents/ethz/thesis/viperserver/target/scala-2.13/viperserver.jar \ - viper.silicon.SiliconRunner .vpr -``` - -Silicon version: `1.1-SNAPSHOT (b4cdf753@(detached))`. Recorded 2026-08-04. - -## Must verify — `known_limitations/loops/` until the stage that fixes them - -Currently all fail: `viper/cfg.rs:266` rejects the back edge, `typecheck/mod.rs:1514` -rejects `while`. Promote each to `passing/loops/` as it starts verifying — the -`known_limitations_still_fail` test breaks the build to force this. - -| case | scenario | Silicon | promoted by | -|---|---|---|---| -| `scalar_sum.vpr` | S1 scalar accumulator | PASS | stage 4 | -| `list_walk.vpr` | S2 predicate traversal, no QP | PASS | stage 4 | -| `loop_under_if.vpr` | S3 loop under a path condition | PASS | stage 4 | -| `zero_iter.vpr` | S11 zero-iteration loop | PASS | stage 4 | -| `wildcard_ro.vpr` | S15 read-only framing via wildcard | PASS | stage 4 | -| `frame_survives.vpr` | frame preserved verbatim across the cut | PASS | stage 4 | -| `goto_loop.vpr` | Prusti's shape: label-carried invariant | PASS | stage 4 | -| `no_invariant.vpr` | S12 invariant-less head, still provable | PASS | stage 4 | -| `nested.vpr` | S7 nested loops | PASS | stage 7 | -| `break_simple.vpr` | S4 `break` out of a loop | PASS | stage 6 | -| `break_state.vpr` | S4 out edge carries live state | PASS | stage 6 | - -## Structural (Peano) loops — `passing/loops/` - -Peano naturals drive the loop by a **discriminator check**, so the cut is exercised with -no integer reasoning anywhere. This is what isolates loop correctness from the -arithmetic gap that blocks the integer cases above. - -| case | what it pins down | Silicon | ours | -|---|---|---|---| -| `peano_countdown.vpr` | data-dependent guard on a havoc'd variable; the post-loop fact comes only from the exit edge's guard negation | PASS | PASS | -| `peano_invariant.vpr` | a **load-bearing** invariant: established, preserved across the body, consumed after | PASS | PASS | -| `peano_havoc_control.vpr` | same program, invariant dropped — must FAIL, or the cut is not havocing | FAIL | FAIL | - -The last is the one that matters. `peano_invariant` passing proves the cut -carries the invariant; `peano_havoc_control` failing proves it does not carry -anything *else*. Without the pair, a cut that simply threaded the pre-loop state -through unchanged would pass the first and be silently unsound. - -## Must be rejected — `failing/loops/` - -Green today for the wrong reason (loops unsupported ⇒ pipeline error, which -counts as rejection). They become meaningful once stage 4 lands. - -| case | why it must fail | Silicon error | -|---|---|---| -| `wildcard_ro_write.vpr` | write permission in the invariant ⇒ frame residual empty ⇒ value not retained | `assert.failed:assertion.false` — `box.f == 10` | -| `havoc_loses_value.vpr` | the cut havocs written vars even when the loop runs zero times | `assert.failed:assertion.false` — `i == 5` | -| `no_invariant_loses.vpr` | S12 — empty invariant ⇒ nothing relates `i` to `n` across the cut | `postcondition.violated:assertion.false` — `i == n` | - -## The load-bearing pair - -`wildcard_ro.vpr` (PASS) and `wildcard_ro_write.vpr` (FAIL) are the same program -differing only in the invariant's permission amount. Together they pin down the -mechanism that makes read-only framing work: - -- **wildcard** — exhale leaves a *positive* residual in the frame, so the frame - retains the value, and `box.f == 10` survives the loop. -- **write** — exhale takes everything, the frame residual is empty, no value - agreement is available, and the assertion correctly fails. - -Silicon's heap at the assertion in the wildcard case: - -``` -box@2@12.f -> ms@11@12 # $k@6@12 + W - $k@7@12 -``` - -`ms@11@12` is a merged snapshot — `singleMerge` emits `snapEqs` equating it to -both sides. Permission is the body's wildcard plus the frame residual `W - $k`. - -This pair is the highest-risk item in the whole plan (`design/loops/PLAN.md` §8): -if our wildcard exhale cannot leave a usable residual, read-only framing is lost -and every invariant gets heavier. It is in the corpus from day one so that -surfaces immediately rather than at stage 8. diff --git a/tests/cases/passing/ctor_arm_pins_ite_condition.vpr b/tests/cases/passing/ctor_arm_pins_ite_condition.vpr index cc036d38..2c3155db 100644 --- a/tests/cases/passing/ctor_arm_pins_ite_condition.vpr +++ b/tests/cases/passing/ctor_arm_pins_ite_condition.vpr @@ -6,8 +6,11 @@ // same premise `ConstFold` uses to fold a `Ctor == Ctor` comparison to `false` // and to declare a two-constructor class inconsistent. // -// The negative half (identical arms, same-constructor arms, and the arm that -// *does* match) lives in `failing/ctor_ite_*_pins_nothing.vpr`. +// The negative half (identical arms and the arm that *does* match) lives in +// `failing/ctor_ite_identical_arms_pin_nothing.vpr` and +// `failing/ctor_ite_matching_arm_pins_no_polarity.vpr`. Same-constructor arms with differing +// payloads entail the condition by injectivity, so that case is in +// `passing/ctor_ite_same_ctor_arms_pin_nothing.vpr`. adt SH { c0() c1(x: Int) } diff --git a/tests/cases/passing/ctor_ite_same_ctor_arms_pin_nothing.vpr b/tests/cases/passing/ctor_ite_same_ctor_arms_pin_nothing.vpr new file mode 100644 index 00000000..60d4c3e8 --- /dev/null +++ b/tests/cases/passing/ctor_ite_same_ctor_arms_pin_nothing.vpr @@ -0,0 +1,20 @@ +// Same-constructor arms of an ite (see ctor_arm_pins_ite_condition.vpr). +// +// `ite-reduce`'s arm-differs pinning fingerprints the constructor's *identity*, +// not the whole term, so two applications of one constructor never separate it, +// even though the payloads here are known to differ. The e-graph tiers +// therefore cannot pin `b`. +// +// The assert is still valid: with `!b` the assumption becomes `c1(y) == c1(x)`, +// injectivity gives `y == x`, and that contradicts `x != y`. The Z3 rung proves +// it. This case was once a soundness canary in failing/, which was a +// misclassification: `b` is entailed, so pinning it is not unsound. + +adt SH { c0() c1(x: Int) } + +method same_ctor_different_payloads(b: Bool, x: Int, y: Int) + requires x != y +{ + assume (b ? c1(x) : c1(y)) == c1(x) + assert b +} diff --git a/tests/cases/known_limitations/goal_needs_case_split_heap_dep.vpr b/tests/cases/passing/goal_needs_case_split_heap_dep.vpr similarity index 100% rename from tests/cases/known_limitations/goal_needs_case_split_heap_dep.vpr rename to tests/cases/passing/goal_needs_case_split_heap_dep.vpr diff --git a/tests/cases/known_limitations/goal_needs_case_split_heap_free.vpr b/tests/cases/passing/goal_needs_case_split_heap_free.vpr similarity index 100% rename from tests/cases/known_limitations/goal_needs_case_split_heap_free.vpr rename to tests/cases/passing/goal_needs_case_split_heap_free.vpr diff --git a/tests/cases/known_limitations/goal_needs_case_split_ternary_call.vpr b/tests/cases/passing/goal_needs_case_split_ternary_call.vpr similarity index 100% rename from tests/cases/known_limitations/goal_needs_case_split_ternary_call.vpr rename to tests/cases/passing/goal_needs_case_split_ternary_call.vpr diff --git a/tests/cases/known_limitations/loops/break_simple.vpr b/tests/cases/passing/loops/break_simple.vpr similarity index 100% rename from tests/cases/known_limitations/loops/break_simple.vpr rename to tests/cases/passing/loops/break_simple.vpr diff --git a/tests/cases/known_limitations/loops/break_state.vpr b/tests/cases/passing/loops/break_state.vpr similarity index 100% rename from tests/cases/known_limitations/loops/break_state.vpr rename to tests/cases/passing/loops/break_state.vpr diff --git a/tests/cases/known_limitations/loops/frame_survives.vpr b/tests/cases/passing/loops/frame_survives.vpr similarity index 100% rename from tests/cases/known_limitations/loops/frame_survives.vpr rename to tests/cases/passing/loops/frame_survives.vpr diff --git a/tests/cases/known_limitations/loops/goto_loop.vpr b/tests/cases/passing/loops/goto_loop.vpr similarity index 100% rename from tests/cases/known_limitations/loops/goto_loop.vpr rename to tests/cases/passing/loops/goto_loop.vpr diff --git a/tests/cases/known_limitations/loops/list_walk.vpr b/tests/cases/passing/loops/list_walk.vpr similarity index 100% rename from tests/cases/known_limitations/loops/list_walk.vpr rename to tests/cases/passing/loops/list_walk.vpr diff --git a/tests/cases/known_limitations/loops/loop_under_if.vpr b/tests/cases/passing/loops/loop_under_if.vpr similarity index 100% rename from tests/cases/known_limitations/loops/loop_under_if.vpr rename to tests/cases/passing/loops/loop_under_if.vpr diff --git a/tests/cases/known_limitations/loops/nested.vpr b/tests/cases/passing/loops/nested.vpr similarity index 100% rename from tests/cases/known_limitations/loops/nested.vpr rename to tests/cases/passing/loops/nested.vpr diff --git a/tests/cases/known_limitations/loops/no_invariant.vpr b/tests/cases/passing/loops/no_invariant.vpr similarity index 100% rename from tests/cases/known_limitations/loops/no_invariant.vpr rename to tests/cases/passing/loops/no_invariant.vpr diff --git a/tests/cases/known_limitations/loops/scalar_sum.vpr b/tests/cases/passing/loops/scalar_sum.vpr similarity index 100% rename from tests/cases/known_limitations/loops/scalar_sum.vpr rename to tests/cases/passing/loops/scalar_sum.vpr diff --git a/tests/cases/known_limitations/loops/wildcard_ro.vpr b/tests/cases/passing/loops/wildcard_ro.vpr similarity index 100% rename from tests/cases/known_limitations/loops/wildcard_ro.vpr rename to tests/cases/passing/loops/wildcard_ro.vpr diff --git a/vendor/egg b/vendor/egg index fb616795..ce7881bf 160000 --- a/vendor/egg +++ b/vendor/egg @@ -1 +1 @@ -Subproject commit fb6167957beb5dd7c784121459e08ebd1ccb1a00 +Subproject commit ce7881bf8c36c3375ea2891d793e97fc226c93c6