copy-fix-terminate: enforce secure termination of the copy circuit #1568
Conversation
github-actions
bot
added
crate-bus-mapping
There was a problem hiding this comment.
Hi @naure, Thanks for the PR, and sorry for the late review. After looking into it, I think this fix does not work. Please check my comments.
| meta.query_fixed(q_enable, Rotation(2)), | ||
| 1.expr(), |
There was a problem hiding this comment.
This is a no-op constraint. q_enable is a fixed column determined at setup time, so there is no point constraining a fixed value equal to a constant.
There was a problem hiding this comment.
I think this would make sense if q_enabled could be 0 in some of the non-padding rows, but this indeed probably shouldn't happen at all as q_enabled is a fixed column and thus determined in advance as CC pointed out - q_enabled just needs to be 1 everywhere I think (at least in some older versions of Halo2, the lookups required to have a fixed column I think, so we need to have at least one fixed column).
There was a problem hiding this comment.
It reads like this: if we are processing an event, then we are not about to hit the end of the circuit.
At the end of the circuit, q_enable switches to 0, which is how we detect the end. The rows just before that end are forced to be padding (is_event=0). This forces the last event to be fully verified by then.
There was a problem hiding this comment.
Yes, if the number of rows with q_enabled = true is constant (which it is), then I think this is all good.
There was a problem hiding this comment.
Hi @naure, what you say makes sense to me now, but I have a nitpick for readability.
It looks like if we unroll this constraint, it will be
is_event * (q_enable - 1)
Which is the same as (q_enable - 1) * is_event. The latter way fits the Selector/Fixed column first convention.
Can we rewrite it to something like this for readability?
cb.condition(meta.query_fixed(q_enable, Rotation(2)) - 1, |cb| {
cb.require_equal(
"The final step must be padding",
is_event,
0.expr(),
| // The tag is then copied to the next step by "rows[0].tag == rows[2].tag". Eventually, | ||
| // q_enable=0. By that point the tag must have switched to Padding, which is only possible with | ||
| // is_last=1. This guarantees that all the final conditions are checked. | ||
| let is_event = tag.value(Rotation::cur())(meta) - tag.constant_expr::<F>(CopyDataType::Padding); |
There was a problem hiding this comment.
tag.constant_expr::<F>(CopyDataType::Padding) part doesn't make sense to me.
Why are we binary decomposing a known value into bits, then binary composing back to constant, instead of using the known value directly?
There was a problem hiding this comment.
Indeed the constant should happen to equal Padding as u64. However, in this context the tag is not a number but a T: AsBits<N>, so this maintain the abstraction by mirroring the value() method just above.
| meta.query_fixed(q_enable, Rotation(2)), | ||
| 1.expr(), |
There was a problem hiding this comment.
Hi @naure, what you say makes sense to me now, but I have a nitpick for readability.
It looks like if we unroll this constraint, it will be
is_event * (q_enable - 1)
Which is the same as (q_enable - 1) * is_event. The latter way fits the Selector/Fixed column first convention.
Can we rewrite it to something like this for readability?
cb.condition(meta.query_fixed(q_enable, Rotation(2)) - 1, |cb| {
cb.require_equal(
"The final step must be padding",
is_event,
0.expr(),
| // The tag is then copied to the next step by "rows[0].tag == rows[2].tag". Eventually, | ||
| // q_enable=0. By that point the tag must have switched to Padding, which is only possible with | ||
| // is_last=1. This guarantees that all the final conditions are checked. | ||
| let is_event = tag.value(Rotation::cur())(meta) - tag.constant_expr::<F>(CopyDataType::Padding); |
610acc2
Description
This PR fixes two soundness issues in the Copy circuit.
There are a number of checks at the end of an event when is_last=1. However, there are no guarantees that this last row exists. The last event may not be checked fully.
The constraints may query cells of the "last two rows", whose content is not constrained. For example, booleans are not necessarily booleans there.
Type of change
Content
This is a backport from Scroll, see more details here: scroll-tech#649. Quoting:
The new constraint constrain_must_terminate guarantees that:
Now to witness generation. There must be two additional rows that are enabled so their content is verified, but not used because they touch disabled rows. See UNUSED_ROWS.
Note that there was already a sanity check that no constraints query reserved rows with the error
active on an unusable row - missing selector?. Rows can be reserved for blinding, or beyond max_rows, or simply to avoid wrap around back to the first row. This check was satisfied by adding two disabled rows (see assign_padding_row(…)). However, this alone was not sound.How Has This Been Tested?