Spectec for binary format of types and instructions

document/core/appendix/index-instructions.py

@@ -359,7 +359,15 @@ def Instruction(version, name, opcode, type=None, validation=None, execution=Non
     Instruction(3.0, r'\REFI31', r'\hex{FB}~\hex{1C}', r'[\I32] \to [(\REF~\I31)]', r'valid-ref.i31', r'exec-ref.i31'),
     Instruction(3.0, r'\I31GETS', r'\hex{FB}~\hex{1D}', r'[\I31REF] \to [\I32]', r'valid-i31.get', r'exec-i31.get'),
     Instruction(3.0, r'\I31GETU', r'\hex{FB}~\hex{1E}', r'[\I31REF] \to [\I32]', r'valid-i31.get', r'exec-i31.get'),
-    Instruction(0.0, None, r'\hex{FB}~\hex{1F} \dots'),
+    Instruction(0.0, None, r'\hex{FB}~\hex{1F}'),
+    Instruction(3.0, r'\STRUCTNEWDESC~x', r'\hex{FB}~\hex{20}', r'[t^\ast~(\REF~\NULL~(\EXACT~y))] \to [(\REF~(\EXACT~x))]', r'valid-struct.new_desc'),
+    Instruction(3.0, r'\STRUCTNEWDEFAULTDESC~x', r'\hex{FB}~\hex{21}', r'[(\REF~\NULL~(\EXACT~y))] \to [(\REF~(\EXACT~x))]', r'valid-struct.new_default_desc'),
+    Instruction(3.0, r'\REFGETDESC~x', r'\hex{FB}~\hex{22}', r'[(\REF~\NULL~\EXACT^?~x)] \to [(\REF~\EXACT^?~y)]', r'valid-ref.get_desc'),
+    Instruction(3.0, r'\REFCASTDESCEQ~(\REF~t)', r'\hex{FB}~\hex{23}', r"[(\REF~t')~(\REF~\NULL~(\EXACT~y))] \to [(\REF~t)]", r'valid-ref.cast_desc_eq'),
+    Instruction(3.0, r'\REFCASTDESCEQ~(\REF~\NULL~t)', r'\hex{FB}~\hex{24}', r"[(\REF~\NULL~t')~(\REF~\NULL~(\EXACT~y))] \to [(\REF~\NULL~t)]", r'valid-ref.cast_desc_eq'),
+    Instruction(3.0, r'\BRONCASTDESCEQ~t_1~t_2', r'\hex{FB}~\hex{25}', r'[t_1~(\REF~\NULL~(\EXACT~y))] \to [t_1\reftypediff t_2]', r'valid-br_on_cast_desc_eq'),
+    Instruction(3.0, r'\BRONCASTDESCEQFAIL~t_1~t_2', r'\hex{FB}~\hex{26}', r'[t_1~(\REF~\NULL~(\EXACT~y))] \to [t_2]', r'valid-br_on_cast_desc_eq_fail'),
+    Instruction(0.0, None, r'\hex{FB}~\hex{27} \dots'),
     Instruction(2.0, r'\I32.\TRUNC\K{\_sat\_}\F32\K{\_s}', r'\hex{FC}~\hex{00}', r'[\F32] \to [\I32]', r'valid-cvtop', r'exec-cvtop', r'op-trunc_sat'),
     Instruction(2.0, r'\I32.\TRUNC\K{\_sat\_}\F32\K{\_u}', r'\hex{FC}~\hex{01}', r'[\F32] \to [\I32]', r'valid-cvtop', r'exec-cvtop', r'op-trunc_sat'),
     Instruction(2.0, r'\I32.\TRUNC\K{\_sat\_}\F64\K{\_s}', r'\hex{FC}~\hex{02}', r'[\F64] \to [\I32]', r'valid-cvtop', r'exec-cvtop', r'op-trunc_sat'),

document/core/appendix/index-types.rst

@@ -32,15 +32,18 @@ Category                                  Constructor
 (reserved)                                                                                       :math:`\hex{68}` .. :math:`\hex{65}`
 :ref:`Reference type <syntax-reftype>`    |REF|                                                  :math:`\hex{64}` (-28 as |Bs7|)
 :ref:`Reference type <syntax-reftype>`    |REF| |NULL|                                           :math:`\hex{63}` (-29 as |Bs7|)
-(reserved)                                                                                       :math:`\hex{62}` .. :math:`\hex{61}`
+:ref:`Heap type <syntax-heaptype>`        :math:`\EXACT~\typeidx`                                :math:`\hex{62}` (-30 as |Bs7|)
+(reserved)                                                                                       :math:`\hex{61}`
 :ref:`Composite type <syntax-comptype>`   :math:`\TFUNC~[\valtype^\ast] \Tarrow[\valtype^\ast]`  :math:`\hex{60}` (-32 as |Bs7|)
 :ref:`Composite type <syntax-comptype>`   :math:`\TSTRUCT~\fieldtype^\ast`                       :math:`\hex{5F}` (-33 as |Bs7|)
 :ref:`Composite type <syntax-comptype>`   :math:`\TARRAY~\fieldtype`                             :math:`\hex{5E}` (-34 as |Bs7|)
 (reserved)                                                                                       :math:`\hex{5D}` .. :math:`\hex{51}`
-:ref:`Sub type <syntax-subtype>`          :math:`\TSUB~\typeidx^\ast~\comptype`                  :math:`\hex{50}` (-48 as |Bs7|)
-:ref:`Sub type <syntax-subtype>`          :math:`\TSUB~\TFINAL~\typeidx^\ast~\comptype`          :math:`\hex{4F}` (-49 as |Bs7|)
+:ref:`Sub type <syntax-subtype>`          :math:`\TSUB~\typeidx^\ast~\desctype`                  :math:`\hex{50}` (-48 as |Bs7|)
+:ref:`Sub type <syntax-subtype>`          :math:`\TSUB~\TFINAL~\typeidx^\ast~\desctype`          :math:`\hex{4F}` (-49 as |Bs7|)
 :ref:`Recursive type <syntax-rectype>`    :math:`\TREC~\subtype^\ast`                            :math:`\hex{4E}` (-50 as |Bs7|)
-(reserved)                                                                                       :math:`\hex{4D}` .. :math:`\hex{41}`
+:ref:`Descriptor type <syntax-desctype>`  :math:`\TDESCRIPTOR~\typeidx`                          :math:`\hex{4D}` (-51 as |Bs7|)
+:ref:`Descriptor type <syntax-desctype>`  :math:`\TDESCRIBES~\typeidx`                           :math:`\hex{4C}` (-52 as |Bs7|)
+(reserved)                                                                                       :math:`\hex{4B}` .. :math:`\hex{41}`
 :ref:`Result type <syntax-resulttype>`    :math:`[\epsilon]`                                     :math:`\hex{40}` (-64 as |Bs7|)
 :ref:`Tag type <syntax-tagtype>`          :math:`\typeuse`                                       (none)
 :ref:`Global type <syntax-globaltype>`    :math:`\mut~\valtype`                                  (none)

document/core/binary/instructions.rst

@@ -58,6 +58,8 @@ Control Instructions
 .. _binary-br_on_non_null:
 .. _binary-br_on_cast:
 .. _binary-br_on_cast_fail:
+.. _binary-br_on_cast_desc_eq:
+.. _binary-br_on_cast_desc_eq_fail:
 .. _binary-return:
 .. _binary-call:
 .. _binary-call_ref:
@@ -158,6 +160,8 @@ Generic :ref:`reference instructions <syntax-instr-ref>` are represented by sing
 .. _binary-ref.as_non_null:
 .. _binary-ref.test:
 .. _binary-ref.cast:
+.. _binary-ref.get_desc:
+.. _binary-ref.cast_desc_eq:
 
 $${grammar: {Binstr/ref}}
 
@@ -176,6 +180,8 @@ Aggregate Instructions
 .. _binary-i31.get_u:
 .. _binary-struct.new:
 .. _binary-struct.new_default:
+.. _binary-struct.new_desc:
+.. _binary-struct.new_default_desc:
 .. _binary-struct.get:
 .. _binary-struct.get_s:
 .. _binary-struct.get_u:

document/core/binary/types.rst

@@ -41,7 +41,7 @@ $${grammar: Bvectype}
 Heap Types
 ~~~~~~~~~~
 
-:ref:`Heap types <syntax-reftype>` are encoded as either a single byte, or as a :ref:`type index <binary-typeidx>` encoded as a positive :ref:`signed integer <binary-sint>`.
+:ref:`Heap types <syntax-heaptype>` are encoded as either a single byte, as the byte ${:0x62} followed by a :ref:`type index <binary-typeidx>`, or as a :ref:`type index <binary-typeidx>` encoded as a positive :ref:`signed integer <binary-sint>`.
 
 $${grammar: Babsheaptype Bheaptype}
 
@@ -118,19 +118,24 @@ Composite Types
 $${grammar: Bmut Bcomptype Bfieldtype Bstoragetype Bpacktype}
 
 
-.. index:: recursive type, sub type, composite type
+.. index:: recursive type, sub type, descriptor type, composite type
    pair: binary format; recursive type
    pair: binary format; sub type
+   pair: binary format; descriptor type
 .. _binary-rectype:
 .. _binary-subtype:
+.. _binary-desctype:
+.. _binary-describes:
+.. _binary-descriptor:
 
 Recursive Types
 ~~~~~~~~~~~~~~~
 
 :ref:`Recursive types <syntax-rectype>` are encoded by the byte ${:0x4E} followed by a :ref:`list <binary-list>` of :ref:`sub types <syntax-subtype>`.
 Additional shorthands are recognized for unary recursions and sub types without super types.
+Each :ref:`composite type <binary-comptype>` may be preceded by a :ref:`describes <syntax-desctype>` clause encoded by the byte ${:0x4C} and a :ref:`type index <binary-typeidx>`, and a :ref:`descriptor <syntax-desctype>` clause encoded by the byte ${:0x4D} and a :ref:`type index <binary-typeidx>`.
 
-$${grammar: Brectype Bsubtype}
+$${grammar: Brectype Bsubtype Bdesctype Bdescribes Bdescriptor}
 
 
 .. index:: limits

document/core/util/macros.def

@@ -844,6 +844,9 @@
 .. |Bstoragetype| mathdef:: \xref{binary/types}{binary-storagetype}{\B{storagetype}}
 .. |Bpacktype| mathdef:: \xref{binary/types}{binary-packtype}{\B{packtype}}
 .. |Bcomptype| mathdef:: \xref{binary/types}{binary-comptype}{\B{comptype}}
+.. |Bdescribes| mathdef:: \xref{binary/types}{binary-describes}{\B{describes}}
+.. |Bdescriptor| mathdef:: \xref{binary/types}{binary-descriptor}{\B{descriptor}}
+.. |Bdesctype| mathdef:: \xref{binary/types}{binary-desctype}{\B{desctype}}
 .. |Bsubtype| mathdef:: \xref{binary/types}{binary-subtype}{\B{subtype}}
 .. |Brectype| mathdef:: \xref{binary/types}{binary-rectype}{\B{rectype}}
 .. |Bglobaltype| mathdef:: \xref{binary/types}{binary-globaltype}{\B{globaltype}}

specification/wasm-latest/5.2-binary.types.spectec

@@ -29,6 +29,7 @@ grammar Babsheaptype : heaptype =
 
 grammar Bheaptype : heaptype =
   | ht:Babsheaptype => ht
+  | 0x62 x:Btypeidx => _HT EXACT (_IDX x)
   | x33:Bs33 => _HT (_IDX $s33_to_u32(x33))  -- if x33 >= 0
 
 grammar Breftype : reftype =
@@ -68,10 +69,19 @@ grammar Bcomptype : comptype =
   | 0x5F ft*:Blist(Bfieldtype) => STRUCT ft*
   | 0x60 t_1*:Bresulttype t_2*:Bresulttype => FUNC t_1* -> t_2*
 
+grammar Bdescribes : describes =
+  | 0x4C x:Btypeidx => DESCRIBES (_IDX x)
+
+grammar Bdescriptor : descriptor =
+  | 0x4D x:Btypeidx => DESCRIPTOR (_IDX x)
+
+grammar Bdesctype : desctype =
+  | (dcs:Bdescribes)? (dcr:Bdescriptor)? ct:Bcomptype => dcs? dcr? ct
+
 grammar Bsubtype : subtype =
-  | 0x4F x*:Blist(Btypeidx) ct:Bcomptype => SUB FINAL (_IDX x)* ct
-  | 0x50 x*:Blist(Btypeidx) ct:Bcomptype => SUB (_IDX x)* ct
-  | ct:Bcomptype => SUB FINAL eps ct
+  | 0x4F x*:Blist(Btypeidx) dct:Bdesctype => SUB FINAL (_IDX x)* dct
+  | 0x50 x*:Blist(Btypeidx) dct:Bdesctype => SUB (_IDX x)* dct
+  | dct:Bdesctype => SUB FINAL eps dct
 
 grammar Brectype : rectype =
   | 0x4E st*:Blist(Bsubtype) => REC st*

specification/wasm-latest/5.3-binary.instructions.spectec

@@ -56,6 +56,10 @@ grammar Binstr/control : instr = ...
     l:Blabelidx ht_1:Bheaptype ht_2:Bheaptype => BR_ON_CAST l (REF null_1? ht_1) (REF null_2? ht_2)
   | 0xFB 25:Bu32 (null_1?, null_2?):Bcastop
     l:Blabelidx ht_1:Bheaptype ht_2:Bheaptype => BR_ON_CAST_FAIL l (REF null_1? ht_1) (REF null_2? ht_2)
+  | 0xFB 37:Bu32 (null_1?, null_2?):Bcastop
+    l:Blabelidx ht_1:Bheaptype ht_2:Bheaptype => BR_ON_CAST_DESC_EQ l (REF null_1? ht_1) (REF null_2? ht_2)
+  | 0xFB 38:Bu32 (null_1?, null_2?):Bcastop
+    l:Blabelidx ht_1:Bheaptype ht_2:Bheaptype => BR_ON_CAST_DESC_EQ_FAIL l (REF null_1? ht_1) (REF null_2? ht_2)
   | ...
 
 grammar Bcatch : catch =
@@ -146,11 +150,16 @@ grammar Binstr/ref : instr = ...
   | 0xFB 21:Bu32 ht:Bheaptype => REF.TEST (REF NULL ht)
   | 0xFB 22:Bu32 ht:Bheaptype => REF.CAST (REF ht)
   | 0xFB 23:Bu32 ht:Bheaptype => REF.CAST (REF NULL ht)
+  | 0xFB 34:Bu32 x:Btypeidx => REF.GET_DESC x
+  | 0xFB 35:Bu32 ht:Bheaptype => REF.CAST_DESC_EQ (REF ht)
+  | 0xFB 36:Bu32 ht:Bheaptype => REF.CAST_DESC_EQ (REF NULL ht)
   | ...
 
 grammar Binstr/struct : instr = ...
   | 0xFB 0:Bu32 x:Btypeidx => STRUCT.NEW x
   | 0xFB 1:Bu32 x:Btypeidx => STRUCT.NEW_DEFAULT x
+  | 0xFB 32:Bu32 x:Btypeidx => STRUCT.NEW_DESC x
+  | 0xFB 33:Bu32 x:Btypeidx => STRUCT.NEW_DEFAULT_DESC x
   | 0xFB 2:Bu32 x:Btypeidx i:Bfieldidx => STRUCT.GET x i
   | 0xFB 3:Bu32 x:Btypeidx i:Bfieldidx => STRUCT.GET S x i
   | 0xFB 4:Bu32 x:Btypeidx i:Bfieldidx => STRUCT.GET U x i