Skip to content

Commit f500d7f

Browse files
rossbergrossberg
committed
[spec] Port Soundness Appendix to SpecTec, pt. 1 (rules for types)
1 parent 92d7e86 commit f500d7f

4 files changed

Lines changed: 32 additions & 154 deletions

File tree

‎document/core/appendix/properties.rst‎

Lines changed: 22 additions & 138 deletions
Original file line numberDiff line numberDiff line change
@@ -40,164 +40,56 @@ Types
4040

4141
Well-formedness for :ref:`extended type forms <type-ext>` is defined as follows.
4242

43+
.. _valid-typeuse-ext:
4344

44-
.. _valid-heaptype-ext:
45+
$${rule-prose: Typeuse_ok/rec}
4546

46-
:ref:`Heap Type <syntax-heaptype-ext>` :math:`\BOTH`
47-
....................................................
47+
$${rule: Typeuse_ok/rec}
4848

49-
* The heap type is valid.
5049

51-
.. math::
52-
\frac{
53-
}{
54-
C \vdashheaptype \BOTH : \OKheaptype
55-
}
50+
.. _valid-heaptype-ext:
5651

57-
:ref:`Heap Type <syntax-heaptype-ext>` :math:`\REC~i`
58-
.....................................................
52+
$${rule-prose: Heaptype_ok/bot}
5953

60-
* The recursive type index :math:`i` must exist in :math:`C.\CRECS`.
61-
62-
* Then the heap type is valid.
63-
64-
.. math::
65-
\frac{
66-
C.\CRECS[i] = \subtype
67-
}{
68-
C \vdashheaptype \REC~i : \OKheaptype
69-
}
54+
$${rule: Heaptype_ok/bot}
7055

7156

7257
.. _valid-valtype-ext:
7358

74-
:ref:`Value Type <syntax-valtype-ext>` :math:`\BOT`
75-
...................................................
76-
77-
* The value type is valid.
59+
$${rule-prose: Valtype_ok/bot}
7860

79-
.. math::
80-
\frac{
81-
}{
82-
C \vdashvaltype \BOT : \OKvaltype
83-
}
61+
$${rule: Valtype_ok/bot}
8462

8563

8664
.. _valid-rectype-ext:
8765

88-
:ref:`Recursive Types <syntax-rectype>` :math:`\TREC~\subtype^\ast`
89-
...................................................................
66+
$${rule-prose: Rectype_ok2}
9067

