From eda7495feb61235948242739517e75feab51ea2e Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Fri, 10 Jul 2026 10:22:20 +0200
Subject: [PATCH] [WIP] Test actually abstracting large nat constants

---
 .../22254-proux01-abstract-large-nat.sh       |   1 +
 test-suite/Makefile                           |   2 +-
 test-suite/bugs/bug_9453.v                    |   7 -
 test-suite/output/NumberNotations.out         |   3 +-
 test-suite/output/Search.out                  |  91 +++++----
 test-suite/output/SearchPattern.out           |  45 +++--
 test-suite/output/Search_bug21821.out         |   6 +
 test-suite/output/Search_headconcl.out        |  12 ++
 theories/Corelib/Init/Nat.v                   | 184 +++++++++++++++++-
 9 files changed, 286 insertions(+), 65 deletions(-)
 create mode 100644 dev/ci/user-overlays/22254-proux01-abstract-large-nat.sh
 delete mode 100644 test-suite/bugs/bug_9453.v

diff --git a/dev/ci/user-overlays/22254-proux01-abstract-large-nat.sh b/dev/ci/user-overlays/22254-proux01-abstract-large-nat.sh
new file mode 100644
index 000000000000..2488f21f4ffd
--- /dev/null
+++ b/dev/ci/user-overlays/22254-proux01-abstract-large-nat.sh
@@ -0,0 +1 @@
+overlay coqutil https://github.com/proux01/coqutil rocq22254 22254
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 925a9e98fae2..6196a3185a03 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -502,7 +502,7 @@ $(addsuffix .log,$(wildcard output-coqchk/*.v)): %.v.log: %.v %.out $(PREREQUISI
 	  output=$*.out.real; \
 	  export LC_CTYPE=C; \
 	  export LANG=C; \
-	  $(call WITH_TIMER,$(patsubst %.v.log,%.chk.log,$@),$(coqchk) -o -silent $(call get_coqchk_prog_args,"$<") -Q $(shell dirname $<) "" -norec $(shell basename $< .v) > $$output 2>&1) ; \
+	  $(call WITH_TIMER,$(patsubst %.v.log,%.chk.log,$@),$(coqchk) -o -silent $(call get_coqchk_prog_args,"$<") -Q $(shell dirname $<) "" $(shell basename $< .v) > $$output 2>&1) ; \
 	  diff -a -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
diff --git a/test-suite/bugs/bug_9453.v b/test-suite/bugs/bug_9453.v
deleted file mode 100644
index 93eb58d2c821..000000000000
--- a/test-suite/bugs/bug_9453.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(* check compatibility with 8.8 and earlier for lack of warnings on the nat 5000 *)
-Set Warnings "+large-nat,+abstract-large-number".
-Fail Check 5001.
-Check 5000.
-(* Error:
-To avoid stack overflow, large numbers in nat are interpreted as applications of
-Nat.of_uint. *)
diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out
index 3f545ed2747d..5efdbd668968 100644
--- a/test-suite/output/NumberNotations.out
+++ b/test-suite/output/NumberNotations.out
@@ -242,7 +242,8 @@ let v : ty := Build_ty Set set in v : ty
      : ty
 let v : ty := Build_ty Type type in v : ty
      : ty
-1
+Nat.Of_uint.locked
+  (Decimal.D0 (Decimal.D0 (Decimal.D0 (Decimal.D0 (Decimal.D1 Decimal.Nil)))))
      : nat
 1000
      : nat
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 8704b54029ce..cdb751cf0149 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -28,17 +28,25 @@ implb: bool -> bool -> bool
 reflect: Prop -> bool -> Set
 andb: bool -> bool -> bool
 orb: bool -> bool -> bool
+Nat.hex_uint_le_1_hdigit: Hexadecimal.uint -> bool
+Nat.uint_le5000: Decimal.uint -> bool
+Nat.uint_le_3_digits: Decimal.uint -> bool
+Nat.uint_le_2_digits: Decimal.uint -> bool
+Nat.uint_le_1_digit: Decimal.uint -> bool
+Nat.hex_uint_le5000: Hexadecimal.uint -> bool
+Nat.hex_uint_le_3_hdigits: Hexadecimal.uint -> bool
+Nat.hex_uint_le_2_hdigits: Hexadecimal.uint -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
 BoolSpec: Prop -> Prop -> bool -> Prop
 Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool
 Nat.leb: nat -> nat -> bool
 Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
-Number.uint_beq: Number.uint -> Number.uint -> bool
+Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
 Number.signed_int_beq: Number.signed_int -> Number.signed_int -> bool
 Decimal.signed_int_beq: Decimal.signed_int -> Decimal.signed_int -> bool
 Nat.eqb: nat -> nat -> bool
-Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
+Number.uint_beq: Number.uint -> Number.uint -> bool
 Nat.ltb: nat -> nat -> bool
 Number.number_beq: Number.number -> Number.number -> bool
 Hexadecimal.signed_int_beq:
@@ -75,8 +83,9 @@ bool_of_sumbool:
 sumbool_of_bool: forall b : bool, {b = true} + {b = false}
 Decimal.internal_signed_int_dec_lb:
   forall x y : Decimal.signed_int, x = y -> Decimal.signed_int_beq x y = true
-Number.internal_signed_int_dec_lb1:
-  forall x y : Number.signed_int, x = y -> Number.signed_int_beq x y = true
+Hexadecimal.internal_signed_int_dec_lb0:
+  forall x y : Hexadecimal.signed_int,
+  x = y -> Hexadecimal.signed_int_beq x y = true
 Number.internal_signed_int_dec_bl1:
   forall x y : Number.signed_int, Number.signed_int_beq x y = true -> x = y
 Decimal.internal_signed_int_dec_bl:
@@ -84,30 +93,29 @@ Decimal.internal_signed_int_dec_bl:
 Hexadecimal.internal_hexadecimal_dec_lb:
   forall x y : Hexadecimal.hexadecimal,
   x = y -> Hexadecimal.hexadecimal_beq x y = true
-Hexadecimal.internal_signed_int_dec_lb0:
-  forall x y : Hexadecimal.signed_int,
-  x = y -> Hexadecimal.signed_int_beq x y = true
-Number.internal_number_dec_lb:
-  forall x y : Number.number, x = y -> Number.number_beq x y = true
+Number.internal_signed_int_dec_lb1:
+  forall x y : Number.signed_int, x = y -> Number.signed_int_beq x y = true
 Hexadecimal.internal_signed_int_dec_bl0:
   forall x y : Hexadecimal.signed_int,
   Hexadecimal.signed_int_beq x y = true -> x = y
+Byte.to_bits:
+  Byte.byte ->
+  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
 Number.internal_uint_dec_lb1:
   forall x y : Number.uint, x = y -> Number.uint_beq x y = true
 Number.internal_uint_dec_bl1:
   forall x y : Number.uint, Number.uint_beq x y = true -> x = y
+Number.internal_number_dec_lb:
+  forall x y : Number.number, x = y -> Number.number_beq x y = true
+Decimal.internal_decimal_dec_lb:
+  forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
 Decimal.internal_decimal_dec_bl:
   forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y
-Number.internal_number_dec_bl:
-  forall x y : Number.number, Number.number_beq x y = true -> x = y
 Byte.of_bits:
   bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
   Byte.byte
-Byte.to_bits:
-  Byte.byte ->
-  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
-Decimal.internal_decimal_dec_lb:
-  forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
+Number.internal_number_dec_bl:
+  forall x y : Number.number, Number.number_beq x y = true -> x = y
 Hexadecimal.internal_hexadecimal_dec_bl:
   forall x y : Hexadecimal.hexadecimal,
   Hexadecimal.hexadecimal_beq x y = true -> x = y
@@ -118,6 +126,10 @@ eq_true_rew_fwd_dep:
 eq_true_rew_dep:
   forall P : forall b : bool, eq_true b -> Type,
   P true is_eq_true -> forall [b : bool] (e : eq_true b), P b e
+Hexadecimal.internal_uint_dec_lb0:
+  forall x : Hexadecimal.uint,
+  (fun x0 : Hexadecimal.uint =>
+   forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x
 Decimal.internal_uint_dec_bl:
   forall x : Decimal.uint,
   (fun x0 : Decimal.uint =>
@@ -126,23 +138,19 @@ Decimal.internal_uint_dec_lb:
   forall x : Decimal.uint,
   (fun x0 : Decimal.uint =>
    forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x
-Hexadecimal.internal_uint_dec_lb0:
-  forall x : Hexadecimal.uint,
-  (fun x0 : Hexadecimal.uint =>
-   forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x
 Hexadecimal.internal_uint_dec_bl0:
   forall x : Hexadecimal.uint,
   (fun x0 : Hexadecimal.uint =>
    forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
-bool_eq_rec:
-  forall (b : bool) (P : bool -> Set),
-  (b = true -> P true) -> (b = false -> P false) -> P b
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 bool_eq_ind:
   forall (b : bool) (P : bool -> Prop),
   (b = true -> P true) -> (b = false -> P false) -> P b
+bool_eq_rec:
+  forall (b : bool) (P : bool -> Set),
+  (b = true -> P true) -> (b = false -> P false) -> P b
 BoolSpec_sind:
   forall [P Q : Prop] (P0 : bool -> SProp),
   (P -> P0 true) ->
@@ -161,13 +169,13 @@ reflect_sind:
   (forall p : P, P0 true (ReflectT P p)) ->
   (forall n : ~ P, P0 false (ReflectF P n)) ->
   forall [b : bool] (r : reflect P b), P0 b r
-reflect_rect:
-  forall [P : Prop] (P0 : forall b : bool, reflect P b -> Type),
+reflect_rec:
+  forall [P : Prop] (P0 : forall b : bool, reflect P b -> Set),
   (forall p : P, P0 true (ReflectT P p)) ->
   (forall n : ~ P, P0 false (ReflectF P n)) ->
   forall [b : bool] (r : reflect P b), P0 b r
-reflect_rec:
-  forall [P : Prop] (P0 : forall b : bool, reflect P b -> Set),
+reflect_rect:
+  forall [P : Prop] (P0 : forall b : bool, reflect P b -> Type),
   (forall p : P, P0 true (ReflectT P p)) ->
   (forall n : ~ P, P0 false (ReflectF P n)) ->
   forall [b : bool] (r : reflect P b), P0 b r
@@ -184,6 +192,10 @@ plus_O_n: forall n : nat, 0 + n = n
 plus_n_O: forall n : nat, n = n + 0
 n_Sn: forall n : nat, n <> S n
 pred_Sn: forall n : nat, n = Nat.pred (S n)
+Nat.Of_uint.unlock:
+  forall d : Decimal.uint, Nat.Of_uint.locked d = Nat.of_uint d
+Nat.Of_hex_uint.unlock:
+  forall d : Hexadecimal.uint, Nat.Of_hex_uint.locked d = Nat.of_hex_uint d
 O_S: forall n : nat, 0 <> S n
 f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
 eq_S: forall x y : nat, x = y -> S x = S y
@@ -192,8 +204,8 @@ min_r: forall n m : nat, m <= n -> Nat.min n m = m
 min_l: forall n m : nat, n <= m -> Nat.min n m = n
 max_r: forall n m : nat, n <= m -> Nat.max n m = m
 max_l: forall n m : nat, m <= n -> Nat.max n m = n
-plus_Sn_m: forall n m : nat, S n + m = S (n + m)
 plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+plus_Sn_m: forall n m : nat, S n + m = S (n + m)
 f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y
 not_eq_S: forall n m : nat, n <> m -> S n <> S m
 mult_n_Sm: forall n m : nat, n * m + n = n * S m
@@ -444,25 +456,28 @@ bool_choice:
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
 Nat.two: nat
-Nat.one: nat
 Nat.zero: nat
+Nat.one: nat
 newdef: nat -> nat
-Nat.succ: nat -> nat
-Nat.log2: nat -> nat
 Nat.sqrt: nat -> nat
+Nat.log2: nat -> nat
+Nat.pred: nat -> nat
 Nat.square: nat -> nat
 Nat.double: nat -> nat
-Nat.pred: nat -> nat
-Nat.ldiff: nat -> nat -> nat
-Nat.tail_mul: nat -> nat -> nat
+Nat.succ: nat -> nat
 Nat.land: nat -> nat -> nat
-Nat.div: nat -> nat -> nat
-Nat.modulo: nat -> nat -> nat
 Nat.lor: nat -> nat -> nat
+Nat.tail_mul: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
+Nat.ldiff: nat -> nat -> nat
+Nat.div: nat -> nat -> nat
+Nat.modulo: nat -> nat -> nat
+Nat.of_num_uint: Number.uint -> nat
 Nat.of_hex_uint: Hexadecimal.uint -> nat
+Nat.abstract5000_of_hex_uint: Hexadecimal.uint -> nat
+Nat.abstract5000_of_uint: Decimal.uint -> nat
 Nat.of_uint: Decimal.uint -> nat
-Nat.of_num_uint: Number.uint -> nat
+Nat.abstract5000_of_num_uint: Number.uint -> nat
 length: forall [A : Type], list A -> nat
 plus_n_O: forall n : nat, n = n + 0
 plus_O_n: forall n : nat, 0 + n = n
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 4a06c5c6eb78..e0da3a27cb88 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -5,6 +5,14 @@ xorb: bool -> bool -> bool
 andb: bool -> bool -> bool
 orb: bool -> bool -> bool
 implb: bool -> bool -> bool
+Nat.uint_le5000: Decimal.uint -> bool
+Nat.uint_le_3_digits: Decimal.uint -> bool
+Nat.uint_le_2_digits: Decimal.uint -> bool
+Nat.uint_le_1_digit: Decimal.uint -> bool
+Nat.hex_uint_le5000: Hexadecimal.uint -> bool
+Nat.hex_uint_le_3_hdigits: Hexadecimal.uint -> bool
+Nat.hex_uint_le_2_hdigits: Hexadecimal.uint -> bool
+Nat.hex_uint_le_1_hdigit: Hexadecimal.uint -> bool
 Nat.odd: nat -> bool
 Nat.even: nat -> bool
 Number.uint_beq: Number.uint -> Number.uint -> bool
@@ -23,36 +31,41 @@ Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
 Decimal.signed_int_beq: Decimal.signed_int -> Decimal.signed_int -> bool
 Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool
 Nat.two: nat
-Nat.zero: nat
 Nat.one: nat
+Nat.zero: nat
 O: nat
-Nat.double: nat -> nat
-Nat.sqrt: nat -> nat
 Nat.div2: nat -> nat
+Nat.sqrt: nat -> nat
+Nat.succ: nat -> nat
 Nat.log2: nat -> nat
 Nat.pred: nat -> nat
 Nat.square: nat -> nat
+Nat.double: nat -> nat
 S: nat -> nat
-Nat.succ: nat -> nat
-Nat.ldiff: nat -> nat -> nat
-Nat.add: nat -> nat -> nat
 Nat.land: nat -> nat -> nat
-Nat.lxor: nat -> nat -> nat
-Nat.sub: nat -> nat -> nat
-Nat.mul: nat -> nat -> nat
-Nat.tail_mul: nat -> nat -> nat
-Nat.max: nat -> nat -> nat
 Nat.tail_add: nat -> nat -> nat
+Nat.ldiff: nat -> nat -> nat
+Nat.tail_mul: nat -> nat -> nat
+Nat.gcd: nat -> nat -> nat
+Nat.lxor: nat -> nat -> nat
 Nat.pow: nat -> nat -> nat
-Nat.min: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.max: nat -> nat -> nat
 Nat.modulo: nat -> nat -> nat
 Nat.div: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
-Nat.gcd: nat -> nat -> nat
+Nat.min: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
+Nat.sub: nat -> nat -> nat
+Nat.mul: nat -> nat -> nat
+Nat.Of_uint.locked: Decimal.uint -> nat
+Nat.abstract5000_of_hex_uint: Hexadecimal.uint -> nat
+Nat.of_uint: Decimal.uint -> nat
 Hexadecimal.nb_digits: Hexadecimal.uint -> nat
-Nat.of_hex_uint: Hexadecimal.uint -> nat
+Nat.abstract5000_of_num_uint: Number.uint -> nat
+Nat.Of_hex_uint.locked: Hexadecimal.uint -> nat
+Nat.abstract5000_of_uint: Decimal.uint -> nat
 Nat.of_num_uint: Number.uint -> nat
-Nat.of_uint: Decimal.uint -> nat
+Nat.of_hex_uint: Hexadecimal.uint -> nat
 Decimal.nb_digits: Decimal.uint -> nat
 Nat.tail_addmul: nat -> nat -> nat -> nat
 Nat.of_hex_uint_acc: Hexadecimal.uint -> nat -> nat
diff --git a/test-suite/output/Search_bug21821.out b/test-suite/output/Search_bug21821.out
index 6e42e891f168..78d4381f1bc9 100644
--- a/test-suite/output/Search_bug21821.out
+++ b/test-suite/output/Search_bug21821.out
@@ -1,4 +1,10 @@
 X: Type
 X2: Type
+Nat.Of_uint.locked: Decimal.uint -> nat
+Nat.Of_hex_uint.locked: Hexadecimal.uint -> nat
+Nat.Of_hex_uint.unlock:
+  forall d : Hexadecimal.uint, Nat.Of_hex_uint.locked d = Nat.of_hex_uint d
+Nat.Of_uint.unlock:
+  forall d : Decimal.uint, Nat.Of_uint.locked d = Nat.of_uint d
 Y: Type
 Y2: Type
diff --git a/test-suite/output/Search_headconcl.out b/test-suite/output/Search_headconcl.out
index b6b2f536b0fa..e865bde06f45 100644
--- a/test-suite/output/Search_headconcl.out
+++ b/test-suite/output/Search_headconcl.out
@@ -11,6 +11,14 @@ xorb: bool -> bool -> bool
 andb: bool -> bool -> bool
 orb: bool -> bool -> bool
 implb: bool -> bool -> bool
+Nat.uint_le5000: Decimal.uint -> bool
+Nat.uint_le_3_digits: Decimal.uint -> bool
+Nat.uint_le_2_digits: Decimal.uint -> bool
+Nat.uint_le_1_digit: Decimal.uint -> bool
+Nat.hex_uint_le5000: Hexadecimal.uint -> bool
+Nat.hex_uint_le_3_hdigits: Hexadecimal.uint -> bool
+Nat.hex_uint_le_2_hdigits: Hexadecimal.uint -> bool
+Nat.hex_uint_le_1_hdigit: Hexadecimal.uint -> bool
 Nat.odd: nat -> bool
 Nat.even: nat -> bool
 Number.uint_beq: Number.uint -> Number.uint -> bool
@@ -32,6 +40,10 @@ mult_n_O: forall n : nat, 0 = n * 0
 plus_O_n: forall n : nat, 0 + n = n
 plus_n_O: forall n : nat, n = n + 0
 pred_Sn: forall n : nat, n = Nat.pred (S n)
+Nat.Of_hex_uint.unlock:
+  forall d : Hexadecimal.uint, Nat.Of_hex_uint.locked d = Nat.of_hex_uint d
+Nat.Of_uint.unlock:
+  forall d : Decimal.uint, Nat.Of_uint.locked d = Nat.of_uint d
 f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
 eq_add_S: forall n m : nat, S n = S m -> n = m
 eq_S: forall x y : nat, x = y -> S x = S y
diff --git a/theories/Corelib/Init/Nat.v b/theories/Corelib/Init/Nat.v
index a2a4f6b023f4..21bc296936fb 100644
--- a/theories/Corelib/Init/Nat.v
+++ b/theories/Corelib/Init/Nat.v
@@ -218,6 +218,186 @@ Definition of_num_uint (d:Number.uint) :=
   | Number.UIntHexadecimal d => of_hex_uint d
   end.
 
+Definition uint_le_1_digit (d : Decimal.uint) : bool :=
+  match d with
+  | Decimal.Nil => true
+  | Decimal.D0 d0
+  | Decimal.D1 d0
+  | Decimal.D2 d0
+  | Decimal.D3 d0
+  | Decimal.D4 d0
+  | Decimal.D5 d0
+  | Decimal.D6 d0
+  | Decimal.D7 d0
+  | Decimal.D8 d0
+  | Decimal.D9 d0 => match d0 with Decimal.Nil => true | _ => false end
+  end.
+
+Definition uint_le_2_digits (d : Decimal.uint) : bool :=
+  match d with
+  | Decimal.Nil => true
+  | Decimal.D0 d0
+  | Decimal.D1 d0
+  | Decimal.D2 d0
+  | Decimal.D3 d0
+  | Decimal.D4 d0
+  | Decimal.D5 d0
+  | Decimal.D6 d0
+  | Decimal.D7 d0
+  | Decimal.D8 d0
+  | Decimal.D9 d0 => uint_le_1_digit d0
+  end.
+
+Definition uint_le_3_digits (d : Decimal.uint) : bool :=
+  match d with
+  | Decimal.Nil => true
+  | Decimal.D0 d0
+  | Decimal.D1 d0
+  | Decimal.D2 d0
+  | Decimal.D3 d0
+  | Decimal.D4 d0
+  | Decimal.D5 d0
+  | Decimal.D6 d0
+  | Decimal.D7 d0
+  | Decimal.D8 d0
+  | Decimal.D9 d0 => uint_le_2_digits d0
+  end.
+
+Definition uint_le5000 (d : Decimal.uint) : bool :=
+  match d with
+  | Decimal.Nil => true
+  | Decimal.D0 d0
+  | Decimal.D1 d0
+  | Decimal.D2 d0
+  | Decimal.D3 d0
+  | Decimal.D4 d0 => uint_le_3_digits d0
+  | Decimal.D5 d0 =>
+      uint_le_2_digits d0
+      || match Decimal.nzhead d0 with Decimal.Nil => true | _ => false end
+  | Decimal.D6 d0
+  | Decimal.D7 d0
+  | Decimal.D8 d0
+  | Decimal.D9 d0 => uint_le_2_digits d0
+  end.
+
+Definition hex_uint_le_1_hdigit (d : Hexadecimal.uint) : bool :=
+  match d with
+  | Hexadecimal.Nil => true
+  | Hexadecimal.D0 d0
+  | Hexadecimal.D1 d0
+  | Hexadecimal.D2 d0
+  | Hexadecimal.D3 d0
+  | Hexadecimal.D4 d0
+  | Hexadecimal.D5 d0
+  | Hexadecimal.D6 d0
+  | Hexadecimal.D7 d0
+  | Hexadecimal.D8 d0
+  | Hexadecimal.D9 d0
+  | Hexadecimal.Da d0
+  | Hexadecimal.Db d0
+  | Hexadecimal.Dc d0
+  | Hexadecimal.Dd d0
+  | Hexadecimal.De d0
+  | Hexadecimal.Df d0 => match d0 with Hexadecimal.Nil => true | _ => false end
+  end.
+
+Definition hex_uint_le_2_hdigits (d : Hexadecimal.uint) : bool :=
+  match d with
+  | Hexadecimal.Nil => true
+  | Hexadecimal.D0 d0
+  | Hexadecimal.D1 d0
+  | Hexadecimal.D2 d0
+  | Hexadecimal.D3 d0
+  | Hexadecimal.D4 d0
+  | Hexadecimal.D5 d0
+  | Hexadecimal.D6 d0
+  | Hexadecimal.D7 d0
+  | Hexadecimal.D8 d0
+  | Hexadecimal.D9 d0
+  | Hexadecimal.Da d0
+  | Hexadecimal.Db d0
+  | Hexadecimal.Dc d0
+  | Hexadecimal.Dd d0
+  | Hexadecimal.De d0
+  | Hexadecimal.Df d0 => hex_uint_le_1_hdigit d0
+  end.
+
+Definition hex_uint_le_3_hdigits (d : Hexadecimal.uint) : bool :=
+  match d with
+  | Hexadecimal.Nil => true
+  | Hexadecimal.D0 d0
+  | Hexadecimal.D1 d0
+  | Hexadecimal.D2 d0
+  | Hexadecimal.D3 d0
+  | Hexadecimal.D4 d0
+  | Hexadecimal.D5 d0
+  | Hexadecimal.D6 d0
+  | Hexadecimal.D7 d0
+  | Hexadecimal.D8 d0
+  | Hexadecimal.D9 d0
+  | Hexadecimal.Da d0
+  | Hexadecimal.Db d0
+  | Hexadecimal.Dc d0
+  | Hexadecimal.Dd d0
+  | Hexadecimal.De d0
+  | Hexadecimal.Df d0 => hex_uint_le_2_hdigits d0
+  end.
+
+Definition hex_uint_le5000 (d : Hexadecimal.uint) : bool :=
+  match d with
+  | Hexadecimal.Nil => true
+  | Hexadecimal.D0 d0
+  | Hexadecimal.D1 d0
+  | Hexadecimal.D2 d0
+  | Hexadecimal.D3 d0
+  | Hexadecimal.D4 d0 => hex_uint_le_3_hdigits d0
+  | Hexadecimal.D5 d0 =>
+      hex_uint_le_2_hdigits d0
+      || match Hexadecimal.nzhead d0 with Hexadecimal.Nil => true | _ => false end
+  | Hexadecimal.D6 d0
+  | Hexadecimal.D7 d0
+  | Hexadecimal.D8 d0
+  | Hexadecimal.D9 d0
+  | Hexadecimal.Da d0
+  | Hexadecimal.Db d0
+  | Hexadecimal.Dc d0
+  | Hexadecimal.Dd d0
+  | Hexadecimal.De d0
+  | Hexadecimal.Df d0 => hex_uint_le_2_hdigits d0
+  end.
+
+Module Type Of_uint_locked.
+Parameter locked : Decimal.uint -> nat.
+Parameter unlock : forall d, locked d = Nat.of_uint d.
+End Of_uint_locked.
+
+Module Of_uint : Of_uint_locked.
+Definition locked := Nat.of_uint.
+Definition unlock d : locked d = Nat.of_uint d := eq_refl.
+End Of_uint.
+
+Definition abstract5000_of_uint (d : Decimal.uint) :=
+  if uint_le5000 d then of_uint d else Of_uint.locked d.
+
+Module Type Of_hex_uint_locked.
+Parameter locked : Hexadecimal.uint -> nat.
+Parameter unlock : forall d, locked d = Nat.of_hex_uint d.
+End Of_hex_uint_locked.
+
+Module Of_hex_uint : Of_hex_uint_locked.
+Definition locked := of_hex_uint.
+Definition unlock d : locked d = Nat.of_hex_uint d := eq_refl.
+End Of_hex_uint.
+
+Definition abstract5000_of_hex_uint (d : Hexadecimal.uint) :=
+  if hex_uint_le5000 d then of_hex_uint d else Of_hex_uint.locked d.
+
+Definition abstract5000_of_num_uint (d : Number.uint) :=
+match d with
+| Number.UIntDecimal d0 => abstract5000_of_uint d0
+| Number.UIntHexadecimal d0 => abstract5000_of_hex_uint d0
+end.
+
 Fixpoint to_little_uint n acc :=
   match n with
   | O => acc
@@ -432,6 +612,6 @@ Arguments of_uint d%_dec_uint_scope.
 Arguments of_int d%_dec_int_scope.
 
 Module Export NumberNotations.
-  Number Notation nat of_num_uint to_num_hex_uint (abstract after 5000) : hex_nat_scope.
-  Number Notation nat of_num_uint to_num_uint (abstract after 5000) : nat_scope.
+  Number Notation nat abstract5000_of_num_uint to_num_hex_uint : hex_nat_scope.
+  Number Notation nat abstract5000_of_num_uint to_num_uint : nat_scope.
 End NumberNotations.