diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index 72c83ea56f..9b2c9a5b8d 100644 --- a/document/core/appendix/algorithm.rst +++ b/document/core/appendix/algorithm.rst @@ -140,6 +140,8 @@ The type of the :ref:`label ` associated with a control frame is e Finally, the current frame can be marked as unreachable. In that case, all existing operand types are purged from the value stack, in order to allow for the :ref:`stack-polymorphism ` logic in :code:`pop_val` to take effect. +Because every function has an implicit outermost label that corresponds to an implicit block frame, +it is an invariant of the validation algorithm that there always is at least one frame on the control stack when validating an instruction, and hence, `ctrls[0]` is always defined. .. note:: Even with the unreachable flag set, consecutive operands are still pushed to and popped from the operand stack.