From 5553153ac2537cb1e13123daf2b7e3a5c0a57964 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Tue, 1 Sep 2026 10:01:26 -0700 Subject: [PATCH] Require matching finality Rule out the nonsensical configurations in which finalities of descriptor and described types are mismatched. In these configurations, it would not be possible for the non-final type to have subtypes, so we might as well require it to be final. Closes #61. --- interpreter/valid/valid.ml | 12 +++-- proposals/custom-descriptors/Overview.md | 26 +++++++++ test/core/custom-descriptors/descriptors.wast | 53 ++++++++++++++----- 3 files changed, 74 insertions(+), 17 deletions(-) diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 50e0ca9ec..3cf4477f4 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -195,22 +195,26 @@ let check_desctype_sub (c : context) (dt : desctype) (dt' : desctype) x x' at = let check_descriptors (dts : deftype list) at = List.iter (fun dt -> let DefT ((RecT dts), x) = dt in - let SubT (_, _, DescT (ut1, ut2, _)) = Lib.List32.nth dts x in + let SubT (fin, _, DescT (ut1, ut2, _)) = Lib.List32.nth dts x in Option.iter (fun ut -> match ut with | Rec x' -> - let SubT (_, _, DescT (_, ut', _)) = Lib.List32.nth dts x' in + let SubT (fin', _, DescT (_, ut', _)) = Lib.List32.nth dts x' in require (ut' = Some (Rec x)) at "described type is not described by descriptor"; - require (x' < x) at "forward use of described type" + require (x' < x) at "forward use of described type"; + require (fin = fin') at + "descriptor and described types have mismatched finality" | _ -> error at "described type is outside rec group" ) ut1; Option.iter (fun ut -> match ut with | Rec x' -> - let SubT (_, _, DescT (ut', _, _)) = Lib.List32.nth dts x' in + let SubT (fin', _, DescT (ut', _, _)) = Lib.List32.nth dts x' in require (ut' = Some (Rec x)) at "type is not described by its descriptor"; + require (fin = fin') at + "descriptor and described types have mismatched finality" | _ -> error at "descriptor type is outside rec group" ) ut2 ) dts diff --git a/proposals/custom-descriptors/Overview.md b/proposals/custom-descriptors/Overview.md index 93b3f69e5..d79acfef1 100644 --- a/proposals/custom-descriptors/Overview.md +++ b/proposals/custom-descriptors/Overview.md @@ -124,6 +124,29 @@ This is the same strategy we use for ensuring supertype chains do not have cycle ) ``` +Descriptor and described types must also have matching finality, +i.e. both must be final or both must be open (non-final). +If a described type were final and its descriptor open, +the descriptor could never have any subtypes because those subtypes would have to describe +subtypes of the described type, which cannot exist. +Conversely, if a described type were open and its descriptor final, +the described type could never have any subtypes because those subtypes would have to have +descriptors that are subtypes of the descriptor, which cannot exist. + +```wasm +(rec + ;; Invalid: $a is final, but $b is open. + (type $a (sub final (descriptor $b) (struct))) + (type $b (sub (describes $a) (struct))) +) + +(rec + ;; Invalid: $x is open, but $y is final. + (type $x (sub (descriptor $y) (struct))) + (type $y (sub final (describes $x) (struct))) +) +``` + Just like any other struct types, struct types with `describes` or `descriptor` clauses support width and depth subtyping. However, the following new subtyping rules are introduced: @@ -142,6 +165,9 @@ However, the following new subtyping rules are introduced: - A declared supertype of a type without a `describes` clause must also not have a `describes` clause. + - A described type and its descriptor type must have matching finality, + i.e. both must be final or both must be open (non-final). + - With shared-everything-threads, a shared described type must have a shared descriptor type and vice versa, and an unshared described type must have an unshared descriptor type and vice versa. diff --git a/test/core/custom-descriptors/descriptors.wast b/test/core/custom-descriptors/descriptors.wast index 713049c67..9106429a7 100644 --- a/test/core/custom-descriptors/descriptors.wast +++ b/test/core/custom-descriptors/descriptors.wast @@ -32,17 +32,6 @@ ) ) -;; Descriptor and described types can have mismatched finality. -(module - (rec - (type $a (sub final (descriptor $b) (struct))) - (type $b (sub (describes $a) (struct))) - ) - (rec - (type $x (sub (descriptor $y) (struct))) - (type $y (sub final (describes $x) (struct))) - ) -) ;; Describes clause must precede descriptor clause. (assert_malformed @@ -231,6 +220,44 @@ "descriptor type must be a struct" ) +;; Descriptor and described types must have matching finality. +(assert_invalid + (module + (rec + (type $a (sub final (descriptor $b) (struct))) + (type $b (sub (describes $a) (struct))) + ) + ) + "descriptor and described types have mismatched finality" +) +(assert_invalid + (module + (rec + (type $x (sub (descriptor $y) (struct))) + (type $y (sub final (describes $x) (struct))) + ) + ) + "descriptor and described types have mismatched finality" +) +(assert_invalid + (module + (rec + (type $a (descriptor $b) (struct)) + (type $b (sub (describes $a) (struct))) + ) + ) + "descriptor and described types have mismatched finality" +) +(assert_invalid + (module + (rec + (type $x (sub (descriptor $y) (struct))) + (type $y (describes $x) (struct)) + ) + ) + "descriptor and described types have mismatched finality" +) + ;; Subtyping (module @@ -533,7 +560,7 @@ (rec (type $A (sub (struct (field i32)))) (type $B (sub $A (descriptor $B.desc) (struct (field i64)))) - (type $B.desc (describes $B) (struct)) + (type $B.desc (sub (describes $B) (struct))) ) ) "sub type 1 does not match super type 0" @@ -545,7 +572,7 @@ ) (rec (type $B (sub $A (descriptor $B.desc) (struct (field i64)))) - (type $B.desc (describes $B) (struct)) + (type $B.desc (sub (describes $B) (struct))) ) ) "sub type 1 does not match super type 0"