feat: Replace C FFI with rust-bindgen

.github/workflows/ci.yml

@@ -17,52 +17,37 @@ jobs:
   lean-test:
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
+      - uses: actions-rust-lang/setup-rust-toolchain@v1
       - uses: leanprover/lean-action@v1
         with:
           build-args: "--wfail -v"
-          test: true
-      - name: Build all targets
-        run: lake run build-all --wfail
       - name: Test Ix CLI
         run: lake test -- cli
       - name: Aiur tests
         run: lake test -- --ignored aiur aiur-hashes ixvm
-      - name: Check lean.h.hash
-        run: lake run check-lean-h-hash
       - name: Check Lean versions match for Ix and compiler bench
         run: diff lean-toolchain Benchmarks/Compile/lean-toolchain
 
   rust-test:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v6
-        with:
-          repository: argumentcomputer/ci-workflows
-      - uses: ./.github/actions/ci-env
-      - uses: actions/checkout@v6
-      - uses: dtolnay/rust-toolchain@stable
+      - uses: actions-rust-lang/setup-rust-toolchain@v1
       - uses: taiki-e/install-action@nextest
-      - uses: Swatinem/rust-cache@v2
-      - name: Tests
-        run: cargo nextest run --release --profile ci --workspace --run-ignored all
-
-  rust-lint:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v6
+      # Install Lean for rust-bindgen step
+      - uses: leanprover/lean-action@v1
         with:
-          repository: argumentcomputer/ci-workflows
-      - uses: ./.github/actions/ci-env
-      - uses: actions/checkout@v6
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+          auto-config: false
+          use-github-cache: false
       - name: Check Rustfmt code style
-        run: cargo fmt --all --check
+        uses: actions-rust-lang/rustfmt@v1
+      - name: Check clippy warnings
+        run: cargo xclippy
       - name: Check *everything* compiles
         run: cargo check --all-targets --all-features --workspace
-      - name: Check clippy warnings
-        run: cargo xclippy -D warnings
+      - name: Tests
+        run: cargo nextest run --release --profile ci --workspace --run-ignored all
       - name: Get Rust version
         run: |
           echo "RUST_VERSION=$(awk -F '"' '/^channel/ {print $2}' rust-toolchain.toml)" | tee -a $GITHUB_ENV

.github/workflows/compile.yml

@@ -20,8 +20,9 @@ jobs:
       - uses: actions/checkout@v6
       - uses: leanprover/lean-action@v1
         with:
+          auto-config: false
+          build: true
           build-args: "ix --wfail -v"
-          test: false
       - run: |
           mkdir -p ~/.local/bin
           echo | lake run install
@@ -56,7 +57,7 @@ jobs:
       - uses: leanprover/lean-action@v1
         with:
           lake-package-directory: ${{ env.COMPILE_DIR }}
-          build: false
+          auto-config: false
           use-github-cache: false
       # FLT and FC take a few minutes to rebuild, so we cache the build artifacts
       - if: matrix.cache_pkg

.github/workflows/ignored.yml

@@ -0,0 +1,47 @@
+name: Extended CI tests
+
+on:
+  push:
+    branches: main
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
+
+jobs:
+  ignored-test:
+    runs-on: warp-ubuntu-latest-x64-32x # Needs 128 GB RAM for Lean compilation
+    steps:
+      - uses: actions/checkout@v6
+      - uses: actions-rust-lang/setup-rust-toolchain@v1
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          test: true
+          test-args: "-- --ignored"
+
+  valgrind:
+    runs-on: warp-ubuntu-latest-x64-16x
+    steps:
+      - uses: actions/checkout@v6
+      - uses: actions-rust-lang/setup-rust-toolchain@v1
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          build: true
+          build-args: "IxTests"
+      - name: Install valgrind
+        run: sudo apt-get update && sudo apt-get install -y valgrind
+      - name: Run tests under valgrind
+        run: |
+          valgrind \
+            --leak-check=full \
+            --show-leak-kinds=definite,possible \
+            --errors-for-leak-kinds=definite \
+            --track-origins=yes \
+            --error-exitcode=1 \
+            .lake/build/bin/IxTests -- --include-ignored aiur aiur-hashes ixvm

Cargo.toml

@@ -1,3 +1,6 @@
+[workspace]
+members = ["lean-ffi"]
+
 [package]
 name = "ix_rs"
 version = "0.1.0"
@@ -11,6 +14,7 @@ anyhow = "1"
 blake3 = "1.8.2"
 itertools = "0.14.0"
 indexmap = { version = "2", features = ["rayon"] }
+lean-ffi = { path = "lean-ffi" }
 multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "14b70601317e4500c7246c32a13ad08b3f560f2e" }
 num-bigint = "0.4.6"
 rayon = "1"
@@ -31,7 +35,6 @@ tracing-subscriber = { version = "0.3", features = ["env-filter"], optional = tr
 bincode = { version = "2.0.1", optional = true }
 serde = { version = "1.0.219", features = ["derive"], optional = true }
 
-
 [dev-dependencies]
 quickcheck = "1.0.3"
 rand = "0.8.5"