diff --git a/specification/wasm-3.0/4.0-execution.configurations.spectec b/specification/wasm-3.0/4.0-execution.configurations.spectec
index fe794ce214..f1a7284359 100644
--- a/specification/wasm-3.0/4.0-execution.configurations.spectec
+++ b/specification/wasm-3.0/4.0-execution.configurations.spectec
@@ -321,9 +321,11 @@ def $growtable(tableinst, n, r) = tableinst'
   -- if tableinst' = { TYPE (at `[i' .. j?] rt), REFS r'* r^n }
   -- if $(i' = |r'*| + n)
   -- (if i' <= j)?
+  -- if i' <= $(2^$size(at) - 1)
 
 def $growmem(meminst, n) = meminst'
   -- if meminst = { TYPE (at `[i .. j?] PAGE), BYTES b* }
   -- if meminst' = { TYPE (at `[i' .. j?] PAGE), BYTES b* (0x00)^(n * $($(64 * $Ki))) }
   -- if $(i' = |b*| / (64 * $Ki) + n)
   -- (if i' <= j)?
+  -- if i' <= $(2^($size(at) - 16))
diff --git a/specification/wasm-latest/4.0-execution.configurations.spectec b/specification/wasm-latest/4.0-execution.configurations.spectec
index fe794ce214..f1a7284359 100644
--- a/specification/wasm-latest/4.0-execution.configurations.spectec
+++ b/specification/wasm-latest/4.0-execution.configurations.spectec
@@ -321,9 +321,11 @@ def $growtable(tableinst, n, r) = tableinst'
   -- if tableinst' = { TYPE (at `[i' .. j?] rt), REFS r'* r^n }
   -- if $(i' = |r'*| + n)
   -- (if i' <= j)?
+  -- if i' <= $(2^$size(at) - 1)
 
 def $growmem(meminst, n) = meminst'
   -- if meminst = { TYPE (at `[i .. j?] PAGE), BYTES b* }
   -- if meminst' = { TYPE (at `[i' .. j?] PAGE), BYTES b* (0x00)^(n * $($(64 * $Ki))) }
   -- if $(i' = |b*| / (64 * $Ki) + n)
   -- (if i' <= j)?
+  -- if i' <= $(2^($size(at) - 16))
diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf
index 1341c39ec4..e68ccc1d9c 100644
Binary files a/spectec/doc/example/output/NanoWasm.pdf and b/spectec/doc/example/output/NanoWasm.pdf differ
diff --git a/spectec/src/backend-interpreter/interpreter.ml b/spectec/src/backend-interpreter/interpreter.ml
index 532dd79a70..b3b419ca40 100644
--- a/spectec/src/backend-interpreter/interpreter.ml
+++ b/spectec/src/backend-interpreter/interpreter.ml
@@ -214,6 +214,8 @@ and eval_expr env expr =
   let rec to_bool source = function
     | BoolV b -> b
     | ListV _ as v -> List.for_all (to_bool source) (unwrap_listv_to_list v)
+    | OptV None -> true
+    | OptV Some v -> to_bool source v
     | _ -> fail_expr source "type mismatch for boolean value"
   in
 
diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
index 5f4f7ee17f..5aae8c8475 100644
--- a/spectec/test-frontend/TEST.md
+++ b/spectec/test-frontend/TEST.md
@@ -5824,6 +5824,7 @@ def $growtable(tableinst : tableinst, nat : nat, ref : ref) : tableinst
     -- if (tableinst' = {TYPE `%%%`_tabletype(at, `[%..%]`_limits(i', j?{j <- `j?`}), rt), REFS r'*{r' <- `r'*`} ++ r^n{}})
     -- if (i'!`%`_u64.0 = (|r'*{r' <- `r'*`}| + n))
     -- (if (i'!`%`_u64.0 <= j!`%`_u64.0))?{j <- `j?`}
+    -- if ((i'!`%`_u64.0 : nat <:> int) <= (((2 ^ $size((at : addrtype <: numtype))) : nat <:> int) - (1 : nat <:> int)))
 
 ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec
 def $growmem(meminst : meminst, nat : nat) : meminst
@@ -5833,6 +5834,7 @@ def $growmem(meminst : meminst, nat : nat) : meminst
     -- if (meminst' = {TYPE `%%PAGE`_memtype(at, `[%..%]`_limits(i', j?{j <- `j?`})), BYTES b*{b <- `b*`} ++ `%`_byte(0)^(n * (64 * $Ki)){}})
     -- if ((i'!`%`_u64.0 : nat <:> rat) = (((|b*{b <- `b*`}| : nat <:> rat) / ((64 * $Ki) : nat <:> rat)) + (n : nat <:> rat)))
     -- (if (i'!`%`_u64.0 <= j!`%`_u64.0))?{j <- `j?`}
+    -- if (i'!`%`_u64.0 <= (2 ^ ((($size((at : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat)))
 
 ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec
 relation Num_ok: `%|-%:%`(store, num, numtype)
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
index cecc9e3429..07faa4f442 100644
--- a/spectec/test-latex/TEST.md
+++ b/spectec/test-latex/TEST.md
@@ -9315,6 +9315,7 @@ $$
 {\land}~ {\mathit{tableinst}'} = \{ \mathsf{type}~({\mathit{at}}~{}[ {i'} .. {j^?} ]~{\mathit{rt}}),\; \mathsf{refs}~{{r'}^\ast}~{r^{n}} \} \\
 {\land}~ {i'} = {|{{r'}^\ast}|} + n \\
 {\land}~ ({i'} \leq j)^? \\
+{\land}~ {i'} \leq {2^{{|{\mathit{at}}|}}} - 1 \\
 \end{array} \\
 \end{array}
 $$
@@ -9327,6 +9328,7 @@ $$
 {\land}~ {\mathit{meminst}'} = \{ \mathsf{type}~({\mathit{at}}~{}[ {i'} .. {j^?} ]~\mathsf{page}),\; \mathsf{bytes}~{b^\ast}~{(\mathtt{0x00})^{n \cdot 64 \, {\mathrm{Ki}}}} \} \\
 {\land}~ {i'} = {|{b^\ast}|} / (64 \, {\mathrm{Ki}}) + n \\
 {\land}~ ({i'} \leq j)^? \\
+{\land}~ {i'} \leq {2^{{|{\mathit{at}}|} - 16}} \\
 \end{array} \\
 \end{array}
 $$
diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
index 58b31cf997..52de5c986f 100644
--- a/spectec/test-middlend/TEST.md
+++ b/spectec/test-middlend/TEST.md
@@ -5814,6 +5814,7 @@ def $growtable(tableinst : tableinst, nat : nat, ref : ref) : tableinst
     -- if (tableinst' = {TYPE `%%%`_tabletype(at, `[%..%]`_limits(i', j?{j <- `j?`}), rt), REFS r'*{r' <- `r'*`} ++ r^n{}})
     -- if (i'!`%`_u64.0 = (|r'*{r' <- `r'*`}| + n))
     -- (if (i'!`%`_u64.0 <= j!`%`_u64.0))?{j <- `j?`}
+    -- if ((i'!`%`_u64.0 : nat <:> int) <= (((2 ^ $size((at : addrtype <: numtype))) : nat <:> int) - (1 : nat <:> int)))
 
 ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec
 def $growmem(meminst : meminst, nat : nat) : meminst
@@ -5823,6 +5824,7 @@ def $growmem(meminst : meminst, nat : nat) : meminst
     -- if (meminst' = {TYPE `%%PAGE`_memtype(at, `[%..%]`_limits(i', j?{j <- `j?`})), BYTES b*{b <- `b*`} ++ `%`_byte(0)^(n * (64 * $Ki)){}})
     -- if ((i'!`%`_u64.0 : nat <:> rat) = (((|b*{b <- `b*`}| : nat <:> rat) / ((64 * $Ki) : nat <:> rat)) + (n : nat <:> rat)))
     -- (if (i'!`%`_u64.0 <= j!`%`_u64.0))?{j <- `j?`}
+    -- if (i'!`%`_u64.0 <= (2 ^ ((($size((at : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat)))
 
 ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec
 relation Num_ok: `%|-%:%`(store, num, numtype)
@@ -17236,6 +17238,7 @@ def $growtable(tableinst : tableinst, nat : nat, ref : ref) : tableinst?
     -- if (tableinst' = {TYPE `%%%`_tabletype(at, `[%..%]`_limits(i', j?{j <- `j?`}), rt), REFS r'*{r' <- `r'*`} ++ r^n{}})
     -- if (i'!`%`_u64.0 = (|r'*{r' <- `r'*`}| + n))
     -- (if (i'!`%`_u64.0 <= j!`%`_u64.0))?{j <- `j?`}
+    -- if ((i'!`%`_u64.0 : nat <:> int) <= (((2 ^ $size((at : addrtype <: numtype))) : nat <:> int) - (1 : nat <:> int)))
   def $growtable{x0 : tableinst, x1 : nat, x2 : ref}(x0, x1, x2) = ?()
 
 ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec
@@ -17246,6 +17249,7 @@ def $growmem(meminst : meminst, nat : nat) : meminst?
     -- if (meminst' = {TYPE `%%PAGE`_memtype(at, `[%..%]`_limits(i', j?{j <- `j?`})), BYTES b*{b <- `b*`} ++ `%`_byte(0)^(n * (64 * $Ki)){}})
     -- if ((i'!`%`_u64.0 : nat <:> rat) = (((|b*{b <- `b*`}| : nat <:> rat) / ((64 * $Ki) : nat <:> rat)) + (n : nat <:> rat)))
     -- (if (i'!`%`_u64.0 <= j!`%`_u64.0))?{j <- `j?`}
+    -- if (i'!`%`_u64.0 <= (2 ^ ((($size((at : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat)))
   def $growmem{x0 : meminst, x1 : nat}(x0, x1) = ?()
 
 ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec
@@ -28784,6 +28788,7 @@ def $growtable(tableinst : tableinst, nat : nat, ref : ref) : tableinst?
     -- if (tableinst' = {TYPE `%%%`_tabletype(at, `[%..%]`_limits(i', j?{j <- `j?`}), rt), REFS r'*{r' <- `r'*`} ++ r^n{}})
     -- if (i'!`%`_u64.0 = (|r'*{r' <- `r'*`}| + n))
     -- (if (i'!`%`_u64.0 <= j!`%`_u64.0))?{j <- `j?`}
+    -- if ((i'!`%`_u64.0 : nat <:> int) <= (((2 ^ $size((at : addrtype <: numtype))) : nat <:> int) - (1 : nat <:> int)))
   def $growtable{x0 : tableinst, x1 : nat, x2 : ref}(x0, x1, x2) = ?()
 
 ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec
@@ -28794,6 +28799,7 @@ def $growmem(meminst : meminst, nat : nat) : meminst?
     -- if (meminst' = {TYPE `%%PAGE`_memtype(at, `[%..%]`_limits(i', j?{j <- `j?`})), BYTES b*{b <- `b*`} ++ `%`_byte(0)^(n * (64 * $Ki)){}})
     -- if ((i'!`%`_u64.0 : nat <:> rat) = (((|b*{b <- `b*`}| : nat <:> rat) / ((64 * $Ki) : nat <:> rat)) + (n : nat <:> rat)))
     -- (if (i'!`%`_u64.0 <= j!`%`_u64.0))?{j <- `j?`}
+    -- if (i'!`%`_u64.0 <= (2 ^ ((($size((at : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat)))
   def $growmem{x0 : meminst, x1 : nat}(x0, x1) = ?()
 
 ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
index b414d010c1..1671b3b180 100644
--- a/spectec/test-prose/TEST.md
+++ b/spectec/test-prose/TEST.md
@@ -25846,7 +25846,11 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i
 
 #. Let :math:`{i'}` be :math:`{|{{r'}^\ast}|} + n`.
 
-#. If :math:`{({i'} \leq j)^?}`, then:
+#. If not :math:`{({i'} \leq j)^?}`, then:
+
+   a. Fail.
+
+#. If :math:`{i'} \leq {2^{{|{\mathit{at}}|}}} - 1`, then:
 
    a. Let :math:`{\mathit{tableinst}'}` be the table instance :math:`\{ \mathsf{type}~({\mathit{at}}~{}[ {i'} .. {j^?} ]~{\mathit{rt}}),\;\allowbreak \mathsf{refs}~{{r'}^\ast}~{r^{n}} \}`.
 
@@ -25863,7 +25867,11 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i
 
 #. Let :math:`{i'}` be :math:`{|{b^\ast}|} / (64 \, {\mathrm{Ki}}) + n`.
 
-#. If :math:`{({i'} \leq j)^?}`, then:
+#. If not :math:`{({i'} \leq j)^?}`, then:
+
+   a. Fail.
+
+#. If :math:`{i'} \leq {2^{{|{\mathit{at}}|} - 16}}`, then:
 
    a. Let :math:`{\mathit{meminst}'}` be the memory instance :math:`\{ \mathsf{type}~({\mathit{at}}~{}[ {i'} .. {j^?} ]~\mathsf{page}),\;\allowbreak \mathsf{bytes}~{b^\ast}~{\mathtt{0x00}^{n \cdot 64 \, {\mathrm{Ki}}}} \}`.
 
@@ -32736,18 +32744,22 @@ add_exninst z exn*
 growtable tableinst n r
 1. Let { TYPE: (at ([ i .. j? ]) rt); REFS: r'* } be tableinst.
 2. Let i' be (|r'*| + n).
-3. If (i' <= j)?, then:
+3. If not (i' <= j)?, then:
+  a. Fail.
+4. If (i' <= ((2 ^ $size(at)) - 1)), then:
   a. Let tableinst' be { TYPE: (at ([ i' .. j? ]) rt); REFS: r'* :: r^n }.
   b. Return tableinst'.
-4. Fail.
+5. Fail.
 
 growmem meminst n
 1. Let { TYPE: at ([ i .. j? ]) PAGE; BYTES: b* } be meminst.
 2. Let i' be ((|b*| / (64 * $Ki())) + n).
-3. If (i' <= j)?, then:
+3. If not (i' <= j)?, then:
+  a. Fail.
+4. If (i' <= (2 ^ ($size(at) - 16))), then:
   a. Let meminst' be { TYPE: at ([ i' .. j? ]) PAGE; BYTES: b* :: 0^(n * (64 * $Ki())) }.
   b. Return meminst'.
-4. Fail.
+5. Fail.
 
 inst_valtype moduleinst t
 1. Let dt* be moduleinst.TYPES.