Merge remote-tracking branch 'origin/master' into release

k-distribution/include/kframework/builtin/domains.md

@@ -254,7 +254,7 @@ An element of a `Map` is constructed via the `|->` operator. The key is on the
 left and the value is on the right.
 
 ```k
-  syntax Map ::= KItem "|->" KItem                      [function, functional, hook(MAP.element), klabel(_|->_), symbol, latex({#1}\mapsto{#2})]
+  syntax Map ::= KItem "|->" KItem                      [function, functional, hook(MAP.element), klabel(_|->_), symbol, latex({#1}\mapsto{#2}), injective]
 
   syntax priorities _|->_ > _Map_ .Map
   syntax non-assoc _|->_
@@ -440,6 +440,11 @@ module MAP-KORE-SYMBOLIC [kore,symbolic]
   rule K1 in_keys(M [ K2 <- _ ]) => true requires K1 ==K K2 orBool K1 in_keys(M) [simplification]
   rule K1 in_keys(M [ K2 <- _ ]) => K1 in_keys(M) requires K1 =/=K K2 [simplification]
 
+  rule {false #Equals @Key in_keys(.Map)} => #Ceil(@Key) [simplification]
+  rule {@Key in_keys(.Map) #Equals false} => #Ceil(@Key) [simplification]
+  rule {false #Equals @Key in_keys(Key' |-> Val @M)} => #Ceil(@Key) #And #Ceil(Key' |-> Val @M) #And #Not({@Key #Equals Key'}) #And {false #Equals @Key in_keys(@M)} [simplification]
+  rule {@Key in_keys(Key' |-> Val @M) #Equals false} => #Ceil(@Key) #And #Ceil(Key' |-> Val @M) #And #Not({@Key #Equals Key'}) #And {@Key in_keys(@M) #Equals false} [simplification]
+
 /*
 // The rule below is automatically generated by the frontend for every sort
 // hooked to MAP.Map. It is left here to serve as documentation.
@@ -533,7 +538,7 @@ The set with zero elements is represented by `.Set`.
 An element of a `Set` is constructed via the `SetItem` operator.
 
 ```k
-  syntax Set ::= SetItem(KItem)               [function, functional, hook(SET.element), klabel(SetItem), symbol]
+  syntax Set ::= SetItem(KItem)               [function, functional, hook(SET.element), klabel(SetItem), symbol, injective]
 ```
 
 ### Set union
@@ -785,7 +790,7 @@ module BOOL-SYNTAX
   syntax Bool ::= "false" [token]
 endmodule
 
-module BOOL
+module BOOL-COMMON
   imports private BASIC-K
   imports BOOL-SYNTAX
 ```
@@ -860,6 +865,25 @@ operations listed above.
 
   rule B1:Bool =/=Bool B2:Bool => notBool (B1 ==Bool B2)
 endmodule
