From f08791b6e824884153f1079673faac441d548f5a Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 27 Jun 2022 11:53:11 +0200 Subject: [PATCH] [spec] Add note about control stack invariant to algorithm --- document/core/appendix/algorithm.rst | 2 ++ 1 file changed, 2 insertions(+) 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.