fix: Prevent panic by Number::modulo (#773 )

In Number::modulo, it calls Number::ints_to_bigint, which could panic. The reason is that calling .to_integer() isn't enough to guarantee that .to_bigint_owned() will return Some, but Number::ints_to_bigint assumes it will and calls unwrap(). In particular, it might be that it's a float corresponding to an integer that's larger than F64_SAFE_INTEGER. The fix is to not call Number::ints_to_bigint (and indeed to delete that entire function, which is only used in this one place), and instead only call unwrap when Some is returned.
fix: Handle i64::MIN / -1 special case
2026-08-05 02:16:11 +00:00 · 2026-07-27 14:06:42 -05:00 · 2026-07-27 12:22:28 -05:00 · 2026-07-24 18:19:20 -07:00 · 2026-07-24 10:13:24 -05:00 · 2026-07-24 10:12:43 -05:00
42 changed files with 2251 additions and 482 deletions
--- a/.dir-locals.el
+++ b/.dir-locals.el
@@ -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" "--")))))
--- a/.github/workflows/codeql.yml
+++ b/.github/workflows/codeql.yml
@@ -62,7 +62,7 @@ jobs:

    steps:
    - name: Checkout repository
-      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1

    # Setup language-specific dependencies BEFORE CodeQL init for proper tracing setup
    - name: Setup Rust
@@ -86,26 +86,26 @@ jobs:

    - name: Setup Python
      if: matrix.language == 'python'
-      uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
+      uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0
      with:
        python-version: '3.10'

    - name: Setup Java
      if: matrix.language == 'java-kotlin'
-      uses: actions/setup-java@be666c2fcd27ec809703dec50e508c2fdc7f6654 # v5.2.0
+      uses: actions/setup-java@03ad4de0992f5dab5e18fcb136590ce7c4a0ac95 # v5.6.0
      with:
        distribution: 'corretto'
        java-version: '8'

    - name: Setup Go
      if: matrix.language == 'go'
-      uses: actions/setup-go@4a3601121dd01d1626a1e23e37211e3254c1c06c # v6.4.0
+      uses: actions/setup-go@b7ad1dad31e06c5925ef5d2fc7ad053ef454303e # v7.0.0
      with:
        go-version: '1.21'

    - name: Setup .NET
      if: matrix.language == 'csharp'
-      uses: actions/setup-dotnet@c2fa09f4bde5ebb9d1777cf28262a3eb3db3ced7 # v5.2.0
+      uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
      with:
        global-json-file: ./bindings/csharp/global.json

@@ -115,12 +115,12 @@ jobs:

    - name: Setup Node.js
      if: matrix.language == 'javascript-typescript'
-      uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v6.4.0
+      uses: actions/setup-node@820762786026740c76f36085b0efc47a31fe5020 # v7.0.0
      with:
        node-version: '18'

    - name: Initialize CodeQL
-      uses: github/codeql-action/init@95e58e9a2cdfd71adc6e0353d5c52f41a045d225 # v4.35.2
+      uses: github/codeql-action/init@e4fba868fa4b1b91e1fdab776edc8cfbe6e9fb81 # v4.37.3
      with:
        languages: ${{ matrix.language }}
        build-mode: ${{ matrix.build-mode }}
@@ -141,7 +141,7 @@ jobs:

    - name: Setup Ruby
      if: matrix.language == 'rust' && contains(matrix.working-directory, 'ruby')
-      uses: ruby/setup-ruby@c4e5b1316158f92e3d49443a9d58b31d25ac0f8f # v1.306.0
+      uses: ruby/setup-ruby@95ef2b042f9d7a56d8268cba8559e2842e2ad01b # v1.321.0
      with:
        ruby-version: '3.4.2'
        bundler-cache: true
@@ -188,6 +188,6 @@ jobs:
      run: cargo xtask build-wasm --release

    - name: Perform CodeQL Analysis
-      uses: github/codeql-action/analyze@95e58e9a2cdfd71adc6e0353d5c52f41a045d225 # v4.35.2
+      uses: github/codeql-action/analyze@e4fba868fa4b1b91e1fdab776edc8cfbe6e9fb81 # v4.37.3
      with:
        category: "/language:${{matrix.language}}"
--- a/.github/workflows/dependabot-refresh-cargo-lockfiles.yml
+++ b/.github/workflows/dependabot-refresh-cargo-lockfiles.yml
@@ -33,7 +33,7 @@ jobs:
      # ONLY cargo update and cargo metadata (which do NOT execute build
      # scripts) may run against this checkout. Do NOT add cargo build/check/
      # test/run steps.
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v4.2.2
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v4.2.2
        with:
          repository: ${{ github.event.pull_request.head.repo.full_name }}
          ref: ${{ github.event.pull_request.head.sha }}
--- a/.github/workflows/dependency-audit.yml
+++ b/.github/workflows/dependency-audit.yml
@@ -27,7 +27,7 @@ jobs:
          - bindings/wasm/Cargo.lock
    steps:
      - name: Checkout repository
-        uses: actions/checkout@v6
+        uses: actions/checkout@v7

      - name: Run cargo audit
        uses: rustsec/audit-check@v2
@@ -53,7 +53,7 @@ jobs:
          - xtask/Cargo.toml
    steps:
      - name: Checkout repository
-        uses: actions/checkout@v6
+        uses: actions/checkout@v7

      - name: Setup Rust
        uses: ./.github/actions/toolchains/rust
--- a/.github/workflows/feature-matrix.yml
+++ b/.github/workflows/feature-matrix.yml
@@ -67,7 +67,7 @@ jobs:
            features: arc,opa-no-std

    steps:
-    - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+    - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
    - name: Setup Rust toolchain
      uses: ./.github/actions/toolchains/rust
    - name: Cache cargo
--- a/.github/workflows/miri.yml
+++ b/.github/workflows/miri.yml
@@ -14,7 +14,7 @@ jobs:
      MIRIFLAGS: "-Zmiri-disable-isolation"
    steps:
      - name: Checkout repository
-        uses: actions/checkout@v6
+        uses: actions/checkout@v7
      - uses: ./.github/actions/toolchains/rust
        with:
          toolchain: nightly
--- a/.github/workflows/pr-extensions.yml
+++ b/.github/workflows/pr-extensions.yml
@@ -20,7 +20,7 @@ jobs:
    runs-on: ubuntu-latest

    steps:
-    - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+    - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
    - name: Setup Rust toolchain
      uses: ./.github/actions/toolchains/rust
    - name: Cache cargo
--- a/.github/workflows/pr.yml
+++ b/.github/workflows/pr.yml
@@ -20,7 +20,7 @@ jobs:
    runs-on: ubuntu-latest

    steps:
-    - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+    - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
    - name: Setup Rust toolchain
      uses: ./.github/actions/toolchains/rust
    - name: Cache cargo
--- a/.github/workflows/publish-java.yml
+++ b/.github/workflows/publish-java.yml
@@ -35,10 +35,10 @@ jobs:
            os: windows-latest
            extension: dll
    steps:
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0
-      - uses: actions/setup-java@be666c2fcd27ec809703dec50e508c2fdc7f6654 # v5.2.0
+      - uses: actions/setup-java@03ad4de0992f5dab5e18fcb136590ce7c4a0ac95 # v5.6.0
        with:
          java-version: 8
          distribution: "corretto"
@@ -46,7 +46,7 @@ jobs:
        with:
          targets: ${{ matrix.target }}
      - if: ${{ matrix.build_cmd == 'zigbuild' }}
-        uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
+        uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0
        with:
          python-version: "3.11"
      - if: ${{ matrix.build_cmd == 'zigbuild' }}
@@ -66,10 +66,10 @@ jobs:
    runs-on: ubuntu-latest
    needs: build
    steps:
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0
-      - uses: actions/setup-java@be666c2fcd27ec809703dec50e508c2fdc7f6654 # v5.2.0
+      - uses: actions/setup-java@03ad4de0992f5dab5e18fcb136590ce7c4a0ac95 # v5.6.0
        with:
          java-version: 8
          distribution: "corretto"
--- a/.github/workflows/publish-python.yml
+++ b/.github/workflows/publish-python.yml
@@ -20,8 +20,8 @@ jobs:
      matrix:
        target: [x86_64, x86, aarch64, armv7, s390x, ppc64le]
    steps:
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
-      - uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0
        with:
          python-version: '3.10'
      - uses: ./.github/actions/toolchains/rust
@@ -52,8 +52,8 @@ jobs:
      matrix:
        target: [x64, x86]
    steps:
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
-      - uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0
        with:
          python-version: '3.10'
          architecture: ${{ matrix.target }}
@@ -84,8 +84,8 @@ jobs:
      matrix:
        target: [x86_64, aarch64, universal2-apple-darwin]
    steps:
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
-      - uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0
        with:
          python-version: '3.10'
      - uses: ./.github/actions/toolchains/rust
--- a/.github/workflows/publish-wasm.yml
+++ b/.github/workflows/publish-wasm.yml
@@ -15,11 +15,11 @@ jobs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0
      # Setup .npmrc file to publish to npm
-      - uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v6.4.0
+      - uses: actions/setup-node@820762786026740c76f36085b0efc47a31fe5020 # v7.0.0
        with:
          node-version: '20.x'
          registry-url: 'https://registry.npmjs.org'
--- a/.github/workflows/release-plz.yml
+++ b/.github/workflows/release-plz.yml
@@ -17,13 +17,13 @@ jobs:
      contents: write
    steps:
      - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0
      - name: Install Rust toolchain
        uses: ./.github/actions/toolchains/rust
      - name: Run release-plz
-        uses: MarcoIeni/release-plz-action@1528104d2ca23787631a1c1f022abb64b34c1e11 # v0.5.128
+        uses: MarcoIeni/release-plz-action@2eb1d8bcb770b4c48ccfaad919734b38b51958c9 # v0.5.131
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
          CARGO_REGISTRY_TOKEN: ${{ secrets.CARGO_REGISTRY_TOKEN }}
--- a/.github/workflows/rust-clippy.yml
+++ b/.github/workflows/rust-clippy.yml
@@ -32,7 +32,7 @@ jobs:
      actions: read # only required for a private repository by github/codeql-action/upload-sarif to get the Action run status
    steps:
      - name: Checkout code
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1

      - name: Setup Rust toolchain
        uses: ./.github/actions/toolchains/rust
@@ -52,7 +52,7 @@ jobs:

      - name: Upload analysis results to GitHub
        if: ${{ hashFiles('rust-clippy-results.sarif') != '' }}
-        uses: github/codeql-action/upload-sarif@95e58e9a2cdfd71adc6e0353d5c52f41a045d225 # v3.29.11
+        uses: github/codeql-action/upload-sarif@e4fba868fa4b1b91e1fdab776edc8cfbe6e9fb81 # v3.29.11
        with:
          sarif_file: rust-clippy-results.sarif
          wait-for-processing: true
--- a/.github/workflows/test-c-cpp.yml
+++ b/.github/workflows/test-c-cpp.yml
@@ -16,7 +16,7 @@ jobs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0

--- a/.github/workflows/test-csharp.yml
+++ b/.github/workflows/test-csharp.yml
@@ -39,7 +39,7 @@ jobs:
              **/release/libregorus_ffi.dylib
    steps:
      - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0
      - uses: ./.github/actions/toolchains/rust
@@ -73,11 +73,11 @@ jobs:
    needs: build-ffi
    steps:
      - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0  
      - uses: ./.github/actions/toolchains/rust
-      - uses: actions/setup-dotnet@c2fa09f4bde5ebb9d1777cf28262a3eb3db3ced7 # v5.2.0
+      - uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
        with:
          global-json-file: ./bindings/csharp/global.json

@@ -131,13 +131,13 @@ jobs:
            target: aarch64-apple-darwin
    steps:
      - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0

      - uses: ./.github/actions/toolchains/rust

-      - uses: actions/setup-dotnet@c2fa09f4bde5ebb9d1777cf28262a3eb3db3ced7 # v5.2.0
+      - uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
        with:
          global-json-file: ./bindings/csharp/global.json

--- a/.github/workflows/test-ffi.yml
+++ b/.github/workflows/test-ffi.yml
@@ -16,7 +16,7 @@ jobs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0
      - uses: ./.github/actions/toolchains/rust
--- a/.github/workflows/test-go.yml
+++ b/.github/workflows/test-go.yml
@@ -16,7 +16,7 @@ jobs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0
      - uses: ./.github/actions/toolchains/rust
@@ -30,7 +30,7 @@ jobs:
      - name: Fetch FFI crate dependencies
        run: cargo fetch --locked --manifest-path bindings/ffi/Cargo.toml

-      - uses: actions/setup-go@4a3601121dd01d1626a1e23e37211e3254c1c06c # v6.4.0
+      - uses: actions/setup-go@b7ad1dad31e06c5925ef5d2fc7ad053ef454303e # v7.0.0
        with:
          architecture: x64

--- a/.github/workflows/test-java.yml
+++ b/.github/workflows/test-java.yml
@@ -16,11 +16,11 @@ jobs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0

-      - uses: actions/setup-java@be666c2fcd27ec809703dec50e508c2fdc7f6654 # v5.2.0
+      - uses: actions/setup-java@03ad4de0992f5dab5e18fcb136590ce7c4a0ac95 # v5.6.0
        with:
          java-version: 8
          distribution: "corretto"
--- a/.github/workflows/test-musl.yml
+++ b/.github/workflows/test-musl.yml
@@ -20,7 +20,7 @@ jobs:
    runs-on: ubuntu-latest

    steps:
-    - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+    - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
    - uses: ./.github/actions/toolchains/rust
      with:
        targets: x86_64-unknown-linux-musl
--- a/.github/workflows/test-no-std.yml
+++ b/.github/workflows/test-no-std.yml
@@ -20,7 +20,7 @@ jobs:
    runs-on: ubuntu-latest

    steps:
-    - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+    - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
    - uses: ./.github/actions/toolchains/rust
      with:
        targets: thumbv7m-none-eabi
--- a/.github/workflows/test-python.yml
+++ b/.github/workflows/test-python.yml
@@ -23,7 +23,7 @@ jobs:
    runs-on: ${{ matrix.host.name }}
    steps:
      - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0
      - uses: ./.github/actions/toolchains/rust
@@ -39,7 +39,7 @@ jobs:
      - name: Fetch Python crate dependencies
        run: cargo fetch --locked --manifest-path bindings/python/Cargo.toml --target ${{ matrix.host.target }}

-      - uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0
        with:
          python-version: "3.10"
          architecture: x64
@@ -68,7 +68,7 @@ jobs:
    runs-on: ${{ matrix.host.name }}
    steps:
      - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0
      - uses: ./.github/actions/toolchains/rust
@@ -82,7 +82,7 @@ jobs:
      - name: Fetch Python crate dependencies
        run: cargo fetch --locked --manifest-path bindings/python/Cargo.toml

-      - uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0
        with:
          python-version: ${{ matrix.python-version }}
          architecture: x64
--- a/.github/workflows/test-ruby.yml
+++ b/.github/workflows/test-ruby.yml
@@ -14,7 +14,7 @@ jobs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0

--- a/.github/workflows/test-wasm.yml
+++ b/.github/workflows/test-wasm.yml
@@ -16,7 +16,7 @@ jobs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          fetch-depth: 0

@@ -33,7 +33,7 @@ jobs:
        run: cargo fetch --locked --manifest-path bindings/wasm/Cargo.toml

      - name: Setup Node
-        uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v6.4.0
+        uses: actions/setup-node@820762786026740c76f36085b0efc47a31fe5020 # v7.0.0
        with:
          node-version: 22

--- a/.github/workflows/tests-debug.yml
+++ b/.github/workflows/tests-debug.yml
@@ -20,7 +20,7 @@ jobs:
    runs-on: ubuntu-latest

    steps:
-    - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+    - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
    - name: Setup Rust toolchain
      uses: ./.github/actions/toolchains/rust
    - name: Cache cargo
--- a/.github/workflows/verus.yml
+++ b/.github/workflows/verus.yml
@@ -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@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+    - 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
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -113,9 +113,9 @@ dependencies = [

 [[package]]
 name = "anyhow"
-version = "1.0.103"
+version = "1.0.104"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2a4385e2e34eb35d6b3efe798b9eb88096925d87726c0798709bf56d9ed84af3"
+checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470"

 [[package]]
 name = "autocfg"
@@ -180,9 +180,9 @@ checksum = "37b2a672a2cb129a2e41c10b1224bb368f9f37a2b16b612598138befd7b37eb5"

 [[package]]
 name = "cc"
-version = "1.2.67"
+version = "1.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e17dd265a7d0f31ef544e1b20e03add05d3b45b491b633b10d67145d2acc1a38"
+checksum = "c89588d05638b5b4594a3348a2d6c20277e43a7f5c5202b05cc56888475a47b8"
 dependencies = [
 "find-msvc-tools",
 "shlex",
@@ -257,9 +257,9 @@ dependencies = [

 [[package]]
 name = "clap"
-version = "4.6.2"
+version = "4.6.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dd059f9da4f5c36b3787f65d38ccaab1cc315f07b01f89abc8359ee6a8205011"
+checksum = "d91e0c145792ef73a6ad36d27c75ac09f1832222a3c209689d90f534685ee5b7"
 dependencies = [
 "clap_builder",
 "clap_derive",
@@ -279,14 +279,14 @@ dependencies = [

 [[package]]
 name = "clap_derive"
-version = "4.6.1"
+version = "4.6.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f2ce8604710f6733aa641a2b3731eaa1e8b3d9973d5e3565da11800813f997a9"
+checksum = "d012d2b9d65aca7f18f4d9878a045bc17899bba951561ba5ec3c2ba1eed9a061"
 dependencies = [
 "heck",
- "proc-macro2 1.0.106",
- "quote 1.0.46",
- "syn 2.0.119",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
+ "syn 3.0.3",
 ]

 [[package]]
@@ -426,8 +426,8 @@ version = "0.2.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "1ac70aa55017e108007fbaf5aa0f54b021c98f92ff8af59d42eda9da96e3dd4f"
 dependencies = [
- "proc-macro2 1.0.106",
- "quote 1.0.46",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
 "syn 2.0.119",
 ]

@@ -537,21 +537,21 @@ dependencies = [

 [[package]]
 name = "futures-core"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7e3450815272ef58cec6d564423f6e755e25379b217b0bc688e295ba24df6b1d"
+checksum = "2cd50c473c80f6d7c3670a752354b8e569b1a7cbfdc0419ec88e5edad85e0dc7"

 [[package]]
 name = "futures-task"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "037711b3d59c33004d3856fbdc83b99d4ff37a24768fa1be9ce3538a1cde4393"
+checksum = "b231ed28831efb4a61a08580c4bc233ec56bc009f4cd8f52da2c3cb97df0c109"

 [[package]]
 name = "futures-util"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "389ca41296e6190b48053de0321d02a77f32f8a5d2461dd38762c0593805c6d6"
+checksum = "a77a90a256fce34da66415271e30f94ee91c57b04b8a2c042d9cf3220179deaa"
 dependencies = [
 "futures-core",
 "futures-task",
@@ -587,9 +587,9 @@ dependencies = [

 [[package]]
 name = "glob"
-version = "0.3.3"
+version = "0.3.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0cc23270f6e1808e30a928bdc84dea0b9b4136a8bc82338574f23baf47bbd280"
+checksum = "e4eba85ea1d0a966a983acd07deee566e67395d2d96b6fb39e62b5a833f1eb0b"

 [[package]]
 name = "globset"
@@ -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"
@@ -848,9 +864,9 @@ dependencies = [

 [[package]]
 name = "jsonschema"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "281c43ff06dcb331e9356d30e38853d559ce3d0a3f693e0b0e102667dec14fb1"
+checksum = "f05a6cff806294a7699d48761d4ae2bdebab7fa2eef05e4a0b83320f0ff46901"
 dependencies = [
 "ahash",
 "bytecount",
@@ -862,6 +878,7 @@ dependencies = [
 "idna",
 "itoa",
 "jsonschema-regex",
+ "jsonschema-value",
 "num-cmp",
 "num-traits",
 "percent-encoding",
@@ -869,19 +886,34 @@ dependencies = [
 "regex",
 "serde",
 "serde_json",
+ "strum",
 "unicode-general-category",
 "uuid-simd",
 ]

 [[package]]
 name = "jsonschema-regex"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ee0b351864e7ffbc5db9273daf7fa1b4d5177b0946713d667ca571b83c0b4045"
+checksum = "84708dd3f6c5327478a96f37378adb27deed6a626cf84d19de780d9e8ae84b17"
 dependencies = [
 "regex-syntax",
 ]

+[[package]]
+name = "jsonschema-value"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fd8c04ab4ce60e42c4e302d3bd9d184652bb56f212495d2eea23573bcbf72556"
+dependencies = [
+ "ahash",
+ "bytecount",
+ "fraction",
+ "num-cmp",
+ "num-traits",
+ "serde_json",
+]
+
 [[package]]
 name = "lazy_static"
 version = "1.5.0"
@@ -893,9 +925,9 @@ dependencies = [

 [[package]]
 name = "libc"
-version = "0.2.186"
+version = "0.2.189"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66"
+checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2"

 [[package]]
 name = "litemap"
@@ -1217,9 +1249,9 @@ dependencies = [

 [[package]]
 name = "proc-macro2"
-version = "1.0.106"
+version = "1.0.107"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
 dependencies = [
 "unicode-ident",
 ]
@@ -1235,11 +1267,11 @@ dependencies = [

 [[package]]
 name = "quote"
-version = "1.0.46"
+version = "1.0.47"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dfbc457d0c7a0759a614551b11a6409e5951f6c7537be1f1b7682b9ae9230368"
+checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
 dependencies = [
- "proc-macro2 1.0.106",
+ "proc-macro2 1.0.107",
 ]

 [[package]]
@@ -1302,29 +1334,29 @@ dependencies = [

 [[package]]
 name = "ref-cast"
-version = "1.0.25"
+version = "1.0.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f354300ae66f76f1c85c5f84693f0ce81d747e2c3f21a45fef496d89c960bf7d"
+checksum = "216e8f773d7923bcba9ceb86a86c93cabb3903a11872fc3f138c49630e50b96d"
 dependencies = [
 "ref-cast-impl",
 ]

 [[package]]
 name = "ref-cast-impl"
-version = "1.0.25"
+version = "1.0.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7186006dcb21920990093f30e3dea63b7d6e977bf1256be20c3563a5db070da"
+checksum = "2c9283685feec7d69af75fb0e858d5e7378f33fe4fc699383b2916ab9273e03c"
 dependencies = [
- "proc-macro2 1.0.106",
- "quote 1.0.46",
- "syn 2.0.119",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
+ "syn 3.0.3",
 ]

 [[package]]
 name = "referencing"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "348e860aeb0b7bd035778fd11dd9cd5290d32e4aed3b8f2274a00287a9fd362b"
+checksum = "980e77f5cfffc592c0e7dfb6d20770a0b96a6ab94d403de7454ed9799505e4ba"
 dependencies = [
 "ahash",
 "fluent-uri",
@@ -1381,7 +1413,7 @@ dependencies = [
 "globset",
 "hashbrown 0.17.1",
 "icu_casemap",
- "indexmap",
+ "indexmap 2.14.0",
 "ipnet",
 "jsonschema",
 "lazy_static",
@@ -1405,6 +1437,7 @@ dependencies = [
 "thiserror",
 "url",
 "uuid",
+ "vstd",
 "walkdir",
 ]

@@ -1457,9 +1490,9 @@ checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd"

 [[package]]
 name = "serde"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e"
+checksum = "4148590afebada386688f18773da617792bf2ef03ffc1e4cbd2b1d45b023e0ba"
 dependencies = [
 "serde_core",
 "serde_derive",
@@ -1467,29 +1500,29 @@ dependencies = [

 [[package]]
 name = "serde_core"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad"
+checksum = "67dca2c9c51e58a4791a4b1ed58308b39c64224d349a935ab5039aa360942a48"
 dependencies = [
 "serde_derive",
 ]

 [[package]]
 name = "serde_derive"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79"
+checksum = "e7a5d71263a5a7d47b41f6b3f06ba276f10cc18b0931f1799f710578e2309348"
 dependencies = [
- "proc-macro2 1.0.106",
- "quote 1.0.46",
- "syn 2.0.119",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
+ "syn 3.0.3",
 ]

 [[package]]
 name = "serde_json"
-version = "1.0.150"
+version = "1.0.151"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e8014e44b4736ed0538adeecded0fce2a272f22dc9578a7eb6b2d9993c74cfb9"
+checksum = "c841b55ecdae098c80dcae9cf767f6f8a0c2cdb3416bbef72181df4d0fe73f14"
 dependencies = [
 "itoa",
 "memchr",
@@ -1504,7 +1537,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",
@@ -1565,6 +1598,27 @@ version = "0.11.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f"

+[[package]]
+name = "strum"
+version = "0.28.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9628de9b8791db39ceda2b119bbe13134770b56c138ec1d3af810d045c04f9bd"
+dependencies = [
+ "strum_macros",
+]
+
+[[package]]
+name = "strum_macros"
+version = "0.28.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ab85eea0270ee17587ed4156089e10b9e6880ee688791d45a905f5b1ca36f664"
+dependencies = [
+ "heck",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
+ "syn 2.0.119",
+]
+
 [[package]]
 name = "syn"
 version = "0.15.44"
@@ -1582,8 +1636,19 @@ version = "2.0.119"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "872831b642d1a07999a962a351ed35b955ea2cfc8f3862091e2a240a84f17297"
 dependencies = [
- "proc-macro2 1.0.106",
- "quote 1.0.46",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
+ "unicode-ident",
+]
+
+[[package]]
+name = "syn"
+version = "3.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "53e9bae58849f64dfa4f5d5ae372c8341f7305f82a3868709269343628b659a3"
+dependencies = [
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
 "unicode-ident",
 ]

@@ -1593,8 +1658,8 @@ version = "0.13.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "728a70f3dbaf5bab7f0c4b1ac8d7ae5ea60a4b5549c8a5914361c99147a709d2"
 dependencies = [
- "proc-macro2 1.0.106",
- "quote 1.0.46",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
 "syn 2.0.119",
 ]

@@ -1612,22 +1677,22 @@ dependencies = [

 [[package]]
 name = "thiserror"
-version = "2.0.18"
+version = "2.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4"
+checksum = "09a43598840e33d5b0331f38c5e30d13bb11c11210a4b58f0d9b18a5a5eefcd9"
 dependencies = [
 "thiserror-impl",
 ]

 [[package]]
 name = "thiserror-impl"
-version = "2.0.18"
+version = "2.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ebc4ee7f67670e9b64d05fa4253e753e016c6c95ff35b89b7941d6b856dec1d5"
+checksum = "43cbfe0cf76104d42a574802844187e84a305e531ed54455f11fbde0f10541cd"
 dependencies = [
- "proc-macro2 1.0.106",
- "quote 1.0.46",
- "syn 2.0.119",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
+ "syn 3.0.3",
 ]

 [[package]]
@@ -1666,7 +1731,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 +1833,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.107",
+ "quote 1.0.47",
+ "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.107",
+ "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.107",
+ "quote 1.0.47",
+ "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.107",
+ "quote 1.0.47",
+ "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"
@@ -1812,7 +1941,7 @@ version = "0.2.126"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "167ce5e579f6bcf889c4f7175a8a5a585de84e8ff93976ce393efa5f2837aab1"
 dependencies = [
- "quote 1.0.46",
+ "quote 1.0.47",
 "wasm-bindgen-macro-support",
 ]

@@ -1823,8 +1952,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f3997c7839262f4ef12cf90b818d6340c18e80f263f1a94bf157d0ec4420380e"
 dependencies = [
 "bumpalo",
- "proc-macro2 1.0.106",
- "quote 1.0.46",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
 "syn 2.0.119",
 "wasm-bindgen-shared",
 ]
@@ -1898,8 +2027,8 @@ version = "0.60.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "053e2e040ab57b9dc951b72c264860db7eb3b0200ba345b4e4c3b14f67855ddf"
 dependencies = [
- "proc-macro2 1.0.106",
- "quote 1.0.46",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
 "syn 2.0.119",
 ]

@@ -1909,8 +2038,8 @@ version = "0.59.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "3f316c4a2570ba26bbec722032c4099d8c8bc095efccdc15688708623367e358"
 dependencies = [
- "proc-macro2 1.0.106",
- "quote 1.0.46",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
 "syn 2.0.119",
 ]

@@ -1997,29 +2126,29 @@ version = "0.8.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "de844c262c8848816172cef550288e7dc6c7b7814b4ee56b3e1553f275f1858e"
 dependencies = [
- "proc-macro2 1.0.106",
- "quote 1.0.46",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
 "syn 2.0.119",
 "synstructure",
 ]

 [[package]]
 name = "zerocopy"
-version = "0.8.54"
+version = "0.8.55"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7cbbc0a705a0fd05cc3676525980d2bf5a9bc4adac6d6475209a7887cf59d19"
+checksum = "b5a105cd7b140f6eeec8acff2ea38135d3cab283ada58540f629fe51e46696eb"
 dependencies = [
 "zerocopy-derive",
 ]

 [[package]]
 name = "zerocopy-derive"
-version = "0.8.54"
+version = "0.8.55"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e2e817b7b52d0c7358d3246da9d69935ebb18116b2b102b4230dac079b4862f5"
+checksum = "0fe976fb70c78cd64cccfe3a6fc142244e8a77b70959b30faf9d0ac37ee228eb"
 dependencies = [
- "proc-macro2 1.0.106",
- "quote 1.0.46",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
 "syn 2.0.119",
 ]

@@ -2038,8 +2167,8 @@ version = "0.1.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "11532158c46691caf0f2593ea8358fed6bbf68a0315e80aae9bd41fbade684a1"
 dependencies = [
- "proc-macro2 1.0.106",
- "quote 1.0.46",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
 "syn 2.0.119",
 "synstructure",
 ]
@@ -2074,8 +2203,8 @@ version = "0.11.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "625dc425cab0dca6dc3c3319506e6593dcb08a9f387ea3b284dbd52a92c40555"
 dependencies = [
- "proc-macro2 1.0.106",
- "quote 1.0.46",
+ "proc-macro2 1.0.107",
+ "quote 1.0.47",
 "syn 2.0.119",
 ]

@@ -2087,7 +2216,7 @@ checksum = "2d04a6b5381502aa6087c94c669499eb1602eb9c5e8198e534de571f7154809b"
 dependencies = [
 "crc32fast",
 "flate2",
- "indexmap",
+ "indexmap 2.14.0",
 "memchr",
 "typed-path",
 "zopfli",
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -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"]
@@ -114,7 +120,7 @@ regex = {version = "1.12.3", optional = true, default-features = false }
 semver = {version = "1.0.28", optional = true, default-features = false }
 url = { version = "2.5.4", optional = true }
 uuid = { version = "1.22.0", default-features = false, features = ["v4", "fast-rng"], optional = true }
-jsonschema = { version = "0.47.0", default-features = false, optional = true }
+jsonschema = { version = "0.48.5", default-features = false, optional = true }
 chrono = { version = "0.4.44", optional = true }
 chrono-tz = { version = "0.10.1", optional = true }
 ipnet = { version = "2.12.0", optional = true, default-features = false }
@@ -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)'] }
--- a/bindings/csharp/Regorus.Tests/MemoryGrowthTests.cs
+++ b/bindings/csharp/Regorus.Tests/MemoryGrowthTests.cs
@@ -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);
--- a/bindings/ffi/Cargo.lock
+++ b/bindings/ffi/Cargo.lock
@@ -92,9 +92,9 @@ dependencies = [

 [[package]]
 name = "anyhow"
-version = "1.0.103"
+version = "1.0.104"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2a4385e2e34eb35d6b3efe798b9eb88096925d87726c0798709bf56d9ed84af3"
+checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470"

 [[package]]
 name = "autocfg"
@@ -159,22 +159,22 @@ checksum = "2ecb53484c9c167ba674026b656d8a27d7657a58e6066aa902bfb1a4aa00ae20"
 dependencies = [
 "clap",
 "heck",
- "indexmap",
+ "indexmap 2.14.0",
 "log",
 "proc-macro2",
 "quote",
 "serde",
 "serde_json",
- "syn",
+ "syn 2.0.119",
 "tempfile",
 "toml",
 ]

 [[package]]
 name = "cc"
-version = "1.2.67"
+version = "1.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e17dd265a7d0f31ef544e1b20e03add05d3b45b491b633b10d67145d2acc1a38"
+checksum = "c89588d05638b5b4594a3348a2d6c20277e43a7f5c5202b05cc56888475a47b8"
 dependencies = [
 "find-msvc-tools",
 "shlex",
@@ -222,9 +222,9 @@ dependencies = [

 [[package]]
 name = "clap"
-version = "4.6.2"
+version = "4.6.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dd059f9da4f5c36b3787f65d38ccaab1cc315f07b01f89abc8359ee6a8205011"
+checksum = "d91e0c145792ef73a6ad36d27c75ac09f1832222a3c209689d90f534685ee5b7"
 dependencies = [
 "clap_builder",
 ]
@@ -311,7 +311,7 @@ checksum = "1ac70aa55017e108007fbaf5aa0f54b021c98f92ff8af59d42eda9da96e3dd4f"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -364,9 +364,9 @@ dependencies = [

 [[package]]
 name = "fastrand"
-version = "2.4.1"
+version = "2.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9f1f227452a390804cdb637b74a86990f2a7d7ba4b7d5693aac9b4dd6defd8d6"
+checksum = "da7c62ceae207dd37ea5b845da6a0696c799f85e97da1ab5b7910be3c1c80223"

 [[package]]
 name = "find-msvc-tools"
@@ -412,21 +412,21 @@ dependencies = [

 [[package]]
 name = "futures-core"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7e3450815272ef58cec6d564423f6e755e25379b217b0bc688e295ba24df6b1d"
+checksum = "2cd50c473c80f6d7c3670a752354b8e569b1a7cbfdc0419ec88e5edad85e0dc7"

 [[package]]
 name = "futures-task"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "037711b3d59c33004d3856fbdc83b99d4ff37a24768fa1be9ce3538a1cde4393"
+checksum = "b231ed28831efb4a61a08580c4bc233ec56bc009f4cd8f52da2c3cb97df0c109"

 [[package]]
 name = "futures-util"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "389ca41296e6190b48053de0321d02a77f32f8a5d2461dd38762c0593805c6d6"
+checksum = "a77a90a256fce34da66415271e30f94ee91c57b04b8a2c042d9cf3220179deaa"
 dependencies = [
 "futures-core",
 "futures-task",
@@ -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"
@@ -691,9 +707,9 @@ dependencies = [

 [[package]]
 name = "jsonschema"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "281c43ff06dcb331e9356d30e38853d559ce3d0a3f693e0b0e102667dec14fb1"
+checksum = "f05a6cff806294a7699d48761d4ae2bdebab7fa2eef05e4a0b83320f0ff46901"
 dependencies = [
 "ahash",
 "bytecount",
@@ -705,6 +721,7 @@ dependencies = [
 "idna",
 "itoa",
 "jsonschema-regex",
+ "jsonschema-value",
 "num-cmp",
 "num-traits",
 "percent-encoding",
@@ -712,19 +729,34 @@ dependencies = [
 "regex",
 "serde",
 "serde_json",
+ "strum",
 "unicode-general-category",
 "uuid-simd",
 ]

 [[package]]
 name = "jsonschema-regex"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ee0b351864e7ffbc5db9273daf7fa1b4d5177b0946713d667ca571b83c0b4045"
+checksum = "84708dd3f6c5327478a96f37378adb27deed6a626cf84d19de780d9e8ae84b17"
 dependencies = [
 "regex-syntax",
 ]

+[[package]]
+name = "jsonschema-value"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fd8c04ab4ce60e42c4e302d3bd9d184652bb56f212495d2eea23573bcbf72556"
+dependencies = [
+ "ahash",
+ "bytecount",
+ "fraction",
+ "num-cmp",
+ "num-traits",
+ "serde_json",
+]
+
 [[package]]
 name = "lazy_static"
 version = "1.5.0"
@@ -733,9 +765,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"

 [[package]]
 name = "libc"
-version = "0.2.186"
+version = "0.2.189"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66"
+checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2"

 [[package]]
 name = "linux-raw-sys"
@@ -975,18 +1007,18 @@ dependencies = [

 [[package]]
 name = "proc-macro2"
-version = "1.0.106"
+version = "1.0.107"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
 dependencies = [
 "unicode-ident",
 ]

 [[package]]
 name = "quote"
-version = "1.0.46"
+version = "1.0.47"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dfbc457d0c7a0759a614551b11a6409e5951f6c7537be1f1b7682b9ae9230368"
+checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
 dependencies = [
 "proc-macro2",
 ]
@@ -1031,29 +1063,29 @@ dependencies = [

 [[package]]
 name = "ref-cast"
-version = "1.0.25"
+version = "1.0.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f354300ae66f76f1c85c5f84693f0ce81d747e2c3f21a45fef496d89c960bf7d"
+checksum = "216e8f773d7923bcba9ceb86a86c93cabb3903a11872fc3f138c49630e50b96d"
 dependencies = [
 "ref-cast-impl",
 ]

 [[package]]
 name = "ref-cast-impl"
-version = "1.0.25"
+version = "1.0.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7186006dcb21920990093f30e3dea63b7d6e977bf1256be20c3563a5db070da"
+checksum = "2c9283685feec7d69af75fb0e858d5e7378f33fe4fc699383b2916ab9273e03c"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
 name = "referencing"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "348e860aeb0b7bd035778fd11dd9cd5290d32e4aed3b8f2274a00287a9fd362b"
+checksum = "980e77f5cfffc592c0e7dfb6d20770a0b96a6ab94d403de7454ed9799505e4ba"
 dependencies = [
 "ahash",
 "fluent-uri",
@@ -1107,7 +1139,7 @@ dependencies = [
 "globset",
 "hashbrown 0.17.1",
 "icu_casemap",
- "indexmap",
+ "indexmap 2.14.0",
 "ipnet",
 "jsonschema",
 "lazy_static",
@@ -1128,6 +1160,7 @@ dependencies = [
 "thiserror",
 "url",
 "uuid",
+ "vstd",
 ]

 [[package]]
@@ -1194,9 +1227,9 @@ checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd"

 [[package]]
 name = "serde"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e"
+checksum = "4148590afebada386688f18773da617792bf2ef03ffc1e4cbd2b1d45b023e0ba"
 dependencies = [
 "serde_core",
 "serde_derive",
@@ -1204,29 +1237,29 @@ dependencies = [

 [[package]]
 name = "serde_core"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad"
+checksum = "67dca2c9c51e58a4791a4b1ed58308b39c64224d349a935ab5039aa360942a48"
 dependencies = [
 "serde_derive",
 ]

 [[package]]
 name = "serde_derive"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79"
+checksum = "e7a5d71263a5a7d47b41f6b3f06ba276f10cc18b0931f1799f710578e2309348"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
 name = "serde_json"
-version = "1.0.150"
+version = "1.0.151"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e8014e44b4736ed0538adeecded0fce2a272f22dc9578a7eb6b2d9993c74cfb9"
+checksum = "c841b55ecdae098c80dcae9cf767f6f8a0c2cdb3416bbef72181df4d0fe73f14"
 dependencies = [
 "itoa",
 "memchr",
@@ -1250,7 +1283,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",
@@ -1299,6 +1332,27 @@ version = "0.11.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f"

+[[package]]
+name = "strum"
+version = "0.28.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9628de9b8791db39ceda2b119bbe13134770b56c138ec1d3af810d045c04f9bd"
+dependencies = [
+ "strum_macros",
+]
+
+[[package]]
+name = "strum_macros"
+version = "0.28.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ab85eea0270ee17587ed4156089e10b9e6880ee688791d45a905f5b1ca36f664"
+dependencies = [
+ "heck",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.119",
+]
+
 [[package]]
 name = "syn"
 version = "2.0.119"
@@ -1310,6 +1364,17 @@ dependencies = [
 "unicode-ident",
 ]

+[[package]]
+name = "syn"
+version = "3.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "53e9bae58849f64dfa4f5d5ae372c8341f7305f82a3868709269343628b659a3"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
 [[package]]
 name = "synstructure"
 version = "0.13.2"
@@ -1318,7 +1383,7 @@ checksum = "728a70f3dbaf5bab7f0c4b1ac8d7ae5ea60a4b5549c8a5914361c99147a709d2"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1336,22 +1401,22 @@ dependencies = [

 [[package]]
 name = "thiserror"
-version = "2.0.18"
+version = "2.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4"
+checksum = "09a43598840e33d5b0331f38c5e30d13bb11c11210a4b58f0d9b18a5a5eefcd9"
 dependencies = [
 "thiserror-impl",
 ]

 [[package]]
 name = "thiserror-impl"
-version = "2.0.18"
+version = "2.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ebc4ee7f67670e9b64d05fa4253e753e016c6c95ff35b89b7941d6b856dec1d5"
+checksum = "43cbfe0cf76104d42a574802844187e84a305e531ed54455f11fbde0f10541cd"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
@@ -1371,7 +1436,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 +1537,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 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",
+ "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"
@@ -1519,7 +1648,7 @@ dependencies = [
 "bumpalo",
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "wasm-bindgen-shared",
 ]

@@ -1553,7 +1682,7 @@ checksum = "053e2e040ab57b9dc951b72c264860db7eb3b0200ba345b4e4c3b14f67855ddf"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1564,7 +1693,7 @@ checksum = "3f316c4a2570ba26bbec722032c4099d8c8bc095efccdc15688708623367e358"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1643,28 +1772,28 @@ checksum = "de844c262c8848816172cef550288e7dc6c7b7814b4ee56b3e1553f275f1858e"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "synstructure",
 ]

 [[package]]
 name = "zerocopy"
-version = "0.8.54"
+version = "0.8.55"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7cbbc0a705a0fd05cc3676525980d2bf5a9bc4adac6d6475209a7887cf59d19"
+checksum = "b5a105cd7b140f6eeec8acff2ea38135d3cab283ada58540f629fe51e46696eb"
 dependencies = [
 "zerocopy-derive",
 ]

 [[package]]
 name = "zerocopy-derive"
-version = "0.8.54"
+version = "0.8.55"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e2e817b7b52d0c7358d3246da9d69935ebb18116b2b102b4230dac079b4862f5"
+checksum = "0fe976fb70c78cd64cccfe3a6fc142244e8a77b70959b30faf9d0ac37ee228eb"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1684,7 +1813,7 @@ checksum = "11532158c46691caf0f2593ea8358fed6bbf68a0315e80aae9bd41fbade684a1"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "synstructure",
 ]

@@ -1720,7 +1849,7 @@ checksum = "625dc425cab0dca6dc3c3319506e6593dcb08a9f387ea3b284dbd52a92c40555"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
--- a/bindings/java/Cargo.lock
+++ b/bindings/java/Cargo.lock
@@ -42,9 +42,9 @@ dependencies = [

 [[package]]
 name = "anyhow"
-version = "1.0.103"
+version = "1.0.104"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2a4385e2e34eb35d6b3efe798b9eb88096925d87726c0798709bf56d9ed84af3"
+checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470"

 [[package]]
 name = "autocfg"
@@ -109,9 +109,9 @@ checksum = "fc652a48c352aef3ea3aed32080501cf3ef6ed5da78602a020c991775b0aff04"

 [[package]]
 name = "cc"
-version = "1.2.67"
+version = "1.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e17dd265a7d0f31ef544e1b20e03add05d3b45b491b633b10d67145d2acc1a38"
+checksum = "c89588d05638b5b4594a3348a2d6c20277e43a7f5c5202b05cc56888475a47b8"
 dependencies = [
 "find-msvc-tools",
 "shlex",
@@ -205,7 +205,7 @@ checksum = "1ac70aa55017e108007fbaf5aa0f54b021c98f92ff8af59d42eda9da96e3dd4f"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -290,21 +290,21 @@ dependencies = [

 [[package]]
 name = "futures-core"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7e3450815272ef58cec6d564423f6e755e25379b217b0bc688e295ba24df6b1d"
+checksum = "2cd50c473c80f6d7c3670a752354b8e569b1a7cbfdc0419ec88e5edad85e0dc7"

 [[package]]
 name = "futures-task"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "037711b3d59c33004d3856fbdc83b99d4ff37a24768fa1be9ce3538a1cde4393"
+checksum = "b231ed28831efb4a61a08580c4bc233ec56bc009f4cd8f52da2c3cb97df0c109"

 [[package]]
 name = "futures-util"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "389ca41296e6190b48053de0321d02a77f32f8a5d2461dd38762c0593805c6d6"
+checksum = "a77a90a256fce34da66415271e30f94ee91c57b04b8a2c042d9cf3220179deaa"
 dependencies = [
 "futures-core",
 "futures-task",
@@ -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"
@@ -361,6 +367,12 @@ dependencies = [
 "foldhash",
 ]

+[[package]]
+name = "heck"
+version = "0.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea"
+
 [[package]]
 name = "iana-time-zone"
 version = "0.1.65"
@@ -488,6 +500,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 +517,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9"
 dependencies = [
 "equivalent",
- "hashbrown",
+ "hashbrown 0.17.1",
 "serde",
 "serde_core",
 ]
@@ -539,7 +561,7 @@ dependencies = [
 "quote",
 "rustc_version",
 "simd_cesu8",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -558,7 +580,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "38c0b942f458fe50cdac086d2f946512305e5631e720728f2a61aabcd47a6264"
 dependencies = [
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -574,9 +596,9 @@ dependencies = [

 [[package]]
 name = "jsonschema"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "281c43ff06dcb331e9356d30e38853d559ce3d0a3f693e0b0e102667dec14fb1"
+checksum = "f05a6cff806294a7699d48761d4ae2bdebab7fa2eef05e4a0b83320f0ff46901"
 dependencies = [
 "ahash",
 "bytecount",
@@ -588,6 +610,7 @@ dependencies = [
 "idna",
 "itoa",
 "jsonschema-regex",
+ "jsonschema-value",
 "num-cmp",
 "num-traits",
 "percent-encoding",
@@ -595,19 +618,34 @@ dependencies = [
 "regex",
 "serde",
 "serde_json",
+ "strum",
 "unicode-general-category",
 "uuid-simd",
 ]

 [[package]]
 name = "jsonschema-regex"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ee0b351864e7ffbc5db9273daf7fa1b4d5177b0946713d667ca571b83c0b4045"
+checksum = "84708dd3f6c5327478a96f37378adb27deed6a626cf84d19de780d9e8ae84b17"
 dependencies = [
 "regex-syntax",
 ]

+[[package]]
+name = "jsonschema-value"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fd8c04ab4ce60e42c4e302d3bd9d184652bb56f212495d2eea23573bcbf72556"
+dependencies = [
+ "ahash",
+ "bytecount",
+ "fraction",
+ "num-cmp",
+ "num-traits",
+ "serde_json",
+]
+
 [[package]]
 name = "lazy_static"
 version = "1.5.0"
@@ -616,9 +654,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"

 [[package]]
 name = "libc"
-version = "0.2.186"
+version = "0.2.189"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66"
+checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2"

 [[package]]
 name = "litemap"
@@ -844,18 +882,18 @@ dependencies = [

 [[package]]
 name = "proc-macro2"
-version = "1.0.106"
+version = "1.0.107"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
 dependencies = [
 "unicode-ident",
 ]

 [[package]]
 name = "quote"
-version = "1.0.46"
+version = "1.0.47"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dfbc457d0c7a0759a614551b11a6409e5951f6c7537be1f1b7682b9ae9230368"
+checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
 dependencies = [
 "proc-macro2",
 ]
@@ -900,34 +938,34 @@ dependencies = [

 [[package]]
 name = "ref-cast"
-version = "1.0.25"
+version = "1.0.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f354300ae66f76f1c85c5f84693f0ce81d747e2c3f21a45fef496d89c960bf7d"
+checksum = "216e8f773d7923bcba9ceb86a86c93cabb3903a11872fc3f138c49630e50b96d"
 dependencies = [
 "ref-cast-impl",
 ]

 [[package]]
 name = "ref-cast-impl"
-version = "1.0.25"
+version = "1.0.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7186006dcb21920990093f30e3dea63b7d6e977bf1256be20c3563a5db070da"
+checksum = "2c9283685feec7d69af75fb0e858d5e7378f33fe4fc699383b2916ab9273e03c"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
 name = "referencing"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "348e860aeb0b7bd035778fd11dd9cd5290d32e4aed3b8f2274a00287a9fd362b"
+checksum = "980e77f5cfffc592c0e7dfb6d20770a0b96a6ab94d403de7454ed9799505e4ba"
 dependencies = [
 "ahash",
 "fluent-uri",
 "getrandom 0.3.4",
- "hashbrown",
+ "hashbrown 0.17.1",
 "itoa",
 "micromap",
 "parking_lot",
@@ -973,7 +1011,7 @@ dependencies = [
 "chrono-tz",
 "data-encoding",
 "globset",
- "indexmap",
+ "indexmap 2.14.0",
 "ipnet",
 "jsonschema",
 "lazy_static",
@@ -994,6 +1032,7 @@ dependencies = [
 "thiserror",
 "url",
 "uuid",
+ "vstd",
 ]

 [[package]]
@@ -1064,9 +1103,9 @@ checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd"

 [[package]]
 name = "serde"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e"
+checksum = "4148590afebada386688f18773da617792bf2ef03ffc1e4cbd2b1d45b023e0ba"
 dependencies = [
 "serde_core",
 "serde_derive",
@@ -1074,29 +1113,29 @@ dependencies = [

 [[package]]
 name = "serde_core"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad"
+checksum = "67dca2c9c51e58a4791a4b1ed58308b39c64224d349a935ab5039aa360942a48"
 dependencies = [
 "serde_derive",
 ]

 [[package]]
 name = "serde_derive"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79"
+checksum = "e7a5d71263a5a7d47b41f6b3f06ba276f10cc18b0931f1799f710578e2309348"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
 name = "serde_json"
-version = "1.0.150"
+version = "1.0.151"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e8014e44b4736ed0538adeecded0fce2a272f22dc9578a7eb6b2d9993c74cfb9"
+checksum = "c841b55ecdae098c80dcae9cf767f6f8a0c2cdb3416bbef72181df4d0fe73f14"
 dependencies = [
 "itoa",
 "memchr",
@@ -1111,7 +1150,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",
@@ -1170,6 +1209,27 @@ version = "1.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6ce2be8dc25455e1f91df71bfa12ad37d7af1092ae736f3a6cd0e37bc7810596"

+[[package]]
+name = "strum"
+version = "0.28.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9628de9b8791db39ceda2b119bbe13134770b56c138ec1d3af810d045c04f9bd"
+dependencies = [
+ "strum_macros",
+]
+
+[[package]]
+name = "strum_macros"
+version = "0.28.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ab85eea0270ee17587ed4156089e10b9e6880ee688791d45a905f5b1ca36f664"
+dependencies = [
+ "heck",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.119",
+]
+
 [[package]]
 name = "syn"
 version = "2.0.119"
@@ -1181,6 +1241,17 @@ dependencies = [
 "unicode-ident",
 ]

+[[package]]
+name = "syn"
+version = "3.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "53e9bae58849f64dfa4f5d5ae372c8341f7305f82a3868709269343628b659a3"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
 [[package]]
 name = "synstructure"
 version = "0.13.2"
@@ -1189,27 +1260,27 @@ checksum = "728a70f3dbaf5bab7f0c4b1ac8d7ae5ea60a4b5549c8a5914361c99147a709d2"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
 name = "thiserror"
-version = "2.0.18"
+version = "2.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4"
+checksum = "09a43598840e33d5b0331f38c5e30d13bb11c11210a4b58f0d9b18a5a5eefcd9"
 dependencies = [
 "thiserror-impl",
 ]

 [[package]]
 name = "thiserror-impl"
-version = "2.0.18"
+version = "2.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ebc4ee7f67670e9b64d05fa4253e753e016c6c95ff35b89b7941d6b856dec1d5"
+checksum = "43cbfe0cf76104d42a574802844187e84a305e531ed54455f11fbde0f10541cd"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
@@ -1284,12 +1355,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 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",
+ "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"
@@ -1341,7 +1476,7 @@ dependencies = [
 "bumpalo",
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "wasm-bindgen-shared",
 ]

@@ -1384,7 +1519,7 @@ checksum = "053e2e040ab57b9dc951b72c264860db7eb3b0200ba345b4e4c3b14f67855ddf"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1395,7 +1530,7 @@ checksum = "3f316c4a2570ba26bbec722032c4099d8c8bc095efccdc15688708623367e358"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1462,28 +1597,28 @@ checksum = "de844c262c8848816172cef550288e7dc6c7b7814b4ee56b3e1553f275f1858e"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "synstructure",
 ]

 [[package]]
 name = "zerocopy"
-version = "0.8.54"
+version = "0.8.55"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7cbbc0a705a0fd05cc3676525980d2bf5a9bc4adac6d6475209a7887cf59d19"
+checksum = "b5a105cd7b140f6eeec8acff2ea38135d3cab283ada58540f629fe51e46696eb"
 dependencies = [
 "zerocopy-derive",
 ]

 [[package]]
 name = "zerocopy-derive"
-version = "0.8.54"
+version = "0.8.55"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e2e817b7b52d0c7358d3246da9d69935ebb18116b2b102b4230dac079b4862f5"
+checksum = "0fe976fb70c78cd64cccfe3a6fc142244e8a77b70959b30faf9d0ac37ee228eb"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1503,7 +1638,7 @@ checksum = "11532158c46691caf0f2593ea8358fed6bbf68a0315e80aae9bd41fbade684a1"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "synstructure",
 ]

@@ -1537,7 +1672,7 @@ checksum = "625dc425cab0dca6dc3c3319506e6593dcb08a9f387ea3b284dbd52a92c40555"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
--- a/bindings/python/Cargo.lock
+++ b/bindings/python/Cargo.lock
@@ -42,9 +42,9 @@ dependencies = [

 [[package]]
 name = "anyhow"
-version = "1.0.103"
+version = "1.0.104"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2a4385e2e34eb35d6b3efe798b9eb88096925d87726c0798709bf56d9ed84af3"
+checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470"

 [[package]]
 name = "autocfg"
@@ -103,9 +103,9 @@ checksum = "175812e0be2bccb6abe50bb8d566126198344f707e304f45c648fd8f2cc0365e"

 [[package]]
 name = "cc"
-version = "1.2.67"
+version = "1.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e17dd265a7d0f31ef544e1b20e03add05d3b45b491b633b10d67145d2acc1a38"
+checksum = "c89588d05638b5b4594a3348a2d6c20277e43a7f5c5202b05cc56888475a47b8"
 dependencies = [
 "find-msvc-tools",
 "shlex",
@@ -189,7 +189,7 @@ checksum = "1ac70aa55017e108007fbaf5aa0f54b021c98f92ff8af59d42eda9da96e3dd4f"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -274,21 +274,21 @@ dependencies = [

 [[package]]
 name = "futures-core"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7e3450815272ef58cec6d564423f6e755e25379b217b0bc688e295ba24df6b1d"
+checksum = "2cd50c473c80f6d7c3670a752354b8e569b1a7cbfdc0419ec88e5edad85e0dc7"

 [[package]]
 name = "futures-task"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "037711b3d59c33004d3856fbdc83b99d4ff37a24768fa1be9ce3538a1cde4393"
+checksum = "b231ed28831efb4a61a08580c4bc233ec56bc009f4cd8f52da2c3cb97df0c109"

 [[package]]
 name = "futures-util"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "389ca41296e6190b48053de0321d02a77f32f8a5d2461dd38762c0593805c6d6"
+checksum = "a77a90a256fce34da66415271e30f94ee91c57b04b8a2c042d9cf3220179deaa"
 dependencies = [
 "futures-core",
 "futures-task",
@@ -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",
 ]
@@ -515,9 +531,9 @@ dependencies = [

 [[package]]
 name = "jsonschema"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "281c43ff06dcb331e9356d30e38853d559ce3d0a3f693e0b0e102667dec14fb1"
+checksum = "f05a6cff806294a7699d48761d4ae2bdebab7fa2eef05e4a0b83320f0ff46901"
 dependencies = [
 "ahash",
 "bytecount",
@@ -529,6 +545,7 @@ dependencies = [
 "idna",
 "itoa",
 "jsonschema-regex",
+ "jsonschema-value",
 "num-cmp",
 "num-traits",
 "percent-encoding",
@@ -536,19 +553,34 @@ dependencies = [
 "regex",
 "serde",
 "serde_json",
+ "strum",
 "unicode-general-category",
 "uuid-simd",
 ]

 [[package]]
 name = "jsonschema-regex"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ee0b351864e7ffbc5db9273daf7fa1b4d5177b0946713d667ca571b83c0b4045"
+checksum = "84708dd3f6c5327478a96f37378adb27deed6a626cf84d19de780d9e8ae84b17"
 dependencies = [
 "regex-syntax",
 ]

+[[package]]
+name = "jsonschema-value"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fd8c04ab4ce60e42c4e302d3bd9d184652bb56f212495d2eea23573bcbf72556"
+dependencies = [
+ "ahash",
+ "bytecount",
+ "fraction",
+ "num-cmp",
+ "num-traits",
+ "serde_json",
+]
+
 [[package]]
 name = "lazy_static"
 version = "1.5.0"
@@ -557,9 +589,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"

 [[package]]
 name = "libc"
-version = "0.2.186"
+version = "0.2.189"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66"
+checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2"

 [[package]]
 name = "litemap"
@@ -773,9 +805,9 @@ checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd"

 [[package]]
 name = "portable-atomic"
-version = "1.13.1"
+version = "1.14.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c33a9471896f1c69cecef8d20cbe2f7accd12527ce60845ff44c153bb2a21b49"
+checksum = "3d20d5497ef88037a52ff98267d066e7f11fcc5e99bbfbd58a42336193aacec3"

 [[package]]
 name = "postcard"
@@ -800,9 +832,9 @@ dependencies = [

 [[package]]
 name = "proc-macro2"
-version = "1.0.106"
+version = "1.0.107"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
 dependencies = [
 "unicode-ident",
 ]
@@ -850,7 +882,7 @@ dependencies = [
 "proc-macro2",
 "pyo3-macros-backend",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -862,14 +894,14 @@ dependencies = [
 "heck",
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
 name = "quote"
-version = "1.0.46"
+version = "1.0.47"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dfbc457d0c7a0759a614551b11a6409e5951f6c7537be1f1b7682b9ae9230368"
+checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
 dependencies = [
 "proc-macro2",
 ]
@@ -914,34 +946,34 @@ dependencies = [

 [[package]]
 name = "ref-cast"
-version = "1.0.25"
+version = "1.0.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f354300ae66f76f1c85c5f84693f0ce81d747e2c3f21a45fef496d89c960bf7d"
+checksum = "216e8f773d7923bcba9ceb86a86c93cabb3903a11872fc3f138c49630e50b96d"
 dependencies = [
 "ref-cast-impl",
 ]

 [[package]]
 name = "ref-cast-impl"
-version = "1.0.25"
+version = "1.0.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7186006dcb21920990093f30e3dea63b7d6e977bf1256be20c3563a5db070da"
+checksum = "2c9283685feec7d69af75fb0e858d5e7378f33fe4fc699383b2916ab9273e03c"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
 name = "referencing"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "348e860aeb0b7bd035778fd11dd9cd5290d32e4aed3b8f2274a00287a9fd362b"
+checksum = "980e77f5cfffc592c0e7dfb6d20770a0b96a6ab94d403de7454ed9799505e4ba"
 dependencies = [
 "ahash",
 "fluent-uri",
 "getrandom 0.3.4",
- "hashbrown",
+ "hashbrown 0.17.1",
 "itoa",
 "micromap",
 "parking_lot",
@@ -987,7 +1019,7 @@ dependencies = [
 "chrono-tz",
 "data-encoding",
 "globset",
- "indexmap",
+ "indexmap 2.14.0",
 "ipnet",
 "jsonschema",
 "lazy_static",
@@ -1008,6 +1040,7 @@ dependencies = [
 "thiserror",
 "url",
 "uuid",
+ "vstd",
 ]

 [[package]]
@@ -1061,9 +1094,9 @@ checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd"

 [[package]]
 name = "serde"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e"
+checksum = "4148590afebada386688f18773da617792bf2ef03ffc1e4cbd2b1d45b023e0ba"
 dependencies = [
 "serde_core",
 "serde_derive",
@@ -1071,29 +1104,29 @@ dependencies = [

 [[package]]
 name = "serde_core"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad"
+checksum = "67dca2c9c51e58a4791a4b1ed58308b39c64224d349a935ab5039aa360942a48"
 dependencies = [
 "serde_derive",
 ]

 [[package]]
 name = "serde_derive"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79"
+checksum = "e7a5d71263a5a7d47b41f6b3f06ba276f10cc18b0931f1799f710578e2309348"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
 name = "serde_json"
-version = "1.0.150"
+version = "1.0.151"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e8014e44b4736ed0538adeecded0fce2a272f22dc9578a7eb6b2d9993c74cfb9"
+checksum = "c841b55ecdae098c80dcae9cf767f6f8a0c2cdb3416bbef72181df4d0fe73f14"
 dependencies = [
 "itoa",
 "memchr",
@@ -1108,7 +1141,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",
@@ -1151,6 +1184,27 @@ version = "1.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6ce2be8dc25455e1f91df71bfa12ad37d7af1092ae736f3a6cd0e37bc7810596"

+[[package]]
+name = "strum"
+version = "0.28.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9628de9b8791db39ceda2b119bbe13134770b56c138ec1d3af810d045c04f9bd"
+dependencies = [
+ "strum_macros",
+]
+
+[[package]]
+name = "strum_macros"
+version = "0.28.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ab85eea0270ee17587ed4156089e10b9e6880ee688791d45a905f5b1ca36f664"
+dependencies = [
+ "heck",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.119",
+]
+
 [[package]]
 name = "syn"
 version = "2.0.119"
@@ -1162,6 +1216,17 @@ dependencies = [
 "unicode-ident",
 ]

+[[package]]
+name = "syn"
+version = "3.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "53e9bae58849f64dfa4f5d5ae372c8341f7305f82a3868709269343628b659a3"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
 [[package]]
 name = "synstructure"
 version = "0.13.2"
@@ -1170,7 +1235,7 @@ checksum = "728a70f3dbaf5bab7f0c4b1ac8d7ae5ea60a4b5549c8a5914361c99147a709d2"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1181,22 +1246,22 @@ checksum = "adb6935a6f5c20170eeceb1a3835a49e12e19d792f6dd344ccc76a985ca5a6ca"

 [[package]]
 name = "thiserror"
-version = "2.0.18"
+version = "2.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4"
+checksum = "09a43598840e33d5b0331f38c5e30d13bb11c11210a4b58f0d9b18a5a5eefcd9"
 dependencies = [
 "thiserror-impl",
 ]

 [[package]]
 name = "thiserror-impl"
-version = "2.0.18"
+version = "2.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ebc4ee7f67670e9b64d05fa4253e753e016c6c95ff35b89b7941d6b856dec1d5"
+checksum = "43cbfe0cf76104d42a574802844187e84a305e531ed54455f11fbde0f10541cd"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
@@ -1271,12 +1336,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 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",
+ "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"
@@ -1318,7 +1447,7 @@ dependencies = [
 "bumpalo",
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "wasm-bindgen-shared",
 ]

@@ -1352,7 +1481,7 @@ checksum = "053e2e040ab57b9dc951b72c264860db7eb3b0200ba345b4e4c3b14f67855ddf"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1363,7 +1492,7 @@ checksum = "3f316c4a2570ba26bbec722032c4099d8c8bc095efccdc15688708623367e358"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1421,28 +1550,28 @@ checksum = "de844c262c8848816172cef550288e7dc6c7b7814b4ee56b3e1553f275f1858e"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "synstructure",
 ]

 [[package]]
 name = "zerocopy"
-version = "0.8.54"
+version = "0.8.55"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7cbbc0a705a0fd05cc3676525980d2bf5a9bc4adac6d6475209a7887cf59d19"
+checksum = "b5a105cd7b140f6eeec8acff2ea38135d3cab283ada58540f629fe51e46696eb"
 dependencies = [
 "zerocopy-derive",
 ]

 [[package]]
 name = "zerocopy-derive"
-version = "0.8.54"
+version = "0.8.55"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e2e817b7b52d0c7358d3246da9d69935ebb18116b2b102b4230dac079b4862f5"
+checksum = "0fe976fb70c78cd64cccfe3a6fc142244e8a77b70959b30faf9d0ac37ee228eb"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1462,7 +1591,7 @@ checksum = "11532158c46691caf0f2593ea8358fed6bbf68a0315e80aae9bd41fbade684a1"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "synstructure",
 ]

@@ -1496,7 +1625,7 @@ checksum = "625dc425cab0dca6dc3c3319506e6593dcb08a9f387ea3b284dbd52a92c40555"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
--- a/bindings/ruby/Cargo.lock
+++ b/bindings/ruby/Cargo.lock
@@ -42,9 +42,9 @@ dependencies = [

 [[package]]
 name = "anyhow"
-version = "1.0.103"
+version = "1.0.104"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2a4385e2e34eb35d6b3efe798b9eb88096925d87726c0798709bf56d9ed84af3"
+checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470"

 [[package]]
 name = "autocfg"
@@ -67,7 +67,7 @@ dependencies = [
 "regex",
 "rustc-hash",
 "shlex 1.3.0",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -121,9 +121,9 @@ checksum = "175812e0be2bccb6abe50bb8d566126198344f707e304f45c648fd8f2cc0365e"

 [[package]]
 name = "cc"
-version = "1.2.67"
+version = "1.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e17dd265a7d0f31ef544e1b20e03add05d3b45b491b633b10d67145d2acc1a38"
+checksum = "c89588d05638b5b4594a3348a2d6c20277e43a7f5c5202b05cc56888475a47b8"
 dependencies = [
 "find-msvc-tools",
 "shlex 2.0.1",
@@ -218,7 +218,7 @@ checksum = "1ac70aa55017e108007fbaf5aa0f54b021c98f92ff8af59d42eda9da96e3dd4f"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -297,21 +297,21 @@ dependencies = [

 [[package]]
 name = "futures-core"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7e3450815272ef58cec6d564423f6e755e25379b217b0bc688e295ba24df6b1d"
+checksum = "2cd50c473c80f6d7c3670a752354b8e569b1a7cbfdc0419ec88e5edad85e0dc7"

 [[package]]
 name = "futures-task"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "037711b3d59c33004d3856fbdc83b99d4ff37a24768fa1be9ce3538a1cde4393"
+checksum = "b231ed28831efb4a61a08580c4bc233ec56bc009f4cd8f52da2c3cb97df0c109"

 [[package]]
 name = "futures-util"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "389ca41296e6190b48053de0321d02a77f32f8a5d2461dd38762c0593805c6d6"
+checksum = "a77a90a256fce34da66415271e30f94ee91c57b04b8a2c042d9cf3220179deaa"
 dependencies = [
 "futures-core",
 "futures-task",
@@ -347,9 +347,9 @@ dependencies = [

 [[package]]
 name = "glob"
-version = "0.3.3"
+version = "0.3.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0cc23270f6e1808e30a928bdc84dea0b9b4136a8bc82338574f23baf47bbd280"
+checksum = "e4eba85ea1d0a966a983acd07deee566e67395d2d96b6fb39e62b5a833f1eb0b"

 [[package]]
 name = "globset"
@@ -363,6 +363,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"
@@ -374,6 +380,12 @@ dependencies = [
 "foldhash",
 ]

+[[package]]
+name = "heck"
+version = "0.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea"
+
 [[package]]
 name = "iana-time-zone"
 version = "0.1.65"
@@ -501,6 +513,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"
@@ -508,7 +530,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9"
 dependencies = [
 "equivalent",
- "hashbrown",
+ "hashbrown 0.17.1",
 "serde",
 "serde_core",
 ]
@@ -547,9 +569,9 @@ dependencies = [

 [[package]]
 name = "jsonschema"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "281c43ff06dcb331e9356d30e38853d559ce3d0a3f693e0b0e102667dec14fb1"
+checksum = "f05a6cff806294a7699d48761d4ae2bdebab7fa2eef05e4a0b83320f0ff46901"
 dependencies = [
 "ahash",
 "bytecount",
@@ -561,6 +583,7 @@ dependencies = [
 "idna",
 "itoa",
 "jsonschema-regex",
+ "jsonschema-value",
 "num-cmp",
 "num-traits",
 "percent-encoding",
@@ -568,19 +591,34 @@ dependencies = [
 "regex",
 "serde",
 "serde_json",
+ "strum",
 "unicode-general-category",
 "uuid-simd",
 ]

 [[package]]
 name = "jsonschema-regex"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ee0b351864e7ffbc5db9273daf7fa1b4d5177b0946713d667ca571b83c0b4045"
+checksum = "84708dd3f6c5327478a96f37378adb27deed6a626cf84d19de780d9e8ae84b17"
 dependencies = [
 "regex-syntax",
 ]

+[[package]]
+name = "jsonschema-value"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fd8c04ab4ce60e42c4e302d3bd9d184652bb56f212495d2eea23573bcbf72556"
+dependencies = [
+ "ahash",
+ "bytecount",
+ "fraction",
+ "num-cmp",
+ "num-traits",
+ "serde_json",
+]
+
 [[package]]
 name = "lazy_static"
 version = "1.5.0"
@@ -589,9 +627,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"

 [[package]]
 name = "libc"
-version = "0.2.186"
+version = "0.2.189"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66"
+checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2"

 [[package]]
 name = "libloading"
@@ -650,7 +688,7 @@ checksum = "47607461fd8e1513cb4f2076c197d8092d921a1ea75bd08af97398f593751892"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -854,18 +892,18 @@ dependencies = [

 [[package]]
 name = "proc-macro2"
-version = "1.0.106"
+version = "1.0.107"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
 dependencies = [
 "unicode-ident",
 ]

 [[package]]
 name = "quote"
-version = "1.0.46"
+version = "1.0.47"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dfbc457d0c7a0759a614551b11a6409e5951f6c7537be1f1b7682b9ae9230368"
+checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
 dependencies = [
 "proc-macro2",
 ]
@@ -920,7 +958,7 @@ dependencies = [
 "quote",
 "regex",
 "shell-words",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -940,34 +978,34 @@ dependencies = [

 [[package]]
 name = "ref-cast"
-version = "1.0.25"
+version = "1.0.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f354300ae66f76f1c85c5f84693f0ce81d747e2c3f21a45fef496d89c960bf7d"
+checksum = "216e8f773d7923bcba9ceb86a86c93cabb3903a11872fc3f138c49630e50b96d"
 dependencies = [
 "ref-cast-impl",
 ]

 [[package]]
 name = "ref-cast-impl"
-version = "1.0.25"
+version = "1.0.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7186006dcb21920990093f30e3dea63b7d6e977bf1256be20c3563a5db070da"
+checksum = "2c9283685feec7d69af75fb0e858d5e7378f33fe4fc699383b2916ab9273e03c"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
 name = "referencing"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "348e860aeb0b7bd035778fd11dd9cd5290d32e4aed3b8f2274a00287a9fd362b"
+checksum = "980e77f5cfffc592c0e7dfb6d20770a0b96a6ab94d403de7454ed9799505e4ba"
 dependencies = [
 "ahash",
 "fluent-uri",
 "getrandom 0.3.4",
- "hashbrown",
+ "hashbrown 0.17.1",
 "itoa",
 "micromap",
 "parking_lot",
@@ -1013,7 +1051,7 @@ dependencies = [
 "chrono-tz",
 "data-encoding",
 "globset",
- "indexmap",
+ "indexmap 2.14.0",
 "ipnet",
 "jsonschema",
 "lazy_static",
@@ -1033,6 +1071,7 @@ dependencies = [
 "thiserror",
 "url",
 "uuid",
+ "vstd",
 ]

 [[package]]
@@ -1098,9 +1137,9 @@ checksum = "1bc711410fbe7399f390ca1c3b60ad0f53f80e95c5eb935e52268a0e2cd49acc"

 [[package]]
 name = "serde"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e"
+checksum = "4148590afebada386688f18773da617792bf2ef03ffc1e4cbd2b1d45b023e0ba"
 dependencies = [
 "serde_core",
 "serde_derive",
@@ -1108,29 +1147,29 @@ dependencies = [

 [[package]]
 name = "serde_core"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad"
+checksum = "67dca2c9c51e58a4791a4b1ed58308b39c64224d349a935ab5039aa360942a48"
 dependencies = [
 "serde_derive",
 ]

 [[package]]
 name = "serde_derive"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79"
+checksum = "e7a5d71263a5a7d47b41f6b3f06ba276f10cc18b0931f1799f710578e2309348"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
 name = "serde_json"
-version = "1.0.150"
+version = "1.0.151"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e8014e44b4736ed0538adeecded0fce2a272f22dc9578a7eb6b2d9993c74cfb9"
+checksum = "c841b55ecdae098c80dcae9cf767f6f8a0c2cdb3416bbef72181df4d0fe73f14"
 dependencies = [
 "itoa",
 "memchr",
@@ -1156,7 +1195,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",
@@ -1211,6 +1250,27 @@ version = "1.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6ce2be8dc25455e1f91df71bfa12ad37d7af1092ae736f3a6cd0e37bc7810596"

+[[package]]
+name = "strum"
+version = "0.28.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9628de9b8791db39ceda2b119bbe13134770b56c138ec1d3af810d045c04f9bd"
+dependencies = [
+ "strum_macros",
+]
+
+[[package]]
+name = "strum_macros"
+version = "0.28.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ab85eea0270ee17587ed4156089e10b9e6880ee688791d45a905f5b1ca36f664"
+dependencies = [
+ "heck",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.119",
+]
+
 [[package]]
 name = "syn"
 version = "2.0.119"
@@ -1222,6 +1282,17 @@ dependencies = [
 "unicode-ident",
 ]

+[[package]]
+name = "syn"
+version = "3.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "53e9bae58849f64dfa4f5d5ae372c8341f7305f82a3868709269343628b659a3"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
 [[package]]
 name = "synstructure"
 version = "0.13.2"
@@ -1230,7 +1301,7 @@ checksum = "728a70f3dbaf5bab7f0c4b1ac8d7ae5ea60a4b5549c8a5914361c99147a709d2"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1241,22 +1312,22 @@ checksum = "55937e1799185b12863d447f42597ed69d9928686b8d88a1df17376a097d8369"

 [[package]]
 name = "thiserror"
-version = "2.0.18"
+version = "2.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4"
+checksum = "09a43598840e33d5b0331f38c5e30d13bb11c11210a4b58f0d9b18a5a5eefcd9"
 dependencies = [
 "thiserror-impl",
 ]

 [[package]]
 name = "thiserror-impl"
-version = "2.0.18"
+version = "2.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ebc4ee7f67670e9b64d05fa4253e753e016c6c95ff35b89b7941d6b856dec1d5"
+checksum = "43cbfe0cf76104d42a574802844187e84a305e531ed54455f11fbde0f10541cd"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
@@ -1331,12 +1402,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 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",
+ "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"
@@ -1378,7 +1513,7 @@ dependencies = [
 "bumpalo",
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "wasm-bindgen-shared",
 ]

@@ -1412,7 +1547,7 @@ checksum = "053e2e040ab57b9dc951b72c264860db7eb3b0200ba345b4e4c3b14f67855ddf"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1423,7 +1558,7 @@ checksum = "3f316c4a2570ba26bbec722032c4099d8c8bc095efccdc15688708623367e358"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1481,28 +1616,28 @@ checksum = "de844c262c8848816172cef550288e7dc6c7b7814b4ee56b3e1553f275f1858e"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "synstructure",
 ]

 [[package]]
 name = "zerocopy"
-version = "0.8.54"
+version = "0.8.55"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7cbbc0a705a0fd05cc3676525980d2bf5a9bc4adac6d6475209a7887cf59d19"
+checksum = "b5a105cd7b140f6eeec8acff2ea38135d3cab283ada58540f629fe51e46696eb"
 dependencies = [
 "zerocopy-derive",
 ]

 [[package]]
 name = "zerocopy-derive"
-version = "0.8.54"
+version = "0.8.55"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e2e817b7b52d0c7358d3246da9d69935ebb18116b2b102b4230dac079b4862f5"
+checksum = "0fe976fb70c78cd64cccfe3a6fc142244e8a77b70959b30faf9d0ac37ee228eb"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1522,7 +1657,7 @@ checksum = "11532158c46691caf0f2593ea8358fed6bbf68a0315e80aae9bd41fbade684a1"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "synstructure",
 ]

@@ -1556,7 +1691,7 @@ checksum = "625dc425cab0dca6dc3c3319506e6593dcb08a9f387ea3b284dbd52a92c40555"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
--- a/bindings/ruby/Gemfile
+++ b/bindings/ruby/Gemfile
@@ -12,5 +12,5 @@ gem "rake", "~> 13.4"
 gem "rake-compiler", "~> 1.3"
 gem "rake-compiler-dock", "~> 1.12"
 gem "rubocop", "~> 1.88", require: false
-gem "rubocop-minitest", "~> 0.39.1", require: false
+gem "rubocop-minitest", "~> 0.40.0", require: false
 gem "rubocop-rake", "~> 0.7.1", require: false
--- a/bindings/ruby/Gemfile.lock
+++ b/bindings/ruby/Gemfile.lock
@@ -9,14 +9,14 @@ GEM
  specs:
    ast (2.4.3)
    drb (2.2.3)
-    json (2.20.0)
-    language_server-protocol (3.17.0.5)
+    json (2.21.1)
+    language_server-protocol (3.17.0.6)
    lint_roller (1.1.0)
    minitest (6.0.6)
      drb (~> 2.0)
      prism (~> 1.5)
    parallel (2.1.0)
-    parser (3.3.11.1)
+    parser (3.3.12.0)
      ast (~> 2.4.1)
      racc
    prism (1.9.0)
@@ -29,7 +29,7 @@ GEM
    rb_sys (0.9.128)
      rake-compiler-dock (= 1.12.0)
    regexp_parser (2.12.0)
-    rubocop (1.88.0)
+    rubocop (1.88.2)
      json (~> 2.3)
      language_server-protocol (~> 3.17.0.2)
      lint_roller (~> 1.1.0)
@@ -40,10 +40,10 @@ GEM
      rubocop-ast (>= 1.49.0, < 2.0)
      ruby-progressbar (~> 1.7)
      unicode-display_width (>= 2.4.0, < 4.0)
-    rubocop-ast (1.49.1)
+    rubocop-ast (1.50.0)
      parser (>= 3.3.7.2)
      prism (~> 1.7)
-    rubocop-minitest (0.39.1)
+    rubocop-minitest (0.40.0)
      lint_roller (~> 1.1)
      rubocop (>= 1.75.0, < 2.0)
      rubocop-ast (>= 1.38.0, < 2.0)
@@ -66,7 +66,7 @@ DEPENDENCIES
  rake-compiler-dock (~> 1.12)
  regorusrb!
  rubocop (~> 1.88)
-  rubocop-minitest (~> 0.39.1)
+  rubocop-minitest (~> 0.40.0)
  rubocop-rake (~> 0.7.1)

 BUNDLED WITH
--- a/bindings/wasm/Cargo.lock
+++ b/bindings/wasm/Cargo.lock
@@ -42,19 +42,19 @@ dependencies = [

 [[package]]
 name = "anyhow"
-version = "1.0.103"
+version = "1.0.104"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2a4385e2e34eb35d6b3efe798b9eb88096925d87726c0798709bf56d9ed84af3"
+checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470"

 [[package]]
 name = "async-trait"
-version = "0.1.89"
+version = "0.1.91"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9035ad2d096bed7955a320ee7e2230574d28fd3c3a0f186cbea1ff3c7eed5dbb"
+checksum = "ae36dc4177970ef04fde5178d3e2429882def40e57a451f919c098f72baa6cec"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
@@ -120,9 +120,9 @@ checksum = "37b2a672a2cb129a2e41c10b1224bb368f9f37a2b16b612598138befd7b37eb5"

 [[package]]
 name = "cc"
-version = "1.2.67"
+version = "1.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e17dd265a7d0f31ef544e1b20e03add05d3b45b491b633b10d67145d2acc1a38"
+checksum = "c89588d05638b5b4594a3348a2d6c20277e43a7f5c5202b05cc56888475a47b8"
 dependencies = [
 "find-msvc-tools",
 "shlex",
@@ -206,7 +206,7 @@ checksum = "1ac70aa55017e108007fbaf5aa0f54b021c98f92ff8af59d42eda9da96e3dd4f"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -291,21 +291,21 @@ dependencies = [

 [[package]]
 name = "futures-core"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7e3450815272ef58cec6d564423f6e755e25379b217b0bc688e295ba24df6b1d"
+checksum = "2cd50c473c80f6d7c3670a752354b8e569b1a7cbfdc0419ec88e5edad85e0dc7"

 [[package]]
 name = "futures-task"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "037711b3d59c33004d3856fbdc83b99d4ff37a24768fa1be9ce3538a1cde4393"
+checksum = "b231ed28831efb4a61a08580c4bc233ec56bc009f4cd8f52da2c3cb97df0c109"

 [[package]]
 name = "futures-util"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "389ca41296e6190b48053de0321d02a77f32f8a5d2461dd38762c0593805c6d6"
+checksum = "a77a90a256fce34da66415271e30f94ee91c57b04b8a2c042d9cf3220179deaa"
 dependencies = [
 "futures-core",
 "futures-task",
@@ -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"
@@ -377,6 +383,12 @@ dependencies = [
 "foldhash",
 ]

+[[package]]
+name = "heck"
+version = "0.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea"
+
 [[package]]
 name = "iana-time-zone"
 version = "0.1.65"
@@ -504,6 +516,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 +533,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9"
 dependencies = [
 "equivalent",
- "hashbrown",
+ "hashbrown 0.17.1",
 "serde",
 "serde_core",
 ]
@@ -541,9 +563,9 @@ dependencies = [

 [[package]]
 name = "jsonschema"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "281c43ff06dcb331e9356d30e38853d559ce3d0a3f693e0b0e102667dec14fb1"
+checksum = "f05a6cff806294a7699d48761d4ae2bdebab7fa2eef05e4a0b83320f0ff46901"
 dependencies = [
 "ahash",
 "bytecount",
@@ -555,6 +577,7 @@ dependencies = [
 "idna",
 "itoa",
 "jsonschema-regex",
+ "jsonschema-value",
 "num-cmp",
 "num-traits",
 "percent-encoding",
@@ -562,19 +585,34 @@ dependencies = [
 "regex",
 "serde",
 "serde_json",
+ "strum",
 "unicode-general-category",
 "uuid-simd",
 ]

 [[package]]
 name = "jsonschema-regex"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ee0b351864e7ffbc5db9273daf7fa1b4d5177b0946713d667ca571b83c0b4045"
+checksum = "84708dd3f6c5327478a96f37378adb27deed6a626cf84d19de780d9e8ae84b17"
 dependencies = [
 "regex-syntax",
 ]

+[[package]]
+name = "jsonschema-value"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fd8c04ab4ce60e42c4e302d3bd9d184652bb56f212495d2eea23573bcbf72556"
+dependencies = [
+ "ahash",
+ "bytecount",
+ "fraction",
+ "num-cmp",
+ "num-traits",
+ "serde_json",
+]
+
 [[package]]
 name = "lazy_static"
 version = "1.5.0"
@@ -583,9 +621,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"

 [[package]]
 name = "libc"
-version = "0.2.186"
+version = "0.2.189"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66"
+checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2"

 [[package]]
 name = "libm"
@@ -843,18 +881,18 @@ dependencies = [

 [[package]]
 name = "proc-macro2"
-version = "1.0.106"
+version = "1.0.107"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
 dependencies = [
 "unicode-ident",
 ]

 [[package]]
 name = "quote"
-version = "1.0.46"
+version = "1.0.47"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dfbc457d0c7a0759a614551b11a6409e5951f6c7537be1f1b7682b9ae9230368"
+checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
 dependencies = [
 "proc-macro2",
 ]
@@ -899,34 +937,34 @@ dependencies = [

 [[package]]
 name = "ref-cast"
-version = "1.0.25"
+version = "1.0.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f354300ae66f76f1c85c5f84693f0ce81d747e2c3f21a45fef496d89c960bf7d"
+checksum = "216e8f773d7923bcba9ceb86a86c93cabb3903a11872fc3f138c49630e50b96d"
 dependencies = [
 "ref-cast-impl",
 ]

 [[package]]
 name = "ref-cast-impl"
-version = "1.0.25"
+version = "1.0.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7186006dcb21920990093f30e3dea63b7d6e977bf1256be20c3563a5db070da"
+checksum = "2c9283685feec7d69af75fb0e858d5e7378f33fe4fc699383b2916ab9273e03c"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
 name = "referencing"
-version = "0.47.0"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "348e860aeb0b7bd035778fd11dd9cd5290d32e4aed3b8f2274a00287a9fd362b"
+checksum = "980e77f5cfffc592c0e7dfb6d20770a0b96a6ab94d403de7454ed9799505e4ba"
 dependencies = [
 "ahash",
 "fluent-uri",
 "getrandom 0.3.4",
- "hashbrown",
+ "hashbrown 0.17.1",
 "itoa",
 "micromap",
 "parking_lot",
@@ -972,7 +1010,7 @@ dependencies = [
 "chrono-tz",
 "data-encoding",
 "globset",
- "indexmap",
+ "indexmap 2.14.0",
 "ipnet",
 "jsonschema",
 "lazy_static",
@@ -992,6 +1030,7 @@ dependencies = [
 "thiserror",
 "url",
 "uuid",
+ "vstd",
 ]

 [[package]]
@@ -1045,9 +1084,9 @@ checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd"

 [[package]]
 name = "serde"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e"
+checksum = "4148590afebada386688f18773da617792bf2ef03ffc1e4cbd2b1d45b023e0ba"
 dependencies = [
 "serde_core",
 "serde_derive",
@@ -1066,29 +1105,29 @@ dependencies = [

 [[package]]
 name = "serde_core"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad"
+checksum = "67dca2c9c51e58a4791a4b1ed58308b39c64224d349a935ab5039aa360942a48"
 dependencies = [
 "serde_derive",
 ]

 [[package]]
 name = "serde_derive"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79"
+checksum = "e7a5d71263a5a7d47b41f6b3f06ba276f10cc18b0931f1799f710578e2309348"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
 name = "serde_json"
-version = "1.0.150"
+version = "1.0.151"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e8014e44b4736ed0538adeecded0fce2a272f22dc9578a7eb6b2d9993c74cfb9"
+checksum = "c841b55ecdae098c80dcae9cf767f6f8a0c2cdb3416bbef72181df4d0fe73f14"
 dependencies = [
 "itoa",
 "memchr",
@@ -1103,7 +1142,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",
@@ -1146,6 +1185,27 @@ version = "1.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6ce2be8dc25455e1f91df71bfa12ad37d7af1092ae736f3a6cd0e37bc7810596"

+[[package]]
+name = "strum"
+version = "0.28.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9628de9b8791db39ceda2b119bbe13134770b56c138ec1d3af810d045c04f9bd"
+dependencies = [
+ "strum_macros",
+]
+
+[[package]]
+name = "strum_macros"
+version = "0.28.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ab85eea0270ee17587ed4156089e10b9e6880ee688791d45a905f5b1ca36f664"
+dependencies = [
+ "heck",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.119",
+]
+
 [[package]]
 name = "syn"
 version = "2.0.119"
@@ -1157,6 +1217,17 @@ dependencies = [
 "unicode-ident",
 ]

+[[package]]
+name = "syn"
+version = "3.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "53e9bae58849f64dfa4f5d5ae372c8341f7305f82a3868709269343628b659a3"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
 [[package]]
 name = "synstructure"
 version = "0.13.2"
@@ -1165,27 +1236,27 @@ checksum = "728a70f3dbaf5bab7f0c4b1ac8d7ae5ea60a4b5549c8a5914361c99147a709d2"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
 name = "thiserror"
-version = "2.0.18"
+version = "2.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4"
+checksum = "09a43598840e33d5b0331f38c5e30d13bb11c11210a4b58f0d9b18a5a5eefcd9"
 dependencies = [
 "thiserror-impl",
 ]

 [[package]]
 name = "thiserror-impl"
-version = "2.0.18"
+version = "2.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ebc4ee7f67670e9b64d05fa4253e753e016c6c95ff35b89b7941d6b856dec1d5"
+checksum = "43cbfe0cf76104d42a574802844187e84a305e531ed54455f11fbde0f10541cd"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 3.0.3",
 ]

 [[package]]
@@ -1262,12 +1333,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 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",
+ "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"
@@ -1335,7 +1470,7 @@ dependencies = [
 "bumpalo",
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "wasm-bindgen-shared",
 ]

@@ -1378,7 +1513,7 @@ checksum = "94eb68555b95bcea5e8cf4abe280b529049479fa995bfc23734af96a6aedc120"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1417,7 +1552,7 @@ checksum = "053e2e040ab57b9dc951b72c264860db7eb3b0200ba345b4e4c3b14f67855ddf"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1428,7 +1563,7 @@ checksum = "3f316c4a2570ba26bbec722032c4099d8c8bc095efccdc15688708623367e358"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1495,28 +1630,28 @@ checksum = "de844c262c8848816172cef550288e7dc6c7b7814b4ee56b3e1553f275f1858e"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "synstructure",
 ]

 [[package]]
 name = "zerocopy"
-version = "0.8.54"
+version = "0.8.55"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7cbbc0a705a0fd05cc3676525980d2bf5a9bc4adac6d6475209a7887cf59d19"
+checksum = "b5a105cd7b140f6eeec8acff2ea38135d3cab283ada58540f629fe51e46696eb"
 dependencies = [
 "zerocopy-derive",
 ]

 [[package]]
 name = "zerocopy-derive"
-version = "0.8.54"
+version = "0.8.55"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e2e817b7b52d0c7358d3246da9d69935ebb18116b2b102b4230dac079b4862f5"
+checksum = "0fe976fb70c78cd64cccfe3a6fc142244e8a77b70959b30faf9d0ac37ee228eb"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
@@ -1536,7 +1671,7 @@ checksum = "11532158c46691caf0f2593ea8358fed6bbf68a0315e80aae9bd41fbade684a1"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 "synstructure",
 ]

@@ -1570,7 +1705,7 @@ checksum = "625dc425cab0dca6dc3c3319506e6593dcb08a9f387ea3b284dbd52a92c40555"
 dependencies = [
 "proc-macro2",
 "quote",
- "syn",
+ "syn 2.0.119",
 ]

 [[package]]
--- a/src/interpreter.rs
+++ b/src/interpreter.rs
@@ -1258,7 +1258,34 @@ impl Interpreter {
            // Apply with modifiers.
            for wm in &stmt.with_mods {
                let path = Parser::get_path_ref_components(&wm.refr)?;
-                let path: Vec<&str> = path.iter().map(|s| s.text()).collect();
+                let mut path: Vec<String> = path.iter().map(|s| s.text().to_string()).collect();
+
+                // Matching OPA, a leading import alias is rewritten before
+                // any lookups: functions register as overrides below,
+                // anything else becomes a data override. Only the alias
+                // component is replaced so bracketed keys containing dots
+                // survive the rewrite.
+                let rewritten: Option<Vec<String>> = match path.split_first() {
+                    Some((head, rest)) if head.as_str() != "data" => {
+                        self.lookup_import(head).and_then(|import_expr| {
+                            // Use the import target's parsed components, not
+                            // its dot-joined string, so bracketed keys
+                            // containing dots survive in the import path too.
+                            let comps = Parser::get_path_ref_components(import_expr).ok()?;
+                            Some(
+                                comps
+                                    .iter()
+                                    .map(|s| s.text().to_string())
+                                    .chain(rest.iter().cloned())
+                                    .collect(),
+                            )
+                        })
+                    }
+                    _ => None,
+                };
+                if let Some(new_path) = rewritten {
+                    path = new_path;
+                }
                let mut target = path.join(".");

                let mut target_is_function = self.lookup_function_by_name(&target).is_some()
@@ -1297,11 +1324,17 @@ impl Interpreter {
                            if self.lookup_function_by_name(&function_path).is_none() {
                                // Lookup without current module path prefixed.
                                function_path = get_path_string(&wm.r#as, None)?;
-                                if self.lookup_function_by_name(&function_path).is_none()
-                                    && !Self::is_builtin(wm.r#as.span(), &function_path)
-                                {
-                                    // bail!(wm.r#as.span().error("could not evaluate expression"));
-                                    skip_exec = true;
+                                if self.lookup_function_by_name(&function_path).is_none() {
+                                    // Resolve an aliased replacement before builtins.
+                                    let resolved = self
+                                        .resolve_fcn_path_through_imports(&function_path)
+                                        .filter(|r| self.compiled_policy.functions.contains_key(r));
+                                    if let Some(resolved) = resolved {
+                                        function_path = resolved;
+                                    } else if !Self::is_builtin(wm.r#as.span(), &function_path) {
+                                        // bail!(wm.r#as.span().error("could not evaluate expression"));
+                                        skip_exec = true;
+                                    }
                                }
                            }
                            self.with_functions
@@ -2371,6 +2404,72 @@ impl Interpreter {
        }
    }

+    /// Look up the import of the current module with the given alias, e.g.
+    /// the `data.a.b` import expression for `b` after `import data.a.b`.
+    fn lookup_import(&self, alias: &str) -> Option<&Ref<Expr>> {
+        if self.compiled_policy.imports.is_empty() {
+            return None;
+        }
+        let import_key = format!("{}.{}", self.current_module_path, alias);
+        self.compiled_policy.imports.get(&import_key)
+    }
+
+    /// Look up the dot-joined target path of an import of the current module
+    /// with the given alias, e.g. `data.a.b` for `b` after `import data.a.b`.
+    fn lookup_import_alias(&self, alias: &str) -> Option<String> {
+        get_path_string(self.lookup_import(alias)?, None).ok()
+    }
+
+    /// Rewrite a path whose leading component is an import alias of the
+    /// current module to the import's target, e.g. `b.f` to `data.a.b.f`
+    /// after `import data.a.b`.
+    fn rewrite_path_through_imports(&self, path: &str) -> Option<String> {
+        if path.starts_with("data.") {
+            return None;
+        }
+
+        let (alias, rest) = match path.split_once('.') {
+            Some((alias, rest)) => (alias, Some(rest)),
+            None => (path, None),
+        };
+        let target = self.lookup_import_alias(alias)?;
+        Some(match rest {
+            Some(rest) => format!("{target}.{rest}"),
+            None => target,
+        })
+    }
+
+    /// Rewrite an import-aliased call path to its target, e.g. `b.f(1)` to
+    /// `data.a.b.f` after `import data.a.b`. Resolves only when the target is
+    /// a known function or default function, so an alias whose target defines
+    /// the called function shadows a like-named builtin namespace, while other
+    /// spellings keep their prior meaning (e.g. a builtin call). OPA instead
+    /// rewrites aliases unconditionally and rejects calls to a missing target
+    /// at compile time.
+    fn resolve_fcn_path_through_imports(&self, path: &str) -> Option<String> {
+        let candidate = self.rewrite_path_through_imports(path)?;
+        (self.compiled_policy.functions.contains_key(&candidate)
+            || self.is_default_function(&candidate))
+        .then_some(candidate)
+    }
+
+    /// True if `path` is the exact path of a `default` function rule.
+    /// `default_rules` also indexes every prefix of a rule path, so it cannot
+    /// be consulted alone: `rule_paths` holds only exact rule paths, and the
+    /// non-empty argument list distinguishes functions from value rules.
+    fn is_default_function(&self, path: &str) -> bool {
+        self.compiled_policy.rule_paths.contains(path)
+            && self
+                .compiled_policy
+                .default_rules
+                .get(path)
+                .is_some_and(|rules| {
+                    rules.iter().any(|(rule, _)| {
+                        matches!(rule.as_ref(), Rule::Default { args, .. } if !args.is_empty())
+                    })
+                })
+    }
+
    fn eval_builtin_call(
        &mut self,
        span: &Span,
@@ -2542,6 +2641,13 @@ impl Interpreter {
            param_values.push(self.eval_expr(p)?);
        }

+        // Resolve a leading import alias before the `with` override and builtin
+        // lookups, so an override keyed by the full path reaches aliased calls
+        // and the alias shadows a like-named builtin namespace (matching OPA).
+        let fcn_path = self
+            .resolve_fcn_path_through_imports(&fcn_path)
+            .unwrap_or(fcn_path);
+
        let orig_fcn_path = fcn_path.clone();

        let mut with_functions_saved = None;
@@ -2718,7 +2824,12 @@ impl Interpreter {
            let value = match self.eval_rule_bodies(ctx, span, bodies) {
                Ok(v) => v,
                Err(e) => {
-                    // If the rule produces an error, save the error.
+                    // If the rule produces an error, save the error. Restore
+                    // the caller's module even so: leaving the callee's module
+                    // in place would make the rest of the caller's body
+                    // resolve paths through the wrong module's imports when
+                    // the error is swallowed below in non-strict mode.
+                    self.set_current_module(prev_module)?;
                    errors.push(e);
                    self.scopes = scopes;
                    continue;
--- a/src/languages/rego/compiler/function_calls.rs
+++ b/src/languages/rego/compiler/function_calls.rs
@@ -63,6 +63,9 @@ impl<'a> Compiler<'a> {
        let original_fcn_path = fcn_path.clone();
        let full_fcn_path = if self.policy.inner.rules.contains_key(&fcn_path) {
            fcn_path
+        } else if let Some(resolved) = self.resolve_fcn_path_through_imports(&original_fcn_path) {
+            // Resolve a leading import alias before module-prefixing and builtins.
+            resolved
        } else {
            get_path_string(fcn, Some(&self.current_package))
                .map_err(|_| CompilerError::InvalidFunctionExpressionWithPackage.at(&span))?
@@ -220,6 +223,37 @@ impl<'a> Compiler<'a> {
        Ok(dest)
    }

+    /// Rewrite an import-aliased call path to its target, e.g. `b.f(1)` to
+    /// `data.a.b.f` after `import data.a.b`. Resolves only when the target is
+    /// a known function (the `rules` map cannot be used here: it also indexes
+    /// value rules and every rule-path prefix, which must not become callable
+    /// through an alias), so an alias whose target defines the called
+    /// function shadows a like-named builtin namespace, while other spellings
+    /// keep their prior meaning (e.g. a builtin call). OPA instead rewrites
+    /// aliases unconditionally and rejects calls to a missing target at
+    /// compile time.
+    fn resolve_fcn_path_through_imports(&self, path: &str) -> Option<String> {
+        if self.policy.inner.imports.is_empty() || path.starts_with("data.") {
+            return None;
+        }
+        let (alias, rest) = match path.split_once('.') {
+            Some((alias, rest)) => (alias, Some(rest)),
+            None => (path, None),
+        };
+        let import_key = format!("{}.{}", self.current_package, alias);
+        let import_expr = self.policy.inner.imports.get(&import_key)?;
+        let target = get_path_string(import_expr, None).ok()?;
+        let candidate = match rest {
+            Some(rest) => format!("{target}.{rest}"),
+            None => target,
+        };
+        self.policy
+            .inner
+            .functions
+            .contains_key(&candidate)
+            .then_some(candidate)
+    }
+
    fn lookup_builtin_arity(&self, name: &str) -> Option<usize> {
        if name == "print" {
            Some(2)
--- a/src/number.rs
+++ b/src/number.rs
@@ -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)]
@@ -140,13 +144,9 @@ impl Number {
        }
    }

-    fn ints_to_bigint(a: &Number, b: &Number) -> (BigInt, BigInt) {
-        (a.to_bigint_owned().unwrap(), b.to_bigint_owned().unwrap())
-    }
-
    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)
    }
@@ -587,7 +587,11 @@ impl Number {
                }
            }
            (Number::Int(a), Number::Int(b)) => {
-                if *a % *b == 0 {
+                if *a == i64::MIN && *b == -1 {
+                    // Rust panics on i64::MIN % -1i64, so handle it specially
+                    let quotient = BigInt::from(*a) / BigInt::from(*b);
+                    Ok(Number::from_bigint_owned(quotient))
+                } else if *a % *b == 0 {
                    if let Some(q) = a.checked_div(*b) {
                        Ok(Number::Int(q))
                    } else {
@@ -656,15 +660,17 @@ impl Number {
    }

    pub fn modulo(self, rhs: &Self) -> Result<Number> {
-        if rhs.is_zero() {
+        // Conversion fails for a non-integral float, and also for an integral
+        // one whose magnitude exceeds 2^53, which cannot be represented exactly.
+        let (a, b) = match (self.to_bigint_owned(), rhs.to_bigint_owned()) {
+            (Some(a), Some(b)) => (a, b),
+            _ => bail!("modulo on floating-point number"),
+        };
+
+        if b.is_zero() {
            bail!("modulo by zero");
        }

-        if !self.is_integer() || !rhs.is_integer() {
-            bail!("modulo on floating-point number");
-        }
-
-        let (a, b) = Number::ints_to_bigint(&self, rhs);
        let rem = a % &b;
        Ok(Number::from_bigint_owned(rem))
    }
@@ -685,6 +691,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()?))
@@ -776,7 +783,8 @@ impl Number {
        if e >= 0 {
            Ok(two_pow_positive(e as u32))
        } else {
-            let denom = two_pow_positive((-e) as u32);
+            // Must cast to i64 before negating in case it's i32::MIN
+            let denom = two_pow_positive((-(e as i64)) as u32);
            Number::from(1u64).divide(&denom)
        }
    }
@@ -785,7 +793,8 @@ impl Number {
        if e >= 0 {
            Ok(ten_pow_positive(e as u32))
        } else {
-            let denom = ten_pow_positive((-e) as u32);
+            // Must cast to i64 before negating in case it's i32::MIN
+            let denom = ten_pow_positive((-(e as i64)) as u32);
            Number::from(1u64).divide(&denom)
        }
    }
@@ -984,3 +993,67 @@ fn scientific_parts_to_bigint(mantissa: &str, exponent: i32) -> Option<BigInt> {

    Some(value)
 }
+
+#[cfg(test)]
+mod tests {
+    #![allow(clippy::expect_used)] // tests expect() to assert arithmetic results
+
+    use super::*;
+    use alloc::string::ToString;
+
+    /// Regression test: `i64::MIN / -1` overflows `i64` and panics in Rust's
+    /// native integer division/remainder. `divide` must promote the result
+    /// instead of panicking.
+    #[test]
+    fn i64_min_by_negative_one() {
+        let quotient = Number::Int(i64::MIN)
+            .divide(&Number::Int(-1))
+            .expect("division should succeed");
+
+        // 2^63 does not fit in i64, but does fit in u64.
+        assert_eq!(quotient.as_u64(), Some(9_223_372_036_854_775_808));
+        assert_eq!(quotient.as_i64(), None);
+        assert_eq!(quotient.as_i128(), Some(9_223_372_036_854_775_808));
+        assert_eq!(
+            *quotient.to_big().expect("to_big should succeed"),
+            -BigInt::from(i64::MIN)
+        );
+
+        // The same overflow case reached via the mixed `Int`/`BigInt` path.
+        let big_quotient = Number::Int(i64::MIN)
+            .divide(&Number::BigInt(Rc::new(BigInt::from(-1))))
+            .expect("division should succeed");
+        assert_eq!(big_quotient.as_u64(), Some(9_223_372_036_854_775_808));
+
+        // `i64::MIN % -1` also panics natively; the result must be zero.
+        let remainder = Number::Int(i64::MIN)
+            .modulo(&Number::Int(-1))
+            .expect("modulo should succeed");
+        assert_eq!(remainder.as_i64(), Some(0));
+    }
+
+    #[test]
+    fn modulo_handles_floats_that_are_really_integers() {
+        // An integral float is a valid operand.
+        assert!(matches!(
+            Number::Float(4.0).modulo(&Number::Int(3)),
+            Ok(Number::UInt(1))
+        ));
+        // `1e300` has no fractional part, but it is too large to convert to an
+        // integer exactly. This must report an error, not panic.
+        assert_eq!(
+            Number::Float(1e300)
+                .modulo(&Number::Int(3))
+                .err()
+                .map(|e| e.to_string()),
+            Some("modulo on floating-point number".to_string())
+        );
+        assert_eq!(
+            Number::Int(3)
+                .modulo(&Number::Float(1e300))
+                .err()
+                .map(|e| e.to_string()),
+            Some("modulo on floating-point number".to_string())
+        );
+    }
+}
--- a/src/rvm/vm/comprehension.rs
+++ b/src/rvm/vm/comprehension.rs
@@ -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,
--- a/tests/interpreter/cases/builtins/numbers/mod.yaml
+++ b/tests/interpreter/cases/builtins/numbers/mod.yaml
@@ -62,3 +62,12 @@ cases:
        x = 1 % 1.1
    query: data.test
    error: modulo on floating-point number
+
+  - note: integral float too large to convert
+    data: {}
+    modules:
+      - |
+        package test
+        x = 100000000000000000e-1 % 2
+    query: data.test
+    error: modulo on floating-point number
--- a/tests/interpreter/cases/import/tests.yaml
+++ b/tests/interpreter/cases/import/tests.yaml
@@ -188,3 +188,435 @@ cases:
        import input
    query: data.test
    want_result: {}
+  - note: function call through import
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        result := lib.double(21)
+    query: data.rules.result
+    want_result: 42
+  - note: function call through import alias
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import rego.v1
+        import data.lib as l
+
+        result := l.double(21)
+    query: data.rules.result
+    want_result: 42
+  - note: function imported directly
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import rego.v1
+        import data.lib.double
+
+        result := double(21)
+    query: data.rules.result
+    want_result: 42
+  - note: function call through import, nested package
+    modules:
+      - |
+        package a.b.c
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import rego.v1
+        import data.a
+
+        result := a.b.c.double(21)
+    query: data.rules.result
+    want_result: 42
+  - note: default function value via import
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        default pick(_) := "fallback"
+
+        pick(x) := x if x == "a"
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        a := lib.pick("a")
+        b := lib.pick("z")
+    query: data.rules
+    want_result:
+      a: a
+      b: fallback
+  - note: with override applies to function call through import
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package lib2
+        import rego.v1
+
+        fake(x) := 1000 + x
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        result := lib.double(5)
+
+        main := x if {
+          x := result with data.lib.double as data.lib2.fake
+        }
+    query: data.rules.main
+    want_result: 1005
+  - note: with override target written through import alias
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package lib2
+        import rego.v1
+
+        fake(x) := 1000 + x
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        result := data.lib.double(5)
+
+        main := x if {
+          x := result with lib.double as data.lib2.fake
+        }
+    query: data.rules.main
+    want_result: 1005
+  - note: with override replacement written through import alias
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package lib2
+        import rego.v1
+
+        fake(x) := 1000 + x
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+        import data.lib2
+
+        result := data.lib.double(5)
+
+        main := x if {
+          x := result with data.lib.double as lib2.fake
+        }
+    query: data.rules.main
+    want_result: 1005
+  - note: import alias shadows builtin namespace
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        unmarshal(_) := {"from": "lib"}
+      - |
+        package rules
+        import rego.v1
+        import data.lib as json
+
+        result := json.unmarshal(`[1,2]`)
+    query: data.rules.result
+    want_result:
+      from: lib
+  - note: with override target written through builtin-shadowing alias
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        unmarshal(_) := {"from": "lib"}
+      - |
+        package lib2
+        import rego.v1
+
+        unmarshal(_) := {"from": "lib2"}
+      - |
+        package rules
+        import rego.v1
+        import data.lib as json
+
+        result := json.unmarshal(`[1]`)
+
+        main := x if {
+          x := result with json.unmarshal as data.lib2.unmarshal
+        }
+    query: data.rules.main
+    want_result:
+      from: lib2
+  - note: with override replacement written through builtin-shadowing alias
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package lib2
+        import rego.v1
+
+        unmarshal(_) := {"from": "lib2"}
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+        import data.lib2 as json
+
+        result := lib.double(5)
+
+        main := x if {
+          x := result with data.lib.double as json.unmarshal
+        }
+    query: data.rules.main
+    want_result:
+      from: lib2
+  - note: with override target aliasing a non-function rule overrides the value
+    modules:
+      - |
+        package flib
+        import rego.v1
+
+        default flag := false
+
+        flag := true if input.x == 1
+      - |
+        package rules
+        import rego.v1
+        import data.flib as fl
+
+        result := data.flib.flag
+
+        main := x if {
+          x := result with fl.flag as 5
+        }
+    query: data.rules.main
+    want_result: 5
+  - note: import shadows module-local rule for function calls
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        lib.double(x) := 100 * x
+
+        main := lib.double(3)
+    query: data.rules.main
+    want_result: 6
+  - note: import shadows module-local value rule for function calls
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        lib.double := 7
+
+        main := lib.double(3)
+    query: data.rules.main
+    want_result: 6
+  - note: fully qualified function call with import present
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        result := data.lib.double(21)
+    query: data.rules.result
+    want_result: 42
+  - note: unknown function through import is an error
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        result := lib.missing(1)
+    query: data.rules.result
+    error: could not find function
+  - note: function call in module without imports
+    modules:
+      - |
+        package rules
+
+        double(x) := 2 * x
+
+        result := double(21)
+    query: data.rules.result
+    want_result: 42
+  - note: call to non-function value rule through import is an error
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        x := 5
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        result := lib.x(1)
+    query: data.rules.result
+    error: could not find function
+  - note: call to rule path prefix through import is an error
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        a.c := 9
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        result := lib.a(7)
+    query: data.rules.result
+    error: could not find function
+  - note: call to prefix of default function through import is an error
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        default a.b(_) := 1
+
+        a.b(x) := x * 2 if x > 10
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        result := lib.a(7)
+    query: data.rules.result
+    error: could not find function
+  - note: default-only function call through import
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        default dfl(_) := 42
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        result := lib.dfl(5)
+    query: data.rules.result
+    want_result: 42
+  - note: overload error does not leak callee module imports
+    strict: false
+    modules:
+      - |
+        package libx
+        import rego.v1
+
+        h(_) := "WRONG"
+      - |
+        package liby
+        import rego.v1
+
+        h(_) := "RIGHT"
+      - |
+        package lib
+        import rego.v1
+        import data.libx as ali
+
+        m(_) := 1
+
+        m(_) := 2
+
+        f(x) := 100 if x == 1
+
+        f(x) := y if {
+          x == 1
+          y := m(1)
+        }
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+        import data.liby as ali
+
+        main := [v, w] if {
+          v := lib.f(1)
+          w := ali.h(1)
+        }
+    query: data.rules.main
+    want_result: [100, "RIGHT"]
+  - note: with target through dotted bracket key import
+    data:
+      "a.b":
+        x: 1
+    modules:
+      - |
+        package rules
+        import rego.v1
+        import data["a.b"] as ab
+
+        main := x if {
+          x := data["a.b"].x with ab.x as 2
+        }
+    query: data.rules.main
+    want_result: 2
--- a/tests/rvm/rego/cases/imports.yaml
+++ b/tests/rvm/rego/cases/imports.yaml
@@ -95,3 +95,204 @@ cases:
        }
    query: data.rules.present
    want_result: true
+  - note: import_function_call
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import data.lib
+        import rego.v1
+
+        result := lib.double(21)
+    query: data.rules.result
+    want_result: 42
+  - note: import_function_call_alias
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import data.lib as mylib
+        import rego.v1
+
+        result := mylib.double(21)
+    query: data.rules.result
+    want_result: 42
+  - note: import_function_directly
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import data.lib.double
+        import rego.v1
+
+        result := double(21)
+    query: data.rules.result
+    want_result: 42
+  - note: import_function_call_nested_package
+    modules:
+      - |
+        package a.b.c
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import data.a
+        import rego.v1
+
+        result := a.b.c.double(21)
+    query: data.rules.result
+    want_result: 42
+  - note: import_alias_shadows_builtin_namespace
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        unmarshal(_) := {"from": "lib"}
+      - |
+        package rules
+        import rego.v1
+        import data.lib as json
+
+        result := json.unmarshal(`[1,2]`)
+    query: data.rules.result
+    want_result:
+      from: lib
+  - note: default_function_value_via_import
+    skip: true  # TODO: cross-package calls to functions with default values fail to compile ("not a valid rule path"), even with fully-qualified paths
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        default pick(_) := "fallback"
+
+        pick(x) := x if x == "a"
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        a := lib.pick("a")
+        b := lib.pick("z")
+    query: data.rules
+    want_result:
+      a: a
+      b: fallback
+  - note: import_shadows_module_local_rule_for_function_calls
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        lib.double(x) := 100 * x
+
+        main := lib.double(3)
+    query: data.rules.main
+    want_result: 6
+  - note: import_shadows_module_local_value_rule_for_function_calls
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        lib.double := 7
+
+        main := lib.double(3)
+    query: data.rules.main
+    want_result: 6
+  - note: import_fully_qualified_function_call
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        result := data.lib.double(21)
+    query: data.rules.result
+    want_result: 42
+  - note: unknown_function_through_import
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        double(x) := 2 * x
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        result := lib.missing(1)
+    query: data.rules.result
+    want_error: "Unknown function"
+  - note: function_call_without_imports
+    modules:
+      - |
+        package rules
+
+        double(x) := 2 * x
+
+        result := double(21)
+    query: data.rules.result
+    want_result: 42
+  - note: non_function_value_rule_through_import
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        x := 5
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        result := lib.x(1)
+    query: data.rules.result
+    want_error: "Unknown function"
+  - note: rule_path_prefix_through_import
+    modules:
+      - |
+        package lib
+        import rego.v1
+
+        a.c := 9
+      - |
+        package rules
+        import rego.v1
+        import data.lib
+
+        result := lib.a(7)
+    query: data.rules.result
+    want_error: "Unknown function"