Update dependency: deps/k_release (#3691)

Co-authored-by: devops <[email protected]> Co-authored-by: Jost Berthold <[email protected]>
runtimeverification · Feb 19, 2024 · 6fd37bd · 6fd37bd
1 parent d943208
commit 6fd37bd
Show file tree

Hide file tree

Showing 28 changed files with 49 additions and 2,075 deletions.
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -114,7 +114,7 @@ jobs:
             stack-2-${{ runner.os }}-ghc-${{ env.ghc_version }}-${{ hashFiles('stack.yaml') }}
             stack-2-${{ runner.os }}-ghc-${{ env.ghc_version }}
 
-      - uses: haskell/actions/setup@v2
+      - uses: haskell-actions/setup@v2
         id: setup-haskell-stack
         with:
           ghc-version: ${{ env.ghc_version }}
@@ -148,7 +148,7 @@ jobs:
             stack-haddock-2-${{ runner.os }}-ghc-${{ env.ghc_version }}-${{ hashFiles('stack.yaml') }}
             stack-haddock-2-${{ runner.os }}-ghc-${{ env.ghc_version }}
 
-      - uses: haskell/actions/setup@v2
+      - uses: haskell-actions/setup@v2
         id: setup-haskell-stack
         with:
           ghc-version: ${{ env.ghc_version }}

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -183,7 +183,7 @@ jobs:
             stack-2-${{ runner.os }}-ghc-${{ env.ghc_version }}-${{ hashFiles('stack.yaml') }}
             stack-2-${{ runner.os }}-ghc-${{ env.ghc_version }}
 
-      - uses: haskell/actions/setup@v2
+      - uses: haskell-actions/setup@v2
         id: setup-haskell-stack
         with:
           ghc-version: ${{ env.ghc_version }}

diff --git a/deps/k_release b/deps/k_release
@@ -1 +1 @@
-6.0.181
+6.2.27
diff --git a/test/issue-1665/test.k b/test/issue-1665/test.k
@@ -3,7 +3,7 @@ module TEST-SYNTAX
 
   syntax Pgm ::= "begin" Int | "end" Int
   syntax Int ::= fun(Int) [function, no-evaluators]
-  syntax Bool ::= isFun(Int) [function, functional, no-evaluators]
+  syntax Bool ::= isFun(Int) [function, total, no-evaluators]
 
 endmodule
 
@@ -14,6 +14,6 @@ module TEST
 
   rule begin X => end fun(X)
 
-  rule [ceil-fun]: #Ceil(fun(X:Int)) => #True requires isFun(X) [simplification]
+  rule [ceil-fun]: #Ceil(fun(X:Int)) => #Top requires isFun(X) [simplification]
 
 endmodule
diff --git a/test/issue-1916/test.k b/test/issue-1916/test.k
@@ -5,7 +5,7 @@ module TEST-SYNTAX
 
   syntax Pgm ::= "begin" | "end"
   syntax Int ::= fun(Int) [function, no-evaluators]
-  syntax Bool ::= isFun(Int) [function, functional, no-evaluators]
+  syntax Bool ::= isFun(Int) [function, total, no-evaluators]
 
 endmodule
 
@@ -16,6 +16,6 @@ module TEST
 
   rule begin => end
 
-  rule [ceil-fun]: #Ceil(fun(X:Int)) => #True requires isFun(X) [simplification]
+  rule [ceil-fun]: #Ceil(fun(X:Int)) => #Top requires isFun(X) [simplification]
 
 endmodule
diff --git a/test/issue-2378/test-spec.k.out.golden b/test/issue-2378/test-spec.k.out.golden
@@ -1,16 +1 @@
-  #Not ( #Exists _Gen0 . #Exists S . {
-    keys ( _M )
-  #Equals
-    S
-    SetItem ( _Gen0 )
-  } )
-#And
-  #Not ( {
-    .Set
-  #Equals
-    keys ( _M )
-  } )
-#And
-  <k>
-    b ( keys ( _M ) ) ~> _DotVar1 ~> .
-  </k>
+b ( keys ( _M ) )
diff --git a/test/map/map-iteration/test-1-spec.k b/test/map/map-iteration/test-1-spec.k
@@ -3,7 +3,6 @@ requires "test.k"
 module TEST-1-SPEC
   imports TEST
 
-  claim <k> runTest( f( a |-> 1 b |-> 2 ) ) </k> => <k> doneTest( b |-> 2 c |-> 3 ) </k>
+  claim <k> runTest( f( a |-> 1 b |-> 2 ) ) => doneTest( b |-> 2 c |-> 3 ) </k>
 
 endmodule
-
diff --git a/test/overloads/simple-lists/broken-spec.k.out.golden b/test/overloads/simple-lists/broken-spec.k.out.golden
@@ -1,3 +1 @@
-<k>
-  i1  i2  .EmptyStmts ~> _DotVar1 ~> .
-</k>
+i1  i2  .EmptyStmts
diff --git a/test/regression-evm/test-dsvalue-peek-pass-rough.sh b/test/regression-evm/test-dsvalue-peek-pass-rough.sh
@@ -13,8 +13,6 @@ exec kore-exec \
     --log-level \
     warning \
     --enable-log-timestamps \
