Fix Wasm-1.0/2.0 spec

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

@@ -5,6 +5,7 @@
 relation Step: config ~> config                 hint(show "E")
 relation Step_pure: admininstr* ~> admininstr*  hint(show "E")
 relation Step_read: config ~> admininstr*       hint(show "E")
+relation Steps: config ~>* config               hint(show "E")
 
 rule Step/pure:
   z; instr*  ~>  z; instr'*
@@ -14,6 +15,23 @@ rule Step/read:
   z; instr*  ~>  z; instr'*
   -- Step_read: z; instr* ~> instr'*
 
+rule Steps/refl:
+  z; admininstr* ~>* z; admininstr*
+
+rule Steps/trans:
+  z; admininstr*  ~>*  z''; admininstr''*
+  -- Step: z; admininstr*  ~>  z'; admininstr'*
+  -- Steps: z'; admininstr'  ~>*  z''; admininstr''*
+
+
+;; Expressions
+
+relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr")
+
+rule Eval_expr:
+  z; instr*  ~>*  z'; val*
+  -- Steps: z; instr*  ~>*  z'; val*
+
 
 ;;
 ;; Instructions

spectec/spec/wasm-1.0/9-module.watsup

@@ -125,31 +125,32 @@ def $allocmodule(s, module, externval*, val*) = (s_4, mm)
 ;; Instantiation
 ;;
 
-def $concat_instr(instr**) : instr*
+def $concat_instr((instr*)*) : instr*
 def $concat_instr(epsilon) = epsilon
-def $concat_instr(instr* instr'**) = instr* $concat_instr(instr'**)
+def $concat_instr((instr*) (instr'*)*) = instr* $concat_instr((instr'*)*)
 
 def $initelem(store, tableaddr, u32*, (funcaddr*)*) : store
 def $initelem(s, ta, epsilon, epsilon) = s
-def $initelem(s, ta, i i'*, a* (a'*)*) = s[.TABLE[ta].ELEM[i:|a*|] = a*]
+def $initelem(s, ta, i i'*, (a*) (a'*)*) = s[.TABLE[ta].ELEM[i:|a*|] = a*]
 
 def $initdata(store, memaddr, u32*, (byte*)*) : store
 def $initdata(s, ma, epsilon, epsilon) = s
-def $initdata(s, ma, i i'*, b* (b'*)*) = s[.MEM[ma].DATA[i:|b*|] = b*]
+def $initdata(s, ma, i i'*, (b*) (b'*)*) = s[.MEM[ma].DATA[i:|b*|] = b*]
 
 def $instantiate(store, module, externval*) : config
 def $instantiate(s, module, externval*) = s'; f; (CALL x')?
   -- if module = MODULE type* import* func* global* table* mem* elem* data* start? export*
   -- if type* = (TYPE functype)*
