From 2a654fe6fb7e625eac2d81bd51290a0888172f7e Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Tue, 9 Jan 2024 13:24:49 +0000 Subject: [PATCH 1/8] docs: remove tierkreis extension from spec Closes #744 and mentions outside motivations --- specification/hugr.md | 58 ++++++------------------------------------- 1 file changed, 8 insertions(+), 50 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 2033aea2a..17123d87b 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -708,9 +708,8 @@ flowchart like a DFG-node. This contains a DSG, and (like a DFG node) has inputs matching the child DSG; but one output, of type `Sum(O,ErrorType)` where O is the outputs of the child DSG. - - There is also a higher-order `catch` operation in the Tierkreis - extension, taking a graph argument; and `run_circuit` will return the - same way. + - It is also possible to use a higher-order `catch` operation in an + extension, taking a graph argument. ### Operation Extensibility @@ -719,8 +718,7 @@ flowchart The goal here is to allow the use of operations and types in the representation that are user defined, or defined and used by extension -tooling. Here “extension tooling” can be our own, e.g. TKET2 or -Tierkreis. These operations cover various flavours: +tooling. These operations cover various flavours: - Instruction sets specific to a target. - Operations that are best expressed in some other format that can be @@ -1009,7 +1007,7 @@ There are three classes of type: ``AnyType`` $\supset$ ``CopyableType`` $\supset notion of equality between values. (While *some* notion of equality is defined on any type with a binary representation, that if the bits are equal then the value is, the converse is not necessarily true - values that are indistinguishable can have different bit representations.) -For example, a `float` type (defined in an extension) would be a ``CopyableType``, but not an ``EqType``. Also, Hugr "classes" loosely correspond to Tierkreis' notion of "constraints". +For example, a `float` type (defined in an extension) would be a ``CopyableType``, but not an ``EqType``. **Rows** The `#` is a *row* which is a sequence of zero or more types. Types in the row can optionally be given names in metadata i.e. this does not affect behaviour of the HUGR. @@ -1037,8 +1035,8 @@ Tuples and Sums are ``CopyableType`` (respectively, ``EqType``) if all their com The type of `Function` includes a set of extensions (that is, [Extensions](#extension-implementation)) which are required to execute the graph. Every node in the HUGR is annotated with the set of extensions required to produce its inputs, and the set of extensions required to execute the node; the union of these two must match the set of extensions on each successor node. -Keeping track of the extension requirements like this allows extension designers and backends -(like tierkreis) to control how/where a module is run. +Keeping track of the extension requirements like this allows extension designers +and backends to control how/where a module is run. Concretely, if a plugin writer adds an extension *X*, then some function from @@ -1047,8 +1045,8 @@ a plugin needs to provide a mechanism to convert the requirement before it can interface with other plugins which don’t know about *X*. -A Tierkreis runtime could be connected to workers which provide means of -running different extensions. By the same mechanism, Tierkreis can reason +A runtime could have access to means of +running different extensions. By the same mechanism, the runtime can reason about where to run different parts of the graph by inspecting their extension requirements. @@ -1716,46 +1714,6 @@ Conversions between integers and floats: | `convert_u` | `int` | `float64` | unsigned int to float | | `convert_s` | `int` | `float64` | signed int to float | -### Higher-order (Tierkreis) Extension - -In **some** contexts, notably the Tierkreis runtime, higher-order -operations allow graphs to be valid dataflow values, and be executed. -These operations allow this. - - - `CallIndirect`: Call a function indirectly. Like `Call`, but the - first input is a standard dataflow function type. This is essentially - `eval` in Tierkreis. - - `catch`: like `CallIndirect`, the first argument is of type - `Function[R]` and the rest of the arguments are of type `I`. - However the result is not `O` but `Sum(O,ErrorType)` - - `parallel`, `sequence`, `partial`? Note that these could be executed - in first order graphs as straightforward (albeit expensive) - manipulations of Graph `struct`s/protobufs\! - -$\displaystyle{\frac{\mathrm{body} : [R] \textbf{Function}[R]([R] \textrm{Var}(I), [R] \textrm{Sum}(\textrm{Var}(I), \textrm{Var}(O))) \quad v : [R] \textrm{Var}(I)}{\textrm{loop}(\mathrm{body}, v) : [R] \textrm{Var}(O)}}$ - -**loop** - In order to run the *body* graph, we need the extensions -R that the graph requires, so -calling the **loop** function requires those same extensions. Since the -result of the body is fed into the input of the graph, it needs to have -the same extension requirements on its inputs and outputs. We require -that *v* is lifted to have extension requirement -R so that it matches the type -of input to the next iterations of the loop. - -$\displaystyle{\frac{\Theta : [R] \textbf{Function}[R](\vec{X}, \vec{Y}) \quad \vec{x} : [R] \vec{X}}{\textbf{call\\_indirect}(\Theta, \vec{x}) : [R] \vec{Y}}}$ - -**CallIndirect** - This has the same feature as **loop**: running a -graph requires its extensions. - -$\displaystyle{\frac{}{\textbf{load\\_const} \langle \textbf{Function}[R](\vec{I}, \vec{O}) \rangle (\mathrm{name}) : [\emptyset] \textbf{Function}[R](\vec{I}, \vec{O})}}$ - -**load_const** - For operations which instantiate a graph (**load\_const** -and **Call**) the functions are given an extra parameter at graph -construction time which corresponds to the function type that they are -meant to instantiate. This type will be given by a typeless edge from -the graph in question to the operation, with the graph’s type added as -an edge weight. ## Glossary From c844a2dd8275cbf11df2b700071f5c0be38c780f Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Tue, 9 Jan 2024 13:27:28 +0000 Subject: [PATCH 2/8] docs: remove type specific constant nodes --- specification/hugr.md | 7 ------- 1 file changed, 7 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 17123d87b..a0a639e95 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1610,12 +1610,6 @@ either differs from or is not part of the [WebAssembly](https://webassembly.github.io/spec/core/exec/numerics.html) specification. -Const nodes: - -| Name | Inputs | Outputs | Meaning | -| ---------------------- | ------ | -------- | --------------------------------------------------------------------- | -| `iconst_u`( \* ) | none | `int` | const node producing unsigned value x (where 0 \<= x \< 2^N) | -| `iconst_s`( \* ) | none | `int` | const node producing signed value x (where -2^(N-1) \<= x \< 2^(N-1)) | Casts: @@ -1687,7 +1681,6 @@ except where stated. | Name | Inputs | Outputs | Meaning | | ----------------- | -------------------- | --------- | ------------------------------------------------------------------------ | -| `fconst`( \* ) | none | `float64` | const node producing a float | | `feq`( \* ) | `float64`, `float64` | `bool` | equality test (as WASM but with 0 and 1 interpreted as `bool`) | | `fne`( \* ) | `float64`, `float64` | `bool` | inequality test (as WASM but with 0 and 1 interpreted as `bool`) | | `flt`( \* ) | `float64`, `float64` | `bool` | "less than" (as WASM but with 0 and 1 interpreted as `bool`) | From 87933ab7a5af7c65823ab4fa87c55d35ab1831e2 Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Tue, 9 Jan 2024 13:32:10 +0000 Subject: [PATCH 3/8] docs: Clarify in spec that the `arithmetic` extension is a collection Closes #747 --- specification/hugr.md | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index a0a639e95..86fece3d1 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1576,10 +1576,11 @@ The following operations are defined: Note that an `and<0>` operation produces the constant value "true" and an `or<0>` operation produces the constant value "false". -### Arithmetic Extension +### Arithmetic Extensions -The Arithmetic Extension provides types and operations for integer and -floating-point operations. +Types and operations for integer and +floating-point operations are provided by a collection of extensions under the +namespace `arithmetic`. We largely adopt (a subset of) the definitions of [WebAssembly 2.0](https://webassembly.github.io/spec/core/index.html), @@ -1591,6 +1592,8 @@ A few additonal operations not included in WebAssembly are also specified, and there are some other small differences (highlighted below). +### `arithmetic.int.types` + The `int` type is parametrized by its width `N`, which is a positive integer. @@ -1610,6 +1613,9 @@ either differs from or is not part of the [WebAssembly](https://webassembly.github.io/spec/core/exec/numerics.html) specification. +### `arithmetic.int` + +This extension defines operations on the integer types. Casts: @@ -1671,9 +1677,15 @@ Other operations: | `irotl`( \* ) | `int`, `int` | `int` | rotate first input left by k bits where k is unsigned interpretation of second input (leftmost bits replace rightmost bits) | | `irotr`( \* ) | `int`, `int` | `int` | rotate first input right by k bits where k is unsigned interpretation of second input (rightmost bits replace leftmost bits) | + +### `arithmetic.float.types` + The `float64` type represents IEEE 754-2019 floating-point data of 64 bits. + +### `arithmetic.float` + Floating-point operations are defined as follows. All operations below follow [WebAssembly](https://webassembly.github.io/spec/core/exec/numerics.html#floating-point-operations) @@ -1698,6 +1710,9 @@ except where stated. | `ffloor` | `float64` | `float64` | floor | | `fceil` | `float64` | `float64` | ceiling | +### `arithmetic.conversions` + + Conversions between integers and floats: | Name | Inputs | Outputs | Meaning | From 9b0a46b529d122b8cc482a238e59a2755446e81b Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Tue, 9 Jan 2024 13:40:40 +0000 Subject: [PATCH 4/8] docs: Mention prelude in core spec Closes #737 --- specification/hugr.md | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 86fece3d1..16e79b082 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1555,8 +1555,29 @@ implementation of this design document is available on GitHub. ## Standard Library -`panic`: panics unconditionally; no inputs, any type of outputs (these -are never produced) +A collection of extensions form the "standard library" for HUGR, and are defined +in this repository. + +### Prelude + +The prelude extension is assumed to be valid and available in all contexts, and +so must be supported by all third-party tooling. + +#### Types + +`usize`: a positive integer size type. + +`array`: a known-size (N) array of type T. + +`qubit`: a linear (non-copyable) qubit type. + +`error`: error type. See [`ErrorType`](#errortype). + +### Operations +| Name | Inputs | Outputs | Meaning | +|--------------------------------|-----------|----------------------------|-----------------------------------------------------------------| +| `new_array` | `T` x N | `array` | Create an array from all the inputs | +| `panic` | ErrorType | - | Immediately end execution and pass contents of error to context | ### Logic Extension From 0a37d5905c14ff271af09bc33c230c66846e09f4 Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Tue, 9 Jan 2024 14:14:02 +0000 Subject: [PATCH 5/8] docs: simplify errortype description --- specification/hugr.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 16e79b082..f5c045893 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -698,9 +698,7 @@ flowchart #### `ErrorType` - - There is some type of errors, perhaps just a string, or - `Tuple(USize,String)` with some errorcode, that is returned along with - the fact that the graph/program panicked. + - A type which operations can use to indicate an error occurred. #### Catch From ed6454d725e8744a318c61688a73cc42b7c26a34 Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Tue, 9 Jan 2024 14:25:42 +0000 Subject: [PATCH 6/8] spec: add panic to prelude --- specification/hugr.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index f5c045893..8f905667d 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1572,10 +1572,10 @@ so must be supported by all third-party tooling. `error`: error type. See [`ErrorType`](#errortype). ### Operations -| Name | Inputs | Outputs | Meaning | -|--------------------------------|-----------|----------------------------|-----------------------------------------------------------------| +| Name | Inputs | Outputs | Meaning | +|-------------------|-----------|---------------|-----------------------------------------------------------------| | `new_array` | `T` x N | `array` | Create an array from all the inputs | -| `panic` | ErrorType | - | Immediately end execution and pass contents of error to context | +| `panic` | ErrorType | - | Immediately end execution and pass contents of error to context | ### Logic Extension From cad288a86b64892d256070770e34968c3ee78db4 Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Tue, 9 Jan 2024 17:16:35 +0000 Subject: [PATCH 7/8] fix indentation Co-authored-by: Alan Lawrence --- specification/hugr.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 8f905667d..20c89afbc 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1611,7 +1611,7 @@ A few additonal operations not included in WebAssembly are also specified, and there are some other small differences (highlighted below). -### `arithmetic.int.types` +#### `arithmetic.int.types` The `int` type is parametrized by its width `N`, which is a positive integer. @@ -1632,7 +1632,7 @@ either differs from or is not part of the [WebAssembly](https://webassembly.github.io/spec/core/exec/numerics.html) specification. -### `arithmetic.int` +#### `arithmetic.int` This extension defines operations on the integer types. @@ -1697,13 +1697,13 @@ Other operations: | `irotr`( \* ) | `int`, `int` | `int` | rotate first input right by k bits where k is unsigned interpretation of second input (rightmost bits replace leftmost bits) | -### `arithmetic.float.types` +#### `arithmetic.float.types` The `float64` type represents IEEE 754-2019 floating-point data of 64 bits. -### `arithmetic.float` +#### `arithmetic.float` Floating-point operations are defined as follows. All operations below follow @@ -1729,7 +1729,7 @@ except where stated. | `ffloor` | `float64` | `float64` | floor | | `fceil` | `float64` | `float64` | ceiling | -### `arithmetic.conversions` +#### `arithmetic.conversions` Conversions between integers and floats: From 2b1b5c00b22126af674e293c413a36d112ce7429 Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Tue, 9 Jan 2024 17:19:06 +0000 Subject: [PATCH 8/8] suggestions from code review --- specification/hugr.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 20c89afbc..feec4fa7e 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -705,8 +705,8 @@ flowchart - At some point we expect to add a first-order `catch` node, somewhat like a DFG-node. This contains a DSG, and (like a DFG node) has inputs matching the child DSG; but one output, of type - `Sum(O,ErrorType)` where O is the outputs of the child DSG. - - It is also possible to use a higher-order `catch` operation in an + `Sum(Tuple(#O),ErrorType)` where O is the outputs of the child DSG. + - It is also possible to define a higher-order `catch` operation in an extension, taking a graph argument. @@ -901,7 +901,7 @@ extensions: extensions: r # Indicates that running this operation also invokes extensions r lowering: file: "graph_op_hugr.bin" - extensions: ["arithmetic", r] # r is the ExtensionSet in "params" + extensions: ["arithmetic.int", r] # r is the ExtensionSet in "params" ``` The declaration of the `params` uses a language that is a distinct, simplified @@ -1034,7 +1034,7 @@ Tuples and Sums are ``CopyableType`` (respectively, ``EqType``) if all their com The type of `Function` includes a set of extensions (that is, [Extensions](#extension-implementation)) which are required to execute the graph. Every node in the HUGR is annotated with the set of extensions required to produce its inputs, and the set of extensions required to execute the node; the union of these two must match the set of extensions on each successor node. Keeping track of the extension requirements like this allows extension designers -and backends to control how/where a module is run. +and third-party tooling to control how/where a module is run. Concretely, if a plugin writer adds an extension *X*, then some function from