Skip to content
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

Simplify Int2Bytes and Bytes2Bytes #290

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Simplify Int2Bytes and Bytes2Bytes #290

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
b29255c
Use local pyk
virgil-serbanuta Apr 29, 2024
4198084
Simplify MapIntToBytes and MapBytesToBytes
virgil-serbanuta Jun 18, 2024
9e947b1
Set Version: 0.1.82
Jun 18, 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
5 changes: 3 additions & 2 deletions kmultiversx/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 = "kmultiversx"
version = "0.1.81"
version = "0.1.82"
description = "Python tools for Elrond semantics"
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand All @@ -20,7 +20,8 @@ mx-semantics = "kmultiversx.kdist.plugin"

[tool.poetry.dependencies]
python = "^3.10"
pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.63", subdirectory = "pykwasm" }
# pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.63", subdirectory = "pykwasm" }
pykwasm = { path = "/mnt/data/runtime-verification/pyk-dependencies/wasm-semantics", develop = true, subdirectory = "pykwasm" }
pycryptodomex = "^3.18.0"
hypothesis = "^6.82.6"

Expand Down
265 changes: 13 additions & 252 deletions kmultiversx/src/kmultiversx/kdist/mx-semantics/data/map-bytes-to-bytes.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,11 +86,6 @@ module MAP-BYTES-TO-BYTES
endmodule

module MAP-BYTES-TO-BYTES-PRIMITIVE
imports MAP-BYTES-TO-BYTES-PRIMITIVE-CONCRETE
imports MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC
endmodule

module MAP-BYTES-TO-BYTES-PRIMITIVE-CONCRETE [concrete]
imports public BOOL
imports private K-EQUAL
imports public MAP-BYTES-TO-BYTES
Expand Down Expand Up @@ -119,205 +114,15 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-CONCRETE [concrete]
rule Key:Bytes in_keys {{ M:MapBytesToBytes }} => wrap(Key) in_keys(M)
endmodule

module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic]
imports public BOOL
imports private K-EQUAL
imports public MAP-BYTES-TO-BYTES
imports private MAP-BYTES-TO-BYTES-KORE-SYMBOLIC

syntax Bytes ::= MapBytesToBytes "{{" Bytes "}}"
[function, symbol(MapBytesToBytes:primitiveLookup)]
syntax Bytes ::= MapBytesToBytes "{{" Bytes "}}" "orDefault" Bytes
[ function, total, symbol(MapBytesToBytes:primitiveLookupOrDefault) ]
syntax MapBytesToBytes ::= MapBytesToBytes "{{" key: Bytes "<-" value: Bytes "}}"
[ function, total, symbol(MapBytesToBytes:primitiveUpdate),
prefer
]
syntax MapBytesToBytes ::= MapBytesToBytes "{{" Bytes "<-" "undef" "}}"
[ function, total, symbol(MapBytesToBytes:primitiveRemove) ]
syntax Bool ::= Bytes "in_keys" "{{" MapBytesToBytes "}}"
[function, total, symbol(MapBytesToBytes:primitiveInKeys)]

// Definitions
// -----------

rule (wrap(Key) Bytes2Bytes|-> V:WrappedBytes M:MapBytesToBytes)
{{ Key:Bytes }}
=> unwrap( V )
ensures notBool Key in_keys {{ M }}

rule (wrap(Key) Bytes2Bytes|-> V:WrappedBytes M:MapBytesToBytes)
{{ Key:Bytes }} orDefault _:Bytes
=> unwrap( V )
ensures notBool Key in_keys {{ M }}
rule M:MapBytesToBytes {{ Key:Bytes }} orDefault V:Bytes
=> V
requires notBool Key in_keys {{ M }}

rule (wrap(Key) Bytes2Bytes|-> _:WrappedBytes M:MapBytesToBytes)
{{ Key:Bytes <- Value:Bytes }}
=> (wrap(Key) Bytes2Bytes|-> wrap(Value)) M
rule M:MapBytesToBytes {{ Key:Bytes <- Value:Bytes }}
=> (wrap(Key) Bytes2Bytes|-> wrap(Value)) M
requires notBool Key in_keys {{ M }}

rule (wrap(Key) Bytes2Bytes|-> _:WrappedBytes M:MapBytesToBytes)
{{ Key:Bytes <- undef }}
=> M
ensures notBool Key in_keys {{ M }}
rule M:MapBytesToBytes {{ Key:Bytes <- undef }}
=> M
requires notBool Key in_keys {{ M }}

