Skip to content

Commit

Permalink
Merge pull request #173 from 0xPolygonMiden/tohrnii-lc-docs
Browse files Browse the repository at this point in the history
feat(docs): add docs for list comprehension
  • Loading branch information
tohrnii authored Mar 7, 2023
2 parents 5db266f + a1e2512 commit 700c7da
Show file tree
Hide file tree
Showing 5 changed files with 62 additions and 0 deletions.
1 change: 1 addition & 0 deletions docs/src/SUMMARY.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
- [File structure](./description/structure.md)
- [Type declarations](./description/declarations.md)
- [Variables](./description/variables.md)
- [Convenience syntax](./description/convenience-syntax.md)
- [Constraint descriptions](./description/constraints.md)
- [AirScript Example](./description/example.md)
- [Keywords](./description/keywords.md)
Expand Down
55 changes: 55 additions & 0 deletions docs/src/description/convenience-syntax.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@
# Convenience syntax

To make writing constraints easier, AirScript provides a number of syntactic conveniences. These are described in this section.

## List comprehension

List comprehension provides a simple way to create new vectors. It is similar to the list comprehension syntax in Python. The following examples show how to use list comprehension in AirScript.

```
let x = [a * 2 for a in b]
```
This will create a new vector with the same length as `b` and the value of each element will be twice that of the corresponding element in `b`.

```
let x = [a + b for (a, b) in (c, d)]
```
This will create a new vector with the same length as `c` and `d` and the value of each element will be the sum of the corresponding elements in `c` and `d`. This will throw an error if `c` and `d` vectors are of unequal lengths.

```
let x = [2^i * a for (i, a) in (0..5, b)]
```
Ranges can also be used as iterables, which makes it easy to refer to an element and its index at the same time. This will create a new vector with length 5 and each element will be the corresponding element in `b` multiplied by 2 raised to the power of the element's index. This will throw an error if `b` is not of length 5.

```
let x = [m + n + o for (m, n, o) in (a, 0..5, c[0..5])]
```
Slices can also be used as iterables. This will create a new vector with length 5 and each element will be the sum of the corresponding elements in `a`, the range 0 to 5, and the first 5 elements of `c`. This will throw an error if `a` is not of length 5 or if c is of length less than 5.

## List folding

List folding provides syntactic convenience for folding vectors into expressions. It is similar to the list folding syntax in Python. List folding can be applied to vectors, list comprehension or identifiers referring to vectors and list comprehension. The following examples show how to use list folding in AirScript.

```
trace_columns:
main: [a[5], b, c]
integrity_constraints:
let x = sum(a)
let y = sum([a[0], a[1], a[2], a[3], a[4]])
let z = sum([a * 2 for a in a])
```

In the above, `x` and `y` both represent the sum of all trace column values in the trace column binding `a`. `z` represents the sum of all trace column values in the trace column binding `a` multiplied by `2`.

```
trace_columns:
main: [a[5], b, c]
integrity_constraints:
let x = prod(a)
let y = prod([a[0], a[1], a[2], a[3], a[4]])
let z = prod([a + 2 for a in a])
```

In the above, `x` and `y` both represent the product of all trace column values in the trace column binding `a`. `z` represents the product of all trace column values in the trace column binding `a` added by `2`.
2 changes: 2 additions & 0 deletions docs/src/description/keywords.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,10 @@ AirScript defines the following keywords:
- `integrity_constraints`: used to declare the [source section](./structure.md#source-sections) where the [integrity constraints are described](./constraints.md#integrity_constraints).
- `let`: used to declare intermediate variables in the boundary_constraints or integrity_constraints source sections.
- `periodic_columns`: used to declare the [source section](./structure.md#source-sections) where the [periodic columns are declared](./declarations.md). _They may only be referenced when defining integrity constraints._
- `prod`: used to fold a list into a single value by multiplying all of the values in the list together.
- `public_inputs`: used to declare the [source section](./structure.md#source-sections) where the [public inputs are declared](./declarations.md). _They may only be referenced when defining boundary constraints._
- `random_values`: used to declare the [source section](./structure.md#source-sections) where the [random values are described](./declarations.md).
- `sum`: used to fold a list into a single value by summing all of the values in the list.
- `trace_columns`: used to declare the [source section](./structure.md#source-sections) where the [execution trace is described](./declarations.md). _They may only be referenced when defining integrity constraints._
- `main`: used to declare the main execution trace.
- `aux`: used to declare the auxiliary execution trace.
Expand Down
1 change: 1 addition & 0 deletions docs/src/description/main.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
- [File structure](./structure.md)
- [Type declarations](./declarations.md)
- [Variables](./variables.md)
- [Convenience syntax](./convenience-syntax.md)
- [Constraint descriptions](./constraints.md)
- [AirScript example](./example.md)
- [Keywords](./keywords.md)
Expand Down
3 changes: 3 additions & 0 deletions docs/src/introduction.md
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,9 @@ AirScript includes the following features:

- **Variables**: Local variables can be declared for use in defining boundary and integrity constraints. Variables can be scalars, vectors or matrices built from expressions (e.g. `let x = k * c[1]'`, `let y = [k * c[1], l * c[2], m * c[3]]` or `let z = [[k * c[1], l * c[2]], [m * c[3], n * c[4]]]`)

The language also includes some convenience syntax like list comprehension and list folding to make writing constraints easier.
(e.g. `let x = [k * c for (k, c) in (k, c[1..4])]`, `let y = sum([k * c for (k, c) in (k, c[1..4])])`)

The language will be specified in detail in the rest of this book.

### CLI
Expand Down

0 comments on commit 700c7da

Please sign in to comment.