docs: Add brief bus documentation

Author: Leo-Besancon

docs/src/SUMMARY.md

@@ -8,6 +8,7 @@
   - [Constraint descriptions](./description/constraints.md)
   - [Variables](./description/variables.md)
   - [Evaluators](./description/evaluators.md)
+  - [Buses](./description/buses.md)
   - [Convenience syntax](./description/convenience.md)
   - [AirScript Example](./description/example.md)
   - [Keywords](./description/keywords.md)

docs/src/description/buses.md

@@ -0,0 +1,63 @@
+# Buses
+
+A bus is a construct that aims to easily describe specific constraints, and can be for instance useful to communicate data between multiple proofs.
+
+## Bus types
+
+## Multiset `unit`
+
+Multiset-based buses can represent constraints specifying given values have been added or removed from a column, in no specific order.
+
+## LogUp `mult`
+
+LogUp-based buses are more complex than multiset buses, and can encode the multiplicity of an element: an element can be added or removed multiple times.
+
+## Defining buses
+
+See the [declaring buses](./declarations.md#buses) for more details.
+
+```
+buses {
+    unit p,
+    mult q,
+}
+```
+
+## Bus boundary constraints
+
+In the boundary constraints section, we can constrain the initial and final state of the bus. Currently, only constraining a bus to be empty (with the  `null` keyword) is supported.
+
+```
+boundary_constraints {
+    enf p.first = null;
+    enf p.last = null;
+}
+```
+
+The above example states that the bus `p` should be empty at the beginning and end of the trace.
+
+## Bus integrity constraints
+
+In the integrity constraints section, we can add and remove elements (as tuples of felts) to and from a bus. In the following examples, `p` and `q` are respectivelly multiset and logup based buses.
+
+```
+integrity_constraints {
+    p.add(a) when s1;
+    p.rem(a, b) when 1 - s2;
+}
+```
+
+Here, `s1` and `1 - s2` are binary selectors: the element is added or removed when the corresponding selector's value is 1.
+
+The global resulting constraint on the column of the bus is the following: `p ′ ⋅ ( ( α 0 + α 1 ⋅ a + α 2 ⋅ b ) ⋅ ( 1 − s2 ) + s2 ) = p ⋅ ( ( α 0 + α 1 ⋅ a ) ⋅ s1 + 1 − s1 ))`, where `α i` corresponds to the i-th random value provided by the verifier.
+
+```
+integrity_constraints {
+    q.rem(e, f, g) when s
+    q.add(a, b, c) for d
+}
+```
+
+Similarly to the previous example elements can be added or removed from `q` with binary selectors. However, as it is a LogUp-based bus, it is also possible to add and remove elements with a given scalar multiplicity with the `for` keyword (here, `d` does not have to be binary).
+
+The global resulting constraint on the column of the bus is the following: `q ′ + s ( α 0 + α 1 ⋅ e + α 2 ⋅ f + α 3 ⋅ g ) = q + d ( α 0 + α 1 ⋅ a + α 2 ⋅ b + α 3 ⋅ c )`, where `α i` corresponds to the i-th random value provided by the verifier.

docs/src/description/declarations.md

@@ -90,6 +90,23 @@ Periodic columns can be referenced by [integrity constraints](./constraints.md#i
 
 When constraints are evaluated, these periodic values always refer to the value of the column in the current row. For example, when evaluating an integrity constraint such as `enf k0 * a = 0`, `k0` would be evaluated as `0` in rows `0`, `1`, `2` of the trace and as `1` in row `3`, and then the cycle would repeat. Attempting to refer to the "next" row of a periodic column, such as by `k0'`, is invalid and will cause a `ParseError`.
 
+
+## Buses (`buses`)
+
+A `buses` section contains declarations for buses used in the description and evaluation of integrity constraints.
+
+
+The following is an example of a valid `buses` source section:
+
+```
+buses {
+    unit p,
+    mult q,
+}
+```
+
+In the above example, we declare two buses: `p` of type `unit`, and `q` of type `mult`. They respectively correspond to a multiset-based bus and a LogUp-based bus, that expand to different constraints. More information on bus types can be found in the [buses](./buses.md) section. 
+
 ## Random values (`random_values`)
 
 A `random_values` section contains declarations for random values provided by the verifier. Random values can be accessed by the named identifier for the whole array or by named bindings to single or grouped random values within the array.

docs/src/description/example.md

@@ -19,6 +19,10 @@ periodic_columns {
     k0: [1, 1, 1, 1, 1, 1, 1, 0],
 }
 
+buses {
+    mult: q,
+}
+
 boundary_constraints {
     # define boundary constraints against the main trace at the first row of the trace.
     enf a.first = stack_inputs[0];
@@ -32,6 +36,9 @@ boundary_constraints {
 
     # set the first row of the auxiliary column p to 1
     enf p.first = 1;
+
+    # set the bus q to be initially empty
+    enf q.first = null;
 }
 
 integrity_constraints {
@@ -49,5 +56,8 @@ integrity_constraints {
 
     # the auxiliary column contains the product of values of c offset by a random value.
     enf p' = p * (c + $rand[0]);
+
+    # add p to the q bus when s = 1
+    q.add(p) when s;
 }
 ```

docs/src/description/keywords.md

@@ -3,8 +3,8 @@
 AirScript defines the following keywords:
 
 - `boundary_constraints`: used to declare the source section where the [boundary constraints are described](./constraints.md#boundary_constraints).
-  - `first`: used to access the value of a trace column at the first row of the trace. _It may only be used when defining boundary constraints._
-  - `last`: used to access the value of a trace column at the last row of the trace. _It may only be used when defining boundary constraints._
+  - `first`: used to access the value of a trace column / bus at the first row of the trace. _It may only be used when defining boundary constraints._
+  - `last`: used to access the value of a trace column / bus at the last row of the trace. _It may only be used when defining boundary constraints._
 - `case`: used to declare arms of [conditional constraints](./convenience.md#conditional-constraints).
 - `const`: used to declare [constants](./declarations.md#constant-constant).
 - `def`: used to [define the name](./organization.md#root-module) of a root AirScript module.

docs/src/description/main.md

@@ -6,6 +6,7 @@
 - [Constraint descriptions](./constraints.md)
 - [Variables](./variables.md)
 - [Evaluators](./evaluators.md)
+- [Buses](./buses.md)
 - [Convenience syntax](./convenience.md)
 - [AirScript Example](./example.md)
 - [Keywords](./keywords.md)

docs/src/description/organization.md

@@ -12,6 +12,7 @@ All modules must start with a module name declaration followed by a set of sourc
 | [trace columns](./declarations.md#execution-trace-trace_columns)                      | required    | not allowed       |
 | [public inputs](./declarations.md#public-inputs-public_inputs)                        | required    | not allowed       |
 | [periodic columns](./declarations.md#periodic-columns-periodic_columns)               | optional    | optional          |
+| [buses](./declarations.md#buses-buses)                                     | optional    | optional          |
 | [random values](./declarations.md#random-values-random_values)                        | optional    | not allowed       |
 | [boundary constraints](./constraints.md#boundary-constraints-boundary_constraints)    | required    | not allowed       |
 | [integrity constraints](./constraints.md#integrity-constraints-integrity_constraints) | required    | not allowed       |

docs/src/introduction.md

@@ -16,6 +16,8 @@ AirScript includes the following features:
 
 - **Random Values**: Users can define random values provided by the verifier (e.g. `alphas: [x, y[14], z],` or `rand: [16],`)
 
+- **Buses**: Users can declare buses (e.g. `unit p,`)
+
 - **Boundary Constraints**: Users can enforce boundary constraints on main and auxiliary trace columns using public inputs, random values, constants and variables.
 
 - **Integrity Constraints**: Users can enforce integrity constraints on main and auxiliary trace columns using trace columns, periodic columns, random values, constants and variables.