Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Witgen not working for bus in block machines #1604

Closed
georgwiese opened this issue Jul 25, 2024 · 1 comment · Fixed by #1628
Closed

Witgen not working for bus in block machines #1604

georgwiese opened this issue Jul 25, 2024 · 1 comment · Fixed by #1628
Assignees
@georgwiese
Milestone
5. Sound Vadcop

Comments

@georgwiese
Copy link
Collaborator

georgwiese commented Jul 25, 2024 •
edited
Loading

See the test added in #1605.

The bus accumulator behaves unlike other witness columns in the block machine: It's constraints are not periodic. In particular, the first accumulator value is constrained differently from the others, and also the accumulator is independent of the block size.
@georgwiese georgwiese mentioned this issue Jul 25, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Jul 25, 2024
@georgwiese
Add test using a bus in each machine (#1605)
58d405a 
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.
@georgwiese georgwiese self-assigned this Jul 29, 2024
@georgwiese georgwiese added this to the 4. Sound Vadcop milestone Jul 29, 2024
@georgwiese
Copy link
Collaborator Author

For a bit of context, the way different stages are currently handled in witgen is this:

  • Identities that reference a challenge of a later stage are removed (before machine detection). As a result, later-stage witness columns usually stay unknown and "belong" to the main machine.
  • Before returning, later-stage witness columns are filtered out.
  • When computing the next-stage witness, the previous witness is passed as an "external witness", which means that any newly allocated row will already have known values for the earlier-stage witness column.

So, if there is a bus in a block machine, in the second stage it will be detected as "belonging" to the block machine, but because the accumulator does not behave like a block machine column, things break.

I feel like the root of the problem is that splitting out machines does not make sense for later-stage witness generation. For example, in std::protocols::permutation the whole purpose of the second-stage accumulator is to combine both sides of the permutation, so it does not "belong" to any machine.

So I'll try to skip machine detection entirely in any stage but the first and treat everything as a monolithic VM.

@georgwiese georgwiese mentioned this issue Jul 30, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Aug 5, 2024
@georgwiese @leonardoalt
Fix witgen for bus accumulators (#1628)
f77c0a7 
Fixes #1604

With this PR, we bypass machine detection during witness generation of
stages > 0. See [this
comment](#1604 (comment))
for a motivation.

This currently needs to be tested manually, as follows:
```
$ RUST_LOG=trace cargo run pil test_data/asm/block_to_block_with_bus.asm -o output -f --field bn254 --prove-with halo2-mock
...
===== Summary for row 7:
    main.acc1 = 20713437912485111384541749944547180564950035591542371144095269313127123163196
    main.acc2 = 5162472027861336027760332823162682203738251621730423286600997430635718406729
    main.z = 3
    main.res = 9
    main_arith.acc1 = 1174804959354163837704655800710094523598328808873663199602934873448685332421
    main_arith.acc2 = 16725770843977939194486072922094592884810112778685611057097206755940090088888
    main_arith.acc1_next = 463668501342879563405020640323131794083013726819708055681247370540753473777
    main_arith.acc2_next = 20043340305711842349747334022818855888193664738087810292789887394167185113571
    main_arith.y = 1
    main_arith.z = 1
    main.dummy = 0
    main.acc1_next = 0
    main.acc2_next = 0
    main_arith.x = 0
    main_arith.sel[0] = 0
---------------------
...
```

Computing `main.acc1 + main_arith.acc1` and `main.acc2 +
main_arith.acc2` both yields
`21888242871839275222246405745257275088548364400416034343698204186575808495617`,
which is the BN254 scalar field prime! In other words, the partial
accumulators sum to 0.

---------

Co-authored-by: Leo <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@georgwiese georgwiese

Labels
None yet
Projects
None yet
Milestone
5. Sound Vadcop
Development

Successfully merging a pull request may close this issue.

Fix witgen for bus accumulators powdr-labs/powdr
1 participant
@georgwiese