From 6940d2c4ff7b3df698df032dcffe5b18e6f17c30 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 30 May 2025 20:08:30 -0400
Subject: [PATCH] fix: block adversarial exploit of non-aborting `assert!`
 (#8559)

This PR fixes an adversarial soundness attack described in #8554. The
attack exploits the fact that `assert!` no longer aborts execution, and
that users can redirect error messages.
Another PR will implement the same fix for `Expr.Data`.
---
 src/Lean/Level.lean    |  7 ++-----
 src/kernel/level.cpp   | 10 ++++++++++
 src/runtime/object.cpp |  5 ++++-
 3 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index 035b4d479b..a8223104b1 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -43,11 +43,8 @@ def Level.Data.hasMVar (c : Level.Data) : Bool :=
 def Level.Data.hasParam (c : Level.Data) : Bool :=
   ((c.shiftRight 33).land 1) == 1
 
-def Level.mkData (h : UInt64) (depth : Nat := 0) (hasMVar hasParam : Bool := false) : Level.Data :=
-  if depth > Nat.pow 2 24 - 1 then panic! "universe level depth is too big"
-  else
-    let r : UInt64 := h.toUInt32.toUInt64 + hasMVar.toUInt64.shiftLeft 32 + hasParam.toUInt64.shiftLeft 33 + depth.toUInt64.shiftLeft 40
-    r
+@[extern "lean_level_mk_data"]
+opaque Level.mkData (h : UInt64) (depth : Nat := 0) (hasMVar hasParam : Bool := false) : Level.Data
 
 instance : Repr Level.Data where
   reprPrec v prec := Id.run do
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index 19163eefe0..183706ec66 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -41,6 +41,16 @@ unsigned get_depth(level const & l) { return lean_level_depth(l.to_obj_arg()); }
 bool has_param(level const & l) { return lean_level_has_param(l.to_obj_arg()); }
 bool has_mvar(level const & l) { return lean_level_has_mvar(l.to_obj_arg()); }
 
+extern "C" uint64_t lean_level_mk_data (uint64_t h, object * depth, uint8_t hasMVar, uint8_t hasParam) {
+    if (!is_scalar(depth))
+        lean_internal_panic("universe level depth is too big");
+    size_t d = unbox(depth);
+    if (d > 16777215)
+        lean_internal_panic("universe level depth is too big");
+    uint32_t h1 = h;
+    return ((uint64_t) h1) + (((uint64_t) hasMVar) << 32) + (((uint64_t) hasParam) << 33) + (((uint64_t)d) << 40);
+}
+
 bool is_explicit(level const & l) {
     switch (kind(l)) {
     case level_kind::Zero:
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index ab12a58c31..425c80dd2a 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -73,8 +73,10 @@ static void abort_on_panic() {
     }
 }
 
+FILE * g_saved_stderr = stderr;
+
 extern "C" LEAN_EXPORT void lean_internal_panic(char const * msg) {
-    std::cerr << "INTERNAL PANIC: " << msg << "\n";
+    fprintf(g_saved_stderr, "INTERNAL PANIC: %s\n", msg);
     abort_on_panic();
     std::exit(1);
 }
@@ -2653,6 +2655,7 @@ extern "C" LEAN_EXPORT lean_external_class * lean_register_external_class(lean_e
 }
 
 void initialize_object() {
+    g_saved_stderr = stderr;  // Save original pointer early
     g_ext_classes       = new std::vector<external_object_class*>();
     g_ext_classes_mutex = new mutex();
     g_array_empty       = lean_alloc_array(0, 0);