Make exact and non-exact heap types the same case

document/core/syntax/types.rst

@@ -92,6 +92,7 @@ The syntax of type uses is :ref:`extended <syntax-typeuse-ext>` with additional
 .. _syntax-i31:
 .. _syntax-heaptype:
 .. _syntax-absheaptype:
+.. _syntax-exact:
 
 Heap Types
 ~~~~~~~~~~

document/core/util/macros.def

@@ -321,6 +321,7 @@
 
 .. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}}
 .. |null| mathdef:: \xref{syntax/types}{syntax-null}{\X{null}}
+.. |exact| mathdef:: \xref{syntax/types}{syntax-exact}{\X{exact}}
 .. |mut| mathdef:: \xref{syntax/types}{syntax-mut}{\X{mut}}
 .. |final| mathdef:: \xref{syntax/types}{syntax-final}{\X{final}}
 .. |init| mathdef:: \xref{valid/conventions}{syntax-init}{\X{init}}

document/core/valid/types.rst

@@ -58,9 +58,9 @@ $${rule-prose: Heaptype_ok/abs}
 
 $${rule: Heaptype_ok/abs}
 
-$${rule-prose: Heaptype_ok/exact}
+$${rule-prose: Heaptype_ok/typeuse}
 
-$${rule: Heaptype_ok/exact}
+$${rule: Heaptype_ok/typeuse}
 
 
 .. index:: reference type, heap type

specification/wasm-latest/1.2-syntax.types.spectec

@@ -7,6 +7,8 @@
 ;; TODO(3, rossberg): add ability to do this inline
 syntax null hint(show NULL) hint(macro "%" "%") = NULL
 
+syntax exact hint(show EXACT) = EXACT
+
 syntax addrtype hint(desc "address type") =
   | I32 | I64
 
@@ -41,7 +43,7 @@ syntax typevar hint(desc "type variable") =
   | _IDX typeidx | REC n hint(show REC.%)
 
 syntax heaptype hint(desc "heap type") =
-  | absheaptype | typeuse | EXACT typeuse
+  | absheaptype | _HT exact? typeuse hint(show % %)
 
 syntax reftype hint(desc "reference type") =
   | REF null? heaptype
@@ -382,8 +384,8 @@ def $subst_addrtype(at, tv*, tu*) = at
 def $subst_numtype(nt, tv*, tu*) = nt
 def $subst_vectype(vt, tv*, tu*) = vt
 
-def $subst_heaptype(tv', tv*, tu*) = $subst_typevar(tv', tv*, tu*)
-def $subst_heaptype(dt, tv*, tu*) = $subst_deftype(dt, tv*, tu*)
+def $subst_heaptype(_HT exact? tv', tv*, tu*) = _HT exact? $subst_typevar(tv', tv*, tu*)
+def $subst_heaptype(_HT exact? dt, tv*, tu*) = _HT exact? $subst_deftype(dt, tv*, tu*)
 def $subst_heaptype(ht, tv*, tu*) = ht  -- otherwise
 
 def $subst_reftype((REF null? ht), tv*, tu*) = REF null? $subst_heaptype(ht, tv*, tu*)
@@ -550,7 +552,7 @@ def $free_typeuse(typevar) = $free_typevar(typevar)
 def $free_typeuse(deftype) = $free_deftype(deftype)
 
 def $free_heaptype(absheaptype) = $free_absheaptype(absheaptype)
-def $free_heaptype(typeuse) = $free_typeuse(typeuse)
+def $free_heaptype(_HT EXACT? typeuse) = $free_typeuse(typeuse)
 
 def $free_reftype(REF null? heaptype) = $free_heaptype(heaptype)
 

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

@@ -21,11 +21,7 @@ rule Heaptype_ok/abs:
   C |- absheaptype : OK
 
 rule Heaptype_ok/typeuse:
-  C |- typeuse : OK
-  -- Typeuse_ok: C |- typeuse : OK
-
-rule Heaptype_ok/exact:
-  C |- EXACT typeuse : OK
+  C |- _HT EXACT? typeuse : OK
   -- Typeuse_ok: C |- typeuse : OK
 
 rule Reftype_ok:
