diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md
index ada7cad4e68..5f747f83c5d 100644
--- a/k-distribution/include/kframework/builtin/domains.md
+++ b/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)]
diff --git a/k-distribution/tests/regression-new/checks/invalidPrec.k.out b/k-distribution/tests/regression-new/checks/invalidPrec.k.out
index ff87d377d94..e38d9e7db65 100644
--- a/k-distribution/tests/regression-new/checks/invalidPrec.k.out
+++ b/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)]
. ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/1.test b/k-distribution/tests/regression-new/mint-llvm-4/1.test
new file mode 100644
index 00000000000..fe9e8f72e07
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/1.test
@@ -0,0 +1 @@
+testBytes2MInt
\ No newline at end of file
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/1.test.out b/k-distribution/tests/regression-new/mint-llvm-4/1.test.out
new file mode 100644
index 00000000000..97f10093fc4
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/1.test.out
@@ -0,0 +1,3 @@
+
+ true ~> .K
+
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/10.test b/k-distribution/tests/regression-new/mint-llvm-4/10.test
new file mode 100644
index 00000000000..f8134bf3497
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/10.test
@@ -0,0 +1 @@
+testPadLeftBytes
\ No newline at end of file
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/10.test.out b/k-distribution/tests/regression-new/mint-llvm-4/10.test.out
new file mode 100644
index 00000000000..97f10093fc4
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/10.test.out
@@ -0,0 +1,3 @@
+
+ true ~> .K
+
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/11.test b/k-distribution/tests/regression-new/mint-llvm-4/11.test
new file mode 100644
index 00000000000..f8672b412f1
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/11.test
@@ -0,0 +1 @@
+testPadRightBytes
\ No newline at end of file
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/11.test.out b/k-distribution/tests/regression-new/mint-llvm-4/11.test.out
new file mode 100644
index 00000000000..97f10093fc4
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/11.test.out
@@ -0,0 +1,3 @@
+
+ true ~> .K
+
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/12.test b/k-distribution/tests/regression-new/mint-llvm-4/12.test
new file mode 100644
index 00000000000..81c47156bb6
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/12.test
@@ -0,0 +1 @@
+testSubstrBytes
\ No newline at end of file
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/12.test.out b/k-distribution/tests/regression-new/mint-llvm-4/12.test.out
new file mode 100644
index 00000000000..97f10093fc4
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/12.test.out
@@ -0,0 +1,3 @@
+
+ true ~> .K
+
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/13.test b/k-distribution/tests/regression-new/mint-llvm-4/13.test
new file mode 100644
index 00000000000..dd849344fa5
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/13.test
@@ -0,0 +1 @@
+testReplaceAtBytes
\ No newline at end of file
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/13.test.out b/k-distribution/tests/regression-new/mint-llvm-4/13.test.out
new file mode 100644
index 00000000000..97f10093fc4
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/13.test.out
@@ -0,0 +1,3 @@
+
+ true ~> .K
+
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/2.test b/k-distribution/tests/regression-new/mint-llvm-4/2.test
new file mode 100644
index 00000000000..cc307ea5468
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/2.test
@@ -0,0 +1 @@
+testMInt2Bytes
\ No newline at end of file
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/2.test.out b/k-distribution/tests/regression-new/mint-llvm-4/2.test.out
new file mode 100644
index 00000000000..97f10093fc4
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/2.test.out
@@ -0,0 +1,3 @@
+
+ true ~> .K
+
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/3.test b/k-distribution/tests/regression-new/mint-llvm-4/3.test
new file mode 100644
index 00000000000..c3e12396bc0
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/3.test
@@ -0,0 +1 @@
+testLengthBytes
\ No newline at end of file
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/3.test.out b/k-distribution/tests/regression-new/mint-llvm-4/3.test.out
new file mode 100644
index 00000000000..97f10093fc4
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/3.test.out
@@ -0,0 +1,3 @@
+
+ true ~> .K
+
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/4.test b/k-distribution/tests/regression-new/mint-llvm-4/4.test
new file mode 100644
index 00000000000..a13d6e155eb
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/4.test
@@ -0,0 +1 @@
+testBytesGet
\ No newline at end of file
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/4.test.out b/k-distribution/tests/regression-new/mint-llvm-4/4.test.out
new file mode 100644
index 00000000000..97f10093fc4
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/4.test.out
@@ -0,0 +1,3 @@
+
+ true ~> .K
+
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/5.test b/k-distribution/tests/regression-new/mint-llvm-4/5.test
new file mode 100644
index 00000000000..661ed8dc8d9
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/5.test
@@ -0,0 +1 @@
+testBytesUpdate
\ No newline at end of file
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/5.test.out b/k-distribution/tests/regression-new/mint-llvm-4/5.test.out
new file mode 100644
index 00000000000..97f10093fc4
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/5.test.out
@@ -0,0 +1,3 @@
+
+ true ~> .K
+
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/6.test b/k-distribution/tests/regression-new/mint-llvm-4/6.test
new file mode 100644
index 00000000000..20eeb4ee2af
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/6.test
@@ -0,0 +1 @@
+getMInt
\ No newline at end of file
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/6.test.out b/k-distribution/tests/regression-new/mint-llvm-4/6.test.out
new file mode 100644
index 00000000000..97f10093fc4
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/6.test.out
@@ -0,0 +1,3 @@
+
+ true ~> .K
+
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/7.test b/k-distribution/tests/regression-new/mint-llvm-4/7.test
new file mode 100644
index 00000000000..cd0b9359dd2
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/7.test
@@ -0,0 +1 @@
+testListSize
\ No newline at end of file
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/7.test.out b/k-distribution/tests/regression-new/mint-llvm-4/7.test.out
new file mode 100644
index 00000000000..97f10093fc4
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/7.test.out
@@ -0,0 +1,3 @@
+
+ true ~> .K
+
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/8.test b/k-distribution/tests/regression-new/mint-llvm-4/8.test
new file mode 100644
index 00000000000..6172b552081
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/8.test
@@ -0,0 +1 @@
+testListUpdate
\ No newline at end of file
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/8.test.out b/k-distribution/tests/regression-new/mint-llvm-4/8.test.out
new file mode 100644
index 00000000000..97f10093fc4
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/8.test.out
@@ -0,0 +1,3 @@
+
+ true ~> .K
+
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/9.test b/k-distribution/tests/regression-new/mint-llvm-4/9.test
new file mode 100644
index 00000000000..54bd3bcbdbf
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/9.test
@@ -0,0 +1 @@
+testMIntPowAll
\ No newline at end of file
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/9.test.out b/k-distribution/tests/regression-new/mint-llvm-4/9.test.out
new file mode 100644
index 00000000000..97f10093fc4
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/9.test.out
@@ -0,0 +1,3 @@
+
+ true ~> .K
+
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/Makefile b/k-distribution/tests/regression-new/mint-llvm-4/Makefile
new file mode 100644
index 00000000000..d1e1f0afa5b
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/Makefile
@@ -0,0 +1,8 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS=--syntax-module TEST
+
+include ../../../include/kframework/ktest.mak
+
diff --git a/k-distribution/tests/regression-new/mint-llvm-4/test.k b/k-distribution/tests/regression-new/mint-llvm-4/test.k
new file mode 100644
index 00000000000..8ffc691507c
--- /dev/null
+++ b/k-distribution/tests/regression-new/mint-llvm-4/test.k
@@ -0,0 +1,124 @@
+module TEST
+
+imports INT
+imports MINT
+imports BYTES
+imports BOOL
+imports LIST
+imports K-EQUAL
+
+ syntax MInt{64}
+ syntax MInt{256}
+
+ // Fixtures
+
+ syntax Bytes ::= "bytesString1" [macro]
+ | "bytesString2" [macro]
+
+ rule bytesString1 => // Bytes must be 256 bits (32 bytes) for some tests
+ b"\x1d)0\xdd\xcc#\xeb\x14)Q\x8bAG\xcf\xd46\xa7\xdb\x8f\xc6&\xc1=N\xb6\xa4\x81%\xc2\xd2\xf4o"
+ rule bytesString2 =>
+ b"a\x00\x1b`\x00\x81`\x0b\x829\xf3`\x01`\x01Us\x8a\n\x19X\x951iBP\xd5p\x04"
+
+
+ syntax List ::= "listOfMInt" [macro]
+ rule listOfMInt => ListItem(2p64) (ListItem(3p64) (ListItem(4p64) .List))
+
+ syntax MInt{256} ::= "mintValue" [function]
+ rule mintValue => 13189850602041981829950296977395610463010118185856010131061817836684537164911p256
+
+ syntax Int ::= "intValue" [function]
+ rule intValue => 13189850602041981829950296977395610463010118185856010131061817836684537164911
+
+
+ // Tests Syntax
+ syntax Bool ::= "testBytes2MInt" [function]
+ | "testMInt2Bytes" [function]
+ | "testLengthBytes" [function]
+ | "testBytesGet" [function]
+ | "testBytesUpdate" [function]
+ | "getMInt" [function]
+ | "testListSize" [function]
+ | "testListUpdate" [function]
+ | "testMIntPow" [function]
+ | "testMIntPowZero" [function]
+ | "testMIntPowOne" [function]
+ | "testMIntPowNegative" [function]
+ | "testMIntPowAll" [function]
+ | "testPadLeftBytes" [function]
+ | "testPadRightBytes" [function]
+ | "testSubstrBytes" [function]
+ | "testReplaceAtBytes" [function]
+
+
+ // Tests Rules
+ rule testMInt2Bytes => // Only supporting 256-bit MInt for this test in Big Endian format
+ MInt2Bytes(mintValue) ==K Int2Bytes(intValue, BE, Unsigned) andBool
+ MInt2Bytes(mintValue) ==K bytesString1
+
+ rule testBytes2MInt => // Only supporting 256-bit MInt for this test in Big Endian format
+ Bytes2MInt(bytesString1)::MInt{256} ==MInt Int2MInt(Bytes2Int(bytesString1, BE, Unsigned))
+
+ rule testLengthBytes =>
+ lengthBytes(bytesString1):Int ==Int MInt2Unsigned(lengthBytes(bytesString1):MInt{64}) andBool
+ lengthBytes(bytesString1):Int ==Int MInt2Unsigned(lengthBytes(bytesString1):MInt{256})
+
+ rule testBytesGet =>
+ {bytesString2[2p64]}:>MInt{64} ==MInt Int2MInt(bytesString2[2]) andBool
+ {bytesString2[2p256]}:>MInt{256} ==MInt Int2MInt(bytesString2[2])
+
+ rule testBytesUpdate =>
+ bytesString2[2p64 <- 10p64] ==K bytesString2[2 <- 10] andBool
+ bytesString2[2p256 <- 10p256] ==K bytesString2[2 <- 10]
+
+ rule getMInt => listOfMInt[1]:KItem ==K listOfMInt[1p64]:KItem andBool
+ listOfMInt[1]:KItem ==K listOfMInt[1p256]:KItem
+
+ rule testListSize =>
+ size(listOfMInt) ==Int MInt2Unsigned(size(listOfMInt)::MInt{64}) andBool
+ size(listOfMInt) ==Int MInt2Unsigned(size(listOfMInt)::MInt{256})
+
+ // This function only support MInt{64} for now, use MInt{256} can cause undefined behavior
+ rule testListUpdate => listOfMInt[2p64 <- 10p64] ==K listOfMInt[2 <- 10p64]
+
+ rule testMIntPow =>
+ MInt2Unsigned(2p256 ^MInt 255p256) ==Int 2 ^Int 255 andBool
+ MInt2Unsigned(2p64 ^MInt 63p64) ==Int 2 ^Int 63
+
+ rule testMIntPowZero =>
+ MInt2Unsigned(2p256 ^MInt 0p256) ==Int 1 andBool
+ MInt2Unsigned(2p64 ^MInt 0p64) ==Int 1
+
+ rule testMIntPowOne =>
+ MInt2Unsigned(2p256 ^MInt 1p256) ==Int 2 andBool
+ MInt2Unsigned(2p64 ^MInt 1p64) ==Int 2
+
+ rule testMIntPowNegative =>
+ MInt2Signed(2p256 ^MInt -10p256) ==Int 0 andBool
+ MInt2Signed(2p64 ^MInt -10p64) ==Int 0
+
+ // MInt exponenciation always assume unsigned results, except for the
+ // exponentiation by zero, which is always 1.
+ rule testMIntPowAll =>
+ testMIntPow andBool testMIntPowZero andBool
+ testMIntPowOne andBool testMIntPowNegative
+
+ rule testPadLeftBytes =>
+ padLeftBytes(bytesString1, 50, 15) ==K padLeftBytes(bytesString1, 50p256, 15p256) andBool
+ padLeftBytes(bytesString1, 50, 15) ==K padLeftBytes(bytesString1, 50p64, 15p64)
+
+ rule testPadRightBytes =>
+ padRightBytes(bytesString1, 50, 15) ==K padRightBytes(bytesString1, 50p256, 15p256) andBool
+ padRightBytes(bytesString1, 50, 15) ==K padRightBytes(bytesString1, 50p64, 15p64)
+
+ rule testSubstrBytes =>
+ substrBytes(bytesString1, 0, 5) ==K substrBytes(bytesString1, 0p64, 5p64) andBool
+ substrBytes(bytesString1, 0, 5) ==K substrBytes(bytesString1, 0p256, 5p256)
+
+ rule testReplaceAtBytes =>
+ replaceAtBytes(bytesString1, 2, String2Bytes("test")) ==K
+ replaceAtBytes(bytesString1, 2p64, String2Bytes("test")) andBool
+ replaceAtBytes(bytesString1, 2, String2Bytes("test")) ==K
+ replaceAtBytes(bytesString1, 2p256, String2Bytes("test"))
+
+endmodule
\ No newline at end of file
diff --git a/pyk/src/pyk/kore/kompiled.py b/pyk/src/pyk/kore/kompiled.py
index 7bcb64e061e..6388b45886b 100644
--- a/pyk/src/pyk/kore/kompiled.py
+++ b/pyk/src/pyk/kore/kompiled.py
@@ -187,7 +187,7 @@ def _to_dict(kore: Kore) -> Any:
def _sort_from_dict(obj: Any) -> Sort:
if isinstance(obj, str):
return SortVar(obj)
- return SortApp(name=obj['name'], sorts=tuple(_to_dict(sort) for sort in obj['sorts']))
+ return SortApp(name=obj['name'], sorts=tuple(_sort_from_dict(sort) for sort in obj['sorts']))
def _symbol_decl_from_dict(dct: Any) -> SymbolDecl:
diff --git a/pyk/src/tests/integration/konvert/test_module_to_kore.py b/pyk/src/tests/integration/konvert/test_module_to_kore.py
index 70484c1f86b..94d620cb282 100644
--- a/pyk/src/tests/integration/konvert/test_module_to_kore.py
+++ b/pyk/src/tests/integration/konvert/test_module_to_kore.py
@@ -56,6 +56,7 @@ def kore_module(definition_dir: Path, definition_info: DefinitionInfo) -> Module
IGNORED_SYMBOL_ATTRS: Final = {"symbol'Kywd'"}
+@pytest.mark.skip('TODO: https://github.com/runtimeverification/k/issues/4653')
def test_module_to_kore(kast_defn: KDefinition, kore_module: Module) -> None:
# Given
expected = kore_module