[spec] Fix upper bound for UTF-8 binary encoding (#2274)

specification/wasm-1.0/A-binary.spectec

diff --git a/specification/wasm-1.0/A-binary.spectec b/specification/wasm-1.0/A-binary.spectec
index ce3ede9..552a61a 100644
--- a/specification/wasm-1.0/A-binary.spectec
+++ b/specification/wasm-1.0/A-binary.spectec
@@ -52,7 +52,7 @@
 def $utf8(ch) = b  -- if ch < U+0080 /\ ch = b
 def $utf8(ch) = b_1 b_2  -- if U+0080 <= ch < U+0800 /\ ch = $(2^6*(b_1 - 0xC0) + (b_2 - 0x80))
 def $utf8(ch) = b_1 b_2 b_3  -- if (U+0800 <= ch < U+D800 \/ U+E000 <= ch < U+10000) /\ ch = $(2^12*(b_1 - 0xE0) + 2^6*(b_2 - 0x80) + (b_3 - 0x80))
-def $utf8(ch) = b_1 b_2 b_3 b_4  -- if (U+10000 <= ch < U+11000) /\ ch = $(2^18*(b_1 - 0xF0) + 2^12*(b_2 - 0x80) + 2^6*(b_3 - 0x80) + (b_4 - 0x80))
+def $utf8(ch) = b_1 b_2 b_3 b_4  -- if (U+10000 <= ch < U+110000) /\ ch = $(2^18*(b_1 - 0xF0) + 2^12*(b_2 - 0x80) + 2^6*(b_3 - 0x80) + (b_4 - 0x80))
 def $utf8(ch*) = $concat_(byte, $utf8(ch)*)
 
 grammar Bname : name =

specification/wasm-2.0/A-binary.spectec

diff --git a/specification/wasm-2.0/A-binary.spectec b/specification/wasm-2.0/A-binary.spectec
index 8570e0b..5935ad3 100644
--- a/specification/wasm-2.0/A-binary.spectec
+++ b/specification/wasm-2.0/A-binary.spectec
@@ -54,7 +54,7 @@
 def $utf8(ch) = b  -- if ch < U+0080 /\ ch = b
 def $utf8(ch) = b_1 b_2  -- if U+0080 <= ch < U+0800 /\ ch = $(2^6*(b_1 - 0xC0) + (b_2 - 0x80))
 def $utf8(ch) = b_1 b_2 b_3  -- if (U+0800 <= ch < U+D800 \/ U+E000 <= ch < U+10000) /\ ch = $(2^12*(b_1 - 0xE0) + 2^6*(b_2 - 0x80) + (b_3 - 0x80))
-def $utf8(ch) = b_1 b_2 b_3 b_4  -- if (U+10000 <= ch < U+11000) /\ ch = $(2^18*(b_1 - 0xF0) + 2^12*(b_2 - 0x80) + 2^6*(b_3 - 0x80) + (b_4 - 0x80))
+def $utf8(ch) = b_1 b_2 b_3 b_4  -- if (U+10000 <= ch < U+110000) /\ ch = $(2^18*(b_1 - 0xF0) + 2^12*(b_2 - 0x80) + 2^6*(b_3 - 0x80) + (b_4 - 0x80))
 def $utf8(ch*) = $concat_(byte, $utf8(ch)*)
 
 grammar Bname : name =

specification/wasm-3.0/5.1-binary.values.spectec

diff --git a/specification/wasm-3.0/5.1-binary.values.spectec b/specification/wasm-3.0/5.1-binary.values.spectec
index 6bb898d..4034c01 100644
--- a/specification/wasm-3.0/5.1-binary.values.spectec
+++ b/specification/wasm-3.0/5.1-binary.values.spectec
@@ -60,7 +60,7 @@
   -- if U+0800 <= ch < U+D800 \/ U+E000 <= ch < U+10000
   -- if ch = $(2^12*(b_1 - 0xE0) + 2^6*$cont(b_2) + $cont(b_3))
 def $utf8(ch) = b_1 b_2 b_3 b_4
-  -- if U+10000 <= ch < U+11000
+  -- if U+10000 <= ch < U+110000
   -- if ch = $(2^18*(b_1 - 0xF0) + 2^12*$cont(b_2) + 2^6*$cont(b_3) + $cont(b_4))
 
 grammar Bname : name =

specification/wasm-latest/5.1-binary.values.spectec

diff --git a/specification/wasm-latest/5.1-binary.values.spectec b/specification/wasm-latest/5.1-binary.values.spectec
index 6bb898d..4034c01 100644
--- a/specification/wasm-latest/5.1-binary.values.spectec
+++ b/specification/wasm-latest/5.1-binary.values.spectec
@@ -60,7 +60,7 @@
   -- if U+0800 <= ch < U+D800 \/ U+E000 <= ch < U+10000
   -- if ch = $(2^12*(b_1 - 0xE0) + 2^6*$cont(b_2) + $cont(b_3))
 def $utf8(ch) = b_1 b_2 b_3 b_4
-  -- if U+10000 <= ch < U+11000
+  -- if U+10000 <= ch < U+110000
   -- if ch = $(2^18*(b_1 - 0xF0) + 2^12*$cont(b_2) + 2^6*$cont(b_3) + $cont(b_4))
 
 grammar Bname : name =

spectec/test-frontend/TEST.md

diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
index cb87eda..46ca315 100644
--- a/spectec/test-frontend/TEST.md
+++ b/spectec/test-frontend/TEST.md
@@ -801,7 +801,7 @@
     -- if (ch!`%`_char.0 = ((((2 ^ 12) * (((b_1!`%`_byte.0 : nat <:> int) - (224 : nat <:> int)) : int <:> nat)) + ((2 ^ 6) * $cont(b_2))) + $cont(b_3)))
   ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec:62.1-64.82
   def $utf8{ch : char, b_1 : byte, b_2 : byte, b_3 : byte, b_4 : byte}([ch]) = [b_1 b_2 b_3 b_4]
-    -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 69632))
+    -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 1114112))
     -- if (ch!`%`_char.0 = (((((2 ^ 18) * (((b_1!`%`_byte.0 : nat <:> int) - (240 : nat <:> int)) : int <:> nat)) + ((2 ^ 12) * $cont(b_2))) + ((2 ^ 6) * $cont(b_3))) + $cont(b_4)))
 }
 

