diff --git a/kmultiversx/pyproject.toml b/kmultiversx/pyproject.toml index 19725e03..939d73cd 100644 --- a/kmultiversx/pyproject.toml +++ b/kmultiversx/pyproject.toml @@ -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. ", diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/list-bytes.k b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/list-bytes.k index c02fa2e1..f1de7b94 100644 --- a/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/list-bytes.k +++ b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/list-bytes.k @@ -10,22 +10,22 @@ 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) @@ -33,11 +33,11 @@ module LIST-BYTES 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 @@ -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) ) @@ -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) @@ -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 @@ -120,5 +127,5 @@ module LIST-BYTES-EXTENSIONS requires 0 <=Int Front andBool 0 <=Int Back andBool size(L) _), + [ 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) ] @@ -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 @@ -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)] )) @@ -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 // ----------- @@ -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 @@ -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 }} @@ -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 }}} @@ -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)) @@ -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)) @@ -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] @@ -414,7 +416,7 @@ 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} @@ -422,7 +424,7 @@ module MAP-BYTES-TO-BYTES-CURLY-BRACE 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})) diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/map-int-to-bytes.k b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/map-int-to-bytes.k index fc0c4a66..da1c0235 100644 --- a/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/map-int-to-bytes.k +++ b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/map-int-to-bytes.k @@ -5,9 +5,9 @@ requires "bytes-type.k" module MAP-INT-TO-BYTES imports private BOOL-SYNTAX imports private INT-SYNTAX - // imports private LIST-INT + imports private LIST-INT imports private LIST-BYTES - imports private LIST + // imports private LIST // imports private SET-INT imports private SET imports INT-TYPE @@ -18,35 +18,35 @@ module MAP-INT-TO-BYTES syntax MapIntToBytes [hook(MAP.Map)] syntax MapIntToBytes ::= MapIntToBytes MapIntToBytes - [ left, function, hook(MAP.concat), klabel(_MapIntToBytes_), - symbol, assoc, comm, unit(.MapIntToBytes), element(_Int2Bytes|->_), + [ left, function, hook(MAP.concat), symbol(_MapIntToBytes_), + assoc, comm, unit(.MapIntToBytes), element(_Int2Bytes|->_), index(0), format(%1%n%2) ] syntax MapIntToBytes ::= ".MapIntToBytes" [ function, total, hook(MAP.unit), - klabel(.MapIntToBytes), symbol + symbol(.MapIntToBytes) ] syntax MapIntToBytes ::= WrappedInt "Int2Bytes|->" WrappedBytes [ function, total, hook(MAP.element), - klabel(_Int2Bytes|->_), symbol, + symbol(_Int2Bytes|->_), injective ] syntax priority _Int2Bytes|->_ > _MapIntToBytes_ .MapIntToBytes syntax non-assoc _Int2Bytes|->_ syntax WrappedBytes ::= MapIntToBytes "[" WrappedInt "]" - [function, hook(MAP.lookup), klabel(MapIntToBytes:lookup), symbol] + [function, hook(MAP.lookup), symbol(MapIntToBytes:lookup)] syntax WrappedBytes ::= MapIntToBytes "[" WrappedInt "]" "orDefault" WrappedBytes [ function, total, hook(MAP.lookupOrDefault), - klabel(MapIntToBytes:lookupOrDefault), symbol + symbol(MapIntToBytes:lookupOrDefault) ] syntax MapIntToBytes ::= MapIntToBytes "[" key: WrappedInt "<-" value: WrappedBytes "]" - [ function, total, klabel(MapIntToBytes:update), symbol, + [ function, total, symbol(MapIntToBytes:update), hook(MAP.update), prefer ] syntax MapIntToBytes ::= MapIntToBytes "[" WrappedInt "<-" "undef" "]" [ function, total, hook(MAP.remove), - klabel(_MapIntToBytes[_<-undef]), symbol + symbol(_MapIntToBytes[_<-undef]) ] syntax MapIntToBytes ::= MapIntToBytes "-Map" MapIntToBytes [ function, total, hook(MAP.difference) ] @@ -63,10 +63,10 @@ module MAP-INT-TO-BYTES // syntax SetInt ::= keys(MapIntToBytes) // [function, total, hook(MAP.keys)] - syntax List ::= "keys_list" "(" MapIntToBytes ")" - [function, hook(MAP.keys_list)] - // syntax ListInt ::= "keys_list" "(" MapIntToBytes ")" + // syntax List ::= "keys_list" "(" MapIntToBytes ")" // [function, hook(MAP.keys_list)] + syntax ListInt ::= "keys_list" "(" MapIntToBytes ")" + [function, hook(MAP.keys_list)] syntax Bool ::= WrappedInt "in_keys" "(" MapIntToBytes ")" [function, total, hook(MAP.in_keys)] @@ -77,11 +77,11 @@ module MAP-INT-TO-BYTES [function, hook(MAP.values)] syntax Int ::= size(MapIntToBytes) - [function, total, hook(MAP.size), klabel(MapIntToBytes.sizeMap), symbol] + [function, total, hook(MAP.size), symbol(MapIntToBytes.sizeMap)] syntax Bool ::= MapIntToBytes "<=Map" MapIntToBytes [function, total, hook(MAP.inclusion)] syntax WrappedInt ::= choice(MapIntToBytes) - [function, hook(MAP.choice), klabel(MapIntToBytes:choice), symbol] + [function, hook(MAP.choice), symbol(MapIntToBytes:choice)] endmodule module MAP-INT-TO-BYTES-PRIMITIVE @@ -95,17 +95,17 @@ module MAP-INT-TO-BYTES-PRIMITIVE-CONCRETE [concrete] imports public MAP-INT-TO-BYTES syntax Bytes ::= MapIntToBytes "{{" Int "}}" - [function, klabel(MapIntToBytes:primitiveLookup), symbol] + [function, symbol(MapIntToBytes:primitiveLookup)] syntax Bytes ::= MapIntToBytes "{{" Int "}}" "orDefault" Bytes - [ function, total, klabel(MapIntToBytes:primitiveLookupOrDefault), symbol ] + [ function, total, symbol(MapIntToBytes:primitiveLookupOrDefault) ] syntax MapIntToBytes ::= MapIntToBytes "{{" key: Int "<-" value: Bytes "}}" - [ function, total, klabel(MapIntToBytes:primitiveUpdate), symbol, + [ function, total, symbol(MapIntToBytes:primitiveUpdate), prefer ] syntax MapIntToBytes ::= MapIntToBytes "{{" Int "<-" "undef" "}}" - [ function, total, klabel(MapIntToBytes:primitiveRemove), symbol ] + [ function, total, symbol(MapIntToBytes:primitiveRemove) ] syntax Bool ::= Int "in_keys" "{{" MapIntToBytes "}}" - [function, total, klabel(MapIntToBytes:primitiveInKeys), symbol] + [function, total, symbol(MapIntToBytes:primitiveInKeys)] rule (M:MapIntToBytes {{ Key:Int }}) => (unwrap( M[wrap(Key)] )) @@ -125,17 +125,17 @@ module MAP-INT-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic] imports private MAP-INT-TO-BYTES-KORE-SYMBOLIC syntax Bytes ::= MapIntToBytes "{{" Int "}}" - [function, symbol, klabel(MapIntToBytes:primitiveLookup)] + [function, symbol(MapIntToBytes:primitiveLookup)] syntax Bytes ::= MapIntToBytes "{{" Int "}}" "orDefault" Bytes - [ function, total, symbol, klabel(MapIntToBytes:primitiveLookupOrDefault) ] + [ function, total, symbol(MapIntToBytes:primitiveLookupOrDefault) ] syntax MapIntToBytes ::= MapIntToBytes "{{" key: Int "<-" value: Bytes "}}" - [ function, total, klabel(MapIntToBytes:primitiveUpdate), symbol, + [ function, total, symbol(MapIntToBytes:primitiveUpdate), prefer ] syntax MapIntToBytes ::= MapIntToBytes "{{" Int "<-" "undef" "}}" - [ function, total, symbol, klabel(MapIntToBytes:primitiveRemove) ] + [ function, total, symbol(MapIntToBytes:primitiveRemove) ] syntax Bool ::= Int "in_keys" "{{" MapIntToBytes "}}" - [function, total, symbol, klabel(MapIntToBytes:primitiveInKeys)] + [function, total, symbol(MapIntToBytes:primitiveInKeys)] // Definitions // ----------- @@ -253,12 +253,12 @@ module MAP-INT-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic] rule (K1 Int2Bytes|-> V1 M:MapIntToBytes) {{ K2 <- V2 }} => (K1 Int2Bytes|-> V1 (M {{ K2 <- V2 }})) requires unwrap( K1 ) =/=K K2 - [simplification] + [simplification, preserves-definedness] rule (K1 Int2Bytes|-> V1 M:MapIntToBytes) {{ K2 <- undef }} => (K1 Int2Bytes|-> V1 (M {{ K2 <- undef }})) requires unwrap( K1 ) =/=K K2 - [simplification] + [simplification, preserves-definedness] rule (K1 Int2Bytes|-> _V M:MapIntToBytes) {{ K2 }} => M {{K2}} requires unwrap( K1 ) =/=K K2 @@ -282,8 +282,8 @@ module MAP-INT-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic] rule K in_keys{{_M:MapIntToBytes {{ K <- undef }} }} => false [simplification] rule K in_keys{{_M:MapIntToBytes {{ K <- _ }} }} => true [simplification] - rule K1 in_keys{{ M:MapIntToBytes {{ K2 <- _ }} }} - => true requires K1 ==K K2 orBool K1 in_keys{{M}} + rule K1 in_keys{{ _M:MapIntToBytes {{ K2 <- _ }} }} + => true requires K1 ==K K2 [simplification] rule K1 in_keys{{ M:MapIntToBytes {{ K2 <- _ }} }} => K1 in_keys {{ M }} @@ -293,7 +293,7 @@ module MAP-INT-TO-BYTES-PRIMITIVE-SYMBOLIC [symbolic] rule K1 in_keys {{ (K2 Int2Bytes|-> V) M:MapIntToBytes }} => 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' Int2Bytes|-> Val @M:MapIntToBytes }}} @@ -322,13 +322,14 @@ module MAP-INT-TO-BYTES-KORE-SYMBOLIC #And #Ceil(@M) #And #Ceil(@K) [simplification] - rule (K Int2Bytes|-> _ M:MapIntToBytes) [ K <- V ] => (K Int2Bytes|-> V M) [simplification] + rule (K Int2Bytes|-> _ M:MapIntToBytes) [ K <- V ] => (K Int2Bytes|-> V M) + [simplification, preserves-definedness] rule M:MapIntToBytes [ K <- V ] => (K Int2Bytes|-> V M) requires notBool (K in_keys(M)) - [simplification] + [simplification, preserves-definedness] rule M:MapIntToBytes [ K <- _ ] [ K <- V ] => M [ K <- V ] [simplification] rule (K1 Int2Bytes|-> V1 M:MapIntToBytes) [ K2 <- V2 ] => (K1 Int2Bytes|-> V1 (M [ K2 <- V2 ])) requires K1 =/=K K2 - [simplification] + [simplification, preserves-definedness] rule (K Int2Bytes|-> _ M:MapIntToBytes) [ K <- undef ] => M ensures notBool (K in_keys(M)) @@ -339,7 +340,7 @@ module MAP-INT-TO-BYTES-KORE-SYMBOLIC rule (K1 Int2Bytes|-> V1 M:MapIntToBytes) [ K2 <- undef ] => (K1 Int2Bytes|-> V1 (M [ K2 <- undef ])) requires K1 =/=K K2 - [simplification] + [simplification, preserves-definedness] rule (K Int2Bytes|-> V M:MapIntToBytes) [ K ] => V ensures notBool (K in_keys(M)) @@ -381,17 +382,17 @@ module MAP-INT-TO-BYTES-KORE-SYMBOLIC rule K in_keys((K Int2Bytes|-> V) M:MapIntToBytes) => true requires definedMapElementConcat(K, V, M) - [simplification(50)] + [simplification(50), preserves-definedness] rule K1 in_keys((K2 Int2Bytes|-> V) M:MapIntToBytes) => 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 Int2Bytes|-> V) M:MapIntToBytes) => 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(.MapIntToBytes)} => #Ceil(@Key) [simplification] @@ -414,7 +415,7 @@ module MAP-INT-TO-BYTES-CURLY-BRACE imports MAP-INT-TO-BYTES syntax MapIntToBytes ::= MapIntToBytes "{" key:WrappedInt "<-" value:WrappedBytes "}" - [function, total, symbol, klabel(MapIntToBytes:curly_update)] + [function, total, symbol(MapIntToBytes:curly_update)] rule M:MapIntToBytes{Key <- Value} => M (Key Int2Bytes|-> Value) requires notBool Key in_keys(M) rule (Key Int2Bytes|-> _ M:MapIntToBytes){Key <- Value} @@ -422,7 +423,7 @@ module MAP-INT-TO-BYTES-CURLY-BRACE rule (M:MapIntToBytes{Key <- Value})(A Int2Bytes|-> B N:MapIntToBytes) => (M (A Int2Bytes|-> B)) {Key <- Value} N requires notBool A ==K Key - [simplification] + [simplification, preserves-definedness] rule M:MapIntToBytes{Key1 <- Value1}[Key2 <- Value2] => ((M:MapIntToBytes[Key2 <- Value2]{Key1 <- Value1}) #And #Not ({Key1 #Equals Key2})) diff --git a/package/version b/package/version index ad069db6..1f7a170d 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.76 +0.1.77