# Blocks and arrays¶

CertSAFE’s mechanism for representing arrays is called **blocks**. Using blocks, a single wire can carry an array of
many values. Arrays can be indexed on one or more dimensions, and the index types can be
fixed-size integer types,
integer interval types, or
enumeration types. Blocks are also compatible with the other notations in
CertSAFE: applying a diagram full of ordinary logic to input variables that have *block dimensions* will automatically
map the logic over the input arrays.

To help illustrate how to write models using blocks notation, this page includes a number of examples. Each example shows C code for a simple program, together with the analogous CertSAFE logic that performs the same function.

Note

For a **walkthrough of how to use arrays when modeling and simulating real-world systems**, see the
Blocks and Arrays Tutorial.

For information on **using array-typed variables in simulations**, see the article on
working with blocks in simulations.

## Concept¶

If you are familiar with matrix-based programming environments such as MATLAB or NumPy, the blocks notation in CertSAFE can often be thought of as a statically-typed version of the same idea. Standard logic is automatically mapped pointwise over input arrays, producing output arrays of the same size. This works for arithmetic, Boolean operators, and even stateful components such as the One Frame Delay.

Note

The term *blocks* is chosen by analogy with *clocks*, which is a feature for conditional execution present in some
other dataflow languages such as Lustre. Blocks are similar to clocks in that they are a property of a network at the
type level that propagates across the model automatically. However, whereas clocks allow logic to be executed *less*
frequently, blocks allow logic to be executed *more* frequently.

Be careful not to confuse the term *blocks* with the common use of the word “block” to refer to a diagram component
in other dataflow languages. In this documentation, the word “blocks” always refers to the CertSAFE arrays feature.

### Example: Pointwise multiplication by 2¶

```
#define SIZE 100
void multiplyAllBy2(int input[SIZE], int output[SIZE]) {
for (int k = 0; k < SIZE; k++)
output[k] = 2 * input[k];
}
```

Note that there is no explicit loop in the CertSAFE diagram. The Inline Multiplier component is automatically vectorized
over the entire input array—whatever size it may be—without any additional notation. The *block key type* annotation
`[0..99]`

, together with the *scalar type* annotation `Int32`

, tells CertSAFE that the diagram above accepts any
array of `Int32`

values that has an innermost dimension whose key type is the
integer interval type `[0..99]`

. Block key types are the most
common use case for integer interval types, because they allow specifying an array with a specific arbitrary integer
size. Block key types are discussed in more detail in subsequent sections of this page.

### Example: Dot product¶

```
double dotProduct(int size, double u[], double v[]) {
double o = 0.0;
for (int k = 0; k < size; k++)
o += u[k] * v[k];
return o;
}
```

Here is an example of a diagram that uses the standard multiplication component together with a *Block Sum* component to
compute the dot product of two vectors of the same length. The multiplication component is automatically vectorized to
operate over matching pairs of input array indices. The λ (lambda) symbol on the single input of the Sum
primitive indicates that the sum is taken over all of the values of the input array along the innermost dimension.

Unlike the C code, in the CertSAFE model the size of the arrays does not have to be passed in as an explicit parameter.
Instead, the size is a polymorphic type parameter that is inferred by the type system from the surrounding context when
this diagram is used as a custom component. The type system infers that the two arrays must have the *same size* and the
*same number of dimensions*, because they are both being fed into the multiplication component to get a single output
array of that size.

Warning

An important difference between CertSAFE and most matrix-based languages is that **arrays with different numbers of
dimensions cannot be mixed freely** in general. For example, attempting to add a vector to a matrix will not
automatically expand the vector with an extra dimension; it is simply a static type error. Missing dimensions must
instead be explicitly added using the *Capture* component. This restriction allows CertSAFE to automatically infer
the dimensionality of all arrays in a model, while preserving the flexibility to use logic with different array
sizes. The details of when explicit dimension conversion is necessary are discussed later in this page.

## Block primitives¶

Array dimensions—commonly called *block dimensions* in the context of CertSAFE—are introduced and eliminated by
special primitive components. There are a handful of dedicated primitives for manipulating block dimensions, while the
rest is handled by special modes of the standard primitives.

### Varargs folds¶

All varargs components (primitives that have a variable number of input pins, such as the Boolean gates) have an
*Inputs* property. By default, this is set to allow two or more individual inputs pins. However, by selecting the
*block* button, the component will instead take a single array-valued input and *fold* over a dimension of the input,
eliminating it from the output. For example, an AND gate set to block level 1, given as input a 1-dimensional array,
will output a single Boolean value that is `True`

if and only if all of the values in the input array are `True`

.

All varargs fold components have an *identity* value, which is produced when the folded dimension is empty—that is,
when the folded dimension’s key type is a data type with no values. The identity value is the mathematical identity for
the binary operation applied by the fold. For example, the identity value for an AND Gate is `True`

