Skip to content

^Int and /Int definedness preservation #2425

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
May 15, 2024
Merged

^Int and /Int definedness preservation #2425

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f9df999
^Int and /Int definedness preservation
May 15, 2024
bbdfa68
Set Version: 1.0.555
rv-auditor May 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion kevm-pyk/pyproject.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "kevm-pyk"
version = "1.0.554"
version = "1.0.555"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/__init__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,4 @@
if TYPE_CHECKING:
from typing import Final

VERSION: Final = '1.0.554'
VERSION: Final = '1.0.555'
6 changes: 3 additions & 3 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,15 +50,15 @@ module BITWISE-SIMPLIFICATION [symbolic]
requires 0 <=Int X
andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
andBool 0 <=Int Y andBool Y <Int X +Int 1
[concrete(X), simplification, comm]
[concrete(X), simplification, comm, preserves-definedness]

// Generalization of: notMaxUIntXXX &Int Y => 0 requires #rangeUInt(XXX, Y)
rule [bitwise-and-notMaxUInt-zero]:
X &Int Y => 0
requires #rangeUInt(256, X)
andBool pow256 -Int X ==Int 2 ^Int ( log2Int ( pow256 -Int X ) )
andBool 0 <=Int Y andBool Y <Int pow256 -Int X
[simplification, concrete(X)]
[simplification, concrete(X), preserves-definedness]

// Generalization of: maxUIntXXX &Int #asWord ( BA )
rule X &Int #asWord ( BA ) => #asWord ( #range(BA, 32 -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) )
Expand Down Expand Up @@ -113,7 +113,7 @@ module BITWISE-SIMPLIFICATION [symbolic]

rule (X <<Int Y) <Int pow256 => true
requires 0 <=Int X andBool 0 <=Int Y andBool Y <Int 256 andBool X <Int 2 ^Int (256 -Int Y)
[simplification]
[simplification, preserves-definedness]

rule 0 <=Int (X <<Int Y) => true requires 0 <=Int X andBool 0 <=Int Y [simplification]

Expand Down
26 changes: 14 additions & 12 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,14 +41,14 @@ module BYTES-SIMPLIFICATION [symbolic]
requires 0 <=Int W
andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int W)
andBool 0 <=Int Y andBool Y <Int 2 ^Int (8 *Int W)
[simplification]
[simplification, preserves-definedness]

rule [buf-inject-ml]:
{ #buf(W:Int, X:Int) #Equals #buf(W:Int, Y:Int) } => { X #Equals Y }
requires 0 <=Int W
andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int W)
andBool 0 <=Int Y andBool Y <Int 2 ^Int (8 *Int W)
[simplification]
[simplification, preserves-definedness]

rule [buf-as-int]: B:Bytes ==K #buf(32, X:Int) => X ==Int #asInteger(B)
requires lengthBytes(B) <=Int 32
Expand All @@ -68,21 +68,21 @@ module BYTES-SIMPLIFICATION [symbolic]
#buf (W:Int , #asWord(B:Bytes)) => #range(B, lengthBytes(B) -Int W, W)
requires 0 <=Int W andBool W <Int lengthBytes(B) andBool lengthBytes(B) <=Int 32
andBool #asWord(B) <Int 2 ^Int (8 *Int W)
[simplification, concrete(W)]
[simplification, concrete(W), preserves-definedness]

rule [buf-asWord-invert-rl]:
#asWord ( #buf ( WB:Int, X:Int ) ) => X
requires 0 <=Int WB andBool 0 <=Int X andBool
( ( WB <=Int 32 andBool X <Int 2 ^Int (WB *Int 8) ) orBool
( WB >Int 32 andBool X <Int pow256 ) )
[simplification, concrete(WB)]
[simplification, concrete(WB), preserves-definedness]

rule [buf-asWord-invert-rl-range]:
#asWord ( #range ( #buf ( WB:Int, X:Int ), S:Int, WR:Int ) ) => X
requires 0 <=Int WB andBool 0 <=Int X andBool 0 <=Int S andBool 0 <=Int WR
andBool S +Int WR ==Int WB
andBool X <Int 2 ^Int (WR *Int 8)
[simplification, concrete(WB, S, WR)]
[simplification, concrete(WB, S, WR), preserves-definedness]

rule [buf-zero-concat-base]:
#buf(W1:Int, 0) +Bytes #buf(W2:Int, 0) => #buf(W1 +Int W2, 0)
Expand Down Expand Up @@ -189,13 +189,13 @@ module BYTES-SIMPLIFICATION [symbolic]
B:Bytes +Bytes #buf(W:Int, X:Int) => #buf(lengthBytes(B) +Int W, X)
requires 0 <=Int W andBool 0 <=Int X andBool X <Int 2 ^Int (W *Int 8)
andBool #asInteger(B) ==Int 0 andBool lengthBytes(B) +Int W <=Int 32
[concrete(B, W), simplification]
[concrete(B, W), simplification, preserves-definedness]

