Make Nativecode.string_of_kn really injective for good.

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

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)

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.