[spectec] Split def of context's RECS field; make struct extension work correctly

Author: rossberg

document/core/appendix/properties.rst

@@ -29,11 +29,7 @@ Contexts
 In order to check :ref:`rolled up <aux-roll-rectype>` recursive types,
 the :ref:`context <context>` is locally extended with an additional component that records the :ref:`sub type <syntax-subtype>` corresponding to each :ref:`recursive type index <syntax-rectypeidx>` within the current :ref:`recursive type <syntax-rectype>`:
 
-.. math::
-   \begin{array}{llll}
-   \production{context} & C &::=&
-     \{~ \dots, \CRECS ~ \subtype^\ast ~\} \\
-   \end{array}
+$${syntax: context/sem}
 
 
 .. index:: value type, reference type, heap type, bottom type, sub type, recursive type, recursive type index

document/core/valid/conventions.rst

@@ -218,7 +218,7 @@ Validity of an individual definition is specified relative to a *context*,
 which collects relevant information about the surrounding :ref:`module <syntax-module>` and the definitions in scope:
 
 * *Types*: the list of :ref:`types <syntax-type>` defined in the current module.
-* *Recursive Types*: the list of :ref:`sub types <syntax-subtype>` in the current group of recursive types.
+.. * *Recursive Types*: the list of :ref:`sub types <syntax-subtype>` in the current group of recursive types.
 * *Functions*: the list of :ref:`functions <syntax-func>` declared in the current module, represented by a :ref:`defined type <syntax-deftype>` that :ref:`expands <aux-expand-deftype>` to their :ref:`function type <syntax-functype>`.
 * *Tables*: the list of :ref:`tables <syntax-table>` declared in the current module, represented by their :ref:`table type <syntax-tabletype>`.
 * *Memories*: the list of :ref:`memories <syntax-mem>` declared in the current module, represented by their :ref:`memory type <syntax-memtype>`.
@@ -238,7 +238,10 @@ The label stack is the only part of the context that changes as validation of an
 
 More concretely, contexts are defined as :ref:`records <notation-record>` ${:C} with abstract syntax:
 
-$${syntax: context}
+$${syntax: context/syn}
+
+.. note::
+   The definition of contexts is :ref:`extended <context-ext>` with additional fields for the purpose of proving :ref:`type soundness <soundness>`.
 
 
 .. index:: ! type closure

document/core/valid/instructions.rst

@@ -33,7 +33,7 @@ Two degrees of polymorphism can be distinguished:
   the entire (or most of the) :ref:`instruction type <syntax-instrtype>` ${instrtype: t_1* -> t_2*} of the instruction is unconstrained.
   That is the case for all :ref:`control instructions <valid-instr-control>` that perform an *unconditional control transfer*, such as ${:UNREACHABLE}, ${:BR}, or ${:RETURN}.
 
-In both cases, the unconstrained types or type sequences can be chosen arbitrarily, as long as they meet the constraints imposed for the surrounding parts of the program.
+In both cases, the unconstrained types or type sequences can be chosen arbitrarily, as long as they are valid in the current :ref:`context <context>` and meet the constraints imposed for the surrounding parts of the program.
 
 .. note::
    For example, the ${:SELECT} instruction is valid with type ${instrtype: t t I32 -> t}, for any possible :ref:`number type <syntax-numtype>` ${:t}.

specification/wasm-latest/2.0-validation.contexts.spectec

@@ -21,9 +21,8 @@ var it : instrtype
 
 ;; Contexts
 
-syntax context hint(desc "context") hint(macro "%" "C%") =
+syntax context/syn hint(desc "context") hint(macro "%" "C%") =
   { TYPES deftype*          hint(desc "type"),
-    RECS subtype*           hint(desc "recursive type"),
     TAGS tagtype*           hint(desc "tag"),
     GLOBALS globaltype*     hint(desc "global"),
     MEMS memtype*           hint(desc "memory"),
@@ -34,7 +33,13 @@ syntax context hint(desc "context") hint(macro "%" "C%") =
     LOCALS localtype*       hint(desc "local"),
     LABELS resulttype*      hint(desc "label"),
     RETURN resulttype?      hint(desc "result"),
-    REFS funcidx*
+    REFS funcidx*           hint(desc "references"),
+    ...
+  }
+
+syntax context/sem hint(macro "%" "C%") =
+  { ...,
+    RECS subtype*           hint(desc "recursive type")
   }
 
 var C : context

spectec/doc/example/output/NanoWasm.pdf