+
+module BOOL-KORE [kore, symbolic]
+  imports BOOL-COMMON
+
+  rule {true #Equals notBool @B} => {false #Equals @B} [simplification]
+  rule {notBool @B #Equals true} => {@B #Equals false} [simplification]
+  rule {false #Equals notBool @B} => {true #Equals @B} [simplification]
+  rule {notBool @B #Equals false} => {@B #Equals true} [simplification]
+
+  rule {true #Equals @B1 andBool @B2} => {true #Equals @B1} #And {true #Equals @B2} [simplification]
+  rule {@B1 andBool @B2 #Equals true} => {@B1 #Equals true} #And {@B2 #Equals true} [simplification]
+  rule {false #Equals @B1 orBool @B2} => {false #Equals @B1} #And {false #Equals @B2} [simplification]
+  rule {@B1 orBool @B2 #Equals false} => {@B1 #Equals false} #And {@B2 #Equals false} [simplification]
+endmodule
+
+module BOOL
+  imports BOOL-COMMON
+  imports BOOL-KORE
+endmodule
 ```
 
 Integers
@@ -1089,11 +1113,20 @@ module INT-KAST [kast]
 
 endmodule
 
-module INT-KORE [kore]
+module INT-KORE [kore, symbolic]
   imports private K-EQUAL
+  imports private BOOL
   imports INT-COMMON
 
-  rule I1:Int ==K I2:Int => I1 ==Int I2
+  rule I1:Int ==K I2:Int => I1 ==Int I2 [simplification]
+  rule {K1 ==Int K2 #Equals true} => {K1 #Equals K2} [simplification]
+  rule {true #Equals K1 ==Int K2} => {K1 #Equals K2} [simplification]
+  rule {K1 ==Int K2 #Equals false} => #Not({K1 #Equals K2}) [simplification]
+  rule {false #Equals K1 ==Int K2} => #Not({K1 #Equals K2}) [simplification]
+  rule {K1 =/=Int K2 #Equals true} => #Not({K1 #Equals K2}) [simplification]
+  rule {true #Equals K1 =/=Int K2} => #Not({K1 #Equals K2}) [simplification]
+  rule {K1 =/=Int K2 #Equals false} => {K1 #Equals K2} [simplification]
+  rule {false #Equals K1 =/=Int K2} => {K1 #Equals K2} [simplification]
 
 endmodule
 
@@ -1592,11 +1625,11 @@ module STRING-KAST [kast]
 
 endmodule
 
-module STRING-KORE [kore]
+module STRING-KORE [kore, symbolic]
   imports private K-EQUAL
   imports STRING-COMMON
 
-  rule S1:String ==K S2:String => S1 ==String S2
+  rule S1:String ==K S2:String => S1 ==String S2 [simplification]
 
 endmodule
 
@@ -2060,11 +2093,19 @@ module K-EQUAL-SYNTAX
 
 endmodule
 
-module K-EQUAL-KORE [kore]
+module K-EQUAL-KORE [kore, symbolic]
   import private BOOL
   import K-EQUAL-SYNTAX
 
-  rule K1:Bool ==K K2:Bool => K1 ==Bool K2
+  rule K1:Bool ==K K2:Bool => K1 ==Bool K2 [simplification]
+  rule {K1 ==K K2 #Equals true} => {K1 #Equals K2} [simplification]
+  rule {true #Equals K1 ==K K2} => {K1 #Equals K2} [simplification]
+  rule {K1 ==K K2 #Equals false} => #Not({K1 #Equals K2}) [simplification]
+  rule {false #Equals K1 ==K K2} => #Not({K1 #Equals K2}) [simplification]
+  rule {K1 =/=K K2 #Equals true} => #Not({K1 #Equals K2}) [simplification]
+  rule {true #Equals K1 =/=K K2} => #Not({K1 #Equals K2}) [simplification]
+  rule {K1 =/=K K2 #Equals false} => {K1 #Equals K2} [simplification]
+  rule {false #Equals K1 =/=K K2} => {K1 #Equals K2} [simplification]
 
 endmodule
 

k-distribution/tests/regression-new/map-symbolic-tests-haskell/lookup-14-spec.k.out

@@ -23,8 +23,8 @@
   {
     true
   #Equals
-    Z:MyId in_keys ( MAP
-    ( X:MyId |-> 1 ) )
+    Z:MyId in_keys ( ( MAP
+    X:MyId |-> 1 ) [ Y:MyId <- 2 ] )
   }
 #And
   {

k-distribution/tests/regression-new/map-symbolic-tests-haskell/lookup-3-spec.k.out

@@ -18,7 +18,7 @@
     true
   #Equals
     Z:MyId in_keys ( MAP
-    ( Y:MyId |-> 1 ) )
+    ( Y:MyId |-> 2 ) )
   }
 #And
   {

k-distribution/tests/regression-new/unification-lemmas/Makefile

@@ -0,0 +1,5 @@
+DEF=test
+TESTDIR=.
+KOMPILE_BACKEND=haskell
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/unification-lemmas/test-spec.k

@@ -0,0 +1,12 @@
+// Copyright (c) 2022 K Team. All Rights Reserved.
+
+requires "test.k"
+
+module TEST-SPEC
+    imports TEST
+
+  claim <k> makeLookup(B) => 1 ... </k>
+    requires lookup(#hashedLocation(B .IntList)) ==Int 1
+     andBool #rangeUInt(B)
+
+endmodule

k-distribution/tests/regression-new/unification-lemmas/test-spec.k.out

@@ -0,0 +1 @@
+#Top

k-distribution/tests/regression-new/unification-lemmas/test.k

@@ -0,0 +1,44 @@
+// Copyright (c) 2020 K Team. All Rights Reserved.
+
+module TEST-SYNTAX
+endmodule
+
+module TEST
+    imports TEST-SYNTAX
+    imports BOOL
+    imports INT
+    imports MAP
+    imports STRING
+    imports MAP-SYMBOLIC
+
+    configuration <k> $PGM:KItem </k>
+
+    syntax KItem ::= makeLookup(Int)
+    rule makeLookup(B) => lookup(#hash(B))
+
+    syntax Int ::= lookup(Hash) [function, no-evaluators]
+                 | #lookupMemory  ( Map , Int ) [function, functional, smtlib(lookupMemory)]
+    syntax Int ::= "pow256" [alias] /* 2 ^Int 256 */
+    rule pow256 => 115792089237316195423570985008687907853269984665640564039457584007913129639936
+
+    syntax KItem ::= runLemma(Int) | doneLemma(Int)
+    rule runLemma(T) => doneLemma(T)
+
+    // -------------------------------------------
+    syntax IntList ::= List{Int, ""}
+
+    syntax Bool ::= #rangeUInt(Int) [function, no-evaluators]
+
+    syntax Hash ::= #hash(Int)
+                  | #hashedLocation( IntList ) [function]
+
+    rule #hashedLocation(       .IntList) => #hash(0)
+    rule #hashedLocation(OFFSET .IntList) => #hash(OFFSET)
+      requires #rangeUInt(OFFSET)
+
+     rule [#lookupMemory.some]:   #lookupMemory( (KEY |-> VAL:Int) _M, KEY ) => VAL modInt 256
+    rule [#lookupMemory.none]:   #lookupMemory(                    M, KEY ) => 0                 requires notBool KEY in_keys(M)
+    //Impossible case, for completeness
+    rule [#lookupMemory.notInt]: #lookupMemory( (KEY |-> VAL    ) _M, KEY ) => 0                 requires notBool isInt(VAL)
+
+endmodule

k-distribution/tests/regression-new/unification-lemmas/test2-spec.k

@@ -0,0 +1,10 @@
+// Copyright (c) 2022 K Team. All Rights Reserved.
+
+requires "test.k"
+
+module TEST2-SPEC
+    imports TEST
+
+    claim <k> runLemma ( #lookupMemory(( KEY |-> 33) (_KEY' |-> 728) (_KEY'' |-> (pow256 +Int 5)) (_KEY''' |-> "hello"), KEY)    ) => doneLemma ( 33  ) ... </k>
+
+endmodule

k-distribution/tests/regression-new/unification-lemmas/test2-spec.k.out

@@ -0,0 +1 @@
+#Top

k-distribution/tests/regression-new/unification-lemmas2/Makefile

@@ -0,0 +1,5 @@
+DEF=with-config
+TESTDIR=.
+KOMPILE_BACKEND=haskell
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/unification-lemmas2/owise-spec.k

@@ -0,0 +1,14 @@
+requires "with-config.k"
+
+module OWISE-SPEC
+    imports WITH-CONFIG
+
+    claim <k> a(AID) => 0 </k>
+        <accounts>
+            <account>
+                <accountID> BID </accountID>
+                <freeBalance> 30 </freeBalance>
+            </account>
+        </accounts>
+        requires AID =/=K BID
+endmodule

k-distribution/tests/regression-new/unification-lemmas2/owise-spec.k.out

@@ -0,0 +1 @@
+#Top

k-distribution/tests/regression-new/unification-lemmas2/with-config.k

@@ -0,0 +1,39 @@
+module WITH-CONFIG
+    imports INT
+    imports COLLECTIONS
+    imports K-EQUAL
+
+    configuration
+        <set-balance>
+            <k> $PGM:KItem </k>
+            <accounts>
+                <account multiplicity="*" type="Map">
+                    <accountID> .AccountId:AccountId </accountID>
+                    <freeBalance> 0 </freeBalance>
+                </account>
+            </accounts>
+        </set-balance>
+
+    syntax KItem ::= Int
+
+    syntax AccountId ::= ".AccountId" | Int
+    // ---------------------------------------
+
+    syntax Int ::= "total_balance" "(" AccountId ")" [function, functional]
+    // -----------------------------------------------------------------------
+    rule total_balance(WHO) => 0 [owise]
+    rule [[ total_balance(WHO) => FREE_BALANCE ]]
+        <account>
+            <accountID> WHO </accountID>
+            <freeBalance> FREE_BALANCE </freeBalance>
+        </account>
+
+    // for one-spec
+    syntax KItem ::= "aa" "(" AccountId ")"
+    rule aa(AID) => total_balance(AID)
+
+    // for owise-spec
+    syntax KItem ::= "a" "(" AccountId ")"
+    rule a(AID) => total_balance(AID)
+
+endmodule