Skip to content

Commit

Permalink
Fix in keys and remove klabels (#284)
Browse files Browse the repository at this point in the history 
* Fix in keys and remove klabels

* Fix unused variable

* Remove invalid requires

* Set Version: 0.1.77

---------

Co-authored-by: devops <[email protected]>
  • Loading branch information
@virgil-serbanuta
virgil-serbanuta and devops authored Jun 12, 2024
1 parent 748b20e commit 5e23591
Show file tree
Hide file tree
Showing 5 changed files with 102 additions and 92 deletions.
2 changes: 1 addition & 1 deletion kmultiversx/pyproject.toml
View file
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.76"
version = "0.1.77"
description = "Python tools for Elrond semantics"
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
41 changes: 24 additions & 17 deletions kmultiversx/src/kmultiversx/kdist/mx-semantics/data/list-bytes.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,34 +10,34 @@ module LIST-BYTES
syntax ListBytes [hook(LIST.List)]
syntax ListBytes ::= ListBytes ListBytes
[ left, function, total, hook(LIST.concat),
klabel(_ListBytes_), symbol, smtlib(smt_seq_concat),
symbol(_ListBytes_), smtlib(smt_seq_concat),
assoc, unit(.ListBytes), element(ListBytesItem),
format(%1%n%2)
]
syntax ListBytes ::= ".ListBytes"
[ function, total, hook(LIST.unit), klabel(.ListBytes),
symbol, smtlib(smt_seq_nil)
[ function, total, hook(LIST.unit), symbol(.ListBytes),
smtlib(smt_seq_nil)
]
syntax ListBytes ::= ListItem(WrappedBytes)
[ function, total, hook(LIST.element), klabel(ListBytesItem),
symbol, smtlib(smt_seq_elem)
[ function, total, hook(LIST.element), symbol(ListBytesItem),
smtlib(smt_seq_elem)
]
syntax WrappedBytes ::= ListBytes "[" Int "]"
[ function, hook(LIST.get), klabel(ListBytes:get), symbol ]
[ function, hook(LIST.get), symbol(ListBytes:get) ]
syntax ListBytes ::= ListBytes "[" index: Int "<-" value: WrappedBytes "]"
[function, hook(LIST.update), symbol, klabel(ListBytes:set)]
[function, hook(LIST.update), symbol(ListBytes:set)]
syntax ListBytes ::= makeListBytes(length: Int, value: WrappedBytes)
[function, hook(LIST.make)]
syntax ListBytes ::= updateList(dest: ListBytes, index: Int, src: ListBytes)
[function, hook(LIST.updateAll)]
syntax ListBytes ::= fillList(ListBytes, index: Int, length: Int, value: WrappedBytes)
[function, hook(LIST.fill)]
syntax ListBytes ::= range(ListBytes, fromFront: Int, fromBack: Int)
[function, hook(LIST.range), klabel(ListBytes:range), symbol]
[function, hook(LIST.range), symbol(ListBytes:range)]
syntax Bool ::= WrappedBytes "in" ListBytes
[function, total, hook(LIST.in), symbol, klabel(_inListBytes_)]
[function, total, hook(LIST.in), symbol(_inListBytes_)]
syntax Int ::= size(ListBytes)
[function, total, hook(LIST.size), symbol, klabel (sizeListBytes), smtlib(smt_seq_len)]
[function, total, hook(LIST.size), symbol(sizeListBytes), smtlib(smt_seq_len)]
endmodule

module LIST-BYTES-EXTENSIONS
Expand All @@ -46,15 +46,15 @@ module LIST-BYTES-EXTENSIONS
imports LIST-BYTES

syntax WrappedBytes ::= ListBytes "[" Int "]" "orDefault" WrappedBytes
[ function, total, klabel(ListBytes:getOrDefault), symbol ]
[ function, total, symbol(ListBytes:getOrDefault) ]

syntax Bytes ::= ListBytes "{{" Int "}}"
[function, symbol, klabel(ListBytes:primitiveLookup)]
[function, symbol(ListBytes:primitiveLookup)]
// -----------------------------------------------------------
rule L:ListBytes {{ I:Int }} => unwrap( L[ I ] )

syntax Bytes ::= ListBytes "{{" Int "}}" "orDefault" Bytes
[ function, total, symbol, klabel(ListBytes:primitiveLookupOrDefault) ]
[ function, total, symbol(ListBytes:primitiveLookupOrDefault) ]
// -----------------------------------------------------------------------------
rule L:ListBytes {{ I:Int }} orDefault Value:Bytes
=> unwrap( L [I] orDefault wrap(Value) )
Expand All @@ -77,9 +77,16 @@ module LIST-BYTES-EXTENSIONS
[simplification]

syntax ListBytes ::= ListItemWrap( Bytes )
[function, total, symbol, klabel(ListBytesItemWrap)]
[function, total, symbol(ListBytesItemWrap)]
rule ListItemWrap( B:Bytes ) => ListItem(wrap(B))


syntax ListBytes ::= ListBytes "{{" Int "<-" Bytes "}}"
[function, symbol(ListBytes:primitiveSet)]
// -----------------------------------------------------------
rule L:ListBytes {{ I:Int <- V:Bytes }}
=> L[ I <- wrap(V)]

// Workaround for the Haskell backend missing the range hook.
// See https://github.com/runtimeverification/haskell-backend/issues/3706
rule range(ListItem(_) L:ListBytes, FromStart:Int, FromEnd:Int)
Expand All @@ -102,7 +109,7 @@ module LIST-BYTES-EXTENSIONS
[simplification]

syntax ListBytes ::= rangeTotal(ListBytes, Int, Int)
[function, total, klabel(ListBytes:rangeTotal), symbol]
[function, total, symbol(ListBytes:rangeTotal)]
// ----------------------------------------------------------
rule rangeTotal(L, Front, Back) => range(L, Front, Back)
requires 0 <=Int Front
Expand All @@ -120,5 +127,5 @@ module LIST-BYTES-EXTENSIONS
requires 0 <=Int Front
andBool 0 <=Int Back
andBool size(L) <Int Front +Int Back

endmodule
70 changes: 36 additions & 34 deletions kmultiversx/src/kmultiversx/kdist/mx-semantics/data/map-bytes-to-bytes.k
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@

requires "bytes-type.k"
// requires "bytes-type.k"
requires "list-bytes.k"

module MAP-BYTES-TO-BYTES
imports private BOOL-SYNTAX
Expand All @@ -18,35 +19,35 @@ module MAP-BYTES-TO-BYTES

syntax MapBytesToBytes [hook(MAP.Map)]
syntax MapBytesToBytes ::= MapBytesToBytes MapBytesToBytes
[ left, function, hook(MAP.concat), klabel(_MapBytesToBytes_),
symbol, assoc, comm, unit(.MapBytesToBytes), element(_Bytes2Bytes|->_),
[ left, function, hook(MAP.concat), symbol(_MapBytesToBytes_),
assoc, comm, unit(.MapBytesToBytes), element(_Bytes2Bytes|->_),
index(0), format(%1%n%2)
]
syntax MapBytesToBytes ::= ".MapBytesToBytes"
[ function, total, hook(MAP.unit),
klabel(.MapBytesToBytes), symbol
symbol(.MapBytesToBytes)
]
syntax MapBytesToBytes ::= WrappedBytes "Bytes2Bytes|->" WrappedBytes
[ function, total, hook(MAP.element),
klabel(_Bytes2Bytes|->_), symbol,
symbol(_Bytes2Bytes|->_),
injective
]

syntax priority _Bytes2Bytes|->_ > _MapBytesToBytes_ .MapBytesToBytes
syntax non-assoc _Bytes2Bytes|->_
syntax WrappedBytes ::= MapBytesToBytes "[" WrappedBytes "]"
[function, hook(MAP.lookup), klabel(MapBytesToBytes:lookup), symbol]
[function, hook(MAP.lookup), symbol(MapBytesToBytes:lookup)]
syntax WrappedBytes ::= MapBytesToBytes "[" WrappedBytes "]" "orDefault" WrappedBytes
[ function, total, hook(MAP.lookupOrDefault),
klabel(MapBytesToBytes:lookupOrDefault), symbol
symbol(MapBytesToBytes:lookupOrDefault)
]
syntax MapBytesToBytes ::= MapBytesToBytes "[" key: WrappedBytes "<-" value: WrappedBytes "]"
[ function, total, klabel(MapBytesToBytes:update), symbol,
[ function, total, symbol(MapBytesToBytes:update),
hook(MAP.update), prefer
]
syntax MapBytesToBytes ::= MapBytesToBytes "[" WrappedBytes "<-" "undef" "]"
[ function, total, hook(MAP.remove),
klabel(_MapBytesToBytes[_<-undef]), symbol
symbol(_MapBytesToBytes[_<-undef])
]
syntax MapBytesToBytes ::= MapBytesToBytes "-Map" MapBytesToBytes
[ function, total, hook(MAP.difference) ]
Expand Down Expand Up @@ -77,11 +78,11 @@ module MAP-BYTES-TO-BYTES
[function, hook(MAP.values)]

syntax Int ::= size(MapBytesToBytes)
[function, total, hook(MAP.size), klabel(MapBytesToBytes.sizeMap), symbol]
[function, total, hook(MAP.size), symbol(MapBytesToBytes.sizeMap)]
syntax Bool ::= MapBytesToBytes "<=Map" MapBytesToBytes
[function, total, hook(MAP.inclusion)]
syntax WrappedBytes ::= choice(MapBytesToBytes)
[function, hook(MAP.choice), klabel(MapBytesToBytes:choice), symbol]
[function, hook(MAP.choice), symbol(MapBytesToBytes:choice)]
endmodule

module MAP-BYTES-TO-BYTES-PRIMITIVE
Expand All @@ -95,17 +96,17 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-CONCRETE [concrete]
imports public MAP-BYTES-TO-BYTES

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

rule (M:MapBytesToBytes {{ Key:Bytes }})
=> (unwrap( M[wrap(Key)] ))
Expand All @@ -125,17 +126,17 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic]
imports private MAP-BYTES-TO-BYTES-KORE-SYMBOLIC

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

// Definitions
// -----------
Expand Down Expand Up @@ -253,12 +254,12 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic]
rule (K1 Bytes2Bytes|-> V1 M:MapBytesToBytes) {{ K2 <- V2 }}
=> (K1 Bytes2Bytes|-> V1 (M {{ K2 <- V2 }}))
requires unwrap( K1 ) =/=K K2
[simplification]
[simplification, preserves-definedness]

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

rule (K1 Bytes2Bytes|-> _V M:MapBytesToBytes) {{ K2 }} => M {{K2}}
requires unwrap( K1 ) =/=K K2
Expand All @@ -282,8 +283,8 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic]

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 orBool K1 in_keys{{M}}
rule K1 in_keys{{ _M:MapBytesToBytes {{ K2 <- _ }} }}
=> true requires K1 ==K K2
[simplification]
rule K1 in_keys{{ M:MapBytesToBytes {{ K2 <- _ }} }}
=> K1 in_keys {{ M }}
Expand All @@ -293,7 +294,7 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic]
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)]
[simplification(100), preserves-definedness]


