runtimeverification · rv-jenkins · Oct 12, 2023 · Sep 29, 2023 · Sep 29, 2023 · Sep 29, 2023
@@ -47,6 +47,7 @@ RUN    apt-get update              \
         libncurses5-dev            \
         libnss3-dev                \
         libreadline-dev            \
+        libsecp256k1-dev           \
         libsqlite3-dev             \
         libssl-dev                 \
         libyaml-dev                \

@@ -9,7 +9,9 @@ RUN    apt-get update        \
     && apt-get upgrade --yes \
     && apt-get install --yes \
             curl             \
-            libtinfo-dev
+            libsecp256k1-dev \
+            libtinfo-dev     \
+            pkg-config
 
 RUN curl -sSL https://get.haskellstack.org/ | sh
 
@@ -31,4 +33,4 @@ RUN cd /home/$USER/.tmp-haskell && stack build --only-snapshot
 ENV LC_ALL=C.UTF-8
 ADD --chown=$USER:$GROUP hs-backend-booster/src/main/native/hs-backend-booster/stack.yaml                    /home/$USER/.tmp-booster/
 ADD --chown=$USER:$GROUP hs-backend-booster/src/main/native/hs-backend-booster/package.yaml                  /home/$USER/.tmp-booster/
-RUN cd /home/$USER/.tmp-booster && stack build --only-snapshot
+RUN cd /home/$USER/.tmp-booster && stack build --only-snapshot
diff --git a/deps/hs-backend-booster_release b/deps/hs-backend-booster_release
@@ -1 +1 @@
-6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566
+5a283f7c85c5b4f66ff477b494c5d138c54706e6
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -2,9 +2,9 @@
   description = "K Framework";
   inputs = {
     nixpkgs.url = "nixpkgs/nixos-23.05";
-    haskell-backend.url = "github:runtimeverification/haskell-backend/63397c713d21322434d572281c1407d929a1189e";
+    haskell-backend.url = "github:runtimeverification/haskell-backend/cdc83446c302961cd6abd2bca8c3e73dde8f6eab";
     booster-backend = {
-      url = "github:runtimeverification/hs-backend-booster/6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566";
+      url = "github:runtimeverification/hs-backend-booster/5a283f7c85c5b4f66ff477b494c5d138c54706e6";
       # NB booster-backend will bring in another dependency on haskell-backend,
       # but the two are not necessarily the same (different more often than not).
       # We get two transitive dependencies on haskell-nix.

diff --git a/haskell-backend/src/main/native/haskell-backend b/haskell-backend/src/main/native/haskell-backend
diff --git a/hs-backend-booster/src/main/native/hs-backend-booster b/hs-backend-booster/src/main/native/hs-backend-booster
diff --git a/package/arch/Dockerfile b/package/arch/Dockerfile
@@ -27,6 +27,7 @@ RUN    pacman -Sy   --noconfirm archlinux-keyring \
                        hub                        \
                        jdk-openjdk                \
                        jemalloc                   \
+                       libsecp256k1               \
                        libyaml                    \
                        lld                        \
                        llvm                       \

diff --git a/package/arch/Dockerfile.stack-deps b/package/arch/Dockerfile.stack-deps
@@ -6,7 +6,9 @@ RUN    pacman -Sy   --noconfirm archlinux-keyring \
     && pacman -Syyu --noconfirm                   \
     && pacman -S    --noconfirm                   \
                         clang                     \
+                        libsecp256k1              \
                         make                      \
+                        pkgconf                   \
                         stack
 
 # The image is built specifically for an environment with this user/group

diff --git a/package/arch/PKGBUILD b/package/arch/PKGBUILD
@@ -8,7 +8,7 @@ arch=('x86_64')
 url="https://github.com/runtimeverification/k"
 license=('custom')
 groups=()
-depends=( 'bison' 'clang' 'diffutils' 'flex' 'fmt' 'gawk' 'gcc' 'gettext' 'gmp' 'grep' 'java-runtime' 'jemalloc' 'libyaml' 'lld' 'llvm' 'make' 'mpfr' 'patch' 'python' 'tar' 'z3' )
+depends=( 'bison' 'clang' 'diffutils' 'flex' 'fmt' 'gawk' 'gcc' 'gettext' 'gmp' 'grep' 'java-runtime' 'jemalloc' 'libsecp256k1' 'libyaml' 'lld' 'llvm' 'make' 'mpfr' 'patch' 'python' 'tar' 'z3' )
 makedepends=( 'boost' 'cmake' 'jdk-openjdk' 'maven' 'python' 'zlib' )
 checkdepends=()
 optdepends=()

diff --git a/package/debian/Dockerfile b/package/debian/Dockerfile
@@ -30,6 +30,7 @@ RUN    apt-get update            \
         libncurses5-dev          \
         libnss3-dev              \
         libreadline-dev          \
+        libsecp256k1-dev         \
         libsqlite3-dev           \
         libssl-dev               \
         libyaml-dev              \

diff --git a/package/debian/compat.focal b/package/debian/compat.focal
diff --git a/package/debian/control.bookworm b/package/debian/control.bookworm
@@ -2,15 +2,15 @@ Source: kframework
 Section: devel
 Priority: optional
 Maintainer: Dwight Guth <[email protected]>
-Build-Depends: clang-14 , cmake , debhelper (>=9) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libyaml-dev , maven , openjdk-17-jdk , zlib1g-dev
+Build-Depends: clang-14 , cmake , debhelper (>=9) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , zlib1g-dev
 Standards-Version: 3.9.6
 Homepage: https://github.com/runtimeverification/k
 
 Package: kframework
 Architecture: any
 Section: devel
 Priority: optional
-Depends: bison , clang-14 , default-jre-headless , flex , gcc , g++ , libboost-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libyaml-0-2 , libz3-4 , lld-14 , pkg-config , llvm-14
+Depends: bison , clang-14 , default-jre-headless , flex , gcc , g++ , libboost-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-1 , libyaml-0-2 , libz3-4 , lld-14 , pkg-config , llvm-14
 Recommends: z3
 Description: K framework toolchain
  Includes K Framework compiler for K language definitions, and K interpreter

diff --git a/package/debian/control.focal b/package/debian/control.focal
diff --git a/package/debian/control.jammy b/package/debian/control.jammy
@@ -2,15 +2,15 @@ Source: kframework
 Section: devel
 Priority: optional
 Maintainer: Dwight Guth <[email protected]>
-Build-Depends: clang-14 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , zlib1g-dev
+Build-Depends: clang-14 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , zlib1g-dev
 Standards-Version: 3.9.6
 Homepage: https://github.com/runtimeverification/k
 
 Package: kframework
 Architecture: any
 Section: devel
 Priority: optional
-Depends: bison , clang-14 , default-jre-headless , flex , gcc , g++ , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libtinfo-dev , libyaml-0-2 , libz3-4 , lld-14 , llvm-14 , pkg-config
+Depends: bison , clang-14 , default-jre-headless , flex , gcc , g++ , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-0 , libtinfo-dev , libyaml-0-2 , libz3-4 , lld-14 , llvm-14 , pkg-config
 Recommends: z3
 Description: K framework toolchain
  Includes K Framework compiler for K language definitions, and K interpreter

diff --git a/package/debian/rules.focal b/package/debian/rules.focal
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566
		5a283f7c85c5b4f66ff477b494c5d138c54706e6
+3 −3		.github/workflows/release.yml
+3 −3		.github/workflows/test.yml
+1 −0		cabal.project.freeze
+1 −1		deps/k_release
+9 −0		docs/hooks.md
+5 −6		flake.nix
+2 −1		kore-rpc-types/kore-rpc-types.cabal
+7 −1		kore-rpc-types/src/Kore/JsonRpc/Types.hs
+26 −5		kore-rpc-types/src/Kore/Syntax/Json/Types.hs
+2 −1		kore/app/rpc/Main.hs
+3 −0		kore/kore.cabal
+2 −2		kore/src/Kore/Attribute/Pattern/ConstructorLike.hs
+2 −2		kore/src/Kore/Attribute/Pattern/Defined.hs
+2 −2		kore/src/Kore/Attribute/Pattern/Function.hs
+4 −4		kore/src/Kore/Attribute/Pattern/Simplified.hs
+2 −2		kore/src/Kore/Attribute/Pattern/Total.hs
+40 −0		kore/src/Kore/Builtin/Krypto.hs
+6 −6		kore/src/Kore/Internal/From.hs
+10 −10		kore/src/Kore/Internal/Predicate.hs
+8 −8		kore/src/Kore/Internal/TermLike.hs
+8 −6		kore/src/Kore/Internal/TermLike/TermLike.hs
+1 −1		kore/src/Kore/JsonRpc.hs
+16 −6		kore/src/Kore/Parser/Parser.y
+2 −2		kore/src/Kore/Rewrite/SMT/Translate.hs
+2 −2		kore/src/Kore/Simplify/And.hs
+3 −3		kore/src/Kore/Simplify/Or.hs
+8 −8		kore/src/Kore/Simplify/Predicate.hs
+2 −2		kore/src/Kore/Simplify/SubstitutionSimplifier.hs
+5 −0		kore/src/Kore/Syntax.hs
+17 −11		kore/src/Kore/Syntax/And.hs
+61 −0		kore/src/Kore/Syntax/BinaryAnd.hs
+86 −0		kore/src/Kore/Syntax/BinaryOr.hs
+13 −11		kore/src/Kore/Syntax/Json/Internal.hs
+25 −20		kore/src/Kore/Syntax/Or.hs
+36 −4		kore/src/Kore/Validate/PatternVerifier.hs
+21 −0		kore/src/Options/SMT.hs
+4 −1		kore/src/SMT.hs
+10 −2		kore/src/SMT/SimpleSMT.hs
+16 −2		kore/test/Test/Kore.hs
+2 −2		kore/test/Test/Kore/Attribute/Pattern/Defined.hs
+6 −6		kore/test/Test/Kore/Attribute/Pattern/FreeVariables.hs
+2 −2		kore/test/Test/Kore/Attribute/Pattern/Function.hs
+6 −6		kore/test/Test/Kore/Attribute/Pattern/Sort.hs
+2 −2		kore/test/Test/Kore/Attribute/Pattern/Total.hs
+4 −2		kore/test/Test/Kore/Builtin/External.hs
+4 −4		kore/test/Test/Kore/Internal/From.hs
+45 −60		kore/test/Test/Kore/Parser/Parser.hs
+4 −4		kore/test/Test/Kore/Simplify/And.hs
+3 −3		kore/test/Test/Kore/Simplify/Or.hs
+2 −2		kore/test/Test/Kore/Syntax/Json.hs
+4 −8		kore/test/Test/Kore/Validate/DefinitionVerifier/PatternVerifier.hs
+3 −0		test/ecdsa/Makefile
+1 −0		test/ecdsa/addr1.ecdsa
+3 −0		test/ecdsa/addr1.ecdsa.out.golden
+1 −0		test/ecdsa/addr2.ecdsa
+3 −0		test/ecdsa/addr2.ecdsa.out.golden
+1 −0		test/ecdsa/addr3.ecdsa
+3 −0		test/ecdsa/addr3.ecdsa.out.golden
+85 −0		test/ecdsa/ecdsa.k
+15 −15		test/imp/max-symbolic.imp.out.golden
+4 −4		test/issue-2010/1.test.out.golden
+7 −0		test/parser/json/README.md
+507 −467		test/parser/json/bool.json
+385 −369		test/parser/json/list.json
+259 −243		test/parser/json/nat.json
+44 −42		test/parser/json/test-issue-94-2.json
+17 −15		test/parser/json/test-pattern-3.json
+17 −15		test/parser/json/test-pattern-4.json
+1 −1		test/rpc-server/add-module/add/response.golden
+1 −1		test/rpc-server/implies/not-implied-stuck/response.golden
+20 −2		test/rpc-server/runTests.py
+10 −10		test/smt-none/program.test.out.golden
+3 −1		.github/workflows/Dockerfile
+24 −5		.github/workflows/test.yml
+7 −0		.github/workflows/update-deps.yml
+2 −2		cabal.project
+6 −0		cabal.project.freeze
+1 −1		deps/blockchain-k-plugin_release
+1 −1		deps/haskell-backend_release
+1 −1		deps/k_release
+4 −4		flake.lock
+2 −1		flake.nix
+3 −3		library/Booster/JsonRpc.hs
+26 −25		library/Booster/JsonRpc/Utils.hs
+6 −1		library/Booster/Pattern/Base.hs
+140 −54		library/Booster/Pattern/Rewrite.hs
+19 −0		library/Booster/Pattern/Util.hs
+7 −5		library/Booster/Syntax/Json/Externalise.hs
+18 −27		library/Booster/Syntax/Json/Internalise.hs
+9 −9		library/Booster/Syntax/ParsedKore/Internalise.hs
+16 −6		library/Booster/Syntax/ParsedKore/Parser.y
+2 −0		package.yaml
+1 −1		stack.yaml
+8 −8		stack.yaml.lock
+393 −400		test/jsonrpc-examples/expected/[email protected]
+390 −397		test/jsonrpc-examples/expected/[email protected]
+519 −479		test/parser/bool.kore.json
+390 −374		test/parser/list.kore.json
+261 −245		test/parser/nat.kore.json
+44 −42		test/parser/test-issue-94-2.kore.json
+17 −15		test/parser/test-pattern-3.kore.json
+17 −15		test/parser/test-pattern-4.kore.json
+1 −1		test/rpc-integration/test-diamond/response-infeasible-branching.booster-dev
+1 −1		test/rpc-integration/test-foundry-bug-report/response-004.json
+1 −1		test/rpc-integration/test-foundry-bug-report/response-005.json
+393 −453		test/rpc-integration/test-foundry-bug-report/response-007.json
+393 −453		test/rpc-integration/test-foundry-bug-report/response-009.json
+393 −453		test/rpc-integration/test-foundry-bug-report/response-011.json
+393 −453		test/rpc-integration/test-foundry-bug-report/response-013.json
+193 −223		test/rpc-integration/test-foundry-bug-report/response-015.json
+3 −2		test/rpc-integration/test-logTiming/test.sh
+1 −1		test/rpc-integration/test-module-addition/response-03-add-new-module.json
+5 −2		tools/booster/Server.hs
+1 −1		tools/rpc-client/RpcClient.hs
+2 −2		unit-tests/Test/Booster/Syntax/Json.hs