From 820f1b7a7815be7b1dbddd8db3c6d3fe262686a4 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 21 Oct 2022 21:27:19 +0200 Subject: [PATCH 1/7] Address additional review of #222, also fixing label types everywhere. This addresses additional review comments to PR #222, that were made after it was merged. The last review comment in the discussion suggests to adjust all validation labels to use label types instead of just result types. Should address all occurrences of validation labels. Additionally adds a boolean catch_label to control frames in the validation algorithm, and some related functionality, fixing the cases for opcodes `catch` and `catch_all`. --- document/core/appendix/algorithm.rst | 32 ++++++++++++------ document/core/appendix/properties.rst | 16 ++++----- document/core/valid/instructions.rst | 48 ++++++++++++++------------- document/core/valid/modules.rst | 2 +- 4 files changed, 56 insertions(+), 42 deletions(-) diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index d03882b9..6e7dee47 100644 --- a/document/core/appendix/algorithm.rst +++ b/document/core/appendix/algorithm.rst @@ -16,7 +16,7 @@ Consequently, it can be integrated directly into a decoder. The algorithm is expressed in typed pseudo code whose semantics is intended to be self-explanatory. -.. index:: value type, stack, label, frame, instruction +.. index:: value type, label type, stack, label, frame, instruction Data Structures ~~~~~~~~~~~~~~~ @@ -51,6 +51,7 @@ the latter surrounding :ref:`structured control instructions `, or :code:`Unknown` when the type is not known. @@ -122,9 +123,16 @@ The control stack is likewise manipulated through auxiliary functions: ctrls.pop() return frame - func label_types(frame : ctrl_frame) : list(val_types) = + func label_val_types(frame : ctrl_frame) : list(val_type) = return (if frame.opcode == loop then frame.start_types else frame.end_types) + func is_catch(frame : ctrl_frame) : bool = + return frame.catch_label + + func set_catch(catch : bool) = + error_if(ctrls.is_empty()) + ctrls[0].catch_label := catch + func unreachable() = vals.resize(ctrls[0].height) ctrls[0].unreachable := true @@ -136,7 +144,9 @@ Popping a frame first checks that the control stack is not empty. It then verifies that the operand stack contains the right types of values expected at the end of the exited block and pops them off the operand stack. Afterwards, it checks that the stack has shrunk back to its initial height. -The type of the :ref:`label ` associated with a control frame is either that of the stack at the start or the end of the frame, determined by the opcode that it originates from. +The result type of the :ref:`label ` associated with a control frame is either that of the stack at the start or the end of the frame, determined by the opcode that it originates from. + +Whether a label has :ref:`label type ` with present |LCATCH| is stored with the boolean :math:`catch_label` of the frame, which can be checked with :math:`is_catch`, or modified in the top control frame with :math:`set_catch`. 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. @@ -219,32 +229,34 @@ Other instructions are checked in a similar manner. error_if(frame.opcode =/= try || frame.opcode =/= catch) let params = tags[x].type.params push_ctrl(catch, params , frame.end_types) + if (frame.opcode =/= try) then set_catch(true) case (catch_all) let frame = pop_ctrl() error_if(frame.opcode =/= try || frame.opcode =/= catch) push_ctrl(catch_all, [], frame.end_types) + if (frame.opcode =/= try) then set_catch(true) case (br n) error_if(ctrls.size() < n) - pop_vals(label_types(ctrls[n])) + pop_vals(label_val_types(ctrls[n])) unreachable() case (br_if n) error_if(ctrls.size() < n) pop_val(I32) - pop_vals(label_types(ctrls[n])) - push_vals(label_types(ctrls[n])) + pop_vals(label_val_types(ctrls[n])) + push_vals(label_val_types(ctrls[n])) case (br_table n* m) pop_val(I32) error_if(ctrls.size() < m) - let arity = label_types(ctrls[m]).size() + let arity = label_val_types(ctrls[m]).size() foreach (n in n*) error_if(ctrls.size() < n) - error_if(label_types(ctrls[n]).size() =/= arity) - push_vals(pop_vals(label_types(ctrls[n]))) - pop_vals(label_types(ctrls[m])) + error_if(label_val_types(ctrls[n]).size() =/= arity) + push_vals(pop_vals(label_val_types(ctrls[n]))) + pop_vals(label_val_types(ctrls[m])) unreachable() .. todo:: diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 837ecb8c..472039fa 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -655,7 +655,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera \frac{ S; C,\CLABELS\,[t^\ast] \vdashinstrseq \instr^\ast : [] \to [t^\ast] \qquad - C.\CLABELS[l] = [t_0^\ast] + C.\CLABELS[l] = \LCATCH^?~[t_0^\ast] }{ S; C,\CLABELS\,[t^\ast] \vdashadmininstr \DELEGATEadm\{l\}~\instr^\ast~\END : [] \to [t^\ast] } @@ -670,14 +670,14 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera * The :ref:`values ` :math:`\val^\ast` must be of type :math:`[t_0^\ast]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector. +* The label type :math:`C.\CLABELS[0]` must be defined in the context. + +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`C.\CLABELS[0]` modified to :math:`(\LCATCH~[t^\ast])` in the |CLABELS| vector. * Under context :math:`C'`, the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^\ast]`. -* Let :math:`C''` be the same :ref:`context ` as :math:`C`, but with the label :math:`[t^\ast]` prepended to the |CLABELS| vector. - -* Then the compound instruction is valid under context :math:`C''` with type :math:`[] \to [t^\ast]`. +* Then the compound instruction is valid under context :math:`C` with type :math:`[] \to [t^\ast]`. .. math:: @@ -686,9 +686,9 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera \qquad (val : t_0)^\ast \qquad - S; C,\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] + S; C,\CLABELS[0]:=(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] }{ - S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] + S; C \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] } @@ -716,7 +716,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera * The instruction sequence :math:`\instr_0^\ast` must be :ref:`valid ` with some type :math:`[t_1^n] \to [t_2^*]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_1^n]` prepended to the |CLABELS| vector. +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`[t_1^n]` prepended to the |CLABELS| vector. * Under context :math:`C'`, the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t_2^*]`. diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index dc5efe55..0c0e8a1d 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1234,7 +1234,7 @@ Memory Instructions } -.. index:: control instructions, structured control, label, block, branch, block type, label index, function index, type index, tag index, vector, polymorphism, context +.. index:: control instructions, structured control, label, block, branch, block type, label index, label type, function index, type index, tag index, vector, polymorphism, context pair: validation; instruction single: abstract syntax; instruction .. _valid-label: @@ -1281,7 +1281,7 @@ Control Instructions * The :ref:`block type ` must be :ref:`valid ` as some :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. @@ -1308,7 +1308,7 @@ Control Instructions * The :ref:`block type ` must be :ref:`valid ` as some :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_1^\ast]` prepended to the |CLABELS| vector. +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`[t_1^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. @@ -1335,7 +1335,7 @@ Control Instructions * The :ref:`block type ` must be :ref:`valid ` as some :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. @@ -1368,23 +1368,25 @@ Control Instructions * The :ref:`block type ` must be :ref:`valid ` as some :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. -* Let :math:`C''` be the same :ref:`context ` as :math:`C`, but with the :ref:`label ` :math:`\LCATCH~[t_2^\ast]` prepended to the |CLABELS| vector. +* Let :math:`C''` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`\LCATCH~[t_2^\ast]` prepended to the |CLABELS| vector. -* For every :math:`(\CATCH~x~\instr_2^\ast)`: +* For every :math:`x_i` and :math:`\instr_{2i}^\ast` in :math:`(\CATCH~x~\instr_2^\ast)^\ast`: * The tag :math:`C.\CTAGS[x]` must be defined in the context :math:`C`. - * Let :math:`[t^\ast] \to []` be its :ref:`tag type `. + * Let :math:`[t_{3i}^\ast] \to [t_{4i}^\ast]` be the :ref:`tag type ` :math:`C.\tags[x]`. + + * The :ref:`result type ` :math:`[t_{4i}^\ast]` must be empty. * Under context :math:`C''`, - the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid ` with type :math:`[t^\ast] \to [t_2^\ast]`. + the instruction sequence :math:`\instr_{2i}^\ast` must be :ref:`valid ` with type :math:`[t_{3i}^\ast] \to [t_2^\ast]`. -* If there is a :math:`(\CATCHALL~\instr_3^\ast)`, then: +* If :math:`(\CATCHALL~\instr_3^\ast)^?` is not empty, then: * Under context :math:`C''`, the instruction sequence :math:`\instr_3^\ast` must be :ref:`valid ` with type :math:`[] \to [t_2^\ast]`. @@ -1458,11 +1460,11 @@ Control Instructions :math:`\RETHROW~l` .................. -* The label :math:`C.\CLABELS[l]` must be defined in the context. +* The label type :math:`C.\CLABELS[l]` must be defined in the context. -* Let :math:`(\LCATCH^?~[t^\ast])` be the :ref:`label type ` :math:`C.\CLABELS[l]`. +* Let :math:`(\LCATCH^?~[t^\ast])` be the :ref:`label type ` :math:`C.\CLABELS[l]`. -* The |LCATCH| must be present in the :ref:`label type ` :math:`C.\CLABELS[l]`. +* The |LCATCH| must be present in the :ref:`label type ` :math:`C.\CLABELS[l]`. * Then the instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. @@ -1485,21 +1487,21 @@ Control Instructions :math:`\BR~l` ............. -* The label :math:`C.\CLABELS[l]` must be defined in the context. +* The label type :math:`C.\CLABELS[l]` must be defined in the context. -* Let :math:`[t^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. +* Let :math:`\LCATCH^?~[t^\ast]` be the :ref:`label type ` :math:`C.\CLABELS[l]`. * Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ - C.\CLABELS[l] = [t^\ast] + C.\CLABELS[l] = \LCATCH^?~[t^\ast] }{ C \vdashinstr \BR~l : [t_1^\ast~t^\ast] \to [t_2^\ast] } .. note:: - The :ref:`label index ` space in the :ref:`context ` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected. + The :ref:`label index ` space in the :ref:`context ` :math:`C` contains the most recent label type first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected. The |BR| instruction is :ref:`stack-polymorphic `. @@ -1509,21 +1511,21 @@ Control Instructions :math:`\BRIF~l` ............... -* The label :math:`C.\CLABELS[l]` must be defined in the context. +* The label type :math:`C.\CLABELS[l]` must be defined in the context. -* Let :math:`[t^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. +* Let :math:`\LCATCH^?~[t^\ast]` be the :ref:`label type ` :math:`C.\CLABELS[l]`. * Then the instruction is valid with type :math:`[t^\ast~\I32] \to [t^\ast]`. .. math:: \frac{ - C.\CLABELS[l] = [t^\ast] + C.\CLABELS[l] = \LCATCH^?~[t^\ast] }{ C \vdashinstr \BRIF~l : [t^\ast~\I32] \to [t^\ast] } .. note:: - The :ref:`label index ` space in the :ref:`context ` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected. + The :ref:`label index ` space in the :ref:`context ` :math:`C` contains the most recent label type first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected. .. _valid-br_table: @@ -1532,10 +1534,10 @@ Control Instructions ........................... -* The label :math:`C.\CLABELS[l_N]` must be defined in the context. +* The label type :math:`C.\CLABELS[l_N]` must be defined in the context. * For all :math:`l_i` in :math:`l^\ast`, - the label :math:`C.\CLABELS[l_i]` must be defined in the context. + the label type :math:`C.\CLABELS[l_i]` must be defined in the context. * There must be a :ref:`result type ` :math:`[t^\ast]`, such that: diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 71a8b1ef..ddf2815c 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -29,7 +29,7 @@ Functions :math:`\func` are classified by :ref:`function types * |CLOCALS| set to the sequence of :ref:`value types ` :math:`t_1^\ast~t^\ast`, concatenating parameters and locals, - * |CLABELS| set to the singular sequence containing only :ref:`result type ` :math:`[t_2^\ast]`. + * |CLABELS| set to the singular sequence containing only :ref:`label type ` :math:`[t_2^\ast]`. * |CRETURN| set to the :ref:`result type ` :math:`[t_2^\ast]`. From 201ff276be6c458e7a819662eb2862bd475f2fcd Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Mon, 24 Oct 2022 19:04:44 +0200 Subject: [PATCH 2/7] fixed typo --- document/core/valid/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 0c0e8a1d..ae662edf 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1379,7 +1379,7 @@ Control Instructions * The tag :math:`C.\CTAGS[x]` must be defined in the context :math:`C`. - * Let :math:`[t_{3i}^\ast] \to [t_{4i}^\ast]` be the :ref:`tag type ` :math:`C.\tags[x]`. + * Let :math:`[t_{3i}^\ast] \to [t_{4i}^\ast]` be the :ref:`tag type ` :math:`C.\CTAGS[x]`. * The :ref:`result type ` :math:`[t_{4i}^\ast]` must be empty. From 41dd586d1ab2700b9662ace5d2eac2788d937a98 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Thu, 17 Nov 2022 23:48:17 +0100 Subject: [PATCH 3/7] Apply suggestions from code review Co-authored-by: Andreas Rossberg --- document/core/appendix/algorithm.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index 6e7dee47..873f7699 100644 --- a/document/core/appendix/algorithm.rst +++ b/document/core/appendix/algorithm.rst @@ -127,7 +127,7 @@ The control stack is likewise manipulated through auxiliary functions: return (if frame.opcode == loop then frame.start_types else frame.end_types) func is_catch(frame : ctrl_frame) : bool = - return frame.catch_label + return frame.opcode = catch || frame.opcode = catch_all func set_catch(catch : bool) = error_if(ctrls.is_empty()) From f97c9d108a999c3c3fd30f25554a113822bed1b8 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 18 Nov 2022 00:50:27 +0100 Subject: [PATCH 4/7] Addressed review comments. --- document/core/appendix/algorithm.rst | 32 +++++++++------------------ document/core/appendix/properties.rst | 11 +++++---- document/core/valid/instructions.rst | 10 ++++----- 3 files changed, 20 insertions(+), 33 deletions(-) diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index 873f7699..8269bb21 100644 --- a/document/core/appendix/algorithm.rst +++ b/document/core/appendix/algorithm.rst @@ -16,7 +16,7 @@ Consequently, it can be integrated directly into a decoder. The algorithm is expressed in typed pseudo code whose semantics is intended to be self-explanatory. -.. index:: value type, label type, stack, label, frame, instruction +.. index:: value type, stack, label, frame, instruction Data Structures ~~~~~~~~~~~~~~~ @@ -51,7 +51,6 @@ the latter surrounding :ref:`structured control instructions `, or :code:`Unknown` when the type is not known. @@ -123,16 +122,9 @@ The control stack is likewise manipulated through auxiliary functions: ctrls.pop() return frame - func label_val_types(frame : ctrl_frame) : list(val_type) = + func label_types(frame : ctrl_frame) : list(val_type) = return (if frame.opcode == loop then frame.start_types else frame.end_types) - func is_catch(frame : ctrl_frame) : bool = - return frame.opcode = catch || frame.opcode = catch_all - - func set_catch(catch : bool) = - error_if(ctrls.is_empty()) - ctrls[0].catch_label := catch - func unreachable() = vals.resize(ctrls[0].height) ctrls[0].unreachable := true @@ -144,9 +136,7 @@ Popping a frame first checks that the control stack is not empty. It then verifies that the operand stack contains the right types of values expected at the end of the exited block and pops them off the operand stack. Afterwards, it checks that the stack has shrunk back to its initial height. -The result type of the :ref:`label ` associated with a control frame is either that of the stack at the start or the end of the frame, determined by the opcode that it originates from. - -Whether a label has :ref:`label type ` with present |LCATCH| is stored with the boolean :math:`catch_label` of the frame, which can be checked with :math:`is_catch`, or modified in the top control frame with :math:`set_catch`. +The type of the :ref:`label ` associated with a control frame is either that of the stack at the start or the end of the frame, determined by the opcode that it originates from. 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. @@ -229,34 +219,32 @@ Other instructions are checked in a similar manner. error_if(frame.opcode =/= try || frame.opcode =/= catch) let params = tags[x].type.params push_ctrl(catch, params , frame.end_types) - if (frame.opcode =/= try) then set_catch(true) case (catch_all) let frame = pop_ctrl() error_if(frame.opcode =/= try || frame.opcode =/= catch) push_ctrl(catch_all, [], frame.end_types) - if (frame.opcode =/= try) then set_catch(true) case (br n) error_if(ctrls.size() < n) - pop_vals(label_val_types(ctrls[n])) + pop_vals(label_types(ctrls[n])) unreachable() case (br_if n) error_if(ctrls.size() < n) pop_val(I32) - pop_vals(label_val_types(ctrls[n])) - push_vals(label_val_types(ctrls[n])) + pop_vals(label_types(ctrls[n])) + push_vals(label_types(ctrls[n])) case (br_table n* m) pop_val(I32) error_if(ctrls.size() < m) - let arity = label_val_types(ctrls[m]).size() + let arity = label_types(ctrls[m]).size() foreach (n in n*) error_if(ctrls.size() < n) - error_if(label_val_types(ctrls[n]).size() =/= arity) - push_vals(pop_vals(label_val_types(ctrls[n]))) - pop_vals(label_val_types(ctrls[m])) + error_if(label_types(ctrls[n]).size() =/= arity) + push_vals(pop_vals(label_types(ctrls[n]))) + pop_vals(label_types(ctrls[m])) unreachable() .. todo:: diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 472039fa..c2a9c792 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -670,15 +670,14 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera * The :ref:`values ` :math:`\val^\ast` must be of type :math:`[t_0^\ast]`. -* The label type :math:`C.\CLABELS[0]` must be defined in the context. - -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`C.\CLABELS[0]` modified to :math:`(\LCATCH~[t^\ast])` in the |CLABELS| vector. +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector. * Under context :math:`C'`, the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^\ast]`. -* Then the compound instruction is valid under context :math:`C` with type :math:`[] \to [t^\ast]`. +* Let :math:`C''` be the same :ref:`context ` as :math:`C`, but with the label :math:`[t^\ast]` prepended to the |CLABELS| vector. +* Then the compound instruction is valid under context :math:`C''` with type :math:`[] \to [t^\ast]`. .. math:: \frac{ @@ -686,9 +685,9 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera \qquad (val : t_0)^\ast \qquad - S; C,\CLABELS[0]:=(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] + S; C,\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] }{ - S; C \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] + S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] } diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index ae662edf..77df7816 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1460,7 +1460,7 @@ Control Instructions :math:`\RETHROW~l` .................. -* The label type :math:`C.\CLABELS[l]` must be defined in the context. +* The label :math:`C.\CLABELS[l]` must be defined in the context. * Let :math:`(\LCATCH^?~[t^\ast])` be the :ref:`label type ` :math:`C.\CLABELS[l]`. @@ -1487,7 +1487,7 @@ Control Instructions :math:`\BR~l` ............. -* The label type :math:`C.\CLABELS[l]` must be defined in the context. +* The label :math:`C.\CLABELS[l]` must be defined in the context. * Let :math:`\LCATCH^?~[t^\ast]` be the :ref:`label type ` :math:`C.\CLABELS[l]`. @@ -1511,7 +1511,7 @@ Control Instructions :math:`\BRIF~l` ............... -* The label type :math:`C.\CLABELS[l]` must be defined in the context. +* The label :math:`C.\CLABELS[l]` must be defined in the context. * Let :math:`\LCATCH^?~[t^\ast]` be the :ref:`label type ` :math:`C.\CLABELS[l]`. @@ -1534,10 +1534,10 @@ Control Instructions ........................... -* The label type :math:`C.\CLABELS[l_N]` must be defined in the context. +* The label :math:`C.\CLABELS[l_N]` must be defined in the context. * For all :math:`l_i` in :math:`l^\ast`, - the label type :math:`C.\CLABELS[l_i]` must be defined in the context. + the label :math:`C.\CLABELS[l_i]` must be defined in the context. * There must be a :ref:`result type ` :math:`[t^\ast]`, such that: From 5f48ba47e4f7af6dedc36f4333e4c95676f87310 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Wed, 23 Nov 2022 16:48:23 +0100 Subject: [PATCH 5/7] Apply suggestions from code review Co-authored-by: Heejin Ahn --- document/core/valid/instructions.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 77df7816..b7799f33 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1377,9 +1377,9 @@ Control Instructions * For every :math:`x_i` and :math:`\instr_{2i}^\ast` in :math:`(\CATCH~x~\instr_2^\ast)^\ast`: - * The tag :math:`C.\CTAGS[x]` must be defined in the context :math:`C`. + * The tag :math:`C.\CTAGS[x_i]` must be defined in the context :math:`C`. - * Let :math:`[t_{3i}^\ast] \to [t_{4i}^\ast]` be the :ref:`tag type ` :math:`C.\CTAGS[x]`. + * Let :math:`[t_{3i}^\ast] \to [t_{4i}^\ast]` be the :ref:`tag type ` :math:`C.\CTAGS[x_i]`. * The :ref:`result type ` :math:`[t_{4i}^\ast]` must be empty. From 77090e2abfa65e95ad15836ff896a244b1d0e751 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Sat, 26 Nov 2022 13:03:29 +0100 Subject: [PATCH 6/7] Reverting changes to typing of CAUGHTadm. Changes to this rule are now done in PR #244 --- document/core/appendix/properties.rst | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index c2a9c792..cfecf1d4 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -670,14 +670,14 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera * The :ref:`values ` :math:`\val^\ast` must be of type :math:`[t_0^\ast]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector. +* The label type :math:`C.\CLABELS[0]` must be defined in the context. + +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`C.\CLABELS[0]` modified to :math:`(\LCATCH~[t^\ast])` in the |CLABELS| vector. * Under context :math:`C'`, the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^\ast]`. -* Let :math:`C''` be the same :ref:`context ` as :math:`C`, but with the label :math:`[t^\ast]` prepended to the |CLABELS| vector. - -* Then the compound instruction is valid under context :math:`C''` with type :math:`[] \to [t^\ast]`. +* Then the compound instruction is valid under context :math:`C` with type :math:`[] \to [t^\ast]`. .. math:: \frac{ @@ -685,9 +685,9 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera \qquad (val : t_0)^\ast \qquad - S; C,\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] + S; C,\CLABELS[0]:=(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] }{ - S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] + S; C \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] } From 104d3805c443fd0eb2485c8fca4330ae0fa56b8d Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Sat, 26 Nov 2022 13:10:32 +0100 Subject: [PATCH 7/7] Revert "Reverting changes to typing of CAUGHTadm." This reverts commit 77090e2abfa65e95ad15836ff896a244b1d0e751. --- document/core/appendix/properties.rst | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index cfecf1d4..c2a9c792 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -670,14 +670,14 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera * The :ref:`values ` :math:`\val^\ast` must be of type :math:`[t_0^\ast]`. -* The label type :math:`C.\CLABELS[0]` must be defined in the context. - -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`C.\CLABELS[0]` modified to :math:`(\LCATCH~[t^\ast])` in the |CLABELS| vector. +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector. * Under context :math:`C'`, the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^\ast]`. -* Then the compound instruction is valid under context :math:`C` with type :math:`[] \to [t^\ast]`. +* Let :math:`C''` be the same :ref:`context ` as :math:`C`, but with the label :math:`[t^\ast]` prepended to the |CLABELS| vector. + +* Then the compound instruction is valid under context :math:`C''` with type :math:`[] \to [t^\ast]`. .. math:: \frac{ @@ -685,9 +685,9 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera \qquad (val : t_0)^\ast \qquad - S; C,\CLABELS[0]:=(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] + S; C,\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] }{ - S; C \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] + S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] }