From b2e9d866521fa204954f70862b642cd5cb0889f7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Mon, 24 Aug 2026 15:47:38 +0200
Subject: [PATCH] Make Nativecode.string_of_kn really injective for good.

This is critical for soundness of native compilation, as otherwise a
definition may overwrite another one. This was not the first time such
a problem arised, see 244d7a9aa.

We go for a belt-and-braces approach and try to make all subcomponents
injective, including the modpath printer.

Fixes #22364: string_of_kn is non-injective.
---
 dev/doc/critical-bugs.md    | 12 +++++++++++
 kernel/nativecode.ml        | 41 +++++++++++++++++++++++++++++++++----
 test-suite/bugs/bug_22364.v | 25 ++++++++++++++++++++++
 3 files changed, 74 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/bugs/bug_22364.v

diff --git a/dev/doc/critical-bugs.md b/dev/doc/critical-bugs.md
index be693f3edb2b..1ff08da1177e 100644
--- a/dev/doc/critical-bugs.md
+++ b/dev/doc/critical-bugs.md
@@ -1011,6 +1011,18 @@ For instance `α` and `__U03b1_` were the same in the native compiler.
 - exploit: see issue
 - risk: ?
 
+#### translation of identifiers from Coq to OCaml was not injective
+
+- component: native
+- introduced: V8.5
+- impacted released versions: V8.5-V9.2.0
+- impacted coqchk versions: none (no native computation in coqchk)
+- fixed in: V9.2.1
+- found by: christos-spearbit
+- GH issue number: rocq-rocq-prover/rocq#22364
+- exploit: see issue
+- risk: systematic when using native compilation
+
 ### Side-effects
 
 #### polymorphic side-effects inside monomorphic definitions incorrectly handled as not inlined
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 4d3abb6a5900..63d14833f805 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1772,20 +1772,53 @@ let string_of_label_def l =
     | None -> ""
     | Some l -> string_of_id l
 
+let escape_underscore s =
+  let len = String.length s in
+  let rec count accu i =
+    if i < len then
+      let accu = match s.[i] with
+      | '_' -> accu + 1
+      | _ -> accu
+      in
+      count accu (i + 1)
+    else accu
+  in
+  let count = count 0 0 in
+  if Int.equal count 0 then s
+  else
+    let nlen = len + count in
+    let ans = Bytes.create nlen in
+    let rec setc pos npos =
+      if pos < len then match s.[pos] with
+      | '_' ->
+        let () = Bytes.set ans npos '_' in
+        let () = Bytes.set ans (npos + 1) '_' in
+        setc (pos + 1) (npos + 2)
+      | c ->
+        let () = Bytes.set ans npos c in
+        setc (pos + 1) (npos + 1)
+    in
+    let () = setc 0 0 in
+    Bytes.unsafe_to_string ans
+
+let escaped_string_of_id s = escape_underscore (string_of_id s)
+
 (* Relativization of module paths *)
 let rec list_of_mp acc = function
-  | MPdot (mp,l) -> list_of_mp (string_of_id l::acc) mp
+  | MPdot (mp, l) -> list_of_mp ("_d" :: escaped_string_of_id l :: acc) mp
   | MPfile dp ->
       let dp = DirPath.repr dp in
-      string_of_dirpath dp :: acc
-  | MPbound mbid -> ("X"^string_of_id (MBId.to_id mbid))::acc
+      let dp = List.map escaped_string_of_id dp in
+      "_f" :: List.rev_append dp acc
+  | MPbound mbid -> "_b" :: escaped_string_of_id (MBId.to_id mbid) :: acc
 
 let list_of_mp mp = list_of_mp [] mp
 
+(* This function **must** be injective for soundness *)
 let string_of_kn kn =
   let (mp,l) = KerName.repr kn in
   let mp = list_of_mp mp in
-  String.concat "_" mp ^ "_" ^ string_of_id l
+  String.concat "_l" mp ^ "_l" ^ (escaped_string_of_id l)
 
 let string_of_con c = string_of_kn (Constant.user c)
 let string_of_mind mind = string_of_kn (MutInd.user mind)
diff --git a/test-suite/bugs/bug_22364.v b/test-suite/bugs/bug_22364.v
new file mode 100644
index 000000000000..55abb2f4f188
--- /dev/null
+++ b/test-suite/bugs/bug_22364.v
@@ -0,0 +1,25 @@
+(* Confusion of kername translation of dot module separators and name underscores. *)
+Module A. Module B. Definition x := true. End B. End A.
+Module A_B. Definition x := false. End A_B.
+
+Lemma via_vm : orb A.B.x A_B.x = true.
+Proof. vm_compute; reflexivity. Qed.
+
+Lemma via_native : orb A.B.x A_B.x = false.
+Proof.
+native_compute.
+Fail reflexivity.
+Abort.
+
+(* Another similar example with underscore at the word boundary *)
+Module X_. Definition foo := true. End X_.
+Module X. Definition _foo := false. End X.
+
+Lemma via_vm' : orb X_.foo X._foo = true.
+Proof. vm_compute; reflexivity. Qed.
+
+Lemma via_native' : orb X_.foo X._foo = false.
+Proof.
+native_compute.
+Fail reflexivity.
+Abort.