Spec for Number as Ord

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>

.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:
+          - "*"

.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}}"

.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

.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

.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

.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:

.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'

.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 }}

.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

.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
 

.github/workflows/test-csharp.yml

@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
 name: bindings/csharp
 
 on:
@@ -31,17 +33,18 @@ jobs:
             target: x86_64-unknown-linux-gnu
             libpath: |
               **/release/libregorus_ffi.so
-          # Disabled for now
-          #- os: macos-latest
-          #  target: aarch64-apple-darwin
-          #  libpath: |
-          #    **/release/libregorus_ffi.dylib
+          - os: macos-latest
+            target: aarch64-apple-darwin
+            libpath: |
+              **/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
+        with:
+          targets: ${{ matrix.runtime.target }}
       - name: Cache cargo
         uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2.8.2
         with:
@@ -56,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.
@@ -70,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
 
@@ -89,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
@@ -99,13 +102,15 @@ jobs:
         run: ls -R ./bindings/csharp/Regorus/tmp
 
       - name: Build Regorus nuget via xtask
-        run: cargo xtask build-csharp --release --clean --artifacts-dir ./bindings/csharp/Regorus/tmp/bindings/ffi/target --enforce-artifacts
+        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: bindings/csharp/Regorus/bin/Release/Regorus*.nupkg
+          path: |
+            bindings/csharp/Regorus/bin/Release/Regorus*.nupkg
+            bindings/csharp/Regorus/bin/Release/Regorus*.snupkg
           if-no-files-found: error
           retention-days: 1
 
@@ -122,17 +127,17 @@ jobs:
             target: x86_64-pc-windows-msvc
           - os: ubuntu-latest
             target: x86_64-unknown-linux-gnu
-          #- os: macos-latest
-          #  target: aarch64-apple-darwin
+          - os: macos-latest
+            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
 
@@ -147,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

.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

.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
 

.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"

.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

.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

.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

.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

.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
 

.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

.gitignore

@@ -48,3 +48,6 @@ bindings/ruby/bin/
 bindings/java/.classpath
 bindings/java/.project
 bindings/java/.settings/
+
+# Emacs temporary files
+*~

CHANGELOG.md

@@ -6,6 +6,16 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+## [0.9.1](https://github.com/microsoft/regorus/compare/regorus-v0.9.0...regorus-v0.9.1) - 2026-02-06
+
+### Fixed
+- Release native C# handles reliably to avoid memory growth ([#571](https://github.com/microsoft/regorus/pull/571)).
+- Centralize C# handle gating with a short dispose wait and deferred release to avoid leaks while blocking new calls ([#571](https://github.com/microsoft/regorus/pull/571)).
+
+### Added
+- Manual C# memory growth tests for both `using` and finalizer paths ([#571](https://github.com/microsoft/regorus/pull/571)).
+- C# test runner options for filtered tests, console logging, and skipping sample apps ([#571](https://github.com/microsoft/regorus/pull/571)).
+
 ## [0.5.0](https://github.com/microsoft/regorus/compare/regorus-v0.4.0...regorus-v0.5.0) - 2025-07-08
 
 ### Added

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"
@@ -1227,7 +1243,7 @@ checksum = "7a2d987857b319362043e95f5353c0535c1f58eec5336fdfcf626430af7def58"
 
 [[package]]
 name = "regorus"
