From 9e7c54e4c5ccef79041e4b5aa6c6b6ef1d5c79a0 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Mon, 21 Apr 2025 17:27:04 +0300 Subject: [PATCH 1/8] apply substitutions only to `` cell in fuzzer --- src/komet/kasmer.py | 3 ++- src/komet/utils.py | 31 +++++++++++++++++++++++++++++++ 2 files changed, 33 insertions(+), 1 deletion(-) diff --git a/src/komet/kasmer.py b/src/komet/kasmer.py index 3b86ada0..4d448b8b 100644 --- a/src/komet/kasmer.py +++ b/src/komet/kasmer.py @@ -42,7 +42,7 @@ ) from .proof import is_functional, run_claim, run_functional_claim from .scval import SCType -from .utils import KSorobanError, concrete_definition +from .utils import KSorobanError, concrete_definition, subst_on_program_cell if TYPE_CHECKING: from collections.abc import Iterable, Mapping @@ -248,6 +248,7 @@ def scval_to_kore(val: SCValue) -> Pattern: check_exit_code=True, max_examples=max_examples, handler=KometFuzzHandler(self.definition, task), + subst_func=subst_on_program_cell, ) def run_prove( diff --git a/src/komet/utils.py b/src/komet/utils.py index 15e0e561..dced9cbd 100644 --- a/src/komet/utils.py +++ b/src/komet/utils.py @@ -8,18 +8,23 @@ from pyk.kast.outer import KRule, read_kast_definition from pyk.kdist import kdist from pyk.konvert import kast_to_kore +from pyk.kore.manip import substitute_vars +from pyk.kore.prelude import generated_top +from pyk.kore.syntax import App from pyk.ktool.kompile import DefinitionInfo from pyk.ktool.kprove import KProve from pyk.ktool.krun import KRun from pyk.utils import single if TYPE_CHECKING: + from collections.abc import Mapping from pathlib import Path from subprocess import CompletedProcess from typing import Any, Final from pyk.kast.inner import KInner, KSort from pyk.kast.outer import KDefinition, KFlatModule + from pyk.kore.syntax import EVar, Pattern from pyk.ktool.kompile import KompileBackend _LOGGER: Final = logging.getLogger(__name__) @@ -92,3 +97,29 @@ def parse_lemmas_module(self, module_path: Path, module_name: str) -> KFlatModul concrete_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm')) library_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm-library')) symbolic_definition = SorobanDefinition(kdist.get('soroban-semantics.haskell')) + + +def subst_on_program_cell(template: Pattern, subst_case: Mapping[EVar, Pattern]) -> Pattern: + """A substitution function that only applies substitutions within the K cell. + Optimizing the fuzzer by restricting changes to relevant parts of the configuration. + + Args: + template: The template configuration containing variables in the K cell. + subst_case: A mapping from variables to their replacement patterns. + """ + + def kasmer_cell(program_cell: Pattern, soroban_cell: Pattern, exit_code_cell: Pattern) -> Pattern: + return App("Lbl'-LT-'kasmer'-GT-'", args=(program_cell, soroban_cell, exit_code_cell)) + + match template: + case App( + "Lbl'-LT-'generatedTop'-GT-'", + args=( + App("Lbl'-LT-'kasmer'-GT-'", args=(program_cell, soroban_cell, exit_code_cell)), + generated_counter_cell, + ), + ): + program_cell_ = substitute_vars(program_cell, subst_case) + return generated_top((kasmer_cell(program_cell_, soroban_cell, exit_code_cell), generated_counter_cell)) + + raise ValueError(template) From 802af390a4c3c3f8e10954141d11e9f1baf982e2 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 21 Apr 2025 14:57:09 +0000 Subject: [PATCH 2/8] Set Version: 0.1.65 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 9810a3b1..c472eaf6 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.64 +0.1.65 diff --git a/pyproject.toml b/pyproject.toml index 29820e6c..e1ea958d 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.64" +version = "0.1.65" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", From 9a3c7241483341ba5a1d52b87b6c3a4a0c9683be Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Mon, 5 May 2025 12:00:59 +0300 Subject: [PATCH 3/8] setup python before code quality checks --- .github/workflows/test.yml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 4b59b973..901255fb 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -39,6 +39,12 @@ jobs: steps: - name: 'Check out code' uses: actions/checkout@v3 + - name: 'Setup Python 3.10' + uses: actions/setup-python@v5 + with: + python-version: '3.10' + - name: 'Install Poetry' + uses: Gr1N/setup-poetry@v9 - name: 'Run code quality checks' run: make check - name: 'Run pyupgrade' From e4cec10bab9456dddcbe3f93a9d3d89286697f63 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 1 Sep 2025 09:39:47 +0000 Subject: [PATCH 4/8] Set Version: 0.1.72 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 7c3ae4e0..8076b7dc 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.71 +0.1.72 diff --git a/pyproject.toml b/pyproject.toml index e2ff9247..a16b48d9 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.71" +version = "0.1.72" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", From febf800224ecb6864211a0fbdf76d61c13ac542e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Burak=20Bilge=20Yal=C3=A7=C4=B1nkaya?= Date: Mon, 1 Sep 2025 12:47:36 +0300 Subject: [PATCH 5/8] Update Dockerfile --- .github/actions/with-docker/Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/actions/with-docker/Dockerfile b/.github/actions/with-docker/Dockerfile index f66e34f9..6e9e9f33 100644 --- a/.github/actions/with-docker/Dockerfile +++ b/.github/actions/with-docker/Dockerfile @@ -32,4 +32,4 @@ RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | bash -s -- -y && rustup target add wasm32-unknown-unknown \ && rustup target add wasm32v1-none -RUN cargo install --locked stellar-cli --features opt +RUN cargo install --locked stellar-cli@23.0.1 From e79e113ea5a9932a6d79584f9e87afc45b45d4ab Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 24 Oct 2025 08:48:30 +0000 Subject: [PATCH 6/8] Set Version: 0.1.73 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 8076b7dc..416eb55e 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.72 +0.1.73 diff --git a/pyproject.toml b/pyproject.toml index a16b48d9..d11ad4f9 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.72" +version = "0.1.73" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", From a3b6f938dd6bce32059ddd91449ecd9e6cca2f96 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 31 Oct 2025 14:22:22 +0300 Subject: [PATCH 7/8] override numpy on Darwin to fix dynamic library issue on Mac+nix --- flake.nix | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/flake.nix b/flake.nix index 65e203eb..d1d063c8 100644 --- a/flake.nix +++ b/flake.nix @@ -69,6 +69,15 @@ (finalPython: prevPython: { kframework = k-framework.packages.${system}.pyk-python310; pykwasm = wasm-semantics.packages.${system}.kwasm-pyk; + # override numpy on Darwin to avoid the missing dynamic library issue + numpy = if pkgs.stdenv.isDarwin + then + prevPython.numpy.override { + blas = null; + lapack = null; + } + else + prevPython.numpy; }); groups = [ ]; checkGroups = [ ]; From f62489e050e47490d8cc4b82409a4b99ebb6ff06 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 31 Oct 2025 14:50:43 +0300 Subject: [PATCH 8/8] tmp --- flake.nix | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/flake.nix b/flake.nix index d1d063c8..0e6df6aa 100644 --- a/flake.nix +++ b/flake.nix @@ -70,12 +70,13 @@ kframework = k-framework.packages.${system}.pyk-python310; pykwasm = wasm-semantics.packages.${system}.kwasm-pyk; # override numpy on Darwin to avoid the missing dynamic library issue - numpy = if pkgs.stdenv.isDarwin - then - prevPython.numpy.override { - blas = null; - lapack = null; - } + numpy = if pkgs.stdenv.isDarwin + then + prevPython.numpy.overrideAttrs (old: { + buildInputs = (old.buildInputs or []) ++ [ pkgs.Accelerate ]; + NPY_BLAS_ORDER = "accelerate"; + NPY_LAPACK_ORDER = "accelerate"; + }) else prevPython.numpy; });