formalize component value definitions

Signed-off-by: Roman Volosatovs <rvolosatovs@riseup.net>

Author: rvolosatovs

design/mvp/Binary.md

@@ -36,6 +36,7 @@ section   ::=    section_0(<core:custom>)         => ϵ
             | s: section_9(<start>)               => [s]
             | i*:section_10(vec(<import>))        => i*
             | e*:section_11(vec(<export>))        => e*
+            | v*:section_12(vec(<value>))         => v* 🪙
 ```
 Notes:
 * Reused Core binary rules: [`core:section`], [`core:custom`], [`core:module`]
@@ -215,12 +216,14 @@ importdecl    ::= in:<importname'> ed:<externdesc>        => (import in ed)
 exportdecl    ::= en:<exportname'> ed:<externdesc>        => (export en ed)
 externdesc    ::= 0x00 0x11 i:<core:typeidx>              => (core module (type i))
                 | 0x01 i:<typeidx>                        => (func (type i))
-                | 0x02 t:<valtype>                        => (value t) 🪙
+                | 0x02 b:<valuebound>                     => (value b) 🪙
                 | 0x03 b:<typebound>                      => (type b)
                 | 0x04 i:<typeidx>                        => (component (type i))
                 | 0x05 i:<typeidx>                        => (instance (type i))
 typebound     ::= 0x00 i:<typeidx>                        => (eq i)
                 | 0x01                                    => (sub resource)
+valuebound    ::= 0x00 i:<valueidx>                       => (eq i) 🪙
+                | 0x01 t:<valtype>                        => t 🪙
 ```
 Notes:
 * The type opcodes follow the same negative-SLEB128 scheme as Core WebAssembly,
