From f60c5163a348cb2c0ba1dacc8bc695df080b528b Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 25 Jun 2025 16:23:40 +0800 Subject: [PATCH 1/7] [local] store test --- src/tests/integration/test-data/specs/xx.k | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 src/tests/integration/test-data/specs/xx.k diff --git a/src/tests/integration/test-data/specs/xx.k b/src/tests/integration/test-data/specs/xx.k new file mode 100644 index 00000000..509ab897 --- /dev/null +++ b/src/tests/integration/test-data/specs/xx.k @@ -0,0 +1,14 @@ +module XX + imports RISCV + + claim [id]: + #CHECK_HALT => #HALT + 0 + + 1 |-> (Bool2Word(0 0) + 2 |-> (Bool2Word(0 0) + + ADDRESS ( 0 ) + requires 0 <=Int X andBool X Date: Wed, 25 Jun 2025 16:43:42 +0800 Subject: [PATCH 2/7] [local] store test --- src/tests/integration/test-data/specs/xx.k | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/tests/integration/test-data/specs/xx.k b/src/tests/integration/test-data/specs/xx.k index 509ab897..c5a3f1cc 100644 --- a/src/tests/integration/test-data/specs/xx.k +++ b/src/tests/integration/test-data/specs/xx.k @@ -7,8 +7,15 @@ module XX 1 |-> (Bool2Word(0 0) 2 |-> (Bool2Word(0 0) + 3 |-> (Bool2Word(0 0) + 4 |-> (Bool2Word(0 <=Int Z &Int 4294967295) => 1) ADDRESS ( 0 ) - requires 0 <=Int X andBool X Date: Wed, 25 Jun 2025 16:43:53 +0800 Subject: [PATCH 3/7] Add &int simp rules --- src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md index 1dcc1499..22c151d4 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md @@ -39,6 +39,9 @@ module INT-SIMPLIFICATIONS [symbolic] ```k rule [int-and-ineq]: 0 <=Int A &Int B => true requires 0 <=Int A andBool 0 <=Int B [simplification] + rule [int-and-ineq-4294967295]: 0 <=Int _ &Int 4294967295 => true [simplification(45)] + rule [int-and-ineq-65535]: 0 <=Int _ &Int 65535 => true [simplification(45)] + rule [int-and-ineq-255]: 0 <=Int _ &Int 255 => true [simplification(45)] rule [int-rhs-ineq]: 0 <=Int A >>Int B => true requires 0 <=Int A andBool 0 <=Int B [simplification] rule [int-add-ineq]: A <=Int A +Int B => true requires 0 <=Int B [simplification] rule [int-add-ineq-0]: 0 <=Int A +Int B => true requires 0 <=Int A andBool 0 <=Int B [simplification] From 13503b191c8c468f528c8b19fcf06eba5db1fad1 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 25 Jun 2025 18:54:49 +0800 Subject: [PATCH 4/7] [local] delte temp test --- src/tests/integration/test-data/specs/xx.k | 21 --------------------- 1 file changed, 21 deletions(-) delete mode 100644 src/tests/integration/test-data/specs/xx.k diff --git a/src/tests/integration/test-data/specs/xx.k b/src/tests/integration/test-data/specs/xx.k deleted file mode 100644 index c5a3f1cc..00000000 --- a/src/tests/integration/test-data/specs/xx.k +++ /dev/null @@ -1,21 +0,0 @@ -module XX - imports RISCV - - claim [id]: - #CHECK_HALT => #HALT - 0 - - 1 |-> (Bool2Word(0 0) - 2 |-> (Bool2Word(0 0) - 3 |-> (Bool2Word(0 0) - 4 |-> (Bool2Word(0 <=Int Z &Int 4294967295) => 1) - - ADDRESS ( 0 ) - requires 0 <=Int X andBool 0 <=Int Y -endmodule - -0 Date: Wed, 25 Jun 2025 18:55:02 +0800 Subject: [PATCH 5/7] Add new simplification rule for integer OR operation and update lemmas module to include ZKEVM harness simplifications. --- .../lemmas/int-simplifications.md | 1 + .../kdist/riscv-semantics/lemmas/lemmas.k | 2 + .../lemmas/zkevm-harness-simplifications.md | 41 +++++++++++++++++++ .../test-data/specs/zkevm-mstore-0.k | 17 ++++++++ 4 files changed, 61 insertions(+) create mode 100644 src/kriscv/kdist/riscv-semantics/lemmas/zkevm-harness-simplifications.md create mode 100644 src/tests/integration/test-data/specs/zkevm-mstore-0.k diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md index 22c151d4..b2d486f8 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md @@ -42,6 +42,7 @@ module INT-SIMPLIFICATIONS [symbolic] rule [int-and-ineq-4294967295]: 0 <=Int _ &Int 4294967295 => true [simplification(45)] rule [int-and-ineq-65535]: 0 <=Int _ &Int 65535 => true [simplification(45)] rule [int-and-ineq-255]: 0 <=Int _ &Int 255 => true [simplification(45)] + rule [int-or-gt]: 0 true requires 0 >Int B => true requires 0 <=Int A andBool 0 <=Int B [simplification] rule [int-add-ineq]: A <=Int A +Int B => true requires 0 <=Int B [simplification] rule [int-add-ineq-0]: 0 <=Int A +Int B => true requires 0 <=Int A andBool 0 <=Int B [simplification] diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/lemmas.k b/src/kriscv/kdist/riscv-semantics/lemmas/lemmas.k index 0094d1d1..0062b65d 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/lemmas.k +++ b/src/kriscv/kdist/riscv-semantics/lemmas/lemmas.k @@ -2,10 +2,12 @@ requires "sparse-bytes-simplifications.md" requires "bytes-simplifications.md" requires "int-simplifications.md" requires "word-simplifications.md" +requires "zkevm-harness-simplifications.md" module LEMMAS imports SPARSE-BYTES-SIMPLIFICATIONS imports BYTES-SIMPLIFICATIONS imports INT-SIMPLIFICATIONS imports WORD-SIMPLIFICATIONS + imports ZKEVM-HARNESS-SIMPLIFICATIONS endmodule diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/zkevm-harness-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/zkevm-harness-simplifications.md new file mode 100644 index 00000000..d0b0559e --- /dev/null +++ b/src/kriscv/kdist/riscv-semantics/lemmas/zkevm-harness-simplifications.md @@ -0,0 +1,41 @@ +# ZKEVM Harness Simplifications + +This file contains simplification rules for the [zkevm-harness](https://github.com/runtimeverification/zkevm-harness). Although these simplification rules are not specific to this project, they are rules that were discovered to be needed within this project. However, we currently do not want to perform a comprehensive organization of rules, so we place these rules here for quick addition of simplification rules. + +Why not put them in the zkevm-harness repository? +1. We currently do not have an out-of-the-box simplification rule testing framework, so we would need to spend additional time creating a new testing framework in the zkevm-harness repository; +2. These rules actually have some general applicability, but considering performance, we may not need to adopt these rules for all verification targets. + +```k +requires "../word.md" +module ZKEVM-HARNESS-SIMPLIFICATIONS [symbolic] + imports INT + imports BYTES + imports K-EQUAL + imports BOOL + imports WORD +``` + +## MSTORE + +The following rules are required to prove the claim in `tests/integration/test-data/specs/zkevm-mstore.k`: + +```k +rule 0 true requires 0 true requires 0 <=Int A andBool 0 true requires 0 Bytes2Int (B, LE, Unsigned) [simplification(45)] +``` + +The following additional rules would be needed to handle the 5th register in the zkevm-mstore claim, but they interfere with the targeted rewriting of the 4th register. Therefore, they are not included in the module above: +``` +rule X false requires 2 ^Int (lengthBytes(B) *Int 8) -Int 1 <=Int X [simplification] +rule A A -Int C X [simplification] +``` + +```k +endmodule +``` \ No newline at end of file diff --git a/src/tests/integration/test-data/specs/zkevm-mstore-0.k b/src/tests/integration/test-data/specs/zkevm-mstore-0.k new file mode 100644 index 00000000..5120fd02 --- /dev/null +++ b/src/tests/integration/test-data/specs/zkevm-mstore-0.k @@ -0,0 +1,17 @@ +module ZKEVM-MSTORE-0 + imports RISCV + + claim [id]: + #CHECK_HALT => #HALT + 0 + + 1 |-> (Bool2Word(0 1) + 2 |-> (Bool2Word(0 <=Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned )) => 1) + 3 |-> (Bool2Word(0 1) + 4 |-> (Bool2Word(0 1) + // 5 |-> (Bool2Word(4294967295 0) + + ADDRESS ( 0 ) + requires 0 Date: Wed, 25 Jun 2025 10:56:40 +0000 Subject: [PATCH 6/7] 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" }, From 39287bf63eca1daa87bbda31759261a2c2768bac Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 25 Jun 2025 19:52:44 +0800 Subject: [PATCH 7/7] Add rules for handling 6th and 7th registers in zkevm-mstore claim and update requirements in test specification. --- .../riscv-semantics/lemmas/zkevm-harness-simplifications.md | 6 ++++++ src/tests/integration/test-data/specs/zkevm-mstore-0.k | 6 +++++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/zkevm-harness-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/zkevm-harness-simplifications.md index d0b0559e..192c4206 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/zkevm-harness-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/zkevm-harness-simplifications.md @@ -36,6 +36,12 @@ rule A A -Int C X [simplification] ``` +To handle the 6-th and 7-th registers in the zkevm-mstore claim, we need the following rules: +```k +rule Bool2Word(B) ==Int 0 => notBool B [simplification] +rule Bool2Word(B) ==Int 1 => B [simplification] +``` + ```k endmodule ``` \ No newline at end of file diff --git a/src/tests/integration/test-data/specs/zkevm-mstore-0.k b/src/tests/integration/test-data/specs/zkevm-mstore-0.k index 5120fd02..9fa0675a 100644 --- a/src/tests/integration/test-data/specs/zkevm-mstore-0.k +++ b/src/tests/integration/test-data/specs/zkevm-mstore-0.k @@ -10,8 +10,12 @@ module ZKEVM-MSTORE-0 3 |-> (Bool2Word(0 1) 4 |-> (Bool2Word(0 1) // 5 |-> (Bool2Word(4294967295 0) + 6 |-> (Bool2Word(Y <=Int Z) => 0) + 7 |-> (Bool2Word(Z <=Int 4294967295) => 1) ADDRESS ( 0 ) - requires 0