Skip to content

Commit

Permalink
Documentation.
Browse files Browse the repository at this point in the history
  • Loading branch information
chriseth committed Feb 29, 2024
1 parent 4611340 commit b52a442
Show file tree
Hide file tree
Showing 8 changed files with 180 additions and 82 deletions.
5 changes: 3 additions & 2 deletions book/src/asm/declarations.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
# Declarations

Symbols can be defined via ``let <name> = <value>;``. The value is a generic [PIL-expression](../pil/expressions.md)
and its type is unconstrained (it can be a value, a function or even a higher-order function).
Symbols can be defined via ``let <name> = <value>;``, or via ``let <name>: <type> = <value>;`` if you want to
specify the type explicitly. The value is an arbitrary [PIL-expression](../pil/expressions.md).
For details, see the [Declarations](../pil/declarations.md) section in the PIL part.

Other symbols available in the current module can be accessed by name, but it is also possible to specify
full relative paths in the form of e.g. ``super::super::module_name::symbol``.
Expand Down
77 changes: 65 additions & 12 deletions book/src/pil/builtins.md
Original file line number Diff line number Diff line change
@@ -1,11 +1,15 @@
# Built-in Functions
# Built-ins

## Functions

The following functions are built into the compiler.
They need to be defined to be accessible, but their assigned value is ignored and the compiler replaces it with the following.

### Array length

`std::array::len: _[] -> int`
```rust
let<T> std::array::len: T[] -> int
```

Returns the length of an array as an integer.

Expand All @@ -17,7 +21,9 @@ let l = std::array::len(x); // returns 3

### Panic

`std::check::panic: string -> !`
```rust
let std::check::panic: string -> !
```

Aborts evaluation and prints its argument as error message as a
side-effect of its evaluation.
Expand All @@ -39,37 +45,47 @@ let secp256k1_inverse = |x|

### Conversions

`std::convert::fe: int -> fe`
```rust
let<T: FromLiteral> std::convert::fe: T -> fe
```

This function is meant to be used on `int`, but also works on `fe` for convenience.

Converts a non-negative integer less than the field modulus to a field element.
It converts a non-negative integer less than the field modulus to a field element.
Causes a type error in all other cases.

If the argument is already a field element, it is returned without modification.

`std::convert::int: fe -> int`
```rust
let<T: FromLiteral> std::convert::int: T -> int
```

This function is meant to be used on `fe`, but also works on `int` for convenience.

Converts a field element to an integer.
It converts a field element to an integer.

If the argument is already an integer, it is returned without modification.

### Printing

`std::debug::print: string -> []`
```rust
let std::debug::print: string -> constr[]
```

This function takes a string and prints it on the standard output during evaluation, as a side-effect of its evaluation.

This function should only be used for debugging purposes.

Any non-string argument is converted to a string first and then printed.

Note that the function does not append a newline at the end.

It returns an empty array so that it can be used at statement level where
It returns an empty `constr` array so that it can be used at statement level where
constraints are expected.

### Modulus

`std::field::modulus: -> int`
```rust
let std::field::modulus: -> int
```

Returns the current field's modulus as an integer.

Expand All @@ -82,3 +98,40 @@ if std::field::modulus() != 2**64 - 2**32 + 1 {
[]
};
```

## Operators

The following operators are supported by powdr-pil with their respective signatures.

```
let<T: Add> +: T, T -> T
let<T: Sub> -: T, T -> T
let<T: Neg> -: T -> T
let<T: Mul> *: T, T -> T
let /: int, int -> int
let %: int, int -> int
let<T: Pow> **: T, int -> T
let <<: int, int -> int
let >>: int, int -> int
let &: int, int -> int
let |: int, int -> int
let ^: int, int -> int
let<T: Ord> <: T, T -> bool
let<T: Ord> <=: T, T -> bool
let<T: Ord> >: T, T -> bool
let<T: Ord> >=: T, T -> bool
let<T: Ord> <: T, T -> bool
let<T: Eq> ==: T, T -> bool
let<T: Eq> !=: T, T -> bool
let =: expr, expr -> constr
let ': expr -> expr
let ||: bool, bool -> bool
let &&: bool, bool -> bool
let !: bool -> bool
```
13 changes: 8 additions & 5 deletions book/src/pil/declarations.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,18 +7,21 @@ from the type of the symbol and the way the symbol is used.
Symbols can be declared using ``let <name>;`` and they can be declared and defined
using ``let <name> = <value>;``, where ``<value>`` is an expression. The [type](./types.md) of the symbol
can be explicitly specified using ``let <name>: <type>;`` and ``let <name>: <type> = <value>;``.
It is even possible to define generic symbols using ``let<TV1, TV1, ..> <name>: <type> = <value>;``,
where the `TV` are newly created type variables that can be used in the type.

This syntax can be used for constants, fixed columns, witness columns and even (higher-order)
functions that can transform expressions. The kind of symbol is deduced by its type and the
way the symbol is used:

- Symbols without a value are witness columns or arrays of witness columns. Their type can be omitted. If it is given, it must be ``col`` or ``col[]``.
- Symbols evaluating to a number or with type ``fe`` are constants.
- Symbols without type but with a value that is a function with a single parameter are fixed columns.
- Symbols defined with a value and type ``col`` (or ``col[]``) are fixed columns (or arrays of fixed columns).
- Symbols without a value are witness columns or arrays of witness columns. Their type can be omitted. If it is given, it must be ``col`` or ``col[k]``.
- Symbols with type ``fe`` are constants.
- Symbols defined with a value and type ``col`` (or ``col[k]``) are fixed columns (or arrays of fixed columns).
- Symbols defined with a value and type ``expr`` (or ``expr[k]``) are intermediate columns (or arrays of intermediate columns).
- Everything else is a "generic symbol" that is not a column or constant.

> Note that the type ``col`` is the same as ``int -> fe``, so ``let w: int -> fe`` also declares a witness column.
> Note that a symbol with declared type ``int -> fe`` is not considered a column.
> Its type has to be ``col`` (or ``col[k]``). See [Types](./types.md) for details.
Examples:

Expand Down
8 changes: 4 additions & 4 deletions book/src/pil/expressions.md
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ The "default" arm with the pattern `_` matches all values.

Example:

```
```rust
let fib = |i| match i {
0 => 1,
1 => 1,
Expand All @@ -62,12 +62,12 @@ let fib = |i| match i {

If expressions take the form ``if <condition> { <true value> } else { <false value> }``, where the "else" part is not optional.

If the condition evaluates to a non-zero number, `<true value>` is evaluated, otherwise `<false value>` is.
If the condition evaluates to ``true``, then `<true value>` is evaluated, otherwise `<false value>` is.


Example:

```
```rust
let is_seven = |i| if i == 7 { 1 } else { 0 };
```

Expand All @@ -88,6 +88,6 @@ Arbitrary parentheses are allowed.

The following example illustrates how you can still use the generic language:

```
```rust
{{#include ../../../test_data/pil/book/generic_to_algebraic.pil}}
```
2 changes: 0 additions & 2 deletions book/src/pil/fixed_columns.md
Original file line number Diff line number Diff line change
Expand Up @@ -30,5 +30,3 @@ A column can be seen as a mapping from integers to field elements. In this conte
```
{{#include ../../../test_data/pil/fixed_columns.pil:mapping}}
```

> Note that conversion from integer to field element is currently implicit, as seen in the first example above.
Loading

0 comments on commit b52a442

Please sign in to comment.