From f9c73c2a64f294c0fdf7b947c30e1db10e57db8b Mon Sep 17 00:00:00 2001
From: Gustavo Delerue <gxdelerue@proton.me>
Date: Thu, 26 Feb 2026 12:52:47 +0000
Subject: [PATCH] Add proper error message on digest mismatch in require

---
 src/ecLoader.ml                      |  5 +++++
 src/ecLoader.mli                     |  2 ++
 src/ecScope.ml                       | 18 ++++++++++++++----
 tests/require_test/easycrypt.project |  6 ++++++
 tests/require_test/foo1/main.ec      |  7 +++++++
 tests/require_test/foo2/main.ec      |  9 +++++++++
 tests/require_test/main.ec           |  7 +++++++
 tests/require_test/require.ec        |  3 +++
 8 files changed, 53 insertions(+), 4 deletions(-)
 create mode 100644 tests/require_test/easycrypt.project
 create mode 100644 tests/require_test/foo1/main.ec
 create mode 100644 tests/require_test/foo2/main.ec
 create mode 100644 tests/require_test/main.ec
 create mode 100644 tests/require_test/require.ec

diff --git a/src/ecLoader.ml b/src/ecLoader.ml
index 25378c19e6..b52f663c25 100644
--- a/src/ecLoader.ml
+++ b/src/ecLoader.ml
@@ -26,6 +26,11 @@ let getkind ext =
   | "eca" -> `EcA
   | _     -> raise (BadExtension ("." ^ ext))
 
+let string_of_namespace ns = 
+  match ns with
+  | `System -> "System"
+  | `Named s -> s
+
 (* -------------------------------------------------------------------- *)
 let create () = { ecl_idirs = []; }
 
diff --git a/src/ecLoader.mli b/src/ecLoader.mli
index 3b5fe2d316..2338f6ad73 100644
--- a/src/ecLoader.mli
+++ b/src/ecLoader.mli
@@ -12,6 +12,8 @@ val getkind : string -> kind
 (* -------------------------------------------------------------------- *)
 type namespace = [ `System | `Named of string ]
 
+val string_of_namespace : namespace -> string
+
 (* -------------------------------------------------------------------- *)
 val create  : unit -> ecloader
 val aslist  : ecloader -> ((namespace option * string) * idx_t) list
diff --git a/src/ecScope.ml b/src/ecScope.ml
index 77325401de..4403502f6d 100644
--- a/src/ecScope.ml
+++ b/src/ecScope.ml
@@ -1816,12 +1816,22 @@ module Theory = struct
         sc_env = EcSection.add_th ~import cth scope.sc_env }
 
   (* ------------------------------------------------------------------ *)
-  let required (scope : scope) (name : required_info) =
+  let required (scope : scope) (rqd : required_info) =
     assert (scope.sc_pr_uc = None);
     List.exists (fun x ->
-        if x.rqd_name = name.rqd_name then (
-          (* FIXME: raise an error message *)
-          assert (x.rqd_digest = name.rqd_digest);
+        if x.rqd_name = rqd.rqd_name then (
+          if (x.rqd_digest <> rqd.rqd_digest) then begin
+            let fullname (ri : required_info) =
+              let namespace =
+                ri.rqd_namespace
+                |> Option.map EcLoader.string_of_namespace
+                |> Option.map (fun s -> s ^ ":")
+                |> Option.value ~default:"" in
+              namespace ^ ri.rqd_name in
+            hierror
+              "Digest mismatch, file %s differs from %s"
+              (fullname x) (fullname rqd)
+          end;
           true)
         else false)
       scope.sc_required
diff --git a/tests/require_test/easycrypt.project b/tests/require_test/easycrypt.project
new file mode 100644
index 0000000000..ff9bcb9f55
--- /dev/null
+++ b/tests/require_test/easycrypt.project
@@ -0,0 +1,6 @@
+[general]
+provers = CVC5@1.0
+provers = Z3@4.12
+
+idirs=Foo2:foo2
+idirs=Foo1:foo1
diff --git a/tests/require_test/foo1/main.ec b/tests/require_test/foo1/main.ec
new file mode 100644
index 0000000000..072e1ab23e
--- /dev/null
+++ b/tests/require_test/foo1/main.ec
@@ -0,0 +1,7 @@
+require import AllCore Int Real.
+
+op foo : real = 1%r.
+
+theory A.
+  op add : real -> real -> real = (+)%r.
+end A.
diff --git a/tests/require_test/foo2/main.ec b/tests/require_test/foo2/main.ec
new file mode 100644
index 0000000000..60b3fd730a
--- /dev/null
+++ b/tests/require_test/foo2/main.ec
@@ -0,0 +1,9 @@
+require import AllCore Int.
+
+op foo : int = 2.
+
+op foo2 : int = 3.
+
+theory A.
+  op add : int -> int -> int = (-).
+end A.
diff --git a/tests/require_test/main.ec b/tests/require_test/main.ec
new file mode 100644
index 0000000000..072e1ab23e
--- /dev/null
+++ b/tests/require_test/main.ec
@@ -0,0 +1,7 @@
+require import AllCore Int Real.
+
+op foo : real = 1%r.
+
+theory A.
+  op add : real -> real -> real = (+)%r.
+end A.
diff --git a/tests/require_test/require.ec b/tests/require_test/require.ec
new file mode 100644
index 0000000000..c986b4bc01
--- /dev/null
+++ b/tests/require_test/require.ec
@@ -0,0 +1,3 @@
+from Foo2 require import Main.
+fail require import Main.
+fail from Foo1 require import Main.