From 72d06798dabac4c0893072bd431ce260b65d742d Mon Sep 17 00:00:00 2001 From: Willem Wyndham Date: Mon, 17 Aug 2026 10:08:33 -0400 Subject: [PATCH 1/4] fix: track the soroban-sdk 26 line with a caret req An exact =26.0.1 pin conflicts with consumers locked to newer 26.x patches (perch locks 26.1.1); the 26.x line is what COMPATIBILITY.md actually promises. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01M52tZC7sppbbo1HDBpj9KK --- Cargo.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cargo.toml b/Cargo.toml index 446d195..44765f6 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,7 +9,7 @@ license = "Apache-2.0" repository = "https://github.com/nidohq/soroban-flux" [workspace.dependencies] -soroban-sdk = "=26.0.1" +soroban-sdk = "26" soroban-flux = { path = "crates/soroban-flux" } # Flux attribute macros. Git-only (no crates.io release); the rev must match # the installed flux toolchain — see COMPATIBILITY.md and the justfile's From dfb1b19753db8f6dbe2747eddebf430e7df0f141 Mon Sep 17 00:00:00 2001 From: Willem Wyndham Date: Mon, 17 Aug 2026 10:24:30 -0400 Subject: [PATCH 2/4] feat: bn254 module + sdk 26-27 compat range MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit BN254_R_BE single-source constant (pinned to decimal r by an independent long-division test), field_order/is_canonical_be/reduce_be helpers for consumers (nido pool + factory, UltraHonk verifiers) — replaces per-repo byte constants and cross-crate drift-guard tests. Widen soroban-sdk req to >=26,<28: perch is on 26, nido/admin-sep on 27; the touched API surface (BytesN/Bytes/U256/Env) is identical. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01M52tZC7sppbbo1HDBpj9KK --- Cargo.lock | 479 +++++++++++++++++++++++------ Cargo.toml | 5 +- crates/probe-sdk26/Cargo.toml | 5 +- crates/soroban-flux/Cargo.toml | 3 + crates/soroban-flux/src/bn254.rs | 43 +++ crates/soroban-flux/src/lib.rs | 1 + crates/soroban-flux/tests/bn254.rs | 61 ++++ 7 files changed, 502 insertions(+), 95 deletions(-) create mode 100644 crates/soroban-flux/src/bn254.rs create mode 100644 crates/soroban-flux/tests/bn254.rs diff --git a/Cargo.lock b/Cargo.lock index c13cdbb..68bd6e5 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -29,6 +29,15 @@ dependencies = [ "libc", ] +[[package]] +name = "arbitrary" +version = "1.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7d5a26814d8dcb93b0e5a0ff3c6d80a8843bafb21b39e8e18a6f05471870e110" +dependencies = [ + "derive_arbitrary", +] + [[package]] name = "ark-bls12-381" version = "0.5.0" @@ -189,6 +198,12 @@ version = "0.22.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "72b3254f16251a8381aa12e40e3c4d2f0199f8c6508fbecb9d91f575e0fbb8c6" +[[package]] +name = "base64ct" +version = "1.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2af50177e190e07a26ab74f8b1efbfe2ef87da2116221318cb1c2e82baf7de06" + [[package]] name = "bitflags" version = "1.3.2" @@ -246,6 +261,18 @@ dependencies = [ "syn 2.0.119", ] +[[package]] +name = "bytes-lit" +version = "0.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9b04f2b1d34cb428043f14aa4c853d14294532e8bbde3b6a3bc2faaaae31a1dd" +dependencies = [ + "num-bigint", + "proc-macro2", + "quote", + "syn 2.0.119", +] + [[package]] name = "cc" version = "1.4.3" @@ -326,6 +353,17 @@ dependencies = [ "serde_json", ] +[[package]] +name = "crate-git-revision" +version = "0.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "54851b5b3f24621804b1cded2820975623c205e3055d2d44031cdb1237339ac8" +dependencies = [ + "serde", + "serde_derive", + "serde_json", +] + [[package]] name = "crypto-bigint" version = "0.5.5" @@ -333,7 +371,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0dc92fb57ca44df6db8059111ab3af99a63d5d0f8375d9972e319a379c6bab76" dependencies = [ "generic-array", - "rand_core 0.6.4", + "rand_core", "subtle", "zeroize", ] @@ -355,7 +393,38 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ce6e4c961d6cd6c9a86db418387425e8bdeaf05b3c8bc1411e6dca4c252f1453" dependencies = [ "hybrid-array", - "rand_core 0.10.1", +] + +[[package]] +name = "ctor" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "67773048316103656a637612c4a62477603b777d91d9c62ff2290f9cde178fdb" +dependencies = [ + "ctor-proc-macro", + "dtor", +] + +[[package]] +name = "ctor-proc-macro" +version = "0.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e2931af7e13dc045d8e9d26afccc6fa115d64e115c9c84b1166288b46f6782c2" + +[[package]] +name = "curve25519-dalek" +version = "4.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "97fb8b7c4503de7d6ae7b42ab72a5a59857b4c937ec27a3d4539dba95b5ab2be" +dependencies = [ + "cfg-if", + "cpufeatures 0.2.17", + "curve25519-dalek-derive", + "digest 0.10.7", + "fiat-crypto 0.2.9", + "rustc_version", + "subtle", + "zeroize", ] [[package]] @@ -368,11 +437,9 @@ dependencies = [ "cpufeatures 0.3.0", "curve25519-dalek-derive", "digest 0.11.3", - "fiat-crypto", - "rand_core 0.10.1", + "fiat-crypto 0.3.0", "rustc_version", "subtle", - "zeroize", ] [[package]] @@ -511,6 +578,17 @@ dependencies = [ "serde_core", ] +[[package]] +name = "derive_arbitrary" +version = "1.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "67e77553c4162a157adbf834ebae5b415acbecbeafc7a74b0e886657506a7611" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.119", +] + [[package]] name = "digest" version = "0.10.7" @@ -539,6 +617,21 @@ version = "1.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "75b325c5dbd37f80359721ad39aca5a29fb04c89279657cffdda8736d0c0b9d2" +[[package]] +name = "dtor" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "404d02eeb088a82cfd873006cb713fe411306c7d182c344905e101fb1167d301" +dependencies = [ + "dtor-proc-macro", +] + +[[package]] +name = "dtor-proc-macro" +version = "0.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f678cf4a922c215c63e0de95eb1ff08a958a81d47e485cf9da1e27bf6305cfa5" + [[package]] name = "dyn-clone" version = "1.0.20" @@ -555,29 +648,30 @@ dependencies = [ "digest 0.10.7", "elliptic-curve", "rfc6979", - "signature 2.2.0", + "signature", ] [[package]] name = "ed25519" -version = "3.0.0" +version = "2.2.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "29fcf32e6c73d1079f83ab4d782de2d81620346a5f38c6237a86a22f8368980a" +checksum = "115531babc129696a58c64a4fef0a8bf9e9698629fb97e9e40767d235cfbcd53" dependencies = [ - "signature 3.0.0", + "pkcs8", + "signature", ] [[package]] name = "ed25519-dalek" -version = "3.0.0" +version = "2.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ebaa1a2bf1290ab3bfe5a7b771d050ebffab2711c19a81691c683a5144a25de" +checksum = "70e796c081cee67dc755e1a36a0a172b897fab85fc3f6bc48307991f64e4eca9" dependencies = [ - "curve25519-dalek", + "curve25519-dalek 4.1.3", "ed25519", - "rand_core 0.10.1", - "sha2 0.11.0", - "signature 3.0.0", + "rand_core", + "serde", + "sha2", "subtle", "zeroize", ] @@ -612,7 +706,7 @@ dependencies = [ "ff", "generic-array", "group", - "rand_core 0.6.4", + "rand_core", "sec1", "subtle", "zeroize", @@ -662,10 +756,16 @@ version = "0.13.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c0b50bfb653653f9ca9095b427bed08ab8d75a137839d9ad64eb11810d5b6393" dependencies = [ - "rand_core 0.6.4", + "rand_core", "subtle", ] +[[package]] +name = "fiat-crypto" +version = "0.2.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "28dea519a9695b9977216879a3ebfddf92f1c08c05d984f8996aecd6ecdc811d" + [[package]] name = "fiat-crypto" version = "0.3.0" @@ -765,7 +865,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f0f9ef7462f7c099f518d754361858f86d8a07af53ba9af0fe635bbccb151a63" dependencies = [ "ff", - "rand_core 0.6.4", + "rand_core", "subtle", ] @@ -995,7 +1095,7 @@ dependencies = [ "cfg-if", "ecdsa", "elliptic-curve", - "sha2 0.10.9", + "sha2", ] [[package]] @@ -1102,7 +1202,7 @@ dependencies = [ "ecdsa", "elliptic-curve", "primeorder", - "sha2 0.10.9", + "sha2", ] [[package]] @@ -1117,6 +1217,16 @@ version = "0.2.17" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd" +[[package]] +name = "pkcs8" +version = "0.10.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f950b2377845cebe5cf8b5165cb3cc1a5e0fa5cfa3e1f7f55707d8fd82e0a7b7" +dependencies = [ + "der", + "spki", +] + [[package]] name = "portable-atomic" version = "1.15.0" @@ -1171,7 +1281,7 @@ name = "probe-sdk26" version = "0.1.0" dependencies = [ "soroban-flux", - "soroban-sdk", + "soroban-sdk 26.1.1", ] [[package]] @@ -1200,7 +1310,7 @@ checksum = "22f6172bdec972074665ed81ed53b71da00bfc44b65a753cfde883ec4c702a1a" dependencies = [ "libc", "rand_chacha", - "rand_core 0.6.4", + "rand_core", ] [[package]] @@ -1210,7 +1320,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88" dependencies = [ "ppv-lite86", - "rand_core 0.6.4", + "rand_core", ] [[package]] @@ -1222,12 +1332,6 @@ dependencies = [ "getrandom", ] -[[package]] -name = "rand_core" -version = "0.10.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "63b8176103e19a2643978565ca18b50549f6101881c443590420e4dc998a3c69" - [[package]] name = "ref-cast" version = "1.0.26" @@ -1415,17 +1519,6 @@ dependencies = [ "digest 0.10.7", ] -[[package]] -name = "sha2" -version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "446ba717509524cb3f22f17ecc096f10f4822d76ab5c0b9822c5f9c284e825f4" -dependencies = [ - "cfg-if", - "cpufeatures 0.3.0", - "digest 0.11.3", -] - [[package]] name = "sha3" version = "0.10.9" @@ -1449,16 +1542,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "77549399552de45a898a580c1b41d445bf730df867cc44e6c0233bbc4b8329de" dependencies = [ "digest 0.10.7", - "rand_core 0.6.4", -] - -[[package]] -name = "signature" -version = "3.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "28d567dcbaf0049cb8ac2608a76cd95ff9e4412e1899d389ee400918ca7537f5" -dependencies = [ - "rand_core 0.10.1", + "rand_core", ] [[package]] @@ -1475,9 +1559,21 @@ checksum = "8ed6a63f02c8539c91a8685a86f4099661ba3da017932f6ebbea6de3f0fa7c90" [[package]] name = "soroban-builtin-sdk-macros" -version = "26.1.3" +version = "26.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cc4a09f48a67357fdad682b601f4a2f3fdd8d897f3a97c2e1704fa22b0a474e0" +dependencies = [ + "itertools", + "proc-macro2", + "quote", + "syn 2.0.119", +] + +[[package]] +name = "soroban-builtin-sdk-macros" +version = "27.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "35a3a2b57b132b800e132d2c81e1818359bb2cf787ca39c61c151d6bd0798403" +checksum = "b77bc93d930032c487cb1506b6ed166b2af49db76d52678ec4887ac621ecce01" dependencies = [ "itertools", "proc-macro2", @@ -1487,43 +1583,109 @@ dependencies = [ [[package]] name = "soroban-env-common" -version = "26.1.3" +version = "26.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ededa4063061c00886490bb3290e416ee0b03d7732a7378ccba7bb19211fb00c" +dependencies = [ + "crate-git-revision 0.0.6", + "ethnum", + "num-derive", + "num-traits", + "soroban-env-macros 26.1.4", + "soroban-wasmi", + "static_assertions", + "stellar-xdr 26.0.1", + "wasmparser", +] + +[[package]] +name = "soroban-env-common" +version = "27.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0c76fad735f9622d8aa0fa0c75838d2023a659a0c57638a783b8b2eb967f7822" +checksum = "6b22e9981cdd444f3aa6734bc58d76195bf7eca3ccf1dd432b875af5d02da068" dependencies = [ - "crate-git-revision", + "arbitrary", + "crate-git-revision 0.0.6", "ethnum", "num-derive", "num-traits", - "soroban-env-macros", + "serde", + "soroban-env-macros 27.0.1", "soroban-wasmi", "static_assertions", - "stellar-xdr", + "stellar-xdr 27.0.0", "wasmparser", ] [[package]] name = "soroban-env-guest" -version = "26.1.3" +version = "26.1.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "15aeed6d7a4dc4d3bba65e2ac92f7eeaa664900bbc82e1055e024bf637d74ed3" +checksum = "1ff2525f31e2453b52e90400a2952ce4618f8925bd03167938573e83c320c33f" dependencies = [ - "soroban-env-common", + "soroban-env-common 26.1.4", "static_assertions", ] +[[package]] +name = "soroban-env-guest" +version = "27.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b6072f99ca6bf8e8d5b04e05d083dac785e5357d9c0f36a6658f819c2fd7d67" +dependencies = [ + "soroban-env-common 27.0.1", + "static_assertions", +] + +[[package]] +name = "soroban-env-host" +version = "26.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "755806fedf2c948e882dff4bf69a8e844c9950b1d534abcadba4026150180274" +dependencies = [ + "ark-bls12-381", + "ark-bn254", + "ark-ec", + "ark-ff", + "ark-serialize", + "curve25519-dalek 5.0.0", + "ecdsa", + "ed25519-dalek", + "elliptic-curve", + "generic-array", + "getrandom", + "hex-literal", + "hmac", + "k256", + "num-derive", + "num-integer", + "num-traits", + "p256", + "rand", + "rand_chacha", + "sec1", + "sha2", + "sha3", + "soroban-builtin-sdk-macros 26.1.4", + "soroban-env-common 26.1.4", + "soroban-wasmi", + "static_assertions", + "stellar-strkey 0.0.13", + "wasmparser", +] + [[package]] name = "soroban-env-host" -version = "26.1.3" +version = "27.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6fb523456b4efe9cdf869233cff5a2a1a5ebfae8c0acc405e57479c83781a20c" +checksum = "2c06afd7c75ce150ce53e4d77a77645b18e3fb61856a0ddc42bfcecdc39fa3b9" dependencies = [ "ark-bls12-381", "ark-bn254", "ark-ec", "ark-ff", "ark-serialize", - "curve25519-dalek", + "curve25519-dalek 5.0.0", "ecdsa", "ed25519-dalek", "elliptic-curve", @@ -1539,10 +1701,10 @@ dependencies = [ "rand", "rand_chacha", "sec1", - "sha2 0.10.9", + "sha2", "sha3", - "soroban-builtin-sdk-macros", - "soroban-env-common", + "soroban-builtin-sdk-macros 27.0.1", + "soroban-env-common 27.0.1", "soroban-wasmi", "static_assertions", "stellar-strkey 0.0.13", @@ -1551,16 +1713,31 @@ dependencies = [ [[package]] name = "soroban-env-macros" -version = "26.1.3" +version = "26.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e446ac7f005d89cb77cc4e2cc006377e1a8c970c9b05d11968a32f78e10e4ef4" +dependencies = [ + "itertools", + "proc-macro2", + "quote", + "serde", + "serde_json", + "stellar-xdr 26.0.1", + "syn 2.0.119", +] + +[[package]] +name = "soroban-env-macros" +version = "27.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2ada3449bb23c964a88a1bf633ac66ca3ebac2061693f53148b199ce816791d0" +checksum = "647811bdd28a3ec40296987f6635781e5e1141c8f5affbbd53ba12b6295b7bb6" dependencies = [ "itertools", "proc-macro2", "quote", "serde", "serde_json", - "stellar-xdr", + "stellar-xdr 27.0.0", "syn 2.0.119", ] @@ -1569,33 +1746,91 @@ name = "soroban-flux" version = "0.1.0" dependencies = [ "flux-rs", - "soroban-sdk", + "soroban-sdk 27.0.6", +] + +[[package]] +name = "soroban-ledger-snapshot" +version = "27.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b59883d8bd0d1aed8d57579a9974ab88eaf787dd0a1af104f6881b5707450558" +dependencies = [ + "serde", + "serde_json", + "serde_with", + "soroban-env-common 27.0.1", + "soroban-env-host 27.0.1", + "thiserror 1.0.69", ] [[package]] name = "soroban-sdk" -version = "26.0.1" +version = "26.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5de6ad39b7070e8703d01c3abad13e75ea5e65b1a5ce5e86b98d724773282044" +checksum = "b4ce2a22afcbfc9407fe32ce789f441636d62cd078a4cc126191932b74b1e6c4" dependencies = [ - "bytes-lit", - "crate-git-revision", + "bytes-lit 0.0.5", + "crate-git-revision 0.0.6", "rand", "rustc_version", "serde", "serde_json", - "soroban-env-guest", - "soroban-env-host", - "soroban-sdk-macros", + "soroban-env-guest 26.1.4", + "soroban-env-host 26.1.4", + "soroban-sdk-macros 26.1.1", "stellar-strkey 0.0.16", "visibility", ] +[[package]] +name = "soroban-sdk" +version = "27.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6c3f21971c84fcfb08957e3e8f5a9a70f134cb07ad9ee053ac7e6d7a887a82af" +dependencies = [ + "arbitrary", + "bytes-lit 0.0.6", + "crate-git-revision 0.0.9", + "ctor", + "derive_arbitrary", + "ed25519-dalek", + "rand", + "rustc_version", + "serde", + "serde_json", + "soroban-env-guest 27.0.1", + "soroban-env-host 27.0.1", + "soroban-ledger-snapshot", + "soroban-sdk-macros 27.0.6", + "stellar-strkey 0.0.16", + "visibility", +] + +[[package]] +name = "soroban-sdk-macros" +version = "26.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6538ceb7d40c01499c2779b449a697c56c62a60bae6e5c5705d3a782075b5028" +dependencies = [ + "darling 0.20.11", + "heck", + "itertools", + "macro-string", + "proc-macro2", + "quote", + "sha2", + "soroban-env-common 26.1.4", + "soroban-spec 26.1.1", + "soroban-spec-rust 26.1.1", + "stellar-xdr 26.0.1", + "syn 2.0.119", +] + [[package]] name = "soroban-sdk-macros" -version = "26.1.0" +version = "27.0.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "abbdc02e0d789df78c25b0d056eb01cc906feab690c74895febc96890a0e6aa0" +checksum = "3bd4a847273d749807fe2eb52e2b9c1917ee482cd6a39465cad5c389548996ad" dependencies = [ "darling 0.20.11", "heck", @@ -1603,11 +1838,11 @@ dependencies = [ "macro-string", "proc-macro2", "quote", - "sha2 0.10.9", - "soroban-env-common", - "soroban-spec", - "soroban-spec-rust", - "stellar-xdr", + "sha2", + "soroban-env-common 27.0.1", + "soroban-spec 27.0.6", + "soroban-spec-rust 27.0.6", + "stellar-xdr 27.0.0", "syn 2.0.119", ] @@ -1618,8 +1853,21 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ca18ced644f86e1e36a0fddb856d45a6a8478296e6b54941fb5e2daa96076bf7" dependencies = [ "base64", - "sha2 0.10.9", - "stellar-xdr", + "sha2", + "stellar-xdr 26.0.1", + "thiserror 1.0.69", + "wasmparser", +] + +[[package]] +name = "soroban-spec" +version = "27.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "473404322827b285cbcd87517f365986bd63af7842c78b2a86ee061715fda61e" +dependencies = [ + "base64", + "sha2", + "stellar-xdr 27.0.0", "thiserror 1.0.69", "wasmparser", ] @@ -1633,9 +1881,25 @@ dependencies = [ "prettyplease", "proc-macro2", "quote", - "sha2 0.10.9", - "soroban-spec", - "stellar-xdr", + "sha2", + "soroban-spec 26.1.1", + "stellar-xdr 26.0.1", + "syn 2.0.119", + "thiserror 1.0.69", +] + +[[package]] +name = "soroban-spec-rust" +version = "27.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2f25698b6ce2125850a9ef075cf9ba1e8d25b4cfa0c46aca42dadd80cc29d881" +dependencies = [ + "prettyplease", + "proc-macro2", + "quote", + "sha2", + "soroban-spec 27.0.6", + "stellar-xdr 27.0.0", "syn 2.0.119", "thiserror 1.0.69", ] @@ -1659,6 +1923,16 @@ version = "0.9.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3763264f6b73151db08c50ff20d7d8a0b8796e021cdea7ceedad07b80155fa0e" +[[package]] +name = "spki" +version = "0.7.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d91ed6c858b01f942cd56b37a94b3e0a1798290327d1236e4d9cf4eaca44d29d" +dependencies = [ + "base64ct", + "der", +] + [[package]] name = "stable_deref_trait" version = "1.2.1" @@ -1677,7 +1951,7 @@ version = "0.0.13" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ee1832fb50c651ad10f734aaf5d31ca5acdfb197a6ecda64d93fcdb8885af913" dependencies = [ - "crate-git-revision", + "crate-git-revision 0.0.6", "data-encoding", ] @@ -1687,7 +1961,7 @@ version = "0.0.16" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "084afcb0d458c3d5d5baa2d294b18f881e62cc258ef539d8fdf68be7dbe45520" dependencies = [ - "crate-git-revision", + "crate-git-revision 0.0.6", "data-encoding", "heapless", ] @@ -1700,13 +1974,32 @@ checksum = "ea6e29c7e1f071c2767916460d006668197843d5d93f0ec8893a26f72a14f595" dependencies = [ "base64", "cfg_eval", - "crate-git-revision", + "crate-git-revision 0.0.6", + "escape-bytes", + "ethnum", + "hex", + "serde", + "serde_with", + "sha2", + "stellar-strkey 0.0.13", +] + +[[package]] +name = "stellar-xdr" +version = "27.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "05ff843326969bdf1ef673dcdba94c08f4a3c8f1e58d6e6ef39b1bd4f749179a" +dependencies = [ + "arbitrary", + "base64", + "cfg_eval", + "crate-git-revision 0.0.6", "escape-bytes", "ethnum", "hex", "serde", "serde_with", - "sha2 0.10.9", + "sha2", "stellar-strkey 0.0.13", ] diff --git a/Cargo.toml b/Cargo.toml index 44765f6..8dea7db 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,7 +9,10 @@ license = "Apache-2.0" repository = "https://github.com/nidohq/soroban-flux" [workspace.dependencies] -soroban-sdk = "26" +# Wide range: consumers span sdk 26 (perch) and 27 (nido, admin-sep). The +# API surface this crate touches (BytesN/Bytes/U256/Env) is stable across +# both; each consumer's lockfile picks its own single version. +soroban-sdk = ">=26.0.1, <28" soroban-flux = { path = "crates/soroban-flux" } # Flux attribute macros. Git-only (no crates.io release); the rev must match # the installed flux toolchain — see COMPATIBILITY.md and the justfile's diff --git a/crates/probe-sdk26/Cargo.toml b/crates/probe-sdk26/Cargo.toml index 559691d..8d074c5 100644 --- a/crates/probe-sdk26/Cargo.toml +++ b/crates/probe-sdk26/Cargo.toml @@ -8,7 +8,10 @@ license.workspace = true [dependencies] soroban-flux = { workspace = true } -soroban-sdk = { workspace = true } +# The probe holds this workspace to the sdk-26 line (the lib crate itself +# accepts 26–27 for consumers); 26.0.x's testutils chain no longer builds +# (ed25519-dalek CryptoRng drift), so track the 26.1 patch line. +soroban-sdk = "26.1" [package.metadata.flux] enabled = true diff --git a/crates/soroban-flux/Cargo.toml b/crates/soroban-flux/Cargo.toml index 297e7db..6c30e0a 100644 --- a/crates/soroban-flux/Cargo.toml +++ b/crates/soroban-flux/Cargo.toml @@ -10,6 +10,9 @@ repository.workspace = true flux-rs = { workspace = true } soroban-sdk = { workspace = true } +[dev-dependencies] +soroban-sdk = { workspace = true, features = ["testutils"] } + [package.metadata.flux] enabled = true diff --git a/crates/soroban-flux/src/bn254.rs b/crates/soroban-flux/src/bn254.rs new file mode 100644 index 0000000..1c0ab9b --- /dev/null +++ b/crates/soroban-flux/src/bn254.rs @@ -0,0 +1,43 @@ +//! BN254 (alt_bn128) scalar-field helpers — the single source of truth for +//! the field order `r` across consumers (nido zk-recovery pool, nido factory, +//! UltraHonk verifiers), replacing per-repo hand-maintained byte constants +//! and their cross-crate drift-guard tests. +//! +//! The byte constant is pinned against the decimal value of `r` by this +//! crate's own tests (`tests/bn254.rs`), and the [`crate::defs`] predicate +//! `bn254_canonical` states the same bound for refinement proofs. + +use soroban_sdk::{Bytes, BytesN, Env, U256}; + +/// Big-endian bytes of the BN254 scalar field order +/// `r = 21888242871839275222246405745257275088548364400416034343698204186575808495617`. +pub const BN254_R_BE: [u8; 32] = [ + 0x30, 0x64, 0x4e, 0x72, 0xe1, 0x31, 0xa0, 0x29, 0xb8, 0x50, 0x45, 0xb6, 0x81, 0x81, 0x58, 0x5d, + 0x28, 0x33, 0xe8, 0x48, 0x79, 0xb9, 0x70, 0x91, 0x43, 0xe1, 0xf5, 0x93, 0xf0, 0x00, 0x00, 0x01, +]; + +/// The field order `r` as a host [`U256`]. +pub fn field_order(env: &Env) -> U256 { + U256::from_be_bytes(env, &Bytes::from_array(env, &BN254_R_BE)) +} + +/// Whether `bytes`, interpreted as a big-endian integer, is a canonical +/// field element (`< r`). Callers decide the failure action (reject vs +/// reduce) — rejecting avoids silently colliding two byte strings onto one +/// element. +pub fn is_canonical_be(env: &Env, bytes: &BytesN<32>) -> bool { + let value = U256::from_be_bytes(env, &Bytes::from_array(env, &bytes.to_array())); + value < field_order(env) +} + +/// `bytes mod r`, big-endian in and out — for deterministically deriving a +/// canonical element from an arbitrary 32-byte digest (e.g. dummy +/// commitments). Real user-supplied elements should be gated with +/// [`is_canonical_be`] instead, never reduced. +pub fn reduce_be(env: &Env, bytes: &BytesN<32>) -> BytesN<32> { + let value = U256::from_be_bytes(env, &Bytes::from_array(env, &bytes.to_array())); + let reduced = value.rem_euclid(&field_order(env)); + let mut out = [0u8; 32]; + reduced.to_be_bytes().copy_into_slice(&mut out); + BytesN::from_array(env, &out) +} diff --git a/crates/soroban-flux/src/lib.rs b/crates/soroban-flux/src/lib.rs index 52e5a6f..041c717 100644 --- a/crates/soroban-flux/src/lib.rs +++ b/crates/soroban-flux/src/lib.rs @@ -19,6 +19,7 @@ #![no_std] +pub mod bn254; pub mod defs; pub mod prelude; pub mod specs; diff --git a/crates/soroban-flux/tests/bn254.rs b/crates/soroban-flux/tests/bn254.rs new file mode 100644 index 0000000..d7a5994 --- /dev/null +++ b/crates/soroban-flux/tests/bn254.rs @@ -0,0 +1,61 @@ +//! Pins `BN254_R_BE` to the decimal field order and checks the helper +//! behavior at the boundary values `r-1`, `r`, `r+1`. + +use soroban_flux::bn254::{is_canonical_be, reduce_be, BN254_R_BE}; +use soroban_sdk::{BytesN, Env}; + +/// Recompute the byte constant from the decimal string with plain bignum +/// arithmetic — no shared code path with the constant itself. +fn r_bytes_from_decimal() -> [u8; 32] { + const R_DEC: &str = + "21888242871839275222246405745257275088548364400416034343698204186575808495617"; + let mut digits: Vec = R_DEC.bytes().map(|b| b - b'0').collect(); + let mut out = [0u8; 32]; + for byte in out.iter_mut().rev() { + // digits mod 256 -> byte; digits /= 256, one long-division pass each. + let mut rem: u32 = 0; + let mut next = Vec::with_capacity(digits.len()); + for &d in &digits { + let cur = rem * 10 + u32::from(d); + next.push((cur / 256) as u8); + rem = cur % 256; + } + while next.first() == Some(&0) { + next.remove(0); + } + *byte = rem as u8; + digits = next; + } + assert!(digits.is_empty(), "r must fit in 32 bytes"); + out +} + +#[test] +fn constant_matches_decimal_r() { + assert_eq!(BN254_R_BE, r_bytes_from_decimal()); +} + +#[test] +fn canonicity_boundaries() { + let env = Env::default(); + + let r = BytesN::from_array(&env, &BN254_R_BE); + assert!(!is_canonical_be(&env, &r), "r itself is not canonical"); + + let mut below = BN254_R_BE; + below[31] -= 1; // ...00_01 -> ...00_00 + let below = BytesN::from_array(&env, &below); + assert!(is_canonical_be(&env, &below), "r - 1 is canonical"); + + let mut above = BN254_R_BE; + above[31] += 1; // ...00_01 -> ...00_02 + let above = BytesN::from_array(&env, &above); + assert!(!is_canonical_be(&env, &above), "r + 1 is not canonical"); + + assert_eq!( + reduce_be(&env, &r), + BytesN::from_array(&env, &[0u8; 32]), + "r mod r == 0" + ); + assert_eq!(reduce_be(&env, &below), below, "(r - 1) mod r == r - 1"); +} From e7af29a950c28687fc47c82f06a2834471cb59b1 Mon Sep 17 00:00:00 2001 From: Willem Wyndham Date: Mon, 17 Aug 2026 10:48:59 -0400 Subject: [PATCH 3/4] =?UTF-8?q?feat(probe):=20contractimpl=20inline-spec?= =?UTF-8?q?=20probe=20=E2=80=94=20sdk=20patch=20obsolete,=20dispatcher=20c?= =?UTF-8?q?hecked=20as=20caller?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Modern soroban-sdk (25+) already strips non-doc/cfg/allow/deny attrs from macro-generated code (pass_through_attr_to_gen_code), so the 2024 flux-rs fork's filter_out_flux_attrs patch is unnecessary. Better: the generated invoke_raw dispatcher is flux-checked as a caller, which makes input refinements on public entry points unprovable — exactly right, since the host can pass anything. Probe pins both findings; recorded in COMPATIBILITY.md. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01M52tZC7sppbbo1HDBpj9KK --- COMPATIBILITY.md | 13 ++++++++ crates/probe-sdk26/src/contract_probe.rs | 38 ++++++++++++++++++++++++ crates/probe-sdk26/src/lib.rs | 1 + 3 files changed, 52 insertions(+) create mode 100644 crates/probe-sdk26/src/contract_probe.rs diff --git a/COMPATIBILITY.md b/COMPATIBILITY.md index 8676f57..4faacdb 100644 --- a/COMPATIBILITY.md +++ b/COMPATIBILITY.md @@ -41,3 +41,16 @@ All three probes green; whole run sub-second warm, ~25 s cold (dep compile). 5. `extern_spec` impl blocks must mirror the SDK's *block structure*, not just signatures: `Vec::new`/`push_back` live in the `T: IntoVal + TryFromVal` block, `len` in a separate unbounded `impl Vec`. + +## contractimpl inline-annotation findings (2026-08-17, probe 4) + +- The 2024 flux-rs sdk-fork patch (`filter_out_flux_attrs`) is **obsolete**: + soroban-sdk 25+ strips all non-doc/cfg/allow/deny attributes from + macro-generated code via `pass_through_attr_to_gen_code`, so `flux_tool::*` + attrs never reach generated copies. Inline `#[sig]` on `#[contractimpl]` + methods works without any sdk patch. +- The generated dispatcher (`__Ty__fn__invoke_raw`) is flux-checked **as a + caller** of the annotated method: input refinements on public entry points + are rejected as unprovable preconditions (the host can pass anything). + Correct pattern: entry points validate at the boundary and carry + postconditions; rich preconditions live on the internal macro-free layer. diff --git a/crates/probe-sdk26/src/contract_probe.rs b/crates/probe-sdk26/src/contract_probe.rs new file mode 100644 index 0000000..116acc3 --- /dev/null +++ b/crates/probe-sdk26/src/contract_probe.rs @@ -0,0 +1,38 @@ +//! Probe 4: an inline flux spec on a `#[contractimpl]` method. +//! +//! Two findings this probe pins down: +//! +//! 1. **Attr stripping is already upstream.** The 2024 flux-rs sdk fork +//! patched the macros to strip `flux_tool::*` attributes from generated +//! copies; modern sdks (25+) do this generally — +//! `pass_through_attr_to_gen_code` allowlists only doc/cfg/allow/deny onto +//! generated code. No sdk patch is needed for inline annotation. +//! +//! 2. **The generated dispatcher is checked as a caller.** `#[contractimpl]` +//! emits `__Probe__probe_spend__invoke_raw`, which calls the method with +//! host-decoded (arbitrary) values — so flux rejects *input refinements* +//! on public entry points as unprovable preconditions. That is soundness, +//! not friction: a real caller can pass any i128. Entry points therefore +//! validate at the boundary and carry postconditions; rich preconditions +//! belong on the internal (macro-free) library layer. + +use soroban_flux::prelude::*; +use soroban_sdk::{contract, contractimpl, Env}; + +#[contract] +pub struct Probe; + +#[contractimpl] +impl Probe { + /// Overdraft-safe spend as a real contract entry point: unrefined inputs + /// (the host can send anything), boundary validation inside, and a + /// flux-proven non-negative result. + #[sig(fn(env: Env, balance: i128, amount: i128) -> i128{v: v >= 0})] + pub fn probe_spend(env: Env, balance: i128, amount: i128) -> i128 { + let _ = env; + if balance < 0 || amount < 0 || amount > balance { + return 0; + } + balance - amount + } +} diff --git a/crates/probe-sdk26/src/lib.rs b/crates/probe-sdk26/src/lib.rs index 672aa18..2a9877e 100644 --- a/crates/probe-sdk26/src/lib.rs +++ b/crates/probe-sdk26/src/lib.rs @@ -10,6 +10,7 @@ #![no_std] +pub mod contract_probe; pub mod extern_specs; pub mod neg; pub mod pure; From 3170467df435aff14e9d7413659f4d04c25e5013 Mon Sep 17 00:00:00 2001 From: Willem Wyndham Date: Mon, 17 Aug 2026 11:03:06 -0400 Subject: [PATCH 4/4] =?UTF-8?q?feat:=20vendor=20the=20flux=20attribute=20s?= =?UTF-8?q?tack=20=E2=80=94=20every=20crate=20now=20crates.io-publishable?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Vendor lib/flux-{attrs-impl,attrs,rs} from flux-rs/flux (MIT) at FLUX_REV as soroban-flux-{attrs-impl,attrs,rs}, using cargo dependency renaming so both the vendored sources and this workspace's flux_rs:: paths stay byte-identical to upstream — only Cargo.toml manifests differ (see crates/soroban-flux-attrs-impl/VENDORED.md). soroban-flux switches from the flux-rs git dep to the vendored path dep, removing the last git dependency from the publish graph (crates.io forbids them). Proven equivalent: cargo flux verifies identically under the vendored stack (the driver interoperates via the flux_tool attribute namespace, not crate identity); stable tests + probes all green. release-plz.toml lands with admin-sep's pattern (workspace release=false + per-package opt-in). Lint policy moves to [lints] tables: first-party crates deny warnings via workspace lints; vendored crates cap to allow so upstream source never has to satisfy this repo's lint bar (and the clippy workspace-wrapper can't fail the build over vendored style). Publishing itself stays deferred per the locked decision. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01M52tZC7sppbbo1HDBpj9KK --- .github/workflows/ci.yml | 6 +- COMPATIBILITY.md | 2 +- Cargo.lock | 51 +- Cargo.toml | 32 +- crates/probe-sdk26/Cargo.toml | 4 +- crates/soroban-flux-attrs-impl/Cargo.toml | 20 + .../soroban-flux-attrs-impl/LICENSE-UPSTREAM | 17 + crates/soroban-flux-attrs-impl/VENDORED.md | 17 + crates/soroban-flux-attrs-impl/build.rs | 6 + crates/soroban-flux-attrs-impl/src/ast.rs | 2847 +++++++++++++++++ .../src/extern_spec.rs | 694 ++++ crates/soroban-flux-attrs-impl/src/lib.rs | 189 ++ crates/soroban-flux-attrs/Cargo.toml | 22 + crates/soroban-flux-attrs/build.rs | 6 + crates/soroban-flux-attrs/src/lib.rs | 253 ++ crates/soroban-flux-rs/Cargo.toml | 22 + crates/soroban-flux-rs/src/bitvec.rs | 451 +++ crates/soroban-flux-rs/src/lib.rs | 104 + justfile | 8 +- release-plz.toml | 32 + 20 files changed, 4742 insertions(+), 41 deletions(-) create mode 100644 crates/soroban-flux-attrs-impl/Cargo.toml create mode 100644 crates/soroban-flux-attrs-impl/LICENSE-UPSTREAM create mode 100644 crates/soroban-flux-attrs-impl/VENDORED.md create mode 100644 crates/soroban-flux-attrs-impl/build.rs create mode 100644 crates/soroban-flux-attrs-impl/src/ast.rs create mode 100644 crates/soroban-flux-attrs-impl/src/extern_spec.rs create mode 100644 crates/soroban-flux-attrs-impl/src/lib.rs create mode 100644 crates/soroban-flux-attrs/Cargo.toml create mode 100644 crates/soroban-flux-attrs/build.rs create mode 100644 crates/soroban-flux-attrs/src/lib.rs create mode 100644 crates/soroban-flux-rs/Cargo.toml create mode 100644 crates/soroban-flux-rs/src/bitvec.rs create mode 100644 crates/soroban-flux-rs/src/lib.rs create mode 100644 release-plz.toml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3430558..befe306 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -22,8 +22,10 @@ jobs: - uses: actions/checkout@v4 - uses: dtolnay/rust-toolchain@stable - uses: Swatinem/rust-cache@v2 - - run: cargo fmt --all --check - - run: cargo clippy --workspace --all-targets -- -D warnings + # fmt/clippy scope excludes the byte-identical vendored flux crates + # (crates/soroban-flux-attrs-impl/VENDORED.md). + - run: cargo fmt -p soroban-flux -p probe-sdk26 --check + - run: cargo clippy --workspace --all-targets - run: cargo test --workspace # The verification gate: cargo flux over every flux-enabled crate. diff --git a/COMPATIBILITY.md b/COMPATIBILITY.md index 4faacdb..cfd788f 100644 --- a/COMPATIBILITY.md +++ b/COMPATIBILITY.md @@ -6,7 +6,7 @@ bump here first, burn in, then roll out. | soroban-flux | flux rev | nightly | soroban-sdk | z3 | fixpoint | status | |---|---|---|---|---|---|---| -| 0.1.0-dev | `283ad73` (2026-08-17) | nightly-2026-02-05 | =26.0.1 | 5.0.0 | nightly (2026-08) | **M0 GO** (2026-08-17) | +| 0.1.0-dev | `283ad73` (2026-08-17) | nightly-2026-02-05 | =26.0.1 | 5.0.0 | nightly (2026-08) | **M0 GO**; attrs vendored (publishable) 2026-08-17 | ## M0 probe log (2026-08-17) — GO diff --git a/Cargo.lock b/Cargo.lock index 68bd6e5..4c0c3df 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -778,32 +778,6 @@ version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d45db016d36b838f563236e9193d0ee6ce38f3f68b6c94e914b4929c96bbb890" -[[package]] -name = "flux-attrs" -version = "0.1.0" -source = "git+https://github.com/flux-rs/flux.git?rev=283ad737569f80951973747ef16f1a89d64d9728#283ad737569f80951973747ef16f1a89d64d9728" -dependencies = [ - "flux-attrs-impl", -] - -[[package]] -name = "flux-attrs-impl" -version = "0.1.0" -source = "git+https://github.com/flux-rs/flux.git?rev=283ad737569f80951973747ef16f1a89d64d9728#283ad737569f80951973747ef16f1a89d64d9728" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.119", -] - -[[package]] -name = "flux-rs" -version = "0.1.0" -source = "git+https://github.com/flux-rs/flux.git?rev=283ad737569f80951973747ef16f1a89d64d9728#283ad737569f80951973747ef16f1a89d64d9728" -dependencies = [ - "flux-attrs", -] - [[package]] name = "fnv" version = "1.0.7" @@ -1745,10 +1719,33 @@ dependencies = [ name = "soroban-flux" version = "0.1.0" dependencies = [ - "flux-rs", + "soroban-flux-rs", "soroban-sdk 27.0.6", ] +[[package]] +name = "soroban-flux-attrs" +version = "0.1.0" +dependencies = [ + "soroban-flux-attrs-impl", +] + +[[package]] +name = "soroban-flux-attrs-impl" +version = "0.1.0" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.119", +] + +[[package]] +name = "soroban-flux-rs" +version = "0.1.0" +dependencies = [ + "soroban-flux-attrs", +] + [[package]] name = "soroban-ledger-snapshot" version = "27.0.6" diff --git a/Cargo.toml b/Cargo.toml index 8dea7db..0e3bd0a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,12 @@ [workspace] resolver = "2" -members = ["crates/soroban-flux", "crates/probe-sdk26"] +members = [ + "crates/soroban-flux", + "crates/soroban-flux-attrs-impl", + "crates/soroban-flux-attrs", + "crates/soroban-flux-rs", + "crates/probe-sdk26", +] [workspace.package] version = "0.1.0" @@ -14,12 +20,24 @@ repository = "https://github.com/nidohq/soroban-flux" # both; each consumer's lockfile picks its own single version. soroban-sdk = ">=26.0.1, <28" soroban-flux = { path = "crates/soroban-flux" } -# Flux attribute macros. Git-only (no crates.io release); the rev must match -# the installed flux toolchain — see COMPATIBILITY.md and the justfile's -# FLUX_REV. Attributes erase to no-ops unless built under the flux driver -# (cfg(flux_sysroot)), so this dep adds zero runtime cost and compiles on -# stable. -flux-rs = { git = "https://github.com/flux-rs/flux.git", rev = "283ad737569f80951973747ef16f1a89d64d9728" } +# Flux attribute macros — VENDORED from github.com/flux-rs/flux (MIT) at the +# FLUX_REV in the justfile/COMPATIBILITY.md, dependency-renamed so both the +# vendored sources and this workspace's `flux_rs::` paths stay byte-identical +# to upstream. Vendoring (rather than the upstream git dep) is what makes +# every crate here publishable to crates.io, which forbids git dependencies. +# Attributes erase to no-ops unless built under the flux driver +# (cfg(flux_sysroot)): zero runtime cost, compiles on stable. +flux-rs = { package = "soroban-flux-rs", path = "crates/soroban-flux-rs", version = "0.1.0" } + +# First-party crates opt in via `[lints] workspace = true`; the vendored +# flux crates instead cap everything to allow in their own manifests so the +# byte-identical upstream source never has to satisfy this repo's lint bar. +[workspace.lints.rust] +warnings = "deny" +unexpected_cfgs = { level = "warn", check-cfg = ["cfg(flux_sysroot)"] } + +[workspace.lints.clippy] +all = "deny" # Match consumer contract profiles (perch/nido): refinement proofs assume # overflow panics, so keep overflow-checks on in release just like the diff --git a/crates/probe-sdk26/Cargo.toml b/crates/probe-sdk26/Cargo.toml index 8d074c5..6e8847b 100644 --- a/crates/probe-sdk26/Cargo.toml +++ b/crates/probe-sdk26/Cargo.toml @@ -16,5 +16,5 @@ soroban-sdk = "26.1" [package.metadata.flux] enabled = true -[lints.rust] -unexpected_cfgs = { level = "warn", check-cfg = ["cfg(flux_sysroot)"] } +[lints] +workspace = true diff --git a/crates/soroban-flux-attrs-impl/Cargo.toml b/crates/soroban-flux-attrs-impl/Cargo.toml new file mode 100644 index 0000000..702678e --- /dev/null +++ b/crates/soroban-flux-attrs-impl/Cargo.toml @@ -0,0 +1,20 @@ +[package] +name = "soroban-flux-attrs-impl" +description = "Vendored flux-attrs-impl (github.com/flux-rs/flux, MIT) — implementation of the Flux attribute macros; source byte-identical to the upstream rev in COMPATIBILITY.md" +version.workspace = true +edition.workspace = true +license = "MIT" +repository.workspace = true + +[dependencies] +proc-macro2 = "1" +quote = "1" +syn = { version = "2.0.110", features = ["full", "extra-traits", "visit-mut"] } + +# Vendored byte-identical upstream source (see VENDORED.md): keep upstream's +# lint posture, never this workspace's. +[lints.rust] +warnings = "allow" + +[lints.clippy] +all = "allow" diff --git a/crates/soroban-flux-attrs-impl/LICENSE-UPSTREAM b/crates/soroban-flux-attrs-impl/LICENSE-UPSTREAM new file mode 100644 index 0000000..969d061 --- /dev/null +++ b/crates/soroban-flux-attrs-impl/LICENSE-UPSTREAM @@ -0,0 +1,17 @@ +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/crates/soroban-flux-attrs-impl/VENDORED.md b/crates/soroban-flux-attrs-impl/VENDORED.md new file mode 100644 index 0000000..6e13048 --- /dev/null +++ b/crates/soroban-flux-attrs-impl/VENDORED.md @@ -0,0 +1,17 @@ +# Vendored from flux-rs/flux + +`soroban-flux-attrs-impl`, `soroban-flux-attrs`, and `soroban-flux-rs` are +byte-identical copies of `lib/flux-attrs-impl`, `lib/flux-attrs`, and +`lib/flux-rs` from https://github.com/flux-rs/flux (MIT — see +LICENSE-UPSTREAM) at the rev recorded in COMPATIBILITY.md / the justfile's +FLUX_REV. Only the Cargo.toml manifests differ (package renames via cargo +dependency renaming, so `src/` never changes). + +Why vendor: crates.io forbids git dependencies, and flux publishes no +crates — vendoring is what makes soroban-flux publishable. The driver +interoperates by attribute namespace (`flux_tool::*`, registered by the +flux driver), not by crate identity, so renamed packages verify identically +(proven by this workspace's probe crate under `cargo flux`). + +To re-vendor after a FLUX_REV bump: +`git -C checkout $FLUX_REV && cp -r lib/flux-{attrs-impl,attrs,rs}/src crates/soroban-flux-*/` then re-run the full gate set. diff --git a/crates/soroban-flux-attrs-impl/build.rs b/crates/soroban-flux-attrs-impl/build.rs new file mode 100644 index 0000000..4e7fa13 --- /dev/null +++ b/crates/soroban-flux-attrs-impl/build.rs @@ -0,0 +1,6 @@ +fn main() { + println!("cargo:rerun-if-env-changed=FLUX_BUILD_SYSROOT"); + if std::env::var("FLUX_BUILD_SYSROOT").is_ok() { + println!("cargo:rustc-cfg=flux_sysroot"); + } +} diff --git a/crates/soroban-flux-attrs-impl/src/ast.rs b/crates/soroban-flux-attrs-impl/src/ast.rs new file mode 100644 index 0000000..cbc9c62 --- /dev/null +++ b/crates/soroban-flux-attrs-impl/src/ast.rs @@ -0,0 +1,2847 @@ +use std::mem; + +use proc_macro2::{TokenStream, TokenTree}; +use quote::{ToTokens, TokenStreamExt, quote, quote_spanned}; +use syn::{ + Attribute, Ident, Result, Token, Visibility, braced, bracketed, + ext::IdentExt, + parenthesized, + parse::{Parse, ParseStream, Peek, discouraged::Speculative}, + punctuated::Punctuated, + token::{self, Mut, Paren}, +}; + +use crate::{flux_tool_attrs, parse_inner, tokens_or_default}; + +pub struct Items(Vec); + +#[derive(Debug)] +pub enum Item { + Const(syn::ItemConst), + Struct(ItemStruct), + Enum(ItemEnum), + Use(syn::ItemUse), + Type(ItemType), + Fn(ItemFn), + Impl(ItemImpl), + Mod(ItemMod), + Trait(ItemTrait), +} + +#[derive(Debug)] +pub struct ItemMod { + pub attrs: Vec, + pub vis: Visibility, + pub unsafety: Option, + pub mod_token: Token![mod], + pub ident: Ident, + pub content: Option<(token::Brace, Vec)>, + pub semi: Option, +} + +#[derive(Debug)] +pub struct ItemTrait { + pub attrs: Vec, + pub vis: Visibility, + pub unsafety: Option, + pub trait_token: Token![trait], + pub ident: Ident, + pub generics: Generics, + pub colon_token: Option, + pub supertraits: Punctuated, + pub brace_token: token::Brace, + pub items: Vec, +} + +impl Parse for ItemTrait { + fn parse(input: ParseStream) -> Result { + let mut attrs = input.call(Attribute::parse_outer)?; + let vis: Visibility = input.parse()?; + let unsafety: Option = input.parse()?; + let trait_token: Token![trait] = input.parse()?; + let ident: Ident = input.parse()?; + let mut generics: Generics = input.parse()?; + + let colon_token: Option = input.parse()?; + + let mut supertraits = Punctuated::new(); + if colon_token.is_some() { + loop { + if input.peek(Token![where]) || input.peek(token::Brace) { + break; + } + supertraits.push_value(input.parse()?); + if input.peek(Token![where]) || input.peek(token::Brace) { + break; + } + supertraits.push_punct(input.parse()?); + } + } + + generics.where_clause = input.parse()?; + + let content; + let brace_token = braced!(content in input); + parse_inner(&content, &mut attrs)?; + let mut items = Vec::new(); + while !content.is_empty() { + items.push(content.parse()?); + } + + Ok(ItemTrait { + attrs, + vis, + unsafety, + trait_token, + ident, + generics, + colon_token, + supertraits, + brace_token, + items, + }) + } +} + +impl ToTokens for ItemTrait { + fn to_tokens(&self, tokens: &mut TokenStream) { + tokens.append_all(outer(&self.attrs)); + #[cfg(flux_sysroot)] + for item in &self.items { + if let TraitItem::Reft(reft) = item { + reft.flux_tool_attr().to_tokens(tokens); + } + } + self.vis.to_tokens(tokens); + self.unsafety.to_tokens(tokens); + self.trait_token.to_tokens(tokens); + self.ident.to_tokens(tokens); + self.generics.to_tokens(tokens, Mode::Rust); + if !self.supertraits.is_empty() { + tokens_or_default(self.colon_token.as_ref(), tokens); + self.supertraits.to_tokens(tokens); + } + self.generics.where_clause.to_tokens(tokens); + self.brace_token.surround(tokens, |tokens| { + tokens.append_all(inner(&self.attrs)); + tokens.append_all(&self.items); + }); + } +} + +#[derive(Debug)] +pub enum TraitItem { + /// An associated constant within the definition of a trait. + Const(syn::TraitItemConst), + + /// An associated function within the definition of a trait. + Fn(TraitItemFn), + + /// An associated type within the definition of a trait. + Type(syn::TraitItemType), + + /// An associated refinements within the definition of a trait. + Reft(TraitItemReft), +} + +impl Parse for TraitItem { + fn parse(input: ParseStream) -> Result { + let mut attrs = input.call(Attribute::parse_outer)?; + flux_tool_attrs(&mut attrs); + let vis: Visibility = input.parse()?; + let ahead = input.fork(); + + let lookahead = ahead.lookahead1(); + let mut item = if lookahead.peek(Token![fn]) || peek_signature(&ahead) { + input.parse().map(TraitItem::Fn) + } else if lookahead.peek(Token![const]) { + let const_token: Token![const] = ahead.parse()?; + let lookahead = ahead.lookahead1(); + if lookahead.peek(Ident) || lookahead.peek(Token![_]) { + input.advance_to(&ahead); + let ident = input.call(Ident::parse_any)?; + let colon_token: Token![:] = input.parse()?; + let ty: syn::Type = input.parse()?; + let default = if let Some(eq_token) = input.parse::>()? { + let expr: syn::Expr = input.parse()?; + Some((eq_token, expr)) + } else { + None + }; + let semi_token: Token![;] = input.parse()?; + Ok(TraitItem::Const(syn::TraitItemConst { + attrs: Vec::new(), + const_token, + ident, + generics: syn::Generics::default(), + colon_token, + ty, + default, + semi_token, + })) + } else if lookahead.peek(Token![async]) + || lookahead.peek(Token![unsafe]) + || lookahead.peek(Token![extern]) + || lookahead.peek(Token![fn]) + { + input.parse().map(TraitItem::Fn) + } else { + Err(lookahead.error()) + } + } else if lookahead.peek(Token![type]) { + parse_trait_item_type(input) + } else if lookahead.peek(kw::reft) { + input.parse().map(TraitItem::Reft) + } else { + Err(lookahead.error()) + }?; + + if !matches!(vis, Visibility::Inherited) { + return Err(syn::Error::new_spanned(vis, "visibility qualifier not allowed here")); + } + + let item_attrs = match &mut item { + TraitItem::Const(item) => &mut item.attrs, + TraitItem::Fn(item) => &mut item.attrs, + TraitItem::Type(item) => &mut item.attrs, + TraitItem::Reft(item) => &mut item.attrs, + }; + attrs.append(item_attrs); + *item_attrs = attrs; + Ok(item) + } +} + +impl ToTokens for TraitItem { + fn to_tokens(&self, tokens: &mut TokenStream) { + match self { + TraitItem::Const(item) => item.to_tokens(tokens), + TraitItem::Fn(item) => item.to_tokens(tokens), + TraitItem::Type(item) => item.to_tokens(tokens), + TraitItem::Reft(_) => {} + } + } +} + +#[derive(Debug)] +pub struct TraitItemFn { + pub attrs: Vec, + pub sig: Signature, + pub default: Option, + pub semi_token: Option, +} + +impl Parse for TraitItemFn { + fn parse(input: ParseStream) -> Result { + let attrs = input.call(Attribute::parse_outer)?; + let sig: Signature = input.parse()?; + + let lookahead = input.lookahead1(); + let (block, semi_token) = if lookahead.peek(token::Brace) { + let block = input.parse()?; + (Some(block), None) + } else if lookahead.peek(Token![;]) { + let semi_token: Token![;] = input.parse()?; + (None, Some(semi_token)) + } else { + return Err(lookahead.error()); + }; + + Ok(TraitItemFn { attrs, sig, default: block, semi_token }) + } +} + +impl ToTokens for TraitItemFn { + fn to_tokens(&self, tokens: &mut TokenStream) { + let TraitItemFn { attrs, sig, default, semi_token } = self; + #[cfg(flux_sysroot)] + { + let flux_sig = ToTokensFlux(sig); + quote!(#[flux_tool::sig(#flux_sig)]).to_tokens(tokens); + } + let rust_sig = ToTokensRust(sig); + quote! { + #(#attrs)* + #rust_sig #default #semi_token + } + .to_tokens(tokens); + } +} + +#[derive(Debug)] +#[cfg_attr(not(flux_sysroot), allow(dead_code))] +pub struct TraitItemReft { + /// This is not actually used + pub attrs: Vec, + pub reft_token: kw::reft, + pub name: Ident, + pub paren_token: token::Paren, + pub params: TokenStream, + pub returns: TokenStream, + #[allow(dead_code)] + pub semi_token: Token![;], +} + +impl TraitItemReft { + #[cfg(flux_sysroot)] + fn flux_tool_attr(&self) -> TokenStream { + quote! { + #[flux_tool::assoc(#self)] + } + } +} + +impl Parse for TraitItemReft { + fn parse(input: ParseStream) -> Result { + let reft_token: kw::reft = input.parse()?; + let name: Ident = input.parse()?; + let content; + let paren_token = parenthesized!(content in input); + let params = content.parse()?; + let mut returns = TokenStream::new(); + while !input.peek(Token![;]) { + returns.append(TokenTree::parse(input)?); + } + let semi_token: Token![;] = input.parse()?; + Ok(TraitItemReft { + attrs: vec![], + reft_token, + name, + paren_token, + params, + returns, + semi_token, + }) + } +} + +#[cfg(flux_sysroot)] +impl ToTokens for TraitItemReft { + fn to_tokens(&self, tokens: &mut TokenStream) { + let TraitItemReft { reft_token, name, paren_token, params, returns, .. } = self; + quote_spanned!(reft_token.span=> fn).to_tokens(tokens); + name.to_tokens(tokens); + paren_token.surround(tokens, |tokens| { + params.to_tokens(tokens); + }); + returns.to_tokens(tokens); + } +} + +#[derive(Debug)] +pub struct ItemFn { + pub attrs: Vec, + pub vis: Visibility, + pub sig: Signature, + pub block: Block, +} + +#[derive(Debug)] +pub struct Generics { + pub lt_token: Option, + pub params: Punctuated, + pub gt_token: Option]>, + pub where_clause: Option, +} + +impl Default for Generics { + fn default() -> Self { + Generics { lt_token: None, params: Punctuated::new(), gt_token: None, where_clause: None } + } +} + +#[derive(Debug)] +pub enum GenericParam { + /// A lifetime parameter: `'a: 'b + 'c + 'd`. + Lifetime(syn::LifetimeParam), + + /// A generic type parameter: `T: Into`. + Type(TypeParam), + + /// A const generic parameter: `const LENGTH: usize`. + Const(syn::ConstParam), +} + +#[derive(Debug)] +pub struct TypeParam { + pub attrs: Vec, + pub ident: Ident, + pub as_token: Option, + pub param_kind: ParamKind, + pub colon_token: Option, + pub bounds: Punctuated, + // pub eq_token: Option, + // pub default: Option, +} + +#[derive(Debug)] +pub enum ParamKind { + Type(Token![type]), + Base(kw::base), + Default, +} + +impl ToTokens for ParamKind { + fn to_tokens(&self, tokens: &mut TokenStream) { + match self { + ParamKind::Type(t) => t.to_tokens(tokens), + ParamKind::Base(t) => t.to_tokens(tokens), + ParamKind::Default => {} + } + } +} + +#[derive(Debug)] +pub struct ItemStruct { + pub attrs: Vec, + pub vis: Visibility, + pub struct_token: Token![struct], + pub ident: Ident, + pub generics: Generics, + #[cfg_attr(not(flux_sysroot), allow(dead_code))] + pub refined_by: Option, + pub fields: Fields, + pub semi_token: Option, +} + +#[derive(Debug)] +pub struct ItemEnum { + pub attrs: Vec, + pub vis: Visibility, + pub enum_token: Token![enum], + pub ident: Ident, + pub generics: Generics, + #[cfg_attr(not(flux_sysroot), allow(dead_code))] + pub refined_by: Option, + pub brace_token: token::Brace, + pub variants: Punctuated, +} + +#[derive(Debug)] +pub struct Variant { + pub attrs: Vec, + + /// Name of the variant. + pub ident: Ident, + + /// Content stored in the variant. + pub fields: Fields, + + /// Explicit discriminant: `Variant = 1` + pub discriminant: Option<(Token![=], syn::Expr)>, + + #[cfg_attr(not(flux_sysroot), allow(dead_code))] + pub ret: Option, +} + +impl Variant { + #[cfg(flux_sysroot)] + fn flux_tool_attr(&self) -> TokenStream { + let variant = ToTokensFlux(self); + quote! { + #[flux_tool::variant(#variant)] + } + } +} + +#[cfg(flux_sysroot)] +impl ToTokens for ToTokensFlux<&Variant> { + fn to_tokens(&self, tokens: &mut TokenStream) { + let variant = &self.0; + variant + .fields + .to_tokens(tokens, |f, tokens| f.ty.to_tokens_inner(tokens, Mode::Flux)); + if let Some(ret) = &variant.ret { + if !matches!(variant.fields, Fields::Unit) { + ret.arrow_token.to_tokens(tokens); + } + ret.path.to_tokens_inner(tokens, Mode::Flux); + ret.bracket_token.surround(tokens, |tokens| { + ret.indices.to_tokens(tokens); + }); + } + } +} + +#[cfg_attr(not(flux_sysroot), allow(dead_code))] +#[derive(Debug)] +pub struct VariantRet { + pub arrow_token: Option]>, + pub path: Path, + pub bracket_token: token::Bracket, + pub indices: TokenStream, +} + +#[derive(Debug)] +pub struct RefinedBy { + pub _refined_by: Option<(kw::refined, kw::by)>, + pub _bracket_token: token::Bracket, + pub params: Punctuated, +} + +impl RefinedBy { + #[cfg(flux_sysroot)] + fn flux_tool_attr(&self) -> TokenStream { + quote! { + #[flux_tool::refined_by(#self)] + } + } +} + +#[derive(Debug)] +pub struct RefinedByParam { + pub ident: Ident, + pub colon_token: Token![:], + pub sort: Sort, +} + +#[derive(Debug)] +pub enum Fields { + /// Named fields of a struct or struct variant such as `Point { x: f64, + /// y: f64 }`. + Named(FieldsNamed), + + /// Unnamed fields of a tuple struct or tuple variant such as `Some(T)`. + Unnamed(FieldsUnnamed), + + /// Unit struct or unit variant such as `None`. + Unit, +} + +impl Fields { + fn to_tokens(&self, tokens: &mut TokenStream, mut f: impl FnMut(&Field, &mut TokenStream)) { + match self { + Fields::Named(fields) => { + fields.brace_token.surround(tokens, |tokens| { + for param in fields.named.pairs() { + f(param.value(), tokens); + param.punct().to_tokens(tokens); + } + }); + } + Fields::Unnamed(fields) => { + fields.paren_token.surround(tokens, |tokens| { + for param in fields.unnamed.pairs() { + f(param.value(), tokens); + param.punct().to_tokens(tokens); + } + }); + } + Fields::Unit => {} + } + } +} + +#[derive(Debug)] +pub struct FieldsNamed { + pub brace_token: token::Brace, + pub named: Punctuated, +} + +#[derive(Debug)] +pub struct FieldsUnnamed { + pub paren_token: token::Paren, + pub unnamed: Punctuated, +} + +#[derive(Debug)] +pub struct Field { + pub attrs: Vec, + + pub vis: Visibility, + + pub _mutability: syn::FieldMutability, + + /// Name of the field, if any. + /// + /// Fields of tuple structs have no names. + pub ident: Option, + + pub colon_token: Option, + + pub ty: Type, +} + +impl Field { + fn parse_unnamed(input: ParseStream) -> Result { + Ok(Field { + attrs: input.call(Attribute::parse_outer)?, + vis: input.parse()?, + _mutability: syn::FieldMutability::None, + ident: None, + colon_token: None, + ty: input.parse()?, + }) + } + + fn parse_named(input: ParseStream) -> Result { + let attrs = input.call(Attribute::parse_outer)?; + let vis: Visibility = input.parse()?; + + let ident = input.parse()?; + let colon_token: Token![:] = input.parse()?; + let ty = input.parse()?; + Ok(Field { + attrs, + vis, + _mutability: syn::FieldMutability::None, + ident: Some(ident), + colon_token: Some(colon_token), + ty, + }) + } + + #[cfg(flux_sysroot)] + fn flux_tool_attr(&self) -> TokenStream { + let flux_ty = ToTokensFlux(&self.ty); + quote! { + #[flux_tool::field(#flux_ty)] + } + } + + fn to_tokens(&self, tokens: &mut TokenStream) { + tokens.append_all(&self.attrs); + self.vis.to_tokens(tokens); + self.ident.to_tokens(tokens); + self.colon_token.to_tokens(tokens); + self.ty.to_tokens_inner(tokens, Mode::Rust); + } +} + +#[derive(Debug)] +pub struct ItemType { + pub attrs: Vec, + pub vis: Visibility, + pub type_token: Token![type], + pub ident: Ident, + pub generics: Generics, + pub index_params: Option, + pub eq_token: Token![=], + pub ty: Box, + pub semi_token: Token![;], +} + +#[derive(Debug)] +pub struct IndexParams { + pub bracket_token: token::Bracket, + pub params: Punctuated, +} + +#[derive(Debug)] +pub struct ItemImpl { + pub attrs: Vec, + pub impl_token: Token![impl], + pub generics: Generics, + pub trait_: Option<(syn::Path, Token![for])>, + /// The Self type of the impl. + pub self_ty: Box, + pub brace_token: token::Brace, + pub items: Vec, +} + +#[derive(Debug)] +pub enum ImplItem { + Fn(ImplItemFn), + Type(syn::ImplItemType), + Reft(ImplItemReft), +} + +#[derive(Debug)] +pub struct ImplItemFn { + pub attrs: Vec, + pub vis: Visibility, + pub sig: Signature, + pub block: Block, +} + +impl Parse for ImplItemFn { + fn parse(input: ParseStream) -> Result { + Ok(ImplItemFn { + attrs: input.call(Attribute::parse_outer)?, + vis: input.parse()?, + sig: input.parse()?, + block: input.parse()?, + }) + } +} + +#[derive(Debug)] +#[cfg_attr(not(flux_sysroot), allow(dead_code))] +pub struct ImplItemReft { + /// This is not actually used + pub attrs: Vec, + pub reft_token: kw::reft, + pub name: Ident, + pub paren_token: token::Paren, + pub params: TokenStream, + pub returns: TokenStream, + pub block: Block, +} + +impl ImplItemReft { + #[cfg(flux_sysroot)] + fn flux_tool_attr(&self) -> TokenStream { + quote! { + #[flux_tool::assoc(#self)] + } + } +} + +impl Parse for ImplItemReft { + fn parse(input: ParseStream) -> Result { + let reft_token: kw::reft = input.parse()?; + let name: Ident = input.parse()?; + let content; + let paren_token = parenthesized!(content in input); + let params = content.parse()?; + let mut returns = TokenStream::new(); + while !input.peek(token::Brace) { + returns.append(TokenTree::parse(input)?); + } + let block: Block = input.parse()?; + Ok(ImplItemReft { attrs: vec![], reft_token, name, paren_token, params, returns, block }) + } +} + +#[cfg(flux_sysroot)] +impl ToTokens for ImplItemReft { + fn to_tokens(&self, tokens: &mut TokenStream) { + let ImplItemReft { reft_token, name, paren_token, params, returns, block, .. } = self; + quote_spanned!(reft_token.span=> fn).to_tokens(tokens); + name.to_tokens(tokens); + paren_token.surround(tokens, |tokens| { + params.to_tokens(tokens); + }); + returns.to_tokens(tokens); + block.to_tokens(tokens); + } +} + +#[derive(Debug)] +pub struct Signature { + pub fn_token: Token![fn], + pub ident: Ident, + pub generics: Generics, + pub paren_token: Paren, + pub inputs: Punctuated, + pub output: ReturnType, + pub requires: Option, + pub ensures: Option, +} + +#[derive(Debug)] +pub struct Ensures { + pub ensures_token: kw::ensures, + pub constraints: Punctuated, +} + +#[derive(Debug)] +pub struct Requires { + pub requires_token: kw::requires, + pub constraint: Expr, +} + +#[derive(Debug)] +pub enum Constraint { + Type { ident: Ident, colon_token: Token![:], ty: Box }, + Expr(Expr), +} + +#[derive(Debug)] +pub enum FnArg { + StrgRef(StrgRef), + Typed(PatType), +} + +#[derive(Debug)] +pub struct PatType { + pub pat: Pat, + pub colon_token: Token![:], + pub ty: Type, + pub pred: Option, +} + +#[derive(Debug)] +pub enum Pat { + Ident(PatIdent), + Wild(Token![_]), +} + +#[derive(Debug)] +pub struct PatIdent { + pub mutability: Option, + pub ident: Ident, +} + +#[derive(Debug)] +pub struct PatTypePredicate { + pub brace_token: token::Brace, + pub pred: Expr, +} + +#[derive(Debug)] +pub struct StrgRef { + pub pat: Pat, + pub colon_token: Token![:], + pub and_token: Token![&], + pub strg_token: kw::strg, + pub ty: Box, +} + +#[derive(Debug)] +pub enum Sort { + BaseSort(BaseSort), + Func { input: FuncSortInput, arrow: Token![->], output: BaseSort }, +} + +#[derive(Debug)] +pub enum FuncSortInput { + Parenthesized { paren_token: token::Paren, inputs: Punctuated }, + Single(BaseSort), +} + +#[derive(Debug)] +pub enum BaseSort { + BitVec(BitVecSort), + App(Ident, SortArguments), +} + +#[derive(Debug)] +pub struct BitVecSort { + pub bitvec_token: kw::bitvec, + pub lt_token: Token![<], + pub lit: syn::LitInt, + pub gt_token: Token![>], +} + +#[derive(Debug)] +pub enum SortArguments { + None, + AngleBracketed(AngleBracketedSortArgs), +} + +#[derive(Debug)] +pub struct AngleBracketedSortArgs { + pub lt_token: Token![<], + pub args: Punctuated, + pub gt_token: Token![>], +} + +#[derive(Debug)] +pub enum Type { + Base(BaseType), + Indexed(TypeIndexed), + Exists(TypeExists), + GeneralExists(TypeGeneralExists), + Reference(TypeReference), + Constraint(TypeConstraint), + Array(TypeArray), + Tuple(TypeTuple), + Ptr(syn::TypePtr), +} + +#[derive(Debug)] +pub struct TypeTuple { + pub paren_token: token::Paren, + pub elems: Punctuated, +} + +impl TypeTuple { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + self.paren_token.surround(tokens, |tokens| { + for elem in self.elems.pairs() { + elem.value().to_tokens_inner(tokens, mode); + elem.punct().to_tokens(tokens); + } + }); + } +} + +#[derive(Debug)] +pub struct TypeIndexed { + pub bty: BaseType, + pub bracket_token: token::Bracket, + pub expr: Expr, +} + +#[derive(Debug)] +pub struct TypeExists { + pub bty: BaseType, + pub brace_token: token::Brace, + pub ident: Ident, + pub colon_token: Token![:], + pub expr: Expr, +} + +#[derive(Debug)] +pub struct TypeGeneralExists { + pub brace_token: token::Brace, + pub params: Punctuated, + pub dot_token: Token![.], + pub ty: Box, + pub or_token: Option, + pub pred: Option, +} + +#[derive(Debug)] +pub struct ExistsParam { + pub ident: Ident, + pub colon_token: Option, + pub sort: Option, +} + +#[derive(Debug)] +pub struct TypeReference { + pub and_token: Token![&], + pub lifetime: Option, + pub mutability: Option, + pub elem: Box, +} + +#[derive(Debug)] +pub struct TypeConstraint { + pub brace_token: token::Brace, + pub ty: Box, + pub or_token: Token![|], + pub pred: Expr, +} + +#[derive(Debug)] +pub struct TypeArray { + pub bracket_token: token::Bracket, + pub ty: Box, + pub semi_token: Token![;], + pub len: TokenStream, +} + +#[derive(Debug)] +pub enum BaseType { + Path(Path), + Slice(TypeSlice), +} + +#[derive(Debug)] +pub struct Path { + pub segments: Punctuated, +} + +#[derive(Debug)] +pub struct TypeSlice { + pub bracket_token: token::Bracket, + pub ty: Box, +} + +#[derive(Debug)] +pub struct PathSegment { + pub ident: Ident, + pub arguments: PathArguments, +} + +#[derive(Debug)] +pub enum PathArguments { + None, + AngleBracketed(AngleBracketedGenericArguments), +} + +#[derive(Debug)] +pub struct AngleBracketedGenericArguments { + pub lt_token: Token![<], + pub args: Punctuated, + pub gt_token: Token![>], +} + +#[derive(Debug)] +pub enum GenericArgument { + Type(Type), +} + +#[derive(Debug)] +pub enum ReturnType { + Default, + Type(Token![->], Box), +} + +pub type Expr = TokenStream; + +#[derive(Debug)] +pub struct Block { + pub brace_token: token::Brace, + pub stmts: TokenStream, +} + +impl Parse for Items { + fn parse(input: ParseStream) -> Result { + let mut result = Vec::new(); + while !input.is_empty() { + let value = input.parse()?; + result.push(value); + } + Ok(Self(result)) + } +} + +impl Parse for Item { + fn parse(input: ParseStream) -> Result { + let mut attrs = input.call(Attribute::parse_outer)?; + flux_tool_attrs(&mut attrs); + let ahead = input.fork(); + let _: Visibility = ahead.parse()?; + let lookahead = ahead.lookahead1(); + let mut item = if lookahead.peek(Token![fn]) { + Item::Fn(input.parse()?) + } else if lookahead.peek(Token![impl]) { + Item::Impl(input.parse()?) + } else if lookahead.peek(Token![mod]) { + Item::Mod(input.parse()?) + } else if lookahead.peek(Token![struct]) { + Item::Struct(input.parse()?) + } else if lookahead.peek(Token![enum]) { + Item::Enum(input.parse()?) + } else if lookahead.peek(Token![use]) { + Item::Use(input.parse()?) + } else if lookahead.peek(Token![type]) { + Item::Type(input.parse()?) + } else if lookahead.peek(Token![trait]) { + Item::Trait(input.parse()?) + } else if lookahead.peek(Token![const]) { + Item::Const(input.parse()?) + } else { + return Err(lookahead.error()); + }; + + item.replace_attrs(attrs); + Ok(item) + } +} + +impl Parse for ItemMod { + fn parse(input: ParseStream) -> Result { + let mut attrs = input.call(Attribute::parse_outer)?; + let vis: Visibility = input.parse()?; + let unsafety: Option = input.parse()?; + let mod_token: Token![mod] = input.parse()?; + let ident: Ident = + if input.peek(Token![try]) { input.call(Ident::parse_any) } else { input.parse() }?; + + let lookahead = input.lookahead1(); + if lookahead.peek(Token![;]) { + Ok(ItemMod { + attrs, + vis, + unsafety, + mod_token, + ident, + content: None, + semi: Some(input.parse()?), + }) + } else if lookahead.peek(token::Brace) { + let content; + let brace_token = braced!(content in input); + parse_inner(&content, &mut attrs)?; + + let mut items = Vec::new(); + while !content.is_empty() { + items.push(content.parse()?); + } + + Ok(ItemMod { + attrs, + vis, + unsafety, + mod_token, + ident, + content: Some((brace_token, items)), + semi: None, + }) + } else { + Err(lookahead.error()) + } + } +} + +impl Parse for ItemStruct { + fn parse(input: ParseStream) -> Result { + let mut attrs = input.call(Attribute::parse_outer)?; + flux_tool_attrs(&mut attrs); + let vis = input.parse::()?; + let struct_token = input.parse::()?; + let ident = input.parse::()?; + let generics = input.parse::()?; + let refined_by = parse_opt_refined_by(input)?; + let (where_clause, fields, semi_token) = data_struct(input)?; + Ok(ItemStruct { + attrs, + vis, + struct_token, + ident, + generics: Generics { where_clause, ..generics }, + refined_by, + fields, + semi_token, + }) + } +} + +impl Parse for Generics { + fn parse(input: ParseStream) -> Result { + if !input.peek(Token![<]) { + return Ok(Generics::default()); + } + + let lt_token: Token![<] = input.parse()?; + + let mut params = Punctuated::new(); + loop { + if input.peek(Token![>]) { + break; + } + + let attrs = input.call(Attribute::parse_outer)?; + let lookahead = input.lookahead1(); + if lookahead.peek(syn::Lifetime) { + params.push_value(GenericParam::Lifetime(syn::LifetimeParam { + attrs, + ..input.parse()? + })); + } else if lookahead.peek(Ident) { + params.push_value(GenericParam::Type(TypeParam { attrs, ..input.parse()? })); + } else if lookahead.peek(Token![const]) { + params.push_value(GenericParam::Const(syn::ConstParam { attrs, ..input.parse()? })); + } else if input.peek(Token![_]) { + params.push_value(GenericParam::Type(TypeParam { + attrs, + ident: input.call(Ident::parse_any)?, + as_token: None, + param_kind: ParamKind::Default, + colon_token: None, + bounds: Punctuated::new(), + // eq_token: None, + // default: None, + })); + } else { + return Err(lookahead.error()); + } + + if input.peek(Token![>]) { + break; + } + let punct = input.parse()?; + params.push_punct(punct); + } + + let gt_token: Token![>] = input.parse()?; + + Ok(Generics { + lt_token: Some(lt_token), + params, + gt_token: Some(gt_token), + where_clause: None, + }) + } +} + +fn opt_parse_where_clause_in_signature(input: ParseStream) -> Result> { + if input.peek(Token![where]) { + parse_where_clause_in_signature(input).map(Some) + } else { + Ok(None) + } +} + +fn parse_where_clause_in_signature(input: ParseStream) -> Result { + Ok(syn::WhereClause { + where_token: input.parse()?, + predicates: { + let mut predicates = Punctuated::new(); + loop { + if input.is_empty() + || input.peek(token::Brace) + || input.peek(Token![,]) + || input.peek(Token![;]) + || input.peek(Token![:]) && !input.peek(Token![::]) + || input.peek(Token![=]) + || input.peek(kw::requires) + || input.peek(kw::ensures) + { + break; + } + let value = input.parse()?; + predicates.push_value(value); + if !input.peek(Token![,]) { + break; + } + let punct = input.parse()?; + predicates.push_punct(punct); + } + predicates + }, + }) +} + +impl Parse for GenericParam { + fn parse(input: ParseStream) -> Result { + let attrs = input.call(Attribute::parse_outer)?; + + let lookahead = input.lookahead1(); + if lookahead.peek(Ident) { + Ok(GenericParam::Type(TypeParam { attrs, ..input.parse()? })) + } else if lookahead.peek(syn::Lifetime) { + Ok(GenericParam::Lifetime(syn::LifetimeParam { attrs, ..input.parse()? })) + } else if lookahead.peek(Token![const]) { + Ok(GenericParam::Const(syn::ConstParam { attrs, ..input.parse()? })) + } else { + Err(lookahead.error()) + } + } +} + +impl Parse for TypeParam { + fn parse(input: ParseStream) -> Result { + let attrs = input.call(Attribute::parse_outer)?; + let ident: Ident = input.parse()?; + + let as_token: Option = input.parse()?; + let mut param_kind = ParamKind::Default; + if as_token.is_some() { + param_kind = input.parse()?; + } + + let colon_token: Option = input.parse()?; + + let mut bounds = Punctuated::new(); + if colon_token.is_some() { + loop { + if input.peek(Token![,]) || input.peek(Token![>]) || input.peek(Token![=]) { + break; + } + let value: syn::TypeParamBound = input.parse()?; + bounds.push_value(value); + if !input.peek(Token![+]) { + break; + } + let punct: Token![+] = input.parse()?; + bounds.push_punct(punct); + } + } + // let eq_token: Option = input.parse()?; + // let default = if eq_token.is_some() { Some(input.parse::()?) } else { None }; + + Ok(TypeParam { + attrs, + ident, + as_token, + param_kind, + colon_token, + bounds, + // eq_token, + // default, + }) + } +} + +impl Parse for ParamKind { + fn parse(input: ParseStream) -> Result { + let lookahead = input.lookahead1(); + if lookahead.peek(Token![type]) { + input.parse().map(ParamKind::Type) + } else if lookahead.peek(kw::base) { + input.parse().map(ParamKind::Base) + } else { + Err(lookahead.error()) + } + } +} + +impl Parse for ItemEnum { + fn parse(input: ParseStream) -> Result { + let mut attrs = input.call(Attribute::parse_outer)?; + flux_tool_attrs(&mut attrs); + let vis = input.parse::()?; + let enum_token = input.parse::()?; + let ident = input.parse::()?; + let generics = input.parse::()?; + let refined_by = parse_opt_refined_by(input)?; + let (where_clause, brace_token, variants) = data_enum(input)?; + Ok(ItemEnum { + attrs, + vis, + enum_token, + ident, + generics: Generics { where_clause, ..generics }, + refined_by, + brace_token, + variants, + }) + } +} + +fn parse_opt_refined_by(input: ParseStream) -> Result> { + if input.peek(kw::refined) || input.peek(token::Bracket) { + input.parse().map(Some) + } else { + Ok(None) + } +} + +impl Parse for RefinedBy { + fn parse(input: ParseStream) -> Result { + let refined_by = + if input.peek(kw::refined) { Some((input.parse()?, input.parse()?)) } else { None }; + let content; + Ok(RefinedBy { + _refined_by: refined_by, + _bracket_token: bracketed!(content in input), + params: Punctuated::parse_terminated(&content)?, + }) + } +} + +impl Parse for RefinedByParam { + fn parse(input: ParseStream) -> Result { + Ok(RefinedByParam { + ident: input.parse()?, + colon_token: input.parse()?, + sort: input.parse()?, + }) + } +} + +impl Parse for Sort { + fn parse(input: ParseStream) -> Result { + if input.peek(token::Paren) { + let content; + let input_sort = FuncSortInput::Parenthesized { + paren_token: parenthesized!(content in input), + inputs: content.parse_terminated(BaseSort::parse, Token![,])?, + }; + Ok(Sort::Func { input: input_sort, arrow: input.parse()?, output: input.parse()? }) + } else { + let sort: BaseSort = input.parse()?; + if input.peek(Token![->]) { + Ok(Sort::Func { + input: FuncSortInput::Single(sort), + arrow: input.parse()?, + output: input.parse()?, + }) + } else { + Ok(Sort::BaseSort(sort)) + } + } + } +} + +impl Parse for BaseSort { + fn parse(input: ParseStream) -> Result { + if input.peek(kw::bitvec) { + Ok(BaseSort::BitVec(BitVecSort { + bitvec_token: input.parse()?, + lt_token: input.parse()?, + lit: input.parse()?, + gt_token: input.parse()?, + })) + } else { + let ident = input.parse()?; + let arguments = if input.peek(Token![<]) && !input.peek(Token![<=]) { + SortArguments::AngleBracketed(input.parse()?) + } else { + SortArguments::None + }; + Ok(BaseSort::App(ident, arguments)) + } + } +} + +impl Parse for AngleBracketedSortArgs { + fn parse(input: ParseStream) -> Result { + Ok(AngleBracketedSortArgs { + lt_token: input.parse()?, + args: parse_until(input, BaseSort::parse, Token![,], Token![>])?, + gt_token: input.parse()?, + }) + } +} + +fn data_enum( + input: ParseStream, +) -> Result<(Option, token::Brace, Punctuated)> { + let where_clause = input.parse()?; + + let content; + let brace = braced!(content in input); + let variants = content.parse_terminated(Variant::parse, Token![,])?; + + Ok((where_clause, brace, variants)) +} + +impl Parse for Variant { + fn parse(input: ParseStream) -> Result { + let attrs = input.call(Attribute::parse_outer)?; + let _visibility: Visibility = input.parse()?; + let ident: Ident = input.parse()?; + let fields = if input.peek(token::Brace) { + Fields::Named(input.parse()?) + } else if input.peek(token::Paren) { + Fields::Unnamed(input.parse()?) + } else { + Fields::Unit + }; + let discriminant = if input.peek(Token![=]) { + let eq_token: Token![=] = input.parse()?; + let discriminant: syn::Expr = input.parse()?; + Some((eq_token, discriminant)) + } else { + None + }; + let ret = parse_opt_variant_ret(input)?; + Ok(Variant { attrs, ident, fields, discriminant, ret }) + } +} + +fn parse_opt_variant_ret(input: ParseStream) -> Result> { + if input.peek(Token![->]) { input.parse().map(Some) } else { Ok(None) } +} + +impl Parse for VariantRet { + fn parse(input: ParseStream) -> Result { + let mut indices = TokenStream::new(); + let content; + Ok(VariantRet { + arrow_token: input.parse()?, + path: input.parse()?, + bracket_token: bracketed!(content in input), + indices: { + loop { + if content.is_empty() { + break; + } + let tt: TokenTree = content.parse()?; + indices.append(tt); + } + indices + }, + }) + } +} + +fn data_struct( + input: ParseStream, +) -> Result<(Option, Fields, Option)> { + let mut lookahead = input.lookahead1(); + let mut where_clause = None; + if lookahead.peek(Token![where]) { + where_clause = Some(input.parse()?); + lookahead = input.lookahead1(); + } + + if where_clause.is_none() && lookahead.peek(token::Paren) { + let fields = input.parse()?; + + lookahead = input.lookahead1(); + if lookahead.peek(Token![where]) { + where_clause = Some(input.parse()?); + lookahead = input.lookahead1(); + } + + if lookahead.peek(Token![;]) { + let semi = input.parse()?; + Ok((where_clause, Fields::Unnamed(fields), Some(semi))) + } else { + Err(lookahead.error()) + } + } else if lookahead.peek(token::Brace) { + let fields = input.parse()?; + Ok((where_clause, Fields::Named(fields), None)) + } else if lookahead.peek(Token![;]) { + let semi = input.parse()?; + Ok((where_clause, Fields::Unit, Some(semi))) + } else { + Err(lookahead.error()) + } +} + +impl Parse for FieldsUnnamed { + fn parse(input: ParseStream) -> Result { + let content; + Ok(FieldsUnnamed { + paren_token: parenthesized!(content in input), + unnamed: content.parse_terminated(Field::parse_unnamed, Token![,])?, + }) + } +} + +impl Parse for FieldsNamed { + fn parse(input: ParseStream) -> Result { + let content; + Ok(FieldsNamed { + brace_token: braced!(content in input), + named: content.parse_terminated(Field::parse_named, Token![,])?, + }) + } +} + +impl Parse for ItemFn { + fn parse(input: ParseStream) -> Result { + Ok(ItemFn { + attrs: input.call(Attribute::parse_outer)?, + vis: input.parse()?, + sig: input.parse()?, + block: input.parse()?, + }) + } +} + +impl Parse for ItemType { + fn parse(input: ParseStream) -> Result { + Ok(ItemType { + attrs: input.call(Attribute::parse_outer)?, + vis: input.parse()?, + type_token: input.parse()?, + ident: input.parse()?, + generics: input.parse()?, + index_params: parse_index_params(input)?, + eq_token: input.parse()?, + ty: input.parse()?, + semi_token: input.parse()?, + }) + } +} + +fn parse_index_params(input: ParseStream) -> Result> { + if input.peek(token::Bracket) { + let content; + Ok(Some(IndexParams { + bracket_token: bracketed!(content in input), + params: Punctuated::parse_terminated(&content)?, + })) + } else { + Ok(None) + } +} + +impl Parse for ItemImpl { + fn parse(input: ParseStream) -> Result { + let content; + let attrs = input.call(Attribute::parse_outer)?; + let impl_token = input.parse()?; + let mut generics: Generics = input.parse()?; + + let mut first_ty = input.parse()?; + + let trait_; + let self_ty; + if input.peek(Token![for]) { + let for_token: Token![for] = input.parse()?; + let mut first_ty_ref = &first_ty; + while let syn::Type::Group(ty) = first_ty_ref { + first_ty_ref = &ty.elem; + } + if let syn::Type::Path(syn::TypePath { qself: None, .. }) = first_ty_ref { + while let syn::Type::Group(ty) = first_ty { + first_ty = *ty.elem; + } + if let syn::Type::Path(syn::TypePath { qself: None, path }) = first_ty { + trait_ = Some((path, for_token)); + } else { + unreachable!(); + } + } else { + return Err(syn::Error::new_spanned(first_ty_ref, "expected trait path")); + } + self_ty = input.parse()?; + } else { + trait_ = None; + self_ty = first_ty; + } + generics.where_clause = input.parse()?; + Ok(ItemImpl { + attrs, + impl_token, + generics, + self_ty: Box::new(self_ty), + trait_, + brace_token: braced!(content in input), + items: { + let mut items = Vec::new(); + while !content.is_empty() { + let value = content.parse()?; + items.push(value); + } + items + }, + }) + } +} + +impl ImplItem { + fn replace_attrs(&mut self, new: Vec) -> Vec { + match self { + ImplItem::Fn(ImplItemFn { attrs, .. }) + | ImplItem::Type(syn::ImplItemType { attrs, .. }) + | ImplItem::Reft(ImplItemReft { attrs, .. }) => mem::replace(attrs, new), + } + } +} + +impl Parse for ImplItem { + fn parse(input: ParseStream) -> Result { + let mut attrs = input.call(Attribute::parse_outer)?; + flux_tool_attrs(&mut attrs); + let ahead = input.fork(); + let _: Visibility = ahead.parse()?; + let lookahead = ahead.lookahead1(); + let mut item = if lookahead.peek(Token![fn]) || peek_signature(&ahead) { + ImplItem::Fn(input.parse()?) + } else if lookahead.peek(Token![type]) { + ImplItem::Type(input.parse()?) + } else if lookahead.peek(kw::reft) { + ImplItem::Reft(input.parse()?) + } else { + return Err(lookahead.error()); + }; + item.replace_attrs(attrs); + Ok(item) + } +} + +impl Parse for Signature { + fn parse(input: ParseStream) -> Result { + let content; + let fn_token = input.parse()?; + let ident = input.parse()?; + let mut generics: Generics = input.parse()?; + let paren_token = parenthesized!(content in input); + let inputs = content.parse_terminated(FnArg::parse, Token![,])?; + let output = input.parse()?; + generics.where_clause = opt_parse_where_clause_in_signature(input)?; + let requires = parse_requires(input)?; + let ensures = parse_ensures(input)?; + Ok(Signature { fn_token, ident, generics, paren_token, inputs, output, requires, ensures }) + } +} + +fn parse_requires(input: ParseStream) -> Result> { + if !input.peek(kw::requires) { + return Ok(None); + } + + let requires_token = input.parse()?; + let mut constraint = TokenStream::new(); + while !(input.is_empty() || input.peek(kw::ensures) || input.peek(token::Brace)) { + let tt: TokenTree = input.parse()?; + constraint.append(tt); + } + Ok(Some(Requires { requires_token, constraint })) +} + +fn parse_ensures(input: ParseStream) -> Result> { + if input.peek(kw::ensures) { + Ok(Some(Ensures { + ensures_token: input.parse()?, + constraints: parse_until(input, Constraint::parse, Token![,], token::Brace)?, + })) + } else { + Ok(None) + } +} + +impl Parse for Constraint { + fn parse(input: ParseStream) -> Result { + let mut expr = TokenStream::new(); + + if input.peek(Ident) || input.peek(Token![self]) { + let ident = parse_ident_or_self(input)?; + if input.peek(Token![:]) { + return Ok(Constraint::Type { + ident, + colon_token: input.parse()?, + ty: input.parse()?, + }); + } + expr.append(ident); + } + + while !(input.is_empty() || input.peek(Token![,]) || input.peek(token::Brace)) { + let tt: TokenTree = input.parse()?; + expr.append(tt); + } + Ok(Constraint::Expr(expr)) + } +} + +impl Parse for FnArg { + fn parse(input: ParseStream) -> Result { + let pat = input.parse()?; + let colon_token = input.parse()?; + let fn_arg = if input.peek(Token![&]) && input.peek2(kw::strg) { + let and_token = input.parse()?; + let strg_token = input.parse()?; + let ty = input.parse()?; + FnArg::StrgRef(StrgRef { pat, colon_token, and_token, strg_token, ty }) + } else if input.peek(Ident) { + let bty: BaseType = input.parse()?; + let mut pred = None; + let ty = if input.peek(token::Bracket) { + let content; + Type::Indexed(TypeIndexed { + bty, + bracket_token: bracketed!(content in input), + expr: content.parse()?, + }) + } else if input.peek(token::Brace) { + let content; + let brace_token = braced!(content in input); + if content.peek(Ident) && content.peek2(Token![:]) { + Type::Exists(TypeExists { + bty, + brace_token, + ident: content.parse()?, + colon_token: content.parse()?, + expr: content.parse()?, + }) + } else { + pred = Some(PatTypePredicate { brace_token, pred: content.parse()? }); + Type::Base(bty) + } + } else { + Type::Base(bty) + }; + FnArg::Typed(PatType { pat, colon_token, ty, pred }) + } else { + FnArg::Typed(PatType { pat, colon_token, ty: input.parse()?, pred: None }) + }; + Ok(fn_arg) + } +} + +impl Parse for Pat { + fn parse(input: ParseStream) -> Result { + let pat = if input.peek(Token![_]) { + Pat::Wild(input.parse()?) + } else { + Pat::Ident(PatIdent { mutability: input.parse()?, ident: parse_ident_or_self(input)? }) + }; + Ok(pat) + } +} + +impl Parse for ReturnType { + fn parse(input: ParseStream) -> Result { + if input.peek(Token![->]) { + Ok(ReturnType::Type(input.parse()?, input.parse()?)) + } else { + Ok(ReturnType::Default) + } + } +} + +impl Parse for Type { + fn parse(input: ParseStream) -> Result { + let ty = if input.peek(Token![&]) { + Type::Reference(input.parse()?) + } else if input.peek(token::Brace) { + let content; + let brace_token = braced!(content in input); + if content.peek(Ident) + && (content.peek2(Token![:]) + || content.peek2(Token![,]) + || content.peek2(Token![.])) + { + let params = parse_until(&content, ExistsParam::parse, Token![,], Token![.])?; + let dot_token = content.parse()?; + let ty = content.parse()?; + let mut or_token = None; + let mut pred = None; + if content.peek(Token![|]) { + or_token = Some(content.parse()?); + pred = Some(content.parse()?); + } + Type::GeneralExists(TypeGeneralExists { + brace_token, + params, + dot_token, + ty, + or_token, + pred, + }) + } else { + Type::Constraint(TypeConstraint { + brace_token, + ty: content.parse()?, + or_token: content.parse()?, + pred: content.parse()?, + }) + } + } else if input.peek(token::Bracket) { + let content; + let bracket_token = bracketed!(content in input); + let ty = content.parse()?; + if content.peek(Token![;]) { + Type::Array(TypeArray { + bracket_token, + ty, + semi_token: content.parse()?, + len: content.parse()?, + }) + } else { + parse_rty(input, BaseType::Slice(TypeSlice { bracket_token, ty }))? + } + } else if input.peek(token::Paren) { + Type::Tuple(input.parse()?) + } else if input.peek(Token![*]) { + Type::Ptr(input.parse()?) + } else { + parse_rty(input, input.parse()?)? + }; + Ok(ty) + } +} + +impl Parse for TypeTuple { + fn parse(input: ParseStream) -> Result { + let content; + Ok(TypeTuple { + paren_token: parenthesized!(content in input), + elems: content.parse_terminated(Type::parse, Token![,])?, + }) + } +} + +fn parse_rty(input: ParseStream, bty: BaseType) -> Result { + let ty = if input.peek(token::Bracket) { + let content; + Type::Indexed(TypeIndexed { + bty, + bracket_token: bracketed!(content in input), + expr: content.parse()?, + }) + } else if input.peek(token::Brace) { + let ahead = input.fork(); + let mut content; + braced!(content in ahead); + if content.peek(Ident) && content.peek2(Token![:]) { + Type::Exists(TypeExists { + bty, + brace_token: braced!(content in input), + ident: content.parse()?, + colon_token: content.parse()?, + expr: content.parse()?, + }) + } else { + Type::Base(bty) + } + } else { + Type::Base(bty) + }; + Ok(ty) +} + +impl Parse for TypeReference { + fn parse(input: ParseStream) -> Result { + Ok(TypeReference { + and_token: input.parse()?, + lifetime: input.parse()?, + mutability: input.parse()?, + elem: input.parse()?, + }) + } +} + +impl Parse for BaseType { + fn parse(input: ParseStream) -> Result { + if input.peek(token::Bracket) { + let content; + Ok(BaseType::Slice(TypeSlice { + bracket_token: bracketed!(content in input), + ty: content.parse()?, + })) + } else { + Ok(BaseType::Path(input.parse()?)) + } + } +} + +impl Parse for Path { + fn parse(input: ParseStream) -> Result { + let mut segments = Punctuated::new(); + segments.push_value(input.parse()?); + while input.peek(Token![::]) { + segments.push_punct(input.parse()?); + segments.push_value(input.parse()?); + } + Ok(Path { segments }) + } +} + +impl Parse for PathSegment { + fn parse(input: ParseStream) -> Result { + let ident = + if input.peek(Token![Self]) { input.call(Ident::parse_any)? } else { input.parse()? }; + let arguments = if input.peek(Token![<]) && !input.peek(Token![<=]) { + PathArguments::AngleBracketed(input.parse()?) + } else { + PathArguments::None + }; + Ok(PathSegment { ident, arguments }) + } +} + +impl Parse for AngleBracketedGenericArguments { + fn parse(input: ParseStream) -> Result { + Ok(AngleBracketedGenericArguments { + lt_token: input.parse()?, + args: parse_until(input, GenericArgument::parse, Token![,], Token![>])?, + gt_token: input.parse()?, + }) + } +} + +impl Parse for GenericArgument { + fn parse(input: ParseStream) -> Result { + Ok(GenericArgument::Type(input.parse()?)) + } +} + +impl Parse for ExistsParam { + fn parse(input: ParseStream) -> Result { + let ident = input.parse()?; + let mut colon_token = None; + let mut sort = None; + if input.peek(Token![:]) { + colon_token = Some(input.parse()?); + sort = Some(input.parse()?); + } + Ok(ExistsParam { ident, colon_token, sort }) + } +} + +impl Parse for Block { + fn parse(input: ParseStream) -> Result { + let content; + Ok(Block { brace_token: braced!(content in input), stmts: content.parse()? }) + } +} + +fn parse_until( + input: ParseStream, + parser: fn(ParseStream) -> Result, + sep: P1, + end: P2, +) -> Result> +where + P1::Token: Parse, +{ + let _ = sep; + let mut params = Punctuated::new(); + loop { + if input.peek(end) { + return Ok(params); + } + params.push_value(parser(input)?); + if input.peek(end) { + return Ok(params); + } + params.push_punct(input.parse()?); + } +} + +fn parse_ident_or_self(input: ParseStream) -> Result { + if input.peek(Token![self]) { input.call(Ident::parse_any) } else { input.parse() } +} + +mod kw { + syn::custom_keyword!(strg); + syn::custom_keyword!(ensures); + syn::custom_keyword!(requires); + syn::custom_keyword!(refined); + syn::custom_keyword!(by); + syn::custom_keyword!(base); + syn::custom_keyword!(bitvec); + syn::custom_keyword!(reft); +} + +#[derive(Copy, Clone, Eq, PartialEq)] +enum Mode { + Flux, + Rust, +} + +impl Item { + fn replace_attrs(&mut self, new: Vec) -> Vec { + match self { + Item::Fn(ItemFn { attrs, .. }) + | Item::Mod(ItemMod { attrs, .. }) + | Item::Impl(ItemImpl { attrs, .. }) + | Item::Enum(ItemEnum { attrs, .. }) + | Item::Struct(ItemStruct { attrs, .. }) + | Item::Use(syn::ItemUse { attrs, .. }) + | Item::Trait(ItemTrait { attrs, .. }) + | Item::Type(ItemType { attrs, .. }) + | Item::Const(syn::ItemConst { attrs, .. }) => mem::replace(attrs, new), + } + } +} + +impl ToTokens for Items { + fn to_tokens(&self, tokens: &mut TokenStream) { + tokens.append_all(&self.0); + } +} + +impl ToTokens for Item { + fn to_tokens(&self, tokens: &mut TokenStream) { + match self { + Item::Fn(item_fn) => item_fn.to_tokens(tokens), + Item::Impl(item_impl) => item_impl.to_tokens(tokens), + Item::Struct(item_struct) => item_struct.to_tokens(tokens), + Item::Enum(item_enum) => item_enum.to_tokens(tokens), + Item::Use(item_use) => item_use.to_tokens(tokens), + Item::Type(item_type) => item_type.to_tokens(tokens), + Item::Mod(item_mod) => item_mod.to_tokens(tokens), + Item::Trait(item_trait) => item_trait.to_tokens(tokens), + Item::Const(item_const) => item_const.to_tokens(tokens), + } + } +} + +impl ToTokens for ItemMod { + fn to_tokens(&self, tokens: &mut TokenStream) { + tokens.append_all(&self.attrs); + self.vis.to_tokens(tokens); + self.unsafety.to_tokens(tokens); + self.mod_token.to_tokens(tokens); + self.ident.to_tokens(tokens); + if let Some((brace, items)) = &self.content { + brace.surround(tokens, |tokens| { + tokens.append_all(items); + }); + } + self.semi.to_tokens(tokens); + } +} + +impl ToTokens for ItemStruct { + fn to_tokens(&self, tokens: &mut TokenStream) { + tokens.append_all(&self.attrs); + #[cfg(flux_sysroot)] + if let Some(refined_by) = &self.refined_by { + refined_by.flux_tool_attr().to_tokens(tokens); + } + self.vis.to_tokens(tokens); + self.struct_token.to_tokens(tokens); + self.ident.to_tokens(tokens); + self.generics.to_tokens(tokens, Mode::Rust); + self.fields.to_tokens(tokens, |field, tokens| { + #[cfg(flux_sysroot)] + field.flux_tool_attr().to_tokens(tokens); + field.to_tokens(tokens); + }); + self.semi_token.to_tokens(tokens); + } +} + +impl ToTokens for ItemEnum { + fn to_tokens(&self, tokens: &mut TokenStream) { + tokens.append_all(&self.attrs); + #[cfg(flux_sysroot)] + if let Some(refined_by) = &self.refined_by { + refined_by.flux_tool_attr().to_tokens(tokens); + } + self.vis.to_tokens(tokens); + self.enum_token.to_tokens(tokens); + self.ident.to_tokens(tokens); + self.generics.to_tokens(tokens, Mode::Rust); + self.brace_token.surround(tokens, |tokens| { + self.variants.to_tokens(tokens); + }); + } +} + +impl ToTokens for Variant { + fn to_tokens(&self, tokens: &mut TokenStream) { + #[cfg(flux_sysroot)] + self.flux_tool_attr().to_tokens(tokens); + tokens.append_all(&self.attrs); + self.ident.to_tokens(tokens); + self.fields.to_tokens(tokens, Field::to_tokens); + if let Some((eq_token, expr)) = &self.discriminant { + eq_token.to_tokens(tokens); + expr.to_tokens(tokens); + } + } +} + +impl ToTokens for RefinedBy { + fn to_tokens(&self, tokens: &mut TokenStream) { + for param in self.params.pairs() { + param.value().to_tokens(tokens); + param.punct().to_tokens(tokens); + } + } +} + +impl ToTokens for RefinedByParam { + fn to_tokens(&self, tokens: &mut TokenStream) { + self.ident.to_tokens(tokens); + self.colon_token.to_tokens(tokens); + self.sort.to_tokens(tokens); + } +} + +impl ToTokens for Sort { + fn to_tokens(&self, tokens: &mut TokenStream) { + match self { + Sort::BaseSort(bsort) => bsort.to_tokens(tokens), + Sort::Func { input, arrow, output } => { + input.to_tokens(tokens); + arrow.to_tokens(tokens); + output.to_tokens(tokens); + } + } + } +} + +impl ToTokens for FuncSortInput { + fn to_tokens(&self, tokens: &mut TokenStream) { + match self { + FuncSortInput::Parenthesized { paren_token, inputs } => { + paren_token.surround(tokens, |tokens| { + inputs.to_tokens(tokens); + }); + } + FuncSortInput::Single(bsort) => bsort.to_tokens(tokens), + } + } +} + +impl ToTokens for BaseSort { + fn to_tokens(&self, tokens: &mut TokenStream) { + match self { + BaseSort::BitVec(bitvec) => bitvec.to_tokens(tokens), + BaseSort::App(ctor, args) => { + ctor.to_tokens(tokens); + args.to_tokens(tokens); + } + } + } +} + +impl ToTokens for BitVecSort { + fn to_tokens(&self, tokens: &mut TokenStream) { + self.bitvec_token.to_tokens(tokens); + self.lt_token.to_tokens(tokens); + self.lit.to_tokens(tokens); + self.gt_token.to_tokens(tokens); + } +} + +impl ToTokens for SortArguments { + fn to_tokens(&self, tokens: &mut TokenStream) { + match self { + SortArguments::None => {} + SortArguments::AngleBracketed(args) => args.to_tokens(tokens), + } + } +} + +impl ToTokens for AngleBracketedSortArgs { + fn to_tokens(&self, tokens: &mut TokenStream) { + self.lt_token.to_tokens(tokens); + self.args.to_tokens(tokens); + self.gt_token.to_tokens(tokens); + } +} + +impl ToTokens for ItemFn { + fn to_tokens(&self, tokens: &mut TokenStream) { + let ItemFn { attrs, vis, sig, block } = self; + #[cfg(flux_sysroot)] + { + let flux_sig = ToTokensFlux(sig); + quote!(#[flux_tool::sig(#flux_sig)]).to_tokens(tokens); + } + let rust_sig = ToTokensRust(sig); + quote! { + #(#attrs)* + #vis #rust_sig #block + } + .to_tokens(tokens); + } +} + +impl ToTokens for ItemType { + fn to_tokens(&self, tokens: &mut TokenStream) { + #[cfg(flux_sysroot)] + self.flux_tool_attr().to_tokens(tokens); + self.to_tokens_inner(tokens, Mode::Rust); + } +} + +#[cfg(flux_sysroot)] +impl ToTokens for ToTokensFlux<&ItemType> { + fn to_tokens(&self, tokens: &mut TokenStream) { + self.0.to_tokens_inner(tokens, Mode::Flux); + } +} + +#[cfg(flux_sysroot)] +impl ToTokens for ToTokensFlux<&Type> { + fn to_tokens(&self, tokens: &mut TokenStream) { + self.0.to_tokens_inner(tokens, Mode::Flux); + } +} + +impl ItemType { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + if mode == Mode::Rust { + tokens.append_all(&self.attrs); + self.vis.to_tokens(tokens); + } + self.type_token.to_tokens(tokens); + self.ident.to_tokens(tokens); + self.generics.to_tokens(tokens, mode); + if let Some(params) = &self.index_params { + params.to_tokens_inner(tokens, mode); + } + self.eq_token.to_tokens(tokens); + self.ty.to_tokens_inner(tokens, mode); + if mode == Mode::Rust { + self.semi_token.to_tokens(tokens); + } + } + + #[cfg(flux_sysroot)] + fn flux_tool_attr(&self) -> TokenStream { + let flux_type = ToTokensFlux(self); + quote! { + #[flux_tool::alias(#flux_type)] + } + } +} + +impl Generics { + fn to_tokens(&self, tokens: &mut TokenStream, mode: Mode) { + if self.params.is_empty() { + return; + } + + tokens_or_default(self.lt_token.as_ref(), tokens); + + for param in self.params.pairs() { + match mode { + Mode::Rust => { + param.to_tokens(tokens); + } + Mode::Flux => { + if let GenericParam::Type(p) = param.value() { + p.to_tokens(tokens, mode); + param.punct().to_tokens(tokens); + } + } + } + } + + tokens_or_default(self.gt_token.as_ref(), tokens); + } +} + +impl ToTokens for GenericParam { + fn to_tokens(&self, tokens: &mut TokenStream) { + match self { + GenericParam::Lifetime(p) => p.to_tokens(tokens), + GenericParam::Type(p) => p.to_tokens(tokens, Mode::Rust), + GenericParam::Const(p) => p.to_tokens(tokens), + } + } +} + +impl TypeParam { + fn to_tokens(&self, tokens: &mut TokenStream, mode: Mode) { + tokens.append_all(outer(&self.attrs)); + self.ident.to_tokens(tokens); + + if mode == Mode::Flux { + if let Some(as_token) = self.as_token { + as_token.to_tokens(tokens); + self.param_kind.to_tokens(tokens); + } + } + + if !self.bounds.is_empty() && mode == Mode::Rust { + tokens_or_default(self.colon_token.as_ref(), tokens); + self.bounds.to_tokens(tokens); + } + // if let Some(default) = &self.default { + // tokens_or_default(self.eq_token.as_ref(), tokens); + // default.to_tokens(tokens); + // } + } +} + +impl IndexParams { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + if mode == Mode::Flux { + self.bracket_token.surround(tokens, |tokens| { + for param in self.params.pairs() { + param.value().to_tokens_inner(tokens); + param.punct().to_tokens(tokens); + } + }); + } + } +} + +impl ToTokens for ItemImpl { + fn to_tokens(&self, tokens: &mut TokenStream) { + tokens.append_all(&self.attrs); + #[cfg(flux_sysroot)] + for item in &self.items { + if let ImplItem::Reft(reft) = item { + reft.flux_tool_attr().to_tokens(tokens); + } + } + self.impl_token.to_tokens(tokens); + self.generics.to_tokens(tokens, Mode::Rust); + if let Some((trait_, for_token)) = &self.trait_ { + trait_.to_tokens(tokens); + for_token.to_tokens(tokens); + } + self.self_ty.to_tokens(tokens); + self.generics.where_clause.to_tokens(tokens); + self.brace_token + .surround(tokens, |tokens| tokens.append_all(&self.items)); + } +} + +impl ToTokens for ImplItem { + fn to_tokens(&self, tokens: &mut TokenStream) { + match self { + ImplItem::Fn(impl_item_fn) => impl_item_fn.to_tokens(tokens), + ImplItem::Type(impl_item_ty) => impl_item_ty.to_tokens(tokens), + ImplItem::Reft(_) => {} + } + } +} + +impl ToTokens for ImplItemFn { + fn to_tokens(&self, tokens: &mut TokenStream) { + let ImplItemFn { attrs, vis, sig, block } = self; + #[cfg(flux_sysroot)] + { + let flux_sig = ToTokensFlux(sig); + quote!(#[flux_tool::sig(#flux_sig)]).to_tokens(tokens); + } + let rust_sig = ToTokensRust(sig); + quote! { + #(#attrs)* + #vis #rust_sig #block + } + .to_tokens(tokens); + } +} + +#[cfg(flux_sysroot)] +struct ToTokensFlux(T); + +#[cfg(flux_sysroot)] +impl ToTokens for ToTokensFlux<&Signature> { + fn to_tokens(&self, tokens: &mut TokenStream) { + self.0.to_tokens_inner(tokens, Mode::Flux); + } +} + +struct ToTokensRust(T); + +impl ToTokens for ToTokensRust<&Signature> { + fn to_tokens(&self, tokens: &mut TokenStream) { + self.0.to_tokens_inner(tokens, Mode::Rust); + } +} + +impl Signature { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + self.fn_token.to_tokens(tokens); + if mode == Mode::Rust { + self.ident.to_tokens(tokens); + } + self.generics.to_tokens(tokens, mode); + self.paren_token.surround(tokens, |tokens| { + for fn_arg in self.inputs.pairs() { + fn_arg.value().to_tokens_inner(tokens, mode); + fn_arg.punct().to_tokens(tokens); + } + }); + self.output.to_tokens_inner(tokens, mode); + if mode == Mode::Rust { + self.generics.where_clause.to_tokens(tokens); + } + if let Some(requires) = &self.requires { + requires.to_tokens_inner(tokens, mode); + } + if let Some(ensures) = &self.ensures { + ensures.to_tokens_inner(tokens, mode); + } + } +} + +impl Requires { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + if mode == Mode::Flux { + self.requires_token.to_tokens(tokens); + self.constraint.to_tokens(tokens); + } + } +} + +impl Ensures { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + if mode == Mode::Flux { + self.ensures_token.to_tokens(tokens); + for constraint in self.constraints.pairs() { + constraint.value().to_tokens_inner(tokens); + constraint.punct().to_tokens(tokens); + } + } + } +} + +impl Constraint { + fn to_tokens_inner(&self, tokens: &mut TokenStream) { + match self { + Constraint::Type { ident, colon_token, ty } => { + ident.to_tokens(tokens); + colon_token.to_tokens(tokens); + ty.to_tokens_inner(tokens, Mode::Flux); + } + Constraint::Expr(e) => e.to_tokens(tokens), + } + } +} + +impl FnArg { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + match self { + FnArg::StrgRef(strg_ref) => strg_ref.to_tokens_inner(tokens, mode), + FnArg::Typed(pat_type) => { + pat_type.to_tokens_inner(tokens, mode); + } + } + } +} + +impl StrgRef { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + self.pat.to_tokens_inner(tokens, mode); + self.colon_token.to_tokens(tokens); + self.and_token.to_tokens(tokens); + match mode { + Mode::Flux => self.strg_token.to_tokens(tokens), + Mode::Rust => { + let span = self.strg_token.span; + quote_spanned!(span=> mut).to_tokens(tokens); + } + } + self.ty.to_tokens_inner(tokens, mode); + } +} + +impl ReturnType { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + match self { + ReturnType::Default => {} + ReturnType::Type(arrow, ty) => { + arrow.to_tokens(tokens); + ty.to_tokens_inner(tokens, mode); + } + } + } +} + +impl PatType { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + self.pat.to_tokens_inner(tokens, mode); + self.colon_token.to_tokens(tokens); + self.ty.to_tokens_inner(tokens, mode); + if mode == Mode::Flux { + if let Some(pred) = &self.pred { + pred.to_tokens_inner(tokens); + } + } + } +} + +impl Pat { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + match self { + Pat::Ident(pat_ident) => pat_ident.to_tokens_inner(tokens, mode), + Pat::Wild(underscore_token) => { + underscore_token.to_tokens(tokens); + } + } + } +} + +impl PatIdent { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + if mode == Mode::Rust { + self.mutability.to_tokens(tokens); + } + self.ident.to_tokens(tokens); + } +} + +impl Type { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + match self { + Type::Base(bty) => bty.to_tokens_inner(tokens, mode), + Type::Indexed(ty_indexed) => ty_indexed.to_tokens_inner(tokens, mode), + Type::Exists(ty_exists) => ty_exists.to_tokens_inner(tokens, mode), + Type::GeneralExists(ty_general_exists) => { + ty_general_exists.to_tokens_inner(tokens, mode); + } + Type::Reference(ty_reference) => ty_reference.to_tokens_inner(tokens, mode), + Type::Constraint(ty_constraint) => ty_constraint.to_tokens_inner(tokens, mode), + Type::Array(ty_array) => ty_array.to_tokens_inner(tokens, mode), + Type::Tuple(tuple) => tuple.to_tokens_inner(tokens, mode), + Type::Ptr(ty_ptr) => ty_ptr.to_tokens(tokens), + } + } +} + +impl TypeReference { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + self.and_token.to_tokens(tokens); + if mode == Mode::Rust { + self.lifetime.to_tokens(tokens); + } + self.mutability.to_tokens(tokens); + self.elem.to_tokens_inner(tokens, mode); + } +} + +impl TypeIndexed { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + self.bty.to_tokens_inner(tokens, mode); + if mode == Mode::Flux { + self.bracket_token.surround(tokens, |tokens| { + self.expr.to_tokens(tokens); + }); + } + } +} + +impl TypeArray { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + self.bracket_token.surround(tokens, |tokens| { + self.ty.to_tokens_inner(tokens, mode); + self.semi_token.to_tokens(tokens); + if mode == Mode::Rust { + self.len.to_tokens(tokens); + } else { + quote!(_).to_tokens(tokens); + } + }); + } +} + +impl TypeConstraint { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + if mode == Mode::Flux { + self.brace_token.surround(tokens, |tokens| { + self.ty.to_tokens_inner(tokens, mode); + self.or_token.to_tokens(tokens); + self.pred.to_tokens(tokens); + }); + } else { + self.ty.to_tokens_inner(tokens, mode); + } + } +} + +impl TypeExists { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + self.bty.to_tokens_inner(tokens, mode); + if mode == Mode::Flux { + self.brace_token.surround(tokens, |tokens| { + self.ident.to_tokens(tokens); + self.colon_token.to_tokens(tokens); + self.expr.to_tokens(tokens); + }); + } + } +} + +impl TypeGeneralExists { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + match mode { + Mode::Flux => { + self.brace_token.surround(tokens, |tokens| { + for param in self.params.pairs() { + param.value().to_tokens_inner(tokens); + param.punct().to_tokens(tokens); + } + self.dot_token.to_tokens(tokens); + self.ty.to_tokens_inner(tokens, mode); + self.or_token.to_tokens(tokens); + self.pred.to_tokens(tokens); + }); + } + Mode::Rust => { + self.ty.to_tokens_inner(tokens, mode); + } + } + } +} + +impl BaseType { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + match self { + BaseType::Path(path) => path.to_tokens_inner(tokens, mode), + BaseType::Slice(type_slice) => { + type_slice.to_tokens_inner(tokens, mode); + } + } + } +} + +impl TypeSlice { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + self.bracket_token.surround(tokens, |tokens| { + self.ty.to_tokens_inner(tokens, mode); + }); + } +} + +impl PatTypePredicate { + fn to_tokens_inner(&self, tokens: &mut TokenStream) { + self.brace_token + .surround(tokens, |tokens| self.pred.to_tokens(tokens)); + } +} + +impl ExistsParam { + fn to_tokens_inner(&self, tokens: &mut TokenStream) { + self.ident.to_tokens(tokens); + self.colon_token.to_tokens(tokens); + self.sort.to_tokens(tokens); + } +} + +impl Path { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + for segment in self.segments.pairs() { + segment.value().to_tokens_inner(tokens, mode); + segment.punct().to_tokens(tokens); + } + } +} + +impl PathSegment { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + self.ident.to_tokens(tokens); + self.arguments.to_tokens_inner(tokens, mode); + } +} + +impl PathArguments { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + match self { + PathArguments::None => {} + PathArguments::AngleBracketed(args) => args.to_tokens_inner(tokens, mode), + } + } +} + +impl AngleBracketedGenericArguments { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + self.lt_token.to_tokens(tokens); + for arg in self.args.pairs() { + arg.value().to_tokens_inner(tokens, mode); + arg.punct().to_tokens(tokens); + } + self.gt_token.to_tokens(tokens); + } +} + +impl GenericArgument { + fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) { + match self { + GenericArgument::Type(ty) => ty.to_tokens_inner(tokens, mode), + } + } +} + +impl ToTokens for Block { + fn to_tokens(&self, tokens: &mut TokenStream) { + self.brace_token + .surround(tokens, |tokens| self.stmts.to_tokens(tokens)); + } +} + +fn outer(attrs: &[Attribute]) -> impl Iterator { + fn is_outer(attr: &&Attribute) -> bool { + match attr.style { + syn::AttrStyle::Outer => true, + syn::AttrStyle::Inner(_) => false, + } + } + attrs.iter().filter(is_outer) +} + +fn inner(attrs: &[Attribute]) -> impl Iterator { + fn is_inner(attr: &&Attribute) -> bool { + match attr.style { + syn::AttrStyle::Outer => false, + syn::AttrStyle::Inner(_) => true, + } + } + attrs.iter().filter(is_inner) +} + +fn peek_signature(input: ParseStream) -> bool { + let fork = input.fork(); + fork.parse::>().is_ok() + && fork.parse::>().is_ok() + && fork.parse::>().is_ok() + && fork.parse::>().is_ok() + && fork.peek(Token![fn]) +} + +struct FlexibleItemType { + vis: Visibility, + #[expect(dead_code)] + defaultness: Option, + type_token: Token![type], + ident: Ident, + generics: syn::Generics, + colon_token: Option, + bounds: Punctuated, + ty: Option<(Token![=], syn::Type)>, + semi_token: Token![;], +} + +enum TypeDefaultness { + #[expect(dead_code)] + Optional, + Disallowed, +} + +#[expect(dead_code)] +enum WhereClauseLocation { + // type Ty where T: 'static = T; + BeforeEq, + // type Ty = T where T: 'static; + AfterEq, + // TODO: goes away once the migration period on rust-lang/rust#89122 is over + Both, +} + +impl FlexibleItemType { + fn parse( + input: ParseStream, + allow_defaultness: TypeDefaultness, + where_clause_location: WhereClauseLocation, + ) -> Result { + let vis: Visibility = input.parse()?; + let defaultness: Option = match allow_defaultness { + TypeDefaultness::Optional => input.parse()?, + TypeDefaultness::Disallowed => None, + }; + let type_token: Token![type] = input.parse()?; + let ident: Ident = input.parse()?; + let mut generics: syn::Generics = input.parse()?; + let (colon_token, bounds) = Self::parse_optional_bounds(input)?; + + match where_clause_location { + WhereClauseLocation::BeforeEq | WhereClauseLocation::Both => { + generics.where_clause = input.parse()?; + } + WhereClauseLocation::AfterEq => {} + } + + let ty = Self::parse_optional_definition(input)?; + + match where_clause_location { + WhereClauseLocation::AfterEq | WhereClauseLocation::Both + if generics.where_clause.is_none() => + { + generics.where_clause = input.parse()?; + } + _ => {} + } + + let semi_token: Token![;] = input.parse()?; + + Ok(FlexibleItemType { + vis, + defaultness, + type_token, + ident, + generics, + colon_token, + bounds, + ty, + semi_token, + }) + } + + fn parse_optional_bounds( + input: ParseStream, + ) -> Result<(Option, Punctuated)> { + let colon_token: Option = input.parse()?; + + let mut bounds = Punctuated::new(); + if colon_token.is_some() { + loop { + if input.peek(Token![where]) || input.peek(Token![=]) || input.peek(Token![;]) { + break; + } + bounds.push_value(input.parse::()?); + if input.peek(Token![where]) || input.peek(Token![=]) || input.peek(Token![;]) { + break; + } + bounds.push_punct(input.parse::()?); + } + } + + Ok((colon_token, bounds)) + } + + fn parse_optional_definition(input: ParseStream) -> Result> { + let eq_token: Option = input.parse()?; + if let Some(eq_token) = eq_token { + let definition: syn::Type = input.parse()?; + Ok(Some((eq_token, definition))) + } else { + Ok(None) + } + } +} + +fn parse_trait_item_type(input: ParseStream) -> Result { + let FlexibleItemType { + vis, + defaultness: _, + type_token, + ident, + generics, + colon_token, + bounds, + ty, + semi_token, + } = FlexibleItemType::parse(input, TypeDefaultness::Disallowed, WhereClauseLocation::AfterEq)?; + + if !matches!(vis, Visibility::Inherited) { + Err(syn::Error::new_spanned(vis, "visibility qualifiers are not permitted here")) + } else { + Ok(TraitItem::Type(syn::TraitItemType { + attrs: Vec::new(), + type_token, + ident, + generics, + colon_token, + bounds, + default: ty, + semi_token, + })) + } +} diff --git a/crates/soroban-flux-attrs-impl/src/extern_spec.rs b/crates/soroban-flux-attrs-impl/src/extern_spec.rs new file mode 100644 index 0000000..99675e9 --- /dev/null +++ b/crates/soroban-flux-attrs-impl/src/extern_spec.rs @@ -0,0 +1,694 @@ +use std::mem; + +use proc_macro2::{Span, TokenStream}; +use quote::{ToTokens, TokenStreamExt, format_ident, quote, quote_spanned}; +use syn::{ + Attribute, Expr, FnArg, GenericArgument, GenericParam, Generics, Ident, Signature, Token, Type, + TypePath, braced, + parse::{Parse, ParseStream}, + parse_quote, parse_quote_spanned, + punctuated::Punctuated, + spanned::Spanned, + token::Brace, +}; + +use crate::{flux_tool_attrs, inner, outer, parse_inner, tokens_or_default}; + +pub(crate) fn transform_extern_spec( + attr: TokenStream, + tokens: TokenStream, +) -> syn::Result { + let mod_path: Option = + if !attr.is_empty() { Some(syn::parse2(attr)?) } else { None }; + let mod_use = mod_path.map(UseWildcard); + let span = tokens.span(); + match syn::parse2::(tokens)? { + ExternItem::Struct(item_struct) => extern_struct_to_tokens(mod_use, item_struct), + ExternItem::Enum(item_enum) => extern_enum_to_tokens(mod_use, item_enum), + ExternItem::Trait(item_trait) => extern_trait_to_tokens(span, mod_use, item_trait), + ExternItem::Fn(extern_fn) => extern_fn_to_tokens(span, mod_use, extern_fn), + ExternItem::Impl(extern_item_impl) => { + extern_impl_to_tokens(span, mod_use, extern_item_impl) + } + } +} + +fn extern_fn_to_tokens( + span: Span, + mod_use: Option, + mut extern_fn: ExternFn, +) -> syn::Result { + extern_fn.prepare(&FnCtxt::Free, true); + Ok(quote_spanned! {span=> + #[allow(unused, dead_code, non_camel_case_types)] + #[flux_tool::extern_spec] + const _: () = { + #mod_use + + #extern_fn + }; + }) +} + +fn extern_enum_to_tokens( + mod_use: Option, + mut item_enum: syn::ItemEnum, +) -> syn::Result { + let span = item_enum.span(); + let ident = item_enum.ident; + + item_enum.ident = format_ident!("__FluxExternSpecEnum__{}", ident); + + flux_tool_attrs(&mut item_enum.attrs); + for variant in &mut item_enum.variants { + flux_tool_attrs(&mut variant.attrs); + } + + let dummy_struct = format_ident!("__FluxExternSpecDummy__{}", ident); + let generics = &item_enum.generics; + let args = generic_params_to_args(&generics.params); + + Ok(quote_spanned! {span=> + #[allow(unused, dead_code, non_camel_case_types)] + #[flux_tool::extern_spec] + const _: () = { + #mod_use + + struct #dummy_struct #generics ( #ident < #args > ); + + #item_enum + }; + }) +} + +fn extern_struct_to_tokens( + mod_use: Option, + mut item_struct: syn::ItemStruct, +) -> syn::Result { + let item_struct_span = item_struct.span(); + let ident = item_struct.ident; + + let generics = &item_struct.generics; + let args = generic_params_to_args(&generics.params); + + // Prepare struct + item_struct.ident = format_ident!("__FluxExternSpecStruct__{}", ident); + flux_tool_attrs(&mut item_struct.attrs); + for field in &mut item_struct.fields { + flux_tool_attrs(&mut field.attrs); + } + if let syn::Fields::Unit = &item_struct.fields { + if !has_opaque_attr(&item_struct.attrs) { + item_struct.attrs.push(parse_quote!(#[flux_tool::opaque])); + } + item_struct.fields = syn::Fields::Unnamed(parse_quote! { (#ident < #args >) }); + } + + // Dummy struct used to extract def_id + let dummy_struct = format_ident!("__FluxExternSpecDummy__{}", ident); + + Ok(quote_spanned! {item_struct_span => + #[allow(unused, dead_code, non_camel_case_types)] + #[flux_tool::extern_spec] + const _: () = { + #mod_use + + struct #dummy_struct #generics (#ident < #args >); + + #item_struct + }; + }) +} + +fn has_opaque_attr(attrs: &[syn::Attribute]) -> bool { + attrs + .iter() + .any(|attr| path_matches(attr.path(), &["flux_tool", "opaque"])) +} + +fn path_matches(path: &syn::Path, x: &[&str]) -> bool { + let mut i = 0; + for segment in &path.segments { + if i == x.len() { + return false; + } + if segment.ident != x[i] { + return false; + } + i += 1; + } + true +} + +fn extern_trait_to_tokens( + span: Span, + mod_use: Option, + mut item_trait: ExternItemTrait, +) -> syn::Result { + item_trait.prepare(); + let item_trait = item_trait; + + Ok(quote_spanned! {span => + #[allow(unused, dead_code, non_camel_case_types)] + #[flux_tool::extern_spec] + const _: () = { + #mod_use + + #item_trait + }; + }) +} + +fn extern_impl_to_tokens( + span: Span, + mod_use: Option, + mut extern_item_impl: ExternItemImpl, +) -> syn::Result { + extern_item_impl.prepare(); + let extern_item_impl = extern_item_impl; // no more mutation + + let self_ty = &extern_item_impl.self_ty; + let (impl_generics, ty_generics, where_clause) = &extern_item_impl.generics.split_for_impl(); + + let dummy_ident = &extern_item_impl.dummy_ident; + let mut fields = generic_params_to_fields(&extern_item_impl.generics.params); + fields.push(parse_quote!(#self_ty)); + + let dummy_impl = if let Some((_, trait_, _)) = &extern_item_impl.trait_ { + Some(quote!( + impl #impl_generics #dummy_ident #ty_generics #where_clause { + fn __flux_extern_extract_impl_id() where #self_ty: #trait_ {} + } + )) + } else { + None + }; + + Ok(quote_spanned! {span=> + #[allow(unused, dead_code, non_camel_case_types)] + #[flux_tool::extern_spec] + const _: () = { + #mod_use + + struct #dummy_ident #impl_generics ( #fields ) #where_clause; + + #dummy_impl + + #extern_item_impl + }; + }) +} + +enum ExternItem { + Struct(syn::ItemStruct), + Enum(syn::ItemEnum), + Trait(ExternItemTrait), + Fn(ExternFn), + Impl(ExternItemImpl), +} + +impl ExternItem { + fn replace_attrs(&mut self, new: Vec) -> Vec { + match self { + ExternItem::Struct(syn::ItemStruct { attrs, .. }) + | ExternItem::Enum(syn::ItemEnum { attrs, .. }) + | ExternItem::Trait(ExternItemTrait { attrs, .. }) + | ExternItem::Fn(ExternFn { attrs, .. }) + | ExternItem::Impl(ExternItemImpl { attrs, .. }) => mem::replace(attrs, new), + } + } +} + +impl Parse for ExternItem { + fn parse(input: ParseStream) -> syn::Result { + let mut attrs = input.call(Attribute::parse_outer)?; + let lookahead = input.lookahead1(); + let mut item = if lookahead.peek(Token![fn]) || lookahead.peek(Token![unsafe]) { + ExternItem::Fn(input.parse()?) + } else if lookahead.peek(Token![impl]) { + ExternItem::Impl(input.parse()?) + } else if lookahead.peek(Token![struct]) { + ExternItem::Struct(input.parse()?) + } else if lookahead.peek(Token![enum]) { + let enm = input.parse(); + ExternItem::Enum(enm?) + } else if lookahead.peek(Token![trait]) { + ExternItem::Trait(input.parse()?) + } else { + return Err(lookahead.error()); + }; + + attrs.extend(item.replace_attrs(Vec::new())); + item.replace_attrs(attrs); + Ok(item) + } +} + +struct ExternItemImpl { + attrs: Vec, + impl_token: Token![impl], + generics: Generics, + trait_: Option<(Option, syn::Path, Token![for])>, + self_ty: Box, + brace_token: Brace, + items: Vec, + dummy_ident: Ident, +} + +impl ExternItemImpl { + fn prepare(&mut self) { + flux_tool_attrs(&mut self.attrs); + let cx = if let Some(trait_) = self.trait_.as_ref().map(|(_, path, _)| path) { + FnCtxt::TraitImpl { trait_, self_ty: &self.self_ty } + } else { + FnCtxt::InherentImpl { self_ty: &self.self_ty } + }; + + for item in &mut self.items { + item.prepare(&cx, false); + } + } +} + +impl ToTokens for ExternItemImpl { + fn to_tokens(&self, tokens: &mut TokenStream) { + let (impl_generics, ty_generics, where_clause) = self.generics.split_for_impl(); + + tokens.append_all(outer(&self.attrs)); + + self.impl_token.to_tokens(tokens); + impl_generics.to_tokens(tokens); + + self.dummy_ident.to_tokens(tokens); + ty_generics.to_tokens(tokens); + + where_clause.to_tokens(tokens); + self.brace_token.surround(tokens, |tokens| { + tokens.append_all(inner(&self.attrs)); + for item in &self.items { + item.to_tokens(tokens); + } + }); + } +} + +struct ExternItemTrait { + attrs: Vec, + trait_token: Token![trait], + ident: Ident, + generics: Generics, + supertrait: Option, + brace_token: Brace, + items: Vec, +} + +impl ExternItemTrait { + fn prepare(&mut self) { + let dummy_ident = format_ident!("__FluxExternTrait{}", self.ident); + let ident = std::mem::replace(&mut self.ident, dummy_ident); + + let ident_span = self.ident.span(); + let args = GenericArgs(&self.generics); + let trait_ = parse_quote_spanned!(ident_span=> #ident #args); + + flux_tool_attrs(&mut self.attrs); + + let cx = FnCtxt::Trait { trait_: &trait_ }; + for item in &mut self.items { + item.prepare(&cx, false); + } + + self.supertrait = Some(trait_); + } +} + +impl ToTokens for ExternItemTrait { + fn to_tokens(&self, tokens: &mut TokenStream) { + tokens.append_all(outer(&self.attrs)); + self.trait_token.to_tokens(tokens); + self.ident.to_tokens(tokens); + self.generics.to_tokens(tokens); + if let Some(supertrait) = &self.supertrait { + tokens.extend(quote!(: #supertrait)); + } + self.generics.where_clause.to_tokens(tokens); + self.brace_token.surround(tokens, |tokens| { + tokens.append_all(inner(&self.attrs)); + for item in &self.items { + item.to_tokens(tokens); + } + }) + } +} + +enum FnCtxt<'a> { + TraitImpl { self_ty: &'a syn::Type, trait_: &'a syn::Path }, + InherentImpl { self_ty: &'a syn::Type }, + Trait { trait_: &'a syn::Path }, + Free, +} + +struct ExternFn { + attrs: Vec, + sig: Signature, + block: Option, +} + +impl ExternFn { + fn prepare(&mut self, cx: &FnCtxt, mangle: bool) { + flux_tool_attrs(&mut self.attrs); + if let FnCtxt::TraitImpl { self_ty, .. } | FnCtxt::InherentImpl { self_ty } = cx { + struct ReplaceSelf<'a> { + self_ty: &'a syn::Type, + } + + impl syn::visit_mut::VisitMut for ReplaceSelf<'_> { + fn visit_type_mut(&mut self, ty: &mut syn::Type) { + if let syn::Type::Path(type_path) = ty { + if type_path.path.is_ident("Self") { + *ty = self.self_ty.clone(); + } + } + } + } + + syn::visit_mut::visit_signature_mut(&mut ReplaceSelf { self_ty }, &mut self.sig); + + self.change_receiver(self_ty); + } + self.fill_body(cx); + if mangle { + self.sig.ident = format_ident!("__flux_extern_spec_{}", self.sig.ident); + } + } + + fn change_receiver(&mut self, self_ty: &syn::Type) { + if let Some(first) = self.sig.inputs.first_mut() { + if let FnArg::Receiver(receiver) = first { + let ident = format_ident!("__self", span = receiver.self_token.span); + + *first = if receiver.colon_token.is_some() { + // If there's a colon this is an arbitrary self types and we leave it as is. + let receiver_ty = &receiver.ty; + parse_quote!(#ident : #receiver_ty) + } else if let Some((ampersand, lft)) = &receiver.reference { + let mutbl = receiver.mutability; + parse_quote!(#ident : #ampersand #lft #mutbl #self_ty) + } else { + parse_quote!(#ident : #self_ty) + }; + } + } + } + + fn fill_body(&mut self, cx: &FnCtxt) { + let ident = &self.sig.ident; + let fn_path = match cx { + FnCtxt::TraitImpl { self_ty, trait_ } => quote!(< #self_ty as #trait_ > :: #ident), + FnCtxt::InherentImpl { self_ty } => quote!(< #self_ty > :: #ident), + FnCtxt::Trait { trait_ } => quote!(< Self as #trait_ > :: #ident), + FnCtxt::Free => quote!(#ident), + }; + let generic_args = generic_params_to_args(&self.sig.generics.params); + let fn_args = fn_params_to_args(&self.sig.inputs); + if self.sig.unsafety.is_some() { + self.block = Some(quote!({ unsafe { #fn_path :: <#generic_args> ( #fn_args ) } })); + } else { + self.block = Some(quote!({ #fn_path :: <#generic_args> ( #fn_args ) })); + } + } +} + +impl ToTokens for ExternFn { + fn to_tokens(&self, tokens: &mut TokenStream) { + debug_assert!(self.block.is_some()); + tokens.append_all(&self.attrs); + self.sig.to_tokens(tokens); + self.block.to_tokens(tokens); + } +} + +impl Parse for ExternFn { + fn parse(input: ParseStream) -> syn::Result { + let attrs = input.call(Attribute::parse_outer)?; + let sig = input.parse()?; + input.parse::()?; + Ok(ExternFn { attrs, sig, block: None }) + } +} + +impl Parse for ExternItemImpl { + fn parse(input: ParseStream) -> syn::Result { + let mut attrs = input.call(Attribute::parse_outer)?; + let impl_token = input.parse()?; + let mut generics: Generics = input.parse()?; + + let mut first_ty: Type = input.parse()?; + let self_ty: Type; + let trait_; + + let is_impl_for = input.peek(Token![for]); + if is_impl_for { + let for_token: Token![for] = input.parse()?; + let mut first_ty_ref = &first_ty; + while let Type::Group(ty) = first_ty_ref { + first_ty_ref = &ty.elem; + } + if let Type::Path(TypePath { qself: None, .. }) = first_ty_ref { + while let Type::Group(ty) = first_ty { + first_ty = *ty.elem; + } + if let Type::Path(TypePath { qself: None, path }) = first_ty { + trait_ = Some((None, path, for_token)); + } else { + unreachable!(); + } + } else { + trait_ = None; + } + self_ty = input.parse()?; + } else { + trait_ = None; + self_ty = first_ty; + } + + generics.where_clause = input.parse()?; + + let content; + let brace_token = braced!(content in input); + parse_inner(&content, &mut attrs)?; + let mut items = Vec::new(); + while !content.is_empty() { + items.push(content.parse()?); + } + + let mut dummy_prefix = "__FluxExternImplStruct".to_string(); + if let Some(trait_path) = trait_.as_ref().map(|(_, path, _)| path) { + dummy_prefix.push_str(&create_dummy_string_from_path(trait_path)?); + } + let dummy_ident = create_dummy_ident(&mut dummy_prefix, &self_ty)?; + + Ok(ExternItemImpl { + attrs, + impl_token, + generics, + trait_, + self_ty: Box::new(self_ty), + brace_token, + items, + dummy_ident, + }) + } +} + +impl Parse for ExternItemTrait { + fn parse(input: ParseStream) -> syn::Result { + let mut attrs = input.call(Attribute::parse_outer)?; + let trait_token = input.parse()?; + let ident: Ident = input.parse()?; + let mut generics: syn::Generics = input.parse()?; + generics.where_clause = input.parse()?; + + let supertrait; + let has_super_trait = input.peek(Token![:]); + if has_super_trait { + input.parse::()?; + supertrait = Some(input.parse::()?); + } else { + supertrait = None; + } + let content; + let brace_token = braced!(content in input); + parse_inner(&content, &mut attrs)?; + let mut items = Vec::new(); + while !content.is_empty() { + items.push(content.parse()?); + } + + Ok(ExternItemTrait { attrs, trait_token, ident, generics, supertrait, brace_token, items }) + } +} + +fn create_dummy_ident(dummy_prefix: &mut String, ty: &syn::Type) -> syn::Result { + use syn::Type::*; + match ty { + Reference(ty_ref) => { + if ty_ref.mutability.is_some() { + dummy_prefix.push_str("Mut"); + }; + dummy_prefix.push_str("Ref"); + create_dummy_ident(dummy_prefix, ty_ref.elem.as_ref()) + } + Slice(ty_slice) => { + dummy_prefix.push_str("Slice"); + create_dummy_ident(dummy_prefix, ty_slice.elem.as_ref()) + } + Path(ty_path) => create_dummy_ident_from_path(dummy_prefix, &ty_path.path), + Ptr(ty_ptr) => { + if ty_ptr.mutability.is_some() { + dummy_prefix.push_str("MutPtr"); + } else { + dummy_prefix.push_str("ConstPtr"); + }; + create_dummy_ident(dummy_prefix, ty_ptr.elem.as_ref()) + } + Array(ty_array) => { + dummy_prefix.push_str("Array"); + create_dummy_ident(dummy_prefix, ty_array.elem.as_ref()) + } + _ => { + Err(syn::Error::new( + ty.span(), + format!("invalid extern_spec: unsupported type {:?}", ty), + )) + } + } +} + +fn create_dummy_string_from_path(path: &syn::Path) -> syn::Result { + if let Some(path_segment) = path.segments.last() { + // Mangle the identifier using the dummy_prefix + let str = format!("{}", path_segment.ident); + Ok(str) + } else { + Err(syn::Error::new(path.span(), format!("invalid extern_spec: empty Path {:?}", path))) + } +} + +fn create_dummy_ident_from_path(dummy_prefix: &str, path: &syn::Path) -> syn::Result { + // For paths, we mangle the last identifier + if let Some(path_segment) = path.segments.last() { + // Mangle the identifier using the dummy_prefix + let ident = Ident::new( + &format!("{}{}", dummy_prefix, path_segment.ident), + path_segment.ident.span(), + ); + Ok(ident) + } else { + Err(syn::Error::new(path.span(), format!("invalid extern_spec: empty Path {:?}", path))) + } +} + +struct GenericArgs<'a>(&'a syn::Generics); + +impl ToTokens for GenericArgs<'_> { + fn to_tokens(&self, tokens: &mut TokenStream) { + tokens_or_default(self.0.lt_token.as_ref(), tokens); + for param in self.0.params.pairs() { + match param.value() { + GenericParam::Lifetime(param) => { + param.lifetime.to_tokens(tokens); + } + GenericParam::Type(param) => { + param.ident.to_tokens(tokens); + } + GenericParam::Const(param) => { + param.ident.to_tokens(tokens); + } + } + param.punct().to_tokens(tokens); + } + tokens_or_default(self.0.gt_token.as_ref(), tokens); + } +} + +// Cribbed from Prusti's extern_spec_rewriter +fn generic_params_to_args( + generic_params: &Punctuated, +) -> Punctuated { + generic_params + .iter() + .map(|param| -> GenericArgument { + let span = param.span(); + match param { + GenericParam::Type(syn::TypeParam { ident, .. }) => { + parse_quote_spanned!(span => #ident ) + } + GenericParam::Lifetime(syn::LifetimeParam { lifetime, .. }) => { + parse_quote_spanned!(span => #lifetime ) + } + GenericParam::Const(syn::ConstParam { ident, .. }) => { + parse_quote_spanned!(span => #ident ) + } + } + }) + .collect() +} + +/// Given a list of generic parameters creates a list of fields that use all non-const parameters +fn generic_params_to_fields( + params: &Punctuated, +) -> Punctuated { + params + .iter() + .filter_map(|param| -> Option { + let span = param.span(); + match param { + GenericParam::Lifetime(syn::LifetimeParam { lifetime, .. }) => { + Some(parse_quote_spanned!(span=> &#lifetime ())) + } + GenericParam::Type(syn::TypeParam { ident, .. }) => { + Some(parse_quote_spanned!(span=> #ident)) + } + GenericParam::Const(..) => None, + } + }) + .collect() +} + +// Cribbed from Prusti's extern_spec_rewriter +fn fn_params_to_args(params: &Punctuated) -> Punctuated { + params + .iter() + .map(|param| -> Expr { + match param { + FnArg::Typed(pat_type) => { + match pat_type.pat.as_ref() { + syn::Pat::Ident(pat) => { + let ident = &pat.ident; + parse_quote!(#ident) + } + _ => { + unimplemented!( + "extern specs don't support patterns other than simple identifiers" + ) + } + } + } + FnArg::Receiver(_) => { + let span = param.span(); + parse_quote_spanned!(span=> self) + } + } + }) + .collect() +} + +struct UseWildcard(syn::Path); + +impl ToTokens for UseWildcard { + fn to_tokens(&self, tokens: &mut TokenStream) { + let path = &self.0; + tokens.extend(quote!(use #path::*;)) + } +} diff --git a/crates/soroban-flux-attrs-impl/src/lib.rs b/crates/soroban-flux-attrs-impl/src/lib.rs new file mode 100644 index 0000000..dd1ae37 --- /dev/null +++ b/crates/soroban-flux-attrs-impl/src/lib.rs @@ -0,0 +1,189 @@ +mod ast; +mod extern_spec; + +use proc_macro2::{Ident, Span, TokenStream}; +use quote::{ToTokens, format_ident, quote, quote_spanned}; +use syn::{ + Attribute, ItemEnum, ItemStruct, Token, bracketed, parse::ParseStream, parse_quote, + spanned::Spanned, +}; + +pub const FLUX_ATTRS: &[&str] = &[ + "assoc", + "field", + "generics", + "invariant", + "opaque", + "reflect", + "refined_by", + "sig", + "trusted", + "trusted_impl", + "proven_externally", + "variant", + "should_fail", + "opts", + "reft", + "no_panic", + "assume_parametric", + "no_suggestions", +]; + +pub fn extern_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream { + extern_spec::transform_extern_spec(attr, tokens).unwrap_or_else(|err| err.to_compile_error()) +} + +pub fn flux_tool_item_attr(name: &str, attr: TokenStream, item: TokenStream) -> TokenStream { + let span = Span::call_site(); + let name = format_ident!("{}", name, span = span); + if attr.is_empty() { + quote_spanned! {span=> + #[flux_tool::#name] + #item + } + } else { + quote_spanned! {span=> + #[flux_tool::#name(#attr)] + #item + } + } +} + +pub fn refined_by(attr: TokenStream, item: TokenStream) -> TokenStream { + let span = item.span(); + let mut item = match syn::parse2::(item) { + Ok(item) => item, + Err(err) => return err.to_compile_error(), + }; + + match &mut item { + syn::Item::Enum(item_enum) => refined_by_enum(item_enum), + syn::Item::Struct(item_struct) => refined_by_struct(item_struct), + _ => return syn::Error::new(span, "expected struct or enum").to_compile_error(), + } + + if cfg!(flux_sysroot) { + quote_spanned! {span=> + #[flux_tool::refined_by(#attr)] + #item + } + } else { + item.to_token_stream() + } +} + +fn refined_by_enum(item_enum: &mut ItemEnum) { + for variant in &mut item_enum.variants { + flux_tool_attrs(&mut variant.attrs); + } +} + +fn refined_by_struct(item_struct: &mut ItemStruct) { + for field in &mut item_struct.fields { + flux_tool_attrs(&mut field.attrs); + } +} + +fn flux_tool_attrs(attrs: &mut Vec) { + if cfg!(flux_sysroot) { + for attr in attrs { + transform_flux_attr(attr); + } + } else { + attrs.retain(|attr| !is_flux_attr(attr)); + } +} + +fn path_is_one_of(path: &syn::Path, idents: &[&str]) -> bool { + idents.iter().any(|ident| path.is_ident(ident)) +} + +fn is_flux_attr(attr: &syn::Attribute) -> bool { + let path = attr.path(); + if path.segments.len() >= 2 { + let ident = &path.segments[0].ident; + ident == "flux" || ident == "flux_rs" + } else { + path_is_one_of(path, FLUX_ATTRS) + } +} + +fn transform_flux_attr(attr: &mut syn::Attribute) { + let path = path_of_attr_mut(attr); + if path.leading_colon.is_some() { + return; + } + if path.segments.len() >= 2 { + let ident = &mut path.segments[0].ident; + if ident == "flux" || ident == "flux_rs" { + *ident = Ident::new("flux_tool", ident.span()); + } + return; + } else if path_is_one_of(path, FLUX_ATTRS) { + *path = parse_quote!(flux_tool::#path); + } +} + +fn path_of_attr_mut(attr: &mut Attribute) -> &mut syn::Path { + match &mut attr.meta { + syn::Meta::Path(path) => path, + syn::Meta::List(metalist) => &mut metalist.path, + syn::Meta::NameValue(namevalue) => &mut namevalue.path, + } +} + +pub fn flux(tokens: TokenStream) -> TokenStream { + syn::parse2::(tokens) + .map_or_else(|err| err.to_compile_error(), ToTokens::into_token_stream) +} + +pub fn defs(tokens: TokenStream) -> TokenStream { + quote! { + #[flux::defs { #tokens }] + const _: () = {}; + } +} + +pub fn tokens_or_default(x: Option<&T>, tokens: &mut TokenStream) { + match x { + Some(t) => t.to_tokens(tokens), + None => T::default().to_tokens(tokens), + } +} + +fn parse_inner(input: ParseStream, attrs: &mut Vec) -> syn::Result<()> { + while input.peek(Token![#]) && input.peek2(Token![!]) { + attrs.push(input.call(single_parse_inner)?); + } + Ok(()) +} + +fn single_parse_inner(input: ParseStream) -> syn::Result { + let content; + Ok(Attribute { + pound_token: input.parse()?, + style: syn::AttrStyle::Inner(input.parse()?), + bracket_token: bracketed!(content in input), + meta: content.parse()?, + }) +} + +fn outer(attrs: &[Attribute]) -> impl Iterator { + fn is_outer(attr: &&Attribute) -> bool { + match attr.style { + syn::AttrStyle::Outer => true, + syn::AttrStyle::Inner(_) => false, + } + } + attrs.iter().filter(is_outer) +} + +fn inner(attrs: &[Attribute]) -> impl Iterator { + fn is_inner(attr: &&Attribute) -> bool { + match attr.style { + syn::AttrStyle::Outer => false, + syn::AttrStyle::Inner(_) => true, + } + } + attrs.iter().filter(is_inner) +} diff --git a/crates/soroban-flux-attrs/Cargo.toml b/crates/soroban-flux-attrs/Cargo.toml new file mode 100644 index 0000000..d623cf4 --- /dev/null +++ b/crates/soroban-flux-attrs/Cargo.toml @@ -0,0 +1,22 @@ +[package] +name = "soroban-flux-attrs" +description = "Vendored flux-attrs (github.com/flux-rs/flux, MIT) — the Flux attribute proc-macros; erase to no-ops unless built under the flux driver" +version.workspace = true +edition.workspace = true +license = "MIT" +repository.workspace = true + +[lib] +proc-macro = true + +[dependencies] +# Dependency-renamed so the vendored source stays byte-identical to upstream. +flux-attrs-impl = { package = "soroban-flux-attrs-impl", path = "../soroban-flux-attrs-impl", version = "0.1.0" } + +# Vendored byte-identical upstream source (see VENDORED.md): keep upstream's +# lint posture, never this workspace's. +[lints.rust] +warnings = "allow" + +[lints.clippy] +all = "allow" diff --git a/crates/soroban-flux-attrs/build.rs b/crates/soroban-flux-attrs/build.rs new file mode 100644 index 0000000..4e7fa13 --- /dev/null +++ b/crates/soroban-flux-attrs/build.rs @@ -0,0 +1,6 @@ +fn main() { + println!("cargo:rerun-if-env-changed=FLUX_BUILD_SYSROOT"); + if std::env::var("FLUX_BUILD_SYSROOT").is_ok() { + println!("cargo:rustc-cfg=flux_sysroot"); + } +} diff --git a/crates/soroban-flux-attrs/src/lib.rs b/crates/soroban-flux-attrs/src/lib.rs new file mode 100644 index 0000000..239b822 --- /dev/null +++ b/crates/soroban-flux-attrs/src/lib.rs @@ -0,0 +1,253 @@ +#[cfg(not(flux_sysroot))] +use attr_dummy as attr_impl; +#[cfg(flux_sysroot)] +use attr_sysroot as attr_impl; +use proc_macro::TokenStream; + +#[proc_macro_attribute] +pub fn alias(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::alias(attr, tokens) +} + +#[proc_macro_attribute] +pub fn sig(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::sig(attr, tokens) +} + +#[proc_macro_attribute] +pub fn spec(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::spec(attr, tokens) +} + +#[proc_macro_attribute] +pub fn specs(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::specs(attr, tokens) +} + +#[proc_macro_attribute] +pub fn qualifiers(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::qualifiers(attr, tokens) +} + +#[proc_macro_attribute] +pub fn reveal(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::reveal(attr, tokens) +} + +#[proc_macro_attribute] +pub fn refined_by(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::refined_by(attr, tokens) +} + +#[proc_macro_attribute] +pub fn invariant(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::invariant(attr, tokens) +} + +#[proc_macro_attribute] +pub fn constant(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::constant(attr, tokens) +} + +#[proc_macro_attribute] +pub fn opaque(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::opaque(attr, tokens) +} + +#[proc_macro_attribute] +pub fn reflect(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::reflect(attr, tokens) +} + +#[proc_macro_attribute] +pub fn opts(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::opts(attr, tokens) +} + +#[proc_macro_attribute] +pub fn trusted(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::trusted(attr, tokens) +} + +#[proc_macro_attribute] +pub fn trusted_impl(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::trusted_impl(attr, tokens) +} + +#[proc_macro_attribute] +pub fn trusted_derive(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::trusted_derive(attr, tokens) +} + +#[proc_macro_attribute] +pub fn proven_externally(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::proven_externally(attr, tokens) +} + +#[proc_macro_attribute] +pub fn generics(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::generics(attr, tokens) +} + +#[proc_macro_attribute] +pub fn assoc(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::assoc(attr, tokens) +} + +#[proc_macro] +pub fn flux(tokens: TokenStream) -> TokenStream { + flux_attrs_impl::flux(tokens.into()).into() +} + +#[proc_macro] +pub fn defs(tokens: TokenStream) -> TokenStream { + attr_impl::defs(tokens) +} + +#[proc_macro_attribute] +pub fn extern_spec(attrs: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::extern_spec(attrs, tokens) +} + +#[proc_macro_attribute] +pub fn ignore(attrs: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::ignore(attrs, tokens) +} + +#[proc_macro_attribute] +pub fn should_fail(attrs: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::should_fail(attrs, tokens) +} + +#[proc_macro_attribute] +pub fn no_panic(attrs: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::no_panic(attrs, tokens) +} + +#[proc_macro_attribute] +pub fn no_panic_if(attrs: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::no_panic_if(attrs, tokens) +} + +#[proc_macro_attribute] +pub fn no_suggestions(attrs: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::no_suggestions(attrs, tokens) +} + +#[proc_macro_attribute] +pub fn reft(attrs: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::reft(attrs, tokens) +} + +#[proc_macro_attribute] +pub fn assume_parametric(attrs: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::assume_parametric(attrs, tokens) +} + +#[cfg(flux_sysroot)] +mod attr_sysroot { + use super::*; + + pub fn extern_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream { + flux_attrs_impl::extern_spec(attr.into(), tokens.into()).into() + } + + pub fn refined_by(attr: TokenStream, item: TokenStream) -> TokenStream { + flux_attrs_impl::refined_by(attr.into(), item.into()).into() + } + + pub fn defs(tokens: TokenStream) -> TokenStream { + flux_attrs_impl::defs(tokens.into()).into() + } + + macro_rules! flux_tool_attrs { + ($($name:ident),+ $(,)?) => { + $( + pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { + flux_attrs_impl::flux_tool_item_attr(stringify!($name), attr.into(), item.into()).into() + } + )* + }; + } + + flux_tool_attrs!( + alias, + spec, + specs, + sig, + qualifiers, + reveal, + constant, + invariant, + opaque, + reflect, + opts, + trusted, + trusted_impl, + trusted_derive, + proven_externally, + generics, + assoc, + ignore, + should_fail, + reft, + no_panic, + no_panic_if, + assume_parametric, + no_suggestions, + ); +} + +#[cfg(not(flux_sysroot))] +mod attr_dummy { + use super::*; + + pub fn refined_by(attr: TokenStream, item: TokenStream) -> TokenStream { + flux_attrs_impl::refined_by(attr.into(), item.into()).into() + } + + pub fn defs(_tokens: TokenStream) -> TokenStream { + TokenStream::new() + } + + pub fn extern_spec(_attrs: TokenStream, _tokens: TokenStream) -> TokenStream { + TokenStream::new() + } + + macro_rules! no_op { + ($($name:ident),+ $(,)?) => { + $( + pub fn $name(_attr: TokenStream, item: TokenStream) -> TokenStream { + item + } + )+ + }; + } + + no_op!( + alias, + spec, + specs, + sig, + qualifiers, + reveal, + invariant, + constant, + opaque, + reflect, + opts, + trusted, + trusted_impl, + trusted_derive, + proven_externally, + generics, + assoc, + ignore, + should_fail, + no_panic, + no_panic_if, + no_suggestions, + reft, + assume_parametric, + ); +} diff --git a/crates/soroban-flux-rs/Cargo.toml b/crates/soroban-flux-rs/Cargo.toml new file mode 100644 index 0000000..2d5b86e --- /dev/null +++ b/crates/soroban-flux-rs/Cargo.toml @@ -0,0 +1,22 @@ +[package] +name = "soroban-flux-rs" +description = "Vendored flux-rs (github.com/flux-rs/flux, MIT) — attrs re-export, assert/unreachable intrinsics, bitvec/defs macros" +version.workspace = true +edition.workspace = true +license = "MIT" +repository.workspace = true + +[dependencies] +# Dependency-renamed so the vendored source stays byte-identical to upstream. +flux-attrs = { package = "soroban-flux-attrs", path = "../soroban-flux-attrs", version = "0.1.0" } + +[package.metadata.flux] +enabled = true + +# Vendored byte-identical upstream source (see VENDORED.md): keep upstream's +# lint posture, never this workspace's. +[lints.rust] +warnings = "allow" + +[lints.clippy] +all = "allow" diff --git a/crates/soroban-flux-rs/src/bitvec.rs b/crates/soroban-flux-rs/src/bitvec.rs new file mode 100644 index 0000000..9bc8ed7 --- /dev/null +++ b/crates/soroban-flux-rs/src/bitvec.rs @@ -0,0 +1,451 @@ +use core::{ + cmp::Ordering, + ops::{Add, BitAnd, BitOr, Not, Rem, Shl, Shr, Sub}, +}; + +use flux_attrs::*; + +// ---------------------------------------------------------------------------------------------------------- + +#[derive(Debug, Clone, Copy, Hash)] +#[opaque] +#[refined_by(x: bitvec<32>)] +#[repr(transparent)] +pub struct BV32(u32); + +#[trusted] +impl PartialOrd for BV32 { + fn partial_cmp(&self, other: &Self) -> Option { + self.0.partial_cmp(&other.0) + } + + #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ule(x, y)])] + fn le(&self, other: &Self) -> bool { + self.0 <= other.0 + } + + #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ult(x, y)])] + fn lt(&self, other: &Self) -> bool { + self.0 < other.0 + } + + #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_uge(x, y)])] + fn ge(&self, other: &Self) -> bool { + self.0 >= other.0 + } + + #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ugt(x, y)])] + fn gt(&self, other: &Self) -> bool { + self.0 > other.0 + } +} + +#[trusted] +impl BV32 { + #[sig(fn (u32[@val]) -> BV32[bv_int_to_bv32(val)])] + pub const fn new(value: u32) -> BV32 { + BV32(value) + } + + #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_add(x, y)])] + pub fn wrapping_add(self, other: BV32) -> BV32 { + BV32(self.0.wrapping_add(other.0)) + } +} + +impl From for BV32 { + #[trusted] + #[sig(fn(u32[@val]) -> BV32[bv_int_to_bv32(val)])] + fn from(value: u32) -> BV32 { + BV32(value) + } +} + +impl Into for BV32 { + #[trusted] + #[sig(fn(BV32[@val]) -> u32[bv_bv32_to_int(val)])] + fn into(self) -> u32 { + self.0 + } +} + +impl Not for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x]) -> BV32[bv_not(x)])] + fn not(self) -> BV32 { + BV32(!self.0) + } +} + +impl BitAnd for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_and(x, y)])] + fn bitand(self, rhs: Self) -> BV32 { + BV32(self.0 & rhs.0) + } +} + +impl BitAnd for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x], u32[@y]) -> BV32[bv_and(x, bv_int_to_bv32(y))])] + fn bitand(self, rhs: u32) -> BV32 { + BV32(self.0 & rhs) + } +} + +impl BitOr for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_or(x, y)])] + fn bitor(self, rhs: Self) -> BV32 { + BV32(self.0 | rhs.0) + } +} + +impl BitOr for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x], u32[@y]) -> BV32[bv_or(x, bv_int_to_bv32(y))])] + fn bitor(self, rhs: u32) -> BV32 { + BV32(self.0 | rhs) + } +} + +impl Shl for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_shl(x, y)])] + fn shl(self, rhs: Self) -> BV32 { + BV32(self.0 << rhs.0) + } +} + +impl Shl for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x], u8[@y]) -> BV32[bv_shl(x, bv_int_to_bv32(y))])] + fn shl(self, rhs: u8) -> BV32 { + BV32(self.0 << rhs) + } +} + +impl Shl for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x], u32[@y]) -> BV32[bv_shl(x, bv_int_to_bv32(y))])] + fn shl(self, rhs: u32) -> BV32 { + BV32(self.0 << rhs) + } +} + +impl Shr for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_lshr(x, y)])] + fn shr(self, rhs: Self) -> BV32 { + BV32(self.0 >> rhs.0) + } +} + +impl Shr for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x], u32[@y]) -> BV32[bv_lshr(x, bv_int_to_bv32(y))])] + fn shr(self, rhs: u32) -> BV32 { + BV32(self.0 >> rhs) + } +} + +impl Shr for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x], u8[@y]) -> BV32[bv_lshr(x, bv_int_to_bv32(y))])] + fn shr(self, rhs: u8) -> BV32 { + BV32(self.0 >> rhs) + } +} + +impl Add for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_add(val1, val2)])] + fn add(self, rhs: Self) -> BV32 { + BV32(self.0 + rhs.0) + } +} + +impl Sub for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_sub(val1, val2)])] + fn sub(self, rhs: Self) -> BV32 { + BV32(self.0.wrapping_add(!rhs.0)) + } +} + +impl Rem for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_urem(val1, val2)])] + fn rem(self, rhs: Self) -> BV32 { + BV32(self.0 & rhs.0) + } +} + +#[trusted] +impl PartialEq for BV32 { + #[sig(fn(&BV32[@val1], &BV32[@val2]) -> bool[val1 == val2])] + fn eq(&self, other: &Self) -> bool { + self.0 == other.0 + } + + #[sig(fn(&BV32[@val1], &BV32[@val2]) -> bool[val1 != val2])] + fn ne(&self, other: &Self) -> bool { + self.0 != other.0 + } +} + +#[trusted] +impl PartialEq for BV32 { + #[sig(fn(&BV32[@val1], &u32[@val2]) -> bool[val1 == bv_int_to_bv32(val2)])] + fn eq(&self, other: &u32) -> bool { + self.0 == *other + } + + #[sig(fn(&BV32[@val1], &u32[@val2]) -> bool[val1 != bv_int_to_bv32(val2)])] + fn ne(&self, other: &u32) -> bool { + self.0 != *other + } +} + +impl Eq for BV32 {} + +// ---------------------------------------------------------------------------------------------------------- + +// ---------------------------------------------------------------------------------------------------------- + +#[derive(Debug, Clone, Copy, Hash)] +#[opaque] +#[refined_by(x: bitvec<8>)] +pub struct BV8(u8); + +#[trusted] +impl PartialOrd for BV8 { + fn partial_cmp(&self, other: &Self) -> Option { + self.0.partial_cmp(&other.0) + } + + #[sig(fn(&BV8[@x], &BV8[@y]) -> bool[bv_ule(x, y)])] + fn le(&self, other: &Self) -> bool { + self.0 <= other.0 + } + + #[sig(fn(&BV8[@x], &BV8[@y]) -> bool[bv_ult(x, y)])] + fn lt(&self, other: &Self) -> bool { + self.0 < other.0 + } + + #[sig(fn(&BV8[@x], &BV8[@y]) -> bool[bv_uge(x, y)])] + fn ge(&self, other: &Self) -> bool { + self.0 >= other.0 + } + + #[sig(fn(&BV8[@x], &BV8[@y]) -> bool[bv_ugt(x, y)])] + fn gt(&self, other: &Self) -> bool { + self.0 > other.0 + } +} + +#[trusted] +impl BV8 { + #[sig(fn (u8[@val]) -> BV8[bv_int_to_bv8(val)])] + pub const fn new(value: u8) -> BV8 { + BV8(value) + } + + #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_add(x, y)])] + pub fn wrapping_add(self, other: BV8) -> BV8 { + BV8(self.0.wrapping_add(other.0)) + } +} + +impl From for BV8 { + #[trusted] + #[sig(fn(u8[@val]) -> BV8[bv_int_to_bv8(val)])] + fn from(value: u8) -> BV8 { + BV8(value) + } +} + +impl Into for BV8 { + #[trusted] + #[sig(fn(BV8[@val]) -> u8[bv_bv8_to_int(val)])] + fn into(self) -> u8 { + self.0 + } +} + +impl Not for BV8 { + type Output = BV8; + + #[trusted] + #[sig(fn(BV8[@x]) -> BV8[bv_not(x)])] + fn not(self) -> BV8 { + BV8(!self.0) + } +} + +impl BitAnd for BV8 { + type Output = BV8; + + #[trusted] + #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_and(x, y)])] + fn bitand(self, rhs: Self) -> BV8 { + BV8(self.0 & rhs.0) + } +} + +impl BitAnd for BV8 { + type Output = BV8; + + #[trusted] + #[sig(fn(BV8[@x], u8[@y]) -> BV8[bv_and(x, bv_int_to_bv8(y))])] + fn bitand(self, rhs: u8) -> BV8 { + BV8(self.0 & rhs) + } +} + +impl BitOr for BV8 { + type Output = BV8; + + #[trusted] + #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_or(x, y)])] + fn bitor(self, rhs: Self) -> BV8 { + BV8(self.0 | rhs.0) + } +} + +impl BitOr for BV8 { + type Output = BV8; + + #[trusted] + #[sig(fn(BV8[@x], u8[@y]) -> BV8[bv_or(x, bv_int_to_bv8(y))])] + fn bitor(self, rhs: u8) -> BV8 { + BV8(self.0 | rhs) + } +} + +impl Shl for BV8 { + type Output = BV8; + + #[trusted] + #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_shl(x, y)])] + fn shl(self, rhs: Self) -> BV8 { + BV8(self.0 << rhs.0) + } +} + +impl Shl for BV8 { + type Output = BV8; + + #[trusted] + #[sig(fn(BV8[@x], u8[@y]) -> BV8[bv_shl(x, bv_int_to_bv8(y))])] + fn shl(self, rhs: u8) -> BV8 { + BV8(self.0 << rhs) + } +} + +impl Shr for BV8 { + type Output = BV8; + + #[trusted] + #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_lshr(x, y)])] + fn shr(self, rhs: Self) -> BV8 { + BV8(self.0 >> rhs.0) + } +} + +impl Shr for BV8 { + type Output = BV8; + + #[trusted] + #[sig(fn(BV8[@x], u8[@y]) -> BV8[bv_lshr(x, bv_int_to_bv8(y))])] + fn shr(self, rhs: u8) -> BV8 { + BV8(self.0 >> rhs) + } +} + +impl Add for BV8 { + type Output = BV8; + + #[trusted] + #[sig(fn(BV8[@val1], BV8[@val2]) -> BV8[bv_add(val1, val2)])] + fn add(self, rhs: Self) -> BV8 { + BV8(self.0 + rhs.0) + } +} + +impl Sub for BV8 { + type Output = BV8; + + #[trusted] + #[sig(fn(BV8[@val1], BV8[@val2]) -> BV8[bv_sub(val1, val2)])] + fn sub(self, rhs: Self) -> BV8 { + BV8(self.0.wrapping_add(!rhs.0)) + } +} + +impl Rem for BV8 { + type Output = BV8; + + #[trusted] + #[sig(fn(BV8[@val1], BV8[@val2]) -> BV8[bv_urem(val1, val2)])] + fn rem(self, rhs: Self) -> BV8 { + BV8(self.0 & rhs.0) + } +} + +#[trusted] +impl PartialEq for BV8 { + #[sig(fn(&BV8[@val1], &BV8[@val2]) -> bool[val1 == val2])] + fn eq(&self, other: &Self) -> bool { + self.0 == other.0 + } + + #[sig(fn(&BV8[@val1], &BV8[@val2]) -> bool[val1 != val2])] + fn ne(&self, other: &Self) -> bool { + self.0 != other.0 + } +} + +#[trusted] +impl PartialEq for BV8 { + #[sig(fn(&BV8[@val1], &u8[@val2]) -> bool[val1 == bv_int_to_bv8(val2)])] + fn eq(&self, other: &u8) -> bool { + self.0 == *other + } + + #[sig(fn(&BV8[@val1], &u8[@val2]) -> bool[val1 != bv_int_to_bv8(val2)])] + fn ne(&self, other: &u8) -> bool { + self.0 != *other + } +} + +impl Eq for BV8 {} diff --git a/crates/soroban-flux-rs/src/lib.rs b/crates/soroban-flux-rs/src/lib.rs new file mode 100644 index 0000000..a186cf6 --- /dev/null +++ b/crates/soroban-flux-rs/src/lib.rs @@ -0,0 +1,104 @@ +#![no_std] +#[cfg_attr(flux, flux::no_suggestions)] +pub mod bitvec; + +pub use attrs::*; +pub use flux_attrs as attrs; + +#[no_suggestions] +#[sig(fn(bool[true]) )] +pub fn assert(_: bool) {} + +#[no_suggestions] +#[sig (fn() -> _ requires false)] +pub fn unreachable() -> ! { + unreachable!("impossible case") +} + +/// Macro for creating detached specifications. +/// +/// # Example +/// ``` +/// flux_rs::macros::detached_spec! { +/// fn inc(n:i32) -> i32[n+1]; +/// fn watermelon(n:usize) -> usize[n+2]; +/// } +/// ``` +#[macro_export] +#[doc(hidden)] +macro_rules! __private_detached_spec { + ($($e:tt)*) => { + #[$crate::specs { + $($e)* + }] + const _: () = (); + }; +} + +/// Macro for creating `invariant qualifier`s +/// # Example +/// ``` +/// invariant!(res: int, i: int, n: int ; res + i == n); +/// ``` +#[macro_export] +#[doc(hidden)] +macro_rules! __private_invariant { + ($($param:ident : $ty:ty),* ; $expr:expr) => { + $crate::defs! { + invariant qualifier Auto($($param: $ty),*) { $expr } + } + $crate::assert($expr); + }; +} + +/// Macro for creating `invariant qualifier`s without an assertion. +/// +/// Unlike [`invariant`](crate::macros::invariant), the body is never re-emitted as Rust, so it +/// may use refinement-only syntax. Sorts are inferred; annotate the ones that can't be, using +/// the same `params ; body` syntax as [`invariant`](crate::macros::invariant). +/// +/// # Example +/// ``` +/// flux_rs::macros::qualifier!(my_plus(res, i) == n); +/// flux_rs::macros::qualifier!(res: int, i: int ; res + i == n); +/// ``` +#[macro_export] +#[doc(hidden)] +macro_rules! __private_qualifier { + ($($param:ident : $ty:ty),+ ; $($body:tt)*) => { + $crate::defs! { + invariant qualifier Auto($($param: $ty),+) { $($body)* } + } + }; + ($($body:tt)*) => { + $crate::defs! { + invariant qualifier Auto() { $($body)* } + } + }; +} + +pub mod macros { + /// Macro for creating detached specifications. + /// + /// # Example + /// ``` + /// flux_rs::macros::detached_spec! { + /// fn inc(n:i32) -> i32[n+1]; + /// fn watermelon(n:usize) -> usize[n+2]; + /// } + /// ``` + pub use crate::__private_detached_spec as detached_spec; + /// Macro for creating `invariant qualifier`s + /// # Example + /// ``` + /// flux_rs::macros::invariant!(res: int, i: int, n: int ; res + i == n); + /// ``` + pub use crate::__private_invariant as invariant; + /// Macro for creating a local `invariant qualifier` hint. + /// # Example + /// ``` + /// flux_rs::macros::qualifier!(my_plus(res, i) == n); + /// flux_rs::macros::qualifier!(res: int, i: int ; res + i == n); + /// ``` + pub use crate::__private_qualifier as qualifier; +} diff --git a/justfile b/justfile index 428cf43..ac5dc3e 100644 --- a/justfile +++ b/justfile @@ -18,9 +18,13 @@ flux *ARGS: test: RUSTUP_TOOLCHAIN=stable cargo test --workspace +# fmt/clippy cover only first-party crates: the soroban-flux-attrs*/-rs +# sources are vendored byte-identical from flux-rs/flux (see +# crates/soroban-flux-attrs-impl/VENDORED.md) and deliberately keep +# upstream's formatting and lint posture. check: - RUSTUP_TOOLCHAIN=stable cargo fmt --all --check - RUSTUP_TOOLCHAIN=stable cargo clippy --workspace --all-targets -- -D warnings + RUSTUP_TOOLCHAIN=stable cargo fmt -p soroban-flux -p probe-sdk26 --check + RUSTUP_TOOLCHAIN=stable cargo clippy --workspace --all-targets # One-shot toolchain bootstrap: z3 + liquid-fixpoint prebuilts, then build # cargo-flux/flux-driver from source at FLUX_REV. Idempotent; ~15 min cold. diff --git a/release-plz.toml b/release-plz.toml new file mode 100644 index 0000000..774d4e7 --- /dev/null +++ b/release-plz.toml @@ -0,0 +1,32 @@ +# admin-sep's publish pattern: nothing releases unless opted in per package, +# so the probe crate can never be published by accident. +[workspace] +release = false + +[[package]] +name = "soroban-flux-attrs-impl" +release = true +changelog_update = true +git_tag_enable = true +git_release_enable = true + +[[package]] +name = "soroban-flux-attrs" +release = true +changelog_update = true +git_tag_enable = true +git_release_enable = true + +[[package]] +name = "soroban-flux-rs" +release = true +changelog_update = true +git_tag_enable = true +git_release_enable = true + +[[package]] +name = "soroban-flux" +release = true +changelog_update = true +git_tag_enable = true +git_release_enable = true