, the identity
value for an OR Gate is `False`

, the identity value for a Min Selector is the maximum value of the scalar data type,
etc.

Note

All primitives that eliminate a block dimension, such as the varargs folds and the Block Switch, are marked with a λ (lambda) symbol on one of their input pins. This is because these components correspond in a formal sense to the lambda expressions from functional programming languages.

### Capture¶

The *Capture* primitive adds a new array dimension by replicating the input value repeatedly. The size of the new
dimension on the output of the Capture component is automatically inferred by the type system in order to match whatever
the output wire is connected to. If the output array is inferred to be of size 10, then giving an input value of `5.0`

to the Capture component results in the output array `[5.0, 5.0, 5.0, 5.0, 5.0, 5.0, 5.0, 5.0, 5.0, 5.0]`

.

The Capture primitive is often used when mixing scalar-typed variables with array-typed variables, or mixing array-typed
variables having different numbers of dimensions. Since CertSAFE requires all inputs to have identical array dimensions
when applying a pointwise operation with multiple inputs, it is necessary to use the Capture component to adapt the
input values to have the correct dimensionality. If the pointwise operation is conceptualized as performing a scalar
operation in a loop, the Capture component can be thought of as *capturing* a variable from outside the loop and
bringing it into the scope of the loop, similar to how nested functions can capture variables from enclosing scopes in
functional programming languages.

### Index¶

The *Index* primitive outputs an array whose value at each position is the current array index along the chosen
dimension. For example, for a single-dimensional array whose key type is the integer interval type `[1..10]`

, the
Index primitive will output the array `[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]`

. This can be used to perform different logic
depending on the current loop index.

### Pack Block and Unpack Block¶

The *Pack Block* primitive provides a convienient syntax for combining multiple scalar values into a one-dimensional
array, or assembling a multi-dimensional array out of lower-dimensional arrays. Similarly, the *Unpack Block* primitive
provides a convienient syntax for extracting one or more scalar values from an array, or slicing lower-dimensional
arrays out of a multi-dimensional array. These components work similarly to the Switch primitive, in that the key data
type and list of keys to pack/unpack are selected through the Properties view. The Pack Block component also requires
all entries to be covered by its input cases, similar to the Switch primitive and the inputs of case tables.

Warning

When using a Pack Block or Unpack Block primitive to assemble or disassemble a multidimensional array, be careful
of which array dimension the primitive is operating on. Remember that the types of the input and output networks are
shown in tooltips on mouseover. As with other block primitives, the dimension on which a Pack Block or Unpack Block
component operates can be modified by editing the *Block Level* property in the Properties view.

### Block Switch and Compose¶

The *Block Switch* and *Compose* primitives are used to access arrays at indices defined by a variable. The Block Switch
takes an array and an index and outputs the value of the array at that index. The Compose component uses the array(s) on
the top of the component to reindex the array on the left of the component, *composing* the arrays together (like
function composition).

The only difference between the Block Switch and Compose primitives is the choice of dimensions being indexed. The Block Switch component eliminates a single array dimension, which can be at any depth in the block stack, by slicing to a chosen position. The Compose component reindexes an input array by accessing one input array at the locations determined by the values of another group of input arrays. Try different property values and check the type signatures in the tooltips to see which primitive is appropriate for any given situation.

### One Index Delay and Fold End¶

The One Index Delay and Fold End primitives are used for writing custom scan and fold operations that perform more general loops than can be expressed using only pointwise operations, adding and removing block levels, and the built-in varargs folds. These primitives are covered in more detail in later sections.

## Block prefixes and key types¶

When the mouse is hovered over a wire in a diagram, CertSAFE will display type information for that variable. This
includes the *block prefix* of the variable, which describes the variable’s block dimensions, and the *scalar type* of
the variable, which is the type of the actual values contained in the array.

The block prefix consists of the symbol ℕ, followed by a list of zero or more additional *key types*, which are the
index types of the variable’s block dimensions. Following the block prefix, CertSAFE displays the symbol ⊢
(the “turnstile”), then the scalar type of the variable. For example, in the image above, the variable is a
two-dimensional array of `Float64`

values, where the first dimension’s key type is `[0..3]`

and the second
dimension’s key type is `Color`

.

CertSAFE models are always executed repeatedly at a fixed global frame rate. This can be thought of like an additional
block dimension, called the *time dimension*. The time dimension is represented by the symbol ℕ (“natural numbers”)
at the beginning of the block prefix, corresponding to the infinite list of frame numbers {0, 1, 2, ...}. This reflects
how a CertSAFE variable is never really a single value, but rather an unbounded stream of values that can be produced
for as long as desired in a simulation.

### Constness¶

