feat: Support Verus verification (#759)

Support for Verus verification. Also add a verus github workflow.

Signed-off-by: Jay Lorch <jaylorch@gmail.com>
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
This commit is contained in:
Jay Lorch
2026-07-22 16:21:00 -07:00
committed by GitHub
parent f98865fc98
commit 4c183e931d
12 changed files with 621 additions and 25 deletions

12
.dir-locals.el Normal file
View File

@@ -0,0 +1,12 @@
;;; Directory Local Variables -*- no-byte-compile: t; -*-
;;; For more information see (info "(emacs) Directory Variables")
;; Regorus is a cargo-verus project (package.metadata.verus.verify = true), so
;; verus-mode.el runs `cargo verus verify' rather than the raw `verus' binary.
;; The cargo-verus path ignores `package.metadata.verus.ide.extra_args' and
;; instead reads `verus-cargo-verus-arguments'. We set it here so that Verus is
;; invoked with the `verus' Cargo feature enabled.
;;
;; Everything before `--' is passed to cargo-verus; everything after `--' is
;; forwarded to the Verus binary. The `--' is required by verus-mode.el.
((verus-mode . ((verus-cargo-verus-arguments . ("--features" "verus" "--")))))

80
.github/workflows/verus.yml vendored Executable file
View File

@@ -0,0 +1,80 @@
# Copyright (c) Microsoft Corporation. All rights reserved.
#
name: verus
on:
push:
branches: [ "main" ]
pull_request:
branches: [ "main" ]
env:
CARGO_TERM_COLOR: always
# This workflow only checks out code, downloads a pinned Verus release asset,
# and runs verification. It never writes to the repository, so restrict the
# GITHUB_TOKEN to read-only access to repository contents.
permissions:
contents: read
jobs:
verify:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
- name: Setup Rust toolchain
uses: ./.github/actions/toolchains/rust
with:
components: ""
- name: Cache cargo
uses: Swatinem/rust-cache@c19371144df3bb44fab255c43d04cbc2ab54d1c4 # v2.9.1
with:
shared-key: ${{ runner.os }}-regorus-verus
- name: Install Verus and run verification
shell: bash
run: |
set -euxo pipefail
asset_url=https://github.com/verus-lang/verus/releases/download/release%2F0.2026.07.12.0b42f4c/verus-0.2026.07.12.0b42f4c-x86-linux.zip
asset_sha256=f6f4f5d08e07d3e1ad721d775bda5ba96b9dd0c73b48fc17f2e071866fbd01c0
test -n "$asset_url"
curl -fsSL "$asset_url" -o verus.zip
# Verify the download integrity before trusting/executing its contents.
echo "${asset_sha256} verus.zip" | sha256sum --check --strict
unzip -q verus.zip -d verus-dist
# Search under an absolute path so that `find` yields absolute paths;
# this keeps the PATH entries below valid regardless of the working
# directory.
verus_bin="$(find "$PWD/verus-dist" -type f -name verus -perm -u+x | head -n1)"
cargo_verus_bin="$(find "$PWD/verus-dist" -type f -name cargo-verus -perm -u+x | head -n1)"
version_json="$(find "$PWD/verus-dist" -type f -name version.json | head -n1)"
test -n "$verus_bin"
test -n "$cargo_verus_bin"
test -n "$version_json"
# Verus is built against a specific Rust toolchain and refuses to run
# against any other version. Read the required toolchain from the
# release metadata so we track it automatically instead of hardcoding.
required_toolchain="$(sed -n 's/.*"toolchain"[[:space:]]*:[[:space:]]*"\([^"]*\)".*/\1/p' "$version_json")"
test -n "$required_toolchain"
echo "Verus requires Rust toolchain: $required_toolchain"
# Install the exact toolchain Verus expects, including the extra
# components (rustc-dev, llvm-tools) that Verus links against and that
# are not part of the default rustup profile.
rustup toolchain install "$required_toolchain" \
--profile minimal \
--component rustc-dev --component llvm-tools --component rustfmt
# Force cargo/rustc to resolve to the Verus toolchain for the commands
# below, overriding any repository/directory toolchain override.
export RUSTUP_TOOLCHAIN="$required_toolchain"
# Put cargo-verus on PATH for the commands below.
export PATH="$(dirname "$cargo_verus_bin"):$(dirname "$verus_bin"):$PATH"
cargo verus --help
cargo fetch --locked
cargo verus verify --locked --features verus

89
Cargo.lock generated
View File

@@ -614,6 +614,12 @@ dependencies = [
"zerocopy",
]
[[package]]
name = "hashbrown"
version = "0.12.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
[[package]]
name = "hashbrown"
version = "0.14.5"
@@ -796,6 +802,16 @@ dependencies = [
"icu_properties",
]
[[package]]
name = "indexmap"
version = "1.9.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99"
dependencies = [
"autocfg",
"hashbrown 0.12.3",
]
[[package]]
name = "indexmap"
version = "2.14.0"
@@ -1381,7 +1397,7 @@ dependencies = [
"globset",
"hashbrown 0.17.1",
"icu_casemap",
"indexmap",
"indexmap 2.14.0",
"ipnet",
"jsonschema",
"lazy_static",
@@ -1405,6 +1421,7 @@ dependencies = [
"thiserror",
"url",
"uuid",
"vstd",
"walkdir",
]
@@ -1504,7 +1521,7 @@ version = "0.9.34+deprecated"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
dependencies = [
"indexmap",
"indexmap 2.14.0",
"itoa",
"ryu",
"serde",
@@ -1666,7 +1683,7 @@ version = "0.25.13+spec-1.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6975367e4d2ef766d86af01ffad14b622fecc8d4357a998fbc4deb6e9bacaf9b"
dependencies = [
"indexmap",
"indexmap 2.14.0",
"toml_datetime",
"toml_parser",
"toml_writer",
@@ -1768,12 +1785,76 @@ version = "0.9.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
[[package]]
name = "verus_builtin"
version = "0.0.0-2026-05-17-0151"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "cab9266bfb5cf45a080f425c560b0e0be2bf81194f0e80258990c49c1829d8b9"
[[package]]
name = "verus_builtin_macros"
version = "0.0.0-2026-07-12-0122"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3fb60e3a141ababe618fbdb759f14aa8544f6346a98a44c1e3a7dbe20b1f2892"
dependencies = [
"proc-macro2 1.0.106",
"quote 1.0.46",
"syn 2.0.119",
"synstructure",
"verus_prettyplease",
"verus_syn",
]
[[package]]
name = "verus_prettyplease"
version = "0.0.0-2026-05-31-0205"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3ffdc94c89109a67c59646f6b6e71b49de394020f45294247dd716470523245b"
dependencies = [
"proc-macro2 1.0.106",
"verus_syn",
]
[[package]]
name = "verus_state_machines_macros"
version = "0.0.0-2026-06-14-0213"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6704a9ce586a5027f87933d9a84817411c937804090a9585c28bf335ac37eefc"
dependencies = [
"indexmap 1.9.3",
"proc-macro2 1.0.106",
"quote 1.0.46",
"verus_syn",
]
[[package]]
name = "verus_syn"
version = "0.0.0-2026-05-31-0205"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "030b774330d5ec618691c2cd6fba8bbb13bd538f3884a1143450baec25749706"
dependencies = [
"proc-macro2 1.0.106",
"quote 1.0.46",
"unicode-ident",
]
[[package]]
name = "vsimd"
version = "0.8.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5c3082ca00d5a5ef149bb8b555a72ae84c9c59f7250f013ac822ac2e49b19c64"
[[package]]
name = "vstd"
version = "0.0.0-2026-07-12-0122"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "dd0a0d328e1d6382af99a65f71677cf4b9200ec24e09fcafa7b1a3af8c8f5111"
dependencies = [
"verus_builtin",
"verus_builtin_macros",
"verus_state_machines_macros",
]
[[package]]
name = "walkdir"
version = "2.5.0"
@@ -2087,7 +2168,7 @@ checksum = "2d04a6b5381502aa6087c94c669499eb1602eb9c5e8198e534de571f7154809b"
dependencies = [
"crc32fast",
"flate2",
"indexmap",
"indexmap 2.14.0",
"memchr",
"typed-path",
"zopfli",

View File

@@ -14,6 +14,11 @@ license = "MIT AND Apache-2.0 AND BSD-3-Clause"
repository = "https://github.com/microsoft/regorus"
keywords = ["interpreter", "no_std", "opa", "policy-as-code", "rego"]
# Support verification with Verus, a Rust verifier (https://github.com/verus-lang/verus)
[package.metadata.verus]
verify = true
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[lib]
@@ -21,6 +26,7 @@ doctest = false
[features]
default = ["full-opa", "arc", "rvm"]
verus = ["dep:vstd"]
arc = []
ast = []
@@ -43,7 +49,7 @@ cache = ["dep:lru"]
rvm = ["dep:postcard", "dep:indexmap"]
semver = ["dep:semver"]
allocator-memory-limits = ["std", "mimalloc", "mimalloc/allocator-memory-limits"]
std = ["rand/std", "rand/std_rng", "serde_json/std", "indexmap?/std", "msvc_spectre_libs", "dep:parking_lot" ]
std = ["rand/std", "rand/std_rng", "serde_json/std", "indexmap?/std", "msvc_spectre_libs", "dep:parking_lot", "vstd?/std" ]
time = ["dep:chrono", "dep:chrono-tz"]
uuid = ["dep:uuid"]
urlquery = ["dep:url"]
@@ -134,6 +140,11 @@ mimalloc = { package = "regorus-mimalloc", path = "mimalloc", version = "2.2.7",
indexmap = { version = "2.13.1", default-features = false, features = ["serde"], optional = true }
postcard = { version = "1.1.3", default-features = false, features = ["alloc"], optional = true }
# Verus-related dependencies.
# vstd is enabled via the `verus` feature. In no_std builds only the `alloc` feature is used;
# the crate's `std` feature additionally enables `vstd/std` (matching vstd's default features).
vstd = { version = "=0.0.0-2026-07-12-0122", optional = true, default-features = false, features = ["alloc"] }
[dev-dependencies]
anyhow = "1.0.102"
cfg-if = "1.0.0"
@@ -214,3 +225,7 @@ doctest=false
# RUSTDOCFLAGS="--cfg docsrs" cargo +nightly doc --all-features --no-deps
all-features = true
rustdoc-args = ["--cfg", "docsrs"]
[lints.rust]
# Allow `verus_keep_ghost` configuration flag (used by Verus)
unexpected_cfgs = { level = "warn", check-cfg = ['cfg(verus_keep_ghost)'] }

View File

@@ -115,6 +115,10 @@ public class MemoryGrowthTests
if (i % LogEvery == 0)
{
// Collect transient managed garbage so the working-set delta reflects
// retained (leaked) memory rather than uncollected allocations. A real
// native leak from a missed Dispose() would survive GC and still be caught.
ForceFullGc();
process.Refresh();
var workingSet = process.WorkingSet64;
var managed = GC.GetTotalMemory(false);
@@ -228,6 +232,10 @@ public class MemoryGrowthTests
if (i % LogEvery == 0)
{
// Collect transient managed garbage so the working-set delta reflects
// retained (leaked) memory rather than uncollected allocations. A real
// native leak from a missed Dispose() would survive GC and still be caught.
ForceFullGc();
process.Refresh();
var workingSet = process.WorkingSet64;
var managed = GC.GetTotalMemory(false);

View File

@@ -159,7 +159,7 @@ checksum = "2ecb53484c9c167ba674026b656d8a27d7657a58e6066aa902bfb1a4aa00ae20"
dependencies = [
"clap",
"heck",
"indexmap",
"indexmap 2.14.0",
"log",
"proc-macro2",
"quote",
@@ -472,6 +472,12 @@ dependencies = [
"regex-syntax",
]
[[package]]
name = "hashbrown"
version = "0.12.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
[[package]]
name = "hashbrown"
version = "0.14.5"
@@ -648,6 +654,16 @@ dependencies = [
"icu_properties",
]
[[package]]
name = "indexmap"
version = "1.9.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99"
dependencies = [
"autocfg",
"hashbrown 0.12.3",
]
[[package]]
name = "indexmap"
version = "2.14.0"
@@ -1107,7 +1123,7 @@ dependencies = [
"globset",
"hashbrown 0.17.1",
"icu_casemap",
"indexmap",
"indexmap 2.14.0",
"ipnet",
"jsonschema",
"lazy_static",
@@ -1128,6 +1144,7 @@ dependencies = [
"thiserror",
"url",
"uuid",
"vstd",
]
[[package]]
@@ -1250,7 +1267,7 @@ version = "0.9.34+deprecated"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
dependencies = [
"indexmap",
"indexmap 2.14.0",
"itoa",
"ryu",
"serde",
@@ -1371,7 +1388,7 @@ version = "0.9.12+spec-1.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "cf92845e79fc2e2def6a5d828f0801e29a2f8acc037becc5ab08595c7d5e9863"
dependencies = [
"indexmap",
"indexmap 2.14.0",
"serde_core",
"serde_spanned",
"toml_datetime",
@@ -1472,12 +1489,76 @@ version = "0.9.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
[[package]]
name = "verus_builtin"
version = "0.0.0-2026-05-17-0151"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "cab9266bfb5cf45a080f425c560b0e0be2bf81194f0e80258990c49c1829d8b9"
[[package]]
name = "verus_builtin_macros"
version = "0.0.0-2026-07-12-0122"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3fb60e3a141ababe618fbdb759f14aa8544f6346a98a44c1e3a7dbe20b1f2892"
dependencies = [
"proc-macro2",
"quote",
"syn",
"synstructure",
"verus_prettyplease",
"verus_syn",
]
[[package]]
name = "verus_prettyplease"
version = "0.0.0-2026-05-31-0205"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3ffdc94c89109a67c59646f6b6e71b49de394020f45294247dd716470523245b"
dependencies = [
"proc-macro2",
"verus_syn",
]
[[package]]
name = "verus_state_machines_macros"
version = "0.0.0-2026-06-14-0213"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6704a9ce586a5027f87933d9a84817411c937804090a9585c28bf335ac37eefc"
dependencies = [
"indexmap 1.9.3",
"proc-macro2",
"quote",
"verus_syn",
]
[[package]]
name = "verus_syn"
version = "0.0.0-2026-05-31-0205"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "030b774330d5ec618691c2cd6fba8bbb13bd538f3884a1143450baec25749706"
dependencies = [
"proc-macro2",
"quote",
"unicode-ident",
]
[[package]]
name = "vsimd"
version = "0.8.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5c3082ca00d5a5ef149bb8b555a72ae84c9c59f7250f013ac822ac2e49b19c64"
[[package]]
name = "vstd"
version = "0.0.0-2026-07-12-0122"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "dd0a0d328e1d6382af99a65f71677cf4b9200ec24e09fcafa7b1a3af8c8f5111"
dependencies = [
"verus_builtin",
"verus_builtin_macros",
"verus_state_machines_macros",
]
[[package]]
name = "wasip2"
version = "1.0.4+wasi-0.2.12"

View File

@@ -350,6 +350,12 @@ dependencies = [
"regex-syntax",
]
[[package]]
name = "hashbrown"
version = "0.12.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
[[package]]
name = "hashbrown"
version = "0.17.1"
@@ -488,6 +494,16 @@ dependencies = [
"icu_properties",
]
[[package]]
name = "indexmap"
version = "1.9.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99"
dependencies = [
"autocfg",
"hashbrown 0.12.3",
]
[[package]]
name = "indexmap"
version = "2.14.0"
@@ -495,7 +511,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9"
dependencies = [
"equivalent",
"hashbrown",
"hashbrown 0.17.1",
"serde",
"serde_core",
]
@@ -927,7 +943,7 @@ dependencies = [
"ahash",
"fluent-uri",
"getrandom 0.3.4",
"hashbrown",
"hashbrown 0.17.1",
"itoa",
"micromap",
"parking_lot",
@@ -973,7 +989,7 @@ dependencies = [
"chrono-tz",
"data-encoding",
"globset",
"indexmap",
"indexmap 2.14.0",
"ipnet",
"jsonschema",
"lazy_static",
@@ -994,6 +1010,7 @@ dependencies = [
"thiserror",
"url",
"uuid",
"vstd",
]
[[package]]
@@ -1111,7 +1128,7 @@ version = "0.9.34+deprecated"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
dependencies = [
"indexmap",
"indexmap 2.14.0",
"itoa",
"ryu",
"serde",
@@ -1284,12 +1301,76 @@ version = "0.9.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
[[package]]
name = "verus_builtin"
version = "0.0.0-2026-05-17-0151"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "cab9266bfb5cf45a080f425c560b0e0be2bf81194f0e80258990c49c1829d8b9"
[[package]]
name = "verus_builtin_macros"
version = "0.0.0-2026-07-12-0122"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3fb60e3a141ababe618fbdb759f14aa8544f6346a98a44c1e3a7dbe20b1f2892"
dependencies = [
"proc-macro2",
"quote",
"syn",
"synstructure",
"verus_prettyplease",
"verus_syn",
]
[[package]]
name = "verus_prettyplease"
version = "0.0.0-2026-05-31-0205"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3ffdc94c89109a67c59646f6b6e71b49de394020f45294247dd716470523245b"
dependencies = [
"proc-macro2",
"verus_syn",
]
[[package]]
name = "verus_state_machines_macros"
version = "0.0.0-2026-06-14-0213"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6704a9ce586a5027f87933d9a84817411c937804090a9585c28bf335ac37eefc"
dependencies = [
"indexmap 1.9.3",
"proc-macro2",
"quote",
"verus_syn",
]
[[package]]
name = "verus_syn"
version = "0.0.0-2026-05-31-0205"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "030b774330d5ec618691c2cd6fba8bbb13bd538f3884a1143450baec25749706"
dependencies = [
"proc-macro2",
"quote",
"unicode-ident",
]
[[package]]
name = "vsimd"
version = "0.8.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5c3082ca00d5a5ef149bb8b555a72ae84c9c59f7250f013ac822ac2e49b19c64"
[[package]]
name = "vstd"
version = "0.0.0-2026-07-12-0122"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "dd0a0d328e1d6382af99a65f71677cf4b9200ec24e09fcafa7b1a3af8c8f5111"
dependencies = [
"verus_builtin",
"verus_builtin_macros",
"verus_state_machines_macros",
]
[[package]]
name = "walkdir"
version = "2.5.0"

View File

@@ -334,6 +334,12 @@ dependencies = [
"regex-syntax",
]
[[package]]
name = "hashbrown"
version = "0.12.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
[[package]]
name = "hashbrown"
version = "0.17.1"
@@ -478,6 +484,16 @@ dependencies = [
"icu_properties",
]
[[package]]
name = "indexmap"
version = "1.9.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99"
dependencies = [
"autocfg",
"hashbrown 0.12.3",
]
[[package]]
name = "indexmap"
version = "2.14.0"
@@ -485,7 +501,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9"
dependencies = [
"equivalent",
"hashbrown",
"hashbrown 0.17.1",
"serde",
"serde_core",
]
@@ -941,7 +957,7 @@ dependencies = [
"ahash",
"fluent-uri",
"getrandom 0.3.4",
"hashbrown",
"hashbrown 0.17.1",
"itoa",
"micromap",
"parking_lot",
@@ -987,7 +1003,7 @@ dependencies = [
"chrono-tz",
"data-encoding",
"globset",
"indexmap",
"indexmap 2.14.0",
"ipnet",
"jsonschema",
"lazy_static",
@@ -1008,6 +1024,7 @@ dependencies = [
"thiserror",
"url",
"uuid",
"vstd",
]
[[package]]
@@ -1108,7 +1125,7 @@ version = "0.9.34+deprecated"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
dependencies = [
"indexmap",
"indexmap 2.14.0",
"itoa",
"ryu",
"serde",
@@ -1271,12 +1288,76 @@ version = "0.9.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
[[package]]
name = "verus_builtin"
version = "0.0.0-2026-05-17-0151"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "cab9266bfb5cf45a080f425c560b0e0be2bf81194f0e80258990c49c1829d8b9"
[[package]]
name = "verus_builtin_macros"
version = "0.0.0-2026-07-12-0122"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3fb60e3a141ababe618fbdb759f14aa8544f6346a98a44c1e3a7dbe20b1f2892"
dependencies = [
"proc-macro2",
"quote",
"syn",
"synstructure",
"verus_prettyplease",
"verus_syn",
]
[[package]]
name = "verus_prettyplease"
version = "0.0.0-2026-05-31-0205"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3ffdc94c89109a67c59646f6b6e71b49de394020f45294247dd716470523245b"
dependencies = [
"proc-macro2",
"verus_syn",
]
[[package]]
name = "verus_state_machines_macros"
version = "0.0.0-2026-06-14-0213"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6704a9ce586a5027f87933d9a84817411c937804090a9585c28bf335ac37eefc"
dependencies = [
"indexmap 1.9.3",
"proc-macro2",
"quote",
"verus_syn",
]
[[package]]
name = "verus_syn"
version = "0.0.0-2026-05-31-0205"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "030b774330d5ec618691c2cd6fba8bbb13bd538f3884a1143450baec25749706"
dependencies = [
"proc-macro2",
"quote",
"unicode-ident",
]
[[package]]
name = "vsimd"
version = "0.8.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5c3082ca00d5a5ef149bb8b555a72ae84c9c59f7250f013ac822ac2e49b19c64"
[[package]]
name = "vstd"
version = "0.0.0-2026-07-12-0122"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "dd0a0d328e1d6382af99a65f71677cf4b9200ec24e09fcafa7b1a3af8c8f5111"
dependencies = [
"verus_builtin",
"verus_builtin_macros",
"verus_state_machines_macros",
]
[[package]]
name = "wasip2"
version = "1.0.4+wasi-0.2.12"

View File

@@ -501,6 +501,16 @@ dependencies = [
"icu_properties",
]
[[package]]
name = "indexmap"
version = "1.9.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99"
dependencies = [
"autocfg",
"hashbrown 0.12.3",
]
[[package]]
name = "indexmap"
version = "2.14.0"
@@ -1013,7 +1023,7 @@ dependencies = [
"chrono-tz",
"data-encoding",
"globset",
"indexmap",
"indexmap 2.14.0",
"ipnet",
"jsonschema",
"lazy_static",
@@ -1033,6 +1043,7 @@ dependencies = [
"thiserror",
"url",
"uuid",
"vstd",
]
[[package]]
@@ -1156,7 +1167,7 @@ version = "0.9.34+deprecated"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
dependencies = [
"indexmap",
"indexmap 2.14.0",
"itoa",
"ryu",
"serde",
@@ -1331,12 +1342,70 @@ version = "0.9.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
[[package]]
name = "verus_builtin"
version = "0.0.0-2026-05-17-0151"
source = "git+https://github.com/verus-lang/verus.git#60c8383d70074f6c00d754b4fb47438995fcb79a"
[[package]]
name = "verus_builtin_macros"
version = "0.0.0-2026-06-14-0213"
source = "git+https://github.com/verus-lang/verus.git#60c8383d70074f6c00d754b4fb47438995fcb79a"
dependencies = [
"proc-macro2",
"quote",
"syn",
"synstructure",
"verus_prettyplease",
"verus_syn",
]
[[package]]
name = "verus_prettyplease"
version = "0.0.0-2026-05-31-0205"
source = "git+https://github.com/verus-lang/verus.git#60c8383d70074f6c00d754b4fb47438995fcb79a"
dependencies = [
"proc-macro2",
"verus_syn",
]
[[package]]
name = "verus_state_machines_macros"
version = "0.0.0-2026-06-14-0213"
source = "git+https://github.com/verus-lang/verus.git#60c8383d70074f6c00d754b4fb47438995fcb79a"
dependencies = [
"indexmap 1.9.3",
"proc-macro2",
"quote",
"verus_syn",
]
[[package]]
name = "verus_syn"
version = "0.0.0-2026-05-31-0205"
source = "git+https://github.com/verus-lang/verus.git#60c8383d70074f6c00d754b4fb47438995fcb79a"
dependencies = [
"proc-macro2",
"quote",
"unicode-ident",
]
[[package]]
name = "vsimd"
version = "0.8.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5c3082ca00d5a5ef149bb8b555a72ae84c9c59f7250f013ac822ac2e49b19c64"
[[package]]
name = "vstd"
version = "0.0.0-2026-06-14-0213"
source = "git+https://github.com/verus-lang/verus.git#60c8383d70074f6c00d754b4fb47438995fcb79a"
dependencies = [
"verus_builtin",
"verus_builtin_macros",
"verus_state_machines_macros",
]
[[package]]
name = "wasip2"
version = "1.0.4+wasi-0.2.12"

View File

@@ -366,6 +366,12 @@ dependencies = [
"regex-syntax",
]
[[package]]
name = "hashbrown"
version = "0.12.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
[[package]]
name = "hashbrown"
version = "0.17.1"
@@ -504,6 +510,16 @@ dependencies = [
"icu_properties",
]
[[package]]
name = "indexmap"
version = "1.9.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99"
dependencies = [
"autocfg",
"hashbrown 0.12.3",
]
[[package]]
name = "indexmap"
version = "2.14.0"
@@ -511,7 +527,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9"
dependencies = [
"equivalent",
"hashbrown",
"hashbrown 0.17.1",
"serde",
"serde_core",
]
@@ -926,7 +942,7 @@ dependencies = [
"ahash",
"fluent-uri",
"getrandom 0.3.4",
"hashbrown",
"hashbrown 0.17.1",
"itoa",
"micromap",
"parking_lot",
@@ -972,7 +988,7 @@ dependencies = [
"chrono-tz",
"data-encoding",
"globset",
"indexmap",
"indexmap 2.14.0",
"ipnet",
"jsonschema",
"lazy_static",
@@ -992,6 +1008,7 @@ dependencies = [
"thiserror",
"url",
"uuid",
"vstd",
]
[[package]]
@@ -1103,7 +1120,7 @@ version = "0.9.34+deprecated"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
dependencies = [
"indexmap",
"indexmap 2.14.0",
"itoa",
"ryu",
"serde",
@@ -1262,12 +1279,76 @@ version = "0.9.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
[[package]]
name = "verus_builtin"
version = "0.0.0-2026-05-17-0151"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "cab9266bfb5cf45a080f425c560b0e0be2bf81194f0e80258990c49c1829d8b9"
[[package]]
name = "verus_builtin_macros"
version = "0.0.0-2026-07-12-0122"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3fb60e3a141ababe618fbdb759f14aa8544f6346a98a44c1e3a7dbe20b1f2892"
dependencies = [
"proc-macro2",
"quote",
"syn",
"synstructure",
"verus_prettyplease",
"verus_syn",
]
[[package]]
name = "verus_prettyplease"
version = "0.0.0-2026-05-31-0205"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3ffdc94c89109a67c59646f6b6e71b49de394020f45294247dd716470523245b"
dependencies = [
"proc-macro2",
"verus_syn",
]
[[package]]
name = "verus_state_machines_macros"
version = "0.0.0-2026-06-14-0213"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6704a9ce586a5027f87933d9a84817411c937804090a9585c28bf335ac37eefc"
dependencies = [
"indexmap 1.9.3",
"proc-macro2",
"quote",
"verus_syn",
]
[[package]]
name = "verus_syn"
version = "0.0.0-2026-05-31-0205"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "030b774330d5ec618691c2cd6fba8bbb13bd538f3884a1143450baec25749706"
dependencies = [
"proc-macro2",
"quote",
"unicode-ident",
]
[[package]]
name = "vsimd"
version = "0.8.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5c3082ca00d5a5ef149bb8b555a72ae84c9c59f7250f013ac822ac2e49b19c64"
[[package]]
name = "vstd"
version = "0.0.0-2026-07-12-0122"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "dd0a0d328e1d6382af99a65f71677cf4b9200ec24e09fcafa7b1a3af8c8f5111"
dependencies = [
"verus_builtin",
"verus_builtin_macros",
"verus_state_machines_macros",
]
[[package]]
name = "walkdir"
version = "2.5.0"

View File

@@ -27,10 +27,14 @@ use num_traits::{One, Signed, ToPrimitive, Zero};
use serde::ser::Serializer;
use serde::Serialize;
#[cfg(feature = "verus")]
use vstd::prelude::*;
use crate::*;
pub type BigInt = NumBigInt;
#[cfg_attr(feature = "verus", verus_verify)]
const F64_SAFE_INTEGER: f64 = 9_007_199_254_740_992.0; // 2^53
#[derive(Clone)]
@@ -145,8 +149,8 @@ impl Number {
}
fn normalize_float(value: f64) -> Number {
if let Some(int) = Self::float_to_small_bigint(value) {
return Self::from_bigint_owned(int);
if let Some(i) = Self::float_to_small_bigint(value) {
return Self::from_bigint_owned(i);
}
Number::Float(value)
}
@@ -685,6 +689,7 @@ impl Number {
}
}
#[allow(clippy::if_then_some_else_none)]
fn ensure_integers(a: &Number, b: &Number) -> Option<(BigInt, BigInt)> {
if a.is_integer() && b.is_integer() {
Some((a.to_bigint_owned()?, b.to_bigint_owned()?))

View File

@@ -226,6 +226,7 @@ impl RegoVM {
}
}
#[allow(clippy::if_then_some_else_none)]
fn execute_comprehension_yield_run_to_completion(
&mut self,
value_reg: u8,
@@ -332,6 +333,7 @@ impl RegoVM {
Ok(())
}
#[allow(clippy::if_then_some_else_none)]
fn execute_comprehension_yield_suspendable(
&mut self,
value_reg: u8,