Skip to content

Introducing new MInt hooks to BYTES, LIST, and MINT modules #4837

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.

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

Open
wants to merge 11 commits into
base: develop
Choose a base branch
from

Conversation

Robertorosmaninho
Copy link
Collaborator

@Robertorosmaninho Robertorosmaninho commented Jun 28, 2025

This PR intends to add these new hooks described below to make it possible to translate our KEVM's wordStack to use MInt instead of Int to get a better performance from it.

The new hooks proposed by this PR are:

1.  syntax {Width} MInt{Width} ::=MInt{Width} "^MInt" MInt{Width}
2.  syntax {Width} Bytes ::= MInt2Bytes(MInt{Width})
3.  syntax {Width} MInt{Width} ::= Bytes2MInt(Bytes)
4.  syntax {Width} MInt{Width} ::= lengthBytes(Bytes)
5.  syntax {Width} Bytes ::= padRightBytes(Bytes, length: MInt{Width}, value: MInt{Width})
6.  syntax {Width} Bytes ::= padLeftBytes(Bytes, length: MInt{Width}, value: MInt{Width})
7.  syntax {Width} Bytes ::= replaceAtBytes(dest: Bytes, index: MInt{Width}, src: Bytes)
8.  syntax {Width} Bytes ::= substrBytes(Bytes, startIndex: MInt{Width}, endIndex: MInt{Width})
9.  syntax {Width} MInt{Width} ::= Bytes "[" MInt{Width} "]"
10. syntax {Width} Bytes ::= Bytes "[" index: MInt{Width} "<-" value: MInt{Width} "]"
11. syntax {Width} MInt{Width} ::= size(List)
12. syntax {Width} List ::= List "[" index: MInt{Width} "<-" value: KItem "]"
13. syntax {Width} KItem ::= List "[" MInt{Width} "]"

Most of these hooks have an initial implementation for 64 and 256-bit integers, the necessary width for KEVM, but it's simple to add other bit widths as needed in the future!

@rv-jenkins rv-jenkins changed the base branch from master to develop June 28, 2025 15:38
@Robertorosmaninho Robertorosmaninho force-pushed the mint64-hooks branch 2 times, most recently from 8fb5336 to c92a760 Compare July 4, 2025 20:04
@Robertorosmaninho Robertorosmaninho force-pushed the mint64-hooks branch 2 times, most recently from 06a61b0 to 74fae1a Compare July 8, 2025 21:33
@Robertorosmaninho Robertorosmaninho marked this pull request as ready for review July 9, 2025 02:33
@Robertorosmaninho Robertorosmaninho self-assigned this Jul 9, 2025
@Robertorosmaninho Robertorosmaninho changed the title [WIP] Introducing new MInt hooks Introducing new MInt hooks to BYTES, LIST, and MINT modules Jul 9, 2025
Copy link
Collaborator

@theo25 theo25 left a comment

Choose a reason for hiding this comment

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

I left a couple of comments but otherwise looks good to me. There are some CI checks failing though so I won't approve until they pass.

@@ -2092,15 +2097,17 @@ of the `Bytes` term).

```k
syntax Bytes ::= Bytes "[" index: Int "<-" value: Int "]" [function, hook(BYTES.update)]
syntax {Width} Bytes ::= Bytes "[" index: MInt{Width} "<-" value: MInt{Width} "]" [function, hook(BYTES.updateMInt)]
Copy link
Collaborator

Choose a reason for hiding this comment

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

you did not mention the limitation of this working only for 64 and 256 bitwidths. Is it not limited to those?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

In this case, only 64-bit. I've updated the List module to contain the limitations for all new hooks.

@@ -1027,6 +1030,7 @@ You can get the number of elements of a list in O(1) time.

```k
syntax Int ::= size(List) [function, total, hook(LIST.size), symbol(sizeList), smtlib(smt_seq_len)]
syntax {Width} MInt{Width} ::= size(List) [function, hook(LIST.sizeMInt), symbol(sizeMInt)]
Copy link
Contributor

Choose a reason for hiding this comment

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

Note that this is a partial function, not defined for sizes greater than 2^width.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I've added a comment about this!

Copy link
Collaborator

@dwightguth dwightguth left a comment

Choose a reason for hiding this comment

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

Lgtm

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

7 participants