spectec/test-latex/TEST.md

diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
index fd4d65c..30daae6 100644
--- a/spectec/test-latex/TEST.md
+++ b/spectec/test-latex/TEST.md
@@ -11569,7 +11569,7 @@
 \end{array} \\
 {\mathrm{utf{\kern-0.1em\scriptstyle 8}}}({\mathit{ch}}) & = & b_1~b_2~b_3~b_4 & \quad
 \begin{array}[t]{@{}l@{}}
-\mbox{if}~ \mathrm{U{+}10000} \leq {\mathit{ch}} < \mathrm{U{+}11000} \\
+\mbox{if}~ \mathrm{U{+}10000} \leq {\mathit{ch}} < \mathrm{U{+}110000} \\
 {\land}~ {\mathit{ch}} = {2^{18}} \cdot (b_1 - \mathtt{0xF0}) + {2^{12}} \cdot {\mathrm{cont}}(b_2) + {2^{6}} \cdot {\mathrm{cont}}(b_3) + {\mathrm{cont}}(b_4) \\
 \end{array} \\
 \end{array}

spectec/test-middlend/TEST.md

diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
index 935453d..219dc65 100644
--- a/spectec/test-middlend/TEST.md
+++ b/spectec/test-middlend/TEST.md
@@ -324,7 +324,7 @@
     -- if (ch!`%`_char.0 = ((((2 ^ 12) * (((b_1!`%`_byte.0 : nat <:> int) - (224 : nat <:> int)) : int <:> nat)) + ((2 ^ 6) * $cont(b_2))) + $cont(b_3)))
   ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec:62.1-64.82
   def $utf8{ch : char, b_1 : byte, b_2 : byte, b_3 : byte, b_4 : byte}([ch]) = [b_1 b_2 b_3 b_4]
-    -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 69632))
+    -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 1114112))
     -- if (ch!`%`_char.0 = (((((2 ^ 18) * (((b_1!`%`_byte.0 : nat <:> int) - (240 : nat <:> int)) : int <:> nat)) + ((2 ^ 12) * $cont(b_2))) + ((2 ^ 6) * $cont(b_3))) + $cont(b_4)))
 }
 
@@ -12231,7 +12231,7 @@
     -- if (ch!`%`_char.0 = ((((2 ^ 12) * (((b_1!`%`_byte.0 : nat <:> int) - (224 : nat <:> int)) : int <:> nat)) + ((2 ^ 6) * $cont(b_2))) + $cont(b_3)))
   ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec:62.1-64.82
   def $utf8{ch : char, b_1 : byte, b_2 : byte, b_3 : byte, b_4 : byte}([ch]) = [b_1 b_2 b_3 b_4]
-    -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 69632))
+    -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 1114112))
     -- if (ch!`%`_char.0 = (((((2 ^ 18) * (((b_1!`%`_byte.0 : nat <:> int) - (240 : nat <:> int)) : int <:> nat)) + ((2 ^ 12) * $cont(b_2))) + ((2 ^ 6) * $cont(b_3))) + $cont(b_4)))
 }
 
@@ -24147,7 +24147,7 @@
     -- if (ch!`%`_char.0 = ((((2 ^ 12) * (((b_1!`%`_byte.0 : nat <:> int) - (224 : nat <:> int)) : int <:> nat)) + ((2 ^ 6) * $cont(b_2))) + $cont(b_3)))
   ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec:62.1-64.82
   def $utf8{ch : char, b_1 : byte, b_2 : byte, b_3 : byte, b_4 : byte}([ch]) = [b_1 b_2 b_3 b_4]
-    -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 69632))
+    -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 1114112))
     -- if (ch!`%`_char.0 = (((((2 ^ 18) * (((b_1!`%`_byte.0 : nat <:> int) - (240 : nat <:> int)) : int <:> nat)) + ((2 ^ 12) * $cont(b_2))) + ((2 ^ 6) * $cont(b_3))) + $cont(b_4)))
 }