-    --log-entries \
-    DebugTransition \
     --prove test-dsvalue-peek-pass-rough-spec.kore \
     --spec-module DSVALUE-PEEK-PASS-ROUGH-SPEC \
     --graph-search breadth-first \

diff --git a/test/regression-evm/test-flipper-addu48u48-fail-rough.sh b/test/regression-evm/test-flipper-addu48u48-fail-rough.sh
@@ -13,8 +13,6 @@ exec kore-exec \
     --log-level \
     warning \
     --enable-log-timestamps \
-    --log-entries \
-    DebugTransition \
     --prove test-flipper-addu48u48-fail-rough-spec.kore \
     --spec-module FLIPPER-ADDU48U48-FAIL-ROUGH-SPEC \
     --graph-search breadth-first \

diff --git a/test/regression-evm/test-functional.sh b/test/regression-evm/test-functional.sh
@@ -13,8 +13,6 @@ exec kore-exec \
     --log-level \
     warning \
     --enable-log-timestamps \
-    --log-entries \
-    DebugTransition \
     --prove test-functional-spec.kore \
     --spec-module FUNCTIONAL-SPEC \
     --graph-search breadth-first \

diff --git a/test/regression-evm/test-lemmas.sh b/test/regression-evm/test-lemmas.sh
@@ -13,8 +13,6 @@ exec kore-exec \
     --log-level \
     warning \
     --enable-log-timestamps \
-    --log-entries \
-    DebugTransition \
     --prove test-lemmas-spec.kore \
     --spec-module LEMMAS-SPEC \
     --graph-search breadth-first \

diff --git a/test/regression-evm/test-storagevar03.sh b/test/regression-evm/test-storagevar03.sh
@@ -13,8 +13,6 @@ exec kore-exec \
     --log-level \
     warning \
     --enable-log-timestamps \
-    --log-entries \
-    DebugTransition \
     --prove test-storagevar03-spec.kore \
     --spec-module STORAGEVAR03-SPEC \
     --graph-search breadth-first \

diff --git a/test/regression-evm/test-sum-to-n.sh b/test/regression-evm/test-sum-to-n.sh
@@ -13,8 +13,6 @@ exec kore-exec \
     --log-level \
     warning \
     --enable-log-timestamps \
-    --log-entries \
-    DebugTransition \
     --prove test-sum-to-n-spec.kore \
     --spec-module SUM-TO-N-SPEC \
     --graph-search breadth-first \

diff --git a/test/regression-evm/test-totalSupply.sh b/test/regression-evm/test-totalSupply.sh
@@ -13,8 +13,6 @@ exec kore-exec \
     --log-level \
     warning \
     --enable-log-timestamps \
-    --log-entries \
-    DebugTransition \
     --prove test-totalSupply-spec.kore \
     --spec-module TOTALSUPPLY-SPEC \
     --graph-search breadth-first \

diff --git a/test/remove-destination/test-1-spec.k.out.golden b/test/remove-destination/test-1-spec.k.out.golden
@@ -34,10 +34,8 @@
       4
     } )
 #And
