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

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:
```k
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!

---------

Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
Co-authored-by: Julian Kuners <julian.kuners@gmail.com>

Author: 3 people

k-distribution/include/kframework/builtin/domains.md

@@ -908,6 +908,7 @@ patterns for doing so, refer to K's
 ```k
 module LIST
   imports private INT-SYNTAX
+  imports private MINT-SYNTAX
   imports private BASIC-K
 
   syntax List [hook(LIST.List)]
@@ -957,21 +958,25 @@ An element can be added to the front of a `List` using the `pushList` operator.
 ### List indexing
 
 You can get an element of a list by its integer offset in O(log(N)) time, or
-effectively constant. Positive indices are 0-indexed from the beginning of the
+effectively constant. Positive `Int` indices are 0-indexed from the beginning of the
 list, and negative indices are -1-indexed from the end of the list. In other
-words, 0 is the first element and -1 is the last element.
+words, 0 is the first element and -1 is the last element. The indice can also be
+`MInt`, which is interprested as an unsigned integer, and therefore, don't support
+negative indices feature. Currently, only 64-bit and 256-bit `MInt` types are supported.
 
 ```k
   syntax KItem ::= List "[" Int "]"           [function, hook(LIST.get), symbol(List:get)]
+  syntax {Width} KItem ::= List "[" MInt{Width} "]" [function, hook(LIST.getMInt), symbol(List:getMInt)]
 ```
 
 ### List update
 
 You can create a new `List` with a new value at a particular index in
-O(log(N)) time, or effectively constant.
+O(log(N)) time, or effectively constant. The index can be either as an `Int` or as an `MInt`. Currently, only 64-bit `MInt` type is supported.
 
 ```k
   syntax List ::= List "[" index: Int "<-" value: KItem "]" [function, hook(LIST.update), symbol(List:set)]
+  syntax {Width} List ::= List "[" index: MInt{Width} "<-" value: KItem "]" [function, hook(LIST.updateMInt), symbol(List:setMInt)]
 ```
 
 ### List of identical elements
@@ -1023,10 +1028,16 @@ comparisons, it is much better to first convert to a set using `List2Set`.
 
 ### List size
 
-You can get the number of elements of a list in O(1) time.
+You can get the number of elements of a list in O(1) time. The output
+size can be either as an `Int` or as an `MInt`. Currently, only 64-bit
+and 256-bit `MInt` types are supported. When using `MInt`, the size is
+interpreted as an unsigned integer, and the size of the list must match
+the bounds of this `MInt` type, that is the size can't be larger than
+`2^64 - 1` for `MInt{64}` and `2^256 - 1` for `MInt{256}`.
 
 ```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)]
 ```
 
 ```k
@@ -2010,6 +2021,7 @@ endmodule
 module BYTES-HOOKED
   imports STRING-SYNTAX
   imports BYTES-SYNTAX
+  imports MINT-SYNTAX
   imports BYTES-STRING-ENCODE
 ```
 
@@ -2085,22 +2097,25 @@ mutations of the input or output value.
 
 ### Bytes update
 
-You can set the value of a particular byte in a `Bytes` object in O(1) time.
-The result is `#False` if `value` is not in the range [0..255] or if `index`
-is not a valid index (ie, less than zero or greater than or equal to the length
-of the `Bytes` term).
+You can set the value of a particular byte in a `Bytes` object in O(1) time,
+either with index and value as `Int` or as an `MInt`. Currently, only 64-bit
+and 256-bit `MInt` types are supported. The result is `#False` if `value` is
+not in the range [0..255] or if `index` is not a valid index (ie, less than
+zero or greater than or equal to the length 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)]
 ```
 
 ### Bytes lookup
 
-You can get the value of a particular byte in a `Bytes` object in O(1) time.
+You can get the value of a particular byte in a `Bytes` object in O(1) time, either as an `Int` or as an `MInt`. Currently, only 64-bit and 256-bit `MInt` types are supported.
 The result is `#False` if `index` is not a valid index (see above).
 
 ```k
   syntax Int ::= Bytes "[" Int "]" [function, hook(BYTES.get)]
+  syntax {Width} MInt{Width} ::= Bytes "[" MInt{Width} "]" [function, hook(BYTES.getMInt)]
 ```
 
 ### Bytes substring
