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/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/kdist/stylus-semantics/hostfuns.md b/src/skribe/kdist/stylus-semantics/hostfuns.md index 9beeecc..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 @@ -33,6 +149,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 +184,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. @@ -150,6 +313,90 @@ 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 ... +``` + + +## 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 @@ -344,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 @@ -353,7 +644,7 @@ The semantics are equivalent to the `BALANCE` opcode. ... .Map - NUM + NUM #endWasm ... ``` @@ -442,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 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 diff --git a/src/skribe/skribe.py b/src/skribe/skribe.py index f09079e..f8cb542 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, @@ -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]: @@ -300,7 +301,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) diff --git a/src/skribe/utils.py b/src/skribe/utils.py index 6b0b2e1..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 = 8000 +RECURSION_LIMIT: Final = 20000 EXIT_CODE_PYK_HOOK: Final = 2 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" },