This PR solves #1374
There are 3 examples included in the PR:
1. `lookup_via_challenges_ext_simple.asm` is the most basic example
which implements {a} in {b} using extension field without using
selectors
2. `lookup_via_challenges_ext_no_selector.asm` implements {a1, a2} in
{b1, b2} using extension field without using selectors
3. `lookup_via_challenges_ext.asm` is a more complex example than others
which implements {a1, a2, a3} in {b1, b2, b3} using extension field
(which also handles tuples using Reed-Solomon fingerprinting). It also
use different lhs and rhs selectors.
---------
Co-authored-by: Georg Wiese <georgwiese@gmail.com>
This PR adds a new memory machine to the standard library that also
supports a `mstore_bootloader` operation: It's like a normal `mstore`,
but the first access to every memory cell *has to* come from this
operation.
As a follow-up, we'll be able to use it in the RISC-V machine (#1462).
I think this is best reviewed by reviewing the diff to the normal memory
machine and comparing it to [the code we have currently inlined in the
RISC-V
machine](abbe26618f/riscv/src/code_gen.rs (L500-L553)):
```diff
3,5c3,7
< // A read/write memory, similar to that of Polygon:
< // https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/pil/mem.pil
< machine Memory with
---
> /// This machine is a slightly extended version of std::machines::memory::Memory,
> /// where in addition to mstore, there is an mstore_bootloader operation. It behaves
> /// just like mstore, except that the first access to each memory cell must come
> /// from the mstore_bootloader operation.
> machine MemoryWithBootloaderWrite with
7c9
< operation_id: m_is_write,
---
> operation_id: operation_id,
13a16
> operation mstore_bootloader<2> m_addr, m_step, m_value ->;
29a33
> col witness m_is_bootloader_write;
30a35,36
> std::utils::force_bool(m_is_bootloader_write);
> col operation_id = m_is_write + 2 * m_is_bootloader_write;
35a42
> (1 - is_mem_op) * m_is_bootloader_write = 0;
37,39c44,45
< // If the next line is a not a write and we have an address change,
< // then the value is zero.
< (1 - m_is_write') * m_change * m_value' = 0;
---
> // The first operation of a new address has to be a bootloader write
> m_change * (1 - m_is_bootloader_write') = 0;
41,42c47,52
< // change has to be 1 in the last row, so that a first read on row zero is constrained to return 0
< (1 - m_change) * LAST = 0;
---
> // m_change has to be 1 in the last row, so that the above constraint is triggered.
> // An exception to this when the last address is -1, which is only possible if there is
> // no memory operation in the entire chunk (because addresses are 32 bit unsigned).
> // This exception is necessary so that there can be valid assignment in this case.
> pol m_change_or_no_memory_operations = (1 - m_change) * (m_addr + 1);
> LAST * m_change_or_no_memory_operations = 0;
46c56
< (1 - m_is_write') * (1 - m_change) * (m_value' - m_value) = 0;
---
> (1 - m_is_write' - m_is_bootloader_write') * (1 - m_change) * (m_value' - m_value) = 0;
➜ powdr git:(memory-with-bootloader-write) ✗
```
Allow VM instructions to use the `link` notation, unifying the way
machines are linked from VMs and block machines.
Previous syntax for "external instructions" not allowed anymore, and
should use the new `link` syntax.
Makes the permutation argument sound on the Goldilocks field by
evaluating polynomials on the extension field introduced in #1310.
I also used the new `Constr::Permutation` variant!
A few test cases (also tested in CI):
#### No extension field
`cargo run pil test_data/std/permutation_via_challenges.asm -o output -f
--field bn254 --prove-with halo2-mock`
This still works and produces the same output as before, thanks to the
PIL evaluator removing multiplications by 0 etc:
```
col witness stage(1) z;
(std::protocols::permutation::is_first * (main.z - 1)) = 0;
((((1 - main.first_four) * ((std::protocols::permutation::beta1 - ((std::protocols::permutation::alpha1 * main.b1) + main.b2)) - 1)) + 1) * main.z') = (((main.first_four * ((std::protocols::permutation::beta1 - ((std::protocols::permutation::alpha1 * main.a1) + main.a2)) - 1)) + 1) * main.z);
```
#### With extension field
`cargo run pil test_data/std/permutation_via_challenges_ext.asm -o
output -f --field bn254 --prove-with halo2-mock`
The constraints are significantly more complex but seem correct to me:
```
col witness stage(1) z1;
col witness stage(1) z2;
(std::protocols::permutation::is_first * (main.z1 - 1)) = 0;
(std::protocols::permutation::is_first * main.z2) = 0;
(((((1 - main.first_four) * ((std::protocols::permutation::beta1 - ((std::protocols::permutation::alpha1 * main.b1) + main.b2)) - 1)) + 1) * main.z1') + ((7 * ((1 - main.first_four) * (std::protocols::permutation::beta2 - (std::protocols::permutation::alpha2 * main.b1)))) * main.z2')) = ((((main.first_four * ((std::protocols::permutation::beta1 - ((std::protocols::permutation::alpha1 * main.a1) + main.a2)) - 1)) + 1) * main.z1) + ((7 * (main.first_four * (std::protocols::permutation::beta2 - (std::protocols::permutation::alpha2 * main.a1)))) * main.z2));
((((1 - main.first_four) * (std::protocols::permutation::beta2 - (std::protocols::permutation::alpha2 * main.b1))) * main.z1') + ((((1 - main.first_four) * ((std::protocols::permutation::beta1 - ((std::protocols::permutation::alpha1 * main.b1) + main.b2)) - 1)) + 1) * main.z2')) = (((main.first_four * (std::protocols::permutation::beta2 - (std::protocols::permutation::alpha2 * main.a1))) * main.z1) + (((main.first_four * ((std::protocols::permutation::beta1 - ((std::protocols::permutation::alpha1 * main.a1) + main.a2)) - 1)) + 1) * main.z2));
```
#### On Goldilocks
Running the first example on GL fails, because using the permutation
argument without the extension field would not be sound. The second
example works, but because we don't support challenges on GL yet, it
doesn't actually run the second-phase witness generation.
---------
Co-authored-by: chriseth <chris@ethereum.org>
We mentioned this at the offsite so I had a go at it.
The stricter `Constr` which enforces left and right to have the same
size:
```
enum Constr {
/// A polynomial identity.
Identity(expr, expr),
/// A lookup constraint with selectors.
Lookup((Option<expr>, Option<expr>), (expr, expr)[]),
/// A permutation constraint with selectors.
Permutation((Option<expr>, Option<expr>), (expr, expr)[]),
/// A connection constraint (copy constraint).
Connection((expr, expr)[])
}
```
This could eventually be made clearer with structs.
This simulates one approach we could go for when moving registers to
memory. The memory machine remains completely unchanged, but the step is
increased by more than 1 in each step of the main machine. This way,
from the point of view of memory, all the memory operations happen at
different time steps, which allows for:
- Reading from the same address twice
- Writing to the same address that we read from (which from the point of
view of memory should happen *after* the read)
The only downside I see with this approach is that this makes the
differences of time steps between memory accesses bigger: Before it was
at most the degree, now it is some small constant times the degree (in
this example 3). The way the memory machine is currently built, the
difference can be at most $2^{32} - 1$, so I think this is fine in
practice. E.g., for a degree $2^{30}$ machine we could do up to 4
parallel reads / writes.
This fixes a soundness bug in the recently added permutation argument:
To fingerprint a list $A = (a_1, ..., a_n)$ with selectors $S = (s_1,
..., s_n)$, we were computing:
$$
\prod_{i = 1}^n (X - s_i \cdot a_i)
$$
As a result, any element $a_i$ can be replaced with $0$, by setting the
selector to $0$!
Now, an element $i$ with $s_i = 0$ does not contribute to the product
anymore:
$$
\prod_{i = 1}^n (s_i \cdot (X - a_i - 1) + 1)
$$
Depends on #1346
Adds a module to the standard library to implement extension field
arithmetic. This should work and be correct on both the Goldilocks and
BN254 field. Needed for #1306.
---------
Co-authored-by: chriseth <chris@ethereum.org>
Similar to what we have in Rust, this adds a function that detects
"known" fields (Goldilocks and BN254 for now). Planning to use that in
#1310 to assert that the field extension module is only used with
compatible fields.
Fixes#844
This PR adds a new machine to the STD: `WriteOnceMemory`. This can be
used in our RISC-V machine for bootloader inputs (#1203).
Most of the issues mentioned in the issue were fixed in the meantime or
had a simple workaround (like defining `let LATCH = 1`). The only
remaining issues were in the machine detection, which I fixed here.
I also re-factor two existing tests.
Allows braced blocks everywhere where expressions are expected.
The statements in those blocks can be `let x` or `let x = ...`.
The former declares a new witness column, the latter just binds a local
variable.
fixes#959
With the recent changes by @pacheco, we can extract our [memory
machine](https://github.com/powdr-labs/powdr/blob/main/riscv/src/compiler.rs#L687-L841)
as a separate machine and add it to the standard library.
The result should be the same as calling the function linked above with
`with_bootloader=false`, except that the memory alignment stuff is not
inlined. For this reason, the machine is not yet used by the RISC-V
machine, but it could be after #1077 is implemented.
[This](eb320dca0c) shows the diff from
what we have in `compiler.rs`.
<!--
Please follow this protocol when creating or reviewing PRs in this
repository:
- Leave the PR as draft until review is required.
- When reviewing a PR, every reviewer should assign themselves as soon
as they
start, so that other reviewers know the PR is covered. You should not be
discouraged from reviewing a PR with assignees, but you will know it is
not
strictly needed.
- Unless the PR is very small, help the reviewers by not making forced
pushes, so
that GitHub properly tracks what has been changed since the last review;
use
"merge" instead of "rebase". It can be squashed after approval.
- Once the comments have been addressed, explicitly let the reviewer
know the PR
is ready again.
-->
