diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index a664ebdea..593b3bc14 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -11,6 +11,7 @@ - [CLI](./cli/README.md) - [asm](./asm/README.md) - [Modules](./asm/modules.md) + - [Declarations](./asm/declarations.md) - [Machines](./asm/machines.md) - [Registers](./asm/registers.md) - [Functions](./asm/functions.md) diff --git a/book/src/asm/declarations.md b/book/src/asm/declarations.md new file mode 100644 index 000000000..090552a08 --- /dev/null +++ b/book/src/asm/declarations.md @@ -0,0 +1,13 @@ +# Declarations + +Symbols can be defined via ``let = ;``. 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). + +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``. + +Here are some examples of how to define and use symbols: + +``` +{{#include ../../../test_data/asm/book/declarations.asm}} +``` \ No newline at end of file diff --git a/test_data/asm/book/declarations.asm b/test_data/asm/book/declarations.asm new file mode 100644 index 000000000..048243c45 --- /dev/null +++ b/test_data/asm/book/declarations.asm @@ -0,0 +1,31 @@ +mod utils { + // This defines a function by means of a lambda expression that + // computes the sum of an array of values. + let sum = |len, arr| match len { 0 => 0, _ => arr[len - 1] + sum(len - 1, arr) }; + // A simple function that returns the input incremented by one. + let incremented = |x| x + 1; + // This is a function that takes an expression as input and returns + // a constraint enforcing this expression increments by a certain value + // between rows. + let constrain_incremented_by = |x, inc| x' == x + inc; +} + +machine Main { + // Machines create local scopes in the way functions create local scopes: + // - all symbols in the machine's module are available without prefix, + // - new symbols can be defined but are only available inside the machine. + reg A; + reg pc[@pc]; + + // This defines a witness column, + let x; + // and now we force it to stay unchanged. + utils::constrain_incremented_by(x, 0); + + // We define an instruction that uses a complicated way to increment a register. + instr incr_a { A = utils::incremented(A) } + + function main { + return; + } +} \ No newline at end of file diff --git a/test_data/asm/book/modules.asm b/test_data/asm/book/modules.asm index 8bb234320..de57a57c8 100644 --- a/test_data/asm/book/modules.asm +++ b/test_data/asm/book/modules.asm @@ -9,6 +9,17 @@ mod submodule_in_folder; use submodule::Other as SubmoduleOther; use submodule_in_folder::Other as FolderSubmoduleOther; +let zero = 0; + +// we can also define modules inline +mod utils { + // Each module has a fresh symbol list. Every external symbol needs to be imported, + // even from the parent module. + use super::zero; + + let one = zero + 1; +} + machine Main { // use a machine from another module by relative path my_module::Other a;