formalize component value definitions

Signed-off-by: Roman Volosatovs <[email protected]>

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`]
@@ -346,6 +347,57 @@ 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:<defval(t)>                 => v (if (type t) = type-index-space[i])
+defval((record lt+))                      ::= (v:<fieldval(f:lt)>)^n        => v^n (if |lt*| > 0 and n = |lt*|)
+defval((variant case*))                   ::= i:<core:u32> v:caseval(c)     => i v (if i < |case*| and c = case[i])
+defval((list t))                          ::= vec(<val(t)>)
+defval((tuple t+))                        ::= (v:<val(e:t)>)^n              => v^n (if |t*| > 0 and n = |t*|)
+defval((flags l+))                        ::= v:<core:u32>                  => v (if |l*| > 0 and v < 2^|l*|)
+defval((enum l*))                         ::= i:<core:u32>                  => i v (if i < |l*|)
+defval((option t))                        ::= 0x00                          => none
+                                            | 0x01 v:<val(t)>               => (some v)
+defval((result t? (error u)?))            ::= 0x00                          => ok
+                                            | 0x00 v:<val(t)>               => (ok v)
+                                            | 0x01                          => error
+                                            | 0x01 v:<val(u)>               => (error v)
+fieldval((field l t))                     ::= v:<val(t)>                    => v
+caseval((case l t?))                      ::= v?:<val(t)>?                  => 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:f32`]
+    - [`core:f64`]
+
 ## Name Section
 
 Like the core wasm [name
@@ -375,7 +427,16 @@ 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: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

@@ -25,6 +25,7 @@ JavaScript runtimes. For a more user-focussed explanation, take a look at the
     * [Canonical built-ins](#canonical-built-ins)
   * [Start definitions](#-start-definitions)
   * [Import and export definitions](#import-and-export-definitions)
+  * [Value definitions](#value-definitions)
 * [Component invariants](#component-invariants)
 * [JavaScript embedding](#JavaScript-embedding)
   * [JS API](#JS-API)
@@ -87,6 +88,7 @@ definition ::= core-prefix(<core:module>)
              | <start> 🪺
              | <import>
              | <export>
+             | <value>
 
 where core-prefix(X) parses '(' 'core' Y ')' when X parses '(' Y ')'
 ```
@@ -1633,7 +1635,12 @@ 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.
 
+### 🪙 Value Definitions
 
+Components may define values in the value index
+```ebnf
+value ::= t:<valtype> v:<val(t)> => (value t v)
+```
 ## Component Invariants
 
 As a consequence of the shared-nothing design described above, all calls into