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,61 @@ 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
+val(f64)                   ::= v:<core:f64>                    => v
+val(char)                  ::= v:<core:u32>                    => v
+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)) (if 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
+
 ## Name Section
 
 Like the core wasm [name
@@ -376,7 +434,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

design/mvp/Explainer.md

@@ -23,7 +23,8 @@ JavaScript runtimes. For a more user-focussed 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 ')'
 ```
@@ -1341,22 +1345,102 @@ 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>
+        | '<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>)
+```
+
+Where `val` definition must match the `valtype` specified.
+
+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:
@@ -1366,6 +1450,34 @@ 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:
+```wasm
+(value $default_url string "https://example.com")
+(export "default-url" (value $default_url))
+```
+
+`default-url` value export will infer `(eq $default_url)` value bound in the component type.
+
+Include a type ascription to explicitly set type to `string`:
+
+```
+(value $default_url string "https://example.com")
+(export "default-url" (value $default_url) (value string))
+```
+
+### 🪙 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
@@ -1927,6 +2039,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