Spec for Number as Ord

Simpler spec for Number::eq
Simplify Number::eq spec
2026-08-05 02:16:11 +00:00 · 2026-03-19 15:52:41 -07:00 · 2026-03-19 14:48:03 -07:00 · 2026-03-19 13:58:10 -07:00 · 2026-03-19 11:52:35 -07:00 · 2026-03-19 11:33:30 -07:00
36 changed files with 1721 additions and 153 deletions
--- a/.github/dependabot.yml
+++ b/.github/dependabot.yml
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 # To get started with Dependabot version updates, you'll need to specify which
 # package ecosystems to update and where the package manifests are located.
 # Please see the documentation for all configuration options:
@@ -9,3 +11,137 @@ updates:
    directory: "/" # Location of package manifests
    schedule:
      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
+    # Ignore vendored mimalloc crates; updates are managed manually.
+    ignore:
+      - dependency-name: "regorus-mimalloc"
+      - dependency-name: "regorus-mimalloc-sys"
+
+  - package-ecosystem: "cargo"
+    directory: "/bindings/ffi"
+    schedule:
+      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
+
+  - package-ecosystem: "cargo"
+    directory: "/bindings/java"
+    schedule:
+      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
+
+  - package-ecosystem: "cargo"
+    directory: "/bindings/python"
+    schedule:
+      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
+
+  - package-ecosystem: "cargo"
+    directory: "/bindings/ruby"
+    schedule:
+      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
+
+  - package-ecosystem: "cargo"
+    directory: "/bindings/ruby/ext/regorusrb"
+    schedule:
+      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
+
+  - package-ecosystem: "cargo"
+    directory: "/bindings/wasm"
+    schedule:
+      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
+
+  - package-ecosystem: "cargo"
+    directory: "/tests/ensure_no_std"
+    schedule:
+      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
+
+  - package-ecosystem: "cargo"
+    directory: "/xtask"
+    schedule:
+      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
+
+  - package-ecosystem: "gomod"
+    directory: "/bindings/go"
+    schedule:
+      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
+
+  - package-ecosystem: "maven"
+    directory: "/bindings/java"
+    schedule:
+      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
+
+  - package-ecosystem: "nuget"
+    directory: "/bindings/csharp"
+    schedule:
+      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
+
+  - package-ecosystem: "pip"
+    directory: "/bindings/python"
+    schedule:
+      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
+
+  - package-ecosystem: "bundler"
+    directory: "/bindings/ruby"
+    schedule:
+      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
+
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      interval: "weekly"
+    groups:
+      per-dependency:
+        patterns:
+          - "*"
--- a/.github/workflows/codeql.yml
+++ b/.github/workflows/codeql.yml
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: "CodeQL Security Analysis"

 on:
@@ -60,7 +62,7 @@ jobs:

    steps:
    - name: Checkout repository
-      uses: actions/checkout@v4
+      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

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

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

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

    - name: Setup Go
      if: matrix.language == 'go'
-      uses: actions/setup-go@v5
+      uses: actions/setup-go@7a3fe6cf4cb3a834922a1244abfce67bcef6a0c5 # v6.2.0
      with:
        go-version: '1.21'

    - name: Setup .NET
      if: matrix.language == 'csharp'
-      uses: actions/setup-dotnet@v4
+      uses: actions/setup-dotnet@baa11fbfe1d6520db94683bd5c7a3818018e4309 # v5.1.0
      with:
        global-json-file: ./bindings/csharp/global.json

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

    - name: Setup Node.js
      if: matrix.language == 'javascript-typescript'
-      uses: actions/setup-node@v4
+      uses: actions/setup-node@6044e13b5dc448c55e2357c09f80417699197238 # v6.2.0
      with:
        node-version: '18'

    - name: Initialize CodeQL
-      uses: github/codeql-action/init@v3
+      uses: github/codeql-action/init@45cbd0c69e560cd9e7cd7f8c32362050c9b7ded2 # v4.32.2
      with:
        languages: ${{ matrix.language }}
        build-mode: ${{ matrix.build-mode }}
@@ -139,7 +141,7 @@ jobs:

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

    - name: Perform CodeQL Analysis
-      uses: github/codeql-action/analyze@v3
+      uses: github/codeql-action/analyze@45cbd0c69e560cd9e7cd7f8c32362050c9b7ded2 # v4.32.2
      with:
        category: "/language:${{matrix.language}}"
--- a/.github/workflows/pr-extensions.yml
+++ b/.github/workflows/pr-extensions.yml
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: tests/release-extensions

 on:
@@ -18,7 +20,7 @@ jobs:
    runs-on: ubuntu-latest

    steps:
-    - uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+    - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
    - name: Setup Rust toolchain
      uses: ./.github/actions/toolchains/rust
    - name: Cache cargo
--- a/.github/workflows/pr.yml
+++ b/.github/workflows/pr.yml
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: tests/release

 on:
@@ -18,7 +20,7 @@ jobs:
    runs-on: ubuntu-latest

    steps:
-    - uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+    - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
    - name: Setup Rust toolchain
      uses: ./.github/actions/toolchains/rust
    - name: Cache cargo
--- a/.github/workflows/publish-java.yml
+++ b/.github/workflows/publish-java.yml
@@ -1,6 +1,9 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: publish-java

-on: workflow_dispatch
+on:
+  workflow_dispatch:

 permissions:
  contents: read
@@ -32,10 +35,10 @@ jobs:
            os: windows-latest
            extension: dll
    steps:
-      - uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0
-      - uses: actions/setup-java@dded0888837ed1f317902acf8a20df0ad188d165 # v5.0.0
+      - uses: actions/setup-java@be666c2fcd27ec809703dec50e508c2fdc7f6654 # v5.2.0
        with:
          java-version: 8
          distribution: "corretto"
@@ -43,7 +46,7 @@ jobs:
        with:
          targets: ${{ matrix.target }}
      - if: ${{ matrix.build_cmd == 'zigbuild' }}
-        uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
+        uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
        with:
          python-version: "3.11"
      - if: ${{ matrix.build_cmd == 'zigbuild' }}
@@ -53,7 +56,7 @@ jobs:
      - run: cargo ${{ matrix.build_cmd || 'build' }} --release --frozen --target ${{ matrix.target }}${{ matrix.glibc && format('.{0}', matrix.glibc) || '' }} --manifest-path ./bindings/java/Cargo.toml
      - run: mkdir -p native/${{ matrix.target }}
      - run: mv target/${{ matrix.target }}/release/*.${{ matrix.extension }} ./native/${{ matrix.target }}/
-      - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+      - uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
        with:
          name: native-libraries-${{ matrix.target }}
          path: native/
@@ -63,24 +66,24 @@ jobs:
    runs-on: ubuntu-latest
    needs: build
    steps:
-      - uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0
-      - uses: actions/setup-java@dded0888837ed1f317902acf8a20df0ad188d165 # v5.0.0
+      - uses: actions/setup-java@be666c2fcd27ec809703dec50e508c2fdc7f6654 # v5.2.0
        with:
          java-version: 8
          distribution: "corretto"
          server-id: ossrh
          server-username: MAVEN_USERNAME
          server-password: MAVEN_PASSWORD
-      - uses: actions/download-artifact@634f93cb2916e3fdff6788551b99b062d0335ce0 # v5.0.0
+      - uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 # v7.0.0
        with:
          pattern: native-libraries-*
          merge-multiple: true
          path: ./bindings/java/native/
      - run: mvn package
        working-directory: ./bindings/java
-      - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+      - uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
        with:
          name: built-jars
          path: ./bindings/java/target/regorus-java-*.jar
--- a/.github/workflows/publish-python.yml
+++ b/.github/workflows/publish-python.yml
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 # This file is autogenerated by maturin v1.4.0
 # To update, run
 #
@@ -18,8 +20,8 @@ jobs:
      matrix:
        target: [x86_64, x86, aarch64, armv7, s390x, ppc64le]
    steps:
-      - uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
-      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
        with:
          python-version: '3.10'
      - uses: ./.github/actions/toolchains/rust
@@ -32,14 +34,14 @@ jobs:
        working-directory: bindings/python

      - name: Build wheels
-        uses: PyO3/maturin-action@63b75c597b83e247fbf4fb7719801cc4220ae9f3 # v1.43.0
+        uses: PyO3/maturin-action@b1bd829e37fef14c63f19162034228a2f3dc1021 # v1.43.0
        with:
          target: ${{ matrix.target }}
          args: --release --out dist --manifest-path bindings/python/Cargo.toml --offline --strip
          sccache: 'true'
          manylinux: auto
      - name: Upload wheels
-        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
        with:
          name: wheels-linux-${{ matrix.target }}
          path: dist
@@ -50,8 +52,8 @@ jobs:
      matrix:
        target: [x64, x86]
    steps:
-      - uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
-      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
        with:
          python-version: '3.10'
          architecture: ${{ matrix.target }}
@@ -65,13 +67,13 @@ jobs:
        working-directory: bindings/python

      - name: Build wheels
-        uses: PyO3/maturin-action@63b75c597b83e247fbf4fb7719801cc4220ae9f3 # v1.43.0
+        uses: PyO3/maturin-action@b1bd829e37fef14c63f19162034228a2f3dc1021 # v1.43.0
        with:
          target: ${{ matrix.target }}
          args: --release --out dist --manifest-path bindings/python/Cargo.toml --frozen --strip
          sccache: 'true'
      - name: Upload wheels
-        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
        with:
          name: wheels-windows-${{ matrix.target }}
          path: dist
@@ -82,8 +84,8 @@ jobs:
      matrix:
        target: [x86_64, aarch64, universal2-apple-darwin]
    steps:
-      - uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
-      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
        with:
          python-version: '3.10'
      - uses: ./.github/actions/toolchains/rust
@@ -96,13 +98,13 @@ jobs:
        working-directory: bindings/python

      - name: Build wheels
-        uses: PyO3/maturin-action@63b75c597b83e247fbf4fb7719801cc4220ae9f3 # v1.43.0
+        uses: PyO3/maturin-action@b1bd829e37fef14c63f19162034228a2f3dc1021 # v1.43.0
        with:
          target: ${{ matrix.target }}
          args: --release --out dist --manifest-path bindings/python/Cargo.toml --offline --strip
          sccache: 'true'
      - name: Upload wheels
-        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
        with:
          name: wheels-macos-${{ matrix.host.target }}
          path: dist
@@ -114,13 +116,13 @@ jobs:
    # if: "startsWith(github.ref, 'refs/tags/')"
    needs: [linux, windows, macos]
    steps:
-      - uses: actions/download-artifact@634f93cb2916e3fdff6788551b99b062d0335ce0 # v5.0.0
+      - uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 # v7.0.0
        with:
          pattern: wheels-*
          merge-multiple: true
          path: wheels
      - name: Publish to PyPI
-        uses: PyO3/maturin-action@63b75c597b83e247fbf4fb7719801cc4220ae9f3 # v1.43.0
+        uses: PyO3/maturin-action@b1bd829e37fef14c63f19162034228a2f3dc1021 # v1.43.0
        env:
          MATURIN_PYPI_TOKEN: ${{ secrets.PYPI_API_TOKEN }}
        with:
--- a/.github/workflows/publish-wasm.yml
+++ b/.github/workflows/publish-wasm.yml
@@ -1,10 +1,13 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: publish-wasm

 permissions:
  pull-requests: write
  contents: write

-on: workflow_dispatch
+on:
+  workflow_dispatch:

 jobs:
  publish-wasm:
@@ -12,11 +15,11 @@ jobs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
-        uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0
      # Setup .npmrc file to publish to npm
-      - uses: actions/setup-node@49933ea5288caeca8642d1e84afbd3f7d6820020 # v4.4.0
+      - uses: actions/setup-node@6044e13b5dc448c55e2357c09f80417699197238 # v6.2.0
        with:
          node-version: '20.x'
          registry-url: 'https://registry.npmjs.org'
--- a/.github/workflows/release-plz.yml
+++ b/.github/workflows/release-plz.yml
@@ -1,10 +1,13 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: Release-plz

 permissions:
  pull-requests: write
  contents: write

-on: workflow_dispatch
+on:
+  workflow_dispatch:

 jobs:
  release-plz:
@@ -14,13 +17,13 @@ jobs:
      contents: write
    steps:
      - name: Checkout repository
-        uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0
      - name: Install Rust toolchain
        uses: ./.github/actions/toolchains/rust
      - name: Run release-plz
-        uses: MarcoIeni/release-plz-action@8724d33cd97b8295051102e2e19ca592962238f5 #v0.5.108
+        uses: MarcoIeni/release-plz-action@52440b50d383aa252927de395c8b2c1e0a9cf8e9 # v0.5.126
        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
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 # This workflow uses actions that are not certified by GitHub.
 # They are provided by a third-party and are governed by
 # separate terms of service, privacy policy, and support
@@ -30,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@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

      - name: Setup Rust toolchain
        uses: ./.github/actions/toolchains/rust
@@ -50,7 +52,7 @@ jobs:
        continue-on-error: true

      - name: Upload analysis results to GitHub
-        uses: github/codeql-action/upload-sarif@c298edae2d512d807fe4bdc57c0ac5a036f61501 # v3.29.11
+        uses: github/codeql-action/upload-sarif@45cbd0c69e560cd9e7cd7f8c32362050c9b7ded2 # 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
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: bindings/c-cpp

 on:
@@ -14,7 +16,7 @@ jobs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
-        uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0

--- a/.github/workflows/test-csharp.yml
+++ b/.github/workflows/test-csharp.yml
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: bindings/csharp

 on:
@@ -37,7 +39,7 @@ jobs:
              **/release/libregorus_ffi.dylib
    steps:
      - name: Checkout repository