@@ -1704,6 +1704,8 @@ let () = render_args_fwd := render_args
 
 let merge_typ t1 t2 =
   match t1.it, t2.it with
+  | StrT (dots1, ids1, fields1, _), StrT (_, ids2, fields2, dots2) ->
+    StrT (dots1, ids1 @ strip_nl ids2, fields1 @ strip_nl fields2, dots2) $ t1.at
   | CaseT (dots1, ids1, cases1, _), CaseT (_, ids2, cases2, dots2) ->
     CaseT (dots1, ids1 @ strip_nl ids2, cases1 @ strip_nl cases2, dots2) $ t1.at
   | _, _ -> assert false

spectec/src/backend-latex/render.ml

@@ -640,6 +640,30 @@ let is_variant_typ = is_x_typ as_variant_typ
 let is_notation_typ = is_x_typ as_notation_typ
 let is_empty_notation_typ = is_x_typ as_empty_notation_typ
 
+let rec find_typfield atom = function
+  | [] -> None
+  | ((atom', _, _) as tf1)::tfs when atom'.it = atom.it -> Some (tf1, tfs)
+  | tf1::tfs ->
+    match find_typfield atom tfs with
+    | None -> None
+    | Some (tf, tfs') -> Some (tf, tf1::tfs')
+
+let rec find_expfield atom = function
+  | [] -> None
+  | ((atom', _) as ef1)::efs when atom'.it = atom.it -> Some (ef1, efs)
+  | ef1::efs ->
+    match find_expfield atom efs with
+    | None -> None
+    | Some (ef, efs') -> Some (ef, ef1::efs')
+
+let rec order_expfields efs = function
+  | [] -> []
+  | (atom, _, _)::tfs' ->
+    (* TODO(4, rossberg): make this not quadratic *)
+    match find_expfield atom efs with
+    | None -> assert false
+    | Some (ef1, efs') -> ef1 :: order_expfields efs' tfs'
+
 
 (* Type Equivalence and Shallow Numeric Subtyping *)
 
@@ -1469,26 +1493,32 @@ and elab_exp_list env (es : exp list) (xts : (id * Il.typ) list) at
     fail at "arity mismatch for expression list"
 
 and elab_expfields env tid (efs : expfield list) (tfs : Il.typfield list) (t0 : Il.typ) at
+  : Il.expfield list attempt =
+  let* efs = elab_expfields' env tid efs tfs t0 at in
+  Ok (order_expfields efs tfs)
+
+and elab_expfields' env tid (efs : expfield list) (tfs : Il.typfield list) (t0 : Il.typ) at
   : Il.expfield list attempt =
   Debug.(log_in_at "el.elab_expfields" at
     (fun _ -> fmt "{%s} : {%s} = %s" (list el_expfield efs) (list il_typfield tfs) (il_typ t0))
   );
   assert (valid_tid tid);
   match efs, tfs with
   | [], [] -> Ok []
-  | (atom1, e)::efs2, (atom2, (tF, _qs, prems), _)::tfs2 when atom1.it = atom2.it ->
-    let* e' = elab_exp env e tF in
-    let* efs2' = elab_expfields env tid efs2 tfs2 t0 at in
-    let e' = if prems = [] then e' else tup_exp' [e'] e.at in
-    Ok ((elab_atom atom1 tid, e') :: efs2')
-  | _, (atom, (tF, _qs, prems), _)::tfs2 ->
+  | [], (atom, (tF, _qs, prems), _)::tfs2 ->
     let atom' = string_of_atom atom in
     let* e1' = cast_empty ("omitted record field `" ^ atom' ^ "`") env tF at in
     let e' = if prems = [] then e1' else tup_exp' [e1'] at in
     let* efs2' = elab_expfields env tid efs tfs2 t0 at in
     Ok ((elab_atom atom tid, e') :: efs2')
-  | (atom, e)::_, [] ->
-    fail_atom e.at atom t0 "undefined or misplaced record field"
+  | (atom, e)::efs2, tfs ->
+    match find_typfield atom tfs with
+    | None -> fail_atom e.at atom t0 "undefined or misplaced record field"
+    | Some ((_, (tF, _qs, prems), _), tfs2) ->
+      let* e' = elab_exp env e tF in
+      let* efs2' = elab_expfields env tid efs2 tfs2 t0 at in
+      let e' = if prems = [] then e' else tup_exp' [e'] e.at in
+      Ok ((elab_atom atom tid, e') :: efs2')
 
 and elab_exp_iter env (es : exp list) (t1, iter) t at : Il.exp attempt =
   let* e' = elab_exp_iter' env es (t1, iter) t at in