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. ", diff --git a/src/komet/kasmer.py b/src/komet/kasmer.py index 3b86ada0..6ac97efb 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: @@ -519,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) 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]) 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 ```