fix: constraint system fix | related fixes in copy circuit#246
Conversation
|
Sorry for the confusion. This change was actually not meant to be made. The current block of code in
I don't think it's necessary, since we are already able to concisely define our circuit (in the copy-circuit) without really needing nested conditions support. It's also in line with the |
ChihChengLiang
left a comment
There was a problem hiding this comment.
LGTM, modulo a small question.
| # 1. It can only ever be a write row, so q_step == 0 and the constraint will be satisfied. | ||
| # 2. Since `lt(..)` will still be computed, it's excepted to throw an exception since | ||
| # dst addr is a very large number: addr += (int(TxLogFieldTag.Data) << 32) + (log_id << 48) | ||
| if rows[0].is_tx_log == FQ.zero(): |
There was a problem hiding this comment.
Why don't we use with cs.condition(rows[0].is_tx_log): here
There was a problem hiding this comment.
Yes, I've documented the reason on top.
If we use:
with cs.condition(cond.expr()) as cs:
cs.constrain_equal(foo(), bar.expr())
then the foo() is still computed (even if cond is 0), just that the constraint will be satisfied.
In the case of TxLog, the addr is a very large number:
addr += (int(TxLogFieldTag.Data) << 32) + (log_id << 48)
And the lt function would panic at the assertion failure, since it's only meant to allow up to N_BYTES_MEMORY_ADDRESS = 5 bytes (it's meant to check addr < src_addr_end kind of a constraint).
Hence I used an if instead of adding a cs.condition
There was a problem hiding this comment.
Oh, I see. What do you think we change the code comment from We skip tx_log because: to We use an if instead of adding a cs.condition?
The following fixes have been made in this PR:
cs.conditionwere not raised since the__exit__did not raise them. This meant, we were never warned about nested conditions not allowed, and any constraint failure within a condition was also completely ignored.CALLDATACOPYmemory read was added even foris_pad = TrueSHA3gadget should do a copy table lookup only iflength > 0. Otherwisecopy_rwc_inc = rlc_acc = 0