Copy Views

Most regular values can be passed around and manipulated with no restriction whatsoever. Those types are automatically marked with the Copy trait. However, in the presence of inverted wires, Spade must impose certain restrictions to ensure all inverted wires are set exactly once.

This means that any inverted type inv T, as well as any compound type or collection containing an inverted type, does not implement the Copy trait and needs to be forcibly consumed exactly once by setting all inverted values in it or passing it to a function, method or type constructor.

However, this restriction makes certain patterns impossible to implement. Functions cannot operate on non-Copy values without consuming them, even if they don’t intend to set any wires. Same goes for data types. This situation arises often when dealing with compound types when trying to implement helper functions:

struct ReadPort {
    request: Option<uint<10>Type used to represent unsigned integers. The generic parameter (<N>) specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.ies the number of bits>,
    response: inv Option<uint<8>Type used to represent unsigned integers. The generic parameter (<N>) specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.ies the number of bits>,
}

fnFunctions together with entityEntities together with fn and pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. are the basic building blocks of Spade circuits. Unlike fn, entity can contain registers and therefore have state and unlike pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline., they do not have a statically known latency or pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. structure. and pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. are the basic building blocks of Spade circuits. Unlike entities and pipelines, functions have no internal state, they are combinational (pure). is_requesting(p: ReadPort) -> boolType used to represent 1-bit values {
    p.request.is_some()
}

fnFunctions together with entityEntities together with fn and pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. are the basic building blocks of Spade circuits. Unlike fn, entity can contain registers and therefore have state and unlike pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline., they do not have a statically known latency or pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. structure. and pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. are the basic building blocks of Spade circuits. Unlike entities and pipelines, functions have no internal state, they are combinational (pure). main(p: ReadPort) {
    letlet is used to define a variable. Spade infers the type of most variables from context, but you can also specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.y the type with : <type> before the =. value = ifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it. is_requesting(p) {
        Some(10)
    } else {
        None
    };

    set p.response = value;
}

This code looks sensible: is_requesting is used to probe the state of p to decide how to respond. However, this code cannot work in Spade, the following errors are emitted by the compiler:

error: swim_blinky::p.response is unused
  ┌─ src/main.spade:6:18
  │
