chore: add test suite, clean up third_party, update CI

.github/workflows/ci.yml

@@ -95,22 +95,15 @@ jobs:
         bazel build @rocq_of_rust_source//:rocq_of_rust_main
         echo "RocqOfRust library built"
 
-    - name: Build example proofs
+    - name: Run tests
       run: |
-        echo "Building example proofs..."
-        bazel build //examples/rust_to_rocq:point_proofs
-        echo "Example proofs verified"
-
-    - name: Build advanced example
-      run: |
-        echo "Building advanced Rust features example..."
-        bazel build //examples/rust_to_rocq:advanced_verified
-        echo "Advanced example verified"
+        echo "Running all tests..."
+        bazel test //examples/rust_to_rocq:all //tests:all --test_output=errors
+        echo "All tests passed"
 
     - name: Collect verified artifacts
       run: |
         mkdir -p verified-artifacts
-        # Copy compiled proof files
         find bazel-bin/examples -name "*.vo" -exec cp {} verified-artifacts/ \;
         find bazel-bin/examples -name "*.v" -exec cp {} verified-artifacts/ \;
         ls -la verified-artifacts/
@@ -155,17 +148,11 @@ jobs:
         restore-keys: |
           bazel-build-${{ runner.os }}-
 
-    - name: Build example proofs
-      run: |
-        echo "Building example proofs on macOS..."
-        bazel build //examples/rust_to_rocq:point_proofs
-        echo "Example proofs verified on macOS"
-
-    - name: Build advanced example
+    - name: Run tests
       run: |
-        echo "Building advanced Rust features example..."
-        bazel build //examples/rust_to_rocq:advanced_verified
-        echo "Advanced example verified"
+        echo "Running all tests on macOS..."
+        bazel test //examples/rust_to_rocq:all //tests:all --test_output=errors
+        echo "All tests passed on macOS"
 
     - name: Collect verified artifacts
       run: |

.gitignore

@@ -5,3 +5,4 @@ bazel-testlogs
 bazel-loom
 .claude/
 MODULE.bazel.lock
+third_party/

tests/BUILD.bazel

@@ -0,0 +1,71 @@
+# Integration tests for rules_rocq_rust
+#
+# These tests verify the full Rust → Rocq translation and compilation pipeline.
+
+load("@rules_rocq_rust//coq_of_rust:defs.bzl", "coq_of_rust_library", "rocq_rust_verified_library")
+load("@rules_rocq_rust//rocq:defs.bzl", "rocq_proof_test")
+
+# =============================================
+# Test 1: Minimal translation + compilation
+# =============================================
+# Verifies the simplest possible Rust file translates and compiles.
+
+rocq_rust_verified_library(
+    name = "minimal_verified",
+    rust_sources = ["minimal.rs"],
+    edition = "2021",
+    extra_flags = ["-impredicative-set"],
+)
+
+rocq_proof_test(
+    name = "minimal_test",
+    srcs = [],
+    deps = [":minimal_verified"],
+)
+
+# =============================================
+# Test 2: Enum translation
+# =============================================
+# Verifies enum variants (unit, tuple) translate correctly.
+
+rocq_rust_verified_library(
+    name = "enums_verified",
+    rust_sources = ["enums.rs"],
+    edition = "2021",
+    extra_flags = ["-impredicative-set"],
+)
+
+rocq_proof_test(
+    name = "enums_test",
+    srcs = [],
+    deps = [":enums_verified"],
+)
+
+# =============================================
+# Test 3: Impl methods
+# =============================================
+# Verifies struct with impl block translates correctly.
+
+rocq_rust_verified_library(
+    name = "impl_methods_verified",
+    rust_sources = ["impl_methods.rs"],
+    edition = "2021",
+    extra_flags = ["-impredicative-set"],
+)
+
+rocq_proof_test(
+    name = "impl_methods_test",
+    srcs = [],
+    deps = [":impl_methods_verified"],
+)
+
+# =============================================
+# Test 4: Translation step only
+# =============================================
+# Verifies coq_of_rust_library produces .v output without compilation.
+
+coq_of_rust_library(
+    name = "minimal_translated",
+    rust_sources = ["minimal.rs"],
+    edition = "2021",
+)

tests/enums.rs

@@ -0,0 +1,14 @@
+/// Test enum translation with variants.
+pub enum Color {
+    Red,
+    Green,
+    Blue,
+    Custom(u8, u8, u8),
+}
+
+pub fn is_red(c: &Color) -> bool {
+    match c {
+        Color::Red => true,
+        _ => false,
+    }
+}

tests/impl_methods.rs

@@ -0,0 +1,20 @@
+/// Test struct with impl block methods.
+pub struct Counter {
+    pub value: u32,
+}
+
+impl Counter {
+    pub fn new() -> Self {
+        Counter { value: 0 }
+    }
+
+    pub fn increment(&self) -> Self {
+        Counter {
+            value: self.value + 1,
+        }
+    }
+
+    pub fn get(&self) -> u32 {
+        self.value
+    }
+}

tests/minimal.rs

@@ -0,0 +1,4 @@
+/// Minimal Rust code for testing the translation pipeline.
+pub fn identity(x: i32) -> i32 {
+    x
+}