Merge remote-tracking branch 'origin/develop' into _update-deps/runti…

…meverification/llvm-backend

.github/actions/setup-pyk-env/action.yml

@@ -15,6 +15,8 @@ runs:
         python-version: ${{ inputs.python-version }}
     - name: 'Install Poetry'
       uses: Gr1N/setup-poetry@v9
+      with:
+        poetry-version: '1.8.5'
     - name: 'Install package'
       shell: bash
       run: poetry -C pyk install

.github/actions/with-k-docker/Dockerfile

@@ -38,5 +38,5 @@ USER user
 WORKDIR /home/user
 
 ENV PATH=/home/user/.local/bin:${PATH}
-RUN    curl -sSL https://install.python-poetry.org | python3 - \
+RUN    curl -sSL https://install.python-poetry.org | python3 - --version 1.8.5 \
     && poetry --version

.github/workflows/master-push.yml

@@ -7,7 +7,7 @@ on:
 jobs:
   gh-release:
     name: 'Publish GitHub Prerelease'
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v4

.github/workflows/release.yml

@@ -21,7 +21,7 @@ jobs:
 
   source-tarball:
     name: 'Create source tarball'
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     environment: production
     steps:
       - name: 'Check out code'
@@ -475,7 +475,7 @@ jobs:
 
   pyk-publish:
     name: 'Publish pyk'
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     environment: production
     permissions:
       id-token: write
@@ -491,6 +491,8 @@ jobs:
 
       - name: Install Poetry
         uses: Gr1N/setup-poetry@v9
+        with:
+          poetry-version: '1.8.5'
 
       - name: Build pyk
         working-directory: pyk
@@ -512,10 +514,10 @@ jobs:
             fi
             sleep 10
           done
-  
+
   notify-dependents:
     name: 'Notify Dependents'
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     needs: pyk-publish
     steps:
       - name: Check out code

.github/workflows/run-actionlint.yml

@@ -4,7 +4,7 @@ on: pull_request
 jobs:
   actionlint:
     name: Run actionlint
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - uses: actions/checkout@v4
       - name: Download actionlint

.github/workflows/test-pr.yml

@@ -11,7 +11,7 @@ concurrency:
 jobs:
   format-check:
     name: 'Java: Linting'
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v4
@@ -30,7 +30,7 @@ jobs:
 
   pyk-code-quality-checks:
     name: 'Pyk: Code Quality & Unit Tests'
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     timeout-minutes: 5
     strategy:
       fail-fast: false
@@ -56,7 +56,7 @@ jobs:
 
   code-quality:
     name: 'Code Quality Checks'
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     needs:
       - format-check
       - pyk-code-quality-checks
@@ -156,7 +156,7 @@ jobs:
     name: 'Pyk: Nix Build'
     strategy:
       matrix:
-        os: [ubuntu-latest, macos-14]
+        os: [ubuntu-24.04, macos-14]
     runs-on: ${{ matrix.os }}
     steps:
       - name: 'Check out code'
@@ -311,7 +311,7 @@ jobs:
   pyk-regression-tests:
     needs: test-frontend-package-ubuntu-jammy
     name: 'Pyk: Regression Tests'
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     timeout-minutes: 30
     steps:
       - name: 'Check out code'

deps/z3

@@ -1 +1 @@
-4.13.0
+4.13.4

package/docker/Dockerfile.ubuntu-noble

@@ -1,4 +1,4 @@
-FROM runtimeverificationinc/z3:ubuntu-noble-4.13.0
+FROM runtimeverificationinc/z3:ubuntu-noble-4.13.4
 
 ENV TZ=America/Chicago
 RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone

pyk/src/pyk/k2lean4/Prelude.lean

@@ -0,0 +1,10 @@
+abbrev SortBool : Type := Int
+abbrev SortBytes: Type := ByteArray
+abbrev SortId : Type := String
+abbrev SortInt : Type := Int
+abbrev SortString : Type := String
+abbrev SortStringBuffer : Type := String
+
+abbrev ListHook (E : Type) : Type := List E
+abbrev MapHook (K : Type) (V : Type) : Type := List (K × V)
+abbrev SetHook (E : Type) : Type := List E

