Skip to content

feat: integrate asm implementation of bin module #809

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
Merged
merged 2 commits into from
Oct 20, 2025
Merged

feat: integrate asm implementation of bin module #809

merged 2 commits into from
Oct 20, 2025

Conversation

DavePearce
Copy link
Collaborator

@DavePearce DavePearce commented Oct 20, 2025 •
edited by cursor bot
Loading

This replaces the legacy lisp constraints for the bin module with a ZK assembly implementation.

Note

Replaces the bin module with a ZKASM implementation (AND/OR/XOR/NOT/BYTE/SIGNEXTEND), adds supporting utilities/opcodes, updates hub lookups to u256 args/result, and removes legacy Lisp constraints/reftables.

  • Core (BIN):
    • Introduces bin/bin.zkasm implementing AND, OR, XOR, NOT, BYTE, SIGNEXTEND over u256.
  • Utilities:
    • Adds util/bit_xoan.zkasm (bitwise ops), util/byte.zkasm (byte extraction), util/signextend.zkasm.
  • Hub Lookups:
    • Updates hub/*/lookups/hub_into_bin.lisp to use bin.ARGUMENT_1, bin.ARGUMENT_2, bin.RES (u256), sourcing via (:: HI LO).
  • Constants:
    • Adds opcode constants in constants/evm.zkasm for SIGNEXTEND, AND, OR, XOR, NOT, BYTE.
  • Build:
    • Points BIN to bin/bin.zkasm; narrows TABLES_* to fork-specific reftables/<fork>/*.lisp.
  • Removals:
    • Deletes legacy bin/columns.lisp, bin/constraints.lisp, bin/lookups/bin_into_binreftable.lisp, and reftables/bin_reftable.lisp.

Written by Cursor Bugbot for commit 775ec5d. This will update automatically on new commits. Configure here.

@DavePearce DavePearce linked an issue Oct 20, 2025 that may be closed by this pull request
feat: use asm implementation of bin module #808
Closed
@DavePearce
integrate asm implementation of bin module
491ee34 
This replaces the legacy lisp constraints for the bin module with a ZK
assembly implementation.
@DavePearce DavePearce force-pushed the 808-feat-use-asm-implementation-of-bin-module branch from c5607fe to 491ee34 Compare October 20, 2025 03:16
cursor[bot]

This comment was marked as outdated.

Sign in to view

letypequividelespoubelles
letypequividelespoubelles approved these changes Oct 20, 2025
View reviewed changes
Copy link
Collaborator

@letypequividelespoubelles letypequividelespoubelles left a comment

Choose a reason for hiding this comment

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

Lgtm, some genuine question.
Compared to the legacy bin, his many cells / constraints do we gain ?

@DavePearce
tweak implementation of bit_xoan
775ec5d 
This teaks the implementation of the bitwise not case in bit_xoan.
@DavePearce
Copy link
Collaborator Author

Constraints for the bin module only:

(module bin)

(inputs
   (INST u8 0x16)
   (ARGUMENT_1'0 u128 0x0)
   (ARGUMENT_1'1 u128 0x0)
   (ARGUMENT_2'0 u128 0x0)
   (ARGUMENT_2'1 u128 0x0)
)

(outputs
   (RES'0 u128 0x0)
   (RES'1 u128 0x0)
)

(computed
   (inst u2 0x2)
   (n u5 0x0)
   (c0'0 u128 0x0)
   (c0'1 u123 0x0)
   (size u5 0x0)
   (c1'0 u128 0x0)
   (c1'1 u123 0x0)
   (bin>bit_xoan_u256[INST] u2 0x2)
   (bin>bit_xoan_u256[ARG_1]'0 u128 0x0)
   (bin>bit_xoan_u256[ARG_1]'1 u128 0x0)
   (bin>bit_xoan_u256[ARG_2]'0 u128 0x0)
   (bin>bit_xoan_u256[ARG_2]'1 u128 0x0)
   (bin<bit_xoan_u256[RES]'0 u128 0x0)
   (bin<bit_xoan_u256[RES]'1 u128 0x0)
   (bin>byte256[word]'0 u128 0x0)
   (bin>byte256[word]'1 u128 0x0)
   (bin>byte256[n] u5 0x0)
   (bin<byte256[res] u8 0x0)
   (bin>signextend[size] u5 0x0)
   (bin>signextend[word]'0 u128 0x0)
   (bin>signextend[word]'1 u128 0x0)
   (bin<signextend[res]'0 u128 0x0)
   (bin<signextend[res]'1 u128 0x0)
   (c$30 u123 0x0)
   (c$31 u123 0x0)
)

(compute bin)
(range INST u8)
(range ARGUMENT_1'0 u128)
(range ARGUMENT_1'1 u128)
(range ARGUMENT_2'0 u128)
(range ARGUMENT_2'1 u128)
(range RES'0 u128)
(range RES'1 u128)
(range inst u2)
(range n u5)
(range c0'0 u128)
(range c0'1 u123)
(range size u5)
(range c1'0 u128)
(range c1'1 u123)
(range bin>bit_xoan_u256[INST] u2)
(range bin>bit_xoan_u256[ARG_1]'0 u128)
(range bin>bit_xoan_u256[ARG_1]'1 u128)
(range bin>bit_xoan_u256[ARG_2]'0 u128)
(range bin>bit_xoan_u256[ARG_2]'1 u128)
(range bin<bit_xoan_u256[RES]'0 u128)
(range bin<bit_xoan_u256[RES]'1 u128)
(range bin>byte256[word]'0 u128)
(range bin>byte256[word]'1 u128)
(range bin>byte256[n] u5)
(range bin<byte256[res] u8)
(range bin>signextend[size] u5)
(range bin>signextend[word]'0 u128)
(range bin>signextend[word]'1 u128)
(range bin<signextend[res]'0 u128)
(range bin<signextend[res]'1 u128)
(range c$30 u123)
(range c$31 u123)
(lookup "bin=>bit_xoan_u256"
   ((bit_xoan_u256:$ret bit_xoan_u256:INST bit_xoan_u256:ARG_1'0 bit_xoan_u256:ARG_1'1 bit_xoan_u256:ARG_2'0 bit_xoan_u256:ARG_2'1 bit_xoan_u256:RES'0 bit_xoan_u256:RES'1))
   ((_ bin:bin>bit_xoan_u256[INST] bin:bin>bit_xoan_u256[ARG_1]'0 bin:bin>bit_xoan_u256[ARG_1]'1 bin:bin>bit_xoan_u256[ARG_2]'0 bin:bin>bit_xoan_u256[ARG_2]'1 bin:bin<bit_xoan_u256[RES]'0 bin:bin<bit_xoan_u256[RES]'1)))
(lookup "bin=>byte256"
   ((_ byte256:word'0 byte256:word'1 byte256:n byte256:res))
   ((_ bin:bin>byte256[word]'0 bin:bin>byte256[word]'1 bin:bin>byte256[n] bin:bin<byte256[res])))
(lookup "bin=>signextend"
   ((_ signextend:size signextend:word'0 signextend:word'1 signextend:res'0 signextend:res'1))
   ((_ bin:bin>signextend[size] bin:bin>signextend[word]'0 bin:bin>signextend[word]'1 bin:bin<signextend[res]'0 bin:bin<signextend[res]'1)))

(vanish "bin:pc0"
   (∧
      (if (== INST 24)
         (∧
            (== inst 0)
            (== bin>bit_xoan_u256[INST] inst)
            (== bin>bit_xoan_u256[ARG_1]'0 ARGUMENT_1'0)
            (== bin>bit_xoan_u256[ARG_1]'1 ARGUMENT_1'1)
            (== bin>bit_xoan_u256[ARG_2]'0 ARGUMENT_2'0)
            (== bin>bit_xoan_u256[ARG_2]'1 ARGUMENT_2'1)
            (== RES'0 bin<bit_xoan_u256[RES]'0)
            (== RES'1 bin<bit_xoan_u256[RES]'1)))
      (if (== INST 23)
         (∧
            (== inst 1)
            (== bin>bit_xoan_u256[INST] inst)
            (== bin>bit_xoan_u256[ARG_1]'0 ARGUMENT_1'0)
            (== bin>bit_xoan_u256[ARG_1]'1 ARGUMENT_1'1)
            (== bin>bit_xoan_u256[ARG_2]'0 ARGUMENT_2'0)
            (== bin>bit_xoan_u256[ARG_2]'1 ARGUMENT_2'1)
            (== RES'0 bin<bit_xoan_u256[RES]'0)
            (== RES'1 bin<bit_xoan_u256[RES]'1)))
      (if (== INST 22)
         (∧
            (== inst 2)
            (== bin>bit_xoan_u256[INST] inst)
            (== bin>bit_xoan_u256[ARG_1]'0 ARGUMENT_1'0)
            (== bin>bit_xoan_u256[ARG_1]'1 ARGUMENT_1'1)
            (== bin>bit_xoan_u256[ARG_2]'0 ARGUMENT_2'0)
            (== bin>bit_xoan_u256[ARG_2]'1 ARGUMENT_2'1)
            (== RES'0 bin<bit_xoan_u256[RES]'0)
            (== RES'1 bin<bit_xoan_u256[RES]'1)))
      (if (== INST 25)
         (∧
            (== inst 3)
            (== bin>bit_xoan_u256[INST] inst)
            (== bin>bit_xoan_u256[ARG_1]'0 ARGUMENT_1'0)
            (== bin>bit_xoan_u256[ARG_1]'1 ARGUMENT_1'1)
            (== bin>bit_xoan_u256[ARG_2]'0 ARGUMENT_2'0)
            (== bin>bit_xoan_u256[ARG_2]'1 ARGUMENT_2'1)
            (== RES'0 bin<bit_xoan_u256[RES]'0)
            (== RES'1 bin<bit_xoan_u256[RES]'1)))
      (if (== INST 26)
         (∧
            (== (+ n (* 32 c$30)) ARGUMENT_1'0)
            (== (+ c0'0 (* 2^128 c0'1)) (+ (* ARGUMENT_1'1 2^123) c$30))
            (if
               (∧ (== c0'0 0) (== c0'1 0))
               (∧
                  (== bin>byte256[word]'0 ARGUMENT_2'0)
                  (== bin>byte256[word]'1 ARGUMENT_2'1)
                  (== bin>byte256[n] n)
                  (== RES'0 bin<byte256[res])
                  (== RES'1 0)))
            (if
               (∨ (!= c0'0 0)
                  (∧ (== c0'0 0) (!= c0'1 0)))
               (∧ (== RES'0 0) (== RES'1 0)))))
      (if (== INST 11)
         (∧
            (== (+ size (* 32 c$31)) ARGUMENT_1'0)
            (== (+ c1'0 (* 2^128 c1'1)) (+ (* ARGUMENT_1'1 2^123) c$31))
            (if
               (∧ (== c1'0 0) (== c1'1 0))
               (∧
                  (== bin>signextend[size] size)
                  (== bin>signextend[word]'0 ARGUMENT_2'0)
                  (== bin>signextend[word]'1 ARGUMENT_2'1)
                  (== RES'0 bin<signextend[res]'0)
                  (== RES'1 bin<signextend[res]'1)))
            (if
               (∨ (!= c1'0 0)
                  (∧ (== c1'0 0) (!= c1'1 0)))
               (∧ (== RES'0 ARGUMENT_2'0) (== RES'1 ARGUMENT_2'1)))))
      (∨ (== INST 11) (== INST 22) (== INST 23) (== INST 24) (== INST 25) (== INST 26))))

Unfortunately, there are a lot of supplementary functions so making a fair comparison will be challenging.

@DavePearce DavePearce merged commit 1413e7d into master Oct 20, 2025
6 checks passed
@DavePearce DavePearce deleted the 808-feat-use-asm-implementation-of-bin-module branch October 20, 2025 21:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@cursor cursor[bot] cursor[bot] left review comments

@letypequividelespoubelles letypequividelespoubelles letypequividelespoubelles approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

feat: use asm implementation of bin module

2 participants

@DavePearce @letypequividelespoubelles