rule Key:Bytes in_keys
{{wrap(Key) Bytes2Bytes|-> _:WrappedBytes M:MapBytesToBytes}}
=> true
ensures notBool Key in_keys {{ M }}
rule _Key:Bytes in_keys {{ .MapBytesToBytes }}
=> false
// TODO: This may create an exponential evaluation tree, depending on how
// caching works in the backend. It should be rewritten to finish in
// O(n^2) or something like that, where n is the number of explicit keys
// in the map.
rule Key:Bytes in_keys
{{Key2:WrappedBytes Bytes2Bytes|-> _:WrappedBytes M:MapBytesToBytes}}
=> Key in_keys {{ M }}
requires Key =/=K unwrap( Key2 )
ensures notBool Key2 in_keys (M)
[simplification]

// Translation rules
rule M:MapBytesToBytes[Key:WrappedBytes]
=> wrap(M{{unwrap( Key )}})
[simplification, symbolic(M)]
rule M:MapBytesToBytes[Key:WrappedBytes]
=> wrap(M{{unwrap( Key )}})
[simplification, symbolic(Key)]
rule M:MapBytesToBytes{{Key}}
=> unwrap( M[wrap(Key)] )
[simplification, concrete]

rule M:MapBytesToBytes [ Key:WrappedBytes ] orDefault Value:WrappedBytes
=> wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
[simplification, symbolic(M)]
rule M:MapBytesToBytes [ Key:WrappedBytes ] orDefault Value:WrappedBytes
=> wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
[simplification, symbolic(Key)]
rule M:MapBytesToBytes [ Key:WrappedBytes ] orDefault Value:WrappedBytes
=> wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
[simplification, symbolic(Value)]
rule M:MapBytesToBytes{{Key}} orDefault Value
=> unwrap( M[wrap(Key)] orDefault wrap(Value) )
[simplification, concrete]

rule M:MapBytesToBytes[Key:WrappedBytes <- Value:WrappedBytes]
=> M {{ unwrap( Key ) <- unwrap( Value ) }}
[simplification, symbolic(M)]
rule M:MapBytesToBytes[Key:WrappedBytes <- Value:WrappedBytes]
=> M {{ unwrap( Key ) <- unwrap( Value ) }}
[simplification, symbolic(Key)]
rule M:MapBytesToBytes[Key:WrappedBytes <- Value:WrappedBytes]
=> M {{ unwrap( Key ) <- unwrap( Value ) }}
[simplification, symbolic(Value)]
rule M:MapBytesToBytes{{Key <- Value}} => M[wrap(Key) <- wrap(Value) ]
[simplification, concrete]

rule M:MapBytesToBytes[Key:WrappedBytes <- undef]
=> M {{ unwrap( Key ) <- undef }}
[simplification, symbolic(M)]
rule M:MapBytesToBytes[Key:WrappedBytes <- undef]
=> M {{ unwrap( Key ) <- undef }}
[simplification, symbolic(Key)]
rule M:MapBytesToBytes{{Key <- undef}} => M[wrap(Key) <- undef]
[simplification, concrete]

rule Key:WrappedBytes in_keys (M:MapBytesToBytes)
=> unwrap( Key ) in_keys {{M}}
[simplification, symbolic(M)]
rule Key:WrappedBytes in_keys (M:MapBytesToBytes)
=> unwrap( Key ) in_keys {{M}}
[simplification, symbolic(Key)]
rule Key in_keys {{M:MapBytesToBytes}} => wrap(Key) in_keys(M)
[simplification, concrete]

// Symbolic execution rules
// ------------------------
syntax Bool ::= definedPrimitiveLookup(MapBytesToBytes, Bytes) [function, total]
rule definedPrimitiveLookup(M:MapBytesToBytes, K:Bytes) => K in_keys{{M}}

