From 962d9652969119907b02514720fb09e12ceb4d4e Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 30 Jun 2025 22:14:29 +0800 Subject: [PATCH 1/5] Add simp rule 4 zkevm project's `SSTORE` --- .../lemmas/bytes-simplifications.md | 4 ++++ .../integration/test-data/specs/zkevm-sstore.k | 14 ++++++++++++++ 2 files changed, 18 insertions(+) create mode 100644 src/tests/integration/test-data/specs/zkevm-sstore.k diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md index 81e0e84f..cea2f8c8 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md @@ -43,6 +43,10 @@ module BYTES-SIMPLIFICATIONS [symbolic] rule [bytes-concat-right-assoc-symb-l]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B1), simplification(40)] rule [bytes-concat-right-assoc-symb-r]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B2), simplification(40)] rule [bytes-concat-left-assoc-conc]: B1:Bytes +Bytes (B2:Bytes +Bytes B3:Bytes) => (B1 +Bytes B2) +Bytes B3 [concrete(B1, B2), symbolic(B3), simplification(40)] + + rule [bytes-concat-substr]: substrBytes(A, I0, J0) +Bytes substrBytes(A, I1, J1) => substrBytes(A, I0, J1) + requires I0 <=Int J0 andBool I1 <=Int J1 andBool J0 ==Int I1 andBool J1 <=Int lengthBytes(A) + [simplification, preserves-definedness] ``` ## Bytes Update Lemmas diff --git a/src/tests/integration/test-data/specs/zkevm-sstore.k b/src/tests/integration/test-data/specs/zkevm-sstore.k new file mode 100644 index 00000000..8a986685 --- /dev/null +++ b/src/tests/integration/test-data/specs/zkevm-sstore.k @@ -0,0 +1,14 @@ +module ZKEVM-SSTORE + imports RISCV + + claim [id]: + #CHECK_HALT => #HALT + 0 + + #bytes(substrBytes(reverseBytes(VALUE), 0, 4) +Bytes substrBytes(reverseBytes(VALUE), 4, 8) +Bytes substrBytes(reverseBytes(VALUE), 8, 12) +Bytes substrBytes(reverseBytes(VALUE), 12, 16) +Bytes substrBytes(reverseBytes(VALUE), 16, 20) +Bytes substrBytes(reverseBytes(VALUE), 20, 24) +Bytes substrBytes(reverseBytes(VALUE), 24, 28) +Bytes substrBytes(reverseBytes(VALUE), 28, 32)) .SparseBytes + => + #bytes(reverseBytes(VALUE)) .SparseBytes + + ADDRESS ( 0 ) + requires lengthBytes(VALUE) ==Int 32 +endmodule From ef48a16ce5ee7a83106db45751584b7c6e2f7f71 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 1 Jul 2025 16:12:07 +0800 Subject: [PATCH 2/5] Add new simplification rule for concatenating byte substrings in BYTES-SIMPLIFICATIONS and update ZKEVM-SSTORE test specification to include padding bytes. --- .../kdist/riscv-semantics/lemmas/bytes-simplifications.md | 3 +++ src/tests/integration/test-data/specs/zkevm-sstore.k | 4 ++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md index cea2f8c8..69c03a6b 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md @@ -47,6 +47,9 @@ module BYTES-SIMPLIFICATIONS [symbolic] rule [bytes-concat-substr]: substrBytes(A, I0, J0) +Bytes substrBytes(A, I1, J1) => substrBytes(A, I0, J1) requires I0 <=Int J0 andBool I1 <=Int J1 andBool J0 ==Int I1 andBool J1 <=Int lengthBytes(A) [simplification, preserves-definedness] + rule [bytes-concat-substr-cxt]: substrBytes(A, I0, J0) +Bytes substrBytes(A, I1, J1) +Bytes B => substrBytes(A, I0, J1) +Bytes B + requires I0 <=Int J0 andBool I1 <=Int J1 andBool J0 ==Int I1 andBool J1 <=Int lengthBytes(A) + [simplification, preserves-definedness] ``` ## Bytes Update Lemmas diff --git a/src/tests/integration/test-data/specs/zkevm-sstore.k b/src/tests/integration/test-data/specs/zkevm-sstore.k index 8a986685..bd49ade5 100644 --- a/src/tests/integration/test-data/specs/zkevm-sstore.k +++ b/src/tests/integration/test-data/specs/zkevm-sstore.k @@ -5,9 +5,9 @@ module ZKEVM-SSTORE #CHECK_HALT => #HALT 0 - #bytes(substrBytes(reverseBytes(VALUE), 0, 4) +Bytes substrBytes(reverseBytes(VALUE), 4, 8) +Bytes substrBytes(reverseBytes(VALUE), 8, 12) +Bytes substrBytes(reverseBytes(VALUE), 12, 16) +Bytes substrBytes(reverseBytes(VALUE), 16, 20) +Bytes substrBytes(reverseBytes(VALUE), 20, 24) +Bytes substrBytes(reverseBytes(VALUE), 24, 28) +Bytes substrBytes(reverseBytes(VALUE), 28, 32)) .SparseBytes + #bytes(b"\x00\x00\x00\x00" +Bytes substrBytes(reverseBytes(VALUE), 0, 4) +Bytes substrBytes(reverseBytes(VALUE), 4, 8) +Bytes substrBytes(reverseBytes(VALUE), 8, 12) +Bytes substrBytes(reverseBytes(VALUE), 12, 16) +Bytes substrBytes(reverseBytes(VALUE), 16, 20) +Bytes substrBytes(reverseBytes(VALUE), 20, 24) +Bytes substrBytes(reverseBytes(VALUE), 24, 28) +Bytes substrBytes(reverseBytes(VALUE), 28, 32) +Bytes b"\x00\x00\x00\x00" ) .SparseBytes => - #bytes(reverseBytes(VALUE)) .SparseBytes + #bytes(b"\x00\x00\x00\x00" +Bytes reverseBytes(VALUE) +Bytes b"\x00\x00\x00\x00" ) .SparseBytes ADDRESS ( 0 ) requires lengthBytes(VALUE) ==Int 32 From ed22fe39f6d3f6852888fb2e0cbd618f801d833f Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 10 Jul 2025 08:18:46 +0000 Subject: [PATCH 3/5] 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 2e03f0fa777a92ca16f00cb80d26aafe904b3c2c Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 10 Jul 2025 16:27:15 +0800 Subject: [PATCH 4/5] Add integration test for BYTES-CONCAT-CONSECUTIVE module to validate concatenation of byte substrings and ensure correct memory representation. --- .../specs/{zkevm-sstore.k => bytes-concat-consecutive.k} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename src/tests/integration/test-data/specs/{zkevm-sstore.k => bytes-concat-consecutive.k} (95%) diff --git a/src/tests/integration/test-data/specs/zkevm-sstore.k b/src/tests/integration/test-data/specs/bytes-concat-consecutive.k similarity index 95% rename from src/tests/integration/test-data/specs/zkevm-sstore.k rename to src/tests/integration/test-data/specs/bytes-concat-consecutive.k index bd49ade5..d15135f7 100644 --- a/src/tests/integration/test-data/specs/zkevm-sstore.k +++ b/src/tests/integration/test-data/specs/bytes-concat-consecutive.k @@ -1,4 +1,4 @@ -module ZKEVM-SSTORE +module BYTES-CONCAT-CONSECUTIVE imports RISCV claim [id]: From 1fc753faee1ffecfaed1c70a06de884247107eae Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 10 Jul 2025 10:28:15 +0000 Subject: [PATCH 5/5] Set Version: 0.1.115 --- 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 c29f5f75..72400828 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.114 +0.1.115 diff --git a/pyproject.toml b/pyproject.toml index 44a23b14..40193db8 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kriscv" -version = "0.1.114" +version = "0.1.115" description = "K tooling for the RISC-V architecture" readme = "README.md" requires-python = "~=3.10" diff --git a/uv.lock b/uv.lock index 1d1bd3ce..372a9af4 100644 --- a/uv.lock +++ b/uv.lock @@ -643,7 +643,7 @@ wheels = [ [[package]] name = "kriscv" -version = "0.1.114" +version = "0.1.115" source = { editable = "." } dependencies = [ { name = "filelock" },