@@ -2109,9 +2124,12 @@ You can get a new `Bytes` object containing a range of bytes from the input
 `Bytes` in O(N) time (where N is the length of the substring). The range
 of bytes included is `[startIndex..endIndex)`. The resulting `Bytes` is
 a copy and mutations to it do not affect mutations to the original `Bytes`.
+Both `startIndex` and `endIndex` can be either `Int` or `MInt` values, but,
+currently, only 64-bit and 256-bit `MInt` types are supported.
 
 ```k
   syntax Bytes ::= substrBytes(Bytes, startIndex: Int, endIndex: Int) [function, hook(BYTES.substr)]
+  syntax {Width} Bytes ::= substrBytes(Bytes, startIndex: MInt{Width}, endIndex: MInt{Width}) [function, hook(BYTES.substrMInt)]
 ```
 
 The function is not total: `substrBytes(B, startIndex, endIndex)` is `#Bottom` if
@@ -2125,10 +2143,13 @@ You can modify a `Bytes` to return a `Bytes` which is equal to `dest` except the
 `N` elements starting at `index` are replaced with the contents of `src` in O(N)
 time. If `--llvm-mutable-bytes` is active, this will not create a new `Bytes`
 object and will instead modify the original on concrete backends. The result is
-`#False` if `index` + `N` is not a valid index.
+`#False` if `index` + `N` is not a valid index. This function accepts both
+`Int` and `MInt` values for `index` and `N`. Currently, only 64-bit and
+256-bit `MInt` types are supported.
 
 ```k
   syntax Bytes ::= replaceAtBytes(dest: Bytes, index: Int, src: Bytes) [function, hook(BYTES.replaceAt)]
+  syntax {Width} Bytes ::= replaceAtBytes(dest: Bytes, index: MInt{Width}, src: Bytes) [function, hook(BYTES.replaceAtMInt)]
 ```
 
 ### Multiple bytes update
@@ -2153,10 +2174,15 @@ left) with the specified `value`. If `--llvm-mutable-bytes` is active, this does
 not create a new `Bytes` object if the input is already at least `length` bytes
 long, and will instead return the input unchanged. The result is `#False` if
 `value` is not in the range `[0..255]`, or if the length is negative.
+We also provide a variant of this function which takes an `MInt` for the
+`length` and `value`. The current implementation only supports 64-bit and
+256-bit `MInt` types.
 
 ```k
   syntax Bytes ::= padRightBytes(Bytes, length: Int, value: Int) [function, hook(BYTES.padRight)]
                  | padLeftBytes(Bytes, length: Int, value: Int) [function, hook(BYTES.padLeft)]
+  syntax {Width} Bytes ::= padRightBytes(Bytes, length: MInt{Width}, value: MInt{Width}) [function, hook(BYTES.padRightMInt)]
+                         | padLeftBytes(Bytes, length: MInt{Width}, value: MInt{Width}) [function, hook(BYTES.padLeftMInt)]
 ```
 
 ### Bytes reverse
@@ -2171,10 +2197,12 @@ original.
 
 ### Bytes length
 
-You can get the length of a `Bytes` term in O(1) time.
+You can get the length of a `Bytes` term in O(1) time. The lenghth can be either
+an `Int` or an `MInt`. Currently, only 64-bit and 256-bit `MInt` types are supported.
 
 ```k
   syntax Int ::= lengthBytes(Bytes) [function, total, hook(BYTES.length), smtlib(lengthBytes)]
+  syntax {Width} MInt{Width} ::= lengthBytes(Bytes) [function, total, hook(BYTES.lengthMInt)]
 ```
 
 
@@ -2865,6 +2893,7 @@ endmodule
 module MINT
   imports MINT-SYNTAX
   imports private INT
+  imports private BYTES
   imports private BOOL
 ```
 
@@ -2896,6 +2925,14 @@ has the correct bitwidth, as this will influence the width of the resulting
   syntax {Width} MInt{Width} ::= Int2MInt(Int) [function, total, hook(MINT.integer), smt-hook(int2bv)]
 ```
 
