Skip to content
This repository was archived by the owner on Jul 5, 2024. It is now read-only.

Refactor bytecode circuit#340

Merged
leolara merged 18 commits into
masterfrom
leo/refactor-bytecode-circuit
Dec 31, 2022
Merged

Refactor bytecode circuit#340
leolara merged 18 commits into
masterfrom
leo/refactor-bytecode-circuit

Conversation

@leolara

@leolara leolara commented Dec 13, 2022

Copy link
Copy Markdown
Contributor

Closes #151

@leolara leolara force-pushed the leo/refactor-bytecode-circuit branch from cde07c3 to 4e375e3 Compare December 15, 2022 04:56
@leolara leolara marked this pull request as ready for review December 16, 2022 10:17
@leolara leolara requested a review from han0110 December 17, 2022 06:36
@andyguzmaneth

Copy link
Copy Markdown
Collaborator

@Brechtpd can you assign a reviewer to this task?

Comment thread specs/bytecode-proof.md Outdated
Comment thread specs/bytecode-proof.md Outdated
Comment thread specs/bytecode-proof.md Outdated
Comment thread specs/bytecode-proof.md Outdated
Comment thread specs/bytecode-proof.md Outdated
Comment thread specs/bytecode-proof.md Outdated
Comment thread specs/bytecode-proof.md Outdated
Comment on lines +54 to +55
if cur.q_last == 1:
assert cur.tag == BytecodeFieldTag.Header

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This doesn't seem to check that length and hash are set to the correct empty values (the to_header checks only check the current row values, and these checks are disabled on this row), so maybe only rows on not(q_last) be considered valid for lookup?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@Brechtpd

So perhaps we could have at the beginning:

if cur.q_first == 1 || cur.q_last== 1:
        assert cur.tag == BytecodeFieldTag.Header

And then apply the main rules to every row including last? That way when it loops from last to first it will check that last is empty?

Is this the right approach in your oponion?

Or how do we express that q_last is not valid for lookup?

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the approach you propose here would work perfectly if not for unusable rows. But because we still have unusable rows (because zk is enabled) this wrap around cannot be exploited easily (there are rows with random data in between the first and last rows). I think just having a q_enabled column in the circuit that is 1 on all rows with valid data (which with the current code would exclude the q_last row) would be the standard way to do it. So I would say the current code works, but just have to be careful to disable lookups on the q_last row by disabling q_enabled there, so just adding a warning in the spec I think is okay.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it'd be easier to to just make sure the length = 0 and hash = EMPTY_HASH when q_last, otherwise it seems we need to add extra computation to the table.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@han0110 @Brechtpd as the last thing that Han said is exactly the header to header check, I did that the last row does that check, as that check does not use the next row it should be ok.

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it'd be easier to to just make sure the length = 0 and hash = EMPTY_HASH when q_last, otherwise it seems we need to add extra computation to the table.

Yeah I guess the lookup table is safe to use without any additional selector as long as we ensure q_last is set to 1 at the very last usable row.

Comment thread tests/test_bytecode_circuit.py Outdated
Comment thread tests/test_bytecode_circuit.py Outdated
unroll(bytes([Opcode.ADD, Opcode.PUSH32, Opcode.ADD]), randomness),
]
verify(k, bytecodes, randomness, True)
verify(k, bytecodes, randomness, False) # Push without data must fail

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should it? I thought this was currently allowed but I could be wrong.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it allowed? Is this because we should allow invalid bytecode to run in the EVM as it would? The EVM would rise an exception and revert the transaction?

In that case perhaps we need some changes to the spec.

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As far as I know this currently is allowed, future EIPs like EIP-3670 may introduce these kinds of checks but I don't think any checks (except on total bytecode size) are currently being done.

Executing this kind of code will result in a revert (which is totally valid to do), but the bytecode of a smart contract may also just just contain sections that are never used by transactions but still needs to be loaded in.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think push without data should be allowed and it's will be padded with n zero when EVM really executes this PUSHn.

The reason this case fails here is because there will be next_push_data_left unassigned in the padding rows, we might need to assign it for the first padding row to pass the assert next.push_data_left == cur.push_data_size

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@han0110 @Brechtpd what I have done (that it seemed more semantic to me but perhaps there is something wrong) is to only assert assert next.push_data_left == when we are in a Byte -> Byte transition, please let me know if there is something wrong with this approach.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This approach also looks much better to me!

@andyguzmaneth

Copy link
Copy Markdown
Collaborator

Thanks for the review! FYI @leolara

leolara and others added 5 commits December 26, 2022 10:42
Co-authored-by: Brecht Devos <Brechtp.Devos@gmail.com>
Co-authored-by: Brecht Devos <Brechtp.Devos@gmail.com>
Co-authored-by: Brecht Devos <Brechtp.Devos@gmail.com>
Co-authored-by: Brecht Devos <Brechtp.Devos@gmail.com>
Co-authored-by: Brecht Devos <Brechtp.Devos@gmail.com>
leolara and others added 3 commits December 26, 2022 10:43
Co-authored-by: Brecht Devos <Brechtp.Devos@gmail.com>
Co-authored-by: Brecht Devos <Brechtp.Devos@gmail.com>

@han0110 han0110 left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The refactor looks really great and codes look well organized! Nice work! Only left 2 comments that might need to be addressed.

Comment on lines +54 to +55
if cur.q_last == 1:
assert cur.tag == BytecodeFieldTag.Header

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it'd be easier to to just make sure the length = 0 and hash = EMPTY_HASH when q_last, otherwise it seems we need to add extra computation to the table.

Comment thread tests/test_bytecode_circuit.py Outdated
unroll(bytes([Opcode.ADD, Opcode.PUSH32, Opcode.ADD]), randomness),
]
verify(k, bytecodes, randomness, True)
verify(k, bytecodes, randomness, False) # Push without data must fail

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think push without data should be allowed and it's will be padded with n zero when EVM really executes this PUSHn.

The reason this case fails here is because there will be next_push_data_left unassigned in the padding rows, we might need to assign it for the first padding row to pass the assert next.push_data_left == cur.push_data_size

Comment thread specs/bytecode-proof.md Outdated
@leolara

leolara commented Dec 30, 2022

Copy link
Copy Markdown
Contributor Author

@han0110 @Brechtpd please check again :-)

@han0110 han0110 left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

All LGTM now!

@Brechtpd Brechtpd left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, great work!

@leolara leolara merged commit 73060c0 into master Dec 31, 2022
@leolara leolara deleted the leo/refactor-bytecode-circuit branch December 31, 2022 01:17
@leolara

leolara commented Dec 31, 2022

Copy link
Copy Markdown
Contributor Author

Thanks @han0110 @Brechtpd @ed255

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Refactor Bytecode circuit to be a finite state machine

4 participants