explicit check for (experimentally determined) border value

--- a/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Thu Jan 16 09:26:56 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Thu Jan 16 09:26:57 2025 +0100
@@ -60,4 +60,25 @@
 test_code check in GHC
 test_code check in Scala
 
+text \<open>Checking the index maximum for \<text>\<open>SML\<close>\<close>
+
+ML \<open>
+fun check_max max =
+  let
+    val _ = IntInf.~>> (0, max);
+    val _ = \<^assert> ((IntInf.~>> (0, Word.+ (max, Word.fromInt 1)); false) handle Size => true)
+  in () end;
+\<close>
+
+definition \<open>check_max = ()\<close>
+
+code_printing constant check \<rightharpoonup>
+  (Eval) "check'_max Bit'_Shifts.word'_max'_index"
+
+definition \<open>anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\<close>
+
+ML \<open>
+\<^code>\<open>anchor\<close>;
+\<close>
+
 end

--- a/src/HOL/Library/Code_Target_Bit_Shifts.thy	Thu Jan 16 09:26:56 2025 +0100
+++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy	Thu Jan 16 09:26:57 2025 +0100
@@ -41,6 +41,7 @@
   type int = IntInf.int
   val push : int -> int -> int
   val drop : int -> int -> int
+  val word_max_index : Word.word (*only for validation*)
 end = struct
 
 type int = IntInf.int;