-  -- if global* = (GLOBAL globaltype instr_G*)*  ;; TODO: expr_G
-  -- if elem* = (ELEM instr_E* x*)*              ;; TODO: expr_E
-  -- if data* = (DATA instr_D* b*)*              ;; TODO: expr_D
+  -- if global* = (GLOBAL globaltype expr_G)*
+  -- if elem* = (ELEM expr_E x*)*
+  -- if data* = (DATA expr_D b*)*
   -- if start? = (START x')?
   -- if mm_init = {TYPE functype*, FUNC $funcs(externval*), GLOBAL $globals(externval*)}
   -- if f_init = { LOCAL epsilon, MODULE mm_init }
-  -- (Step_read : s; f_init; instr_G* ~> val)*
-  -- (Step_read : s; f_init; instr_E* ~> (CONST I32 i_E))*
-  -- (Step_read : s; f_init; instr_D* ~> (CONST I32 i_D))*
+  -- if z = s; f_init
+  -- (Eval_expr : z; expr_G ~>* z; val)*
+  -- (Eval_expr : z; expr_E ~>* z; (CONST I32 i_E))*
+  -- (Eval_expr : z; expr_D ~>* z; (CONST I32 i_D))*
   -- if (s', mm) = $allocmodule(s, module, externval*, val*)
   -- if s'' = $initelem(s', mm.TABLE[0], i_E*, mm.FUNC[x]**)
   -- if s''' = $initdata(s'', mm.MEM[0], i_D*, b**)

spectec/spec/wasm-1.0/A-binary.watsup

@@ -43,9 +43,9 @@ grammar Bf64 : f64 = | p:Bf(64) => p
 
 ;; Names
 
-def $concat_bytes(byte**) : byte*  hint(show $concat(%))
+def $concat_bytes((byte*)*) : byte*  hint(show $concat(%))
 def $concat_bytes(epsilon) = epsilon
-def $concat_bytes(b* b'**) = b* $concat_bytes(b'**)
+def $concat_bytes((b*) (b'*)*) = b* $concat_bytes((b'*)*)
 
 def $utf8(name) : byte*
 def $utf8(c) = b  -- if c < U+0080 /\ c = b
@@ -496,9 +496,9 @@ grammar Belem : elem =
 
 ;; Code section
 
-def $concat_locals(local**) : local*  hint(show $concat(%))
+def $concat_locals((local*)*) : local*  hint(show $concat(%))
 def $concat_locals(epsilon) = epsilon
-def $concat_locals(loc* loc'**) = loc* $concat_locals(loc'**)
+def $concat_locals((loc*) (loc'*)*) = loc* $concat_locals((loc'*)*)
 
 
 syntax code = (local*, expr)

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

@@ -5,6 +5,7 @@
 relation Step: config ~> config                 hint(show "E")
 relation Step_pure: admininstr* ~> admininstr*  hint(show "E")
 relation Step_read: config ~> admininstr*       hint(show "E")
+relation Steps: config ~>* config               hint(show "E")
 
 rule Step/pure:
   z; instr*  ~>  z; instr'*
@@ -14,6 +15,23 @@ rule Step/read:
   z; instr*  ~>  z; instr'*
   -- Step_read: z; instr* ~> instr'*
 
+rule Steps/refl:
+  z; admininstr* ~>* z; admininstr*
+
+rule Steps/trans:
+  z; admininstr*  ~>*  z''; admininstr''*
+  -- Step: z; admininstr*  ~>  z'; admininstr'*
+  -- Steps: z'; admininstr'  ~>*  z''; admininstr''*
+
+
+;; Expressions
+
+relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr")
+
+rule Eval_expr:
+  z; instr*  ~>*  z'; val*
+  -- Steps: z; instr*  ~>*  z'; val*
+
 
 ;;
 ;; Instructions

spectec/spec/wasm-2.0/9-module.watsup

@@ -90,7 +90,7 @@ def $allocdata(s, byte*) = (s[.DATA =.. di], |s.DATA|)
 
 def $allocdatas(store, (byte*)*) : (store, dataaddr*)
 def $allocdatas(s, epsilon) = (s, epsilon)
-def $allocdatas(s, byte* byte'**) = (s_2, da da'*)
+def $allocdatas(s, (byte*) (byte'*)*) = (s_2, da da'*)
   -- if (s_1, da) = $allocdata(s, byte*)
   -- if (s_2, da'*) = $allocdatas(s_1, (byte'*)*)
 
@@ -151,9 +151,9 @@ def $allocmodule(s, module, externval*, val*, (ref*)*) = (s_6, mm)
 ;; Instantiation
 ;;
 
-def $concat_instr(instr**) : instr*
+def $concat_instr((instr*)*) : instr*
 def $concat_instr(epsilon) = epsilon
-def $concat_instr(instr* instr'**) = instr* $concat_instr(instr'**)
+def $concat_instr((instr*) (instr'*)*) = instr* $concat_instr((instr'*)*)
 
 def $runelem(elem, idx) : instr*
 def $runelem(ELEM reftype expr* (PASSIVE), i) = epsilon
@@ -172,15 +172,16 @@ def $instantiate(store, module, externval*) : config
 def $instantiate(s, module, externval*) = s'; f; instr_E* instr_D* (CALL x)?
   -- if module = MODULE type* import* func* global* table* mem* elem* data* start? export*
   -- if type* = (TYPE functype)*
-  -- if global* = (GLOBAL globaltype instr_G*)*    ;; TODO: expr_G
-  -- if elem* = (ELEM reftype instr_E** elemmode)* ;; TODO: expr_E*
+  -- if global* = (GLOBAL globaltype expr_G)*
+  -- if elem* = (ELEM reftype expr_E* elemmode)*
   -- if start? = (START x)?
   -- if n_E = |elem*|
   -- if n_D = |data*|
   -- if mm_init = {TYPE functype*, FUNC $funcs(externval*), GLOBAL $globals(externval*)}
   -- if f_init = { LOCAL epsilon, MODULE mm_init }
-  -- (Step_read : s; f_init; instr_G* ~> val)*
-  -- (Step_read : s; f_init; instr_E* ~> ref)**
+  -- if z = s; f_init
+  -- (Eval_expr : z; expr_G ~>* z; val)*
+  -- (Eval_expr : z; expr_E ~>* z; ref)**
   -- if (s', mm) = $allocmodule(s, module, externval*, val*, (ref*)*)
   -- if f = { LOCAL epsilon, MODULE mm }
   -- if instr_E* = $concat_instr($runelem(elem*[i], i)^(i<n_E))

spectec/spec/wasm-2.0/A-binary.watsup

@@ -44,9 +44,9 @@ grammar Bf64 : f64 = | p:Bf(64) => p
 
 ;; Names
 
-def $concat_bytes(byte**) : byte*  hint(show $concat(%))
+def $concat_bytes((byte*)*) : byte*  hint(show $concat(%))
 def $concat_bytes(epsilon) = epsilon
-def $concat_bytes(b* b'**) = b* $concat_bytes(b'**)
+def $concat_bytes((b*) (b'*)*) = b* $concat_bytes((b'*)*)
 
 def $utf8(name) : byte*
 def $utf8(c) = b  -- if c < U+0080 /\ c = b
@@ -576,7 +576,7 @@ grammar Belemkind : reftype hint(desc "element kind") =
 
 def $concat_locals(local**) : local*  hint(show $concat(%))
 def $concat_locals(epsilon) = epsilon
-def $concat_locals(loc* loc'**) = loc* $concat_locals(loc'**)
+def $concat_locals((loc*) (loc'*)*) = loc* $concat_locals((loc'*)*)
 
 
 syntax code = (local*, expr)

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

@@ -5,6 +5,7 @@
 relation Step: config ~> config                 hint(show "E")
 relation Step_pure: admininstr* ~> admininstr*  hint(show "E")
 relation Step_read: config ~> admininstr*       hint(show "E")
+relation Steps: config ~>* config               hint(show "E")
 
 rule Step/pure:
   z; instr*  ~>  z; instr'*
@@ -14,23 +15,22 @@ rule Step/read:
   z; instr*  ~>  z; instr'*
   -- Step_read: z; instr* ~> instr'*
 
+rule Steps/refl:
+  z; admininstr* ~>* z; admininstr*
 
-;; Expressions
+rule Steps/trans:
+  z; admininstr*  ~>*  z''; admininstr''*
+  -- Step: z; admininstr*  ~>  z'; admininstr'*
+  -- Steps: z'; admininstr'  ~>*  z''; admininstr''*
 
-relation Eval: config ~>* state; val*  hint(show "E-expr")
-relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr")
 
-rule Eval/done:
-  z; val* ~>* z; val*
+;; Expressions
 
-rule Eval/step:
-  z; admininstr*  ~>*  z''; val*
-  -- Step: z; admininstr*  ~>  z'; admininstr'*
-  -- Eval: z'; admininstr'  ~>*  z''; val*
+relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr")
 
 rule Eval_expr:
   z; instr*  ~>*  z'; val*
-  -- Eval: z; instr*  ~>*  z; val*
+  -- Steps: z; instr*  ~>*  z'; val*
 
 
 ;;

spectec/test-frontend/TEST.md

@@ -3581,12 +3581,12 @@ relation Step_read: `%~>%*`(config, admininstr*)
 
 ;; 8-reduction.watsup:5.1-5.63
 relation Step: `%~>%`(config, config)
-  ;; 8-reduction.watsup:9.1-11.34
+  ;; 8-reduction.watsup:10.1-12.34
   rule pure {instr* : instr*, instr'* : instr*, z : state}:
     `%~>%`(`%;%*`(z, (instr <: admininstr)*{instr}), `%;%*`(z, (instr' <: admininstr)*{instr'}))
     -- Step_pure: `%*~>%*`((instr <: admininstr)*{instr}, (instr' <: admininstr)*{instr'})
 
-  ;; 8-reduction.watsup:13.1-15.37
+  ;; 8-reduction.watsup:14.1-16.37
   rule read {instr* : instr*, instr'* : instr*, z : state}:
     `%~>%`(`%;%*`(z, (instr <: admininstr)*{instr}), `%;%*`(z, (instr' <: admininstr)*{instr'}))
     -- Step_read: `%~>%*`(`%;%*`(z, (instr <: admininstr)*{instr}), (instr' <: admininstr)*{instr'})
@@ -3692,28 +3692,28 @@ relation Step: `%~>%`(config, config)
   rule data.drop {x : idx, z : state}:
     `%~>%`(`%;%*`(z, [DATA.DROP_admininstr(x)]), `%;%*`($with_data(z, x, []), []))
 
-;; 8-reduction.watsup:20.1-20.59
+;; 8-reduction.watsup:8.1-8.63
 rec {
 
-;; 8-reduction.watsup:20.1-20.59
-relation Eval: `%~>*%;%*`(config, state, val*)
-  ;; 8-reduction.watsup:23.1-24.22
-  rule done {val* : val*, z : state}:
-    `%~>*%;%*`(`%;%*`(z, (val <: admininstr)*{val}), z, val*{val})
+;; 8-reduction.watsup:8.1-8.63
+relation Steps: `%~>*%`(config, config)
+  ;; 8-reduction.watsup:18.1-19.36
+  rule refl {admininstr* : admininstr*, z : state}:
+    `%~>*%`(`%;%*`(z, admininstr*{admininstr}), `%;%*`(z, admininstr*{admininstr}))
 
-  ;; 8-reduction.watsup:26.1-29.43
-  rule step {admininstr* : admininstr*, admininstr' : admininstr, val* : val*, z : state, z' : state, z'' : state}:
-    `%~>*%;%*`(`%;%*`(z, admininstr*{admininstr}), z'', val*{val})
+  ;; 8-reduction.watsup:21.1-24.53
+  rule trans {admininstr* : admininstr*, admininstr' : admininstr, admininstr''* : admininstr*, z : state, z' : state, z'' : state}:
+    `%~>*%`(`%;%*`(z, admininstr*{admininstr}), `%;%*`(z'', admininstr''*{admininstr''}))
     -- Step: `%~>%`(`%;%*`(z, admininstr*{admininstr}), `%;%*`(z', admininstr'*{}))
-    -- Eval: `%~>*%;%*`(`%;%*`(z', [admininstr']), z'', val*{val})
+    -- Steps: `%~>*%`(`%;%*`(z', [admininstr']), `%;%*`(z'', admininstr''*{admininstr''}))
 }
 
-;; 8-reduction.watsup:21.1-21.69
+;; 8-reduction.watsup:29.1-29.69
 relation Eval_expr: `%;%~>*%;%*`(state, expr, state, val*)
-  ;; 8-reduction.watsup:31.1-33.35
+  ;; 8-reduction.watsup:31.1-33.37
   rule _ {instr* : instr*, val* : val*, z : state, z' : state}:
     `%;%~>*%;%*`(z, instr*{instr}, z', val*{val})
-    -- Eval: `%~>*%;%*`(`%;%*`(z, (instr <: admininstr)*{instr}), z, val*{val})
+    -- Steps: `%~>*%`(`%;%*`(z, (instr <: admininstr)*{instr}), `%;%*`(z', (val <: admininstr)*{val}))
 
 ;; 9-module.watsup:7.1-7.34
 rec {
@@ -8054,6 +8054,8 @@ $\boxed{{{{\mathit{instr}}}^\ast} \hookrightarrow {{{\mathit{instr}}}^\ast}}$
 
 $\boxed{{\mathit{config}} \hookrightarrow {{{\mathit{instr}}}^\ast}}$
 
+$\boxed{{\mathit{config}} \hookrightarrow^\ast {\mathit{config}}}$
+
 $$
 \begin{array}{@{}l@{}lcl@{}l@{}}
 {[\textsc{\scriptsize E{-}pure}]} \quad & {\mathit{z}} ; {{\mathit{instr}}^\ast} &\hookrightarrow& {\mathit{z}} ; {{\mathit{instr}'}^\ast} &\quad
@@ -8063,25 +8065,23 @@ $$
 \end{array}
 $$
 
-\vspace{1ex}
-
-$\boxed{{\mathit{config}} \hookrightarrow^\ast {\mathit{state}} ; {{\mathit{val}}^\ast}}$
-
-$\boxed{{\mathit{state}} ; {\mathit{expr}} \hookrightarrow^\ast {\mathit{state}} ; {{\mathit{val}}^\ast}}$
-
 $$
 \begin{array}{@{}l@{}lcl@{}l@{}}
-{[\textsc{\scriptsize E{-}expr{-}done}]} \quad & {\mathit{z}} ; {{\mathit{val}}^\ast} &\hookrightarrow^\ast& {\mathit{z}} ; {{\mathit{val}}^\ast} &  \\
-{[\textsc{\scriptsize E{-}expr{-}step}]} \quad & {\mathit{z}} ; {{{\mathit{instr}}}^\ast} &\hookrightarrow^\ast& {\mathit{z}''} ; {{\mathit{val}}^\ast} &\quad
+{[\textsc{\scriptsize E{-}refl}]} \quad & {\mathit{z}} ; {{{\mathit{instr}}}^\ast} &\hookrightarrow^\ast& {\mathit{z}} ; {{{\mathit{instr}}}^\ast} &  \\
+{[\textsc{\scriptsize E{-}trans}]} \quad & {\mathit{z}} ; {{{\mathit{instr}}}^\ast} &\hookrightarrow^\ast& {\mathit{z}''} ; {{{\mathit{instr}}''}^\ast} &\quad
   \mbox{if}~{\mathit{z}} ; {{{\mathit{instr}}}^\ast} \hookrightarrow {\mathit{z}'} ; {{{\mathit{instr}}'}^\ast} \\
- &&&&\quad {\land}~{\mathit{z}'} ; {{\mathit{instr}}'} \hookrightarrow^\ast {\mathit{z}''} ; {{\mathit{val}}^\ast} \\
+ &&&&\quad {\land}~{\mathit{z}'} ; {{\mathit{instr}}'} \hookrightarrow^\ast {\mathit{z}''} ; {{{\mathit{instr}}''}^\ast} \\
 \end{array}
 $$
 
+\vspace{1ex}
+
+$\boxed{{\mathit{state}} ; {\mathit{expr}} \hookrightarrow^\ast {\mathit{state}} ; {{\mathit{val}}^\ast}}$
+
 $$
 \begin{array}{@{}l@{}lcl@{}l@{}}
 {[\textsc{\scriptsize E{-}expr}]} \quad & {\mathit{z}} ; {{\mathit{instr}}^\ast} &\hookrightarrow^\ast& {\mathit{z}'} ; {{\mathit{val}}^\ast} &\quad
-  \mbox{if}~{\mathit{z}} ; {{\mathit{instr}}^\ast} \hookrightarrow^\ast {\mathit{z}} ; {{\mathit{val}}^\ast} \\
+  \mbox{if}~{\mathit{z}} ; {{\mathit{instr}}^\ast} \hookrightarrow^\ast {\mathit{z}'} ; {{\mathit{val}}^\ast} \\
 \end{array}
 $$
 

spectec/test-latex/TEST.md

@@ -257,8 +257,6 @@ warning: rule `Elem_ok` was never spliced
 warning: rule `Elemmode_ok/active` was never spliced
 warning: rule `Elemmode_ok/passive` was never spliced
 warning: rule `Elemmode_ok/declare` was never spliced
-warning: rule `Eval/done` was never spliced
-warning: rule `Eval/step` was never spliced
 warning: rule `Eval_expr` was never spliced
 warning: rule `Expand` was never spliced
 warning: rule `Export_ok` was never spliced
@@ -571,6 +569,8 @@ warning: rule `Step_read/memory.copy-gt` was never spliced
 warning: rule `Step_read/memory.init-oob` was never spliced
 warning: rule `Step_read/memory.init-zero` was never spliced
 warning: rule `Step_read/memory.init-succ` was never spliced
+warning: rule `Steps/refl` was never spliced
+warning: rule `Steps/trans` was never spliced
 warning: rule `Storagetype_ok/val` was never spliced
 warning: rule `Storagetype_ok/packed` was never spliced
 warning: rule `Storagetype_sub/val` was never spliced