diff --git a/media/201903-report-chalmers.md b/media/201903-report-chalmers.md
index 10ad7770e..886c3402b 100644
--- a/media/201903-report-chalmers.md
+++ b/media/201903-report-chalmers.md
@@ -800,7 +800,7 @@ This is the full definition of the `(memory.grow)` operation:
#then SIZE
#else -1
#fi ...
- wrap(0) Int2Int|-> wrap(ADDR)
+ 0 |-> ADDR
ADDR
MAX
diff --git a/media/memory-demo/memory-spec.k b/media/memory-demo/memory-spec.k
index 3c12d7cdd..e8dc009c5 100644
--- a/media/memory-demo/memory-spec.k
+++ b/media/memory-demo/memory-spec.k
@@ -2,14 +2,14 @@ module MEMORY-SPEC
imports WASM
rule ( memory.size ) => (i32.const SZ) ...
- wrap(0) Int2Int|-> wrap(A)
+ 0 |-> A
A
SZ
rule (memory.grow (i32.const X)) => (i32.const SZ) ...
- wrap(0) Int2Int|-> wrap(A)
+ 0 |-> A
A
SZ => (SZ +Int X)
@@ -21,7 +21,7 @@ module MEMORY-SPEC
andBool SZ >=Int 0
rule (memory.grow (i32.const X)) => (i32.const -1) ...
- wrap(0) Int2Int|-> wrap(A)
+ 0 |-> A
A
SZ
diff --git a/media/memory-demo/wasm.k b/media/memory-demo/wasm.k
index d17cd5707..4d3e548da 100644
--- a/media/memory-demo/wasm.k
+++ b/media/memory-demo/wasm.k
@@ -104,7 +104,7 @@ endmodule
false
rule (( memory ) ~> ELSE) => ELSE
- .MapIntToInt => wrap(0) Int2Int|-> wrap(NEXT)
+ .Map => 0 |-> NEXT
NEXT => NEXT +Int 1
(.Bag =>
@@ -118,7 +118,7 @@ endmodule
syntax Instr ::= "(" "memory.size" ")"
// --------------------------------------
rule ( memory.size ) => ( i32.const SZ ) ...
- wrap(0) Int2Int|-> wrap(A)
+ 0 |-> A
A
SZ
@@ -131,7 +131,7 @@ endmodule
rule (memory.grow I:Instr) => I ~> (memory.grow) ...
rule (memory.grow) => (i32.const SZ) ...
< i32 > V : S => S
- wrap(0) Int2Int|-> wrap(A)
+ 0 |-> A
A
SZ => SZ +Int V
diff --git a/package/version b/package/version
index f0768f091..7c3ae4e02 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.70
+0.1.71
diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml
index 0924280e6..372bce5d2 100644
--- a/pykwasm/pyproject.toml
+++ b/pykwasm/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
[tool.poetry]
name = "pykwasm"
-version = "0.1.70"
+version = "0.1.71"
description = ""
authors = [
"Runtime Verification, Inc. ",
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/map-int-to-int.k b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/map-int-to-int.k
deleted file mode 100644
index 8bb1ece79..000000000
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/map-int-to-int.k
+++ /dev/null
@@ -1,463 +0,0 @@
-
-requires "int-type.k"
-// requires "int-type.k"
-requires "list-int.k"
-
-module MAP-INT-TO-INT
- imports private BOOL-SYNTAX
- imports private INT-SYNTAX
- imports private LIST-INT
- imports private LIST-INT
- // imports private LIST
- // imports private SET-INT
- imports private SET
- imports INT-TYPE
- imports INT-TYPE
-
- syntax Int
- syntax Int
-
- syntax MapIntToInt [hook(MAP.Map)]
- syntax MapIntToInt ::= MapIntToInt MapIntToInt
- [ left, function, hook(MAP.concat), symbol(_MapIntToInt_),
- assoc, comm, unit(.MapIntToInt), element(_Int2Int|->_),
- index(0), format(%1%n%2)
- ]
- syntax MapIntToInt ::= ".MapIntToInt"
- [ function, total, hook(MAP.unit),
- symbol(.MapIntToInt)
- ]
- syntax MapIntToInt ::= WrappedInt "Int2Int|->" WrappedInt
- [ function, total, hook(MAP.element),
- symbol(_Int2Int|->_),
- injective
- ]
-
- syntax priority _Int2Int|->_ > _MapIntToInt_ .MapIntToInt
- syntax non-assoc _Int2Int|->_
- syntax WrappedInt ::= MapIntToInt "[" WrappedInt "]"
- [function, hook(MAP.lookup), symbol(MapIntToInt:lookup)]
- syntax WrappedInt ::= MapIntToInt "[" WrappedInt "]" "orDefault" WrappedInt
- [ function, total, hook(MAP.lookupOrDefault),
- symbol(MapIntToInt:lookupOrDefault)
- ]
- syntax MapIntToInt ::= MapIntToInt "[" key: WrappedInt "<-" value: WrappedInt "]"
- [ function, total, symbol(MapIntToInt:update),
- hook(MAP.update), prefer
- ]
- syntax MapIntToInt ::= MapIntToInt "[" WrappedInt "<-" "undef" "]"
- [ function, total, hook(MAP.remove),
- symbol(_MapIntToInt[_<-undef])
- ]
- syntax MapIntToInt ::= MapIntToInt "-Map" MapIntToInt
- [ function, total, hook(MAP.difference) ]
- syntax MapIntToInt ::= updateMap(MapIntToInt, MapIntToInt)
- [function, total, hook(MAP.updateAll)]
-
- syntax MapIntToInt ::= removeAll(MapIntToInt, Set)
- [function, total, hook(MAP.removeAll)]
- // syntax MapIntToInt ::= removeAll(MapIntToInt, SetInt)
- // [function, total, hook(MAP.removeAll)]
-
- syntax Set ::= keys(MapIntToInt)
- [function, total, hook(MAP.keys)]
- // syntax SetInt ::= keys(MapIntToInt)
- // [function, total, hook(MAP.keys)]
-
- // syntax List ::= "keys_list" "(" MapIntToInt ")"
- // [function, hook(MAP.keys_list)]
- syntax ListInt ::= "keys_list" "(" MapIntToInt ")"
- [function, hook(MAP.keys_list)]
-
- syntax Bool ::= WrappedInt "in_keys" "(" MapIntToInt ")"
- [function, total, hook(MAP.in_keys)]
-
- // syntax List ::= values(MapIntToInt)
- // [function, hook(MAP.values)]
- syntax ListInt ::= values(MapIntToInt)
- [function, hook(MAP.values)]
-
- syntax Int ::= size(MapIntToInt)
- [function, total, hook(MAP.size), symbol(MapIntToInt.sizeMap)]
- syntax Bool ::= MapIntToInt "<=Map" MapIntToInt
- [function, total, hook(MAP.inclusion)]
- syntax WrappedInt ::= choice(MapIntToInt)
- [function, hook(MAP.choice), symbol(MapIntToInt:choice)]
-endmodule
-
-module MAP-INT-TO-INT-PRIMITIVE
- imports MAP-INT-TO-INT-PRIMITIVE-CONCRETE
- imports MAP-INT-TO-INT-PRIMITIVE-SYMBOLIC
-endmodule
-
-module MAP-INT-TO-INT-PRIMITIVE-CONCRETE [concrete]
- imports public BOOL
- imports private K-EQUAL
- imports public MAP-INT-TO-INT
-
- syntax Int ::= MapIntToInt "{{" Int "}}"
- [function, symbol(MapIntToInt:primitiveLookup)]
- syntax Int ::= MapIntToInt "{{" Int "}}" "orDefault" Int
- [ function, total, symbol(MapIntToInt:primitiveLookupOrDefault) ]
- syntax MapIntToInt ::= MapIntToInt "{{" key: Int "<-" value: Int "}}"
- [ function, total, symbol(MapIntToInt:primitiveUpdate),
- prefer
- ]
- syntax MapIntToInt ::= MapIntToInt "{{" Int "<-" "undef" "}}"
- [ function, total, symbol(MapIntToInt:primitiveRemove) ]
- syntax Bool ::= Int "in_keys" "{{" MapIntToInt "}}"
- [function, total, symbol(MapIntToInt:primitiveInKeys)]
-
- rule (M:MapIntToInt {{ Key:Int }})
- => (unwrap( M[wrap(Key)] ))
- rule M:MapIntToInt {{ Key:Int }} orDefault Value:Int
- => unwrap( M[wrap(Key)] orDefault wrap(Value) )
- rule M:MapIntToInt {{ Key:Int <- Value:Int }}
- => M[wrap(Key) <- wrap(Value)]
- rule M:MapIntToInt {{ Key:Int <- undef }}
- => M[wrap(Key) <- undef]
- rule Key:Int in_keys {{ M:MapIntToInt }} => wrap(Key) in_keys(M)
-endmodule
-
-module MAP-INT-TO-INT-PRIMITIVE-SYMBOLIC [symbolic]
- imports public BOOL
- imports private K-EQUAL
- imports public MAP-INT-TO-INT
- imports private MAP-INT-TO-INT-KORE-SYMBOLIC
-
- syntax Int ::= MapIntToInt "{{" Int "}}"
- [function, symbol(MapIntToInt:primitiveLookup)]
- syntax Int ::= MapIntToInt "{{" Int "}}" "orDefault" Int
- [ function, total, symbol(MapIntToInt:primitiveLookupOrDefault) ]
- syntax MapIntToInt ::= MapIntToInt "{{" key: Int "<-" value: Int "}}"
- [ function, total, symbol(MapIntToInt:primitiveUpdate),
- prefer
- ]
- syntax MapIntToInt ::= MapIntToInt "{{" Int "<-" "undef" "}}"
- [ function, total, symbol(MapIntToInt:primitiveRemove) ]
- syntax Bool ::= Int "in_keys" "{{" MapIntToInt "}}"
- [function, total, symbol(MapIntToInt:primitiveInKeys)]
-
- // Definitions
- // -----------
-
- rule (wrap(Key) Int2Int|-> V:WrappedInt M:MapIntToInt)
- {{ Key:Int }}
- => unwrap( V )
- ensures notBool Key in_keys {{ M }}
-
- rule (wrap(Key) Int2Int|-> V:WrappedInt M:MapIntToInt)
- {{ Key:Int }} orDefault _:Int
- => unwrap( V )
- ensures notBool Key in_keys {{ M }}
- rule M:MapIntToInt {{ Key:Int }} orDefault V:Int
- => V
- requires notBool Key in_keys {{ M }}
-
- rule (wrap(Key) Int2Int|-> _:WrappedInt M:MapIntToInt)
- {{ Key:Int <- Value:Int }}
- => (wrap(Key) Int2Int|-> wrap(Value)) M
- rule M:MapIntToInt {{ Key:Int <- Value:Int }}
- => (wrap(Key) Int2Int|-> wrap(Value)) M
- requires notBool Key in_keys {{ M }}
-
- rule (wrap(Key) Int2Int|-> _:WrappedInt M:MapIntToInt)
- {{ Key:Int <- undef }}
- => M
- ensures notBool Key in_keys {{ M }}
- rule M:MapIntToInt {{ Key:Int <- undef }}
- => M
- requires notBool Key in_keys {{ M }}
-
- rule Key:Int in_keys
- {{wrap(Key) Int2Int|-> _:WrappedInt M:MapIntToInt}}
- => true
- ensures notBool Key in_keys {{ M }}
- rule _Key:Int in_keys {{ .MapIntToInt }}
- => 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:Int in_keys
- {{Key2:WrappedInt Int2Int|-> _:WrappedInt M:MapIntToInt}}
- => Key in_keys {{ M }}
- requires Key =/=K unwrap( Key2 )
- ensures notBool Key2 in_keys (M)
- [simplification]
-
- // Translation rules
- rule M:MapIntToInt[Key:WrappedInt]
- => wrap(M{{unwrap( Key )}})
- [simplification, symbolic(M)]
- rule M:MapIntToInt[Key:WrappedInt]
- => wrap(M{{unwrap( Key )}})
- [simplification, symbolic(Key)]
- rule M:MapIntToInt{{Key}}
- => unwrap( M[wrap(Key)] )
- [simplification, concrete]
-
- rule M:MapIntToInt [ Key:WrappedInt ] orDefault Value:WrappedInt
- => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
- [simplification, symbolic(M)]
- rule M:MapIntToInt [ Key:WrappedInt ] orDefault Value:WrappedInt
- => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
- [simplification, symbolic(Key)]
- rule M:MapIntToInt [ Key:WrappedInt ] orDefault Value:WrappedInt
- => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
- [simplification, symbolic(Value)]
- rule M:MapIntToInt{{Key}} orDefault Value
- => unwrap( M[wrap(Key)] orDefault wrap(Value) )
- [simplification, concrete]
-
- rule M:MapIntToInt[Key:WrappedInt <- Value:WrappedInt]
- => M {{ unwrap( Key ) <- unwrap( Value ) }}
- [simplification, symbolic(M)]
- rule M:MapIntToInt[Key:WrappedInt <- Value:WrappedInt]
- => M {{ unwrap( Key ) <- unwrap( Value ) }}
- [simplification, symbolic(Key)]
- rule M:MapIntToInt[Key:WrappedInt <- Value:WrappedInt]
- => M {{ unwrap( Key ) <- unwrap( Value ) }}
- [simplification, symbolic(Value)]
- rule M:MapIntToInt{{Key <- Value}} => M[wrap(Key) <- wrap(Value) ]
- [simplification, concrete]
-
- rule M:MapIntToInt[Key:WrappedInt <- undef]
- => M {{ unwrap( Key ) <- undef }}
- [simplification, symbolic(M)]
- rule M:MapIntToInt[Key:WrappedInt <- undef]
- => M {{ unwrap( Key ) <- undef }}
- [simplification, symbolic(Key)]
- rule M:MapIntToInt{{Key <- undef}} => M[wrap(Key) <- undef]
- [simplification, concrete]
-
- rule Key:WrappedInt in_keys (M:MapIntToInt)
- => unwrap( Key ) in_keys {{M}}
- [simplification, symbolic(M)]
- rule Key:WrappedInt in_keys (M:MapIntToInt)
- => unwrap( Key ) in_keys {{M}}
- [simplification, symbolic(Key)]
- rule Key in_keys {{M:MapIntToInt}} => wrap(Key) in_keys(M)
- [simplification, concrete]
-
- // Symbolic execution rules
- // ------------------------
- syntax Bool ::= definedPrimitiveLookup(MapIntToInt, Int) [function, total]
- rule definedPrimitiveLookup(M:MapIntToInt, K:Int) => K in_keys{{M}}
-
- rule #Ceil(@M:MapIntToInt {{@K:Int}})
- => {definedPrimitiveLookup(@M, @K) #Equals true}
- #And #Ceil(@M) #And #Ceil(@K)
- [simplification]
-
- rule M:MapIntToInt {{ K <- _ }} {{ K <- V }} => M {{ K <- V }} [simplification]
- rule (K1 Int2Int|-> V1 M:MapIntToInt) {{ K2 <- V2 }}
- => (K1 Int2Int|-> V1 (M {{ K2 <- V2 }}))
- requires unwrap( K1 ) =/=K K2
- [simplification, preserves-definedness]
-
- rule (K1 Int2Int|-> V1 M:MapIntToInt) {{ K2 <- undef }}
- => (K1 Int2Int|-> V1 (M {{ K2 <- undef }}))
- requires unwrap( K1 ) =/=K K2
- [simplification, preserves-definedness]
-
- rule (K1 Int2Int|-> _V M:MapIntToInt) {{ K2 }} => M {{K2}}
- requires unwrap( K1 ) =/=K K2
- ensures notBool (K1 in_keys(M))
- [simplification]
- rule (_MAP:MapIntToInt {{ K <- V1 }}) {{ K }} => V1 [simplification]
- rule ( MAP:MapIntToInt {{ K1 <- _V1 }}) {{ K2 }} => MAP {{ K2 }}
- requires K1 =/=K K2
- [simplification]
-
- rule (K1 Int2Int|-> _V M:MapIntToInt) {{ K2 }} orDefault D
- => M {{K2}} orDefault D
- requires unwrap( K1 ) =/=K K2
- ensures notBool (K1 in_keys(M))
- [simplification]
- rule (_MAP:MapIntToInt {{ K <- V1 }}) {{ K }} orDefault _ => V1 [simplification]
- rule ( MAP:MapIntToInt {{ K1 <- _V1 }}) {{ K2 }} orDefault D
- => MAP {{ K2 }} orDefault D
- requires K1 =/=K K2
- [simplification]
-
- rule K in_keys{{_M:MapIntToInt {{ K <- undef }} }} => false [simplification]
- rule K in_keys{{_M:MapIntToInt {{ K <- _ }} }} => true [simplification]
- rule K1 in_keys{{ _M:MapIntToInt {{ K2 <- _ }} }}
- => true requires K1 ==K K2
- [simplification]
- rule K1 in_keys{{ M:MapIntToInt {{ K2 <- _ }} }}
- => K1 in_keys {{ M }}
- requires K1 =/=K K2
- [simplification]
-
- rule K1 in_keys {{ (K2 Int2Int|-> V) M:MapIntToInt }}
- => 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' Int2Int|-> Val @M:MapIntToInt }}}
- => #Ceil(@Key) #And #Ceil(Key' Int2Int|-> Val @M)
- #And #Not({ @Key #Equals unwrap( Key' ) })
- #And {false #Equals @Key in_keys{{@M}}}
- [simplification]
- rule {@Key in_keys{{Key' Int2Int|-> Val @M:MapIntToInt}} #Equals false}
- => #Ceil(@Key) #And #Ceil(Key' Int2Int|-> Val @M)
- #And #Not({@Key #Equals unwrap( Key' ) })
- #And {@Key in_keys{{@M}} #Equals false}
- [simplification]
-
-endmodule
-
-module MAP-INT-TO-INT-KORE-SYMBOLIC
- imports MAP-INT-TO-INT
- imports private K-EQUAL
- imports private BOOL
-
- syntax Bool ::= definedMapElementConcat(WrappedInt, WrappedInt, MapIntToInt) [function, total]
- rule definedMapElementConcat(K, _V, M:MapIntToInt) => notBool K in_keys(M)
-
- rule #Ceil(@M:MapIntToInt [@K:WrappedInt])
- => {(@K in_keys(@M)) #Equals true}
- #And #Ceil(@M) #And #Ceil(@K)
- [simplification]
-
- rule (K Int2Int|-> _ M:MapIntToInt) [ K <- V ] => (K Int2Int|-> V M)
- [simplification, preserves-definedness]
- rule M:MapIntToInt [ K <- V ] => (K Int2Int|-> V M) requires notBool (K in_keys(M))
- [simplification, preserves-definedness]
- rule M:MapIntToInt [ K <- _ ] [ K <- V ] => M [ K <- V ] [simplification]
- rule (K1 Int2Int|-> V1 M:MapIntToInt) [ K2 <- V2 ] => (K1 Int2Int|-> V1 (M [ K2 <- V2 ]))
- requires K1 =/=K K2
- [simplification, preserves-definedness]
-
- rule (K Int2Int|-> _ M:MapIntToInt) [ K <- undef ] => M
- ensures notBool (K in_keys(M))
- [simplification]
- rule M:MapIntToInt [ K <- undef ] => M
- requires notBool (K in_keys(M))
- [simplification]
- rule (K1 Int2Int|-> V1 M:MapIntToInt) [ K2 <- undef ]
- => (K1 Int2Int|-> V1 (M [ K2 <- undef ]))
- requires K1 =/=K K2
- [simplification, preserves-definedness]
-
- rule (K Int2Int|-> V M:MapIntToInt) [ K ] => V
- ensures notBool (K in_keys(M))
- [simplification]
- rule (K1 Int2Int|-> _V M:MapIntToInt) [ K2 ] => M [K2]
- requires K1 =/=K K2
- ensures notBool (K1 in_keys(M))
- [simplification]
- rule (_MAP:MapIntToInt [ K <- V1 ]) [ K ] => V1 [simplification]
- rule ( MAP:MapIntToInt [ K1 <- _V1 ]) [ K2 ] => MAP [ K2 ]
- requires K1 =/=K K2
- [simplification]
-
- rule (K Int2Int|-> V M:MapIntToInt) [ K ] orDefault _ => V
- ensures notBool (K in_keys(M))
- [simplification]
- rule (K1 Int2Int|-> _V M:MapIntToInt) [ K2 ] orDefault D
- => M [K2] orDefault D
- requires K1 =/=K K2
- ensures notBool (K1 in_keys(M))
- [simplification]
- rule (_MAP:MapIntToInt [ K <- V1 ]) [ K ] orDefault _ => V1 [simplification]
- rule ( MAP:MapIntToInt [ K1 <- _V1 ]) [ K2 ] orDefault D
- => MAP [ K2 ] orDefault D
- requires K1 =/=K K2
- [simplification]
- rule .MapIntToInt [ _ ] orDefault D => D [simplification]
-
- rule K in_keys(_M:MapIntToInt [ K <- undef ]) => false [simplification]
- rule K in_keys(_M:MapIntToInt [ K <- _ ]) => true [simplification]
- rule K1 in_keys(M:MapIntToInt [ K2 <- _ ])
- => true requires K1 ==K K2 orBool K1 in_keys(M)
- [simplification]
- rule K1 in_keys(M:MapIntToInt [ K2 <- _ ])
- => K1 in_keys(M)
- requires K1 =/=K K2
- [simplification]
-
- rule K in_keys((K Int2Int|-> V) M:MapIntToInt)
- => true
- requires definedMapElementConcat(K, V, M)
- [simplification(50), preserves-definedness]
- rule K1 in_keys((K2 Int2Int|-> V) M:MapIntToInt)
- => K1 in_keys(M)
- requires true
- andBool definedMapElementConcat(K2, V, M)
- andBool K1 =/=K K2
- [simplification(50), preserves-definedness]
- rule K1 in_keys((K2 Int2Int|-> V) M:MapIntToInt)
- => K1 ==K K2 orBool K1 in_keys(M)
- requires definedMapElementConcat(K2, V, M)
- [simplification(100), preserves-definedness]
-
-
- rule {false #Equals @Key in_keys(.MapIntToInt)} => #Ceil(@Key) [simplification]
- rule {@Key in_keys(.MapIntToInt) #Equals false} => #Ceil(@Key) [simplification]
- rule {false #Equals @Key in_keys(Key' Int2Int|-> Val @M:MapIntToInt)}
- => #Ceil(@Key) #And #Ceil(Key' Int2Int|-> Val @M)
- #And #Not({@Key #Equals Key'})
- #And {false #Equals @Key in_keys(@M)}
- [simplification]
- rule {@Key in_keys(Key' Int2Int|-> Val @M:MapIntToInt) #Equals false}
- => #Ceil(@Key) #And #Ceil(Key' Int2Int|-> Val @M)
- #And #Not({@Key #Equals Key'})
- #And {@Key in_keys(@M) #Equals false}
- [simplification]
-endmodule
-
-module MAP-INT-TO-INT-CURLY-BRACE
- imports private BOOL
- imports private K-EQUAL-SYNTAX
- imports MAP-INT-TO-INT
-
- syntax MapIntToInt ::= MapIntToInt "{" key:WrappedInt "<-" value:WrappedInt "}"
- [function, total, symbol(MapIntToInt:curly_update)]
- rule M:MapIntToInt{Key <- Value} => M (Key Int2Int|-> Value)
- requires notBool Key in_keys(M)
- rule (Key Int2Int|-> _ M:MapIntToInt){Key <- Value}
- => M (Key Int2Int|-> Value)
- rule (M:MapIntToInt{Key <- Value})(A Int2Int|-> B N:MapIntToInt)
- => (M (A Int2Int|-> B)) {Key <- Value} N
- requires notBool A ==K Key
- [simplification, preserves-definedness]
-
- rule M:MapIntToInt{Key1 <- Value1}[Key2 <- Value2]
- => ((M:MapIntToInt[Key2 <- Value2]{Key1 <- Value1}) #And #Not ({Key1 #Equals Key2}))
- #Or ((M:MapIntToInt[Key2 <- Value2]) #And {Key1 #Equals Key2})
- [simplification(20)]
- rule M:MapIntToInt[Key <- Value]
- => M:MapIntToInt{Key <- Value}
- [simplification(100)]
- rule M:MapIntToInt{Key1 <- _Value1}[Key2] orDefault Value2
- => M[Key2] orDefault Value2
- requires Key1 =/=K Key2
- [simplification]
- rule _M:MapIntToInt{Key <- Value1}[Key] orDefault _Value2
- => Value1
- [simplification]
- // rule M:MapIntToInt{Key1 <- Value1}[Key2] orDefault Value2
- // => (M[Key2] orDefault Value2 #And #Not ({Key1 #Equals Key2}))
- // #Or (Value1 #And {Key1 #Equals Key2})
- // [simplification]
- rule M:MapIntToInt{Key1 <- Value1}[Key2]
- => (M[Key2] #And #Not ({Key1 #Equals Key2}))
- #Or (Value1 #And {Key1 #Equals Key2})
- [simplification]
-
- rule Key1 in_keys(_:MapIntToInt{Key1 <- _})
- => true
- [simplification(50)]
- rule Key1 in_keys(M:MapIntToInt{Key2 <- _})
- => Key1 in_keys(M)
- requires notBool Key1 ==K Key2
- [simplification(50)]
- rule K1 in_keys(M:MapIntToInt { K2 <- _ })
- => K1 ==K K2 orBool K1 in_keys(M)
- [simplification(100)]
-
-endmodule
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/test.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/test.md
index 59c0fb6f9..a9a27dc59 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/test.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/test.md
@@ -569,7 +569,7 @@ This checks that the last allocated memory has the given size and max value.
CUR
IDS
- wrap(#ContextLookup(IDS, TFIDX)) Int2Int|-> wrap(ADDR)
+ #ContextLookup(IDS, TFIDX) |-> ADDR
...
@@ -588,7 +588,7 @@ This checks that the last allocated memory has the given size and max value.
rule #assertMemoryData MODIDX (KEY , VAL) _MSG => .K ...
MODIDX
- wrap(0) Int2Int|-> wrap(ADDR)
+ 0 |-> ADDR
...
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
index e649bb103..f7b2d3006 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
@@ -5,7 +5,6 @@ WebAssembly State and Semantics
requires "data.md"
requires "data/list-int.k"
requires "data/list-ref.k"
-requires "data/map-int-to-int.k"
requires "data/sparse-bytes.k"
requires "data/tools.k"
requires "numeric.md"
@@ -184,8 +183,7 @@ Semantics
module WASM
imports LIST-INT
imports LIST-INT-PRIMITIVE
- imports MAP-INT-TO-INT
- imports MAP-INT-TO-INT-PRIMITIVE
+ imports MAP
imports WASM-COMMON-SYNTAX
imports WASM-INTERNAL-SYNTAX
imports WASM-DATA
@@ -219,9 +217,9 @@ module WASM
.Map
0
.Map
- .MapIntToInt
+ .Map
.Map
- .MapIntToInt
+ .Map
0
.Map
.Map
@@ -943,7 +941,7 @@ The `get` and `set` instructions read and write globals.
CUR
... TID |-> TA ...
- ... wrap(EID) Int2Int|-> wrap(EA) ...
+ ... EID |-> EA ...
...
@@ -976,7 +974,7 @@ The `get` and `set` instructions read and write globals.
CUR
CUR
- ... wrap(EID) Int2Int|-> wrap(EA) ...
+ ... EID |-> EA ...
...
@@ -1366,7 +1364,7 @@ The importing and exporting parts of specifications are dealt with in the respec
CUR
IDS => #saveId(IDS, ID, 0)
- .MapIntToInt => (wrap(0) Int2Int|-> wrap(NEXTADDR))
+ .Map => (0 |-> NEXTADDR)
...
NEXTADDR => NEXTADDR +Int 1
@@ -1397,14 +1395,15 @@ The value is encoded as bytes and stored at the "effective address", which is th
rule #store(ITYPE:IValType, SOP, OFFSET) => ITYPE . SOP (IDX +Int OFFSET) VAL ...
< ITYPE > VAL : < i32 > IDX : VALSTACK => VALSTACK
- rule store { WIDTH EA VAL } => store { WIDTH EA VAL (MEMADDRS{{0}} orDefault 0) } ...
+ rule store { WIDTH EA VAL } => store { WIDTH EA VAL ({MEMADDRS[0] orDefault 0}:>Int) } ...
CUR
CUR
MEMADDRS
...
- requires 0 in_keys{{MEMADDRS}} andBool size(MEMADDRS) ==Int 1
+ requires 0 in_keys(MEMADDRS) andBool size(MEMADDRS) ==Int 1 andBool isInt(MEMADDRS[0] orDefault 0)
+ [preserves-definedness]
rule store { WIDTH EA VAL ADDR } => .K ...
@@ -1456,14 +1455,15 @@ Sort `Signedness` is defined in module `BYTES`.
rule ITYPE . load16_s EA:Int => load { ITYPE i16 EA Signed } ...
rule i64 . load32_s EA:Int => load { i64 i32 EA Signed } ...
- rule load { ITYPE WIDTH EA SIGN } => load { ITYPE WIDTH EA SIGN (MEMADDRS{{0}} orDefault 0)} ...
+ rule load { ITYPE WIDTH EA SIGN } => load { ITYPE WIDTH EA SIGN ({MEMADDRS[0] orDefault 0}:>Int)} ...
CUR
CUR
MEMADDRS
...
- requires 0 in_keys{{MEMADDRS}} andBool size(MEMADDRS) ==Int 1
+ requires 0 in_keys(MEMADDRS) andBool size(MEMADDRS) ==Int 1 andBool isInt(MEMADDRS[0] orDefault 0)
+ [preserves-definedness]
rule load { ITYPE WIDTH EA SIGN ADDR:Int} => load { ITYPE WIDTH EA SIGN DATA } ...
@@ -1498,7 +1498,7 @@ The `size` operation returns the size of the memory, measured in pages.
CUR
CUR
- wrap(0) Int2Int|-> wrap(ADDR)
+ 0 |-> ADDR
...
@@ -1524,7 +1524,7 @@ By setting the `` field in the configuration to `true
CUR
CUR
- wrap(0) Int2Int|-> wrap(ADDR)
+ 0 |-> ADDR
...
@@ -1540,7 +1540,7 @@ By setting the `` field in the configuration to `true
CUR
CUR
- wrap(0) Int2Int|-> wrap(ADDR)
+ 0 |-> ADDR
...
@@ -1617,7 +1617,7 @@ Element Segments
CUR
FADDRS
- ADDRS => ADDRS {{ NEXTIDX <- NEXTADDR }}
+ ADDRS => ADDRS [ NEXTIDX <- NEXTADDR ]
NEXTIDX => NEXTIDX +Int 1
IDS => #saveId(IDS, OID, 0)
...
@@ -1658,7 +1658,7 @@ The `data` initializer simply puts these bytes into the specified memory, starti
CUR
CUR
- wrap(MEMIDX) Int2Int|-> wrap(ADDR)
+ MEMIDX |-> ADDR
...
@@ -1779,14 +1779,14 @@ The value of a global gets copied when it is imported.
CUR
IDS => #saveId(IDS, OID, 0)
- .MapIntToInt => wrap(0) Int2Int|-> wrap(ADDR)
+ .Map => 0 |-> ADDR
...
... MOD |-> MODIDX ...
MODIDX
IDS'
- ... wrap(#ContextLookup(IDS' , TFIDX)) Int2Int|-> wrap(ADDR) ...
+ ... #ContextLookup(IDS' , TFIDX) |-> ADDR ...
... NAME |-> TFIDX ...
...
diff --git a/tests/proofs/memory-spec.k b/tests/proofs/memory-spec.k
index 6ec2442a1..04ef37314 100644
--- a/tests/proofs/memory-spec.k
+++ b/tests/proofs/memory-spec.k
@@ -7,7 +7,7 @@ module MEMORY-SPEC
CUR
CUR
- wrap(0) Int2Int|-> wrap(MEMADDR)
+ 0 |-> MEMADDR
...
@@ -24,7 +24,7 @@ module MEMORY-SPEC
CUR
CUR
- wrap(0) Int2Int|-> wrap(MEMADDR)
+ 0 |-> MEMADDR
...
diff --git a/tests/proofs/wrc20-spec.k b/tests/proofs/wrc20-spec.k
index 0f2a1734f..4a71fdbf7 100644
--- a/tests/proofs/wrc20-spec.k
+++ b/tests/proofs/wrc20-spec.k
@@ -20,7 +20,7 @@ module WRC20-SPEC
CUR
#wrc20ReverseBytesTypeIdx |-> #wrc20ReverseBytesType
- wrap(0) Int2Int|-> wrap(MEMADDR)
+ 0 |-> MEMADDR
_ => ?_
NEXTFUNCIDX => NEXTFUNCIDX +Int 1
...