Skip to content
This repository was archived by the owner on Apr 25, 2025. It is now read-only.

Add prose for typing rule of CAUGHTadm #229

Merged
merged 1 commit into from
Sep 12, 2022
Merged

Add prose for typing rule of CAUGHTadm #229

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 15 additions & 4 deletions document/core/appendix/properties.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -646,14 +646,25 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
:math:`\CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END`
.........................................................

.. todo::
Add prose.
* The :ref:`external tag value <syntax-externval>` :math:`\EVTAG~\tagaddr` must be :ref:`valid <valid-externval-tag>` with some :ref:`external tag type <syntax-externtype>` :math:`\ETTAG~[t_0^\ast] \to []`.

* The :ref:`values <syntax-val>` :math:`\val^\ast` must be of type :math:`[t_0^\ast]`.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this isn't defined as written, and requires a loop over the individual values.


* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems wrong. Note that the typing rule requires that there already is a labeltype t* at the front of the labels (which you need to check!), and this is just adjusting it.


* Under context :math:`C'`,
the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[] \to [t^\ast]`.

* Let :math:`C''` be the same :ref:`context <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]`.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I see, what you are trying. But the context C is an input, you cannot construct another one here. If there are constraints on it, those have to be checked.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@rossberg, looking for past review comments I had forgotten I found this, which was the reason for the (still misplaced) change you found in PR#241. How should this prose and rule look like after all?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The prose needs to first check the topmost entry of its input context C, and then construct C' from it by updating that, and check the body under that C'.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@rossberg, I made PR #244 to match your description, but I'm not entirely sure about the notation I used.



.. math::
\frac{
S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t'^\ast]\to[]
S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t_0^\ast]\to[]
\qquad
(val : t')^\ast
(val : t_0)^\ast
\qquad
S; C,\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast]
}{
Expand Down