6 │ fn is_requesting(p: ReadPort) -> bool {
  │                  ^ swim_blinky::p.response is unused
  │
  = note: swim_blinky::p.response is an inverted wire (`inv`) which must be set

error: Use of consumed resource
   ┌─ src/main.spade:17:9
   │
11 │     let value = if is_requesting(p) {
   │                                  - Previously used here
   ·
17 │     set p.response = value;
   │         ^^^^^^^^^^ Use of consumed resource

These errors are the two sides of the same coin-shaped problem: ReadPort contains inv wires, so it does not implement Copy. Non-Copy types need to be consumed exactly once and passing non-Copy values as parameters to a function, method or type constructor consumes it. All those factors together explain both errors:

Inside is_requesting, p is a non-Copy value with parts which must be consumed once. However, the method is only reading information from it, never setting any wires nor calling any function which consumes anything. The error indicates which part remains to be consumed: the response field.
Inside main, p is also a non-Copy value with parts which must be consumed once, but now the problem is that it is consumed twice: once when passed to is_requesting, and another when setting p.response.

A function like is_requesting above, one which does not set any inverted wires, doesn’t need to consume self. In fact, if it’s forced to do so, the function becomes useless, as it will prevent using the value properly while failing to compile because it doesn’t set any inverted wires itself. Fortunately, Spade offers a mechanism to deal with cases like this in the form of copy views.

How To Use Copy Views

Using the & operator on a value creates a copy view of it. The data inside a copy view cannot be accessed directly, so * is required to extract the original value from the copy view.

However, when * is applied to a value of type &T, it requires T to implement the Copy trait. This feature ensures only Copy values can be obtained from a copy view, so &T itself is marked as Copy too, letting copy views be passed around freely.

fnFunctions together with entityEntities together with fn and pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. are the basic building blocks of Spade circuits. Unlike fn, entity can contain registers and therefore have state and unlike pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline., they do not have a statically known latency or pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. structure. and pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. are the basic building blocks of Spade circuits. Unlike entities and pipelines, functions have no internal state, they are combinational (pure). main() {
    letlet is used to define a variable. Spade infers the type of most variables from context, but you can also specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.y the type with : <type> before the =. a: uint<8>Type used to represent unsigned integers. The generic parameter (<N>) specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.ies the number of bits = 0u8;
    letlet is used to define a variable. Spade infers the type of most variables from context, but you can also specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.y the type with : <type> before the =. b: &uint<8>Type used to represent unsigned integers. The generic parameter (<N>) specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.ies the number of bits = &a;
    letlet is used to define a variable. Spade infers the type of most variables from context, but you can also specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.y the type with : <type> before the =. c: uint<8>Type used to represent unsigned integers. The generic parameter (<N>) specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.ies the number of bits = *b;

    letlet is used to define a variable. Spade infers the type of most variables from context, but you can also specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.y the type with : <type> before the =. x: inv boolType used to represent 1-bit values = port().1;
    letlet is used to define a variable. Spade infers the type of most variables from context, but you can also specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.y the type with : <type> before the =. y: &inv boolType used to represent 1-bit values = &x;
    letlet is used to define a variable. Spade infers the type of most variables from context, but you can also specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.y the type with : <type> before the =. z: inv boolType used to represent 1-bit values = *x; // error: `inv boolType used to represent 1-bit values` does not implement `Copy`

    // `&` did not consume `x`, so it must still be set
    set x = false;

    // `y` can be passed around many times
    do_something_with_copy_view(y);
    do_something_with_copy_view(y);
    do_something_with_copy_view(y);
}

fnFunctions together with entityEntities together with fn and pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. are the basic building blocks of Spade circuits. Unlike fn, entity can contain registers and therefore have state and unlike pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline., they do not have a statically known latency or pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. structure. and pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. are the basic building blocks of Spade circuits. Unlike entities and pipelines, functions have no internal state, they are combinational (pure). do_something_with_copy_view() { /* ... */ }

Copy views integrate seamlessly with . field access to ensure the copy view layer is always preserved.

struct Strout {
    x: inv boolType used to represent 1-bit values,
    y: (int<4>Type used to represent signed integers. The generic parameter (<N>) specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.ies the number of bits, inv int<8>Type used to represent signed integers. The generic parameter (<N>) specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.ies the number of bits),
}

fnFunctions together with entityEntities together with fn and pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. are the basic building blocks of Spade circuits. Unlike fn, entity can contain registers and therefore have state and unlike pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline., they do not have a statically known latency or pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. structure. and pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. are the basic building blocks of Spade circuits. Unlike entities and pipelines, functions have no internal state, they are combinational (pure). main(s: &Strout, t: &inv Strout) {
    letlet is used to define a variable. Spade infers the type of most variables from context, but you can also specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.y the type with : <type> before the =. s_y: &(int<4>Type used to represent signed integers. The generic parameter (<N>) specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.ies the number of bits, inv int<4>Type used to represent signed integers. The generic parameter (<N>) specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.ies the number of bits) = s.y;
    letlet is used to define a variable. Spade infers the type of most variables from context, but you can also specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.y the type with : <type> before the =. s_y_0: &int<4>Type used to represent signed integers. The generic parameter (<N>) specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.ies the number of bits = y.0;

    // It also works across chained field access
    letlet is used to define a variable. Spade infers the type of most variables from context, but you can also specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.y the type with : <type> before the =. s_y_0_again: int<4>Type used to represent signed integers. The generic parameter (<N>) specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.ies the number of bits = *s.y.0;

    // `inv` flipping fields is also compatible with copy views
    letlet is used to define a variable. Spade infers the type of most variables from context, but you can also specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.y the type with : <type> before the =. t_y_1: int<8>Type used to represent signed integers. The generic parameter (<N>) specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.ies the number of bits = *t.y.1;
}

Methods can take copy views using &self instead of self as an argument. When calling methods, & or * are inserted automatically to make the value match the type required by the method.

Using copy views, the previous example can be implemented by making is_requesting take a copy view instead.

fnFunctions together with entityEntities together with fn and pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. are the basic building blocks of Spade circuits. Unlike fn, entity can contain registers and therefore have state and unlike pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline., they do not have a statically known latency or pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. structure. and pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. are the basic building blocks of Spade circuits. Unlike entities and pipelines, functions have no internal state, they are combinational (pure). is_requesting(p: &ReadPort) -> boolType used to represent 1-bit values {
    p.request.is_some()
}

fnFunctions together with entityEntities together with fn and pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. are the basic building blocks of Spade circuits. Unlike fn, entity can contain registers and therefore have state and unlike pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline., they do not have a statically known latency or pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. structure. and pipelineDefines a pipeline. The number in in the parentheses is input-to-output latency of the pipeline. are the basic building blocks of Spade circuits. Unlike entities and pipelines, functions have no internal state, they are combinational (pure). main(p: ReadPort) {
    letlet is used to define a variable. Spade infers the type of most variables from context, but you can also specifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it.y the type with : <type> before the =. value = ifReturns the value of the first branch if the condition is true, otherwise the second branch.
Note that unlike software languages, Spade does not have conditional execution. You do not conditionally assign values inside if expressions, you compute a value and return it. is_requesting(p) {
        Some(10)
    } else {
        None
    };

    set p.response = value; // <-- `p` is consumed here
}

Inspecting Inverted Wires

Inverted wires are meant to be set to a value, so it is rarely necessary to read it from the inverted wire itself (although it may be desirable to avoid intermediate bindings). Copy views introduce the possibility of needing to read an inverted wire whose value is not readily available in the same scope where the copy view is being handled.

Fortunately, copy views also are the mechanism which allows inverted wires to be passed around without consuming them. The inspect method turns any &inv T value into &T, which may later be converted into a regular value with *.