-  <k>
-    a ( K:Int |-> V:Int
-    M ) ~> _DotVar1 ~> .
-  </k>
+  a ( K:Int |-> V:Int
+  M )
 #And
   {
     false

diff --git a/test/save-proofs/test-1-spec.k b/test/save-proofs/test-1-spec.k
@@ -4,5 +4,5 @@ requires "save-proofs.k"
 module TEST-1-SPEC
   imports SAVE-PROOFS
 
-  claim BB(X:Int) => CC(X:Int)
+  claim <k> BB(X:Int) => CC(X:Int) </k>
 endmodule
diff --git a/test/save-proofs/test-1-spec.k.save-proofs.kore.golden b/test/save-proofs/test-1-spec.k.save-proofs.kore.golden
@@ -17,33 +17,37 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d
                         LblBB'LParUndsRParUnds'SAVE-PROOFS'Unds'KItem'Unds'Int{}(
                             /* T Fn D Sfa */ VarX:SortInt{}
                         ),
-                        /* T Fn D Sfa */ Var'Unds'DotVar1:SortK{}
+                        /* T Fn D Sfa Cl */ dotk{}()
                     )
                 ),
                 /* T Fn D Spa */
                 Lbl'-LT-'generatedCounter'-GT-'{}(
-                    /* T Fn D Sfa */ Var'Unds'DotVar2:SortInt{}
+                    /* T Fn D Sfa */ Var'Unds'Gen0:SortInt{}
                 )
             )
         ),
         /* Spa */
         weakAlwaysFinally{SortGeneratedTopCell{}}(
-            /* T Fn D Spa */
-            Lbl'-LT-'generatedTop'-GT-'{}(
+            /* Spa */
+            \exists{SortGeneratedTopCell{}}(
+                Var'QuesUnds'Gen1:SortInt{},
                 /* T Fn D Spa */
-                Lbl'-LT-'k'-GT-'{}(
+                Lbl'-LT-'generatedTop'-GT-'{}(
                     /* T Fn D Spa */
-                    kseq{}(
+                    Lbl'-LT-'k'-GT-'{}(
                         /* T Fn D Spa */
-                        LblCC'LParUndsRParUnds'SAVE-PROOFS'Unds'KItem'Unds'Int{}(
-                            /* T Fn D Sfa */ VarX:SortInt{}
-                        ),
-                        /* T Fn D Sfa */ Var'Unds'DotVar1:SortK{}
+                        kseq{}(
+                            /* T Fn D Spa */
+                            LblCC'LParUndsRParUnds'SAVE-PROOFS'Unds'KItem'Unds'Int{}(
+                                /* T Fn D Sfa */ VarX:SortInt{}
+                            ),
+                            /* T Fn D Sfa Cl */ dotk{}()
+                        )
+                    ),
+                    /* T Fn D Spa */
+                    Lbl'-LT-'generatedCounter'-GT-'{}(
+                        /* T Fn D Sfa */ Var'QuesUnds'Gen1:SortInt{}
                     )
-                ),
-                /* T Fn D Spa */
-                Lbl'-LT-'generatedCounter'-GT-'{}(
-                    /* T Fn D Sfa */ Var'Unds'DotVar2:SortInt{}
                 )
             )
         )

diff --git a/test/save-proofs/test-2-spec.k b/test/save-proofs/test-2-spec.k
@@ -7,7 +7,7 @@ module TEST-2-SPEC
   imports SAVE-PROOFS
 
   // This claim would fail, but it is loaded from the saved claims.
-  claim BB(X:Int) => CC(X:Int)
+  claim <k> BB(X:Int) => CC(X:Int) </k>
   // This claim requires the first claim.
-  claim AA(X:Int) => DD(X:Int)
+  claim <k> AA(X:Int) => DD(X:Int) </k>
 endmodule
diff --git a/test/set/set-iteration/test-1-spec.k b/test/set/set-iteration/test-1-spec.k
@@ -3,7 +3,7 @@ requires "test.k"
 module TEST-1-SPEC
   imports TEST
 
-  claim <k> runTest( f( SetItem(a) SetItem(b) ) ) </k>
-    => <k> doneTest( SetItem(b) SetItem(c) ) </k>
+  claim <k> runTest( f( SetItem(a) SetItem(b) ) )
+    => doneTest( SetItem(b) SetItem(c) ) </k>
 
 endmodule
diff --git a/test/set/set-iteration/test-2-spec.k b/test/set/set-iteration/test-2-spec.k
@@ -3,8 +3,8 @@ requires "test.k"
 module TEST-2-SPEC
   imports TEST
 
-  claim <k> runTest( f( SetItem(X:Element) SetItem(Y:Element) ) ) </k>
-    => <k> doneTest( SetItem(g(X)) SetItem(g(Y)) ) </k>
+  claim <k> runTest( f( SetItem(X:Element) SetItem(Y:Element) ) )
+    => doneTest( SetItem(g(X)) SetItem(g(Y)) ) </k>
     requires
       (X =/=K Y)
       andBool (g(X) =/=K g(Y))

diff --git a/test/set/set-iteration/test.k b/test/set/set-iteration/test.k
@@ -7,13 +7,13 @@ module TEST
 
   syntax Element ::= "a" | "b" | "c"
 
-  syntax Element ::= g(Element) [function, functional]
+  syntax Element ::= g(Element) [function, total]
 
   rule g(a) => b
   rule g(b) => c
   rule g(c) => a
 
-  syntax Set ::= f(Set) [function, functional]
+  syntax Set ::= f(Set) [function, total]
 
   rule f(.Set) => .Set
   rule f(SetItem(E:Element) S:Set) => SetItem(g(E)) f(S)

diff --git a/test/simplification/Makefile b/test/simplification/Makefile
@@ -1,10 +1,12 @@
 DEF = simplification
 include $(CURDIR)/../include.mk
 
+.PHONY: a-spec.k.out
+
 a-spec.k.out: KORE_EXEC_OPTS = --debug-attempt-equation=SIMPLIFICATION.f.positive
 
 a-spec.k.out: a-spec.k simplification.k $(TEST_DEPS)
 	@echo ">>>" $(CURDIR) "kprove" $<
 	rm -f $@
 	$(KPROVE) $(KPROVE_OPTS) $(KPROVE_SPEC) 1> /dev/null 2> $@ || true
-	grep -q "equation is not applicable" $@ || mv $@ $@.fail
+	grep -q "equation is not applicable" $@ && rm $@ || mv $@ $@.fail
-Original file line number
+Diff line change
@@ Expand Up / @@ -34,10 +34,8 @@ @@
         } )
     #And
-      <k>
-        a ( K:Int |-> V:Int
-        M ) ~> _DotVar1 ~> .
-      </k>
+      a ( K:Int |-> V:Int
+      M )
     #And
       {
         false
@@ Expand Down @@