bloomberg · CharlesCNorton · Feb 25, 2026
diff --git a/scripts/run-diff-tests.sh b/scripts/run-diff-tests.sh
@@ -0,0 +1,124 @@
+#!/bin/bash
+# Differential testing: Crane C++ vs Rocq OCaml extraction
+# Compiles both sides, runs both, diffs output.
+set -e
+
+SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
+PROJECT_ROOT="$(cd "$SCRIPT_DIR/.." && pwd)"
+BASICS="$PROJECT_ROOT/tests/basics"
+
+PASS=0
+FAIL=0
+ERRORS=""
+
+# Build all .vo files (triggers both Crane and OCaml extraction)
+echo "=== Building with dune ==="
+cd "$PROJECT_ROOT"
+eval $(opam env --switch=default --set-switch)
+dune build tests/basics 2>&1
+
+# Second pass: Crane writes .cpp/.h to source tree during coqc;
+# dune's (source_tree .) snapshots before build, so generated files
+# aren't visible until the second build.
+dune build tests/basics 2>&1
+
+run_diff_test() {
+    local name="$1"
+    local subdir="$2"
+    local ocaml_module="$3"  # extracted .ml basename (without .ml)
+    local cpp_exe="$subdir/${name}.d.exe"
+    local build_dir="_build/default/tests/basics"
+
+    echo ""
+    echo "--- $name ---"
+
+    # Build C++ diff harness
+    if [ ! -f "$build_dir/$subdir/${name}.d.exe" ]; then
+        echo "  Building C++ diff harness..."
+        dune build "tests/basics/$subdir/${name}.d.exe" 2>&1
+    fi
+
+    # Find the extracted OCaml .ml file
+    # OCaml Extraction writes to the theory root (tests/basics/), not the subdir
+    local ml_file="$BASICS/${ocaml_module}.ml"
+    local mli_file="$BASICS/${ocaml_module}.mli"
+    local ml_harness="$BASICS/$subdir/${name}.d.ml"
+
+    if [ ! -f "$ml_file" ]; then
+        echo "  ERROR: extracted $ml_file not found"
+        FAIL=$((FAIL + 1))
+        ERRORS="$ERRORS\n  $name: missing $ml_file"
+        return
+    fi
+
+    if [ ! -f "$ml_harness" ]; then
+        echo "  ERROR: OCaml harness $ml_harness not found"
+        FAIL=$((FAIL + 1))
+        ERRORS="$ERRORS\n  $name: missing $ml_harness"
+        return
+    fi
+
+    # Compile OCaml side
+    echo "  Compiling OCaml..."
+    local ocaml_build_dir="$BASICS/$subdir/_ocaml_diff"
+    mkdir -p "$ocaml_build_dir"
+
+    # Compile .mli -> .cmi if it exists
+    if [ -f "$mli_file" ]; then
+        ocamlfind ocamlopt -package stdlib-shims -I "$ocaml_build_dir" \
+            -c "$mli_file" -o "$ocaml_build_dir/${ocaml_module}.cmi" 2>&1
+    fi
+
+    # Compile extracted .ml -> .cmx
+    ocamlfind ocamlopt -package stdlib-shims -I "$ocaml_build_dir" \
+        -c "$ml_file" -o "$ocaml_build_dir/${ocaml_module}.cmx" 2>&1
+
+    # Compile harness .ml -> .cmx
+    ocamlfind ocamlopt -package stdlib-shims -I "$ocaml_build_dir" \
+        -c "$ml_harness" -o "$ocaml_build_dir/${name}.d.cmx" 2>&1
+
+    # Link
+    ocamlfind ocamlopt -package stdlib-shims -linkpkg \
+        "$ocaml_build_dir/${ocaml_module}.cmx" \
+        "$ocaml_build_dir/${name}.d.cmx" \
+        -o "$ocaml_build_dir/${name}.d.ocaml" 2>&1
+
+    # Run both
+    echo "  Running C++..."
+    local cpp_out
+    cpp_out=$("$build_dir/$subdir/${name}.d.exe" 2>&1)
+
+    echo "  Running OCaml..."
+    local ml_out
+    ml_out=$("$ocaml_build_dir/${name}.d.ocaml" 2>&1)
+
+    # Diff
+    if [ "$cpp_out" = "$ml_out" ]; then
+        echo "  PASS"
+        PASS=$((PASS + 1))
+    else
+        echo "  FAIL: output differs"
+        echo "  C++:"
+        echo "$cpp_out" | sed 's/^/    /'
+        echo "  OCaml:"
+        echo "$ml_out" | sed 's/^/    /'
+        FAIL=$((FAIL + 1))
+        ERRORS="$ERRORS\n  $name: output mismatch"
+    fi
+}
+
+# Run differential tests
+# Args: test_name subdir ocaml_module_basename
+run_diff_test "ack" "ack" "ack_ocaml"
+run_diff_test "mutual_mod" "mutual_mod" "mutual_mod_ocaml"
+run_diff_test "module" "module" "module_ocaml"
+
+# Summary
+echo ""
+echo "=== Differential Test Results ==="
+echo "  Passed: $PASS"
+echo "  Failed: $FAIL"
+if [ $FAIL -gt 0 ]; then
+    echo -e "  Errors:$ERRORS"
+    exit 1
+fi
diff --git a/tests/basics/ack/Ack.v b/tests/basics/ack/Ack.v
@@ -20,5 +20,6 @@ Require Crane.Mapping.Std.
 Require Crane.Mapping.NatIntStd.
 Crane Extraction "ack" Ack.
 
