From a54fd38a3fa72264ae4615140b8d1433accdc8a6 Mon Sep 17 00:00:00 2001 From: madita Date: Wed, 10 Jun 2026 10:41:07 +0200 Subject: [PATCH 01/11] z3: add z3.rs submodule and switch Cargo to local path Switches from a pinned git revision to a local submodule path so the z3.rs sources are available for local modifications. --- .github/workflows/rust.yml | 8 +- .gitmodules | 3 + Cargo.lock | 608 +++++++++++-------------------------- Cargo.toml | 4 +- z3.rs | 1 + 5 files changed, 185 insertions(+), 439 deletions(-) create mode 100644 .gitmodules create mode 160000 z3.rs diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 167c8096..7b65a5d8 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -10,6 +10,8 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v6 + with: + submodules: recursive - name: Install packages shell: bash run: | @@ -23,8 +25,10 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v6 + with: + submodules: recursive - uses: dtolnay/rust-toolchain@stable - with: + with: components: rustfmt - run: cargo fmt --all -- --check @@ -33,6 +37,8 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v6 + with: + submodules: recursive - name: Install packages shell: bash run: | diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 00000000..7ad24648 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "z3.rs"] + path = z3.rs + url = https://github.com/prove-rs/z3.rs.git diff --git a/Cargo.lock b/Cargo.lock index eaddbd7e..603c0be3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -32,21 +32,6 @@ dependencies = [ "libc", ] -[[package]] -name = "anstream" -version = "0.6.21" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "43d5b281e737544384e969a5ccad3f1cdd24b48086a0fc1b2a5262a26b8f4f4a" -dependencies = [ - "anstyle", - "anstyle-parse 0.2.7", - "anstyle-query", - "anstyle-wincon", - "colorchoice", - "is_terminal_polyfill", - "utf8parse", -] - [[package]] name = "anstream" version = "1.0.0" @@ -54,7 +39,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "824a212faf96e9acacdbd09febd34438f8f711fb84e09a8916013cd7815ca28d" dependencies = [ "anstyle", - "anstyle-parse 1.0.0", + "anstyle-parse", "anstyle-query", "anstyle-wincon", "colorchoice", @@ -68,15 +53,6 @@ version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "940b3a0ca603d1eade50a4846a2afffd5ef57a9feac2c0e2ec2e14f9ead76000" -[[package]] -name = "anstyle-parse" -version = "0.2.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4e7644824f0aa2c7b9384579234ef10eb7efb6a0deb83f9630a49594dd9c15c2" -dependencies = [ - "utf8parse", -] - [[package]] name = "anstyle-parse" version = "1.0.0" @@ -114,9 +90,9 @@ checksum = "7f202df86484c868dbad7eaa557ef785d5c66295e41b460ef922eca0723b842c" [[package]] name = "ar_archive_writer" -version = "0.5.1" +version = "0.5.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7eb93bbb63b9c227414f6eb3a0adfddca591a8ce1e9b60661bb08969b87e340b" +checksum = "4087686b4b0a3427190bae57a1d9a478dbb2d40c5dc1bd6e2b6d797913bdd348" dependencies = [ "object", ] @@ -148,9 +124,9 @@ dependencies = [ [[package]] name = "autocfg" -version = "1.5.0" +version = "1.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8" +checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53" [[package]] name = "base64" @@ -164,7 +140,7 @@ version = "0.72.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "993776b509cfb49c750f11b8f07a46fa23e0a1386ffc01fb1e7d343efc387895" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", "cexpr", "clang-sys", "itertools 0.13.0", @@ -172,7 +148,7 @@ dependencies = [ "quote", "regex", "rustc-hash", - "shlex", + "shlex 1.3.0", "syn", ] @@ -214,9 +190,9 @@ checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" [[package]] name = "bitflags" -version = "2.11.0" +version = "2.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "843867be96c8daad0d758b57df9392b6d8d271134fce549de6ce169ff98a92af" +checksum = "b4388bee8683e3d04af747c73422af53102d2bd24d9eadb6cbc100baef4b43f8" [[package]] name = "bitmaps" @@ -247,9 +223,9 @@ dependencies = [ [[package]] name = "built" -version = "0.8.0" +version = "0.8.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f4ad8f11f288f48ca24471bbd51ac257aaeaaa07adae295591266b792902ae64" +checksum = "5c0e531d93d39c34eef561e929e8a7f86d77a5af08aac4f6d6e39976c51858e9" dependencies = [ "chrono", "git2", @@ -257,9 +233,9 @@ dependencies = [ [[package]] name = "bumpalo" -version = "3.20.2" +version = "3.20.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5d20789868f4b01b2f2caec9f5c4e0213b41e3e5702a50157d699ae31ced2fcb" +checksum = "72f5acc6cb2ba439de613abc23857ec3d78374d8ed5ac84e9d11336e87da8649" [[package]] name = "byteorder" @@ -304,7 +280,7 @@ dependencies = [ "replace_with", "serde", "serde_json", - "shlex", + "shlex 1.3.0", "stacker", "string-interner", "tempfile", @@ -318,14 +294,14 @@ dependencies = [ [[package]] name = "cc" -version = "1.2.57" +version = "1.2.64" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7a0dd1ca384932ff3641c8718a02769f1698e7563dc6974ffd03346116310423" +checksum = "dad887fd958be91b5098c0248def011f4523ab786cd411be668777e55063501f" dependencies = [ "find-msvc-tools", "jobserver", "libc", - "shlex", + "shlex 2.0.1", ] [[package]] @@ -351,9 +327,9 @@ checksum = "613afe47fcd5fac7ccf1db93babcb082c5994d996f20b8b159f2ad1658eb5724" [[package]] name = "chrono" -version = "0.4.44" +version = "0.4.45" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c673075a2e0e5f4a1dde27ce9dee1ea4558c7ffe648f576438a20ca1d2acc4b0" +checksum = "1aa79e62e7697b8e29b513a68abacf485adcd1fe8284a4316c5ae868e6633327" dependencies = [ "iana-time-zone", "num-traits", @@ -373,9 +349,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.6.0" +version = "4.6.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b193af5b67834b676abd72466a96c1024e6a6ad978a1f484bd90b85c94041351" +checksum = "1ddb117e43bbf7dacf0a4190fef4d345b9bad68dfc649cb349e7d17d28428e51" dependencies = [ "clap_builder", "clap_derive", @@ -387,7 +363,7 @@ version = "4.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "714a53001bf66416adb0e2ef5ac857140e7dc3a0c48fb28b2f10762fc4b5069f" dependencies = [ - "anstream 1.0.0", + "anstream", "anstyle", "clap_lex", "strsim", @@ -395,18 +371,18 @@ dependencies = [ [[package]] name = "clap_complete" -version = "4.6.0" +version = "4.6.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "19c9f1dde76b736e3681f28cec9d5a61299cbaae0fce80a68e43724ad56031eb" +checksum = "e0a7a9bfdb35811f9e59832f0f05975114d2251b415fb534108e6f34060fd772" dependencies = [ "clap", ] [[package]] name = "clap_derive" -version = "4.6.0" +version = "4.6.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1110bd8a634a1ab8cb04345d8d878267d57c3cf1b38d91b71af6686408bbca6a" +checksum = "f2ce8604710f6733aa641a2b3731eaa1e8b3d9973d5e3565da11800813f997a9" dependencies = [ "heck", "proc-macro2", @@ -445,9 +421,9 @@ dependencies = [ [[package]] name = "cmake" -version = "0.1.57" +version = "0.1.58" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "75443c44cd6b379beb8c5b45d85d0773baf31cce901fe7bb252f4eff3008ef7d" +checksum = "c0f78a02292a74a88ac736019ab962ece0bc380e3f977bf72e376c5d78ff0678" dependencies = [ "cc", ] @@ -542,9 +518,9 @@ dependencies = [ [[package]] name = "dashmap" -version = "6.1.0" +version = "6.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5041cc499144891f3790297212f32a74fb938e5136a14943f338ef9e0ae276cf" +checksum = "e6361d5c062261c78a176addb82d4c821ae42bed6089de0e12603cd25de2059c" dependencies = [ "cfg-if", "crossbeam-utils", @@ -576,21 +552,10 @@ version = "0.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1e0e367e4e7da84520dedcac1901e4da967309406d1e51017ae1abfb97adbd38" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", "objc2", ] -[[package]] -name = "displaydoc" -version = "0.2.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "97369cbbc041bc366949bc74d34658d6cda5621039731c6310521892a3a20ae0" -dependencies = [ - "proc-macro2", - "quote", - "syn", -] - [[package]] name = "egg" version = "0.11.0" @@ -613,9 +578,9 @@ dependencies = [ [[package]] name = "either" -version = "1.15.0" +version = "1.16.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "48c757948c5ede0e46177b7add2e67155f70e33c07fea8284df6576da70b3719" +checksum = "91622ff5e7162018101f2fea40d6ebf4a78bbe5a49736a2020649edf9693679e" [[package]] name = "ena" @@ -685,9 +650,9 @@ checksum = "5692dd7b5a1978a5aeb0ce83b7655c58ca8efdcb79d21036ea249da95afec2c6" [[package]] name = "fastrand" -version = "2.3.0" +version = "2.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "37909eebbb50d72f9059c3b6d82c0463f2ff062c9e95845c43a6c9c0355411be" +checksum = "9f1f227452a390804cdb637b74a86990f2a7d7ba4b7d5693aac9b4dd6defd8d6" [[package]] name = "find-msvc-tools" @@ -733,12 +698,27 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2" [[package]] -name = "form_urlencoded" -version = "1.2.2" +name = "futures-core" +version = "0.3.32" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cb4cb245038516f5f85277875cdaa4f7d2c9a0fa0468de06ed190163b1581fcf" +checksum = "7e3450815272ef58cec6d564423f6e755e25379b217b0bc688e295ba24df6b1d" + +[[package]] +name = "futures-task" +version = "0.3.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "037711b3d59c33004d3856fbdc83b99d4ff37a24768fa1be9ce3538a1cde4393" + +[[package]] +name = "futures-util" +version = "0.3.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "389ca41296e6190b48053de0321d02a77f32f8a5d2461dd38762c0593805c6d6" dependencies = [ - "percent-encoding", + "futures-core", + "futures-task", + "pin-project-lite", + "slab", ] [[package]] @@ -778,15 +758,14 @@ dependencies = [ [[package]] name = "git2" -version = "0.20.4" +version = "0.21.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7b88256088d75a56f8ecfa070513a775dd9107f6530ef14919dac831af9cfe2b" +checksum = "ddddbf932745a6be37109b6112d3ee09696106f848449069d3a57bba937ab82e" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", "libc", "libgit2-sys", "log", - "url", ] [[package]] @@ -814,9 +793,9 @@ dependencies = [ [[package]] name = "hashbrown" -version = "0.16.1" +version = "0.17.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "841d1cc9bed7f9236f321df977030373f4a4163ae1a7dbfe1a51a2c1a51d9100" +checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a" [[package]] name = "hdrhistogram" @@ -862,114 +841,12 @@ dependencies = [ "cc", ] -[[package]] -name = "icu_collections" -version = "2.1.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4c6b649701667bbe825c3b7e6388cb521c23d88644678e83c0c4d0a621a34b43" -dependencies = [ - "displaydoc", - "potential_utf", - "yoke", - "zerofrom", - "zerovec", -] - -[[package]] -name = "icu_locale_core" -version = "2.1.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "edba7861004dd3714265b4db54a3c390e880ab658fec5f7db895fae2046b5bb6" -dependencies = [ - "displaydoc", - "litemap", - "tinystr", - "writeable", - "zerovec", -] - -[[package]] -name = "icu_normalizer" -version = "2.1.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5f6c8828b67bf8908d82127b2054ea1b4427ff0230ee9141c54251934ab1b599" -dependencies = [ - "icu_collections", - "icu_normalizer_data", - "icu_properties", - "icu_provider", - "smallvec", - "zerovec", -] - -[[package]] -name = "icu_normalizer_data" -version = "2.1.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7aedcccd01fc5fe81e6b489c15b247b8b0690feb23304303a9e560f37efc560a" - -[[package]] -name = "icu_properties" -version = "2.1.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "020bfc02fe870ec3a66d93e677ccca0562506e5872c650f893269e08615d74ec" -dependencies = [ - "icu_collections", - "icu_locale_core", - "icu_properties_data", - "icu_provider", - "zerotrie", - "zerovec", -] - -[[package]] -name = "icu_properties_data" -version = "2.1.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "616c294cf8d725c6afcd8f55abc17c56464ef6211f9ed59cccffe534129c77af" - -[[package]] -name = "icu_provider" -version = "2.1.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "85962cf0ce02e1e0a629cc34e7ca3e373ce20dda4c4d7294bbd0bf1fdb59e614" -dependencies = [ - "displaydoc", - "icu_locale_core", - "writeable", - "yoke", - "zerofrom", - "zerotrie", - "zerovec", -] - [[package]] name = "id-arena" version = "2.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3d3067d79b975e8844ca9eb072e16b31c3c1c36928edf9c6789548c524d0d954" -[[package]] -name = "idna" -version = "1.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3b0875f23caa03898994f6ddc501886a45c7d3d62d04d2d90788d47be1b1e4de" -dependencies = [ - "idna_adapter", - "smallvec", - "utf8_iter", -] - -[[package]] -name = "idna_adapter" -version = "1.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3acae9609540aa318d1bc588455225fb2085b9ed0c4f6bd0d9d5bcd86f1a0344" -dependencies = [ - "icu_normalizer", - "icu_properties", -] - [[package]] name = "im-rc" version = "15.1.0" @@ -986,12 +863,12 @@ dependencies = [ [[package]] name = "indexmap" -version = "2.13.0" +version = "2.14.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7714e70437a7dc3ac8eb7e6f8df75fd8eb422675fc7678aff7364301092b1017" +checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9" dependencies = [ "equivalent", - "hashbrown 0.16.1", + "hashbrown 0.17.1", "serde", "serde_core", ] @@ -1035,9 +912,9 @@ dependencies = [ [[package]] name = "itoa" -version = "1.0.17" +version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "92ecc6618181def0457392ccd0ee51198e065e016d1d527a7ac1b6dc7c1f09d2" +checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" [[package]] name = "jani" @@ -1059,11 +936,12 @@ dependencies = [ [[package]] name = "js-sys" -version = "0.3.91" +version = "0.3.102" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b49715b7073f385ba4bc528e5747d02e66cb39c6146efb66b781f131f0fb399c" +checksum = "03d04c30968dffe80775bd4d7fb676131cd04a1fb46d2686dbffbaec2d9dfd31" dependencies = [ - "once_cell", + "cfg-if", + "futures-util", "wasm-bindgen", ] @@ -1121,15 +999,15 @@ checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2" [[package]] name = "libc" -version = "0.2.183" +version = "0.2.186" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5b646652bf6661599e1da8901b3b9522896f01e736bad5f723fe7a3a27f899d" +checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66" [[package]] name = "libgit2-sys" -version = "0.18.3+1.9.2" +version = "0.18.5+1.9.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c9b3acc4b91781bb0b3386669d325163746af5f6e4f73e6d2d630e09a35f3487" +checksum = "005d6ae6eac1912906073e069f7db60b1fa98e052a68227824afe3e3a1c59ca2" dependencies = [ "cc", "libc", @@ -1149,11 +1027,11 @@ dependencies = [ [[package]] name = "libtest-mimic" -version = "0.8.1" +version = "0.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5297962ef19edda4ce33aaa484386e0a5b3d7f2f4e037cbeee00503ef6b29d33" +checksum = "14e6ba06f0ade6e504aff834d7c34298e5155c6baca353cc6a4aaff2f9fd7f33" dependencies = [ - "anstream 0.6.21", + "anstream", "anstyle", "clap", "escape8259", @@ -1161,9 +1039,9 @@ dependencies = [ [[package]] name = "libz-sys" -version = "1.1.25" +version = "1.1.29" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d52f4c29e2a68ac30c9087e1b772dc9f44a2b66ed44edf2266cf2be9b03dafc1" +checksum = "85bc9657773828b90eeb625adff10eeac83cc21bbfd8e23a03eaa8a33c9e28d9" dependencies = [ "cc", "libc", @@ -1177,12 +1055,6 @@ version = "0.12.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "32a66949e030da00e8c7d4434b251670a91556f4144941d37452769c25d58a53" -[[package]] -name = "litemap" -version = "0.8.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6373607a59f0be73a39b6fe456b8192fcc3585f602af20751600e974dd455e77" - [[package]] name = "lock_api" version = "0.4.14" @@ -1194,9 +1066,9 @@ dependencies = [ [[package]] name = "log" -version = "0.4.29" +version = "0.4.32" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897" +checksum = "953f07c43838f8e6f9758cab68bf5bed85465e7587ebe0b823f1bcd81978ad3a" [[package]] name = "lsp-server" @@ -1235,9 +1107,9 @@ dependencies = [ [[package]] name = "memchr" -version = "2.8.0" +version = "2.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f8ca58f447f06ed17d5fc4043ce1b10dd205e060fb3ce5b979b8ed8e59ff3f79" +checksum = "88904434abc2901f197fe8cc55f0445e7ded921dba5911dad2e2b39b48e663c4" [[package]] name = "memory-stats" @@ -1273,11 +1145,11 @@ checksum = "650eef8c711430f1a879fdd01d4745a7deea475becfb90269c06775983bbf086" [[package]] name = "nix" -version = "0.30.1" +version = "0.31.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "74523f3a35e05aba87a1d978330aef40f67b0304ac79c1c00b294c9830543db6" +checksum = "cf20d2fde8ff38632c426f1165ed7436270b44f199fc55284c38276f9db47c3d" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", "cfg-if", "cfg_aliases", "libc", @@ -1390,7 +1262,7 @@ version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "73ad74d880bb43877038da939b7427bba67e9dd42004a18b809ba7d87cee241c" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", "objc2", "objc2-foundation", ] @@ -1411,7 +1283,7 @@ version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2a180dd8642fa45cdb7dd721cd4c11b1cadd4929ce112ebd8b9f5803cc79d536" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", "dispatch2", "objc2", ] @@ -1422,7 +1294,7 @@ version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e022c9d066895efa1345f8e33e584b9f958da2fd4cd116792e15e07e4720a807" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", "dispatch2", "objc2", "objc2-core-foundation", @@ -1455,7 +1327,7 @@ version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0cde0dfb48d25d2b4862161a4d5fcc0e3c24367869ad306b0c9ec0073bfed92d" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", "objc2", "objc2-core-foundation", "objc2-core-graphics", @@ -1473,7 +1345,7 @@ version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e3e0adef53c21f888deb4fa59fc59f7eb17404926ee8a6f59f5df0fd7f9f3272" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", "block2", "libc", "objc2", @@ -1486,7 +1358,7 @@ version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "180788110936d59bab6bd83b6060ffdfffb3b922ba1396b312ae795e1de9d81d" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", "objc2", "objc2-core-foundation", ] @@ -1497,7 +1369,7 @@ version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "96c1358452b371bf9f104e21ec536d37a650eb10f7ee379fff67d2e08d537f1f" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", "objc2", "objc2-core-foundation", "objc2-foundation", @@ -1509,7 +1381,7 @@ version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d87d638e33c06f577498cbcc50491496a3ed4246998a7fbba7ccb98b1e7eab22" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", "block2", "objc2", "objc2-cloud-kit", @@ -1557,9 +1429,9 @@ checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe" [[package]] name = "os_info" -version = "3.14.0" +version = "3.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e4022a17595a00d6a369236fdae483f0de7f0a339960a53118b818238e132224" +checksum = "9cf20a545b305cf1da722b236b5155c9bb35f1d5ceb28c048bd96ca842f41b5b" dependencies = [ "android_system_properties", "log", @@ -1600,12 +1472,6 @@ version = "0.2.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "df94ce210e5bc13cb6651479fa48d14f601d9858cfe0467f43ae157023b938d3" -[[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.8.3" @@ -1641,9 +1507,9 @@ checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd" [[package]] name = "pkg-config" -version = "0.3.32" +version = "0.3.33" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7edddbd0b52d732b21ad9a5fab5c704c14cd949e5e9a1ec5929a24fded1b904c" +checksum = "19f132c84eca552bf34cab8ec81f1c1dcc229b811638f9d283dceabe58c5569e" [[package]] name = "portable-atomic" @@ -1651,15 +1517,6 @@ version = "1.13.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c33a9471896f1c69cecef8d20cbe2f7accd12527ce60845ff44c153bb2a21b49" -[[package]] -name = "potential_utf" -version = "0.1.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b73949432f5e2a09657003c25bca5e19a0e9c84f8058ca374f49e0ebe605af77" -dependencies = [ - "zerovec", -] - [[package]] name = "ppv-lite86" version = "0.2.21" @@ -1717,13 +1574,13 @@ dependencies = [ [[package]] name = "proptest" -version = "1.10.0" +version = "1.11.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "37566cb3fdacef14c0737f9546df7cfeadbfbc9fef10991038bf5015d0c80532" +checksum = "4b45fcc2344c680f5025fe57779faef368840d0bd1f42f216291f0dc4ace4744" dependencies = [ "bit-set 0.8.0", "bit-vec 0.8.0", - "bitflags 2.11.0", + "bitflags 2.13.0", "num-traits", "rand", "rand_chacha", @@ -1736,9 +1593,9 @@ dependencies = [ [[package]] name = "psm" -version = "0.1.30" +version = "0.1.31" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3852766467df634d74f0b2d7819bf8dc483a0eb2e3b0f50f756f9cfe8b0d18d8" +checksum = "645dbe486e346d9b5de3ef16ede18c26e6c70ad97418f4874b8b1889d6e761ea" dependencies = [ "ar_archive_writer", "cc", @@ -1788,9 +1645,9 @@ checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf" [[package]] name = "rand" -version = "0.9.2" +version = "0.9.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6db2770f06117d490610c7488547d543617b21bfa07796d7a12f6f1bd53850d1" +checksum = "44c5af06bb1b7d3216d91932aed5265164bf384dc89cd6ba05cf59a35f5f76ea" dependencies = [ "rand_chacha", "rand_core 0.9.5", @@ -1845,7 +1702,7 @@ version = "11.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "498cd0dc59d73224351ee52a95fee0f1a617a2eae0e7d9d720cc622c73a54186" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", ] [[package]] @@ -1854,7 +1711,7 @@ version = "0.5.18" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ed2bf2547551a7053d6fdfafda3f938979645c44812fbfcda098faae3f1a362d" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", ] [[package]] @@ -1879,9 +1736,9 @@ dependencies = [ [[package]] name = "regex" -version = "1.12.3" +version = "1.12.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e10754a14b9137dd7b1e3e5b0493cc9171fdd105e0ab477f51b72e7f3ac0e276" +checksum = "f1292b7759ae1cb9ec195452d1390a074f0cd8541ab7a5a8c31cd6db45d4a6ba" dependencies = [ "aho-corasick", "memchr", @@ -1902,9 +1759,9 @@ dependencies = [ [[package]] name = "regex-syntax" -version = "0.8.10" +version = "0.8.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dc897dd8d9e8bd1ed8cdad82b5966c3e0ecae09fb1907d58efaa013543185d0a" +checksum = "d6f6ff9a378485b298a5286656da665ba74413d36db0979633275d2e708145d4" [[package]] name = "replace_with" @@ -1914,9 +1771,9 @@ checksum = "51743d3e274e2b18df81c4dc6caf8a5b8e15dbe799e0dca05c7617380094e884" [[package]] name = "rustc-hash" -version = "2.1.1" +version = "2.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "357703d41365b4b27c590e3ed91eabb1b663f07c4c084095e60cbed4362dff0d" +checksum = "94300abf3f1ae2e2b8ffb7b58043de3d399c73fa6f4b73826402a5c457614dbe" [[package]] name = "rustix" @@ -1924,7 +1781,7 @@ version = "1.1.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b6fe4565b9518b83ef4f91bb47ce29620ca828bd32cb7e408f0062e9930ba190" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", "errno", "libc", "linux-raw-sys", @@ -1973,7 +1830,7 @@ dependencies = [ "indicatif", "serde", "serde_json", - "shlex", + "shlex 1.3.0", ] [[package]] @@ -1984,9 +1841,9 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "semver" -version = "1.0.27" +version = "1.0.28" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d767eb0aabc880b29956c35734170f26ed551a859dbd361d140cdbeca61ab1e2" +checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd" [[package]] name = "serde" @@ -2020,9 +1877,9 @@ dependencies = [ [[package]] name = "serde_json" -version = "1.0.149" +version = "1.0.150" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "83fc039473c5595ace860d8c4fafa220ff474b3fc6bfdb4293327f1a37e94d86" +checksum = "e8014e44b4736ed0538adeecded0fce2a272f22dc9578a7eb6b2d9993c74cfb9" dependencies = [ "itoa", "memchr", @@ -2044,9 +1901,9 @@ dependencies = [ [[package]] name = "sha3" -version = "0.10.8" +version = "0.10.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "75872d278a8f37ef87fa0ddbda7802605cb18344497949862c0d4dcb291eba60" +checksum = "77fd7028345d415a4034cf8777cd4f8ab1851274233b45f84e3d955502d93874" dependencies = [ "digest", "keccak", @@ -2067,17 +1924,23 @@ version = "1.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" +[[package]] +name = "shlex" +version = "2.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8fadd59c855ef2080decdef8ff161eb6661b86933c9d82e5ba29dc602a55aba" + [[package]] name = "simd-adler32" -version = "0.3.8" +version = "0.3.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e320a6c5ad31d271ad523dcf3ad13e2767ad8b1cb8f047f75a8aeaf8da139da2" +checksum = "703d5c7ef118737c72f1af64ad2f6f8c5e1921f818cdcb97b8fe6fc69bf66214" [[package]] name = "siphasher" -version = "1.0.2" +version = "1.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b2aa850e253778c88a04c3d7323b043aeda9d3e30d5971937c1855769763678e" +checksum = "8ee5873ec9cce0195efcb7a4e9507a04cd49aec9c83d0389df45b1ef7ba2e649" [[package]] name = "sized-chunks" @@ -2090,28 +1953,28 @@ dependencies = [ ] [[package]] -name = "smallvec" -version = "1.15.1" +name = "slab" +version = "0.4.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03" +checksum = "0c790de23124f9ab44544d7ac05d60440adc586479ce501c1d6d7da3cd8c9cf5" [[package]] -name = "stable_deref_trait" -version = "1.2.1" +name = "smallvec" +version = "1.15.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ce2be8dc25455e1f91df71bfa12ad37d7af1092ae736f3a6cd0e37bc7810596" +checksum = "8ed6a63f02c8539c91a8685a86f4099661ba3da017932f6ebbea6de3f0fa7c90" [[package]] name = "stacker" -version = "0.1.23" +version = "0.1.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "08d74a23609d509411d10e2176dc2a4346e3b4aea2e7b1869f19fdedbc71c013" +checksum = "640c8cdd92b6b12f5bcb1803ca3bbf5ab96e5e6b6b96b9ab77dabe9e880b3190" dependencies = [ "cc", "cfg-if", "libc", "psm", - "windows-sys 0.59.0", + "windows-sys 0.61.2", ] [[package]] @@ -2161,26 +2024,15 @@ checksum = "7c68d531d83ec6c531150584c42a4290911964d5f0d79132b193b67252a23b71" [[package]] name = "syn" -version = "2.0.117" +version = "2.0.118" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99" +checksum = "1b9ae57f904213ebb649ce6895b8a66c66f0203b9319718f69a5612a065b1422" dependencies = [ "proc-macro2", "quote", "unicode-ident", ] -[[package]] -name = "synstructure" -version = "0.13.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "728a70f3dbaf5bab7f0c4b1ac8d7ae5ea60a4b5549c8a5914361c99147a709d2" -dependencies = [ - "proc-macro2", - "quote", - "syn", -] - [[package]] name = "tempfile" version = "3.27.0" @@ -2261,21 +2113,11 @@ dependencies = [ "cfg-if", ] -[[package]] -name = "tinystr" -version = "0.8.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "42d3e9c45c09de15d06dd8acf5f4e0e399e85927b7f00711024eb7ae10fa4869" -dependencies = [ - "displaydoc", - "zerovec", -] - [[package]] name = "tokio" -version = "1.50.0" +version = "1.52.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "27ad5e34374e03cfffefc301becb44e9dc3c17584f414349ebe29ed26661822d" +checksum = "8fc7f01b389ac15039e4dc9531aa973a135d7a4135281b12d7c1bc79fd57fffe" dependencies = [ "pin-project-lite", "tokio-macros", @@ -2283,9 +2125,9 @@ dependencies = [ [[package]] name = "tokio-macros" -version = "2.6.1" +version = "2.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5c55a2eff8b69ce66c84f85e1da1c233edc36ceb85a2058d11b0d6a3c7e7569c" +checksum = "385a6cb71ab9ab790c5fe8d67f1645e6c450a7ce006a33de03daa956cf70a496" dependencies = [ "proc-macro2", "quote", @@ -2374,9 +2216,9 @@ checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a" [[package]] name = "typenum" -version = "1.19.0" +version = "1.20.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "562d481066bde0658276a35467c4af00bdc6ee726305698a55b86e61d7ad82bb" +checksum = "b6f5e870be6c3b371b77fe0ee0bafb859fa4964b4404c27de1d380043c4dda20" [[package]] name = "unarray" @@ -2408,24 +2250,6 @@ version = "0.5.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "81e544489bf3d8ef66c953931f56617f423cd4b5494be343d9b9d3dda037b9a3" -[[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 = "utf8parse" version = "0.2.2" @@ -2477,11 +2301,11 @@ checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b" [[package]] name = "wasip2" -version = "1.0.2+wasi-0.2.9" +version = "1.0.4+wasi-0.2.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9517f9239f02c069db75e65f174b3da828fe5f5b945c4dd26bd25d89c03ebcf5" +checksum = "b67efb37e106e55ce722a510d6b5f9c17f083e5fc79afc2badeb12cc313d9487" dependencies = [ - "wit-bindgen", + "wit-bindgen 0.57.1", ] [[package]] @@ -2490,14 +2314,14 @@ version = "0.4.0+wasi-0.3.0-rc-2026-01-06" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5428f8bf88ea5ddc08faddef2ac4a67e390b88186c703ce6dbd955e1c145aca5" dependencies = [ - "wit-bindgen", + "wit-bindgen 0.51.0", ] [[package]] name = "wasm-bindgen" -version = "0.2.114" +version = "0.2.125" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6532f9a5c1ece3798cb1c2cfdba640b9b3ba884f5db45973a6f442510a87d38e" +checksum = "8ddb3f79143bced6de84270411622a2699cee572fc0875aeaf1e7867cf9fca1a" dependencies = [ "cfg-if", "once_cell", @@ -2508,9 +2332,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro" -version = "0.2.114" +version = "0.2.125" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "18a2d50fcf105fb33bb15f00e7a77b772945a2ee45dcf454961fd843e74c18e6" +checksum = "4e21a184b13fb19e157296e2c46056aec9092264fab83e4ba59e68c61b323c3d" dependencies = [ "quote", "wasm-bindgen-macro-support", @@ -2518,9 +2342,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.114" +version = "0.2.125" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "03ce4caeaac547cdf713d280eda22a730824dd11e6b8c3ca9e42247b25c631e3" +checksum = "fecefd9c35bd935a20fc3fc344b5f29138961e4f47fb03297d88f2587afb5ebd" dependencies = [ "bumpalo", "proc-macro2", @@ -2531,9 +2355,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-shared" -version = "0.2.114" +version = "0.2.125" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "75a326b8c223ee17883a4251907455a2431acc2791c98c26279376490c378c16" +checksum = "23939e44bb9a5d7576fa2b563dc2e136628f1224e88a8deed09e04858b77871f" dependencies = [ "unicode-ident", ] @@ -2566,7 +2390,7 @@ version = "0.244.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "47b807c72e1bac69382b3a6fb3dbe8ea4c0ed87ff5629b8685ae6b9a611028fe" dependencies = [ - "bitflags 2.11.0", + "bitflags 2.13.0", "hashbrown 0.15.5", "indexmap", "semver", @@ -2574,9 +2398,9 @@ dependencies = [ [[package]] name = "web-sys" -version = "0.3.91" +version = "0.3.102" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "854ba17bb104abfb26ba36da9729addc7ce7f06f5c0f90f3c391f8461cca21f9" +checksum = "a6430a72df5eb332242960fe84b3002a241163998241eb596d4f739b9757061d" dependencies = [ "js-sys", "wasm-bindgen", @@ -2691,15 +2515,6 @@ dependencies = [ "windows-targets", ] -[[package]] -name = "windows-sys" -version = "0.59.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" -dependencies = [ - "windows-targets", -] - [[package]] name = "windows-sys" version = "0.61.2" @@ -2782,6 +2597,12 @@ dependencies = [ "wit-bindgen-rust-macro", ] +[[package]] +name = "wit-bindgen" +version = "0.57.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e" + [[package]] name = "wit-bindgen-core" version = "0.51.0" @@ -2831,7 +2652,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9d66ea20e9553b30172b5e831994e35fbde2d165325bec84fc43dbf6f4eb9cb2" dependencies = [ "anyhow", - "bitflags 2.11.0", + "bitflags 2.13.0", "indexmap", "log", "serde", @@ -2861,45 +2682,15 @@ dependencies = [ "wasmparser", ] -[[package]] -name = "writeable" -version = "0.6.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9edde0db4769d2dc68579893f2306b26c6ecfbe0ef499b013d731b7b9247e0b9" - [[package]] name = "yansi" version = "1.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cfe53a6657fd280eaa890a3bc59152892ffa3e30101319d168b781ed6529b049" -[[package]] -name = "yoke" -version = "0.8.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72d6e5c6afb84d73944e5cedb052c4680d5657337201555f9f2a16b7406d4954" -dependencies = [ - "stable_deref_trait", - "yoke-derive", - "zerofrom", -] - -[[package]] -name = "yoke-derive" -version = "0.8.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b659052874eb698efe5b9e8cf382204678a0086ebf46982b79d6ca3182927e5d" -dependencies = [ - "proc-macro2", - "quote", - "syn", - "synstructure", -] - [[package]] name = "z3" version = "0.13.2" -source = "git+https://github.com/prove-rs/z3.rs.git?rev=8ae4720c2a2647bd7dca6a29fdec2fc4b69a5989#8ae4720c2a2647bd7dca6a29fdec2fc4b69a5989" dependencies = [ "log", "num", @@ -2909,7 +2700,6 @@ dependencies = [ [[package]] name = "z3-sys" version = "0.9.3" -source = "git+https://github.com/prove-rs/z3.rs.git?rev=8ae4720c2a2647bd7dca6a29fdec2fc4b69a5989#8ae4720c2a2647bd7dca6a29fdec2fc4b69a5989" dependencies = [ "bindgen", "cmake", @@ -2937,72 +2727,18 @@ dependencies = [ [[package]] name = "zerocopy" -version = "0.8.42" +version = "0.8.52" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f2578b716f8a7a858b7f02d5bd870c14bf4ddbbcf3a4c05414ba6503640505e3" +checksum = "ce1022995ff5ff5d841ad7d994facc23098cd40152f2c1d11cd607c6f530653f" dependencies = [ "zerocopy-derive", ] [[package]] name = "zerocopy-derive" -version = "0.8.42" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7e6cc098ea4d3bd6246687de65af3f920c430e236bee1e3bf2e441463f08a02f" -dependencies = [ - "proc-macro2", - "quote", - "syn", -] - -[[package]] -name = "zerofrom" -version = "0.1.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "50cc42e0333e05660c3587f3bf9d0478688e15d870fab3346451ce7f8c9fbea5" -dependencies = [ - "zerofrom-derive", -] - -[[package]] -name = "zerofrom-derive" -version = "0.1.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d71e5d6e06ab090c67b5e44993ec16b72dcbaabc526db883a360057678b48502" -dependencies = [ - "proc-macro2", - "quote", - "syn", - "synstructure", -] - -[[package]] -name = "zerotrie" -version = "0.2.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2a59c17a5562d507e4b54960e8569ebee33bee890c70aa3fe7b97e85a9fd7851" -dependencies = [ - "displaydoc", - "yoke", - "zerofrom", -] - -[[package]] -name = "zerovec" -version = "0.11.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6c28719294829477f525be0186d13efa9a3c602f7ec202ca9e353d310fb9a002" -dependencies = [ - "yoke", - "zerofrom", - "zerovec-derive", -] - -[[package]] -name = "zerovec-derive" -version = "0.11.2" +version = "0.8.52" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eadce39539ca5cb3985590102671f2567e659fca9666581ad3411d59207951f3" +checksum = "1ae7f38b72ec2a254e2b87ef277cf2cd4fb97cbebf944faa6f33354da0867930" dependencies = [ "proc-macro2", "quote", diff --git a/Cargo.toml b/Cargo.toml index a247b1f6..0ce132ec 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -91,5 +91,5 @@ opt-level = 3 # we need to have cargo fetch z3.rs from the git repository, otherwise it will # not download the git submodule with z3's sources in them. [patch.crates-io] -z3 = { git = 'https://github.com/prove-rs/z3.rs.git', rev = "8ae4720c2a2647bd7dca6a29fdec2fc4b69a5989" } -z3-sys = { git = 'https://github.com/prove-rs/z3.rs.git', rev = "8ae4720c2a2647bd7dca6a29fdec2fc4b69a5989" } +z3 = { path = 'z3.rs/z3' } +z3-sys = { path = 'z3.rs/z3-sys' } diff --git a/z3.rs b/z3.rs new file mode 160000 index 00000000..8ae4720c --- /dev/null +++ b/z3.rs @@ -0,0 +1 @@ +Subproject commit 8ae4720c2a2647bd7dca6a29fdec2fc4b69a5989 From fd87c5b6089d73388e496a67c9256968be981899 Mon Sep 17 00:00:00 2001 From: madita Date: Thu, 11 Jun 2026 15:49:34 +0200 Subject: [PATCH 02/11] ast/smt: add signed integer literals Adds a LitKind::Int variant, with parsing and SMT translation support. --- src/ast/expr.rs | 66 +++++++++++++++++++++++++++++++- src/ast/util.rs | 1 + src/front/parser/grammar.lalrpop | 3 ++ src/front/parser/parser_util.rs | 16 +++++++- src/mc/mod.rs | 3 ++ src/smt/translate_exprs.rs | 14 ++++--- src/tyctx.rs | 1 + src/vc/subst.rs | 2 +- 8 files changed, 95 insertions(+), 11 deletions(-) diff --git a/src/ast/expr.rs b/src/ast/expr.rs index 8c6bf235..ed504d59 100644 --- a/src/ast/expr.rs +++ b/src/ast/expr.rs @@ -2,7 +2,7 @@ use std::{fmt, str::FromStr}; -use num::{BigInt, BigRational, BigUint, One, Zero}; +use num::{BigInt, BigRational, BigUint, One, Signed, Zero}; use z3rro::eureal::ConcreteEUReal; use crate::{ @@ -373,6 +373,8 @@ pub enum LitKind { Str(Symbol), /// An unsigned integer literal (`123`). UInt(BigUint), + /// A signed integer literal (`123`). + Int(BigInt), /// A number literal represented by a fraction. Frac(BigRational), /// Infinity, @@ -393,6 +395,7 @@ impl LitKind { pub fn is_bot(&self) -> bool { match self { LitKind::UInt(num) => num.is_zero(), + LitKind::Int(num) => num.is_zero(), LitKind::Frac(frac) => frac.is_zero(), LitKind::Bool(b) => !b, _ => false, @@ -412,6 +415,33 @@ impl LitKind { _ => None, } } + + pub fn is_zero(&self) -> bool { + match self { + LitKind::UInt(num) => num.is_zero(), + LitKind::Int(num) => num.is_zero(), + LitKind::Frac(frac) => frac.is_zero(), + _ => false, + } + } + + pub fn is_one(&self) -> bool { + match self { + LitKind::UInt(num) => num.is_one(), + LitKind::Int(num) => num.is_one(), + LitKind::Frac(frac) => frac.is_one(), + _ => false, + } + } + + pub fn is_negative(&self) -> bool { + match self { + LitKind::UInt(_) => false, + LitKind::Int(num) => num.is_negative(), + LitKind::Frac(frac) => frac.is_negative(), + _ => false, + } + } } impl FromStr for LitKind { @@ -427,6 +457,7 @@ impl fmt::Display for LitKind { match self { LitKind::Str(symbol) => f.write_fmt(format_args!("\"{symbol}\"")), LitKind::UInt(num) => num.fmt(f), + LitKind::Int(num) => num.fmt(f), LitKind::Frac(frac) => frac.fmt(f), LitKind::Infinity => f.write_str("∞"), LitKind::Bool(b) => b.fmt(f), @@ -616,7 +647,7 @@ impl ExprBuilder { match ty { TyKind::Bool | TyKind::UInt | TyKind::UReal | TyKind::EUReal => self.bot_lit(ty), TyKind::Int => self.cast(TyKind::Int, self.uint(0)), - TyKind::Real => self.cast(TyKind::Real, self.frac_lit(Zero::zero())), + TyKind::Real => self.cast(TyKind::Real, self.frac_lit_not_extended(Zero::zero())), _ => panic!("type {ty} has no zero element"), } } @@ -649,6 +680,14 @@ impl ExprBuilder { }) } + pub fn int_lit(&self, value: BigInt) -> Expr { + Shared::new(ExprData { + kind: ExprKind::Lit(Spanned::new(self.span, LitKind::Int(value))), + ty: Some(TyKind::Int), + span: self.span, + }) + } + pub fn frac_lit(&self, value: BigRational) -> Expr { Shared::new(ExprData { kind: ExprKind::Lit(Spanned::new(self.span, LitKind::Frac(value))), @@ -656,6 +695,29 @@ impl ExprBuilder { span: self.span, }) } + + pub fn frac_lit_not_extended(&self, value: BigRational) -> Expr { + Shared::new(ExprData { + kind: ExprKind::Lit(Spanned::new(self.span, LitKind::Frac(value))), + ty: Some(TyKind::UReal), + span: self.span, + }) + } + + pub fn signed_frac_lit(&self, value: BigRational) -> Expr { + Shared::new(ExprData { + kind: ExprKind::Lit(Spanned::new(self.span, LitKind::Frac(value))), + ty: Some(TyKind::Real), + span: self.span, + }) + } + + pub fn abs_diff(&self, lhs: Expr, rhs: Expr, ty: TyKind) -> Expr { + let diff = self.binary(BinOpKind::Sub, Some(ty.clone()), lhs.clone(), rhs.clone()); + let neg_diff = self.binary(BinOpKind::Sub, Some(ty.clone()), rhs.clone(), lhs.clone()); + let ge = self.binary(BinOpKind::Ge, Some(TyKind::Bool), lhs, rhs); + self.ite(Some(ty), ge, diff, neg_diff) + } } #[cfg(test)] diff --git a/src/ast/util.rs b/src/ast/util.rs index 0e5490f7..e2eb5ea6 100644 --- a/src/ast/util.rs +++ b/src/ast/util.rs @@ -139,6 +139,7 @@ pub fn is_bot_lit(expr: &Expr) -> bool { } } + /// Remove [`ExprKind::Cast`] from this expression. This is mainly used to make /// the pretty-printed expression look less verbose. pub fn remove_casts(expr: &Expr) -> Expr { diff --git a/src/front/parser/grammar.lalrpop b/src/front/parser/grammar.lalrpop index 2bde2fec..c140f687 100644 --- a/src/front/parser/grammar.lalrpop +++ b/src/front/parser/grammar.lalrpop @@ -3,6 +3,7 @@ use crate::front::parser::parser_util::*; use std::str::FromStr; use std::cell::RefCell; use num::bigint::BigUint; +use num::BigInt; grammar( file: FileId, @@ -75,7 +76,9 @@ SymInfty: () = { "∞", "\\infty" } pub LitKind: LitKind = { => LitKind::Str(Symbol::intern(&s[1..s.len()-1])), => LitKind::UInt(BigUint::from_str(num).unwrap()), + "-" => LitKind::Int(-BigInt::from_str(num).unwrap()), => LitKind::Frac(parse_decimal(num).unwrap()), + "-" => LitKind::Frac(-parse_decimal(num).unwrap()), SymInfty => LitKind::Infinity, "true" => LitKind::Bool(true), "false" => LitKind::Bool(false), diff --git a/src/front/parser/parser_util.rs b/src/front/parser/parser_util.rs index 31e0419d..d6d8be0a 100644 --- a/src/front/parser/parser_util.rs +++ b/src/front/parser/parser_util.rs @@ -21,8 +21,20 @@ pub fn parse_decimal(num: &str) -> Result { let (integer, comma) = num.split_at(pos); let comma = &comma[1..]; // remove the dot let comma_len = u32::try_from(comma.len()).map_err(|_| DecimalParseError)?; - let numer: BigInt = - BigInt::from_str(&format!("{integer}{comma}")).map_err(|_| DecimalParseError)?; + + // Handle optional sign + let (sign, integer_digits) = if let Some(stripped) = integer.strip_prefix('-') { + (-1, stripped) + } else if let Some(stripped) = integer.strip_prefix('+') { + (1, stripped) + } else { + (1, integer) + }; + + let numer: BigInt = BigInt::from_str(&format!("{integer_digits}{comma}")) + .map_err(|_| DecimalParseError)? + * sign; + let denom: BigInt = BigInt::from(10).pow(comma_len); Ok(Ratio::new_raw(numer, denom)) } else { diff --git a/src/mc/mod.rs b/src/mc/mod.rs index a84a5d80..78d578e1 100644 --- a/src/mc/mod.rs +++ b/src/mc/mod.rs @@ -462,6 +462,9 @@ impl<'a> ExprTranslator<'a> { LitKind::UInt(val) => Ok(Expression::from( TryInto::::try_into(val).map_err(|_| unsupported_expr_err())?, )), + LitKind::Int(val) => Ok(Expression::from( + TryInto::::try_into(val).map_err(|_| unsupported_expr_err())?, + )), LitKind::Bool(val) => Ok(Expression::from(*val)), LitKind::Frac(frac) => Ok(Expression::from(BinaryExpression { op: BinaryOp::Divide, diff --git a/src/smt/translate_exprs.rs b/src/smt/translate_exprs.rs index 8ca7f14e..22f8d2ed 100644 --- a/src/smt/translate_exprs.rs +++ b/src/smt/translate_exprs.rs @@ -324,9 +324,10 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> { } ExprKind::Quant(_, _, _, _) => todo!(), ExprKind::Subst(_, _, _) => todo!(), - ExprKind::Lit(lit) => { - panic!("illegal exprkind {:?} of expression {:?}", &lit.node, &expr) - } + ExprKind::Lit(lit) => match &lit.node { + LitKind::Int(value) => Int::from_big_int(self.ctx.ctx, value), + _ => panic!("illegal exprkind {:?} of expression {:?}", &lit.node, &expr), + }, }; if is_expr_worth_caching(expr) { @@ -447,9 +448,10 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> { } ExprKind::Quant(_, _, _, _) => todo!(), ExprKind::Subst(_, _, _) => todo!(), - ExprKind::Lit(lit) => { - panic!("illegal exprkind {:?} of expression {:?}", &lit.node, &expr) - } + ExprKind::Lit(lit) => match &lit.node { + LitKind::Frac(frac) => Real::from_big_rational(self.ctx.ctx, frac), + _ => panic!("illegal exprkind {:?} of expression {:?}", &lit.node, &expr), + }, }; if is_expr_worth_caching(expr) { diff --git a/src/tyctx.rs b/src/tyctx.rs index 2352914d..e9a123ea 100644 --- a/src/tyctx.rs +++ b/src/tyctx.rs @@ -151,6 +151,7 @@ impl TyCtx { match lit { LitKind::Str(_) => TyKind::String, LitKind::UInt(_) => TyKind::UInt, + LitKind::Int(_) => TyKind::Int, LitKind::Frac(_) => TyKind::UReal, LitKind::Infinity => TyKind::EUReal, LitKind::Bool(_) => TyKind::Bool, diff --git a/src/vc/subst.rs b/src/vc/subst.rs index b497ebc2..5a121206 100644 --- a/src/vc/subst.rs +++ b/src/vc/subst.rs @@ -30,7 +30,7 @@ struct SubstFrame { /// A structure to apply variable substitutions in expressions. pub struct Subst<'a> { - tcx: &'a TyCtx, + pub tcx: &'a TyCtx, cur: SubstFrame, stack: Vec, pub limits_ref: LimitsRef, From 9ebe390abee3c1b2e46e93da0f7b20ef07863603 Mon Sep 17 00:00:00 2001 From: madita Date: Thu, 11 Jun 2026 15:48:13 +0200 Subject: [PATCH 03/11] ast: add range syntax Adds optional lower/upper bound ranges to parameters and variable declarations and restrict counterexamples to that range. --- src/ast/decl.rs | 11 ++++ src/ast/util.rs | 1 + src/driver/commands/verify.rs | 13 +++-- src/driver/mod.rs | 1 + src/driver/ranges.rs | 52 +++++++++++++++++++ src/driver/smt_proof.rs | 28 ++++++++-- src/front/parser/grammar.lalrpop | 38 ++++++++++++-- .../precedence_update/grammar_old.lalrpop | 8 +-- src/front/resolve.rs | 1 + src/opt/fuzz_test.rs | 1 + src/procs/spec_call.rs | 1 + src/proof_rules/mciver_ast.rs | 1 + src/proof_rules/omega.rs | 1 + src/proof_rules/util.rs | 4 ++ src/slicing/selection.rs | 1 + src/slicing/transform.rs | 1 + src/slicing/transform_test.rs | 1 + src/tyctx.rs | 2 +- 18 files changed, 150 insertions(+), 16 deletions(-) create mode 100644 src/driver/ranges.rs diff --git a/src/ast/decl.rs b/src/ast/decl.rs index b87d52e1..4ade3447 100644 --- a/src/ast/decl.rs +++ b/src/ast/decl.rs @@ -213,6 +213,12 @@ impl SimplePretty for DeclRef { } } +#[derive(Clone, Copy, Debug)] +pub struct Range { + pub lower: u64, + pub upper: u64, +} + /// A variable declaration consists of a name, a type, and a mutability kind, and /// an optional initial expression. #[derive(Debug, Clone)] @@ -225,6 +231,9 @@ pub struct VarDecl { /// If this declaration was created by cloning another variable declaration, /// we track the original name here. pub created_from: Option, + + // Optionally a range can be tracked to help invariant synthesis + pub range: Option, } impl VarDecl { @@ -237,6 +246,7 @@ impl VarDecl { init: None, span: param.span, created_from: None, + range: param.range.clone(), }; DeclRef::new(var_decl) } @@ -412,6 +422,7 @@ pub struct Param { pub ty: Box, pub literal_only: bool, pub span: Span, + pub range: Option, } impl SimplePretty for Param { diff --git a/src/ast/util.rs b/src/ast/util.rs index e2eb5ea6..6b91e3f4 100644 --- a/src/ast/util.rs +++ b/src/ast/util.rs @@ -187,6 +187,7 @@ mod test { init: None, span: Span::dummy_span(), created_from: None, + range: None, }))); let mut expr = builder.binary( BinOpKind::And, diff --git a/src/driver/commands/verify.rs b/src/driver/commands/verify.rs index 35ca7619..60597bc0 100644 --- a/src/driver/commands/verify.rs +++ b/src/driver/commands/verify.rs @@ -4,7 +4,7 @@ use clap::Args; use z3rro::{prover::ProveResult, util::ReasonUnknown}; use crate::{ - ast::FileId, + ast::{Expr, FileId}, driver::{ commands::{ mk_cli_server, @@ -20,7 +20,8 @@ use crate::{ front::parse_and_tycheck, item::Item, quant_proof::lower_quant_prove_task, - smt_proof::{run_smt_prove_task, set_global_z3_params}, + ranges::{collect_ranges_from_decls, create_range_constraint}, + smt_proof::{run_smt_prove_task_with_ranges, set_global_z3_params}, }, proof_rules::calculus::get_soundness_map, resource_limits::{await_with_resource_limits, LimitError, LimitsRef}, @@ -272,7 +273,12 @@ fn verify_files_main( let soundness_blame = &verify_unit.proc_soundness; // Running the SMT prove task: translating to Z3, running the solver. - let result = run_smt_prove_task( + let ranges = collect_ranges_from_decls(&tcx.declarations.borrow()); + let ranges_constraints: Vec = ranges + .iter() + .map(|(ident, (range, ty))| create_range_constraint(ident.clone(), range, ty.clone())) + .collect(); + let result = run_smt_prove_task_with_ranges( options, &limits_ref, &tcx, @@ -282,6 +288,7 @@ fn verify_files_main( slice_vars, vc_is_valid, soundness_blame, + &ranges_constraints, )?; // Handle reasons to stop the verifier. diff --git a/src/driver/mod.rs b/src/driver/mod.rs index 10b862c3..4fd27360 100644 --- a/src/driver/mod.rs +++ b/src/driver/mod.rs @@ -6,4 +6,5 @@ pub mod error; pub mod front; pub mod item; pub mod quant_proof; +pub mod ranges; pub mod smt_proof; diff --git a/src/driver/ranges.rs b/src/driver/ranges.rs new file mode 100644 index 00000000..d138f686 --- /dev/null +++ b/src/driver/ranges.rs @@ -0,0 +1,52 @@ +use std::rc::Rc; + +use indexmap::IndexMap; +use num::BigRational; + +use crate::ast::{BinOpKind, DeclKind, Expr, ExprBuilder, Ident, Range, Span, TyKind}; + +/// Builds a Boolean expression `range.lower <= ident <= range.upper` in type `ty`. +pub fn create_range_constraint(ident: Ident, range: &Range, ty: TyKind) -> Expr { + let builder = ExprBuilder::new(Span::dummy_span()); + + let (var, lower_lit, upper_lit) = match ty { + TyKind::UReal => { + let var = builder.var_ty(ident.clone(), TyKind::UReal); + let lower = + builder.frac_lit_not_extended(BigRational::from_integer(range.lower.into())); + let upper = + builder.frac_lit_not_extended(BigRational::from_integer(range.upper.into())); + (var, lower, upper) + } + _ => { + let var = builder.var_ty(ident.clone(), TyKind::UInt); + let lower = builder.uint(range.lower.into()); + let upper = builder.uint(range.upper.into()); + (var, lower, upper) + } + }; + + let lower = builder.binary(BinOpKind::Le, Some(TyKind::Bool), lower_lit, var.clone()); + + let upper = builder.binary(BinOpKind::Le, Some(TyKind::Bool), var, upper_lit); + + builder.binary(BinOpKind::And, Some(TyKind::Bool), lower, upper) +} + +/// Returns a map from variable identifiers to their declared `(Range, TyKind)` pairs. +pub fn collect_ranges_from_decls( + declarations: &IndexMap>, +) -> IndexMap { + let mut ranges = IndexMap::new(); + + for (ident, decl) in declarations.iter() { + if let DeclKind::VarDecl(var_ref) = decl.as_ref() { + let var = var_ref.borrow(); + if let Some(range) = &var.range { + ranges.insert(*ident, (range.clone(), var.ty.clone())); + } + } + } + + ranges +} diff --git a/src/driver/smt_proof.rs b/src/driver/smt_proof.rs index 98d5842b..e790577b 100644 --- a/src/driver/smt_proof.rs +++ b/src/driver/smt_proof.rs @@ -27,6 +27,7 @@ use crate::driver::commands::options::{ use crate::driver::commands::verify::VerifyCommand; use crate::driver::error::CaesarError; use crate::driver::item::SourceUnitName; +use crate::ast::Expr; use crate::driver::quant_proof::{BoolVcProveTask, QuantVcProveTask}; use crate::proof_rules::calculus::ProcSoundness; use crate::slicing::transform::SliceStmts; @@ -147,6 +148,21 @@ pub fn run_smt_prove_task( slice_vars: SliceStmts, vc_is_valid: BoolVcProveTask, proc_soundness: &ProcSoundness, +) -> Result { + run_smt_prove_task_with_ranges(options, limits_ref, tcx, depgraph, name, server, slice_vars, vc_is_valid, proc_soundness, &[]) +} + +pub fn run_smt_prove_task_with_ranges( + options: &VerifyCommand, + limits_ref: &LimitsRef, + tcx: &TyCtx, + depgraph: &DepGraph, + name: &SourceUnitName, + server: &mut dyn Server, + slice_vars: SliceStmts, + vc_is_valid: BoolVcProveTask, + proc_soundness: &ProcSoundness, + ranges_constraints: &[Expr], ) -> Result { let ctx = Context::new(&z3::Config::default()); let function_encoder = mk_function_encoder(tcx, depgraph, options)?; @@ -164,7 +180,7 @@ pub fn run_smt_prove_task( } let mut result = - vc_is_valid.run_solver(options, limits_ref, name, &ctx, &mut translate, &slice_vars)?; + vc_is_valid.run_solver_with_ranges(options, limits_ref, name, &ctx, &mut translate, &slice_vars,ranges_constraints)?; server .handle_vc_check_result(name, &mut result, &mut translate, proc_soundness) @@ -297,7 +313,7 @@ impl<'ctx> SmtVcProveTask<'ctx> { } /// Run the solver(s) on this SMT formula. - pub fn run_solver<'smt>( + pub fn run_solver_with_ranges<'smt>( self, options: &VerifyCommand, limits_ref: &LimitsRef, @@ -305,19 +321,23 @@ impl<'ctx> SmtVcProveTask<'ctx> { ctx: &'ctx Context, translate: &mut TranslateExprs<'smt, 'ctx>, slice_vars: &SliceStmts, + ranges_constraints: &[Expr], ) -> Result, CaesarError> { let span = info_span!("SAT check"); let _entered = span.enter(); - let prover = mk_valid_query_prover(limits_ref, ctx, translate, &self.vc); + let mut prover = mk_valid_query_prover(limits_ref, ctx, translate, &self.vc); + for constraint in ranges_constraints { + prover.add_assumption(&translate.t_bool(&constraint)); + } if options.debug_options.z3_probe { let goal = Goal::new(ctx, false, false, false); for assertion in prover.get_assertions() { goal.assert(&assertion); } eprintln!( - "Probe results for {}:\n{}", + "In verifier (getting pvar cex): Probe results for {}:\n{}", name, ProbeSummary::probe(ctx, &goal) ); diff --git a/src/front/parser/grammar.lalrpop b/src/front/parser/grammar.lalrpop index c140f687..0682e0e9 100644 --- a/src/front/parser/grammar.lalrpop +++ b/src/front/parser/grammar.lalrpop @@ -44,6 +44,13 @@ Ident: Ident = { }, } +Range: Range = + "[" "," "]" + => Range { + lower: lo.parse::().expect("range lower bound does not fit in u64"), + upper: hi.parse::().expect("range upper bound does not fit in u64"), + }; + // --------------------------------------- // Types @@ -174,7 +181,7 @@ QuantOp: QuantOp = { QuantVar: QuantVar = { ":" - => QuantVar::Fresh(DeclRef::new(VarDecl { name, ty, kind: VarKind::Quant, init: None, span: span(file, l, r), created_from: None })) + => QuantVar::Fresh(DeclRef::new(VarDecl { name, ty, kind: VarKind::Quant, init: None, span: span(file, l, r), created_from: None, range: None })) } QuantAnn: QuantAnn = { @@ -203,9 +210,31 @@ pub SpannedStmts: Spanned> = { StmtKind: StmtKind = { => StmtKind::Seq(block.node), "var" ":" "=" - => StmtKind::Var(DeclRef::new(VarDecl { name: ident, ty, kind: VarKind::Mut, init: Some(rhs), span: span(file, l, r), created_from: None })), + => StmtKind::Var(DeclRef::new(VarDecl { name: ident, ty, kind: VarKind::Mut, init: Some(rhs), span: span(file, l, r), created_from: None, range: None })), "var" ":" - => StmtKind::Var(DeclRef::new(VarDecl { name: ident, ty, kind: VarKind::Mut, init: None, span: span(file, l, r), created_from: None })), + => StmtKind::Var(DeclRef::new(VarDecl { name: ident, ty, kind: VarKind::Mut, init: None, span: span(file, l, r), created_from: None, range: None})), + "var" ":" "=" + => StmtKind::Var(DeclRef::new(VarDecl { + name: ident, + ty, + kind: VarKind::Mut, + init: Some(rhs), + span: span(file, l, r), + created_from: None, + range: Some(rng), + })), + + "var" ":" + => StmtKind::Var(DeclRef::new(VarDecl { + name: ident, + ty, + kind: VarKind::Mut, + init: None, + span: span(file, l, r), + created_from: None, + range: Some(rng), + })), + > "=" => StmtKind::Assign(lhs, rhs), "(" > ")" => { let call = Shared::new(ExprData { @@ -271,7 +300,8 @@ ParamList: Spanned> = { } Param: Param = { - ":" => Param { name, ty: Box::new(ty), literal_only: false ,span: span(file, l, r) } + ":" => Param { name, ty: Box::new(ty), literal_only: false ,span: span(file, l, r), range: None }, + ":" => Param { name, ty: Box::new(ty), literal_only: false ,span: span(file, l, r), range: Some(rng) }, } ProcSpec: ProcSpec = { diff --git a/src/front/parser/precedence_update/grammar_old.lalrpop b/src/front/parser/precedence_update/grammar_old.lalrpop index 94036527..7442ff16 100644 --- a/src/front/parser/precedence_update/grammar_old.lalrpop +++ b/src/front/parser/precedence_update/grammar_old.lalrpop @@ -87,7 +87,7 @@ QuantOp: QuantOp = { QuantVar: QuantVar = { ":" - => QuantVar::Fresh(DeclRef::new(VarDecl { name, ty, kind: VarKind::Quant, init: None, span: span(file, l, r), created_from: None })) + => QuantVar::Fresh(DeclRef::new(VarDecl { name, ty, kind: VarKind::Quant, init: None, span: span(file, l, r), created_from: None, range: None })) } QuantAnn: QuantAnn = { @@ -193,9 +193,9 @@ pub SpannedStmts: Spanned> = { StmtKind: StmtKind = { => StmtKind::Seq(block.node), "var" ":" "=" - => StmtKind::Var(DeclRef::new(VarDecl { name: ident, ty, kind: VarKind::Mut, init: Some(rhs), span: span(file, l, r), created_from: None })), + => StmtKind::Var(DeclRef::new(VarDecl { name: ident, ty, kind: VarKind::Mut, init: Some(rhs), span: span(file, l, r), created_from: None, range: None })), "var" ":" - => StmtKind::Var(DeclRef::new(VarDecl { name: ident, ty, kind: VarKind::Mut, init: None, span: span(file, l, r), created_from: None })), + => StmtKind::Var(DeclRef::new(VarDecl { name: ident, ty, kind: VarKind::Mut, init: None, span: span(file, l, r), created_from: None, range: None })), > "=" => StmtKind::Assign(lhs, rhs), > => StmtKind::Assign(vec![], call), "havoc" > => StmtKind::Havoc(Direction::Down, vars), @@ -254,7 +254,7 @@ ParamList: Spanned> = { } Param: Param = { - ":" => Param { name, ty: Box::new(ty), literal_only: false ,span: span(file, l, r) } + ":" => Param { name, ty: Box::new(ty), literal_only: false ,span: span(file, l, r), range: None } } ProcSpec: ProcSpec = { diff --git a/src/front/resolve.rs b/src/front/resolve.rs index f183b9e8..29cc07ad 100644 --- a/src/front/resolve.rs +++ b/src/front/resolve.rs @@ -283,6 +283,7 @@ impl<'tcx> VisitorMut for Resolve<'tcx> { init: Some(val.clone()), span, created_from: None, + range: None, })); self.with_subscope(|this| { this.declare(decl)?; diff --git a/src/opt/fuzz_test.rs b/src/opt/fuzz_test.rs index e987de41..cf71e713 100644 --- a/src/opt/fuzz_test.rs +++ b/src/opt/fuzz_test.rs @@ -68,6 +68,7 @@ impl ExprGen { init: None, span: Span::dummy_span(), created_from: None, + range: None, }))) }); } diff --git a/src/procs/spec_call.rs b/src/procs/spec_call.rs index 9d3d497a..1c85f255 100644 --- a/src/procs/spec_call.rs +++ b/src/procs/spec_call.rs @@ -247,6 +247,7 @@ impl<'tcx> SpecCall<'tcx> { init: Some(value), span, created_from: Some(param.name), + range: None, }; let decl = DeclRef::new(var_decl); self.tcx.declare(DeclKind::VarDecl(decl.clone())); diff --git a/src/proof_rules/mciver_ast.rs b/src/proof_rules/mciver_ast.rs index 05691ff9..117fa5d7 100644 --- a/src/proof_rules/mciver_ast.rs +++ b/src/proof_rules/mciver_ast.rs @@ -101,6 +101,7 @@ impl Encoding for ASTAnnotation { init: None, span: call_span, created_from: None, + range: None, }; // Declare the free variable to be used in the omega invariant resolve.declare(DeclKind::VarDecl(DeclRef::new(var_decl)))?; diff --git a/src/proof_rules/omega.rs b/src/proof_rules/omega.rs index a76270ab..2101274c 100644 --- a/src/proof_rules/omega.rs +++ b/src/proof_rules/omega.rs @@ -80,6 +80,7 @@ impl Encoding for OmegaInvAnnotation { init: None, span: call_span, created_from: None, + range: None, }; // Declare the free variable to be used in the omega invariant resolve.declare(DeclKind::VarDecl(DeclRef::new(var_decl)))?; diff --git a/src/proof_rules/util.rs b/src/proof_rules/util.rs index 191453eb..5f67c1d0 100644 --- a/src/proof_rules/util.rs +++ b/src/proof_rules/util.rs @@ -115,6 +115,7 @@ pub fn new_ident_with_name(tcx: &TyCtx, ty: &TyKind, span: Span, name: &str) -> init: None, span, created_from: None, + range: None, }; let decl = DeclRef::new(var_decl); tcx.declare(DeclKind::VarDecl(decl)); @@ -148,6 +149,7 @@ pub fn get_init_idents(tcx: &TyCtx, span: Span, idents: &[Ident]) -> Vec init: None, span, created_from: Some(*ident), + range: None, }; let decl = DeclRef::new(var_decl); tcx.declare(DeclKind::VarDecl(decl.clone())); @@ -324,6 +326,7 @@ pub fn intrinsic_param(file: FileId, name: &str, ty: TyKind, literal_only: bool) ty: Box::new(ty), literal_only, span: Span::dummy_file_span(file), + range: None, } } @@ -340,6 +343,7 @@ pub fn params_from_idents(idents: Vec, tcx: &TyCtx) -> Vec { ty: Box::new(var.ty.clone()), literal_only: false, span: ident.span, + range: None, }) } } diff --git a/src/slicing/selection.rs b/src/slicing/selection.rs index cd13877a..ada8156d 100644 --- a/src/slicing/selection.rs +++ b/src/slicing/selection.rs @@ -128,6 +128,7 @@ impl SliceAnnotation { ty: Box::new(TyKind::String), literal_only: true, span: Span::dummy_span(), + range: None, }]), span: Span::dummy_span(), } diff --git a/src/slicing/transform.rs b/src/slicing/transform.rs index 8e8fe7f1..38f1c317 100644 --- a/src/slicing/transform.rs +++ b/src/slicing/transform.rs @@ -138,6 +138,7 @@ impl<'tcx> StmtSliceVisitor<'tcx> { init: None, span, created_from: None, + range: None, }))); // return a variable expression with that new ident diff --git a/src/slicing/transform_test.rs b/src/slicing/transform_test.rs index af794b4f..8836eed6 100644 --- a/src/slicing/transform_test.rs +++ b/src/slicing/transform_test.rs @@ -90,6 +90,7 @@ impl TransformTestCtx { init: None, span: Span::dummy_span(), created_from: None, + range: None, }))) } Self { diff --git a/src/tyctx.rs b/src/tyctx.rs index e9a123ea..1811fe85 100644 --- a/src/tyctx.rs +++ b/src/tyctx.rs @@ -23,7 +23,7 @@ pub struct TyCtx { /// /// It's an [`IndexMap`] to ensure stable iteration order over declarations. /// This keeps the SMT-LIB output deterministic. - declarations: RefCell>>, + pub declarations: RefCell>>, /// Global identifiers are those that are available in every new resolver at /// the top scope. Adding a global is essentially an "export" of a source /// and initializing a resolver with them is using "imports". From 881d2f748c64830b22aba6cb004230bdf32b21c4 Mon Sep 17 00:00:00 2001 From: madita Date: Thu, 11 Jun 2026 15:50:13 +0200 Subject: [PATCH 04/11] ast: add syn function declarations Adds a syn func declaration form for marking functions as synthesis targets. --- src/ast/decl.rs | 1 + src/front/parser/grammar.lalrpop | 6 ++-- .../precedence_update/grammar_old.lalrpop | 4 +-- src/smt/mod.rs | 10 ++++-- src/smt/uninterpreted.rs | 33 +++++++++++++++---- 5 files changed, 41 insertions(+), 13 deletions(-) diff --git a/src/ast/decl.rs b/src/ast/decl.rs index 4ade3447..976b7a9f 100644 --- a/src/ast/decl.rs +++ b/src/ast/decl.rs @@ -513,6 +513,7 @@ pub struct FuncDecl { /// well. Functions with bodies are always computable, but this field will /// be `false` (because not explicitly marked). pub computable: bool, + pub syn: bool, pub span: Span, } diff --git a/src/front/parser/grammar.lalrpop b/src/front/parser/grammar.lalrpop index 0682e0e9..948b28f7 100644 --- a/src/front/parser/grammar.lalrpop +++ b/src/front/parser/grammar.lalrpop @@ -316,9 +316,11 @@ DomainDecl: DomainDecl = { DomainSpec: DomainSpec = { "func" ":" - => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output, body: RefCell::new(None), computable: comp.is_some(), span: span(file, l, r) })), + => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output, body: RefCell::new(None), syn: false, computable: comp.is_some(), span: span(file, l, r) })), "func" ":" "=" - => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output, body: RefCell::new(Some(body)), computable: false, span: span(file, l, r) })), + => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output, body: RefCell::new(Some(body)), syn: false, computable: false, span: span(file, l, r) })), + "syn" "func" ":" + => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output: output, body: RefCell::new(None), syn: true, computable: false, span: span(file, l, r) })), "axiom" => DomainSpec::Axiom(DeclRef::new(AxiomDecl{ name, axiom, span: span(file, l, r) })) } diff --git a/src/front/parser/precedence_update/grammar_old.lalrpop b/src/front/parser/precedence_update/grammar_old.lalrpop index 7442ff16..852c286f 100644 --- a/src/front/parser/precedence_update/grammar_old.lalrpop +++ b/src/front/parser/precedence_update/grammar_old.lalrpop @@ -269,9 +269,9 @@ DomainDecl: DomainDecl = { DomainSpec: DomainSpec = { "func" ":" - => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output, body: RefCell::new(None), computable: comp.is_some(), span: span(file, l, r) })), + => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output, body: RefCell::new(None), syn: false, computable: comp.is_some(), span: span(file, l, r) })), "func" ":" "=" - => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output, body: RefCell::new(Some(body)), computable: false, span: span(file, l, r) })), + => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output, body: RefCell::new(Some(body)), syn: false, computable: false, span: span(file, l, r) })), "axiom" => DomainSpec::Axiom(DeclRef::new(AxiomDecl{ name, axiom, span: span(file, l, r) })) } diff --git a/src/smt/mod.rs b/src/smt/mod.rs index 1ad07517..b3a9bd45 100644 --- a/src/smt/mod.rs +++ b/src/smt/mod.rs @@ -22,7 +22,7 @@ pub mod pretty_model; pub mod symbolic; mod symbols; pub mod translate_exprs; -mod uninterpreted; +pub mod uninterpreted; /// Which dependencies to include in the SMT context. #[derive(Debug)] @@ -101,7 +101,13 @@ impl<'ctx> SmtCtx<'ctx> { self.function_encoder.translate_signature(self, &func) { let domain = domain.iter().collect_vec(); - self.uninterpreteds.add_function(name, &domain, &range) + self.uninterpreteds.add_function( + name, + &domain, + &range, + func.syn, + func.inputs.clone(), + ) } } } diff --git a/src/smt/uninterpreted.rs b/src/smt/uninterpreted.rs index 62b8eeee..79e7aac4 100644 --- a/src/smt/uninterpreted.rs +++ b/src/smt/uninterpreted.rs @@ -1,6 +1,6 @@ //! Uninterpreted sorts and functions. -use std::collections::HashMap; +use indexmap::IndexMap; use z3::{ ast::{Ast, Bool, Dynamic}, @@ -8,7 +8,7 @@ use z3::{ }; use z3rro::prover::Prover; -use crate::ast::Ident; +use crate::ast::{Ident, Param, Spanned}; use super::symbols::Symbolizer; @@ -17,11 +17,18 @@ use super::symbols::Symbolizer; pub struct Uninterpreteds<'ctx> { ctx: &'ctx Context, symbolizer: Symbolizer, - sorts: HashMap>, - functions: HashMap>, + sorts: IndexMap>, + pub functions: IndexMap>, axioms: Vec<(Ident, Bool<'ctx>)>, } +#[derive(Debug)] +pub struct FuncEntry<'ctx> { + pub(crate) decl: FuncDecl<'ctx>, + pub(crate) syn: bool, + pub inputs: Spanned>, +} + impl<'ctx> Uninterpreteds<'ctx> { pub fn new(ctx: &'ctx Context) -> Self { Self { @@ -32,6 +39,9 @@ impl<'ctx> Uninterpreteds<'ctx> { axioms: Default::default(), } } + pub fn functions(&self) -> &IndexMap> { + &self.functions + } pub fn add_sort(&mut self, ident: Ident) { let symbol = self.symbolizer.get(ident); @@ -40,10 +50,19 @@ impl<'ctx> Uninterpreteds<'ctx> { assert!(prev.is_none()); } - pub fn add_function(&mut self, ident: Ident, domain: &[&Sort<'ctx>], range: &Sort<'ctx>) { + pub fn add_function( + &mut self, + ident: Ident, + domain: &[&Sort<'ctx>], + range: &Sort<'ctx>, + syn: bool, + inputs: Spanned>, + ) { let symbol = self.symbolizer.get(ident); let decl = FuncDecl::new(self.ctx, symbol, domain, range); - let prev = self.functions.insert(ident, decl); + let prev = self + .functions + .insert(ident, FuncEntry { decl, syn, inputs }); assert!(prev.is_none()); } @@ -56,7 +75,7 @@ impl<'ctx> Uninterpreteds<'ctx> { .functions .get(&ident) .unwrap_or_else(|| panic!("function {ident} is not declared")); - decl.apply(args) + decl.decl.apply(args) } pub fn add_axiom(&mut self, ident: Ident, axiom: Bool<'ctx>) { From 099b78cac73948669c85f9f6fea5966acada919e Mon Sep 17 00:00:00 2001 From: madita Date: Wed, 10 Jun 2026 17:05:15 +0200 Subject: [PATCH 05/11] ast: RemoveCastsVisitor strips nested casts Fully unwrapped nested casts in a single visitor pass. --- src/ast/util.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/util.rs b/src/ast/util.rs index 6b91e3f4..a309a98a 100644 --- a/src/ast/util.rs +++ b/src/ast/util.rs @@ -154,7 +154,7 @@ impl VisitorMut for RemoveCastsVisitor { type Err = (); fn visit_expr(&mut self, e: &mut Expr) -> Result<(), Self::Err> { - if let ExprKind::Cast(inner) = &mut e.kind { + while let ExprKind::Cast(inner) = &mut e.kind { *e = inner.clone(); } walk_expr(self, e) From 4bd4321c9f7b8b7ed9f4b259fd9e0f57bdb1a3a0 Mon Sep 17 00:00:00 2001 From: madita Date: Wed, 10 Jun 2026 10:43:06 +0200 Subject: [PATCH 06/11] intrinsic: add nonneg_cast Adds a nonneg_cast intrinsic that reinterprets a signed Int/Real as UInt/UReal. It's an unchecked cast that requires the user to ensure the validity themselves. --- src/driver/front.rs | 6 ++- src/intrinsic/mod.rs | 1 + src/intrinsic/nonneg_cast.rs | 102 +++++++++++++++++++++++++++++++++++ 3 files changed, 108 insertions(+), 1 deletion(-) create mode 100644 src/intrinsic/nonneg_cast.rs diff --git a/src/driver/front.rs b/src/driver/front.rs index 06c095a5..511eb22b 100644 --- a/src/driver/front.rs +++ b/src/driver/front.rs @@ -30,7 +30,10 @@ use crate::{ resolve::Resolve, tycheck::Tycheck, }, - intrinsic::{annotations::init_calculi, distributions::init_distributions, list::init_lists}, + intrinsic::{ + annotations::init_calculi, distributions::init_distributions, list::init_lists, + nonneg_cast::init_nonneg_cast, + }, mc, pretty::{Doc, SimplePretty}, procs::monotonicity::MonotonicityVisitor, @@ -301,6 +304,7 @@ pub fn init_tcx(files: &mut Files) -> TyCtx { init_encodings(files, &mut tcx); init_distributions(files, &mut tcx); init_lists(files, &mut tcx); + init_nonneg_cast(files, &mut tcx); init_slicing(&mut tcx); tcx } diff --git a/src/intrinsic/mod.rs b/src/intrinsic/mod.rs index c8a4bff1..c50d1e49 100644 --- a/src/intrinsic/mod.rs +++ b/src/intrinsic/mod.rs @@ -8,6 +8,7 @@ pub mod annotations; pub mod distributions; pub mod list; +pub mod nonneg_cast; use std::{any::Any, fmt, rc::Rc}; diff --git a/src/intrinsic/nonneg_cast.rs b/src/intrinsic/nonneg_cast.rs new file mode 100644 index 00000000..ff9ace7a --- /dev/null +++ b/src/intrinsic/nonneg_cast.rs @@ -0,0 +1,102 @@ +//! Intrinsic for casting a signed expression to its unsigned counterpart +//! (Int -> UInt, Real -> UReal) without a bounds check. The non-negativity +//! obligation is added to the VC separately. + +use std::rc::Rc; + +use z3rro::{UInt, UReal}; + +use crate::{ + ast::{DeclKind, Expr, Files, Ident, Span, Symbol, TyKind}, + front::tycheck::{Tycheck, TycheckError}, + smt::{symbolic::Symbolic, translate_exprs::TranslateExprs}, + tyctx::TyCtx, +}; + +use super::FuncIntrin; + +pub fn init_nonneg_cast(_files: &mut Files, tcx: &mut TyCtx) { + let nonneg_cast_name = Ident::with_dummy_span(Symbol::intern("nonneg_cast")); + let nonneg_cast = NonnegCastIntrin(nonneg_cast_name); + tcx.declare(DeclKind::FuncIntrin(Rc::new(nonneg_cast))); + tcx.add_global(nonneg_cast_name); +} + +/// Unchecked cast from Int/Real to UInt/UReal. The argument must be >= 0; +/// this is tracked as a separate obligation added to the VC. +#[derive(Debug)] +pub struct NonnegCastIntrin(Ident); + +impl FuncIntrin for NonnegCastIntrin { + fn name(&self) -> Ident { + self.0 + } + + fn tycheck( + &self, + tycheck: &mut Tycheck<'_>, + call_span: Span, + args: &mut [Expr], + ) -> Result { + let x = if let [ref mut x] = args { + x + } else { + return Err(TycheckError::ArgumentCountMismatch { + span: call_span, + callee: args.len(), + caller: 1, + }); + }; + + if tycheck.try_cast(call_span, &TyKind::Int, x).is_ok() { + Ok(TyKind::UInt) + } else { + tycheck.try_cast(call_span, &TyKind::Real, x)?; + Ok(TyKind::UReal) + } + } + + fn translate_call<'smt, 'ctx>( + &self, + translate: &mut TranslateExprs<'smt, 'ctx>, + args: &[Expr], + ) -> Symbolic<'ctx> { + let ty = &args[0].ty; + + match ty { + Some(TyKind::Int) => { + let x = translate.t_int(&args[0]); + Symbolic::UInt(UInt::unchecked_from_int(x)) + } + + Some(TyKind::UInt) => { + let x_uint = translate.t_uint(&args[0]); + let x = x_uint.as_int(); + Symbolic::UInt(UInt::unchecked_from_int(x.clone())) + } + + Some(TyKind::Real) => { + let x = translate.t_real(&args[0]); + let value = UReal::unchecked_from_real(x); + Symbolic::UReal(value) + } + + Some(TyKind::UReal) => { + let x = translate.t_ureal(&args[0]); + let x = x.as_real(); + let value = UReal::unchecked_from_real(x.clone()); + Symbolic::UReal(value) + } + + Some(TyKind::EUReal) => { + let x = translate.t_eureal(&args[0]); + let x = x.get_ureal(); + let x = x.as_real(); + let value = UReal::unchecked_from_real(x.clone()); + Symbolic::UReal(value) + } + + _ => unreachable!("nonneg_cast only defined for numeric types"), + } + } +} From 299e71fac5da86490352ec173782608a46e4d20a Mon Sep 17 00:00:00 2001 From: madita Date: Wed, 10 Jun 2026 10:43:06 +0200 Subject: [PATCH 07/11] smt: translate Iverson brackets to numeric types Adds SMT handlers for [cond] in Int, UInt, Real, and UReal contexts, encoding them as branch-on-condition with 0/1 values. --- src/smt/translate_exprs.rs | 35 ++++++++++++++++++++++++++++++++--- 1 file changed, 32 insertions(+), 3 deletions(-) diff --git a/src/smt/translate_exprs.rs b/src/smt/translate_exprs.rs index 22f8d2ed..cb3fcc77 100644 --- a/src/smt/translate_exprs.rs +++ b/src/smt/translate_exprs.rs @@ -10,8 +10,8 @@ use z3::{ use crate::{ ast::{ - util::FreeVariableCollector, BinOpKind, DeclKind, Expr, ExprKind, Ident, LitKind, - QuantOpKind, QuantVar, Shared, Trigger, TyKind, UnOpKind, + util::FreeVariableCollector, BinOpKind, DeclKind, Expr, ExprBuilder, ExprKind, Ident, + LitKind, QuantOpKind, QuantVar, Shared, Span, Trigger, TyKind, UnOpKind, }, scope_map::ScopeMap, smt::funcs::fuel::literals::LiteralExprSet, @@ -310,6 +310,14 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> { }, ExprKind::Unary(un_op, operand) => match un_op.node { UnOpKind::Parens => self.t_int(operand), + UnOpKind::Iverson => { + let builder = ExprBuilder::new(Span::dummy_span()); + + let cond = self.t_bool(operand); + let lhs = self.t_int(&builder.one_lit(&TyKind::Int)); + let rhs = self.t_int(&builder.zero_lit(&TyKind::Int)); + Int::branch(&cond, &lhs, &rhs) + } _ => panic!("illegal exprkind {:?} of expression {:?}", un_op, &expr), }, ExprKind::Cast(operand) => { @@ -371,6 +379,14 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> { }, ExprKind::Unary(un_op, operand) => match un_op.node { UnOpKind::Parens => self.t_uint(operand), + UnOpKind::Iverson => { + let builder = ExprBuilder::new(Span::dummy_span()); + + let cond = self.t_bool(operand); + let lhs = self.t_uint(&builder.one_lit(&TyKind::UInt)); + let rhs = self.t_uint(&builder.zero_lit(&TyKind::UInt)); + UInt::branch(&cond, &lhs, &rhs) + } _ => panic!("illegal exprkind"), }, ExprKind::Cast(operand) => { @@ -426,6 +442,13 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> { }, ExprKind::Unary(un_op, operand) => match un_op.node { UnOpKind::Parens => self.t_real(operand), + UnOpKind::Iverson => { + let operand = self.t_bool(operand); + EUReal::iverson(self.ctx.eureal(), &operand) + .get_ureal() + .as_real() + .clone() + } _ => panic!("illegal exprkind {:?} of expression {:?}", un_op, &expr), }, ExprKind::Cast(operand) => { @@ -500,6 +523,12 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> { }, ExprKind::Unary(un_op, operand) => match un_op.node { UnOpKind::Parens => self.t_ureal(operand), + UnOpKind::Iverson => { + let operand = self.t_bool(operand); + EUReal::iverson(self.ctx.eureal(), &operand) + .get_ureal() + .clone() + } _ => panic!("illegal exprkind {:?} of expression {:?}", un_op, &expr), }, ExprKind::Cast(operand) => { @@ -851,4 +880,4 @@ impl<'ctx> TranslateCache<'ctx> { } } -type CacheExpr = RefEqShared; +type CacheExpr = RefEqShared; \ No newline at end of file From a0fe56bd88ac4c5dd742038a74ec912e68223501 Mon Sep 17 00:00:00 2001 From: madita Date: Thu, 11 Jun 2026 15:57:59 +0200 Subject: [PATCH 08/11] opt: add NeutralsRemover optimizer Introduces NeutralsRemover, which eliminates zero/infinity neutral elements using SMT-guided rewrites. Wires it into the quantitative proving pipeline and makes TyCtx references immutable throughout. --- src/ast/util.rs | 58 ++++++++ src/driver/quant_proof.rs | 30 +++- src/opt/mod.rs | 1 + src/opt/qelim.rs | 4 +- src/opt/remove_neutrals.rs | 289 +++++++++++++++++++++++++++++++++++++ 5 files changed, 375 insertions(+), 7 deletions(-) create mode 100644 src/opt/remove_neutrals.rs diff --git a/src/ast/util.rs b/src/ast/util.rs index a309a98a..d5df0544 100644 --- a/src/ast/util.rs +++ b/src/ast/util.rs @@ -1,6 +1,8 @@ // Using [`IndexSet`], which is a HashSet that preserves the insertion order, for deterministic results use indexmap::IndexSet; +use crate::ast::UnOpKind; + use super::{ visit::{walk_expr, walk_stmt, VisitorMut}, Direction, Expr, ExprKind, Ident, StmtKind, @@ -139,6 +141,62 @@ pub fn is_bot_lit(expr: &Expr) -> bool { } } +pub fn is_zero_lit(expr: &Expr) -> bool { + match &expr.kind { + ExprKind::Lit(lit) => lit.node.is_zero(), + ExprKind::Cast(inner) => match &inner.kind { + ExprKind::Lit(lit) => lit.node.is_zero(), + _ => false, + }, + ExprKind::Unary(un_op, inner) => match un_op.node { + UnOpKind::Parens => is_zero_lit(inner), + _ => false, + }, + _ => false, + } +} + +pub fn is_lit(expr: &Expr) -> bool { + match &expr.kind { + ExprKind::Lit(_) => true, + ExprKind::Cast(inner) => is_lit(inner), + ExprKind::Unary(un_op, inner) => match un_op.node { + UnOpKind::Parens => is_lit(inner), + _ => false, + }, + _ => false, + } +} + +pub fn is_neg_lit(expr: &Expr) -> bool { + match &expr.kind { + ExprKind::Lit(lit) => lit.node.is_negative(), + ExprKind::Cast(inner) => match &inner.kind { + ExprKind::Lit(lit) => lit.node.is_negative(), + _ => false, + }, + ExprKind::Unary(un_op, inner) => match un_op.node { + UnOpKind::Parens => is_neg_lit(inner), + _ => false, + }, + _ => false, + } +} + +pub fn is_one_lit(expr: &Expr) -> bool { + match &expr.kind { + ExprKind::Lit(lit) => lit.node.is_one(), + ExprKind::Cast(inner) => match &inner.kind { + ExprKind::Lit(lit) => lit.node.is_one(), + _ => false, + }, + ExprKind::Unary(un_op, inner) => match un_op.node { + UnOpKind::Parens => is_one_lit(inner), + _ => false, + }, + _ => false, + } +} /// Remove [`ExprKind::Cast`] from this expression. This is mainly used to make /// the pretty-printed expression look less verbose. diff --git a/src/driver/quant_proof.rs b/src/driver/quant_proof.rs index ae74a3af..aa97e78e 100644 --- a/src/driver/quant_proof.rs +++ b/src/driver/quant_proof.rs @@ -12,8 +12,8 @@ use crate::{ depgraph::Dependencies, driver::{commands::verify::VerifyCommand, error::CaesarError, item::SourceUnitName}, opt::{ - boolify::Boolify, egraph, qelim::Qelim, relational::Relational, unfolder::Unfolder, - RemoveParens, + boolify::Boolify, egraph, qelim::Qelim, relational::Relational, + remove_neutrals::NeutralsRemover, unfolder::Unfolder, RemoveParens, }, resource_limits::{LimitError, LimitsRef}, smt::{funcs::axiomatic::AxiomaticFunctionEncoder, DepConfig, SmtCtx}, @@ -27,12 +27,13 @@ use crate::{ pub fn lower_quant_prove_task( options: &VerifyCommand, limits_ref: &LimitsRef, - tcx: &mut TyCtx, + tcx: &TyCtx, name: &SourceUnitName, mut quant_task: QuantVcProveTask, ) -> Result { // 1. Unfolding (applies substitutions) quant_task.unfold(options, limits_ref, tcx)?; + quant_task.remove_neutrals(limits_ref, tcx)?; // 2. Quantifier elimination if !options.opt_options.no_qelim { @@ -72,7 +73,7 @@ pub fn lower_quant_prove_task( } /// Quantitative verification conditions that are to be checked. -#[derive(Debug)] +#[derive(Debug, Clone)] pub struct QuantVcProveTask { pub deps: Dependencies, pub direction: Direction, @@ -107,8 +108,27 @@ impl QuantVcProveTask { } } + pub fn remove_neutrals( + &mut self, + limits_ref: &LimitsRef, + tcx: &TyCtx, + ) -> Result<(), LimitError> { + let span = info_span!("unfolding"); + let _entered = span.enter(); + let ctx = Context::new(&Config::default()); + let dep_config = DepConfig::SpecsOnly; + let smt_ctx = SmtCtx::new( + &ctx, + tcx, + Box::new(AxiomaticFunctionEncoder::default()), + dep_config, + ); + let mut neutrals_remover = NeutralsRemover::new(limits_ref.clone(), &smt_ctx); + neutrals_remover.visit_expr(&mut self.expr) + } + /// Apply quantitative quantifier elimination. - pub fn qelim(&mut self, tcx: &mut TyCtx, limits_ref: &LimitsRef) -> Result<(), CaesarError> { + pub fn qelim(&mut self, tcx: &TyCtx, limits_ref: &LimitsRef) -> Result<(), CaesarError> { let mut qelim = Qelim::new(tcx); qelim.qelim(self); // Apply/eliminate substitutions again diff --git a/src/opt/mod.rs b/src/opt/mod.rs index e795f244..b33b3f6f 100644 --- a/src/opt/mod.rs +++ b/src/opt/mod.rs @@ -26,6 +26,7 @@ pub mod egraph; mod fuzz_test; pub mod qelim; pub mod relational; +pub mod remove_neutrals; pub mod unfolder; /// This "optimization" removes all parentheses. This makes matching easier in diff --git a/src/opt/qelim.rs b/src/opt/qelim.rs index cd599883..31493d8b 100644 --- a/src/opt/qelim.rs +++ b/src/opt/qelim.rs @@ -12,11 +12,11 @@ use crate::{ }; pub struct Qelim<'tcx> { - tcx: &'tcx mut TyCtx, + tcx: &'tcx TyCtx, } impl<'tcx> Qelim<'tcx> { - pub fn new(tcx: &'tcx mut TyCtx) -> Self { + pub fn new(tcx: &'tcx TyCtx) -> Self { Qelim { tcx } } diff --git a/src/opt/remove_neutrals.rs b/src/opt/remove_neutrals.rs new file mode 100644 index 00000000..8b7c4b20 --- /dev/null +++ b/src/opt/remove_neutrals.rs @@ -0,0 +1,289 @@ +use std::ops::DerefMut; + +use z3::SatResult; +use z3rro::prover::{IncrementalMode, Prover}; + +use crate::{ + ast::{ + util::{is_bot_lit, is_lit, is_neg_lit, is_one_lit, is_top_lit, is_zero_lit, remove_casts}, + visit::{walk_expr, VisitorMut}, + BinOpKind, Expr, ExprBuilder, ExprData, ExprKind, Ident, Shared, Span, Spanned, Symbol, + TyKind, UnOpKind, + }, + resource_limits::{LimitError, LimitsRef}, + smt::SmtCtx, + vc::subst::Subst, +}; + +use crate::smt::translate_exprs::TranslateExprs; + +pub struct NeutralsRemover<'smt, 'ctx> { + /// The expressions may contain substitutions. We keep track of those. + subst: Subst<'smt>, + + /// Context to translate to SMT. + translate: TranslateExprs<'smt, 'ctx>, + + /// The prover keeps track of the conditions to reach the current + /// sub-expression. The proof check returns `Proof` if it's unreachable. + /// Since the conditions are not complete, a result of `Counterexample` does + /// not prove that a sub-expression is guaranteed to be reachable. + prover: Prover<'ctx>, +} + +impl<'smt, 'ctx> NeutralsRemover<'smt, 'ctx> { + pub fn new(limits_ref: LimitsRef, ctx: &'smt SmtCtx<'ctx>) -> Self { + // it's important that we use the native incremental mode here, because + // the performance benefit from the neutrals_remover relies on many very fast + // SAT checks. + let prover = Prover::new(ctx.ctx(), IncrementalMode::Native); + + NeutralsRemover { + subst: Subst::new(ctx.tcx(), &limits_ref), + translate: TranslateExprs::new(ctx), + prover, + } + } + + /// Call `f` surrounded by `push()` and `pop()` calls to the prover. + fn with_prover_scope(&mut self, f: impl FnOnce(&mut Self) -> T) -> T { + self.prover.push(); + let res = f(self); + self.prover.pop(); + res + } + + /// Check whether `expr` is currently satisfiable. If `expr` is + /// unsatisfiable, return `None`. If it is satisfiable, then call `callback` + /// assuming `expr` is true. + fn with_sat(&mut self, expr: &Expr, callback: impl FnOnce(&mut Self) -> T) -> Option { + let expr_z3 = self.translate.t_bool(expr); + + // Add any new assumptions produced by translating `expr`. + self.translate + .local_scope() + .add_assumptions_to_prover(&mut self.prover); + + self.with_prover_scope(|this| { + this.prover.add_assumption(&expr_z3); + tracing::trace!(expr_z3=%expr_z3, "added expr to neutrals_remover solver"); + // here we want to do a SAT check and not a proof search. if the + // expression is e.g. `false`, then we want to get `Unsat` from the + // solver and not `Proof`! + if this.prover.check_sat() == SatResult::Unsat { + tracing::trace!(solver=?this.prover, "eliminated zero expr"); + None + } else { + Some(callback(this)) + } + }) + } + + /// Evaluate `callback` assuming `expr` is not bottom. Returns `None` if + /// `expr` is statically bottom, skipping the callback. + fn with_nonbot(&mut self, expr: &Expr, callback: impl FnOnce(&mut Self) -> T) -> Option { + match &expr.kind { + ExprKind::Unary(un_op, operand) => match un_op.node { + UnOpKind::Embed | UnOpKind::Iverson => { + // If an embed or Iverson expression are nonzero, we know + // the Boolean expression must be true. + return self.with_sat(operand, callback); + } + UnOpKind::Parens => { + return self.with_nonbot(operand, callback); + } + _ => {} + }, + _ if is_bot_lit(expr) => return None, + _ => {} + } + Some(callback(self)) + } + + /// Evaluate `callback` assuming `expr` is not top. Returns `None` if + /// `expr` is statically top, skipping the callback. + fn with_nontop(&mut self, expr: &Expr, callback: impl FnOnce(&mut Self) -> T) -> Option { + match &expr.kind { + ExprKind::Unary(un_op, operand) => { + if let UnOpKind::Embed = un_op.node { + // If an embed expression is not top, then its Boolean + // condition must be false. + return self.with_sat(&negate_expr(operand.clone()), callback); + } + } + _ if is_top_lit(expr) => return None, + _ => {} + } + Some(callback(self)) + } +} +impl<'smt, 'ctx> VisitorMut for NeutralsRemover<'smt, 'ctx> { + type Err = LimitError; + + fn visit_expr(&mut self, e: &mut Expr) -> Result<(), Self::Err> { + self.subst.limits_ref.check_limits()?; + let ty = e.ty.clone().unwrap(); + + match &mut e.deref_mut().kind { + // ----- variable subst ----- + ExprKind::Var(ident) => { + if let Some(subst) = self.subst.lookup_var(*ident) { + *e = subst.clone(); + } + Ok(()) + } + ExprKind::Call(func_ident, args) => { + let nonneg_cast_name = Ident::with_dummy_span(Symbol::intern("nonneg_cast")); + let _ = self.visit_exprs(args); + if func_ident.name == nonneg_cast_name.name { + let builder = ExprBuilder::new(Span::dummy_span()); + if is_neg_lit(&args[0]) { + *e = builder.zero_lit(&TyKind::UReal); + } else if is_lit(&args[0]) { + // using cast doesn't work, because maybe the type is unsinged. + // but since we know the value is positive, we can do this. + *e = Expr::new(ExprData { + kind: remove_casts(&args[0].clone()).kind.clone(), + ty: Some(TyKind::UReal), + span: args[0].span, + }); + } + } + Ok(()) + } + + // ----- subst node ----- + ExprKind::Subst(ident, subst, body) => { + self.visit_expr(subst)?; + self.subst.push_subst(*ident, subst.clone()); + self.visit_expr(body)?; + self.subst.pop(); + *e = body.clone(); + Ok(()) + } + + // ----- binary operators ----- + ExprKind::Binary(bin_op, lhs, rhs) => { + // Always visit children first + self.visit_expr(lhs)?; + self.visit_expr(rhs)?; + + use BinOpKind::*; + + match bin_op.node { + // MUL: remove 1 + Mul => { + if is_one_lit(lhs) { + *e = rhs.clone(); + return Ok(()); + } + if is_one_lit(rhs) { + *e = lhs.clone(); + return Ok(()); + } + // remove lhs 0 + if is_zero_lit(lhs) { + *e = lhs.clone(); + return Ok(()); + } + // remove rhs 0 + if is_zero_lit(rhs) { + *e = rhs.clone(); + return Ok(()); + } + Ok(()) + } + // ADD: remove 0 + Add => { + if is_zero_lit(lhs) { + *e = rhs.clone(); + return Ok(()); + } + if is_zero_lit(rhs) { + *e = lhs.clone(); + return Ok(()); + } + Ok(()) + } + + // AND: remove true + BinOpKind::And => { + // 1) bottom(lhs) -> result is bottom + let nonbot: Option> = + self.with_nonbot(lhs, |_| Ok(())); + if nonbot.is_none() { + let b = ExprBuilder::new(e.span); + *e = b.bot_lit(&ty); + return Ok(()); + } + + // 2) lhs == true (top) -> result = rhs + let nontop: Option> = + self.with_nontop(lhs, |_| Ok(())); + if nontop.is_none() { + *e = rhs.clone(); + return Ok(()); + } + + // 3) if lhs => rhs, remove rhs + { + let builder = ExprBuilder::new(Span::dummy_span()); + + // build (lhs && !rhs) + let not_rhs = + builder.unary(UnOpKind::Not, Some(ty.clone()), rhs.clone()); + let lhs_and_not_rhs = + builder.binary(BinOpKind::And, Some(ty), lhs.clone(), not_rhs); + + // if lhs && !rhs is unsat, lhs => rhs holds + let implied = self.with_sat(&lhs_and_not_rhs, |_| ()); + if implied.is_none() { + *e = lhs.clone(); // keep only lhs + return Ok(()); + } + } + + // 4) keep both sides + Ok(()) + } + + // OR: remove false + Or => { + // top(lhs) -> result is top (infinity is the absorber of Sup) + let nontop: Option> = + self.with_nontop(lhs, |_| Ok(())); + if nontop.is_none() { + let b = ExprBuilder::new(e.span); + *e = b.top_lit(&ty); + return Ok(()); + } + + // bot is the neutral for Or + if is_bot_lit(lhs) { + *e = rhs.clone(); + return Ok(()); + } + if is_bot_lit(rhs) { + *e = lhs.clone(); + return Ok(()); + } + + Ok(()) + } + + _ => Ok(()), + } + } + + _ => walk_expr(self, e), + } + } +} + +fn negate_expr(expr: Expr) -> Expr { + Shared::new(ExprData { + kind: ExprKind::Unary(Spanned::with_dummy_span(UnOpKind::Not), expr), + ty: Some(TyKind::Bool), + span: Span::dummy_span(), + }) +} From 99bf049ce206bc0ca4007cbc642165d5f4e3a2d4 Mon Sep 17 00:00:00 2001 From: madita Date: Thu, 11 Jun 2026 15:57:59 +0200 Subject: [PATCH 09/11] synthesis: introduce template-based CEGIS invariant synthesis Adds a synth command that runs a counterexample-guided inductive synthesis (CEGIS) loop to find function bodies using templates. --- src/ast/decl.rs | 2 +- src/ast/expr.rs | 8 + src/ast/util.rs | 48 +- src/driver/commands/mod.rs | 6 + src/driver/commands/options.rs | 83 ++ src/driver/commands/refinement.rs | 3 +- src/driver/commands/synth.rs | 478 +++++++++++ src/driver/commands/verify.rs | 9 +- src/driver/item.rs | 10 +- src/driver/ranges.rs | 6 +- src/driver/smt_proof.rs | 81 +- src/front/parser/grammar.lalrpop | 2 +- src/main.rs | 1 + src/smt/translate_exprs.rs | 2 +- src/synthesis/cegis.rs | 542 ++++++++++++ src/synthesis/k_induction.rs | 112 +++ src/synthesis/mod.rs | 5 + .../rec_functions/approx_encoding.rs | 666 +++++++++++++++ src/synthesis/rec_functions/mod.rs | 5 + src/synthesis/rec_functions/soundness.rs | 173 ++++ src/synthesis/report.rs | 150 ++++ src/synthesis/templates/conditions.rs | 435 ++++++++++ src/synthesis/templates/mod.rs | 800 ++++++++++++++++++ src/synthesis/templates/pipeline.rs | 257 ++++++ src/synthesis/templates/refinements.rs | 196 +++++ 25 files changed, 4055 insertions(+), 25 deletions(-) create mode 100644 src/driver/commands/synth.rs create mode 100644 src/synthesis/cegis.rs create mode 100644 src/synthesis/k_induction.rs create mode 100644 src/synthesis/mod.rs create mode 100644 src/synthesis/rec_functions/approx_encoding.rs create mode 100644 src/synthesis/rec_functions/mod.rs create mode 100644 src/synthesis/rec_functions/soundness.rs create mode 100644 src/synthesis/report.rs create mode 100644 src/synthesis/templates/conditions.rs create mode 100644 src/synthesis/templates/mod.rs create mode 100644 src/synthesis/templates/pipeline.rs create mode 100644 src/synthesis/templates/refinements.rs diff --git a/src/ast/decl.rs b/src/ast/decl.rs index 976b7a9f..db293efd 100644 --- a/src/ast/decl.rs +++ b/src/ast/decl.rs @@ -246,7 +246,7 @@ impl VarDecl { init: None, span: param.span, created_from: None, - range: param.range.clone(), + range: param.range, }; DeclRef::new(var_decl) } diff --git a/src/ast/expr.rs b/src/ast/expr.rs index ed504d59..f464b491 100644 --- a/src/ast/expr.rs +++ b/src/ast/expr.rs @@ -688,6 +688,14 @@ impl ExprBuilder { }) } + pub fn uint_lit(&self, value: BigUint) -> Expr { + Shared::new(ExprData { + kind: ExprKind::Lit(Spanned::new(self.span, LitKind::UInt(value))), + ty: Some(TyKind::UInt), + span: self.span, + }) + } + pub fn frac_lit(&self, value: BigRational) -> Expr { Shared::new(ExprData { kind: ExprKind::Lit(Spanned::new(self.span, LitKind::Frac(value))), diff --git a/src/ast/util.rs b/src/ast/util.rs index d5df0544..b55a0587 100644 --- a/src/ast/util.rs +++ b/src/ast/util.rs @@ -5,7 +5,7 @@ use crate::ast::UnOpKind; use super::{ visit::{walk_expr, walk_stmt, VisitorMut}, - Direction, Expr, ExprKind, Ident, StmtKind, + Direction, Expr, ExprKind, Ident, LitKind, StmtKind, }; /// Helper to find all free variables in expressions. @@ -198,6 +198,41 @@ pub fn is_one_lit(expr: &Expr) -> bool { } } +/// Returns `true` if `expr` contains any negative numeric literal. +fn has_negative_lit(expr: &Expr) -> bool { + if let ExprKind::Lit(lit) = &expr.kind { + return lit.node.is_negative(); + } + expr.children().into_iter().any(has_negative_lit) +} + +/// Strips `nonneg_cast(arg)` call nodes when `arg` contains no negative numeric literals, +pub fn strip_nonneg_cast_if_nonneg(expr: &Expr) -> Expr { + let mut res = expr.clone(); + StripNonnegCastVisitor.visit_expr(&mut res).unwrap(); + res +} + +struct StripNonnegCastVisitor; + +impl VisitorMut for StripNonnegCastVisitor { + type Err = (); + + fn visit_expr(&mut self, e: &mut Expr) -> Result<(), Self::Err> { + if let ExprKind::Call(func, args) = &e.kind { + if func.name.to_string() == "nonneg_cast" { + if let [arg] = args.as_slice() { + if !has_negative_lit(arg) { + *e = arg.clone(); + return walk_expr(self, e); + } + } + } + } + walk_expr(self, e) + } +} + /// Remove [`ExprKind::Cast`] from this expression. This is mainly used to make /// the pretty-printed expression look less verbose. pub fn remove_casts(expr: &Expr) -> Expr { @@ -265,3 +300,14 @@ mod test { ); } } + +/// Extract a `u128` from an expression that is a `UInt` literal. +/// Panics if the expression is not a `UInt` literal — callers must ensure this via type-checking. +pub fn lit_u128(expr: &Expr) -> u128 { + if let ExprKind::Lit(lit) = &expr.kind { + if let LitKind::UInt(value) = &lit.node { + return u128::try_from(value).unwrap(); + } + } + unreachable!() +} diff --git a/src/driver/commands/mod.rs b/src/driver/commands/mod.rs index 33503a63..46d5056c 100644 --- a/src/driver/commands/mod.rs +++ b/src/driver/commands/mod.rs @@ -4,6 +4,7 @@ pub mod model_check; pub mod options; pub mod refinement; pub mod run_lsp; +pub mod synth; pub mod verify; use std::{ @@ -23,6 +24,7 @@ use crate::{ options::{DebugOptions, InputOptions}, refinement::run_verify_entailment_command, run_lsp::run_lsp_command, + synth::run_synth, verify::{run_verify_command, VerifyCommand}, }, servers::{CliServer, SharedServer}, @@ -65,6 +67,7 @@ impl CaesarCli { CaesarCommand::Mc(options) => run_model_checking_command(options), CaesarCommand::Lsp(options) => run_lsp_command(options).await, CaesarCommand::ShellCompletions(options) => run_shell_completions_command(options), + CaesarCommand::Synth(options) => run_synth(options).await, CaesarCommand::Other(_) => unreachable!(), } } @@ -98,6 +101,8 @@ pub enum CaesarCommand { Lsp(VerifyCommand), /// Generate shell completions for the Caesar binary. ShellCompletions(ShellCompletionsCommand), + /// Synthesize function bodies to satisfy annotated `syn func` templates. + Synth(VerifyCommand), /// This is to support the default `verify` command. #[command(external_subcommand)] #[command(hide(true))] @@ -112,6 +117,7 @@ impl CaesarCommand { CaesarCommand::Lsp(verify_options) => Some(&verify_options.debug_options), CaesarCommand::Mc(mc_options) => Some(&mc_options.debug_options), CaesarCommand::ShellCompletions(_) => None, + CaesarCommand::Synth(verify_options) => Some(&verify_options.debug_options), CaesarCommand::Other(_vec) => unreachable!(), } } diff --git a/src/driver/commands/options.rs b/src/driver/commands/options.rs index 062423d4..e3e53c88 100644 --- a/src/driver/commands/options.rs +++ b/src/driver/commands/options.rs @@ -409,3 +409,86 @@ pub enum SliceVerifyMethod { #[value(name = "exists-forall")] ExistsForall, } + +/// Controls which axis the outer synthesis loop refines on each iteration. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, ValueEnum)] +pub enum RefinementMode { + /// Single CEGIS attempt with one interval region; no refinement (default). + #[default] + None, + /// Increase the number of piecewise regions each iteration, using declared + /// type ranges (e.g. `a: UInt [0,3]`) to compute equal-width interval + /// boundaries. Requires at least one range declaration; errors otherwise. + Fixed, + /// Increase the polynomial degree by 1 each iteration. + Degree, + /// Use template variables as region-split boundaries; increase the number + /// of intervals each iteration (like Fixed, but boundaries are synthesised + /// rather than computed from equal-width arithmetic). + Variable, + /// For files that use `@k_induction(k, inv(...))`: start with the k written + /// in the annotation and increase it by 1 on each outer iteration that fails + /// to find a valid invariant. The template regions are held at 1 (no + /// piecewise splitting) while k is being searched. + KInduction, +} + +#[derive(Debug, Default, Args)] +#[command(next_help_heading = "Synthesizer Options")] +pub struct SynthesizerOptions { + /// Polynomial degree for the template. In `degree` refinement mode this is + /// the starting degree, which increases by 1 each outer iteration. + #[arg(long)] + pub degree: Option, + + /// Print syn_benchmarks timing and statistics on success. + #[arg(long)] + pub syn_benchmarks: bool, + + /// Print verbose CEGIS info: loop headers, counterexamples, and close-CEX counts. + #[arg(long)] + pub syn_verbose: bool, + + /// Print the template expression before CEGIS starts. + #[arg(long)] + pub print_template: bool, + + /// Use a bare polynomial template without loop-aware structure. + /// By default, when a loop is detected, the template is built with the loop + /// guard treated structurally. This flag disables that and uses a plain + /// polynomial in all cases. + #[arg(long)] + pub bare_template: bool, + + /// Use unsigned (non-negative) coefficients in the template. + #[arg(long)] + pub unsigned_coefficients: bool, + + /// Maximum number of outer refinement iterations. + #[arg(long)] + pub max_refinements: Option, + + /// Use fuel-bounded recursive function encoding: insert assume statements + /// that bound recursive calls during CEGIS, then verify soundness on the + /// original VC (without assumes) after a candidate invariant is found. + #[arg(long)] + pub rec_functions: bool, + + /// Template refinement strategy. + /// + /// `none` (default): single CEGIS attempt, no refinement. `fixed`: + /// increase piecewise regions each iteration using declared range + /// boundaries (requires range declarations). `degree`: keep regions + /// fixed at 1 and increase the polynomial degree. `variable`: like + /// `fixed` but region boundaries are synthesised by CEGIS. + #[arg(long, default_value = "none")] + pub refinement_mode: RefinementMode, + + /// Per-iteration time limit in seconds for the soundness check that follows + /// a successful CEGIS round (only active when --rec-functions is set). + /// If the check does not conclude within this budget the fuel bound is + /// increased and synthesis retries, preserving the remaining global budget + /// for subsequent iterations. + #[arg(long, default_value = "30")] + pub soundness_timeout: u64, +} diff --git a/src/driver/commands/refinement.rs b/src/driver/commands/refinement.rs index 33aa3bc0..c538cbe4 100644 --- a/src/driver/commands/refinement.rs +++ b/src/driver/commands/refinement.rs @@ -150,8 +150,7 @@ async fn verify_entailment( // Lowering the quantitative task to a Boolean one. This contains (lazy) // unfolding, quantifier elimination, and various optimizations // (depending on options). - let vc_is_valid = - lower_quant_prove_task(options, &limits_ref, &mut tcx, &first_name, vc_expr)?; + let vc_is_valid = lower_quant_prove_task(options, &limits_ref, &tcx, &first_name, vc_expr)?; // Running the SMT prove task: translating to Z3, running the solver. let slice_vars = first_slice_stmts.extend(second_slice_stmts); diff --git a/src/driver/commands/synth.rs b/src/driver/commands/synth.rs new file mode 100644 index 00000000..b995a7b8 --- /dev/null +++ b/src/driver/commands/synth.rs @@ -0,0 +1,478 @@ +use crate::ast::util::FreeVariableCollector; +use crate::ast::visit::VisitorMut; +use crate::ast::{Expr, Ident, Symbol}; +use crate::depgraph::DepGraph; +use crate::driver::commands::options::{FunctionEncodingOption, RefinementMode}; +use crate::driver::item::SourceUnitName; +use crate::driver::ranges::{collect_ranges_from_decls, create_range_constraint}; +use crate::synthesis::cegis::{get_synth_functions, run_cegis_loop, CegisData, CegisProof}; +use crate::synthesis::k_induction::{ + collect_k_induction_calls, read_k_induction_k, set_k_induction_k, +}; +use crate::synthesis::rec_functions::InsertAssumeBeforeCalls; +use crate::synthesis::rec_functions::{ + run_soundness_check, SoundnessCheckConfig, SoundnessOutcome, +}; +use crate::synthesis::report::{self as synth_report, SynthStats}; +use crate::synthesis::templates::{build_and_inline_templates, RefinementState, TemplateConfig}; +use crate::tyctx::TyCtx; +use crate::{ + ast::{DeclKind, DomainSpec, FileId}, + driver::{ + commands::{mk_cli_server, print_timings, verify::VerifyCommand}, + core_verify::{lower_core_verify_task, CoreVerifyTask}, + error::{finalize_caesar_result, CaesarError}, + front::{parse_and_tycheck, SourceUnit}, + quant_proof::{lower_quant_prove_task, BoolVcProveTask, QuantVcProveTask}, + smt_proof::{mk_function_encoder_override, set_global_z3_params}, + }, + resource_limits::{await_with_resource_limits, LimitsRef}, + servers::{Server, SharedServer}, + smt::{translate_exprs::TranslateExprs, DepConfig, SmtCtx}, +}; + +#[allow(clippy::collapsible_match)] +fn get_functions_from_source_unit(source_unit: &SourceUnit) -> Vec { + let mut funcs = Vec::new(); + if let SourceUnit::Decl(decl) = source_unit { + if let DeclKind::DomainDecl(domain_ref) = decl { + let domain = domain_ref.borrow(); + for spec in &domain.body { + if let DomainSpec::Function(func_ref) = spec { + funcs.push(func_ref.borrow().name); + } + } + } + } + funcs +} +use indexmap::{IndexMap, IndexSet}; +use std::time::Instant; +use std::{ops::DerefMut, process::ExitCode, sync::Arc}; +use z3::Context; + +pub async fn run_synth(mut options: VerifyCommand) -> ExitCode { + let (user_files, server) = match mk_cli_server(&options.input_options) { + Ok(result) => result, + Err(code) => return code, + }; + options.slice_options.no_slice_error = true; + if options.synth_options.rec_functions + && options.opt_options.function_encoding == FunctionEncodingOption::FuelParam + { + options.opt_options.function_encoding = FunctionEncodingOption::FuelMono; + } + let options = Arc::new(options); + let result = synth_files(&options, &server, user_files).await; + + if options.debug_options.timing { + print_timings(); + } + + finalize_caesar_result(server, &options.rlimit_options, result) +} + +// Synthesize invariants for a list of `user_files`. +pub async fn synth_files( + options: &Arc, + server: &SharedServer, + user_files: Vec, +) -> Result { + let handle = |limits_ref: LimitsRef| { + let options = options.clone(); + let server = server.clone(); + tokio::task::spawn_blocking(move || { + // Use a larger stack (50 MB) since the verifier recurses deeply. + let stack_size = 50 * 1024 * 1024; + stacker::maybe_grow(stack_size, stack_size, move || { + let mut server = server.lock().unwrap(); + synth_main(&options, limits_ref, server.deref_mut(), &user_files) + }) + }) + }; + let limits_ref = LimitsRef::new( + Some(Instant::now() + options.rlimit_options.timeout()), + Some(options.rlimit_options.mem_limit()), + ); + await_with_resource_limits(limits_ref, handle).await?? +} + +// Synchronously synthesize invariants for the given files using CEGIS. +fn synth_main( + options: &VerifyCommand, + limits_ref: LimitsRef, + server: &mut dyn Server, + user_files: &[FileId], +) -> Result { + // Parse once upfront to collect item names and (for KInduction) the initial k. + let (mut module_init, _) = parse_and_tycheck( + &options.input_options, + &options.debug_options, + server, + user_files, + )?; + // Refinement counter: for KInduction this is k, for Degree it's the polynomial degree, + // for Fixed/Variable it's the number of piecewise intervals. + let refinement_mode = options.synth_options.refinement_mode; + let initial_degree = options.synth_options.degree.unwrap_or(1); + let initial_refinement_iter: usize = match refinement_mode { + RefinementMode::KInduction => read_k_induction_k(&mut module_init).unwrap_or(1) as usize, + RefinementMode::Degree => initial_degree, + _ => 1, + }; + // Items proven across all outer iterations. + let mut proven_item_names: IndexSet = IndexSet::new(); + let mut stats = SynthStats::new(); + // Fuel for the guarded encoding; bumped on each soundness-check failure. + let mut current_fuel: usize = options.opt_options.max_fuel; + + // Collect names upfront; they're stable across re-parses. + let item_names: Vec = module_init + .items + .iter() + .map(|item| item.name().to_string()) + .collect(); + + // Process each item sequentially: complete all refinement iterations for + // one item before starting the next. + for target_name in &item_names { + let mut refinement_iter = initial_refinement_iter; + let max_refinement_iter = if refinement_mode == RefinementMode::None { + refinement_iter + } else { + refinement_iter + options.synth_options.max_refinements.unwrap_or(300) + }; + + 'refinement: while refinement_iter <= max_refinement_iter { + let effective_split_count = match refinement_mode { + RefinementMode::Degree | RefinementMode::KInduction => 1, + _ => refinement_iter, + }; + let effective_degree = match refinement_mode { + RefinementMode::Degree => refinement_iter, + _ => initial_degree, + }; + + if options.synth_options.syn_verbose { + match refinement_mode { + RefinementMode::Degree => println!("Degree {refinement_iter}"), + RefinementMode::None => println!("Single CEGIS attempt"), + RefinementMode::Variable | RefinementMode::Fixed => { + println!("{refinement_iter} interval(s)") + } + RefinementMode::KInduction => { + println!("Iteration {refinement_iter} (k-induction, k={refinement_iter})") + } + } + } + + // Re-parse on every refinement iteration to get a clean type context. + let start_parse = Instant::now(); + let (mut module, mut tcx) = parse_and_tycheck( + &options.input_options, + &options.debug_options, + server, + user_files, + )?; + if options.synth_options.syn_benchmarks { + println!("Parse time = {:.2}s", start_parse.elapsed().as_secs_f64()); + } + + if refinement_mode == RefinementMode::Fixed + && collect_ranges_from_decls(&tcx.declarations.borrow()).is_empty() + { + return Err(CaesarError::UserError( + "--refinement-mode fixed requires at least one type range declaration (e.g. `a: UInt [0,3]`)" + .into(), + )); + } + + // Update k in every @k_induction(k, ...) annotation to the current + // refinement iteration, so the encoding uses the right unrolling depth. + if refinement_mode == RefinementMode::KInduction { + set_k_induction_k(&mut module, refinement_iter as u128); + } + + // Collect inv_call args from @k_induction before the module is consumed, + // so we can reprint the updated annotation in the synthesized output. + let k_induction_calls = if refinement_mode == RefinementMode::KInduction { + collect_k_induction_calls(&mut module) + } else { + Default::default() + }; + + let refinement = RefinementState { + mode: refinement_mode, + iter: refinement_iter, + effective_split_count, + effective_degree, + }; + + module.register_with_server(server)?; + module.check_calculus_rules(&mut tcx)?; + module.apply_encodings(&mut tcx, server)?; + + let mut depgraph = module.generate_depgraph(&options.opt_options.function_encoding)?; + + let domain_funcs: Vec = if options.synth_options.rec_functions { + module + .items + .iter() + .flat_map(|item| get_functions_from_source_unit(item)) + .collect() + } else { + vec![] + }; + + set_global_z3_params(options, &limits_ref); + + for item in module.items { + if item.name().to_string() != *target_name { + continue; + } + + // Skip non-proc items (e.g. domain declarations) that have no VC to synthesize. + let Some(mut synth_unit) = + item.flat_map(|unit| CoreVerifyTask::from_source_unit(unit, &mut depgraph)) + else { + break 'refinement; + }; + + // Clone before applying assumes so the soundness check can use the original VC. + let mut orig_unit = None; + if options.synth_options.rec_functions { + orig_unit = Some(synth_unit.value().clone()); + let task = synth_unit.value_mut(); + let mut visitor = InsertAssumeBeforeCalls { + func_idents: &domain_funcs, + direction: task.direction, + tcx: &tcx, + max_fuel: current_fuel, + }; + visitor.visit_block(&mut task.block).unwrap(); + } + + limits_ref.check_limits()?; + let (name, mut synth_unit) = synth_unit.enter_with_name(); + let name_str = name.to_string(); + server.set_ongoing_unit(name)?; + + if options.debug_options.print_core_procs { + println!("Core HeyVL (with assume statements) for `{name}`:"); + println!("{}", *synth_unit); + } + + let (vc_expr, _) = lower_core_verify_task( + &mut tcx, + name, + options, + &limits_ref, + server, + &mut synth_unit, + )?; + + let vc_is_valid = + lower_quant_prove_task(options, &limits_ref, &tcx, name, vc_expr.clone())?; + + // Compute the original (no-assume) VC while &mut tcx is still available. + let vc_expr_orig_opt: Option = + if options.synth_options.rec_functions { + let (vc, _) = lower_core_verify_task( + &mut tcx, + name, + options, + &limits_ref, + server, + &mut orig_unit.unwrap(), + )?; + Some(vc) + } else { + None + }; + + let cegis_config = CegisItemConfig { + tcx: &tcx, + depgraph: &depgraph, + options, + limits_ref: &limits_ref, + current_fuel, + refinement: &refinement, + }; + let (instantiated_templates, range_constraints) = run_cegis_for_item( + &cegis_config, + name, + vc_expr, + vc_is_valid, + &mut stats, + &k_induction_calls, + )?; + + // soundness check: verify the found invariant also holds on the original VC (no assumes) + if options.synth_options.rec_functions { + if let Some(instantiated_templates) = instantiated_templates { + if let Some(vc_expr_orig) = vc_expr_orig_opt { + let soundness_config = SoundnessCheckConfig { + options, + limits_ref: &limits_ref, + depgraph: &depgraph, + name, + current_fuel, + }; + match run_soundness_check( + instantiated_templates, + &range_constraints, + vc_expr_orig, + &mut tcx, + &soundness_config, + &domain_funcs, + )? { + SoundnessOutcome::Proved => { + proven_item_names.insert(name_str.clone()); + break 'refinement; + } + SoundnessOutcome::RetryWithFuel => { + current_fuel += 1; + continue 'refinement; + } + SoundnessOutcome::NoConclusion => {} + } + } + } + } else if instantiated_templates.is_some() { + // Non-recursive: invariant found by CEGIS is immediately valid. + proven_item_names.insert(name_str.clone()); + break 'refinement; + } + } + + refinement_iter += 1; + } + } + + if proven_item_names.is_empty() { + println!("No template instantiation found that leads to a verifying function body."); + } + Ok(!proven_item_names.is_empty()) +} + +struct CegisItemConfig<'a> { + tcx: &'a TyCtx, + depgraph: &'a DepGraph, + options: &'a VerifyCommand, + limits_ref: &'a LimitsRef, + current_fuel: usize, + refinement: &'a RefinementState, +} + +type CegisItemResult = (Option>, Vec); + +/// Run the CEGIS loop for one synthesis item and return the instantiated +/// templates (if any) and the range constraints collected from declarations. +fn run_cegis_for_item( + config: &CegisItemConfig<'_>, + name: &SourceUnitName, + vc_expr: QuantVcProveTask, + vc_is_valid: BoolVcProveTask, + stats: &mut SynthStats, + k_induction_calls: &IndexMap, +) -> Result { + let ctx = Context::new(&z3::Config::default()); + let tcx = config.tcx; + let depgraph = config.depgraph; + let options = config.options; + let limits_ref = config.limits_ref; + let refinement = config.refinement; + let current_fuel = config.current_fuel; + let function_encoder = mk_function_encoder_override( + tcx, + depgraph, + options, + // rec_functions: disable synonym axiom during CEGIS so the solver only + // sees the guarded approximation; the soundness check re-enables it. + options.synth_options.rec_functions || options.opt_options.no_synonym_axiom, + Some(current_fuel), + )?; + let smt_ctx = SmtCtx::new( + &ctx, + tcx, + function_encoder, + DepConfig::Set(vc_is_valid.get_dependencies()), + ); + let mut translate = TranslateExprs::new(&smt_ctx); + + let mut vc_expr = vc_expr; + let mut vc_is_valid = vc_is_valid; + + let template_config = TemplateConfig { + options, + limits_ref, + refinement, + }; + let (templates, tvars) = build_and_inline_templates( + &mut translate, + &mut vc_expr, + &mut vc_is_valid, + &template_config, + name, + stats, + )?; + + let synth_funcs = get_synth_functions(smt_ctx.uninterpreteds()); + + let tvar_ident_set: IndexSet = tvars.iter().map(|(id, _)| *id).collect(); + let pvar_idents: IndexSet = FreeVariableCollector::new() + .collect_and_clear(&mut vc_is_valid.vc) + .difference(&tvar_ident_set) + .cloned() + .collect(); + + let range_constraints: Vec = collect_ranges_from_decls(&tcx.declarations.borrow()) + .iter() + .map(|(ident, (range, ty))| create_range_constraint(*ident, range, ty.clone())) + .collect(); + + let cegis_data = CegisData { + templates, + pvar_idents, + tvars, + range_constraints, + boolean_vc: vc_is_valid, + vc_expr, + }; + + let cegis_proof = run_cegis_loop( + &cegis_data, + &ctx, + &mut translate, + options, + limits_ref, + name, + stats, + )?; + + let instantiated_templates = cegis_proof.map( + |CegisProof { + instantiated_templates, + instantiated_tasks, + duration_check, + }| { + if options.synth_options.syn_benchmarks { + synth_report::print_benchmark_info( + stats, + duration_check, + refinement.iter, + &instantiated_tasks, + ); + } + synth_report::print_synthesized_bodies( + &instantiated_tasks, + &synth_funcs, + k_induction_calls, + refinement.iter, + ); + instantiated_templates + }, + ); + + Ok((instantiated_templates, cegis_data.range_constraints)) +} diff --git a/src/driver/commands/verify.rs b/src/driver/commands/verify.rs index 60597bc0..44f7b474 100644 --- a/src/driver/commands/verify.rs +++ b/src/driver/commands/verify.rs @@ -11,7 +11,7 @@ use crate::{ model_check::run_model_checking, options::{ DebugOptions, InputOptions, LanguageServerOptions, ModelCheckingOptions, - OptimizationOptions, ResourceLimitOptions, SliceOptions, + OptimizationOptions, ResourceLimitOptions, SliceOptions, SynthesizerOptions, }, print_timings, }, @@ -50,6 +50,9 @@ pub struct VerifyCommand { #[command(flatten)] pub debug_options: DebugOptions, + + #[command(flatten)] + pub synth_options: SynthesizerOptions, } pub async fn run_verify_command(options: VerifyCommand) -> ExitCode { @@ -268,7 +271,7 @@ fn verify_files_main( // Lowering the quantitative task to a Boolean one. This contains (lazy) // unfolding, quantifier elimination, and various optimizations // (depending on options). - let vc_is_valid = lower_quant_prove_task(options, &limits_ref, &mut tcx, name, vc_expr)?; + let vc_is_valid = lower_quant_prove_task(options, &limits_ref, &tcx, name, vc_expr)?; let soundness_blame = &verify_unit.proc_soundness; @@ -276,7 +279,7 @@ fn verify_files_main( let ranges = collect_ranges_from_decls(&tcx.declarations.borrow()); let ranges_constraints: Vec = ranges .iter() - .map(|(ident, (range, ty))| create_range_constraint(ident.clone(), range, ty.clone())) + .map(|(ident, (range, ty))| create_range_constraint(*ident, range, ty.clone())) .collect(); let result = run_smt_prove_task_with_ranges( options, diff --git a/src/driver/item.rs b/src/driver/item.rs index c730b28b..5b4c8ae8 100644 --- a/src/driver/item.rs +++ b/src/driver/item.rs @@ -89,6 +89,14 @@ impl Item { &self.name } + pub fn value(&self) -> &T { + &self.item + } + + pub fn value_mut(&mut self) -> &mut T { + &mut self.item + } + pub fn enter_mut(&mut self) -> ItemEntered<'_, T> { ItemEntered { item: &mut self.item, @@ -146,7 +154,7 @@ impl Deref for Item { } pub struct ItemEntered<'a, T> { - item: &'a mut T, + pub item: &'a mut T, _entered: tracing::span::Entered<'a>, } diff --git a/src/driver/ranges.rs b/src/driver/ranges.rs index d138f686..1eccb60d 100644 --- a/src/driver/ranges.rs +++ b/src/driver/ranges.rs @@ -11,7 +11,7 @@ pub fn create_range_constraint(ident: Ident, range: &Range, ty: TyKind) -> Expr let (var, lower_lit, upper_lit) = match ty { TyKind::UReal => { - let var = builder.var_ty(ident.clone(), TyKind::UReal); + let var = builder.var_ty(ident, TyKind::UReal); let lower = builder.frac_lit_not_extended(BigRational::from_integer(range.lower.into())); let upper = @@ -19,7 +19,7 @@ pub fn create_range_constraint(ident: Ident, range: &Range, ty: TyKind) -> Expr (var, lower, upper) } _ => { - let var = builder.var_ty(ident.clone(), TyKind::UInt); + let var = builder.var_ty(ident, TyKind::UInt); let lower = builder.uint(range.lower.into()); let upper = builder.uint(range.upper.into()); (var, lower, upper) @@ -43,7 +43,7 @@ pub fn collect_ranges_from_decls( if let DeclKind::VarDecl(var_ref) = decl.as_ref() { let var = var_ref.borrow(); if let Some(range) = &var.range { - ranges.insert(*ident, (range.clone(), var.ty.clone())); + ranges.insert(*ident, (*range, var.ty.clone())); } } } diff --git a/src/driver/smt_proof.rs b/src/driver/smt_proof.rs index e790577b..00e8a995 100644 --- a/src/driver/smt_proof.rs +++ b/src/driver/smt_proof.rs @@ -20,6 +20,7 @@ use z3rro::{ util::{PrefixWriter, ReasonUnknown}, }; +use crate::ast::Expr; use crate::depgraph::DepGraph; use crate::driver::commands::options::{ DebugOptions, FunctionEncodingOption, QuantifierInstantiation, SliceVerifyMethod, @@ -27,7 +28,6 @@ use crate::driver::commands::options::{ use crate::driver::commands::verify::VerifyCommand; use crate::driver::error::CaesarError; use crate::driver::item::SourceUnitName; -use crate::ast::Expr; use crate::driver::quant_proof::{BoolVcProveTask, QuantVcProveTask}; use crate::proof_rules::calculus::ProcSoundness; use crate::slicing::transform::SliceStmts; @@ -149,10 +149,22 @@ pub fn run_smt_prove_task( vc_is_valid: BoolVcProveTask, proc_soundness: &ProcSoundness, ) -> Result { - run_smt_prove_task_with_ranges(options, limits_ref, tcx, depgraph, name, server, slice_vars, vc_is_valid, proc_soundness, &[]) + run_smt_prove_task_with_ranges( + options, + limits_ref, + tcx, + depgraph, + name, + server, + slice_vars, + vc_is_valid, + proc_soundness, + &[], + ) } -pub fn run_smt_prove_task_with_ranges( +#[allow(clippy::too_many_arguments)] +pub fn run_smt_prove_task_with_ranges<'a>( options: &VerifyCommand, limits_ref: &LimitsRef, tcx: &TyCtx, @@ -161,8 +173,8 @@ pub fn run_smt_prove_task_with_ranges( server: &mut dyn Server, slice_vars: SliceStmts, vc_is_valid: BoolVcProveTask, - proc_soundness: &ProcSoundness, - ranges_constraints: &[Expr], + proc_soundness: &'a ProcSoundness, + ranges_constraints: &'a [Expr], ) -> Result { let ctx = Context::new(&z3::Config::default()); let function_encoder = mk_function_encoder(tcx, depgraph, options)?; @@ -179,8 +191,14 @@ pub fn run_smt_prove_task_with_ranges( tracing::info!("Z3 tracing output will be written to `z3.log`."); } - let mut result = - vc_is_valid.run_solver_with_ranges(options, limits_ref, name, &ctx, &mut translate, &slice_vars,ranges_constraints)?; + let mut result = vc_is_valid.run_solver_with_ranges( + options, + limits_ref, + name, + &mut translate, + &slice_vars, + ranges_constraints, + )?; server .handle_vc_check_result(name, &mut result, &mut translate, proc_soundness) @@ -194,6 +212,26 @@ pub fn mk_function_encoder<'ctx>( tcx: &TyCtx, depgraph: &DepGraph, options: &VerifyCommand, +) -> Result + 'ctx>, CaesarError> { + mk_function_encoder_override( + tcx, + depgraph, + options, + options.opt_options.no_synonym_axiom, + None, + ) +} + +/// Like [`mk_function_encoder`] but lets the caller override the +/// `no_synonym_axiom` setting and the fuel bound independently of the CLI +/// options. When `max_fuel_override` is `Some(k)`, the fuel-based encodings +/// use `k` instead of `options.opt_options.max_fuel`. +pub fn mk_function_encoder_override<'ctx>( + tcx: &TyCtx, + depgraph: &DepGraph, + options: &VerifyCommand, + no_synonym_axiom: bool, + max_fuel_override: Option, ) -> Result + 'ctx>, CaesarError> { let fe_opt = options.opt_options.function_encoding; let partial_encoding = if options.opt_options.no_partial_strengthening { @@ -227,13 +265,13 @@ pub fn mk_function_encoder<'ctx>( let fuel_options = FuelEncodingOptions { fuel_functions, partial_encoding, - max_fuel: options.opt_options.max_fuel, + max_fuel: max_fuel_override.unwrap_or(options.opt_options.max_fuel), computation: matches!( fe_opt, FunctionEncodingOption::FuelMonoComputation | FunctionEncodingOption::FuelParamComputation ), - synonym_axiom: !options.opt_options.no_synonym_axiom, + synonym_axiom: !no_synonym_axiom, }; match fe_opt { FunctionEncodingOption::FuelMono | FunctionEncodingOption::FuelMonoComputation => { @@ -318,7 +356,6 @@ impl<'ctx> SmtVcProveTask<'ctx> { options: &VerifyCommand, limits_ref: &LimitsRef, name: &SourceUnitName, - ctx: &'ctx Context, translate: &mut TranslateExprs<'smt, 'ctx>, slice_vars: &SliceStmts, ranges_constraints: &[Expr], @@ -326,10 +363,11 @@ impl<'ctx> SmtVcProveTask<'ctx> { let span = info_span!("SAT check"); let _entered = span.enter(); + let ctx = translate.ctx.ctx(); let mut prover = mk_valid_query_prover(limits_ref, ctx, translate, &self.vc); for constraint in ranges_constraints { - prover.add_assumption(&translate.t_bool(&constraint)); + prover.add_assumption(&translate.t_bool(constraint)); } if options.debug_options.z3_probe { let goal = Goal::new(ctx, false, false, false); @@ -337,7 +375,7 @@ impl<'ctx> SmtVcProveTask<'ctx> { goal.assert(&assertion); } eprintln!( - "In verifier (getting pvar cex): Probe results for {}:\n{}", + "Probe results for {}:\n{}", name, ProbeSummary::probe(ctx, &goal) ); @@ -442,6 +480,25 @@ impl<'ctx> SmtVcProveTask<'ctx> { } } +/// Check whether `vc` is valid under the current SMT context and the given +/// range assumptions. Returns the solver verdict and, on counterexample, the +/// model. Uses a fresh one-shot prover — no slicing, no server notification. +pub fn check_valid<'smt, 'ctx>( + vc: &Bool<'ctx>, + limits_ref: &LimitsRef, + translate: &mut TranslateExprs<'smt, 'ctx>, + ranges_constraints: &[Expr], +) -> (ProveResult, Option>) { + let ctx = translate.ctx.ctx(); + let mut prover = mk_valid_query_prover(limits_ref, ctx, translate, vc); + for constraint in ranges_constraints { + prover.add_assumption(&translate.t_bool(constraint)); + } + let result = prover.check_proof(); + let model = prover.get_model(); + (result, model) +} + fn mk_valid_query_prover<'smt, 'ctx>( limits_ref: &LimitsRef, ctx: &'ctx Context, diff --git a/src/front/parser/grammar.lalrpop b/src/front/parser/grammar.lalrpop index 948b28f7..82372240 100644 --- a/src/front/parser/grammar.lalrpop +++ b/src/front/parser/grammar.lalrpop @@ -320,7 +320,7 @@ DomainSpec: DomainSpec = { "func" ":" "=" => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output, body: RefCell::new(Some(body)), syn: false, computable: false, span: span(file, l, r) })), "syn" "func" ":" - => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output: output, body: RefCell::new(None), syn: true, computable: false, span: span(file, l, r) })), + => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output, body: RefCell::new(None), syn: true, computable: false, span: span(file, l, r) })), "axiom" => DomainSpec::Axiom(DeclRef::new(AxiomDecl{ name, axiom, span: span(file, l, r) })) } diff --git a/src/main.rs b/src/main.rs index a1df5e82..76fe2cd8 100644 --- a/src/main.rs +++ b/src/main.rs @@ -22,6 +22,7 @@ mod scope_map; mod servers; mod slicing; mod smt; +mod synthesis; mod timing; mod tyctx; mod vc; diff --git a/src/smt/translate_exprs.rs b/src/smt/translate_exprs.rs index cb3fcc77..59bb20aa 100644 --- a/src/smt/translate_exprs.rs +++ b/src/smt/translate_exprs.rs @@ -880,4 +880,4 @@ impl<'ctx> TranslateCache<'ctx> { } } -type CacheExpr = RefEqShared; \ No newline at end of file +type CacheExpr = RefEqShared; diff --git a/src/synthesis/cegis.rs b/src/synthesis/cegis.rs new file mode 100644 index 00000000..f971df74 --- /dev/null +++ b/src/synthesis/cegis.rs @@ -0,0 +1,542 @@ +use indexmap::{IndexMap, IndexSet}; +use num::{BigInt, BigRational, Signed, Zero}; +use std::time::{Duration, Instant}; + +use z3::{Context, Goal}; +use z3rro::{ + eureal::ConcreteEUReal, + model::{InstrumentedModel, SmtEval}, + probes::ProbeSummary, + prover::{IncrementalMode, ProveResult, Prover}, + util::ReasonUnknown, +}; + +use crate::{ + ast::{ + self, visit::VisitorMut, Expr, ExprBuilder, ExprData, ExprKind, Ident, LitKind, Shared, + Span, TyKind, + }, + driver::{ + commands::verify::VerifyCommand, + error::CaesarError, + item::SourceUnitName, + quant_proof::{BoolVcProveTask, QuantVcProveTask}, + smt_proof::{check_valid, SmtVcProveTask}, + }, + opt::unfolder::Unfolder, + resource_limits::LimitsRef, + smt::{ + symbolic::Symbolic, + translate_exprs::TranslateExprs, + uninterpreted::{FuncEntry, Uninterpreteds}, + SmtCtx, + }, + synthesis::{report::SynthStats, templates::TemplateEntry}, +}; + +const MAX_CEGIS_ITERS: usize = 3000; +const CLOSE_CEX_DISTANCE_THRESHOLD: i64 = 3; +const MAX_CLOSE_CEX_COUNT: usize = 100; + +pub fn create_subst_mapping<'ctx>( + idents: &IndexSet, + model: &InstrumentedModel<'ctx>, + translate: &mut crate::smt::translate_exprs::TranslateExprs<'_, 'ctx>, +) -> IndexMap { + let builder = ExprBuilder::new(Span::dummy_span()); + let mut mapping = IndexMap::new(); + + for &ident in idents { + let var_expr = builder.var(ident, translate.ctx.tcx()); + let symbolic = translate.t_symbolic(&var_expr); + + let lit_opt = match &symbolic { + Symbolic::Bool(v) => { + let b = v + .eval(model) + .unwrap_or_else(|e| panic!("SMT eval failed for Bool {ident:?}: {e}")); + Some(builder.bool_lit(b)) + } + + Symbolic::Int(v) => { + let i: BigInt = v + .eval(model) + .unwrap_or_else(|e| panic!("SMT eval failed for Int {ident:?}: {e}")); + Some(builder.int_lit(i)) + } + + Symbolic::UInt(v) => { + let i: BigInt = v + .eval(model) + .unwrap_or_else(|e| panic!("SMT eval failed for UInt {ident:?}: {e}")); + + let lit = if let Some(u) = i.to_biguint() { + builder.uint_lit(u) + } else { + // Negative value from model — shouldn't happen for UInt, but fall back gracefully + builder.frac_lit(BigRational::from_integer(i)) + }; + + Some(lit) + } + + Symbolic::Real(v) => { + let r: BigRational = v + .eval(model) + .unwrap_or_else(|e| panic!("SMT eval failed for Real {ident:?}: {e}")); + Some(builder.signed_frac_lit(r)) + } + + Symbolic::UReal(v) => { + let r: BigRational = v + .eval(model) + .unwrap_or_else(|e| panic!("SMT eval failed for UReal {ident:?}: {e}")); + Some(builder.frac_lit_not_extended(r)) + } + + Symbolic::EUReal(v) => { + let r = v + .eval(model) + .unwrap_or_else(|e| panic!("SMT eval failed for EUReal {ident:?}: {e}")); + + let lit = match r { + ConcreteEUReal::Real(rat) => builder.frac_lit(rat), + ConcreteEUReal::Infinity => builder.infinity_lit(), + }; + + Some(lit) + } + + Symbolic::List(_) | Symbolic::Fuel(_) | Symbolic::Uninterpreted(_) => None, + }; + + if let Some(lit) = lit_opt { + mapping.insert(ident, lit); + } + } + + mapping +} + +/// Wraps `vc` in nested `Subst` nodes for each entry in `mapping`, then unfolds. +pub fn subst_from_mapping<'ctx>( + mapping: &IndexMap, + vc: &Expr, + limits_ref: &LimitsRef, + smt_ctx: &SmtCtx<'ctx>, +) -> Result { + let mut wrapped = vc.clone(); + for (&ident, expr) in mapping { + let ty = wrapped.ty.clone(); + let inner = wrapped; + wrapped = Shared::new(ExprData { + kind: ExprKind::Subst(ident, expr.clone(), inner), + ty, + span: vc.span, + }); + } + + let mut unfolder = Unfolder::new(limits_ref.clone(), smt_ctx); + unfolder.visit_expr(&mut wrapped)?; + Ok(wrapped) +} + +pub fn get_model_for_constraints<'smt, 'ctx, 'tcx: 'ctx>( + prover: &mut Prover<'ctx>, + options: &VerifyCommand, + constraints: BoolVcProveTask, + translate: &mut TranslateExprs<'smt, 'ctx>, + idents: &IndexSet, + ctx: &'ctx Context, +) -> Result>, CaesarError> { + let mut smt_task = SmtVcProveTask::translate(constraints, translate); + + if !options.opt_options.no_simplify { + smt_task.simplify(); + } + + prover.add_assumption(&smt_task.vc); + + if options.debug_options.print_smt { + println!("Current solver state for constraints:"); + println!("{}", prover.get_smtlib().into_string()); + } + + if options.debug_options.z3_probe { + let goal = Goal::new(ctx, false, false, false); + for assertion in prover.get_assertions() { + goal.assert(&assertion); + } + eprintln!( + "Constraint Probe results: {}", + ProbeSummary::probe(ctx, &goal) + ); + } + let res = prover.check_sat(); + + match res { + z3::SatResult::Unsat | z3::SatResult::Unknown => return Ok(None), + z3::SatResult::Sat => {} + } + + if let Some(model) = prover.get_model() { + let mapping = create_subst_mapping(idents, &model, translate); + Ok(Some(mapping)) + } else { + Ok(None) + } +} + +/// Returns a canonical string representation of `map`, used for CEGIS cycle detection. +pub fn canonical_form(map: &IndexMap) -> String { + let mut items: Vec<_> = map.iter().collect(); + + items.sort_by_key(|(ident, _)| ident.name); + + items + .into_iter() + .map(|(ident, expr)| format!("{}={}", ident, expr)) + .collect::>() + .join(";") +} + +/// Returns all synthesised (`syn`) functions from the uninterpreted-function store. +pub fn get_synth_functions<'ctx>( + uninterps: &'ctx Uninterpreteds<'ctx>, +) -> IndexMap> { + uninterps + .functions() + .iter() + .filter_map(|(id, f)| f.syn.then_some((*id, f))) + .collect() +} + +/// Returns the absolute difference between two numeric literal expressions, or zero for non-numeric. +pub fn expr_lit_distance(a: &Expr, b: &Expr) -> BigRational { + match (expr_to_rational(a), expr_to_rational(b)) { + (Some(rat_a), Some(rat_b)) => (rat_a - rat_b).abs(), + _ => BigRational::zero(), + } +} + +// Extracts a rational value from a literal; None for non-numeric literals. +pub fn expr_to_rational(e: &Expr) -> Option { + match &e.kind { + ExprKind::Lit(lit) => match &lit.node { + LitKind::UInt(n) => Some(BigRational::from(BigInt::from(n.clone()))), + LitKind::Int(n) => Some(BigRational::from(n.clone())), + LitKind::Frac(f) => Some(f.clone()), + _ => None, + }, + _ => None, + } +} + +/// All data for one per-item CEGIS session: templates, program variables, +/// range constraints, and the verification condition. +pub struct CegisData { + pub templates: Vec, + pub pvar_idents: IndexSet, + pub tvars: Vec<(Ident, TyKind)>, + pub range_constraints: Vec, + pub boolean_vc: BoolVcProveTask, + pub vc_expr: QuantVcProveTask, +} + +pub struct VerifyOutcome { + /// The template-variable assignment used for this check (zeros for unset vars). + pub zero_extended_mapping: IndexMap, + pub kind: VerifyOutcomeKind, +} + +pub enum VerifyOutcomeKind { + Proof, + /// Program-variable counterexample extracted from the model. + Counterexample(IndexMap), + Unknown(ReasonUnknown), + /// Solver returned counterexample but produced no model. + NoModel, +} + +/// Run the verifier side of one CEGIS iteration: instantiate the current +/// template-variable mapping, check the VC, and return the outcome. +pub fn verify_candidate<'smt, 'ctx>( + data: &CegisData, + tvar_mapping: &IndexMap, + limits_ref: &LimitsRef, + translate: &mut TranslateExprs<'smt, 'ctx>, +) -> Result { + let builder = ExprBuilder::new(Span::dummy_span()); + + let zero_extended_mapping: IndexMap = data + .tvars + .iter() + .map(|(id, ty)| { + let val = tvar_mapping + .get(id) + .cloned() + .unwrap_or_else(|| builder.zero_lit(ty)); + (*id, val) + }) + .collect(); + + let bool_vc_inst = subst_from_mapping( + &zero_extended_mapping, + &data.boolean_vc.vc, + limits_ref, + translate.ctx, + )?; + let vc_z3 = translate.t_bool(&bool_vc_inst); + let (prove_result, model) = check_valid(&vc_z3, limits_ref, translate, &data.range_constraints); + + let kind = match prove_result { + ProveResult::Proof => VerifyOutcomeKind::Proof, + ProveResult::Counterexample => match model { + Some(model) => { + let cex_mapping = create_subst_mapping(&data.pvar_idents, &model, translate); + VerifyOutcomeKind::Counterexample(cex_mapping) + } + None => VerifyOutcomeKind::NoModel, + }, + ProveResult::Unknown(reason) => VerifyOutcomeKind::Unknown(reason), + }; + + Ok(VerifyOutcome { + zero_extended_mapping, + kind, + }) +} + +/// Run the synthesizer side of one CEGIS iteration: add the counterexample +/// constraint to the incremental prover and find new template-variable values. +pub fn synthesize_from_cex<'smt, 'ctx>( + data: &CegisData, + prover: &mut Prover<'ctx>, + prover_initialized: &mut bool, + options: &VerifyCommand, + limits_ref: &LimitsRef, + translate: &mut TranslateExprs<'smt, 'ctx>, + cex_mapping: &IndexMap, +) -> Result>, CaesarError> { + if !*prover_initialized { + translate.ctx.add_lit_axioms_to_prover(prover); + translate.ctx.uninterpreteds().add_axioms_to_prover(prover); + // Pre-initialize template vars so their type invariants (e.g. >= 0 for UReal) + // are in the local scope before add_assumptions_to_prover flushes it. + for (tvar_id, _) in &data.tvars { + translate.get_local(*tvar_id); + } + translate.local_scope().add_assumptions_to_prover(prover); + for constraint in &data.range_constraints { + prover.add_assumption(&translate.t_bool(constraint)); + } + *prover_initialized = true; + } + + let bool_vc_inst = + subst_from_mapping(cex_mapping, &data.boolean_vc.vc, limits_ref, translate.ctx)?; + let cex_task = BoolVcProveTask { + quant_vc: data.vc_expr.clone(), + vc: bool_vc_inst, + }; + get_model_for_constraints( + prover, + options, + cex_task, + translate, + &data.tvars.iter().map(|(id, _)| *id).collect(), + translate.ctx.ctx(), + ) +} + +/// Proof found by the CEGIS loop: the synthesized function bodies and the +/// verification tasks used to confirm them. +pub struct CegisProof { + pub instantiated_templates: Vec<(Ident, Expr)>, + pub instantiated_tasks: Vec<(Ident, QuantVcProveTask, usize, usize, bool)>, + pub duration_check: Duration, +} + +/// Run the CEGIS loop: repeatedly verify the current candidate and synthesize +/// a new one from counterexamples until a proof is found or the iteration +/// budget is exhausted. Returns `None` if no proof was found. +pub fn run_cegis_loop<'smt, 'ctx>( + data: &CegisData, + ctx: &'ctx Context, + translate: &mut TranslateExprs<'smt, 'ctx>, + options: &VerifyCommand, + limits_ref: &LimitsRef, + name: &SourceUnitName, + stats: &mut SynthStats, +) -> Result, CaesarError> { + let direction = data.vc_expr.direction; + + let mut tvar_mapping: IndexMap = IndexMap::new(); + let mut seen_tvar_maps: IndexSet = IndexSet::new(); + let mut seen_cex_maps: IndexSet = IndexSet::new(); + let mut prover = Prover::new(ctx, IncrementalMode::Native); + if let Some(remaining) = limits_ref.time_left() { + prover.set_timeout(remaining); + } + let mut prover_initialized = false; + let mut close_cex_count: usize = 0; + let mut prev_cex_mapping: Option> = None; + let mut duration_check = Duration::ZERO; + let mut proof: Option = None; + let mut iteration: usize = 0; + + loop { + iteration += 1; + if options.synth_options.syn_verbose { + println!("=== CEGIS loop {iteration} ==="); + } + + let check_start = Instant::now(); + let outcome = verify_candidate(data, &tvar_mapping, limits_ref, translate)?; + duration_check += check_start.elapsed(); + + if !seen_tvar_maps.insert(canonical_form(&outcome.zero_extended_mapping)) { + return Err(CaesarError::UserError( + "Template-variable mapping appeared twice; CEGIS is cycling.".into(), + )); + } + + match outcome.kind { + VerifyOutcomeKind::Proof => { + let vc_deps = data.vc_expr.deps.clone(); + let mut instantiated_tasks = Vec::new(); + let mut instantiated_templates = Vec::new(); + for t in data.templates.iter() { + let concrete_expr = subst_from_mapping( + &outcome.zero_extended_mapping, + &t.expr, + limits_ref, + translate.ctx, + )?; + instantiated_templates.push((t.synth_name, concrete_expr.clone())); + let mut task = QuantVcProveTask { + expr: concrete_expr, + direction, + deps: vc_deps.clone(), + }; + task.remove_neutrals(limits_ref, translate.ctx.tcx())?; + instantiated_tasks.push(( + t.synth_name, + task, + t.guards_before_pruning, + t.guards_after_pruning, + t.loop_mode, + )); + } + proof = Some(CegisProof { + instantiated_templates, + instantiated_tasks, + duration_check, + }); + break; + } + + VerifyOutcomeKind::Counterexample(cex_mapping) => { + stats.cex_count += 1; + + if options.synth_options.syn_verbose { + println!("Counterexample:"); + let mut entries: Vec<_> = cex_mapping.iter().collect(); + entries.sort_by_key(|(id, _)| &id.name); + for (id, val) in &entries { + println!(" {} -> {val}", id.name); + } + println!(); + } + + if !seen_cex_maps.insert(canonical_form(&cex_mapping)) { + return Err(CaesarError::UserError( + "Counterexample appeared twice; CEGIS is cycling.".into(), + )); + } + + if let Some(ref prev) = prev_cex_mapping { + let pvars: Vec<_> = cex_mapping + .iter() + .filter(|(id, _)| !data.tvars.iter().any(|(tid, _)| tid == *id)) + .collect(); + let has_numeric = pvars.iter().any(|(_, val)| expr_to_rational(val).is_some()); + // Distance is meaningless when all program variables are Boolean: + // expr_lit_distance returns 0 for non-numeric pairs, so every CEX + // would appear "close" and trigger premature refinement. + if has_numeric { + let dist: BigRational = pvars + .iter() + .filter_map(|(id, val)| { + prev.get(*id) + .map(|prev_val| expr_lit_distance(val, prev_val)) + }) + .sum(); + if dist <= BigRational::from_integer(CLOSE_CEX_DISTANCE_THRESHOLD.into()) { + close_cex_count += 1; + if options.synth_options.syn_verbose { + println!( + "Close CEX (distance={dist}), total count: {close_cex_count}" + ); + } + if close_cex_count >= MAX_CLOSE_CEX_COUNT { + if options.synth_options.syn_verbose { + println!( + "Close CEX threshold reached ({close_cex_count} total, \ + distance <= {CLOSE_CEX_DISTANCE_THRESHOLD}); \ + moving to next template refinement." + ); + } + stats.close_cex_refinements += 1; + break; + } + } + } // if has_numeric + } + if iteration >= MAX_CEGIS_ITERS { + if options.synth_options.syn_verbose { + println!("Reached max CEGIS iterations ({iteration}) for `{name}`."); + } + break; + } + + match synthesize_from_cex( + data, + &mut prover, + &mut prover_initialized, + options, + limits_ref, + translate, + &cex_mapping, + )? { + Some(new_tvar_map) => tvar_mapping = new_tvar_map, + None => { + if options.synth_options.syn_verbose { + println!( + "No template model found; stopping CEGIS after iteration {iteration}." + ); + } + break; + } + } + prev_cex_mapping = Some(cex_mapping); + } + + VerifyOutcomeKind::NoModel => { + if options.synth_options.syn_verbose { + println!("Counterexample had no model; stopping."); + } + break; + } + + VerifyOutcomeKind::Unknown(reason) => { + if options.synth_options.syn_verbose { + println!("Solver returned unknown for `{name}`: {reason}"); + } + break; + } + } + } + + Ok(proof) +} diff --git a/src/synthesis/k_induction.rs b/src/synthesis/k_induction.rs new file mode 100644 index 00000000..9f54457e --- /dev/null +++ b/src/synthesis/k_induction.rs @@ -0,0 +1,112 @@ +use std::convert::Infallible; + +use indexmap::IndexMap; +use num::BigUint; + +use crate::{ + ast::util::lit_u128, + ast::{ + visit::{walk_stmt, VisitorMut}, + ExprData, ExprKind, LitKind, Shared, Spanned, Stmt, StmtKind, Symbol, + }, + driver::front::{Module, SourceUnit}, +}; + +/// Returns the `k` argument of the first `@k_induction` annotation found in `module`, if any. +pub fn read_k_induction_k(module: &mut Module) -> Option { + let mut visitor = FindK; + for item in &mut module.items { + let result = match item.value_mut() { + SourceUnit::Decl(decl) => visitor.visit_decl(decl), + SourceUnit::Raw(block) => visitor.visit_block(block), + }; + if let Err(k) = result { + return Some(k); + } + } + None +} + +/// Collects all `@k_induction(k, inv_call)` annotations in `module` and +/// returns a map from synth-function name to the invariant call string. +pub fn collect_k_induction_calls(module: &mut Module) -> IndexMap { + let mut visitor = CollectKCalls(IndexMap::new()); + for item in &mut module.items { + match item.value_mut() { + SourceUnit::Decl(decl) => visitor.visit_decl(decl).unwrap(), + SourceUnit::Raw(block) => visitor.visit_block(block).unwrap(), + } + } + visitor.0 +} + +/// Traverses `module` and replaces the k literal in every `@k_induction(k, ...)` +/// annotation with `new_k`. +pub fn set_k_induction_k(module: &mut Module, new_k: u128) { + let mut visitor = SetK(new_k); + for item in &mut module.items { + match item.value_mut() { + SourceUnit::Decl(decl) => visitor.visit_decl(decl).unwrap(), + SourceUnit::Raw(block) => visitor.visit_block(block).unwrap(), + } + } +} + +struct FindK; + +impl VisitorMut for FindK { + type Err = u128; + + fn visit_stmt(&mut self, s: &mut Stmt) -> Result<(), u128> { + if let StmtKind::Annotation(_, ident, args, _) = &s.node { + if ident.name == *"k_induction" { + if let Some(first) = args.first() { + return Err(lit_u128(first)); + } + } + } + walk_stmt(self, s) + } +} + +struct CollectKCalls(IndexMap); + +impl VisitorMut for CollectKCalls { + type Err = Infallible; + + fn visit_stmt(&mut self, s: &mut Stmt) -> Result<(), Infallible> { + if let StmtKind::Annotation(_, ident, args, _) = &s.node { + if ident.name == *"k_induction" && args.len() == 2 { + let inv_expr = &args[1]; + let inv_str = inv_expr.to_string(); + if let ExprKind::Call(func_ident, _) = &inv_expr.kind { + self.0.entry(func_ident.name).or_insert(inv_str); + } + } + } + walk_stmt(self, s) + } +} + +struct SetK(u128); + +impl VisitorMut for SetK { + type Err = Infallible; + + fn visit_stmt(&mut self, s: &mut Stmt) -> Result<(), Infallible> { + if let StmtKind::Annotation(_, ident, args, _) = &mut s.node { + if ident.name == *"k_induction" { + if let Some(first) = args.first_mut() { + *first = Shared::new(ExprData { + kind: ExprKind::Lit(Spanned::with_dummy_span(LitKind::UInt( + BigUint::from(self.0), + ))), + ty: first.ty.clone(), + span: first.span, + }); + } + } + } + walk_stmt(self, s) + } +} diff --git a/src/synthesis/mod.rs b/src/synthesis/mod.rs new file mode 100644 index 00000000..dcc82bdf --- /dev/null +++ b/src/synthesis/mod.rs @@ -0,0 +1,5 @@ +pub mod cegis; +pub mod k_induction; +pub mod rec_functions; +pub mod report; +pub mod templates; diff --git a/src/synthesis/rec_functions/approx_encoding.rs b/src/synthesis/rec_functions/approx_encoding.rs new file mode 100644 index 00000000..b9b2b662 --- /dev/null +++ b/src/synthesis/rec_functions/approx_encoding.rs @@ -0,0 +1,666 @@ +use crate::{ + ast::{ + visit::{walk_expr, walk_stmt, VisitorMut}, + BinOpKind, DeclKind, Direction, Expr, ExprBuilder, ExprData, ExprKind, Ident, Shared, Span, + Spanned, Stmt, StmtKind, TyKind, UnOpKind, + }, + tyctx::TyCtx, +}; + +// Collects every call expression `f(args)` where `f` is one of the target +// functions, anywhere inside a walked expression. +struct CallCollector<'a> { + funcs: &'a [Ident], + tcx: &'a TyCtx, + calls: Vec, +} + +impl<'a> CallCollector<'a> { + fn new(funcs: &'a [Ident], tcx: &'a TyCtx) -> Self { + Self { + funcs, + tcx, + calls: Vec::new(), + } + } + + /// Returns true if `func` is a `FuncDecl` with a defining body (as opposed to uninterpreted). + fn has_body(&self, func: &Ident) -> bool { + self.tcx + .get(*func) + .and_then(|decl| { + if let DeclKind::FuncDecl(func_ref) = decl.as_ref() { + Some(func_ref.borrow().body.borrow().is_some()) + } else { + None + } + }) + .unwrap_or(false) + } +} + +impl<'a> VisitorMut for CallCollector<'a> { + type Err = (); + + fn visit_expr(&mut self, e: &mut Expr) -> Result<(), Self::Err> { + if let ExprKind::Call(ref func, _) = e.kind { + if self.funcs.contains(func) && self.has_body(func) { + self.calls.push(e.clone()); + // Don't recurse: this call's definedness guard already covers + // any nested calls by inlining the body. + return Ok(()); + } + } + walk_expr(self, e) + } +} + +// Substitutes every free occurrence of `var` with `val` in an expression, +// stopping at binders that shadow `var` (capture-avoiding). +struct SubstVisitor<'a> { + var: Ident, + val: &'a Expr, +} + +impl<'a> VisitorMut for SubstVisitor<'a> { + type Err = (); + + fn visit_expr(&mut self, e: &mut Expr) -> Result<(), Self::Err> { + enum Action { + Replace, + SubstValOnly, + BodyOnly, + Skip, + Walk, + } + let action = match &e.kind { + ExprKind::Var(v) if *v == self.var => Action::Replace, + ExprKind::Subst(bound, _, _) if *bound == self.var => Action::SubstValOnly, + ExprKind::Quant(_, qvars, _, _) if qvars.iter().any(|qv| qv.name() == self.var) => { + Action::Skip + } + ExprKind::Quant(..) => Action::BodyOnly, + _ => Action::Walk, + }; + match action { + Action::Replace => *e = self.val.clone(), + Action::SubstValOnly => { + if let ExprKind::Subst(_, by, _) = &mut e.kind { + self.visit_expr(by)?; + } + } + Action::BodyOnly => { + if let ExprKind::Quant(_, _, _, body) = &mut e.kind { + self.visit_expr(body)?; + } + } + Action::Skip => {} + Action::Walk => walk_expr(self, e)?, + } + Ok(()) + } +} + +fn subst_var(expr: &Expr, var: &Ident, val: &Expr) -> Expr { + let mut result = expr.clone(); + SubstVisitor { var: *var, val } + .visit_expr(&mut result) + .unwrap(); + result +} + +// Returns the body (if any) and formal parameter names of `func` from `tcx`. +fn get_func_body_params(func: &Ident, tcx: &TyCtx) -> Option<(Option, Vec)> { + tcx.get(*func).and_then(|decl| { + if let DeclKind::FuncDecl(func_ref) = decl.as_ref() { + let func_decl = func_ref.borrow(); + let body = func_decl.body.borrow().clone(); + let params = func_decl.inputs.node.iter().map(|p| p.name).collect(); + Some((body, params)) + } else { + None + } + }) +} + +// Compute the fuel-limited approximant e^fuel of `expr` (def:approxexpr): +// replace each call to a target function with its inlined body, recursing at +// fuel-1, and leave the call node as-is when fuel is exhausted (f^0). +fn approx_expr(expr: &Expr, fuel: usize, func_idents: &[Ident], tcx: &TyCtx) -> Expr { + let builder = ExprBuilder::new(expr.span); + + match &expr.kind { + ExprKind::Call(func, args) if func_idents.contains(func) => { + let body_params = get_func_body_params(func, tcx); + + match body_params { + Some((Some(body), params)) if fuel > 0 => { + let mut inst_body = body; + for (param, arg) in params.iter().zip(args.iter()) { + inst_body = subst_var(&inst_body, param, arg); + } + approx_expr(&inst_body, fuel - 1, func_idents, tcx) + } + // Fuel exhausted or no body: return the call node unchanged (f^0). + _ => expr.clone(), + } + } + + ExprKind::Var(_) | ExprKind::Call(_, _) | ExprKind::Lit(_) => expr.clone(), + + ExprKind::Ite(cond, then_, else_) => { + let then_approx = approx_expr(then_, fuel, func_idents, tcx); + let else_approx = approx_expr(else_, fuel, func_idents, tcx); + builder.ite(expr.ty.clone(), cond.clone(), then_approx, else_approx) + } + + ExprKind::Binary(bin_op, lhs, rhs) => { + let lhs_approx = approx_expr(lhs, fuel, func_idents, tcx); + let rhs_approx = approx_expr(rhs, fuel, func_idents, tcx); + builder.binary(bin_op.node, expr.ty.clone(), lhs_approx, rhs_approx) + } + + ExprKind::Unary(un_op, inner) => { + let inner_approx = approx_expr(inner, fuel, func_idents, tcx); + builder.unary(un_op.node, expr.ty.clone(), inner_approx) + } + + ExprKind::Cast(inner) => { + let inner_approx = approx_expr(inner, fuel, func_idents, tcx); + Shared::new(ExprData { + kind: ExprKind::Cast(inner_approx), + ty: expr.ty.clone(), + span: expr.span, + }) + } + + ExprKind::Subst(bound, subst_val, body) => { + let subst_body = subst_var(body, bound, subst_val); + approx_expr(&subst_body, fuel, func_idents, tcx) + } + + ExprKind::Quant(quant, vars, triggers, body) => { + let body_approx = approx_expr(body, fuel, func_idents, tcx); + Shared::new(ExprData { + kind: ExprKind::Quant(*quant, vars.clone(), triggers.clone(), body_approx), + ty: expr.ty.clone(), + span: expr.span, + }) + } + } +} + +fn cast_to_eureal(expr: Expr) -> Expr { + if expr.ty.as_ref() == Some(&TyKind::EUReal) { + return expr; + } + let span = expr.span; + Shared::new(ExprData { + kind: ExprKind::Cast(expr), + ty: Some(TyKind::EUReal), + span, + }) +} + +// Compute the Boolean guard B_k(b) for a Boolean sub-expression b. +// B_k(b) is true iff the fuel-k approximant of b does not bottom out (\bot). +// Mirrors the short-circuit semantics of Boolean operators: +// - && has absorber false: one false operand makes the conjunction defined. +// - || has absorber true: one true operand makes the disjunction defined. +fn bool_definedness_guard(expr: &Expr, fuel: usize, func_idents: &[Ident], tcx: &TyCtx) -> Expr { + let builder = ExprBuilder::new(expr.span); + + match &expr.kind { + // Literals and variables are always defined. + ExprKind::Lit(_) | ExprKind::Var(_) => builder.bool_lit(true), + + // Comparison (a1 op a2): both quantitative operands must be defined. + ExprKind::Binary(bin_op, lhs, rhs) + if matches!( + bin_op.node, + BinOpKind::Eq + | BinOpKind::Ne + | BinOpKind::Lt + | BinOpKind::Le + | BinOpKind::Ge + | BinOpKind::Gt + ) => + { + let lhs_def = definedness_guard(lhs, fuel, func_idents, tcx); + let rhs_def = definedness_guard(rhs, fuel, func_idents, tcx); + builder.binary(BinOpKind::And, Some(TyKind::Bool), lhs_def, rhs_def) + } + + // Boolean conjunction (b1 && b2): absorber is false. + // B_k(b1 && b2) = (B_k(b1) && b1_approx=false) + // || (B_k(b2) && b2_approx=false) + // || (B_k(b1) && B_k(b2)) + ExprKind::Binary(bin_op, lhs, rhs) if bin_op.node == BinOpKind::And => { + let lhs_approx = approx_expr(lhs, fuel, func_idents, tcx); + let rhs_approx = approx_expr(rhs, fuel, func_idents, tcx); + let lhs_def = bool_definedness_guard(lhs, fuel, func_idents, tcx); + let rhs_def = bool_definedness_guard(rhs, fuel, func_idents, tcx); + let false_lit = builder.bool_lit(false); + let lhs_is_false = builder.binary( + BinOpKind::Eq, + Some(TyKind::Bool), + lhs_approx, + false_lit.clone(), + ); + let rhs_is_false = + builder.binary(BinOpKind::Eq, Some(TyKind::Bool), rhs_approx, false_lit); + let lhs_absorbed = builder.binary( + BinOpKind::And, + Some(TyKind::Bool), + lhs_def.clone(), + lhs_is_false, + ); + let rhs_absorbed = builder.binary( + BinOpKind::And, + Some(TyKind::Bool), + rhs_def.clone(), + rhs_is_false, + ); + let both_def = builder.binary(BinOpKind::And, Some(TyKind::Bool), lhs_def, rhs_def); + let one_absorbed = builder.binary( + BinOpKind::Or, + Some(TyKind::Bool), + lhs_absorbed, + rhs_absorbed, + ); + builder.binary(BinOpKind::Or, Some(TyKind::Bool), one_absorbed, both_def) + } + + // Boolean disjunction (b1 || b2): absorber is true. + // B_k(b1 || b2) = (B_k(b1) && b1_approx=true) + // || (B_k(b2) && b2_approx=true) + // || (B_k(b1) && B_k(b2)) + ExprKind::Binary(bin_op, lhs, rhs) if bin_op.node == BinOpKind::Or => { + let lhs_approx = approx_expr(lhs, fuel, func_idents, tcx); + let rhs_approx = approx_expr(rhs, fuel, func_idents, tcx); + let lhs_def = bool_definedness_guard(lhs, fuel, func_idents, tcx); + let rhs_def = bool_definedness_guard(rhs, fuel, func_idents, tcx); + let true_lit = builder.bool_lit(true); + let lhs_is_true = builder.binary( + BinOpKind::Eq, + Some(TyKind::Bool), + lhs_approx, + true_lit.clone(), + ); + let rhs_is_true = + builder.binary(BinOpKind::Eq, Some(TyKind::Bool), rhs_approx, true_lit); + let lhs_absorbed = builder.binary( + BinOpKind::And, + Some(TyKind::Bool), + lhs_def.clone(), + lhs_is_true, + ); + let rhs_absorbed = builder.binary( + BinOpKind::And, + Some(TyKind::Bool), + rhs_def.clone(), + rhs_is_true, + ); + let both_def = builder.binary(BinOpKind::And, Some(TyKind::Bool), lhs_def, rhs_def); + let one_absorbed = builder.binary( + BinOpKind::Or, + Some(TyKind::Bool), + lhs_absorbed, + rhs_absorbed, + ); + builder.binary(BinOpKind::Or, Some(TyKind::Bool), one_absorbed, both_def) + } + + // Boolean negation (!b): propagate through. + ExprKind::Unary(un_op, inner) if un_op.node == UnOpKind::Not => { + bool_definedness_guard(inner, fuel, func_idents, tcx) + } + + // Subst: apply substitution and recurse. + ExprKind::Subst(bound, subst_val, body) => { + let subst_body = subst_var(body, bound, subst_val); + bool_definedness_guard(&subst_body, fuel, func_idents, tcx) + } + + // Anything else (calls, other unary, quantifiers): delegate to G_k. + _ => definedness_guard(expr, fuel, func_idents, tcx), + } +} + +// Compute the quantitative definedness guard G_k(e) for expression e (def:defguard). +// G_k(e) is true iff the fuel-k approximant e^k does not bottom out (\bot). +// Mirrors the \bot-extended semantics of quantitative operators (def:botabsorption): +// - * and \sqcap have absorber 0: one zero operand makes the result defined. +// - \sqcup has absorber \infty: one infinite operand makes the result defined. +// - -> has absorbers 0 (left) and \infty (right). +// - <- has absorbers \infty (left) and 0 (right). +// ITE additionally requires B_k on the condition, then guards only the selected branch. +// Target function calls recurse at fuel-1; at fuel 0 the call returns \bot, so G_0 = false. +fn definedness_guard(expr: &Expr, fuel: usize, func_idents: &[Ident], tcx: &TyCtx) -> Expr { + let builder = ExprBuilder::new(expr.span); + + match &expr.kind { + // Target function call: inline (if body exists) or mark as \bot. + // Functions without a body (synthesis constants) are always defined. + ExprKind::Call(func, args) if func_idents.contains(func) => { + let body_params = get_func_body_params(func, tcx); + + match body_params { + Some((Some(body), params)) => { + if fuel == 0 { + builder.bool_lit(false) // \bot: fuel exhausted + } else { + let mut inst_body = body; + for (param, arg) in params.iter().zip(args.iter()) { + inst_body = subst_var(&inst_body, param, arg); + } + definedness_guard(&inst_body, fuel - 1, func_idents, tcx) + } + } + // No body (synthesis constant) or not found: always defined. + _ => builder.bool_lit(true), + } + } + + // Variables, non-target calls, and literals (including infinity) are always defined. + ExprKind::Var(_) | ExprKind::Call(_, _) | ExprKind::Lit(_) => builder.bool_lit(true), + + // ITE: condition must be defined (B_k), and the selected branch must be defined (G_k). + ExprKind::Ite(cond, then_, else_) => { + let cond_def = bool_definedness_guard(cond, fuel, func_idents, tcx); + let then_def = definedness_guard(then_, fuel, func_idents, tcx); + let else_def = definedness_guard(else_, fuel, func_idents, tcx); + let branch_def = builder.ite(Some(TyKind::Bool), cond.clone(), then_def, else_def); + builder.binary(BinOpKind::And, Some(TyKind::Bool), cond_def, branch_def) + } + + // Multiplication and infimum (\cap): absorber is 0. + // Defined if: (G_k(lhs) && lhs_approx=0) || (G_k(rhs) && rhs_approx=0) + // || (G_k(lhs) && G_k(rhs)) + ExprKind::Binary(bin_op, lhs, rhs) + if matches!(bin_op.node, BinOpKind::Mul | BinOpKind::Inf) => + { + let lhs_approx = approx_expr(lhs, fuel, func_idents, tcx); + let rhs_approx = approx_expr(rhs, fuel, func_idents, tcx); + let lhs_def = definedness_guard(lhs, fuel, func_idents, tcx); + let rhs_def = definedness_guard(rhs, fuel, func_idents, tcx); + let ty = lhs + .ty + .as_ref() + .or(rhs.ty.as_ref()) + .unwrap_or(&TyKind::EUReal); + let zero = builder.zero_lit(ty); + let lhs_is_zero = + builder.binary(BinOpKind::Eq, Some(TyKind::Bool), lhs_approx, zero.clone()); + let rhs_is_zero = builder.binary(BinOpKind::Eq, Some(TyKind::Bool), rhs_approx, zero); + let lhs_absorbed = builder.binary( + BinOpKind::And, + Some(TyKind::Bool), + lhs_def.clone(), + lhs_is_zero, + ); + let rhs_absorbed = builder.binary( + BinOpKind::And, + Some(TyKind::Bool), + rhs_def.clone(), + rhs_is_zero, + ); + let both_def = builder.binary(BinOpKind::And, Some(TyKind::Bool), lhs_def, rhs_def); + let one_absorbed = builder.binary( + BinOpKind::Or, + Some(TyKind::Bool), + lhs_absorbed, + rhs_absorbed, + ); + builder.binary(BinOpKind::Or, Some(TyKind::Bool), one_absorbed, both_def) + } + + // Supremum (\cup): absorber is infinity. + // Defined if: (G_k(lhs) && lhs_approx=infinity) || (G_k(rhs) && rhs_approx=infinity) + // || (G_k(lhs) && G_k(rhs)) + ExprKind::Binary(bin_op, lhs, rhs) if bin_op.node == BinOpKind::Sup => { + let lhs_approx = cast_to_eureal(approx_expr(lhs, fuel, func_idents, tcx)); + let rhs_approx = cast_to_eureal(approx_expr(rhs, fuel, func_idents, tcx)); + let lhs_def = definedness_guard(lhs, fuel, func_idents, tcx); + let rhs_def = definedness_guard(rhs, fuel, func_idents, tcx); + let inf = builder.infinity_lit(); + let lhs_is_inf = + builder.binary(BinOpKind::Eq, Some(TyKind::Bool), lhs_approx, inf.clone()); + let rhs_is_inf = builder.binary(BinOpKind::Eq, Some(TyKind::Bool), rhs_approx, inf); + let lhs_absorbed = builder.binary( + BinOpKind::And, + Some(TyKind::Bool), + lhs_def.clone(), + lhs_is_inf, + ); + let rhs_absorbed = builder.binary( + BinOpKind::And, + Some(TyKind::Bool), + rhs_def.clone(), + rhs_is_inf, + ); + let both_def = builder.binary(BinOpKind::And, Some(TyKind::Bool), lhs_def, rhs_def); + let one_absorbed = builder.binary( + BinOpKind::Or, + Some(TyKind::Bool), + lhs_absorbed, + rhs_absorbed, + ); + builder.binary(BinOpKind::Or, Some(TyKind::Bool), one_absorbed, both_def) + } + + // Implication (->): left absorber is 0, right absorber is infinity. + // Defined if: (G_k(lhs) && lhs_approx=0) || (G_k(rhs) && rhs_approx=infinity) + // || (G_k(lhs) && G_k(rhs)) + ExprKind::Binary(bin_op, lhs, rhs) if bin_op.node == BinOpKind::Impl => { + let lhs_approx = approx_expr(lhs, fuel, func_idents, tcx); + let rhs_approx = cast_to_eureal(approx_expr(rhs, fuel, func_idents, tcx)); + let lhs_def = definedness_guard(lhs, fuel, func_idents, tcx); + let rhs_def = definedness_guard(rhs, fuel, func_idents, tcx); + let ty = lhs + .ty + .as_ref() + .or(rhs.ty.as_ref()) + .unwrap_or(&TyKind::EUReal); + let zero = builder.zero_lit(ty); + let inf = builder.infinity_lit(); + let lhs_is_zero = builder.binary(BinOpKind::Eq, Some(TyKind::Bool), lhs_approx, zero); + let rhs_is_inf = builder.binary(BinOpKind::Eq, Some(TyKind::Bool), rhs_approx, inf); + let lhs_absorbed = builder.binary( + BinOpKind::And, + Some(TyKind::Bool), + lhs_def.clone(), + lhs_is_zero, + ); + let rhs_absorbed = builder.binary( + BinOpKind::And, + Some(TyKind::Bool), + rhs_def.clone(), + rhs_is_inf, + ); + let both_def = builder.binary(BinOpKind::And, Some(TyKind::Bool), lhs_def, rhs_def); + let one_absorbed = builder.binary( + BinOpKind::Or, + Some(TyKind::Bool), + lhs_absorbed, + rhs_absorbed, + ); + builder.binary(BinOpKind::Or, Some(TyKind::Bool), one_absorbed, both_def) + } + + // Co-implication (<-): left absorber is infinity, right absorber is 0. + // Defined if: (G_k(lhs) && lhs_approx=infinity) || (G_k(rhs) && rhs_approx=0) + // || (G_k(lhs) && G_k(rhs)) + ExprKind::Binary(bin_op, lhs, rhs) if bin_op.node == BinOpKind::CoImpl => { + let lhs_approx = cast_to_eureal(approx_expr(lhs, fuel, func_idents, tcx)); + let rhs_approx = approx_expr(rhs, fuel, func_idents, tcx); + let lhs_def = definedness_guard(lhs, fuel, func_idents, tcx); + let rhs_def = definedness_guard(rhs, fuel, func_idents, tcx); + let ty = lhs + .ty + .as_ref() + .or(rhs.ty.as_ref()) + .unwrap_or(&TyKind::EUReal); + let zero = builder.zero_lit(ty); + let inf = builder.infinity_lit(); + let lhs_is_inf = builder.binary(BinOpKind::Eq, Some(TyKind::Bool), lhs_approx, inf); + let rhs_is_zero = builder.binary(BinOpKind::Eq, Some(TyKind::Bool), rhs_approx, zero); + let lhs_absorbed = builder.binary( + BinOpKind::And, + Some(TyKind::Bool), + lhs_def.clone(), + lhs_is_inf, + ); + let rhs_absorbed = builder.binary( + BinOpKind::And, + Some(TyKind::Bool), + rhs_def.clone(), + rhs_is_zero, + ); + let both_def = builder.binary(BinOpKind::And, Some(TyKind::Bool), lhs_def, rhs_def); + let one_absorbed = builder.binary( + BinOpKind::Or, + Some(TyKind::Bool), + lhs_absorbed, + rhs_absorbed, + ); + builder.binary(BinOpKind::Or, Some(TyKind::Bool), one_absorbed, both_def) + } + + // All other binary operators: defined iff both operands are defined. + ExprKind::Binary(_, lhs, rhs) => { + let lhs_def = definedness_guard(lhs, fuel, func_idents, tcx); + let rhs_def = definedness_guard(rhs, fuel, func_idents, tcx); + builder.binary(BinOpKind::And, Some(TyKind::Bool), lhs_def, rhs_def) + } + + // Boolean embedding ?(b), Iverson [b], and negation !b: delegate to B_k. + ExprKind::Unary(un_op, inner) + if matches!( + un_op.node, + UnOpKind::Embed | UnOpKind::Iverson | UnOpKind::Not + ) => + { + bool_definedness_guard(inner, fuel, func_idents, tcx) + } + + // Other unary (Non, Parens, etc.): propagate through G_k. + ExprKind::Unary(_, inner) => definedness_guard(inner, fuel, func_idents, tcx), + + // Cast: propagate through. + ExprKind::Cast(inner) => definedness_guard(inner, fuel, func_idents, tcx), + + // Subst: substitute the value into the body, then check definedness. + ExprKind::Subst(bound, subst_val, body) => { + let subst_body = subst_var(body, bound, subst_val); + definedness_guard(&subst_body, fuel, func_idents, tcx) + } + + // Quant: propagate through the body. + ExprKind::Quant(_, _, _, body) => definedness_guard(body, fuel, func_idents, tcx), + } +} + +/// Visitor that inserts `assume(embed(is_defined(call)))` statements before each recursive call, +/// guarding the CEGIS verification condition against fuel exhaustion. +pub struct InsertAssumeBeforeCalls<'a> { + pub(crate) func_idents: &'a [Ident], + pub(crate) direction: Direction, + pub(crate) tcx: &'a TyCtx, + /// How many recursive unrolling steps to perform when building the + /// well-definedness guard. Matches `--max-fuel` from the CLI options. + pub(crate) max_fuel: usize, +} + +impl<'a> InsertAssumeBeforeCalls<'a> { + /// Collect every call to a target (recursive) function inside `e`. + fn guarded_calls(&self, e: &Expr) -> Vec { + let mut collector = CallCollector::new(self.func_idents, self.tcx); + let mut e_clone = e.clone(); + collector.visit_expr(&mut e_clone).unwrap(); + collector.calls + } + + /// Emit `assume(embed(def_guard))` for each call, prepended before `original`. + fn make_definedness_assumes( + &self, + span: Span, + calls: Vec, + original: StmtKind, + ) -> StmtKind { + let builder = ExprBuilder::new(Span::dummy_span()); + let mut stmts = Vec::new(); + + for call_expr in calls { + // def_guard: the call is defined (does not bottom out due to fuel exhaustion). + // definedness_guard returns false only when a recursive call exhausts + // fuel, never when the function legitimately returns infinity. + let mut def_guard = + definedness_guard(&call_expr, self.max_fuel, self.func_idents, self.tcx); + // In the coproc (Up) direction, assume uses dual semantics, so we negate. + if self.direction == Direction::Up { + def_guard = builder.unary(UnOpKind::Not, Some(TyKind::Bool), def_guard); + } + let assume_expr = builder.unary(UnOpKind::Embed, Some(TyKind::EUReal), def_guard); + stmts.push(Spanned { + span, + node: StmtKind::Assume(self.direction, assume_expr), + }); + } + + stmts.push(Spanned { + span, + node: original, + }); + + StmtKind::Seq(stmts) + } +} + +impl<'a> VisitorMut for InsertAssumeBeforeCalls<'a> { + type Err = (); + + fn visit_stmt(&mut self, s: &mut Stmt) -> Result<(), Self::Err> { + let span = s.span; + + // If/While: recurse into bodies first, then wrap calls from the condition. + // The early return below would skip the body walk, so we handle these separately. + if matches!(s.node, StmtKind::If(..) | StmtKind::While(..)) { + let calls = match &s.node { + StmtKind::If(cond, _, _) | StmtKind::While(cond, _) => self.guarded_calls(cond), + _ => unreachable!(), + }; + walk_stmt(self, s)?; + if !calls.is_empty() { + let original = std::mem::replace(&mut s.node, StmtKind::Seq(vec![])); + s.node = self.make_definedness_assumes(span, calls, original); + } + return Ok(()); + } + + let calls: Vec = match &s.node { + StmtKind::Var(decl) => decl + .borrow() + .init + .as_ref() + .map(|e| self.guarded_calls(e)) + .unwrap_or_default(), + + StmtKind::Assign(_, e) + | StmtKind::Assert(_, e) + | StmtKind::Assume(_, e) + | StmtKind::Compare(_, e) + | StmtKind::Tick(e) => self.guarded_calls(e), + + _ => Vec::new(), + }; + + if !calls.is_empty() { + let original = std::mem::replace(&mut s.node, StmtKind::Seq(vec![])); + s.node = self.make_definedness_assumes(span, calls, original); + return Ok(()); + } + + walk_stmt(self, s) + } +} diff --git a/src/synthesis/rec_functions/mod.rs b/src/synthesis/rec_functions/mod.rs new file mode 100644 index 00000000..1a186b80 --- /dev/null +++ b/src/synthesis/rec_functions/mod.rs @@ -0,0 +1,5 @@ +pub mod approx_encoding; +pub mod soundness; + +pub use approx_encoding::InsertAssumeBeforeCalls; +pub use soundness::{run_soundness_check, SoundnessCheckConfig, SoundnessOutcome}; diff --git a/src/synthesis/rec_functions/soundness.rs b/src/synthesis/rec_functions/soundness.rs new file mode 100644 index 00000000..d050017f --- /dev/null +++ b/src/synthesis/rec_functions/soundness.rs @@ -0,0 +1,173 @@ +use crate::{ + ast::{ + visit::{walk_expr, VisitorMut}, + DeclKind, Expr, ExprKind, Ident, + }, + depgraph::DepGraph, + driver::{ + commands::verify::VerifyCommand, + error::CaesarError, + item::SourceUnitName, + quant_proof::{lower_quant_prove_task, QuantVcProveTask}, + smt_proof::{check_valid, mk_function_encoder_override}, + }, + resource_limits::{LimitsRef, MemorySize}, + smt::{translate_exprs::TranslateExprs, DepConfig, SmtCtx}, + tyctx::TyCtx, +}; + +pub struct SoundnessCheckConfig<'a> { + pub options: &'a VerifyCommand, + pub limits_ref: &'a LimitsRef, + pub depgraph: &'a DepGraph, + pub name: &'a SourceUnitName, + pub current_fuel: usize, +} + +fn inline_nullary_call_in_domain_bodies( + func_name: Ident, + replacement: &Expr, + all_domain_funcs: &[Ident], + tcx: &TyCtx, +) { + struct Replacer { + func: Ident, + replacement: Expr, + } + impl VisitorMut for Replacer { + type Err = (); + fn visit_expr(&mut self, e: &mut Expr) -> Result<(), ()> { + if let ExprKind::Call(ref f, ref args) = e.kind { + if *f == self.func && args.is_empty() { + *e = self.replacement.clone(); + return Ok(()); + } + } + walk_expr(self, e) + } + } + + for &ident in all_domain_funcs { + if let Some(decl) = tcx.get(ident) { + if let DeclKind::FuncDecl(func_ref) = decl.as_ref() { + let body_opt: Option = func_ref.borrow().body.borrow().clone(); + if let Some(mut body) = body_opt { + let mut replacer = Replacer { + func: func_name, + replacement: replacement.clone(), + }; + replacer.visit_expr(&mut body).unwrap(); + *func_ref.borrow().body.borrow_mut() = Some(body); + } + } + } + } +} +use std::time::{Duration, Instant}; +use z3::Context; +use z3rro::prover::ProveResult; + +const MAX_FUEL_INCREASES: usize = 5; + +/// Result of the soundness check run after a successful CEGIS iteration. +pub enum SoundnessOutcome { + Proved, + RetryWithFuel, + NoConclusion, +} + +/// Re-verify the original VC (without assume guards) with the synthesized +/// function bodies plugged in, to check the candidate invariant is actually sound. +pub fn run_soundness_check( + instantiated_templates: Vec<(Ident, Expr)>, + range_constraints: &[Expr], + vc_expr_orig: QuantVcProveTask, + tcx: &mut TyCtx, + config: &SoundnessCheckConfig<'_>, + target_funcs: &[Ident], +) -> Result { + let depgraph = config.depgraph; + let options = config.options; + let limits_ref = config.limits_ref; + let name = config.name; + let current_fuel = config.current_fuel; + println!("Checking soundness: verifying invariant holds without assume statements..."); + + // Install each instantiated template as the function body so the encoder treats it as defined. + for (synth_name, concrete_template) in &instantiated_templates { + if let Some(decl) = tcx.get(*synth_name) { + if let DeclKind::FuncDecl(func_ref) = decl.as_ref() { + *func_ref.borrow().body.borrow_mut() = Some(concrete_template.clone()); + } + } + inline_nullary_call_in_domain_bodies(*synth_name, concrete_template, target_funcs, tcx); + } + + let ctx_sound = Context::new(&z3::Config::default()); + let function_encoder_sound = + mk_function_encoder_override(tcx, depgraph, options, false, Some(current_fuel))?; + + let vc_orig_valid = + lower_quant_prove_task(options, limits_ref, tcx, name, vc_expr_orig.clone())?; + + let dep_config_sound = DepConfig::Set(vc_orig_valid.get_dependencies()); + let smt_ctx_sound = SmtCtx::new(&ctx_sound, tcx, function_encoder_sound, dep_config_sound); + let mut translate_sound = TranslateExprs::new(&smt_ctx_sound); + + let soundness_cap = Duration::from_secs(options.synth_options.soundness_timeout); + let soundness_deadline = { + let now = Instant::now(); + let cap_deadline = now + soundness_cap; + match limits_ref.time_left() { + Some(remaining) => cap_deadline.min(now + remaining), + None => cap_deadline, + } + }; + let soundness_limits_ref = LimitsRef::new(Some(soundness_deadline), None::); + + let vc_z3 = translate_sound.t_bool(&vc_orig_valid.vc); + let (prove_result, _) = check_valid( + &vc_z3, + &soundness_limits_ref, + &mut translate_sound, + range_constraints, + ); + + match prove_result { + ProveResult::Proof => { + println!("Soundness check passed: invariant holds without assume statements."); + Ok(SoundnessOutcome::Proved) + } + ProveResult::Counterexample => { + if current_fuel.saturating_sub(options.opt_options.max_fuel) < MAX_FUEL_INCREASES { + println!( + "Soundness check failed at fuel {current_fuel}; \ + retrying with fuel {}.", + current_fuel + 1 + ); + Ok(SoundnessOutcome::RetryWithFuel) + } else { + println!( + "Soundness check FAILED after {MAX_FUEL_INCREASES} fuel increases; \ + invariant does NOT hold without assume statements.", + ); + Ok(SoundnessOutcome::NoConclusion) + } + } + ProveResult::Unknown(_) => { + if current_fuel.saturating_sub(options.opt_options.max_fuel) < MAX_FUEL_INCREASES { + println!( + "Soundness check inconclusive at fuel {current_fuel}; \ + retrying with fuel {}.", + current_fuel + 1 + ); + Ok(SoundnessOutcome::RetryWithFuel) + } else { + println!( + "Soundness check inconclusive after {MAX_FUEL_INCREASES} fuel increases; giving up.", + ); + Ok(SoundnessOutcome::NoConclusion) + } + } + } +} diff --git a/src/synthesis/report.rs b/src/synthesis/report.rs new file mode 100644 index 00000000..a53ae77b --- /dev/null +++ b/src/synthesis/report.rs @@ -0,0 +1,150 @@ +use crate::ast::{ + util::{remove_casts, strip_nonneg_cast_if_nonneg}, + visit::{walk_expr, VisitorMut}, + BinOpKind, Expr, ExprKind, Ident, Symbol, UnOpKind, +}; +use crate::driver::quant_proof::QuantVcProveTask; +use crate::smt::uninterpreted::FuncEntry; +use indexmap::IndexMap; +use std::time::{Duration, Instant}; + +/// Counts the number of piecewise linear terms (`[guard] * polynomial`) in an expression. +pub struct PiecewiseLinearCounter { + pub count: usize, +} + +impl PiecewiseLinearCounter { + pub fn new() -> Self { + Self { count: 0 } + } +} + +impl VisitorMut for PiecewiseLinearCounter { + type Err = (); + + fn visit_expr(&mut self, expr: &mut Expr) -> Result<(), Self::Err> { + if let ExprKind::Binary(bin_op, lhs, _) = &expr.kind { + if bin_op.node == BinOpKind::Mul { + if let ExprKind::Unary(un_op, _) = &lhs.kind { + if un_op.node == UnOpKind::Iverson { + self.count += 1; + } + } + } + } + + walk_expr(self, expr) + } +} + +/// Running counters and timings accumulated across the whole synthesis session. +/// Passed by mutable reference through template building and the CEGIS loop so +/// all stats stay together and can be printed in one place. +pub struct SynthStats { + /// Wall-clock start of the entire synthesis run. + pub start: Instant, + /// Total counterexamples produced by the verifier. + pub cex_count: usize, + /// SAT checks spent building template expressions. + pub template_sat_checks: usize, + /// Time spent in template building. + pub duration_template_build: Duration, + /// Outer refinement iterations triggered by the close-CEX heuristic. + pub close_cex_refinements: usize, +} + +impl SynthStats { + pub fn new() -> Self { + SynthStats { + start: Instant::now(), + cex_count: 0, + template_sat_checks: 0, + duration_template_build: Duration::ZERO, + close_cex_refinements: 0, + } + } +} + +pub fn print_benchmark_info( + stats: &SynthStats, + duration_check: Duration, + refinement_iter: usize, + instantiated_tasks: &[(Ident, QuantVcProveTask, usize, usize, bool)], +) { + println!("\n=== Benchmark info ==="); + println!( + "Total synthesis: {:.2}s", + stats.start.elapsed().as_secs_f64() + ); + println!( + "Template building: {:.2}s", + stats.duration_template_build.as_secs_f64() + ); + println!( + "Verification checks: {:.2}s", + duration_check.as_secs_f64() + ); + println!("Outer iterations: {refinement_iter}"); + println!("Close CEX refinements: {}", stats.close_cex_refinements); + println!("Counterexamples: {}", stats.cex_count); + println!("SAT checks (template): {}", stats.template_sat_checks); + for (inv_name, task, guards_before_pruning, guards_after_pruning, loop_mode) in + instantiated_tasks + { + let mut counter = PiecewiseLinearCounter::new(); + counter.visit_expr(&mut task.expr.clone()).unwrap(); + let loop_extra = usize::from(*loop_mode); + println!( + "guards_before ({inv_name}): {}", + guards_before_pruning + 1 + loop_extra + ); + println!( + "guards_after ({inv_name}): {}", + guards_after_pruning + 1 + loop_extra + ); + println!( + "invariant_size ({inv_name}): {}", + counter.count + 1 + loop_extra + ); + } + println!("======================\n"); +} + +pub fn print_synthesized_bodies<'ctx>( + instantiated_tasks: &[(Ident, QuantVcProveTask, usize, usize, bool)], + synth_funcs: &IndexMap>, + k_induction_calls: &IndexMap, + refinement_iter: usize, +) { + println!("Synthesized function bodies:"); + for (inv_name, task, _, _, _) in instantiated_tasks { + let params_str = synth_funcs + .get(inv_name) + .map(|entry| { + entry + .inputs + .node + .iter() + .map(|p| format!("{}: {}", p.name.name, p.ty)) + .collect::>() + .join(", ") + }) + .unwrap_or_default(); + let ret_ty = task + .expr + .ty + .as_ref() + .map(|t| t.to_string()) + .unwrap_or_default(); + if let Some(inv_call) = k_induction_calls.get(&inv_name.name) { + println!(" @k_induction({refinement_iter}, {inv_call})"); + } + println!( + " syn func {}({}) : {} =\n {}\n", + inv_name, + params_str, + ret_ty, + strip_nonneg_cast_if_nonneg(&remove_casts(&task.expr)) + ); + } +} diff --git a/src/synthesis/templates/conditions.rs b/src/synthesis/templates/conditions.rs new file mode 100644 index 00000000..4635dfe7 --- /dev/null +++ b/src/synthesis/templates/conditions.rs @@ -0,0 +1,435 @@ +use indexmap::{IndexMap, IndexSet}; +use num::BigUint; +use z3::{Config, Context, SatResult}; +use z3rro::prover::Prover; + +use crate::{ + ast::{ + util::FreeVariableCollector, BinOpKind, Expr, ExprBuilder, ExprData, ExprKind, Ident, + LitKind, Shared, Spanned, TyKind, UnOpKind, + }, + resource_limits::LimitsRef, + smt::{ + funcs::axiomatic::AxiomaticFunctionEncoder, translate_exprs::TranslateExprs, DepConfig, + SmtCtx, + }, + synthesis::cegis::subst_from_mapping, + tyctx::TyCtx, +}; + +use super::PVarToFVarMap; + +pub(super) fn collect_program_vars(expr: &Expr) -> IndexSet { + let mut collector = FreeVariableCollector::new(); + collector.collect_and_clear(&mut expr.clone()) +} + +/// Collects all ITE conditions and Iverson operands from `expr`, deduplicated by string representation. +pub fn collect_bool_conditions(expr: &Expr) -> Vec { + let mut out = Vec::new(); + let mut seen: IndexSet = IndexSet::new(); + collect_bool_conditions_rec(expr, &mut out, &mut seen); + out +} + +fn collect_bool_conditions_rec(expr: &Expr, out: &mut Vec, seen: &mut IndexSet) { + match &expr.kind { + ExprKind::Ite(cond, then_branch, else_branch) => { + record_if_new(cond, out, seen); + collect_bool_conditions_rec(cond, out, seen); + collect_bool_conditions_rec(then_branch, out, seen); + collect_bool_conditions_rec(else_branch, out, seen); + } + ExprKind::Unary(op, operand) if matches!(op.node, UnOpKind::Iverson) => { + record_if_new(operand, out, seen); + collect_bool_conditions_rec(operand, out, seen); + } + _ => { + for child in expr.children() { + collect_bool_conditions_rec(child, out, seen); + } + } + } +} + +fn record_if_new(expr: &Expr, out: &mut Vec, seen: &mut IndexSet) { + let key = expr.to_string(); + if seen.insert(key) { + out.push(expr.clone()); + } +} + +/// Collects Boolean conditions from `vc_expr` whose free variables all appear in some +/// call-site substitution map, then rewrites each surviving condition into the synthesis +/// target's formal parameters. +pub fn collect_relevant_bool_conditions( + vc_expr: &Expr, + mappings: Vec, + tcx: &TyCtx, + limits_ref: LimitsRef, +) -> (Vec, IndexMap) { + let ctx = Context::new(&Config::default()); + let smt_ctx = SmtCtx::new( + &ctx, + tcx, + Box::new(AxiomaticFunctionEncoder::default()), + DepConfig::SpecsOnly, + ); + + let mut pvar_to_fvar_map: IndexMap = IndexMap::new(); + let mut out: Vec = Vec::new(); + let mut seen_strs: IndexSet = IndexSet::new(); + + for b in collect_bool_conditions(vc_expr) { + let vars = collect_program_vars(&b); + + for mapping in &mappings { + if vars.iter().all(|v| mapping.contains_key(v)) { + let wrapped = subst_from_mapping(mapping, &b, &limits_ref, &smt_ctx).unwrap(); + + let key = wrapped.to_string(); + if seen_strs.insert(key) { + out.push(wrapped); + } + + for (pvar, fvar_expr) in mapping { + pvar_to_fvar_map.insert(*pvar, fvar_expr.clone()); + } + } + } + } + + // Always populate pvar_to_fvar_map from all call-site mappings, not just those that happened + // to match a boolean condition. This ensures the guard/post substitution in loop mode works + // even when no boolean condition references the call argument variables. + for mapping in &mappings { + for (pvar, fvar_expr) in mapping { + pvar_to_fvar_map + .entry(*pvar) + .or_insert_with(|| fvar_expr.clone()); + } + } + + (out, pvar_to_fvar_map) +} + +// Normalises `(a - c1) == c2` to `a == (c1 + c2)` for UInt literals, so that +// conditions of the form `(n - 1) == k` from inner-loop invariants are +// deduplicated against the equivalent outer-scope `n == (k+1)` conditions. +pub(super) fn normalize_condition(expr: &Expr) -> Expr { + let ExprKind::Binary(op, lhs, rhs) = &expr.kind else { + return expr.clone(); + }; + if !matches!(op.node, BinOpKind::Eq) { + return expr.clone(); + } + let ExprKind::Binary(sub_op, inner_lhs, inner_rhs) = &lhs.kind else { + return expr.clone(); + }; + if !matches!(sub_op.node, BinOpKind::Sub) { + return expr.clone(); + } + let ExprKind::Lit(offset_lit) = &inner_rhs.kind else { + return expr.clone(); + }; + let ExprKind::Lit(val_lit) = &rhs.kind else { + return expr.clone(); + }; + let LitKind::UInt(offset) = &offset_lit.node else { + return expr.clone(); + }; + let LitKind::UInt(val) = &val_lit.node else { + return expr.clone(); + }; + let sum: BigUint = offset + val; + let new_rhs = Shared::new(ExprData { + kind: ExprKind::Lit(Spanned::with_dummy_span(LitKind::UInt(sum))), + ty: rhs.ty.clone(), + span: rhs.span, + }); + Shared::new(ExprData { + kind: ExprKind::Binary(*op, inner_lhs.clone(), new_rhs), + ty: expr.ty.clone(), + span: expr.span, + }) +} + +// Flattens a (possibly nested) right- or left-associative conjunction into a +// flat list of its conjuncts. +fn flatten_and(expr: &Expr, out: &mut Vec) { + match &expr.kind { + ExprKind::Binary(op, lhs, rhs) if matches!(op.node, BinOpKind::And) => { + flatten_and(lhs, out); + flatten_and(rhs, out); + } + _ => out.push(expr.clone()), + } +} + +// Flattens, deduplicates, and drops tautological conjuncts; returns `true` when all are dropped. +pub(super) fn simplify_conjunction(expr: &Expr, builder: &ExprBuilder) -> Expr { + let mut conjuncts = Vec::new(); + flatten_and(expr, &mut conjuncts); + + let mut seen: IndexSet = IndexSet::new(); + let filtered: Vec = conjuncts + .into_iter() + .filter(|c| !is_syntactic_tautology(c) && seen.insert(c.to_string())) + .collect(); + + match filtered.len() { + 0 => builder.bool_lit(true), + _ => filtered + .into_iter() + .reduce(|acc, c| builder.binary(BinOpKind::And, Some(TyKind::Bool), acc, c)) + .unwrap(), + } +} + +// Returns `true` for expressions that are syntactically always true and can +// therefore be dropped from the Boolean splitting conditions. +pub(super) fn is_syntactic_tautology(expr: &Expr) -> bool { + match &expr.kind { + ExprKind::Lit(lit) => matches!(lit.node, LitKind::Bool(true)), + ExprKind::Binary(op, lhs, rhs) => { + // x == x, x <= x, x >= x are reflexively true. + if matches!(op.node, BinOpKind::Eq | BinOpKind::Le | BinOpKind::Ge) + && (Shared::as_ptr(lhs) == Shared::as_ptr(rhs) + || lhs.to_string() == rhs.to_string()) + { + return true; + } + // 0 <= x is always true when x has type UInt. + if matches!(op.node, BinOpKind::Le) + && lhs.to_string() == "0" + && rhs.ty.as_ref() == Some(&TyKind::UInt) + { + return true; + } + // A conjunction is a tautology only when both sides are. + matches!(op.node, BinOpKind::And) + && is_syntactic_tautology(lhs) + && is_syntactic_tautology(rhs) + } + _ => false, + } +} + +pub(super) fn is_true_lit(e: &Expr) -> bool { + matches!(&e.kind, ExprKind::Lit(s) if matches!(s.node, LitKind::Bool(true))) +} + +// A group of Boolean conditions to enumerate during template-region exploration. +pub(super) enum ConditionGroup { + /// A single condition: try both `true` and `false`. + Independent(Expr), + /// A set of mutually-exclusive `var == literal` conditions for the same + /// variable: try each member individually, then the "none of them" case. + Exclusive(Vec), +} + +// Extracts a stable string key for the LHS of an equality condition, +// looking through cast wrappers. +fn extract_var_key(expr: &Expr) -> Option { + match &expr.kind { + ExprKind::Var(id) => Some(id.name.to_string()), + ExprKind::Cast(inner) => extract_var_key(inner), + _ => None, + } +} + +// Groups `var == literal` conditions for the same variable as `Exclusive`; all others stay `Independent`. +pub(super) fn group_exclusive_conditions(exprs: Vec) -> Vec { + let mut eq_groups: IndexMap> = IndexMap::new(); + let mut independent: Vec = Vec::new(); + + for expr in exprs { + let mut grouped = false; + if let ExprKind::Binary(op, lhs, rhs) = &expr.kind { + if matches!(op.node, BinOpKind::Eq) { + if let Some(key) = extract_var_key(lhs) { + if matches!(rhs.kind, ExprKind::Lit(_)) { + eq_groups.entry(key).or_default().push(expr.clone()); + grouped = true; + } + } + } + } + if !grouped { + independent.push(expr); + } + } + + let mut groups: Vec = independent + .into_iter() + .map(ConditionGroup::Independent) + .collect(); + + for (_, members) in eq_groups { + if members.len() > 1 { + groups.push(ConditionGroup::Exclusive(members)); + } else { + // Single equality — keep as independent. + groups.push(ConditionGroup::Independent( + members.into_iter().next().unwrap(), + )); + } + } + + groups +} + +// `lhs && rhs` with identity simplification: drops a literal `true` on either +// side so that template guards don't accumulate leading `true && ...`. +pub(super) fn and_simplify(builder: &ExprBuilder, lhs: Expr, rhs: Expr) -> Expr { + if is_true_lit(&lhs) { + rhs + } else if is_true_lit(&rhs) { + lhs + } else { + builder.binary(BinOpKind::And, Some(TyKind::Bool), lhs, rhs) + } +} + +// Enumerates all satisfiable truth-assignments of `groups` with incremental push/pop SAT +// and collects the resulting case guards (Boolean conjunctions) into `valid_guards`. +pub(super) fn explore_condition_groups<'smt, 'ctx>( + idx: usize, + groups: &[ConditionGroup], + builder: &mut ExprBuilder, + translate: &mut TranslateExprs<'smt, 'ctx>, + prover: &mut Prover<'ctx>, + partial_guard: Expr, + valid_guards: &mut Vec, +) -> usize { + if idx == groups.len() { + valid_guards.push(partial_guard); + return 0; + } + + let mut num_sat_checks = 0; + + match &groups[idx] { + ConditionGroup::Independent(b) => { + let neg = builder.unary(UnOpKind::Not, Some(TyKind::Bool), b.clone()); + // Pairs: (condition to test, its opposite) — try !b first, then b. + let cases = [(neg.clone(), b.clone()), (b.clone(), neg)]; + for (cond, opposite) in cases { + let cond_z3 = translate.t_bool(&cond); + let opposite_z3 = translate.t_bool(&opposite); + + // Tautology check: if the opposite is UNSAT under current assumptions, + // `cond` is implied — it adds no information to the guard. + prover.push(); + prover.add_assumption(&opposite_z3); + num_sat_checks += 1; + let opposite_is_sat = prover.check_sat() == SatResult::Sat; + prover.pop(); + + // Reachability check: prune the branch if `cond` itself is UNSAT. + prover.push(); + prover.add_assumption(&cond_z3); + num_sat_checks += 1; + if prover.check_sat() == SatResult::Sat { + let new_guard = if opposite_is_sat { + and_simplify(builder, partial_guard.clone(), cond) + } else { + tracing::trace!("implied condition at depth {idx}, not added to guard"); + partial_guard.clone() + }; + num_sat_checks += explore_condition_groups( + idx + 1, + groups, + builder, + translate, + prover, + new_guard, + valid_guards, + ); + } else { + tracing::trace!("pruned UNSAT at depth {idx}"); + } + prover.pop(); + } + } + + ConditionGroup::Exclusive(members) => { + for member in members { + let cond_z3 = translate.t_bool(member); + let neg_member = builder.unary(UnOpKind::Not, Some(TyKind::Bool), member.clone()); + let neg_z3 = translate.t_bool(&neg_member); + + // Tautology check: if !member is UNSAT, member is always true — don't add to guard. + prover.push(); + prover.add_assumption(&neg_z3); + num_sat_checks += 1; + let neg_is_sat = prover.check_sat() == SatResult::Sat; + prover.pop(); + + prover.push(); + prover.add_assumption(&cond_z3); + num_sat_checks += 1; + if prover.check_sat() == SatResult::Sat { + let new_guard = if neg_is_sat { + and_simplify(builder, partial_guard.clone(), member.clone()) + } else { + tracing::trace!( + "implied exclusive member at depth {idx}, not added to guard" + ); + partial_guard.clone() + }; + num_sat_checks += explore_condition_groups( + idx + 1, + groups, + builder, + translate, + prover, + new_guard, + valid_guards, + ); + } else { + tracing::trace!("pruned UNSAT for exclusive member at depth {idx}"); + } + prover.pop(); + } + + // Try the "none of them" case (all members false). + prover.push(); + let mut none_guard = partial_guard.clone(); + for member in members { + let neg = builder.unary(UnOpKind::Not, Some(TyKind::Bool), member.clone()); + let member_z3 = translate.t_bool(member); + let neg_z3 = translate.t_bool(&neg); + + // Tautology check: if `member` is UNSAT, then `!member` is implied — don't add to guard. + prover.push(); + prover.add_assumption(&member_z3); + num_sat_checks += 1; + let member_is_sat = prover.check_sat() == SatResult::Sat; + prover.pop(); + + prover.add_assumption(&neg_z3); + if member_is_sat { + none_guard = and_simplify(builder, none_guard, neg); + } + } + num_sat_checks += 1; + if prover.check_sat() == SatResult::Sat { + num_sat_checks += explore_condition_groups( + idx + 1, + groups, + builder, + translate, + prover, + none_guard, + valid_guards, + ); + } else { + tracing::trace!("pruned UNSAT for 'none' case at depth {idx}"); + } + prover.pop(); + } + } + + num_sat_checks +} diff --git a/src/synthesis/templates/mod.rs b/src/synthesis/templates/mod.rs new file mode 100644 index 00000000..b58a423d --- /dev/null +++ b/src/synthesis/templates/mod.rs @@ -0,0 +1,800 @@ +mod conditions; +mod pipeline; +mod refinements; + +pub use pipeline::build_and_inline_templates; + +use conditions::{ + and_simplify, collect_program_vars, collect_relevant_bool_conditions, explore_condition_groups, + group_exclusive_conditions, is_syntactic_tautology, is_true_lit, normalize_condition, + simplify_conjunction, ConditionGroup, +}; +use refinements::{get_fix_region_splits, get_variable_region_splits}; + +use indexmap::{IndexMap, IndexSet}; +use num::{BigInt, BigRational, BigUint}; +use z3::SatResult; +use z3rro::prover::{IncrementalMode, Prover}; + +use crate::{ + ast::{ + decl, BinOpKind, DeclKind, DeclRef, Expr, ExprBuilder, ExprData, ExprKind, Ident, LitKind, + Range, Shared, Span, Spanned, Symbol, TyKind, UnOpKind, VarDecl, VarKind, + }, + driver::commands::{options::RefinementMode, verify::VerifyCommand}, + resource_limits::LimitsRef, + smt::{ + funcs::axiomatic::AxiomaticFunctionEncoder, translate_exprs::TranslateExprs, uninterpreted, + DepConfig, SmtCtx, + }, + synthesis::cegis::subst_from_mapping, + tyctx::TyCtx, +}; + +/// Refinement state for one outer CEGIS iteration. +pub struct RefinementState { + pub mode: RefinementMode, + pub iter: usize, + pub effective_split_count: usize, + pub effective_degree: usize, +} + +/// Common config for template-building calls. +pub struct TemplateConfig<'a> { + pub options: &'a VerifyCommand, + pub limits_ref: &'a LimitsRef, + pub refinement: &'a RefinementState, +} + +/// Polynomial shape shared between the piece builder and the piecewise assembler. +struct PolySpec<'a> { + synth_name: &'a Ident, + fvar_decls: &'a [VarDecl], + signed_output_type: TyKind, + max_degree: usize, +} + +// Maps program variables to the formal-variable expressions they were passed as at a call site. +pub type PVarToFVarMap = IndexMap; + +pub struct TemplateResult { + pub expr: Expr, + pub template_idents: Vec<(Ident, TyKind)>, + pub guards_before_pruning: usize, + pub guards_after_pruning: usize, + pub num_sat_checks: usize, + pub loop_mode: bool, +} + +pub struct TemplateEntry { + pub synth_name: Ident, + pub expr: Expr, + pub guards_before_pruning: usize, + pub guards_after_pruning: usize, + pub loop_mode: bool, +} + +/// For each call to `target_ident` in `expr`, returns a map from formal parameter to +/// the program variable passed at that call site (plain-variable arguments only). +pub fn collect_call_var_param_maps( + expr: &Expr, + target_ident: &Ident, + fvars: &[Expr], +) -> Vec { + let mut out = Vec::new(); + collect_call_var_param_maps_rec(expr, target_ident, fvars, &mut out); + out +} + +fn collect_call_var_param_maps_rec( + expr: &Expr, + target_ident: &Ident, + fvars: &[Expr], + out: &mut Vec, +) { + match &expr.kind { + ExprKind::Call(func_ident, args) if func_ident.name == target_ident.name => { + if args.len() == fvars.len() { + let map: PVarToFVarMap = args + .iter() + .zip(fvars.iter()) + .filter_map(|(arg, param)| { + if let ExprKind::Var(id) = &arg.kind { + Some((*id, param.clone())) + } else { + None + } + }) + .collect(); + + if !map.is_empty() { + out.push(map); + } + } + // Always recurse into call arguments. + for arg in args { + collect_call_var_param_maps_rec(arg, target_ident, fvars, out); + } + } + _ => { + for child in expr.children() { + collect_call_var_param_maps_rec(child, target_ident, fvars, out); + } + } + } +} + +// Generates all monomials of exactly `degree` from `vars` (combinations with repetition). +fn gen_monomials( + vars: &[Expr], + degree: usize, + start: usize, + current: &mut Vec, + out: &mut Vec>, +) { + if current.len() == degree { + out.push(current.clone()); + return; + } + for i in start..vars.len() { + current.push(vars[i].clone()); + gen_monomials(vars, degree, i, current, out); + current.pop(); + } +} + +// Left-folds a product over `factors`; panics if `factors` is empty. +fn multiply_all(builder: &ExprBuilder, ty: &TyKind, factors: &[Expr]) -> Expr { + factors[1..].iter().fold(factors[0].clone(), |acc, f| { + builder.binary(BinOpKind::Mul, Some(ty.clone()), acc, f.clone()) + }) +} + +// Builds a `c_0 + sum_i c_i * x^i` polynomial with fresh coefficient tvars. +// The result still needs to be wrapped in `nonneg_cast` by the caller. +fn build_polynomial_combination( + piece_id: String, + spec: &PolySpec<'_>, + builder: &ExprBuilder, + tcx: &TyCtx, + declare_tvar: &mut dyn FnMut(String) -> decl::VarDecl, +) -> Expr { + let synth_name = spec.synth_name; + let fvar_decls = spec.fvar_decls; + let signed_output_type = spec.signed_output_type.clone(); + let max_degree = spec.max_degree; + let fvar_exprs: Vec = fvar_decls + .iter() + .map(|v| { + let raw = builder.var(v.name, tcx); + if raw.ty.as_ref() == Some(&signed_output_type) { + raw + } else { + builder.cast(signed_output_type.clone(), raw) + } + }) + .collect(); + + let mut poly: Option = None; + for degree in 1..=max_degree { + let mut monomials = Vec::new(); + gen_monomials(&fvar_exprs, degree, 0, &mut Vec::new(), &mut monomials); + + for (idx, mono) in monomials.into_iter().enumerate() { + let prod = multiply_all(builder, &signed_output_type, &mono); + let coeff_name = format!("tvar_{synth_name}_{piece_id}_deg{degree}_m{idx}"); + let coeff = builder.var(declare_tvar(coeff_name).name, tcx); + let term = builder.binary( + BinOpKind::Mul, + Some(signed_output_type.clone()), + coeff, + prod, + ); + poly = Some(match poly { + None => term, + Some(acc) => { + builder.binary(BinOpKind::Add, Some(signed_output_type.clone()), acc, term) + } + }); + } + } + + let constant = builder.var( + declare_tvar(format!("tvar_{synth_name}_{piece_id}_const")).name, + tcx, + ); + match poly { + None => constant, + Some(acc) => builder.binary( + BinOpKind::Add, + Some(signed_output_type.clone()), + acc, + constant, + ), + } +} + +/// Sums one fresh polynomial per satisfiable (guard, split) pair into a piecewise expression. +/// The result is in `signed_output_type`; the caller wraps it in `nonneg_cast`. +fn assemble_piecewise_expression<'smt, 'ctx>( + spec: &PolySpec<'_>, + collected_guards: &[Expr], + split_conditions: &[Expr], + builder: &mut ExprBuilder, + translate: &mut TranslateExprs<'smt, 'ctx>, + declare_tvar: &mut dyn FnMut(String) -> decl::VarDecl, +) -> (Expr, usize) { + let ctx = translate.ctx.ctx(); + let tcx = translate.ctx.tcx(); + let signed_output_type = spec.signed_output_type.clone(); + let mut final_expr: Option = None; + let mut num_sat_checks = 0; + let mut prover = Prover::new(ctx, IncrementalMode::Native); + + for (i_idx, guard) in collected_guards.iter().enumerate() { + for (s_idx, split) in split_conditions.iter().enumerate() { + let region = and_simplify(builder, guard.clone(), split.clone()); + + let expr_z3 = translate.t_bool(®ion); + prover.push(); + prover.add_assumption(&expr_z3); + num_sat_checks += 1; + let sat = prover.check_sat() == SatResult::Sat; + prover.pop(); + + if !sat { + continue; + } + + let piece_poly = build_polynomial_combination( + format!("{}_{}", i_idx, s_idx), + spec, + builder, + tcx, + declare_tvar, + ); + + let term = if is_true_lit(guard) && is_true_lit(split) { + piece_poly + } else { + let iverson = + builder.unary(UnOpKind::Iverson, Some(signed_output_type.clone()), region); + builder.binary( + BinOpKind::Mul, + Some(signed_output_type.clone()), + iverson, + piece_poly, + ) + }; + + final_expr = Some(match final_expr { + None => term, + Some(acc) => { + builder.binary(BinOpKind::Add, Some(signed_output_type.clone()), acc, term) + } + }); + } + } + + // If every (guard, split) pair was UNSAT, fall back to a single unconstrained + // polynomial so the synthesis still has coefficients to work with. + let expr = final_expr.unwrap_or_else(|| { + build_polynomial_combination( + "unconstrained".to_string(), + spec, + builder, + tcx, + declare_tvar, + ) + }); + (expr, num_sat_checks) +} + +// Recursively removes any sub-expression whose top node is a `Quant`. +// Binary nodes with one quant side keep the other; nodes with both sides +// quantified become `false`; a top-level quant becomes `true`. +fn strip_quant_subexprs(expr: &Expr) -> Expr { + let builder = ExprBuilder::new(expr.span); + match &expr.kind { + ExprKind::Quant(..) => builder.bool_lit(true), + ExprKind::Binary(op, lhs, rhs) => { + let lhs_q = matches!(lhs.kind, ExprKind::Quant(..)); + let rhs_q = matches!(rhs.kind, ExprKind::Quant(..)); + match (lhs_q, rhs_q) { + (true, false) => strip_quant_subexprs(rhs), + (false, true) => strip_quant_subexprs(lhs), + (true, true) => match expr.ty.as_ref() { + Some(ty) if !matches!(ty, TyKind::Bool) => builder.zero_lit(ty), + _ => builder.bool_lit(false), + }, + (false, false) => Shared::new(ExprData { + kind: ExprKind::Binary( + *op, + strip_quant_subexprs(lhs), + strip_quant_subexprs(rhs), + ), + ty: expr.ty.clone(), + span: expr.span, + }), + } + } + ExprKind::Ite(cond, then_expr, else_expr) => Shared::new(ExprData { + kind: ExprKind::Ite( + strip_quant_subexprs(cond), + strip_quant_subexprs(then_expr), + strip_quant_subexprs(else_expr), + ), + ty: expr.ty.clone(), + span: expr.span, + }), + ExprKind::Unary(op, operand) => Shared::new(ExprData { + kind: ExprKind::Unary(*op, strip_quant_subexprs(operand)), + ty: expr.ty.clone(), + span: expr.span, + }), + _ => expr.clone(), + } +} + +// Looks for `synth_name(...) <=/= ite(guard, body, post)` in `expr` and extracts +// (guard, post) if found. +fn extract_loop_guard_and_post(expr: &Expr, synth_name: &Ident) -> Option<(Expr, Expr)> { + if let ExprKind::Binary(bin_op, lhs, rhs) = &expr.kind { + if matches!(bin_op.node, BinOpKind::CoCompare | BinOpKind::Compare) { + if matches!(&lhs.kind, ExprKind::Call(f, _) if f.name == synth_name.name) { + if let ExprKind::Ite(cond, _, else_branch) = &rhs.kind { + let post = unwrap_post_sup(&strip_quant_subexprs(else_branch)); + return Some((cond.clone(), post)); + } + } + return extract_loop_guard_and_post(lhs, synth_name) + .or_else(|| extract_loop_guard_and_post(rhs, synth_name)); + } + } + for child in expr.children() { + if let Some(res) = extract_loop_guard_and_post(child, synth_name) { + return Some(res); + } + } + None +} + +// Peels off leading `Sup` wrappers, keeping the left branch. +fn unwrap_post_sup(expr: &Expr) -> Expr { + match &expr.kind { + ExprKind::Binary(op, left, _) if matches!(op.node, BinOpKind::Sup) => unwrap_post_sup(left), + _ => expr.clone(), + } +} + +// Creates a literal of value `v` in `ty`; falls back to a `Real` fractional literal for non-integer types. +fn make_uint_lit(v: u64, ty: &TyKind, builder: &ExprBuilder) -> Expr { + match ty { + TyKind::UInt => Shared::new(ExprData { + kind: ExprKind::Lit(Spanned::with_dummy_span(LitKind::UInt(BigUint::from(v)))), + ty: Some(TyKind::UInt), + span: Span::dummy_span(), + }), + TyKind::Int => Shared::new(ExprData { + kind: ExprKind::Lit(Spanned::with_dummy_span(LitKind::Int(BigInt::from(v)))), + ty: Some(TyKind::Int), + span: Span::dummy_span(), + }), + _ => builder.signed_frac_lit(BigRational::from_integer(BigInt::from(v))), + } +} + +// Returns `true` if `expr` contains a call to `target`. +fn expr_contains_call(expr: &Expr, target: &Ident) -> bool { + match &expr.kind { + ExprKind::Call(f, args) => { + if f.name == target.name { + return true; + } + args.iter().any(|a| expr_contains_call(a, target)) + } + _ => expr + .children() + .into_iter() + .any(|c| expr_contains_call(c, target)), + } +} + +/// Builds the piecewise polynomial template for `synth_name` and returns a [`TemplateResult`]. +pub fn build_template_expression<'smt, 'ctx>( + config: &TemplateConfig<'_>, + synth_name: &Ident, + synth_val: &uninterpreted::FuncEntry, + vc_expr: &Expr, + builder: &mut ExprBuilder, + translate: &mut TranslateExprs<'smt, 'ctx>, + vc_expr_unfolded: &Expr, +) -> TemplateResult { + let options = config.options; + let limits_ref = config.limits_ref.clone(); + let split_count = config.refinement.effective_split_count; + let disable_loop_mode = config.options.synth_options.bare_template; + let max_degree = config.refinement.effective_degree; + let refinement_mode = config.refinement.mode; + let ctx = translate.ctx.ctx(); + let tcx = translate.ctx.tcx(); + let loop_parts = extract_loop_guard_and_post(vc_expr_unfolded, synth_name); + let loop_mode = loop_parts.is_some() && !disable_loop_mode; + + let output_type = if loop_mode { + TyKind::EUReal + } else { + let mut ty = TyKind::EUReal; + if let Some(DeclKind::FuncDecl(func_ref)) = tcx.get(*synth_name).as_deref() { + ty = func_ref.borrow().output.clone(); + } + ty + }; + + let signed_output_type = if options.synth_options.unsigned_coefficients { + match output_type { + TyKind::UInt => TyKind::UInt, + TyKind::EUReal => TyKind::UReal, + ref t => t.clone(), + } + } else { + match output_type { + TyKind::UInt => TyKind::Int, + _ => TyKind::Real, + } + }; + + let mut template_idents: Vec<(Ident, TyKind)> = Vec::new(); + let mut num_sat_checks = 0; + + let mut fvar_decls = Vec::new(); + let mut fvar_exprs = Vec::new(); + let mut fvar_exprs_for_conds = Vec::new(); + let mut bool_fvar_exprs = Vec::new(); + + for param in &synth_val.inputs.node { + let vardecl = VarDecl::from_param(param, VarKind::Input) + .try_unwrap() + .unwrap(); + let raw = builder.var(vardecl.name, tcx); + fvar_exprs_for_conds.push(raw.clone()); + if vardecl.ty == TyKind::Bool { + bool_fvar_exprs.push(raw); + } else { + fvar_decls.push(vardecl); + fvar_exprs.push(raw); + } + } + + let mappings = collect_call_var_param_maps(vc_expr, synth_name, &fvar_exprs_for_conds); + + let mut declare_tvar = |name: String| -> decl::VarDecl { + let full_name = format!("{}_sc{}_fn{}", name, split_count + 1, synth_name); + let ident = Ident::with_dummy_span(Symbol::intern(&full_name)); + let decl = VarDecl { + name: ident, + ty: signed_output_type.clone(), + kind: VarKind::Input, + init: None, + span: Span::dummy_span(), + created_from: None, + range: None, + }; + tcx.declare(crate::ast::DeclKind::VarDecl(DeclRef::new(decl.clone()))); + template_idents.push((decl.name, signed_output_type.clone())); + decl + }; + + let cond_smt_ctx = SmtCtx::new( + ctx, + tcx, + Box::new(AxiomaticFunctionEncoder::default()), + DepConfig::SpecsOnly, + ); + + let (mut bool_exprs, pvar_to_fvar_map) = if split_count >= 1 { + collect_relevant_bool_conditions(vc_expr, mappings, tcx, limits_ref.clone()) + } else { + (Vec::new(), IndexMap::new()) + }; + + let subst = + |e: &Expr| subst_from_mapping(&pvar_to_fvar_map, e, &limits_ref, &cond_smt_ctx).unwrap(); + + let loop_info: Option<(Expr, Expr)> = if let Some((guard, post)) = loop_parts { + if disable_loop_mode { + let unfolded_mappings = + collect_call_var_param_maps(vc_expr_unfolded, synth_name, &fvar_exprs_for_conds); + let ert_guard_map: IndexMap = { + let mut map = pvar_to_fvar_map.clone(); + for mapping in &unfolded_mappings { + for (pvar, fvar_expr) in mapping { + map.entry(*pvar).or_insert_with(|| fvar_expr.clone()); + } + } + map + }; + let guard_subst = + subst_from_mapping(&ert_guard_map, &guard, &limits_ref, &cond_smt_ctx).unwrap(); + tracing::debug!("loop guard (@ert, adding as bool condition): {guard_subst}"); + let guard_key = guard_subst.to_string(); + if !bool_exprs.iter().any(|e| e.to_string() == guard_key) { + bool_exprs.push(guard_subst); + } + None + } else { + let guard_subst = subst(&guard); + tracing::debug!("loop guard: {guard_subst}"); + + // If the guard uses variables that aren't formal parameters of the synth function + // (e.g. a loop guard on `f` when inv only takes `tc`), the ITE template would + // leak program-scope variables. Fall back to a plain polynomial. + let fvar_names: IndexSet<_> = fvar_exprs_for_conds + .iter() + .filter_map(|e| { + if let ExprKind::Var(id) = &e.kind { + Some(id.name) + } else { + None + } + }) + .collect(); + let guard_fvars = collect_program_vars(&guard_subst); + if guard_fvars.iter().any(|v| !fvar_names.contains(&v.name)) { + tracing::debug!( + "loop guard uses non-parameter variables ({:?}); disabling loop mode", + guard_fvars + .iter() + .filter(|v| !fvar_names.contains(&v.name)) + .map(|v| v.name.to_string()) + .collect::>() + ); + None + } else { + let guard_str = guard_subst.to_string(); + bool_exprs.retain(|e| e.to_string() != guard_str); + + let post_full = subst(&post); + Some((guard_subst, post_full)) + } + } + } else { + None + }; + + tracing::debug!("bool conditions (raw, {} total):", bool_exprs.len()); + for b in &bool_exprs { + tracing::debug!(" {b}"); + } + + // Simplify, normalise, deduplicate, and drop self-referential conditions. + let mut seen_norm: IndexSet = IndexSet::new(); + let bool_exprs: Vec = bool_exprs + .into_iter() + .map(|e| simplify_conjunction(&e, builder)) + .map(|e| normalize_condition(&e)) + .filter(|e| !is_syntactic_tautology(e) && seen_norm.insert(e.to_string())) + .filter(|e| !expr_contains_call(e, synth_name)) + .collect(); + + tracing::debug!( + "bool conditions after simplification ({} total):", + bool_exprs.len() + ); + for b in &bool_exprs { + tracing::debug!(" {b}"); + } + + let ranged_fvars: Vec<(Expr, Range)> = fvar_decls + .iter() + .filter_map(|v| Some((builder.var(v.name, tcx), v.range?))) + .collect(); + + let mut prover = Prover::new(ctx, IncrementalMode::Native); + for (var, range) in &ranged_fvars { + let var_ty = var.ty.clone().unwrap_or(TyKind::UInt); + for (typed_var, lo_lit, hi_lit) in [ + ( + var.clone(), + make_uint_lit(range.lower, &var_ty, builder), + make_uint_lit(range.upper, &var_ty, builder), + ), + ( + { + if var_ty == TyKind::Real { + var.clone() + } else { + builder.cast(TyKind::Real, var.clone()) + } + }, + builder.signed_frac_lit(BigRational::from_integer(BigInt::from(range.lower))), + builder.signed_frac_lit(BigRational::from_integer(BigInt::from(range.upper))), + ), + ] { + let ge = builder.binary(BinOpKind::Ge, Some(TyKind::Bool), typed_var.clone(), lo_lit); + let le = builder.binary(BinOpKind::Le, Some(TyKind::Bool), typed_var, hi_lit); + let range_constraint = builder.binary(BinOpKind::And, Some(TyKind::Bool), ge, le); + let range_z3 = translate.t_bool(&range_constraint); + prover.add_assumption(&range_z3); + } + } + + // In loop mode the template lives inside ite(guard, ..., post), so guard is always true + // there. Add it as an assumption so tautological conditions get pruned correctly. + if let Some((ref guard, _)) = loop_info { + let guard_z3 = translate.t_bool(guard); + prover.add_assumption(&guard_z3); + tracing::debug!("loop mode: added guard as prover assumption: {guard}"); + } + + // Drop conditions whose negation is UNSAT under the declared ranges (always true). + let mut filtered_bool_exprs: Vec = Vec::new(); + for e in bool_exprs { + let neg = builder.unary(UnOpKind::Not, Some(TyKind::Bool), e.clone()); + let neg_z3 = translate.t_bool(&neg); + prover.push(); + prover.add_assumption(&neg_z3); + num_sat_checks += 1; + let negation_sat = prover.check_sat() == SatResult::Sat; + prover.pop(); + if negation_sat { + filtered_bool_exprs.push(e); + } + } + let bool_exprs = filtered_bool_exprs; + + tracing::debug!( + "bool conditions after range filtering ({} total):", + bool_exprs.len() + ); + for b in &bool_exprs { + tracing::debug!(" {b}"); + } + + // In variable mode, skip bool params already covered by a VC-derived condition group + // to avoid redundant cross-products like `(!res1 && !res2) && (!res1 && has_disease)`. + let bool_exprs_strs: IndexSet = bool_exprs.iter().map(|e| e.to_string()).collect(); + let effective_bool_fvar_exprs: Vec = if matches!( + refinement_mode, + RefinementMode::Variable | RefinementMode::Degree + ) { + bool_fvar_exprs + .iter() + .filter(|fvar| !bool_exprs_strs.contains(&fvar.to_string())) + .cloned() + .collect() + } else { + bool_fvar_exprs.clone() + }; + + // In loop mode the guard is always true in the then-branch, so don't split on it — + // that would generate redundant [guard] / [!guard] Iverson brackets. + let effective_bool_fvar_exprs: Vec = if let Some((ref guard, _)) = loop_info { + let guard_str = guard.to_string(); + effective_bool_fvar_exprs + .into_iter() + .filter(|fvar| fvar.to_string() != guard_str) + .collect() + } else { + effective_bool_fvar_exprs + }; + + let split_conditions = if matches!( + refinement_mode, + RefinementMode::Variable | RefinementMode::Degree + ) { + get_variable_region_splits( + &fvar_exprs, + &effective_bool_fvar_exprs, + split_count, + builder, + tcx, + &mut declare_tvar, + ) + } else { + get_fix_region_splits( + &ranged_fvars, + &effective_bool_fvar_exprs, + split_count, + builder, + ) + }; + + let condition_groups = group_exclusive_conditions(bool_exprs); + tracing::debug!( + "{} condition groups ({} exclusive, {} independent) × {} split conditions", + condition_groups.len(), + condition_groups + .iter() + .filter(|g| matches!(g, ConditionGroup::Exclusive(_))) + .count(), + condition_groups + .iter() + .filter(|g| matches!(g, ConditionGroup::Independent(_))) + .count(), + split_conditions.len(), + ); + + let guards_before_pruning: usize = condition_groups.iter().fold(1, |acc, g| match g { + ConditionGroup::Independent(_) => acc * 2, + ConditionGroup::Exclusive(members) => acc * (members.len() + 1), + }) * split_conditions.len(); + + // `valid_guards` collects the satisfiable case guards (one Boolean conjunction per region). + let mut valid_guards: Vec = Vec::new(); + num_sat_checks += explore_condition_groups( + 0, + &condition_groups, + builder, + translate, + &mut prover, + builder.bool_lit(true), + &mut valid_guards, + ); + tracing::debug!("{} satisfiable guard assignments", valid_guards.len()); + + let poly_spec = PolySpec { + synth_name, + fvar_decls: &fvar_decls, + signed_output_type: signed_output_type.clone(), + max_degree, + }; + let (piecewise, sat_count) = assemble_piecewise_expression( + &poly_spec, + &valid_guards, + &split_conditions, + builder, + translate, + &mut declare_tvar, + ); + num_sat_checks += sat_count; + + // Apply nonneg_cast to the polynomial piecewise expression. + let nonneg_cast_name = Ident::with_dummy_span(Symbol::intern("nonneg_cast")); + let clamped_ty = if matches!(signed_output_type, TyKind::Int | TyKind::UInt) { + TyKind::UInt + } else { + TyKind::UReal + }; + let clamped = Shared::new(ExprData { + kind: ExprKind::Call(nonneg_cast_name, vec![piecewise]), + ty: Some(clamped_ty), + span: Span::dummy_span(), + }); + // Cast clamped result up to output_type (e.g. UReal -> EUReal in loop mode). + let clamped_in_output = if clamped.ty.as_ref() != Some(&output_type) { + builder.cast(output_type.clone(), clamped) + } else { + clamped + }; + // In loop mode: ITE(guard, clamped_eureal, post_full). post_full stays EUReal — + // no downcast needed, so infinity is preserved correctly in the else branch. + let mut final_expr = if let Some((guard, post_full)) = loop_info { + builder.ite( + Some(output_type.clone()), + guard, + clamped_in_output, + post_full, + ) + } else { + clamped_in_output + }; + + let free_vars = collect_program_vars(&final_expr); + let subst_iter = free_vars.into_iter().filter_map(|id| { + fvar_decls + .iter() + .position(|d| d.name.name == id.name) + .map(|idx| (id, fvar_exprs[idx].clone())) + }); + final_expr = builder.subst(final_expr, subst_iter); + + TemplateResult { + expr: final_expr, + template_idents, + guards_before_pruning, + guards_after_pruning: valid_guards.len() * split_conditions.len(), + num_sat_checks, + loop_mode, + } +} diff --git a/src/synthesis/templates/pipeline.rs b/src/synthesis/templates/pipeline.rs new file mode 100644 index 00000000..c299ef99 --- /dev/null +++ b/src/synthesis/templates/pipeline.rs @@ -0,0 +1,257 @@ +use crate::{ + ast::{ + util::remove_casts, + visit::{walk_expr, VisitorMut}, + BinOpKind, DeclKind, Expr, ExprBuilder, ExprData, ExprKind, Ident, Shared, Span, TyKind, + }, + driver::{ + error::CaesarError, + item::SourceUnitName, + quant_proof::{lower_quant_prove_task, BoolVcProveTask, QuantVcProveTask}, + }, + opt::unfolder::Unfolder, + smt::{ + funcs::axiomatic::AxiomaticFunctionEncoder, translate_exprs::TranslateExprs, + uninterpreted::FuncEntry, DepConfig, SmtCtx, + }, + synthesis::{cegis::get_synth_functions, report::SynthStats}, + tyctx::TyCtx, +}; + +fn wrap_with_subst(body: Expr, parameters: &[Ident], args: &[Expr], span: Span) -> Expr { + let mut wrapped = body; + for (parameter, actual_expr) in parameters.iter().zip(args.iter()) { + let ty = wrapped.ty.clone(); + let inner = wrapped; + wrapped = Shared::new(ExprData { + kind: ExprKind::Subst(*parameter, actual_expr.clone(), inner), + ty, + span, + }); + } + wrapped +} + +pub struct FunctionInliner<'smt, 'ctx> { + pub target: Ident, + pub entry: &'ctx FuncEntry<'ctx>, + pub body: &'ctx Expr, + pub tcx: &'smt TyCtx, + inlining_stack: Vec, +} + +impl<'smt, 'ctx> FunctionInliner<'smt, 'ctx> { + pub fn new( + target: Ident, + entry: &'ctx FuncEntry<'ctx>, + body: &'ctx Expr, + tcx: &'smt TyCtx, + ) -> Self { + Self { + target, + entry, + body, + tcx, + inlining_stack: Vec::new(), + } + } +} + +impl<'smt, 'ctx> VisitorMut for FunctionInliner<'smt, 'ctx> { + type Err = (); + + fn visit_expr(&mut self, expr: &mut Expr) -> Result<(), Self::Err> { + let span = expr.span; + match &mut expr.kind { + ExprKind::Call(func_ident, args) if *func_ident == self.target => { + let param_idents: Vec = + self.entry.inputs.node.iter().map(|p| p.name).collect(); + *expr = wrap_with_subst(self.body.clone(), ¶m_idents, args, span); + Ok(()) + } + ExprKind::Call(func_ident, args) => { + if self.inlining_stack.contains(func_ident) { + return walk_expr(self, expr); + } + if let Some(DeclKind::FuncDecl(func_ref)) = self.tcx.get(*func_ident).as_deref() { + let func = func_ref.borrow(); + let body_opt = func.body.borrow(); + let param_idents: Vec = + func.inputs.node.iter().map(|p| p.name).collect(); + if let Some(body_expr) = body_opt.clone() { + self.inlining_stack.push(*func_ident); + let mut wrapped = wrap_with_subst(body_expr, ¶m_idents, args, span); + let result = self.visit_expr(&mut wrapped); + self.inlining_stack.pop(); + result?; + *expr = wrapped; + return Ok(()); + } + return walk_expr(self, expr); + } + walk_expr(self, expr) + } + _ => walk_expr(self, expr), + } + } +} +use super::{build_template_expression, TemplateConfig, TemplateEntry, TemplateResult}; +use std::time::Instant; + +type TemplatesResult = Result<(Vec, Vec<(Ident, TyKind)>), CaesarError>; + +/// Build a template for every synth function, cross-inline them into each other, +/// inline the results into the VC, and conjoin nonnegativity constraints. +/// Modifies `vc_expr` and `vc_is_valid` in place; returns the template list and +/// collected template variable bindings. +pub fn build_and_inline_templates<'smt, 'ctx>( + translate: &mut TranslateExprs<'smt, 'ctx>, + vc_expr: &mut QuantVcProveTask, + vc_is_valid: &mut BoolVcProveTask, + config: &TemplateConfig<'_>, + name: &SourceUnitName, + stats: &mut SynthStats, +) -> TemplatesResult { + let smt_ctx = translate.ctx; + let synth_funcs = get_synth_functions(smt_ctx.uninterpreteds()); + if synth_funcs.is_empty() { + return Ok((Vec::new(), Vec::new())); + } + + let mut builder = ExprBuilder::new(Span::dummy_span()); + let mut templates: Vec = Vec::new(); + let mut tvars: Vec<(Ident, TyKind)> = Vec::new(); + + let tcx = translate.ctx.tcx(); + + // Build a template for each synthesised function. + for (synth_name, synth_val) in synth_funcs.iter() { + let start_template = Instant::now(); + + let mut vc_unfolded = vc_expr.expr.clone(); + Unfolder::new(config.limits_ref.clone(), smt_ctx).visit_expr(&mut vc_unfolded)?; + + let TemplateResult { + expr: template, + template_idents: tvar_idents, + guards_before_pruning, + guards_after_pruning, + num_sat_checks, + loop_mode, + } = build_template_expression( + config, + synth_name, + synth_val, + &vc_expr.expr, + &mut builder, + translate, + &vc_unfolded, + ); + + stats.template_sat_checks += num_sat_checks; + let elapsed_template = start_template.elapsed(); + stats.duration_template_build += elapsed_template; + tvars.extend(tvar_idents); + + // Unfold the template before storing it. + let ctx_local = z3::Context::new(&z3::Config::default()); + let smt_ctx_local = SmtCtx::new( + &ctx_local, + tcx, + Box::new(AxiomaticFunctionEncoder::default()), + DepConfig::SpecsOnly, + ); + let mut template_expr = template; + Unfolder::new(config.limits_ref.clone(), &smt_ctx_local).visit_expr(&mut template_expr)?; + + if config.options.synth_options.syn_benchmarks { + println!( + "Template building for `{}` took: {:.2}s", + synth_name, + elapsed_template.as_secs_f64() + ); + } + if config.options.synth_options.print_template { + println!( + "template for `{}`: {}", + synth_name, + remove_casts(&template_expr) + ); + } + templates.push(TemplateEntry { + synth_name: *synth_name, + expr: template_expr, + guards_before_pruning, + guards_after_pruning, + loop_mode, + }); + } + + // Cross-inline templates into one another (single pass; synth functions are non-recursive). + let ctx_local = z3::Context::new(&z3::Config::default()); + let smt_ctx_local = SmtCtx::new( + &ctx_local, + tcx, + Box::new(AxiomaticFunctionEncoder::default()), + DepConfig::SpecsOnly, + ); + for i in 0..templates.len() { + let other_templates: Vec<(Ident, Expr)> = templates + .iter() + .enumerate() + .filter(|(j, _)| *j != i) + .map(|(_, t)| (t.synth_name, t.expr.clone())) + .collect(); + for (func_ident, other_template) in &other_templates { + let func_entry = synth_funcs + .get(func_ident) + .expect("synth function disappeared during cross-inlining"); + FunctionInliner::new(*func_ident, func_entry, other_template, tcx) + .visit_expr(&mut templates[i].expr) + .unwrap(); + } + Unfolder::new(config.limits_ref.clone(), &smt_ctx_local) + .visit_expr(&mut templates[i].expr)?; + } + + // Inline all templates into the main VC. + for t in templates.iter() { + let func_entry = synth_funcs + .get(&t.synth_name) + .expect("synth function disappeared before VC inlining"); + FunctionInliner::new(t.synth_name, func_entry, &t.expr, tcx) + .visit_expr(&mut vc_expr.expr) + .unwrap(); + } + + *vc_is_valid = lower_quant_prove_task( + config.options, + config.limits_ref, + tcx, + name, + vc_expr.clone(), + )?; + + // Conjoin template >= 0 for each synthesised function. + for t in &templates { + let template_expr = &t.expr; + let Some(ty) = template_expr.ty.clone() else { + continue; + }; + let zero = builder.zero_lit(&ty); + let constraint = builder.binary( + BinOpKind::Ge, + Some(TyKind::Bool), + template_expr.clone(), + zero, + ); + vc_is_valid.vc = builder.binary( + BinOpKind::And, + Some(TyKind::Bool), + vc_is_valid.vc.clone(), + constraint, + ); + } + + Ok((templates, tvars)) +} diff --git a/src/synthesis/templates/refinements.rs b/src/synthesis/templates/refinements.rs new file mode 100644 index 00000000..1260caa8 --- /dev/null +++ b/src/synthesis/templates/refinements.rs @@ -0,0 +1,196 @@ +use std::cmp::min; + +use num::{BigInt, BigRational}; + +use crate::ast::{decl, BinOpKind, Expr, ExprBuilder, ExprKind, LitKind, Range, TyKind, UnOpKind}; +use crate::tyctx::TyCtx; + +/// Splits each range-annotated variable into `split_count` equal-width intervals and returns +/// one Boolean predicate per Cartesian-product cell. Bool vars get two regions: `var` / `!var`. +pub fn get_fix_region_splits( + ranged_vars: &[(Expr, Range)], + bool_vars: &[Expr], + split_count: usize, + builder: &mut ExprBuilder, +) -> Vec { + if ranged_vars.is_empty() && bool_vars.is_empty() || split_count == 0 { + return vec![builder.bool_lit(true)]; + } + + let mut all_intervals: Vec> = Vec::new(); + + for (var, range) in ranged_vars { + let (lo, hi) = (range.lower, range.upper); + + // A range of size 0 or 1 cannot be split; emit a single interval [lo, hi]. + if hi <= lo { + let lo_expr = builder.signed_frac_lit(BigRational::from_integer(BigInt::from(lo))); + let hi_expr = builder.signed_frac_lit(BigRational::from_integer(BigInt::from(hi))); + let real_var = builder.cast(TyKind::Real, var.clone()); + let ge = builder.binary(BinOpKind::Ge, Some(TyKind::Bool), real_var.clone(), lo_expr); + let le = builder.binary(BinOpKind::Le, Some(TyKind::Bool), real_var, hi_expr); + all_intervals.push(vec![builder.binary( + BinOpKind::And, + Some(TyKind::Bool), + ge, + le, + )]); + continue; + } + + let num_parts = min(hi - lo, split_count as u64); + + // Ensure the variable is in the Real domain for comparison. + let real_var = if matches!(var.ty, Some(TyKind::Real)) { + var.clone() + } else { + builder.cast(TyKind::Real, var.clone()) + }; + + let mut var_intervals = Vec::new(); + for i in 1..=(num_parts) { + let (part_lo, part_hi) = if i == 1 { + (lo, lo + (hi - lo) / num_parts) + } else if i < num_parts { + ( + 1 + lo + ((i - 1) * (hi - lo) / num_parts), + lo + (i * (hi - lo) / num_parts), + ) + } else { + (1 + lo + ((i - 1) * (hi - lo) / num_parts), hi) + }; + + let lo_expr = builder.signed_frac_lit(BigRational::from_integer(BigInt::from(part_lo))); + let hi_expr = builder.signed_frac_lit(BigRational::from_integer(BigInt::from(part_hi))); + + let ge = builder.binary(BinOpKind::Ge, Some(TyKind::Bool), real_var.clone(), lo_expr); + let le = builder.binary(BinOpKind::Le, Some(TyKind::Bool), real_var.clone(), hi_expr); + var_intervals.push(builder.binary(BinOpKind::And, Some(TyKind::Bool), ge, le)); + } + + all_intervals.push(var_intervals); + } + + for var in bool_vars { + let neg = builder.unary(UnOpKind::Not, Some(TyKind::Bool), var.clone()); + all_intervals.push(vec![var.clone(), neg]); + } + + cartesian_and(&all_intervals, builder) +} + +/// Like `get_fix_region_splits` but uses fresh synthesized boundary template variables instead of +/// equal-width arithmetic intervals. No range annotations needed. Returns `[true]` if no vars. +pub fn get_variable_region_splits( + fvars: &[Expr], + bool_vars: &[Expr], + split_count: usize, + builder: &mut ExprBuilder, + tcx: &TyCtx, + declare_tvar: &mut dyn FnMut(String) -> decl::VarDecl, +) -> Vec { + if (fvars.is_empty() || split_count <= 1) && bool_vars.is_empty() { + return vec![builder.bool_lit(true)]; + } + + let mut all_intervals: Vec> = Vec::new(); + + for (var_idx, var) in + fvars + .iter() + .enumerate() + .take(if split_count <= 1 { 0 } else { fvars.len() }) + { + let real_var = if matches!(var.ty, Some(TyKind::Real)) { + var.clone() + } else { + builder.cast(TyKind::Real, var.clone()) + }; + + // Declare split_count - 1 boundary template variables. + let mut boundaries: Vec = Vec::new(); + for bnd_idx in 0..(split_count - 1) { + let name = format!("tvar_bnd_v{var_idx}_b{bnd_idx}"); + let boundary_decl = declare_tvar(name); + let boundary = builder.var(boundary_decl.name, tcx); + let boundary_real = if boundary_decl.ty == TyKind::Real { + boundary + } else { + builder.cast(TyKind::Real, boundary) + }; + boundaries.push(boundary_real); + } + + let mut var_intervals = Vec::new(); + + // First interval: var < b_0 + var_intervals.push(builder.binary( + BinOpKind::Lt, + Some(TyKind::Bool), + real_var.clone(), + boundaries[0].clone(), + )); + + // Middle intervals: b_{i-1} <= var < b_i + for i in 1..split_count - 1 { + let ge = builder.binary( + BinOpKind::Ge, + Some(TyKind::Bool), + real_var.clone(), + boundaries[i - 1].clone(), + ); + let lt = builder.binary( + BinOpKind::Lt, + Some(TyKind::Bool), + real_var.clone(), + boundaries[i].clone(), + ); + var_intervals.push(builder.binary(BinOpKind::And, Some(TyKind::Bool), ge, lt)); + } + + // Last interval: var >= b_{k-2} + var_intervals.push(builder.binary( + BinOpKind::Ge, + Some(TyKind::Bool), + real_var, + boundaries[split_count - 2].clone(), + )); + + all_intervals.push(var_intervals); + } + + for var in bool_vars { + let neg = builder.unary(UnOpKind::Not, Some(TyKind::Bool), var.clone()); + all_intervals.push(vec![var.clone(), neg]); + } + + cartesian_and(&all_intervals, builder) +} + +fn is_true_lit(e: &Expr) -> bool { + matches!(&e.kind, ExprKind::Lit(s) if matches!(s.node, LitKind::Bool(true))) +} + +fn and_simplify(builder: &ExprBuilder, lhs: Expr, rhs: Expr) -> Expr { + if is_true_lit(&lhs) { + rhs + } else if is_true_lit(&rhs) { + lhs + } else { + builder.binary(BinOpKind::And, Some(TyKind::Bool), lhs, rhs) + } +} + +// Returns every combination of one element per inner `Vec`, joined with `And`. +fn cartesian_and(lists: &[Vec], builder: &ExprBuilder) -> Vec { + lists + .iter() + .fold(vec![builder.bool_lit(true)], |acc, list| { + acc.iter() + .flat_map(|prefix| { + list.iter() + .map(move |item| and_simplify(builder, prefix.clone(), item.clone())) + }) + .collect() + }) +} From cf18e5c1fc162334bae8258a341badb36ff62a8d Mon Sep 17 00:00:00 2001 From: madita Date: Thu, 11 Jun 2026 15:58:06 +0200 Subject: [PATCH 10/11] z3rro: fix model evaluation for large and negative values Replaces the as_i64() fallback with string-based parsing of Z3's debug representation, handling integers and rationals that do not fit in a 64-bit signed integer. --- z3rro/src/model.rs | 110 +++++++++++++++++++++++++++++++-------------- 1 file changed, 77 insertions(+), 33 deletions(-) diff --git a/z3rro/src/model.rs b/z3rro/src/model.rs index ef1ea82b..56543567 100644 --- a/z3rro/src/model.rs +++ b/z3rro/src/model.rs @@ -185,16 +185,80 @@ impl<'ctx> SmtEval<'ctx> for Int<'ctx> { type Value = BigInt; fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { - // TODO: Z3's as_i64 only returns an i64 value. is there something more complete? - let value = model - .eval_ast(self, true) - .ok_or(SmtEvalError::EvalError)? - .as_i64() - .ok_or(SmtEvalError::ParseError)?; - Ok(BigInt::from(value)) + let res = model.eval_ast(self, true).ok_or(SmtEvalError::EvalError)?; + if let Some(value) = res.as_i64() { + return Ok(BigInt::from(value)); + } + parse_z3_integer(&format!("{res:?}")) } } +/// Parse a Z3 real value from its debug string representation. +/// +/// Z3 can produce several formats when `as_real()` doesn't fit in i64: +/// `(/ num.0 denom.0)`, `(- (/ num.0 denom.0))`, `(/ (- num.0) denom.0)` +fn parse_z3_real_string(s: &str) -> Result { + let s = s.trim(); + + // Strip outer "(- ...)" negation wrapper + if let Some(inner) = s.strip_prefix("(- ").and_then(|t| t.strip_suffix(')')) { + return parse_z3_real_string(inner).map(|r| -r); + } + + // Parse "(/ num denom)" where num/denom may themselves be "(- n.0)" + if let Some(body) = s.strip_prefix("(/ ").and_then(|t| t.strip_suffix(')')) { + let (num_str, den_str) = split_two_sexpr(body).ok_or(SmtEvalError::ParseError)?; + let numerator = parse_z3_integer(num_str.trim())?; + let denominator = parse_z3_integer(den_str.trim())?; + return Ok(BigRational::new(numerator, denominator)); + } + + // Plain integer (with or without ".0" suffix) + parse_z3_integer(s).map(BigRational::from) +} + +/// Parse a Z3 integer atom: `"42.0"`, `"42"`, or `"(- 42.0)"`. +fn parse_z3_integer(s: &str) -> Result { + let s = s.trim(); + if let Some(inner) = s.strip_prefix("(- ").and_then(|t| t.strip_suffix(')')) { + return parse_z3_integer(inner).map(|n| -n); + } + let s = s.trim_end_matches(".0"); + BigInt::from_str(s).map_err(|_| SmtEvalError::ParseError) +} + +/// Split a body string into exactly two s-expressions (atoms or parenthesised). +fn split_two_sexpr(s: &str) -> Option<(&str, &str)> { + let s = s.trim(); + let (first_end, second_start) = if s.starts_with('(') { + let mut depth = 0usize; + let mut end = 0; + for (i, c) in s.char_indices() { + match c { + '(' => depth += 1, + ')' => { + depth -= 1; + if depth == 0 { + end = i + 1; + break; + } + } + _ => {} + } + } + (end, end) + } else { + let end = s.find(|c: char| c.is_ascii_whitespace()).unwrap_or(s.len()); + (end, end) + }; + let first = &s[..first_end]; + let rest = s[second_start..].trim_start(); + if first.is_empty() || rest.is_empty() { + return None; + } + Some((first, rest)) +} + /// Evaluate a raw SMT value for display. /// /// This only recognizes z3rro's built-in list and array encodings and @@ -218,38 +282,18 @@ impl<'ctx> SmtEval<'ctx> for Real<'ctx> { type Value = BigRational; fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { - let res = model - .eval_ast(self, false) // TODO - .ok_or(SmtEvalError::EvalError)?; + let res = model.eval_ast(self, true).ok_or(SmtEvalError::EvalError)?; // The .as_real() method only returns a pair of i64 values. If the // results don't fit in these types, we start some funky string parsing. if let Some((num, den)) = res.as_real() { Ok(BigRational::new(num.into(), den.into())) } else { - // we parse a string of the form "(/ num.0 denom.0)" - let division_expr = format!("{res:?}"); - if !division_expr.starts_with("(/ ") || !division_expr.ends_with(".0)") { - return Err(SmtEvalError::ParseError); - } - - let mut parts = division_expr.split_ascii_whitespace(); - - let first_part = parts.next().ok_or(SmtEvalError::ParseError)?; - if first_part != "(/" { - return Err(SmtEvalError::ParseError); - } - - let second_part = parts.next().ok_or(SmtEvalError::ParseError)?; - let second_part = second_part.replace(".0", ""); - let numerator = BigInt::from_str(&second_part).map_err(|_| SmtEvalError::ParseError)?; - - let third_part = parts.next().ok_or(SmtEvalError::ParseError)?; - let third_part = third_part.replace(".0)", ""); - let denominator = - BigInt::from_str(&third_part).map_err(|_| SmtEvalError::ParseError)?; - - Ok(BigRational::new(numerator, denominator)) + // Parse Z3 real string representations. Possible formats: + // "(/ num.0 denom.0)" + // "(- (/ num.0 denom.0))" + // "(/ (- num.0) denom.0)" + parse_z3_real_string(&format!("{res:?}")) } } } From e1b84a47dad24dc50b5e9b297748a8ac8779bc2d Mon Sep 17 00:00:00 2001 From: madita Date: Mon, 15 Jun 2026 17:28:47 +0200 Subject: [PATCH 11/11] tests: add synthesis benchmark test suite Adds HeyVL test cases for invariant synthesis across four benchmark families: cegispro, ecoimp, polynomial, and seq_loops. --- .../cegispro/bounded_rw_multi_step.heyvl | 29 +++++++++++ tests/synthesis/cegispro/chain.heyvl | 32 ++++++++++++ tests/synthesis/cegispro/grid_small.heyvl | 24 +++++++++ tests/synthesis/cegispro/k_geo.heyvl | 27 ++++++++++ tests/synthesis/cegispro/zero_conf.heyvl | 50 +++++++++++++++++++ tests/synthesis/ecoimp/b_bridge.heyvl | 26 ++++++++++ tests/synthesis/ecoimp/i_condand.heyvl | 25 ++++++++++ tests/synthesis/ecoimp/i_geo.heyvl | 28 +++++++++++ tests/synthesis/ecoimp/i_no_loop.heyvl | 27 ++++++++++ tests/synthesis/polynomial/poly_geo_1.heyvl | 23 +++++++++ tests/synthesis/polynomial/sum.heyvl | 23 +++++++++ tests/synthesis/seq_loops/flip_twice.heyvl | 29 +++++++++++ 12 files changed, 343 insertions(+) create mode 100644 tests/synthesis/cegispro/bounded_rw_multi_step.heyvl create mode 100644 tests/synthesis/cegispro/chain.heyvl create mode 100644 tests/synthesis/cegispro/grid_small.heyvl create mode 100644 tests/synthesis/cegispro/k_geo.heyvl create mode 100644 tests/synthesis/cegispro/zero_conf.heyvl create mode 100644 tests/synthesis/ecoimp/b_bridge.heyvl create mode 100644 tests/synthesis/ecoimp/i_condand.heyvl create mode 100644 tests/synthesis/ecoimp/i_geo.heyvl create mode 100644 tests/synthesis/ecoimp/i_no_loop.heyvl create mode 100644 tests/synthesis/polynomial/poly_geo_1.heyvl create mode 100644 tests/synthesis/polynomial/sum.heyvl create mode 100644 tests/synthesis/seq_loops/flip_twice.heyvl diff --git a/tests/synthesis/cegispro/bounded_rw_multi_step.heyvl b/tests/synthesis/cegispro/bounded_rw_multi_step.heyvl new file mode 100644 index 00000000..ff49546f --- /dev/null +++ b/tests/synthesis/cegispro/bounded_rw_multi_step.heyvl @@ -0,0 +1,29 @@ +// RUN: @caesar synth --timeout 60 --refinement-mode fixed @file +// XFAIL: timeout + +domain Invariants { + syn func for_rw(ts: UInt [1,5], tx:UInt [0,2000000]) : EUReal +} + +@wp coproc bounded_rw_multi() -> (x: UInt [0,200000]) +pre 0.4 +post [x == 200000] +{ + var s: UInt [1,5] = unif(1,5) + @invariant(for_rw(s,x)) + while(0 (c: UInt [0,2]) +pre 0.8 +post [c == 1] +{ + var x: UInt [0,1000000000000] = 0 + c = 0 + + @invariant( + chain_inv(c,x) + ) + while ( + c <= 0 + && + x < 1000000000000 + ) { + var prob_choice: Bool = flip(0.000000000001) + if prob_choice { + c = 1 + } else { + x = x + 1 + } + } +} diff --git a/tests/synthesis/cegispro/grid_small.heyvl b/tests/synthesis/cegispro/grid_small.heyvl new file mode 100644 index 00000000..990644ef --- /dev/null +++ b/tests/synthesis/cegispro/grid_small.heyvl @@ -0,0 +1,24 @@ +// RUN: @caesar synth --refinement-mode fixed @file + +domain Invariants { + syn func for_grid_small(ta: UInt [0,10], tb:UInt [0,10]) : EUReal +} +@wp coproc grid_small() -> (a: UInt [0,10], b: UInt [0,10]) +pre 0.9 +post [a < 10 && 10 <= b] +{ + + a = 0 + b = 0 + + @invariant(for_grid_small(a,b)) + while(a<10 && b<10){ + + var prob_choice: Bool = flip(0.5) + if prob_choice { + a = a+1 + } else { + b = b+1 + } + } +} diff --git a/tests/synthesis/cegispro/k_geo.heyvl b/tests/synthesis/cegispro/k_geo.heyvl new file mode 100644 index 00000000..ba7fce0e --- /dev/null +++ b/tests/synthesis/cegispro/k_geo.heyvl @@ -0,0 +1,27 @@ +// RUN: @caesar synth @file + +domain MoreInvariants { + syn func k_geo_inv(k: UInt, N:UInt, x: UInt, y: UInt) : EUReal + +} +@wp coproc k_geo (N: UInt) -> (y:UInt) +pre N+1 +post y +{ + var x: UInt = 0 + y = 0 + var k: UInt = 0 + + var coin: Bool = true + @invariant(k_geo_inv(k,N,x,y)) + while k<= N { + coin = flip(0.5) + if coin { + k = k+1 + y = y+x + x = 0 + } + else { x = x+1} + + } +} diff --git a/tests/synthesis/cegispro/zero_conf.heyvl b/tests/synthesis/cegispro/zero_conf.heyvl new file mode 100644 index 00000000..e9692113 --- /dev/null +++ b/tests/synthesis/cegispro/zero_conf.heyvl @@ -0,0 +1,50 @@ +// RUN: @caesar synth --refinement-mode fixed @file + +domain Invariants { + syn func zero_conf_inv( + tstart: UInt [0,1], + testablished: UInt [0,1], + tcurprobe: UInt [0,100000000] + ) : EUReal +} + +coproc zero_conf () -> (established : UInt [0,1]) +pre 0.53 +post [established == 1] +{ + var start: UInt [0,1] = 1 + var curprobe: UInt [0,100000000] = 0 + + established = 0 + + @invariant( + zero_conf_inv(start, established, curprobe) + ) + while ( + curprobe < 100000000 && + established <= 0 && + start <= 1 + ) { + + if (start == 1) { + + var prob_choice: Bool = flip(0.5) + if prob_choice { + start = 0 + } else { + start = 0 + established = 1 + } + + } else { + + var prob_choice: Bool = flip(0.999999999) + if prob_choice { + curprobe = curprobe + 1 + } else { + start = 1 + curprobe = 0 + } + } + } +} diff --git a/tests/synthesis/ecoimp/b_bridge.heyvl b/tests/synthesis/ecoimp/b_bridge.heyvl new file mode 100644 index 00000000..5c7b655d --- /dev/null +++ b/tests/synthesis/ecoimp/b_bridge.heyvl @@ -0,0 +1,26 @@ +// RUN: @caesar synth --timeout 60 --refinement-mode degree @file + +domain MoreInvariants { + syn func bridge_inv(x: UInt, a: UInt, b: UInt) : EUReal +} + +@ert +coproc main(init_a: UInt, init_b: UInt, init_x: UInt) -> (a: UInt, b: UInt, x: UInt) + pre bridge_inv(init_x, init_b, init_a) + post 0 +{ + var prob_choice: Bool + a = init_a + b = init_b + x = init_x + @invariant(bridge_inv(x, b, a)) + while a < x && x < b { + tick 1 + prob_choice = flip(1/2) + if prob_choice { + x = x - 1 + } else { + x = x + 1 + } + } +} diff --git a/tests/synthesis/ecoimp/i_condand.heyvl b/tests/synthesis/ecoimp/i_condand.heyvl new file mode 100644 index 00000000..de664308 --- /dev/null +++ b/tests/synthesis/ecoimp/i_condand.heyvl @@ -0,0 +1,25 @@ +// RUN: @caesar synth --refinement-mode degree @file + +domain MoreInvariants { + syn func condand_inv(n: Int, m: Int) : EUReal +} + +@ert +coproc main(init_n: Int, init_m: Int) -> (n: Int, m: Int) + pre condand_inv(init_n, init_m) + post 0 +{ + var prob_choice: Bool + n = init_n + m = init_m + @invariant(condand_inv(n, m)) + while 0 < n && 0 < m { + prob_choice = flip(1/2) + if prob_choice { + n = n - 1 + } else { + m = m - 1 + } + tick 1 + } +} diff --git a/tests/synthesis/ecoimp/i_geo.heyvl b/tests/synthesis/ecoimp/i_geo.heyvl new file mode 100644 index 00000000..3c04e7e1 --- /dev/null +++ b/tests/synthesis/ecoimp/i_geo.heyvl @@ -0,0 +1,28 @@ +// RUN: @caesar synth --refinement-mode degree @file + +domain MoreInvariants { + syn func geo_inv(b: Int) : EUReal +} + +@ert +coproc main() -> (c: Int, b: Int) + pre geo_inv(0) + post 0 +{ + var prob_choice: Bool + b = 0 + @invariant(geo_inv(b)) + while 0 < b { + prob_choice = flip(1/2) + if prob_choice { + c = 1 + b = 0 + tick 1 + } else { + c = 0 + tick 1 + } + tick 2 + } + tick 1 +} diff --git a/tests/synthesis/ecoimp/i_no_loop.heyvl b/tests/synthesis/ecoimp/i_no_loop.heyvl new file mode 100644 index 00000000..98a9aeb0 --- /dev/null +++ b/tests/synthesis/ecoimp/i_no_loop.heyvl @@ -0,0 +1,27 @@ +// RUN: @caesar synth --refinement-mode degree @file + +domain MoreInvariants { + syn func no_loop_inv() : EUReal +} + +@ert +coproc main() -> (flag: Int, z: Int) + pre no_loop_inv() + post 0 +{ + var prob_choice: Bool + prob_choice = flip(1/2) + if prob_choice { + flag = 0 + tick 3 + } else { + prob_choice = flip(1/2) + if prob_choice { + flag = 1 + tick 5 + } else { + flag = 1 + tick 7 + } + } +} diff --git a/tests/synthesis/polynomial/poly_geo_1.heyvl b/tests/synthesis/polynomial/poly_geo_1.heyvl new file mode 100644 index 00000000..26cd45cb --- /dev/null +++ b/tests/synthesis/polynomial/poly_geo_1.heyvl @@ -0,0 +1,23 @@ +// RUN: @caesar synth --refinement-mode degree --unsigned-coefficients @file + +domain Invariants { + syn func syninv(c:UInt, coin: Bool) : EUReal +} + +@wp coproc flipWithspec() -> (c:UInt) +pre syninv(0,true) +post c*c +{ + c = 0 + var coin: Bool = true + @invariant(syninv(c,coin)) + while coin { + + var prob_choice: Bool = flip(0.6) + if prob_choice { + c = c + 1 + } else { + coin = false + } + } +} diff --git a/tests/synthesis/polynomial/sum.heyvl b/tests/synthesis/polynomial/sum.heyvl new file mode 100644 index 00000000..b905b798 --- /dev/null +++ b/tests/synthesis/polynomial/sum.heyvl @@ -0,0 +1,23 @@ +// RUN: @caesar synth --timeout 60 --refinement-mode degree --unsigned-coefficients @file + +domain Invariants { + syn func sum_inv(n: UInt, x: UInt, p: UReal) : UReal +} + +proc loop_proc(init_n: UInt, init_x: UInt, p: UReal) -> (x: UInt) +pre init_x + [init_n > 0]*((p*init_n)/2) +post x +{ + var n: UInt = init_n + x = init_x + + @invariant(sum_inv(n, x, p)) + while (n > 0) { + var prob_choice: Bool = flip(p) + if prob_choice { + x = x + n + } else { + } + n = n - 1 + } +} diff --git a/tests/synthesis/seq_loops/flip_twice.heyvl b/tests/synthesis/seq_loops/flip_twice.heyvl new file mode 100644 index 00000000..53654688 --- /dev/null +++ b/tests/synthesis/seq_loops/flip_twice.heyvl @@ -0,0 +1,29 @@ +// RUN: @caesar synth @file + +domain Invariants { + syn func first_loop(tc:UInt, tcoin: Bool) : EUReal + syn func second_loop(tc:UInt, tcoin: Bool) : EUReal + +} +@wp coproc fliptwice () -> (c:UInt) +pre 2 +post c +{ + c = 0 + var coin: Bool = true + @invariant(first_loop(c,coin)) + while coin { + coin = flip(0.5) + if coin { + c = c+1 + } + else {} + + } + coin = true + @invariant(second_loop(c,coin)) + while coin { + var prob_choice: Bool = flip(0.5) + if prob_choice { c = c + 1 } else { coin = false } + } +}