91-
* Let :math:`C'` be the current :ref:`context <context>` :math:`C`, but where |CRECS| is :math:`\subtype^\ast`.
92-
93-
* There must be a :ref:`type index <syntax-typeidx>` :math:`x`, such that for each :ref:`sub type <syntax-subtype>` :math:`\subtype_i` in :math:`\subtype^\ast`:
94-
95-
* Under the context :math:`C'`, the :ref:`sub type <syntax-subtype>` :math:`\subtype_i` must be :ref:`valid <valid-subtype>` for :ref:`type index <syntax-typeidx>` :math:`x+i` and :ref:`recursive type index <syntax-rectypeidx>` :math:`i`.
96-
97-
* Then the recursive type is valid for the :ref:`type index <syntax-typeidx>` :math:`x`.
98-
99-
.. math::
100-
\frac{
101-
C,\CRECS~\subtype^\ast \vdashrectype \TREC~\subtype^\ast : {\OKrectype}(x,0)
102-
}{
103-
C \vdashrectype \TREC~\subtype^\ast : {\OKrectype}(x)
104-
}
105-
106-
.. math::
107-
\frac{
108-
}{
109-
C \vdashrectype \TREC~\epsilon : {\OKrectype}(x,i)
110-
}
111-
\qquad
112-
\frac{
113-
C \vdashsubtype \subtype : {\OKsubtype}(x,i)
114-
\qquad
115-
C \vdashrectype \TREC~{\subtype'}^\ast : {\OKrectype}(x+1,i+1)
116-
}{
117-
C \vdashrectype \TREC~\subtype~{\subtype'}^\ast : {\OKrectype}(x,i)
118-
}
119-
120-
.. note::
121-
These rules are a generalisation of the ones :ref:`previously given <valid-rectype>`.
68+
$${rule: {Rectype_ok2/empty Rectype_ok2/cons}}
12269

12370

12471
.. _valid-subtype-ext:
12572

126-
:ref:`Sub types <syntax-subtype>` :math:`\TSUB~\TFINAL^?~\X{ht}^\ast~\comptype`
127-
...............................................................................
73+
$${rule-prose: Subtype_ok2}
12874

129-
* The :ref:`composite type <syntax-comptype>` :math:`\comptype` must be :ref:`valid <valid-comptype>`.
75+
$${rule: Subtype_ok2}
13076

131-
* The sequence :math:`\X{ht}^\ast` may be no longer than :math:`1`.
132-
133-
* For every :ref:`heap type <syntax-heaptype>` :math:`\X{ht}_k` in :math:`\X{ht}^\ast`:
134-
135-
* The :ref:`heap type <syntax-heaptype>` :math:`\X{ht}_k` must be ordered before a :ref:`type index <syntax-typeidx>` :math:`x` and :ref:`recursive type index <syntax-rectypeidx>` a :math:`i`, meaning:
136-
137-
- Either :math:`\X{ht}_k` is a :ref:`defined type <syntax-deftype>`.
138-
139-
- Or :math:`\X{ht}_k` is a :ref:`type index <syntax-typeidx>` :math:`y_k` that is smaller than :math:`x`.
140-
141-
- Or :math:`\X{ht}_k` is a :ref:`recursive type index <syntax-rectypeidx>` :math:`\REC~j_k` where :math:`j_k` is smaller than :math:`i`.
142-
143-
* Let :ref:`sub type <syntax-subtype>` :math:`\subtype_k` be the :ref:`unrolling <aux-unroll-heaptype>` of the :ref:`heap type <syntax-heaptype>` :math:`\X{ht}_k`, meaning:
144-
145-
- Either :math:`\X{ht}_k` is a :ref:`defined type <syntax-deftype>` :math:`\deftype_k`, then :math:`\subtype_k` must be the :ref:`unrolling <aux-unroll-deftype>` of :math:`\deftype_k`.
146-
147-
- Or :math:`\X{ht}_k` is a :ref:`type index <syntax-typeidx>` :math:`y_k`, then :math:`\subtype_k` must be the :ref:`unrolling <aux-unroll-deftype>` of the :ref:`defined type <syntax-deftype>` :math:`C.\CTYPES[y_k]`.
148-
149-
- Or :math:`\X{ht}_k` is a :ref:`recursive type index <syntax-rectypeidx>` :math:`\REC~j_k`, then :math:`\subtype_k` must be :math:`C.\CRECS[j_k]`.
150-
151-
* The :ref:`sub type <syntax-subtype>` :math:`\subtype_k` must not contain :math:`\TFINAL`.
152-
153-
* Let :math:`\comptype'_k` be the :ref:`composite type <syntax-comptype>` in :math:`\subtype_k`.
154-
155-
* The :ref:`composite type <syntax-comptype>` :math:`\comptype` must :ref:`match <match-comptype>` :math:`\comptype'_k`.
156-
157-
* Then the sub type is valid for the :ref:`type index <syntax-typeidx>` :math:`x` and :ref:`recursive type index <syntax-rectypeidx>` :math:`i`.
158-
159-
.. math::
160-
\frac{
161-
\begin{array}{@{}c@{}}
162-
|\X{ht}^\ast| \leq 1
163-
\qquad
164-
(\X{ht} \prec x,i)^\ast
165-
\qquad
166-
(\unrollht_{C}(\X{ht}) = \TSUB~{\X{ht}'}^\ast~\comptype')^\ast
167-
\\
168-
C \vdashcomptype \comptype : \OKcomptype
169-
\qquad
170-
(C \vdashcomptypematch \comptype \subcomptypematch \comptype')^\ast
171-
\end{array}
172-
}{
173-
C \vdashsubtype \TSUB~\TFINAL^?~\X{ht}^\ast~\comptype : {\OKsubtype}(x,i)
174-
}
77+
where:
17578

17679
.. _aux-unroll-heaptype:
17780

178-
where:
179-
180-
.. math::
181-
\begin{array}{@{}lll@{}}
182-
(\deftype \prec x,i) &=& {\F{true}} \\
183-
(y \prec x,i) &=& y < x \\
184-
(\REC~j \prec x,i) &=& j < i \\
185-
[2ex]
186-
\unrollht_{C}(\deftype) &=& \unrolldt(\deftype) \\
187-
\unrollht_{C}(y) &=& \unrolldt(C.\CTYPES[y]) \\
188-
\unrollht_{C}(\REC~j) &=& C.\CRECS[j] \\
189-
\end{array}
81+
$${definition: unrollht_ before}
19082

19183
.. note::
192-
This rule is a generalisation of the ones :ref:`previously given <valid-subtype>`, which only allowed type indices as supertypes.
84+
The new rules for :ref:`recursive types <syntax-rectype>` and :ref:`sub types <syntax-subtype>` complement the ones :ref:`previously given <valid-subtype>`,
85+
which only allowed regular :ref:`type indices <syntax-typeidx>` as supertypes.
86+
They define validity of :ref:`rolled-up <aux-roll-rectype>` recursive types,
87+
like they occur in :ref:`defined types <syntax-deftype>`.
19388

19489

19590
.. index:: defined type, recursive type, unroll, expand
19691
.. _valid-deftype:
19792

198-
:ref:`Defined types <syntax-deftype>` :math:`\rectype.i`
199-
........................................................
200-
20193
$${rule-prose: Deftype_ok}
20294

20395
$${rule: Deftype_ok}
@@ -209,21 +101,13 @@ $${rule: Deftype_ok}
209101
Subtyping
210102
~~~~~~~~~
211103

212-
In a :ref:`rolled-up <aux-roll-rectype>` :ref:`recursive type <syntax-rectype>`, a :ref:`recursive type indices <syntax-rectypeidx>` :math:`\REC~i` :ref:`matches <match-heaptype>` another :ref:`heap type <syntax-heaptype>` :math:`\X{ht}` if:
213-
214-
* Let :math:`\TSUB~\TFINAL^?~{\X{ht}'}^\ast~\comptype` be the :ref:`sub type <syntax-subtype>` :math:`C.\CRECS[i]`.
215-
216-
* The heap type :math:`\X{ht}` is contained in :math:`{\X{ht}'}^\ast`.
104+
Inside a :ref:`rolled-up <aux-roll-rectype>` :ref:`recursive type <syntax-rectype>`, a :ref:`recursive type index <syntax-rectypeidx>` can :ref:`match <match-heaptype>` another :ref:`heap type <syntax-heaptype>`.
217105

218-
.. math::
219-
\frac{
220-
C.\CRECS[i] = \TSUB~\TFINAL^?~(\X{ht}_1^\ast~\X{ht}~\X{ht}_2^\ast)~\comptype
221-
}{
222-
C \vdashheaptypematch \REC~i \subheaptypematch \X{ht}
223-
}
106+
$${rule: Heaptype_sub/rec}
224107

225108
.. note::
226-
This rule is only invoked when checking :ref:`validity <valid-rectype-ext>` of :ref:`rolled-up <aux-roll-rectype>` :ref:`recursive types <syntax-rectype>`.
109+
This rule complements the previously given rules for :ref:`matching heap types <match-heaptype>`.
110+
It is only invoked when checking :ref:`validity <valid-rectype-ext>` of :ref:`rolled-up <aux-roll-rectype>` :ref:`recursive types <syntax-rectype>`.
227111

228112

229113
.. index:: value, value type, result, result type, trap, exception, throw

‎document/core/valid/matching.rst‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -39,11 +39,10 @@ Heap Types
3939
$${rule-prose: Heaptype_sub}
4040

4141
$${rule:
42-
{Heaptype_sub/refl Heaptype_sub/trans}
42+
{Heaptype_sub/refl} {Heaptype_sub/trans}
4343
{Heaptype_sub/eq-any Heaptype_sub/i31-eq Heaptype_sub/struct-eq Heaptype_sub/array-eq}
4444
{Heaptype_sub/struct Heaptype_sub/array Heaptype_sub/func}
4545
{Heaptype_sub/typeidx-l Heaptype_sub/typeidx-r}
46-
{Heaptype_sub/rec}
4746
{Heaptype_sub/none Heaptype_sub/nofunc} {Heaptype_sub/noexn Heaptype_sub/noextern}
4847
{Heaptype_sub/bot}
4948
}

‎document/core/valid/types.rst‎

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -196,17 +196,11 @@ Recursive Types
196196

197197
:ref:`Recursive types <syntax-rectype>` are validated with respect to the first :ref:`type index <syntax-typeidx>` defined by the recursive group.
198198

199-
:math:`\TREC~\subtype^\ast`
200-
...........................
201-
202199
$${rule-prose: Rectype_ok}
203200

204201
$${rule: {Rectype_ok/empty Rectype_ok/cons}}
205202

206203

207-
:math:`\TSUB~\TFINAL^?~y^\ast~\comptype`
208-
........................................
209-
210204
$${rule-prose: Subtype_ok}
211205

212206
$${rule: Subtype_ok}

‎specification/wasm-latest/2.1-validation.types.spectec‎

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -84,9 +84,9 @@ rule Expand_use/typeidx: _IDX typeidx ~~_C comptype -- Expand: C.TYPES[typeidx]
8484
;; Type definitions
8585

8686
syntax oktypeidx hint(show OK#((typeidx))) hint(prose_desc "type index") =
87-
| OK typeidx hint(show OK#(%)) hint(macro "%subtype") hint(prose "%1")
87+
| OK typeidx hint(show OK#(%)) hint(macro "%subtype") hint(prose "%1")
8888
syntax oktypenat hint(show OK#(n)) =
89-
| OK nat hint(show OK#(%)) hint(macro "%subtypeext")
89+
| OK nat hint(show OK#(%)) hint(macro "%subtypeext") hint(prose "%1")
9090

9191
relation Packtype_ok: context |- packtype : OK hint(name "K-pack") hint(macro "%packtype")
9292
relation Fieldtype_ok: context |- fieldtype : OK hint(name "K-field") hint(macro "%fieldtype")
@@ -155,21 +155,22 @@ rule Subtype_ok:
155155
-- Comptype_ok: C |- comptype : OK
156156
-- (Comptype_sub: C |- comptype <: comptype')*
157157

158-
def $before(typeuse, nat) : bool hint(show % << %) hint(macro "before")
158+
def $before(typeuse, nat) : bool hint(show % << %) hint(macro none)
159159
def $before(REC j, i) = j < i
160160
def $before(typeuse, i) = true -- otherwise
161161

162-
def $unrollht(context, heaptype) : subtype hint(show $unroll_(%,%))
163-
def $unrollht(C, deftype) = $unrolldt(deftype)
164-
def $unrollht(C, _IDX typeidx) = $unrolldt(C.TYPES[typeidx])
165-
def $unrollht(C, REC i) = C.RECS[i]
162+
def $unrollht_(context, heaptype) : subtype
163+
def $unrollht_(C, deftype) = $unrolldt(deftype)
164+
def $unrollht_(C, _IDX typeidx) = $unrolldt(C.TYPES[typeidx])
165+
def $unrollht_(C, REC i) = C.RECS[i]
166166

167167
rule Subtype_ok2:
168168
C |- SUB FINAL? typeuse* comptype : OK(i)
169169
-- if |typeuse*| <= 1
170170
-- (Typeuse_ok: C |- typeuse : OK)*
171171
-- (if $before(typeuse, i))*
172-
-- (if $unrollht(C, typeuse) = SUB typeuse'* comptype')*
172+
----
173+
-- (if $unrollht_(C, typeuse) = SUB typeuse'* comptype')*
173174
----
174175
-- Comptype_ok: C |- comptype : OK
175176
-- (Comptype_sub: C |- comptype <: comptype')*

0 commit comments

Comments
 (0)