Variables whose values are inferred to not change over time are
indicated in the user interface by prefixing the symbol ℕ with **const**. Similarly, CertSAFE also tries to infer
when a variable’s value does not change when moving along a block dimension, and prefixes such dimensions with
**const**. For example, the following variable is a 1-dimensional array indexed on `[1..5]`

, where the contents of the
array may change over time, but at any given time all five of the slots in the array have the same value as each other.

## The block stack¶

By default, primitive components that manipulate the block dimensions of variables always act upon the *innermost*
dimension of the block prefix—that is, the dimension closest to the right-hand end. This makes the block prefix behave
as a sort of last-in-first-out *block stack*.

For example, the component shown to the right sums the values of an array across the innermost block dimension. If given
as input a 3-dimensional array with key types `[0..3]`

, `[1..10]`

, and `[1..5]`

, it will return as output a
2-dimensional array with key types `[0..3]`

and `[1..10]`

, with each value in the output array being the sum of 5
values from the input array.

All block primitives provide one or more parameters that determine the dimension(s) on which the primitive operates.
Dimension parameters are indexed from the right, so that the innermost dimension is numbered 1, the next-innermost
dimension is numbered 2, etc. In the example above, the Block Sum primitive has a *Block Level* parameter that by
default is set to 1, meaning that it operates on the innermost block dimension.

Changing the Block Level parameter to 2 (using the Properties view) results in the modified component shown to the
right. If given as input a 3-dimensional array with key types `[0..3]`

, `[1..10]`

, and `[1..5]`

, this modified
component will return as output a 2-dimensional array with key types `[0..3]`

and `[1..5]`

, with each value in the
output array being the sum of 10 values from the input array.

Note

Currently, there is a maximum depth limit of 16 levels in any block prefix. That is, no array can have more than 16 dimensions. This is unlikely to be a constraint for most real-world models—it is the equivalent of writing 16 pairs of square brackets in a variable declaration in C.

## Block prefix variables¶

When viewed in definition mode, block prefix types contain *block prefix variables*. A block prefix variable is a
placeholder in a block prefix where additional dimensions may be inserted. Block prefix variables enable *block
polymorphism*, where the number and types of array dimensions can vary between different instances of a component.
This is similar to ordinary data type polymorphism, but with lists of array
dimensions instead of individual data types.

A block prefix variable is represented in the user interface by Γ (uppercase Greek letter gamma), possibly followed by a number to distinguish the variable from other block prefix variables that may be substituted with different lists of key types. In a definition-mode block prefix, the block prefix variable always appears between the ℕ symbol and the leftmost key type. Additional array dimensions can be inserted at this location through type inference from the surrounding context in which the component is used. This produces the “block stack” behavior discussed above.

*All* CertSAFE components, including user-defined custom components, are block polymorphic in the sense of having block
prefix variables in their types. This means that any component that works on scalar values can also be applied pointwise
to 1-D arrays, 2-D arrays, etc. This also means that any component that works on 1-D arrays can be applied to 2-D
arrays, in which case it will operate pointwise across the outer array dimension. This concept generalizes no matter how
many dimensions appear in the type of the component and how many additional dimensions are substituted for the block
prefix variable.

### Example: Block Switch¶

This Block Switch component can be applied to a one-dimensional input array with a scalar selector value to produce a scalar output. It could have the following types:

Inputs | Outputs |
---|---|

selector : ℕ ⊢ Int8 |
o : ℕ ⊢ Float32 |

i : ℕ, Int8 ⊢ Float32 |

However, it can *also* be applied to a two-dimensional input array with a one-dimensional array input on the selector
pin to produce a one-dimensional array as output. This applies the Block Switch pointwise with respect to the outer
dimension of the two-dimensional input array. The types might look like this:

Inputs | Outputs |
---|---|

selector : ℕ, [1..5] ⊢ Int8 |
o : ℕ, [1..5] ⊢ Float32 |

i : ℕ, [1..5], Int8 ⊢ Float32 |

### Example: Literal¶

The block prefix of any pure logic is simply “**pure** ℕ, Γ”. This means that pure logic does not depend on
the time dimension, and can be applied to zero or more array dimensions indexed on any types. As a particular case of
the general principle, the Literal primitive is pure, so it can be applied to any number of block dimensions to generate
an array filled with a single literal value. For example, connecting a Literal component with a value of `9`

directly
to logic that requires an array of size 10 will automatically produce the array `[9, 9, 9, 9, 9, 9, 9, 9, 9, 9]`

.
Effectively, the `9`

Literal component is being replicated 10 times, or executed 10 times in a loop.

## Writing arbitrary loops with One Index Delay¶

It is possible to model many different types of logic using only the basic operations of adding and removing block
levels and applying built-in folds such as the AND Gate or Sum primitives. However, some behaviors cannot be expressed
using only these operations. To address such situations, CertSAFE provides another, very general block primitive called
the *One Index Delay*. Using the One Index Delay primitive together with the other block primitives, it is possible to
write any logic that can be expressed using bounded loops.

