[spectec] Backport missing instantiation checks to Wasm 1.0/2.0 specs

specification/wasm-1.0/0-aux.spectec

@@ -40,3 +40,7 @@ def $list_(syntax X, w) = w
 def $concat_(syntax X, (X*)*) : X*  hint(show $concat(%2))
 def $concat_(syntax X, eps) = eps
 def $concat_(syntax X, (w*) (w'*)*) = w* $concat_(X, (w'*)*)
+
+def $disjoint_(syntax X, X*) : bool  hint(show %2 $disjoint) hint(macro none)
+def $disjoint_(syntax X, eps) = true
+def $disjoint_(syntax X, w w'*) = ~(w <- w'*) /\ $disjoint_(X, w'*)

specification/wasm-1.0/6-typing.spectec

@@ -404,15 +404,15 @@ rule Start_ok:
 ;; Module im/exports
 
 relation Import_ok: context |- import : externtype        hint(show "T-import")
-relation Export_ok: context |- export : externtype        hint(show "T-export")
+relation Export_ok: context |- export : name externtype   hint(show "T-export")
 relation Externidx_ok: context |- externidx : externtype  hint(show "T-externidx")
 
 rule Import_ok:
   C |- IMPORT name_1 name_2 xt : xt
   -- Externtype_ok: |- xt : OK
 
 rule Export_ok:
-  C |- EXPORT name externidx : xt
+  C |- EXPORT name externidx : name xt
   -- Externidx_ok: C |- externidx : xt
 
 
@@ -450,11 +450,11 @@ rule Module_ok:
   -- (Elem_ok: C |- elem : OK)*
   -- (Data_ok: C |- data : OK)*
   -- (Start_ok: C |- start : OK)?
-  -- (Export_ok: C |- export : xt)*
+  -- (Export_ok: C |- export : nm xt)*
   ----
   -- if |tt*| <= 1
   -- if |mt*| <= 1
-  ;; -- TODO: disjoint export names
+  -- if $disjoint_(name, nm*)
   ----
   -- if C = {TYPES ft'*, FUNCS ift* ft*, GLOBALS igt* gt*, TABLES itt* tt*, MEMS imt* mt*}
   ----

specification/wasm-1.0/9-module.spectec

@@ -1,3 +1,32 @@
+;;
+;; External addresses
+;;
+
+relation Externaddr_ok: store |- externaddr : externtype  hint(macro "%externaddr")
+
+rule Externaddr_ok/global:
+  s |- GLOBAL a : GLOBAL globalinst.TYPE
+  -- if s.GLOBALS[a] = globalinst
+
+rule Externaddr_ok/mem:
+  s |- MEM a : MEM meminst.TYPE
+  -- if s.MEMS[a] = meminst
+
+rule Externaddr_ok/table:
+  s |- TABLE a : TABLE tableinst.TYPE
+  -- if s.TABLES[a] = tableinst
+
+rule Externaddr_ok/func:
+  s |- FUNC a : FUNC funcinst.TYPE
+  -- if s.FUNCS[a] = funcinst
+
+rule Externaddr_ok/sub:
+  s |- externaddr : xt
+  -- Externaddr_ok: s |- externaddr : xt'
+  -- Externtype_ok: |- xt : OK
+  -- Externtype_sub: |- xt' <: xt
+
+
 ;;
 ;; Projections
 ;;
@@ -139,6 +168,8 @@ def $initdata(s, moduleinst, i i'*, (b*) (b'*)*) = s_2
 
 def $instantiate(store, module, externaddr*) : config
 def $instantiate(s, module, externaddr*) = s_3; f; (CALL x')?
+  -- Module_ok: |- module : xt_I* -> xt_E*
+  -- (Externaddr_ok: s |- externaddr : xt_I)*
   -- if module = MODULE type* import* func* global* table* mem* elem* data* start? export*
   -- if type* = (TYPE functype)*
   -- if global* = (GLOBAL globaltype expr_G)*

specification/wasm-2.0/0-aux.spectec

@@ -43,6 +43,10 @@ def $concat_(syntax X, (w*) (w'*)*) = w* $concat_(X, (w'*)*)
 def $inv_concat_(syntax X, X*) : (X*)*
 def $inv_concat_ hint(builtin)
 
+def $disjoint_(syntax X, X*) : bool  hint(show %2 $disjoint) hint(macro none)
+def $disjoint_(syntax X, eps) = true
+def $disjoint_(syntax X, w w'*) = ~(w <- w'*) /\ $disjoint_(X, w'*)
+
 
 ;; [{1, 2}, {a, b, c}] -> {[1, a], [1, b], [1, c], [2, a], [2, b], [2, c]}
 def $setproduct_(syntax X, (X*)*) : (X*)*  hint(show %latex("{\\Large\\times}") %2)

specification/wasm-2.0/6-typing.spectec

@@ -645,15 +645,15 @@ rule Start_ok:
 ;; Module im/exports
 
 relation Import_ok: context |- import : externtype        hint(show "T-import")
-relation Export_ok: context |- export : externtype        hint(show "T-export")
+relation Export_ok: context |- export : name externtype   hint(show "T-export")
 relation Externidx_ok: context |- externidx : externtype  hint(show "T-externidx")
 
 rule Import_ok:
   C |- IMPORT name_1 name_2 xt : xt
   -- Externtype_ok: |- xt : OK
 
 rule Export_ok:
-  C |- EXPORT name externidx : xt
+  C |- EXPORT name externidx : name xt
   -- Externidx_ok: C |- externidx : xt
 
 
@@ -693,10 +693,10 @@ rule Module_ok:
   ----
   -- (Func_ok: C |- func : ft)*
   -- (Start_ok: C |- start : OK)?
-  -- (Export_ok: C |- export : xt)*
+  -- (Export_ok: C |- export : nm xt)*
   ----
   -- if |mt*| <= 1
-  ;; -- TODO: disjoint export names
+  -- if $disjoint_(name, nm*)
   ----
   -- if C = {TYPES ft'*, FUNCS ift* ft*, GLOBALS igt* gt*, TABLES itt* tt*, MEMS imt* mt*, ELEMS rt*, DATAS OK^n}
   ----

specification/wasm-2.0/9-module.spectec

@@ -1,3 +1,32 @@
+;;
+;; External addresses
+;;
+
+relation Externaddr_ok: store |- externaddr : externtype  hint(macro "%externaddr")
+
+rule Externaddr_ok/global:
+  s |- GLOBAL a : GLOBAL globalinst.TYPE
+  -- if s.GLOBALS[a] = globalinst
+
+rule Externaddr_ok/mem:
+  s |- MEM a : MEM meminst.TYPE
+  -- if s.MEMS[a] = meminst
+
+rule Externaddr_ok/table:
+  s |- TABLE a : TABLE tableinst.TYPE
+  -- if s.TABLES[a] = tableinst
+
+rule Externaddr_ok/func:
+  s |- FUNC a : FUNC funcinst.TYPE
+  -- if s.FUNCS[a] = funcinst
+
+rule Externaddr_ok/sub:
+  s |- externaddr : xt
+  -- Externaddr_ok: s |- externaddr : xt'
+  -- Externtype_ok: |- xt : OK
+  -- Externtype_sub: |- xt' <: xt
+
+
 ;;
 ;; Projections
 ;;
@@ -166,6 +195,8 @@ def $rundata(DATA byte* (ACTIVE 0 instr*), i) =
 
 def $instantiate(store, module, externaddr*) : config
 def $instantiate(s, module, externaddr*) = s'; f; instr_E* instr_D* (CALL x)?
+  -- Module_ok: |- module : xt_I* -> xt_E*
+  -- (Externaddr_ok: s |- externaddr : xt_I)*
   -- if module = MODULE type* import* func* global* table* mem* elem* data* start? export*
   -- if type* = (TYPE functype)*
   -- if global* = (GLOBAL globaltype expr_G)*

spectec/src/backend-interpreter/relation.ml

@@ -44,7 +44,9 @@ let ref_ok =
   | vs -> Numerics.error_values "$Ref_ok" vs
 
 let module_ok v =
+(* Use Wasm-3 validator for Wasm-1+2 as well. Does not work for negative tests!
   if !Construct.version <> 3 then failwith "This hardcoded function ($Module_ok) should be only called with test version 3.0";
+*)
   match v with
   | [ m ] ->
     (try