From 4400af71623c6906243c26bb78cc1a53b69a4fe1 Mon Sep 17 00:00:00 2001 From: Roman Volosatovs Date: Wed, 10 Apr 2024 15:31:28 +0200 Subject: [PATCH 01/24] formalize component value definitions Signed-off-by: Roman Volosatovs --- design/mvp/Binary.md | 75 ++++++++++++++++- design/mvp/Explainer.md | 175 ++++++++++++++++++++++++++++++++++++---- 2 files changed, 233 insertions(+), 17 deletions(-) diff --git a/design/mvp/Binary.md b/design/mvp/Binary.md index 550b9c43..750cb1b3 100644 --- a/design/mvp/Binary.md +++ b/design/mvp/Binary.md @@ -36,6 +36,7 @@ section ::= section_0() => ϵ | s: section_9() => [s] | i*:section_10(vec()) => i* | e*:section_11(vec()) => e* + | v*:section_12(vec()) => v* 🪙 ``` Notes: * Reused Core binary rules: [`core:section`], [`core:custom`], [`core:module`] @@ -218,12 +219,14 @@ importdecl ::= in: ed: => (import in ed) exportdecl ::= en: ed: => (export en ed) externdesc ::= 0x00 0x11 i: => (core module (type i)) | 0x01 i: => (func (type i)) - | 0x02 t: => (value t) 🪙 + | 0x02 b: => (value b) 🪙 | 0x03 b: => (type b) | 0x04 i: => (component (type i)) | 0x05 i: => (instance (type i)) typebound ::= 0x00 i: => (eq i) | 0x01 => (sub resource) +valuebound ::= 0x00 i: => (eq i) 🪙 + | 0x01 t: => t 🪙 ``` Notes: * The type opcodes follow the same negative-SLEB128 scheme as Core WebAssembly, @@ -350,6 +353,64 @@ Notes: * `` 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: v: => (value t v) +val(bool) ::= 0x00 => false + | 0x01 => true +val(u8) ::= v: => v +val(s8) ::= v: => v +val(s16) ::= v: => v +val(u16) ::= v: => v +val(s32) ::= v: => v +val(u32) ::= v: => v +val(s64) ::= v: => v +val(u64) ::= v: => v +val(f32) ::= v: => v (if !isnan(v)) + | 0x00 0x00 0xC0 0x7F => nan +val(f64) ::= v: => v (if !isnan(v)) + | 0x00 0x00 0x00 0x00 0x00 0x00 0xF8 0x7F => nan +val(char) ::= v: => v (if v < 0xD800 or 0xE000 <= v <= 0x10FFFF) +val(string) ::= v: => v +val(i:) ::= v: => v +val((record (field l t)+)) ::= v+:+ => (record v+) +val((variant (case l t?)+) ::= i: v?:? => (variant l[i] v?) +val((list t)) ::= v:vec() => (list v) +val((tuple t+)) ::= v+:+ => (tuple v+) +val((flags l+)) ::= v: => (flags (l[i] for i in 0..N-1 if v & 2^i > 0)) (where N = |l+|) +val((enum l+)) ::= i: => (enum l[i]) +val((option t)) ::= 0x00 => none + | 0x01 v: => (some v) +val((result)) ::= 0x00 => ok + | 0x01 => error +val((result t)) ::= 0x00 v: => (ok v) + | 0x01 => error +val((result (error u))) ::= 0x00 => ok + | 0x01 v: => (error v) +val((result t (error u))) ::= 0x00 v: => (ok v) + | 0x01 v: => (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 @@ -379,7 +440,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 @@ -391,3 +462,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 diff --git a/design/mvp/Explainer.md b/design/mvp/Explainer.md index d7b6f2a6..bf47dbce 100644 --- a/design/mvp/Explainer.md +++ b/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() | 🪺 | | + | 🪙 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 @@ -568,10 +570,12 @@ externdesc ::= ( (type ) ) | | | - | (value ) 🪙 + | (value ) 🪙 | (type ) typebound ::= (eq ) | (sub resource) +valuebound ::= (eq ) 🪙 + | 🪙 where bind-id(X) parses '(' sort ? Y ')' when X parses '(' sort Y ')' ``` @@ -737,7 +741,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": @@ -1355,22 +1359,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 (value )* (result (value ?))*) +value ::= (value ? ) +val ::= false | true + | + | | NaN + | '' + | + | (record +) + | (variant "