Note

CertSAFE does not currently provide any mechanism for writing unbounded loops, or loops whose maximum length is not known until the loop executes. This is intentional: it ensures that a single frame of execution cannot run forever, which is an important constraint for real-time systems. Using the One Index Delay component together with switching logic, it is possible to emulate loops whose length varies at runtime, as long as an upper bound on the length of the loop is known at modeling time.

The One Index Delay component is analogous to the One Frame Delay component—in fact, they are the same primitive, just
with the *Block Level* parameter set differently. Whereas the One Frame Delay outputs the value of the input delayed by
one frame along the time dimension, the One Index Delay outputs the value of the input delayed by one index along a
block dimension. When a One Index Delay component is inserted into a dependency cycle, the effect is that values at
later indices in the array are defined in terms of values at earlier indices in the array.

### Example: Generalized Fibonacci numbers¶

```
#define SIZE 10
void generalizedFibonacciNumbers(int f0, int f1, int fibs[SIZE]) {
fibs[0] = f0;
fibs[1] = f1;
for (int k = 2; k < SIZE; k++)
fibs[k] = fibs[k - 1] + fibs[k - 2];
}
```

This code computes the first 10 terms of a generalized Fibonacci sequence, where \(f_0\) and \(f_1\) are
parameters and then the rest of the terms are defined by \(f_{k+2} = f_k + f_{k+1}\). The CertSAFE diagram uses the
One Index Delay component twice to look up the previous and second-previous values of the array as it is being produced.
Note that we need Capture components on the initial condition pins of the One Index Delays to make these pins
scalar-typed. Without the Capture components, the `f0`

and `f1`

input variables would be inferred as array-typed and
the One Index Delays would access their first indices for the IC values (similarly to how a One Frame Delay accesses the
value of its IC pin on the first frame).

## Extracting the last value with Fold End¶

When using the One Index Delay component, sometimes you just want the final value computed by the loop (a *fold*
operation) rather than the entire history of intermediate values (a *scan* operation). It is possible to extract the
last value from the array produced by the One Index Delay component using a Block Switch with a Literal value on the
selector pin; however, this does not work polymorphically for arrays indexed on different key types. The *Fold End*
primitive handles this automatically. A Fold End component behaves like a Block Switch with a Literal selector input
that polymorphically changes to the appropriate value for any non-empty array key type. This allows the final value of
a loop to be extracted without needing the index of the final value to be written into the diagram as an explicit
Literal.

### Example: Babylonian square root¶

```
double babylonianSqrt(double x) {
double y = x;
for (int k = 1; k <= 10; k++)
y = 0.5 * (y + (x / y));
return y;
}
```

This code computes an approximation to the square root of \(x\) by applying 10 iterations of the
Babylonian method. It starts with
\(y_0 = x\) and then iterates \(y_{k+1} = \frac{1}{2} \left(y_k + \frac{x}{y_k}\right)\). In the C code, it is
not necessary to store all of the intermediate values \(y_1, \dots, y_{10}\) during the computation; instead, a
single mutable `y`

variable is repeatedly overwritten. CertSAFE uses immutable variables rather than mutable
variables, so in the CertSAFE diagram, the variable `yk`

is an array containing all of the values
\(y_1, \dots, y_{10}\), and a Fold End component is used to extract the final value.

## Block dependencies¶

Similar to how the One Frame Delay component can break an illegal dependency cycle in a diagram, the One Index Delay component can also break certain illegal dependency cycles. Specifically, a One Index Delay can break a dependency cycle only if any fold operation in the dependency cycle is over a dimension further to the right in the block prefix than the dimension that the One Index Delay component is delaying across. The time dimension ℕ is considered to be the leftmost dimension in the block prefix, so a One Frame Delay component can break any dependency cycle regardless of what block operations it contains.

### Example: Dependency cycles¶

The diagram above is illegal because the Block Sum eliminates the dimension that the One Index Delay is delaying across, before the Capture component reintroduces it in a cycle.

However, this similar diagram is legal because the Capture component introduces a new dimension that is eliminated by the Block Sum component, and the new dimension is further to the right in the block prefix from the dimension that the One Index Delay is delaying across.

### Dependency line labels¶

When mousing over the pins of a component, CertSAFE will display numeric labels on the dependency lines between pairs of pins that involve block operations.

- For a solid blue line, the number is the largest
*N*such that a loopback in the containing diagram with a level*N*index delay is illegal. If no number is displayed, then there are no folds along the dependency, so any delay makes the loopback legal. - For a dashed gray line, the number is the smallest
*N*such that a loopback in the containing diagram with a level*N*fold is illegal. If no number is displayed, then there is a time delay along the dependency, so the loopback is legal no matter what fold is added in the containing diagram.