rule [range-buf-zero-concat-extend]:
B1:Bytes +Bytes #buf(W:Int, X:Int) +Bytes B2 => #buf(lengthBytes(B1) +Int W, X) +Bytes B2
requires 0 <=Int W andBool 0 <=Int X andBool X <Int 2 ^Int (W *Int 8)
andBool #asInteger(B1) ==Int 0 andBool lengthBytes(B1) +Int W <=Int 32
[concrete(B1, W), simplification]
[concrete(B1, W), simplification, preserves-definedness]

rule [range-memUpdate-before]:
#range(B1:Bytes [ S1:Int := B2:Bytes ], S2:Int, W2:Int) =>
Expand All @@ -220,13 +220,13 @@ module BYTES-SIMPLIFICATION [symbolic]
#range (#buf(W1:Int, X:Int), S2:Int, W2:Int) => #buf(W2, 0)
requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int (W1 -Int (S2 +Int W2)))
andBool 0 <=Int S2 andBool 0 <=Int W2 andBool S2 +Int W2 <=Int W1
[simplification, concrete(W1, S2, W2)]
[simplification, concrete(W1, S2, W2), preserves-definedness]

rule [range-buf-value]:
#range (#buf(W1:Int, X:Int), S2:Int, W2:Int) => #buf(W2, X)
requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int W2)
andBool 0 <=Int S2 andBool 0 <=Int W2 andBool W1 ==Int S2 +Int W2
[simplification, concrete(W1, S2, W2)]
[simplification, concrete(W1, S2, W2), preserves-definedness]

rule [range-padRightToWidth]:
#range(#padRightToWidth(_, BUF), 0, WIDTH) => BUF
Expand All @@ -239,7 +239,7 @@ module BYTES-SIMPLIFICATION [symbolic]
andBool #asInteger( BZ ) ==Int 0
andBool lengthBytes( BZ ) ==Int S
andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
[simplification, concrete(BZ, S, W), comm]
[simplification, concrete(BZ, S, W), comm, preserves-definedness]

rule [range-eq-check-ml]:
{ BZ +Bytes #range ( B, S, W ) #Equals B } => #Top
Expand All @@ -248,7 +248,7 @@ module BYTES-SIMPLIFICATION [symbolic]
andBool #asInteger( BZ ) ==Int 0
andBool lengthBytes( BZ ) ==Int S
andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
[simplification, concrete(BZ, S, W), comm]
[simplification, concrete(BZ, S, W), comm, preserves-definedness]

// Memory update

Expand Down Expand Up @@ -291,7 +291,9 @@ module BYTES-SIMPLIFICATION [symbolic]

// #asWord

rule #asWord(WS) >>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(WS) >>Int M => #asWord(#range(WS, 0, lengthBytes(WS) -Int (M /Int 8) ))
requires 0 <=Int M andBool M modInt 8 ==Int 0
[simplification, preserves-definedness]

// This simplification needs to be generalised properly
rule notMaxUInt224 &Int #asWord(#padRightToWidth(32, BUF)) => #asWord(#padRightToWidth(32, BUF))
Expand Down
6 changes: 3 additions & 3 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,20 +68,20 @@ module EVM-INT-SIMPLIFICATION-COMMON
rule [asWord-lt-concat]:
#asWord ( BA1 +Bytes BA2 ) <Int X => #asWord ( BA1 ) <Int ( X -Int #asWord ( BA2 ) ) /Int ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) )
requires ( X -Int #asWord ( BA2 ) ) modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) ) ==Int 0
[concrete(BA2, X), simplification]
[concrete(BA2, X), simplification, preserves-definedness]

rule [asWord-lt-range]:
#asWord ( #range ( _:Bytes, S, W ) ) <Int X => true
requires 0 <=Int S andBool 0 <=Int W
andBool 2 ^Int ( 8 *Int W ) <=Int X
[simplification, concrete(S, W, X)]
[simplification, concrete(S, W, X), preserves-definedness]

rule [lt-asWord-range]:
X <Int #asWord ( #range ( B:Bytes, S, W ) ) => X <Int #asWord ( B )
requires 0 <=Int S andBool 0 <=Int W
andBool lengthBytes(B) ==Int S +Int W
andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
[simplification, concrete(X, S, W)]
[simplification, concrete(X, S, W), preserves-definedness]

// ###########################################################################
// chop
Expand Down
4 changes: 0 additions & 4 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -159,10 +159,6 @@ module LEMMAS-HASKELL [symbolic]
requires D ==Int 256 ^Int log256Int(D) andBool D >=Int 0
andBool lengthBytes(BUF) >=Int log256Int(D) [simplification, preserves-definedness]

rule #asWord(#buf(N, BUF)) => BUF
requires #range(0 < N <= 32)
andBool #range(0 <= BUF < 2 ^Int (N *Int 8)) [simplification]

rule notBool (X ==Int 0) => X ==Int 1 requires #rangeBool(X) [simplification]
rule notBool (X ==Int 1) => X ==Int 0 requires #rangeBool(X) [simplification]
rule bool2Word(X ==Int 1) => X requires #rangeBool(X) [simplification]
Expand Down
2 changes: 1 addition & 1 deletion package/version
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
1.0.554
1.0.555