-        uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0
      - uses: ./.github/actions/toolchains/rust
@@ -57,7 +59,7 @@ jobs:
        run: cargo xtask build-ffi --release --target ${{ matrix.runtime.target }}
        
      - name: Upload regorus ffi shared library
-        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
        with:
          name: regorus-ffi-artifacts-${{ matrix.runtime.target }}
          # Note: The full path of each artifact relative to . is preserved.
@@ -71,11 +73,11 @@ jobs:
    needs: build-ffi
    steps:
      - name: Checkout repository
-        uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0  
      - uses: ./.github/actions/toolchains/rust
-      - uses: actions/setup-dotnet@3e891b0cb619bf60e2c25674b222b8940e2c1c25 # v4.1.0
+      - uses: actions/setup-dotnet@baa11fbfe1d6520db94683bd5c7a3818018e4309 # v5.1.0
        with:
          global-json-file: ./bindings/csharp/global.json

@@ -90,7 +92,7 @@ jobs:
        run: cargo fetch --locked

      - name: Download regorus ffi shared libraries
-        uses: actions/download-artifact@634f93cb2916e3fdff6788551b99b062d0335ce0 # v5.0.0
+        uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 # v7.0.0
        with:
          pattern: regorus-ffi-artifacts-*
          merge-multiple: true
@@ -103,7 +105,7 @@ jobs:
        run: cargo xtask build-csharp --release --clean --artifacts-dir ./bindings/csharp/Regorus/tmp/bindings/ffi/target --enforce-artifacts --repository-commit ${{ github.sha }} --include-symbols

      - name: Upload Regorus nuget
-        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
        with:
          name: regorus-nuget
          path: |
@@ -129,13 +131,13 @@ jobs:
            target: aarch64-apple-darwin
    steps:
      - name: Checkout repository
-        uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0

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

-      - uses: actions/setup-dotnet@3e891b0cb619bf60e2c25674b222b8940e2c1c25 # v4.1.0
+      - uses: actions/setup-dotnet@baa11fbfe1d6520db94683bd5c7a3818018e4309 # v5.1.0
        with:
          global-json-file: ./bindings/csharp/global.json

@@ -150,7 +152,7 @@ jobs:
        run: cargo fetch --locked

      - name: Download regorus nuget
-        uses: actions/download-artifact@634f93cb2916e3fdff6788551b99b062d0335ce0 # v5.0.0
+        uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 # v7.0.0
        with:
          name: regorus-nuget
          path: ./bindings/csharp/Regorus/bin/Release
--- a/.github/workflows/test-ffi.yml
+++ b/.github/workflows/test-ffi.yml
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: bindings/ffi

 on:
@@ -14,7 +16,7 @@ jobs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
-        uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0
      - uses: ./.github/actions/toolchains/rust
--- a/.github/workflows/test-go.yml
+++ b/.github/workflows/test-go.yml
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: bindings/go

 on:
@@ -14,7 +16,7 @@ jobs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
-        uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0
      - uses: ./.github/actions/toolchains/rust
@@ -28,7 +30,7 @@ jobs:
      - name: Fetch FFI crate dependencies
        run: cargo fetch --locked --manifest-path bindings/ffi/Cargo.toml

-      - uses: actions/setup-go@41dfa10bad2bb2ae585af6ee5bb4d7d973ad74ed # v5.1.0
+      - uses: actions/setup-go@7a3fe6cf4cb3a834922a1244abfce67bcef6a0c5 # v6.2.0
        with:
          architecture: x64

--- a/.github/workflows/test-java.yml
+++ b/.github/workflows/test-java.yml
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: bindings/java

 on:
@@ -14,11 +16,11 @@ jobs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
-        uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0

-      - uses: actions/setup-java@dded0888837ed1f317902acf8a20df0ad188d165 # v5.0.0
+      - uses: actions/setup-java@be666c2fcd27ec809703dec50e508c2fdc7f6654 # v5.2.0
        with:
          java-version: 8
          distribution: "corretto"
--- a/.github/workflows/test-musl.yml
+++ b/.github/workflows/test-musl.yml
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: musl

 on:
@@ -18,7 +20,7 @@ jobs:
    runs-on: ubuntu-latest

    steps:
-    - uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+    - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
    - 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
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: bindings/no-std

 on:
@@ -18,7 +20,7 @@ jobs:
    runs-on: ubuntu-latest

    steps:
-    - uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+    - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
    - uses: ./.github/actions/toolchains/rust
      with:
        targets: thumbv7m-none-eabi
--- a/.github/workflows/test-python.yml
+++ b/.github/workflows/test-python.yml
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: bindings/python

 on:
@@ -21,7 +23,7 @@ jobs:
    runs-on: ${{ matrix.host.name }}
    steps:
      - name: Checkout repository
-        uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0
      - uses: ./.github/actions/toolchains/rust
@@ -37,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@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
+      - uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
        with:
          python-version: "3.10"
          architecture: x64
@@ -49,7 +51,7 @@ jobs:
        run: cargo xtask build-python --release --target ${{ matrix.host.target }} --target-dir bindings/python/dist --frozen

      - name: Upload wheel artefacts
-        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
        with:
          name: regorus-wheel-${{ matrix.host.name }}
          path: bindings/python/dist/regorus-*.whl
@@ -63,7 +65,7 @@ jobs:
    runs-on: ${{ matrix.host }}
    steps:
      - name: Checkout repository
-        uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0
      - uses: ./.github/actions/toolchains/rust
@@ -77,7 +79,7 @@ jobs:
      - name: Fetch Python crate dependencies
        run: cargo fetch --locked --manifest-path bindings/python/Cargo.toml

-      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
+      - uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
        with:
          python-version: ${{ matrix.python-version }}
          architecture: x64
--- a/.github/workflows/test-ruby.yml
+++ b/.github/workflows/test-ruby.yml
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: bindings/ruby

 on:
@@ -12,12 +14,12 @@ jobs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
-        uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0

      - name: Setup Ruby and Rust
-        uses: oxidize-rb/actions/setup-ruby-and-rust@7ca44a16e287e5ff7dd72ab53f4bd41cbf34a571 #v1.26
+        uses: oxidize-rb/actions/setup-ruby-and-rust@e5f9a49a7812a078584072f6e3f657ad247c8771 # v1.26
        with:
          bundler: 2.6.5
          rubygems: 3.6.5
--- a/.github/workflows/test-wasm.yml
+++ b/.github/workflows/test-wasm.yml
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: bindings/wasm

 on:
@@ -14,7 +16,7 @@ jobs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
-        uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          fetch-depth: 0

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

      - name: Setup Node
-        uses: actions/setup-node@49933ea5288caeca8642d1e84afbd3f7d6820020 # v4.4.0
+        uses: actions/setup-node@6044e13b5dc448c55e2357c09f80417699197238 # v6.2.0
        with:
          node-version: 22

--- a/.github/workflows/tests-debug.yml
+++ b/.github/workflows/tests-debug.yml
@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: tests/debug

 on:
@@ -18,7 +20,7 @@ jobs:
    runs-on: ubuntu-latest

    steps:
-    - uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955 # v4
+    - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
    - name: Setup Rust toolchain
      uses: ./.github/actions/toolchains/rust
    - name: Cache cargo
--- a/.gitignore
+++ b/.gitignore
@@ -48,3 +48,6 @@ bindings/ruby/bin/
 bindings/java/.classpath
 bindings/java/.project
 bindings/java/.settings/
