Another step towards #1572
Builds on #1574
I modified witness generation as follows:
- Each machine keeps track of its current size; whenever a fixed column
value is read, it has to pass the requested size as well.
- If fixed columns are available in several sizes, witness generation
starts out by using the largest size, as before
- When finalizing a block machine, it "downsizes" the machine to the
smallest possible value
Doing this for other machine types (e.g. VM, memory, etc) should be done
in another PR.
In the `vm_to_block_dynamic_length.pil` example, witness generation now
pics the minimum size instead of the maximum size for `main_arith`
```
$ cargo run pil test_data/pil/vm_to_block_dynamic_length.pil -o output -f --field bn254 --prove-with halo2-mock-composite
...
== Proving machine: main (size 256)
==> Machine proof of 256 rows (0 bytes) computed in 60.174583ms
size: 256
Machine: main__rom
== Proving machine: main__rom (size 256)
==> Machine proof of 256 rows (0 bytes) computed in 33.310292ms
size: 32
Machine: main_arith
== Proving machine: main_arith (size 32)
==> Machine proof of 32 rows (0 bytes) computed in 2.766541ms
```
Fixes#1496
Also, a step towards #1572
This PR implements the steps needed in `CompositeBackend` to implement
dynamic VADCOP.
In summary:
- If a machines size (a.k.a. "degree") is set to `None`, fixed columns
are computed in all powers of too in some hard-coded range. This fixes
#1572. As a result, machines with a size set to `None` are available in
multiple sizes. If the size is explicitly set by the user, the machine
is only available in that one size.
- Note that the ASM linker still sets the size of machines without a
size. So, currently, this can only happen when coming from PIL directly.
- `CompositeBackend` instantiates a new backend for each machine *and
size*:
- The verification key contains a key for each machine and size.
- When proving, it it uses the backend of whatever size the witness has.
The size chosen is also stored in the proof.
- When verifying, the verification key of the reported size is used.
- Witness generation currently chooses the largest available size. This
will change in a future PR.
This is an example:
```
$ cargo run pil test_data/pil/vm_to_block_dynamic_length.pil -o output -f --field bn254 --prove-with halo2-mock-composite
...
== Proving machine: main (size 256)
==> Machine proof of 256 rows (0 bytes) computed in 209.101166ms
== Proving machine: main__rom (size 256)
==> Machine proof of 256 rows (0 bytes) computed in 226.87175ms
== Proving machine: main_arith (size 1024)
==> Machine proof of 1024 rows (0 bytes) computed in 432.807583ms
```
This PR adds `number::VariablySizedColumns`, which can store several
sizes of the same column. Currently, we always just have one size, but
as part of #1496, we can relax that.
This PR splits from the main Trait implementation PR #1450 to simplify
the review process.
It includes only the parsing of the traits (not impls) and some
functionality necessary for the code to compile.
---------
Co-authored-by: chriseth <chris@ethereum.org>
Fixes#1494
- use cbor for witness and constant files (moving polygon serialisation
to the relevant backend)
- add `degree` field on `Symbol`, inherited from the namespace degree
- have each machine in witgen operate over its own degree
- fail in the backend if we have many degrees
Just like the `VmProcessor`, with this PR the `BlockProcessor` never
processes an identity again that has been completed.
This should be a slight performance optimization (when the "default"
sequence iterator is used), but more importantly it:
- Fixes#1385
- Allows us to remove error-prone code (see below)
- Helps with witgen for stateful machines, like those who access memory
Another step towards VadCoP (#1495)
With this PR, the `CompositeBackend` splits the given PIL into multiple
machines and creates a proof for each machine.
The rough algorithm is as follows:
1. The PIL is split into namespaces
2. Any lookups or permutations that reference multiple namespaces are
removed.
3. Any other constraints that reference multiple namespaces lead to the
two namespaces being merged.
This is an example:
```
$ RUST_LOG=debug cargo run pil test_data/asm/block_to_block.asm -o output -f --prove-with halo2-composite --field bn254
...
Skipping connecting identity: main.instr_add { main.x, main.y, main.z } in 1 { main_arith.x, main_arith.y, main_arith.z };
== Proving machine: main
PIL:
namespace main(8);
col fixed x(i) { i / 4 };
col fixed y(i) { i / 4 + 1 };
col witness z;
col witness res;
col fixed latch = [0, 0, 0, 1]*;
main.res' = (1 - main.latch) * (main.res + main.z);
(1 - main.instr_add) * (main.x + main.y - main.z) = 0;
col fixed instr_add = [0, 1]*;
Starting proof generation...
Generating PK for snark...
Generating proof...
Time taken: 149.459458ms
Proof generation done.
== Proving machine: main_arith
PIL:
namespace main_arith(8);
col witness x;
col witness y;
col witness z;
main_arith.z = main_arith.x + main_arith.y;
Starting proof generation...
Generating PK for snark...
Generating proof...
Time taken: 150.752125ms
Proof generation done.
Writing output/block_to_block_proof.bin.
```
Seems seems to work across the entire codebase and allows us to create
Halo2 proofs by machine!
For STARK backends, we typically expect that IDs (e.g. Polynomial IDs,
constraint IDs, ...) are re-assigned, which is not yet happening in this
implementation. As mentioned in the comment, the easiest way to fix that
would be to fix#1488 and re-parse the PIL file.
Some witness generation fixes needed to make #1508 work:
- When we check whether we already answered the query, we assumed that
the latch row is the last row; now, we use the actual latch row.
- That same check might access any row in the last block, so now we
never finalize the last block.
This PR builds on top of #1393.
It mainly modifies the grammar by changing the way SelectedExpressions
are declared, to allow blocks to be empty.
---------
Co-authored-by: chriseth <chris@ethereum.org>
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>
*Cherry-picked b1a07bd9a7 from #1380, and
extended on it.*
Fixes#1382.
With this PR, a lookup like `selector { byte_lower + 256 * byte_upper }
in { <some other machine> }` works, even if the range constraints on
`byte_lower` and `byte_upper` are not "global". For example, they could
be implemented as `selector { byte_lower } in { BYTES }` (i.e.,
`byte_lower` is only range constrained when the machine call is active).
To make this work, I changed the `Machine::process_plookup` interface
like this:
```diff
fn process_plookup<'b, Q: QueryCallback<T>>(
&mut self,
mutable_state: &'b mut MutableState<'a, 'b, T, Q>,
identity_id: u64,
- args: &[AffineExpression<&'a AlgebraicReference, T>],
+ caller_rows: &'b RowPair<'b, 'a, T>,
) -> EvalResult<'a, T>;
```
The `RowPair` passed by the caller contains all range constraints known
at runtime. The LHS of the lookup (or permutation) is no longer
evaluated by the caller but by the callee. For this, the callee needs to
remember the identity associated with the `identity_id` (before this PR,
most machines just remembered the RHS, not the full identity). I don't
expect there to be any performance implications, because we only invoke
one machine (since #1154).
### Benchmark results
```
executor-benchmark/keccak
time: [14.609 s 14.645 s 14.678 s]
change: [-2.5984% -2.3127% -2.0090%] (p = 0.00 < 0.05)
Performance has improved.
executor-benchmark/many_chunks_chunk_0
time: [39.299 s 39.380 s 39.452 s]
change: [-3.9505% -3.6909% -3.4063%] (p = 0.00 < 0.05)
Performance has improved.
```
---------
Co-authored-by: Leo <leo@powdrlabs.com>
Cherry-picked ef6a72fcfa from #1380.
With this PR, we track whether a call to a machine led to some side
effect (e.g. added a block). In that case, the processed identity should
count has having led to some progress, even if no values were returned
to the calling machine. An example would be writing values to memory,
which does not return any values and hence does not change the state of
the caller.
Fixes an issue that @leonardoalt had on his `binary-mux2` branch.
There are two ways to have a block machine that is connected via a
permutation:
1. Use permutations `<sel> { ... } is (sub.sel * sub.LATCH) { ... }`.
This makes sure only rows where `sub.LATCH` is `1` can be selected. This
is what we do when we compile from ASM to PIL.
2. Use permutations `<sel> { ... } is sub.sel { ... }`, but also a
constraint `(1 - sub.LATCH) * sub.sel = 0`. This achieves something
similar.
The problem is that in the second case, detecting the block size is
harder, because the latch doesn't appear anywhere in the selector. So we
used to look into *all* fixed columns to detect the period. But this
includes fixed columns that might have a larger period (as is the case
for the multiplexer machine).
This PR simply removes support for the second approach. I think this is
fine in practice, as I don't see a disadvantage of the first approach
and when you come from ASM everything works as expected. I did need to
adjust `test_data/pil/block_lookup_or_permutation.pil`, which used the
second approach.
This PR is part of issue https://github.com/powdr-labs/powdr/pull/1345.
In particular, it adds the struct Number to Expressions to homogenize
the structure before including source references.
This PR attempts various issues around using challenges in hints, which
is blocking #1306:
1. Hints of later-phase witness columns are now removed in witgen, as
these columns don't need to be computed yet anyway and the hint might be
accessing a challenge that does not exist.
2. The query callback is now cloned for each phase of witness generation
(because otherwise it was only available in the first phase).
3. `SymbolicEvaluator` no longer panics when encountering challenges,
but returns an error. This evaluator is used to detect patterns in
identities, like `A' - A = 0`. This means that we can't detect patterns
in identities that involve challenges, but at least it doesn't panic.
4. `witgen::query_processor::Symbols` can now evaluate challenges.
5. `witgen::query_processor::Symbols` now also looks up intermediate
"polynomials" (which includes challenges). This is necessary because we
don't currently inline intermediate polynomials in hints (which we do
for identities).
I added a test that demonstrates that challenges can now be used in
hints.
This PR adds witness generation support for copy constraints: Whenever a
cell value is determined, this value is copied to all cells in its
equivalence class. This allows us to do witgen for arbitrary Plonkish
circuits (which would be detected as block machines) *as long as the
circuit is topologically sorted* (because otherwise, our row-by-row
solving strategy does not work.
Copy constraints are currently only supported in the language as
`connect` identities, as opposed to lists of cell pairs that belong to
the same equivalence class. Connecting this to the PIL input should be
part of another PR.
@leonardoalt got a failing assertion in one of his tests because the
rows in the Poseidon machine where exhausted. With this PR, this
situation is detected earlier, leading to a better error message:
```
=> Error: Table rows exhausted for machine Secondary machine 3: main_poseidon_gl (BlockMachine)
```
The global range constraints are now part of `FixedData`. Also, I got
rid of the row factory, anyone with a reference to `FixedData` can now
just call `Row::fresh(fixed_data, row_index)`. This simplifies things
and should help with #1276.
This is only needed for RISCV, but witgen is more general than RISCV and
should allow memory accesses anywhere, especially since we have the std
memory machine.
The RISCV executor also checks this so it won't go unchecked.
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.
With this PR, we remember the mapping from Lookup / Permutation Identity
to Machine. This is cleaner, lets us save some work when calling a
machine and allows us to fail earlier if no machine can answer the call
(at machine extraction time, rather than runtime.
Changes:
- `Machine::process_plookup()`: Instead of passing in `right` and
`kind`, machines now only receive an `IdentityId`. If the machine needs
to access any of the expressions, references to it have to be stored
with the machine.
- `Machine::identities()`: New function that lets us ask the machine for
which identities it feels respondible.
- The `Machines` struct now stores the mapping from `IdentityId` to
machine index, allowing us to replace the loop of trying all machines
with a simple call to `Machines::call()`.
- The identity kind is now also stored in `Identity::id`. Previously,
this only stored a `usize` which is not necessarily unique. As mentioned
above, this change could be merged as part of a separate PR.
#### Benchmark Results:
```
executor-benchmark/keccak
time: [8.7242 s 8.9755 s 9.3876 s]
change: [-4.7814% +0.8652% +7.4252%] (p = 0.79 > 0.05)
No change in performance detected.
executor-benchmark/many_chunks_chunk_0
time: [38.731 s 39.313 s 40.081 s]
change: [-5.6906% -3.9986% -1.8421%] (p = 0.00 < 0.05)
Performance has improved.
```