rule {false #Equals @Key in_keys{{ Key' Bytes2Bytes|-> Val @M:MapBytesToBytes }}}
Expand Down Expand Up @@ -322,13 +323,14 @@ module MAP-BYTES-TO-BYTES-KORE-SYMBOLIC
#And #Ceil(@M) #And #Ceil(@K)
[simplification]

rule (K Bytes2Bytes|-> _ M:MapBytesToBytes) [ K <- V ] => (K Bytes2Bytes|-> V M) [simplification]
rule (K Bytes2Bytes|-> _ M:MapBytesToBytes) [ K <- V ] => (K Bytes2Bytes|-> V M)
[simplification, preserves-definedness]
rule M:MapBytesToBytes [ K <- V ] => (K Bytes2Bytes|-> V M) requires notBool (K in_keys(M))
[simplification]
[simplification, preserves-definedness]
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 K1 =/=K K2
[simplification]
[simplification, preserves-definedness]

rule (K Bytes2Bytes|-> _ M:MapBytesToBytes) [ K <- undef ] => M
ensures notBool (K in_keys(M))
Expand All @@ -339,7 +341,7 @@ module MAP-BYTES-TO-BYTES-KORE-SYMBOLIC
rule (K1 Bytes2Bytes|-> V1 M:MapBytesToBytes) [ K2 <- undef ]
=> (K1 Bytes2Bytes|-> V1 (M [ K2 <- undef ]))
requires K1 =/=K K2
[simplification]
[simplification, preserves-definedness]

rule (K Bytes2Bytes|-> V M:MapBytesToBytes) [ K ] => V
ensures notBool (K in_keys(M))
Expand Down Expand Up @@ -381,17 +383,17 @@ module MAP-BYTES-TO-BYTES-KORE-SYMBOLIC
rule K in_keys((K Bytes2Bytes|-> V) M:MapBytesToBytes)
=> true
requires definedMapElementConcat(K, V, M)
[simplification(50)]
[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 K1 =/=K K2
[simplification(50)]
[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)
[simplification(100)]
[simplification(100), preserves-definedness]


rule {false #Equals @Key in_keys(.MapBytesToBytes)} => #Ceil(@Key) [simplification]
Expand All @@ -414,15 +416,15 @@ module MAP-BYTES-TO-BYTES-CURLY-BRACE
imports MAP-BYTES-TO-BYTES

syntax MapBytesToBytes ::= MapBytesToBytes "{" key:WrappedBytes "<-" value:WrappedBytes "}"
[function, total, symbol, klabel(MapBytesToBytes:curly_update)]
[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]
[simplification, preserves-definedness]

rule M:MapBytesToBytes{Key1 <- Value1}[Key2 <- Value2]
=> ((M:MapBytesToBytes[Key2 <- Value2]{Key1 <- Value1}) #And #Not ({Key1 #Equals Key2}))
Expand Down
Loading

0 comments on commit 5e23591

Please sign in to comment.