+
+# Emacs temporary files
+*~
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -545,6 +545,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"
@@ -695,6 +701,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.13.0"
@@ -1239,7 +1255,7 @@ dependencies = [
 "dashmap",
 "data-encoding",
 "globset",
- "indexmap",
+ "indexmap 2.13.0",
 "ipnet",
 "jsonschema",
 "lazy_static",
@@ -1260,6 +1276,7 @@ dependencies = [
 "thiserror",
 "url",
 "uuid",
+ "vstd",
 "walkdir",
 ]

@@ -1359,7 +1376,7 @@ version = "0.9.34+deprecated"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
 dependencies = [
- "indexmap",
+ "indexmap 2.13.0",
 "itoa",
 "ryu",
 "serde",
@@ -1505,7 +1522,7 @@ version = "0.22.27"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "41fe8c660ae4257887cf66394862d21dbca4a6ddd26f04a3560410406a2f819a"
 dependencies = [
- "indexmap",
+ "indexmap 2.13.0",
 "toml_datetime",
 "toml_write",
 "winnow",
@@ -1594,12 +1611,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-03-17-2326"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d7ab914ab490975465ecb3286edceecb0743c3628ddeefcdf25158683e83e2fe"
+
+[[package]]
+name = "verus_builtin_macros"
+version = "0.0.0-2026-03-17-2326"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "46f1f1ee124e0bcb5cec79836ff015d138ea53bff51839a85b8364cdc8b79232"
+dependencies = [
+ "proc-macro2 1.0.106",
+ "quote 1.0.44",
+ "syn 2.0.114",
+ "synstructure",
+ "verus_prettyplease",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_prettyplease"
+version = "0.0.0-2026-03-15-0111"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "eadebc1e3b522b32c178fd2fb882e691880ff983415497232c74aa9b72bc0b65"
+dependencies = [
+ "proc-macro2 1.0.106",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_state_machines_macros"
+version = "0.0.0-2026-03-15-0111"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b824c6405f8e8a063ca4a26fca1f454cb02de0c1c4da685e3e7f1974899129d5"
+dependencies = [
+ "indexmap 1.9.3",
+ "proc-macro2 1.0.106",
+ "quote 1.0.44",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_syn"
+version = "0.0.0-2026-03-15-0111"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1694faf01f89e1abc996da7b8d24a4e0d1ebd70147dc659e7a5dd680af696772"
+dependencies = [
+ "proc-macro2 1.0.106",
+ "quote 1.0.44",
+ "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-03-17-2326"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "13bbf59dfaa6a7bcb327412c778a5d2b2c226dc65473a981ae6ec53a04c75aba"
+dependencies = [
+ "verus_builtin",
+ "verus_builtin_macros",
+ "verus_state_machines_macros",
+]
+
 [[package]]
 name = "walkdir"
 version = "2.5.0"
--- 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"]

+# Enable verification with Verus
+
+[package.metadata.verus]
+verify = true
+
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

 [lib]
@@ -130,6 +135,9 @@ mimalloc = { package = "regorus-mimalloc", path = "mimalloc", version = "2.2.6",
 indexmap = { version = "2.12.1", default-features = false, features = ["serde"], optional = true }
 bincode = { version = "2.0.1", default-features = false, features = ["alloc", "serde"], optional = true }

+# Use Verus for verification
+vstd = { version = "0.0.0-2026-03-17-2326" }
+
 [dev-dependencies]
 anyhow = "1.0.45"
 cfg-if = "1.0.0"
@@ -200,3 +208,6 @@ doctest=false
 # RUSTDOCFLAGS="--cfg docsrs" cargo +nightly doc --all-features --no-deps
 all-features = true
 rustdoc-args = ["--cfg", "docsrs"]
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(verus_keep_ghost)'] }
--- a/bindings/csharp/global.json
+++ b/bindings/csharp/global.json
@@ -1,10 +1,10 @@
 {
-    "msbuild-sdks": {
-      "Microsoft.Build.NoTargets": "3.7.56"
-    },
-    "sdk": {
-      "allowPrerelease": false,
-      "version": "8.0.412",
-      "rollForward": "latestFeature"
-    }
+  "msbuild-sdks": {
+    "Microsoft.Build.NoTargets": "3.7.134"
+  },
+  "sdk": {
+    "allowPrerelease": false,
+    "version": "8.0.412",
+    "rollForward": "latestFeature"
+  }
 }
--- a/bindings/java/pom.xml
+++ b/bindings/java/pom.xml
@@ -48,13 +48,13 @@
    <dependency>
      <groupId>junit</groupId>
      <artifactId>junit</artifactId>
-      <version>3.8.1</version>
+      <version>4.13.2</version>
      <scope>test</scope>
    </dependency>
    <dependency>
      <groupId>com.google.code.gson</groupId>
      <artifactId>gson</artifactId>
-      <version>2.10.1</version>
+      <version>2.13.2</version>
      <scope>test</scope>
    </dependency>
  </dependencies>
@@ -76,7 +76,7 @@
      <plugin>
        <artifactId>exec-maven-plugin</artifactId>
        <groupId>org.codehaus.mojo</groupId>
-        <version>3.1.0</version>
+        <version>3.6.3</version>
        <executions>
          <execution>
            <!-- Build a debug release for tests -->
@@ -97,7 +97,7 @@

      <plugin>
        <artifactId>maven-surefire-plugin</artifactId>
-        <version>3.2.5</version>
+        <version>3.5.4</version>
        <configuration>
          <!-- Add debug build to Java path, so it's discoverable by JVM. This is only for tests. -->
          <argLine>-Djava.library.path=${project.basedir}/target/debug:${java.library.path}</argLine>
@@ -108,7 +108,7 @@
      <plugin>
        <groupId>org.apache.maven.plugins</groupId>
        <artifactId>maven-javadoc-plugin</artifactId>
-        <version>3.6.3</version>
+        <version>3.12.0</version>
        <executions>
          <execution>
            <id>attach-javadoc</id>
@@ -123,7 +123,7 @@
      <plugin>
        <groupId>org.apache.maven.plugins</groupId>
        <artifactId>maven-source-plugin</artifactId>
-        <version>3.3.0</version>
+        <version>3.4.0</version>
        <executions>
          <execution>
            <id>attach-sources</id>
--- a/bindings/ruby/Cargo.lock
+++ b/bindings/ruby/Cargo.lock
@@ -551,9 +551,9 @@ checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897"

 [[package]]
 name = "magnus"
-version = "0.7.1"
+version = "0.8.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3d87ae53030f3a22e83879e666cb94e58a7bdf31706878a0ba48752994146dab"
+checksum = "3b36a5b126bbe97eb0d02d07acfeb327036c6319fd816139a49824a83b7f9012"
 dependencies = [
 "magnus-macros",
 "rb-sys",
@@ -563,9 +563,9 @@ dependencies = [

 [[package]]
 name = "magnus-macros"
-version = "0.6.0"
+version = "0.8.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5968c820e2960565f647819f5928a42d6e874551cab9d88d75e3e0660d7f71e3"
+checksum = "47607461fd8e1513cb4f2076c197d8092d921a1ea75bd08af97398f593751892"
 dependencies = [
 "proc-macro2",
 "quote",
@@ -578,20 +578,6 @@ version = "2.7.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f52b00d39961fc5b2736ea853c9cc86238e165017a493d1d5c8eac6bdc4cc273"

-[[package]]
-name = "mimalloc"
-version = "2.2.6"
-dependencies = [
- "mimalloc-sys",
-]
-
-[[package]]
-name = "mimalloc-sys"
-version = "0.0.0"
-dependencies = [
- "cc",
-]
-
 [[package]]
 name = "minimal-lexical"
 version = "0.2.1"
@@ -852,9 +838,9 @@ dependencies = [

 [[package]]
 name = "rb-sys-env"
-version = "0.1.2"
+version = "0.2.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a35802679f07360454b418a5d1735c89716bde01d35b1560fc953c1415a0b3bb"
+checksum = "cca7ad6a7e21e72151d56fe2495a259b5670e204c3adac41ee7ef676ea08117a"

 [[package]]
 name = "redox_syscall"
@@ -930,7 +916,7 @@ checksum = "7a2d987857b319362043e95f5353c0535c1f58eec5336fdfcf626430af7def58"

 [[package]]
 name = "regorus"
-version = "0.5.0"
+version = "0.9.1"
 dependencies = [
 "anyhow",
 "chrono",
@@ -940,24 +926,39 @@ dependencies = [
 "ipnet",
 "jsonschema",
 "lazy_static",
- "mimalloc",
 "msvc_spectre_libs",
 "num-bigint",
 "num-traits",
 "rand",
 "regex",
+ "regorus-mimalloc",
 "semver",
 "serde",
 "serde_json",
 "serde_yaml",
+ "spin",
 "thiserror",
 "url",
 "uuid",
 ]

+[[package]]
+name = "regorus-mimalloc"
+version = "2.2.6"
+dependencies = [
+ "regorus-mimalloc-sys",
+]
+
+[[package]]
+name = "regorus-mimalloc-sys"
+version = "2.2.6"
+dependencies = [
+ "cc",
+]
+
 [[package]]
 name = "regorusrb"
-version = "0.6.0"
+version = "0.9.1"
 dependencies = [
 "magnus",
 "regorus",
@@ -1046,9 +1047,9 @@ dependencies = [

 [[package]]
 name = "serde_magnus"
-version = "0.9.0"
+version = "0.11.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "51b8b945a2dadb221f1c5490cfb411cab6c3821446b8eca50ee07e5a3893ec51"
+checksum = "8ff64c88ddd26acdcad5a501f18bcc339927b77b69f4a03bfaf2a6fc5ba2ac4b"
 dependencies = [
 "magnus",
 "serde",
@@ -1092,6 +1093,12 @@ version = "1.15.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03"

+[[package]]
+name = "spin"
+version = "0.9.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6980e8d7511241f8acf4aebddbb1ff938df5eebe98691418c4468d0b72a96a67"
+
 [[package]]
 name = "stable_deref_trait"
 version = "1.2.1"
--- a/bindings/ruby/Gemfile
+++ b/bindings/ruby/Gemfile
@@ -7,10 +7,10 @@ gemspec

 # These gems are required for local development and testing,
 # but won't be included in the published gem
-gem "minitest", "~> 5.25"
-gem "rake", "~> 13.2"
-gem "rake-compiler", "~> 1.2"
-gem "rake-compiler-dock", "~> 1.9"
-gem "rubocop", "~> 1.73", require: false
-gem "rubocop-minitest", "~> 0.37.1", require: false
+gem "minitest", "~> 6.0"
+gem "rake", "~> 13.3"
+gem "rake-compiler", "~> 1.3"
+gem "rake-compiler-dock", "~> 1.11"
+gem "rubocop", "~> 1.84", require: false
+gem "rubocop-minitest", "~> 0.38.2", require: false
 gem "rubocop-rake", "~> 0.7.1", require: false
--- a/bindings/ruby/Gemfile.lock
+++ b/bindings/ruby/Gemfile.lock
@@ -7,25 +7,27 @@ PATH
 GEM
  remote: https://rubygems.org/
  specs:
-    ast (2.4.2)
-    json (2.10.2)
-    language_server-protocol (3.17.0.4)
+    ast (2.4.3)
+    json (2.18.1)
+    language_server-protocol (3.17.0.5)
    lint_roller (1.1.0)
-    minitest (5.25.4)
-    parallel (1.26.3)
-    parser (3.3.7.1)
+    minitest (6.0.1)
+      prism (~> 1.5)
+    parallel (1.27.0)
+    parser (3.3.10.1)
      ast (~> 2.4.1)
      racc
+    prism (1.9.0)
    racc (1.8.1)
    rainbow (3.1.1)
-    rake (13.2.1)
-    rake-compiler (1.2.9)
+    rake (13.3.1)
+    rake-compiler (1.3.1)
      rake
-    rake-compiler-dock (1.9.1)
-    rb_sys (0.9.111)
-      rake-compiler-dock (= 1.9.1)
-    regexp_parser (2.10.0)
-    rubocop (1.73.2)
+    rake-compiler-dock (1.11.0)
+    rb_sys (0.9.124)
+      rake-compiler-dock (= 1.11.0)
+    regexp_parser (2.11.3)
+    rubocop (1.84.1)
      json (~> 2.3)
      language_server-protocol (~> 3.17.0.2)
      lint_roller (~> 1.1.0)
@@ -33,35 +35,36 @@ GEM
      parser (>= 3.3.0.2)
      rainbow (>= 2.2.2, < 4.0)
      regexp_parser (>= 2.9.3, < 3.0)
-      rubocop-ast (>= 1.38.0, < 2.0)
+      rubocop-ast (>= 1.49.0, < 2.0)
      ruby-progressbar (~> 1.7)
      unicode-display_width (>= 2.4.0, < 4.0)
-    rubocop-ast (1.38.1)
-      parser (>= 3.3.1.0)
-    rubocop-minitest (0.37.1)
+    rubocop-ast (1.49.0)
+      parser (>= 3.3.7.2)
+      prism (~> 1.7)
+    rubocop-minitest (0.38.2)
      lint_roller (~> 1.1)
-      rubocop (>= 1.72.1, < 2.0)
+      rubocop (>= 1.75.0, < 2.0)
      rubocop-ast (>= 1.38.0, < 2.0)
    rubocop-rake (0.7.1)
      lint_roller (~> 1.1)
      rubocop (>= 1.72.1)
    ruby-progressbar (1.13.0)
-    unicode-display_width (3.1.4)
-      unicode-emoji (~> 4.0, >= 4.0.4)
-    unicode-emoji (4.0.4)
+    unicode-display_width (3.2.0)
+      unicode-emoji (~> 4.1)
+    unicode-emoji (4.2.0)

 PLATFORMS
  ruby
  x86_64-linux

 DEPENDENCIES
-  minitest (~> 5.25)
-  rake (~> 13.2)
-  rake-compiler (~> 1.2)
-  rake-compiler-dock (~> 1.9)
+  minitest (~> 6.0)
+  rake (~> 13.3)
+  rake-compiler (~> 1.3)
+  rake-compiler-dock (~> 1.11)
  regorusrb!
-  rubocop (~> 1.73)
-  rubocop-minitest (~> 0.37.1)
+  rubocop (~> 1.84)
+  rubocop-minitest (~> 0.38.2)
  rubocop-rake (~> 0.7.1)

 BUNDLED WITH
--- a/bindings/ruby/ext/regorusrb/Cargo.toml
+++ b/bindings/ruby/ext/regorusrb/Cargo.toml
@@ -16,7 +16,7 @@ ast = ["regorus/ast"]
 coverage = ["regorus/coverage"]

 [dependencies]
-magnus = { version = "0.7.1" }
+magnus = { version = "0.8.2" }
 regorus = { path = "../../../..", default-features = false, features = ["arc"] }
 serde_json = "1.0.140"
-serde_magnus = "0.9.0"
+serde_magnus = "0.11.0"
--- a/src/builtins/numbers.rs
+++ b/src/builtins/numbers.rs
@@ -21,6 +21,8 @@ use anyhow::{bail, Result};
 #[cfg(feature = "std")]
 use rand::Rng;

+use vstd::prelude::*;
+
 pub fn register(m: &mut builtins::BuiltinsMap<&'static str, builtins::BuiltinFcn>) {
    m.insert("abs", (abs, 1));
    m.insert("ceil", (ceil, 1));
@@ -188,3 +190,13 @@ fn intn(span: &Span, params: &[Ref<Expr>], args: &[Value], _strict: bool) -> Res
        _ => Value::Undefined,
    })
 }
+
+// Prove properties with Verus
+
+verus! {
+    proof fn lemma_test_one_plus_one_equals_two()
+        ensures
+            1 + 1 == 2,
+    {
+    }
+}
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -3,7 +3,9 @@

 // Unsafe code should not be used.
 // Hard to reason about correctness, and maintainability.
-#![forbid(unsafe_code)]
+#![cfg_attr(not(verus_keep_ghost), forbid(unsafe_code))]
+#![cfg_attr(verus_keep_ghost, feature(proc_macro_hygiene))]
+#![cfg_attr(verus_keep_ghost, feature(stmt_expr_attributes))]
 // Ensure that all lint names are valid.
 #![deny(unknown_lints)]
 // Fail-fast lints: correctness, safety, and API surface
@@ -125,6 +127,7 @@ mod compiler;
 mod engine;
 mod indexchecker;
 mod interpreter;
+mod verusspec;

 pub mod languages {
    #[cfg(feature = "azure-rbac")]
--- a/src/number.rs
+++ b/src/number.rs
@@ -27,12 +27,29 @@ use num_traits::{One, Signed, ToPrimitive, Zero};
 use serde::ser::Serializer;
 use serde::Serialize;

+#[cfg(verus_keep_ghost)]
+use vstd::float::*;
+use vstd::prelude::*;
+#[cfg(verus_keep_ghost)]
+use vstd::std_specs::cmp::*;
+#[cfg(verus_keep_ghost)]
+use vstd::std_specs::convert::*;
+
 use crate::*;

+#[cfg(verus_keep_ghost)]
+use crate::verusspec::bigint::*;
+use crate::verusspec::float::*;
+
+#[verus_verify]
 pub type BigInt = NumBigInt;

+verus! { // TODO: Change to #[verus_verify] after PR #2243
 const F64_SAFE_INTEGER: f64 = 9_007_199_254_740_992.0; // 2^53
+}

+#[verus_verify]
+#[verus_verify(external_derive)]
 #[derive(Clone)]
 pub enum Number {
    UInt(u64),
@@ -41,7 +58,210 @@ pub enum Number {
    BigInt(Rc<BigInt>),
 }

+#[cfg(verus_keep_ghost)]
+verus! {
+
+pub assume_specification[ <Number as Clone>::clone ](n: &Number) -> (res: Number)
+    ensures
+        res == n,
+;
+
+pub enum NumberView {
+    Integer(int),
+    Float(f64),
+}
+
+impl View for Number
+{
+    type V = NumberView;
+
+    open spec fn view(&self) -> NumberView
+    {
+        match self {
+            Number::UInt(n) => NumberView::Integer(n as int),
+            Number::Int(n) => NumberView::Integer(n as int),
+            Number::Float(f) => NumberView::Float(*f),
+            Number::BigInt(b) => NumberView::Integer(b@),
+        }
+    }
+}
+
+pub open spec fn float_to_small_int(value: f64) -> Option<int>
+{
+    if !value.is_finite_spec() ||
+       !spec_f64_fract(value).eq_spec(&0.0f64) ||
+       spec_f64_abs(value) > 9_007_199_254_740_992.0 {
+        None
+    }
+    else if value >= 0.0 {
+        if ieee_float_cast::<u64, f64>(ieee_float_cast::<f64, u64>(value)).eq_spec(&value) {
+            Some(ieee_float_cast::<f64, u64>(value) as int)
+        }
+        else {
+            None
+        }
+    }
+    else {
+        if ieee_float_cast::<i64, f64>(ieee_float_cast::<f64, i64>(value)).eq_spec(&value) {
+            Some(ieee_float_cast::<f64, i64>(value) as int)
+        }
+        else {
+            None
+        }
+    }
+}
+
+impl NumberView {
+    pub open spec fn to_int(&self) -> Option<int>
+    {
+        match *self {
+            Self::Integer(n) => Some(n),
+            Self::Float(f) => float_to_small_int(f),
+        }
+    }
+
+    pub open spec fn to_f64_lossy_ensures(self: Self, f: f64) -> bool
+    {
+        match self {
+            NumberView::Integer(v) =>
+            {
+                ||| 0 <= v <= u64::MAX && f == ieee_float_cast::<u64, f64>(v as u64)
+                ||| i64::MIN <= v <= i64::MAX && f == ieee_float_cast::<i64, f64>(v as i64)
+                ||| exists|bi: BigInt| {
+                    &&& bi@ == v
+                    &&& match #[trigger] verusspec::bigint::ToPrimitiveSpec::spec_to_f64(&bi) {
+                        Some(x) => f == x,
+                        None => f == if v < 0 { spec_f64_neg_infinity() } else { spec_f64_infinity() }
+                    }
+                }
+            },
+            NumberView::Float(v) => f == v,
+        }
+    }
+}
+
+impl FromSpecImpl<BigInt> for Number {
+    open spec fn obeys_from_spec() -> bool
+    {
+        false
+    }
+
+    uninterp spec fn from_spec(v: BigInt) -> Number;
+}
+
+impl FromSpecImpl<u64> for Number {
+    open spec fn obeys_from_spec() -> bool
+    {
+        false
+    }
+
+    uninterp spec fn from_spec(v: u64) -> Number;
+}
+
+impl FromSpecImpl<usize> for Number {
+    open spec fn obeys_from_spec() -> bool
+    {
+        false
+    }
+
+    uninterp spec fn from_spec(v: usize) -> Number;
+}
+
+impl FromSpecImpl<u128> for Number {
+    open spec fn obeys_from_spec() -> bool
+    {
+        false
+    }
+
+    uninterp spec fn from_spec(v: u128) -> Number;
+}
+
+impl FromSpecImpl<i64> for Number {
+    open spec fn obeys_from_spec() -> bool
+    {
+        false
+    }
+
+    uninterp spec fn from_spec(v: i64) -> Number;
+}
+
+impl FromSpecImpl<i128> for Number {
+    open spec fn obeys_from_spec() -> bool
+    {
+        false
+    }
+
+    uninterp spec fn from_spec(v: i128) -> Number;
+}
+
+impl FromSpecImpl<f64> for Number {
+    open spec fn obeys_from_spec() -> bool
+    {
+        false
+    }
+
+    uninterp spec fn from_spec(v: f64) -> Number;
+}
+
+impl PartialEqSpecImpl for Number {
+    open spec fn obeys_eq_spec() -> bool
+    {
+        false
+    }
+
+    open spec fn eq_spec(&self, other: &Self) -> bool
+    {
+        *self == *other
+    }
+}
+
 impl Number {
+    spec fn spec_to_f64_lossy(&self) -> f64
+    {
+        match *self {
+            Number::UInt(v) => ieee_float_cast::<u64, f64>(v),
+            Number::Int(v) => ieee_float_cast::<i64, f64>(v),
+            Number::Float(v) => v,
+            Number::BigInt(v) => {
+                if let Some(f) = <BigInt as ToPrimitiveSpec>::spec_to_f64(&v) {
+                    f
+                } else if v@ < 0 {
+                    spec_f64_neg_infinity()
+                } else {
+                    spec_f64_infinity()
+                }
+            },
+        }
+    }
+}
+
+impl OrdSpecImpl for Number {
+    open spec fn obeys_cmp_spec() -> bool
+    {
+        true
+    }
+
+    closed spec fn cmp_spec(&self, other: &Self) -> Ordering
+    {
+         match (self@.to_int(), other@.to_int()) {
+             (Some(n1), Some(n2)) => n1.cmp_spec(&n2),
+             _ => {
+                 let f1 = self.spec_to_f64_lossy();
+                 let f2 = self.spec_to_f64_lossy();
+                 f1.partial_cmp_spec(&f2).unwrap_or(Ordering::Equal)
+            },
+        }
+    }
+}
+
+} // end verus!
+
+#[verus_verify]
+impl Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value@),
+    )]
    fn from_bigint_owned(value: BigInt) -> Self {
        if value.is_zero() {
            return Number::Int(0);
@@ -60,6 +280,10 @@ impl Number {
        Number::BigInt(Rc::new(value))
    }

+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value as int),
+    )]
    fn from_i128(value: i128) -> Self {
        if value >= 0 {
            if let Ok(u) = u64::try_from(value) {
@@ -74,6 +298,19 @@ impl Number {
        }
    }

+    #[verus_spec(result =>
+        ensures
+            match self@ {
+                NumberView::Integer(n) => result matches Some(bi) && bi@ == n,
+                NumberView::Float(f) =>
+                {
+                    match result {
+                        Some(bi) => float_to_small_int(f) == Some(bi@),
+                        None => float_to_small_int(f) is None,
+                    }
+                },
+            },
+    )]
    fn to_bigint_owned(&self) -> Option<BigInt> {
        match self {
            Number::UInt(v) => Some(BigInt::from(*v)),
@@ -83,7 +320,21 @@ impl Number {
        }
    }

+    #[verus_spec(result =>
+        ensures
+            match result {
+                Some(bi) => float_to_small_int(value) == Some(bi@),
+                None => float_to_small_int(value) is None,
+            },
+    )]
    fn float_to_small_bigint(value: f64) -> Option<BigInt> {
+        proof! {
+            axiom_f64_obeys_eq_spec();
+            axiom_f64_obeys_partial_cmp_spec();
+            axiom_f64_ops_deterministic();
+            axiom_f64_comparisons_match_ieee();
+        }
+
        if !value.is_finite() || value.fract() != 0.0 {
            return None;
        }
@@ -94,12 +345,12 @@ impl Number {

        if value >= 0.0 {
            let u = value as u64;
-            if (u as f64) == value {
+            if u as f64 == value {
                return Some(BigInt::from(u));
            }
        } else {
            let i = value as i64;
-            if (i as f64) == value {
+            if i as f64 == value {
                return Some(BigInt::from(i));
            }
        }
@@ -107,6 +358,17 @@ impl Number {
        None
    }

+    #[verus_spec(result =>
+        ensures
+            match self@ {
+                NumberView::Integer(n) => result matches Some(bi) && bi@ == n,
+                NumberView::Float(f) =>
+                    match result {
+                        Some(bi) => float_to_small_int(f) == Some(bi@),
+                        None => float_to_small_int(f) is None,
+                    },
+            },
+    )]
    fn to_bigint_rc(&self) -> Option<Rc<BigInt>> {
        match self {
            Number::BigInt(v) => Some(v.clone()),
@@ -114,7 +376,13 @@ impl Number {
        }
    }

+    #[verus_spec(result =>
+        ensures
+            self@.to_f64_lossy_ensures(result),
+            result == self.spec_to_f64_lossy(),
+    )]
    fn to_f64_lossy(&self) -> f64 {
+        proof! { axiom_f64_ops_deterministic(); }
        match self {
            Number::UInt(v) => *v as f64,
            Number::Int(v) => *v as f64,
@@ -123,15 +391,23 @@ impl Number {
                if let Some(f) = v.to_f64() {
                    f
                } else if v.is_negative() {
-                    f64::NEG_INFINITY
+                    f64_neg_infinity()
                } else {
-                    f64::INFINITY
+                    f64_infinity()
                }
            }
        }
    }

+    #[verus_spec(result =>
+        ensures
+            match self@ {
+                NumberView::Integer(n) => result == (n == 0),
+                NumberView::Float(f) => result == f.eq_spec(&0.0f64),
+            },
+    )]
    fn is_zero(&self) -> bool {
+        proof! { axiom_f64_obeys_eq_spec(); }
        match self {
            Number::UInt(0) | Number::Int(0) => true,
            Number::Float(f) => *f == 0.0,
@@ -140,17 +416,39 @@ impl Number {
        }
    }

+    #[verus_spec(result =>
+        requires
+            a@ is Integer,
+            b@ is Integer,
+        ensures
+            a@ matches NumberView::Integer(m) && result.0@ == m,
+            b@ matches NumberView::Integer(n) && result.1@ == n,
+    )]
    fn ints_to_bigint(a: &Number, b: &Number) -> (BigInt, BigInt) {
        (a.to_bigint_owned().unwrap(), b.to_bigint_owned().unwrap())
    }

+    #[verus_spec(result =>
+        ensures
+            match result@ {
+                NumberView::Integer(n) => float_to_small_int(value) == Some(n),
+                NumberView::Float(f) => float_to_small_int(value) is None && f == value,
+            }
+    )]
    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)
    }

+    #[verus_spec(result =>
+        ensures
+            match self@ {
+                NumberView::Integer(v) => if 0 <= v <= u32::MAX { result == Some(v as u32) } else { result is None },
+                NumberView::Float(_) => result is None,
+            },
+    )]
    fn as_u32(&self) -> Option<u32> {
        match self {
            Number::UInt(v) if *v <= u32::MAX as u64 => Some(*v as u32),
@@ -179,25 +477,45 @@ impl Serialize for Number {
    }
 }

+#[verus_verify]
 impl From<BigInt> for Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value@),
+    )]
    fn from(value: BigInt) -> Self {
        Number::from_bigint_owned(value)
    }
 }

