Fix CI

document/core/exec/instructions.rst

@@ -3599,12 +3599,6 @@ $${rule: {Step_pure/call_indirect}}
 
 $${rule: {Step_read/return_call}}
 
-.. math::
-   \begin{array}{lcl@{\qquad}l}
-   (\RETURNCALL~x) &\stepto& (\RETURNINVOKE~a)
-     & (\iff (\CALL~x) \stepto (\INVOKE~a))
-   \end{array}
-
 
 .. _exec-return_call_ref:
 
@@ -3627,14 +3621,6 @@ $${rule: {Step_read/return_call}}
 
 $${rule: {Step_read/return_call_ref-*}}
 
-.. math::
-   \begin{array}{lcl@{\qquad}l}
-   \val~(\RETURNCALLREF~x) &\stepto& (\RETURNINVOKE~a)
-     & (\iff \val~(\CALLREF~x) \stepto (\INVOKE~a)) \\
-   \val~(\RETURNCALLREF~x) &\stepto& \TRAP
-     & (\iff \val~(\CALLREF~x) \stepto \TRAP) \\
-   \end{array}
-
 
 .. _exec-return_call_indirect:
 
@@ -3683,14 +3669,6 @@ $${rule: {Step_read/return_call_ref-*}}
 
 $${rule: {Step_pure/return_call_indirect}}
 
-.. math::
-   \begin{array}{lcl@{\qquad}l}
-   \val~(\RETURNCALLINDIRECT~x~y) &\stepto& (\RETURNINVOKE~a)
-     & (\iff \val~(\CALLINDIRECT~x~y) \stepto (\INVOKE~a)) \\
-   \val~(\RETURNCALLINDIRECT~x~y) &\stepto& \TRAP
-     & (\iff \val~(\CALLINDIRECT~x~y) \stepto \TRAP) \\
-   \end{array}
-
 
 .. index:: instruction, instruction sequence, block
 .. _exec-instr-seq:

document/core/syntax/types.rst

@@ -71,11 +71,12 @@ Conventions
 $${definition-ignore: vsize}
 
 
-.. index:: ! heap type, store, type index, ! abstract type, ! concrete type, ! unboxed scalar
+.. index:: ! heap type, store, type index, ! type use, ! abstract type, ! concrete type, ! unboxed scalar
    pair: abstract syntax; heap type
 .. _type-abstract:
 .. _type-concrete:
 .. _syntax-i31:
+.. _syntax-typeuse:
 .. _syntax-heaptype:
 
 Heap Types
@@ -91,7 +92,7 @@ There are three disjoint hierarchies of heap types:
 The values from the latter two hierarchies are interconvertible by ways of the ${instr: EXTERN.CONVERT_ANY} and ${instr: ANY.CONVERT_EXTERN} instructions.
 That is, both type hierarchies are inhabited by an isomorphic set of values, but may have different, incompatible representations in practice.
 
-$${syntax: {absheaptype/syn heaptype/syn}}
+$${syntax: {absheaptype/syn heaptype typeuse/syn}}
 
 A heap type is either *abstract* or *concrete*.
 
@@ -125,9 +126,10 @@ Their observable value range is limited to 31 bits.
    they can be used to form the types of all null :ref:`references <syntax-reftype>` in their respective hierarchy.
    For example, ${:(REF NULL NOFUNC)} is the generic type of a null reference compatible with all function reference types.
 
-A concrete heap type consists of a :ref:`type index <syntax-typeidx>` and classifies an object of the respective :ref:`type <syntax-type>` defined in a module.
+A concrete heap type consists of a *type use*, which is a :ref:`type index <syntax-typeidx>`.
+It classifies an object of the respective :ref:`type <syntax-type>` defined in a module.
 
-The syntax of heap types is :ref:`extended <syntax-heaptype-ext>` with additional forms for the purpose of specifying :ref:`validation <valid>` and :ref:`execution <exec>`.
+The syntax of abstract heap types and type uses is :ref:`extended <syntax-heaptype-ext>` with additional forms for the purpose of specifying :ref:`validation <valid>` and :ref:`execution <exec>`.
 
 
 .. index:: ! reference type, heap type, reference, table, function, function type, null

spectec/spec/wasm-3.0/5-runtime-aux.watsup

@@ -76,7 +76,7 @@ def $store((s; f)) = s
 def $frame((s; f)) = f
 
 
-def $funcaddr(state) : funcaddr*      hint(show %.MODULE.FUNC)
+def $funcaddr(state) : funcaddr*      hint(show %.MODULE.FUNCS)
 def $funcaddr((s; f)) = f.MODULE.FUNCS
 
 def $funcinst(state) : funcinst*      hint(show %.FUNCS)

spectec/spec/wasm-3.0/8-reduction.watsup

@@ -185,6 +185,7 @@ rule Step_read/return_call_ref-frame-null:
 
 rule Step_read/return_call_ref-frame-addr:
   z; (FRAME_ k `{f} val'* val^n (REF.FUNC_ADDR a) (RETURN_CALL_REF yy) instr*)  ~>  val^n (REF.FUNC_ADDR a) (CALL_REF yy)
+
   -- Expand: $funcinst(z)[a].TYPE ~~ FUNC (t_1^n -> t_2^m)
 
 

spectec/src/backend-latex/render.ml

@@ -834,7 +834,7 @@ and render_conditions env rhs tabs prems =
     | Nl::prems'' ->
       "\\multicolumn{2}{l@{}}{ " ^ rhs ^ " } \\\\\n  " ^ tabs,
       prems'', tabs, " \\multicolumn{2}{l@{}}{\\quad ", "}"
-    | _ -> rhs ^  "\n  &", prems', tabs ^ "&", "\\quad ", ""
+    | _ -> rhs ^  "\n  &", prems', tabs ^ "&", "\\qquad ", ""
   in
   let prems''', first =
     match prems'' with