From 36a96746fc3b573ce6c4703a71cd31df4bc2f11f Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 30 Jun 2025 15:59:33 +0800 Subject: [PATCH 1/3] Simp rules 4 zkevm project `SLOAD` --- .../riscv-semantics/lemmas/int-simplifications.md | 3 +++ src/tests/integration/test-data/specs/zkevm-sload.k | 12 ++++++++++++ 2 files changed, 15 insertions(+) create mode 100644 src/tests/integration/test-data/specs/zkevm-sload.k diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md index 1dcc1499..db470824 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md @@ -76,6 +76,9 @@ module INT-SIMPLIFICATIONS [symbolic] rule [int-or-bytes-2]: Bytes2Int(b"\x00\x00" +Bytes X, LE, Unsigned) |Int Bytes2Int(Y, LE, Unsigned) => Bytes2Int(Y +Bytes X, LE, Unsigned) requires lengthBytes(Y) ==Int 2 [simplification] + rule [int-or-bytes-2s]: Bytes2Int(b"\x00\x00" +Bytes X, LE, Unsigned) |Int Bytes2Int(Y +Bytes b"\x00\x00", LE, Unsigned) => Bytes2Int(Y +Bytes X, LE, Unsigned) + requires lengthBytes(Y) ==Int 2 andBool lengthBytes(X) ==Int 2 + [simplification] rule [int-or-bytes-3]: Bytes2Int(b"\x00\x00\x00" +Bytes X, LE, Unsigned) |Int Bytes2Int(Y, LE, Unsigned) => Bytes2Int(Y +Bytes X, LE, Unsigned) requires lengthBytes(Y) ==Int 3 [simplification] diff --git a/src/tests/integration/test-data/specs/zkevm-sload.k b/src/tests/integration/test-data/specs/zkevm-sload.k new file mode 100644 index 00000000..0d5a4248 --- /dev/null +++ b/src/tests/integration/test-data/specs/zkevm-sload.k @@ -0,0 +1,12 @@ +module ZKEVM-SLOAD + imports RISCV + + claim [id]: + #CHECK_HALT => #HALT + 0 + + 1 |-> ((Bytes2Int(b"\x00\x00" +Bytes reverseBytes(substrBytes(KEY, 16, 18)), LE, Unsigned) |Int Bytes2Int(reverseBytes(substrBytes(KEY, 18, 20)) +Bytes b"\x00\x00", LE, Unsigned)) &Int 4294967295 => Bytes2Int(reverseBytes(substrBytes(KEY, 16, 20)), LE, Unsigned)) + + ADDRESS ( 0 ) + requires lengthBytes(KEY) ==Int 32 +endmodule From 27bb929df7612c22b5828f3f54804cc3b7ffd9e0 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 10 Jul 2025 07:48:34 +0000 Subject: [PATCH 2/3] Set Version: 0.1.114 --- package/version | 2 +- pyproject.toml | 2 +- uv.lock | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index c21e67e6..c29f5f75 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.113 +0.1.114 diff --git a/pyproject.toml b/pyproject.toml index 30b13bdd..44a23b14 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kriscv" -version = "0.1.113" +version = "0.1.114" description = "K tooling for the RISC-V architecture" readme = "README.md" requires-python = "~=3.10" diff --git a/uv.lock b/uv.lock index fe1f6a2b..1d1bd3ce 100644 --- a/uv.lock +++ b/uv.lock @@ -643,7 +643,7 @@ wheels = [ [[package]] name = "kriscv" -version = "0.1.113" +version = "0.1.114" source = { editable = "." } dependencies = [ { name = "filelock" }, From b8af360a40df57651c798eaf353db015a5a8acfd Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 10 Jul 2025 16:14:05 +0800 Subject: [PATCH 3/3] Add new integration test case for INT-OR-BYTES-2S module This commit introduces a new K framework specification for the INT-OR-BYTES-2S module, which includes a claim that checks the behavior of the `#CHECK_HALT` instruction and its relation to the `#HALT` condition. The specification also includes requirements for the length of the `KEY` variable. --- .../test-data/specs/{zkevm-sload.k => int-or-bytes-2s.k} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename src/tests/integration/test-data/specs/{zkevm-sload.k => int-or-bytes-2s.k} (95%) diff --git a/src/tests/integration/test-data/specs/zkevm-sload.k b/src/tests/integration/test-data/specs/int-or-bytes-2s.k similarity index 95% rename from src/tests/integration/test-data/specs/zkevm-sload.k rename to src/tests/integration/test-data/specs/int-or-bytes-2s.k index 0d5a4248..b7beaafc 100644 --- a/src/tests/integration/test-data/specs/zkevm-sload.k +++ b/src/tests/integration/test-data/specs/int-or-bytes-2s.k @@ -1,4 +1,4 @@ -module ZKEVM-SLOAD +module INT-OR-BYTES-2S imports RISCV claim [id]: