Rocq backend

specification/wasm-1.0/B-soundness.spectec

@@ -129,13 +129,13 @@ rule Globalinst_ok:
   -- Val_ok: |- val : t
 
 rule Meminst_ok:
-  s |- {TYPE `[n..m], BYTES b*} : `[n..m]
-  -- Memtype_ok: |- `[n..m] : OK
+  s |- {TYPE `[n..m?], BYTES b*} : `[n..m?]
+  -- Memtype_ok: |- `[n..m?] : OK
   -- if |b*| = $(n * $($(64 * $Ki)))
 
 rule Tableinst_ok:
-  s |- {TYPE `[n..m] , REFS (fa?)*} : `[n..m]
-  -- Tabletype_ok: |- `[n..m] : OK
+  s |- {TYPE `[n..m?] , REFS (fa?)*} : `[n..m?]
+  -- Tabletype_ok: |- `[n..m?] : OK
   -- ((Externaddr_ok: s |- FUNC fa : FUNC ft)?)*
   -- if |(fa?)*| = n
 
@@ -204,12 +204,12 @@ rule Extend_globalinst:
   -- if mut = MUT \/ val = val'
 
 rule Extend_meminst:
-  {TYPE `[n..m], BYTES b*} `<= {TYPE `[n'..m], BYTES b'*}
+  {TYPE `[n..m?], BYTES b*} `<= {TYPE `[n'..m?], BYTES b'*}
   -- if n <= n'
   -- if |b*| <= |b'*|
 
 rule Extend_tableinst:
-  {TYPE `[n..m], REFS ref*} `<= {TYPE `[n'..m], REFS ref'*}
+  {TYPE `[n..m?], REFS ref*} `<= {TYPE `[n'..m?], REFS ref'*}
   -- if n <= n'
   -- if |ref*| <= |ref'*|
 
@@ -240,6 +240,6 @@ rule State_ok:
   -- Frame_ok: s |- f : C
 
 rule Config_ok:
-  |- s; f; instr* : t?
+  |- s; f; admininstr* : t?
   -- State_ok: |- s; f : C
   -- Expr_ok2: s; C |- admininstr* : t?

specification/wasm-2.0/8-reduction.spectec

@@ -2,9 +2,9 @@
 ;; Configurations
 ;;
 
-relation Step: config ~> config                 hint(show "E") hint(tabular)
-relation Step_pure: admininstr* ~> admininstr*  hint(show "E") hint(tabular)
-relation Step_read: config ~> admininstr*       hint(show "E") hint(tabular)
+relation Step: config ~> config                 hint(show "E") hint(tabular) hint(mode %1 -> %2) hint(wfopt) 
+relation Step_pure: admininstr* ~> admininstr*  hint(show "E") hint(tabular) hint(mode %1 -> %2) hint(wfopt) 
+relation Step_read: config ~> admininstr*       hint(show "E") hint(tabular) hint(mode %1 -> %2) hint(wfopt) 
 relation Steps: config ~>* config               hint(show "E") hint(tabular)
 
 rule Step/pure:

specification/wasm-2.0/9-module.spectec

@@ -158,7 +158,7 @@ def $runelem(ELEM reftype expr* (ACTIVE x instr*), i) =
   instr* (CONST I32 0) (CONST I32 n) (TABLE.INIT x i) (ELEM.DROP i)
   -- if n = |expr*|
 
-def $rundata(data, idx) : instr*
+def $rundata(data, idx) : instr* hint(partial)
 def $rundata(DATA byte* (PASSIVE), i) = eps
 def $rundata(DATA byte* (ACTIVE 0 instr*), i) =
   instr* (CONST I32 0) (CONST I32 n) (MEMORY.INIT i) (DATA.DROP i)

specification/wasm-2.0/B-soundness.spectec

@@ -107,7 +107,7 @@ rule Instrs_ok2/seq:
   -- Instrs_ok2: s; C |- admininstr_2* : t_2* -> t_3*
 
 rule Instrs_ok2/sub:
-  s; C |- instr* : t'_1* -> t'_2*
+  s; C |- admininstr* : t'_1* -> t'_2*
   -- Instrs_ok2: s; C |- admininstr* : t_1* -> t_2*
   -- Resulttype_sub: |- t'_1* <: t_1*
   -- Resulttype_sub: |- t_2* <: t'_2*
@@ -161,13 +161,13 @@ rule Globalinst_ok:
   -- Val_ok: s |- val : t
 
 rule Meminst_ok:
-  s |- {TYPE `[n..m] PAGE, BYTES b*} : `[n..m] PAGE
-  -- Memtype_ok: |- `[n..m] PAGE : OK
+  s |- {TYPE `[n..m?] PAGE, BYTES b*} : `[n..m?] PAGE
+  -- Memtype_ok: |- `[n..m?] PAGE : OK
   -- if |b*| = $(n * $($(64 * $Ki)))
 
 rule Tableinst_ok:
-  s |- {TYPE `[n..m] rt , REFS ref*} : `[n..m] rt
-  -- Tabletype_ok: |- `[n..m] rt : OK
+  s |- {TYPE `[n..m?] rt , REFS ref*} : `[n..m?] rt
+  -- Tabletype_ok: |- `[n..m?] rt : OK
   -- (Ref_ok : s |- ref : rt)*
   -- if |ref*| = n
 
@@ -254,12 +254,12 @@ rule Extend_globalinst:
   -- if mut = MUT \/ val = val'
 
 rule Extend_meminst:
-  {TYPE `[n..m] PAGE, BYTES b*} `<= {TYPE `[n'..m] PAGE, BYTES b'*}
+  {TYPE `[n..m?] PAGE, BYTES b*} `<= {TYPE `[n'..m?] PAGE, BYTES b'*}
   -- if n <= n'
   -- if |b*| <= |b'*|
 
 rule Extend_tableinst:
-  {TYPE `[n..m] rt, REFS ref*} `<= {TYPE `[n'..m] rt, REFS ref'*}
+  {TYPE `[n..m?] rt, REFS ref*} `<= {TYPE `[n'..m?] rt, REFS ref'*}
   -- if n <= n'
   -- if |ref*| <= |ref'*|
 
@@ -300,6 +300,6 @@ rule State_ok:
   -- Frame_ok: s |- f : C
 
 rule Config_ok:
-  |- s; f; instr* : t*
+  |- s; f; admininstr* : t*
   -- State_ok: |- s; f : C
   -- Expr_ok2: s; C |- admininstr* : t*

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

@@ -398,7 +398,7 @@ def $subst_comptype((FUNC t_1* -> t_2*), tv*, tu*) = FUNC $subst_valtype(t_1, tv
 def $subst_subtype((SUB final? tu'* ct), tv*, tu*) =
   SUB final? $subst_typeuse(tu', tv*, tu*)* $subst_comptype(ct, tv*, tu*)
 
-def $minus_recs(typevar*, typeuse*) : (typevar*, typeuse*) hint(partial)
+def $minus_recs(typevar*, typeuse*) : (typevar*, typeuse*) hint(partial) hint(recfunc)
 def $minus_recs(eps, eps) = (eps, eps)
 def $minus_recs((REC n) tv*, tu_1 tu*) = $minus_recs(tv*, tu*)
 def $minus_recs((_IDX x) tv*, tu_1 tu*) = ((_IDX x) tv'*, tu_1 tu'*)

specification/wasm-3.0/3.2-numerics.vector.spectec

@@ -51,11 +51,11 @@ def $irelaxed_swizzle_lane_(N, c*, i) = $relaxed2($R_swizzle, iN(N), 0, c*[i \ |
 
 ;; Lanewise operations
 
-def $ivunop_(shape, def $f_(N, iN(N)) : iN(N), vec_(V128)) : vec_(V128)*
+def $ivunop_(shape, def $f_(N, iN(N)) : iN(N), vec_(V128)) : vec_(V128)* hint(partial)
 def $fvunop_(shape, def $f_(N, fN(N)) : fN(N)*, vec_(V128)) : vec_(V128)*
 
-def $ivbinop_(shape, def $f_(N, iN(N), iN(N)) : iN(N), vec_(V128), vec_(V128)) : vec_(V128)*
-def $ivbinopsx_(shape, def $f_(N, sx, iN(N), iN(N)) : iN(N), sx, vec_(V128), vec_(V128)) : vec_(V128)*
+def $ivbinop_(shape, def $f_(N, iN(N), iN(N)) : iN(N), vec_(V128), vec_(V128)) : vec_(V128)* hint(partial)
+def $ivbinopsx_(shape, def $f_(N, sx, iN(N), iN(N)) : iN(N), sx, vec_(V128), vec_(V128)) : vec_(V128)* hint(partial)
 def $ivbinopsxnd_(shape, def $f_(N, sx, iN(N), iN(N)) : iN(N)*, sx, vec_(V128), vec_(V128)) : vec_(V128)*
 def $fvbinop_(shape, def $f_(N, fN(N), fN(N)) : fN(N)*, vec_(V128), vec_(V128)) : vec_(V128)*
 
@@ -66,12 +66,12 @@ def $ivrelop_(shape, def $f_(N, iN(N), iN(N)) : u32, vec_(V128), vec_(V128)) : v
 def $ivrelopsx_(shape, def $f_(N, sx, iN(N), iN(N)) : u32, sx, vec_(V128), vec_(V128)) : vec_(V128)
 def $fvrelop_(shape, def $f_(N, fN(N), fN(N)) : u32, vec_(V128), vec_(V128)) : vec_(V128)
 
-def $ivshiftop_(shape, def $f_(N, iN(N), u32) : iN(N), vec_(V128), u32) : vec_(V128)
-def $ivshiftopsx_(shape, def $f_(N, sx, iN(N), u32) : iN(N), sx, vec_(V128), u32) : vec_(V128)
+def $ivshiftop_(shape, def $f_(N, iN(N), u32) : iN(N), vec_(V128), u32) : vec_(V128) hint(partial)
+def $ivshiftopsx_(shape, def $f_(N, sx, iN(N), u32) : iN(N), sx, vec_(V128), u32) : vec_(V128) hint(partial)
 
 def $ivbitmaskop_(shape, vec_(V128)) : u32
-def $ivswizzlop_(shape, def $f_(N, iN(N)*, iN(N)) : iN(N), vec_(V128), vec_(V128)) : vec_(V128)
-def $ivshufflop_(shape, laneidx*, vec_(V128), vec_(V128)) : vec_(V128)
+def $ivswizzlop_(shape, def $f_(N, iN(N)*, iN(N)) : iN(N), vec_(V128), vec_(V128)) : vec_(V128) hint(partial)
+def $ivshufflop_(shape, laneidx*, vec_(V128), vec_(V128)) : vec_(V128) hint(partial)
 
 
 def $ivunop_(Jnn X M, def $f_, v_1) = $inv_lanes_(Jnn X M, c*)
@@ -189,7 +189,7 @@ def $vbitmaskop_(ishape, vec_(V128)) : u32
     hint(show VBITMASK#$_(%1,%2))
 def $vswizzlop_(bshape, vswizzlop_(bshape), vec_(V128), vec_(V128)) : vec_(V128)
     hint(show %2#$_(%1,%3,%4))
-def $vshufflop_(bshape, laneidx*, vec_(V128), vec_(V128)) : vec_(V128)
+def $vshufflop_(bshape, laneidx*, vec_(V128), vec_(V128)) : vec_(V128) hint(partial)
     hint(show VSHUFFLE#$_(%1,%2,%3,%4))
 
 def $vnarrowop__(shape_1, shape_2, sx, vec_(V128), vec_(V128)) : vec_(V128)

specification/wasm-3.0/7.1-soundness.configurations.spectec

@@ -86,13 +86,13 @@ rule Globalinst_ok:
   -- Val_ok: s |- val : t
 
 rule Meminst_ok:
-  s |- {TYPE at `[n..m] PAGE, BYTES b*} : at `[n..m] PAGE
-  -- Memtype_ok: {} |- at `[n..m] PAGE : OK
+  s |- {TYPE at `[n..m?] PAGE, BYTES b*} : at `[n..m?] PAGE
+  -- Memtype_ok: {} |- at `[n..m?] PAGE : OK
   -- if |b*| = $(n * $($(64 * $Ki)))
 
 rule Tableinst_ok:
-  s |- {TYPE at `[n..m] rt, REFS ref*} : at `[n..m] rt
-  -- Tabletype_ok: {} |- at `[n..m] rt : OK
+  s |- {TYPE at `[n..m?] rt, REFS ref*} : at `[n..m?] rt
+  -- Tabletype_ok: {} |- at `[n..m?] rt : OK
   -- if |ref*| = n
   -- (Ref_ok: s |- ref : rt)*
 
@@ -262,12 +262,12 @@ rule Extend_globalinst:
   -- if mut? = MUT \/ val = val'
 
 rule Extend_meminst:
-  {TYPE at `[n..m] PAGE, BYTES b*} `<= {TYPE at `[n'..m] PAGE, BYTES b'*}
+  {TYPE at `[n..m?] PAGE, BYTES b*} `<= {TYPE at `[n'..m?] PAGE, BYTES b'*}
   -- if n <= n'
   -- if |b*| <= |b'*|
 
 rule Extend_tableinst:
-  {TYPE at `[n..m] rt, REFS ref*} `<= {TYPE at `[n'..m] rt, REFS ref'*}
+  {TYPE at `[n..m?] rt, REFS ref*} `<= {TYPE at `[n'..m?] rt, REFS ref'*}
   -- if n <= n'
   -- if |ref*| <= |ref'*|
 

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

@@ -398,7 +398,7 @@ def $subst_comptype((FUNC t_1* -> t_2*), tv*, tu*) = FUNC $subst_valtype(t_1, tv
 def $subst_subtype((SUB final? tu'* ct), tv*, tu*) =
   SUB final? $subst_typeuse(tu', tv*, tu*)* $subst_comptype(ct, tv*, tu*)
 
-def $minus_recs(typevar*, typeuse*) : (typevar*, typeuse*) hint(partial)
+def $minus_recs(typevar*, typeuse*) : (typevar*, typeuse*) hint(partial) hint(recfunc)
 def $minus_recs(eps, eps) = (eps, eps)
 def $minus_recs((REC n) tv*, tu_1 tu*) = $minus_recs(tv*, tu*)
 def $minus_recs((_IDX x) tv*, tu_1 tu*) = ((_IDX x) tv'*, tu_1 tu'*)

specification/wasm-latest/3.2-numerics.vector.spectec

@@ -51,11 +51,11 @@ def $irelaxed_swizzle_lane_(N, c*, i) = $relaxed2($R_swizzle, iN(N), 0, c*[i \ |
 
 ;; Lanewise operations
 
-def $ivunop_(shape, def $f_(N, iN(N)) : iN(N), vec_(V128)) : vec_(V128)*
+def $ivunop_(shape, def $f_(N, iN(N)) : iN(N), vec_(V128)) : vec_(V128)* hint(partial)
 def $fvunop_(shape, def $f_(N, fN(N)) : fN(N)*, vec_(V128)) : vec_(V128)*
 
-def $ivbinop_(shape, def $f_(N, iN(N), iN(N)) : iN(N), vec_(V128), vec_(V128)) : vec_(V128)*
-def $ivbinopsx_(shape, def $f_(N, sx, iN(N), iN(N)) : iN(N), sx, vec_(V128), vec_(V128)) : vec_(V128)*
+def $ivbinop_(shape, def $f_(N, iN(N), iN(N)) : iN(N), vec_(V128), vec_(V128)) : vec_(V128)* hint(partial)
+def $ivbinopsx_(shape, def $f_(N, sx, iN(N), iN(N)) : iN(N), sx, vec_(V128), vec_(V128)) : vec_(V128)* hint(partial)
 def $ivbinopsxnd_(shape, def $f_(N, sx, iN(N), iN(N)) : iN(N)*, sx, vec_(V128), vec_(V128)) : vec_(V128)*
 def $fvbinop_(shape, def $f_(N, fN(N), fN(N)) : fN(N)*, vec_(V128), vec_(V128)) : vec_(V128)*
 
@@ -66,12 +66,12 @@ def $ivrelop_(shape, def $f_(N, iN(N), iN(N)) : u32, vec_(V128), vec_(V128)) : v
 def $ivrelopsx_(shape, def $f_(N, sx, iN(N), iN(N)) : u32, sx, vec_(V128), vec_(V128)) : vec_(V128)
 def $fvrelop_(shape, def $f_(N, fN(N), fN(N)) : u32, vec_(V128), vec_(V128)) : vec_(V128)
 
-def $ivshiftop_(shape, def $f_(N, iN(N), u32) : iN(N), vec_(V128), u32) : vec_(V128)
-def $ivshiftopsx_(shape, def $f_(N, sx, iN(N), u32) : iN(N), sx, vec_(V128), u32) : vec_(V128)
+def $ivshiftop_(shape, def $f_(N, iN(N), u32) : iN(N), vec_(V128), u32) : vec_(V128) hint(partial)
+def $ivshiftopsx_(shape, def $f_(N, sx, iN(N), u32) : iN(N), sx, vec_(V128), u32) : vec_(V128) hint(partial)
 
 def $ivbitmaskop_(shape, vec_(V128)) : u32
-def $ivswizzlop_(shape, def $f_(N, iN(N)*, iN(N)) : iN(N), vec_(V128), vec_(V128)) : vec_(V128)
-def $ivshufflop_(shape, laneidx*, vec_(V128), vec_(V128)) : vec_(V128)
+def $ivswizzlop_(shape, def $f_(N, iN(N)*, iN(N)) : iN(N), vec_(V128), vec_(V128)) : vec_(V128) hint(partial)
+def $ivshufflop_(shape, laneidx*, vec_(V128), vec_(V128)) : vec_(V128) hint(partial)
 
 
 def $ivunop_(Jnn X M, def $f_, v_1) = $inv_lanes_(Jnn X M, c*)
@@ -189,7 +189,7 @@ def $vbitmaskop_(ishape, vec_(V128)) : u32
     hint(show VBITMASK#$_(%1,%2))
 def $vswizzlop_(bshape, vswizzlop_(bshape), vec_(V128), vec_(V128)) : vec_(V128)
     hint(show %2#$_(%1,%3,%4))
-def $vshufflop_(bshape, laneidx*, vec_(V128), vec_(V128)) : vec_(V128)
+def $vshufflop_(bshape, laneidx*, vec_(V128), vec_(V128)) : vec_(V128) hint(partial)
     hint(show VSHUFFLE#$_(%1,%2,%3,%4))
 
 def $vnarrowop__(shape_1, shape_2, sx, vec_(V128), vec_(V128)) : vec_(V128)

specification/wasm-latest/7.1-soundness.configurations.spectec

@@ -86,13 +86,13 @@ rule Globalinst_ok:
   -- Val_ok: s |- val : t
 
 rule Meminst_ok:
-  s |- {TYPE at `[n..m] PAGE, BYTES b*} : at `[n..m] PAGE
-  -- Memtype_ok: {} |- at `[n..m] PAGE : OK
+  s |- {TYPE at `[n..m?] PAGE, BYTES b*} : at `[n..m?] PAGE
+  -- Memtype_ok: {} |- at `[n..m?] PAGE : OK
   -- if |b*| = $(n * $($(64 * $Ki)))
 
 rule Tableinst_ok:
-  s |- {TYPE at `[n..m] rt, REFS ref*} : at `[n..m] rt
-  -- Tabletype_ok: {} |- at `[n..m] rt : OK
+  s |- {TYPE at `[n..m?] rt, REFS ref*} : at `[n..m?] rt
+  -- Tabletype_ok: {} |- at `[n..m?] rt : OK
   -- if |ref*| = n
   -- (Ref_ok: s |- ref : rt)*