From cd70715d10316a888b7c0795304ff00e1c23a2e8 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Thu, 13 Mar 2025 18:23:27 +0300 Subject: [PATCH 1/8] implement `constructFuzzState` step --- src/komet/kdist/soroban-semantics/kasmer.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/komet/kdist/soroban-semantics/kasmer.md b/src/komet/kdist/soroban-semantics/kasmer.md index a538b197..8f57345d 100644 --- a/src/komet/kdist/soroban-semantics/kasmer.md +++ b/src/komet/kdist/soroban-semantics/kasmer.md @@ -154,5 +154,15 @@ module KASMER #resetHost => .K ... (_:HostCell => .HostStack ... ) + + syntax SorobanCell + + syntax Step ::= constructFuzzState(Steps, SorobanCell) [symbol(constructFuzzState)] + // ------------------------------------------------------------------------------ + rule [constructFuzzState]: + constructFuzzState(STEPS, SOROBAN_CELL) .Steps => STEPS + (_:SorobanCell => SOROBAN_CELL) + [priority(10)] + endmodule ``` From 5f28ea70dc9b52dc60be46f6e397238856f88c0c Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Thu, 13 Mar 2025 18:24:06 +0300 Subject: [PATCH 2/8] optimize fuzzer using `constructFuzzState` --- src/komet/kasmer.py | 45 ++++++++++++++++++++++++---------------- src/komet/kast/manip.py | 31 +++++++++++++++++++++++++++ src/komet/kast/syntax.py | 4 ++++ 3 files changed, 62 insertions(+), 18 deletions(-) create mode 100644 src/komet/kast/manip.py diff --git a/src/komet/kasmer.py b/src/komet/kasmer.py index 3b86ada0..dd0c1184 100644 --- a/src/komet/kasmer.py +++ b/src/komet/kasmer.py @@ -26,11 +26,14 @@ from rich.console import Console from rich.progress import BarColumn, MofNCompleteColumn, Progress, TextColumn, TimeElapsedColumn +from komet.kast.manip import get_soroban_cell + from .kast.syntax import ( SC_VOID, STEPS_TERMINATOR, account_id, call_tx, + construct_fuzz_state, contract_id, deploy_contract, sc_bool, @@ -142,9 +145,7 @@ def kast_from_wasm(self, wasm: Path) -> KInner: return wasm2kast(open(wasm, 'rb')) @staticmethod - def deploy_test( - contract: KInner, child_contracts: tuple[KInner, ...], init: bool - ) -> tuple[KInner, dict[str, KInner]]: + def deploy_test(contract: KInner, child_contracts: tuple[KInner, ...], init: bool) -> KInner: """Takes a wasm soroban contract and its dependencies as kast terms and deploys them in a fresh configuration. Args: @@ -192,14 +193,11 @@ def call_init() -> tuple[KInner, ...]: kore_result = KoreParser(proc_res.stdout).pattern() kast_result = kore_to_kast(concrete_definition.kdefinition, kore_result) - conf, subst = split_config_from(kast_result) - - return conf, subst + return kast_result def run_test( self, - conf: KInner, - subst: dict[str, KInner], + init_conf: KInner, binding: ContractBinding, max_examples: int, task: FuzzTask, @@ -207,9 +205,7 @@ def run_test( """Given a configuration with a deployed test contract, fuzz over the tests for the supplied binding. Args: - conf: The template configuration. - subst: A substitution mapping such that 'Subst(subst).apply(conf)' gives the initial configuration with the - deployed contract. + init_conf: The initial configuration with the deployed contract. binding: The contract binding that specifies the test name and parameters. max_examples: The maximum number of fuzzing test cases to generate and execute. @@ -228,18 +224,30 @@ def make_kvar(i: int) -> KInner: def make_evar(i: int) -> EVar: return EVar(f"VarARG\'Unds\'{i}", SortApp('SortScVal')) - def make_steps(args: Iterable[KInner]) -> KInner: - return steps_of([set_exit_code(1), call_tx(from_acct, to_acct, name, args, result), set_exit_code(0)]) + def make_steps(args: Iterable[KInner], soroban_cell: KInner) -> KInner: + steps = steps_of([set_exit_code(1), call_tx(from_acct, to_acct, name, args, result), set_exit_code(0)]) + return steps_of([construct_fuzz_state(steps, soroban_cell)]) def scval_to_kore(val: SCValue) -> Pattern: return kast_to_kore(self.definition.kdefinition, val.to_kast(), KSort('ScVal')) - vars = [make_kvar(i) for i in range(len(binding.inputs))] - subst['PROGRAM_CELL'] = make_steps(vars) + def soroban_cell_strategy() -> SearchStrategy[Pattern]: + cell = get_soroban_cell(init_conf) + cell_kore = kast_to_kore(self.definition.kdefinition, cell, KSort('SorobanCell')) + return strategies.just(cell_kore) + + empty_config = self.definition.kdefinition.init_config(KSort('GeneratedTopCell')) + conf, subst = split_config_from(empty_config) + + arg_vars = [make_kvar(i) for i in range(len(binding.inputs))] + soroban_cell_var = KVariable('INITSTATE', KSort('SorobanCell')) + subst['PROGRAM_CELL'] = make_steps(arg_vars, soroban_cell_var) + template_config = Subst(subst).apply(conf) template_config_kore = kast_to_kore(self.definition.kdefinition, template_config, KSort('GeneratedTopCell')) template_subst = {make_evar(i): b.strategy().map(scval_to_kore) for i, b in enumerate(binding.inputs)} + template_subst[EVar('VarINITSTATE', SortApp('SortSorobanCell'))] = soroban_cell_strategy() fuzz( self.definition.path, @@ -314,14 +322,14 @@ def deploy_and_run( contract_kast = self.kast_from_wasm(contract_wasm) child_kasts = tuple(self.kast_from_wasm(c) for c in child_wasms) - conf, subst = self.deploy_test(contract_kast, child_kasts, has_init) + init_conf = self.deploy_test(contract_kast, child_kasts, has_init) failed: list[FuzzError] = [] with FuzzProgress(test_bindings, max_examples) as progress: for task in progress.fuzz_tasks: try: task.start() - self.run_test(conf, subst, task.binding, max_examples, task) + self.run_test(init_conf, task.binding, max_examples, task) task.end() except FuzzError as e: failed.append(e) @@ -365,7 +373,8 @@ def deploy_and_prove( contract_kast = self.kast_from_wasm(contract_wasm) child_kasts = tuple(self.kast_from_wasm(c) for c in child_wasms) - conf, subst = self.deploy_test(contract_kast, child_kasts, has_init) + init_conf = self.deploy_test(contract_kast, child_kasts, has_init) + conf, subst = split_config_from(init_conf) with FuzzProgress(test_bindings, 1) as progress: for task in progress.fuzz_tasks: diff --git a/src/komet/kast/manip.py b/src/komet/kast/manip.py new file mode 100644 index 00000000..1d828562 --- /dev/null +++ b/src/komet/kast/manip.py @@ -0,0 +1,31 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +from pyk.kast.inner import KApply, KLabel + +if TYPE_CHECKING: + from pyk.kast.inner import KInner + + +def get_soroban_cell(config: KInner) -> KInner: + match config: + case KApply( + KLabel(''), + ( + KApply( + KLabel(''), + ( + _, + soroban_cell, + _, + ), + ), + _, + ), + ): + match soroban_cell: + case KApply(KLabel(''), _): + return soroban_cell + + raise ValueError('Malformed config term') diff --git a/src/komet/kast/syntax.py b/src/komet/kast/syntax.py index 0b1cab38..fa0ead2d 100644 --- a/src/komet/kast/syntax.py +++ b/src/komet/kast/syntax.py @@ -108,3 +108,7 @@ def sc_map(m: dict[KInner, KInner] | Iterable[tuple[KInner, KInner]]) -> KInner: SC_VOID: Final = KApply('SCVal:Void', ()) + + +def construct_fuzz_state(steps: KInner, soroban_cell: KInner) -> KInner: + return KApply('constructFuzzState', [steps, soroban_cell]) From 1b53f73dfa06837b6a8e33f8dca6498e5bd46a46 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 13 Mar 2025 15:39:33 +0000 Subject: [PATCH 3/8] Set Version: 0.1.60 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 09d8256a..1ec9b0b6 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.59 +0.1.60 diff --git a/pyproject.toml b/pyproject.toml index 14c5fe7a..ac3be3ce 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.59" +version = "0.1.60" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", From 37b621b34941807d62b591d653f8f891c04b833e Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 14 Mar 2025 19:41:26 +0300 Subject: [PATCH 4/8] don't include the soroban cell to counterexamples --- src/komet/kasmer.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/komet/kasmer.py b/src/komet/kasmer.py index dd0c1184..6ac97efb 100644 --- a/src/komet/kasmer.py +++ b/src/komet/kasmer.py @@ -528,7 +528,9 @@ def handle_failure(self, args: Mapping[EVar, Pattern]) -> None: self.task.fail() sorted_keys = sorted(args.keys(), key=lambda k: k.name) - counterexample = tuple(self.definition.krun.kore_to_kast(args[k]) for k in sorted_keys) + counterexample = tuple( + self.definition.krun.kore_to_kast(args[k]) for k in sorted_keys if k.name != 'VarINITSTATE' + ) raise FuzzError(self.task.binding.name, counterexample) From 3b90a3704c2b7de8a9f03e0741aaad4264c90389 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 14 Mar 2025 16:42:12 +0000 Subject: [PATCH 5/8] Set Version: 0.1.61 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 1ec9b0b6..a2d633db 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.60 +0.1.61 diff --git a/pyproject.toml b/pyproject.toml index ac3be3ce..05368538 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.60" +version = "0.1.61" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", From 70debd8f635cac3c78fc0bea2e70bf0c452f9553 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 3 Apr 2025 12:44:37 +0000 Subject: [PATCH 6/8] Set Version: 0.1.62 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index a2d633db..fbde3d5a 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.61 +0.1.62 diff --git a/pyproject.toml b/pyproject.toml index cfd770de..90538967 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.61" +version = "0.1.62" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", From 14db77a67c31989068c14de18ec30cd2c56bc871 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 15 Apr 2025 13:41:30 +0000 Subject: [PATCH 7/8] Set Version: 0.1.64 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index abf5cfcd..9810a3b1 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.63 +0.1.64 diff --git a/pyproject.toml b/pyproject.toml index 978d1233..f28aaf47 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.63" +version = "0.1.64" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", From c84f173d0c81bbbb88da2f7f2756e520a790900d Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 21 Apr 2025 08:52:27 +0000 Subject: [PATCH 8/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. ",