fix: block potential adversarial exploit of non-aborting assert!

This PR is similar to #8559, but for `Expr.mkData`

src/Lean/Expr.lean

@@ -166,32 +166,13 @@ def BinderInfo.toUInt64 : BinderInfo → UInt64
   | .strictImplicit => 2
   | .instImplicit   => 3
 
-def Expr.mkData
-    (h : UInt64) (looseBVarRange : Nat := 0) (approxDepth : UInt32 := 0)
-    (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false)
-    : Expr.Data :=
-  let approxDepth : UInt8 := if approxDepth > 255 then 255 else approxDepth.toUInt8
-  assert! (looseBVarRange ≤ Nat.pow 2 20 - 1)
-  let r : UInt64 :=
-      h.toUInt32.toUInt64 +
-      approxDepth.toUInt64.shiftLeft 32 +
-      hasFVar.toUInt64.shiftLeft 40 +
-      hasExprMVar.toUInt64.shiftLeft 41 +
-      hasLevelMVar.toUInt64.shiftLeft 42 +
-      hasLevelParam.toUInt64.shiftLeft 43 +
-      looseBVarRange.toUInt64.shiftLeft 44
-  r
+@[extern "lean_expr_mk_data"]
+opaque Expr.mkData (h : UInt64) (looseBVarRange : Nat := 0) (approxDepth : UInt32 := 0)
+    (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) : Expr.Data
 
 /-- Optimized version of `Expr.mkData` for applications. -/
-@[inline] def Expr.mkAppData (fData : Data) (aData : Data) : Data :=
-  let depth          := (max fData.approxDepth.toUInt16 aData.approxDepth.toUInt16) + 1
-  let approxDepth    := if depth > 255 then 255 else depth.toUInt8
-  let looseBVarRange := max fData.looseBVarRange aData.looseBVarRange
-  let hash           := mixHash fData aData
-  let fData : UInt64 := fData
-  let aData : UInt64 := aData
-  assert! (looseBVarRange ≤ (Nat.pow 2 20 - 1).toUInt32)
-  ((fData ||| aData) &&& ((15 : UInt64) <<< (40 : UInt64))) ||| hash.toUInt32.toUInt64 ||| (approxDepth.toUInt64 <<< (32 : UInt64)) ||| (looseBVarRange.toUInt64 <<< (44 : UInt64))
+@[extern "lean_expr_mk_app_data"]
+opaque Expr.mkAppData (fData : Data) (aData : Data) : Data
 
 @[inline] def Expr.mkDataForBinder (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt32) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) : Expr.Data :=
   Expr.mkData h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam

src/kernel/expr.cpp

@@ -102,6 +102,29 @@ bool has_univ_param(expr const & e) { return lean_expr_has_level_param(e.to_obj_
 extern "C" unsigned lean_expr_loose_bvar_range(object * e);
 unsigned get_loose_bvar_range(expr const & e) { return lean_expr_loose_bvar_range(e.to_obj_arg()); }
 
+extern "C" LEAN_EXPORT uint64_t lean_expr_mk_data(uint64_t hash, object * bvarRange, uint32_t approxDepth, uint8_t hasFVar, uint8_t hasExprMVar, uint8_t hasLevelMVar, uint8_t hasLevelParam) {
+    if (approxDepth > 255) approxDepth = 255;
+    if (!is_scalar(bvarRange)) lean_internal_panic("too many bound variables");
+    size_t range = unbox(bvarRange);
+    if (range > 1048575) lean_internal_panic("too many bound variables");
+    uint32_t r = range;
+    uint32_t h = hash;
+    return ((uint64_t) h) + (((uint64_t) approxDepth) << 32) + (((uint64_t) hasFVar) << 40)
+    + (((uint64_t) hasExprMVar) << 41) + (((uint64_t) hasLevelMVar) << 42) + (((uint64_t) hasLevelParam) << 43)
+    + (((uint64_t) r) << 44);
+}
+
+inline uint16_t get_approx_depth(uint64_t data) { return (data >> 32) & 255; }
+inline uint32_t get_bvar_range(uint64_t data) { return data >> 44; }
+
+extern "C" LEAN_EXPORT uint64_t lean_expr_mk_app_data(uint64_t fData, uint64_t aData) {
+  uint16_t depth = std::max(get_approx_depth(fData), get_approx_depth(aData)) + 1;
+  if (depth > 255) depth = 255;
+  uint32_t range = std::max(get_bvar_range(fData), get_bvar_range(aData));
+  uint32_t h = hash(fData, aData);
+  return ((fData | aData) & (((uint64_t) 15) << 40)) | ((uint64_t) h) | (((uint64_t) depth) << 32) | (((uint64_t) range) << 44);
+}
+
 // =======================================
 // Constructors
 

src/kernel/level.cpp

@@ -41,7 +41,7 @@ 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) {
+extern "C" LEAN_EXPORT 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);