@@ -347,6 +350,64 @@ Notes:
 * `<integrity-metadata>` is as defined by the
   [SRI](https://www.w3.org/TR/SRI/#dfn-integrity-metadata) spec.
 
+## 🪙 Value Definitions
+
+(See [Value Definitions](Explainer.md#value-definitions) in the explainer.)
+
+```ebnf
+value                      ::= t:<valtype> v:<val(t)>                  => (value t v)
+val(bool)                  ::= 0x00                                    => false
+                             | 0x01                                    => true
+val(u8)                    ::= v:<core:u8>                             => v
+val(s8)                    ::= v:<core:s8>                             => v
+val(s16)                   ::= v:<core:s16>                            => v
+val(u16)                   ::= v:<core:u16>                            => v
+val(s32)                   ::= v:<core:s32>                            => v
+val(u32)                   ::= v:<core:u32>                            => v
+val(s64)                   ::= v:<core:s64>                            => v
+val(u64)                   ::= v:<core:u64>                            => v
+val(f32)                   ::= v:<core:f32>                            => v (if !isnan(v))
+                             | 0x00 0x00 0xC0 0x7F                     => nan
+val(f64)                   ::= v:<core:f64>                            => v (if !isnan(v))
+                             | 0x00 0x00 0x00 0x00 0x00 0x00 0xF8 0x7F => nan
+val(char)                  ::= v:<core:u32>                            => v (if v < 0xD800 or 0xE000 <= v <= 0x10FFFF)
+val(string)                ::= v:<core:name>                           => v
+val(i:<typeidx>)           ::= v:<val(type-index-space[i])>            => v
+val((record (field l t)+)) ::= v+:<val(t)>+                            => (record v+)
+val((variant (case l t?)+) ::= i:<core:u32> v?:<val(t[i])>?            => (variant l[i] v?)
+val((list t))              ::= v:vec(<val(t)>)                         => (list v)
+val((tuple t+))            ::= v+:<val(t)>+                            => (tuple v+)
+val((flags l+))            ::= v:<core:uN>                             => (flags (l[i] for i in 0..N-1 if v & 2^i > 0)) (where N = |l+|)
+val((enum l+))             ::= i:<core:u32>                            => (enum l[i])
+val((option t))            ::= 0x00                                    => none
+                             | 0x01 v:<val(t)>                         => (some v)
+val((result))              ::= 0x00                                    => ok
+                             | 0x01                                    => error
+val((result t))            ::= 0x00 v:<val(t)>                         => (ok v)
+                             | 0x01                                    => error
+val((result (error u)))    ::= 0x00                                    => ok
+                             | 0x01 v:<val(u)>                         => (error v)
+val((result t (error u)))  ::= 0x00 v:<val(t)>                         => (ok v)
+                             | 0x01 v:<val(u)>                         => (error v)
+```
+
+Notes:
+* Reused Core binary rules:
+    - [`core:name`]
+    - [`core:s8`]
+    - [`core:s16`]
+    - [`core:s32`]
+    - [`core:s64`]
+    - [`core:u8`]
+    - [`core:u16`]
+    - [`core:u32`]
+    - [`core:u64`]
+    - [`core:uN`]
+    - [`core:f32`]
+    - [`core:f64`]
+* `&` operator is used to denote bitwise AND operation, which performs AND on every bit of two numbers in their binary form
+* `isnan` is a function, which takes a floating point number as a parameter and returns `true` iff it represents a NaN as defined in [IEEE 754 standard]
+
 ## Name Section
 
 Like the core wasm [name
@@ -376,7 +437,17 @@ appear once within a `name` section, for example component instances can only be
 named once.
 
 
+[`core:s8`]: https://webassembly.github.io/spec/core/binary/values.html#integers
+[`core:u8`]: https://webassembly.github.io/spec/core/binary/values.html#integers
+[`core:s16`]: https://webassembly.github.io/spec/core/binary/values.html#integers
+[`core:u16`]: https://webassembly.github.io/spec/core/binary/values.html#integers
+[`core:s32`]: https://webassembly.github.io/spec/core/binary/values.html#integers
 [`core:u32`]: https://webassembly.github.io/spec/core/binary/values.html#integers
+[`core:s64`]: https://webassembly.github.io/spec/core/binary/values.html#integers
+[`core:u64`]: https://webassembly.github.io/spec/core/binary/values.html#integers
+[`core:uN`]: https://webassembly.github.io/spec/core/binary/values.html#integers
+[`core:f32`]: https://webassembly.github.io/spec/core/binary/values.html#floating-point
+[`core:f64`]: https://webassembly.github.io/spec/core/binary/values.html#floating-point
 [`core:section`]: https://webassembly.github.io/spec/core/binary/modules.html#binary-section
 [`core:custom`]: https://webassembly.github.io/spec/core/binary/modules.html#custom-section
 [`core:module`]: https://webassembly.github.io/spec/core/binary/modules.html#binary-module
@@ -388,3 +459,5 @@ named once.
 
 [type-imports]: https://github.com/WebAssembly/proposal-type-imports/blob/master/proposals/type-imports/Overview.md
 [module-linking]: https://github.com/WebAssembly/module-linking/blob/main/proposals/module-linking/Explainer.md
+
+[IEEE 754 standard]: https://ieeexplore.ieee.org/document/8766229

design/mvp/Explainer.md

@@ -23,7 +23,8 @@ JavaScript runtimes. For a more user-focused explanation, take a look at the
   * [Canonical definitions](#canonical-definitions)
     * [Canonical ABI](#canonical-built-ins)
     * [Canonical built-ins](#canonical-built-ins)
-  * [Start definitions](#-start-definitions)
+  * [Value definitions](#value-definitions)
+  * [Start definitions](#start-definitions)
   * [Import and export definitions](#import-and-export-definitions)
 * [Component invariants](#component-invariants)
 * [JavaScript embedding](#JavaScript-embedding)
@@ -87,6 +88,7 @@ definition ::= core-prefix(<core:module>)
              | <start> 🪺
              | <import>
              | <export>
+             | <value> 🪙
 
 where core-prefix(X) parses '(' 'core' Y ')' when X parses '(' Y ')'
 ```
@@ -296,7 +298,7 @@ contain any valid UTF-8 string).
 
 🪙 The `value` sort refers to a value that is provided and consumed during
 instantiation. How this works is described in the
-[start definitions](#start-definitions) section.
+[value definitions](#value-definitions) section.
 
 To see a non-trivial example of component instantiation, we'll first need to
 introduce a few other definitions below that allow components to import, define
@@ -564,10 +566,12 @@ externdesc    ::= (<sort> (type <u32>) )
                 | <functype>
                 | <componenttype>
                 | <instancetype>
-                | (value <valtype>) 🪙
+                | (value <valuebound>) 🪙
                 | (type <typebound>)
 typebound     ::= (eq <typeidx>)
                 | (sub resource)
+valuebound    ::= (eq <valueidx>) 🪙
+                | <valtype> 🪙
 
 where bind-id(X) parses '(' sort <id>? Y ')' when X parses '(' sort Y ')'
 ```
@@ -733,7 +737,7 @@ definitions.
 
 🪙 The `value` case of `externdesc` describes a runtime value that is imported or
 exported at instantiation time as described in the
-[start definitions](#start-definitions) section below.
+[value definitions](#value-definitions) section below.
 
 The `type` case of `externdesc` describes an imported or exported type along
 with its "bound":
@@ -1348,22 +1352,100 @@ number of threads that can be expected to execute concurrently.
 See the [CanonicalABI.md](CanonicalABI.md#canonical-definitions) for detailed
 definitions of each of these built-ins and their interactions.
 
+### 🪙 Value Definitions
 
-### 🪙 Start Definitions
+Value definitions (in the value index space) are like immutable `global` definitions
+in Core WebAssembly except that validation requires them to be consumed exactly
+once at instantiation-time (i.e., they are [linear]).
+
+Components may define values in the value index space using following syntax:
 
-Like modules, components can have start functions that are called during
-instantiation. Unlike modules, components can call start functions at multiple
-points during instantiation with each such call having parameters and results.
-Thus, `start` definitions in components look like function calls:
 ```ebnf
-start ::= (start <funcidx> (value <valueidx>)* (result (value <id>?))*)
+value ::= (value <id>? <valtype> <val>)
+val   ::= false | true
+        | <core:i64>
+        | <core:f64> | NaN
+        | '<core:char>'
+        | <core:name>
+        | (record <val>+)
+        | (variant "<label>" <val>?)
+        | (list <val>*)
+        | (tuple <val>+)
+        | (flags "<label>"*)
+        | (enum "<label>")
+        | none | (some <val>)
+        | ok | (ok <val>) | error | (error <val>)
+```
+
+The validation rules for `value` require the `val` to match the `valtype`.  For example:
+```wasm
+(component
+  (value $a bool true)
+  (value $b u8 1)
+  (value $c u16 2)
+  (value $d u32 3)
+  (value $e u64 4)
+  (value $f u8 5)
+  (value $g u16 6)
+  (value $h u32 7)
+  (value $i u64 8)
+  (value $j f32 9.1)
+  (value $k f64 9.2)
+  (value $l char 'a')
+  (value $m string "hello")
+  (value $n (record (field "a" bool) (field "b" u8)) (record true 1))
+  (value $o (variant (case "a" bool) (case "b" u8)) (variant "b" 1))
+  (value $p (list (result (option u8)))
+    (list
+      error
+      (ok (some 1))
+      (ok none)
+      error
+      (ok (some 2))
+    )
+  )
+  (value $q (tuple u8 u16 u32) (tuple 1 2 3))
+
+  (type $abc (flags "a" "b" "c"))
+  (value $r $abc (flags "a" "c"))
+
+  (value $s (enum "a" "b" "c") (enum "b"))
+
+  (type $complex
+    (tuple
+      (record
+        (field "a" (option string))
+        (field "b" (tuple (option u8) string))
+      )
+      (list char)
+      $abc
+      string
+    )
+  )
+  (value $complex1 (type $complex)
+    (tuple
+      (record
+        none
+        (tuple none "empty")
+      )
+      (list)
+      (flags)
+      ""
+    )
+  )
+  (value $complex2 (type $complex)
+    (tuple
+      (record
+        (some "example")
+        (tuple (some 42) "hello")
+      )
+      (list 'a' 'b' 'c')
+      (flags "b" "a")
+      "hi"
+    )
+  )
+)
 ```
-The `(value <valueidx>)*` list specifies the arguments passed to `funcidx` by
-indexing into the *value index space*. Value definitions (in the value index
-space) are like immutable `global` definitions in Core WebAssembly except that
-validation requires them to be consumed exactly once at instantiation-time
-(i.e., they are [linear]). The arity and types of the two value lists are
-validated to match the signature of `funcidx`.
 
 As with all definition sorts, values may be imported and exported by
 components. As an example value import:
@@ -1373,6 +1455,45 @@ components. As an example value import:
 As this example suggests, value imports can serve as generalized [environment
 variables], allowing not just `string`, but the full range of `valtype`.
 
+Values can also be exported.  For example:
+```wasm
+(component
+  (import "system-port" (value $port u16))
+  (value $url string "https://example.com")
+  (export "default-url" (value $url))
+  (export "default-port" (value $port))
+)
+```
+The inferred type of this component is:
+```wasm
+(component
+  (import "system-port" (value $port u16))
+  (value $url string "https://example.com")
+  (export "default-url" (value (eq $url)))
+  (export "default-port" (value (eq $port)))
+)
+```
+Thus, by default, the precise constant or import being exported is propagated
+into the component's type and thus its public interface.  In this way, value exports
+can act as semantic configuration data provided by the component to the host
+or other client tooling.
+Components can also keep the exact value being exported abstract (so that the
+precise value is not part of the type and public interface) using the "type ascription"
+feature mentioned in the [imports and exports](#import-and-export-definitions) section below.
+
+### 🪙 Start Definitions
+
+Like modules, components can have start functions that are called during
+instantiation. Unlike modules, components can call start functions at multiple
+points during instantiation with each such call having parameters and results.
+Thus, `start` definitions in components look like function calls:
+```ebnf
+start ::= (start <funcidx> (value <valueidx>)* (result (value <id>?))*)
+```
+The `(value <valueidx>)*` list specifies the arguments passed to `funcidx` by
+indexing into the *value index space*. The arity and types of the two value lists are
+validated to match the signature of `funcidx`.
+
 With this, we can define a component that imports a string and computes a new
 exported string at instantiation time:
 ```wasm
@@ -1650,6 +1771,25 @@ the standard [avoidance problem] that appears in module systems with abstract
 types. In particular, it ensures that a client of a component is able to
 externally define a type compatible with the exports of the component.
 
+Similar to type exports, value exports may also ascribe a type to keep the precise
+value from becoming part of the type and public interface.
+
+For example:
+```wasm
+(component
+  (value $url string "https://example.com")
+  (export "default-url" (value $url) (value string))
+)
+```
+
+The inferred type of this component is:
+```wasm
+(component
+  (export "default-url" (value string))
+)
+```
+
+Note, that the `url` value definition is absent from the component type
 
 ## Component Invariants
 
@@ -1934,6 +2074,9 @@ and will be added over the coming months to complete the MVP proposal:
 [Index Space]: https://webassembly.github.io/spec/core/syntax/modules.html#indices
 [Abbreviations]: https://webassembly.github.io/spec/core/text/conventions.html#abbreviations
 
+[`core:i64`]: https://webassembly.github.io/spec/core/syntax/values.html#integers
+[`core:f64`]: https://webassembly.github.io/spec/core/syntax/values.html#floating-point
+[`core:char`]: https://webassembly.github.io/spec/core/syntax/values.html#syntax-name
 [`core:name`]: https://webassembly.github.io/spec/core/syntax/values.html#syntax-name
 [`core:module`]: https://webassembly.github.io/spec/core/text/modules.html#text-module
 [`core:type`]: https://webassembly.github.io/spec/core/text/modules.html#types