From b1de6804af4dbd9ab19c36a8a98486d6eae5074a Mon Sep 17 00:00:00 2001 From: qian-hu <88806138+qian-hu@users.noreply.github.com> Date: Tue, 3 Oct 2023 06:36:09 -0400 Subject: [PATCH] Upstream lemmas from Wormhole engagement (#1866) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Add notMaxUInt constants * Add bitwise-arithmetic lemmas * Upstream bytes-simplification lemmas from Wormhole * Upstream lemmas from Wormhole engagement * Set Version: 1.0.187 * Revert "Upstream lemmas from Wormhole engagement" This reverts commit 22f83927da5c22a813e6ca5266ae611e3aafd801. * Set Version: 1.0.210 * Update include/kframework/word.md Co-authored-by: Everett Hildenbrandt * Set Version: 1.0.211 * Set Version: 1.0.212 * Set Version: 1.0.213 * Set Version: 1.0.219 * Set Version: 1.0.227 * Set Version: 1.0.228 * generalize lemmas * Set Version: 1.0.244 * Set Version: 1.0.249 * Set Version: 1.0.296 * Set Version: 1.0.309 * cleanup * simplification fix * Set Version: 1.0.310 * removing simplification * Fix simplification * Add claims for lemmas * Update bytes-simplification.k * Add more claims for lemmas --------- Co-authored-by: devops Co-authored-by: Everett Hildenbrandt Co-authored-by: Petar Maksimovic Co-authored-by: Petar Maksimović --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- .../lemmas/bitwise-simplification.k | 47 ++++++++++++++- .../lemmas/bytes-simplification.k | 10 +++- .../src/kevm_pyk/kproj/evm-semantics/word.md | 12 ++++ package/version | 2 +- tests/specs/functional/lemmas-spec.k | 58 +++++++++++++++++++ 7 files changed, 127 insertions(+), 6 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/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 1f21f317aa..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 @@ -5,17 +5,24 @@ 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 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] @@ -40,8 +47,36 @@ 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( 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 maxUInt160 &Int (X |Int (notMaxUInt160 &Int Y:Int)) => X requires #rangeUInt(160, X) andBool 0 <=Int Y [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 < 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 @@ -52,4 +87,12 @@ module BITWISE-SIMPLIFICATION [symbolic] lengthBytes(X) +Int 32 >Int notMaxUInt5 &Int ( lengthBytes(X) +Int 31 ) => true [simplification, smt-lemma] + // ########################################################################### + // shift + // ########################################################################### + + rule (X < true requires 0 <=Int X andBool 0 <=Int Y andBool Y true requires 0 <=Int X andBool 0 <=Int Y [simplification] + endmodule 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 db96ce0a93..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 @@ -69,6 +69,13 @@ module BYTES-SIMPLIFICATION [symbolic] requires 0 <=Int W1 andBool 0 <=Int W2 [simplification] + rule [buf-shift]: + #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 >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] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md index 38de992338..afc975f115 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md @@ -426,20 +426,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 */ 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 diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k index ecf0795002..a810f6769c 100644 --- a/tests/specs/functional/lemmas-spec.k +++ b/tests/specs/functional/lemmas-spec.k @@ -402,6 +402,64 @@ 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 ( 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 ) + 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 ) + + // 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 ) + + 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 // ---------