From 1c367ab25ba6f47e7345d59fbc7eb25961b514ea Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 16 Jan 2026 19:18:33 +0300 Subject: [PATCH 01/10] Fix argument type list parsing --- src/skribe/contract.py | 27 +++++++++++++++++++++++++-- src/skribe/skribe.py | 4 ++-- 2 files changed, 27 insertions(+), 4 deletions(-) diff --git a/src/skribe/contract.py b/src/skribe/contract.py index 721855f..47cd189 100644 --- a/src/skribe/contract.py +++ b/src/skribe/contract.py @@ -6,6 +6,7 @@ from pathlib import Path from typing import TYPE_CHECKING, Any, TypeAlias +from eth_abi.grammar import TupleType, parse from eth_abi.tools._strategies import get_abi_strategy from hypothesis import strategies from kontrol.solc_to_k import Contract as EVMContract @@ -119,8 +120,30 @@ def is_foundry_test(ctr: EVMContract) -> bool: return False +def get_arg_types(m: Method) -> tuple[str, ...]: + """ + Return the argument type strings of a method. + + This function exists because `Method.arg_types` flattens tuple arguments, + into their component types. That flattening loses information about the + original ABI shape (for example, whether an argument was a tuple or an + array of tuples). + """ + + sig = m.signature + arg_types_from_sig = sig[sig.index('(') :] + + if arg_types_from_sig == '()': + return () + else: + parsed_arg_types = parse(arg_types_from_sig) + assert isinstance(parsed_arg_types, TupleType) + return tuple(c.to_type_str() for c in parsed_arg_types.components) + + def argument_strategy(m: Method) -> SearchStrategy[bytes]: - input_strategies = (get_abi_strategy(arg) for arg in m.arg_types) + arg_types = get_arg_types(m) + input_strategies = (get_abi_strategy(arg) for arg in arg_types) tuple_strategy = strategies.tuples(*input_strategies) - encoder = partial(call_data, m.name, m.arg_types) + encoder = partial(call_data, m.name, arg_types) return tuple_strategy.map(encoder) diff --git a/src/skribe/skribe.py b/src/skribe/skribe.py index f09079e..acd045d 100644 --- a/src/skribe/skribe.py +++ b/src/skribe/skribe.py @@ -21,7 +21,7 @@ from pyk.utils import run_process from pykwasm.wasm2kast import wasm2kast -from skribe.contract import StylusContract, argument_strategy, is_foundry_test, setup_method +from skribe.contract import StylusContract, argument_strategy, get_arg_types, is_foundry_test, setup_method from .kast.syntax import ( call_stylus, @@ -300,7 +300,7 @@ def handle_failure(self, args: Mapping[EVar, Pattern]) -> None: calldata_kast = self.definition.krun.kore_to_kast(args[CALLDATA_EVAR]) assert isinstance(calldata_kast, KToken) calldata = pretty_bytes(calldata_kast) - decoded = decode(self.task.binding.arg_types, calldata[4:]) + decoded = decode(get_arg_types(self.task.binding), calldata[4:]) description = f'{self.task.binding.contract_name}.{self.task.binding.name}' raise FuzzError(description, decoded) From 7f5a9d97211cc942c218f57dbd97b6e8cdf9420a Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 16 Jan 2026 19:19:08 +0300 Subject: [PATCH 02/10] increase fuzzing deadline --- src/skribe/skribe.py | 1 + 1 file changed, 1 insertion(+) diff --git a/src/skribe/skribe.py b/src/skribe/skribe.py index acd045d..f8cb542 100644 --- a/src/skribe/skribe.py +++ b/src/skribe/skribe.py @@ -204,6 +204,7 @@ def calldata_to_kore(data: bytes) -> Pattern: max_examples=max_examples, handler=KometFuzzHandler(self.definition, task), subst_func=subst_on_k_cell, + deadline=20000, ) def select_tests(self, contract: ArbitrumContract, id: str | None) -> list[Method]: From 5b9af0aabbff8d343884ac2f0b30fb72231bd399 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 16 Jan 2026 19:37:19 +0300 Subject: [PATCH 03/10] Increase Python recursion depth limit --- src/skribe/utils.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/skribe/utils.py b/src/skribe/utils.py index 6b0b2e1..db6b3d5 100644 --- a/src/skribe/utils.py +++ b/src/skribe/utils.py @@ -33,7 +33,7 @@ from pyk.kore.syntax import EVar, Pattern from pyk.ktool.kompile import KompileBackend -RECURSION_LIMIT: Final = 8000 +RECURSION_LIMIT: Final = 16000 EXIT_CODE_PYK_HOOK: Final = 2 From 707aec9c2e9858a19cc91e25ce1db9abf61db4fe Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 16 Jan 2026 19:37:40 +0300 Subject: [PATCH 04/10] Ignore `#hasValidInitCode` check --- src/skribe/kdist/stylus-semantics/skribe.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/skribe/kdist/stylus-semantics/skribe.md b/src/skribe/kdist/stylus-semantics/skribe.md index 9c09d0d..ca5d2f4 100644 --- a/src/skribe/kdist/stylus-semantics/skribe.md +++ b/src/skribe/kdist/stylus-semantics/skribe.md @@ -128,6 +128,12 @@ module SKRIBE ``` +### Patches for Skribe tests + +```k + rule #hasValidInitCode(_MEMWIDTH, _SCHED) => true [priority(10)] +``` + ### Cheatcode calling mechanism for Skribe ```k From 2aab0e8a3c17f7cd8bc973f89f561dfe739c5dd5 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 16 Jan 2026 19:44:25 +0300 Subject: [PATCH 05/10] implement host functions: `msg_sender`, `native_keccak256` --- src/skribe/kdist/stylus-semantics/hostfuns.md | 47 +++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/src/skribe/kdist/stylus-semantics/hostfuns.md b/src/skribe/kdist/stylus-semantics/hostfuns.md index 9beeecc..d0699c0 100644 --- a/src/skribe/kdist/stylus-semantics/hostfuns.md +++ b/src/skribe/kdist/stylus-semantics/hostfuns.md @@ -33,6 +33,23 @@ handle reentrancy explicitly. #endWasm ... ``` +## msg_sender + +Gets the address of the calling account. + +```k + rule [hostCall-msg-sender]: + hostCall ( "vm_hooks" , "msg_sender" , [ i32 .ValTypes ] -> [ .ValTypes ] ) + => #memStore( DEST_PTR , Int2Bytes(20, ADDR, BE) ) + ... + + + 0 |-> < i32 > DEST_PTR + + ADDR + #endWasm ... +``` + ## msg_value Get the ETH value in wei sent to the program. @@ -51,6 +68,36 @@ Get the ETH value in wei sent to the program. ``` +## native_keccak256 + +Computes the `keccak256` hash of the given data. + +```k + rule [hostCall-native-keccak256]: + hostCall ( "vm_hooks" , "native_keccak256" , [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ] ) + => pushStack(RESULT_OFFSET) + ~> #memLoad(DATA_OFFSET, DATA_LEN) + ~> hostCallAux("vm_hooks", "native_keccak256") + ... + + + 0 |-> < i32 > DATA_OFFSET + 1 |-> < i32 > DATA_LEN + 2 |-> < i32 > RESULT_OFFSET + + CALL_VALUE + #endWasm ... + + rule [hostCallAux-native-keccak256]: + hostCallAux ( "vm_hooks" , "native_keccak256" ) + => #memStore(DEST_OFFSET, Int2Bytes(32, keccak(DATA), BE)) + ... + + DATA:Bytes : DEST_OFFSET:Int : S => S + #endWasm ... + +``` + ## read_args Reads the call data into Wasm memory. From b120c1cbaacaa55b2de87b1c6ea85c9e66838c2b Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Mon, 19 Jan 2026 15:08:36 +0300 Subject: [PATCH 06/10] implement `transient_store_bytes32`/`transient_load_bytes32` --- src/skribe/kdist/stylus-semantics/hostfuns.md | 69 +++++++++++++++++++ 1 file changed, 69 insertions(+) diff --git a/src/skribe/kdist/stylus-semantics/hostfuns.md b/src/skribe/kdist/stylus-semantics/hostfuns.md index d0699c0..d5efdaf 100644 --- a/src/skribe/kdist/stylus-semantics/hostfuns.md +++ b/src/skribe/kdist/stylus-semantics/hostfuns.md @@ -197,6 +197,75 @@ Equivalent to the [`SLOAD`](https://www.evm.codes/#54) opcode in EVM. #endWasm ... ``` +## transient_load_bytes32 + +Reads a 32-byte value from transient storage. +Equivalent to the `TLOAD` opcode in EVM. + +```k + rule [hostCall-transient-load-bytes32]: + hostCall ( "vm_hooks" , "transient_load_bytes32" , [ i32 i32 .ValTypes ] -> [ .ValTypes ] ) + => pushStack(DEST_OFFSET) + ~> #memLoad( KEY_OFFSET , 32 ) + ~> hostCallAux( "vm_hooks" , "transient_load_bytes32" ) + ... + + + 0 |-> < i32 > KEY_OFFSET + 1 |-> < i32 > DEST_OFFSET + + #endWasm ... + + rule [hostCallAux-transient-load-bytes32]: + hostCallAux ( "vm_hooks" , "transient_load_bytes32" ) + => #memStore( + DEST_OFFSET, + Int2Bytes(32, #lookup(TSTORAGE, #asWord(KEY)), BE) + ) + ... + + KEY:Bytes : DEST_OFFSET:Int : S => S + ACCT + + ACCT + TSTORAGE + ... + + #endWasm ... +``` + +## transient_store_bytes32 + +Writes a 32-byte value to transient storage. +Equivalent to the `TSTORE` opcode in EVM. + +```k + rule [hostCall-transient-store-bytes32]: + hostCall ( "vm_hooks" , "transient_store_bytes32" , [ i32 i32 .ValTypes ] -> [ .ValTypes ] ) + => #memLoad( VAL_OFFSET , 32 ) + ~> #memLoad( KEY_OFFSET , 32 ) + ~> hostCallAux( "vm_hooks" , "transient_store_bytes32" ) + ... + + + 0 |-> < i32 > KEY_OFFSET + 1 |-> < i32 > VAL_OFFSET + + #endWasm ... + + rule [hostCallAux-transient-store-bytes32]: + hostCallAux ( "vm_hooks" , "transient_store_bytes32" ) => .K ... + KEY:Bytes : VAL:Bytes : S => S + ACCT + + ACCT + STORAGE => STORAGE [ #asWord(KEY) <- #asWord(VAL) ] + ... + + #endWasm ... +``` + + ## write_result ```k From 91c8abfa275ce2659fd26bae2fd57a46631ce522 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Mon, 19 Jan 2026 15:08:46 +0300 Subject: [PATCH 07/10] implement `exit_early` --- src/skribe/kdist/stylus-semantics/hostfuns.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/skribe/kdist/stylus-semantics/hostfuns.md b/src/skribe/kdist/stylus-semantics/hostfuns.md index d5efdaf..2f0a0b5 100644 --- a/src/skribe/kdist/stylus-semantics/hostfuns.md +++ b/src/skribe/kdist/stylus-semantics/hostfuns.md @@ -266,6 +266,21 @@ Equivalent to the `TSTORE` opcode in EVM. ``` +## exit_early + +This is just a tracing (no-op) function. +```k + rule [hostCall-exit-early]: + hostCall ( "vm_hooks" , "exit_early" , [ i32 .ValTypes ] -> [ .ValTypes ] ) + => .K ... + + + 0 |-> < i32 > _EC + + #endWasm ... + +``` + ## write_result ```k From 8b43ac0910bb336427f8f65518e8c4ba66a52e6f Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Tue, 20 Jan 2026 12:46:26 +0300 Subject: [PATCH 08/10] implement `math_mul_mod`/`math_div`/`math_mod`/`math_add_mod` --- src/skribe/kdist/stylus-semantics/hostfuns.md | 174 +++++++++++++++++- 1 file changed, 173 insertions(+), 1 deletion(-) diff --git a/src/skribe/kdist/stylus-semantics/hostfuns.md b/src/skribe/kdist/stylus-semantics/hostfuns.md index 2f0a0b5..ef60bbc 100644 --- a/src/skribe/kdist/stylus-semantics/hostfuns.md +++ b/src/skribe/kdist/stylus-semantics/hostfuns.md @@ -11,6 +11,122 @@ module HOSTFUNS syntax InternalInstr ::= hostCallAux(String, String) [symbol(hostCallAux)] + syntax InternalInstr ::= #memLoadWord( Int ) + // --------------------------------------------- + rule #memLoadWord(PTR) => #memLoad(PTR, 32) ~> #asWordFromStack ... + +``` + +## math_mul_mod + +```k + rule [hostCall-math-mul-mod]: + hostCall ( "vm_hooks" , "math_mul_mod" , [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ] ) + => pushStack(VALUE_PTR) + ~> #memLoadWord(MODULUS_PTR) + ~> #memLoadWord(MULTIPLIER_PTR) + ~> #memLoadWord(VALUE_PTR) + ~> hostCallAux ( "vm_hooks" , "math_mul_mod" ) + ... + + + 0 |-> < i32 > VALUE_PTR + 1 |-> < i32 > MULTIPLIER_PTR + 2 |-> < i32 > MODULUS_PTR + + #endWasm ... + + rule [hostCallAux-math-mul-mod]: + hostCallAux ( "vm_hooks" , "math_mul_mod" ) + => #memStore(RES_PTR, Int2Bytes(32, (VALUE *Int MULTIPLIER) %Word MODULUS, BE)) + ... + + VALUE : MULTIPLIER : MODULUS : RES_PTR : S => S + #endWasm ... + +``` + +## math_div + +```k + rule [hostCall-math-div]: + hostCall ( "vm_hooks" , "math_div" , [ i32 i32 .ValTypes ] -> [ .ValTypes ] ) + => pushStack(A_PTR) + ~> #memLoadWord(B_PTR) + ~> #memLoadWord(A_PTR) + ~> hostCallAux ( "vm_hooks" , "math_div" ) + ... + + + 0 |-> < i32 > A_PTR + 1 |-> < i32 > B_PTR + + #endWasm ... + + rule [hostCallAux-math-div]: + hostCallAux ( "vm_hooks" , "math_div" ) + => #memStore(RES_PTR, Int2Bytes(32, A /Word B, BE)) + ... + + A : B : RES_PTR : S => S + #endWasm ... + +``` + +## math_mod + +```k + rule [hostCall-math-mod]: + hostCall ( "vm_hooks" , "math_mod" , [ i32 i32 .ValTypes ] -> [ .ValTypes ] ) + => pushStack(A_PTR) + ~> #memLoadWord(B_PTR) + ~> #memLoadWord(A_PTR) + ~> hostCallAux ( "vm_hooks" , "math_mod" ) + ... + + + 0 |-> < i32 > A_PTR + 1 |-> < i32 > B_PTR + + #endWasm ... + + rule [hostCallAux-math-mod]: + hostCallAux ( "vm_hooks" , "math_mod" ) + => #memStore(RES_PTR, Int2Bytes(32, A %Word B, BE)) + ... + + A : B : RES_PTR : S => S + #endWasm ... + +``` + +## math_add_mod + +```k + rule [hostCall-math-add-mod]: + hostCall ( "vm_hooks" , "math_add_mod" , [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ] ) + => pushStack(W0_PTR) + ~> #memLoadWord(W2_PTR) + ~> #memLoadWord(W1_PTR) + ~> #memLoadWord(W0_PTR) + ~> hostCallAux ( "vm_hooks" , "math_add_mod" ) + ... + + + 0 |-> < i32 > W0_PTR + 1 |-> < i32 > W1_PTR + 2 |-> < i32 > W2_PTR + + #endWasm ... + + rule [hostCallAux-math-add-mod]: + hostCallAux ( "vm_hooks" , "math_add_mod" ) + => #memStore(RES_PTR, Int2Bytes(32, (W0 +Int W1) %Word W2, BE)) + ... + + W0 : W1 : W2 : RES_PTR : S => S + #endWasm ... + ``` ## msg_reentrant @@ -475,6 +591,50 @@ The semantics are equivalent to the `BALANCE` opcode. ``` +## account_codehash + +```k + rule [hostCall-account-codehash]: + hostCall ( "vm_hooks" , "account_codehash" , [ i32 i32 .ValTypes ] -> [ .ValTypes ] ) + => pushStack(DEST_PTR) + ~> #memLoad(ADDR_PTR, 20) + ~> #asWordFromStack + ~> hostCallAux ( "vm_hooks" , "account_codehash" ) + ... + + + 0 |-> < i32 > ADDR_PTR + 1 |-> < i32 > DEST_PTR + + #endWasm ... + + rule [hostCallAux-account-codehash]: + hostCallAux ( "vm_hooks" , "account_codehash" ) + => #memStore( DEST_PTR , Int2Bytes(32, keccak(CODE), BE) ) + ~> #waitCommands + ... + + ACCT : DEST_PTR:Int : S => S + + ACCT + CODE + ... + + (.K => #accessAccounts ACCT) ~> #endWasm ... + + + rule [hostCallAux-account-codehash-ow]: + hostCallAux ( "vm_hooks" , "account_codehash" ) + => #memStore( DEST_PTR , Int2Bytes(32, 0, BE) ) + ~> #waitCommands + ... + + ACCT : DEST_PTR:Int : S => S + (.K => #accessAccounts ACCT) ~> #endWasm ... + [owise] +``` + + ## block_number ```k @@ -484,7 +644,7 @@ The semantics are equivalent to the `BALANCE` opcode. ... .Map - NUM + NUM #endWasm ... ``` @@ -573,6 +733,18 @@ The semantics are equivalent to the `BALANCE` opcode. ``` +## emit_log + +TODO: implement logs + +```k + rule [hostCall-emit-log]: + hostCall ( "vm_hooks" , "emit_log" , [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ] ) + => .K ... + + #endWasm ... +``` + ```k endmodule ``` \ No newline at end of file From fde9cd25b425c504a645cb41a89b7230ee7d6f7b Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Thu, 22 Jan 2026 13:04:42 +0300 Subject: [PATCH 09/10] increase recursion limit further --- src/skribe/utils.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/skribe/utils.py b/src/skribe/utils.py index db6b3d5..b08fecc 100644 --- a/src/skribe/utils.py +++ b/src/skribe/utils.py @@ -33,7 +33,7 @@ from pyk.kore.syntax import EVar, Pattern from pyk.ktool.kompile import KompileBackend -RECURSION_LIMIT: Final = 16000 +RECURSION_LIMIT: Final = 20000 EXIT_CODE_PYK_HOOK: Final = 2 From c41dcab5e40538ffc916c0ecdc130b3849410683 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 10 Feb 2026 13:52:44 +0000 Subject: [PATCH 10/10] Set Version: 0.1.24 --- package/version | 2 +- pyproject.toml | 2 +- uv.lock | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 001d752..5a48b6b 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.23 +0.1.24 diff --git a/pyproject.toml b/pyproject.toml index 524a7a7..da1c09d 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "skribe" -version = "0.1.23" +version = "0.1.24" description = "Property testing for Stylus smart contracts" readme = "README.md" requires-python = "~=3.10" diff --git a/uv.lock b/uv.lock index bd21405..cadd791 100644 --- a/uv.lock +++ b/uv.lock @@ -1815,7 +1815,7 @@ wheels = [ [[package]] name = "skribe" -version = "0.1.23" +version = "0.1.24" source = { editable = "." } dependencies = [ { name = "kontrol" },