From aa76e2c64f86b85b8b75700b0c38c11d8b514835 Mon Sep 17 00:00:00 2001 From: qian-hu <88806138+qian-hu@users.noreply.github.com> Date: Fri, 26 May 2023 23:56:19 -0400 Subject: [PATCH 01/27] Add notMaxUInt constants --- include/kframework/word.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/include/kframework/word.md b/include/kframework/word.md index b8284ef254..776653843b 100644 --- a/include/kframework/word.md +++ b/include/kframework/word.md @@ -241,20 +241,32 @@ The maximum and minimum values of each type are defined below. rule maxUFixed128x10 => 3402823669209384634633746074317682114550000000000 /* ( 2^128 - 1) * 10^10 */ syntax Int ::= "notMaxUInt5" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFE0 */ + | "notMaxUInt8" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00 */ + | "notMaxUInt16" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF0000 */ + | "notMaxUInt32" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00000000 */ + | "notMaxUInt64" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF0000000000000000 */ | "notMaxUInt96" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF000000000000000000000000 */ | "notMaxUInt128" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00000000000000000000000000000000 */ | "notMaxUInt160" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFF0000000000000000000000000000000000000000 */ | "notMaxUInt192" [alias] /* FFFFFFFFFFFFFFFF000000000000000000000000000000000000000000000000 */ | "notMaxUInt208" [alias] /* FFFFFFFFFFFF0000000000000000000000000000000000000000000000000000 */ | "notMaxUInt224" [alias] /* FFFFFFFF00000000000000000000000000000000000000000000000000000000 */ + | "notMaxUInt240" [alias] /* FFFF000000000000000000000000000000000000000000000000000000000000 */ + | "notMaxUInt248" [alias] /* FF00000000000000000000000000000000000000000000000000000000000000 */ // ------------------------------------------------------------------------------------------------------------- rule notMaxUInt5 => 115792089237316195423570985008687907853269984665640564039457584007913129639904 + rule notMaxUInt8 => 115792089237316195423570985008687907853269984665640564039457584007913129639680 + rule notMaxUInt16 => 115792089237316195423570985008687907853269984665640564039457584007913129574400 + rule notMaxUInt32 => 115792089237316195423570985008687907853269984665640564039457584007908834672640 + rule notMaxUInt64 => 115792089237316195423570985008687907853269984665640564039439137263839420088320 rule notMaxUInt96 => 115792089237316195423570985008687907853269984665561335876943319670319585689600 rule notMaxUInt128 => 115792089237316195423570985008687907852929702298719625575994209400481361428480 rule notMaxUInt160 => 115792089237316195423570985007226406215939081747436879206741300988257197096960 rule notMaxUInt192 => 115792089237316195417293883273301227089434195242432897623355228563449095127040 rule notMaxUInt208 => 115792089237315784047431654707177369110974345328014318355491175612947292487680 rule notMaxUInt224 => 115792089210356248756420345214020892766250353992003419616917011526809519390720 + rule notMaxUInt240 => 115790322390251417039241401711187164934754157181743688420499462401711837020160 + rule notMaxUInt248 => 115339776388732929035197660848497720713218148788040405586178452820382218977280 syntax Int ::= "eth" [macro] | "maxBlockNum" [macro] /* 7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF == (2 ^ 256) - (2 ^ 255) - 1 */ From 8327f39ff6ad883a8881e77022b961847e7d9726 Mon Sep 17 00:00:00 2001 From: qian-hu <88806138+qian-hu@users.noreply.github.com> Date: Fri, 26 May 2023 23:57:26 -0400 Subject: [PATCH 02/27] Add bitwise-arithmetic lemmas --- .../lemmas/bitwise-simplification.k | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/include/kframework/lemmas/bitwise-simplification.k b/include/kframework/lemmas/bitwise-simplification.k index 1f21f317aa..8963194072 100644 --- a/include/kframework/lemmas/bitwise-simplification.k +++ b/include/kframework/lemmas/bitwise-simplification.k @@ -12,6 +12,9 @@ module BITWISE-SIMPLIFICATION [symbolic] rule A |Int 0 => A [simplification] rule A |Int A => A [simplification] + rule 1 |Int _ ==Int 0 => false [simplification] + rule (A |Int B) ==Int (B |Int A) => true [simplification, smt-lemma] + // ########################################################################### // bit-and // ########################################################################### @@ -20,6 +23,8 @@ module BITWISE-SIMPLIFICATION [symbolic] rule _ &Int 0 => 0 [simplification] rule A &Int A => A [simplification] + rule A &Int B => B &Int A [symbolic(A), concrete(B), simplification] + rule chop ( ( maxUInt48 &Int X:Int ) *Int Y:Int ) => ( maxUInt48 &Int X:Int ) *Int Y requires 0 <=Int X andBool 0 <=Int Y andBool Y <=Int pow208 [simplification] @@ -40,7 +45,20 @@ module BITWISE-SIMPLIFICATION [symbolic] rule [bitwise-and-lt]: (X &Int Y) true requires 0 <=Int X andBool 0 <=Int Y andBool (X true requires 0 <=Int X andBool 0 <=Int Y andBool X 0 requires #rangeUInt( 8, X) [simplification] + rule notMaxUInt16 &Int X => 0 requires #rangeUInt( 16, X) [simplification] + rule notMaxUInt32 &Int X => 0 requires #rangeUInt( 32, X) [simplification] + rule notMaxUInt64 &Int X => 0 requires #rangeUInt( 64, X) [simplification] rule notMaxUInt160 &Int X => 0 requires #rangeUInt(160, X) [simplification] + + rule notMaxUInt240 &Int (X < X < X < X requires #rangeUInt( 8, X) andBool 0 <=Int Y [simplification] + rule maxUInt16 &Int (X |Int ( notMaxUInt16 &Int Y:Int)) => X requires #rangeUInt( 16, X) andBool 0 <=Int Y [simplification] + rule maxUInt32 &Int (X |Int ( notMaxUInt32 &Int Y:Int)) => X requires #rangeUInt( 32, X) andBool 0 <=Int Y [simplification] + rule maxUInt64 &Int (X |Int ( notMaxUInt64 &Int Y:Int)) => X requires #rangeUInt( 64, X) andBool 0 <=Int Y [simplification] rule maxUInt160 &Int (X |Int (notMaxUInt160 &Int Y:Int)) => X requires #rangeUInt(160, X) andBool 0 <=Int Y [simplification] rule [lengthBytes-upInt-32-lower-bound]: @@ -52,4 +70,16 @@ module BITWISE-SIMPLIFICATION [symbolic] lengthBytes(X) +Int 32 >Int notMaxUInt5 &Int ( lengthBytes(X) +Int 31 ) => true [simplification, smt-lemma] + // ########################################################################### + // shift + // ########################################################################### + + rule (X < true requires #rangeUInt(240, X) [simplification] + rule (X < true requires #rangeUInt( 16, X) [simplification] + rule (X < true requires #rangeUInt( 8, X) [simplification] + + rule (X < true requires 0 <=Int X [simplification, smt-lemma] + + rule 0 <=Int (X < true requires 0 <=Int X andBool 0 <=Int Y [simplification] + endmodule From 26a1589af929bdfb67bf8ee52d078d208ebf641b Mon Sep 17 00:00:00 2001 From: qian-hu <88806138+qian-hu@users.noreply.github.com> Date: Sat, 27 May 2023 00:04:40 -0400 Subject: [PATCH 03/27] Upstream bytes-simplification lemmas from Wormhole --- include/kframework/lemmas/bytes-simplification.k | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/include/kframework/lemmas/bytes-simplification.k b/include/kframework/lemmas/bytes-simplification.k index 4d01ceb70c..560a9ac9d5 100644 --- a/include/kframework/lemmas/bytes-simplification.k +++ b/include/kframework/lemmas/bytes-simplification.k @@ -66,6 +66,11 @@ module BYTES-SIMPLIFICATION [symbolic] requires 0 <=Int W1 andBool 0 <=Int W2 [simplification] + rule #buf(32 , #asWord(B:Bytes)) => B requires lengthBytes(B) ==Int 32 [simplification] + + rule #buf(32, X < #buf(1, X) +Bytes #buf(31, 0) requires #rangeUInt( 8, X) [simplification] + rule #buf(32, X < #buf(2, X) +Bytes #buf(30, 0) requires #rangeUInt(16, X) [simplification] + // #range rule [range-empty]: From 22f83927da5c22a813e6ca5266ae611e3aafd801 Mon Sep 17 00:00:00 2001 From: qian-hu <88806138+qian-hu@users.noreply.github.com> Date: Sat, 27 May 2023 00:53:34 -0400 Subject: [PATCH 04/27] Upstream lemmas from Wormhole engagement --- .../lemmas/bitwise-simplification.k | 1 + .../kframework/lemmas/bytes-simplification.k | 3 ++ include/kframework/lemmas/lemmas.k | 6 +++ tests/specs/functional/lemmas-spec.k | 45 +++++++++++++++++++ 4 files changed, 55 insertions(+) diff --git a/include/kframework/lemmas/bitwise-simplification.k b/include/kframework/lemmas/bitwise-simplification.k index 8963194072..6e7d81aa60 100644 --- a/include/kframework/lemmas/bitwise-simplification.k +++ b/include/kframework/lemmas/bitwise-simplification.k @@ -55,6 +55,7 @@ module BITWISE-SIMPLIFICATION [symbolic] rule notMaxUInt240 &Int (X < X < X < X requires #rangeUInt (32, X) [simplification] rule maxUInt8 &Int (X |Int ( notMaxUInt8 &Int Y:Int)) => X requires #rangeUInt( 8, X) andBool 0 <=Int Y [simplification] rule maxUInt16 &Int (X |Int ( notMaxUInt16 &Int Y:Int)) => X requires #rangeUInt( 16, X) andBool 0 <=Int Y [simplification] rule maxUInt32 &Int (X |Int ( notMaxUInt32 &Int Y:Int)) => X requires #rangeUInt( 32, X) andBool 0 <=Int Y [simplification] diff --git a/include/kframework/lemmas/bytes-simplification.k b/include/kframework/lemmas/bytes-simplification.k index 560a9ac9d5..c80bd2f446 100644 --- a/include/kframework/lemmas/bytes-simplification.k +++ b/include/kframework/lemmas/bytes-simplification.k @@ -232,6 +232,9 @@ module BYTES-SIMPLIFICATION [symbolic] rule #padToWidth(32, #asByteStack(V)) => #buf(32, V) requires #rangeUInt(256, V) [simplification] + rule maxUInt8 &Int #asWord(B) => #asWord(#range(B ,31 ,1)) requires lengthBytes(B) ==Int 32 [simplification] + rule maxUInt16 &Int #asWord(B) => #asWord(#range(B ,30 ,2)) requires lengthBytes(B) ==Int 32 [simplification] + // #ecrec rule lengthBytes ( #ecrec ( _ , _ , _ , _ ) ) <=Int 32 => true diff --git a/include/kframework/lemmas/lemmas.k b/include/kframework/lemmas/lemmas.k index f41acbcf55..32cec9992f 100644 --- a/include/kframework/lemmas/lemmas.k +++ b/include/kframework/lemmas/lemmas.k @@ -24,6 +24,7 @@ module LEMMAS [symbolic] // chop range & simplification rule chop(I) => I requires #rangeUInt( 256 , I ) [simplification] + rule chop(I) => I modInt pow256 [simplification, smt-lemma] rule 0 <=Int chop(_V) => true [simplification, smt-lemma] rule chop(_V) true [simplification] @@ -75,6 +76,7 @@ module LEMMAS [symbolic] //Required for #Ceil(#buf) rule 0 <=Int keccak( _ ) => true [simplification] rule keccak( _ ) true [simplification] + rule keccak( _ ) ==Int maxUInt256 => false [simplification] // ######################## // Map Reasoning @@ -181,6 +183,10 @@ module LEMMAS-HASKELL [symbolic, kore] rule N modInt pow160 => N requires #rangeUInt(160, N) [simplification] + rule ( ( X modInt N ) +Int Y ) modInt N => (X +Int Y) modInt N [simplification] + + rule X xorInt maxUInt256 => maxUInt256 -Int X requires #rangeUInt(256, X) [simplification] + // ; Z3 version 4.8.12 // (set-option :smt.mbqi true) // diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k index 117d8c6e8b..da6e8902ab 100644 --- a/tests/specs/functional/lemmas-spec.k +++ b/tests/specs/functional/lemmas-spec.k @@ -307,6 +307,10 @@ module LEMMAS-SPEC claim [chop-range-inferred]: runLemma(X doneLemma(X requires #rangeUInt(256, X) andBool #rangeUInt(256, Y) andBool Y <=Int maxUInt256 /Int X + claim [chop-successor-key]: runLemma ( #lookup ( STORAGE [ chop ( KEY +Int 1 ) <- _ ] , KEY ) ) => doneLemma ( #lookup ( STORAGE , KEY ) ) ... + + claim [chop-successor]: runLemma ( chop ( KEY +Int 1 ) =/=Int KEY ) => doneLemma ( true ) ... + // #padToWidth simplification // -------------------------- @@ -331,6 +335,14 @@ module LEMMAS-SPEC claim [bytes-reassociation]: runLemma ( ((((A +Bytes B) +Bytes C) +Bytes D) +Bytes E) +Bytes F ) => doneLemma ( A +Bytes (B +Bytes (C +Bytes (D +Bytes (E +Bytes F)))) ) ... + claim [length-concat]: runLemma ( lengthBytes ( #range ( #buf ( 32 , _X ) , 3 , 29 ) +Bytes b"\x01" +Bytes #buf ( 2 , Y ) ) ) + => doneLemma ( 32 ) ... + requires #rangeUInt ( 16 , Y ) + + claim [concat-ranges]: runLemma ( #asWord ( #range ( #buf ( 32 , X ) , 0 , 29 ) +Bytes #range ( #buf ( 32 , X ) , 29 , 3 ) ) ) + => doneLemma ( X ) ... + requires #rangeUInt ( 256 , X ) + // bitwise-and identity // -------------------- @@ -399,6 +411,39 @@ module LEMMAS-SPEC claim runLemma ( N &Int maxUInt8 ) => doneLemma ( N ) ... requires #rangeUInt(8, N) claim runLemma ( maxUInt8 &Int N ) => doneLemma ( N ) ... requires #rangeUInt(8, N) + // shift + // ----- + + claim [shift-range]: runLemma ( #rangeUInt ( 256 , X < doneLemma ( true ) ... requires #rangeUInt ( 16 , X ) + + claim [shift-mod]: runLemma ( ( X < doneLemma ( X < requires #rangeUInt ( 16 , X ) + + claim [shift-248]: runLemma ( ( X < doneLemma ( true ) ... requires #rangeUInt ( 8 , X ) + + claim [lowest-8-bits]: + runLemma ( maxUInt8 &Int #asWord ( #range ( #buf ( 32 , X ) , 1 , 31 ) +Bytes #range ( #buf ( 32 , #asWord ( b"\x01" +Bytes #range ( #buf ( 32 , Y ) , 0 , 2 ) +Bytes #range ( #buf ( 32 , Z ) , 0 , 29 ) ) ) , 0 , 1 ) ) ) => + doneLemma ( 1 ) ... + + requires #rangeUInt ( 256 , X ) + andBool #rangeUInt ( 256 , Y ) + andBool #rangeUInt ( 256 , Z ) + + claim [highest-8-bits]: + runLemma ( maxUInt8 &Int #asWord ( #range ( #buf ( 32 , ( notMaxUInt248 &Int ( ( X < + doneLemma ( X ) ... + + requires #rangeUInt ( 8 , X ) + + claim [highest-16-bits]: + runLemma ( maxUInt16 &Int #asWord ( #range ( #buf ( 32 , X ) , 3 , 29 ) +Bytes b"\x01" +Bytes #range ( #buf ( 32 , ( notMaxUInt240 &Int ( ( Y < + doneLemma ( Y ) ... + + requires #rangeUInt ( 256 , X ) andBool #rangeUInt ( 16 , Y ) + + claim [one-byte-range]: + runLemma ( #asWord ( #range ( #buf ( 32 , notMaxUInt248 &Int ( X < doneLemma ( true ) ... + requires #rangeUInt ( 8 , X ) + // ecrecover // --------- From f45dcab8689a1081069c214a8841e6c2a0d6b28f Mon Sep 17 00:00:00 2001 From: devops Date: Sat, 27 May 2023 05:20:17 +0000 Subject: [PATCH 05/27] Set Version: 1.0.187 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 1b03f8c325..a0481853bf 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.186" +version = "1.0.187" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 4aa6aa8520..94d4f0453e 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.186) unstable; urgency=medium +kevm (1.0.187) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 309a6e284f..53faade98a 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.186 +1.0.187 From dcca53cc9f7d0e16bfc7ebd4f722ba3ac0696f3b Mon Sep 17 00:00:00 2001 From: qian-hu <88806138+qian-hu@users.noreply.github.com> Date: Sat, 27 May 2023 10:52:04 -0400 Subject: [PATCH 06/27] Revert "Upstream lemmas from Wormhole engagement" This reverts commit 22f83927da5c22a813e6ca5266ae611e3aafd801. --- .../lemmas/bitwise-simplification.k | 1 - .../kframework/lemmas/bytes-simplification.k | 3 -- include/kframework/lemmas/lemmas.k | 6 --- tests/specs/functional/lemmas-spec.k | 45 ------------------- 4 files changed, 55 deletions(-) diff --git a/include/kframework/lemmas/bitwise-simplification.k b/include/kframework/lemmas/bitwise-simplification.k index 6e7d81aa60..8963194072 100644 --- a/include/kframework/lemmas/bitwise-simplification.k +++ b/include/kframework/lemmas/bitwise-simplification.k @@ -55,7 +55,6 @@ module BITWISE-SIMPLIFICATION [symbolic] rule notMaxUInt240 &Int (X < X < X < X requires #rangeUInt (32, X) [simplification] rule maxUInt8 &Int (X |Int ( notMaxUInt8 &Int Y:Int)) => X requires #rangeUInt( 8, X) andBool 0 <=Int Y [simplification] rule maxUInt16 &Int (X |Int ( notMaxUInt16 &Int Y:Int)) => X requires #rangeUInt( 16, X) andBool 0 <=Int Y [simplification] rule maxUInt32 &Int (X |Int ( notMaxUInt32 &Int Y:Int)) => X requires #rangeUInt( 32, X) andBool 0 <=Int Y [simplification] diff --git a/include/kframework/lemmas/bytes-simplification.k b/include/kframework/lemmas/bytes-simplification.k index c80bd2f446..560a9ac9d5 100644 --- a/include/kframework/lemmas/bytes-simplification.k +++ b/include/kframework/lemmas/bytes-simplification.k @@ -232,9 +232,6 @@ module BYTES-SIMPLIFICATION [symbolic] rule #padToWidth(32, #asByteStack(V)) => #buf(32, V) requires #rangeUInt(256, V) [simplification] - rule maxUInt8 &Int #asWord(B) => #asWord(#range(B ,31 ,1)) requires lengthBytes(B) ==Int 32 [simplification] - rule maxUInt16 &Int #asWord(B) => #asWord(#range(B ,30 ,2)) requires lengthBytes(B) ==Int 32 [simplification] - // #ecrec rule lengthBytes ( #ecrec ( _ , _ , _ , _ ) ) <=Int 32 => true diff --git a/include/kframework/lemmas/lemmas.k b/include/kframework/lemmas/lemmas.k index 32cec9992f..f41acbcf55 100644 --- a/include/kframework/lemmas/lemmas.k +++ b/include/kframework/lemmas/lemmas.k @@ -24,7 +24,6 @@ module LEMMAS [symbolic] // chop range & simplification rule chop(I) => I requires #rangeUInt( 256 , I ) [simplification] - rule chop(I) => I modInt pow256 [simplification, smt-lemma] rule 0 <=Int chop(_V) => true [simplification, smt-lemma] rule chop(_V) true [simplification] @@ -76,7 +75,6 @@ module LEMMAS [symbolic] //Required for #Ceil(#buf) rule 0 <=Int keccak( _ ) => true [simplification] rule keccak( _ ) true [simplification] - rule keccak( _ ) ==Int maxUInt256 => false [simplification] // ######################## // Map Reasoning @@ -183,10 +181,6 @@ module LEMMAS-HASKELL [symbolic, kore] rule N modInt pow160 => N requires #rangeUInt(160, N) [simplification] - rule ( ( X modInt N ) +Int Y ) modInt N => (X +Int Y) modInt N [simplification] - - rule X xorInt maxUInt256 => maxUInt256 -Int X requires #rangeUInt(256, X) [simplification] - // ; Z3 version 4.8.12 // (set-option :smt.mbqi true) // diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k index da6e8902ab..117d8c6e8b 100644 --- a/tests/specs/functional/lemmas-spec.k +++ b/tests/specs/functional/lemmas-spec.k @@ -307,10 +307,6 @@ module LEMMAS-SPEC claim [chop-range-inferred]: runLemma(X doneLemma(X requires #rangeUInt(256, X) andBool #rangeUInt(256, Y) andBool Y <=Int maxUInt256 /Int X - claim [chop-successor-key]: runLemma ( #lookup ( STORAGE [ chop ( KEY +Int 1 ) <- _ ] , KEY ) ) => doneLemma ( #lookup ( STORAGE , KEY ) ) ... - - claim [chop-successor]: runLemma ( chop ( KEY +Int 1 ) =/=Int KEY ) => doneLemma ( true ) ... - // #padToWidth simplification // -------------------------- @@ -335,14 +331,6 @@ module LEMMAS-SPEC claim [bytes-reassociation]: runLemma ( ((((A +Bytes B) +Bytes C) +Bytes D) +Bytes E) +Bytes F ) => doneLemma ( A +Bytes (B +Bytes (C +Bytes (D +Bytes (E +Bytes F)))) ) ... - claim [length-concat]: runLemma ( lengthBytes ( #range ( #buf ( 32 , _X ) , 3 , 29 ) +Bytes b"\x01" +Bytes #buf ( 2 , Y ) ) ) - => doneLemma ( 32 ) ... - requires #rangeUInt ( 16 , Y ) - - claim [concat-ranges]: runLemma ( #asWord ( #range ( #buf ( 32 , X ) , 0 , 29 ) +Bytes #range ( #buf ( 32 , X ) , 29 , 3 ) ) ) - => doneLemma ( X ) ... - requires #rangeUInt ( 256 , X ) - // bitwise-and identity // -------------------- @@ -411,39 +399,6 @@ module LEMMAS-SPEC claim runLemma ( N &Int maxUInt8 ) => doneLemma ( N ) ... requires #rangeUInt(8, N) claim runLemma ( maxUInt8 &Int N ) => doneLemma ( N ) ... requires #rangeUInt(8, N) - // shift - // ----- - - claim [shift-range]: runLemma ( #rangeUInt ( 256 , X < doneLemma ( true ) ... requires #rangeUInt ( 16 , X ) - - claim [shift-mod]: runLemma ( ( X < doneLemma ( X < requires #rangeUInt ( 16 , X ) - - claim [shift-248]: runLemma ( ( X < doneLemma ( true ) ... requires #rangeUInt ( 8 , X ) - - claim [lowest-8-bits]: - runLemma ( maxUInt8 &Int #asWord ( #range ( #buf ( 32 , X ) , 1 , 31 ) +Bytes #range ( #buf ( 32 , #asWord ( b"\x01" +Bytes #range ( #buf ( 32 , Y ) , 0 , 2 ) +Bytes #range ( #buf ( 32 , Z ) , 0 , 29 ) ) ) , 0 , 1 ) ) ) => - doneLemma ( 1 ) ... - - requires #rangeUInt ( 256 , X ) - andBool #rangeUInt ( 256 , Y ) - andBool #rangeUInt ( 256 , Z ) - - claim [highest-8-bits]: - runLemma ( maxUInt8 &Int #asWord ( #range ( #buf ( 32 , ( notMaxUInt248 &Int ( ( X < - doneLemma ( X ) ... - - requires #rangeUInt ( 8 , X ) - - claim [highest-16-bits]: - runLemma ( maxUInt16 &Int #asWord ( #range ( #buf ( 32 , X ) , 3 , 29 ) +Bytes b"\x01" +Bytes #range ( #buf ( 32 , ( notMaxUInt240 &Int ( ( Y < - doneLemma ( Y ) ... - - requires #rangeUInt ( 256 , X ) andBool #rangeUInt ( 16 , Y ) - - claim [one-byte-range]: - runLemma ( #asWord ( #range ( #buf ( 32 , notMaxUInt248 &Int ( X < doneLemma ( true ) ... - requires #rangeUInt ( 8 , X ) - // ecrecover // --------- From a975eb5bbe4148d798d7b729a06654eab39ce176 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 14 Jun 2023 16:57:15 +0000 Subject: [PATCH 07/27] Set Version: 1.0.210 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index adfdf42175..768ad542d3 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.209" +version = "1.0.210" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 6b6f5cbeee..514fba6b15 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.209) unstable; urgency=medium +kevm (1.0.210) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index ccd4d2ae2d..47682b6723 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.209 +1.0.210 From 2f1dfaf4f05ee5b0138c46eb5c3da536a90dffd0 Mon Sep 17 00:00:00 2001 From: qian-hu <88806138+qian-hu@users.noreply.github.com> Date: Wed, 14 Jun 2023 12:57:42 -0400 Subject: [PATCH 08/27] Update include/kframework/word.md Co-authored-by: Everett Hildenbrandt --- include/kframework/word.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/include/kframework/word.md b/include/kframework/word.md index 776653843b..7bddac15e7 100644 --- a/include/kframework/word.md +++ b/include/kframework/word.md @@ -255,10 +255,10 @@ The maximum and minimum values of each type are defined below. | "notMaxUInt248" [alias] /* FF00000000000000000000000000000000000000000000000000000000000000 */ // ------------------------------------------------------------------------------------------------------------- rule notMaxUInt5 => 115792089237316195423570985008687907853269984665640564039457584007913129639904 - rule notMaxUInt8 => 115792089237316195423570985008687907853269984665640564039457584007913129639680 - rule notMaxUInt16 => 115792089237316195423570985008687907853269984665640564039457584007913129574400 - rule notMaxUInt32 => 115792089237316195423570985008687907853269984665640564039457584007908834672640 - rule notMaxUInt64 => 115792089237316195423570985008687907853269984665640564039439137263839420088320 + rule notMaxUInt8 => 115792089237316195423570985008687907853269984665640564039457584007913129639680 + rule notMaxUInt16 => 115792089237316195423570985008687907853269984665640564039457584007913129574400 + rule notMaxUInt32 => 115792089237316195423570985008687907853269984665640564039457584007908834672640 + rule notMaxUInt64 => 115792089237316195423570985008687907853269984665640564039439137263839420088320 rule notMaxUInt96 => 115792089237316195423570985008687907853269984665561335876943319670319585689600 rule notMaxUInt128 => 115792089237316195423570985008687907852929702298719625575994209400481361428480 rule notMaxUInt160 => 115792089237316195423570985007226406215939081747436879206741300988257197096960 From eab32d5e0846d1a3bede7467e22f774f4d2c499e Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 19 Jun 2023 22:43:26 +0000 Subject: [PATCH 09/27] Set Version: 1.0.211 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 768ad542d3..f735e6787a 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.210" +version = "1.0.211" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 514fba6b15..3b70a75a48 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.210) unstable; urgency=medium +kevm (1.0.211) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 47682b6723..2be0ce8ccf 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.210 +1.0.211 From 97e4f9ebad95638655fa191fe12df95da6fe150b Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 20 Jun 2023 19:00:41 +0000 Subject: [PATCH 10/27] Set Version: 1.0.212 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index f735e6787a..854bf86784 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.211" +version = "1.0.212" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 3b70a75a48..83c6c1301d 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.211) unstable; urgency=medium +kevm (1.0.212) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 2be0ce8ccf..0bc56ce003 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.211 +1.0.212 From 3a66b8e207a91e9aef3f5b830c0a66200ee210a5 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 21 Jun 2023 13:22:53 +0000 Subject: [PATCH 11/27] Set Version: 1.0.213 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index f51cd2761d..c5bfd97fc7 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.212" +version = "1.0.213" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 83c6c1301d..279ca0bed3 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.212) unstable; urgency=medium +kevm (1.0.213) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 0bc56ce003..8e8f9d43d1 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.212 +1.0.213 From c79870ec7578b31ece652cb87d9758dccd9f80ae Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 26 Jun 2023 19:34:12 +0000 Subject: [PATCH 12/27] Set Version: 1.0.219 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index b1ef85fedf..2aadea42e3 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.218" +version = "1.0.219" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 6e42ca3523..bdc59ce308 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.218) unstable; urgency=medium +kevm (1.0.219) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 4de9573d26..7249adaa72 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.218 +1.0.219 From 384077fd38c2db21e5738c38310f6fe926474726 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 4 Jul 2023 04:03:44 +0000 Subject: [PATCH 13/27] Set Version: 1.0.227 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index fd5b814f3e..2c995eb7c9 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.226" +version = "1.0.227" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 3b16f40b9f..3ffb8adab1 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.226) unstable; urgency=medium +kevm (1.0.227) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index e5a4b3e5b7..cba437c2d7 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.226 +1.0.227 From 5fd741cc1a0f790a52b624d0d0358e3717c90b5e Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 4 Jul 2023 16:04:01 +0000 Subject: [PATCH 14/27] Set Version: 1.0.228 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 302aed5242..a899171080 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.227" +version = "1.0.228" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 3ffb8adab1..92e78c9839 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.227) unstable; urgency=medium +kevm (1.0.228) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index cba437c2d7..58073fda70 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.227 +1.0.228 From e8814f36af8ef544369ec342ab3bb955ba958574 Mon Sep 17 00:00:00 2001 From: qian-hu <88806138+qian-hu@users.noreply.github.com> Date: Tue, 1 Aug 2023 13:33:30 -0400 Subject: [PATCH 15/27] generalize lemmas --- include/kframework/lemmas/bitwise-simplification.k | 6 +----- include/kframework/lemmas/bytes-simplification.k | 10 ++++++---- 2 files changed, 7 insertions(+), 9 deletions(-) diff --git a/include/kframework/lemmas/bitwise-simplification.k b/include/kframework/lemmas/bitwise-simplification.k index 8963194072..f2b32019d0 100644 --- a/include/kframework/lemmas/bitwise-simplification.k +++ b/include/kframework/lemmas/bitwise-simplification.k @@ -74,11 +74,7 @@ module BITWISE-SIMPLIFICATION [symbolic] // shift // ########################################################################### - rule (X < true requires #rangeUInt(240, X) [simplification] - rule (X < true requires #rangeUInt( 16, X) [simplification] - rule (X < true requires #rangeUInt( 8, X) [simplification] - - rule (X < true requires 0 <=Int X [simplification, smt-lemma] + rule (X < true requires 0 <=Int X andBool 0 <=Int Y andBool Y true requires 0 <=Int X andBool 0 <=Int Y [simplification] diff --git a/include/kframework/lemmas/bytes-simplification.k b/include/kframework/lemmas/bytes-simplification.k index 2ca5514ec2..8d005d3e8b 100644 --- a/include/kframework/lemmas/bytes-simplification.k +++ b/include/kframework/lemmas/bytes-simplification.k @@ -69,10 +69,12 @@ module BYTES-SIMPLIFICATION [symbolic] requires 0 <=Int W1 andBool 0 <=Int W2 [simplification] - rule #buf(32 , #asWord(B:Bytes)) => B requires lengthBytes(B) ==Int 32 [simplification] - - rule #buf(32, X < #buf(1, X) +Bytes #buf(31, 0) requires #rangeUInt( 8, X) [simplification] - rule #buf(32, X < #buf(2, X) +Bytes #buf(30, 0) requires #rangeUInt(16, X) [simplification] + rule [buf-shift]: + #buf(W:Int, X < #buf(W -Int Y, X) +Bytes #buf(Y, 0) + requires 0 <=Int W andBool W <=Int 32 + andBool 0 <=Int X andBool X Date: Tue, 1 Aug 2023 17:42:10 +0000 Subject: [PATCH 16/27] Set Version: 1.0.244 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 2b77789d12..0c8fbba93e 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.243" +version = "1.0.244" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 5242de0625..99ecd012eb 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.243) unstable; urgency=medium +kevm (1.0.244) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 2fc2871cc9..37f7a66260 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.243 \ No newline at end of file +1.0.244 From ec5beed363c92e4d0c9618a1bf0560930e7720cb Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 8 Aug 2023 17:03:15 +0000 Subject: [PATCH 17/27] Set Version: 1.0.249 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 11f9d06bd3..97ba724e17 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.248" +version = "1.0.249" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index d29d9243bf..2fef431de3 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.248) unstable; urgency=medium +kevm (1.0.249) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index e94c454622..fb8d264788 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.248 +1.0.249 From 63c4407b40f0d1ceaef7179e28dae737f33dbd6b Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 19 Sep 2023 20:46:57 +0000 Subject: [PATCH 18/27] Set Version: 1.0.296 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index a93a44ac39..260dc7ece3 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.295" +version = "1.0.296" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index db0aca2a46..cd26398c31 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.295' +VERSION: Final = '1.0.296' diff --git a/package/debian/changelog b/package/debian/changelog index 71e23d7d4a..6280244e89 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.295) unstable; urgency=medium +kevm (1.0.296) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 8628b0c583..b5d581ae64 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.295 +1.0.296 From 4a80da56aa587360fb40606ac9ec5863ab67a094 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 2 Oct 2023 08:53:34 +0000 Subject: [PATCH 19/27] Set Version: 1.0.309 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index fe9059258c..13a3cb915d 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.308" +version = "1.0.309" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index d8d62791fa..a56fa043b1 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.308' +VERSION: Final = '1.0.309' diff --git a/package/version b/package/version index 7b64a80cde..fcb1b3a84a 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.308 +1.0.309 From 8cad2bba98eb32b4534b6a24d5ea5df86d4925e9 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Mon, 2 Oct 2023 11:20:22 +0200 Subject: [PATCH 20/27] cleanup --- .../lemmas/bitwise-simplification.k | 35 ++++++++++++++----- 1 file changed, 27 insertions(+), 8 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k index f2b32019d0..dabeb175ce 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k @@ -5,25 +5,29 @@ module BITWISE-SIMPLIFICATION [symbolic] imports WORD // ########################################################################### - // inc-or + // bit-or // ########################################################################### rule 0 |Int A => A [simplification] rule A |Int 0 => A [simplification] rule A |Int A => A [simplification] - rule 1 |Int _ ==Int 0 => false [simplification] + rule A |Int B => B |Int A [simplification(40), concrete(B), symbolic(A)] + + rule X |Int _ ==Int 0 => false requires 0 true [simplification, smt-lemma] // ########################################################################### // bit-and // ########################################################################### + rule A &Int B => B &Int A [symbolic(A), concrete(B), simplification] + rule 0 &Int _ => 0 [simplification] rule _ &Int 0 => 0 [simplification] rule A &Int A => A [simplification] - rule A &Int B => B &Int A [symbolic(A), concrete(B), simplification] + rule 1 &Int X => X modInt 2 [simplification] rule chop ( ( maxUInt48 &Int X:Int ) *Int Y:Int ) => ( maxUInt48 &Int X:Int ) *Int Y requires 0 <=Int X andBool 0 <=Int Y andBool Y <=Int pow208 [simplification] @@ -46,20 +50,35 @@ module BITWISE-SIMPLIFICATION [symbolic] rule [bitwise-or-lt-pow256]: (X |Int Y) true requires 0 <=Int X andBool 0 <=Int Y andBool X 0 requires #rangeUInt( 5, X) [simplification] rule notMaxUInt8 &Int X => 0 requires #rangeUInt( 8, X) [simplification] rule notMaxUInt16 &Int X => 0 requires #rangeUInt( 16, X) [simplification] rule notMaxUInt32 &Int X => 0 requires #rangeUInt( 32, X) [simplification] rule notMaxUInt64 &Int X => 0 requires #rangeUInt( 64, X) [simplification] + rule notMaxUInt96 &Int X => 0 requires #rangeUInt( 96, X) [simplification] + rule notMaxUInt128 &Int X => 0 requires #rangeUInt(128, X) [simplification] rule notMaxUInt160 &Int X => 0 requires #rangeUInt(160, X) [simplification] + rule notMaxUInt192 &Int X => 0 requires #rangeUInt(192, X) [simplification] + rule notMaxUInt208 &Int X => 0 requires #rangeUInt(208, X) [simplification] + rule notMaxUInt224 &Int X => 0 requires #rangeUInt(224, X) [simplification] + rule notMaxUInt240 &Int X => 0 requires #rangeUInt(240, X) [simplification] + rule notMaxUInt248 &Int X => 0 requires #rangeUInt(248, X) [simplification] rule notMaxUInt240 &Int (X < X < X < X requires #rangeUInt( 8, X) andBool 0 <=Int Y [simplification] - rule maxUInt16 &Int (X |Int ( notMaxUInt16 &Int Y:Int)) => X requires #rangeUInt( 16, X) andBool 0 <=Int Y [simplification] - rule maxUInt32 &Int (X |Int ( notMaxUInt32 &Int Y:Int)) => X requires #rangeUInt( 32, X) andBool 0 <=Int Y [simplification] - rule maxUInt64 &Int (X |Int ( notMaxUInt64 &Int Y:Int)) => X requires #rangeUInt( 64, X) andBool 0 <=Int Y [simplification] - rule maxUInt160 &Int (X |Int (notMaxUInt160 &Int Y:Int)) => X requires #rangeUInt(160, X) andBool 0 <=Int Y [simplification] + rule maxUInt8 &Int (X |Int (notMaxUInt8 &Int _)) => maxUInt8 &Int X [simplification] + rule maxUInt16 &Int (X |Int (notMaxUInt16 &Int _)) => maxUInt16 &Int X [simplification] + rule maxUInt32 &Int (X |Int (notMaxUInt32 &Int _)) => maxUInt32 &Int X [simplification] + rule maxUInt64 &Int (X |Int (notMaxUInt64 &Int _)) => maxUInt64 &Int X [simplification] + rule maxUInt96 &Int (X |Int (notMaxUInt96 &Int _)) => maxUInt96 &Int X [simplification] + rule maxUInt128 &Int (X |Int (notMaxUInt128 &Int _)) => maxUInt128 &Int X [simplification] + rule maxUInt160 &Int (X |Int (notMaxUInt160 &Int _)) => maxUInt160 &Int X [simplification] + rule maxUInt192 &Int (X |Int (notMaxUInt192 &Int _)) => maxUInt192 &Int X [simplification] + rule maxUInt208 &Int (X |Int (notMaxUInt208 &Int _)) => maxUInt208 &Int X [simplification] + rule maxUInt224 &Int (X |Int (notMaxUInt224 &Int _)) => maxUInt224 &Int X [simplification] + rule maxUInt240 &Int (X |Int (notMaxUInt240 &Int _)) => maxUInt240 &Int X [simplification] + rule maxUInt248 &Int (X |Int (notMaxUInt248 &Int _)) => maxUInt248 &Int X [simplification] rule [lengthBytes-upInt-32-lower-bound]: lengthBytes(X) <=Int notMaxUInt5 &Int ( lengthBytes(X) +Int 31 ) => true From 3365bcd65579559e9f5202b199f71c4b0d32050e Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Mon, 2 Oct 2023 12:35:20 +0200 Subject: [PATCH 21/27] simplification fix --- .../kproj/evm-semantics/lemmas/bytes-simplification.k | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k index 081eda8f2f..c5deb7a60d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k @@ -70,12 +70,12 @@ module BYTES-SIMPLIFICATION [symbolic] [simplification] rule [buf-shift]: - #buf(W:Int, X < #buf(W -Int Y, X) +Bytes #buf(Y, 0) + #buf(W:Int, X < #buf(W -Int Y, X) +Bytes #buf(Y, 0) requires 0 <=Int W andBool W <=Int 32 andBool 0 <=Int X andBool X >Int M => #asWord(#range(WS, 0, lengthBytes(WS) -Int (M /Int 8) )) requires 0 <=Int M andBool M modInt 8 ==Int 0 [simplification] - rule #asWord(#padRightToWidth(32, BUF)) &Int notMaxUInt224 => #asWord(#padRightToWidth(32, BUF)) + // This simplification needs to be generalised properly + rule notMaxUInt224 &Int #asWord(#padRightToWidth(32, BUF)) => #asWord(#padRightToWidth(32, BUF)) requires lengthBytes(BUF) <=Int 4 [simplification] rule #padToWidth(32, #asByteStack(V)) => #buf(32, V) requires #rangeUInt(256, V) [simplification] From 10f6b18197c3b3ff1936e10bca7217d2408e1e91 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 2 Oct 2023 11:19:39 +0000 Subject: [PATCH 22/27] Set Version: 1.0.310 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 13a3cb915d..19bae199fa 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.309" +version = "1.0.310" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index a56fa043b1..71d04aadc1 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.309' +VERSION: Final = '1.0.310' diff --git a/package/version b/package/version index fcb1b3a84a..c8d4d5a4ea 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.309 +1.0.310 From 4a726fa58e98205183824d5ac7e041036dd31dee Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Mon, 2 Oct 2023 13:49:55 +0200 Subject: [PATCH 23/27] removing simplification --- .../kproj/evm-semantics/lemmas/bitwise-simplification.k | 2 -- 1 file changed, 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k index dabeb175ce..c857bb8da8 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k @@ -27,8 +27,6 @@ module BITWISE-SIMPLIFICATION [symbolic] rule _ &Int 0 => 0 [simplification] rule A &Int A => A [simplification] - rule 1 &Int X => X modInt 2 [simplification] - rule chop ( ( maxUInt48 &Int X:Int ) *Int Y:Int ) => ( maxUInt48 &Int X:Int ) *Int Y requires 0 <=Int X andBool 0 <=Int Y andBool Y <=Int pow208 [simplification] From 5647759d6108aebb04f3ae044db85519b6957096 Mon Sep 17 00:00:00 2001 From: qian-hu <88806138+qian-hu@users.noreply.github.com> Date: Mon, 2 Oct 2023 19:24:39 -0400 Subject: [PATCH 24/27] Fix simplification --- .../kproj/evm-semantics/lemmas/bytes-simplification.k | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k index c5deb7a60d..0d8c66f4d4 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k @@ -70,10 +70,10 @@ module BYTES-SIMPLIFICATION [symbolic] [simplification] rule [buf-shift]: - #buf(W:Int, X < #buf(W -Int Y, X) +Bytes #buf(Y, 0) + #buf(W:Int, X < #buf(W -Int (Y /Int 8), X) +Bytes #buf(Y /Int 8, 0) requires 0 <=Int W andBool W <=Int 32 - andBool 0 <=Int X andBool X Date: Mon, 2 Oct 2023 19:26:59 -0400 Subject: [PATCH 25/27] Add claims for lemmas --- tests/specs/functional/lemmas-spec.k | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k index ecf0795002..fe567cb41d 100644 --- a/tests/specs/functional/lemmas-spec.k +++ b/tests/specs/functional/lemmas-spec.k @@ -402,6 +402,30 @@ module LEMMAS-SPEC claim runLemma ( N &Int maxUInt8 ) => doneLemma ( N ) ... requires #rangeUInt(8, N) claim runLemma ( maxUInt8 &Int N ) => doneLemma ( N ) ... requires #rangeUInt(8, N) + // bitwise + // ------- + + claim runLemma ( notMaxUInt8 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 8 , X ) + claim runLemma ( notMaxUInt16 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 16 , X ) + claim runLemma ( notMaxUInt32 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 32 , X ) + claim runLemma ( notMaxUInt64 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 64 , X ) + claim runLemma ( notMaxUInt240 &Int ( X < doneLemma( X < requires #rangeUInt ( 16 , X ) + claim runLemma ( notMaxUInt248 &Int ( X < doneLemma( X < requires #rangeUInt ( 8 , X ) + claim runLemma ( maxUInt8 &Int ( X |Int ( notMaxUInt8 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 8 , X ) andBool 0 <=Int Y + claim runLemma ( maxUInt16 &Int ( X |Int ( notMaxUInt16 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 16 , X ) andBool 0 <=Int Y + claim runLemma ( maxUInt32 &Int ( X |Int ( notMaxUInt32 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 32 , X ) andBool 0 <=Int Y + claim runLemma ( maxUInt64 &Int ( X |Int ( notMaxUInt64 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 64 , X ) andBool 0 <=Int Y + claim runLemma ( #buf ( 32 , #asWord ( X ) ) ) => doneLemma( X ) requires lengthBytes(X) ==Int 32 + claim runLemma ( #buf ( 32 , X < doneLemma( #buf ( 1 , X ) +Bytes #buf ( 31 , 0 ) ) ... requires #rangeUInt ( 8 , X ) + claim runLemma ( #buf ( 32 , X < doneLemma( #buf ( 2 , X ) +Bytes #buf ( 30 , 0 ) ) ... requires #rangeUInt ( 16 , X ) + + // shift + // ----- + + claim [shift-16] : runLemma ( ( X < doneLemma ( true ) ... requires #rangeUInt ( 240 , X ) + claim [shift-240]: runLemma ( ( X < doneLemma ( true ) ... requires #rangeUInt ( 16 , X ) + claim [shift-248]: runLemma ( ( X < doneLemma ( true ) ... requires #rangeUInt ( 8 , X ) + // ecrecover // --------- From 8e0ff8c620faa4129933bb31f73104c450ccdb2d Mon Sep 17 00:00:00 2001 From: qian-hu <88806138+qian-hu@users.noreply.github.com> Date: Mon, 2 Oct 2023 19:36:00 -0400 Subject: [PATCH 26/27] Update bytes-simplification.k --- .../kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k index 0d8c66f4d4..51dec90e2a 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k @@ -70,7 +70,7 @@ module BYTES-SIMPLIFICATION [symbolic] [simplification] rule [buf-shift]: - #buf(W:Int, X < #buf(W -Int (Y /Int 8), X) +Bytes #buf(Y /Int 8, 0) + #buf(W:Int, X < #buf(W -Int (Y /Int 8), X) +Bytes #buf(Y /Int 8, 0) requires 0 <=Int W andBool W <=Int 32 andBool 0 <=Int X andBool X Date: Mon, 2 Oct 2023 21:09:52 -0400 Subject: [PATCH 27/27] Add more claims for lemmas --- tests/specs/functional/lemmas-spec.k | 50 +++++++++++++++++++++++----- 1 file changed, 42 insertions(+), 8 deletions(-) diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k index fe567cb41d..a810f6769c 100644 --- a/tests/specs/functional/lemmas-spec.k +++ b/tests/specs/functional/lemmas-spec.k @@ -405,16 +405,36 @@ module LEMMAS-SPEC // bitwise // ------- - claim runLemma ( notMaxUInt8 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 8 , X ) - claim runLemma ( notMaxUInt16 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 16 , X ) - claim runLemma ( notMaxUInt32 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 32 , X ) - claim runLemma ( notMaxUInt64 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 64 , X ) + claim runLemma ( notMaxUInt5 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 5 , X ) + claim runLemma ( notMaxUInt8 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 8 , X ) + claim runLemma ( notMaxUInt16 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 16 , X ) + claim runLemma ( notMaxUInt32 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 32 , X ) + claim runLemma ( notMaxUInt64 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 64 , X ) + claim runLemma ( notMaxUInt96 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 96 , X ) + claim runLemma ( notMaxUInt128 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 128 , X ) + claim runLemma ( notMaxUInt160 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 160 , X ) + claim runLemma ( notMaxUInt192 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 192 , X ) + claim runLemma ( notMaxUInt208 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 208 , X ) + claim runLemma ( notMaxUInt224 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 224 , X ) + claim runLemma ( notMaxUInt240 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 240 , X ) + claim runLemma ( notMaxUInt248 &Int X ) => doneLemma( 0 ) ... requires #rangeUInt ( 248 , X ) + claim runLemma ( notMaxUInt240 &Int ( X < doneLemma( X < requires #rangeUInt ( 16 , X ) claim runLemma ( notMaxUInt248 &Int ( X < doneLemma( X < requires #rangeUInt ( 8 , X ) - claim runLemma ( maxUInt8 &Int ( X |Int ( notMaxUInt8 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 8 , X ) andBool 0 <=Int Y - claim runLemma ( maxUInt16 &Int ( X |Int ( notMaxUInt16 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 16 , X ) andBool 0 <=Int Y - claim runLemma ( maxUInt32 &Int ( X |Int ( notMaxUInt32 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 32 , X ) andBool 0 <=Int Y - claim runLemma ( maxUInt64 &Int ( X |Int ( notMaxUInt64 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 64 , X ) andBool 0 <=Int Y + + claim runLemma ( maxUInt8 &Int ( X |Int ( notMaxUInt8 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 8 , X ) + claim runLemma ( maxUInt16 &Int ( X |Int ( notMaxUInt16 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 16 , X ) + claim runLemma ( maxUInt32 &Int ( X |Int ( notMaxUInt32 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 32 , X ) + claim runLemma ( maxUInt64 &Int ( X |Int ( notMaxUInt64 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 64 , X ) + claim runLemma ( maxUInt96 &Int ( X |Int ( notMaxUInt96 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 96 , X ) + claim runLemma ( maxUInt128 &Int ( X |Int ( notMaxUInt128 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 128 , X ) + claim runLemma ( maxUInt160 &Int ( X |Int ( notMaxUInt160 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 160 , X ) + claim runLemma ( maxUInt192 &Int ( X |Int ( notMaxUInt192 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 192 , X ) + claim runLemma ( maxUInt208 &Int ( X |Int ( notMaxUInt208 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 208 , X ) + claim runLemma ( maxUInt224 &Int ( X |Int ( notMaxUInt224 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 224 , X ) + claim runLemma ( maxUInt240 &Int ( X |Int ( notMaxUInt240 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 240 , X ) + claim runLemma ( maxUInt248 &Int ( X |Int ( notMaxUInt248 &Int Y ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 248 , X ) + claim runLemma ( #buf ( 32 , #asWord ( X ) ) ) => doneLemma( X ) requires lengthBytes(X) ==Int 32 claim runLemma ( #buf ( 32 , X < doneLemma( #buf ( 1 , X ) +Bytes #buf ( 31 , 0 ) ) ... requires #rangeUInt ( 8 , X ) claim runLemma ( #buf ( 32 , X < doneLemma( #buf ( 2 , X ) +Bytes #buf ( 30 , 0 ) ) ... requires #rangeUInt ( 16 , X ) @@ -426,6 +446,20 @@ module LEMMAS-SPEC claim [shift-240]: runLemma ( ( X < doneLemma ( true ) ... requires #rangeUInt ( 16 , X ) claim [shift-248]: runLemma ( ( X < doneLemma ( true ) ... requires #rangeUInt ( 8 , X ) + claim [shift-range]: runLemma ( #rangeUInt ( 256 , X < doneLemma ( true ) ... requires #rangeUInt ( 16 , X ) + claim [shift-mod]: runLemma ( ( X < doneLemma ( X < requires #rangeUInt ( 16 , X ) + + // concat + // ------ + + claim runLemma ( lengthBytes ( #range ( #buf ( 32 , _X ) , 3 , 29 ) +Bytes b"\x01" +Bytes #buf ( 2 , Y ) ) ) + => doneLemma ( 32 ) ... + requires #rangeUInt ( 16 , Y ) + + claim runLemma ( #asWord ( #range ( #buf ( 32 , X ) , 0 , 29 ) +Bytes #range ( #buf ( 32 , X ) , 29 , 3 ) ) ) + => doneLemma ( X ) ... + requires #rangeUInt ( 256 , X ) + // ecrecover // ---------