-(* Require Extraction. *)
-(* Extraction "ack.ml" Ack. *)
+(* OCaml extraction for differential testing *)
+From Stdlib Require Extraction ExtrOcamlBasic ExtrOcamlNatInt.
+Extraction "ack_ocaml.ml" Ack.ack.
diff --git a/tests/basics/ack/ack.d.cpp b/tests/basics/ack/ack.d.cpp
@@ -0,0 +1,21 @@
+// Differential test harness: prints canonical output for diffing against OCaml
+#include <ack.h>
+#include <cstdio>
+int main() {
+    printf("ack(0,0)=%u\n", Ack::ack(0, 0));
+    printf("ack(0,1)=%u\n", Ack::ack(0, 1));
+    printf("ack(0,5)=%u\n", Ack::ack(0, 5));
+    printf("ack(1,0)=%u\n", Ack::ack(1, 0));
+    printf("ack(1,1)=%u\n", Ack::ack(1, 1));
+    printf("ack(1,5)=%u\n", Ack::ack(1, 5));
+    printf("ack(2,0)=%u\n", Ack::ack(2, 0));
+    printf("ack(2,1)=%u\n", Ack::ack(2, 1));
+    printf("ack(2,2)=%u\n", Ack::ack(2, 2));
+    printf("ack(2,4)=%u\n", Ack::ack(2, 4));
+    printf("ack(3,0)=%u\n", Ack::ack(3, 0));
+    printf("ack(3,1)=%u\n", Ack::ack(3, 1));
+    printf("ack(3,2)=%u\n", Ack::ack(3, 2));
+    printf("ack(3,3)=%u\n", Ack::ack(3, 3));
+    printf("ack(3,7)=%u\n", Ack::ack(3, 7));
+    return 0;
+}
diff --git a/tests/basics/ack/ack.d.ml b/tests/basics/ack/ack.d.ml
@@ -0,0 +1,17 @@
+(* Differential test harness: prints canonical output for diffing against C++ *)
+let () =
+  Printf.printf "ack(0,0)=%d\n" (Ack_ocaml.Ack.ack 0 0);
+  Printf.printf "ack(0,1)=%d\n" (Ack_ocaml.Ack.ack 0 1);
+  Printf.printf "ack(0,5)=%d\n" (Ack_ocaml.Ack.ack 0 5);
+  Printf.printf "ack(1,0)=%d\n" (Ack_ocaml.Ack.ack 1 0);
+  Printf.printf "ack(1,1)=%d\n" (Ack_ocaml.Ack.ack 1 1);
+  Printf.printf "ack(1,5)=%d\n" (Ack_ocaml.Ack.ack 1 5);
+  Printf.printf "ack(2,0)=%d\n" (Ack_ocaml.Ack.ack 2 0);
+  Printf.printf "ack(2,1)=%d\n" (Ack_ocaml.Ack.ack 2 1);
+  Printf.printf "ack(2,2)=%d\n" (Ack_ocaml.Ack.ack 2 2);
+  Printf.printf "ack(2,4)=%d\n" (Ack_ocaml.Ack.ack 2 4);
+  Printf.printf "ack(3,0)=%d\n" (Ack_ocaml.Ack.ack 3 0);
+  Printf.printf "ack(3,1)=%d\n" (Ack_ocaml.Ack.ack 3 1);
+  Printf.printf "ack(3,2)=%d\n" (Ack_ocaml.Ack.ack 3 2);
+  Printf.printf "ack(3,3)=%d\n" (Ack_ocaml.Ack.ack 3 3);
+  Printf.printf "ack(3,7)=%d\n" (Ack_ocaml.Ack.ack 3 7)
diff --git a/tests/basics/dune b/tests/basics/dune
@@ -20,7 +20,12 @@
  (rule
   (alias runtest)
   (deps ack.t.exe)
-  (action (run ./ack.t.exe))))
+  (action (run ./ack.t.exe)))
+ (rule
+  (targets ack.d.exe)
+  (deps Ack.vo ack.d.cpp (source_tree .))
+  (action
+   (run %{project_root}/scripts/compile-std.sh %{project_root} ack.d.exe ack.cpp ack.d.cpp))))
 
 (subdir binom
  (rule
@@ -86,7 +91,12 @@
  (rule
   (alias runtest)
   (deps module.t.exe)
-  (action (run ./module.t.exe))))
+  (action (run ./module.t.exe)))
+ (rule
+  (targets module.d.exe)
+  (deps Module.vo module.d.cpp (source_tree .))
+  (action
+   (run %{project_root}/scripts/compile-std.sh %{project_root} module.d.exe module.cpp module.d.cpp))))
 
 (subdir multi_ind_functor
  (rule
@@ -119,7 +129,12 @@
  (rule
   (alias runtest)
   (deps mutual_mod.t.exe)
-  (action (run ./mutual_mod.t.exe))))
+  (action (run ./mutual_mod.t.exe)))
+ (rule
+  (targets mutual_mod.d.exe)
+  (deps MutualMod.vo mutual_mod.d.cpp (source_tree .))
+  (action
+   (run %{project_root}/scripts/compile-std.sh %{project_root} mutual_mod.d.exe mutual_mod.cpp mutual_mod.d.cpp))))
 
 (subdir nat
  (rule

diff --git a/tests/basics/module/Module.v b/tests/basics/module/Module.v
@@ -90,3 +90,7 @@ Require Crane.Mapping.Std.
 Require Crane.Mapping.NatIntStd.
 
 Crane Extraction "module" mymap.
+
+(* OCaml extraction for differential testing *)
+From Stdlib Require Extraction ExtrOcamlBasic ExtrOcamlNatInt.
+Extraction "module_ocaml.ml" mymap NatMap.find.
diff --git a/tests/basics/module/module.d.cpp b/tests/basics/module/module.d.cpp
@@ -0,0 +1,14 @@
+// Differential test harness: prints canonical output for diffing against OCaml
+#include "module.h"
+#include <cstdio>
+int main() {
+    auto r1 = NatMap::find(1, mymap);
+    printf("find(1)=%s\n", r1.has_value() ? (std::to_string(r1.value())).c_str() : "None");
+    auto r2 = NatMap::find(2, mymap);
+    printf("find(2)=%s\n", r2.has_value() ? (std::to_string(r2.value())).c_str() : "None");
+    auto r3 = NatMap::find(3, mymap);
+    printf("find(3)=%s\n", r3.has_value() ? (std::to_string(r3.value())).c_str() : "None");
+    auto r4 = NatMap::find(4, mymap);
+    printf("find(4)=%s\n", r4.has_value() ? (std::to_string(r4.value())).c_str() : "None");
+    return 0;
+}
diff --git a/tests/basics/module/module.d.ml b/tests/basics/module/module.d.ml
@@ -0,0 +1,11 @@
+(* Differential test harness: prints canonical output for diffing against C++ *)
+let print_find key map =
+  match Module_ocaml.NatMap.find key map with
+  | Some v -> Printf.printf "find(%d)=%d\n" key v
+  | None -> Printf.printf "find(%d)=None\n" key
+
+let () =
+  print_find 1 Module_ocaml.mymap;
+  print_find 2 Module_ocaml.mymap;
+  print_find 3 Module_ocaml.mymap;
+  print_find 4 Module_ocaml.mymap
diff --git a/tests/basics/mutual_mod/MutualMod.v b/tests/basics/mutual_mod/MutualMod.v
@@ -42,3 +42,7 @@ Require Crane.Mapping.Std.
 Require Crane.Mapping.NatIntStd.
 
 Crane Extraction "mutual_mod" test_even_len test_odd_len.
+
+(* OCaml extraction for differential testing *)
+From Stdlib Require Extraction ExtrOcamlBasic ExtrOcamlNatInt.
+Extraction "mutual_mod_ocaml.ml" test_even_len test_odd_len.
diff --git a/tests/basics/mutual_mod/mutual_mod.d.cpp b/tests/basics/mutual_mod/mutual_mod.d.cpp
@@ -0,0 +1,8 @@
+// Differential test harness: prints canonical output for diffing against OCaml
+#include "mutual_mod.h"
+#include <cstdio>
+int main() {
+    printf("test_even_len=%u\n", test_even_len);
+    printf("test_odd_len=%u\n", test_odd_len);
+    return 0;
+}
diff --git a/tests/basics/mutual_mod/mutual_mod.d.ml b/tests/basics/mutual_mod/mutual_mod.d.ml
@@ -0,0 +1,4 @@
+(* Differential test harness: prints canonical output for diffing against C++ *)
+let () =
+  Printf.printf "test_even_len=%d\n" Mutual_mod_ocaml.test_even_len;
+  Printf.printf "test_odd_len=%d\n" Mutual_mod_ocaml.test_odd_len