From ccc8c36592d30706dd2b2bfc8e14eb6ffcf62be8 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 1 Jul 2025 18:51:40 +0800 Subject: [PATCH 1/4] Simp rule 4 zkevm project's `PUSH` --- .../riscv-semantics/lemmas/int-simplifications.md | 4 ++++ src/tests/integration/test-data/specs/zkevm-push.k | 12 ++++++++++++ 2 files changed, 16 insertions(+) create mode 100644 src/tests/integration/test-data/specs/zkevm-push.k diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md index 1a489d3d..c1c6b92e 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md @@ -33,6 +33,10 @@ module INT-SIMPLIFICATIONS [symbolic] [simplification] rule [int-and-add-assoc-32]: ((X &Int 4294967295) +Int Y) &Int 4294967295 => (X +Int Y) &Int 4294967295 [simplification] + rule [bytes2int-and-255]: Bytes2Int(X, LE, Unsigned) &Int 255 => Bytes2Int(X, LE, Unsigned) + requires lengthBytes(X) <=Int 1 [simplification] + rule [bytes2int-or-under-255]: Bytes2Int(b"\x00" +Bytes X, LE, Unsigned) |Int Y => Bytes2Int(Int2Bytes(Y, LE, Unsigned) +Bytes X, LE, Unsigned) + requires Y #CHECK_HALT => #HALT + 0 + + 1 |-> ((Bytes2Int(OP0, LE, Unsigned) &Int 255) < Bytes2Int(b"`" +Bytes OP0, LE, Unsigned)) + + ADDRESS(0) + requires lengthBytes(OP0) ==Int 1 +endmodule From c327e6e2fc58a2bb0969df4c0e7e8e61d0805312 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 1 Jul 2025 10:53:04 +0000 Subject: [PATCH 2/4] Set Version: 0.1.118 --- 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 8b060688..1fcba8fa 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.117 +0.1.118 diff --git a/pyproject.toml b/pyproject.toml index 99538f5f..7716c21c 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kriscv" -version = "0.1.117" +version = "0.1.118" description = "K tooling for the RISC-V architecture" readme = "README.md" requires-python = "~=3.10" diff --git a/uv.lock b/uv.lock index caf36829..c7723c7c 100644 --- a/uv.lock +++ b/uv.lock @@ -643,7 +643,7 @@ wheels = [ [[package]] name = "kriscv" -version = "0.1.117" +version = "0.1.118" source = { editable = "." } dependencies = [ { name = "filelock" }, From 218ec5cd9299bc6a692b5e72ca2e681cc867fe5c Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 1 Jul 2025 19:32:10 +0800 Subject: [PATCH 3/4] Add equality lemma for integer simplifications and update ZKEVM-PUSH test specification with a new condition for register 2. --- .../riscv-semantics/lemmas/int-simplifications.md | 10 ++++++++++ src/tests/integration/test-data/specs/zkevm-push.k | 1 + 2 files changed, 11 insertions(+) diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md index c1c6b92e..e6717ac8 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md @@ -39,6 +39,16 @@ module INT-SIMPLIFICATIONS [symbolic] requires Y + (X &Int ((1 <>Int (lengthBytes(B0) *Int 8)) ==Int Bytes2Int(B1, LE, Unsigned) + [simplification, concrete(B0)] +``` + ## Inequality Lemmas ```k diff --git a/src/tests/integration/test-data/specs/zkevm-push.k b/src/tests/integration/test-data/specs/zkevm-push.k index 9ac0763e..676699e6 100644 --- a/src/tests/integration/test-data/specs/zkevm-push.k +++ b/src/tests/integration/test-data/specs/zkevm-push.k @@ -6,6 +6,7 @@ module ZKEVM-PUSH 0 1 |-> ((Bytes2Int(OP0, LE, Unsigned) &Int 255) < Bytes2Int(b"`" +Bytes OP0, LE, Unsigned)) + 2 |-> (Bool2Word(239 ==Int Bytes2Int(b"`" +Bytes OP0, LE, Unsigned)) => 0) ADDRESS(0) requires lengthBytes(OP0) ==Int 1 From 287186ea410538596a6fe4650ffc12658223cd54 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 1 Jul 2025 20:00:29 +0800 Subject: [PATCH 4/4] Enhance integer simplifications with definedness preservation and update ZKEVM-PUSH test specification to include length condition for OP1. --- src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md | 3 ++- src/tests/integration/test-data/specs/zkevm-push.k | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md index e6717ac8..dec09d78 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md @@ -46,7 +46,8 @@ module INT-SIMPLIFICATIONS [symbolic] (X &Int ((1 <>Int (lengthBytes(B0) *Int 8)) ==Int Bytes2Int(B1, LE, Unsigned) - [simplification, concrete(B0)] + [simplification, concrete(B0), preserves-definedness] + // without preserves-definedness, the rule is not applicable to B1 == substrBytes(B2, I, J) ``` ## Inequality Lemmas diff --git a/src/tests/integration/test-data/specs/zkevm-push.k b/src/tests/integration/test-data/specs/zkevm-push.k index 676699e6..7f04bc84 100644 --- a/src/tests/integration/test-data/specs/zkevm-push.k +++ b/src/tests/integration/test-data/specs/zkevm-push.k @@ -7,7 +7,8 @@ module ZKEVM-PUSH 1 |-> ((Bytes2Int(OP0, LE, Unsigned) &Int 255) < Bytes2Int(b"`" +Bytes OP0, LE, Unsigned)) 2 |-> (Bool2Word(239 ==Int Bytes2Int(b"`" +Bytes OP0, LE, Unsigned)) => 0) + 3 |-> (Bool2Word(239 ==Int Bytes2Int(b"a" +Bytes substrBytes(OP1, 0, 1), LE, Unsigned)) => 0) ADDRESS(0) - requires lengthBytes(OP0) ==Int 1 + requires lengthBytes(OP0) ==Int 1 andBool lengthBytes(OP1) ==Int 2 endmodule