+#[verus_verify]
 impl From<u64> for Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value as int),
+    )]
    fn from(value: u64) -> Self {
        Number::UInt(value)
    }
 }

+#[verus_verify]
 impl From<usize> for Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value as int),
+    )]
    fn from(value: usize) -> Self {
        Number::UInt(value as u64)
    }
 }

+#[verus_verify]
 impl From<u128> for Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value as int),
+    )]
    fn from(value: u128) -> Self {
        if let Ok(n) = u64::try_from(value) {
            Number::UInt(n)
@@ -207,19 +525,34 @@ impl From<u128> for Number {
    }
 }

+#[verus_verify]
 impl From<i64> for Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value as int),
+    )]
    fn from(value: i64) -> Self {
        Number::Int(value)
    }
 }

+#[verus_verify]
 impl From<i128> for Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value as int),
+    )]
    fn from(value: i128) -> Self {
        Number::from_i128(value)
    }
 }

+#[verus_verify]
 impl From<f64> for Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Float(value),
+    )]
    fn from(value: f64) -> Self {
        Number::Float(value)
    }
@@ -287,8 +620,25 @@ impl FromStr for Number {
    }
 }

+#[verus_verify]
 impl PartialEq for Number {
+    #[verus_spec(result =>
+        ensures
+            match (self@.to_int(), other@.to_int()) {
+                (Some(n1), Some(n2)) => result == (n1 == n2),
+                _ => exists|f1: f64, f2: f64| #![trigger self@.to_f64_lossy_ensures(f1), other@.to_f64_lossy_ensures(f2)] {
+                    &&& self@.to_f64_lossy_ensures(f1)
+                    &&& other@.to_f64_lossy_ensures(f2)
+                    &&& result == (!f1.is_nan_spec() && !f2.is_nan_spec() && f1.eq_spec(&f2))
+                },
+            },
+    )]
    fn eq(&self, other: &Self) -> bool {
+        proof! {
+            axiom_bigint_obeys_eq_spec();
+            axiom_f64_obeys_eq_spec();
+        }
+
        if let (Some(a), Some(b)) = (self.to_bigint_owned(), other.to_bigint_owned()) {
            return a == b;
        }
@@ -304,12 +654,31 @@ impl PartialEq for Number {

 impl Eq for Number {}

+#[verus_verify]
 impl Ord for Number {
+    #[verus_spec(result =>
+         ensures
+             match (self@.to_int(), other@.to_int()) {
+                 (Some(n1), Some(n2)) => result == n1.cmp_spec(&n2),
+                 _ => exists|f1: f64, f2: f64| #![trigger self@.to_f64_lossy_ensures(f1), other@.to_f64_lossy_ensures(f2)] {
+                     &&& self@.to_f64_lossy_ensures(f1)
+                     &&& other@.to_f64_lossy_ensures(f2)
+                     &&& result == f1.partial_cmp_spec(&f2).unwrap_or(Ordering::Equal)
+                },
+            },
+    )]
    fn cmp(&self, other: &Self) -> Ordering {
+        proof! {
+            axiom_f64_obeys_partial_cmp_spec();
+            axiom_bigint_obeys_cmp_spec();
+        }
        if let (Some(a), Some(b)) = (self.to_bigint_owned(), other.to_bigint_owned()) {
            return a.cmp(&b);
        }

+        proof! {
+            assume(false);
+        }
        self.to_f64_lossy()
            .partial_cmp(&other.to_f64_lossy())
            .unwrap_or(Ordering::Equal)
--- a/src/verusspec/bigint.rs
+++ b/src/verusspec/bigint.rs
@@ -0,0 +1,712 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+#![allow(
+    clippy::arithmetic_side_effects,
+    clippy::float_cmp,
+    clippy::unwrap_used,
+    clippy::unreachable,
+    clippy::option_if_let_else,
+    clippy::unseparated_literal_suffix,
+    clippy::as_conversions,
+    clippy::unused_trait_names,
+    clippy::pattern_type_mismatch
+)]
+
+#[cfg(verus_keep_ghost)]
+use core::cmp::Ordering;
+#[cfg(verus_keep_ghost)]
+use num_bigint::BigInt;
+#[cfg(verus_keep_ghost)]
+use vstd::std_specs::cmp::OrdSpec;
+use vstd::prelude::*;
+
+verus! {
+
+#[cfg(verus_keep_ghost)]
+#[verifier::external_type_specification]
+#[verifier::external_body]
+pub struct ExNumBigInt(num_bigint::BigInt);
+
+pub assume_specification[ <BigInt as Clone>::clone ](n: &BigInt) -> (res: BigInt)
+    ensures
+        res == n,
+;
+
+#[cfg(verus_keep_ghost)]
+pub trait BigIntAdditionalSpecFns {
+    spec fn view(&self) -> int;
+}
+
+#[cfg(verus_keep_ghost)]
+impl BigIntAdditionalSpecFns for BigInt {
+    uninterp spec fn view(&self) -> int;
+}
+
+// Conditions
+
+pub assume_specification[ <BigInt as num_traits::Zero>::is_zero ](x: &BigInt) -> (res: bool)
+    ensures
+        res == (x@ == 0),
+;
+
+pub assume_specification[ <BigInt as num_traits::Signed>::is_negative ](x: &BigInt) -> (res: bool)
+    ensures
+        res == (x@ < 0),
+;
+
+// PartialEq
+
+pub axiom fn axiom_bigint_obeys_eq_spec()
+    ensures
+        <BigInt as vstd::std_specs::cmp::PartialEqSpec>::obeys_eq_spec(),
+;
+
+pub axiom fn axiom_bigint_obeys_partial_cmp_spec()
+    ensures
+        <BigInt as vstd::std_specs::cmp::PartialOrdSpec>::obeys_partial_cmp_spec(),
+;
+
+pub assume_specification[ <BigInt as core::cmp::PartialEq>::eq ](x: &BigInt, y: &BigInt) -> (res: bool)
+    ensures
+        res == (x@ == y@),
+;
+
+// Ord
+
+pub axiom fn axiom_bigint_obeys_cmp_spec()
+    ensures
+        <BigInt as vstd::std_specs::cmp::OrdSpec>::obeys_cmp_spec(),
+        forall|b1: &BigInt, b2: &BigInt| b1.cmp_spec(b2) == b1@.cmp_spec(&b2@),
+;
+
+pub assume_specification[ <BigInt as core::cmp::Ord>::cmp ](x: &BigInt, y: &BigInt) -> (res: Ordering)
+    ensures
+        res == x@.cmp_spec(&y@),
+;
+
+// From
+
+pub assume_specification[ <BigInt as core::convert::From<i64>>::from ](i: i64) -> (res: BigInt)
+    ensures
+        res@ == i,
+;
+
+pub assume_specification[ <BigInt as core::convert::From<i128>>::from ](i: i128) -> (res: BigInt)
+    ensures
+        res@ == i,
+;
+
+pub assume_specification[ <BigInt as core::convert::From<u64>>::from ](u: u64) -> (res: BigInt)
+    ensures
+        res@ == u,
+;
+
+pub assume_specification[ <BigInt as core::convert::From<u128>>::from ](u: u128) -> (res: BigInt)
+    ensures
+        res@ == u,
+;
+
+// Negation
+
+pub assume_specification[ <BigInt as core::ops::Neg>::neg ](x: BigInt) -> (y: BigInt)
+    ensures
+        y@ == -x@,
+;
+
+// Addition
+
+pub assume_specification[ <BigInt as core::ops::Add>::add ](x: BigInt, y: BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ + y@,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&BigInt>>::add ](x: BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ + (*y)@,
+;
+
+pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Add<&BigInt>>::add ](x: &'b BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == (*x)@ + (*y)@,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u8>>::add ](x: BigInt, y: u8) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u16>>::add ](x: BigInt, y: u16) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u32>>::add ](x: BigInt, y: u32) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u64>>::add ](x: BigInt, y: u64) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u128>>::add ](x: BigInt, y: u128) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i8>>::add ](x: BigInt, y: i8) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i16>>::add ](x: BigInt, y: i16) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i32>>::add ](x: BigInt, y: i32) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i64>>::add ](x: BigInt, y: i64) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i128>>::add ](x: BigInt, y: i128) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u8>>::add ](x: BigInt, y: &u8) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u16>>::add ](x: BigInt, y: &u16) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u32>>::add ](x: BigInt, y: &u32) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u64>>::add ](x: BigInt, y: &u64) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u128>>::add ](x: BigInt, y: &u128) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i8>>::add ](x: BigInt, y: &i8) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i16>>::add ](x: BigInt, y: &i16) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i32>>::add ](x: BigInt, y: &i32) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i64>>::add ](x: BigInt, y: &i64) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i128>>::add ](x: BigInt, y: &i128) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+// Subtraction
+
+pub assume_specification[ <BigInt as core::ops::Sub>::sub ](x: BigInt, y: BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ - y@,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&BigInt>>::sub ](x: BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ - (*y)@,
+;
+
+pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Sub<&BigInt>>::sub ](x: &'b BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == (*x)@ - (*y)@,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u8>>::sub ](x: BigInt, y: u8) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u16>>::sub ](x: BigInt, y: u16) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u32>>::sub ](x: BigInt, y: u32) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u64>>::sub ](x: BigInt, y: u64) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u128>>::sub ](x: BigInt, y: u128) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i8>>::sub ](x: BigInt, y: i8) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i16>>::sub ](x: BigInt, y: i16) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i32>>::sub ](x: BigInt, y: i32) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i64>>::sub ](x: BigInt, y: i64) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i128>>::sub ](x: BigInt, y: i128) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u8>>::sub ](x: BigInt, y: &u8) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u16>>::sub ](x: BigInt, y: &u16) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u32>>::sub ](x: BigInt, y: &u32) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u64>>::sub ](x: BigInt, y: &u64) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u128>>::sub ](x: BigInt, y: &u128) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i8>>::sub ](x: BigInt, y: &i8) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i16>>::sub ](x: BigInt, y: &i16) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i32>>::sub ](x: BigInt, y: &i32) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i64>>::sub ](x: BigInt, y: &i64) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i128>>::sub ](x: BigInt, y: &i128) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+// Multiplication
+
+pub assume_specification[ <BigInt as core::ops::Mul>::mul ](x: BigInt, y: BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ * y@,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Mul<&BigInt>>::mul ](x: BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ * (*y)@,
+;
+
+pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Mul<&BigInt>>::mul ](x: &'b BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == (*x)@ * (*y)@,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u8>>::mul ](x: BigInt, y: u8) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u16>>::mul ](x: BigInt, y: u16) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u32>>::mul ](x: BigInt, y: u32) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u64>>::mul ](x: BigInt, y: u64) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u128>>::mul ](x: BigInt, y: u128) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i8>>::mul ](x: BigInt, y: i8) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i16>>::mul ](x: BigInt, y: i16) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i32>>::mul ](x: BigInt, y: i32) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i64>>::mul ](x: BigInt, y: i64) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i128>>::mul ](x: BigInt, y: i128) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Mul<&u8>>::mul ](x: BigInt, y: &u8) -> (o: BigInt)
+    ensures
+        o@ == x@ * *y,
+;
+
+// Division
+
+pub assume_specification[ <BigInt as core::ops::Div>::div ](x: BigInt, y: BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ / y@,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Div<&BigInt>>::div ](x: BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ / (*y)@,
+;
+
+pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Div<&BigInt>>::div ](x: &'b BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == (*x)@ / (*y)@,
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u8>>::div ](x: BigInt, y: u8) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u16>>::div ](x: BigInt, y: u16) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u32>>::div ](x: BigInt, y: u32) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u64>>::div ](x: BigInt, y: u64) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u128>>::div ](x: BigInt, y: u128) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i8>>::div ](x: BigInt, y: i8) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i16>>::div ](x: BigInt, y: i16) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i32>>::div ](x: BigInt, y: i32) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i64>>::div ](x: BigInt, y: i64) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i128>>::div ](x: BigInt, y: i128) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Div<&u8>>::div ](x: BigInt, y: &u8) -> (o: BigInt)
+    ensures
+        o@ == x@ / (*y as int),
+;
+
+} // end verus!
+
+// Verus's encoding of ToPrimitive relies on an unstable feature
+// `sized_hierarchy`, so we can only talk about it when verifying.
+// So, we wrap it all in `#[cfg(verus_keep_ghost)]`.
+
+#[cfg(verus_keep_ghost)]
+verus! {
+
+// ToPrimitive
+
+#[verifier::external_trait_specification]
+#[verifier::external_trait_extension(ToPrimitiveSpec via ToPrimitiveSpecImpl)]
+pub trait ExToPrimitive {
+    type ExternalTraitSpecificationFor: num_traits::ToPrimitive;
+
+    spec fn obeys_to_primitive_spec() -> bool;
+
+    spec fn spec_to_int(&self) -> Option<int>;
+
+    fn to_isize(&self) -> (res: Option<isize>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(isize::MIN <= n <= isize::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_i8(&self) -> (res: Option<i8>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i8::MIN <= n <= i8::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_i16(&self) -> (res: Option<i16>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i16::MIN <= n <= i16::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_i32(&self) -> (res: Option<i32>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i32::MIN <= n <= i32::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_i64(&self) -> (res: Option<i64>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i64::MIN <= n <= i64::MAX),
+                },
+    ;
+
+    fn to_i128(&self) -> (res: Option<i128>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i128::MIN <= n <= i128::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_usize(&self) -> (res: Option<usize>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(usize::MIN <= n <= usize::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_u8(&self) -> (res: Option<u8>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u8::MIN <= n <= u8::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_u16(&self) -> (res: Option<u16>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u16::MIN <= n <= u16::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_u32(&self) -> (res: Option<u32>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u32::MIN <= n <= u32::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_u64(&self) -> (res: Option<u64>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u64::MIN <= n <= u64::MAX),
+                },
+    ;
+
+    fn to_u128(&self) -> (res: Option<u128>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u128::MIN <= n <= u128::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    spec fn spec_to_f32(&self) -> Option<f32>;
+
+    fn to_f32(&self) -> (res: Option<f32>)
+        ensures
+            Self::obeys_to_primitive_spec() ==> res == self.spec_to_f32(),
+        default_ensures
+            true,
+    ;
+
+    spec fn spec_to_f64(&self) -> Option<f64>;
+
+    fn to_f64(&self) -> (res: Option<f64>)
+        ensures
+            Self::obeys_to_primitive_spec() ==> res == self.spec_to_f64(),
+        default_ensures
+            true,
+    ;
+}
+
+impl ToPrimitiveSpecImpl for num_bigint::BigInt
+{
+    open spec fn obeys_to_primitive_spec() -> bool
+    {
+        true
+    }
+
+    open spec fn spec_to_int(&self) -> Option<int>
+    {
+        Some(self@)
+    }
+
+    uninterp spec fn spec_to_f32(&self) -> Option<f32>;
+
+    uninterp spec fn spec_to_f64(&self) -> Option<f64>;
+}
+
+// These are the methods of ToPrimitive that BigInt implements because there is no default in ToPrimitive
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_i64 ](x: &BigInt) -> (res: Option<i64>);
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_u64 ](x: &BigInt) -> (res: Option<u64>);
+
+// These are the methods of ToPrimitive that BigInt overrides the defaults for because they'd otherwise be wrong
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_i128 ](x: &BigInt) -> (res: Option<i128>);
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_u128 ](x: &BigInt) -> (res: Option<u128>);
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_f32 ](x: &BigInt) -> (res: Option<f32>);
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_f64 ](x: &BigInt) -> (res: Option<f64>);
+
+} // end verus! hidden by cfg(verus_keep_ghost)
--- a/src/verusspec/float.rs
+++ b/src/verusspec/float.rs
@@ -0,0 +1,122 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+#![allow(
+    clippy::arithmetic_side_effects,
+    clippy::float_cmp,
+    clippy::unwrap_used,
+    clippy::unreachable,
+    clippy::option_if_let_else,
+    clippy::unseparated_literal_suffix,
+    clippy::as_conversions,
+    clippy::unused_trait_names,
+    clippy::pattern_type_mismatch
+)]
+
+#[cfg(verus_keep_ghost)]
+use vstd::float::*;
+#[cfg(verus_keep_ghost)]
+use vstd::std_specs::cmp::PartialEqIs;
+#[cfg(verus_keep_ghost)]
+use vstd::std_specs::cmp::PartialOrdIs;
+use vstd::prelude::*;
+
+verus! {
+
+pub axiom fn axiom_f64_obeys_eq_spec()
+    ensures
+        <f64 as vstd::std_specs::cmp::PartialEqSpec>::obeys_eq_spec(),
+;
+
+pub axiom fn axiom_f64_obeys_partial_cmp_spec()
+    ensures
+        <f64 as vstd::std_specs::cmp::PartialOrdSpec>::obeys_partial_cmp_spec(),
+;
+
+pub axiom fn axiom_f64_comparisons_match_ieee()
+    ensures
+        forall|f1: f64, f2: f64| #[trigger] f1.ieee_lt(f2) <==> f1.is_lt(&f2),
+        forall|f1: f64, f2: f64| #[trigger] f1.ieee_le(f2) <==> f1.is_le(&f2),
+        forall|f1: f64, f2: f64| #[trigger] f1.ieee_gt(f2) <==> f1.is_gt(&f2),
+        forall|f1: f64, f2: f64| #[trigger] f1.ieee_ge(f2) <==> f1.is_ge(&f2),
+;
+
+pub axiom fn axiom_f64_ops_deterministic()
+    ensures
+        <f64 as vstd::std_specs::ops::NegSpec>::obeys_neg_spec(),
+        <f64 as vstd::std_specs::ops::AddSpec>::obeys_add_spec(),
+        <f64 as vstd::std_specs::ops::SubSpec>::obeys_sub_spec(),
+        <f64 as vstd::std_specs::ops::MulSpec>::obeys_mul_spec(),
+        <f64 as vstd::std_specs::ops::DivSpec>::obeys_div_spec(),
+        forall|n: i8, f: f64| float_cast_spec::<i8, f64>(n, f) ==> f == ieee_float_cast::<i8, f64>(n),
+        forall|n: u8, f: f64| float_cast_spec::<u8, f64>(n, f) ==> f == ieee_float_cast::<u8, f64>(n),
+        forall|n: i8, f: f64| float_cast_spec::<f64, i8>(f, n) ==> n == ieee_float_cast::<f64, i8>(f),
+        forall|n: u8, f: f64| float_cast_spec::<f64, u8>(f, n) ==> n == ieee_float_cast::<f64, u8>(f),
+        forall|n: i16, f: f64| float_cast_spec::<i16, f64>(n, f) ==> f == ieee_float_cast::<i16, f64>(n),
+        forall|n: u16, f: f64| float_cast_spec::<u16, f64>(n, f) ==> f == ieee_float_cast::<u16, f64>(n),
+        forall|n: i16, f: f64| float_cast_spec::<f64, i16>(f, n) ==> n == ieee_float_cast::<f64, i16>(f),
+        forall|n: u16, f: f64| float_cast_spec::<f64, u16>(f, n) ==> n == ieee_float_cast::<f64, u16>(f),
+        forall|n: i32, f: f64| float_cast_spec::<i32, f64>(n, f) ==> f == ieee_float_cast::<i32, f64>(n),
+        forall|n: u32, f: f64| float_cast_spec::<u32, f64>(n, f) ==> f == ieee_float_cast::<u32, f64>(n),
+        forall|n: i32, f: f64| float_cast_spec::<f64, i32>(f, n) ==> n == ieee_float_cast::<f64, i32>(f),
+        forall|n: u32, f: f64| float_cast_spec::<f64, u32>(f, n) ==> n == ieee_float_cast::<f64, u32>(f),
+        forall|n: i64, f: f64| float_cast_spec::<i64, f64>(n, f) ==> f == ieee_float_cast::<i64, f64>(n),
+        forall|n: u64, f: f64| float_cast_spec::<u64, f64>(n, f) ==> f == ieee_float_cast::<u64, f64>(n),
+        forall|n: i64, f: f64| float_cast_spec::<f64, i64>(f, n) ==> n == ieee_float_cast::<f64, i64>(f),
+        forall|n: u64, f: f64| float_cast_spec::<f64, u64>(f, n) ==> n == ieee_float_cast::<f64, u64>(f),
+        forall|n: i128, f: f64| float_cast_spec::<i128, f64>(n, f) ==> f == ieee_float_cast::<i128, f64>(n),
+        forall|n: u128, f: f64| float_cast_spec::<u128, f64>(n, f) ==> f == ieee_float_cast::<u128, f64>(n),
+        forall|n: i128, f: f64| float_cast_spec::<f64, i128>(f, n) ==> n == ieee_float_cast::<f64, i128>(f),
+        forall|n: u128, f: f64| float_cast_spec::<f64, u128>(f, n) ==> n == ieee_float_cast::<f64, u128>(f),
+;
+
+pub assume_specification [ f64::is_finite ](f: f64) -> (res: bool)
+    ensures
+        res == f.is_finite_spec(),
+;
+
+pub uninterp spec fn spec_f64_fract(f: f64) -> f64;
+
+pub assume_specification [ f64::fract ](f: f64) -> (res: f64)
+    requires
+        f.is_finite_spec(),
+    ensures
+        res == spec_f64_fract(f),
+;
+
+pub uninterp spec fn spec_f64_abs(f: f64) -> f64;
+
+pub assume_specification [ f64::abs ](f: f64) -> (res: f64)
+    requires
+        f.is_finite_spec(),
+    ensures
+        res == spec_f64_abs(f),
+;
+
+pub assume_specification [ f64::is_nan ](f: f64) -> (res: bool)
+    ensures
+        res == f.is_nan_spec(),
+;
+
+pub uninterp spec fn spec_f64_neg_infinity() -> f64;
+
+#[inline]
+#[verifier::external_body]
+pub fn f64_neg_infinity() -> (res: f64)
+    ensures
+        res == spec_f64_neg_infinity(),
+{
+    f64::NEG_INFINITY
+}
+
+pub uninterp spec fn spec_f64_infinity() -> f64;
+
+#[inline]
+#[verifier::external_body]
+pub fn f64_infinity() -> (res: f64)
+    ensures
+        res == spec_f64_infinity(),
+{
+    f64::INFINITY
+}
+
+} // end verus!
--- a/src/verusspec/mod.rs
+++ b/src/verusspec/mod.rs
@@ -0,0 +1,3 @@
+pub(crate) mod bigint;
+pub(crate) mod float;
+pub(crate) mod utils;
--- a/src/verusspec/utils.rs
+++ b/src/verusspec/utils.rs
@@ -0,0 +1,65 @@
+use anyhow::{bail, Result};
+use std::format;
+use std::string::String;
+
+use vstd::prelude::*;
+
+verus! {
+
+#[cfg(verus_keep_ghost)]
+#[verifier::external_body]
+pub fn verus_format_helper() -> String
+{
+    format!("who cares")
+}
+
+macro_rules! verus_format {
+    ( $( $tt0:tt )* ) => {
+        {
+            #[cfg(not(verus_keep_ghost))]
+            { format!($($tt0)*) }
+            #[cfg(verus_keep_ghost)]
+            { verus_format_helper() }
+        }
+    }
+}
+
+#[allow(dead_code)]
+fn my_test_verus_format(fcn: &'static str, x: u32) -> String
+{
+    verus_format!("The parameters are `{fcn}` and `{x}`")
+}
+
+#[cfg(verus_keep_ghost)]
+#[verifier::external_type_specification]
+#[verifier::external_body]
+pub struct ExAnyhowError(anyhow::Error);
+
+#[cfg(verus_keep_ghost)]
+#[verifier::external_body]
+pub fn verus_bail_helper<T>() -> Result<T>
+{
+    bail!("who cares")
+}
+
+macro_rules! verus_bail {
+    ( $( $tt0:tt )* ) => {
+        {
+            #[cfg(not(verus_keep_ghost))]
+            { bail!($($tt0)*) }
+            #[cfg(verus_keep_ghost)]
+            { return verus_bail_helper(); }
+        }
+    }
+}
+
+#[allow(dead_code)]
+fn my_test_verus_bail(fcn: &'static str, x: u32) -> Result<()>
+{
+    if x > 0 {
+        verus_bail!("Invalid parameters `{}` and `{}`", fcn, x)
+    }
+    Ok(())
+}
+
+} // end verus!
Author	SHA1	Message	Date
Jay Lorch	f44e019f41	Spec for Number as Ord	2026-03-19 15:52:41 -07:00
Jay Lorch	2b4ab8e12d	Simpler spec for Number::eq	2026-03-19 14:48:03 -07:00
Jay Lorch	41c2d502fa	Simplify Number::eq spec	2026-03-19 13:58:10 -07:00
Jay Lorch	85e58c6f6c	Simplify float comparisons by assuming IEEE	2026-03-19 11:52:35 -07:00
Jay Lorch	9e18ded98e	Simplify float spec by avoiding partial_cmp_spec	2026-03-19 11:33:30 -07:00
Jay Lorch	2e454f2708	Simplify float specs by assuming determinism	2026-03-19 10:49:59 -07:00
Jay Lorch	d107c1b647	Use float specs in latest Verus	2026-03-18 18:21:10 -07:00
Jay Lorch	462e39f2ad	Switch to attribute syntax	2026-03-12 18:31:02 -07:00
Jay Lorch	7e1afe0e86	More specs for Number	2026-03-11 17:43:20 -07:00
Jay Lorch	faa3efb8b8	Update Cargo.toml to use public vstd crate	2026-03-04 10:05:58 -08:00
Jay Lorch	100be610db	Don't shut off so much of bigint when not verifying	2026-03-03 17:00:30 -08:00
Jay Lorch	586d631f09	Got cargo build working	2026-03-03 16:46:09 -08:00
Jay Lorch	5819992d17	More progress toward cargo build	2026-03-03 16:44:31 -08:00
Jay Lorch	90894aa8e1	Progress to cargo build success	2026-03-03 16:35:05 -08:00
Jay Lorch	1f2a2ecb41	More specs for Number	2026-03-03 16:20:59 -08:00
Jay Lorch	ba987998c4	More Number proofs	2026-03-03 15:58:36 -08:00
Jay Lorch	c3813c8876	Avoid some build errors	2026-03-03 15:16:35 -08:00
Jay Lorch	6ab452989f	Proofs about some float operations	2026-03-03 14:43:45 -08:00
Jay Lorch	4865364b48	Verus specs for BigNum, Number	2026-02-27 15:52:00 -08:00
Jay Lorch	156772c523	Add Verus dependencies	2026-02-17 13:25:11 -08:00
dependabot[bot]	8814eda0ae	Bump the per-dependency group with 1 update (#587 ) Bumps Microsoft.Build.NoTargets from 3.7.56 to 3.7.134 --- updated-dependencies: - dependency-name: Microsoft.Build.NoTargets dependency-version: 3.7.134 dependency-type: direct:production update-type: version-update:semver-patch dependency-group: per-dependency ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>	2026-02-12 16:47:12 -06:00
dependabot[bot]	b4a69a13ba	build(deps): bump the per-dependency group (#585 ) --- updated-dependencies: - dependency-name: magnus dependency-version: 0.8.2 dependency-type: direct:production update-type: version-update:semver-minor dependency-group: per-dependency - dependency-name: regorus dependency-version: 0.9.1 dependency-type: direct:production update-type: version-update:semver-minor dependency-group: per-dependency - dependency-name: serde_magnus dependency-version: 0.11.0 dependency-type: direct:production update-type: version-update:semver-minor dependency-group: per-dependency ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>	2026-02-12 09:53:36 -06:00
dependabot[bot]	e83a47497a	build(deps): bump the per-dependency group (#586 ) Bumps the per-dependency group in /bindings/ruby with 7 updates: \| Package \| From \| To \| \| --- \| --- \| --- \| \| [minitest](https://github.com/minitest/minitest) \| `5.25.4` \| `6.0.1` \| \| [rake](https://github.com/ruby/rake) \| `13.2.1` \| `13.3.1` \| \| [rake-compiler](https://github.com/rake-compiler/rake-compiler) \| `1.2.9` \| `1.3.1` \| \| [rake-compiler-dock](https://github.com/rake-compiler/rake-compiler-dock) \| `1.9.1` \| `1.11.0` \| \| [rubocop](https://github.com/rubocop/rubocop) \| `1.73.2` \| `1.84.1` \| \| [rubocop-minitest](https://github.com/rubocop/rubocop-minitest) \| `0.37.1` \| `0.38.2` \| \| [rb_sys](https://github.com/oxidize-rb/rb-sys) \| `0.9.111` \| `0.9.124` \| Updates `minitest` from 5.25.4 to 6.0.1 - [Changelog](https://github.com/minitest/minitest/blob/master/History.rdoc) - [Commits](https://github.com/minitest/minitest/compare/v5.25.4...v6.0.1) Updates `rake` from 13.2.1 to 13.3.1 - [Release notes](https://github.com/ruby/rake/releases) - [Changelog](https://github.com/ruby/rake/blob/master/History.rdoc) - [Commits](https://github.com/ruby/rake/compare/v13.2.1...v13.3.1) Updates `rake-compiler` from 1.2.9 to 1.3.1 - [Release notes](https://github.com/rake-compiler/rake-compiler/releases) - [Changelog](https://github.com/rake-compiler/rake-compiler/blob/master/History.md) - [Commits](https://github.com/rake-compiler/rake-compiler/compare/v1.2.9...v1.3.1) Updates `rake-compiler-dock` from 1.9.1 to 1.11.0 - [Release notes](https://github.com/rake-compiler/rake-compiler-dock/releases) - [Changelog](https://github.com/rake-compiler/rake-compiler-dock/blob/main/CHANGELOG.md) - [Commits](https://github.com/rake-compiler/rake-compiler-dock/compare/v1.9.1...v1.11.0) Updates `rubocop` from 1.73.2 to 1.84.1 - [Release notes](https://github.com/rubocop/rubocop/releases) - [Changelog](https://github.com/rubocop/rubocop/blob/master/CHANGELOG.md) - [Commits](https://github.com/rubocop/rubocop/compare/v1.73.2...v1.84.1) Updates `rubocop-minitest` from 0.37.1 to 0.38.2 - [Release notes](https://github.com/rubocop/rubocop-minitest/releases) - [Changelog](https://github.com/rubocop/rubocop-minitest/blob/master/CHANGELOG.md) - [Commits](https://github.com/rubocop/rubocop-minitest/compare/v0.37.1...v0.38.2) Updates `rb_sys` from 0.9.111 to 0.9.124 - [Release notes](https://github.com/oxidize-rb/rb-sys/releases) - [Commits](https://github.com/oxidize-rb/rb-sys/compare/v0.9.111...v0.9.124) --- updated-dependencies: - dependency-name: minitest dependency-version: 6.0.1 dependency-type: direct:production update-type: version-update:semver-major dependency-group: per-dependency - dependency-name: rake dependency-version: 13.3.1 dependency-type: direct:production update-type: version-update:semver-minor dependency-group: per-dependency - dependency-name: rake-compiler dependency-version: 1.3.1 dependency-type: direct:production update-type: version-update:semver-minor dependency-group: per-dependency - dependency-name: rake-compiler-dock dependency-version: 1.11.0 dependency-type: direct:production update-type: version-update:semver-minor dependency-group: per-dependency - dependency-name: rubocop dependency-version: 1.84.1 dependency-type: direct:production update-type: version-update:semver-minor dependency-group: per-dependency - dependency-name: rubocop-minitest dependency-version: 0.38.2 dependency-type: direct:production update-type: version-update:semver-minor dependency-group: per-dependency - dependency-name: rb_sys dependency-version: 0.9.124 dependency-type: direct:production update-type: version-update:semver-patch dependency-group: per-dependency ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>	2026-02-12 09:53:00 -06:00
dependabot[bot]	241c1d445b	build(deps-dev): bump the per-dependency group (#583 ) Bumps the per-dependency group in /bindings/java with 6 updates: \| Package \| From \| To \| \| --- \| --- \| --- \| \| [junit:junit](https://github.com/junit-team/junit4) \| `3.8.1` \| `4.13.2` \| \| [com.google.code.gson:gson](https://github.com/google/gson) \| `2.10.1` \| `2.13.2` \| \| [org.codehaus.mojo:exec-maven-plugin](https://github.com/mojohaus/exec-maven-plugin) \| `3.1.0` \| `3.6.3` \| \| [org.apache.maven.plugins:maven-surefire-plugin](https://github.com/apache/maven-surefire) \| `3.2.5` \| `3.5.4` \| \| [org.apache.maven.plugins:maven-javadoc-plugin](https://github.com/apache/maven-javadoc-plugin) \| `3.6.3` \| `3.12.0` \| \| [org.apache.maven.plugins:maven-source-plugin](https://github.com/apache/maven-source-plugin) \| `3.3.0` \| `3.4.0` \| Updates `junit:junit` from 3.8.1 to 4.13.2 - [Release notes](https://github.com/junit-team/junit4/releases) - [Changelog](https://github.com/junit-team/junit4/blob/main/doc/ReleaseNotes4.13.2.md) - [Commits](https://github.com/junit-team/junit4/commits/r4.13.2) Updates `com.google.code.gson:gson` from 2.10.1 to 2.13.2 - [Release notes](https://github.com/google/gson/releases) - [Changelog](https://github.com/google/gson/blob/main/CHANGELOG.md) - [Commits](https://github.com/google/gson/compare/gson-parent-2.10.1...gson-parent-2.13.2) Updates `org.codehaus.mojo:exec-maven-plugin` from 3.1.0 to 3.6.3 - [Release notes](https://github.com/mojohaus/exec-maven-plugin/releases) - [Commits](https://github.com/mojohaus/exec-maven-plugin/compare/exec-maven-plugin-3.1.0...3.6.3) Updates `org.apache.maven.plugins:maven-surefire-plugin` from 3.2.5 to 3.5.4 - [Release notes](https://github.com/apache/maven-surefire/releases) - [Commits](https://github.com/apache/maven-surefire/compare/surefire-3.2.5...surefire-3.5.4) Updates `org.apache.maven.plugins:maven-javadoc-plugin` from 3.6.3 to 3.12.0 - [Release notes](https://github.com/apache/maven-javadoc-plugin/releases) - [Commits](https://github.com/apache/maven-javadoc-plugin/compare/maven-javadoc-plugin-3.6.3...maven-javadoc-plugin-3.12.0) Updates `org.apache.maven.plugins:maven-source-plugin` from 3.3.0 to 3.4.0 - [Release notes](https://github.com/apache/maven-source-plugin/releases) - [Commits](https://github.com/apache/maven-source-plugin/compare/maven-source-plugin-3.3.0...maven-source-plugin-3.4.0) --- updated-dependencies: - dependency-name: junit:junit dependency-version: 4.13.2 dependency-type: direct:development update-type: version-update:semver-major dependency-group: per-dependency - dependency-name: com.google.code.gson:gson dependency-version: 2.13.2 dependency-type: direct:development update-type: version-update:semver-minor dependency-group: per-dependency - dependency-name: org.codehaus.mojo:exec-maven-plugin dependency-version: 3.6.3 dependency-type: direct:development update-type: version-update:semver-minor dependency-group: per-dependency - dependency-name: org.apache.maven.plugins:maven-surefire-plugin dependency-version: 3.5.4 dependency-type: direct:development update-type: version-update:semver-minor dependency-group: per-dependency - dependency-name: org.apache.maven.plugins:maven-javadoc-plugin dependency-version: 3.12.0 dependency-type: direct:development update-type: version-update:semver-minor dependency-group: per-dependency - dependency-name: org.apache.maven.plugins:maven-source-plugin dependency-version: 3.4.0 dependency-type: direct:development update-type: version-update:semver-minor dependency-group: per-dependency ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>	2026-02-12 09:46:33 -06:00
dependabot[bot]	4054d1b6b6	build(deps): bump the per-dependency group with 12 updates (#593 ) Bumps the per-dependency group with 12 updates: \| Package \| From \| To \| \| --- \| --- \| --- \| \| [actions/checkout](https://github.com/actions/checkout) \| `4.3.1` \| `6.0.2` \| \| [actions/setup-python](https://github.com/actions/setup-python) \| `5.6.0` \| `6.2.0` \| \| [actions/setup-java](https://github.com/actions/setup-java) \| `4.8.0` \| `5.2.0` \| \| [actions/setup-go](https://github.com/actions/setup-go) \| `5.1.0` \| `6.2.0` \| \| [actions/setup-dotnet](https://github.com/actions/setup-dotnet) \| `4.1.0` \| `5.1.0` \| \| [actions/setup-node](https://github.com/actions/setup-node) \| `4.4.0` \| `6.2.0` \| \| [github/codeql-action](https://github.com/github/codeql-action) \| `3.32.2` \| `4.32.2` \| \| [actions/upload-artifact](https://github.com/actions/upload-artifact) \| `4.6.2` \| `6.0.0` \| \| [actions/download-artifact](https://github.com/actions/download-artifact) \| `5.0.0` \| `7.0.0` \| \| [PyO3/maturin-action](https://github.com/pyo3/maturin-action) \| `63b75c597b83e247fbf4fb7719801cc4220ae9f3` \| `b1bd829e37fef14c63f19162034228a2f3dc1021` \| \| [MarcoIeni/release-plz-action](https://github.com/marcoieni/release-plz-action) \| `0.5.108` \| `0.5.126` \| \| [oxidize-rb/actions](https://github.com/oxidize-rb/actions) \| `1.2.6` \| `1.4.4` \| Updates `actions/checkout` from 4.3.1 to 6.0.2 - [Release notes](https://github.com/actions/checkout/releases) - [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md) - [Commits](`34e114876b...de0fac2e45`) Updates `actions/setup-python` from 5.6.0 to 6.2.0 - [Release notes](https://github.com/actions/setup-python/releases) - [Commits](`a26af69be9...a309ff8b42`) Updates `actions/setup-java` from 4.8.0 to 5.2.0 - [Release notes](https://github.com/actions/setup-java/releases) - [Commits](https://github.com/actions/setup-java/compare/v4.8.0...be666c2fcd27ec809703dec50e508c2fdc7f6654) Updates `actions/setup-go` from 5.1.0 to 6.2.0 - [Release notes](https://github.com/actions/setup-go/releases) - [Commits](https://github.com/actions/setup-go/compare/v5.1.0...7a3fe6cf4cb3a834922a1244abfce67bcef6a0c5) Updates `actions/setup-dotnet` from 4.1.0 to 5.1.0 - [Release notes](https://github.com/actions/setup-dotnet/releases) - [Commits](https://github.com/actions/setup-dotnet/compare/v4.1.0...baa11fbfe1d6520db94683bd5c7a3818018e4309) Updates `actions/setup-node` from 4.4.0 to 6.2.0 - [Release notes](https://github.com/actions/setup-node/releases) - [Commits](`49933ea528...6044e13b5d`) Updates `github/codeql-action` from 3.32.2 to 4.32.2 - [Release notes](https://github.com/github/codeql-action/releases) - [Changelog](https://github.com/github/codeql-action/blob/main/CHANGELOG.md) - [Commits](https://github.com/github/codeql-action/compare/v3.32.2...45cbd0c69e560cd9e7cd7f8c32362050c9b7ded2) Updates `actions/upload-artifact` from 4.6.2 to 6.0.0 - [Release notes](https://github.com/actions/upload-artifact/releases) - [Commits](`ea165f8d65...b7c566a772`) Updates `actions/download-artifact` from 5.0.0 to 7.0.0 - [Release notes](https://github.com/actions/download-artifact/releases) - [Commits](`634f93cb29...37930b1c2a`) Updates `PyO3/maturin-action` from 63b75c597b83e247fbf4fb7719801cc4220ae9f3 to b1bd829e37fef14c63f19162034228a2f3dc1021 - [Release notes](https://github.com/pyo3/maturin-action/releases) - [Commits](`63b75c597b...b1bd829e37`) Updates `MarcoIeni/release-plz-action` from 0.5.108 to 0.5.126 - [Release notes](https://github.com/marcoieni/release-plz-action/releases) - [Commits](`8724d33cd9...52440b50d3`) Updates `oxidize-rb/actions` from 1.2.6 to 1.4.4 - [Release notes](https://github.com/oxidize-rb/actions/releases) - [Commits](`7ca44a16e2...e5f9a49a78`) --- updated-dependencies: - dependency-name: actions/checkout dependency-version: 6.0.2 dependency-type: direct:production update-type: version-update:semver-major dependency-group: per-dependency - dependency-name: actions/setup-python dependency-version: 6.2.0 dependency-type: direct:production update-type: version-update:semver-major dependency-group: per-dependency - dependency-name: actions/setup-java dependency-version: 5.2.0 dependency-type: direct:production update-type: version-update:semver-major dependency-group: per-dependency - dependency-name: actions/setup-go dependency-version: 6.2.0 dependency-type: direct:production update-type: version-update:semver-major dependency-group: per-dependency - dependency-name: actions/setup-dotnet dependency-version: 5.1.0 dependency-type: direct:production update-type: version-update:semver-major dependency-group: per-dependency - dependency-name: actions/setup-node dependency-version: 6.2.0 dependency-type: direct:production update-type: version-update:semver-major dependency-group: per-dependency - dependency-name: github/codeql-action dependency-version: 4.32.2 dependency-type: direct:production update-type: version-update:semver-major dependency-group: per-dependency - dependency-name: actions/upload-artifact dependency-version: 6.0.0 dependency-type: direct:production update-type: version-update:semver-major dependency-group: per-dependency - dependency-name: actions/download-artifact dependency-version: 7.0.0 dependency-type: direct:production update-type: version-update:semver-major dependency-group: per-dependency - dependency-name: PyO3/maturin-action dependency-version: b1bd829e37fef14c63f19162034228a2f3dc1021 dependency-type: direct:production dependency-group: per-dependency - dependency-name: MarcoIeni/release-plz-action dependency-version: 0.5.126 dependency-type: direct:production update-type: version-update:semver-patch dependency-group: per-dependency - dependency-name: oxidize-rb/actions dependency-version: 1.4.4 dependency-type: direct:production update-type: version-update:semver-minor dependency-group: per-dependency ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>	2026-02-12 06:30:19 -06:00
Anand Krishnamoorthi	8f7ca44bdf	chore(dependabot): expand coverage and pin workflows (#579 ) - Expand dependabot coverage across Rust subcrates and other ecosystems. - Group updates per dependency and ignore vendored mimalloc crates. - Pin GitHub Actions to exact SHAs in existing workflows.	2026-02-11 17:43:48 -06:00