From e0c9431ea122708d65a4752fa25eb046c434203d Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Thu, 22 Oct 2026 15:57:10 +0200 Subject: [PATCH 01/26] Add the z3 crate as a dependency Uses the gh-release build of Z3 and the num feature for arbitrary-precision integer and real literals. --- Cargo.lock | 1696 +++++++++++++++++++++++++++++++++++++++++++++++----- Cargo.toml | 1 + 2 files changed, 1547 insertions(+), 150 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 300d924..fd78818 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 deb6ff6..eedb4a9 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`. From 950464e444b8208c0cc4fdd7964100135b36a7f6 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Thu, 22 Oct 2026 14:09:54 +0200 Subject: [PATCH 02/26] Translate VMIR types to Z3 sorts Adds the verify::z3 module with a sort cache covering the builtin types, Option, field/predicate address sorts and ADTs. --- src/verify/mod.rs | 1 + src/verify/z3/mod.rs | 130 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 131 insertions(+) create mode 100644 src/verify/z3/mod.rs diff --git a/src/verify/mod.rs b/src/verify/mod.rs index cc8088b..29bf6cf 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/z3/mod.rs b/src/verify/z3/mod.rs new file mode 100644 index 0000000..9d3e7a8 --- /dev/null +++ b/src/verify/z3/mod.rs @@ -0,0 +1,130 @@ +use itertools::Itertools; +use crate::verify::lang::Symbolic; + +use z3::{DatatypeAccessor, DatatypeBuilder, DatatypeSort, Sort}; +use crate::verify::context::VerifyContext; +use crate::{vmir, HashMap, HashSet}; +use crate::vmir::Type; + + +#[derive(Default)] +pub(crate) struct Z3Sorts { + sorts: HashMap, + adts: HashMap, + // which adts we are currently building + building: HashSet, +} + +impl Z3Sorts { + pub(crate) fn option(&mut self, cx: &VerifyContext, ty: &Type, inner: &Type) -> &DatatypeSort { + if !self.adts.contains_key(ty) { + let inner_sort = self.sort(cx, inner); + let name = format!("adt@{ty}"); // `adt@Option` + let dt = DatatypeBuilder::new(name.as_str()) + .variant( + &format!("{name}.Some"), + vec![(&format!("{name}.Some.0"), DatatypeAccessor::sort(inner_sort))], + ) + .variant(&format!("{name}.None"), vec![]) + .finish(); + self.adts.insert(ty.clone(), dt); + } + &self.adts[ty] + } + pub(crate) fn sort(&mut self, cx: &VerifyContext, ty: &Type) -> Sort { + if let Some(s) = self.sorts.get(ty) { + return s.clone(); + } + 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 &cx.decls[*id] { + vmir::Declaration::Domain(d) => { + debug_assert!(args.is_empty(), "domains are monomorphic"); + Sort::uninterpreted(format!("dom@{}", cx.interner.resolve(&d.name)).into()) + } + vmir::Declaration::Adt(adt) => self.adt(cx, ty, adt, args).sort.clone(), + _ => unreachable!("Type::Domain must name a domain or an ADT"), + }, + Type::Snap(id) => { + let vmir::Declaration::Resource(r) = &cx.decls[*id] else { + unreachable!("Type::Snap must name a resource"); + }; + + Sort::uninterpreted(format!("snap@{}", cx.interner.resolve(&r.name)).into()) + }, + Type::Option(inner) => self.option(cx, ty, inner).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}", cx.groups.resolve(group)).into(), + ), + Type::Generic(_) => unreachable!("generics are substituted before reaching Z3"), + }; + self.sorts.insert(ty.clone(), sort.clone()); + sort + } + + pub(crate) fn adt( + &mut self, + cx: &VerifyContext, + ty: &Type, + adt: &vmir::Adt, + args: &[Type], + ) -> &DatatypeSort { + if !self.adts.contains_key(ty) { + self.building.insert(ty.clone()); + let base = format!("adt@{}", cx.interner.resolve(&adt.name)); + let name = if args.is_empty() { + base.to_string() + } else { + format!("{base}<{}>", args.iter().join(",")) + }; + let mut builder = DatatypeBuilder::new(name.as_str()); + for (v, variant) in adt.variants.iter().enumerate() { + let ctor = match variant.name { + Some(n) => format!("{name}.{}", cx.interner.resolve(&n)), + None => format!("{name}#{v}"), + }; + let mut acc_names = Vec::new(); + let mut accs = Vec::new(); + for (i, field) in variant.field_types.iter().enumerate() { + let field = field.subst_generics(args); + acc_names.push(format!("{ctor}.{i}")); + accs.push(if field == *ty { + // Self-reference: the sort doesn't exist yet, refer by name. + DatatypeAccessor::datatype(name.as_str()) + } else if self.building.contains(&field) { + todo!("mutually recursive ADTs need datatype_builder::create_datatypes") + } else { + DatatypeAccessor::sort(self.sort(cx, &field)) + }); + } + let fields = acc_names.iter().map(String::as_str).zip(accs).collect(); + builder = builder.variant(&ctor, fields); + } + self.building.swap_remove(ty); + self.adts.insert(ty.clone(), builder.finish()); + } + &self.adts[ty] + } +} +fn symbol_to_z3(context: &VerifyContext, symbol : &Symbolic) { + + match symbol { + Symbolic::Fresh(i) => { + let ty = context.fresh_types.get(i).expect("fresh type not found"); + + + + } + Symbolic::Lit(_) => {} + Symbolic::Binary(_, _) => {} + Symbolic::Ite(_) => {} + Symbolic::FuncApp(_, _, _) => {} + Symbolic::RealCast(_) => {} + Symbolic::Forall(_, _) => {} + } +} \ No newline at end of file From a8f763d177d8cdc43ec5e354aab8508236b9f129 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Thu, 22 Oct 2026 15:56:51 +0200 Subject: [PATCH 03/26] Classify verifier function ids with FuncKind FuncRegistry::kind tells whether a FuncId is a declared function, an ADT constructor/projection/tester, a limited twin or a precondition token, so the Z3 translation knows how to encode each application. This first version recovers the kind by searching the registry's maps. --- src/verify/func_registry.rs | 53 +++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/src/verify/func_registry.rs b/src/verify/func_registry.rs index 982dff2..384d9a3 100644 --- a/src/verify/func_registry.rs +++ b/src/verify/func_registry.rs @@ -28,6 +28,17 @@ 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 { @@ -381,6 +392,48 @@ impl FuncRegistry { .cloned() .unwrap_or_else(|| format!("d{}", adt.0)) } + + /// Inefficient way to lookup what kind of a function the FuncId is. + /// TODO: add a special lookup for this + pub fn kind(&self, f_id: FuncId) -> FuncKind { + // Check if they are functions belonging to builtin option type + match f_id { + BUILTIN_OPTION_SOME => return FuncKind::Cons { + head: BUILTIN_OPTION_HEAD, + variant: 0 + }, + BUILTIN_OPTION_NONE => return FuncKind::Cons { + head: BUILTIN_OPTION_HEAD, + variant: 1 + }, + BUILTIN_OPTION_VALUE => return FuncKind::Proj { head : BUILTIN_OPTION_HEAD, variant: 0, field: 0 }, + BUILTIN_OPTION_IS_SOME => return FuncKind::IsVariant { head : BUILTIN_OPTION_HEAD, variant: 0 }, + BUILTIN_OPTION_IS_NONE => return FuncKind::IsVariant { head : BUILTIN_OPTION_HEAD, variant: 1 }, + _ => {} + } + + // Check if it is an adt constructor + if let Some((&(head, variant), _)) = self.cons.iter().find(|&(_, &id)| id == f_id) { + return FuncKind::Cons { head, variant }; + } + // adt projection + if let Some((&(head, variant, field), _)) = self.proj.iter().find(|&(_, &id)| id == f_id) { + return FuncKind::Proj { head, variant, field }; + } + // adt tester + if let Some((&(head, variant), _)) = self.adt_is.iter().find(|&(_, &id)| id == f_id) { + return FuncKind::IsVariant { head, variant }; + } + // recursive (limited) + if let Some((&m, _)) = self.limited.iter().find(|&(_, &id)| id == f_id) { + return FuncKind::Limited(m); + } + // pre token + if let Some((&m, _)) = self.fn_pre_token.iter().find(|&(_, &id)| id == f_id) { + return FuncKind::PreToken(m); + } + FuncKind::Decl(MemberId(f_id.0)) + } } /// Derives the verifier `FuncId` for a plain, declaration-backed function. From 713865188abc0d86d1e34d0b5d2eb07d8bd02dfe Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Thu, 22 Oct 2026 16:32:36 +0200 Subject: [PATCH 04/26] Translate the e-graph to Z3 terms Every e-class becomes a Z3 constant of its exact type and every e-node one equation c_class == [node], covering literals (including big integers and reals), arithmetic, ite, casts and function applications. The translation is a set of free functions over VerifyContext, whose new z3translator field holds the sort and datatype caches, so the e-graph and the caches are never borrowed at the same time. --- src/verify/context/mod.rs | 5 + src/verify/z3/mod.rs | 513 ++++++++++++++++++++++++++++++-------- 2 files changed, 417 insertions(+), 101 deletions(-) diff --git a/src/verify/context/mod.rs b/src/verify/context/mod.rs index 9e4e813..245116b 100644 --- a/src/verify/context/mod.rs +++ b/src/verify/context/mod.rs @@ -16,6 +16,7 @@ use crate::{ }; use lasso::{Rodeo, Spur}; use typed_index_collections::TiVec; +use crate::verify::z3::Z3Translation; /// Display name for a member id, off a bare `(interner, decls)` pair — the same /// resolution [`VerifyContext::member_name`] does, callable where only the two @@ -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/z3/mod.rs b/src/verify/z3/mod.rs index 9d3e7a8..218b941 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -1,130 +1,441 @@ use itertools::Itertools; -use crate::verify::lang::Symbolic; +use crate::verify::lang::{FuncId, Symbolic}; -use z3::{DatatypeAccessor, DatatypeBuilder, DatatypeSort, Sort}; +use z3::{DatatypeAccessor, DatatypeBuilder, DatatypeSort, FuncDecl, Sort}; +use z3::ast::{Ast, Bool, Dynamic, Int}; use crate::verify::context::VerifyContext; use crate::{vmir, HashMap, HashSet}; -use crate::vmir::Type; - +use crate::vmir::{BinOp, Literal, MemberId, Type}; +use crate::verify::func_registry::{FuncKind, BUILTIN_OPTION_NONE, BUILTIN_OPTION_SOME, BUILTIN_OPTION_IS_SOME, BUILTIN_OPTION_IS_NONE, BUILTIN_OPTION_VALUE, BUILTIN_OPTION_HEAD}; +use egg::Id; +/// 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. #[derive(Default)] -pub(crate) struct Z3Sorts { +pub(crate) struct Z3Translation { sorts: HashMap, adts: HashMap, // which adts we are currently building building: HashSet, } -impl Z3Sorts { - pub(crate) fn option(&mut self, cx: &VerifyContext, ty: &Type, inner: &Type) -> &DatatypeSort { - if !self.adts.contains_key(ty) { - let inner_sort = self.sort(cx, inner); - let name = format!("adt@{ty}"); // `adt@Option` - let dt = DatatypeBuilder::new(name.as_str()) - .variant( - &format!("{name}.Some"), - vec![(&format!("{name}.Some.0"), DatatypeAccessor::sort(inner_sort))], - ) - .variant(&format!("{name}.None"), vec![]) - .finish(); - self.adts.insert(ty.clone(), dt); +/// 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) { + let vmir::Declaration::Function(fun) = &ctxt.decls[func] else { + unreachable!("FuncApp of declaration {} that is not a function", func.0); + }; + let params = fun.params.iter().map(|t| t.subst_generics(tys)).collect(); + (params, fun.ret.subst_generics(tys)) +} + +/// The type of e-class `id` (translation.typ, "Class sorts"). Exact or a panic: +/// every node whose type is certain must agree, and at least one must exist. +/// Unlike `types::infer_type` this never guesses. +fn class_type(ctxt: &VerifyContext, id: Id) -> Type { + let mut memo = crate::dhash::HashMap::default(); + exact_class_type(ctxt, id, &mut memo) + .unwrap_or_else(|| panic!("e-class {id} has no node with a certain type")) +} + +/// `None` when no node of the class has a certain type. `memo` maps a class to +/// its result; `None` is pre-seeded so an `Ite` cycle back into a class still +/// being resolved counts as uncertain rather than looping. +fn exact_class_type( + ctxt: &VerifyContext, + id: Id, + memo: &mut crate::dhash::HashMap>, +) -> Option { + let id = ctxt.egraph.find(id); + if let Some(ty) = memo.get(&id) { + return ty.clone(); + } + memo.insert(id, None); + let mut found: Option = None; + for node in &ctxt.egraph[id].nodes { + let Some(ty) = exact_node_type(ctxt, node, memo) else { + continue; + }; + match &found { + None => found = Some(ty), + Some(prev) if *prev == ty => {} + Some(prev) => panic!("e-class {id} mixes types {prev} and {ty}"), } - &self.adts[ty] } - pub(crate) fn sort(&mut self, cx: &VerifyContext, ty: &Type) -> Sort { - if let Some(s) = self.sorts.get(ty) { - return s.clone(); + memo.insert(id, found.clone()); + found +} + +/// The type of one e-node, or `None` when it is not certain. +fn exact_node_type( + ctxt: &VerifyContext, + node: &Symbolic, + memo: &mut crate::dhash::HashMap>, +) -> 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([_, then, _]) => exact_class_type(ctxt, *then, memo), + Symbolic::FuncApp(f, tys, _) => match *f { + BUILTIN_OPTION_SOME | BUILTIN_OPTION_NONE => Some(Type::Option(Box::new(tys[0].clone()))), + BUILTIN_OPTION_VALUE => Some(tys[0].clone()), + BUILTIN_OPTION_IS_SOME | BUILTIN_OPTION_IS_NONE => Some(Type::Bool), + // The return type is a function of `(f, tys)`. With no type + // arguments `f` has exactly one instantiation, so the type + // `func_ret_types` recorded for it is the right one. With type + // arguments it may be another instantiation's: uncertain. + _ if tys.is_empty() => ctxt.func_ret_types.get(f).cloned(), + _ => None, + }, + } +} + +/// One equation `c_{class} == ⟦node⟧` per e-node (translation.typ, "The e-graph"). +pub(crate) fn build_facts(ctxt: &mut VerifyContext) -> Vec { + // Snapshot the classes first: translating needs `ctxt` mutably (the sort + // cache), so the e-graph cannot stay borrowed while we iterate it. + let classes: Vec<(Id, Vec)> = ctxt + .egraph + .classes() + .map(|class| (class.id, class.nodes.clone())) + .collect(); + let mut facts = Vec::new(); + for (id, nodes) in classes { + let class_const = class_const(ctxt, id); + // A `Forall` gets no equation: its class constant stays a free + // `Bool`, and its instances are already in the e-graph as + // `ite(forall, body, true) == true` (translation.typ, "The e-graph"). + for node in nodes.iter().filter(|node| !matches!(node, Symbolic::Forall(..))) { + let node_expression = symbol_to_z3(ctxt, node); + facts.push(class_const.eq(node_expression)); } - 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 &cx.decls[*id] { - vmir::Declaration::Domain(d) => { - debug_assert!(args.is_empty(), "domains are monomorphic"); - Sort::uninterpreted(format!("dom@{}", cx.interner.resolve(&d.name)).into()) - } - vmir::Declaration::Adt(adt) => self.adt(cx, ty, adt, args).sort.clone(), - _ => unreachable!("Type::Domain must name a domain or an ADT"), - }, - Type::Snap(id) => { - let vmir::Declaration::Resource(r) = &cx.decls[*id] else { - unreachable!("Type::Snap must name a resource"); - }; - - Sort::uninterpreted(format!("snap@{}", cx.interner.resolve(&r.name)).into()) - }, - Type::Option(inner) => self.option(cx, ty, inner).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}", cx.groups.resolve(group)).into(), - ), - Type::Generic(_) => unreachable!("generics are substituted before reaching Z3"), - }; - self.sorts.insert(ty.clone(), sort.clone()); - sort } + facts +} - pub(crate) fn adt( - &mut self, - cx: &VerifyContext, - ty: &Type, - adt: &vmir::Adt, - args: &[Type], - ) -> &DatatypeSort { - if !self.adts.contains_key(ty) { - self.building.insert(ty.clone()); - let base = format!("adt@{}", cx.interner.resolve(&adt.name)); - let name = if args.is_empty() { - base.to_string() - } else { - format!("{base}<{}>", args.iter().join(",")) +pub(crate) fn option<'c>(ctxt: &'c mut VerifyContext, ty: &Type, inner: &Type) -> &'c DatatypeSort { + if !ctxt.z3translator.adts.contains_key(ty) { + let inner_sort = sort(ctxt, inner); + let name = format!("adt@{ty}"); // `adt@Option` + let dt = DatatypeBuilder::new(name.as_str()) + .variant( + &format!("{name}.Some"), + vec![(&format!("{name}.Some.0"), DatatypeAccessor::sort(inner_sort))], + ) + .variant(&format!("{name}.None"), vec![]) + .finish(); + ctxt.z3translator.adts.insert(ty.clone(), dt); + } + &ctxt.z3translator.adts[ty] +} + +fn class_const_given_sort(ctxt: &VerifyContext, id: Id, sort: &Sort) -> Dynamic { + Dynamic::new_const(format!("c_{}", ctxt.egraph.find(id)), sort) +} + +fn class_const(ctxt: &mut VerifyContext, id: Id) -> Dynamic { + let typ = class_type(ctxt, id); + let sort = sort(ctxt, &typ); + 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(a) => adt(ctxt, ty, a, args).sort.clone(), + _ => unreachable!("Type::Domain must name a domain or an ADT"), + }, + Type::Snap(id) => { + let vmir::Declaration::Resource(r) = &decls[*id] else { + unreachable!("Type::Snap must name a resource"); }; - let mut builder = DatatypeBuilder::new(name.as_str()); - for (v, variant) in adt.variants.iter().enumerate() { - let ctor = match variant.name { - Some(n) => format!("{name}.{}", cx.interner.resolve(&n)), - None => format!("{name}#{v}"), - }; - let mut acc_names = Vec::new(); - let mut accs = Vec::new(); - for (i, field) in variant.field_types.iter().enumerate() { - let field = field.subst_generics(args); - acc_names.push(format!("{ctor}.{i}")); - accs.push(if field == *ty { - // Self-reference: the sort doesn't exist yet, refer by name. - DatatypeAccessor::datatype(name.as_str()) - } else if self.building.contains(&field) { - todo!("mutually recursive ADTs need datatype_builder::create_datatypes") - } else { - DatatypeAccessor::sort(self.sort(cx, &field)) - }); + + Sort::uninterpreted(format!("snap@{}", interner.resolve(&r.name)).into()) + }, + Type::Option(inner) => option(ctxt, ty, inner).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 substituted before reaching Z3"), + }; + ctxt.z3translator.sorts.insert(ty.clone(), sort.clone()); + sort +} + +fn symbol_to_z3(ctxt: &mut VerifyContext, symbol: &Symbolic) -> Dynamic { + match symbol { + Symbolic::Fresh(i) => { + let ty = ctxt.fresh_types.get(i).expect("fresh type not found").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]) => { + let operand_ty = op.sort().unwrap_or_else(|| class_type(ctxt, *l)); + 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!(), + } + } + 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!(), + } } - let fields = acc_names.iter().map(String::as_str).zip(accs).collect(); - builder = builder.variant(&ctor, fields); } - self.building.swap_remove(ty); - self.adts.insert(ty.clone(), builder.finish()); } - &self.adts[ty] + Symbolic::Ite([cond, then, els]) => { + let then_ty = class_type(ctxt, *then); + 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 ty = class_type(ctxt, *id); + let sort = sort(ctxt, &ty); + let class = class_const_given_sort(ctxt, *id, &sort).as_int().unwrap(); + class.to_real().into() + }, + Symbolic::Forall(_, _) => todo!(), } } -fn symbol_to_z3(context: &VerifyContext, symbol : &Symbolic) { - match symbol { - Symbolic::Fresh(i) => { - let ty = context.fresh_types.get(i).expect("fresh type not found"); +// 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 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 arg_refs: Vec<&dyn Ast> = arg_consts.iter().map(|a| a as &dyn Ast).collect(); + FuncDecl::new(name, &domain_refs, &range).apply(&arg_refs) +} + +fn translate_function(ctxt: &mut VerifyContext, f_id: &FuncId, ty: &Box<[Type]>, args: &Box<[Id]>) -> Dynamic { + + let function_type = ctxt.alloc.kind(*f_id); + + match function_type { + // A function, a domain function, or a field/predicate address + // 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); + // Snapshots use the uninterpreted encoding (translation.typ, + // "ADTs and snapshots"); ADTs and Option are datatypes. + if let Type::Snap(_) = adt_ty { + uninterpreted_app(ctxt, *f_id, ty, &field_tys, &adt_ty, args) + } else { + 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); + // TODO: bad performance building the whole vec for nothing + let field_ty = field_types(ctxt, head, variant, ty).swap_remove(field); + // Snapshots use the uninterpreted encoding (translation.typ, + // "ADTs and snapshots"); ADTs and Option are datatypes. + if let Type::Snap(_) = adt_ty { + uninterpreted_app(ctxt, *f_id, ty, &[adt_ty.clone()], &field_ty, args) + } else { + 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?` + FuncKind::IsVariant { + head, + variant + } => { + let adt_ty = adt_type(ctxt, head, ty); + if let Type::Snap(_) = adt_ty { + // Snapshot: uninterpreted tester, `snap -> Bool`. + uninterpreted_app(ctxt, *f_id, ty, &[adt_ty.clone()], &Type::Bool, args) + } else { + 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) + }, + } +} + +pub(crate) fn adt<'c>( + ctxt: &'c mut VerifyContext, + ty: &Type, + adt: &vmir::Adt, + args: &[Type], +) -> &'c DatatypeSort { + if !ctxt.z3translator.adts.contains_key(ty) { + ctxt.z3translator.building.insert(ty.clone()); + let base = format!("adt@{}", ctxt.interner.resolve(&adt.name)); + let name = if args.is_empty() { + base.to_string() + } else { + format!("{base}<{}>", args.iter().join(",")) + }; + let mut builder = DatatypeBuilder::new(name.as_str()); + for (v, variant) in adt.variants.iter().enumerate() { + let ctor = match variant.name { + Some(n) => format!("{name}.{}", ctxt.interner.resolve(&n)), + None => format!("{name}#{v}"), + }; + let mut acc_names = Vec::new(); + let mut accs = Vec::new(); + for (i, field) in variant.field_types.iter().enumerate() { + let field = field.subst_generics(args); + acc_names.push(format!("{ctor}.{i}")); + accs.push(if field == *ty { + // Self-reference: the sort doesn't exist yet, refer by name. + DatatypeAccessor::datatype(name.as_str()) + } else if ctxt.z3translator.building.contains(&field) { + todo!("mutually recursive ADTs need datatype_builder::create_datatypes") + } else { + DatatypeAccessor::sort(sort(ctxt, &field)) + }); + } + let fields = acc_names.iter().map(String::as_str).zip(accs).collect(); + builder = builder.variant(&ctor, fields); } - Symbolic::Lit(_) => {} - Symbolic::Binary(_, _) => {} - Symbolic::Ite(_) => {} - Symbolic::FuncApp(_, _, _) => {} - Symbolic::RealCast(_) => {} - Symbolic::Forall(_, _) => {} + ctxt.z3translator.building.swap_remove(ty); + ctxt.z3translator.adts.insert(ty.clone(), builder.finish()); } -} \ No newline at end of file + &ctxt.z3translator.adts[ty] +} From d58da77d81f6dda6061233dc8525f593a482d13d Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Thu, 22 Oct 2026 16:49:47 +0200 Subject: [PATCH 05/26] Try Z3 as the last prover rung prove_by_z3 asserts the e-graph facts and the full path condition (block cube plus the instruction's literals) and checks the negated goal; unsat proves it. It runs only after every e-graph tier has failed, and only when SILVER_OXIDE_Z3 is set. --- src/verify/context/mod.rs | 4 ++++ src/verify/context/prove.rs | 48 +++++++++++++++++++++++++++++++++---- src/verify/z3/mod.rs | 18 +++++++++++++- 3 files changed, 64 insertions(+), 6 deletions(-) diff --git a/src/verify/context/mod.rs b/src/verify/context/mod.rs index 245116b..d335874 100644 --- a/src/verify/context/mod.rs +++ b/src/verify/context/mod.rs @@ -105,6 +105,9 @@ pub(crate) struct VerifyContext<'a> { /// where the set memoizes the *verdict* alone. Empty-pc goals still union /// (productive: `eq-true-union`/congruence off a proven `Eq`). oob_memo: bool, + /// `SILVER_OXIDE_Z3`: run the Z3 rung (`prove_by_z3`) when every e-graph + /// tier has failed. Off by default. + use_z3: bool, /// Canonical class ids of implications already proven `true`, consulted at /// the `memo` tier when `oob_memo` is on. Keyed by `egraph.find(imp)`: two distinct /// obligations only share a class via congruence — which means their goals @@ -199,6 +202,7 @@ impl<'a> VerifyContext<'a> { clean: None, has_wildcard: decls_have_wildcard(decls), oob_memo: std::env::var_os("SILVER_OXIDE_OOB_MEMO").is_some(), + use_z3: std::env::var_os("SILVER_OXIDE_Z3").is_some(), proven_imps: crate::dhash::HashSet::default(), current_cube: Vec::new(), in_block: false, diff --git a/src/verify/context/prove.rs b/src/verify/context/prove.rs index e3990e1..83aa2d0 100644 --- a/src/verify/context/prove.rs +++ b/src/verify/context/prove.rs @@ -12,7 +12,7 @@ use crate::dhash::HashMap; use egg::Language as _; - +use z3::SatResult; use crate::{ verify::{ analysis::ConstFold, @@ -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,40 @@ impl<'a> VerifyContext<'a> { } } + + fn prove_by_z3( + &mut self, + goal: egg::Id, + pc_lits: &[(egg::Id, Polarity)], + ) -> bool { + if !self.use_z3 { + return false; + } + let solver = z3::Solver::new(); + + let facts = crate::verify::z3::build_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); + + facts.iter().for_each(|fact| solver.assert(fact)); + pc_cond.iter().for_each(|pc_cond| solver.assert(pc_cond)); + + solver.assert(!goal_z3); + + let res = solver.check(); + + 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) diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index 218b941..3513c00 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -1,3 +1,4 @@ +use std::process::id; use itertools::Itertools; use crate::verify::lang::{FuncId, Symbolic}; @@ -5,7 +6,7 @@ use z3::{DatatypeAccessor, DatatypeBuilder, DatatypeSort, FuncDecl, Sort}; use z3::ast::{Ast, Bool, Dynamic, Int}; use crate::verify::context::VerifyContext; use crate::{vmir, HashMap, HashSet}; -use crate::vmir::{BinOp, Literal, MemberId, Type}; +use crate::vmir::{BinOp, Literal, MemberId, Polarity, Type}; use crate::verify::func_registry::{FuncKind, BUILTIN_OPTION_NONE, BUILTIN_OPTION_SOME, BUILTIN_OPTION_IS_SOME, BUILTIN_OPTION_IS_NONE, BUILTIN_OPTION_VALUE, BUILTIN_OPTION_HEAD}; use egg::Id; @@ -122,6 +123,21 @@ pub(crate) fn build_facts(ctxt: &mut VerifyContext) -> Vec { facts } +pub(crate) fn build_goal(ctxt: &mut VerifyContext, id: egg::Id) -> Bool { + let node = ctxt.egraph.find(id); + class_const(ctxt, node).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(ctxt, *id); + match p { + Polarity::Positive => c_const.as_bool().unwrap(), + Polarity::Negative => !c_const.as_bool().unwrap(), + } + }).collect() +} + pub(crate) fn option<'c>(ctxt: &'c mut VerifyContext, ty: &Type, inner: &Type) -> &'c DatatypeSort { if !ctxt.z3translator.adts.contains_key(ty) { let inner_sort = sort(ctxt, inner); From 68514c1652e68bfdee3feaa5acbe75a2a09ee261 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Mon, 26 Oct 2026 14:42:57 +0100 Subject: [PATCH 06/26] Encode ADTs, snapshots and Option as Z3 datatypes Datatypes are declared on first use, together with every undeclared datatype reachable through their fields in a single create_datatypes call, so recursive and mutually recursive datatypes resolve by name. Constructors and projections translate to the datatype's own constructor and accessor functions, and the per-kind function translation moves into translate_function. --- src/verify/z3/mod.rs | 392 ++++++++++++++++++++++++++----------------- 1 file changed, 236 insertions(+), 156 deletions(-) diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index 3513c00..d83aeea 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -1,14 +1,17 @@ -use std::process::id; -use itertools::Itertools; use crate::verify::lang::{FuncId, Symbolic}; +use itertools::Itertools; -use z3::{DatatypeAccessor, DatatypeBuilder, DatatypeSort, FuncDecl, Sort}; -use z3::ast::{Ast, Bool, Dynamic, Int}; use crate::verify::context::VerifyContext; -use crate::{vmir, HashMap, HashSet}; +use crate::verify::func_registry::{ + BUILTIN_OPTION_HEAD, FuncKind, +}; use crate::vmir::{BinOp, Literal, MemberId, Polarity, Type}; -use crate::verify::func_registry::{FuncKind, BUILTIN_OPTION_NONE, BUILTIN_OPTION_SOME, BUILTIN_OPTION_IS_SOME, BUILTIN_OPTION_IS_NONE, BUILTIN_OPTION_VALUE, BUILTIN_OPTION_HEAD}; +use crate::{HashMap, vmir}; use egg::Id; +use std::borrow::Cow; +use z3::ast::{Ast, Bool, Dynamic, Int}; +use z3::datatype_builder::create_datatypes; +use z3::{DatatypeAccessor, DatatypeBuilder, DatatypeSort, FuncDecl, Sort}; /// The translator's caches, kept in `VerifyContext::z3translator` so sorts and /// datatypes are created once per context. The translation itself is the free @@ -17,19 +20,39 @@ use egg::Id; pub(crate) struct Z3Translation { sorts: HashMap, adts: HashMap, - // which adts we are currently building - building: HashSet, } /// 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) { - let vmir::Declaration::Function(fun) = &ctxt.decls[func] else { - unreachable!("FuncApp of declaration {} that is not a function", func.0); - }; - let params = fun.params.iter().map(|t| t.subst_generics(tys)).collect(); - (params, fun.ret.subst_generics(tys)) + 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"). Exact or a panic: @@ -86,16 +109,16 @@ fn exact_node_type( Symbolic::RealCast(_) => Some(Type::Real), Symbolic::Forall(..) => Some(Type::Bool), Symbolic::Ite([_, then, _]) => exact_class_type(ctxt, *then, memo), - Symbolic::FuncApp(f, tys, _) => match *f { - BUILTIN_OPTION_SOME | BUILTIN_OPTION_NONE => Some(Type::Option(Box::new(tys[0].clone()))), - BUILTIN_OPTION_VALUE => Some(tys[0].clone()), - BUILTIN_OPTION_IS_SOME | BUILTIN_OPTION_IS_NONE => Some(Type::Bool), - // The return type is a function of `(f, tys)`. With no type - // arguments `f` has exactly one instantiation, so the type - // `func_ret_types` recorded for it is the right one. With type - // arguments it may be another instantiation's: uncertain. - _ if tys.is_empty() => ctxt.func_ret_types.get(f).cloned(), - _ => 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), }, } } @@ -115,7 +138,10 @@ pub(crate) fn build_facts(ctxt: &mut VerifyContext) -> Vec { // A `Forall` gets no equation: its class constant stays a free // `Bool`, and its instances are already in the e-graph as // `ite(forall, body, true) == true` (translation.typ, "The e-graph"). - for node in nodes.iter().filter(|node| !matches!(node, Symbolic::Forall(..))) { + for node in nodes + .iter() + .filter(|node| !matches!(node, Symbolic::Forall(..))) + { let node_expression = symbol_to_z3(ctxt, node); facts.push(class_const.eq(node_expression)); } @@ -129,29 +155,15 @@ pub(crate) fn build_goal(ctxt: &mut VerifyContext, id: egg::Id) -> Bool { } pub(crate) fn build_pc(ctxt: &mut VerifyContext, pc: &[(egg::Id, Polarity)]) -> Vec { - pc.iter().map(|(id, p)| { - let c_const = class_const(ctxt, *id); - match p { - Polarity::Positive => c_const.as_bool().unwrap(), - Polarity::Negative => !c_const.as_bool().unwrap(), - } - }).collect() -} - -pub(crate) fn option<'c>(ctxt: &'c mut VerifyContext, ty: &Type, inner: &Type) -> &'c DatatypeSort { - if !ctxt.z3translator.adts.contains_key(ty) { - let inner_sort = sort(ctxt, inner); - let name = format!("adt@{ty}"); // `adt@Option` - let dt = DatatypeBuilder::new(name.as_str()) - .variant( - &format!("{name}.Some"), - vec![(&format!("{name}.Some.0"), DatatypeAccessor::sort(inner_sort))], - ) - .variant(&format!("{name}.None"), vec![]) - .finish(); - ctxt.z3translator.adts.insert(ty.clone(), dt); - } - &ctxt.z3translator.adts[ty] + pc.iter() + .map(|(id, p)| { + let c_const = class_const(ctxt, *id); + match p { + Polarity::Positive => c_const.as_bool().unwrap(), + Polarity::Negative => !c_const.as_bool().unwrap(), + } + }) + .collect() } fn class_const_given_sort(ctxt: &VerifyContext, id: Id, sort: &Sort) -> Dynamic { @@ -181,23 +193,16 @@ pub(crate) fn sort(ctxt: &mut VerifyContext, ty: &Type) -> Sort { debug_assert!(args.is_empty(), "domains are monomorphic"); Sort::uninterpreted(format!("dom@{}", interner.resolve(&d.name)).into()) } - vmir::Declaration::Adt(a) => adt(ctxt, ty, a, args).sort.clone(), + vmir::Declaration::Adt(_) => datatype(ctxt, ty).sort.clone(), _ => unreachable!("Type::Domain must name a domain or an ADT"), }, - Type::Snap(id) => { - let vmir::Declaration::Resource(r) = &decls[*id] else { - unreachable!("Type::Snap must name a resource"); - }; - - Sort::uninterpreted(format!("snap@{}", interner.resolve(&r.name)).into()) - }, - Type::Option(inner) => option(ctxt, ty, inner).sort.clone(), + 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 substituted before reaching Z3"), + 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 @@ -206,7 +211,11 @@ pub(crate) fn sort(ctxt: &mut VerifyContext, ty: &Type) -> Sort { fn symbol_to_z3(ctxt: &mut VerifyContext, symbol: &Symbolic) -> Dynamic { match symbol { Symbolic::Fresh(i) => { - let ty = ctxt.fresh_types.get(i).expect("fresh type not found").clone(); + let ty = ctxt + .fresh_types + .get(i) + .expect("fresh type not found") + .clone(); Dynamic::new_const(format!("fresh{i}"), &sort(ctxt, &ty)) } Symbolic::Lit(literal) => match literal { @@ -231,7 +240,7 @@ fn symbol_to_z3(ctxt: &mut VerifyContext, symbol: &Symbolic) -> Dynamic { BinOp::DivI => l.div(&r).into(), BinOp::Mod => l.modulo(&r).into(), BinOp::LtI => l.lt(&r).into(), - _ => unreachable!(), + _ => unreachable!("excluded by outer matching"), } } BinOp::AddR | BinOp::SubR | BinOp::MulR | BinOp::DivR | BinOp::LtR => { @@ -242,7 +251,7 @@ fn symbol_to_z3(ctxt: &mut VerifyContext, symbol: &Symbolic) -> Dynamic { BinOp::MulR => (l * r).into(), BinOp::DivR => l.div(&r).into(), BinOp::LtR => l.lt(&r).into(), - _ => unreachable!(), + _ => unreachable!("excluded by outer matching"), } } } @@ -250,39 +259,44 @@ fn symbol_to_z3(ctxt: &mut VerifyContext, symbol: &Symbolic) -> Dynamic { Symbolic::Ite([cond, then, els]) => { let then_ty = class_type(ctxt, *then); let sort = sort(ctxt, &then_ty); - let cond = class_const_given_sort(ctxt, *cond, &Sort::bool()).as_bool().unwrap(); + 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 ty = class_type(ctxt, *id); let sort = sort(ctxt, &ty); let class = class_const_given_sort(ctxt, *id, &sort).as_int().unwrap(); class.to_real().into() - }, - Symbolic::Forall(_, _) => todo!(), + } + 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())) + 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") + _ => 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 + return if variant == 0 { + vec![tys[0].clone()] + } else { + vec![] + }; // Some(T) / None } match &ctxt.decls[head] { vmir::Declaration::Adt(adt) => adt.variants[variant] @@ -311,7 +325,12 @@ fn uninterpreted_app( ret: &Type, args: &[Id], ) -> Dynamic { - assert_eq!(params.len(), args.len(), "arity mismatch applying fn{}", f.0); + 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() @@ -329,129 +348,190 @@ fn uninterpreted_app( FuncDecl::new(name, &domain_refs, &range).apply(&arg_refs) } -fn translate_function(ctxt: &mut VerifyContext, f_id: &FuncId, ty: &Box<[Type]>, args: &Box<[Id]>) -> Dynamic { - +fn translate_function( + ctxt: &mut VerifyContext, + f_id: &FuncId, + ty: &Box<[Type]>, + args: &Box<[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 - } => { + FuncKind::Cons { variant, head } => { let adt_ty = adt_type(ctxt, head, ty); let field_tys = field_types(ctxt, head, variant, ty); - - // Snapshots use the uninterpreted encoding (translation.typ, - // "ADTs and snapshots"); ADTs and Option are datatypes. - if let Type::Snap(_) = adt_ty { - uninterpreted_app(ctxt, *f_id, ty, &field_tys, &adt_ty, args) - } else { - let fields = args.iter().zip(&field_tys).map(|(arg, ty)| { + let fields = args + .iter() + .zip(&field_tys) + .map(|(arg, ty)| { let s = sort(ctxt, ty); class_const_given_sort(ctxt, *arg, &s) - }).collect::>(); + }) + .collect::>(); - let field_refs = fields.iter().map(|f| f as &dyn Ast).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) - } - }, + 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 + field, } => { let adt_ty = adt_type(ctxt, head, ty); - // TODO: bad performance building the whole vec for nothing - let field_ty = field_types(ctxt, head, variant, ty).swap_remove(field); - - // Snapshots use the uninterpreted encoding (translation.typ, - // "ADTs and snapshots"); ADTs and Option are datatypes. - if let Type::Snap(_) = adt_ty { - uninterpreted_app(ctxt, *f_id, ty, &[adt_ty.clone()], &field_ty, args) - } else { - 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?` - FuncKind::IsVariant { - head, - variant - } => { + 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); - if let Type::Snap(_) = adt_ty { - // Snapshot: uninterpreted tester, `snap -> Bool`. - uninterpreted_app(ctxt, *f_id, ty, &[adt_ty.clone()], &Type::Bool, args) - } else { - 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]) - } - }, + 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 }) } -pub(crate) fn adt<'c>( - ctxt: &'c mut VerifyContext, - ty: &Type, - adt: &vmir::Adt, - args: &[Type], -) -> &'c DatatypeSort { +/// 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) { - ctxt.z3translator.building.insert(ty.clone()); - let base = format!("adt@{}", ctxt.interner.resolve(&adt.name)); - let name = if args.is_empty() { - base.to_string() - } else { - format!("{base}<{}>", args.iter().join(",")) + 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; }; - let mut builder = DatatypeBuilder::new(name.as_str()); - for (v, variant) in adt.variants.iter().enumerate() { - let ctor = match variant.name { - Some(n) => format!("{name}.{}", ctxt.interner.resolve(&n)), - None => format!("{name}#{v}"), - }; - let mut acc_names = Vec::new(); + 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 (i, field) in variant.field_types.iter().enumerate() { - let field = field.subst_generics(args); - acc_names.push(format!("{ctor}.{i}")); - accs.push(if field == *ty { - // Self-reference: the sort doesn't exist yet, refer by name. - DatatypeAccessor::datatype(name.as_str()) - } else if ctxt.z3translator.building.contains(&field) { - todo!("mutually recursive ADTs need datatype_builder::create_datatypes") - } else { - DatatypeAccessor::sort(sort(ctxt, &field)) - }); + 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)), + }, + )); } - let fields = acc_names.iter().map(String::as_str).zip(accs).collect(); - builder = builder.variant(&ctor, fields); + builder = builder.variant(ctor, accs); } - ctxt.z3translator.building.swap_remove(ty); - ctxt.z3translator.adts.insert(ty.clone(), builder.finish()); + 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); } - &ctxt.z3translator.adts[ty] } From 12b9240e8cf734fdcba03bc0fa0608a84d473008 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Tue, 27 Oct 2026 12:44:12 +0100 Subject: [PATCH 07/26] Store FuncKind per id when minting it FuncRegistry now records each id's kind as it mints it, so kind() is a map lookup instead of a search over every registry map. FuncRegistry::new now builds on empty(), so the builtin Option ids, names and rules are defined once. --- src/verify/context/mod.rs | 6 +- src/verify/context/prove.rs | 13 +-- src/verify/func_registry.rs | 172 +++++++++++++++++++----------------- src/verify/z3/mod.rs | 16 ++-- 4 files changed, 107 insertions(+), 100 deletions(-) diff --git a/src/verify/context/mod.rs b/src/verify/context/mod.rs index d335874..28f17f0 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, @@ -16,7 +17,6 @@ use crate::{ }; use lasso::{Rodeo, Spur}; use typed_index_collections::TiVec; -use crate::verify::z3::Z3Translation; /// Display name for a member id, off a bare `(interner, decls)` pair — the same /// resolution [`VerifyContext::member_name`] does, callable where only the two @@ -135,7 +135,7 @@ pub(crate) struct VerifyContext<'a> { block_dead: bool, /// Sort and datatype caches of the Z3 translation (`verify::z3`). - pub(crate) z3translator: Z3Translation + pub(crate) z3translator: Z3Translation, } /// Whether any declaration uses a `wildcard` permission. Scanned once per unit at @@ -208,7 +208,7 @@ impl<'a> VerifyContext<'a> { in_block: false, scratch: None, block_dead: false, - z3translator : Z3Translation::default() + z3translator: Z3Translation::default(), } } diff --git a/src/verify/context/prove.rs b/src/verify/context/prove.rs index 83aa2d0..7c6f9ff 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 z3::SatResult; 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 @@ -836,12 +836,7 @@ impl<'a> VerifyContext<'a> { } } - - fn prove_by_z3( - &mut self, - goal: egg::Id, - pc_lits: &[(egg::Id, Polarity)], - ) -> bool { + fn prove_by_z3(&mut self, goal: egg::Id, pc_lits: &[(egg::Id, Polarity)]) -> bool { if !self.use_z3 { return false; } @@ -866,7 +861,7 @@ impl<'a> VerifyContext<'a> { match res { SatResult::Unsat => true, SatResult::Unknown => false, - SatResult::Sat => false + SatResult::Sat => false, } } diff --git a/src/verify/func_registry.rs b/src/verify/func_registry.rs index 384d9a3..94f4982 100644 --- a/src/verify/func_registry.rs +++ b/src/verify/func_registry.rs @@ -31,20 +31,33 @@ 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 }, + 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 @@ -142,36 +155,12 @@ 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() }; // Mint every head up front. Lazily minting on first use would leave // `ctor_head` incomplete for any `ConstFold` built before that use, and @@ -193,36 +182,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(), } } @@ -258,7 +293,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 } @@ -273,7 +308,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 } @@ -344,10 +379,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); @@ -356,7 +394,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)); } @@ -377,10 +422,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 } @@ -393,46 +439,12 @@ impl FuncRegistry { .unwrap_or_else(|| format!("d{}", adt.0)) } - /// Inefficient way to lookup what kind of a function the FuncId is. - /// TODO: add a special lookup for this - pub fn kind(&self, f_id: FuncId) -> FuncKind { - // Check if they are functions belonging to builtin option type - match f_id { - BUILTIN_OPTION_SOME => return FuncKind::Cons { - head: BUILTIN_OPTION_HEAD, - variant: 0 - }, - BUILTIN_OPTION_NONE => return FuncKind::Cons { - head: BUILTIN_OPTION_HEAD, - variant: 1 - }, - BUILTIN_OPTION_VALUE => return FuncKind::Proj { head : BUILTIN_OPTION_HEAD, variant: 0, field: 0 }, - BUILTIN_OPTION_IS_SOME => return FuncKind::IsVariant { head : BUILTIN_OPTION_HEAD, variant: 0 }, - BUILTIN_OPTION_IS_NONE => return FuncKind::IsVariant { head : BUILTIN_OPTION_HEAD, variant: 1 }, - _ => {} - } - - // Check if it is an adt constructor - if let Some((&(head, variant), _)) = self.cons.iter().find(|&(_, &id)| id == f_id) { - return FuncKind::Cons { head, variant }; - } - // adt projection - if let Some((&(head, variant, field), _)) = self.proj.iter().find(|&(_, &id)| id == f_id) { - return FuncKind::Proj { head, variant, field }; - } - // adt tester - if let Some((&(head, variant), _)) = self.adt_is.iter().find(|&(_, &id)| id == f_id) { - return FuncKind::IsVariant { head, variant }; - } - // recursive (limited) - if let Some((&m, _)) = self.limited.iter().find(|&(_, &id)| id == f_id) { - return FuncKind::Limited(m); - } - // pre token - if let Some((&m, _)) = self.fn_pre_token.iter().find(|&(_, &id)| id == f_id) { - return FuncKind::PreToken(m); - } - FuncKind::Decl(MemberId(f_id.0)) + /// Looks up the function kind + pub fn kind(&self, f_id: &FuncId) -> FuncKind { + self.kind + .get(f_id) + .expect(&format!("unknown FuncId {f_id:?}")) + .clone() } } diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index d83aeea..776e33e 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -2,14 +2,12 @@ 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::func_registry::{BUILTIN_OPTION_HEAD, FuncKind}; 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, Int}; +use z3::ast::{Ast, Bool, Dynamic}; use z3::datatype_builder::create_datatypes; use z3::{DatatypeAccessor, DatatypeBuilder, DatatypeSort, FuncDecl, Sort}; @@ -28,7 +26,9 @@ pub(crate) struct Z3Translation { 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.") + 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.") @@ -109,7 +109,7 @@ fn exact_node_type( Symbolic::RealCast(_) => Some(Type::Real), Symbolic::Forall(..) => Some(Type::Bool), Symbolic::Ite([_, then, _]) => exact_class_type(ctxt, *then, memo), - Symbolic::FuncApp(f, tys, _) => match ctxt.alloc.kind(*f) { + 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)), @@ -354,7 +354,7 @@ fn translate_function( ty: &Box<[Type]>, args: &Box<[Id]>, ) -> Dynamic { - let function_type = ctxt.alloc.kind(*f_id); + let function_type = ctxt.alloc.kind(f_id); match function_type { // A function, a domain function, or a field/predicate address @@ -453,7 +453,7 @@ fn datatype_shape(ctxt: &VerifyContext, ty: &Type) -> Option { Cow::Owned(r.derive_snapshot().expect("adt of resource")), &[], ), - _ => unreachable!("snapshot can only be taken from resources.") + _ => unreachable!("snapshot can only be taken from resources."), }, _ => return None, }; From 359431d1586606a9e84329697fdfbbf51e694a8d Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Mon, 26 Oct 2026 15:14:50 +0100 Subject: [PATCH 08/26] Report Z3 rung build and solve time VerifyStats gains a z3_timing trend (not gated), split into building the problem and Solver::check. verify --breakdown prints it and --json includes it. --- README.md | 2 +- src/bin/verify.rs | 9 ++++++++- src/verify/context/prove.rs | 4 ++++ src/verify/stats.rs | 32 ++++++++++++++++++++++++++++++++ 4 files changed, 45 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 01f8f7a..fe098c0 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 e2db49b..4268c21 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/prove.rs b/src/verify/context/prove.rs index 7c6f9ff..f255c45 100644 --- a/src/verify/context/prove.rs +++ b/src/verify/context/prove.rs @@ -840,6 +840,7 @@ impl<'a> VerifyContext<'a> { if !self.use_z3 { return false; } + let t_build = std::time::Instant::now(); let solver = z3::Solver::new(); let facts = crate::verify::z3::build_facts(self); @@ -855,8 +856,11 @@ impl<'a> VerifyContext<'a> { pc_cond.iter().for_each(|pc_cond| solver.assert(pc_cond)); solver.assert(!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(); + stats::bump(|s| s.z3_timing.0.solve += t_solve.elapsed().as_secs_f64()); match res { SatResult::Unsat => true, diff --git a/src/verify/stats.rs b/src/verify/stats.rs index 3b119f9..77da067 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,28 @@ 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. 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, +} + +/// [`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 +295,7 @@ impl VerifyStats { prove_ite_decompose, timing, graph_timing, + z3_timing, rule_timing, } = self; let n = |v: &u64| Json::from(*v); @@ -319,6 +344,13 @@ 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)), + ]), + ), ( "rule_timing", Json::obj(rule_timing.0.iter().map(|(k, t)| { From 2cbdae3b62ae5b05888872e9b502565ce11b075f Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Tue, 27 Oct 2026 13:15:30 +0100 Subject: [PATCH 09/26] fixup! Try Z3 as the last prover rung prove_by_z3 asserts the e-graph facts and the full path condition (block cube plus the instruction's literals) and checks the negated goal; unsat proves it. It runs only after every e-graph tier has failed, and only when SILVER_OXIDE_Z3 is set. --- src/verify/context/mod.rs | 4 ---- src/verify/context/prove.rs | 3 --- src/verify/func_registry.rs | 11 +++++++++++ 3 files changed, 11 insertions(+), 7 deletions(-) diff --git a/src/verify/context/mod.rs b/src/verify/context/mod.rs index 28f17f0..d500360 100644 --- a/src/verify/context/mod.rs +++ b/src/verify/context/mod.rs @@ -105,9 +105,6 @@ pub(crate) struct VerifyContext<'a> { /// where the set memoizes the *verdict* alone. Empty-pc goals still union /// (productive: `eq-true-union`/congruence off a proven `Eq`). oob_memo: bool, - /// `SILVER_OXIDE_Z3`: run the Z3 rung (`prove_by_z3`) when every e-graph - /// tier has failed. Off by default. - use_z3: bool, /// Canonical class ids of implications already proven `true`, consulted at /// the `memo` tier when `oob_memo` is on. Keyed by `egraph.find(imp)`: two distinct /// obligations only share a class via congruence — which means their goals @@ -202,7 +199,6 @@ impl<'a> VerifyContext<'a> { clean: None, has_wildcard: decls_have_wildcard(decls), oob_memo: std::env::var_os("SILVER_OXIDE_OOB_MEMO").is_some(), - use_z3: std::env::var_os("SILVER_OXIDE_Z3").is_some(), proven_imps: crate::dhash::HashSet::default(), current_cube: Vec::new(), in_block: false, diff --git a/src/verify/context/prove.rs b/src/verify/context/prove.rs index f255c45..ac9aae9 100644 --- a/src/verify/context/prove.rs +++ b/src/verify/context/prove.rs @@ -837,9 +837,6 @@ impl<'a> VerifyContext<'a> { } fn prove_by_z3(&mut self, goal: egg::Id, pc_lits: &[(egg::Id, Polarity)]) -> bool { - if !self.use_z3 { - return false; - } let t_build = std::time::Instant::now(); let solver = z3::Solver::new(); diff --git a/src/verify/func_registry.rs b/src/verify/func_registry.rs index 94f4982..7c96a49 100644 --- a/src/verify/func_registry.rs +++ b/src/verify/func_registry.rs @@ -162,6 +162,17 @@ impl FuncRegistry { variant_names, ..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. From e1f666f1bef48f84314164227c8b2f9e2ed5d8a4 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Tue, 27 Oct 2026 13:20:38 +0100 Subject: [PATCH 10/26] promoted tests that are no longer failing --- tests/cases/known_limitations/loops/ORACLE.md | 88 ------------------- .../goal_needs_case_split_heap_dep.vpr | 0 .../goal_needs_case_split_heap_free.vpr | 0 .../goal_needs_case_split_ternary_call.vpr | 0 .../loops/break_simple.vpr | 0 .../loops/break_state.vpr | 0 .../loops/frame_survives.vpr | 0 .../loops/goto_loop.vpr | 0 .../loops/list_walk.vpr | 0 .../loops/loop_under_if.vpr | 0 .../loops/nested.vpr | 0 .../loops/no_invariant.vpr | 0 .../loops/scalar_sum.vpr | 0 .../loops/wildcard_ro.vpr | 0 14 files changed, 88 deletions(-) delete mode 100644 tests/cases/known_limitations/loops/ORACLE.md rename tests/cases/{known_limitations => passing}/goal_needs_case_split_heap_dep.vpr (100%) rename tests/cases/{known_limitations => passing}/goal_needs_case_split_heap_free.vpr (100%) rename tests/cases/{known_limitations => passing}/goal_needs_case_split_ternary_call.vpr (100%) rename tests/cases/{known_limitations => passing}/loops/break_simple.vpr (100%) rename tests/cases/{known_limitations => passing}/loops/break_state.vpr (100%) rename tests/cases/{known_limitations => passing}/loops/frame_survives.vpr (100%) rename tests/cases/{known_limitations => passing}/loops/goto_loop.vpr (100%) rename tests/cases/{known_limitations => passing}/loops/list_walk.vpr (100%) rename tests/cases/{known_limitations => passing}/loops/loop_under_if.vpr (100%) rename tests/cases/{known_limitations => passing}/loops/nested.vpr (100%) rename tests/cases/{known_limitations => passing}/loops/no_invariant.vpr (100%) rename tests/cases/{known_limitations => passing}/loops/scalar_sum.vpr (100%) rename tests/cases/{known_limitations => passing}/loops/wildcard_ro.vpr (100%) diff --git a/tests/cases/known_limitations/loops/ORACLE.md b/tests/cases/known_limitations/loops/ORACLE.md deleted file mode 100644 index da83d38..0000000 --- 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/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 From 74085faa40de672fe7656557384fe7a8a71624fa Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Tue, 27 Oct 2026 13:25:37 +0100 Subject: [PATCH 11/26] formatting & clippy --- src/verify/func_registry.rs | 6 +++--- src/verify/z3/mod.rs | 8 +++++--- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/verify/func_registry.rs b/src/verify/func_registry.rs index 7c96a49..bb40c25 100644 --- a/src/verify/func_registry.rs +++ b/src/verify/func_registry.rs @@ -452,10 +452,10 @@ impl FuncRegistry { /// Looks up the function kind pub fn kind(&self, f_id: &FuncId) -> FuncKind { - self.kind + *self + .kind .get(f_id) - .expect(&format!("unknown FuncId {f_id:?}")) - .clone() + .unwrap_or_else(|| panic!("unknown FuncId {f_id:?}")) } } diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index 776e33e..b87833e 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -351,8 +351,8 @@ fn uninterpreted_app( fn translate_function( ctxt: &mut VerifyContext, f_id: &FuncId, - ty: &Box<[Type]>, - args: &Box<[Id]>, + ty: &[Type], + args: &[Id], ) -> Dynamic { let function_type = ctxt.alloc.kind(f_id); @@ -403,7 +403,9 @@ fn translate_function( 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]) + 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. From 411596c6ec412fbde906028a5aa19960b1647283 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Tue, 27 Oct 2026 14:03:27 +0100 Subject: [PATCH 12/26] if the class type can not be inferred, then the fact is dropped. --- src/verify/z3/mod.rs | 64 +++++++++++++++++++++++++++++--------------- 1 file changed, 43 insertions(+), 21 deletions(-) diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index b87833e..e8cf4f4 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -55,13 +55,13 @@ fn function_signature(ctxt: &VerifyContext, func: MemberId, tys: &[Type]) -> (Ve } } -/// The type of e-class `id` (translation.typ, "Class sorts"). Exact or a panic: -/// every node whose type is certain must agree, and at least one must exist. -/// Unlike `types::infer_type` this never guesses. -fn class_type(ctxt: &VerifyContext, id: Id) -> Type { +/// The type of e-class `id` (translation.typ, "Class sorts"), or `None` when no +/// node of the class has a certain type. Every node whose type is certain must +/// agree. Unlike `types::infer_type` this never guesses: without a sort the +/// class cannot be declared to Z3, so its facts are left out instead. +fn class_type(ctxt: &VerifyContext, id: Id) -> Option { let mut memo = crate::dhash::HashMap::default(); exact_class_type(ctxt, id, &mut memo) - .unwrap_or_else(|| panic!("e-class {id} has no node with a certain type")) } /// `None` when no node of the class has a certain type. `memo` maps a class to @@ -124,6 +124,8 @@ fn exact_node_type( } /// 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 build_facts(ctxt: &mut VerifyContext) -> Vec { // Snapshot the classes first: translating needs `ctxt` mutably (the sort // cache), so the e-graph cannot stay borrowed while we iterate it. @@ -134,7 +136,12 @@ pub(crate) fn build_facts(ctxt: &mut VerifyContext) -> Vec { .collect(); let mut facts = Vec::new(); for (id, nodes) in classes { - let class_const = class_const(ctxt, id); + let Some(class_const) = class_const(ctxt, id) else { + eprintln!( + "[z3] warning: e-class {id} has no node with a certain type; dropping its facts" + ); + continue; + }; // A `Forall` gets no equation: its class constant stays a free // `Bool`, and its instances are already in the e-graph as // `ite(forall, body, true) == true` (translation.typ, "The e-graph"). @@ -142,7 +149,12 @@ pub(crate) fn build_facts(ctxt: &mut VerifyContext) -> Vec { .iter() .filter(|node| !matches!(node, Symbolic::Forall(..))) { - let node_expression = symbol_to_z3(ctxt, node); + let Some(node_expression) = symbol_to_z3(ctxt, node) else { + eprintln!( + "[z3] warning: an operand of `{node}` in e-class {id} has no certain type; dropping its fact" + ); + continue; + }; facts.push(class_const.eq(node_expression)); } } @@ -150,17 +162,20 @@ pub(crate) fn build_facts(ctxt: &mut VerifyContext) -> Vec { } pub(crate) fn build_goal(ctxt: &mut VerifyContext, id: egg::Id) -> Bool { - let node = ctxt.egraph.find(id); - class_const(ctxt, node).as_bool().unwrap() + 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(ctxt, *id); + let c_const = class_const_given_sort(ctxt, *id, &Sort::bool()) + .as_bool() + .unwrap(); match p { - Polarity::Positive => c_const.as_bool().unwrap(), - Polarity::Negative => !c_const.as_bool().unwrap(), + Polarity::Positive => c_const, + Polarity::Negative => !c_const, } }) .collect() @@ -170,10 +185,11 @@ fn class_const_given_sort(ctxt: &VerifyContext, id: Id, sort: &Sort) -> Dynamic Dynamic::new_const(format!("c_{}", ctxt.egraph.find(id)), sort) } -fn class_const(ctxt: &mut VerifyContext, id: Id) -> Dynamic { - let typ = class_type(ctxt, id); +/// `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); - class_const_given_sort(ctxt, id, &sort) + Some(class_const_given_sort(ctxt, id, &sort)) } pub(crate) fn sort(ctxt: &mut VerifyContext, ty: &Type) -> Sort { @@ -208,8 +224,9 @@ pub(crate) fn sort(ctxt: &mut VerifyContext, ty: &Type) -> Sort { sort } -fn symbol_to_z3(ctxt: &mut VerifyContext, symbol: &Symbolic) -> Dynamic { - match symbol { +/// `⟦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 @@ -225,7 +242,12 @@ fn symbol_to_z3(ctxt: &mut VerifyContext, symbol: &Symbolic) -> Dynamic { Literal::Real(value) => z3::ast::Real::from_big_rational(value).into(), }, Symbolic::Binary(op, [l, r]) => { - let operand_ty = op.sort().unwrap_or_else(|| class_type(ctxt, *l)); + // `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); @@ -257,7 +279,7 @@ fn symbol_to_z3(ctxt: &mut VerifyContext, symbol: &Symbolic) -> Dynamic { } } Symbolic::Ite([cond, then, els]) => { - let then_ty = class_type(ctxt, *then); + 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() @@ -268,13 +290,13 @@ fn symbol_to_z3(ctxt: &mut VerifyContext, symbol: &Symbolic) -> Dynamic { } Symbolic::FuncApp(id, ty, args) => translate_function(ctxt, id, ty, args), Symbolic::RealCast(id) => { - let ty = class_type(ctxt, *id); + let ty = class_type(ctxt, *id)?; let sort = sort(ctxt, &ty); let class = class_const_given_sort(ctxt, *id, &sort).as_int().unwrap(); class.to_real().into() } Symbolic::Forall(_, _) => todo!("implement translation for forall nodes"), - } + }) } // the type build by heads constructor at instantiation typs From 5331e62bde428404d38e1fa57d403d3dbc612609 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Tue, 27 Oct 2026 14:06:06 +0100 Subject: [PATCH 13/26] moved wrongly annotated test as failing to passing --- .../ctor_ite_same_ctor_arms_pin_nothing.vpr | 16 --------------- .../passing/ctor_arm_pins_ite_condition.vpr | 7 +++++-- .../ctor_ite_same_ctor_arms_pin_nothing.vpr | 20 +++++++++++++++++++ 3 files changed, 25 insertions(+), 18 deletions(-) delete mode 100644 tests/cases/failing/ctor_ite_same_ctor_arms_pin_nothing.vpr create mode 100644 tests/cases/passing/ctor_ite_same_ctor_arms_pin_nothing.vpr 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 60f8e0c..0000000 --- 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/passing/ctor_arm_pins_ite_condition.vpr b/tests/cases/passing/ctor_arm_pins_ite_condition.vpr index cc036d3..2c3155d 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 0000000..60d4c3e --- /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 +} From 2a1344a1490c754a71b866192948167cf1beabae Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Tue, 27 Oct 2026 15:33:54 +0100 Subject: [PATCH 14/26] implement cache for class_types --- src/verify/z3/mod.rs | 92 +++++++++++++++++++++++++++----------------- 1 file changed, 56 insertions(+), 36 deletions(-) diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index e8cf4f4..e3ced61 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -18,6 +18,7 @@ use z3::{DatatypeAccessor, DatatypeBuilder, DatatypeSort, FuncDecl, Sort}; pub(crate) struct Z3Translation { sorts: HashMap, adts: HashMap, + class_types: HashMap, } /// Parameter and return types of function declaration `func` at instantiation @@ -56,48 +57,69 @@ fn function_signature(ctxt: &VerifyContext, func: MemberId, tys: &[Type]) -> (Ve } /// The type of e-class `id` (translation.typ, "Class sorts"), or `None` when no -/// node of the class has a certain type. Every node whose type is certain must -/// agree. Unlike `types::infer_type` this never guesses: without a sort the -/// class cannot be declared to Z3, so its facts are left out instead. -fn class_type(ctxt: &VerifyContext, id: Id) -> Option { - let mut memo = crate::dhash::HashMap::default(); - exact_class_type(ctxt, id, &mut memo) +/// 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 } -/// `None` when no node of the class has a certain type. `memo` maps a class to -/// its result; `None` is pre-seeded so an `Ite` cycle back into a class still -/// being resolved counts as uncertain rather than looping. -fn exact_class_type( +/// `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, - memo: &mut crate::dhash::HashMap>, ) -> Option { let id = ctxt.egraph.find(id); - if let Some(ty) = memo.get(&id) { - return ty.clone(); + if let Some(ty) = cache.get(&id) { + return Some(ty.clone()); } - memo.insert(id, None); - let mut found: Option = None; - for node in &ctxt.egraph[id].nodes { - let Some(ty) = exact_node_type(ctxt, node, memo) else { - continue; - }; - match &found { - None => found = Some(ty), - Some(prev) if *prev == ty => {} - Some(prev) => panic!("e-class {id} mixes types {prev} and {ty}"), - } + 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()); } - memo.insert(id, found.clone()); - found + ty } -/// The type of one e-node, or `None` when it is not certain. -fn exact_node_type( - ctxt: &VerifyContext, - node: &Symbolic, - memo: &mut crate::dhash::HashMap>, -) -> Option { +/// 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(), @@ -108,7 +130,7 @@ fn exact_node_type( }, Symbolic::RealCast(_) => Some(Type::Real), Symbolic::Forall(..) => Some(Type::Bool), - Symbolic::Ite([_, then, _]) => exact_class_type(ctxt, *then, memo), + 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), @@ -290,9 +312,7 @@ fn symbol_to_z3(ctxt: &mut VerifyContext, symbol: &Symbolic) -> Option } Symbolic::FuncApp(id, ty, args) => translate_function(ctxt, id, ty, args), Symbolic::RealCast(id) => { - let ty = class_type(ctxt, *id)?; - let sort = sort(ctxt, &ty); - let class = class_const_given_sort(ctxt, *id, &sort).as_int().unwrap(); + let class = class_const(ctxt, *id)?.as_int().unwrap(); class.to_real().into() } Symbolic::Forall(_, _) => todo!("implement translation for forall nodes"), From dfcc8f60982e704370108069f1bb6713c8a9d571 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Tue, 27 Oct 2026 15:48:35 +0100 Subject: [PATCH 15/26] add func_cache --- src/verify/z3/mod.rs | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index e3ced61..d89cdc0 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -19,6 +19,7 @@ pub(crate) struct Z3Translation { sorts: HashMap, adts: HashMap, class_types: HashMap, + func_cache : HashMap, FuncDecl>> } /// Parameter and return types of function declaration `func` at instantiation @@ -373,21 +374,29 @@ fn uninterpreted_app( "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 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 arg_refs: Vec<&dyn Ast> = arg_consts.iter().map(|a| a as &dyn Ast).collect(); - FuncDecl::new(name, &domain_refs, &range).apply(&arg_refs) + 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( From ffac45cf823abfea6cc7e01d3242ddb8f49cf001 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Tue, 27 Oct 2026 16:49:40 +0100 Subject: [PATCH 16/26] wip: don't rebuild the whole z3 query every time --- src/verify/context/prove.rs | 8 ++--- src/verify/z3/mod.rs | 66 ++++++++++++++++++------------------- 2 files changed, 36 insertions(+), 38 deletions(-) diff --git a/src/verify/context/prove.rs b/src/verify/context/prove.rs index ac9aae9..f712e36 100644 --- a/src/verify/context/prove.rs +++ b/src/verify/context/prove.rs @@ -840,7 +840,7 @@ impl<'a> VerifyContext<'a> { let t_build = std::time::Instant::now(); let solver = z3::Solver::new(); - let facts = crate::verify::z3::build_facts(self); + crate::verify::z3::sync_facts(self, &vec![]); let goal_z3 = crate::verify::z3::build_goal(self, goal); @@ -849,14 +849,12 @@ impl<'a> VerifyContext<'a> { let pc: Vec<_> = self.current_cube().iter().chain(pc_lits).copied().collect(); let pc_cond = crate::verify::z3::build_pc(self, &pc); - facts.iter().for_each(|fact| solver.assert(fact)); - pc_cond.iter().for_each(|pc_cond| solver.assert(pc_cond)); + let query = [pc_cond, vec![!goal_z3]].concat(); - solver.assert(!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(); + let res = solver.check_assumptions(&query); stats::bump(|s| s.z3_timing.0.solve += t_solve.elapsed().as_secs_f64()); match res { diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index d89cdc0..d0458fc 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -9,7 +9,7 @@ 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, Sort}; +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 @@ -19,7 +19,9 @@ pub(crate) struct Z3Translation { sorts: HashMap, adts: HashMap, class_types: HashMap, - func_cache : HashMap, FuncDecl>> + func_cache : HashMap, FuncDecl>>, + max_node_id: usize, + solver : Solver, } /// Parameter and return types of function declaration `func` at instantiation @@ -149,42 +151,40 @@ fn local_node_type(ctxt: &VerifyContext, node: &Symbolic) -> Option { /// 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 build_facts(ctxt: &mut VerifyContext) -> Vec { - // Snapshot the classes first: translating needs `ctxt` mutably (the sort - // cache), so the e-graph cannot stay borrowed while we iterate it. - let classes: Vec<(Id, Vec)> = ctxt - .egraph - .classes() - .map(|class| (class.id, class.nodes.clone())) - .collect(); - let mut facts = Vec::new(); - for (id, nodes) in classes { - let Some(class_const) = class_const(ctxt, id) else { - eprintln!( - "[z3] warning: e-class {id} has no node with a certain type; dropping its facts" - ); +pub(crate) fn sync_facts(ctxt: &mut VerifyContext, class_merges: &Vec<(Id, Id)>) { + + 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; - }; - // A `Forall` gets no equation: its class constant stays a free - // `Bool`, and its instances are already in the e-graph as - // `ite(forall, body, true) == true` (translation.typ, "The e-graph"). - for node in nodes - .iter() - .filter(|node| !matches!(node, Symbolic::Forall(..))) - { - let Some(node_expression) = symbol_to_z3(ctxt, node) else { - eprintln!( - "[z3] warning: an operand of `{node}` in e-class {id} has no certain type; dropping its fact" - ); - continue; - }; - facts.push(class_const.eq(node_expression)); } + 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; + }; + ctxt.z3translator.solver.assert(c.eq(expr)); } - facts + ctxt.z3translator.max_node_id = end; + + class_merges.iter().for_each(|(a, b)| { + match (class_const(ctxt, *a), class_const(ctxt, *b)) { + (Some(c_a), Some(c_b)) => ctxt.z3translator.solver.assert(c_a.eq(c_b)), + (_, _) => eprintln!("[z3] warning: could not find class_const for {a} or {b}"), + } + }); } -pub(crate) fn build_goal(ctxt: &mut VerifyContext, id: egg::Id) -> Bool { +pub(crate) fn build_goal(ctxt: &mut VerifyContext, id: Id) -> Bool { class_const_given_sort(ctxt, id, &Sort::bool()) .as_bool() .unwrap() From 584c169f1f1e062bdbaed0ab156b11b79ab1696e Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Tue, 27 Oct 2026 17:02:01 +0100 Subject: [PATCH 17/26] update egg to have the union log --- vendor/egg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vendor/egg b/vendor/egg index fb61679..ce7881b 160000 --- a/vendor/egg +++ b/vendor/egg @@ -1 +1 @@ -Subproject commit fb6167957beb5dd7c784121459e08ebd1ccb1a00 +Subproject commit ce7881bf8c36c3375ea2891d793e97fc226c93c6 From cf672b69daa6ba349a671e8b05209075fd775172 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Tue, 27 Oct 2026 17:12:42 +0100 Subject: [PATCH 18/26] use the union log to merge classes --- src/verify/context/prove.rs | 2 +- src/verify/z3/mod.rs | 31 ++++++++++++++++++++++++++----- 2 files changed, 27 insertions(+), 6 deletions(-) diff --git a/src/verify/context/prove.rs b/src/verify/context/prove.rs index f712e36..88fbc7a 100644 --- a/src/verify/context/prove.rs +++ b/src/verify/context/prove.rs @@ -840,7 +840,7 @@ impl<'a> VerifyContext<'a> { let t_build = std::time::Instant::now(); let solver = z3::Solver::new(); - crate::verify::z3::sync_facts(self, &vec![]); + crate::verify::z3::sync_facts(self); let goal_z3 = crate::verify::z3::build_goal(self, goal); diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index d0458fc..68b9f9e 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -21,6 +21,7 @@ pub(crate) struct Z3Translation { class_types: HashMap, func_cache : HashMap, FuncDecl>>, max_node_id: usize, + max_merges_is: usize, solver : Solver, } @@ -151,7 +152,7 @@ fn local_node_type(ctxt: &VerifyContext, node: &Symbolic) -> Option { /// 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, class_merges: &Vec<(Id, Id)>) { +pub(crate) fn sync_facts(ctxt: &mut VerifyContext) { let start = ctxt.z3translator.max_node_id; let end = ctxt.egraph.nodes().len(); @@ -176,12 +177,16 @@ pub(crate) fn sync_facts(ctxt: &mut VerifyContext, class_merges: &Vec<(Id, Id)>) } ctxt.z3translator.max_node_id = end; - class_merges.iter().for_each(|(a, b)| { - match (class_const(ctxt, *a), class_const(ctxt, *b)) { + 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)) => ctxt.z3translator.solver.assert(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 { @@ -204,8 +209,24 @@ pub(crate) fn build_pc(ctxt: &mut VerifyContext, pc: &[(egg::Id, Polarity)]) -> .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 { - Dynamic::new_const(format!("c_{}", ctxt.egraph.find(id)), sort) + 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`]). From 6aa50575b470f7e6f5038dc21de3f1436b4b70c9 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Tue, 27 Oct 2026 17:27:14 +0100 Subject: [PATCH 19/26] actually use the solver that aggregates the facts --- src/verify/context/prove.rs | 3 +-- src/verify/z3/mod.rs | 8 ++------ 2 files changed, 3 insertions(+), 8 deletions(-) diff --git a/src/verify/context/prove.rs b/src/verify/context/prove.rs index 88fbc7a..f897145 100644 --- a/src/verify/context/prove.rs +++ b/src/verify/context/prove.rs @@ -838,7 +838,6 @@ 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(); - let solver = z3::Solver::new(); crate::verify::z3::sync_facts(self); @@ -854,7 +853,7 @@ impl<'a> VerifyContext<'a> { 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_assumptions(&query); + let res = self.z3translator.solver.check_assumptions(&query); stats::bump(|s| s.z3_timing.0.solve += t_solve.elapsed().as_secs_f64()); match res { diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index 68b9f9e..9ebc65c 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -22,7 +22,7 @@ pub(crate) struct Z3Translation { func_cache : HashMap, FuncDecl>>, max_node_id: usize, max_merges_is: usize, - solver : Solver, + pub(crate) solver : Solver, } /// Parameter and return types of function declaration `func` at instantiation @@ -272,11 +272,7 @@ pub(crate) fn sort(ctxt: &mut VerifyContext, ty: &Type) -> Sort { fn symbol_to_z3(ctxt: &mut VerifyContext, symbol: &Symbolic) -> Option { Some(match symbol { Symbolic::Fresh(i) => { - let ty = ctxt - .fresh_types - .get(i) - .expect("fresh type not found") - .clone(); + let ty = ctxt.fresh_types.get(i)?.clone(); Dynamic::new_const(format!("fresh{i}"), &sort(ctxt, &ty)) } Symbolic::Lit(literal) => match literal { From 7bee4902733988bfa906590a9012f2ec74a3dbbd Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Wed, 28 Oct 2026 10:33:02 +0100 Subject: [PATCH 20/26] stats: count Z3 calls and time solver creation and asserts The Z3 rung reported only build and solve wall time. Benchmarking the solver lifecycle needs more: how often the rung runs, what Z3 answers, how many facts it is given, and how much of the time is creating the solver and the FFI assert calls alone. `Z3Timing` gains `init`, `assert`, `calls`, `unsat`, `sat`, `unknown` and `facts`; `build` and `solve` keep their meaning, so older logs stay comparable. All of it is a non-gated trend, like the existing timing fields. --- src/verify/context/prove.rs | 11 ++++++++++- src/verify/stats.rs | 21 +++++++++++++++++++- src/verify/z3/mod.rs | 38 ++++++++++++++++++++++++++++++++++--- 3 files changed, 65 insertions(+), 5 deletions(-) diff --git a/src/verify/context/prove.rs b/src/verify/context/prove.rs index f897145..1a1e3d4 100644 --- a/src/verify/context/prove.rs +++ b/src/verify/context/prove.rs @@ -854,7 +854,16 @@ impl<'a> VerifyContext<'a> { let t_solve = std::time::Instant::now(); let res = self.z3translator.solver.check_assumptions(&query); - stats::bump(|s| s.z3_timing.0.solve += t_solve.elapsed().as_secs_f64()); + stats::bump(|s| { + s.z3_timing.0.solve += t_solve.elapsed().as_secs_f64(); + s.z3_timing.0.calls += 1; + s.z3_timing.0.facts += query.len() as u64; + 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, diff --git a/src/verify/stats.rs b/src/verify/stats.rs index 77da067..05c2316 100644 --- a/src/verify/stats.rs +++ b/src/verify/stats.rs @@ -173,7 +173,8 @@ 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. Non-deterministic — a trend, never gated. +/// 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 @@ -181,6 +182,17 @@ pub struct Z3Timing { 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, } /// [`Z3Timing`] wrapper, `Eq`-transparent like [`TimingTrend`]. @@ -349,6 +361,13 @@ impl VerifyStats { 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)), ]), ), ( diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index 9ebc65c..aed464b 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -14,7 +14,6 @@ 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. -#[derive(Default)] pub(crate) struct Z3Translation { sorts: HashMap, adts: HashMap, @@ -25,6 +24,39 @@ pub(crate) struct Z3Translation { 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 solver one context keeps for all its queries; its creation is counted as +/// `z3_timing.init`. +pub(crate) fn new_solver() -> Solver { + let t = std::time::Instant::now(); + let solver = Solver::new(); + crate::verify::stats::bump(|s| s.z3_timing.0.init += t.elapsed().as_secs_f64()); + solver +} + +/// `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. @@ -173,7 +205,7 @@ pub(crate) fn sync_facts(ctxt: &mut VerifyContext) { eprintln!("[z3] warning: could not create the class_const for {class}"); continue; }; - ctxt.z3translator.solver.assert(c.eq(expr)); + assert_fact(&ctxt.z3translator.solver, &c.eq(expr)); } ctxt.z3translator.max_node_id = end; @@ -182,7 +214,7 @@ pub(crate) fn sync_facts(ctxt: &mut VerifyContext) { 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)) => ctxt.z3translator.solver.assert(c_a.eq(c_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}"), } } From 2e74ff0d947d2d561eaf55873fd9a5f98c1af439 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Wed, 28 Oct 2026 10:33:03 +0100 Subject: [PATCH 21/26] z3: discard what the solver learns on a throwaway graph `with_scratch_graph` runs code on a clone of the live e-graph and then restores the live graph. The clone hands out ids past the live graph's, and after the restore those ids are handed out again, for different terms. The persistent solver kept the clone's facts about them, its watermarks pointed past the restored graph (so new nodes below them were never synced), and the class-sort cache kept the clone's sorts. The scratch extent is now a solver scope: `enter_scratch` pushes and saves the watermarks and the sort cache, `leave_scratch` pops and restores them. `z3_timing.scratch_scopes` counts the scopes in which something had to be discarded. --- src/verify/context/prove.rs | 2 ++ src/verify/stats.rs | 4 ++++ src/verify/z3/mod.rs | 36 ++++++++++++++++++++++++++++++++++++ 3 files changed, 42 insertions(+) diff --git a/src/verify/context/prove.rs b/src/verify/context/prove.rs index 1a1e3d4..c12a909 100644 --- a/src/verify/context/prove.rs +++ b/src/verify/context/prove.rs @@ -1009,7 +1009,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/stats.rs b/src/verify/stats.rs index 05c2316..fe9a174 100644 --- a/src/verify/stats.rs +++ b/src/verify/stats.rs @@ -193,6 +193,9 @@ pub struct Z3Timing { 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`]. @@ -368,6 +371,7 @@ impl VerifyStats { ("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)), ]), ), ( diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index aed464b..b41f3a6 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -4,6 +4,7 @@ use itertools::Itertools; use crate::verify::context::VerifyContext; use crate::verify::func_registry::{BUILTIN_OPTION_HEAD, FuncKind}; use crate::vmir::{BinOp, Literal, MemberId, Polarity, Type}; +use crate::verify::stats; use crate::{HashMap, vmir}; use egg::Id; use std::borrow::Cow; @@ -47,6 +48,41 @@ pub(crate) fn new_solver() -> Solver { 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(); From bc1caab0c34b9e90895b288ded1f10134857811a Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Wed, 28 Oct 2026 10:33:04 +0100 Subject: [PATCH 22/26] z3: limit each check of the persistent solver (default 2 s) The persistent incremental solver answers most queries in milliseconds but can spend minutes on one (enum_v5_p1 never finished). The solver parameter `timeout` ends such a check as `unknown`, which the rung already treats as "not proven", so it can only lose a proof, never add one. `SILVER_OXIDE_Z3_TIMEOUT_MS` overrides the 2000 ms default. --- src/verify/z3/mod.rs | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index b41f3a6..8d6b99b 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -41,9 +41,20 @@ impl Default for Z3Translation { /// 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_TIMEOUT_MS` (default 2000 ms). +/// The persistent solver can get stuck on one query for minutes; a timeout ends +/// it as `unknown`, which the rung treats as "not proven". pub(crate) fn new_solver() -> Solver { let t = std::time::Instant::now(); let solver = Solver::new(); + let ms = std::env::var("SILVER_OXIDE_Z3_TIMEOUT_MS") + .ok() + .and_then(|v| v.parse().ok()) + .unwrap_or(2000); + let mut params = z3::Params::new(); + params.set_u32("timeout", ms); + solver.set_params(¶ms); crate::verify::stats::bump(|s| s.z3_timing.0.init += t.elapsed().as_secs_f64()); solver } From b4f22ba0d7089b30a09e0dba53bbb60a86d3d9d6 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Wed, 28 Oct 2026 13:12:19 +0100 Subject: [PATCH 23/26] z3: limit each check by resource units instead of time Replace the 2 s timeout with rlimit 1,500,000 (SILVER_OXIDE_Z3_RLIMIT), the value that best matched 2 s over 2,680 traced checks. The most expensive proof on the benchmark suite used 39,864 units, so no proof is lost, and the verdict no longer depends on machine speed or load. --- src/verify/z3/mod.rs | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index 8d6b99b..e238012 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -42,18 +42,21 @@ impl Default for Z3Translation { /// 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_TIMEOUT_MS` (default 2000 ms). -/// The persistent solver can get stuck on one query for minutes; a timeout ends -/// it as `unknown`, which the rung treats as "not proven". +/// 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(); let solver = Solver::new(); - let ms = std::env::var("SILVER_OXIDE_Z3_TIMEOUT_MS") + let rlimit = std::env::var("SILVER_OXIDE_Z3_RLIMIT") .ok() .and_then(|v| v.parse().ok()) - .unwrap_or(2000); + .unwrap_or(1_500_000); let mut params = z3::Params::new(); - params.set_u32("timeout", ms); + 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 From 6e55c4f36b9b0f9ee3bbda94db7abcbd45d6226d Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Wed, 28 Oct 2026 20:38:41 +0100 Subject: [PATCH 24/26] formatting --- src/verify/z3/mod.rs | 26 ++++++++++++++++++-------- 1 file changed, 18 insertions(+), 8 deletions(-) diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index e238012..8d730e7 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -3,8 +3,8 @@ use itertools::Itertools; use crate::verify::context::VerifyContext; use crate::verify::func_registry::{BUILTIN_OPTION_HEAD, FuncKind}; -use crate::vmir::{BinOp, Literal, MemberId, Polarity, Type}; use crate::verify::stats; +use crate::vmir::{BinOp, Literal, MemberId, Polarity, Type}; use crate::{HashMap, vmir}; use egg::Id; use std::borrow::Cow; @@ -19,10 +19,10 @@ pub(crate) struct Z3Translation { sorts: HashMap, adts: HashMap, class_types: HashMap, - func_cache : HashMap, FuncDecl>>, + func_cache: HashMap, FuncDecl>>, max_node_id: usize, max_merges_is: usize, - pub(crate) solver : Solver, + pub(crate) solver: Solver, } impl Default for Z3Translation { @@ -235,7 +235,6 @@ fn local_node_type(ctxt: &VerifyContext, node: &Symbolic) -> Option { /// 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 { @@ -247,7 +246,9 @@ pub(crate) fn sync_facts(ctxt: &mut VerifyContext) { continue; } let Some(expr) = symbol_to_z3(ctxt, &node) else { - eprintln!("[z3] warning: an operand of `{node}` has no certain type; dropping its fact"); + eprintln!( + "[z3] warning: an operand of `{node}` has no certain type; dropping its fact" + ); continue; }; let class = ctxt.egraph.find(id); @@ -262,7 +263,7 @@ pub(crate) fn sync_facts(ctxt: &mut VerifyContext) { 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]; + 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}"), @@ -481,7 +482,12 @@ fn uninterpreted_app( .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)) { + 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); @@ -493,7 +499,11 @@ fn uninterpreted_app( 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); + ctxt.z3translator + .func_cache + .entry(f) + .or_default() + .insert(tys.into(), func_decl); res } } From ae3345c6c362ebacf6074d08060932b70f54daf5 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Thu, 29 Oct 2026 10:46:15 +0100 Subject: [PATCH 25/26] z3: assert the path condition and goal in a scope, not as assumptions The same persistent plain solver, but each query's path condition and negated goal are asserted between push and pop instead of passed to check_assumptions. Compared against ramon/add-z3-ladder-step it isolates the effect of the query form on the plain incremental solver. --- src/verify/context/prove.rs | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/verify/context/prove.rs b/src/verify/context/prove.rs index c12a909..a0b17c6 100644 --- a/src/verify/context/prove.rs +++ b/src/verify/context/prove.rs @@ -848,16 +848,23 @@ impl<'a> VerifyContext<'a> { let pc: Vec<_> = self.current_cube().iter().chain(pc_lits).copied().collect(); let pc_cond = crate::verify::z3::build_pc(self, &pc); - let query = [pc_cond, vec![!goal_z3]].concat(); + // 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 = self.z3translator.solver.check_assumptions(&query); + 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; - s.z3_timing.0.facts += query.len() as u64; match res { SatResult::Unsat => s.z3_timing.0.unsat += 1, SatResult::Sat => s.z3_timing.0.sat += 1, From b64aebb80c5e24efdde84631269f71afd4ea57f2 Mon Sep 17 00:00:00 2001 From: TheRayMan Date: Thu, 29 Oct 2026 12:32:41 +0100 Subject: [PATCH 26/26] z3: use the options Silicon sets Set, once per process and before the first context exists, the options from Silicon's z3config.smt2 that change how Z3 solves: auto_config off, MBQI off, the simplex arithmetic solver (smt.arith.solver 2), case_split 3, delay_units, qi.eager_threshold 100 and qi.max_multi_patterns 1000. The options that only concern Silicon's SMT-LIB pipe or how output is printed are left out. A test checks that Z3 accepted every one, since it only warns about an unknown parameter. Co-Authored-By: Claude Opus 5.5 --- src/verify/z3/mod.rs | 45 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/src/verify/z3/mod.rs b/src/verify/z3/mod.rs index 8d730e7..79091fd 100644 --- a/src/verify/z3/mod.rs +++ b/src/verify/z3/mod.rs @@ -39,6 +39,35 @@ impl Default for Z3Translation { } } +/// 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`. /// @@ -50,6 +79,7 @@ impl Default for Z3Translation { /// 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() @@ -697,3 +727,18 @@ fn declare_datatypes(ctxt: &mut VerifyContext, root: &Type) { 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}"); + } + } +}