Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Process identities in order (if possible) (#2323)
Needed for the automatic pre-compile experiments @leonardoalt is running. Changes the order in which **runtime** witgen for block machines processes identities. ### Motivation The problem this solves is that sometimes processing an identity has side effects, specifically links to memory: the order in which you execute them matters. In practice, this is usually not an issue, because: - In the main machine, rows are processed in order anyway, and rows correspond to time steps of the computation. - A machine like [`Keccakf16Memory`](https://github.com/powdr-labs/powdr/blob/main/std/machines/hash/keccakf16_memory.asm) only reads and writes each address once, and the value to write depends on the read value, so in order to do the write, the read needs to happen first. This is guaranteed by the current algorithm. But in the general case, there is no guarantee, because witgen doesn't know about the notion of time. For example, if the value written is a constant, it can be executed by witgen as soon as the address is known, even if there is also a read of a smaller time step. The workaround that this PR implements is that identities are processed *in the order they appear in PIL*, as much as possible. In particular, an identity will only be processed, if no previous identity (or the outer query or any prover function) led to a progress. With this, the user can get witgen to execute memory operations in the correct order. This issue came up by some pre-compile experiments of Leo. ### Implementation The previous algorithm processed a given row like this: ```python progress = True while progress: progress = False for identity in identities: progress |= process(identity) progress |= process(prover_queries) progress |= process(outer_query) ``` With this PR, we do this: ```python while round(): pass def round(): if process(outer_query): return True if process(prover_queries): return True for identity in identities: if process(identity): return True return False ``` What this gets us is that an identity is only executed *if no previous identity identity has made progress*. The order of identities is the order in which it appears in the PIL (I think!). This allows us to control the order in which stateful machine calls, like memory accesses, are executed. I guess this can make the solving of the first block significantly (afterwards, the sequence cache should remove any identities that did not lead to progress). As an upper bound, witgen for `test_data/std/keccakf16_memory_test.asm` takes 347s now (instead of 309 on `main`) :)
- Loading branch information