-version = "0.9.0"
+version = "0.9.1"
 dependencies = [
  "anyhow",
  "bincode",
@@ -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"

Cargo.toml

@@ -8,12 +8,17 @@ members = [
 [package]
 name = "regorus"
 description = "A fast, lightweight Rego (OPA policy language) interpreter"
-version = "0.9.0"
+version = "0.9.1"
 edition = "2021"
 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)'] }

bindings/csharp/Benchmarks/CompiledPolicyEvaluationBenchmark.cs

@@ -12,7 +12,7 @@ namespace Benchmarks
     public class CompiledPolicyEvaluationBenchmark
     {
         private static readonly string TestDataPath = Path.Combine(
-            Directory.GetCurrentDirectory(), 
+            Directory.GetCurrentDirectory(),
             "..", "..", "..",
             "benches", "evaluation", "test_data"
         );
@@ -33,7 +33,7 @@ namespace Benchmarks
         private static readonly string[] PolicyNames = new[]
         {
             "rbac_policy",
-            "api_access_policy", 
+            "api_access_policy",
             "data_sensitivity_policy",
             "time_based_policy",
             "data_processing_policy",
@@ -46,21 +46,21 @@ namespace Benchmarks
         private static List<(string Policy, string[] Inputs)> LoadPoliciesWithInputs()
         {
             var result = new List<(string Policy, string[] Inputs)>();
-            
+
             foreach (var (policyFile, inputFiles) in PolicyInputFiles)
             {
                 var policyPath = Path.Combine(TestDataPath, "policies", policyFile);
                 var policy = File.ReadAllText(policyPath);
-                
+
                 var inputs = inputFiles.Select(inputFile =>
                 {
                     var inputPath = Path.Combine(TestDataPath, "inputs", inputFile);
                     return File.ReadAllText(inputPath);
                 }).ToArray();
-                
+
                 result.Add((policy, inputs));
             }
-            
+
             return result;
         }
 
@@ -68,14 +68,14 @@ namespace Benchmarks
         {
             var policiesWithInputs = LoadPoliciesWithInputs();
             var compiledPolicies = new List<CompiledPolicy>();
-            
+
             foreach (var (policy, _) in policiesWithInputs)
             {
-                var modules = new[] { new PolicyModule { Id = "policy.rego", Content = policy } };
+                var modules = new[] { new PolicyModule("policy.rego", policy) };
                 var compiled = Compiler.CompilePolicyWithEntrypoint("{}", modules, "data.bench.allow");
                 compiledPolicies.Add(compiled);
             }
-            
+
             return compiledPolicies;
         }
 
@@ -84,13 +84,13 @@ namespace Benchmarks
             var cpuCount = Environment.ProcessorCount;
             var maxThreads = cpuCount * 2;
             var threadCounts = new List<int> { 1, 2 };
-            
+
             // Add even numbers from 4 to maxThreads
             for (int i = 4; i <= maxThreads; i += 2)
             {
                 threadCounts.Add(i);
             }
-            
+
             Console.WriteLine($"Running compiled policy benchmark with max_threads: {maxThreads}");
             Console.WriteLine($"Testing with thread counts: {string.Join(", ", threadCounts)}");
             Console.WriteLine();
@@ -120,19 +120,19 @@ namespace Benchmarks
             const int durationSeconds = 3;
             var policiesWithInputs = LoadPoliciesWithInputs();
             List<CompiledPolicy>? compiledPolicies = null;
-            
+
             if (useSharedPolicies)
             {
                 compiledPolicies = PrepareSharedCompiledPolicies();
             }
-            
+
             Console.WriteLine($"Warming up with {threads} threads for {warmupSeconds} seconds...");
-            
+
             // Warmup phase
             var (_, _, _, _) = RunBenchmarkPhase(threads, warmupSeconds, policiesWithInputs, compiledPolicies, useSharedPolicies, isWarmup: true);
-            
+
             Console.WriteLine($"Running benchmark with {threads} threads for {durationSeconds} seconds...");
-            
+
             // Actual benchmark phase
             var (totalEvaluations, evaluationTime, policyCounters, allocatedBytes) = RunBenchmarkPhase(threads, durationSeconds, policiesWithInputs, compiledPolicies, useSharedPolicies, isWarmup: false);
 
@@ -155,7 +155,7 @@ namespace Benchmarks
             {
                 foreach (var policy in compiledPolicies)
                 {
-                    policy.Dispose();
+                    DisposeCompiledPolicy(policy);
                 }
             }
 
@@ -173,8 +173,8 @@ namespace Benchmarks
         }
 
         private static (int totalEvaluations, TimeSpan evaluationTime, Dictionary<string, int> policyCounters, long allocatedBytes) RunBenchmarkPhase(
-            int threads, 
-            int durationSeconds, 
+            int threads,
+            int durationSeconds,
             List<(string Policy, string[] Inputs)> policiesWithInputs,
             List<CompiledPolicy>? compiledPolicies,
             bool useSharedPolicies,
@@ -208,10 +208,10 @@ namespace Benchmarks
                     }
 
                     barrier.SignalAndWait();
-                    
+
                     int evaluationCount = 0;
                     var localEvaluationTime = TimeSpan.Zero;
-                    
+
                     while (!stopExecution)
                     {
                         // Use different policy for each iteration
@@ -226,23 +226,29 @@ namespace Benchmarks
                         {
                             // Measure only the evaluation call
                             var evalStopwatch = Stopwatch.StartNew();
-                            
+
                             if (useSharedPolicies)
                             {
                                 var result = compiledPolicies![policyIdx].EvalWithInput(input);
                             }
                             else
                             {
-                                // Compile policy in each iteration
-                                var modules = new[] { new PolicyModule { Id = "policy.rego", Content = policy } };
+                                // Compile policy in each iteration.
+                                var modules = new[] { new PolicyModule("policy.rego", policy) };
                                 var compiled = Compiler.CompilePolicyWithEntrypoint("{}", modules, "data.bench.allow");
-                                var result = compiled.EvalWithInput(input);
-                                compiled.Dispose();
+                                try
+                                {
+                                    var result = compiled.EvalWithInput(input);
+                                }
+                                finally
+                                {
+                                    DisposeCompiledPolicy(compiled);
+                                }
                             }
-                            
+
                             evalStopwatch.Stop();
                             localEvaluationTime += evalStopwatch.Elapsed;
-                            
+
                             // Track successful evaluations (only during actual benchmark, not warmup)
                             if (!isWarmup)
                             {
@@ -256,10 +262,10 @@ namespace Benchmarks
                         {
                             // Ignore evaluation errors for benchmarking purposes
                         }
-                        
+
                         evaluationCount++;
                     }
-                    
+
                     // Store the actual evaluation time for this thread
                     if (!isWarmup)
                     {
@@ -284,11 +290,23 @@ namespace Benchmarks
 
             var totalEvaluations = policyCounters.Values.Sum();
             var totalEvaluationTime = evaluationTimes.Values.Aggregate(TimeSpan.Zero, (sum, time) => sum + time);
-            
+
             // Use pure evaluation time (consistent with Rust benchmark)
             var evaluationTime = totalEvaluationTime == TimeSpan.Zero ? stopwatch.Elapsed : totalEvaluationTime;
-            
+
             return (totalEvaluations, evaluationTime, policyCounters, allocatedBytes);
         }
+
+        private static void DisposeCompiledPolicy(CompiledPolicy policy)
+        {
+            try
+            {
+                policy.Dispose();
+            }
+            catch (TimeoutException ex)
+            {
+                Console.WriteLine($"Warning: {ex.Message}");
+            }
+        }
     }
 }

bindings/csharp/Benchmarks/EngineEvaluationBenchmark.cs

@@ -12,7 +12,7 @@ namespace Benchmarks
     public class EngineEvaluationBenchmark
     {
         private static readonly string TestDataPath = Path.Combine(
-            Directory.GetCurrentDirectory(), 
+            Directory.GetCurrentDirectory(),
             "..", "..", "..",
             "benches", "evaluation", "test_data"
         );
@@ -33,7 +33,7 @@ namespace Benchmarks
         private static readonly string[] PolicyNames = new[]
         {
             "rbac_policy",
-            "api_access_policy", 
+            "api_access_policy",
             "data_sensitivity_policy",
             "time_based_policy",
             "data_processing_policy",
@@ -46,21 +46,21 @@ namespace Benchmarks
         private static List<(string Policy, string[] Inputs)> LoadPoliciesWithInputs()
         {
             var result = new List<(string Policy, string[] Inputs)>();
-            
+
             foreach (var (policyFile, inputFiles) in PolicyInputFiles)
             {
                 var policyPath = Path.Combine(TestDataPath, "policies", policyFile);
                 var policy = File.ReadAllText(policyPath);
-                
+
                 var inputs = inputFiles.Select(inputFile =>
                 {
                     var inputPath = Path.Combine(TestDataPath, "inputs", inputFile);
                     return File.ReadAllText(inputPath);
                 }).ToArray();
-                
+
                 result.Add((policy, inputs));
             }
-            
+
             return result;
         }
 
@@ -68,12 +68,12 @@ namespace Benchmarks
         {
             var policiesWithInputs = LoadPoliciesWithInputs();
             var engines = new List<Engine>();
-            
+
             foreach (var (policy, _) in policiesWithInputs)
             {
                 var engine = new Engine();
                 engine.AddPolicy("policy.rego", policy);
-                
+
                 // Warm up the engine to ensure it's fully prepared for evaluation
                 // This prevents each cloned engine from repeating preparation work
                 engine.SetInputJson("{}");
@@ -85,10 +85,10 @@ namespace Benchmarks
                 {
                     // Ignore warmup errors
                 }
-                
+
                 engines.Add(engine);
             }
-            
+
             return engines;
         }
 
@@ -97,13 +97,13 @@ namespace Benchmarks
             var cpuCount = Environment.ProcessorCount;
             var maxThreads = cpuCount * 2;
             var threadCounts = new List<int> { 1, 2 };
-            
+
             // Add even numbers from 4 to maxThreads
             for (int i = 4; i <= maxThreads; i += 2)
             {
                 threadCounts.Add(i);
             }
-            
+
             Console.WriteLine($"Running engine benchmark with max_threads: {maxThreads}");
             Console.WriteLine($"Testing with thread counts: {string.Join(", ", threadCounts)}");
             Console.WriteLine();
@@ -132,14 +132,14 @@ namespace Benchmarks
             const int warmupSeconds = 3;
             const int durationSeconds = 3;
             var policiesWithInputs = LoadPoliciesWithInputs();
-            
+
             Console.WriteLine($"Warming up with {threads} threads for {warmupSeconds} seconds...");
-            
+
             // Warmup phase
             var (_, _, _) = RunBenchmarkPhase(threads, warmupSeconds, policiesWithInputs, useClonedEngines, isWarmup: true);
-            
+
             Console.WriteLine($"Running benchmark with {threads} threads for {durationSeconds} seconds...");
-            
+
             // Actual benchmark phase
             var (totalEvaluations, evaluationTime, policyCounters) = RunBenchmarkPhase(threads, durationSeconds, policiesWithInputs, useClonedEngines, isWarmup: false);
 
@@ -165,8 +165,8 @@ namespace Benchmarks
         }
 
         private static (int totalEvaluations, TimeSpan evaluationTime, Dictionary<string, int> policyCounters) RunBenchmarkPhase(
-            int threads, 
-            int durationSeconds, 
+            int threads,
+            int durationSeconds,
             List<(string Policy, string[] Inputs)> policiesWithInputs,
             bool useClonedEngines,
             bool isWarmup)
@@ -199,10 +199,10 @@ namespace Benchmarks
                 tasks[threadId] = Task.Run(() =>
                 {
                     barrier.SignalAndWait();
-                    
+
                     int evaluationCount = 0;
                     var localEvaluationTime = TimeSpan.Zero;
-                    
+
                     while (!stopExecution)
                     {
                         // Use different policy for each iteration
@@ -217,7 +217,7 @@ namespace Benchmarks
                         {
                             // Measure only the engine operations
                             var evalStopwatch = Stopwatch.StartNew();
-                            
+
                             Engine engine;
                             if (useClonedEngines)
                             {
@@ -228,14 +228,14 @@ namespace Benchmarks
                                 engine = new Engine();
                                 engine.AddPolicy("policy.rego", policy);
                             }
-                            
+
                             engine.SetInputJson(input);
                             var result = engine.EvalRule("data.bench.allow");
                             engine.Dispose();
-                            
+
                             evalStopwatch.Stop();
                             localEvaluationTime += evalStopwatch.Elapsed;
-                            
+
                             // Track successful evaluations (only during actual benchmark, not warmup)
                             if (!isWarmup)
                             {
@@ -249,10 +249,10 @@ namespace Benchmarks
                         {
                             // Ignore evaluation errors for benchmarking purposes
                         }
-                        
+
                         evaluationCount++;
                     }
-                    
+
                     // Store the actual evaluation time for this thread
                     if (!isWarmup)
                     {
@@ -283,10 +283,10 @@ namespace Benchmarks
 
             var totalEvaluations = policyCounters.Values.Sum();
             var totalEvaluationTime = evaluationTimes.Values.Aggregate(TimeSpan.Zero, (sum, time) => sum + time);
-            
+
             // Use pure evaluation time (consistent with Rust benchmark)
             var evaluationTime = totalEvaluationTime == TimeSpan.Zero ? stopwatch.Elapsed : totalEvaluationTime;
-            
+
             return (totalEvaluations, evaluationTime, policyCounters);
         }
     }

bindings/csharp/Benchmarks/Program.cs

@@ -7,7 +7,7 @@ namespace Benchmarks
         static void Main(string[] args)
         {
             Console.WriteLine("=== Regorus C# Benchmarks ===\n");
-            
+
             try
             {
                 Console.WriteLine("Running Engine Evaluation Benchmark...");
@@ -17,9 +17,9 @@ namespace Benchmarks
             {
                 Console.WriteLine($"Engine benchmark failed: {ex.Message}");
             }
-            
+
             Console.WriteLine("\n" + new string('=', 80) + "\n");
-            
+
             try
             {
                 Console.WriteLine("Running Compiled Policy Evaluation Benchmark...");
@@ -29,7 +29,7 @@ namespace Benchmarks
             {
                 Console.WriteLine($"Compiled policy benchmark failed: {ex.Message}");
             }
-            
+
             Console.WriteLine("\n=== Benchmarks Complete ===");
         }
     }

bindings/csharp/Directory.Packages.props

@@ -1,7 +1,7 @@
 <Project>
   <PropertyGroup>
     <ManagePackageVersionsCentrally>true</ManagePackageVersionsCentrally>
-    <RegorusPackageVersion>0.9.0</RegorusPackageVersion>
+    <RegorusPackageVersion>0.9.1</RegorusPackageVersion>
     <RegorusPackageVersionSuffix Condition="'$(VersionSuffix)' != ''">-$(VersionSuffix)</RegorusPackageVersionSuffix>
   </PropertyGroup>
 

bindings/csharp/Regorus.Tests/MemoryGrowthTests.cs

@@ -0,0 +1,320 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Diagnostics;
+using Microsoft.VisualStudio.TestTools.UnitTesting;
+using Regorus;
+
+namespace Regorus.Tests;
+
+[TestClass]
+[DoNotParallelize]
+public class MemoryGrowthTests
+{
+    private static int Iterations =>
+        int.TryParse(Environment.GetEnvironmentVariable("REGORUS_MEMORY_TEST_ITERS"), out var value) ? value : 50_000;
+
+    private static int LogEvery =>
+        int.TryParse(Environment.GetEnvironmentVariable("REGORUS_MEMORY_TEST_LOG_EVERY"), out var value) ? value : 500;
+
+    private static int GcEvery
+    {
+        get
+        {
+            if (!int.TryParse(Environment.GetEnvironmentVariable("REGORUS_MEMORY_TEST_GC_EVERY"), out var value))
+            {
+                value = LogEvery;
+            }
+
+            return value <= 0 ? LogEvery : value;
+        }
+    }
+
+    private static long? MaxWorkingSetDeltaBytes
+    {
+        get
+        {
+            if (!long.TryParse(Environment.GetEnvironmentVariable("REGORUS_MEMORY_TEST_MAX_DELTA_MB"), out var mb))
+            {
+                mb = 32;
+            }
+
+            if (mb <= 0)
+            {
+                return null;
+            }
+
+            return mb * 1024L * 1024L;
+        }
+    }
+
+    private static ulong? GlobalRegorusMemoryLimitBytes
+    {
+        get
+        {
+            if (!ulong.TryParse(Environment.GetEnvironmentVariable("REGORUS_MEMORY_TEST_GLOBAL_REGORUS_LIMIT_MB"), out var mb))
+            {
+                return null;
+            }
+
+            if (mb == 0)
+            {
+                return null;
+            }
+
+            return mb * 1024UL * 1024UL;
+        }
+    }
+
+    private static void WithOptionalGlobalRegorusMemoryLimit(Action action)
+    {
+        var priorLimit = MemoryLimits.GetGlobalMemoryLimit();
+        try
+        {
+            if (GlobalRegorusMemoryLimitBytes is { } limit)
+            {
+                MemoryLimits.SetGlobalMemoryLimit(limit);
+            }
+
+            action();
+        }
+        finally
+        {
+            MemoryLimits.SetGlobalMemoryLimit(priorLimit);
+        }
+    }
+
+    private static void ForceFullGc()
+    {
+        GC.Collect();
+        GC.WaitForPendingFinalizers();
+        GC.Collect();
+    }
+
+
+    [TestMethod]
+    public void Engine_create_eval_dispose_does_not_grow_working_set()
+    {
+        WithOptionalGlobalRegorusMemoryLimit(() =>
+        {
+            var process = Process.GetCurrentProcess();
+            process.Refresh();
+            var baseline = process.WorkingSet64;
+            var maxDelta = 0L;
+            var baselineManaged = GC.GetTotalMemory(false);
+            var maxManagedDelta = 0L;
+
+            for (var i = 1; i <= Iterations; i++)
+            {
+                using (var engine = new Engine())
+                {
+                    engine.AddPolicy("test.rego", "package test\nx = 1\nmessage = `Hello`");
+                    _ = engine.EvalRule("data.test.message");
+                }
+
+                if (i % LogEvery == 0)
+                {
+                    process.Refresh();
+                    var workingSet = process.WorkingSet64;
+                    var managed = GC.GetTotalMemory(false);
+                    var delta = workingSet - baseline;
+                    var managedDelta = managed - baselineManaged;
+                    if (delta > maxDelta)
+                    {
+                        maxDelta = delta;
+                    }
+                    if (managedDelta > maxManagedDelta)
+                    {
+                        maxManagedDelta = managedDelta;
+                    }
+                    Console.WriteLine($"\n\n\u001b[1m{i} ws_mb={workingSet / 1048576.0:F1} managed_mb={managed / 1048576.0:F1} delta_mb={delta / 1048576.0:F1}\u001b[0m\n\n");
+                }
+            }
+
+            if (MaxWorkingSetDeltaBytes is { } limit)
+            {
+                Console.WriteLine($"\n\n\u001b[1mSUMMARY: max ws delta {maxDelta / 1048576.0:F1} MB (limit {limit / 1048576.0:F1} MB); max managed delta {maxManagedDelta / 1048576.0:F1} MB.\u001b[0m\n\n");
+                Assert.IsTrue(
+                    maxDelta <= limit,
+                    $"Working set grew by {maxDelta / 1048576.0:F1} MB (limit {limit / 1048576.0:F1} MB). Managed heap max delta {maxManagedDelta / 1048576.0:F1} MB.");
+            }
+        });
+    }
+
+    [TestMethod]
+    public void Engine_create_eval_finalize_does_not_grow_working_set()
+    {
+        WithOptionalGlobalRegorusMemoryLimit(() =>
+        {
+            var process = Process.GetCurrentProcess();
+            process.Refresh();
+            var baseline = process.WorkingSet64;
+            var maxDelta = 0L;
+            var baselineManaged = GC.GetTotalMemory(false);
+            var maxManagedDelta = 0L;
+
+            for (var i = 1; i <= Iterations; i++)
+            {
+                var engine = new Engine();
+                engine.AddPolicy("test.rego", "package test\nx = 1\nmessage = `Hello`");
+                _ = engine.EvalRule("data.test.message");
+
+                if (i % GcEvery == 0)
+                {
+                    ForceFullGc();
+                }
+
+                if (i % LogEvery == 0)
+                {
+                    process.Refresh();
+                    var workingSet = process.WorkingSet64;
+                    var managed = GC.GetTotalMemory(false);
+                    var delta = workingSet - baseline;
+                    var managedDelta = managed - baselineManaged;
+                    if (delta > maxDelta)
+                    {
+                        maxDelta = delta;
+                    }
+                    if (managedDelta > maxManagedDelta)
+                    {
+                        maxManagedDelta = managedDelta;
+                    }
+                    Console.WriteLine($"\n\n\u001b[1m{i} ws_mb={workingSet / 1048576.0:F1} managed_mb={managed / 1048576.0:F1} delta_mb={delta / 1048576.0:F1}\u001b[0m\n\n");
+                }
+            }
+
+            if (MaxWorkingSetDeltaBytes is { } limit)
+            {
+                Console.WriteLine($"\n\n\u001b[1mSUMMARY: max ws delta {maxDelta / 1048576.0:F1} MB (limit {limit / 1048576.0:F1} MB); max managed delta {maxManagedDelta / 1048576.0:F1} MB.\u001b[0m\n\n");
+                Assert.IsTrue(
+                    maxDelta <= limit,
+                    $"Working set grew by {maxDelta / 1048576.0:F1} MB (limit {limit / 1048576.0:F1} MB). Managed heap max delta {maxManagedDelta / 1048576.0:F1} MB.");
+            }
+        });
+    }
+
+
+    [TestMethod]
+    public void Rvm_rehydrate_execute_dispose_does_not_grow_working_set()
+    {
+        WithOptionalGlobalRegorusMemoryLimit(() =>
+        {
+            var modules = new[]
+            {
+                new PolicyModule("test.rego", "package test\nallow = true"),
+            };
+
+            using var compiled = Program.CompileFromModules("{}", modules, new[] { "data.test.allow" });
+            var serialized = compiled.SerializeBinary();
+
+            var process = Process.GetCurrentProcess();
+            process.Refresh();
+            var baseline = process.WorkingSet64;
+            var maxDelta = 0L;
+            var baselineManaged = GC.GetTotalMemory(false);
+            var maxManagedDelta = 0L;
+
+            for (var i = 1; i <= Iterations; i++)
+            {
+                using (var vm = new Rvm())
+                using (var program = Program.DeserializeBinary(serialized, out _))
+                {
+                    vm.LoadProgram(program);
+                    vm.SetDataJson("{}");
+                    vm.SetInputJson("{}");
+                    _ = vm.ExecuteEntryPoint(0);
+                }
+
+                if (i % LogEvery == 0)
+                {
+                    process.Refresh();
+                    var workingSet = process.WorkingSet64;
+                    var managed = GC.GetTotalMemory(false);
+                    var delta = workingSet - baseline;
+                    var managedDelta = managed - baselineManaged;
+                    if (delta > maxDelta)
+                    {
+                        maxDelta = delta;
+                    }
+                    if (managedDelta > maxManagedDelta)
+                    {
+                        maxManagedDelta = managedDelta;
+                    }
+                    Console.WriteLine($"\n\n\u001b[1m{i} ws_mb={workingSet / 1048576.0:F1} managed_mb={managed / 1048576.0:F1} delta_mb={delta / 1048576.0:F1}\u001b[0m\n\n");
+                }
+            }
+
+            if (MaxWorkingSetDeltaBytes is { } limit)
+            {
+                Console.WriteLine($"\n\n\u001b[1mSUMMARY: max ws delta {maxDelta / 1048576.0:F1} MB (limit {limit / 1048576.0:F1} MB); max managed delta {maxManagedDelta / 1048576.0:F1} MB.\u001b[0m\n\n");
+                Assert.IsTrue(
+                    maxDelta <= limit,
+                    $"Working set grew by {maxDelta / 1048576.0:F1} MB (limit {limit / 1048576.0:F1} MB). Managed heap max delta {maxManagedDelta / 1048576.0:F1} MB.");
+            }
+        });
+    }
+
+    [TestMethod]
+    public void Rvm_rehydrate_execute_finalize_does_not_grow_working_set()
+    {
+        WithOptionalGlobalRegorusMemoryLimit(() =>
+        {
+            var modules = new[]
+            {
+                new PolicyModule("test.rego", "package test\nallow = true"),
+            };
+
+            using var compiled = Program.CompileFromModules("{}", modules, new[] { "data.test.allow" });
+            var serialized = compiled.SerializeBinary();
+
+            var process = Process.GetCurrentProcess();
+            process.Refresh();
+            var baseline = process.WorkingSet64;
+            var maxDelta = 0L;
+            var baselineManaged = GC.GetTotalMemory(false);
+            var maxManagedDelta = 0L;
+
+            for (var i = 1; i <= Iterations; i++)
+            {
+                var vm = new Rvm();
+                var program = Program.DeserializeBinary(serialized, out _);
+                vm.LoadProgram(program);
+                vm.SetDataJson("{}");
+                vm.SetInputJson("{}");
+                _ = vm.ExecuteEntryPoint(0);
+
+                if (i % GcEvery == 0)
+                {
+                    ForceFullGc();
+                }
+
+                if (i % LogEvery == 0)
+                {
+                    process.Refresh();
+                    var workingSet = process.WorkingSet64;
+                    var managed = GC.GetTotalMemory(false);
+                    var delta = workingSet - baseline;
+                    var managedDelta = managed - baselineManaged;
+                    if (delta > maxDelta)
+                    {
+                        maxDelta = delta;
+                    }
+                    if (managedDelta > maxManagedDelta)
+                    {
+                        maxManagedDelta = managedDelta;
+                    }
+                    Console.WriteLine($"\n\n\u001b[1m{i} ws_mb={workingSet / 1048576.0:F1} managed_mb={managed / 1048576.0:F1} delta_mb={delta / 1048576.0:F1}\u001b[0m\n\n");
+                }
+            }
+
+            if (MaxWorkingSetDeltaBytes is { } limit)
+            {
+                Console.WriteLine($"\n\n\u001b[1mSUMMARY: max ws delta {maxDelta / 1048576.0:F1} MB (limit {limit / 1048576.0:F1} MB); max managed delta {maxManagedDelta / 1048576.0:F1} MB.\u001b[0m\n\n");
+                Assert.IsTrue(
+                    maxDelta <= limit,
+                    $"Working set grew by {maxDelta / 1048576.0:F1} MB (limit {limit / 1048576.0:F1} MB). Managed heap max delta {maxManagedDelta / 1048576.0:F1} MB.");
+            }
+        });
+    }
+}

bindings/csharp/Regorus.Tests/RegorusTests.cs

@@ -193,10 +193,19 @@ public class RegorusTests
 
         var result = engine.GetPolicyPackageNames();
 
-        var packageNames = JsonNode.Parse(result!);
+        Assert.IsNotNull(result);
 
-        Assert.AreEqual("test", packageNames![0]["package_name"].ToString());
-        Assert.AreEqual("test.nested.name", packageNames![1]["package_name"].ToString());
+        var packageNames = JsonNode.Parse(result);
+        Assert.IsNotNull(packageNames);
+
+        var packageArray = packageNames.AsArray();
+        var firstPackage = packageArray[0]?.AsObject();
+        var secondPackage = packageArray[1]?.AsObject();
+
+        Assert.IsNotNull(firstPackage);
+        Assert.IsNotNull(secondPackage);
+        Assert.AreEqual("test", firstPackage!["package_name"]!.GetValue<string>());
+        Assert.AreEqual("test.nested.name", secondPackage!["package_name"]!.GetValue<string>());
     }
 
     [TestMethod]
@@ -209,71 +218,84 @@ public class RegorusTests
 
         var result = engine.GetPolicyParameters();
 
-        var parameters = JsonNode.Parse(result!);
+        Assert.IsNotNull(result);
 
-        Assert.AreEqual(1, parameters![0]["parameters"].AsArray().Count);
-        Assert.AreEqual(1, parameters![0]["modifiers"].AsArray().Count);
+        var parameters = JsonNode.Parse(result);
+        Assert.IsNotNull(parameters);
 
-        Assert.AreEqual("a", parameters![0]["parameters"][0]["name"].ToString());
-        Assert.AreEqual("b", parameters![0]["modifiers"][0]["name"].ToString());
+        var parametersArray = parameters.AsArray();
+        var firstEntry = parametersArray[0]?.AsObject();
+        Assert.IsNotNull(firstEntry);
+
+        var parameterList = firstEntry!["parameters"]!.AsArray();
+        var modifierList = firstEntry["modifiers"]!.AsArray();
+
+        Assert.AreEqual(1, parameterList.Count);
+        Assert.AreEqual(1, modifierList.Count);
+
+        var parameterName = parameterList[0]?.AsObject()?["name"]?.GetValue<string>();
+        var modifierName = modifierList[0]?.AsObject()?["name"]?.GetValue<string>();
+
+        Assert.AreEqual("a", parameterName);
+        Assert.AreEqual("b", modifierName);
     }
 
-      [TestMethod]
-      public void Global_memory_limit_can_be_set_and_cleared()
-      {
+    [TestMethod]
+    public void Global_memory_limit_can_be_set_and_cleared()
+    {
         lock (LimitLock)
         {
-          using var guard = new MemoryLimitScope();
+            using var guard = new MemoryLimitScope();
 
-          MemoryLimits.SetGlobalMemoryLimit(null);
-          Assert.IsNull(MemoryLimits.GetGlobalMemoryLimit());
-
-          const ulong limit = 32 * 1024;
-          MemoryLimits.SetGlobalMemoryLimit(limit);
-          Assert.AreEqual(limit, MemoryLimits.GetGlobalMemoryLimit());
-
-          MemoryLimits.SetGlobalMemoryLimit(null);
-          Assert.IsNull(MemoryLimits.GetGlobalMemoryLimit());
-        }
-      }
-
-      [TestMethod]
-      public void Memory_limit_violations_surface_from_engine_calls()
-      {
-        lock (LimitLock)
-        {
-          using var guard = new MemoryLimitScope();
-          using var engine = new Engine();
-
-          const ulong limit = 1;
-          var payload = new string('x', 128 * 1024);
-
-          MemoryLimits.FlushThreadMemoryCounters();
-          MemoryLimits.SetGlobalMemoryLimit(limit);
-
-          try
-          {
-            var ex = Assert.ThrowsException<InvalidOperationException>(
-              () => engine.SetInputJson($"{{\"payload\":\"{payload}\"}}"));
-            StringAssert.Contains(ex.Message, "execution exceeded memory limit");
-          }
-          finally
-          {
             MemoryLimits.SetGlobalMemoryLimit(null);
-            MemoryLimits.FlushThreadMemoryCounters();
-          }
-        }
-      }
+            Assert.IsNull(MemoryLimits.GetGlobalMemoryLimit());
 
-      [TestMethod]
-      public void Evaluation_fails_when_input_pushes_policy_over_global_limit()
-      {
+            const ulong limit = 32 * 1024;
+            MemoryLimits.SetGlobalMemoryLimit(limit);
+            Assert.AreEqual(limit, MemoryLimits.GetGlobalMemoryLimit());
+
+            MemoryLimits.SetGlobalMemoryLimit(null);
+            Assert.IsNull(MemoryLimits.GetGlobalMemoryLimit());
+        }
+    }
+
+    [TestMethod]
+    public void Memory_limit_violations_surface_from_engine_calls()
+    {
         lock (LimitLock)
         {
-          using var guard = new MemoryLimitScope();
-          using var engine = new Engine();
+            using var guard = new MemoryLimitScope();
+            using var engine = new Engine();
 
-          const string policy = """
+            const ulong limit = 1;
+            var payload = new string('x', 128 * 1024);
+
+            MemoryLimits.FlushThreadMemoryCounters();
+            MemoryLimits.SetGlobalMemoryLimit(limit);
+
+            try
+            {
+                var ex = Assert.ThrowsException<InvalidOperationException>(
+                  () => engine.SetInputJson($"{{\"payload\":\"{payload}\"}}"));
+                StringAssert.Contains(ex.Message, "execution exceeded memory limit");
+            }
+            finally
+            {
+                MemoryLimits.SetGlobalMemoryLimit(null);
+                MemoryLimits.FlushThreadMemoryCounters();
+            }
+        }
+    }
+
+    [TestMethod]
+    public void Evaluation_fails_when_input_pushes_policy_over_global_limit()
+    {
+        lock (LimitLock)
+        {
+            using var guard = new MemoryLimitScope();
+            using var engine = new Engine();
+
+            const string policy = """
 package memorylimit
 
 import rego.v1
@@ -281,96 +303,152 @@ import rego.v1
 stretched := concat("", [input.block | numbers.range(0, input.repeat - 1)[_]])
 """;
 
-          engine.AddPolicy("memorylimit.rego", policy);
+            engine.AddPolicy("memorylimit.rego", policy);
 
-          MemoryLimits.FlushThreadMemoryCounters();
-          const ulong limit = 4 * 1024 * 1024;
-          MemoryLimits.SetGlobalMemoryLimit(limit);
+            MemoryLimits.FlushThreadMemoryCounters();
+            const ulong limit = 4 * 1024 * 1024;
+            MemoryLimits.SetGlobalMemoryLimit(limit);
 
-          var block = new string('x', 16 * 1024);
+            var block = new string('x', 16 * 1024);
 
-          var smallInput = JsonSerializer.Serialize(new { block, repeat = 16 });
-          engine.SetInputJson(smallInput);
-          var smallResult = engine.EvalRule("data.memorylimit.stretched");
-          Assert.IsNotNull(smallResult);
-          var stretched = JsonSerializer.Deserialize<string>(smallResult);
-          Assert.IsNotNull(stretched, "Policy should return a string result.");
-          Assert.AreEqual(block.Length * 16, stretched!.Length, "Policy should expand the payload under the limit.");
+            var smallInput = JsonSerializer.Serialize(new { block, repeat = 16 });
+            engine.SetInputJson(smallInput);
+            var smallResult = engine.EvalRule("data.memorylimit.stretched");
+            Assert.IsNotNull(smallResult);
+            var stretched = JsonSerializer.Deserialize<string>(smallResult);
+            Assert.IsNotNull(stretched, "Policy should return a string result.");
+            Assert.AreEqual(block.Length * 16, stretched!.Length, "Policy should expand the payload under the limit.");
 
-          var largeInput = JsonSerializer.Serialize(new { block, repeat = 4096 });
-          engine.SetInputJson(largeInput);
+            var largeInput = JsonSerializer.Serialize(new { block, repeat = 4096 });
+            engine.SetInputJson(largeInput);
 
-          var ex = Assert.ThrowsException<InvalidOperationException>(
-            () => engine.EvalRule("data.memorylimit.stretched"));
-          StringAssert.Contains(ex.Message, "execution exceeded memory limit");
+            var ex = Assert.ThrowsException<InvalidOperationException>(
+              () => engine.EvalRule("data.memorylimit.stretched"));
+            StringAssert.Contains(ex.Message, "execution exceeded memory limit");
         }
-      }
+    }
 
-      [TestMethod]
-      public void Thread_flush_threshold_roundtrips()
-      {
+    [TestMethod]
+    public void Thread_flush_threshold_roundtrips()
+    {
         lock (LimitLock)
         {
-          var original = MemoryLimits.GetThreadMemoryFlushThreshold();
-          try
-          {
-            const ulong threshold = 256 * 1024;
-            MemoryLimits.SetThreadFlushThresholdOverride(threshold);
-            Assert.AreEqual(threshold, MemoryLimits.GetThreadMemoryFlushThreshold());
-
-            MemoryLimits.SetThreadFlushThresholdOverride(null);
-            var restored = MemoryLimits.GetThreadMemoryFlushThreshold();
-            Assert.IsTrue(restored.HasValue, "Clearing override should restore allocator default.");
-            if (original.HasValue)
+            var original = MemoryLimits.GetThreadMemoryFlushThreshold();
+            try
             {
-              Assert.AreEqual(original, restored);
+                const ulong threshold = 256 * 1024;
+                MemoryLimits.SetThreadFlushThresholdOverride(threshold);
+                Assert.AreEqual(threshold, MemoryLimits.GetThreadMemoryFlushThreshold());
+
+                MemoryLimits.SetThreadFlushThresholdOverride(null);
+                var restored = MemoryLimits.GetThreadMemoryFlushThreshold();
+                Assert.IsTrue(restored.HasValue, "Clearing override should restore allocator default.");
+                if (original.HasValue)
+                {
+                    Assert.AreEqual(original, restored);
+                }
+            }
+            finally
+            {
+                MemoryLimits.SetThreadFlushThresholdOverride(original);
             }
-          }
-          finally
-          {
-            MemoryLimits.SetThreadFlushThresholdOverride(original);
-          }
         }
-      }
-
-  [TestMethod]
-  public void SetInputJson_has_negligible_allocations_after_warmup()
-  {
-    using var engine = new Engine();
-    const string payload = "{}";
-
-    // Warm up the engine and JIT to ensure subsequent measurements are representative.
-    for (int i = 0; i < 16; i++)
-    {
-      engine.SetInputJson(payload);
     }
 
-    GC.Collect();
-    GC.WaitForPendingFinalizers();
-    GC.Collect();
-
-    const int iterations = 256;
-    var before = GC.GetAllocatedBytesForCurrentThread();
-
-    for (int i = 0; i < iterations; i++)
+    [TestMethod]
+    public void SetInputJson_has_negligible_allocations_after_warmup()
     {
-      engine.SetInputJson(payload);
+        using var engine = new Engine();
+        const string payload = "{}";
+
+        // Warm up the engine and JIT to ensure subsequent measurements are representative.
+        for (int i = 0; i < 16; i++)
+        {
+            engine.SetInputJson(payload);
+        }
+
+        GC.Collect();
+        GC.WaitForPendingFinalizers();
+        GC.Collect();
+
+        const int iterations = 256;
+        var before = GC.GetAllocatedBytesForCurrentThread();
+
+        for (int i = 0; i < iterations; i++)
+        {
+            engine.SetInputJson(payload);
+        }
+
+        var after = GC.GetAllocatedBytesForCurrentThread();
+        var allocated = Math.Max(0, after - before);
+        var bytesPerOp = allocated / (double)iterations;
+
+        // Runtime bookkeeping (delegate caches, GC write barriers) differs across platforms, so
+        // we measure bytes per call rather than absolute totals and allow a small budget.
+        // CI will flag regressions where marshalling starts allocating per invocation.
+
+        // Allow a small budget for delegates and runtime bookkeeping while still flagging regressions.
+        Assert.IsTrue(
+          bytesPerOp <= 512,
+          $"Expected ≤512 B/op after warmup, but observed {bytesPerOp:F2} B/op (total {allocated} bytes)."
+        );
     }
 
-    var after = GC.GetAllocatedBytesForCurrentThread();
-  var allocated = Math.Max(0, after - before);
-  var bytesPerOp = allocated / (double)iterations;
+    [TestMethod]
+    public void Disposed_objects_throw_object_disposed_exception()
+    {
+        var engine = new Engine();
+        engine.Dispose();
+        Assert.ThrowsException<ObjectDisposedException>(() => engine.EvalRule("data.test.message"));
 
-  // Runtime bookkeeping (delegate caches, GC write barriers) differs across platforms, so
-  // we measure bytes per call rather than absolute totals and allow a small budget.
-  // CI will flag regressions where marshalling starts allocating per invocation.
+        var program = Program.CreateEmpty();
+        program.Dispose();
+        Assert.ThrowsException<ObjectDisposedException>(() => program.SerializeBinary());
 
-    // Allow a small budget for delegates and runtime bookkeeping while still flagging regressions.
-    Assert.IsTrue(
-      bytesPerOp <= 512,
-      $"Expected ≤512 B/op after warmup, but observed {bytesPerOp:F2} B/op (total {allocated} bytes)."
-    );
-  }
+        var rvm = new Rvm();
+        rvm.Dispose();
+        Assert.ThrowsException<ObjectDisposedException>(() => rvm.Execute());
+
+        var modules = new[] { new PolicyModule("test.rego", "package test\nallow = true") };
+        var compiled = Compiler.CompilePolicyWithEntrypoint("{}", modules, "data.test.allow");
+        compiled.Dispose();
+        Assert.ThrowsException<ObjectDisposedException>(() => compiled.EvalWithInput("{}"));
+    }
+
+    [TestMethod]
+    public void Registry_helpers_return_empty_after_clear()
+    {
+        TargetRegistry.Clear();
+        Assert.IsTrue(TargetRegistry.IsEmpty);
+        Assert.AreEqual(0, TargetRegistry.GetNames().Count);
+
+        SchemaRegistry.ClearResources();
+        SchemaRegistry.ClearEffects();
+        Assert.IsTrue(SchemaRegistry.IsResourceRegistryEmpty);
+        Assert.IsTrue(SchemaRegistry.IsEffectRegistryEmpty);
+        Assert.AreEqual(0, SchemaRegistry.GetResourceNames().Count);
+        Assert.AreEqual(0, SchemaRegistry.GetEffectNames().Count);
+    }
+
+    [TestMethod]
+    public void Utf8_marshalling_handles_large_unicode_payloads()
+    {
+        var payload = string.Concat(new string('ß', 2048), "-✓-", new string('漢', 1024));
+
+        using var engine = new Engine();
+        engine.AddPolicy("test.rego", "package test\nmessage = input.msg");
+        engine.SetInputJson(JsonSerializer.Serialize(new { msg = payload }));
+
+        var result = engine.EvalRule("data.test.message");
+
+        Assert.IsNotNull(result);
+
+        // Compare by parsing the JSON string to avoid encoder differences across platforms.
+        var parsed = JsonSerializer.Deserialize<string>(result);
+        Assert.IsNotNull(parsed);
+
+        Assert.AreEqual(payload, parsed);
+    }
 
     private sealed class MemoryLimitScope : IDisposable
     {

bindings/csharp/Regorus.Tests/RvmProgramTests.cs

@@ -96,9 +96,9 @@ allow if {
         Assert.AreEqual("true", result, "expected allow=true");
     }
 
-      [TestMethod]
-      public void Program_host_await_suspend_and_resume_succeeds()
-      {
+    [TestMethod]
+    public void Program_host_await_suspend_and_resume_succeeds()
+    {
         var modules = new[] { new PolicyModule("host_await.rego", HostAwaitPolicy) };
         var entryPoints = new[] { "data.demo.allow" };
 
@@ -115,5 +115,5 @@ allow if {
 
         var resumed = vm.Resume("{\"tier\":\"gold\"}");
         Assert.AreEqual("true", resumed, "expected allow=true after resume");
-      }
+    }
 }

bindings/csharp/Regorus/CompiledPolicy.cs

@@ -3,7 +3,6 @@
 
 using System;
 using System.Text.Json;
-using System.Threading;
 using Regorus.Internal;
 
 #nullable enable
@@ -18,20 +17,15 @@ namespace Regorus
     /// Each instance represents a unique native policy object.
     /// 
     /// Thread Safety: This class is thread-safe for all operations. Multiple threads
-    /// can safely call EvalWithInput() concurrently, and Dispose() will safely wait
-    /// for all active evaluations to complete before freeing resources. No external
-    /// synchronization is required.
+    /// can safely call EvalWithInput() concurrently. Dispose() blocks new calls, waits
+    /// briefly, and defers the native release to the last in-flight caller if needed.
+    /// No external synchronization is required.
     /// </summary>
-    public unsafe sealed class CompiledPolicy : IDisposable
+    public unsafe sealed class CompiledPolicy : SafeHandleWrapper
     {
-    private RegorusCompiledPolicyHandle? _handle;
-    private readonly ManualResetEventSlim _idleEvent = new(initialState: true);
-    private int _isDisposed;
-    private int _activeEvaluations;
-
         internal CompiledPolicy(RegorusCompiledPolicyHandle handle)
+            : base(handle, nameof(CompiledPolicy))
         {
-            _handle = handle ?? throw new ArgumentNullException(nameof(handle));
         }
 
         /// <summary>
@@ -45,36 +39,16 @@ namespace Regorus
         /// <exception cref="ObjectDisposedException">Thrown when the policy has been disposed</exception>
         public string? EvalWithInput(string inputJson)
         {
-            // Increment active evaluations count
-            var active = System.Threading.Interlocked.Increment(ref _activeEvaluations);
-            if (active == 1)
+            return Internal.Utf8Marshaller.WithUtf8(inputJson, inputPtr =>
             {
-                _idleEvent.Reset();
-            }
-            try
-            {
-                ThrowIfDisposed();
-
-                return Internal.Utf8Marshaller.WithUtf8(inputJson, inputPtr =>
+                return UseHandle(policyPtr =>
                 {
-                    return UseHandle(policyPtr =>
+                    unsafe
                     {
-                        unsafe
-                        {
-                            return CheckAndDropResult(Internal.API.regorus_compiled_policy_eval_with_input((Internal.RegorusCompiledPolicy*)policyPtr, (byte*)inputPtr));
-                        }
-                    });
+                        return CheckAndDropResult(Internal.API.regorus_compiled_policy_eval_with_input((Internal.RegorusCompiledPolicy*)policyPtr, (byte*)inputPtr));
+                    }
                 });
-            }
-            finally
-            {
-                // Decrement active evaluations count
-                var remaining = System.Threading.Interlocked.Decrement(ref _activeEvaluations);
-                if (remaining == 0)
-                {
-                    _idleEvent.Set();
-                }
-            }
+            });
         }
 
         /// <summary>
@@ -86,7 +60,6 @@ namespace Regorus
         /// <exception cref="ObjectDisposedException">Thrown when the policy has been disposed</exception>
         public PolicyInfo GetPolicyInfo()
         {
-            ThrowIfDisposed();
             var jsonResult = UseHandle(policyPtr =>
             {
                 unsafe
@@ -94,7 +67,7 @@ namespace Regorus
                     return CheckAndDropResult(Internal.API.regorus_compiled_policy_get_policy_info((Internal.RegorusCompiledPolicy*)policyPtr));
                 }
             });
-            
+
             if (string.IsNullOrEmpty(jsonResult))
             {
                 throw new Exception("Failed to get policy info: empty response");
@@ -106,8 +79,8 @@ namespace Regorus
                 {
                     PropertyNameCaseInsensitive = true
                 };
-                
-                return JsonSerializer.Deserialize<PolicyInfo>(jsonResult!, options) 
+
+                return JsonSerializer.Deserialize<PolicyInfo>(jsonResult!, options)
                     ?? throw new Exception("Failed to deserialize policy info");
             }
             catch (JsonException ex)
@@ -116,106 +89,9 @@ namespace Regorus
             }
         }
 
-        public void Dispose()
-        {
-            Dispose(disposing: true);
-            GC.SuppressFinalize(this);
-        }
-
-        private void Dispose(bool disposing)
-        {
-            if (System.Threading.Interlocked.CompareExchange(ref _isDisposed, 1, 0) == 0)
-            {
-                var handle = _handle;
-                if (handle != null)
-                {
-                    _idleEvent.Wait();
-                    
-                    handle.Dispose();
-                    _handle = null;
-                }
-
-                _idleEvent.Dispose();
-            }
-        }
-
-        private void ThrowIfDisposed()
-        {
-            if (_isDisposed != 0 || _handle is null || _handle.IsClosed)
-                throw new ObjectDisposedException(nameof(CompiledPolicy));
-        }
-
         private string? CheckAndDropResult(Internal.RegorusResult result)
         {
-            try
-            {
-                if (result.status != Internal.RegorusStatus.Ok)
-                {
-                    var message = Internal.Utf8Marshaller.FromUtf8(result.error_message);
-                    throw result.status.CreateException(message);
-                }
-
-                return result.data_type switch
-                {
-                    Internal.RegorusDataType.String => Internal.Utf8Marshaller.FromUtf8(result.output),
-                    Internal.RegorusDataType.Boolean => result.bool_value.ToString().ToLowerInvariant(),
-                    Internal.RegorusDataType.Integer => result.int_value.ToString(),
-                    Internal.RegorusDataType.None => null,
-                    _ => Internal.Utf8Marshaller.FromUtf8(result.output)
-                };
-            }
-            finally
-            {
-                Internal.API.regorus_result_drop(result);
-            }
-        }
-
-        private RegorusCompiledPolicyHandle GetHandleForUse()
-        {
-            var handle = _handle;
-            if (handle is null || handle.IsClosed || handle.IsInvalid)
-            {
-                throw new ObjectDisposedException(nameof(CompiledPolicy));
-            }
-            return handle;
-        }
-
-        internal T UseHandle<T>(Func<IntPtr, T> func)
-        {
-            var handle = GetHandleForUse();
-            bool addedRef = false;
-            try
-            {
-                handle.DangerousAddRef(ref addedRef);
-                var pointer = handle.DangerousGetHandle();
-                if (pointer == IntPtr.Zero)
-                {
-                    throw new ObjectDisposedException(nameof(CompiledPolicy));
-                }
-
-                return func(pointer);
-            }
-            finally
-            {
-                if (addedRef)
-                {
-                    handle.DangerousRelease();
-                }
-            }
-        }
-
-        internal T UseHandleForInterop<T>(Func<IntPtr, T> func)
-        {
-            return UseHandle(func);
-        }
-
-        private void UseHandle(Action<IntPtr> action)
-        {
-            UseHandle<object?>(handlePtr =>
-            {
-                action(handlePtr);
-                return null;
-            });
+            return Internal.ResultHelpers.GetStringResult(result);
         }
     }
 }

bindings/csharp/Regorus/Compiler.cs

@@ -12,17 +12,17 @@ namespace Regorus
     /// <summary>
     /// Represents a policy module with an ID and content.
     /// </summary>
-    public struct PolicyModule
+    public readonly struct PolicyModule
     {
         /// <summary>
-        /// Gets or sets the unique identifier for this policy module.
+        /// Gets the unique identifier for this policy module.
         /// </summary>
-        public string Id { get; set; }
+        public string Id { get; }
 
         /// <summary>
-        /// Gets or sets the Rego policy content.
+        /// Gets the Rego policy content.
         /// </summary>
-        public string Content { get; set; }
+        public string Content { get; }
 
         /// <summary>
         /// Initializes a new instance of the PolicyModule struct.
@@ -53,50 +53,40 @@ namespace Regorus
         /// <exception cref="Exception">Thrown when compilation fails</exception>
         public static CompiledPolicy CompilePolicyWithEntrypoint(string dataJson, IEnumerable<PolicyModule> modules, string entryPointRule)
         {
-            var modulesArray = modules.ToArray();
-
-            var nativeModules = new Internal.RegorusPolicyModule[modulesArray.Length];
-            var pinnedStrings = new List<Utf8Marshaller.PinnedUtf8>(modulesArray.Length * 2);
-
-            try
+            if (modules is null)
             {
-                for (int i = 0; i < modulesArray.Length; i++)
+                throw new ArgumentNullException(nameof(modules));
+            }
+
+            return CompilePolicyWithEntrypoint(dataJson, modules.ToArray(), entryPointRule);
+        }
+
+        /// <summary>
+        /// Compiles a policy from data and modules with a specific entry point rule.
+        /// </summary>
+        public static CompiledPolicy CompilePolicyWithEntrypoint(string dataJson, IReadOnlyList<PolicyModule> modules, string entryPointRule)
+        {
+            if (modules is null)
+            {
+                throw new ArgumentNullException(nameof(modules));
+            }
+
+            using var pinnedModules = Internal.ModuleMarshalling.PinPolicyModules(modules);
+
+            return Utf8Marshaller.WithUtf8(dataJson, dataPtr =>
+                Utf8Marshaller.WithUtf8(entryPointRule, entryPointPtr =>
                 {
-                    var idPinned = Utf8Marshaller.Pin(modulesArray[i].Id);
-                    var contentPinned = Utf8Marshaller.Pin(modulesArray[i].Content);
-                    pinnedStrings.Add(idPinned);
-                    pinnedStrings.Add(contentPinned);
-
-                    nativeModules[i] = new Internal.RegorusPolicyModule
+                    unsafe
                     {
-                        id = idPinned.Pointer,
-                        content = contentPinned.Pointer
-                    };
-                }
-
-                return Utf8Marshaller.WithUtf8(dataJson, dataPtr =>
-                    Utf8Marshaller.WithUtf8(entryPointRule, entryPointPtr =>
-                    {
-                        unsafe
+                        fixed (Internal.RegorusPolicyModule* modulesPtr = pinnedModules.Buffer)
                         {
-                            fixed (Internal.RegorusPolicyModule* modulesPtr = nativeModules)
-                            {
-                                var result = Internal.API.regorus_compile_policy_with_entrypoint(
-                                    (byte*)dataPtr, modulesPtr, (UIntPtr)modulesArray.Length, (byte*)entryPointPtr);
+                            var result = Internal.API.regorus_compile_policy_with_entrypoint(
+                                (byte*)dataPtr, modulesPtr, (UIntPtr)pinnedModules.Length, (byte*)entryPointPtr);
 
-                                var policy = GetCompiledPolicyResult(result);
-                                return policy;
-                            }
+                            return GetCompiledPolicyResult(result);
                         }
-                    }));
-            }
-            finally
-            {
-                foreach (var pinned in pinnedStrings)
-                {
-                    pinned.Dispose();
-                }
-            }
+                    }
+                }));
         }
 
         /// <summary>
@@ -110,49 +100,39 @@ namespace Regorus
         /// <exception cref="Exception">Thrown when compilation fails</exception>
         public static CompiledPolicy CompilePolicyForTarget(string dataJson, IEnumerable<PolicyModule> modules)
         {
-            var modulesArray = modules.ToArray();
-
-            var nativeModules = new Internal.RegorusPolicyModule[modulesArray.Length];
-            var pinnedStrings = new List<Utf8Marshaller.PinnedUtf8>(modulesArray.Length * 2);
-
-            try
+            if (modules is null)
             {
-                for (int i = 0; i < modulesArray.Length; i++)
+                throw new ArgumentNullException(nameof(modules));
+            }
+
+            return CompilePolicyForTarget(dataJson, modules.ToArray());
+        }
+
+        /// <summary>
+        /// Compiles a target-aware policy from data and modules.
+        /// </summary>
+        public static CompiledPolicy CompilePolicyForTarget(string dataJson, IReadOnlyList<PolicyModule> modules)
+        {
+            if (modules is null)
+            {
+                throw new ArgumentNullException(nameof(modules));
+            }
+
+            using var pinnedModules = Internal.ModuleMarshalling.PinPolicyModules(modules);
+
+            return Utf8Marshaller.WithUtf8(dataJson, dataPtr =>
+            {
+                unsafe
                 {
-                    var idPinned = Utf8Marshaller.Pin(modulesArray[i].Id);
-                    var contentPinned = Utf8Marshaller.Pin(modulesArray[i].Content);
-                    pinnedStrings.Add(idPinned);
-                    pinnedStrings.Add(contentPinned);
-
-                    nativeModules[i] = new Internal.RegorusPolicyModule
+                    fixed (Internal.RegorusPolicyModule* modulesPtr = pinnedModules.Buffer)
                     {
-                        id = idPinned.Pointer,
-                        content = contentPinned.Pointer
-                    };
-                }
+                        var result = Internal.API.regorus_compile_policy_for_target(
+                            (byte*)dataPtr, modulesPtr, (UIntPtr)pinnedModules.Length);
 
-                return Utf8Marshaller.WithUtf8(dataJson, dataPtr =>
-                {
-                    unsafe
-                    {
-                        fixed (Internal.RegorusPolicyModule* modulesPtr = nativeModules)
-                        {
-                            var result = Internal.API.regorus_compile_policy_for_target(
-                                (byte*)dataPtr, modulesPtr, (UIntPtr)modulesArray.Length);
-
-                            var policy = GetCompiledPolicyResult(result);
-                            return policy;
-                        }
+                        return GetCompiledPolicyResult(result);
                     }
-                });
-            }
-            finally
-            {
-                foreach (var pinned in pinnedStrings)
-                {
-                    pinned.Dispose();
                 }
-            }
+            });
         }
 
         private static CompiledPolicy GetCompiledPolicyResult(Internal.RegorusResult result)

bindings/csharp/Regorus/Engine.cs

@@ -16,14 +16,11 @@ namespace Regorus
     /// Cloning is cheap and involves only incrementing reference counts for shared immutable objects like parsed policies,
     /// data etc. Mutable state is deep copied as needed.
     /// </summary>
-    public unsafe sealed class Engine : IDisposable
+    public unsafe sealed class Engine : SafeHandleWrapper
     {
-        private RegorusEngineHandle? _handle;
-        private int _isDisposed;
-
         public Engine()
+            : base(RegorusEngineHandle.Create(), nameof(Engine))
         {
-            _handle = RegorusEngineHandle.Create();
         }
 
         public static void SetFallbackExecutionTimerConfig(ExecutionTimerConfig config)
@@ -37,42 +34,13 @@ namespace Regorus
             CheckAndDropResult(Regorus.Internal.API.regorus_clear_fallback_execution_timer_config());
         }
 
-        public void Dispose()
-        {
-            Dispose(disposing: true);
-
-            // This object will be cleaned up by the Dispose method.
-            // Therefore, call GC.SuppressFinalize to
-            // take this object off the finalization queue
-            // and prevent finalization code for this object
-            // from executing a second time.
-            GC.SuppressFinalize(this);
-        }
-
-        // Dispose(bool disposing) executes in two distinct scenarios.
-        // If disposing equals true, the method has been called directly
-        // or indirectly by a user's code. Managed and unmanaged resources
-        // can be disposed.
-        // If disposing equals false, the method has been called by the
-        // runtime from inside the finalizer and you should not reference
-        // other objects. Only unmanaged resources can be disposed.
-        void Dispose(bool disposing)
-        {
-            if (System.Threading.Interlocked.CompareExchange(ref _isDisposed, 1, 0) == 0)
-            {
-                _handle?.Dispose();
-                _handle = null;
-            }
-        }
-
         private Engine(RegorusEngineHandle handle)
+            : base(handle, nameof(Engine))
         {
-            _handle = handle ?? throw new ArgumentNullException(nameof(handle));
         }
 
         public Engine Clone()
         {
-            ThrowIfDisposed();
             return UseHandle(enginePtr =>
             {
                 unsafe
@@ -91,402 +59,198 @@ namespace Regorus
 
         public void SetStrictBuiltinErrors(bool strict)
         {
-            ThrowIfDisposed();
             UseHandle(enginePtr =>
             {
-                unsafe
-                {
-                    CheckAndDropResult(Regorus.Internal.API.regorus_engine_set_strict_builtin_errors((Regorus.Internal.RegorusEngine*)enginePtr, strict));
-                }
+                CheckAndDropResult(Regorus.Internal.API.regorus_engine_set_strict_builtin_errors((Regorus.Internal.RegorusEngine*)enginePtr, strict));
             });
         }
 
         public void SetExecutionTimerConfig(ExecutionTimerConfig config)
         {
-            ThrowIfDisposed();
             var nativeConfig = config.ToNative();
             UseHandle(enginePtr =>
             {
-                unsafe
-                {
-                    var localConfig = nativeConfig;
-                    CheckAndDropResult(Regorus.Internal.API.regorus_engine_set_execution_timer_config((Regorus.Internal.RegorusEngine*)enginePtr, &localConfig));
-                }
+                var localConfig = nativeConfig;
+                CheckAndDropResult(Regorus.Internal.API.regorus_engine_set_execution_timer_config((Regorus.Internal.RegorusEngine*)enginePtr, &localConfig));
             });
         }
 
         public void ClearExecutionTimerConfig()
         {
-            ThrowIfDisposed();
             UseHandle(enginePtr =>
             {
-                unsafe
-                {
-                    CheckAndDropResult(Regorus.Internal.API.regorus_engine_clear_execution_timer_config((Regorus.Internal.RegorusEngine*)enginePtr));
-                }
+                CheckAndDropResult(Regorus.Internal.API.regorus_engine_clear_execution_timer_config((Regorus.Internal.RegorusEngine*)enginePtr));
             });
         }
         public string? AddPolicy(string path, string rego)
         {
-            ThrowIfDisposed();
             return Utf8Marshaller.WithUtf8(path, pathPtr =>
                 Utf8Marshaller.WithUtf8(rego, regoPtr =>
-                {
-                    unsafe
-                    {
-                        return UseHandle(enginePtr =>
-                        {
-                            unsafe
-                            {
-                                return CheckAndDropResult(Regorus.Internal.API.regorus_engine_add_policy((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)pathPtr, (byte*)regoPtr));
-                            }
-                        });
-                    }
-                }));
+                    UseHandle(enginePtr =>
+                        CheckAndDropResult(Regorus.Internal.API.regorus_engine_add_policy((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)pathPtr, (byte*)regoPtr))
+                    )));
         }
 
         public void SetRegoV0(bool enable)
         {
-            ThrowIfDisposed();
             UseHandle(enginePtr =>
             {
-                unsafe
-                {
-                    CheckAndDropResult(Regorus.Internal.API.regorus_engine_set_rego_v0((Regorus.Internal.RegorusEngine*)enginePtr, enable));
-                }
+                CheckAndDropResult(Regorus.Internal.API.regorus_engine_set_rego_v0((Regorus.Internal.RegorusEngine*)enginePtr, enable));
             });
         }
 
         public string? AddPolicyFromFile(string path)
         {
-            ThrowIfDisposed();
             return Utf8Marshaller.WithUtf8(path, pathPtr =>
             {
-                unsafe
-                {
-                    return UseHandle(enginePtr =>
-                    {
-                        unsafe
-                        {
-                            return CheckAndDropResult(Regorus.Internal.API.regorus_engine_add_policy_from_file((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)pathPtr));
-                        }
-                    });
-                }
+                return UseHandle(enginePtr =>
+                    CheckAndDropResult(Regorus.Internal.API.regorus_engine_add_policy_from_file((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)pathPtr))
+                );
             });
 
         }
 
         public void AddDataJson(string data)
         {
-            ThrowIfDisposed();
             Utf8Marshaller.WithUtf8(data, dataPtr =>
             {
-                unsafe
+                UseHandle(enginePtr =>
                 {
-                    UseHandle(enginePtr =>
-                    {
-                        unsafe
-                        {
-                            CheckAndDropResult(Regorus.Internal.API.regorus_engine_add_data_json((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)dataPtr));
-                        }
-                    });
-                }
+                    CheckAndDropResult(Regorus.Internal.API.regorus_engine_add_data_json((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)dataPtr));
+                });
             });
 
         }
 
         public void AddDataFromJsonFile(string path)
         {
-            ThrowIfDisposed();
             Utf8Marshaller.WithUtf8(path, pathPtr =>
             {
-                unsafe
+                UseHandle(enginePtr =>
                 {
-                    UseHandle(enginePtr =>
-                    {
-                        unsafe
-                        {
-                            CheckAndDropResult(Regorus.Internal.API.regorus_engine_add_data_from_json_file((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)pathPtr));
-                        }
-                    });
-                }
+                    CheckAndDropResult(Regorus.Internal.API.regorus_engine_add_data_from_json_file((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)pathPtr));
+                });
             });
 
         }
 
         public void SetInputJson(string input)
         {
-            ThrowIfDisposed();
             Utf8Marshaller.WithUtf8(input, inputPtr =>
             {
-                unsafe
+                UseHandle(enginePtr =>
                 {
-                    UseHandle(enginePtr =>
-                    {
-                        unsafe
-                        {
-                            CheckAndDropResult(Regorus.Internal.API.regorus_engine_set_input_json((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)inputPtr));
-                        }
-                    });
-                }
+                    CheckAndDropResult(Regorus.Internal.API.regorus_engine_set_input_json((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)inputPtr));
+                });
             });
         }
 
         public void SetInputFromJsonFile(string path)
         {
-            ThrowIfDisposed();
             Utf8Marshaller.WithUtf8(path, pathPtr =>
             {
-                unsafe
+                UseHandle(enginePtr =>
                 {
-                    UseHandle(enginePtr =>
-                    {
-                        unsafe
-                        {
-                            CheckAndDropResult(Regorus.Internal.API.regorus_engine_set_input_from_json_file((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)pathPtr));
-                        }
-                    });
-                }
+                    CheckAndDropResult(Regorus.Internal.API.regorus_engine_set_input_from_json_file((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)pathPtr));
+                });
             });
         }
 
         public string? EvalQuery(string query)
         {
-            ThrowIfDisposed();
             return Utf8Marshaller.WithUtf8(query, queryPtr =>
             {
-                unsafe
-                {
-                    return UseHandle(enginePtr =>
-                    {
-                        unsafe
-                        {
-                            return CheckAndDropResult(Regorus.Internal.API.regorus_engine_eval_query((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)queryPtr));
-                        }
-                    });
-                }
+                return UseHandle(enginePtr =>
+                    CheckAndDropResult(Regorus.Internal.API.regorus_engine_eval_query((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)queryPtr))
+                );
             });
         }
 
         public string? EvalRule(string rule)
         {
-            ThrowIfDisposed();
             return Utf8Marshaller.WithUtf8(rule, rulePtr =>
             {
-                unsafe
-                {
-                    return UseHandle(enginePtr =>
-                    {
-                        unsafe
-                        {
-                            return CheckAndDropResult(Regorus.Internal.API.regorus_engine_eval_rule((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)rulePtr));
-                        }
-                    });
-                }
+                return UseHandle(enginePtr =>
+                    CheckAndDropResult(Regorus.Internal.API.regorus_engine_eval_rule((Regorus.Internal.RegorusEngine*)enginePtr, (byte*)rulePtr))
+                );
             });
         }
 
         public void SetEnableCoverage(bool enable)
         {
-            ThrowIfDisposed();
             UseHandle(enginePtr =>
             {
-                unsafe
-                {
-                    CheckAndDropResult(Regorus.Internal.API.regorus_engine_set_enable_coverage((Regorus.Internal.RegorusEngine*)enginePtr, enable));
-                }
+                CheckAndDropResult(Regorus.Internal.API.regorus_engine_set_enable_coverage((Regorus.Internal.RegorusEngine*)enginePtr, enable));
             });
         }
 
         public void ClearCoverageData()
         {
-            ThrowIfDisposed();
             UseHandle(enginePtr =>
             {
-                unsafe
-                {
-                    CheckAndDropResult(Regorus.Internal.API.regorus_engine_clear_coverage_data((Regorus.Internal.RegorusEngine*)enginePtr));
-                }
+                CheckAndDropResult(Regorus.Internal.API.regorus_engine_clear_coverage_data((Regorus.Internal.RegorusEngine*)enginePtr));
             });
         }
 
         public string? GetCoverageReport()
         {
-            ThrowIfDisposed();
             return UseHandle(enginePtr =>
             {
-                unsafe
-                {
-                    return CheckAndDropResult(Regorus.Internal.API.regorus_engine_get_coverage_report((Regorus.Internal.RegorusEngine*)enginePtr));
-                }
+                return CheckAndDropResult(Regorus.Internal.API.regorus_engine_get_coverage_report((Regorus.Internal.RegorusEngine*)enginePtr));
             });
         }
 
         public string? GetCoverageReportPretty()
         {
-            ThrowIfDisposed();
             return UseHandle(enginePtr =>
             {
-                unsafe
-                {
-                    return CheckAndDropResult(Regorus.Internal.API.regorus_engine_get_coverage_report_pretty((Regorus.Internal.RegorusEngine*)enginePtr));
-                }
+                return CheckAndDropResult(Regorus.Internal.API.regorus_engine_get_coverage_report_pretty((Regorus.Internal.RegorusEngine*)enginePtr));
             });
         }
 
         public void SetGatherPrints(bool enable)
         {
-            ThrowIfDisposed();
             UseHandle(enginePtr =>
             {
-                unsafe
-                {
-                    CheckAndDropResult(Regorus.Internal.API.regorus_engine_set_gather_prints((Regorus.Internal.RegorusEngine*)enginePtr, enable));
-                }
+                CheckAndDropResult(Regorus.Internal.API.regorus_engine_set_gather_prints((Regorus.Internal.RegorusEngine*)enginePtr, enable));
             });
         }
 
         public string? TakePrints()
         {
-            ThrowIfDisposed();
             return UseHandle(enginePtr =>
             {
-                unsafe
-                {
-                    return CheckAndDropResult(Regorus.Internal.API.regorus_engine_take_prints((Regorus.Internal.RegorusEngine*)enginePtr));
-                }
+                return CheckAndDropResult(Regorus.Internal.API.regorus_engine_take_prints((Regorus.Internal.RegorusEngine*)enginePtr));
             });
         }
 
         public string? GetAstAsJson()
         {
-            ThrowIfDisposed();
             return UseHandle(enginePtr =>
             {
-                unsafe
-                {
-                    return CheckAndDropResult(Regorus.Internal.API.regorus_engine_get_ast_as_json((Regorus.Internal.RegorusEngine*)enginePtr));
-                }
+                return CheckAndDropResult(Regorus.Internal.API.regorus_engine_get_ast_as_json((Regorus.Internal.RegorusEngine*)enginePtr));
             });
         }
 
         public string? GetPolicyPackageNames()
         {
-            ThrowIfDisposed();
             return UseHandle(enginePtr =>
             {
-                unsafe
-                {
-                    return CheckAndDropResult(Regorus.Internal.API.regorus_engine_get_policy_package_names((Regorus.Internal.RegorusEngine*)enginePtr));
-                }
+                return CheckAndDropResult(Regorus.Internal.API.regorus_engine_get_policy_package_names((Regorus.Internal.RegorusEngine*)enginePtr));
             });
         }
 
         public string? GetPolicyParameters()
         {
-            ThrowIfDisposed();
             return UseHandle(enginePtr =>
             {
-                unsafe
-                {
-                    return CheckAndDropResult(Regorus.Internal.API.regorus_engine_get_policy_parameters((Regorus.Internal.RegorusEngine*)enginePtr));
-                }
+                return CheckAndDropResult(Regorus.Internal.API.regorus_engine_get_policy_parameters((Regorus.Internal.RegorusEngine*)enginePtr));
             });
         }
 
-    private static string? StringFromUtf8(IntPtr ptr)
+        private static string? CheckAndDropResult(Regorus.Internal.RegorusResult result)
         {
-
-#if NETSTANDARD2_1
-			return Marshal.PtrToStringUTF8(ptr);
-#else
-            int len = 0;
-            while (Marshal.ReadByte(ptr, len) != 0) { ++len; }
-            byte[] buffer = new byte[len];
-            Marshal.Copy(ptr, buffer, 0, buffer.Length);
-            return Encoding.UTF8.GetString(buffer);
-#endif
-        }
-
-    private static string? CheckAndDropResult(Regorus.Internal.RegorusResult result)
-        {
-            try
-            {
-                if (result.status != Regorus.Internal.RegorusStatus.Ok)
-                {
-                    var message = Utf8Marshaller.FromUtf8(result.error_message);
-                    throw result.status.CreateException(message);
-                }
-
-                return result.data_type switch
-                {
-                    Regorus.Internal.RegorusDataType.String => Utf8Marshaller.FromUtf8(result.output),
-                    Regorus.Internal.RegorusDataType.Boolean => result.bool_value.ToString().ToLowerInvariant(),
-                    Regorus.Internal.RegorusDataType.Integer => result.int_value.ToString(),
-                    Regorus.Internal.RegorusDataType.None => null,
-                    _ => Utf8Marshaller.FromUtf8(result.output)
-                };
-            }
-            finally
-            {
-                Regorus.Internal.API.regorus_result_drop(result);
-            }
-        }
-
-        private void ThrowIfDisposed()
-        {
-            if (_isDisposed != 0 || _handle is null || _handle.IsClosed)
-            {
-                throw new ObjectDisposedException(nameof(Engine));
-            }
-        }
-
-        internal RegorusEngineHandle GetHandleForUse()
-        {
-            var handle = _handle;
-            if (handle is null || handle.IsClosed || handle.IsInvalid)
-            {
-                throw new ObjectDisposedException(nameof(Engine));
-            }
-            return handle;
-        }
-
-        internal void UseHandle(Action<IntPtr> action)
-        {
-            UseHandle<object?>(handlePtr =>
-            {
-                action(handlePtr);
-                return null;
-            });
-        }
-
-        internal T UseHandle<T>(Func<IntPtr, T> func)
-        {
-            var handle = GetHandleForUse();
-            bool addedRef = false;
-            try
-            {
-                handle.DangerousAddRef(ref addedRef);
-                var pointer = handle.DangerousGetHandle();
-                if (pointer == IntPtr.Zero)
-                {
-                    throw new ObjectDisposedException(nameof(Engine));
-                }
-
-                return func(pointer);
-            }
-            finally
-            {
-                if (addedRef)
-                {
-                    handle.DangerousRelease();
-                }
-            }
-        }
-
-        internal T UseHandleForInterop<T>(Func<IntPtr, T> func)
-        {
-            return UseHandle(func);
+            return ResultHelpers.GetStringResult(result);
         }
 
     }

bindings/csharp/Regorus/MemoryLimits.cs

@@ -89,12 +89,14 @@ namespace Regorus
                     );
                 }
 
-                if (result.int_value < 0)
+                try
                 {
-                    throw new OverflowException($"{errorContext}: native value was negative ({result.int_value})");
+                    return checked((ulong)result.int_value);
+                }
+                catch (OverflowException ex)
+                {
+                    throw new OverflowException($"{errorContext}: native value was out of range ({result.int_value})", ex);
                 }
-
-                return (ulong)result.int_value;
             }
             finally
             {

bindings/csharp/Regorus/ModuleMarshalling.cs

@@ -0,0 +1,156 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Buffers;
+using System.Collections.Generic;
+using Regorus;
+
+#nullable enable
+
+namespace Regorus.Internal
+{
+    internal static unsafe class ModuleMarshalling
+    {
+        internal sealed class PinnedPolicyModules : IDisposable
+        {
+            private readonly List<Utf8Marshaller.PinnedUtf8> _pins;
+            private bool _disposed;
+
+            internal PinnedPolicyModules(RegorusPolicyModule[] buffer, int length, List<Utf8Marshaller.PinnedUtf8> pins)
+            {
+                Buffer = buffer;
+                Length = length;
+                _pins = pins;
+            }
+
+            internal RegorusPolicyModule[] Buffer { get; }
+
+            internal int Length { get; }
+
+            public void Dispose()
+            {
+                if (_disposed)
+                {
+                    return;
+                }
+
+                foreach (var pin in _pins)
+                {
+                    pin.Dispose();
+                }
+
+                ArrayPool<RegorusPolicyModule>.Shared.Return(Buffer, clearArray: true);
+                _disposed = true;
+            }
+        }
+
+        internal sealed class PinnedEntryPoints : IDisposable
+        {
+            private readonly List<Utf8Marshaller.PinnedUtf8> _pins;
+            private bool _disposed;
+
+            internal PinnedEntryPoints(IntPtr[] buffer, int length, List<Utf8Marshaller.PinnedUtf8> pins)
+            {
+                Buffer = buffer;
+                Length = length;
+                _pins = pins;
+            }
+
+            internal IntPtr[] Buffer { get; }
+
+            internal int Length { get; }
+
+            public void Dispose()
+            {
+                if (_disposed)
+                {
+                    return;
+                }
+
+                foreach (var pin in _pins)
+                {
+                    pin.Dispose();
+                }
+
+                ArrayPool<IntPtr>.Shared.Return(Buffer, clearArray: true);
+                _disposed = true;
+            }
+        }
+
+        internal static PinnedPolicyModules PinPolicyModules(IReadOnlyList<PolicyModule> modules)
+        {
+            if (modules is null)
+            {
+                throw new ArgumentNullException(nameof(modules));
+            }
+
+            var count = modules.Count;
+            var buffer = ArrayPool<RegorusPolicyModule>.Shared.Rent(count);
+            var pins = new List<Utf8Marshaller.PinnedUtf8>(count * 2);
+
+            try
+            {
+                for (int i = 0; i < count; i++)
+                {
+                    var idPinned = Utf8Marshaller.Pin(modules[i].Id);
+                    var contentPinned = Utf8Marshaller.Pin(modules[i].Content);
+                    pins.Add(idPinned);
+                    pins.Add(contentPinned);
+
+                    buffer[i] = new RegorusPolicyModule
+                    {
+                        id = idPinned.Pointer,
+                        content = contentPinned.Pointer
+                    };
+                }
+
+                return new PinnedPolicyModules(buffer, count, pins);
+            }
+            catch
+            {
+                foreach (var pin in pins)
+                {
+                    pin.Dispose();
+                }
+
+                ArrayPool<RegorusPolicyModule>.Shared.Return(buffer, clearArray: true);
+                throw;
+            }
+        }
+
+        internal static PinnedEntryPoints PinEntryPoints(IReadOnlyList<string> entryPoints)
+        {
+            if (entryPoints is null)
+            {
+                throw new ArgumentNullException(nameof(entryPoints));
+            }
+
+            var count = entryPoints.Count;
+            var buffer = ArrayPool<IntPtr>.Shared.Rent(count);
+            var pins = new List<Utf8Marshaller.PinnedUtf8>(count);
+
+            try
+            {
+                for (int i = 0; i < count; i++)
+                {
+                    var entryPinned = Utf8Marshaller.Pin(entryPoints[i]);
+                    pins.Add(entryPinned);
+                    buffer[i] = (IntPtr)entryPinned.Pointer;
+                }
+
+                return new PinnedEntryPoints(buffer, count, pins);
+            }
+            catch
+            {
+                foreach (var pin in pins)
+                {
+                    pin.Dispose();
+                }
+
+                ArrayPool<IntPtr>.Shared.Return(buffer, clearArray: true);
+                throw;
+            }
+        }
+    }
+}

bindings/csharp/Regorus/Program.cs

@@ -13,14 +13,11 @@ namespace Regorus
     /// <summary>
     /// Represents a compiled RVM program.
     /// </summary>
-    public unsafe sealed class Program : IDisposable
+    public unsafe sealed class Program : SafeHandleWrapper
     {
-        private RegorusProgramHandle? _handle;
-        private int _isDisposed;
-
         private Program(RegorusProgramHandle handle)
+            : base(handle, nameof(Program))
         {
-            _handle = handle ?? throw new ArgumentNullException(nameof(handle));
         }
 
         /// <summary>
@@ -36,63 +33,57 @@ namespace Regorus
         /// </summary>
         public static Program CompileFromModules(string dataJson, IEnumerable<PolicyModule> modules, IEnumerable<string> entryPoints)
         {
-            var modulesArray = modules.ToArray();
-            var entryPointsArray = entryPoints.ToArray();
-            if (entryPointsArray.Length == 0)
+            if (modules is null)
+            {
+                throw new ArgumentNullException(nameof(modules));
+            }
+
+            if (entryPoints is null)
+            {
+                throw new ArgumentNullException(nameof(entryPoints));
+            }
+
+            return CompileFromModules(dataJson, modules.ToArray(), entryPoints.ToArray());
+        }
+
+        /// <summary>
+        /// Compile an RVM program from modules and entry points.
+        /// </summary>
+        public static Program CompileFromModules(string dataJson, IReadOnlyList<PolicyModule> modules, IReadOnlyList<string> entryPoints)
+        {
+            if (modules is null)
+            {
+                throw new ArgumentNullException(nameof(modules));
+            }
+
+            if (entryPoints is null)
+            {
+                throw new ArgumentNullException(nameof(entryPoints));
+            }
+
+            if (entryPoints.Count == 0)
             {
                 throw new ArgumentException("At least one entry point is required.", nameof(entryPoints));
             }
 
-            var nativeModules = new RegorusPolicyModule[modulesArray.Length];
-            var pinnedStrings = new List<Utf8Marshaller.PinnedUtf8>(modulesArray.Length * 2 + entryPointsArray.Length);
-            var entryPointers = new IntPtr[entryPointsArray.Length];
+            using var pinnedModules = ModuleMarshalling.PinPolicyModules(modules);
+            using var pinnedEntryPoints = ModuleMarshalling.PinEntryPoints(entryPoints);
 
-            try
+            return Utf8Marshaller.WithUtf8(dataJson, dataPtr =>
             {
-                for (int i = 0; i < modulesArray.Length; i++)
+                fixed (RegorusPolicyModule* modulesPtr = pinnedModules.Buffer)
+                fixed (IntPtr* entryPtr = pinnedEntryPoints.Buffer)
                 {
-                    var idPinned = Utf8Marshaller.Pin(modulesArray[i].Id);
-                    var contentPinned = Utf8Marshaller.Pin(modulesArray[i].Content);
-                    pinnedStrings.Add(idPinned);
-                    pinnedStrings.Add(contentPinned);
+                    var result = API.regorus_program_compile_from_modules(
+                        (byte*)dataPtr,
+                        modulesPtr,
+                        (UIntPtr)pinnedModules.Length,
+                        (byte**)entryPtr,
+                        (UIntPtr)pinnedEntryPoints.Length);
 
-                    nativeModules[i] = new RegorusPolicyModule
-                    {
-                        id = idPinned.Pointer,
-                        content = contentPinned.Pointer
-                    };
+                    return GetProgramResult(result);
                 }
-
-                for (int i = 0; i < entryPointsArray.Length; i++)
-                {
-                    var entryPinned = Utf8Marshaller.Pin(entryPointsArray[i]);
-                    pinnedStrings.Add(entryPinned);
-                    entryPointers[i] = (IntPtr)entryPinned.Pointer;
-                }
-
-                return Utf8Marshaller.WithUtf8(dataJson, dataPtr =>
-                {
-                    fixed (RegorusPolicyModule* modulesPtr = nativeModules)
-                    fixed (IntPtr* entryPtr = entryPointers)
-                    {
-                        var result = API.regorus_program_compile_from_modules(
-                            (byte*)dataPtr,
-                            modulesPtr,
-                            (UIntPtr)modulesArray.Length,
-                            (byte**)entryPtr,
-                            (UIntPtr)entryPointsArray.Length);
-
-                        return GetProgramResult(result);
-                    }
-                });
-            }
-            finally
-            {
-                foreach (var pinned in pinnedStrings)
-                {
-                    pinned.Dispose();
-                }
-            }
+            });
         }
 
         /// <summary>
@@ -104,44 +95,48 @@ namespace Regorus
             {
                 throw new ArgumentNullException(nameof(engine));
             }
+            if (entryPoints is null)
+            {
+                throw new ArgumentNullException(nameof(entryPoints));
+            }
 
-            var entryPointsArray = entryPoints.ToArray();
-            if (entryPointsArray.Length == 0)
+            return CompileFromEngine(engine, entryPoints.ToArray());
+        }
+
+        /// <summary>
+        /// Compile an RVM program from an engine instance and entry points.
+        /// </summary>
+        public static Program CompileFromEngine(Engine engine, IReadOnlyList<string> entryPoints)
+        {
+            if (engine is null)
+            {
+                throw new ArgumentNullException(nameof(engine));
+            }
+
+            if (entryPoints is null)
+            {
+                throw new ArgumentNullException(nameof(entryPoints));
+            }
+
+            if (entryPoints.Count == 0)
             {
                 throw new ArgumentException("At least one entry point is required.", nameof(entryPoints));
             }
 
-            var pinnedStrings = new List<Utf8Marshaller.PinnedUtf8>(entryPointsArray.Length);
-            var entryPointers = new IntPtr[entryPointsArray.Length];
-            try
-            {
-                for (int i = 0; i < entryPointsArray.Length; i++)
-                {
-                    var entryPinned = Utf8Marshaller.Pin(entryPointsArray[i]);
-                    pinnedStrings.Add(entryPinned);
-                    entryPointers[i] = (IntPtr)entryPinned.Pointer;
-                }
+            using var pinnedEntryPoints = ModuleMarshalling.PinEntryPoints(entryPoints);
 
-                return engine.UseHandleForInterop(enginePtr =>
-                {
-                    fixed (IntPtr* entryPtr = entryPointers)
-                    {
-                        var result = API.regorus_engine_compile_program_with_entrypoints(
-                            (RegorusEngine*)enginePtr,
-                            (byte**)entryPtr,
-                            (UIntPtr)entryPointsArray.Length);
-
-                        return GetProgramResult(result);
-                    }
-                });
-            }
-            finally
+            return engine.UseHandleForInterop(enginePtr =>
             {
-                foreach (var pinned in pinnedStrings)
+                fixed (IntPtr* entryPtr = pinnedEntryPoints.Buffer)
                 {
-                    pinned.Dispose();
+                    var result = API.regorus_engine_compile_program_with_entrypoints(
+                        (RegorusEngine*)enginePtr,
+                        (byte**)entryPtr,
+                        (UIntPtr)pinnedEntryPoints.Length);
+
+                    return GetProgramResult(result);
                 }
-            }
+            });
         }
 
         /// <summary>
@@ -169,7 +164,6 @@ namespace Regorus
         /// </summary>
         public byte[] SerializeBinary()
         {
-            ThrowIfDisposed();
             return UseHandle(programPtr =>
             {
                 var result = API.regorus_program_serialize_binary((RegorusProgram*)programPtr);
@@ -182,70 +176,12 @@ namespace Regorus
         /// </summary>
         public string? GenerateListing()
         {
-            ThrowIfDisposed();
             return UseHandle(programPtr =>
             {
                 return CheckAndDropResult(API.regorus_program_generate_listing((RegorusProgram*)programPtr));
             });
         }
 
-        public void Dispose()
-        {
-            Dispose(disposing: true);
-            GC.SuppressFinalize(this);
-        }
-
-        private void Dispose(bool disposing)
-        {
-            if (System.Threading.Interlocked.CompareExchange(ref _isDisposed, 1, 0) == 0)
-            {
-                _handle?.Dispose();
-                _handle = null;
-            }
-        }
-
-        private void ThrowIfDisposed()
-        {
-            if (_isDisposed != 0 || _handle is null || _handle.IsClosed)
-            {
-                throw new ObjectDisposedException(nameof(Program));
-            }
-        }
-
-        internal RegorusProgramHandle GetHandleForUse()
-        {
-            var handle = _handle;
-            if (handle is null || handle.IsClosed || handle.IsInvalid)
-            {
-                throw new ObjectDisposedException(nameof(Program));
-            }
-            return handle;
-        }
-
-        internal T UseHandle<T>(Func<IntPtr, T> func)
-        {
-            var handle = GetHandleForUse();
-            bool addedRef = false;
-            try
-            {
-                handle.DangerousAddRef(ref addedRef);
-                var pointer = handle.DangerousGetHandle();
-                if (pointer == IntPtr.Zero)
-                {
-                    throw new ObjectDisposedException(nameof(Program));
-                }
-
-                return func(pointer);
-            }
-            finally
-            {
-                if (addedRef)
-                {
-                    handle.DangerousRelease();
-                }
-            }
-        }
-
         private static Program GetProgramResult(RegorusResult result)
         {
             try
@@ -272,27 +208,7 @@ namespace Regorus
 
         private static string? CheckAndDropResult(RegorusResult result)
         {
-            try
-            {
-                if (result.status != RegorusStatus.Ok)
-                {
-                    var message = Utf8Marshaller.FromUtf8(result.error_message);
-                    throw result.status.CreateException(message);
-                }
-
-                return result.data_type switch
-                {
-                    RegorusDataType.String => Utf8Marshaller.FromUtf8(result.output),
-                    RegorusDataType.Boolean => result.bool_value.ToString().ToLowerInvariant(),
-                    RegorusDataType.Integer => result.int_value.ToString(),
-                    RegorusDataType.None => null,
-                    _ => Utf8Marshaller.FromUtf8(result.output)
-                };
-            }
-            finally
-            {
-                API.regorus_result_drop(result);
-            }
+            return ResultHelpers.GetStringResult(result);
         }
 
         private static byte[] ExtractBuffer(RegorusResult result)

bindings/csharp/Regorus/Regorus.csproj

@@ -8,9 +8,18 @@
        <LangVersion>10.0</LangVersion>
 
         <!-- See https://learn.microsoft.com/en-us/dotnet/core/tools/dotnet-pack -->
-        <VersionPrefix>0.9.0</VersionPrefix>
+        <VersionPrefix>0.9.1</VersionPrefix>
         <VersionSuffix>$(VersionSuffix)</VersionSuffix>
         <PackageReadmeFile>README.md</PackageReadmeFile>
+        <PackageLicenseExpression>MIT AND Apache-2.0 AND BSD-3-Clause</PackageLicenseExpression>
+        <PackageProjectUrl>https://github.com/microsoft/regorus</PackageProjectUrl>
+        <RepositoryUrl>https://github.com/microsoft/regorus</RepositoryUrl>
+        <RepositoryType>git</RepositoryType>
+        <Authors>Microsoft</Authors>
+        <Company>Microsoft</Company>
+        <PackageTags>rego;policy;engine;authorization;opa;rust</PackageTags>
+        <Description>Fast, lightweight Rego interpreter and policy engine for .NET, powered by Rust.</Description>
+        <Copyright>Copyright (c) Microsoft Corporation.</Copyright>
     </PropertyGroup>
 
     <PropertyGroup>
@@ -46,10 +55,14 @@
 
          <Error Text="$(RegorusFFIArtifactsDir)/x86_64-unknown-linux-gnu/$(RegorusFFIArtifactsProfile)/libregorus_ffi.so missing."
              Condition="!Exists('$(RegorusFFIArtifactsDir)/x86_64-unknown-linux-gnu/$(RegorusFFIArtifactsProfile)/libregorus_ffi.so')" />
+
+         <Error Text="$(RegorusFFIArtifactsDir)/aarch64-apple-darwin/$(RegorusFFIArtifactsProfile)/libregorus_ffi.dylib missing."
+             Condition="!Exists('$(RegorusFFIArtifactsDir)/aarch64-apple-darwin/$(RegorusFFIArtifactsProfile)/libregorus_ffi.dylib')" />
     </Target>
 
     <ItemGroup>
         <None Include="docs/README.md" Pack="true"  PackagePath="/" />
+        <None Include="../../../LICENSE" Pack="true" PackagePath="/" />
 
         <!-- Copy each binary to expected location within the package -->
         <None Include="$(RegorusFFIArtifactsDir)/x86_64-pc-windows-msvc/$(RegorusFFIArtifactsProfile)/*.dll" Pack="true" PackagePath="runtimes/win-x64/native/" />

bindings/csharp/Regorus/ResultHelpers.cs

@@ -0,0 +1,73 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+
+#nullable enable
+
+namespace Regorus.Internal
+{
+    internal static unsafe class ResultHelpers
+    {
+        internal static string? GetStringResult(RegorusResult result)
+        {
+            try
+            {
+                if (result.status != RegorusStatus.Ok)
+                {
+                    var message = Utf8Marshaller.FromUtf8(result.error_message);
+                    throw result.status.CreateException(message);
+                }
+
+                return result.data_type switch
+                {
+                    RegorusDataType.String => Utf8Marshaller.FromUtf8(result.output),
+                    RegorusDataType.Boolean => result.bool_value.ToString().ToLowerInvariant(),
+                    RegorusDataType.Integer => result.int_value.ToString(),
+                    RegorusDataType.None => null,
+                    _ => Utf8Marshaller.FromUtf8(result.output)
+                };
+            }
+            finally
+            {
+                API.regorus_result_drop(result);
+            }
+        }
+
+        internal static bool GetBoolResult(RegorusResult result)
+        {
+            try
+            {
+                if (result.status != RegorusStatus.Ok)
+                {
+                    var message = Utf8Marshaller.FromUtf8(result.error_message);
+                    throw result.status.CreateException(message);
+                }
+
+                return result.data_type == RegorusDataType.Boolean && result.bool_value;
+            }
+            finally
+            {
+                API.regorus_result_drop(result);
+            }
+        }
+
+        internal static long GetIntResult(RegorusResult result)
+        {
+            try
+            {
+                if (result.status != RegorusStatus.Ok)
+                {
+                    var message = Utf8Marshaller.FromUtf8(result.error_message);
+                    throw result.status.CreateException(message);
+                }
+
+                return result.data_type == RegorusDataType.Integer ? result.int_value : 0;
+            }
+            finally
+            {
+                API.regorus_result_drop(result);
+            }
+        }
+    }
+}

bindings/csharp/Regorus/Rvm.cs

@@ -7,22 +7,35 @@ using Regorus.Internal;
 #nullable enable
 namespace Regorus
 {
+    /// <summary>
+    /// Execution mode for the RVM runtime.
+    /// </summary>
+    public enum ExecutionMode : byte
+    {
+        /// <summary>
+        /// Run to completion without yielding.
+        /// </summary>
+        RunToCompletion = 0,
+
+        /// <summary>
+        /// Suspendable execution mode.
+        /// </summary>
+        Suspendable = 1,
+    }
+
     /// <summary>
     /// Wrapper for the Regorus RVM runtime.
     /// </summary>
-    public unsafe sealed class Rvm : IDisposable
+    public unsafe sealed class Rvm : SafeHandleWrapper
     {
-        private RegorusRvmHandle? _handle;
-        private int _isDisposed;
-
         public Rvm()
+            : base(RegorusRvmHandle.Create(), nameof(Rvm))
         {
-            _handle = RegorusRvmHandle.Create();
         }
 
         private Rvm(RegorusRvmHandle handle)
+            : base(handle, nameof(Rvm))
         {
-            _handle = handle ?? throw new ArgumentNullException(nameof(handle));
         }
 
         /// <summary>
@@ -47,13 +60,12 @@ namespace Regorus
         /// </summary>
         public void LoadProgram(Program program)
         {
-            ThrowIfDisposed();
             if (program is null)
             {
                 throw new ArgumentNullException(nameof(program));
             }
 
-            program.UseHandle(programPtr =>
+            program.UseHandleForInterop(programPtr =>
             {
                 UseHandle(vmPtr =>
                 {
@@ -69,7 +81,6 @@ namespace Regorus
         /// </summary>
         public void SetDataJson(string dataJson)
         {
-            ThrowIfDisposed();
             Utf8Marshaller.WithUtf8(dataJson, dataPtr =>
             {
                 UseHandle(vmPtr =>
@@ -85,7 +96,6 @@ namespace Regorus
         /// </summary>
         public void SetInputJson(string inputJson)
         {
-            ThrowIfDisposed();
             Utf8Marshaller.WithUtf8(inputJson, inputPtr =>
             {
                 UseHandle(vmPtr =>
@@ -101,7 +111,6 @@ namespace Regorus
         /// </summary>
         public void SetExecutionMode(byte mode)
         {
-            ThrowIfDisposed();
             UseHandle(vmPtr =>
             {
                 CheckAndDropResult(API.regorus_rvm_set_execution_mode((RegorusRvm*)vmPtr, mode));
@@ -109,12 +118,19 @@ namespace Regorus
             });
         }
 
+        /// <summary>
+        /// Set the execution mode.
+        /// </summary>
+        public void SetExecutionMode(ExecutionMode mode)
+        {
+            SetExecutionMode((byte)mode);
+        }
+
         /// <summary>
         /// Execute the program and return the JSON result.
         /// </summary>
         public string? Execute()
         {
-            ThrowIfDisposed();
             return UseHandle(vmPtr =>
             {
                 return CheckAndDropResult(API.regorus_rvm_execute((RegorusRvm*)vmPtr));
@@ -126,7 +142,6 @@ namespace Regorus
         /// </summary>
         public string? ExecuteEntryPoint(string entryPoint)
         {
-            ThrowIfDisposed();
             return Utf8Marshaller.WithUtf8(entryPoint, entryPtr =>
             {
                 return UseHandle(vmPtr =>
@@ -141,7 +156,6 @@ namespace Regorus
         /// </summary>
         public string? ExecuteEntryPoint(ulong index)
         {
-            ThrowIfDisposed();
             return UseHandle(vmPtr =>
             {
                 return CheckAndDropResult(API.regorus_rvm_execute_entry_point_by_index((RegorusRvm*)vmPtr, (UIntPtr)index));
@@ -153,7 +167,6 @@ namespace Regorus
         /// </summary>
         public string? Resume(string? resumeValueJson)
         {
-            ThrowIfDisposed();
             if (resumeValueJson is null)
             {
                 return UseHandle(vmPtr =>
@@ -176,70 +189,12 @@ namespace Regorus
         /// </summary>
         public string? GetExecutionState()
         {
-            ThrowIfDisposed();
             return UseHandle(vmPtr =>
             {
                 return CheckAndDropResult(API.regorus_rvm_get_execution_state((RegorusRvm*)vmPtr));
             });
         }
 
-        public void Dispose()
-        {
-            Dispose(disposing: true);
-            GC.SuppressFinalize(this);
-        }
-
-        private void Dispose(bool disposing)
-        {
-            if (System.Threading.Interlocked.CompareExchange(ref _isDisposed, 1, 0) == 0)
-            {
-                _handle?.Dispose();
-                _handle = null;
-            }
-        }
-
-        private void ThrowIfDisposed()
-        {
-            if (_isDisposed != 0 || _handle is null || _handle.IsClosed)
-            {
-                throw new ObjectDisposedException(nameof(Rvm));
-            }
-        }
-
-        internal RegorusRvmHandle GetHandleForUse()
-        {
-            var handle = _handle;
-            if (handle is null || handle.IsClosed || handle.IsInvalid)
-            {
-                throw new ObjectDisposedException(nameof(Rvm));
-            }
-            return handle;
-        }
-
-        internal T UseHandle<T>(Func<IntPtr, T> func)
-        {
-            var handle = GetHandleForUse();
-            bool addedRef = false;
-            try
-            {
-                handle.DangerousAddRef(ref addedRef);
-                var pointer = handle.DangerousGetHandle();
-                if (pointer == IntPtr.Zero)
-                {
-                    throw new ObjectDisposedException(nameof(Rvm));
-                }
-
-                return func(pointer);
-            }
-            finally
-            {
-                if (addedRef)
-                {
-                    handle.DangerousRelease();
-                }
-            }
-        }
-
         private static Rvm GetRvmResult(RegorusResult result)
         {
             try
@@ -266,27 +221,7 @@ namespace Regorus
 
         private static string? CheckAndDropResult(RegorusResult result)
         {
-            try
-            {
-                if (result.status != RegorusStatus.Ok)
-                {
-                    var message = Utf8Marshaller.FromUtf8(result.error_message);
-                    throw result.status.CreateException(message);
-                }
-
-                return result.data_type switch
-                {
-                    RegorusDataType.String => Utf8Marshaller.FromUtf8(result.output),
-                    RegorusDataType.Boolean => result.bool_value.ToString().ToLowerInvariant(),
-                    RegorusDataType.Integer => result.int_value.ToString(),
-                    RegorusDataType.None => null,
-                    _ => Utf8Marshaller.FromUtf8(result.output)
-                };
-            }
-            finally
-            {
-                API.regorus_result_drop(result);
-            }
+            return ResultHelpers.GetStringResult(result);
         }
     }
 }

bindings/csharp/Regorus/SafeHandleWrapper.cs

@@ -0,0 +1,272 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Runtime.InteropServices;
+
+#nullable enable
+namespace Regorus
+{
+    /// <summary>
+    /// Base class for native handle wrappers that coordinates handle usage and disposal.
+    ///
+    /// Behavior summary:
+    /// - UseHandle: blocks Dispose while running; throws ObjectDisposedException if disposal has started or the handle is invalid.
+    /// - Dispose: marks disposing and blocks new calls; waits briefly for in-flight calls to finish, then defers native release to the last exiting call if needed.
+    /// - Handles are never exposed directly; derived classes can only work through UseHandle helpers.
+    ///
+    /// Concurrency model:
+    /// - _state tracks lifecycle transitions (Active -> DisposeRequested -> Released).
+    /// - HandleGate tracks in-flight operations and enforces the "no new calls after Dispose" rule.
+    /// - SafeHandle is pinned per call via DangerousAddRef to prevent use-after-free while native work runs.
+    /// - If Dispose times out, the last in-flight caller performs the release to avoid leaks.
+    /// </summary>
+    public abstract class SafeHandleWrapper : IDisposable
+    {
+        private static readonly TimeSpan DefaultDisposeTimeout = TimeSpan.FromMilliseconds(50);
+        private const int StateActive = 0;
+        private const int StateDisposeRequested = 1;
+        private const int StateReleased = 2;
+        private readonly HandleGate _gate;
+        private readonly string _ownerName;
+        private int _state;
+        private SafeHandle? _handle;
+
+        protected SafeHandleWrapper(SafeHandle handle, string ownerName)
+        {
+            // Cache ownership info and initialize the gate before any use to avoid racing disposal.
+            _handle = handle ?? throw new ArgumentNullException(nameof(handle));
+            _ownerName = ownerName ?? throw new ArgumentNullException(nameof(ownerName));
+            _gate = new HandleGate(ownerName);
+            // Default to a very short wait when in-flight calls exist; release is deferred to the last caller if needed.
+        }
+
+        protected void UseHandle(Action<IntPtr> action)
+        {
+            // Reuse the generic path to keep add/ref/release in one place.
+            UseHandle<object?>(ptr =>
+            {
+                action(ptr);
+                return null;
+            });
+        }
+
+        protected T UseHandle<T>(Func<IntPtr, T> func)
+        {
+            // Fast reject if dispose was requested.
+            if (System.Threading.Volatile.Read(ref _state) != StateActive)
+            {
+                throw new ObjectDisposedException(_ownerName);
+            }
+
+            // Enter gate so Dispose waits for in-flight native calls.
+            _gate.Enter();
+            bool addedRef = false;
+            SafeHandle? handle = null;
+            try
+            {
+                // Race: Dispose could begin after Enter; GetHandleForUse validates the handle again.
+                handle = GetHandleForUse();
+                // DangerousAddRef pins the SafeHandle so Dispose cannot close it mid-call.
+                handle.DangerousAddRef(ref addedRef);
+                var pointer = handle.DangerousGetHandle();
+                // Validate pointer after AddRef in case handle became invalid between checks.
+                if (pointer == IntPtr.Zero)
+                {
+                    throw new ObjectDisposedException(_ownerName);
+                }
+
+                return func(pointer);
+            }
+            finally
+            {
+                // Always release the DangerousAddRef to avoid leaking the native handle.
+                if (addedRef)
+                {
+                    handle?.DangerousRelease();
+                }
+
+                // Leave gate so Dispose can proceed when the last caller exits.
+                var idle = _gate.Exit();
+                // Race: Dispose may have timed out while we were in-flight.
+                // The last exiting caller performs the native release to avoid leaks.
+                if (idle && System.Threading.Volatile.Read(ref _state) == StateDisposeRequested)
+                {
+                    TryReleaseHandle();
+                }
+            }
+        }
+
+        internal T UseHandleForInterop<T>(Func<IntPtr, T> func)
+        {
+            // Explicit alias for interop-specific call sites.
+            return UseHandle(func);
+        }
+
+        internal void UseHandleForInterop(Action<IntPtr> action)
+        {
+            // Explicit alias for interop-specific call sites.
+            UseHandle(action);
+        }
+
+        private void ThrowIfDisposed()
+        {
+            // Fast check for dispose state so callers fail deterministically.
+            if (System.Threading.Volatile.Read(ref _state) != StateActive)
+            {
+                throw new ObjectDisposedException(_ownerName);
+            }
+
+            // Validate the underlying SafeHandle is still usable; avoids races with release.
+            var handle = _handle;
+            if (handle is null || handle.IsClosed || handle.IsInvalid)
+            {
+                throw new ObjectDisposedException(_ownerName);
+            }
+        }
+
+        private SafeHandle GetHandleForUse()
+        {
+            // Centralized gate for derived classes to grab the handle safely.
+            // This is a second line of defense in case disposal began after the initial state check.
+            var handle = _handle;
+            if (handle is null || handle.IsClosed || handle.IsInvalid)
+            {
+                throw new ObjectDisposedException(_ownerName);
+            }
+            return handle;
+        }
+
+        public void Dispose()
+        {
+            // Only the first caller runs disposal; others become no-ops.
+            if (System.Threading.Interlocked.CompareExchange(ref _state, StateDisposeRequested, StateActive) == StateActive)
+            {
+                // Block new calls and wait briefly if there are in-flight operations.
+                var completed = _gate.TryBeginDispose(DefaultDisposeTimeout, out var hadActive);
+                if (completed)
+                {
+                    // Either no active calls or they drained within the short timeout.
+                    TryReleaseHandle();
+                }
+                else
+                {
+                    // Defer release to the last in-flight caller to avoid leaks without blocking indefinitely.
+                    // Race: if the last in-flight caller already exited, there will be no Exit() to trigger release.
+                    // Re-check active state and release immediately in that case.
+                    if (!hadActive || _gate.IsIdle)
+                    {
+                        TryReleaseHandle();
+                    }
+                }
+            }
+
+            GC.SuppressFinalize(this);
+        }
+
+        private void TryReleaseHandle()
+        {
+            if (System.Threading.Interlocked.CompareExchange(ref _state, StateReleased, StateDisposeRequested) != StateDisposeRequested)
+            {
+                return;
+            }
+
+            // Once released, no caller should be able to observe a valid handle.
+            // SafeHandle.Dispose closes the native resource; null to prevent reuse after dispose.
+            _handle?.Dispose();
+            _handle = null;
+            // Release the wait handle resources after disposal completes.
+            _gate.Dispose();
+        }
+
+        /// <summary>
+        /// Tracks in-flight operations and coordinates disposal.
+        /// </summary>
+        private sealed class HandleGate : IDisposable
+        {
+            private readonly string _ownerName;
+            private readonly System.Threading.ManualResetEventSlim _idle = new(initialState: true);
+            private int _active;
+            private int _disposing;
+
+            internal HandleGate(string ownerName)
+            {
+                _ownerName = ownerName;
+            }
+
+            internal void Enter()
+            {
+                // If disposal already started, reject new work immediately.
+                if (System.Threading.Volatile.Read(ref _disposing) != 0)
+                {
+                    ThrowDisposed();
+                }
+
+                // Track active callers; first one resets idle event.
+                var active = System.Threading.Interlocked.Increment(ref _active);
+                if (active == 1)
+                {
+                    _idle.Reset();
+                }
+
+                // Re-check disposing to handle races where Dispose began after increment.
+                if (System.Threading.Volatile.Read(ref _disposing) != 0)
+                {
+                    Exit();
+                    ThrowDisposed();
+                }
+            }
+
+            internal bool Exit()
+            {
+                // Last caller signals idle so Dispose can continue.
+                if (System.Threading.Interlocked.Decrement(ref _active) == 0)
+                {
+                    _idle.Set();
+                    return true;
+                }
+
+                return false;
+            }
+
+            internal bool IsIdle => System.Threading.Volatile.Read(ref _active) == 0;
+
+            internal bool TryBeginDispose(TimeSpan timeout, out bool hadActive)
+            {
+                // Set disposing flag once; subsequent calls treat as already disposing.
+                if (System.Threading.Interlocked.Exchange(ref _disposing, 1) != 0)
+                {
+                    hadActive = System.Threading.Volatile.Read(ref _active) != 0;
+                    return true;
+                }
+
+                hadActive = System.Threading.Volatile.Read(ref _active) != 0;
+                if (!hadActive)
+                {
+                    // No in-flight callers; disposal can proceed without waiting.
+                    return true;
+                }
+
+                // Wait for active callers to drain; optional timeout avoids blocking forever.
+                if (timeout == System.Threading.Timeout.InfiniteTimeSpan)
+                {
+                    _idle.Wait();
+                    return true;
+                }
+
+                // Race note: callers may finish between the timeout decision and Wait call; Wait handles that safely.
+                return _idle.Wait(timeout);
+            }
+
+            private void ThrowDisposed()
+            {
+                throw new ObjectDisposedException(_ownerName);
+            }
+
+            public void Dispose()
+            {
+                _idle.Dispose();
+            }
+        }
+    }
+}

bindings/csharp/Regorus/SafeHandles.cs

@@ -44,7 +44,7 @@ namespace Regorus
 
         protected override bool ReleaseHandle()
         {
-            if (!IsInvalid && !IsClosed)
+            if (!IsInvalid)
             {
                 unsafe
                 {
@@ -76,7 +76,7 @@ namespace Regorus
 
         protected override bool ReleaseHandle()
         {
-            if (!IsInvalid && !IsClosed)
+            if (!IsInvalid)
             {
                 unsafe
                 {
@@ -124,7 +124,7 @@ namespace Regorus
 
         protected override bool ReleaseHandle()
         {
-            if (!IsInvalid && !IsClosed)
+            if (!IsInvalid)
             {
                 unsafe
                 {
@@ -172,7 +172,7 @@ namespace Regorus
 
         protected override bool ReleaseHandle()
         {
-            if (!IsInvalid && !IsClosed)
+            if (!IsInvalid)
             {
                 unsafe
                 {

bindings/csharp/Regorus/SchemaRegistry.cs

@@ -2,6 +2,8 @@
 // Licensed under the MIT License.
 
 using System;
+using System.Collections.Generic;
+using System.Text.Json;
 using Regorus.Internal;
 
 #nullable enable
@@ -27,7 +29,7 @@ namespace Regorus
                 {
                     unsafe
                     {
-                        CheckAndDropResult(Internal.API.regorus_resource_schema_register((byte*)namePtr, (byte*)schemaPtr));
+                        ResultHelpers.GetStringResult(Internal.API.regorus_resource_schema_register((byte*)namePtr, (byte*)schemaPtr));
                     }
                 });
             });
@@ -46,7 +48,7 @@ namespace Regorus
                 unsafe
                 {
                     var result = Internal.API.regorus_resource_schema_contains((byte*)namePtr);
-                    return GetBoolResult(result);
+                    return ResultHelpers.GetBoolResult(result);
                 }
             });
         }
@@ -61,7 +63,7 @@ namespace Regorus
             get
             {
                 var result = Internal.API.regorus_resource_schema_len();
-                return GetIntResult(result);
+                return ResultHelpers.GetIntResult(result);
             }
         }
 
@@ -75,7 +77,7 @@ namespace Regorus
             get
             {
                 var result = Internal.API.regorus_resource_schema_is_empty();
-                return GetBoolResult(result);
+                return ResultHelpers.GetBoolResult(result);
             }
         }
 
@@ -86,7 +88,16 @@ namespace Regorus
         /// <exception cref="Exception">Thrown when the operation fails</exception>
         public static string ListResourceNames()
         {
-            return CheckAndDropResult(Internal.API.regorus_resource_schema_list_names()) ?? "[]";
+            return ResultHelpers.GetStringResult(Internal.API.regorus_resource_schema_list_names()) ?? "[]";
+        }
+
+        /// <summary>
+        /// List all registered resource schema names as managed strings.
+        /// </summary>
+        public static IReadOnlyList<string> GetResourceNames()
+        {
+            var json = ListResourceNames();
+            return JsonSerializer.Deserialize<string[]>(json) ?? Array.Empty<string>();
         }
 
         /// <summary>
@@ -102,7 +113,7 @@ namespace Regorus
                 unsafe
                 {
                     var result = Internal.API.regorus_resource_schema_remove((byte*)namePtr);
-                    return GetBoolResult(result);
+                    return ResultHelpers.GetBoolResult(result);
                 }
             });
         }
@@ -113,7 +124,7 @@ namespace Regorus
         /// <exception cref="Exception">Thrown when the operation fails</exception>
         public static void ClearResources()
         {
-            CheckAndDropResult(Internal.API.regorus_resource_schema_clear());
+            ResultHelpers.GetStringResult(Internal.API.regorus_resource_schema_clear());
         }
 
         /// <summary>
@@ -130,7 +141,7 @@ namespace Regorus
                 {
                     unsafe
                     {
-                        CheckAndDropResult(Internal.API.regorus_effect_schema_register((byte*)namePtr, (byte*)schemaPtr));
+                        ResultHelpers.GetStringResult(Internal.API.regorus_effect_schema_register((byte*)namePtr, (byte*)schemaPtr));
                     }
                 });
             });
@@ -149,7 +160,7 @@ namespace Regorus
                 unsafe
                 {
                     var result = Internal.API.regorus_effect_schema_contains((byte*)namePtr);
-                    return GetBoolResult(result);
+                    return ResultHelpers.GetBoolResult(result);
                 }
             });
         }
@@ -164,7 +175,7 @@ namespace Regorus
             get
             {
                 var result = Internal.API.regorus_effect_schema_len();
-                return GetIntResult(result);
+                return ResultHelpers.GetIntResult(result);
             }
         }
 
@@ -178,7 +189,7 @@ namespace Regorus
             get
             {
                 var result = Internal.API.regorus_effect_schema_is_empty();
-                return GetBoolResult(result);
+                return ResultHelpers.GetBoolResult(result);
             }
         }
 
@@ -189,7 +200,16 @@ namespace Regorus
         /// <exception cref="Exception">Thrown when the operation fails</exception>
         public static string ListEffectNames()
         {
-            return CheckAndDropResult(Internal.API.regorus_effect_schema_list_names()) ?? "[]";
+            return ResultHelpers.GetStringResult(Internal.API.regorus_effect_schema_list_names()) ?? "[]";
+        }
+
+        /// <summary>
+        /// List all registered effect schema names as managed strings.
+        /// </summary>
+        public static IReadOnlyList<string> GetEffectNames()
+        {
+            var json = ListEffectNames();
+            return JsonSerializer.Deserialize<string[]>(json) ?? Array.Empty<string>();
         }
 
         /// <summary>
@@ -205,7 +225,7 @@ namespace Regorus
                 unsafe
                 {
                     var result = Internal.API.regorus_effect_schema_remove((byte*)namePtr);
-                    return GetBoolResult(result);
+                    return ResultHelpers.GetBoolResult(result);
                 }
             });
         }
@@ -216,68 +236,7 @@ namespace Regorus
         /// <exception cref="Exception">Thrown when the operation fails</exception>
         public static void ClearEffects()
         {
-            CheckAndDropResult(Internal.API.regorus_effect_schema_clear());
-        }
-
-        private static string? CheckAndDropResult(Internal.RegorusResult result)
-        {
-            try
-            {
-                if (result.status != Internal.RegorusStatus.Ok)
-                {
-                    var message = Utf8Marshaller.FromUtf8(result.error_message);
-                    throw result.status.CreateException(message);
-                }
-
-                return result.data_type switch
-                {
-                    Internal.RegorusDataType.String => Utf8Marshaller.FromUtf8(result.output),
-                    Internal.RegorusDataType.Boolean => result.bool_value.ToString().ToLowerInvariant(),
-                    Internal.RegorusDataType.Integer => result.int_value.ToString(),
-                    Internal.RegorusDataType.None => null,
-                    _ => Utf8Marshaller.FromUtf8(result.output)
-                };
-            }
-            finally
-            {
-                Internal.API.regorus_result_drop(result);
-            }
-        }
-
-        private static bool GetBoolResult(Internal.RegorusResult result)
-        {
-            try
-            {
-                if (result.status != Internal.RegorusStatus.Ok)
-                {
-                    var message = Utf8Marshaller.FromUtf8(result.error_message);
-                    throw result.status.CreateException(message);
-                }
-
-                return result.data_type == Internal.RegorusDataType.Boolean ? result.bool_value : false;
-            }
-            finally
-            {
-                Internal.API.regorus_result_drop(result);
-            }
-        }
-
-        private static long GetIntResult(Internal.RegorusResult result)
-        {
-            try
-            {
-                if (result.status != Internal.RegorusStatus.Ok)
-                {
-                    var message = Utf8Marshaller.FromUtf8(result.error_message);
-                    throw result.status.CreateException(message);
-                }
-
-                return result.data_type == Internal.RegorusDataType.Integer ? result.int_value : 0;
-            }
-            finally
-            {
-                Internal.API.regorus_result_drop(result);
-            }
+            ResultHelpers.GetStringResult(Internal.API.regorus_effect_schema_clear());
         }
     }
 }

bindings/csharp/Regorus/TargetRegistry.cs

@@ -2,6 +2,8 @@
 // Licensed under the MIT License.
 
 using System;
+using System.Collections.Generic;
+using System.Text.Json;
 using Regorus.Internal;
 
 #nullable enable
@@ -26,7 +28,7 @@ namespace Regorus
             {
                 unsafe
                 {
-                    CheckAndDropResult(Internal.API.regorus_register_target_from_json((byte*)targetPtr));
+                    ResultHelpers.GetStringResult(Internal.API.regorus_register_target_from_json((byte*)targetPtr));
                 }
             });
         }
@@ -44,7 +46,7 @@ namespace Regorus
                 unsafe
                 {
                     var result = Internal.API.regorus_target_registry_contains((byte*)namePtr);
-                    return GetBoolResult(result);
+                    return ResultHelpers.GetBoolResult(result);
                 }
             });
         }
@@ -56,7 +58,16 @@ namespace Regorus
         /// <exception cref="Exception">Thrown when the operation fails</exception>
         public static string ListNames()
         {
-            return CheckAndDropResult(Internal.API.regorus_target_registry_list_names()) ?? "[]";
+            return ResultHelpers.GetStringResult(Internal.API.regorus_target_registry_list_names()) ?? "[]";
+        }
+
+        /// <summary>
+        /// Get a list of all registered target names as managed strings.
+        /// </summary>
+        public static IReadOnlyList<string> GetNames()
+        {
+            var json = ListNames();
+            return JsonSerializer.Deserialize<string[]>(json) ?? Array.Empty<string>();
         }
 
         /// <summary>
@@ -72,7 +83,7 @@ namespace Regorus
                 unsafe
                 {
                     var result = Internal.API.regorus_target_registry_remove((byte*)namePtr);
-                    return GetBoolResult(result);
+                    return ResultHelpers.GetBoolResult(result);
                 }
             });
         }
@@ -83,7 +94,7 @@ namespace Regorus
         /// <exception cref="Exception">Thrown when the operation fails</exception>
         public static void Clear()
         {
-            CheckAndDropResult(Internal.API.regorus_target_registry_clear());
+            ResultHelpers.GetStringResult(Internal.API.regorus_target_registry_clear());
         }
 
         /// <summary>
@@ -96,10 +107,9 @@ namespace Regorus
             get
             {
                 var result = Internal.API.regorus_target_registry_len();
-                return GetIntResult(result);
+                return ResultHelpers.GetIntResult(result);
             }
         }
-
         /// <summary>
         /// Check if the target registry is empty.
         /// </summary>
@@ -110,68 +120,7 @@ namespace Regorus
             get
             {
                 var result = Internal.API.regorus_target_registry_is_empty();
-                return GetBoolResult(result);
-            }
-        }
-
-        private static string? CheckAndDropResult(Internal.RegorusResult result)
-        {
-            try
-            {
-                if (result.status != Internal.RegorusStatus.Ok)
-                {
-                    var message = Utf8Marshaller.FromUtf8(result.error_message);
-                    throw result.status.CreateException(message);
-                }
-
-                return result.data_type switch
-                {
-                    Internal.RegorusDataType.String => Utf8Marshaller.FromUtf8(result.output),
-                    Internal.RegorusDataType.Boolean => result.bool_value.ToString().ToLowerInvariant(),
-                    Internal.RegorusDataType.Integer => result.int_value.ToString(),
-                    Internal.RegorusDataType.None => null,
-                    _ => Utf8Marshaller.FromUtf8(result.output)
-                };
-            }
-            finally
-            {
-                Internal.API.regorus_result_drop(result);
-            }
-        }
-
-        private static bool GetBoolResult(Internal.RegorusResult result)
-        {
-            try
-            {
-                if (result.status != Internal.RegorusStatus.Ok)
-                {
-                    var message = Utf8Marshaller.FromUtf8(result.error_message);
-                    throw result.status.CreateException(message);
-                }
-
-                return result.data_type == Internal.RegorusDataType.Boolean ? result.bool_value : false;
-            }
-            finally
-            {
-                Internal.API.regorus_result_drop(result);
-            }
-        }
-
-        private static long GetIntResult(Internal.RegorusResult result)
-        {
-            try
-            {
-                if (result.status != Internal.RegorusStatus.Ok)
-                {
-                    var message = Utf8Marshaller.FromUtf8(result.error_message);
-                    throw result.status.CreateException(message);
-                }
-
-                return result.data_type == Internal.RegorusDataType.Integer ? result.int_value : 0;
-            }
-            finally
-            {
-                Internal.API.regorus_result_drop(result);
+                return ResultHelpers.GetBoolResult(result);
             }
         }
     }

bindings/csharp/Regorus/Utf8Marshaller.cs

@@ -17,10 +17,10 @@ namespace Regorus.Internal
     /// </summary>
     internal static class Utf8Marshaller
     {
-    // Mirrors BCL patterns (e.g., System.Text.Json encoding helpers) by stackalloc'ing
-    // up to 512 bytes to cover common short strings while keeping the stack usage well
-    // below typical per-frame limits; larger payloads fall back to pooled buffers.
-    private const int StackAllocThreshold = 512;
+        // Mirrors BCL patterns (e.g., System.Text.Json encoding helpers) by stackalloc'ing
+        // up to 512 bytes to cover common short strings while keeping the stack usage well
+        // below typical per-frame limits; larger payloads fall back to pooled buffers.
+        private const int StackAllocThreshold = 512;
 
         /// <summary>
         /// Represents a pooled and pinned UTF-8 buffer suitable for scenarios where

bindings/csharp/TargetExampleApp/Program.cs

@@ -65,7 +65,7 @@ triplet_count := count([1 |
     private const string EXECUTION_TIMER_QUERY = "data.limits.timer.triplet_count";
     private const int EXECUTION_TIMER_VALUE_COUNT = 40;
 
-        private const string RVM_POLICY = """
+    private const string RVM_POLICY = """
 package demo
 import rego.v1
 
@@ -78,7 +78,7 @@ allow if {
 }
 """;
 
-        private const string RVM_DATA = """
+    private const string RVM_DATA = """
 {
     "roles": {
         "alice": ["admin", "reader"]
@@ -86,13 +86,13 @@ allow if {
 }
 """;
 
-        private const string RVM_INPUT = """
+    private const string RVM_INPUT = """
 {
     "user": "alice"
 }
 """;
 
-        private const string HOST_AWAIT_POLICY = """
+    private const string HOST_AWAIT_POLICY = """
 package demo
 import rego.v1
 
@@ -105,7 +105,7 @@ allow if {
 }
 """;
 
-        private const string HOST_AWAIT_INPUT = """
+    private const string HOST_AWAIT_INPUT = """
     {
         "account": {
             "id": "acct-1",
@@ -216,7 +216,7 @@ allow if {
 
         var nonCompliantResult = compiledPolicy.EvalWithInput(NON_COMPLIANT_STORAGE_ACCOUNT);
         Console.WriteLine($"Result: {nonCompliantResult}");
-        
+
         // 4. Demonstrate thread-safe concurrent evaluation
         Console.WriteLine("\n4. Testing concurrent evaluation from multiple threads:");
         DemonstrateConcurrentEvaluation(compiledPolicy);
@@ -246,42 +246,44 @@ allow if {
         };
 
         Console.WriteLine($"Starting {testInputs.Length} concurrent evaluations...");
-        
-        var tasks = testInputs.Select(input => 
-            Task.Run(() => {
+
+        var tasks = testInputs.Select(input =>
+            Task.Run(() =>
+            {
                 var (threadName, json) = input;
                 var stopwatch = System.Diagnostics.Stopwatch.StartNew();
-                
+
                 // Multiple evaluations per thread to stress test
                 var results = new List<string>();
                 for (int i = 0; i < 1000; i++)
                 {
-                    var result = compiledPolicy.EvalWithInput(json);
+                    var result = compiledPolicy.EvalWithInput(json)
+                        ?? throw new System.InvalidOperationException("Expected EvalWithInput to return a JSON value.");
                     results.Add(result);
                 }
-                
+
                 stopwatch.Stop();
                 var microseconds = stopwatch.ElapsedTicks * 1000000 / System.Diagnostics.Stopwatch.Frequency;
-                
+
                 // Verify all results are identical (thread safety)
                 var firstResult = results[0];
                 var allIdentical = results.All(r => r == firstResult);
-                
+
                 Console.WriteLine($"✓ {threadName}: {results.Count} evaluations in {microseconds}μs, " +
                                 $"Results consistent: {allIdentical}");
-                
+
                 return (threadName, results.Count, microseconds, allIdentical);
             })
         ).ToArray();
 
         // Wait for all threads to complete
         var results = Task.WhenAll(tasks).Result;
-        
+
         Console.WriteLine("\nConcurrency test results:");
         var totalEvaluations = results.Sum(r => r.Item2);
         var maxTime = results.Max(r => r.Item3);
         var allConsistent = results.All(r => r.allIdentical);
-        
+
         Console.WriteLine($"✓ Total evaluations: {totalEvaluations}");
         Console.WriteLine($"✓ Max thread time: {maxTime}μs");
         Console.WriteLine($"✓ All threads consistent: {allConsistent}");
@@ -292,28 +294,28 @@ allow if {
     static void DemonstratePolicyInfo(Regorus.CompiledPolicy compiledPolicy)
     {
         Console.WriteLine("Getting policy metadata using GetPolicyInfo()...");
-        
+
         try
         {
             var policyInfo = compiledPolicy.GetPolicyInfo();
-            
+
             Console.WriteLine($"✓ Policy Information Retrieved:");
             Console.WriteLine($"  Target Name: {policyInfo.TargetName ?? "None"}");
             Console.WriteLine($"  Effect Rule: {policyInfo.EffectRule ?? "None"}");
             Console.WriteLine($"  Entrypoint Rule: {policyInfo.EntrypointRule}");
-            
+
             Console.WriteLine($"  Module IDs ({policyInfo.ModuleIds.Count}):");
             foreach (var moduleId in policyInfo.ModuleIds)
             {
                 Console.WriteLine($"    - {moduleId}");
             }
-            
+
             Console.WriteLine($"  Applicable Resource Types ({policyInfo.ApplicableResourceTypes.Count}):");
             foreach (var resourceType in policyInfo.ApplicableResourceTypes)
             {
                 Console.WriteLine($"    - {resourceType}");
             }
-            
+
             if (policyInfo.Parameters != null && policyInfo.Parameters.Count > 0)
             {
                 Console.WriteLine($"  Policy Parameters:");
@@ -333,7 +335,7 @@ allow if {
                             Console.WriteLine($"          Description: {param.Description}");
                         }
                     }
-                    
+
                     if (parameterSet.Modifiers.Count > 0)
                     {
                         Console.WriteLine($"      Modifiers ({parameterSet.Modifiers.Count}):");
@@ -348,11 +350,11 @@ allow if {
             {
                 Console.WriteLine("  No parameter information available");
             }
-            
+
             // Demonstrate JSON serialization of policy info
             Console.WriteLine("\n✓ Policy Info as JSON:");
-            var jsonOptions = new JsonSerializerOptions 
-            { 
+            var jsonOptions = new JsonSerializerOptions
+            {
                 WriteIndented = true,
                 PropertyNamingPolicy = JsonNamingPolicy.CamelCase
             };

bindings/csharp/TestApp/Program.cs

@@ -42,7 +42,8 @@ w.Restart();
 
 // Set input and eval rule.
 engine.SetInputFromJsonFile("../../../tests/aci/input.json");
-var value = engine.EvalRule("data.framework.mount_overlay");
+var value = engine.EvalRule("data.framework.mount_overlay")
+    ?? throw new System.InvalidOperationException("Expected EvalRule to return a JSON value.");
 
 #if NET8_0_OR_GREATER
 var valueDoc = System.Text.Json.JsonDocument.Parse(value);

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"
+  }
 }

bindings/ffi/Cargo.lock

@@ -950,7 +950,7 @@ checksum = "7a2d987857b319362043e95f5353c0535c1f58eec5336fdfcf626430af7def58"
 
 [[package]]
 name = "regorus"
-version = "0.9.0"
+version = "0.9.1"
 dependencies = [
  "anyhow",
  "bincode",
@@ -981,7 +981,7 @@ dependencies = [
 
 [[package]]
 name = "regorus-ffi"
-version = "0.9.0"
+version = "0.9.1"
 dependencies = [
  "anyhow",
  "cbindgen",

bindings/ffi/Cargo.toml

@@ -2,8 +2,9 @@
 
 [package]
 name = "regorus-ffi"
-version = "0.9.0"
+version = "0.9.1"
 edition = "2021"
+license = "MIT AND Apache-2.0 AND BSD-3-Clause"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 [lib]

bindings/java/Cargo.lock

@@ -826,7 +826,7 @@ checksum = "7a2d987857b319362043e95f5353c0535c1f58eec5336fdfcf626430af7def58"
 
 [[package]]
 name = "regorus"
-version = "0.9.0"
+version = "0.9.1"
 dependencies = [
  "anyhow",
  "bincode",
@@ -856,7 +856,7 @@ dependencies = [
 
 [[package]]
 name = "regorus-java"
-version = "0.9.0"
+version = "0.9.1"
 dependencies = [
  "anyhow",
  "jni",

bindings/java/Cargo.toml

@@ -2,10 +2,11 @@
 
 [package]
 name = "regorus-java"
-version = "0.9.0"
+version = "0.9.1"
 edition = "2021"
 repository = "https://github.com/microsoft/regorus/bindings/java"
 description = "Java bindings for Regorus - a fast, lightweight Rego interpreter written in Rust"
+license = "MIT AND Apache-2.0 AND BSD-3-Clause"
 keywords = ["interpreter", "opa", "policy-as-code", "rego"]
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

bindings/java/pom.xml

@@ -9,7 +9,7 @@
 
   <groupId>com.microsoft.regorus</groupId>
   <artifactId>regorus-java</artifactId>
-  <version>0.9.0</version>
+  <version>0.9.1</version>
 
   <name>Regorus Java</name>
   <description>Java bindings for Regorus - a fast, lightweight Rego interpreter written in Rust</description>
@@ -18,7 +18,15 @@
   <licenses>
     <license>
       <name>MIT License</name>
-      <url>https://opensource.org/blog/license/mit</url>
+      <url>https://opensource.org/licenses/MIT</url>
+    </license>
+    <license>
+      <name>Apache License 2.0</name>
+      <url>https://www.apache.org/licenses/LICENSE-2.0</url>
+    </license>
+    <license>
+      <name>BSD 3-Clause License</name>
+      <url>https://opensource.org/licenses/BSD-3-Clause</url>
     </license>
   </licenses>
 
@@ -40,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>
@@ -68,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 -->
@@ -89,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>
@@ -100,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>
@@ -115,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>

bindings/python/Cargo.lock

@@ -885,7 +885,7 @@ checksum = "7a2d987857b319362043e95f5353c0535c1f58eec5336fdfcf626430af7def58"
 
 [[package]]
 name = "regorus"
-version = "0.9.0"
+version = "0.9.1"
 dependencies = [
  "anyhow",
  "bincode",
@@ -929,7 +929,7 @@ dependencies = [
 
 [[package]]
 name = "regoruspy"
-version = "0.9.0"
+version = "0.9.1"
 dependencies = [
  "anyhow",
  "ordered-float",

bindings/python/Cargo.toml

@@ -2,10 +2,11 @@
 
 [package]
 name = "regoruspy"
-version = "0.9.0"
+version = "0.9.1"
 edition = "2021"
 repository = "https://github.com/microsoft/regorus/bindings/python"
 description = "Python bindings for Regorus - a fast, lightweight Rego interpreter written in Rust"
+license = "MIT AND Apache-2.0 AND BSD-3-Clause"
 keywords = ["interpreter", "opa", "policy-as-code", "rego"]
 
 

bindings/python/pyproject.toml

@@ -5,7 +5,11 @@ build-backend = "maturin"
 [project]
 name = "regorus"
 requires-python = ">=3.8"
+license = { text = "MIT AND Apache-2.0 AND BSD-3-Clause" }
 classifiers = [
+    "License :: OSI Approved :: Apache Software License",
+    "License :: OSI Approved :: BSD License",
+    "License :: OSI Approved :: MIT License",
     "Programming Language :: Rust",
     "Programming Language :: Python :: Implementation :: CPython",
     "Programming Language :: Python :: Implementation :: PyPy",

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"

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

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

bindings/ruby/ext/regorusrb/Cargo.toml

@@ -1,8 +1,9 @@
 [package]
 name = "regorusrb"
-version = "0.9.0"
+version = "0.9.1"
 edition = "2024"
 description = "Ruby bindings for Regorus - a fast, lightweight Rego interpreter written in Rust"
+license = "MIT AND Apache-2.0 AND BSD-3-Clause"
 publish = false
 
 [lib]
@@ -15,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"

bindings/ruby/lib/regorus/version.rb

@@ -1,5 +1,5 @@
 # frozen_string_literal: true
 
 module Regorus
-  VERSION = "0.9.0"
+  VERSION = "0.9.1"
 end

bindings/ruby/regorusrb.gemspec

@@ -9,7 +9,7 @@ Gem::Specification.new do |spec|
 
   spec.summary = "Ruby bindings for Regorus - a fast, lightweight Rego interpreter written in Rust"
   spec.homepage = "https://github.com/microsoft/regorus/blob/main/bindings/ruby"
-  spec.license = "MIT"
+  spec.licenses = ["MIT", "Apache-2.0", "BSD-3-Clause"]
   spec.required_ruby_version = ">= 3.4.2"
   spec.required_rubygems_version = ">= 3.6.5"
 

bindings/wasm/Cargo.lock

@@ -883,7 +883,7 @@ checksum = "7a2d987857b319362043e95f5353c0535c1f58eec5336fdfcf626430af7def58"
 
 [[package]]
 name = "regorus"
-version = "0.9.0"
+version = "0.9.1"
 dependencies = [
  "anyhow",
  "bincode",
@@ -912,7 +912,7 @@ dependencies = [
 
 [[package]]
 name = "regorusjs"
-version = "0.9.0"
+version = "0.9.1"
 dependencies = [
  "getrandom 0.2.17",
  "getrandom 0.3.4",

bindings/wasm/Cargo.toml

@@ -2,10 +2,11 @@
 
 [package]
 name = "regorusjs"
-version = "0.9.0"
+version = "0.9.1"
 edition = "2021"
 repository = "https://github.com/microsoft/regorus/bindings/wasm"
 description = "WASM bindings for Regorus - a fast, lightweight Rego interpreter written in Rust"
+license = "MIT AND Apache-2.0 AND BSD-3-Clause"
 keywords = ["interpreter", "opa", "policy-as-code", "rego"]
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

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,
+    {
+    }
+}

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")]

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)

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)

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!

src/verusspec/mod.rs

@@ -0,0 +1,3 @@
+pub(crate) mod bigint;
+pub(crate) mod float;
+pub(crate) mod utils;

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!

tests/interpreter/cases/arithmetic/mod.rs

@@ -27,6 +27,34 @@ fn basic() -> Result<()> {
     div {
       21 / 5 == 4.2
     }
+
+    eq1 { 1 == 1.0 }
+    eq2 { 1 == 1.00 }
+    neq1 { 1 != 1.0001 }
+
+    sum { 0.1 + 0.2 == 0.3 }
+    diff { 0.3 - 0.2 == 0.1 }
+    product { 0.1 * 0.2 == 0.02 }
+    quotient { 0.3 / 0.1 == 3.0 }
+
+    lt { 1 < 1.0001 }
+    le { 1 <= 1.0 }
+    gt { 1.0001 > 1 }
+    ge { 1.0 >= 1 }
+    neg_lt { -1 < 0 }
+    neg_le { -1 <= -1 }
+
+    div1 { 1 / 2 == 0.5 }
+    div2 { 5 / 2 == 2.5 }
+
+    neg1 { -1 == -1 }
+    neg2 { -1 + 2 == 1 }
+    neg3 { -(2 + 3) == -5 }
+    neg4 { 1 - -1 == 2 }
+
+    big1 { 1000000000000000000000 + 1 == 1000000000000000000001 }
+    big2 { 2 * 1000000000000000000000 == 2000000000000000000000 }
+    big3 { 2 / 1e18 == 2e-18 }
 "#;
 
     let expected = vec![Value::from_json_str(
@@ -34,7 +62,29 @@ fn basic() -> Result<()> {
     "add" : true,
     "sub" : true,
     "mul" : true,
-    "div" : true
+    "div" : true,
+    "eq1": true,
+    "eq2": true,
+    "neq1": true,
+    "sum": true,
+    "diff": true,
+    "product": true,
+    "quotient": true,
+    "lt": true,
+    "le": true,
+    "gt": true,
+    "ge": true,
+    "neg_lt": true,
+    "neg_le": true,
+    "div1": true,
+    "div2": true,
+    "neg1": true,
+    "neg2": true,
+    "neg3": true,
+    "neg4": true,
+    "big1": true,
+    "big2": true,
+    "big3": true
 }"#,
     )?];
 

tests/interpreter/cases/arithmetic/tests.yaml

@@ -19,3 +19,100 @@ cases:
       c: 1
       d: -2
     
+  - note: integer-float-equality
+    data: {}
+    modules:
+      - |
+        package test
+
+        eq1 = 1 == 1.0
+        eq2 = 1 == 1.00
+        neq1 = 1 != 1.0001
+    query: data.test
+    want_result:
+      eq1: true
+      eq2: true
+      neq1: true
+
+  - note: float-precision
+    data: {}
+    modules:
+      - |
+        package test
+
+        sum = 0.1 + 0.2
+        diff = 0.3 - 0.2
+        product = 0.1 * 0.2
+        quotient = 0.3 / 0.1
+    query: data.test
+    want_result:
+      sum: 0.30000000000000004
+      diff: 0.09999999999999998
+      product: 0.020000000000000004
+      quotient: 2.9999999999999996
+
+  - note: numeric-comparisons
+    data: {}
+    modules:
+      - |
+        package test
+
+        lt = 1 < 1.0001
+        le = 1 <= 1.0
+        gt = 1.0001 > 1
+        ge = 1.0 >= 1
+        neg_lt = -1 < 0
+        neg_le = -1 <= -1
+    query: data.test
+    want_result:
+      lt: true
+      le: true
+      gt: true
+      ge: true
+      neg_lt: true
+      neg_le: true
+
+  - note: division
+    data: {}
+    modules:
+      - |
+        package test
+
+        div1 = 1 / 2
+        div2 = 5 / 2
+    query: data.test
+    want_result:
+      div1: 0.5
+      div2: 2.5
+
+  - note: negative-number-arithmetic
+    data: {}
+    modules:
+      - |
+        package test
+
+        neg1 = -1
+        neg2 = -1 + 2
+        neg3 = 0 - (2 + 3)
+        neg4 = 1 - -1
+    query: data.test
+    want_result:
+      neg1: -1
+      neg2: 1
+      neg3: -5
+      neg4: 2
+
+  - note: big-numbers
+    data: {}
+    modules:
+      - |
+        package test
+
+        big1 = 1000000000000000000000 + 1
+        big2 = 2 * 1000000000000000000000
+        big3 = 2 / 1e18
+    query: data.test
+    want_result:
+      big1: 1000000000000000000001
+      big2: 2000000000000000000000
+      big3: 2e-18

xtask/src/tasks/bindings/all.rs

@@ -36,6 +36,8 @@ impl BuildAllBindingsCommand {
             clean: false,
             artifacts_dir: Some(ffi_dir.clone()),
             enforce_artifacts: false,
+            repository_commit: None,
+            include_symbols: false,
         })?;
 
         if nuget_result.packages.is_empty() {
@@ -133,6 +135,9 @@ impl TestAllBindingsCommand {
             enforce_artifacts: false,
             force_nuget: false,
             nuget_dir: None,
+            test_filter: None,
+            skip_apps: false,
+            console_logger: false,
         }
         .run()?;
 

xtask/src/tasks/bindings/csharp.rs

@@ -35,6 +35,14 @@ pub struct BuildNugetCommand {
     /// Require all platform artefacts to exist before packing.
     #[arg(long)]
     pub enforce_artifacts: bool,
+
+    /// Include repository commit metadata in the package.
+    #[arg(long = "repository-commit", value_name = "SHA")]
+    pub repository_commit: Option<String>,
+
+    /// Build a symbols package (snupkg).
+    #[arg(long)]
+    pub include_symbols: bool,
 }
 
 /// Parsed build options shared across tasks that need a NuGet package.
@@ -45,6 +53,8 @@ pub struct BuildNugetConfig {
     pub clean: bool,
     pub artifacts_dir: Option<PathBuf>,
     pub enforce_artifacts: bool,
+    pub repository_commit: Option<String>,
+    pub include_symbols: bool,
 }
 
 /// Result of a NuGet build, including generated artefacts.
@@ -86,6 +96,8 @@ pub fn build_nuget_package(config: &BuildNugetConfig) -> Result<BuildNugetResult
         &profile,
         !config.enforce_artifacts,
         config.clean,
+        config.repository_commit.as_deref(),
+        config.include_symbols,
     )?;
 
     let packages = find_packages(&package_dir)?;
@@ -132,6 +144,8 @@ fn invoke_dotnet_pack(
     profile: &str,
     ignore_missing: bool,
     clean: bool,
+    repository_commit: Option<&str>,
+    include_symbols: bool,
 ) -> Result<PathBuf> {
     let project_dir = root.join("bindings/csharp/Regorus");
     let artifacts_dir_str = artifacts_dir
@@ -140,6 +154,12 @@ fn invoke_dotnet_pack(
 
     let profile_arg = format!("/p:RegorusFFIArtifactsProfile={}", profile);
     let dir_arg = format!("/p:RegorusFFIArtifactsDir={}", artifacts_dir_str);
+    let repo_commit_arg = repository_commit.map(|sha| format!("/p:RepositoryCommit={}", sha));
+    let symbols_args = if include_symbols {
+        Some(("/p:IncludeSymbols=true", "/p:SymbolPackageFormat=snupkg"))
+    } else {
+        None
+    };
 
     if clean {
         clean_msbuild_project(&project_dir)?;
@@ -169,6 +189,9 @@ fn invoke_dotnet_pack(
     build.arg("minimal");
     build.arg(&dir_arg);
     build.arg(&profile_arg);
+    if let Some(arg) = &repo_commit_arg {
+        build.arg(arg);
+    }
     if ignore_missing {
         build.arg("/p:IgnoreMissingArtifacts=true");
     }
@@ -182,6 +205,13 @@ fn invoke_dotnet_pack(
     pack.arg(configuration);
     pack.arg(&dir_arg);
     pack.arg(&profile_arg);
+    if let Some(arg) = &repo_commit_arg {
+        pack.arg(arg);
+    }
+    if let Some((include_symbols_arg, symbols_format_arg)) = symbols_args {
+        pack.arg(include_symbols_arg);
+        pack.arg(symbols_format_arg);
+    }
     if ignore_missing {
         pack.arg("/p:IgnoreMissingArtifacts=true");
     }
@@ -217,6 +247,8 @@ impl BuildNugetCommand {
             clean: self.clean,
             artifacts_dir: self.artifacts_dir.clone(),
             enforce_artifacts: self.enforce_artifacts,
+            repository_commit: self.repository_commit.clone(),
+            include_symbols: self.include_symbols,
         }
     }
 }
@@ -276,6 +308,18 @@ pub struct TestCsharpCommand {
     /// Restore and test using Regorus NuGet artefacts located at DIR. Defaults to bindings/csharp/Regorus/bin/<configuration>.
     #[arg(long = "nuget-dir", value_name = "DIR")]
     pub nuget_dir: Option<PathBuf>,
+
+    /// Optional dotnet test filter to apply when running Regorus.Tests.
+    #[arg(long = "test-filter", value_name = "FILTER")]
+    pub test_filter: Option<String>,
+
+    /// Skip building/running the C# sample apps (TestApp, TargetExampleApp).
+    #[arg(long = "skip-apps")]
+    pub skip_apps: bool,
+
+    /// Emit console logger output for dotnet test.
+    #[arg(long = "console-logger")]
+    pub console_logger: bool,
 }
 
 impl TestCsharpCommand {
@@ -307,6 +351,8 @@ impl TestCsharpCommand {
             clean: self.clean,
             artifacts_dir: self.artifacts_dir.clone(),
             enforce_artifacts: self.enforce_artifacts,
+            repository_commit: None,
+            include_symbols: false,
         };
 
         let mut packages = find_packages(&package_dir)?;
@@ -378,6 +424,9 @@ impl TestCsharpCommand {
             &package_dir,
             self.clean,
             &package_cache,
+            self.test_filter.as_deref(),
+            self.skip_apps,
+            self.console_logger,
         )?;
 
         Ok(())
@@ -390,6 +439,9 @@ fn run_regorus_tests(
     package_dir: &Path,
     clean: bool,
     package_cache: &Path,
+    test_filter: Option<&str>,
+    skip_apps: bool,
+    console_logger: bool,
 ) -> Result<()> {
     let nuget_source = package_dir
         .to_str()
@@ -423,9 +475,22 @@ fn run_regorus_tests(
     test.arg(configuration);
     test.arg("--arch");
     test.arg(dotnet_host_arch());
+    if console_logger {
+        test.arg("--logger");
+        test.arg("console;verbosity=detailed");
+    }
+    if let Some(filter) = test_filter {
+        test.arg("--");
+        test.arg("--filter");
+        test.arg(filter);
+    }
     test.env("NUGET_PACKAGES", package_cache);
     run_command(test, "dotnet test (Regorus.Tests)")?;
 
+    if skip_apps {
+        return Ok(());
+    }
+
     let test_app = workspace.join("bindings/csharp/TestApp");
     if clean {
         clean_msbuild_project(&test_app)?;