[spec] Define soundness rules in SpecTec

document/core/Makefile

@@ -352,7 +352,7 @@ latex:
 latexpdf: $(GENERATED)
 	$(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
 	@echo "Running LaTeX files through pdflatex..."
-	$(MAKE) -C $(BUILDDIR)/latex LATEXMKOPTS=" </dev/null" all-pdf >$(BUILDDIR)/latex/LOG 2>&1 || cat $(BUILDDIR)/latex/LOG
+	$(MAKE) -C $(BUILDDIR)/latex LATEXMKOPTS=" -file-line-error -halt-on-error" all-pdf >$(BUILDDIR)/latex/LOG 2>&1 || cat $(BUILDDIR)/latex/LOG
 	@echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
 
 .PHONY: latexpdfja

document/core/appendix/properties.rst

@@ -287,6 +287,14 @@ Results
    }
 
 
+.. _valid-localtype:
+.. _valid-context:
+
+.. todo
+   Context Validity
+   ~~~~~~~~~~~~~~~~
+
+
 .. _module-context:
 .. _valid-store:
 

document/core/util/macros.def

@@ -1183,6 +1183,7 @@
 .. |vdashtabletype| mathdef:: \xref{valid/types}{valid-tabletype}{\vdash}
 .. |vdashmemtype| mathdef:: \xref{valid/types}{valid-memtype}{\vdash}
 .. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash}
+.. |vdashlocaltype| mathdef:: \xref{appendix/properties}{valid-localtype}{\vdash}
 .. |vdashtagtype| mathdef:: \xref{valid/types}{valid-tagtype}{\vdash}
 .. |vdashexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\vdash}
 .. |vdashdeftype| mathdef:: \xref{appendix/properties}{valid-deftype}{\vdash}
@@ -1209,6 +1210,7 @@
 .. |OKtabletype| mathdef:: \xref{valid/types}{valid-tabletype}{\K{ok}}
 .. |OKmemtype| mathdef:: \xref{valid/types}{valid-memtype}{\K{ok}}
 .. |OKglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\K{ok}}
+.. |OKlocaltype| mathdef:: \xref{appendix/properties}{valid-localtype}{\K{ok}}
 .. |OKtagtype| mathdef:: \xref{valid/types}{valid-tagtype}{\K{ok}}
 .. |OKexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\K{ok}}
 .. |OKlimits| mathdef:: \xref{valid/types}{valid-limits}{\K{ok}}
@@ -1302,6 +1304,9 @@
 .. |zeroop| mathdef:: \xref{syntax/instructions}{aux-zeroop}{\F{zeroop}}
 .. |halfop| mathdef:: \xref{syntax/instructions}{aux-halfop}{\F{halfop}}
 
+.. |vdashcontext| mathdef:: \xref{appendix/properties}{valid-context}{\vdash}
+.. |OKcontext| mathdef:: \xref{appendix/properties}{valid-context}{\K{ok}}
+
 
 .. Execution
 .. ---------

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

@@ -24,6 +24,9 @@ rule Heaptype_ok/typeuse:
   C |- typeuse : OK
   -- Typeuse_ok: C |- typeuse : OK
 
+rule Heaptype_ok/bot:
+  C |- BOT : OK
+
 rule Reftype_ok:
   C |- REF NULL? heaptype : OK
   -- Heaptype_ok: C |- heaptype : OK
@@ -46,9 +49,14 @@ rule Valtype_ok/bot:
 
 ;; Result & instruction types
 
+relation Localtype_ok: context |- localtype : OK  hint(name "K-local") hint(macro "%localtype")
 relation Resulttype_ok: context |- resulttype : OK  hint(name "K-result") hint(macro "%resulttype")
 relation Instrtype_ok: context |- instrtype : OK    hint(name "K-instr")  hint(macro "%instrtype")
 
+rule Localtype_ok:
+  C |- init t : OK
+  -- Valtype_ok: C |- t : OK
+
 rule Resulttype_ok:
   C |- t* : OK
   -- (Valtype_ok: C |- t : OK)*
@@ -161,6 +169,7 @@ def $unrollht(C, REC i) = C.RECS[i]
 rule Subtype_ok2:
   C |- SUB FINAL? typeuse* compttype : OK x i
   -- if |typeuse*| <= 1
+  -- (Typeuse_ok: C |- typeuse : OK)*
   -- (if $before(typeuse, x, i))*
   -- (if $unrollht(C, typeuse) = SUB typeuse'* comptype')*
   ----
@@ -176,7 +185,7 @@ rule Rectype_ok/cons:
   -- Subtype_ok: C |- subtype_1 : OK(x)
   -- Rectype_ok: C |- REC subtype* : OK($(x+1))
 
-rule Rectype_ok/_rec2:
+rule Rectype_ok/rec2:
   C |- REC subtype* : OK(x)
   -- Rectype_ok2: C, RECS subtype* |- REC subtype* : OK x 0
 

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

@@ -637,7 +637,7 @@ rule Instrs_ok/frame:
 
 rule Expr_ok:
   C |- instr* : t*
-  -- Instrs_ok: C |- instr* : eps ->_(eps) t*
+  -- Instrs_ok: C |- instr* : eps -> t*
 
 
 ;; Constant expressions

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

@@ -81,6 +81,23 @@ rule Val_ok/ref:
   -- Ref_ok: s |- ref : rt
 
 
+;; Field values
+
+relation Packval_ok: store |- packval : packtype
+relation Fieldval_ok: store |- fieldval : storagetype
+
+rule Packval_ok:
+  s |- PACK pt c : pt
+
+rule Fieldval_ok/val:
+  s |- val : t
+  -- Val_ok: s |- val : t
+
+rule Fieldval_ok/packval:
+  s |- packval : pt
+  -- Packval_ok: s |- packval : pt
+
+
 ;; External addresses
 
 relation Externaddr_ok: store |- externaddr : externtype  hint(macro "%externaddr")

specification/wasm-3.0/7.0-soundness.contexts.spectec

@@ -0,0 +1,35 @@
+;; Contexts
+
+relation Context_ok: |- context : OK  hint(macro "%context")
+
+rule Context_ok:
+  |- C : OK
+  -- if C =
+    { TYPES dt^n,
+      RECS st^m,
+      TAGS jt*,
+      GLOBALS gt*,
+      MEMS mt*,
+      TABLES tt*,
+      FUNCS dt_F*,
+      DATAS ok*,
+      ELEMS et*,
+      LOCALS lct*,
+      LABELS rt*,
+      RETURN rt'?,
+      REFS x*
+    }
+  -- if C_0 = {TYPES dt^n}
+  -- (Deftype_ok: {TYPES dt^n[0 : i]} |- dt : OK)^(i<n)
+  -- (Subtype_ok2: {TYPES dt^n, RECS st^m} |- st : OK $(n + i) i)^(i<m)
+  -- (Tagtype_ok: C_0 |- jt : OK)*
+  -- (Globaltype_ok: C_0 |- gt : OK)*
+  -- (Memtype_ok: C_0 |- mt : OK)*
+  -- (Tabletype_ok: C_0 |- tt : OK)*
+  -- (Deftype_ok: C_0 |- dt_F : OK)*
+  -- (Expand: dt_F ~~ FUNC t_1 -> t_2)*
+  -- (Reftype_ok: C_0 |- et : OK)*
+  -- (Localtype_ok: C_0 |- lct : OK)*
+  -- (Resulttype_ok: C_0 |- rt : OK)*
+  -- (Resulttype_ok: C_0 |- rt' : OK)?
+  -- (if x < |dt_F*|)*