+### Mint and Bytes conversion
+You can convert from an `MInt` to a `Bytes` using the `MInt2Bytes` function.
+Currently we only support converting `MInt`s of width 256 to `Bytes` in a Big Endian format.
+```k
+  syntax {Width} Bytes ::= MInt2Bytes(MInt{Width}) [function, total, hook(MINT.MInt2bytes)]
+  syntax {Width} MInt{Width} ::= Bytes2MInt(Bytes) [function, total, hook(MINT.bytes2MInt)] 
+```
+
 ### MInt min and max values
 
 You can get the minimum and maximum values of a signed or unsigned `MInt`
@@ -2938,6 +2975,8 @@ You can:
 
 * Compute the bitwise complement `~MInt` of an `MInt`.
 * Compute the unary negation `--MInt` of an `MInt`.
+* Compute the power `^MInt` of two `MInt`s interpreted as unsigned integers.
+  Currently, only 64 and 256-bits is supported.
 * Compute the product `*MInt` of two `MInt`s.
 * Compute the quotient `/sMInt` of two `MInt`s interpreted as signed integers.
 * Compute the modulus `%sMInt` of two `MInt`s interpreted as signed integers.
@@ -2960,7 +2999,8 @@ You can:
   syntax {Width} MInt{Width} ::= "~MInt" MInt{Width} [function, total, hook(MINT.not), smt-hook(bvnot)]
                                | "--MInt" MInt{Width} [function, total, hook(MINT.neg), smt-hook(bvuminus)]
                                > left:
-                                 MInt{Width} "*MInt" MInt{Width} [function, total, hook(MINT.mul), smt-hook(bvmul)]
+                                 MInt{Width} "^MInt" MInt{Width} [function, total, hook(MINT.pow)]
+                               | MInt{Width} "*MInt" MInt{Width} [function, total, hook(MINT.mul), smt-hook(bvmul)]
                                | MInt{Width} "/sMInt" MInt{Width} [function, hook(MINT.sdiv), smt-hook(bvsdiv)]
                                | MInt{Width} "%sMInt" MInt{Width} [function, hook(MINT.srem), smt-hook(bvsrem)]
                                | MInt{Width} "/uMInt" MInt{Width} [function, hook(MINT.udiv), smt-hook(bvudiv)]

k-distribution/tests/regression-new/checks/invalidPrec.k.out

@@ -1,5 +1,5 @@
 [Error] Compiler: Inconsistent token precedence detected.
 	Source(domains.md)
-	Location(1199,18,1199,52)
-	1199 |	  syntax Int ::= r"[0-9]+" [prefer, token, prec(2)]
+	Location(1210,18,1210,52)
+	1210 |	  syntax Int ::= r"[0-9]+" [prefer, token, prec(2)]
 	     .	                 ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

k-distribution/tests/regression-new/mint-llvm-4/1.test

@@ -0,0 +1 @@
+testBytes2MInt

k-distribution/tests/regression-new/mint-llvm-4/1.test.out

@@ -0,0 +1,3 @@
+<k>
+  true ~> .K
+</k>

k-distribution/tests/regression-new/mint-llvm-4/10.test

@@ -0,0 +1 @@
+testPadLeftBytes

k-distribution/tests/regression-new/mint-llvm-4/10.test.out

@@ -0,0 +1,3 @@
+<k>
+  true ~> .K
+</k>

k-distribution/tests/regression-new/mint-llvm-4/11.test

@@ -0,0 +1 @@
+testPadRightBytes

k-distribution/tests/regression-new/mint-llvm-4/11.test.out

@@ -0,0 +1,3 @@
+<k>
+  true ~> .K
+</k>

k-distribution/tests/regression-new/mint-llvm-4/12.test

@@ -0,0 +1 @@
+testSubstrBytes

k-distribution/tests/regression-new/mint-llvm-4/12.test.out

@@ -0,0 +1,3 @@
+<k>
+  true ~> .K
+</k>