From f83a375df438067de1eafc25a2b5e249b7115a92 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 21 Nov 2023 09:03:52 +0100 Subject: [PATCH] [spec] Add missing length condition to br_table prose (#1709) --- document/core/valid/instructions.rst | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index afcda69c01..43dfe9abfb 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1412,17 +1412,22 @@ Control Instructions ........................... -* The label :math:`C.\CLABELS[l_N]` must be defined in the context. +* The :ref:`label ` :math:`C.\CLABELS[l_N]` must be defined in the context. -* For all :math:`l_i` in :math:`l^\ast`, +* For each :ref:`label ` :math:`l_i` in :math:`l^\ast`, the label :math:`C.\CLABELS[l_i]` must be defined in the context. * There must be a sequence :math:`t^\ast` of :ref:`operand types `, such that: + * The length of the sequence :math:`t^\ast` is the same as the length of the sequence :math:`C.\CLABELS[l_N]`. + * For each :ref:`operand type ` :math:`t_j` in :math:`t^\ast` and corresponding type :math:`t'_{Nj}` in :math:`C.\CLABELS[l_N]`, :math:`t_j` :ref:`matches ` :math:`t'_{Nj}`. - * For all :math:`l_i` in :math:`l^\ast`, - and for each :ref:`operand type ` :math:`t_j` in :math:`t^\ast` and corresponding type :math:`t'_{ij}` in :math:`C.\CLABELS[l_i]`, :math:`t_j` :ref:`matches ` :math:`t'_{ij}`. + * For each :ref:`label ` :math:`l_i` in :math:`l^\ast`: + + * The length of the sequence :math:`t^\ast` is the same as the length of the sequence :math:`C.\CLABELS[l_i]`. + + * For each :ref:`operand type ` :math:`t_j` in :math:`t^\ast` and corresponding type :math:`t'_{ij}` in :math:`C.\CLABELS[l_i]`, :math:`t_j` :ref:`matches ` :math:`t'_{ij}`. * Then the instruction is valid with type :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]`, for any sequences of :ref:`operand types ` :math:`t_1^\ast` and :math:`t_2^\ast`.