rule #Ceil(@M:MapBytesToBytes {{@K:Bytes}})
=> {definedPrimitiveLookup(@M, @K) #Equals true}
#And #Ceil(@M) #And #Ceil(@K)
[simplification]

rule M:MapBytesToBytes {{ K <- _ }} {{ K <- V }} => M {{ K <- V }} [simplification]
rule (K1 Bytes2Bytes|-> V1 M:MapBytesToBytes) {{ K2 <- V2 }}
=> (K1 Bytes2Bytes|-> V1 (M {{ K2 <- V2 }}))
requires unwrap( K1 ) =/=K K2
[simplification, preserves-definedness]

rule (K1 Bytes2Bytes|-> V1 M:MapBytesToBytes) {{ K2 <- undef }}
=> (K1 Bytes2Bytes|-> V1 (M {{ K2 <- undef }}))
requires unwrap( K1 ) =/=K K2
[simplification, preserves-definedness]

rule (K1 Bytes2Bytes|-> _V M:MapBytesToBytes) {{ K2 }} => M {{K2}}
requires unwrap( K1 ) =/=K K2
ensures notBool (K1 in_keys(M))
[simplification]
rule (_MAP:MapBytesToBytes {{ K <- V1 }}) {{ K }} => V1 [simplification]
rule ( MAP:MapBytesToBytes {{ K1 <- _V1 }}) {{ K2 }} => MAP {{ K2 }}
requires K1 =/=K K2
[simplification]

rule (K1 Bytes2Bytes|-> _V M:MapBytesToBytes) {{ K2 }} orDefault D
=> M {{K2}} orDefault D
requires unwrap( K1 ) =/=K K2
ensures notBool (K1 in_keys(M))
[simplification]
rule (_MAP:MapBytesToBytes {{ K <- V1 }}) {{ K }} orDefault _ => V1 [simplification]
rule ( MAP:MapBytesToBytes {{ K1 <- _V1 }}) {{ K2 }} orDefault D
=> MAP {{ K2 }} orDefault D
requires K1 =/=K K2
[simplification]

rule K in_keys{{_M:MapBytesToBytes {{ K <- undef }} }} => false [simplification]
rule K in_keys{{_M:MapBytesToBytes {{ K <- _ }} }} => true [simplification]
rule K1 in_keys{{ _M:MapBytesToBytes {{ K2 <- _ }} }}
=> true requires K1 ==K K2
[simplification]
rule K1 in_keys{{ M:MapBytesToBytes {{ K2 <- _ }} }}
=> K1 in_keys {{ M }}
requires K1 =/=K K2
[simplification]

rule K1 in_keys {{ (K2 Bytes2Bytes|-> V) M:MapBytesToBytes }}
=> K1 ==K unwrap( K2 ) orBool K1 in_keys {{ M }}
requires definedMapElementConcat(K2, V, M)
[simplification(100), preserves-definedness]


rule {false #Equals @Key in_keys{{ Key' Bytes2Bytes|-> Val @M:MapBytesToBytes }}}
=> #Ceil(@Key) #And #Ceil(Key' Bytes2Bytes|-> Val @M)
#And #Not({ @Key #Equals unwrap( Key' ) })
#And {false #Equals @Key in_keys{{@M}}}
[simplification]
rule {@Key in_keys{{Key' Bytes2Bytes|-> Val @M:MapBytesToBytes}} #Equals false}
=> #Ceil(@Key) #And #Ceil(Key' Bytes2Bytes|-> Val @M)
#And #Not({@Key #Equals unwrap( Key' ) })
#And {@Key in_keys{{@M}} #Equals false}
[simplification]

module MAP-BYTES-TO-BYTES-SYMBOLIC
imports MAP-BYTES-TO-BYTES-KORE-SYMBOLIC
endmodule

module MAP-BYTES-TO-BYTES-KORE-SYMBOLIC
module MAP-BYTES-TO-BYTES-KORE-SYMBOLIC [symbolic]
imports MAP-BYTES-TO-BYTES
imports private K-EQUAL
imports private BOOL

syntax Bool ::= definedMapElementConcat(WrappedBytes, WrappedBytes, MapBytesToBytes) [function, total]
rule definedMapElementConcat(K, _V, M:MapBytesToBytes) => notBool K in_keys(M)

rule #Ceil(@M:MapBytesToBytes [@K:WrappedBytes])
=> {(@K in_keys(@M)) #Equals true}
#And #Ceil(@M) #And #Ceil(@K)
Expand All @@ -328,21 +133,27 @@ module MAP-BYTES-TO-BYTES-KORE-SYMBOLIC
rule M:MapBytesToBytes [ K <- V ] => (K Bytes2Bytes|-> V M) requires notBool (K in_keys(M))
[simplification, preserves-definedness]
rule M:MapBytesToBytes [ K <- _ ] [ K <- V ] => M [ K <- V ] [simplification]
// Adding the definedness condition `notBool (K1 in_keys(M))` in the ensures clause of the following rule would be redundant
// because K1 also appears in the rhs, preserving the case when it's #Bottom.
rule (K1 Bytes2Bytes|-> V1 M:MapBytesToBytes) [ K2 <- V2 ] => (K1 Bytes2Bytes|-> V1 (M [ K2 <- V2 ]))
requires K1 =/=K K2
[simplification, preserves-definedness]

// Symbolic remove
rule (K Bytes2Bytes|-> _ M:MapBytesToBytes) [ K <- undef ] => M
ensures notBool (K in_keys(M))
[simplification]
rule M:MapBytesToBytes [ K <- undef ] => M
requires notBool (K in_keys(M))
[simplification]
// Adding the definedness condition `notBool (K1 in_keys(M))` in the ensures clause of the following rule would be redundant
// because K1 also appears in the rhs, preserving the case when it's #Bottom.
rule (K1 Bytes2Bytes|-> V1 M:MapBytesToBytes) [ K2 <- undef ]
=> (K1 Bytes2Bytes|-> V1 (M [ K2 <- undef ]))
requires K1 =/=K K2
[simplification, preserves-definedness]

// Symbolic lookup
rule (K Bytes2Bytes|-> V M:MapBytesToBytes) [ K ] => V
ensures notBool (K in_keys(M))
[simplification]
Expand Down Expand Up @@ -370,6 +181,7 @@ module MAP-BYTES-TO-BYTES-KORE-SYMBOLIC
[simplification]
rule .MapBytesToBytes [ _ ] orDefault D => D [simplification]

// Symbolic in_keys
rule K in_keys(_M:MapBytesToBytes [ K <- undef ]) => false [simplification]
rule K in_keys(_M:MapBytesToBytes [ K <- _ ]) => true [simplification]
rule K1 in_keys(M:MapBytesToBytes [ K2 <- _ ])
Expand All @@ -382,17 +194,17 @@ module MAP-BYTES-TO-BYTES-KORE-SYMBOLIC

rule K in_keys((K Bytes2Bytes|-> V) M:MapBytesToBytes)
=> true
requires definedMapElementConcat(K, V, M)
requires notBool K in_keys(M)
[simplification(50), preserves-definedness]
rule K1 in_keys((K2 Bytes2Bytes|-> V) M:MapBytesToBytes)
=> K1 in_keys(M)
requires true
andBool definedMapElementConcat(K2, V, M)
andBool (notBool K2 in_keys(M))
andBool K1 =/=K K2
[simplification(50), preserves-definedness]
rule K1 in_keys((K2 Bytes2Bytes|-> V) M:MapBytesToBytes)
=> K1 ==K K2 orBool K1 in_keys(M)
requires definedMapElementConcat(K2, V, M)
requires notBool K2 in_keys(M)
[simplification(100), preserves-definedness]


Expand All @@ -410,54 +222,3 @@ module MAP-BYTES-TO-BYTES-KORE-SYMBOLIC
[simplification]
endmodule

module MAP-BYTES-TO-BYTES-CURLY-BRACE
imports private BOOL
imports private K-EQUAL-SYNTAX
imports MAP-BYTES-TO-BYTES

syntax MapBytesToBytes ::= MapBytesToBytes "{" key:WrappedBytes "<-" value:WrappedBytes "}"
[function, total, symbol(MapBytesToBytes:curly_update)]
rule M:MapBytesToBytes{Key <- Value} => M (Key Bytes2Bytes|-> Value)
requires notBool Key in_keys(M)
rule (Key Bytes2Bytes|-> _ M:MapBytesToBytes){Key <- Value}
=> M (Key Bytes2Bytes|-> Value)
rule (M:MapBytesToBytes{Key <- Value})(A Bytes2Bytes|-> B N:MapBytesToBytes)
=> (M (A Bytes2Bytes|-> B)) {Key <- Value} N
requires notBool A ==K Key
[simplification, preserves-definedness]

rule M:MapBytesToBytes{Key1 <- Value1}[Key2 <- Value2]
=> ((M:MapBytesToBytes[Key2 <- Value2]{Key1 <- Value1}) #And #Not ({Key1 #Equals Key2}))
#Or ((M:MapBytesToBytes[Key2 <- Value2]) #And {Key1 #Equals Key2})
[simplification(20)]
rule M:MapBytesToBytes[Key <- Value]
=> M:MapBytesToBytes{Key <- Value}
[simplification(100)]
rule M:MapBytesToBytes{Key1 <- _Value1}[Key2] orDefault Value2
=> M[Key2] orDefault Value2
requires Key1 =/=K Key2
[simplification]
rule _M:MapBytesToBytes{Key <- Value1}[Key] orDefault _Value2
=> Value1
[simplification]
// rule M:MapBytesToBytes{Key1 <- Value1}[Key2] orDefault Value2
// => (M[Key2] orDefault Value2 #And #Not ({Key1 #Equals Key2}))
// #Or (Value1 #And {Key1 #Equals Key2})
// [simplification]
rule M:MapBytesToBytes{Key1 <- Value1}[Key2]
=> (M[Key2] #And #Not ({Key1 #Equals Key2}))
#Or (Value1 #And {Key1 #Equals Key2})
[simplification]

rule Key1 in_keys(_:MapBytesToBytes{Key1 <- _})
=> true
[simplification(50)]
rule Key1 in_keys(M:MapBytesToBytes{Key2 <- _})
=> Key1 in_keys(M)
requires notBool Key1 ==K Key2
[simplification(50)]
rule K1 in_keys(M:MapBytesToBytes { K2 <- _ })
=> K1 ==K K2 orBool K1 in_keys(M)
[simplification(100)]

endmodule
Loading
Loading