Fixes#1190
Fixes https://github.com/powdr-labs/powdr/issues/1488
```
// creates intermediate column.
let x: inter = ...
// same here, expects an array on the rhs
let x: inter[k] = ...
// Creates an intermediate column, this is printed from Analyzed
col x = ...;
// Creates an array of intermediate columns, this is printed from analyzed and it's actually new syntax.
col x[k] = ...;
// old syntax for intermediate columns, this just defines a "generic variable" after the change,
// essentially an intermediate column that is always inlined.
let x: expr = ...;
```
---------
Co-authored-by: Leo <leo@powdrlabs.com>
Addressing #1607 -- changing the implementation for constraining public
values to reflect changes from #1543, as well as a slight refactoring of
PowdrCircuit struct to include publics.
This brings down proof and verification key sizes.
I didn't touch the eStark backends, because I think they need the JSON
file and I also got some strange errors doing the same there (couldn't
deserialize a serialized `StarkInfo`).
What we can have after this PR:
- only dynamic namespaces
- dynamic main, others dynamic or static
What we still cannot have:
- static main and another machines dynamic
The change to `_linker_first_step` can be reverted after #1565
This PR splits from the main Trait implementation PR
https://github.com/powdr-labs/powdr/pull/1450 to simplify the review
process.
It includes only the parsing of the impls (trait parsing PR here: #1489
) and some functionality necessary for the code to compile.
---------
Co-authored-by: chriseth <chris@ethereum.org>
This marks more tests as ignored because they are slow.
It also adds a list of "nightly tests", which are ignored tests that are
explicitly excluded in the regular PR runs (but executed in the nightly
run that runs all tests).
The previous version of link_merging.asm is not working correctly since
the `operation sub<1>` implementation is wrong. With this PR, `operation
sub<1>` implementation is fixed.
I started this in order to test #1603. However, due to #1604, currently
only one machine has a bus so far. This should be fixed as part of
#1604.
Then, what we would expect is that both machines have the same final
accumulator values, assuming challenges are shared across machines.
Conversion from ELF now has feature parity with conversion from
assembly, so I am setting it as the default.
---------
Co-authored-by: Leandro Pacheco <contact@leandropacheco.com>
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 continues the task to replace lookups by links. The advantages
of this approach are:
- with a link, the two machines can have different degrees and be proven
separately
- with a lookup, only a monolithic proof works
- some backends such as Plonky3 do not support lookups
- this is backwards compatible, since in the monolithic setting, links
are turned into lookups
In the compiler, we currently reduce each machine to another machine
which has only pil code and links. To this end, in the case of virtual
machines, we encode the program in fixed columns. This change introduces
a separate machine to store the ROM. Therefore, each VM gets turned into
not one, but two machines:
```
machine MyVM {
}
```
becomes
```
machine MyVM {
MyVMROM _rom;
}
machine MyVMROM {
}
```
We introduce a new name alongside the original name, which pollutes the
module. When raised, it was decided that we should not currently allow
defining the ROM machine *inside* the VM.
A better long term solution would be to have a generic `ROM` machine in
the stdlib which can be instantiated with the fixed columns which encode
the program, using them in the `get_line` operation. There are a few
missing pieces in the asm language to enable that.
A new iteration of #1476.
These added tests demonstrate that #1488 is *mostly* solved (see [this
comment](https://github.com/powdr-labs/powdr/issues/1488#issuecomment-2220759508)
though): We parse, optimize, serialize, and re-parse all test files. A
small number of test files need to be blacklisted for reasons explained
in the comments.
Computes & prints the maximum degree of any identity for every machine.
Example output for Keccak:
```
Instantiating a composite backend with 7 machines:
* main:
* Number of witness columns: 247
* Number of fixed columns: 195
* Maximum identity degree: 4
* Number of identities:
* Polynomial: 68
* Plookup: 16
* main_binary:
* Number of witness columns: 9
* Number of fixed columns: 2
* Maximum identity degree: 2
* Number of identities:
* Polynomial: 8
* main_binary_byte_binary:
* Number of witness columns: 1
* Number of fixed columns: 4
* Maximum identity degree: 1
* Number of identities:
* Polynomial: 1
* main_memory:
* Number of witness columns: 9
* Number of fixed columns: 2
* Maximum identity degree: 3
* Number of identities:
* Polynomial: 12
* Plookup: 2
* main_shift:
* Number of witness columns: 8
* Number of fixed columns: 3
* Maximum identity degree: 2
* Number of identities:
* Polynomial: 7
* main_shift_byte_shift:
* Number of witness columns: 1
* Number of fixed columns: 5
* Maximum identity degree: 1
* Number of identities:
* Polynomial: 1
* main_split_gl:
* Number of witness columns: 9
* Number of fixed columns: 9
* Maximum identity degree: 3
* Number of identities:
* Polynomial: 7
* Plookup: 1
```
This PR contains the following changes:
- I renamed a bunch of functions `verify_*` to `run_pilcom_*`, because I
think it better describes what they do
- They all call `run_pilcom_with_backend_variant`, which works analogous
to `gen_estark_proof_with_backend_variant` and
`test_halo2_with_backend_variant`
- In functions like `run_pilcom_test_file` (previously
`verify_test_file`), which are used for many tests, we now test both the
monolithic and composite backend variant (but share the generated
witness & constants). This is anlogous to `gen_estark_proof` and
`test_halo2`
- In the RISC-V tests, we only test the composite variant, because with
registers in memory (#1443) we don't expect the monolithic backend
variant to work anymore.
Related to the issue of implementing basic bus (#1497), I have
implemented basic bus together with an example
(`permutation_via_bus.asm`) as specified inside the issue.
Currently, `test_data/std/bus_permutation_via_challenges.asm` works as
intended (To make it sound, stage(1) witness columns need to be exposed
publicly and verifier needs to check such as `out_z1 + out_z2 = 0`) We
can now check using RUST_LOG=trace and adding the final z1 and z2 is
equal to 0.
However, `test_data/std/bus_permutation_via_challenges_ext.asm` is not
working correctly as intended. This will be fixed with the following
commits.
This should help us to collect more data and get a better understanding
of the factors that drive proof times and sizes.
Example:
```
$ cargo run pil test_data/asm/block_to_block.asm -o output -f --field bn254 --prove-with halo2-composite
...
Instantiating a composite backend with 2 machines:
* main:
* Number of witness columns: 3
* Number of fixed columns: 4
* Number of identities:
* Polynomial: 3
* main_arith:
* Number of witness columns: 4
* Number of fixed columns: 0
* Number of identities:
* Polynomial: 2
== Proving machine: main (size 8)
Starting proof generation...
Generating PK for snark...
Generating proof...
Time taken: 151.890834ms
Proof generation done.
==> Machine proof of 1753 bytes computed in 292.9045ms
== Proving machine: main_arith (size 8)
Starting proof generation...
Generating PK for snark...
Generating proof...
Time taken: 154.678333ms
Proof generation done.
==> Machine proof of 1625 bytes computed in 276.353375ms
Proof generation took 0.5694918s
Proof size: 3402 bytes
Writing output/block_to_block_proof.bin.
```
Also in preparation for registers in memory.
Removing the `public`s for continuations as discussed with @georgwiese ,
since those are not sound anyway and we might change it completely soon.