@@ -167,15 +163,15 @@ def $before(_IDX typeidx, x, i) = typeidx < x
 def $before(REC j, x, i) = j < i
 
 def $unrollht(context, heaptype) : subtype  hint(show $unroll_(%,%))
-def $unrollht(C, deftype) = $unrolldt(deftype)
-def $unrollht(C, _IDX typeidx) = $unrolldt(C.TYPES[typeidx])
-def $unrollht(C, REC i) = C.RECS[i]
+def $unrollht(C, _HT EXACT? deftype) = $unrolldt(deftype)
+def $unrollht(C, _HT EXACT? _IDX typeidx) = $unrolldt(C.TYPES[typeidx])
+def $unrollht(C, _HT EXACT? REC i) = C.RECS[i]
 
 rule Subtype_ok2:
   C |- SUB FINAL? typeuse* desctype : OK x i
   -- if |typeuse*| <= 1
   -- (if $before(typeuse, x, i))*
-  -- (if $unrollht(C, typeuse) = SUB typeuse'* desctype')*
+  -- (if $unrollht(C, _HT typeuse) = SUB typeuse'* desctype')*
   ----
   -- Desctype_ok: C |- desctype : OK
   -- (Desctype_sub: C |- desctype <: desctype')*

specification/wasm-latest/2.2-validation.subtyping.spectec

@@ -21,8 +21,8 @@ rule Heaptype_sub/refl:
   C |- heaptype <: heaptype
 
 rule Heaptype_sub/exact-l:
-  C |- EXACT typeuse <: heaptype
-  -- Heaptype_sub: C |- typeuse <: heaptype
+  C |- _HT EXACT typeuse <: heaptype
+  -- Heaptype_sub: C |- _HT typeuse <: heaptype
 
 rule Heaptype_sub/trans:
   C |- heaptype_1 <: heaptype_2
@@ -43,31 +43,31 @@ rule Heaptype_sub/array-eq:
   C |- ARRAY <: EQ
 
 rule Heaptype_sub/struct:
-  C |- deftype <: STRUCT
+  C |- _HT deftype <: STRUCT
   -- Expand: deftype ~~ STRUCT fieldtype*
 
 rule Heaptype_sub/array:
-  C |- deftype <: ARRAY
+  C |- _HT deftype <: ARRAY
   -- Expand: deftype ~~ ARRAY fieldtype
 
 rule Heaptype_sub/func:
-  C |- deftype <: FUNC
+  C |- _HT deftype <: FUNC
   -- Expand: deftype ~~ FUNC t_1* -> t_2*
 
 rule Heaptype_sub/def:
-  C |- deftype_1 <: deftype_2
+  C |- _HT deftype_1 <: _HT deftype_2
   -- Deftype_sub: C |- deftype_1 <: deftype_2
 
 rule Heaptype_sub/typeidx-l:
-  C |- _IDX typeidx <: heaptype
-  -- Heaptype_sub: C |- C.TYPES[typeidx] <: heaptype
+  C |- _HT _IDX typeidx <: heaptype
+  -- Heaptype_sub: C |- _HT C.TYPES[typeidx] <: heaptype
 
 rule Heaptype_sub/typeidx-r:
-  C |- heaptype <: _IDX typeidx
-  -- Heaptype_sub: C |- heaptype <: C.TYPES[typeidx]
+  C |- heaptype <: _HT _IDX typeidx
+  -- Heaptype_sub: C |- heaptype <: _HT C.TYPES[typeidx]
 
 rule Heaptype_sub/rec:
-  C |- REC i <: typeuse*[j]
+  C |- _HT REC i <: _HT typeuse*[j]
   -- if C.RECS[i] = SUB final? typeuse* desctype
 
 rule Heaptype_sub/none:
@@ -183,8 +183,8 @@ rule Comptype_sub/func:
 ;; TODO: Check descriptor square rules
 rule Desctype_sub:
   C |- (DESCRIBES tu_11) (DESCRIPTOR tu_12) ct_1 <: (DESCRIBES tu_21) (DESCRIPTOR tu_22) ct_2
-  -- Heaptype_sub: C |- tu_11 <: tu_21
-  -- Heaptype_sub: C |- tu_12 <: tu_22
+  -- Heaptype_sub: C |- _HT tu_11 <: _HT tu_21
+  -- Heaptype_sub: C |- _HT tu_12 <: _HT tu_22
   -- Comptype_sub: C |- ct_1 <: ct_2
 
 
@@ -195,7 +195,7 @@ rule Deftype_sub/refl:
 rule Deftype_sub/super:
   C |- deftype_1 <: deftype_2
   -- if $unrolldt(deftype_1) = SUB final? typeuse* desctype
-  -- Heaptype_sub: C |- typeuse*[i] <: deftype_2
+  -- Heaptype_sub: C |- _HT typeuse*[i] <: _HT deftype_2
 
 
 ;; External types

specification/wasm-latest/2.3-validation.instructions.spectec

@@ -123,7 +123,7 @@ rule Instr_ok/call:
   -- Expand: C.FUNCS[x] ~~ FUNC t_1* -> t_2*
 
 rule Instr_ok/call_ref:
-  C |- CALL_REF (_IDX x) : t_1* (REF NULL (_IDX x)) -> t_2*
+  C |- CALL_REF (_IDX x) : t_1* (REF NULL (_HT _IDX x)) -> t_2*
   -- Expand: C.TYPES[x] ~~ FUNC t_1* -> t_2*
 
 rule Instr_ok/call_indirect:
@@ -147,7 +147,7 @@ rule Instr_ok/return_call:
 
 ;; TODO(3, rossberg): enable t_2* <: C.RETURN
 rule Instr_ok/return_call_ref:
-  C |- RETURN_CALL_REF (_IDX x) : t_3* t_1* (REF NULL (_IDX x)) -> t_4*
+  C |- RETURN_CALL_REF (_IDX x) : t_3* t_1* (REF NULL (_HT _IDX x)) -> t_4*
   -- Expand: C.TYPES[x] ~~ FUNC t_1* -> t_2*
   -- if C.RETURN = (t'_2*)
   -- Resulttype_sub: C |- t_2* <: t'_2*
@@ -210,7 +210,7 @@ rule Instr_ok/ref.null:
   -- Heaptype_ok: C |- ht : OK
 
 rule Instr_ok/ref.func:
-  C |- REF.FUNC x : eps -> (REF dt)
+  C |- REF.FUNC x : eps -> (REF (_HT dt))
   -- if C.FUNCS[x] = dt
   -- if x <- C.REFS
 
@@ -250,84 +250,84 @@ rule Instr_ok/i31.get:
 ;; Structure instructions
 
 rule Instr_ok/struct.new:
-  C |- STRUCT.NEW x : $unpack(zt)* -> (REF (_IDX x))
+  C |- STRUCT.NEW x : $unpack(zt)* -> (REF (_HT _IDX x))
   -- Expand: C.TYPES[x] ~~ STRUCT (mut? zt)*
 
 rule Instr_ok/struct.new_default:
-  C |- STRUCT.NEW_DEFAULT x : eps -> (REF (_IDX x))
+  C |- STRUCT.NEW_DEFAULT x : eps -> (REF (_HT _IDX x))
   -- Expand: C.TYPES[x] ~~ STRUCT (mut? zt)*
   -- (Defaultable: |- $unpack(zt) DEFAULTABLE)*
 
 def $is_packtype(storagetype) : bool             hint(show %1 = $unpack(%1)) hint(prose "%1 is a packed type")
 def $is_packtype(zt) = zt =/= $unpack(zt)
 
 rule Instr_ok/struct.get:
-  C |- STRUCT.GET sx? x i : (REF NULL (_IDX x)) -> $unpack(zt)
+  C |- STRUCT.GET sx? x i : (REF NULL (_HT _IDX x)) -> $unpack(zt)
   -- Expand: C.TYPES[x] ~~ STRUCT ft*
   -- if ft*[i] = mut? zt
   -- if sx? =/= eps <=> $is_packtype(zt)
 
 rule Instr_ok/struct.set:
-  C |- STRUCT.SET x i : (REF NULL (_IDX x)) $unpack(zt) -> eps
+  C |- STRUCT.SET x i : (REF NULL (_HT _IDX x)) $unpack(zt) -> eps
   -- Expand: C.TYPES[x] ~~ STRUCT ft*
   -- if ft*[i] = MUT zt
 
 
 ;; Array instructions
 
 rule Instr_ok/array.new:
-  C |- ARRAY.NEW x : $unpack(zt) I32 -> (REF (_IDX x))
+  C |- ARRAY.NEW x : $unpack(zt) I32 -> (REF (_HT _IDX x))
   -- Expand: C.TYPES[x] ~~ ARRAY (mut? zt)
 
 rule Instr_ok/array.new_default:
-  C |- ARRAY.NEW_DEFAULT x : I32 -> (REF (_IDX x))
+  C |- ARRAY.NEW_DEFAULT x : I32 -> (REF (_HT _IDX x))
   -- Expand: C.TYPES[x] ~~ ARRAY (mut? zt)
   -- Defaultable: |- $unpack(zt) DEFAULTABLE
 
 rule Instr_ok/array.new_fixed:
-  C |- ARRAY.NEW_FIXED x n : $unpack(zt)^n -> (REF (_IDX x))
+  C |- ARRAY.NEW_FIXED x n : $unpack(zt)^n -> (REF (_HT _IDX x))
   -- Expand: C.TYPES[x] ~~ ARRAY (mut? zt)
 
 rule Instr_ok/array.new_elem:
-  C |- ARRAY.NEW_ELEM x y : I32 I32 -> (REF (_IDX x))
+  C |- ARRAY.NEW_ELEM x y : I32 I32 -> (REF (_HT _IDX x))
   -- Expand: C.TYPES[x] ~~ ARRAY (mut? rt)
   -- Reftype_sub: C |- C.ELEMS[y] <: rt
 
 rule Instr_ok/array.new_data:
-  C |- ARRAY.NEW_DATA x y : I32 I32 -> (REF (_IDX x))
+  C |- ARRAY.NEW_DATA x y : I32 I32 -> (REF (_HT _IDX x))
   -- Expand: C.TYPES[x] ~~ ARRAY (mut? zt)
   -- if $unpack(zt) = numtype \/ $unpack(zt) = vectype
   -- if C.DATAS[y] = OK
 
 rule Instr_ok/array.get:
-  C |- ARRAY.GET sx? x : (REF NULL (_IDX x)) I32 -> $unpack(zt)
+  C |- ARRAY.GET sx? x : (REF NULL (_HT _IDX x)) I32 -> $unpack(zt)
   -- Expand: C.TYPES[x] ~~ ARRAY (mut? zt)
   -- if sx? = eps <=> $is_packtype(zt)
 
 rule Instr_ok/array.set:
-  C |- ARRAY.SET x : (REF NULL (_IDX x)) I32 $unpack(zt) -> eps
+  C |- ARRAY.SET x : (REF NULL (_HT _IDX x)) I32 $unpack(zt) -> eps
   -- Expand: C.TYPES[x] ~~ ARRAY (MUT zt)
 
 rule Instr_ok/array.len:
   C |- ARRAY.LEN : (REF NULL ARRAY) -> I32
 
 rule Instr_ok/array.fill:
-  C |- ARRAY.FILL x : (REF NULL (_IDX x)) I32 $unpack(zt) I32 -> eps
+  C |- ARRAY.FILL x : (REF NULL (_HT _IDX x)) I32 $unpack(zt) I32 -> eps
   -- Expand: C.TYPES[x] ~~ ARRAY (MUT zt)
 
 rule Instr_ok/array.copy:
-  C |- ARRAY.COPY x_1 x_2 : (REF NULL (_IDX x_1)) I32 (REF NULL (_IDX x_2)) I32 I32 -> eps
+  C |- ARRAY.COPY x_1 x_2 : (REF NULL (_HT _IDX x_1)) I32 (REF NULL (_HT _IDX x_2)) I32 I32 -> eps
   -- Expand: C.TYPES[x_1] ~~ ARRAY (MUT zt_1)
   -- Expand: C.TYPES[x_2] ~~ ARRAY (mut? zt_2)
   -- Storagetype_sub: C |- zt_2 <: zt_1
 
 rule Instr_ok/array.init_elem:
-  C |- ARRAY.INIT_ELEM x y : (REF NULL (_IDX x)) I32 I32 I32 -> eps
+  C |- ARRAY.INIT_ELEM x y : (REF NULL (_HT _IDX x)) I32 I32 I32 -> eps
   -- Expand: C.TYPES[x] ~~ ARRAY (MUT zt)
   -- Storagetype_sub: C |- C.ELEMS[y] <: zt
 
 rule Instr_ok/array.init_data:
-  C |- ARRAY.INIT_DATA x y : (REF NULL (_IDX x)) I32 I32 I32 -> eps
+  C |- ARRAY.INIT_DATA x y : (REF NULL (_HT _IDX x)) I32 I32 I32 -> eps
   -- Expand: C.TYPES[x] ~~ ARRAY (MUT zt)
   -- if $unpack(zt) = numtype \/ $unpack(zt) = vectype
   -- if C.DATAS[y] = OK

specification/wasm-latest/4.1-execution.values.spectec

@@ -40,15 +40,15 @@ rule Ref_ok/i31:
   s |- REF.I31_NUM i : (REF I31)
 
 rule Ref_ok/struct:
-  s |- REF.STRUCT_ADDR a : (REF dt)
+  s |- REF.STRUCT_ADDR a : (REF (_HT dt))
   -- if s.STRUCTS[a].TYPE = dt
 
 rule Ref_ok/array:
-  s |- REF.ARRAY_ADDR a : (REF dt)
+  s |- REF.ARRAY_ADDR a : (REF (_HT dt))
   -- if s.ARRAYS[a].TYPE = dt
 
 rule Ref_ok/func:
-  s |- REF.FUNC_ADDR a : (REF dt)
+  s |- REF.FUNC_ADDR a : (REF (_HT dt))
   -- if s.FUNCS[a].TYPE = dt
 
 rule Ref_ok/exn:

specification/wasm-latest/4.3-execution.instructions.spectec

@@ -203,10 +203,10 @@ rule Step_read/return_call_ref-frame-addr:
 
 
 rule Step_pure/call_indirect:
-  (CALL_INDIRECT x yy)  ~>  (TABLE.GET x) (REF.CAST (REF NULL yy)) (CALL_REF yy)
+  (CALL_INDIRECT x yy)  ~>  (TABLE.GET x) (REF.CAST (REF NULL (_HT yy))) (CALL_REF yy)
 
 rule Step_pure/return_call_indirect:
-  (RETURN_CALL_INDIRECT x yy)  ~>  (TABLE.GET x) (REF.CAST (REF NULL yy)) (RETURN_CALL_REF yy)
+  (RETURN_CALL_INDIRECT x yy)  ~>  (TABLE.GET x) (REF.CAST (REF NULL (_HT yy))) (RETURN_CALL_REF yy)
 
 
 rule Step_pure/frame-vals:
@@ -616,7 +616,7 @@ rule Step/data.drop:
 ;; Reference instructions
 
 rule Step_read/ref.null-idx:
-  z; (REF.NULL (_IDX x))  ~>  (REF.NULL $type(z, x))
+  z; (REF.NULL (_HT _IDX x))  ~>  (REF.NULL (_HT $type(z, x)))
 
 rule Step_read/ref.func:
   z; (REF.FUNC x)  ~>  (REF.FUNC_ADDR $moduleinst(z).FUNCS[x])

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

@@ -29,7 +29,7 @@ grammar Babsheaptype : heaptype =
 
 grammar Bheaptype : heaptype =
   | ht:Babsheaptype => ht
-  | x33:Bs33 => _IDX $s33_to_u32(x33)  -- if x33 >= 0
+  | x33:Bs33 => _HT (_IDX $s33_to_u32(x33))  -- if x33 >= 0
 
 grammar Breftype : reftype =
   | 0x63 ht:Bheaptype => REF NULL ht

specification/wasm-latest/6.2-text.types.spectec

@@ -30,7 +30,7 @@ grammar Tabsheaptype : heaptype =
 
 grammar Theaptype_(I) : heaptype =
   | ht:Tabsheaptype => ht
-  | x:Ttypeidx_(I) => _IDX x
+  | x:Ttypeidx_(I) => _HT (_IDX x)
 
 grammar Tnull : null =
   | "null" => NULL