pyk/src/pyk/k2lean4/__init__.py

@@ -0,0 +1 @@
+from .k2lean4 import K2Lean4

pyk/src/pyk/k2lean4/k2lean4.py

@@ -0,0 +1,86 @@
+from __future__ import annotations
+
+import re
+from dataclasses import dataclass
+from typing import TYPE_CHECKING
+
+from ..konvert import unmunge
+from ..kore.internal import CollectionKind
+from ..kore.syntax import SortApp
+from ..utils import check_type
+from .model import Abbrev, Ctor, ExplBinder, Inductive, Module, Signature, Term
+
+if TYPE_CHECKING:
+    from typing import Final
+
+    from ..kore.internal import KoreDefn
+    from .model import Command
+
+
+_VALID_LEAN_IDENT: Final = re.compile(
+    "_[a-zA-Z0-9_?!']+|[a-zA-Z][a-zA-Z0-9_?!']*"
+)  # Simplified to characters permitted in KORE in the first place
+
+
+@dataclass(frozen=True)
+class K2Lean4:
+    defn: KoreDefn
+
+    def sort_module(self) -> Module:
+        commands = []
+        commands += self._inductives()
+        commands += self._collections()
+        return Module(commands=commands)
+
+    def _inductives(self) -> list[Command]:
+        def is_inductive(sort: str) -> bool:
+            decl = self.defn.sorts[sort]
+            return not decl.hooked and 'hasDomainValues' not in decl.attrs_by_key
+
+        sorts = sorted(sort for sort in self.defn.sorts if is_inductive(sort))
+        return [self._inductive(sort) for sort in sorts]
+
+    def _inductive(self, sort: str) -> Inductive:
+        subsorts = sorted(self.defn.subsorts.get(sort, ()))
+        symbols = sorted(self.defn.constructors.get(sort, ()))
+        ctors: list[Ctor] = []
+        ctors.extend(self._inj_ctor(sort, subsort) for subsort in subsorts)
+        ctors.extend(self._symbol_ctor(sort, symbol) for symbol in symbols)
+        return Inductive(sort, Signature((), Term('Type')), ctors=ctors)
+
+    def _inj_ctor(self, sort: str, subsort: str) -> Ctor:
+        return Ctor(f'inj_{subsort}', Signature((ExplBinder(('x',), Term(subsort)),), Term(sort)))
+
+    def _symbol_ctor(self, sort: str, symbol: str) -> Ctor:
+        param_sorts = (
+            check_type(sort, SortApp).name for sort in self.defn.symbols[symbol].param_sorts
+        )  # TODO eliminate check_type
+        symbol = self._symbol_ident(symbol)
+        binders = tuple(ExplBinder((f'x{i}',), Term(sort)) for i, sort in enumerate(param_sorts))
+        return Ctor(symbol, Signature(binders, Term(sort)))
+
+    @staticmethod
+    def _symbol_ident(symbol: str) -> str:
+        if symbol.startswith('Lbl'):
+            symbol = symbol[3:]
+        symbol = unmunge(symbol)
+        if not _VALID_LEAN_IDENT.fullmatch(symbol):
+            symbol = f'«{symbol}»'
+        return symbol
+
+    def _collections(self) -> list[Command]:
+        return [self._collection(sort) for sort in sorted(self.defn.collections)]
+
+    def _collection(self, sort: str) -> Abbrev:
+        coll = self.defn.collections[sort]
+        elem = self.defn.symbols[coll.element]
+        sorts = ' '.join(check_type(sort, SortApp).name for sort in elem.param_sorts)  # TODO eliminate check_type
+        assert sorts
+        match coll.kind:
+            case CollectionKind.LIST:
+                val = Term(f'ListHook {sorts}')
+            case CollectionKind.MAP:
+                val = Term(f'MapHook {sorts}')
+            case CollectionKind.SET:
+                val = Term(f'SetHook {sorts}')
+        return Abbrev(sort, val, Signature((), Term('Type')))